Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover
theory CSP_Prover = CSP_tactic: (*-------------------------------------------*
| CSP-Prover |
| December 2004 |
| February 2005 (modified) |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_Prover = CSP_tactic:
(*****************************************************************
1. CSP-Prover
2.
3.
4.
*****************************************************************)
(*-------------------------------------------------------*
| |
| default LET _ IN _ |
| |
*-------------------------------------------------------*)
syntax
"_LetinUFP" :: "('n,'a) procDF => ('n,'a) proc => ('n,'a) procRC"
("//(2LET /_ )/(2IN /_)/" [53,53] 53)
translations
"LET df IN P" == "LET:Ufp df IN P" (* default LET _ IN _ *)
(*-------------------------------------------------------*
| |
| adding ... to automatic simplification rules |
| |
*-------------------------------------------------------*)
(* automatically unfolded functions *)
declare Ext_choice_step_def [simp]
declare Parallel_step_def [simp]
declare Hiding_step_def [simp]
declare Renaming_step_def [simp]
declare Seq_compo_step_def [simp]
(*-------------------------------------------------------------*
| |
| Users may be sometimes required to apply "Int_prefix_def" |
| for unfoling "! x:X -> P". Do you like the following ? |
| |
| declare Int_pre_choice_def [simp] |
| |
| Users may be sometimes required to apply "Send_prefix_def" |
| for unfoling "a ! x: -> P". Do you like the following ? |
| |
| declare Send_prefix_def [simp] |
| |
| Users may be sometimes required to apply "Rec_prefix_def" |
| for unfoling "a ? x:X -> P". Do you like the following ? |
| |
| declare Rec_prefix_def [simp] |
| |
*-------------------------------------------------------------*)
(* NO *)
(*----------------------------------------------------------------------*
| |
| To unfold (resp. fold) syntactic-sugar for Ext_ and Int_pre_choices |
| choices, use "unfold csp_ss_def" (resp. "fold csp_ss_def"). |
| |
*----------------------------------------------------------------------*)
(*---------------------------------------------------------------------*
| Nondet_send_prefix_def : non-deterministic sending |
| Rep_int_choice_fun_def : Replicated internal choice with a function |
*---------------------------------------------------------------------*)
(* "inj_on_def" is needed for resolving (inv f) in R_Prefix_def *)
declare inj_on_def [simp]
(*------------------------------------*
| |
| laws automatically applied |
| |
*------------------------------------*)
(* intro! intro? are automatically applied by "rule". *)
(* intro! is automatically applied by "rules" and "auto". *)
(* CSP_SF_law_commut *)
declare csp_commut [simp]
(* CSP_SF_law_ref *)
declare csp_Int_choice_right [intro!]
declare csp_Rep_int_choice_right [intro!]
(*
declare csp_Int_choice_left1 [intro?]
declare csp_Int_choice_left2 [intro?]
declare csp_Int_choice_left3 [intro?]
declare csp_Rep_int_choice_left [intro?]
declare csp_Rep_int_choice_left_x [intro?]
declare csp_decompo_subset [intro?]
declare csp_Ext_choice_right [intro?]
declare csp_Int_choice_Ext_choice [intro?]
*)
(* CSP_SF_law_SKIP *)
declare csp_SKIP [simp]
lemmas csp_SKIP_sym [simp]
= csp_SKIP[THEN csp_sym]
(*
declare csp_SKIP_rw [simp]
*)
(* CSP_SF_law_decompo *)
declare csp_rm_head [intro!]
declare csp_decompo [simp]
(*
declare csp_free_decompo [intro!]
declare csp_decompo [intro!]
declare csp_free_decompo_left [intro!]
declare csp_free_decompo_right [intro!]
declare csp_decompo_left [intro!]
declare csp_decompo_right [intro!]
declare csp_free_decompo_flag_left [intro!]
declare csp_free_decompo_flag_right [intro!]
declare csp_decompo_flag_left [intro!]
declare csp_decompo_flag_right [intro!]
*)
(* CSP_SF_law_dist *)
declare csp_dist [simp]
lemmas csp_dist_sym [simp]
= csp_dist[THEN csp_sym]
declare csp_Rep_dist [simp]
lemmas csp_Rep_dist_sym [simp]
= csp_Rep_dist[THEN csp_sym]
(*
declare csp_dist_rw [simp]
declare csp_dist_rw_left [simp]
declare csp_dist_rw_right [simp]
declare csp_Rep_dist_rw [simp]
declare csp_Rep_dist_rw_left [simp]
declare csp_Rep_dist_rw_right [simp]
*)
(* CSP_SF_law_fp_cms *)
declare csp_check [intro!]
lemmas csp_fp_induct = csp_fp_induct_cms
declare csp_unwind [simp]
lemmas csp_unwind_sym [simp]
= csp_unwind[THEN csp_sym]
(*
declare csp_unwind_rw [simp]
declare csp_fp_induct_cms [intro!]
*)
(* CSP_SF_law_fp_cpo *)
declare csp_check_cpo [intro!]
declare csp_unwind_cpo [simp]
lemmas csp_unwind_cpo_sym [simp]
= csp_unwind_cpo[THEN csp_sym]
(* CSP_SF_law_step *)
declare csp_step [simp]
lemmas csp_step_sym [simp]
= csp_step[THEN csp_sym]
(*
declare csp_step_rw [simp]
declare csp_step_rw_left [simp]
declare csp_step_rw_right [simp]
declare light_csp_step_rw [simp]
declare light_csp_step_rw_left [simp]
declare light_csp_step_rw_right [simp]
*)
(* CSP_SF_law_etc *)
declare csp_Conditional [simp]
declare csp_simp [simp]
lemmas csp_simp_sym [simp]
= csp_simp[THEN csp_sym]
(*
declare csp_Conditional_split [simp]
declare csp_Conditional_split_rw [simp]
declare csp_Conditional_rw [simp]
declare csp_reflex [intro!]
declare csp_reflex_ex [intro!]
declare csp_simp [simp]
lemmas csp_simp_sym [simp]
= csp_simp[THEN csp_sym]
declare csp_eq_ref [intro?]
declare csp_ref_eq [intro?]
declare csp_trans [intro?]
declare csp_sym [intro!]
declare csp_symE [elim!]
*)
(*
declare csp_Int_simp_rw [simp]
declare csp_Ext_simp_rw [simp]
declare csp_Mix_simp_rw [simp]
declare csp_simp_rw [simp]
declare csp_Timeout_right [intro!]
*)
(***************************************************************
Domain theory
***************************************************************)
declare memT_IntT [simp]
declare memT_UnT [simp]
declare memF_IntF [simp]
declare memF_UnF [simp]
end
lemmas csp_SKIP_sym:
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN SKIP ;; P_1
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN P_1 ;; SKIP
LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (SKIP |[X_1]| Qf_1 x) =F LET:fp_1 df_1 IN SKIP |[X_1]| ? :Y_1 -> Qf_1
LET:fp_1 df_1 IN ? x:(Y_1 - X_1) -> (Pf_1 x |[X_1]| SKIP) =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| SKIP
LET:fp_1 df_1 IN SKIP =F LET:fp_1 df_1 IN SKIP |[X_1]| SKIP
LET:fp_1 df_1 IN SKIP =F LET:fp_1 df_1 IN SKIP -- X_1
LET:fp_1 df_1 IN SKIP =F LET:fp_1 df_1 IN SKIP [[r_1]]
lemmas csp_dist_sym:
LET:fp_1 df_1 IN P1_1 [+] Q_1 |~| P2_1 [+] Q_1 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1
LET:fp_1 df_1 IN P_1 [+] Q1_1 |~| P_1 [+] Q2_1 =F LET:fp_1 df_1 IN P_1 [+] (Q1_1 |~| Q2_1)
LET:fp_1 df_1 IN P1_1 |[X_1]| Q_1 |~| P2_1 |[X_1]| Q_1 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) |[X_1]| Q_1
LET:fp_1 df_1 IN P_1 |[X_1]| Q1_1 |~| P_1 |[X_1]| Q2_1 =F LET:fp_1 df_1 IN P_1 |[X_1]| (Q1_1 |~| Q2_1)
LET:fp_1 df_1 IN P1_1 -- X_1 |~| P2_1 -- X_1 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) -- X_1
LET:fp_1 df_1 IN P1_1 [[r_1]] |~| P2_1 [[r_1]] =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) [[r_1]]
LET:fp_1 df_1 IN P1_1 ;; Q_1 |~| P2_1 ;; Q_1 =F LET:fp_1 df_1 IN (P1_1 |~| P2_1) ;; Q_1
lemmas csp_Rep_dist_sym:
X_1 ≠ {} ==> LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [+] Q_1 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [+] Q_1
X_1 ≠ {} ==> LET:fp_1 df_1 IN ! x:X_1 .. P_1 [+] Qf_1 x =F LET:fp_1 df_1 IN P_1 [+] (! :X_1 .. Qf_1)
Y_1 ≠ {} ==> LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x |[X_1]| Q_1 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) |[X_1]| Q_1
Y_1 ≠ {} ==> LET:fp_1 df_1 IN ! x:Y_1 .. P_1 |[X_1]| Qf_1 x =F LET:fp_1 df_1 IN P_1 |[X_1]| (! :Y_1 .. Qf_1)
LET:fp_1 df_1 IN ! x:Y_1 .. Pf_1 x -- X_1 =F LET:fp_1 df_1 IN (! :Y_1 .. Pf_1) -- X_1
LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x [[r_1]] =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) [[r_1]]
LET:fp_1 df_1 IN ! x:X_1 .. Pf_1 x ;; Q_1 =F LET:fp_1 df_1 IN (! :X_1 .. Pf_1) ;; Q_1
lemmas csp_fp_induct:
[| !!C. nohide (df1 C); !!C. guard (df1 C); !!C. nohide (df2 C); !!C. guard (df2 C); LET df2 IN Rewrite P1 By f12 =F LET df2 IN P2; !!C. LET df2 IN Rewrite (df1 C) By f12 =F LET df2 IN f12 C |] ==> LET:fp df1 IN P1 =F LET:fp df2 IN P2
[| !!C. nohide (df1 C); !!C. guard (df1 C); !!C. nohide (df2 C); !!C. guard (df2 C); LET df2 IN Rewrite P1 By f12 <=F LET df2 IN P2; !!C. LET df2 IN Rewrite (df1 C) By f12 <=F LET df2 IN f12 C |] ==> LET:fp df1 IN P1 <=F LET:fp df2 IN P2
lemmas csp_unwind_sym:
[| !!C. nohide (df_1 C); !!C. guard (df_1 C) |] ==> LET:fp_1 df_1 IN df_1 C_1 =F LET:fp_1 df_1 IN <C_1>
lemmas csp_unwind_cpo_sym:
LET:Lfp df_1 IN df_1 C_1 =F LET:Lfp df_1 IN <C_1>
lemmas csp_step_sym:
LET:fp_1 df_1 IN ? x:{} -> DIV =F LET:fp_1 df_1 IN STOP
LET:fp_1 df_1 IN ? x:{a_1} -> P_1 =F LET:fp_1 df_1 IN a_1 -> P_1
LET:fp_1 df_1 IN Ext_choice_step X_1 Y_1 Pf_1 Qf_1 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 [+] ? :Y_1 -> Qf_1
LET:fp_1 df_1 IN Parallel_step X_1 Y_1 Z_1 Pf_1 Qf_1 =F LET:fp_1 df_1 IN ? :Y_1 -> Pf_1 |[X_1]| ? :Z_1 -> Qf_1
LET:fp_1 df_1 IN Hiding_step X_1 Y_1 Pf_1 =F LET:fp_1 df_1 IN (? :Y_1 -> Pf_1) -- X_1
LET:fp_1 df_1 IN Renaming_step r_1 X_1 Pf_1 =F LET:fp_1 df_1 IN (? :X_1 -> Pf_1) [[r_1]]
LET:fp_1 df_1 IN Seq_compo_step X_1 Pf_1 Q_1 =F LET:fp_1 df_1 IN ? :X_1 -> Pf_1 ;; Q_1
lemmas csp_simp_sym:
LET:fp_1 df_1 IN ! x:{} .. DIV =F LET:fp_1 df_1 IN DIV
LET:fp_1 df_1 IN Pf_1 a_1 =F LET:fp_1 df_1 IN ! :{a_1} .. Pf_1
LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 ==> LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN P_1 |~| Q_1
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN Q_1 [+] P_1
LET:fp_1 df_1 IN Q_1 =F LET:fp_1 df_1 IN STOP ==> LET:fp_1 df_1 IN P_1 =F LET:fp_1 df_1 IN P_1 [+] Q_1
[|
LET:fp_1 df_1 IN P1_1 =F
LET:fp_1 df_1 IN STOP;
LET:fp_1 df_1 IN P2_1 =F
LET:fp_1 df_1 IN STOP |]
==>
LET:fp_1 df_1 IN Q_1 =F
LET:fp_1 df_1 IN (P1_1 |~| P2_1) [+] Q_1