Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_Main (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| February 2005 (modified) |
| June 2005 (modified) |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| April 2006 (modified) |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_T_Main
imports CSP_T_tactic CSP_T_surj
begin
(*--------------------------------------------*
| |
| decomposition considering refinement |
| |
*--------------------------------------------*)
lemmas cspT_mono_ref = cspT_free_mono
cspT_Act_prefix_mono cspT_Ext_pre_choice_mono
cspT_IF_mono cspT_decompo_subset
lemmas cspT_decompo_ref = cspT_mono_ref cspT_cong
(*-------------------------------------------------------*
| |
| adding ... to automatically check Procfun |
| |
*-------------------------------------------------------*)
(*-------------------------------------------------------------*
| |
| 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]
(* top *)
declare cspT_top [simp]
declare cspT_Ent_choice_left_ref [simp]
(*-------------------[test of CSP_T]------------------------*
datatype Event = eva | evb
datatype PNSpec = AB
datatype PNImpl = A
consts
PNfunSpec :: "PNSpec => (PNSpec, Event) proc"
PNfunImpl :: "PNImpl => (PNImpl, Event) proc"
primrec
"PNfunSpec AB = eva -> $AB |~| evb -> $AB"
primrec
"PNfunImpl A = eva -> $A"
defs (overloaded)
Set_PNfunSpec_def : "PNfun == PNfunSpec"
Set_PNfunImpl_def : "PNfun == PNfunImpl"
FPmode_def : "FPmode == CMSmode"
declare Set_PNfunSpec_def [simp]
declare Set_PNfunImpl_def [simp]
declare FPmode_def [simp]
lemma example_test_01: "PNfun AB = eva -> $AB |~| evb -> $AB"
by (simp)
lemma example_test_02: "PNfun A = eva -> $A"
by (simp)
consts
Spec_Impl :: "PNSpec => (PNImpl, Event) proc"
primrec
"Spec_Impl AB = $A"
consts
Spec :: "(PNSpec, Event) proc"
Impl :: "(PNImpl, Event) proc"
defs
Spec_def : "Spec == $AB"
Impl_def : "Impl == $A"
lemma guardedfun_ex[simp]:
"guardedfun PNfunSpec"
"guardedfun PNfunImpl"
by (simp add: guardedfun_def, rule allI, induct_tac p, simp)+
lemma example_test_fp: "Spec <=T Impl"
apply (simp add: Spec_def Impl_def)
apply (rule cspT_fp_induct_left[of _ "Spec_Impl"])
apply (simp_all)
apply (simp)
apply (induct_tac p)
apply (simp)
apply (rule cspT_rw_right)
apply (rule cspT_unwind)
apply (simp_all)
apply (simp)
apply (rule cspT_Int_choice_left1)
apply (simp)
done
-- you have to note that you cannot prove "$AB <=T $A"
-- because $AB has a wider type "(PNSpec,'s) proc" than
-- "(PNSpec,Event) proc".
*-------------------[test of CSP_T]------------------------*)
end
lemma cspT_mono_ref:
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
[| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
[| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
[| sumset C2.0 ⊆ sumset C1.0;
!!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
[| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
[| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
[| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
[| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
[| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf
lemma cspT_decompo_ref:
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 <=T[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 <=T[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 <=T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P <=T[M1.0,M2.0] Q |] ==> P -- X <=T[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P <=T[M1.0,M2.0] Q |] ==> P [[r1.0]] <=T[M1.0,M2.0] Q [[r2.0]]
[| P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 <=T[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P <=T[M1.0,M2.0] Q |] ==> P |. n1.0 <=T[M1.0,M2.0] Q |. n2.0
[| a = b; P <=T[M1.0,M2.0] Q |] ==> a -> P <=T[M1.0,M2.0] b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ? :X -> Pf <=T[M1.0,M2.0] ? :Y -> Qf
[| b1.0 = b2.0; P1.0 <=T[M1.0,M2.0] Q1.0; P2.0 <=T[M1.0,M2.0] Q2.0 |]
==> IF b1.0 THEN P1.0 ELSE P2.0 <=T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
[| sumset C2.0 ⊆ sumset C1.0;
!!c. c ∈ sumset C2.0 ==> Pf c <=T[M1.0,M2.0] Qf c |]
==> !! :C1.0 .. Pf <=T[M1.0,M2.0] !! :C2.0 .. Qf
[| N2.0 ⊆ N1.0; !!n. n ∈ N2.0 ==> Pf n <=T[M1.0,M2.0] Qf n |]
==> !nat :N1.0 .. Pf <=T[M1.0,M2.0] !nat :N2.0 .. Qf
[| Ys ⊆ Xs; !!X. X ∈ Ys ==> Pf X <=T[M1.0,M2.0] Qf X |]
==> !set :Xs .. Pf <=T[M1.0,M2.0] !set :Ys .. Qf
[| Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ! :X .. Pf <=T[M1.0,M2.0] ! :Y .. Qf
[| inj f; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> !<f> :X .. Pf <=T[M1.0,M2.0] !<f> :Y .. Qf
[| Y ≠ {}; Y ⊆ X; !!a. a ∈ Y ==> Pf a <=T[M1.0,M2.0] Qf a |]
==> ! x:X .. x -> Pf x <=T[M1.0,M2.0] ? :Y -> Qf
[| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
==> P1.0 [+] P2.0 =T[M1.0,M2.0] Q1.0 [+] Q2.0
[| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
==> P1.0 |~| P2.0 =T[M1.0,M2.0] Q1.0 |~| Q2.0
[| X = Y; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
==> P1.0 |[X]| P2.0 =T[M1.0,M2.0] Q1.0 |[Y]| Q2.0
[| X = Y; P =T[M1.0,M2.0] Q |] ==> P -- X =T[M1.0,M2.0] Q -- Y
[| r1.0 = r2.0; P =T[M1.0,M2.0] Q |] ==> P [[r1.0]] =T[M1.0,M2.0] Q [[r2.0]]
[| P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
==> P1.0 ;; P2.0 =T[M1.0,M2.0] Q1.0 ;; Q2.0
[| n1.0 = n2.0; P =T[M1.0,M2.0] Q |] ==> P |. n1.0 =T[M1.0,M2.0] Q |. n2.0
[| a = b; P =T[M1.0,M2.0] Q |] ==> a -> P =T[M1.0,M2.0] b -> Q
[| X = Y; !!a. a ∈ Y ==> Pf a =T[M1.0,M2.0] Qf a |]
==> ? :X -> Pf =T[M1.0,M2.0] ? :Y -> Qf
[| C1.0 = C2.0; !!c. c ∈ sumset C1.0 ==> Pf c =T[M1.0,M2.0] Qf c |]
==> !! :C1.0 .. Pf =T[M1.0,M2.0] !! :C2.0 .. Qf
[| Xs1.0 = Xs2.0; !!X. X ∈ Xs1.0 ==> Pf X =T[M1.0,M2.0] Qf X |]
==> !set :Xs1.0 .. Pf =T[M1.0,M2.0] !set :Xs2.0 .. Qf
[| N1.0 = N2.0; !!n. n ∈ N1.0 ==> Pf n =T[M1.0,M2.0] Qf n |]
==> !nat :N1.0 .. Pf =T[M1.0,M2.0] !nat :N2.0 .. Qf
[| X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
==> ! :X1.0 .. Pf =T[M1.0,M2.0] ! :X2.0 .. Qf
[| inj f; X1.0 = X2.0; !!x. x ∈ X1.0 ==> Pf x =T[M1.0,M2.0] Qf x |]
==> !<f> :X1.0 .. Pf =T[M1.0,M2.0] !<f> :X2.0 .. Qf
[| b1.0 = b2.0; P1.0 =T[M1.0,M2.0] Q1.0; P2.0 =T[M1.0,M2.0] Q2.0 |]
==> IF b1.0 THEN P1.0 ELSE P2.0 =T[M1.0,M2.0] IF b2.0 THEN Q1.0 ELSE Q2.0
lemma cspT_SKIP_DIV_resolve_sym:
? x:(Y1 - X1) -> (SKIP |[X1]| Qf1 x) =T[M1.0,M1.0] SKIP |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) =T[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| SKIP
? x:(Y1 - X1) -> (DIV |[X1]| Qf1 x) [+] DIV =T[M1.0,M1.0]
DIV |[X1]| ? :Y1 -> Qf1
? x:(Y1 - X1) -> (Pf1 x |[X1]| DIV) [+] DIV =T[M1.0,M1.0]
? :Y1 -> Pf1 |[X1]| DIV
SKIP =T[M2.0,M1.0] SKIP [+] DIV
SKIP =T[M2.0,M1.0] DIV [+] SKIP
DIV =T[M2.0,M1.0] SKIP |[X1]| DIV
DIV =T[M2.0,M1.0] DIV |[X1]| SKIP
SKIP =T[M2.0,M1.0] SKIP |[X1]| SKIP
DIV =T[M2.0,M1.0] DIV |[X1]| DIV
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] SKIP =T[M1.0,M1.0]
(? :Y1 -> Pf1 [+] SKIP) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] SKIP =T[M1.0,M1.0]
SKIP |[X1]| (? :Y1 -> Pf1 [+] SKIP)
? x:(Y1 - X1) -> (Pf1 x |[X1]| SKIP) [+] DIV =T[M1.0,M1.0]
(? :Y1 -> Pf1 [+] DIV) |[X1]| SKIP
? x:(Y1 - X1) -> (SKIP |[X1]| Pf1 x) [+] DIV =T[M1.0,M1.0]
SKIP |[X1]| (? :Y1 -> Pf1 [+] DIV)
P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] SKIP) |[X1]| DIV
DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] SKIP)
P1 |[X1]| DIV =T[M1.0,M1.0] (P1 [+] DIV) |[X1]| DIV
DIV |[X1]| P1 =T[M1.0,M1.0] DIV |[X1]| (P1 [+] DIV)
SKIP =T[M2.0,M1.0] SKIP -- X1
DIV =T[M2.0,M1.0] DIV -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] DIV |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1
=T[M1.0,M1.0] (? :Y1 -> Pf1 [+] DIV) -- X1
? x:(Y1 - X1) -> Pf1 x -- X1 [+] SKIP |~| ! x:(Y1 ∩ X1) .. Pf1 x -- X1
=T[M1.0,M1.0] (? :Y1 -> Pf1 [+] SKIP) -- X1
SKIP =T[M2.0,M1.0] SKIP [[r1]]
DIV =T[M2.0,M1.0] DIV [[r1]]
P2.0 =T[M1.0,M1.0] SKIP ;; P2.0
P2.0 =T[M1.0,M1.0] P2.0 ;; SKIP
DIV =T[M2.0,M1.0] DIV ;; P1
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [> SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [> DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [> DIV) ;; Q1
SKIP =T[M2.0,M1.0] SKIP |. Suc n1
DIV =T[M2.0,M1.0] 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[M1.0,M1.0] (? :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[M1.0,M1.0] (? :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[M1.0,M1.0] (? :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[M1.0,M1.0] (? :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[M1.0,M1.0] (? :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[M1.0,M1.0] ? :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[M1.0,M1.0] (? :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[M1.0,M1.0] ? :Y1 -> Pf1 |[X1]| (? :Z1 -> Qf1 [+] DIV)
? x:X1 -> (Pf1 x ;; Q1) [> Q1 =T[M1.0,M1.0] (? :X1 -> Pf1 [+] SKIP) ;; Q1
? x:X1 -> (Pf1 x ;; Q1) [+] DIV =T[M1.0,M1.0] (? :X1 -> Pf1 [+] DIV) ;; Q1
lemma cspT_all_dist_sym:
P1.1 [+] Q1 |~| P2.1 [+] Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) [+] Q1
P1 [+] Q1.1 |~| P1 [+] Q2.1 =T[M1.0,M1.0] P1 [+] (Q1.1 |~| Q2.1)
P1.1 |[X1]| Q1 |~| P2.1 |[X1]| Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |[X1]| Q1
P1 |[X1]| Q1.1 |~| P1 |[X1]| Q2.1 =T[M1.0,M1.0] P1 |[X1]| (Q1.1 |~| Q2.1)
P1.1 -- X1 |~| P2.1 -- X1 =T[M1.0,M1.0] (P1.1 |~| P2.1) -- X1
P1.1 [[r1]] |~| P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 |~| P2.1) [[r1]]
P1.1 ;; Q1 |~| P2.1 ;; Q1 =T[M1.0,M1.0] (P1.1 |~| P2.1) ;; Q1
P1.1 |. n1 |~| P2.1 |. n1 =T[M1.0,M1.0] (P1.1 |~| P2.1) |. n1
!! :C1 .. Pf1 |~| !! :C1 .. Qf1 =T[M1.0,M1.0] !! c:C1 .. (Pf1 c |~| Qf1 c)
!nat :N1 .. Pf1 |~| !nat :N1 .. Qf1 =T[M1.0,M1.0] !nat n:N1 .. (Pf1 n |~| Qf1 n)
!set :Xs1 .. Pf1 |~| !set :Xs1 .. Qf1 =T[M1.0,M1.0]
!set X:Xs1 .. (Pf1 X |~| Qf1 X)
! :X1 .. Pf1 |~| ! :X1 .. Qf1 =T[M1.0,M1.0] ! a:X1 .. (Pf1 a |~| Qf1 a)
inj f1
==> !<f1> :X1 .. Pf1 |~| !<f1> :X1 .. Qf1 =T[M1.0,M1.0]
!<f1> a:X1 .. (Pf1 a |~| Qf1 a)
IF (sumset C1 = {}) THEN (DIV [+] Q1) ELSE (!! c:C1 .. Pf1 c [+] Q1)
=T[M1.0,M1.0] (!! :C1 .. Pf1) [+] Q1
IF (sumset C1 = {}) THEN (P1 [+] DIV) ELSE (!! c:C1 .. P1 [+] Qf1 c)
=T[M1.0,M1.0] P1 [+] (!! :C1 .. Qf1)
IF (sumset C1 = {}) THEN (DIV |[X1]| Q1) ELSE (!! c:C1 .. Pf1 c |[X1]| Q1)
=T[M1.0,M1.0] (!! :C1 .. Pf1) |[X1]| Q1
IF (sumset C1 = {}) THEN (P1 |[X1]| DIV) ELSE (!! c:C1 .. P1 |[X1]| Qf1 c)
=T[M1.0,M1.0] P1 |[X1]| (!! :C1 .. Qf1)
!! c:C1 .. Pf1 c -- X1 =T[M1.0,M1.0] (!! :C1 .. Pf1) -- X1
!! c:C1 .. Pf1 c [[r1]] =T[M1.0,M1.0] (!! :C1 .. Pf1) [[r1]]
!! c:C1 .. Pf1 c ;; Q1 =T[M1.0,M1.0] (!! :C1 .. Pf1) ;; Q1
!! c:C1 .. Pf1 c |. m1 =T[M1.0,M1.0] (!! :C1 .. Pf1) |. m1
IF (N1 = {}) THEN (DIV [+] Q1) ELSE (!nat n:N1 .. Pf1 n [+] Q1) =T[M1.0,M1.0]
(!nat :N1 .. Pf1) [+] Q1
IF (N1 = {}) THEN (P1 [+] DIV) ELSE (!nat n:N1 .. P1 [+] Qf1 n) =T[M1.0,M1.0]
P1 [+] (!nat :N1 .. Qf1)
IF (N1 = {}) THEN (DIV |[X1]| Q1) ELSE (!nat n:N1 .. Pf1 n |[X1]| Q1)
=T[M1.0,M1.0] (!nat :N1 .. Pf1) |[X1]| Q1
IF (N1 = {}) THEN (P1 |[X1]| DIV) ELSE (!nat n:N1 .. P1 |[X1]| Qf1 n)
=T[M1.0,M1.0] P1 |[X1]| (!nat :N1 .. Qf1)
!nat n:N1 .. Pf1 n -- X1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) -- X1
!nat n:N1 .. Pf1 n [[r1]] =T[M1.0,M1.0] (!nat :N1 .. Pf1) [[r1]]
!nat n:N1 .. Pf1 n ;; Q1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) ;; Q1
!nat n:N1 .. Pf1 n |. m1 =T[M1.0,M1.0] (!nat :N1 .. Pf1) |. m1
IF (Xs1 = {}) THEN (DIV [+] Q1) ELSE (!set X:Xs1 .. Pf1 X [+] Q1) =T[M1.0,M1.0]
(!set :Xs1 .. Pf1) [+] Q1
IF (Xs1 = {}) THEN (P1 [+] DIV) ELSE (!set X:Xs1 .. P1 [+] Qf1 X) =T[M1.0,M1.0]
P1 [+] (!set :Xs1 .. Qf1)
IF (Xs1 = {}) THEN (DIV |[Y1]| Q1) ELSE (!set X:Xs1 .. Pf1 X |[Y1]| Q1)
=T[M1.0,M1.0] (!set :Xs1 .. Pf1) |[Y1]| Q1
IF (Xs1 = {}) THEN (P1 |[Y1]| DIV) ELSE (!set X:Xs1 .. P1 |[Y1]| Qf1 X)
=T[M1.0,M1.0] P1 |[Y1]| (!set :Xs1 .. Qf1)
!set X:Xs1 .. Pf1 X -- Y1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) -- Y1
!set X:Xs1 .. Pf1 X [[r1]] =T[M1.0,M1.0] (!set :Xs1 .. Pf1) [[r1]]
!set X:Xs1 .. Pf1 X ;; Q1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) ;; Q1
!set X:Xs1 .. Pf1 X |. m1 =T[M1.0,M1.0] (!set :Xs1 .. Pf1) |. m1
IF (X1 = {}) THEN (DIV [+] Q1) ELSE (! x:X1 .. Pf1 x [+] Q1) =T[M1.0,M1.0]
(! :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN (P1 [+] DIV) ELSE (! x:X1 .. P1 [+] Qf1 x) =T[M1.0,M1.0]
P1 [+] (! :X1 .. Qf1)
IF (Y1 = {}) THEN (DIV |[X1]| Q1) ELSE (! x:Y1 .. Pf1 x |[X1]| Q1)
=T[M1.0,M1.0] (! :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN (P1 |[X1]| DIV) ELSE (! x:Y1 .. P1 |[X1]| Qf1 x)
=T[M1.0,M1.0] P1 |[X1]| (! :Y1 .. Qf1)
! x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (! :Y1 .. Pf1) -- X1
! x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (! :X1 .. Pf1) [[r1]]
! x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (! :X1 .. Pf1) ;; Q1
! x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (! :X1 .. Pf1) |. n1
IF (X1 = {}) THEN (DIV [+] Q1) ELSE (!<f1> x:X1 .. Pf1 x [+] Q1) =T[M1.0,M1.0]
(!<f1> :X1 .. Pf1) [+] Q1
IF (X1 = {}) THEN (P1 [+] DIV) ELSE (!<f1> x:X1 .. P1 [+] Qf1 x) =T[M1.0,M1.0]
P1 [+] (!<f1> :X1 .. Qf1)
IF (Y1 = {}) THEN (DIV |[X1]| Q1) ELSE (!<f1> x:Y1 .. Pf1 x |[X1]| Q1)
=T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) |[X1]| Q1
IF (Y1 = {}) THEN (P1 |[X1]| DIV) ELSE (!<f1> x:Y1 .. P1 |[X1]| Qf1 x)
=T[M1.0,M1.0] P1 |[X1]| (!<f1> :Y1 .. Qf1)
!<f1> x:Y1 .. Pf1 x -- X1 =T[M1.0,M1.0] (!<f1> :Y1 .. Pf1) -- X1
!<f1> x:X1 .. Pf1 x [[r1]] =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) [[r1]]
!<f1> x:X1 .. Pf1 x ;; Q1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) ;; Q1
!<f1> x:X1 .. Pf1 x |. n1 =T[M1.0,M1.0] (!<f1> :X1 .. Pf1) |. n1
P1.1 [[r1]] [+] P2.1 [[r1]] =T[M1.0,M1.0] (P1.1 [+] P2.1) [[r1]]
P1.1 |. n1 [+] P2.1 |. n1 =T[M1.0,M1.0] (P1.1 [+] P2.1) |. n1
lemma cspT_unwind_sym:
[| Pf1 = PNfun;
FPmode = CPOmode ∨ FPmode = CMSmode ∧ guardedfun Pf1 ∨ FPmode = MIXmode |]
==> Pf1 p1 =T $p1
lemma cspT_step_sym:
? :{} -> Pf1 =T[M2.0,M1.0] STOP
? x:{a1} -> P1 =T[M1.0,M1.0] 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[M1.0,M1.0] ? :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[M1.0,M1.0] ? :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[M1.0,M1.0] (? :Y1 -> Pf1) -- X1
? y:(r1 `` X1) -> (! x:{x : X1. (x, y) ∈ r1} .. Pf1 x [[r1]]) =T[M1.0,M1.0]
(? :X1 -> Pf1) [[r1]]
? x:X1 -> (Pf1 x ;; Q1) =T[M1.0,M1.0] ? :X1 -> Pf1 ;; Q1
? x:X1 -> Pf1 x |. n1 =T[M1.0,M1.0] (? :X1 -> Pf1) |. Suc n1