Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| February 2005 (modified) |
| June 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T = CSP_T_tactic:
(*-------------------------------------------------------*
| |
| adding ... to automatically check Procfun |
| |
*-------------------------------------------------------*)
declare Procfun_def [intro!]
declare ProcX_def [simp]
declare gSKIPX_def [simp]
declare gProcX_def [simp]
declare nohideX_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_prefix_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_T_law_basic *)
declare cspT_commut [simp]
(* CSP_T_law_ref *)
declare cspT_Int_choice_right [intro!]
declare cspT_Rep_int_choice_right [intro!]
(* CSP_T_law_SKIP *)
declare cspT_SKIP_DIV_resolve [simp]
lemmas cspT_SKIP_DIV_resolve_sym [simp]
= cspT_SKIP_DIV_resolve[THEN cspT_sym]
(* CSP_T_law_decompo *)
declare cspT_rm_head [intro!]
declare cspT_decompo [simp]
(* CSP_T_law_dist *)
declare cspT_all_dist [simp]
lemmas cspT_all_dist_sym [simp]
= cspT_all_dist[THEN cspT_sym]
declare cspT_unwind [simp]
lemmas cspT_unwind_sym [simp]
= cspT_unwind[THEN cspT_sym]
(* CSP_T_law_step *)
declare cspT_step [simp]
lemmas cspT_step_sym [simp]
= cspT_step[THEN cspT_sym]
(* CSP_T_law_etc *)
declare cspT_choice_IF [simp]
end
lemmas cspT_SKIP_DIV_resolve_sym:
? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =T SKIP |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =T ? :Y1 -> Pf1 |[X1]| SKIP
? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =T DIV |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| DIV) [+] DIV =T ? :Y1 -> Pf1 |[X1]| DIV
SKIP =T SKIP [+] DIV
SKIP =T DIV [+] SKIP
DIV =T SKIP |[X1]| DIV
DIV =T DIV |[X1]| SKIP
SKIP =T SKIP |[X1]| SKIP
DIV =T DIV |[X1]| DIV
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =T SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =T (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =T SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)
P1 |[X1]| DIV =T (P1 [+] SKIP) |[X1]| DIV
DIV |[X1]| P1 =T DIV |[X1]| (P1 [+] SKIP)
P1 |[X1]| DIV =T (P1 [+] DIV) |[X1]| DIV
DIV |[X1]| P1 =T DIV |[X1]| (P1 [+] DIV)
SKIP =T SKIP -- X1
DIV =T DIV -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 =T (? :Y1 -> Pf1 [+] DIV) -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 =T (? :Y1 -> Pf1 [+] SKIP) -- X1
SKIP =T SKIP [[r1]]
DIV =T DIV [[r1]]
P2.0 =T SKIP ;; P2.0
P2.0 =T P2.0 ;; SKIP
DIV =T DIV ;; P1
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T (? :X1 -> Pf1 [> SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [> DIV =T (? :X1 -> Pf1 [> DIV) ;; Q1
SKIP =T SKIP |. Suc n1
DIV =T DIV |. n1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP) =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> (DIV |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| DIV) =T (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| DIV) =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> (DIV |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP) =T (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> SKIP |[X1]| ? :Z1 -> Qf1 =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| ? :Z1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x [> ? :Y1 -> Pf1 |[X1]| SKIP =T ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> DIV |[X1]| ? :Z1 -> Qf1 =T (? :Y1 -> Pf1 [+] DIV) |[X1]| ? :Z1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x [> ? :Y1 -> Pf1 |[X1]| DIV =T ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T (? :X1 -> Pf1 [+] SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [+] DIV =T (? :X1 -> Pf1 [+] DIV) ;; Q1
lemmas cspT_SKIP_DIV_resolve_sym:
? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =T SKIP |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =T ? :Y1 -> Pf1 |[X1]| SKIP
? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =T DIV |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| DIV) [+] DIV =T ? :Y1 -> Pf1 |[X1]| DIV
SKIP =T SKIP [+] DIV
SKIP =T DIV [+] SKIP
DIV =T SKIP |[X1]| DIV
DIV =T DIV |[X1]| SKIP
SKIP =T SKIP |[X1]| SKIP
DIV =T DIV |[X1]| DIV
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =T SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =T (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =T SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)
P1 |[X1]| DIV =T (P1 [+] SKIP) |[X1]| DIV
DIV |[X1]| P1 =T DIV |[X1]| (P1 [+] SKIP)
P1 |[X1]| DIV =T (P1 [+] DIV) |[X1]| DIV
DIV |[X1]| P1 =T DIV |[X1]| (P1 [+] DIV)
SKIP =T SKIP -- X1
DIV =T DIV -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 =T (? :Y1 -> Pf1 [+] DIV) -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1 =T (? :Y1 -> Pf1 [+] SKIP) -- X1
SKIP =T SKIP [[r1]]
DIV =T DIV [[r1]]
P2.0 =T SKIP ;; P2.0
P2.0 =T P2.0 ;; SKIP
DIV =T DIV ;; P1
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T (? :X1 -> Pf1 [> SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [> DIV =T (? :X1 -> Pf1 [> DIV) ;; Q1
SKIP =T SKIP |. Suc n1
DIV =T DIV |. n1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP) =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> (DIV |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| DIV) =T (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> (SKIP |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| DIV) =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> (DIV |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP) =T (? :Y1 -> Pf1 [+] DIV) |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE (? :Y1 -> Pf1 [+] SKIP) |[X1]| Qf1 x [> SKIP |[X1]| ? :Z1 -> Qf1 =T (? :Y1 -> Pf1 [+] SKIP) |[X1]| ? :Z1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] SKIP) ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x [> ? :Y1 -> Pf1 |[X1]| SKIP =T ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] SKIP)
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE (? :Y1 -> Pf1 [+] DIV) |[X1]| Qf1 x [> DIV |[X1]| ? :Z1 -> Qf1 =T (? :Y1 -> Pf1 [+] DIV) |[X1]| ? :Z1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| (? :Z1 -> Qf1 [+] DIV) ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x [> ? :Y1 -> Pf1 |[X1]| DIV =T ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T (? :X1 -> Pf1 [+] SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [+] DIV =T (? :X1 -> Pf1 [+] DIV) ;; Q1
lemmas cspT_all_dist_sym:
P1.1 [+] Q1 |~| P2.1 [+] Q1 =T (P1.1 |~| P2.1) [+] Q1
P1 [+] Q1.1 |~| P1 [+] Q2.1 =T P1 [+] (Q1.1 |~| Q2.1)
P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =T (P1.1 |~| P2.1) |[X1]| Q1
P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =T P1 |[X1]| (Q1.1 |~| Q2.1)
P1.1 -- X1 |~| P2.1 -- X1 =T (P1.1 |~| P2.1) -- X1
P1.1 [[r1]] |~| P2.1 [[r1]] =T (P1.1 |~| P2.1) [[r1]]
P1.1 ;; Q1 |~| P2.1 ;; Q1 =T (P1.1 |~| P2.1) ;; Q1
P1.1 |. n1 |~| P2.1 |. n1 =T (P1.1 |~| P2.1) |. n1
!! :C1 .. Pf1 |~| !! :C1 .. Qf1 =T !! c:C1 .. (Pf1 c |~| Qf1 c)
IF (C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =T (!! :C1 .. Pf1) [+] Q1
IF (C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =T P1 [+] (!! :C1 .. Qf1)
IF (C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 =T (!! :C1 .. Pf1) |[X1]| Q1
IF (C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c =T P1 |[X1]| (!! :C1 .. Qf1)
!! c:C1 .. Pf1 c -- X1 =T (!! :C1 .. Pf1) -- X1
!! c:C1 .. Pf1 c [[r1]] =T (!! :C1 .. Pf1) [[r1]]
!! c:C1 .. Pf1 c ;; Q1 =T (!! :C1 .. Pf1) ;; Q1
!! c:C1 .. Pf1 c |. n1 =T (!! :C1 .. Pf1) |. n1
IF (X1 = {}) THEN DIV [+] Q1 ELSE !!<f1> x:X1 .. Pf1 x [+] Q1 =T (!!<f1> :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN P1 [+] DIV ELSE !!<f1> x:X1 .. P1 [+] Qf1 x =T P1 [+] (!!<f1> :X1 .. Qf1)
IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !!<f1> x:Y1 .. Pf1 x |[X1]| Q1 =T (!!<f1> :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !!<f1> x:Y1 .. P1 |[X1]| Qf1 x =T P1 |[X1]| (!!<f1> :Y1 .. Qf1)
!!<f1> x:Y1 .. Pf1 x -- X1 =T (!!<f1> :Y1 .. Pf1) -- X1
!!<f1> x:X1 .. Pf1 x [[r1]] =T (!!<f1> :X1 .. Pf1) [[r1]]
!!<f1> x:X1 .. Pf1 x ;; Q1 =T (!!<f1> :X1 .. Pf1) ;; Q1
!!<f1> x:X1 .. Pf1 x |. n1 =T (!!<f1> :X1 .. Pf1) |. n1
IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =T (! :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =T P1 [+] (! :X1 .. Qf1)
IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =T (! :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =T P1 |[X1]| (! :Y1 .. Qf1)
! x:Y1 .. Pf1 x -- X1 =T (! :Y1 .. Pf1) -- X1
! x:X1 .. Pf1 x [[r1]] =T (! :X1 .. Pf1) [[r1]]
! x:X1 .. Pf1 x ;; Q1 =T (! :X1 .. Pf1) ;; Q1
! x:X1 .. Pf1 x |. n1 =T (! :X1 .. Pf1) |. n1
P1.1 [[r1]] [+] P2.1 [[r1]] =T (P1.1 [+] P2.1) [[r1]]
P1.1 |. n1 [+] P2.1 |. n1 =T (P1.1 [+] P2.1) |. n1
lemmas cspT_all_dist_sym:
P1.1 [+] Q1 |~| P2.1 [+] Q1 =T (P1.1 |~| P2.1) [+] Q1
P1 [+] Q1.1 |~| P1 [+] Q2.1 =T P1 [+] (Q1.1 |~| Q2.1)
P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =T (P1.1 |~| P2.1) |[X1]| Q1
P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =T P1 |[X1]| (Q1.1 |~| Q2.1)
P1.1 -- X1 |~| P2.1 -- X1 =T (P1.1 |~| P2.1) -- X1
P1.1 [[r1]] |~| P2.1 [[r1]] =T (P1.1 |~| P2.1) [[r1]]
P1.1 ;; Q1 |~| P2.1 ;; Q1 =T (P1.1 |~| P2.1) ;; Q1
P1.1 |. n1 |~| P2.1 |. n1 =T (P1.1 |~| P2.1) |. n1
!! :C1 .. Pf1 |~| !! :C1 .. Qf1 =T !! c:C1 .. (Pf1 c |~| Qf1 c)
IF (C1 = {}) THEN DIV [+] Q1 ELSE !! c:C1 .. Pf1 c [+] Q1 =T (!! :C1 .. Pf1) [+] Q1
IF (C1 = {}) THEN P1 [+] DIV ELSE !! c:C1 .. P1 [+] Qf1 c =T P1 [+] (!! :C1 .. Qf1)
IF (C1 = {}) THEN DIV |[X1]| Q1 ELSE !! c:C1 .. Pf1 c |[X1]| Q1 =T (!! :C1 .. Pf1) |[X1]| Q1
IF (C1 = {}) THEN P1 |[X1]| DIV ELSE !! c:C1 .. P1 |[X1]| Qf1 c =T P1 |[X1]| (!! :C1 .. Qf1)
!! c:C1 .. Pf1 c -- X1 =T (!! :C1 .. Pf1) -- X1
!! c:C1 .. Pf1 c [[r1]] =T (!! :C1 .. Pf1) [[r1]]
!! c:C1 .. Pf1 c ;; Q1 =T (!! :C1 .. Pf1) ;; Q1
!! c:C1 .. Pf1 c |. n1 =T (!! :C1 .. Pf1) |. n1
IF (X1 = {}) THEN DIV [+] Q1 ELSE !!<f1> x:X1 .. Pf1 x [+] Q1 =T (!!<f1> :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN P1 [+] DIV ELSE !!<f1> x:X1 .. P1 [+] Qf1 x =T P1 [+] (!!<f1> :X1 .. Qf1)
IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE !!<f1> x:Y1 .. Pf1 x |[X1]| Q1 =T (!!<f1> :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE !!<f1> x:Y1 .. P1 |[X1]| Qf1 x =T P1 |[X1]| (!!<f1> :Y1 .. Qf1)
!!<f1> x:Y1 .. Pf1 x -- X1 =T (!!<f1> :Y1 .. Pf1) -- X1
!!<f1> x:X1 .. Pf1 x [[r1]] =T (!!<f1> :X1 .. Pf1) [[r1]]
!!<f1> x:X1 .. Pf1 x ;; Q1 =T (!!<f1> :X1 .. Pf1) ;; Q1
!!<f1> x:X1 .. Pf1 x |. n1 =T (!!<f1> :X1 .. Pf1) |. n1
IF (X1 = {}) THEN DIV [+] Q1 ELSE ! x:X1 .. Pf1 x [+] Q1 =T (! :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN P1 [+] DIV ELSE ! x:X1 .. P1 [+] Qf1 x =T P1 [+] (! :X1 .. Qf1)
IF (Y1 = {}) THEN DIV |[X1]| Q1 ELSE ! x:Y1 .. Pf1 x |[X1]| Q1 =T (! :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN P1 |[X1]| DIV ELSE ! x:Y1 .. P1 |[X1]| Qf1 x =T P1 |[X1]| (! :Y1 .. Qf1)
! x:Y1 .. Pf1 x -- X1 =T (! :Y1 .. Pf1) -- X1
! x:X1 .. Pf1 x [[r1]] =T (! :X1 .. Pf1) [[r1]]
! x:X1 .. Pf1 x ;; Q1 =T (! :X1 .. Pf1) ;; Q1
! x:X1 .. Pf1 x |. n1 =T (! :X1 .. Pf1) |. n1
P1.1 [[r1]] [+] P2.1 [[r1]] =T (P1.1 [+] P2.1) [[r1]]
P1.1 |. n1 [+] P2.1 |. n1 =T (P1.1 [+] P2.1) |. n1
lemmas cspT_unwind_sym:
PF1 ∈ ProcFun ==> PF1 (FIX PF1) p1 =T (FIX PF1) p1
PF1 ∈ gProcFun ==> PF1 (FIX! PF1) p1 =T (FIX! PF1) p1
lemmas cspT_unwind_sym:
PF1 ∈ ProcFun ==> PF1 (FIX PF1) p1 =T (FIX PF1) p1
PF1 ∈ gProcFun ==> PF1 (FIX! PF1) p1 =T (FIX! PF1) p1
lemmas cspT_step_sym:
? :{} -> Pf1 =T STOP
? x:{a1} -> P1 =T a1 -> P1
? x:(X1 ∪ Y1) -> IF (x ∈ X1 ∧ x ∈ Y1) THEN Pf1 x |~| Qf1 x ELSE IF (x ∈ X1) THEN Pf1 x ELSE Qf1 x =T ? :X1 -> Pf1 [+] ? :Y1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x =T ? :Y1 -> Pf1 |[X1]| ? :Z1 -> Qf1
IF (Y1 ∩ X1 = {}) THEN ? x:Y1 -> Pf1 x -- X1 ELSE ? x:(Y1 - X1) -> Pf1 x -- X1 [> (! x:(Y1 ∩ X1) .. Pf1 x -- X1) =T (? :Y1 -> Pf1) -- X1
? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =T (? :X1 -> Pf1) [[r1]]
? x:X1 -> (Pf1 x ;; Q1) =T ? :X1 -> Pf1 ;; Q1
? x:X1 -> Pf1 x |. n1 =T (? :X1 -> Pf1) |. Suc n1
lemmas cspT_step_sym:
? :{} -> Pf1 =T STOP
? x:{a1} -> P1 =T a1 -> P1
? x:(X1 ∪ Y1) -> IF (x ∈ X1 ∧ x ∈ Y1) THEN Pf1 x |~| Qf1 x ELSE IF (x ∈ X1) THEN Pf1 x ELSE Qf1 x =T ? :X1 -> Pf1 [+] ? :Y1 -> Qf1
? x:(X1 ∩ Y1 ∩ Z1 ∪ (Y1 - X1) ∪ (Z1 - X1)) -> IF (x ∈ X1) THEN Pf1 x |[X1]| Qf1 x ELSE IF (x ∈ Y1 ∧ x ∈ Z1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 |~| ? :Y1 -> Pf1 |[X1]| Qf1 x ELSE IF (x ∈ Y1) THEN Pf1 x |[X1]| ? :Z1 -> Qf1 ELSE ? :Y1 -> Pf1 |[X1]| Qf1 x =T ? :Y1 -> Pf1 |[X1]| ? :Z1 -> Qf1
IF (Y1 ∩ X1 = {}) THEN ? x:Y1 -> Pf1 x -- X1 ELSE ? x:(Y1 - X1) -> Pf1 x -- X1 [> (! x:(Y1 ∩ X1) .. Pf1 x -- X1) =T (? :Y1 -> Pf1) -- X1
? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =T (? :X1 -> Pf1) [[r1]]
? x:X1 -> (Pf1 x ;; Q1) =T ? :X1 -> Pf1 ;; Q1
? x:X1 -> Pf1 x |. n1 =T (? :X1 -> Pf1) |. Suc n1