Up to index of Isabelle/HOL/CSP/CSP_T/CSP_F
theory CSP_F_law_basic(*-------------------------------------------* | CSP-Prover on Isabelle2004 | | December 2004 | | June 2005 (modified) | | September 2005 (modified) | | | | CSP-Prover on Isabelle2005 | | October 2005 (modified) | | January 2006 (modified) | | April 2006 (modified) | | March 2007 (modified) | | August 2007 (modified) | | | | CSP-Prover on Isabelle2009 | | June 2009 (modified) | | | | Yoshinao Isobe (AIST JAPAN) | *-------------------------------------------*) theory CSP_F_law_basic imports CSP_F_law_decompo CSP_T_law_basic begin (***************************************************************** 1. Commutativity 2. Associativity 3. Idempotence 4. Left Commutativity 5. IF *****************************************************************) (********************************************************* IF bool *********************************************************) (*------------------* | csp law | *------------------*) lemma cspF_IF_split: "IF b THEN P ELSE Q =F[M,M] (if b then P else Q)" apply (simp add: cspF_semantics) apply (simp add: traces_def) apply (simp add: failures_def) done lemma cspF_IF_True: "IF True THEN P ELSE Q =F[M,M] P" apply (rule cspF_rw_left) apply (rule cspF_IF_split) by (simp) lemma cspF_IF_False: "IF False THEN P ELSE Q =F[M,M] Q" apply (rule cspF_rw_left) apply (rule cspF_IF_split) by (simp) lemmas cspF_IF = cspF_IF_True cspF_IF_False (*-----------------------------------* | Idempotence | *-----------------------------------*) lemma cspF_Ext_choice_idem: "P [+] P =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Ext_choice_idem) apply (rule order_antisym) apply (rule, simp add: in_traces in_failures) apply (elim conjE disjE) apply (simp_all) apply (rule proc_F2_F4) apply (simp_all) apply (rule, simp add: in_traces in_failures) done lemma cspF_Int_choice_idem: "P |~| P =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_idem) apply (rule order_antisym) apply (rule, simp add: in_failures)+ done (*------------------* | csp law | *------------------*) lemmas cspF_idem = cspF_Ext_choice_idem cspF_Int_choice_idem (*-----------------------------------* | Commutativity | *-----------------------------------*) (********************************************************* Ext choice *********************************************************) lemma cspF_Ext_choice_commut: "P [+] Q =F[M,M] Q [+] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Ext_choice_commut) apply (rule order_antisym) apply (rule, simp add: in_failures, fast)+ done (********************************************************* Int choice *********************************************************) lemma cspF_Int_choice_commut: "P |~| Q =F[M,M] Q |~| P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_commut) apply (rule order_antisym) apply (rule, simp add: in_failures, fast)+ done (********************************************************* Parallel *********************************************************) lemma cspF_Parallel_commut: "P |[X]| Q =F[M,M] Q |[X]| P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Parallel_commut) apply (rule order_antisym) apply (rule, simp add: in_failures) apply (elim conjE exE) apply (rule_tac x="Z" in exI) apply (rule_tac x="Y" in exI, simp) apply (rule conjI, fast) apply (rule_tac x="t" in exI) apply (rule_tac x="sa" in exI) apply (simp add: par_tr_sym) apply (rule, simp add: in_failures) apply (elim conjE exE) apply (rule_tac x="Z" in exI) apply (rule_tac x="Y" in exI, simp) apply (rule conjI, fast) apply (rule_tac x="t" in exI) apply (rule_tac x="sa" in exI) apply (simp add: par_tr_sym) done (*------------------* | csp law | *------------------*) lemmas cspF_commut = cspF_Ext_choice_commut cspF_Int_choice_commut cspF_Parallel_commut (*-----------------------------------* | Associativity | *-----------------------------------*) lemma cspF_Ext_choice_assoc: "P [+] (Q [+] R) =F[M,M] (P [+] Q) [+] R" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Ext_choice_assoc) apply (rule order_antisym) apply (rule, simp add: in_failures in_traces) apply (force) apply (rule, simp add: in_failures in_traces) apply (force) done lemma cspF_Ext_choice_assoc_sym: "(P [+] Q) [+] R =F[M,M] P [+] (Q [+] R)" apply (rule cspF_sym) apply (simp add: cspF_Ext_choice_assoc) done lemma cspF_Int_choice_assoc: "P |~| (Q |~| R) =F[M,M] (P |~| Q) |~| R" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_assoc) apply (rule order_antisym) apply (rule, simp add: in_failures)+ done lemma cspF_Int_choice_assoc_sym: "(P |~| Q) |~| R =F[M,M] P |~| (Q |~| R)" apply (rule cspF_sym) apply (simp add: cspF_Int_choice_assoc) done (*------------------* | csp law | *------------------*) lemmas cspF_assoc = cspF_Ext_choice_assoc cspF_Int_choice_assoc lemmas cspF_assoc_sym = cspF_Ext_choice_assoc_sym cspF_Int_choice_assoc_sym (*-----------------------------------* | Left Commutativity | *-----------------------------------*) lemma cspF_Ext_choice_left_commut: "P [+] (Q [+] R) =F[M,M] Q [+] (P [+] R)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Ext_choice_left_commut) apply (rule order_antisym) apply (rule, simp add: in_failures in_traces) apply (force) apply (rule, simp add: in_failures in_traces) apply (force) done lemma cspF_Int_choice_left_commut: "P |~| (Q |~| R) =F[M,M] Q |~| (P |~| R)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_left_commut) apply (rule order_antisym) apply (rule, simp add: in_failures)+ done lemmas cspF_left_commut = cspF_Ext_choice_left_commut cspF_Int_choice_left_commut (*-----------------------------------* | Unit | *-----------------------------------*) (*** STOP [+] P ***) lemma cspF_Ext_choice_unit_l: "STOP [+] P =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Ext_choice_unit_l) apply (rule order_antisym) apply (rule, simp add: in_traces in_failures) apply (elim conjE disjE) apply (simp_all) apply (rule proc_F2_F4) apply (simp_all) apply (rule, simp add: in_failures) done lemma cspF_Ext_choice_unit_r: "P [+] STOP =F[M,M] P" apply (rule cspF_rw_left) apply (rule cspF_Ext_choice_commut) apply (simp add: cspF_Ext_choice_unit_l) done lemmas cspF_Ext_choice_unit = cspF_Ext_choice_unit_l cspF_Ext_choice_unit_r lemma cspF_Int_choice_unit_l: "DIV |~| P =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_unit_l) apply (rule order_antisym) apply (rule, simp add: in_failures) apply (rule, simp add: in_failures) done lemma cspF_Int_choice_unit_r: "P |~| DIV =F[M,M] P" apply (rule cspF_rw_left) apply (rule cspF_Int_choice_commut) apply (simp add: cspF_Int_choice_unit_l) done lemmas cspF_Int_choice_unit = cspF_Int_choice_unit_l cspF_Int_choice_unit_r lemmas cspF_unit = cspF_Ext_choice_unit cspF_Int_choice_unit (*-----------------------------------* | !!-empty | *-----------------------------------*) lemma cspF_Rep_int_choice_sum_DIV: "sumset C = {} ==> !! : C .. Pf =F[M1,M2] DIV" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_DIV) apply (simp add: failures_def) apply (simp add: empF_def) done lemma cspF_Rep_int_choice_nat_DIV: "!nat :{} .. Pf =F[M1,M2] DIV" by (simp add: Rep_int_choice_ss_def cspF_Rep_int_choice_sum_DIV) lemma cspF_Rep_int_choice_set_DIV: "!set :{} .. Pf =F[M1,M2] DIV" by (simp add: Rep_int_choice_ss_def cspF_Rep_int_choice_sum_DIV) lemma cspF_Rep_int_choice_com_DIV: "! :{} .. Pf =F[M1,M2] DIV" by (simp add: Rep_int_choice_com_def cspF_Rep_int_choice_set_DIV) lemma cspF_Rep_int_choice_f_DIV: "inj f ==> !<f> :{} .. Pf =F[M1,M2] DIV" by (simp add: Rep_int_choice_f_def cspF_Rep_int_choice_com_DIV) lemmas cspF_Rep_int_choice_DIV = cspF_Rep_int_choice_sum_DIV cspF_Rep_int_choice_nat_DIV cspF_Rep_int_choice_set_DIV cspF_Rep_int_choice_com_DIV cspF_Rep_int_choice_f_DIV lemmas cspF_Rep_int_choice_DIV_sym = cspF_Rep_int_choice_DIV[THEN cspF_sym] lemmas cspF_Rep_int_choice_empty = cspF_Rep_int_choice_DIV lemma cspF_DIV_top: "P <=F DIV" apply (simp add: cspF_semantics) apply (simp add: traces_def failures_def) done (*-----------------------------------* | !!-unit | *-----------------------------------*) lemma cspF_Rep_int_choice_sum_unit: "sumset C ~= {} ==> !! c:C .. P =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_unit) apply (rule order_antisym) apply (rule, simp add: in_failures) apply (rule, simp add: in_failures) apply (force) done lemma cspF_Rep_int_choice_nat_unit: "N ~= {} ==> !nat n:N .. P =F[M,M] P" by (simp add: Rep_int_choice_ss_def cspF_Rep_int_choice_sum_unit) lemma cspF_Rep_int_choice_set_unit: "Xs ~= {} ==> !set X:Xs .. P =F[M,M] P" by (simp add: Rep_int_choice_ss_def cspF_Rep_int_choice_sum_unit) lemma cspF_Rep_int_choice_com_unit: "X ~= {} ==> ! a:X .. P =F[M,M] P" by (simp add: Rep_int_choice_com_def cspF_Rep_int_choice_set_unit) lemma cspF_Rep_int_choice_f_unit: "X ~= {} ==> !<f> a:X .. P =F[M,M] P" by (simp add: Rep_int_choice_f_def cspF_Rep_int_choice_com_unit) lemmas cspF_Rep_int_choice_unit = cspF_Rep_int_choice_sum_unit cspF_Rep_int_choice_nat_unit cspF_Rep_int_choice_set_unit cspF_Rep_int_choice_com_unit cspF_Rep_int_choice_f_unit (*-----------------------------------* | !!-const | *-----------------------------------*) (* const *) lemma cspF_Rep_int_choice_sum_const: "[| sumset C ~= {} ; ALL c: sumset C. Pf c = P |] ==> !! :C .. Pf =F[M,M] P" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_const) apply (rule order_antisym) apply (rule, simp add: in_failures) apply (rule, simp add: in_failures) apply (force) done lemma cspF_Rep_int_choice_nat_const: "[| N ~= {} ; ALL n:N. Pf n = P |] ==> !nat :N .. Pf =F[M,M] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_const, auto) lemma cspF_Rep_int_choice_set_const: "[| Xs ~= {} ; ALL X:Xs. Pf X = P |] ==> !set :Xs .. Pf =F[M,M] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_const, auto) lemma cspF_Rep_int_choice_com_const: "[| X ~= {} ; ALL a:X. Pf a = P |] ==> ! :X .. Pf =F[M,M] P" apply (simp add: Rep_int_choice_com_def) by (rule cspF_Rep_int_choice_set_const, auto) lemma cspF_Rep_int_choice_f_const: "[| inj f ; X ~= {} ; ALL a:X. Pf a = P |] ==> !<f> :X .. Pf =F[M,M] P" apply (simp add: Rep_int_choice_f_def) by (rule cspF_Rep_int_choice_com_const, auto) lemmas cspF_Rep_int_choice_const = cspF_Rep_int_choice_sum_const cspF_Rep_int_choice_nat_const cspF_Rep_int_choice_set_const cspF_Rep_int_choice_com_const cspF_Rep_int_choice_f_const (*-----------------------------------* | |~|-!!-union | *-----------------------------------*) lemma cspF_Int_Rep_int_choice_sum_union: "C1 =type= C2 ==> (!! :C1 .. P1f) |~| (!! :C2 .. P2f) =F[M,M] (!! c:(C1 Uns C2) .. IF (c : sumset C1 & c : sumset C2) THEN (P1f c |~| P2f c) ELSE IF (c : sumset C1) THEN P1f c ELSE P2f c)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_Rep_int_choice_union) apply (rule order_antisym) apply (rule) apply (simp add: in_failures) apply (elim conjE bexE disjE) apply (rule_tac x="c" in bexI) apply (simp) apply (simp) apply (rule_tac x="c" in bexI) apply (simp) apply (simp) (* => *) apply (rule) apply (simp add: in_failures) apply (elim conjE exE bexE) apply (simp_all) apply (elim disjE) apply (simp_all) apply (case_tac "c : sumset C2") apply (simp add: in_failures) apply (force) apply (simp add: in_failures) apply (force) apply (case_tac "c : sumset C1") apply (simp add: in_failures) apply (force) apply (simp add: in_failures) apply (force) done lemma cspF_Int_Rep_int_choice_nat_union: "(!nat :N1 .. P1f) |~| (!nat :N2 .. P2f) =F[M,M] (!nat n:(N1 Un N2) .. IF (n : N1 & n : N2) THEN (P1f n |~| P2f n) ELSE IF (n : N1) THEN P1f n ELSE P2f n)" apply (simp add: Rep_int_choice_ss_def) apply (rule cspF_rw_left) apply (rule cspF_Int_Rep_int_choice_sum_union) apply (simp_all) apply (rule cspF_decompo) by (auto) lemma cspF_Int_Rep_int_choice_set_union: "(!set :Xs1 .. P1f) |~| (!set :Xs2 .. P2f) =F[M,M] (!set X:(Xs1 Un Xs2) .. IF (X : Xs1 & X : Xs2) THEN (P1f X |~| P2f X) ELSE IF (X : Xs1) THEN P1f X ELSE P2f X)" apply (simp add: Rep_int_choice_ss_def) apply (rule cspF_rw_left) apply (rule cspF_Int_Rep_int_choice_sum_union) apply (simp_all) apply (rule cspF_decompo) by (auto) lemma cspF_Int_Rep_int_choice_com_union: "(! :X1 .. P1f) |~| (! :X2 .. P2f) =F[M,M] (! a:(X1 Un X2) .. IF (a : X1 & a : X2) THEN (P1f a |~| P2f a) ELSE IF (a : X1) THEN P1f a ELSE P2f a)" apply (simp add: Rep_int_choice_com_def) apply (rule cspF_rw_left) apply (rule cspF_Int_Rep_int_choice_set_union) apply (simp_all) apply (rule cspF_decompo) by (auto) lemma cspF_Int_Rep_int_choice_f_union: "inj f ==> (!<f> :X1 .. P1f) |~| (!<f> :X2 .. P2f) =F[M,M] (!<f> a:(X1 Un X2) .. IF (a : X1 & a : X2) THEN (P1f a |~| P2f a) ELSE IF (a : X1) THEN P1f a ELSE P2f a)" apply (simp add: Rep_int_choice_f_def) apply (rule cspF_rw_left) apply (rule cspF_Int_Rep_int_choice_com_union) apply (rule cspF_decompo) apply (auto simp add: inj_image_mem_iff) done lemmas cspF_Int_Rep_int_choice_union = cspF_Int_Rep_int_choice_sum_union cspF_Int_Rep_int_choice_nat_union cspF_Int_Rep_int_choice_set_union cspF_Int_Rep_int_choice_com_union cspF_Int_Rep_int_choice_f_union (*-----------------------------------* | !!-union-|~| | *-----------------------------------*) lemma cspF_Rep_int_choice_sum_union_Int: "C1 =type= C2 ==> (!! :(C1 Uns C2) .. Pf) =F[M,M] (!! c:C1 .. Pf c) |~| (!! c:C2 .. Pf c)" apply (rule cspF_rw_right) apply (rule cspF_Int_Rep_int_choice_union) apply (simp) apply (rule cspF_decompo) apply (simp) apply (rule cspF_rw_right) apply (rule cspF_IF_split) apply (simp) apply (simp add: cspF_idem[THEN cspF_sym]) apply (intro impI) apply (rule cspF_rw_right) apply (rule cspF_IF_split) apply (simp) done lemma cspF_Rep_int_choice_nat_union_Int: "(!nat :(N1 Un N2) .. Pf) =F[M,M] (!nat n:N1 .. Pf n) |~| (!nat n:N2 .. Pf n)" apply (simp add: Rep_int_choice_ss_def) apply (rule cspF_rw_right) apply (rule cspF_Rep_int_choice_sum_union_Int[THEN cspF_sym]) apply (simp_all) done lemma cspF_Rep_int_choice_set_union_Int: "(!set :(Xs1 Un Xs2) .. Pf) =F[M,M] (!set X:Xs1 .. Pf X) |~| (!set X:Xs2 .. Pf X)" apply (simp add: Rep_int_choice_ss_def) apply (rule cspF_rw_right) apply (rule cspF_Rep_int_choice_sum_union_Int[THEN cspF_sym]) apply (simp_all) done lemma cspF_Rep_int_choice_com_union_Int: "(! :(X1 Un X2) .. Pf) =F[M,M] (! a:X1 .. Pf a) |~| (! a:X2 .. Pf a)" apply (simp add: Rep_int_choice_com_def) apply (rule cspF_rw_right) apply (rule cspF_Rep_int_choice_set_union_Int[THEN cspF_sym]) apply (rule cspF_decompo) apply (auto) done lemma cspF_Rep_int_choice_f_union_Int: "(!<f> :(X1 Un X2) .. Pf) =F[M,M] (!<f> x:X1 .. Pf x) |~| (!<f> x:X2 .. Pf x)" apply (simp add: Rep_int_choice_f_def) apply (rule cspF_rw_right) apply (rule cspF_Rep_int_choice_com_union_Int[THEN cspF_sym]) apply (rule cspF_decompo) apply (auto) done lemmas cspF_Rep_int_choice_union_Int = cspF_Rep_int_choice_sum_union_Int cspF_Rep_int_choice_nat_union_Int cspF_Rep_int_choice_set_union_Int cspF_Rep_int_choice_com_union_Int cspF_Rep_int_choice_f_union_Int (********************************************************* Depth_rest *********************************************************) (*------------------* | csp law | *------------------*) lemma cspF_Depth_rest_Zero: "P |. 0 =F[M1,M2] DIV" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Depth_rest_Zero) apply (rule order_antisym) (* => *) apply (rule) apply (simp add: in_failures) apply (force) (* <= *) apply (rule) apply (simp add: in_failures) done lemma cspF_Depth_rest_min: "P |. n |. m =F[M,M] P |. min n m" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Depth_rest_min) apply (simp add: failures.simps) apply (simp add: min_rs) done lemma cspF_Depth_rest_congE: "[| P =F[M1,M2] Q ; ALL m. P |. m =F[M1,M2] Q |. m ==> S |] ==> S" apply (simp add: cspF_semantics) apply (simp add: traces.simps) apply (simp add: failures.simps) done lemma cspF_Depth_rest_n: "P |. n |. n =F[M,M] P |. n" apply (rule cspF_rw_left) apply (rule cspF_Depth_rest_min) apply (simp) done (*------------------* | !nat-rest | *------------------*) lemma cspF_nat_Depth_rest_UNIV: "P =F[M,M] !nat n .. (P |. n)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_nat_Depth_rest_UNIV) apply (rule order_antisym) (* <= *) apply (rule) apply (simp add: in_failures) apply (case_tac "noTick s") apply (rule_tac x="Suc (lengtht s)" in exI) apply (simp) apply (rule_tac x="lengtht s" in exI) apply (simp) apply (rule_tac x="(butlastt s)" in exI) apply (simp add: Tick_decompo) apply (simp add: noTick_butlast) (* => *) apply (rule) apply (simp add: in_failures) done lemma cspF_nat_Depth_rest_lengthset: "P =F[M,M] !nat n:(lengthset P (fstF o M)) .. (P |. n)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_nat_Depth_rest_lengthset) apply (rule order_antisym) (* <= *) apply (rule) apply (simp add: in_failures) apply (case_tac "noTick s") apply (rule_tac x="Suc (lengtht s)" in bexI) apply (simp) apply (simp add: lengthset_def) apply (rule_tac x="s" in exI) apply (simp add: proc_T2) apply (rule_tac x="lengtht s" in bexI) apply (simp) apply (rule_tac x="(butlastt s)" in exI) apply (simp add: Tick_decompo) apply (simp add: noTick_butlast) apply (simp add: lengthset_def) apply (rule_tac x="s" in exI) apply (simp add: proc_T2) (* => *) apply (rule) apply (simp add: in_failures) done lemmas cspF_nat_Depth_rest = cspF_nat_Depth_rest_UNIV cspF_nat_Depth_rest_lengthset (*------------------* | ?-partial | *------------------*) lemma cspF_Ext_pre_choice_partial: "? :X -> Pf =F[M,M] ? x:X -> (IF (x:X) THEN Pf x ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done (*------------------* | !!-partial | *------------------*) lemma cspF_Rep_int_choice_sum_partial: "!! :C .. Pf =F[M,M] !! c:C .. (IF (c: sumset C) THEN Pf c ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done lemma cspF_Rep_int_choice_nat_partial: "!nat :N .. Pf =F[M,M] !nat n:N .. (IF (n:N) THEN Pf n ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done lemma cspF_Rep_int_choice_set_partial: "!set :Xs .. Pf =F[M,M] !set X:Xs .. (IF (X:Xs) THEN Pf X ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done lemma cspF_Rep_int_choice_com_partial: "! :X .. Pf =F[M,M] ! a:X .. (IF (a:X) THEN Pf a ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done lemma cspF_Rep_int_choice_f_partial: "inj f ==> !<f> :X .. Pf =F[M,M] !<f> a:X .. (IF (a:X) THEN Pf a ELSE DIV)" apply (rule cspF_decompo) apply (simp_all) apply (rule cspF_rw_right) apply (rule cspF_IF) apply (simp) done lemmas cspF_Rep_int_choice_partial = cspF_Rep_int_choice_sum_partial cspF_Rep_int_choice_nat_partial cspF_Rep_int_choice_set_partial cspF_Rep_int_choice_com_partial cspF_Rep_int_choice_f_partial (* =================================================== * | addition for CSP-Prover 5 | * =================================================== *) (* --------------------------------------------------- * unfold only the first Sending and Receiving * --------------------------------------------------- *) lemma cspF_first_Send_prefix: "a ! v -> P =F[M,M] a v -> P" by (simp add: csp_prefix_ss_def) lemma cspF_first_Rec_prefix: "a ? x:X -> Pf x =F[M,M] ? : (a ` X) -> (%x. (Pf ((inv a) x)))" by (simp add: csp_prefix_ss_def) lemma cspF_first_Int_pre_choice: "! :X -> Pf =F[M,M] ! :X .. (%x. x -> (Pf x))" by (simp add: csp_prefix_ss_def) lemma cspF_first_Nondet_send_prefix: "a !? x:X -> Pf x =F[M,M] ! :(a ` X) -> (%x. (Pf ((inv a) x)))" by (simp add: csp_prefix_ss_def) lemmas cspF_first_prefix_ss = cspF_first_Send_prefix cspF_first_Rec_prefix cspF_first_Int_pre_choice cspF_first_Nondet_send_prefix (* --------------------------------------------------- * Associativity of Sequential composition * --------------------------------------------------- *) lemma cspF_Seq_compo_assoc: "(P ;; Q) ;; R =F[M,M] P ;; (Q ;; R)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Seq_compo_assoc) apply (rule order_antisym) apply (rule) apply (simp add: in_traces in_failures) apply (elim disjE conjE exE) apply (force) apply (rule disjI2) apply (simp) apply (rule_tac x="sa" in exI) apply (rule_tac x="t" in exI) apply (simp) apply (subgoal_tac "noTick (sa ^^^ <Tick>)") apply (rotate_tac 3) apply (erule rem_asmE) apply (simp) apply (simp) apply (simp) apply (rule disjI2) apply (simp add: appt_decompo) apply (elim disjE conjE exE) apply (simp) apply (elim disjE conjE exE) apply (simp) apply (simp) apply (rule_tac x="sb" in exI) apply (rule_tac x="t" in exI) apply (simp) apply (rule disjI2) apply (rule_tac x="<>" in exI) apply (rule_tac x="t" in exI) apply (simp) apply (simp) apply (rotate_tac -2) apply (drule sym) apply (simp) apply (rotate_tac -2) apply (drule sym) apply (simp) apply (simp) apply (rule_tac x="sb" in exI) apply (rule_tac x="u ^^^ t" in exI) apply (simp add: appt_assoc) apply (rule disjI2) apply (rule_tac x="u" in exI) apply (rule_tac x="t" in exI) apply (simp) (* => *) apply (rule) apply (simp add: in_traces in_failures) apply (elim disjE conjE exE) apply (simp) apply (rule disjI1) apply (simp) apply (rule disjI2) apply (rule_tac x="sa" in exI) apply (rule_tac x="t" in exI) apply (simp) apply (rule disjI2) apply (rule_tac x="sa ^^^ sb" in exI) apply (rule_tac x="ta" in exI) apply (simp add: appt_assoc) apply (rule disjI2) apply (rule_tac x="sa" in exI) apply (rule_tac x="sb ^^^ <Tick>" in exI) apply (simp) done lemma cspF_Seq_compo_assoc_sym: "P ;; (Q ;; R) =F[M,M] (P ;; Q) ;; R" apply (rule cspF_sym) apply (simp add: cspF_Seq_compo_assoc) done (* ---------------------------------------------- * decompose right internal choice * ---------------------------------------------- *) lemma cspF_Int_choice_eq_right: "[| P =F[M1,M2] Q1 ; P =F[M1,M2] Q2 |] ==> P =F[M1,M2] Q1 |~| Q2" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Int_choice_eq_right) apply (rule order_antisym) apply (rule) apply (simp add: in_failures) apply (rule) apply (simp add: in_failures) done (* -------- right -------- *) lemma cspF_Rep_int_choice_sum_eq_right_ALL: "[| sumset C ~= {} ; ALL c : (sumset C). P =F[M1,M2] Qf c |] ==> P =F[M1,M2] !! :C .. Qf" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_sum_eq_right_ALL) apply (rule order_antisym) apply (rule) apply (simp add: in_failures) apply (subgoal_tac "EX c. c: sumset C") apply (erule exE) apply (drule_tac x="c" in bspec, simp) apply (erule conjE) apply (erule order_antisymE) apply (erule subsetFE_ALL) apply (drule_tac x="s" in spec) apply (drule_tac x="X" in spec) apply (simp) apply (fast) apply (fast) apply (rule) apply (simp add: in_failures) apply (erule bexE) apply (drule_tac x="c" in bspec, simp) apply (erule conjE) apply (erule order_antisymE) apply (rotate_tac -1) apply (erule subsetFE_ALL) apply (drule_tac x="s" in spec) apply (drule_tac x="X" in spec) apply (simp) done lemma cspF_Rep_int_choice_sum_eq_right: "[| sumset C ~= {} ; !! c. c : (sumset C) ==> P =F[M1,M2] Qf c |] ==> P =F[M1,M2] !! :C .. Qf" by (simp add: cspF_Rep_int_choice_sum_eq_right_ALL) (* nat *) lemma cspF_Rep_int_choice_nat_eq_right: "[| N ~= {} ; !! n. n : N ==> P =F[M1,M2] Qf n |] ==> P =F[M1,M2] !nat :N .. Qf" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_right, auto) lemma cspF_Rep_int_choice_set_eq_right: "[| Xs ~= {} ; !! X. X : Xs ==> P =F[M1,M2] Qf X |] ==> P =F[M1,M2] !set :Xs .. Qf" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_right, auto) lemma cspF_Rep_int_choice_com_eq_right: "[| X ~= {} ; !! a. a:X ==> P =F[M1,M2] Qf a |] ==> P =F[M1,M2] ! :X .. Qf" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_right, auto) lemma cspF_Rep_int_choice_f_eq_right: "[| inj f ; X ~= {} ; !! a. a:X ==> P =F[M1,M2] Qf a |] ==> P =F[M1,M2] !<f> :X .. Qf" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_right, auto) lemmas cspF_int_eq_right = cspF_Rep_int_choice_sum_eq_right cspF_Rep_int_choice_nat_eq_right cspF_Rep_int_choice_set_eq_right cspF_Rep_int_choice_com_eq_right cspF_Rep_int_choice_f_eq_right cspF_Int_choice_eq_right (* -------- left -------- *) lemma cspF_Int_choice_eq_left: "[| Q1 =F[M1,M2] P ; Q2 =F[M1,M2] P |] ==> Q1 |~| Q2 =F[M1,M2] P" apply (rule cspF_sym) apply (rule cspF_int_eq_right) apply (rule cspF_sym, simp) apply (rule cspF_sym, simp) done lemma cspF_Rep_int_choice_sum_eq_left: "[| sumset C ~= {} ; !! c. c : (sumset C) ==> Qf c =F[M1,M2] P |] ==> !! :C .. Qf =F[M1,M2] P" apply (rule cspF_sym, rule cspF_int_eq_right, simp) apply (rule cspF_sym, simp) done lemma cspF_Rep_int_choice_nat_eq_left: "[| N ~= {} ; !! n. n : N ==> Qf n =F[M1,M2] P |] ==> !nat :N .. Qf =F[M1,M2] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_left, auto) lemma cspF_Rep_int_choice_set_eq_left: "[| Xs ~= {} ; !! X. X : Xs ==> Qf X =F[M1,M2] P |] ==> !set :Xs .. Qf =F[M1,M2] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_left, auto) lemma cspF_Rep_int_choice_com_eq_left: "[| X ~= {} ; !! a. a:X ==> Qf a =F[M1,M2] P |] ==> ! :X .. Qf =F[M1,M2] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_left, auto) lemma cspF_Rep_int_choice_f_eq_left: "[| inj f ; X ~= {} ; !! a. a:X ==> Qf a =F[M1,M2] P |] ==> !<f> :X .. Qf =F[M1,M2] P" apply (simp add: Rep_int_choice_ss_def) by (rule cspF_Rep_int_choice_sum_eq_left, auto) lemmas cspF_int_eq_left = cspF_Rep_int_choice_sum_eq_left cspF_Rep_int_choice_nat_eq_left cspF_Rep_int_choice_set_eq_left cspF_Rep_int_choice_com_eq_left cspF_Rep_int_choice_f_eq_left cspF_Int_choice_eq_left (* ---------------------------------------------- * replicated internal choice -> binary ... * ---------------------------------------------- *) (* ---- Un ---- *) (* nat *) lemma cspF_Rep_int_choice_nat_Un: "!nat n:(N1 Un N2) .. Pf n =F[M,M] !nat n:N1 .. Pf n |~| !nat n:N2 .. Pf n" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_nat_Un) apply (rule order_antisym) apply (auto simp add: in_failures) done (* set *) lemma cspF_Rep_int_choice_set_Un: "!set X:(Xs1 Un Xs2) .. Pf X =F[M,M] !set X:Xs2 .. Pf X |~| !set X:Xs1 .. Pf X" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_set_Un) apply (rule order_antisym) apply (auto simp add: in_failures) done (* com *) lemma cspF_Rep_int_choice_com_Un: "! x:(X1 Un X2) .. Pf x =F[M,M] ! x:X1 .. Pf x |~| ! x:X2 .. Pf x" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_com_Un) apply (rule order_antisym) apply (auto simp add: in_failures) done (* f *) lemma cspF_Rep_int_choice_f_Un: "inj f ==> !<f> x:(X1 Un X2) .. Pf x =F[M,M] !<f> x:X1 .. Pf x |~| !<f> x:X2 .. Pf x" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_f_Un) apply (rule order_antisym) apply (auto simp add: in_failures) done lemmas cspF_Rep_int_choice_Un = cspF_Rep_int_choice_nat_Un cspF_Rep_int_choice_set_Un cspF_Rep_int_choice_com_Un cspF_Rep_int_choice_f_Un (* ---- insert ---- *) (* nat *) lemma cspF_Rep_int_choice_nat_insert: "!nat n:(insert m N) .. Pf n =F[M,M] Pf m |~| !nat n:N .. Pf n" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_nat_insert) apply (rule order_antisym) apply (auto simp add: in_failures) done (* set *) lemma cspF_Rep_int_choice_set_insert: "!set X:(insert Y Xs) .. Pf X =F[M,M] Pf Y |~| !set X:Xs .. Pf X" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_set_insert) apply (rule order_antisym) apply (auto simp add: in_failures) done (* com *) lemma cspF_Rep_int_choice_com_insert: "! x:(insert a X) .. Pf x =F[M,M] Pf a |~| ! x:X .. Pf x" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_com_insert) apply (rule order_antisym) apply (auto simp add: in_failures) done (* f *) lemma cspF_Rep_int_choice_f_insert: "inj f ==> !<f> x:(insert a X) .. Pf x =F[M,M] Pf a |~| !<f> x:X .. Pf x" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_f_insert) apply (rule order_antisym) apply (auto simp add: in_failures) done lemmas cspF_Rep_int_choice_insert = cspF_Rep_int_choice_nat_insert cspF_Rep_int_choice_set_insert cspF_Rep_int_choice_com_insert cspF_Rep_int_choice_f_insert lemmas cspF_Rep_int_choice_sepa = cspF_Rep_int_choice_insert cspF_Rep_int_choice_Un (* ---------------------------------------------- * simplify replicated internal choice * ---------------------------------------------- *) lemma cspF_Rep_int_choice_com_map_f: "inj f ==> ! x:(f ` X) .. Pf x =F[M,M] !<f> x:X .. Pf (f x)" apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_com_map_f) apply (rule order_antisym) apply (auto simp add: in_failures) done lemma cspF_Rep_int_choice_f_map_f: "[| inj f ; inj g |] ==> !<f> x:(g ` X) .. Pf x =F[M,M] !<f o g> x:X .. Pf (g x)" apply (subgoal_tac "inj (f o g)") apply (simp add: cspF_cspT_semantics) apply (simp add: cspT_Rep_int_choice_f_map_f) apply (rule order_antisym) apply (auto simp add: in_failures) apply (auto simp add: inj_on_def) done lemmas cspF_Rep_int_choice_f_map = cspF_Rep_int_choice_com_map_f cspF_Rep_int_choice_f_map_f end