Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T
theory CSP_T_contraction(*-------------------------------------------* | CSP-Prover on Isabelle2004 | | December 2004 | | July 2005 (modified) | | August 2005 (modified) | | | | CSP-Prover on Isabelle2005 | | October 2005 (modified) | | November 2005 (modified) | | | | Yoshinao Isobe (AIST JAPAN) | *-------------------------------------------*) theory CSP_T_contraction = CSP_T_tracesfun + RS_prod: (***************************************************************** 1. contraction tracesfun 2. contraction tracesFun 3. contraction [[ ]]Tfun 4. contraction [[ ]]TFun *****************************************************************) (*============================================* | gSKIP | *============================================*) lemma gSKIP_to_Tick_notin_traces: "Pf : gSKIPfun ==> <Tick> ~:t traces (Pf f)" apply (rule gSKIPfun.induct[of Pf]) apply (simp_all add: in_traces) apply (rule impI) apply (elim conjE disjE) apply (simp_all) apply (rule conjI) apply (intro allI impI) apply (erule noTick_rmTickE) apply (simp) apply (auto) done lemma ALL_gSKIP_to_Tick_notin_traces: "ALL Pf f. Pf : gSKIPfun --> <Tick> ~:t traces (Pf f)" by (simp add: gSKIP_to_Tick_notin_traces) (*--------------------------------* | STOP,SKIP,DIV | *--------------------------------*) (*** Constant_contraction ***) lemma map_alpha_Constant: "0 <= alpha ==> map_alpha (%f. P) alpha" apply (simp add: map_alpha_def) apply (simp add: real_mult_order_eq) done (*** non_expanding_Constant ***) lemma non_expanding_Constant: "non_expanding (%f. P)" by (simp add: non_expanding_def map_alpha_Constant) (*** Constant_contraction_alpha ***) lemma contraction_alpha_Constant: "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (%x. P) alpha" by (simp add: contraction_alpha_def map_alpha_Constant) (*** STOP ***) lemma map_alpha_tracesfun_STOP: "0 <= alpha ==> map_alpha (tracesfun (%f. STOP)) alpha" by (simp add: tracesfun_simp map_alpha_Constant) lemma non_expanding_tracesfun_STOP: "non_expanding (tracesfun (%f. STOP))" by (simp add: non_expanding_def map_alpha_tracesfun_STOP) lemma contraction_alpha_tracesfun_STOP: "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. STOP)) alpha" by (simp add: tracesfun_simp contraction_alpha_Constant) (*** SKIP ***) lemma map_alpha_tracesfun_SKIP: "0 <= alpha ==> map_alpha (tracesfun (%f. SKIP)) alpha" by (simp add: tracesfun_simp map_alpha_Constant) lemma non_expanding_tracesfun_SKIP: "non_expanding (tracesfun (%f. SKIP))" by (simp add: non_expanding_def map_alpha_tracesfun_SKIP) lemma contraction_alpha_tracesfun_SKIP: "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. SKIP)) alpha" by (simp add: tracesfun_simp contraction_alpha_Constant) (*** DIV ***) lemma map_alpha_tracesfun_DIV: "0 <= alpha ==> map_alpha (tracesfun (%f. DIV)) alpha" by (simp add: tracesfun_simp map_alpha_Constant) lemma non_expanding_tracesfun_DIV: "non_expanding (tracesfun (%f. DIV))" by (simp add: non_expanding_def map_alpha_tracesfun_DIV) lemma contraction_alpha_tracesfun_DIV: "[| 0 <= alpha ; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. DIV)) alpha" by (simp add: tracesfun_simp contraction_alpha_Constant) (*--------------------------------* | Act_prefix | *--------------------------------*) lemma contraction_half_traces_Act_prefix_lm: "distance (traces (a -> P), traces (a -> Q)) * 2 = distance (traces P, traces Q)" apply (rule sym) apply (rule rest_Suc_dist_half[simplified]) apply (rule allI) apply (simp add: rest_domT_eq_iff) apply (rule iffI) (* => *) apply (rule allI) apply (simp add: in_traces) apply (rule iffI) (* => *) apply (elim conjE exE disjE, simp) apply (drule_tac x="sa" in spec) apply (simp) (* <= *) apply (elim conjE exE disjE, simp) apply (drule_tac x="sa" in spec) apply (simp) (* <= *) apply (rule allI) apply (drule_tac x="<Ev a> ^^ s" in spec) apply (simp add: in_traces) done (*** contraction_half ***) lemma contraction_half_tracesfun_Act_prefix: "non_expanding (tracesfun Pf) ==> contraction_alpha (tracesfun (%f. a -> Pf f)) (1 / 2)" apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def) apply (intro allI) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) apply (simp add: contraction_half_traces_Act_prefix_lm) done (*** contraction ***) lemma contraction_tracesfun_Act_prefix: "non_expanding (tracesfun Pf) ==> contraction (tracesfun (%f. a -> Pf f))" apply (simp add: contraction_def) apply (rule_tac x="1/2" in exI) by (simp add: contraction_half_tracesfun_Act_prefix) (*** non_expanding ***) lemma non_expanding_tracesfun_Act_prefix: "non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. a -> Pf f))" apply (rule contraction_non_expanding) by (simp add: contraction_tracesfun_Act_prefix) (*--------------------------------* | Ext_pre_choice | *--------------------------------*) (*** rest_domT (subset) ***) lemma Ext_pre_choice_Act_prefix_rest_domT_sub: "[| ALL a : X. traces (a -> Pf a) .|. n <= traces (a -> Qf a) .|. n |] ==> traces (? a:X -> Pf a) .|. n <= traces (? a:X -> Qf a) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) apply (elim conjE exE disjE) apply (simp_all) apply (drule_tac x="a" in bspec, simp) apply (drule_tac x="t" in spec) apply (simp add: in_traces) done (*** rest_domT (equal) ***) lemma Ext_pre_choice_Act_prefix_rest_domT: "[| ALL a : X. traces (a -> Pf a) .|. n = traces (a -> Qf a) .|. n |] ==> traces (? a:X -> Pf a) .|. n = traces (? a:X -> Qf a) .|. n" apply (rule order_antisym) by (simp_all add: Ext_pre_choice_Act_prefix_rest_domT_sub) (*** distT lemma ***) lemma Ext_pre_choice_Act_prefix_distT_nonempty: "[| X ~= {} ; PQs = {(traces (a -> Pf a), traces (a -> Qf a))|a. a : X} |] ==> (EX PQ. PQ:PQs & distance(traces (? a:X -> Pf a), traces (? a:X -> Qf a)) <= distance(fst PQ, snd PQ))" apply (rule rest_to_dist_pair) apply (force) apply (intro allI impI) apply (rule Ext_pre_choice_Act_prefix_rest_domT) apply (rule ballI) apply (simp) apply (drule_tac x="traces (a -> Pf a)" in spec) apply (drule_tac x="traces (a -> Qf a)" in spec) by (auto) (*** contraction lemma ***) lemma contraction_half_tracesfun_Ext_pre_choice_lm: "[| X ~= {} ; ALL a. distance (traces (Pf a), traces (Qf a)) <= distance (x1, x2) |] ==> distance (traces (? a:X -> Pf a), traces (? a:X -> Qf a)) * 2 <= distance (x1, x2)" apply (insert Ext_pre_choice_Act_prefix_distT_nonempty [of X "{(traces (a -> Pf a), traces (a -> Qf a)) |a. a : X}" Pf Qf]) apply (simp) apply (elim conjE exE) apply (simp) apply (subgoal_tac "distance (traces (aa -> Pf aa), traces (aa -> Qf aa)) * 2 = distance (traces (Pf aa), traces (Qf aa))") apply (drule_tac x="aa" in spec) apply (force) by (simp add: contraction_half_traces_Act_prefix_lm) (*** contraction_half ***) lemma contraction_half_tracesfun_Ext_pre_choice: "ALL a. non_expanding (tracesfun (Pff a)) ==> contraction_alpha (tracesfun (%f. ? a:X -> (Pff a f))) (1 / 2)" apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def) apply (case_tac "X = {}") apply (simp add: tracesfun_simp) apply (simp add: tracesfun_def) by (simp add: contraction_half_tracesfun_Ext_pre_choice_lm) (*** Ext_pre_choice_evalT_contraction ***) lemma contraction_tracesfun_Ext_pre_choice: "ALL a. non_expanding (tracesfun (Pff a)) ==> contraction (tracesfun (%f. ? a:X -> (Pff a f)))" apply (simp add: contraction_def) apply (rule_tac x="1/2" in exI) by (simp add: contraction_half_tracesfun_Ext_pre_choice) (*** Ext_pre_choice_evalT_non_expanding ***) lemma non_expanding_tracesfun_Ext_pre_choice: "ALL a. non_expanding (tracesfun (Pff a)) ==> non_expanding (tracesfun (%f. ? a:X -> (Pff a f)))" apply (rule contraction_non_expanding) by (simp add: contraction_tracesfun_Ext_pre_choice) (*--------------------------------* | Ext_choice | *--------------------------------*) (*** rest_domT (subset) ***) lemma Ext_choice_rest_domT_sub: "[| traces P1 .|. n <= traces P2 .|. n ; traces Q1 .|. n <= traces Q2 .|. n |] ==> traces (P1 [+] Q1) .|. n <= traces (P2 [+] Q2) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) by (auto) (*** rest_domT (equal) ***) lemma Ext_choice_rest_domT: "[| traces P1 .|. n = traces P2 .|. n ; traces Q1 .|. n = traces Q2 .|. n |] ==> traces (P1 [+] Q1) .|. n = traces (P2 [+] Q2) .|. n" apply (rule order_antisym) by (simp_all add: Ext_choice_rest_domT_sub) (*** distT lemma ***) lemma Ext_choice_distT: "PQs = {(traces P1, traces P2), (traces Q1, traces Q2)} ==> (EX PQ. PQ:PQs & distance(traces (P1 [+] Q1), traces (P2 [+] Q2)) <= distance((fst PQ), (snd PQ)))" apply (rule rest_to_dist_pair) by (auto intro: Ext_choice_rest_domT) (*** map_alpha T lemma ***) lemma map_alpha_tracesfun_Ext_choice_lm: "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ; distance (traces Q1, traces Q2) <= alpha * distance (x1, x2) |] ==> distance (traces (P1 [+] Q1), traces (P2 [+] Q2)) <= alpha * distance (x1, x2)" apply (insert Ext_choice_distT [of "{(traces P1, traces P2), (traces Q1, traces Q2)}" P1 P2 Q1 Q2]) by (auto) (*** map_alpha ***) lemma map_alpha_tracesfun_Ext_choice: "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. (Pf f [+] Qf f))) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_tracesfun_Ext_choice_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_Ext_choice: "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. (Pf f [+] Qf f)))" by (simp add: non_expanding_def map_alpha_tracesfun_Ext_choice) (*** contraction ***) lemma contraction_alpha_tracesfun_Ext_choice: "[| contraction_alpha (tracesfun Pf) alpha ; contraction_alpha (tracesfun Qf) alpha|] ==> contraction_alpha (tracesfun (%f. (Pf f [+] Qf f))) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_Ext_choice) (*--------------------------------* | Int_choice | *--------------------------------*) (*** map_alpha ***) lemma map_alpha_tracesfun_Int_choice: "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. (Pf f |~| Qf f))) alpha" by (simp add: map_alpha_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice) (*** non_expanding ***) lemma non_expanding_tracesfun_Int_choice: "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. (Pf f |~| Qf f)))" by (simp add: non_expanding_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice) (*** contraction ***) lemma contraction_alpha_tracesfun_Int_choice: "[| contraction_alpha (tracesfun Pf) alpha ; contraction_alpha (tracesfun Qf) alpha|] ==> contraction_alpha (tracesfun (%f. (Pf f |~| Qf f))) alpha" by (simp add: contraction_alpha_tracesfun_Ext_choice tracesfun_Int_choice_Ext_choice) (*--------------------------------* | Rep_int_choice | *--------------------------------*) (*** rest_domT (subset) ***) lemma Rep_int_choice_rest_domT_sub: "[| ALL c : C. traces (Pf c) .|. n <= traces (Qf c) .|. n |] ==> traces (!! :C .. Pf) .|. n <= traces (!! :C .. Qf) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) by (auto) (*** rest_domT (equal) ***) lemma Rep_int_choice_rest_domT: "[| ALL c : C. traces (Pf c) .|. n = traces (Qf c) .|. n |] ==> traces (!! :C .. Pf) .|. n = traces (!! :C .. Qf) .|. n" apply (rule order_antisym) by (simp_all add: Rep_int_choice_rest_domT_sub) (*** distT lemma ***) lemma Rep_int_choice_distT_nonempty: "[| C ~= {} ; PQs = {(traces (Pf c), traces (Qf c))|c. c : C} |] ==> (EX PQ. PQ:PQs & distance(traces (!! :C .. Pf), traces (!! :C .. Qf)) <= distance(fst PQ, snd PQ))" apply (rule rest_to_dist_pair) apply (fast) apply (intro allI impI) apply (rule Rep_int_choice_rest_domT) by (auto) (*** map_alpha T lemma ***) lemma map_alpha_tracesfun_Rep_int_choice_lm: "[| C ~= {} ; ALL c. distance (traces (Pf c), traces (Qf c)) <= alpha * distance (x1, x2) |] ==> distance(traces (!! :C .. Pf), traces (!! :C .. Qf)) <= alpha * distance(x1, x2)" apply (insert Rep_int_choice_distT_nonempty [of C "{(traces (Pf c), traces (Qf c))|c. c : C}" Pf Qf]) apply (simp) apply (elim conjE exE, simp) apply (drule_tac x="c" in spec) by (force) (*** map_alpha ***) lemma map_alpha_tracesfun_Rep_int_choice: "ALL c. map_alpha (tracesfun (Pff c)) alpha ==> map_alpha (tracesfun (%f. !! c:C .. (Pff c f))) alpha" apply (simp add: map_alpha_def) apply (case_tac "C = {}") apply (simp add: tracesfun_simp) apply (simp add: real_mult_order_eq) apply (simp add: tracesfun_def) apply (simp add: map_alpha_tracesfun_Rep_int_choice_lm) done (*** non_expanding ***) lemma non_expanding_tracesfun_Rep_int_choice: "ALL c. non_expanding (tracesfun (Pff c)) ==> non_expanding (tracesfun (%f. !! c:C .. (Pff c f)))" by (simp add: non_expanding_def map_alpha_tracesfun_Rep_int_choice) (*** Rep_int_choice_evalT_contraction_alpha ***) lemma contraction_alpha_tracesfun_Rep_int_choice: "ALL c. contraction_alpha (tracesfun (Pff c)) alpha ==> contraction_alpha (tracesfun (%f. !! c:C .. (Pff c f))) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_Rep_int_choice) (*--------------------------------* | IF | *--------------------------------*) (*** rest_domT (subset) ***) lemma IF_rest_domT_sub: "[| traces P1 .|. n <= traces P2 .|. n ; traces Q1 .|. n <= traces Q2 .|. n |] ==> traces (IF b THEN P1 ELSE Q1) .|. n <= traces (IF b THEN P2 ELSE Q2) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) done (*** rest_domT (equal) ***) lemma IF_rest_domT: "[| traces P1 .|. n = traces P2 .|. n ; traces Q1 .|. n = traces Q2 .|. n |] ==> traces (IF b THEN P1 ELSE Q1) .|. n = traces (IF b THEN P2 ELSE Q2) .|. n" apply (rule order_antisym) by (simp_all add: IF_rest_domT_sub) (*** distT lemma ***) lemma IF_distT: "PQs = {(traces P1, traces P2), (traces Q1, traces Q2)} ==> (EX PQ. PQ:PQs & distance(traces (IF b THEN P1 ELSE Q1), traces (IF b THEN P2 ELSE Q2)) <= distance((fst PQ), (snd PQ)))" apply (rule rest_to_dist_pair) by (auto intro: IF_rest_domT) (*** map_alpha T lemma ***) lemma map_alpha_tracesfun_IF_lm: "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ; distance (traces Q1, traces Q2) <= alpha * distance (x1, x2) |] ==> distance(traces (IF b THEN P1 ELSE Q1), traces (IF b THEN P2 ELSE Q2)) <= alpha * distance (x1, x2)" apply (insert IF_distT [of "{(traces P1, traces P2), (traces Q1, traces Q2)}" P1 P2 Q1 Q2 b]) by (auto) (*** map_alpha ***) lemma map_alpha_tracesfun_IF: "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f))) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_tracesfun_IF_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_IF: "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f)))" by (simp add: non_expanding_def map_alpha_tracesfun_IF) (*** contraction_alpha ***) lemma contraction_alpha_tracesfun_IF: "[| contraction_alpha (tracesfun Pf) alpha ; contraction_alpha (tracesfun Qf) alpha|] ==> contraction_alpha (tracesfun (%f. IF b THEN (Pf f) ELSE (Qf f))) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_IF) (*--------------------------------* | Parallel | *--------------------------------*) (*** rest_domT (subset) ***) lemma Parallel_rest_domT_sub: "[| traces P1 .|. n <= traces P2 .|. n ; traces Q1 .|. n <= traces Q2 .|. n |] ==> traces (P1 |[X]| Q1) .|. n <= traces (P2 |[X]| Q2) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) apply (elim conjE exE) apply (rule_tac x="s" in exI) apply (rule_tac x="ta" in exI) apply (simp) apply (erule par_tr_lengthtE) by (auto) (*** rest_domT (equal) ***) lemma Parallel_rest_domT: "[| traces P1 .|. n = traces P2 .|. n ; traces Q1 .|. n = traces Q2 .|. n |] ==> traces (P1 |[X]| Q1) .|. n = traces (P2 |[X]| Q2) .|. n" apply (rule order_antisym) by (simp_all add: Parallel_rest_domT_sub) (*** distT lemma ***) lemma Parallel_distT: "PQs = {(traces P1, traces P2), (traces Q1, traces Q2)} ==> (EX PQ. PQ:PQs & distance(traces (P1 |[X]| Q1), traces (P2 |[X]| Q2)) <= distance((fst PQ), (snd PQ)))" apply (rule rest_to_dist_pair) by (auto intro: Parallel_rest_domT) (*** map_alpha T lemma ***) lemma map_alpha_tracesfun_Parallel_lm: "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ; distance (traces Q1, traces Q2) <= alpha * distance (x1, x2) |] ==> distance (traces (P1 |[X]| Q1), traces (P2 |[X]| Q2)) <= alpha * distance (x1, x2)" apply (insert Parallel_distT [of "{(traces P1, traces P2), (traces Q1, traces Q2)}" P1 P2 Q1 Q2 X]) by (auto) (*** map_alpha ***) lemma map_alpha_tracesfun_Parallel: "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. (Pf f |[X]| Qf f))) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_tracesfun_Parallel_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_Parallel: "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. (Pf f |[X]| Qf f)))" by (simp add: non_expanding_def map_alpha_tracesfun_Parallel) (*** contraction_alpha ***) lemma contraction_alpha_tracesfun_Parallel: "[| contraction_alpha (tracesfun Pf) alpha ; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. (Pf f |[X]| Qf f))) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_Parallel) (*--------------------------------* | Hiding | *--------------------------------*) (* cms rules for Hiding is not necessary because processes are guarded. *) (*--------------------------------* | Renaming | *--------------------------------*) (*** rest_domT (subset) ***) lemma Renaming_rest_domT_sub: "traces P .|. n <= traces Q .|. n ==> traces (P [[r]]) .|. n <= traces (Q [[r]]) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) apply (elim conjE exE) apply (rule_tac x="s" in exI) apply (drule_tac x="s" in spec) by (simp add: ren_tr_lengtht) (*** rest_domT (equal) ***) lemma Renaming_rest_domT: "traces P .|. n = traces Q .|. n ==> traces (P [[r]]) .|. n = traces (Q [[r]]) .|. n" apply (rule order_antisym) by (simp_all add: Renaming_rest_domT_sub) (*** distT lemma ***) lemma Renaming_distT: "distance(traces (P [[r]]), traces (Q [[r]])) <= distance(traces P, traces Q)" apply (rule rest_distance_subset) by (auto intro: Renaming_rest_domT) (*** map_alphaT lemma ***) lemma map_alpha_tracesfun_Renaming_lm: "distance(traces P, traces Q) <= alpha * distance (x1, x2) ==> distance(traces (P [[r]]), traces (Q [[r]])) <= alpha * distance(x1, x2)" apply (insert Renaming_distT[of P r Q]) by (simp) (*** map_alpha ***) lemma map_alpha_tracesfun_Renaming: "map_alpha (tracesfun Pf) alpha ==> map_alpha (tracesfun (%f. (Pf f) [[r]])) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_tracesfun_Renaming_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_Renaming: "non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. (Pf f) [[r]]))" by (simp add: non_expanding_def map_alpha_tracesfun_Renaming) (*** contraction_alpha ***) lemma contraction_alpha_tracesfun_Renaming: "contraction_alpha (tracesfun Pf) alpha ==> contraction_alpha (tracesfun (%f. (Pf f) [[r]])) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_Renaming) (*--------------------------------* | Seq_compo | *--------------------------------*) (*** rest_domT (subset) ***) lemma Seq_compo_rest_domT_sub: "[| traces P1 .|. n <= traces P2 .|. n ; traces Q1 .|. n <= traces Q2 .|. n |] ==> traces (P1 ;; Q1) .|. n <= traces (P2 ;; Q2) .|. n" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) apply (elim conjE exE disjE) (* case 1 *) apply (rule disjI1) apply (insert trace_last_noTick_or_Tick) apply (rotate_tac -1) apply (drule_tac x="s" in spec) apply (erule disjE) apply (rule_tac x="s" in exI, simp) apply (elim conjE exE) apply (rule_tac x="sa" in exI, simp) apply (drule_tac x="sa" in spec, simp) apply (drule mp) apply (rule memT_prefix_closed, simp_all, simp) (* case 2 *) apply (case_tac "~ noTick s", simp) apply (insert trace_last_nil_or_unnil) apply (rotate_tac -1) apply (drule_tac x="ta" in spec) apply (erule disjE) apply (rule disjI1) (* ta = []t *) apply (rule_tac x="s" in exI, simp) apply (drule_tac x="s" in spec, simp) apply (drule mp) apply (rule memT_prefix_closed, simp_all, simp) apply (rule disjI2) (* ta ~= []t *) apply (elim conjE exE, simp) apply (drule_tac x="s ^^ <Tick>" in spec) apply (drule_tac x=" sa ^^ <a>" in spec) apply (simp) apply (rule_tac x="s" in exI) apply (rule_tac x="sa ^^ <a>" in exI) apply (simp) done (*** rest_domT (equal) ***) lemma Seq_compo_rest_domT: "[| traces P1 .|. n = traces P2 .|. n ; traces Q1 .|. n = traces Q2 .|. n |] ==> traces (P1 ;; Q1) .|. n = traces (P2 ;; Q2) .|. n" apply (rule order_antisym) by (simp_all add: Seq_compo_rest_domT_sub) (*** distT lemma ***) lemma Seq_compo_distT: "PQs = {(traces P1, traces P2), (traces Q1, traces Q2)} ==> (EX PQ. PQ:PQs & distance(traces (P1 ;; Q1), traces (P2 ;; Q2)) <= distance((fst PQ), (snd PQ)))" apply (rule rest_to_dist_pair) by (auto intro: Seq_compo_rest_domT) (*** map_alpha T lemma ***) lemma map_alpha_transfun_Seq_compo_lm: "[| distance (traces P1, traces P2) <= alpha * distance (x1, x2) ; distance (traces Q1, traces Q2) <= alpha * distance (x1, x2) |] ==> distance (traces (P1 ;; Q1), traces (P2 ;; Q2)) <= alpha * distance (x1, x2)" apply (insert Seq_compo_distT [of "{(traces P1, traces P2), (traces Q1, traces Q2)}" P1 P2 Q1 Q2]) by (auto) (*** map_alpha ***) lemma map_alpha_transfun_Seq_compo: "[| map_alpha (tracesfun Pf) alpha ; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. (Pf f ;; Qf f))) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_transfun_Seq_compo_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_Seq_compo: "[| non_expanding (tracesfun Pf) ; non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. (Pf f ;; Qf f)))" by (simp add: non_expanding_def map_alpha_transfun_Seq_compo) (*** contraction_alpha ***) lemma contraction_alpha_tracesfun_Seq_compo: "[| contraction_alpha (tracesfun Pf) alpha ; contraction_alpha (tracesfun Qf) alpha|] ==> contraction_alpha (tracesfun (%f. (Pf f ;; Qf f))) alpha" by (simp add: contraction_alpha_def map_alpha_transfun_Seq_compo) (*--------------------------------* | Seq_compo (gSKIP) | *--------------------------------*) (*** rest_domT (subset) ***) lemma gSKIP_Seq_compo_rest_domT_sub: "[| traces P1 .|. (Suc n) <= traces P2 .|. (Suc n) ; traces Q1 .|. n <= traces Q2 .|. n ; <Tick> ~:t traces P1 ; <Tick> ~:t traces P2 |] ==> traces (P1 ;; Q1) .|. (Suc n) <= traces (P2 ;; Q2) .|. (Suc n)" apply (simp add: subdomT_iff) apply (intro allI impI) apply (simp add: in_rest_domT) apply (simp add: in_traces) apply (elim conjE exE disjE) (* case 1 *) apply (rule disjI1) apply (insert trace_last_noTick_or_Tick) apply (rotate_tac -1) apply (drule_tac x="s" in spec) apply (erule disjE) apply (rule_tac x="s" in exI, simp) apply (elim conjE exE) apply (rule_tac x="sa" in exI, simp) apply (drule_tac x="sa" in spec, simp) apply (drule mp) apply (rule memT_prefix_closed, simp_all, simp) (* case 2 *) apply (case_tac "~ noTick s", simp) apply (insert trace_last_nil_or_unnil) apply (rotate_tac -1) apply (drule_tac x="ta" in spec) apply (erule disjE) apply (rule disjI1) (* ta = []t *) apply (rule_tac x="s" in exI, simp) apply (drule_tac x="s" in spec, simp) apply (drule mp) apply (rule memT_prefix_closed, simp_all, simp) apply (rule disjI2) (* ta ~= []t *) apply (elim conjE exE, simp) apply (drule_tac x="s ^^ <Tick>" in spec) apply (drule_tac x=" sa ^^ <a>" in spec) apply (simp) apply (rule_tac x="s" in exI) apply (rule_tac x="sa ^^ <a>" in exI) apply (simp) apply (insert trace_last_nil_or_unnil) apply (rotate_tac -1) apply (drule_tac x="s" in spec) apply (erule disjE) apply (auto) done (*** rest_domT (equal) ***) lemma gSKIP_Seq_compo_rest_domT: "[| traces P1 .|. (Suc n) = traces P2 .|. (Suc n) ; traces Q1 .|. n = traces Q2 .|. n ; <Tick> ~:t traces P1 ; <Tick> ~:t traces P2 |] ==> traces (P1 ;; Q1) .|. (Suc n) = traces (P2 ;; Q2) .|. (Suc n)" apply (rule order_antisym) by (simp_all add: gSKIP_Seq_compo_rest_domT_sub) (*** map_alpha T lemma ***) lemma gSKIP_map_alpha_transfun_Seq_compo_lm: "[| distance (traces P1, traces P2) * 2 <= (1/2)^n ; distance (traces Q1, traces Q2) <= (1/2)^n ; <Tick> ~:t traces P1 ; <Tick> ~:t traces P2 |] ==> distance (traces (P1 ;; Q1), traces (P2 ;; Q2)) * 2 <= (1/2)^n" apply (insert gSKIP_Seq_compo_rest_domT[of P1 n P2 Q1 Q2]) apply (simp add: distance_rs_le_1) done (*** map_alpha ***) lemma gSKIP_contraction_half_transfun_Seq_compo: "[| contraction_alpha (tracesfun Pf) (1/2) ; non_expanding (tracesfun Qf) ; Pf : gSKIPfun |] ==> contraction_alpha (tracesfun (%f. (Pf f ;; Qf f))) (1/2)" apply (simp add: contraction_alpha_def non_expanding_def map_alpha_def) apply (intro allI) apply (drule_tac x="x" in spec) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (drule_tac x="y" in spec) apply (case_tac "x = y", simp) apply (simp add: distance_iff) apply (simp add: tracesfun_def) apply (insert ALL_gSKIP_to_Tick_notin_traces) apply (frule_tac x="Pf" in spec) apply (drule_tac x="Pf" in spec) apply (drule_tac x="(%p. Proc_T (x p))" in spec) apply (drule_tac x="(%p. Proc_T (y p))" in spec) apply (simp add: gSKIP_map_alpha_transfun_Seq_compo_lm) done (*--------------------------------* | Depth_rest | *--------------------------------*) (*** rest_domT (equal) ***) lemma Depth_rest_rest_domT: "traces P .|. n = traces Q .|. n ==> traces (P |. m) .|. n = traces (Q |. m) .|. n" apply (simp add: traces.simps) apply (simp add: min_rs) apply (rule rest_equal_preserve) apply (simp) apply (simp add: min_def) done (*** distT lemma ***) lemma Depth_rest_distT: "distance(traces (P |. m), traces (Q |. m)) <= distance(traces P, traces Q)" apply (rule rest_distance_subset) by (auto intro: Depth_rest_rest_domT) (*** map_alphaT lemma ***) lemma map_alpha_tracesfun_Depth_rest_lm: "distance(traces P, traces Q) <= alpha * distance (x1, x2) ==> distance(traces (P |. m), traces (Q |. m)) <= alpha * distance(x1, x2)" apply (insert Depth_rest_distT[of P m Q]) by (simp) (*** map_alpha ***) lemma map_alpha_tracesfun_Depth_rest: "map_alpha (tracesfun Pf) alpha ==> map_alpha (tracesfun (%f. (Pf f) |. m)) alpha" apply (simp add: map_alpha_def) apply (intro allI) apply (erule conjE) apply (drule_tac x="x" in spec) apply (drule_tac x="y" in spec) apply (simp add: tracesfun_def) by (simp add: map_alpha_tracesfun_Depth_rest_lm) (*** non_expanding ***) lemma non_expanding_tracesfun_Depth_rest: "non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. (Pf f) |. m))" by (simp add: non_expanding_def map_alpha_tracesfun_Depth_rest) (*** contraction_alpha ***) lemma contraction_alpha_tracesfun_Depth_rest: "contraction_alpha (tracesfun Pf) alpha ==> contraction_alpha (tracesfun (%f. (Pf f) |. m)) alpha" by (simp add: contraction_alpha_def map_alpha_tracesfun_Depth_rest) (*--------------------------------* | variable | *--------------------------------*) (*** non_expanding ***) lemma non_expanding_tracesfun_variable: "non_expanding (tracesfun (%f. f p))" apply (simp add: tracesfun_def) apply (simp add: traces_Proc_T) apply (simp add: non_expanding_prod_variable) done (*--------------------------------* | Procfun | *--------------------------------*) (***************************************************************** | non_expanding | *****************************************************************) lemma non_expanding_tracesfun: "Pf : nohidefun ==> non_expanding (tracesfun Pf)" apply (rule nohidefun.induct[of Pf]) apply (simp) apply (simp add: non_expanding_tracesfun_variable) apply (simp add: non_expanding_tracesfun_STOP) apply (simp add: non_expanding_tracesfun_SKIP) apply (simp add: non_expanding_tracesfun_DIV) apply (simp add: non_expanding_tracesfun_Act_prefix) apply (simp add: non_expanding_tracesfun_Ext_pre_choice) apply (simp add: non_expanding_tracesfun_Ext_choice) apply (simp add: non_expanding_tracesfun_Int_choice) apply (simp add: non_expanding_tracesfun_Rep_int_choice) apply (simp add: non_expanding_tracesfun_IF) apply (simp add: non_expanding_tracesfun_Parallel) (* hiding --> const *) apply (simp add: tracesfun_def) apply (simp add: non_expanding_Constant) apply (simp add: non_expanding_tracesfun_Renaming) apply (simp add: non_expanding_tracesfun_Seq_compo) apply (simp add: non_expanding_tracesfun_Depth_rest) done (*=============================================================* | [[P]]Tfun | *=============================================================*) lemma non_expanding_semTfun: "Pf : nohidefun ==> non_expanding [[Pf]]Tfun" by (simp add: semT_to_traces non_expanding_tracesfun) (*=============================================================* | tracesFun | *=============================================================*) lemma non_expanding_tracesFun: "PF : nohideFun ==> non_expanding (tracesFun PF)" apply (simp add: prod_non_expand) apply (rule allI) apply (simp add: proj_tracesFun_tracesfun) apply (simp add: nohideFun_def) apply (drule_tac x="i" in spec) apply (simp add: non_expanding_tracesfun) done (*=============================================================* | [[P]]TFun | *=============================================================*) lemma non_expanding_semTFun: "PF : nohideFun ==> non_expanding [[PF]]TFun" apply (simp add: semT_to_traces non_expanding_tracesFun) done (***************************************************************** | contraction | *****************************************************************) lemma contraction_alpha_tracesfun_lm: "Pf : gProcfun ==> contraction_alpha (tracesfun Pf) (1/2)" apply (rule gProcfun.induct[of Pf]) apply (simp) apply (simp add: contraction_alpha_tracesfun_STOP) apply (simp add: contraction_alpha_tracesfun_SKIP) apply (simp add: contraction_alpha_tracesfun_DIV) apply (simp add: contraction_half_tracesfun_Act_prefix non_expanding_tracesfun) apply (simp add: contraction_half_tracesfun_Ext_pre_choice non_expanding_tracesfun) apply (simp add: contraction_alpha_tracesfun_Ext_choice) apply (simp add: contraction_alpha_tracesfun_Int_choice) apply (simp add: contraction_alpha_tracesfun_Rep_int_choice) apply (simp add: contraction_alpha_tracesfun_IF) apply (simp add: contraction_alpha_tracesfun_Parallel) (* hiding --> const *) apply (simp add: tracesfun_def) apply (simp add: contraction_alpha_Constant) apply (simp add: contraction_alpha_tracesfun_Renaming) apply (simp) apply (elim conjE disjE) apply (simp add: gSKIP_contraction_half_transfun_Seq_compo non_expanding_tracesfun) apply (simp add: contraction_alpha_tracesfun_Seq_compo) apply (simp add: contraction_alpha_tracesfun_Depth_rest) done lemma contraction_alpha_tracesfun: "Pf : gProcfun ==> contraction_alpha (tracesfun Pf) (1/2)" by (simp add: contraction_alpha_tracesfun_lm) (*=============================================================* | [[P]]Tfun | *=============================================================*) lemma contraction_alpha_semTfun: "Pf : gProcfun ==> contraction_alpha [[Pf]]Tfun (1/2)" by (simp add: semT_to_traces contraction_alpha_tracesfun) (*=============================================================* | tracesfun P | *=============================================================*) lemma contraction_alpha_tracesFun: "PF : gProcFun ==> contraction_alpha (tracesFun PF) (1/2)" apply (simp add: prod_contra_alpha) apply (rule allI) apply (simp add: proj_tracesFun_tracesfun) apply (simp add: nohideFun_def gProcFun_def) apply (drule_tac x="i" in spec) apply (simp add: contraction_alpha_tracesfun) done lemma contraction_tracesFun: "PF : gProcFun ==> contraction (tracesFun PF)" apply (simp add: contraction_def) apply (rule_tac x="1/2" in exI) apply (simp add: contraction_alpha_tracesFun) done (*=============================================================* | [[P]]TFun | *=============================================================*) lemma contraction_alpha_semTFun: "PF : gProcFun ==> contraction_alpha [[PF]]TFun (1/2)" by (simp add: semT_to_traces contraction_alpha_tracesFun) lemma contraction_semTFun: "PF : gProcFun ==> contraction [[PF]]TFun" by (simp add: semT_to_traces contraction_tracesFun) end
lemma gSKIP_to_Tick_notin_traces:
Pf ∈ gSKIPfun ==> <Tick> ~:t traces (Pf f)
lemma ALL_gSKIP_to_Tick_notin_traces:
∀Pf f. Pf ∈ gSKIPfun --> <Tick> ~:t traces (Pf f)
lemma map_alpha_Constant:
0 ≤ alpha ==> map_alpha (%f. P) alpha
lemma non_expanding_Constant:
non_expanding (%f. P)
lemma contraction_alpha_Constant:
[| 0 ≤ alpha; alpha < 1 |] ==> contraction_alpha (%x. P) alpha
lemma map_alpha_tracesfun_STOP:
0 ≤ alpha ==> map_alpha (tracesfun (%f. STOP)) alpha
lemma non_expanding_tracesfun_STOP:
non_expanding (tracesfun (%f. STOP))
lemma contraction_alpha_tracesfun_STOP:
[| 0 ≤ alpha; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. STOP)) alpha
lemma map_alpha_tracesfun_SKIP:
0 ≤ alpha ==> map_alpha (tracesfun (%f. SKIP)) alpha
lemma non_expanding_tracesfun_SKIP:
non_expanding (tracesfun (%f. SKIP))
lemma contraction_alpha_tracesfun_SKIP:
[| 0 ≤ alpha; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. SKIP)) alpha
lemma map_alpha_tracesfun_DIV:
0 ≤ alpha ==> map_alpha (tracesfun (%f. DIV)) alpha
lemma non_expanding_tracesfun_DIV:
non_expanding (tracesfun (%f. DIV))
lemma contraction_alpha_tracesfun_DIV:
[| 0 ≤ alpha; alpha < 1 |] ==> contraction_alpha (tracesfun (%f. DIV)) alpha
lemma contraction_half_traces_Act_prefix_lm:
distance (traces (a -> P), traces (a -> Q)) * 2 = distance (traces P, traces Q)
lemma contraction_half_tracesfun_Act_prefix:
non_expanding (tracesfun Pf) ==> contraction_alpha (tracesfun (%f. a -> Pf f)) (1 / 2)
lemma contraction_tracesfun_Act_prefix:
non_expanding (tracesfun Pf) ==> contraction (tracesfun (%f. a -> Pf f))
lemma non_expanding_tracesfun_Act_prefix:
non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. a -> Pf f))
lemma Ext_pre_choice_Act_prefix_rest_domT_sub:
∀a∈X. traces (a -> Pf a) .|. n ≤ traces (a -> Qf a) .|. n ==> traces (? :X -> Pf) .|. n ≤ traces (? :X -> Qf) .|. n
lemma Ext_pre_choice_Act_prefix_rest_domT:
∀a∈X. traces (a -> Pf a) .|. n = traces (a -> Qf a) .|. n ==> traces (? :X -> Pf) .|. n = traces (? :X -> Qf) .|. n
lemma Ext_pre_choice_Act_prefix_distT_nonempty:
[| X ≠ {}; PQs = {(traces (a -> Pf a), traces (a -> Qf a)) |a. a ∈ X} |] ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (? :X -> Pf), traces (? :X -> Qf)) ≤ distance (fst PQ, snd PQ)
lemma contraction_half_tracesfun_Ext_pre_choice_lm:
[| X ≠ {}; ∀a. distance (traces (Pf a), traces (Qf a)) ≤ distance (x1.0, x2.0) |] ==> distance (traces (? :X -> Pf), traces (? :X -> Qf)) * 2 ≤ distance (x1.0, x2.0)
lemma contraction_half_tracesfun_Ext_pre_choice:
∀a. non_expanding (tracesfun (Pff a)) ==> contraction_alpha (tracesfun (%f. ? a:X -> Pff a f)) (1 / 2)
lemma contraction_tracesfun_Ext_pre_choice:
∀a. non_expanding (tracesfun (Pff a)) ==> contraction (tracesfun (%f. ? a:X -> Pff a f))
lemma non_expanding_tracesfun_Ext_pre_choice:
∀a. non_expanding (tracesfun (Pff a)) ==> non_expanding (tracesfun (%f. ? a:X -> Pff a f))
lemma Ext_choice_rest_domT_sub:
[| traces P1.0 .|. n ≤ traces P2.0 .|. n; traces Q1.0 .|. n ≤ traces Q2.0 .|. n |] ==> traces (P1.0 [+] Q1.0) .|. n ≤ traces (P2.0 [+] Q2.0) .|. n
lemma Ext_choice_rest_domT:
[| traces P1.0 .|. n = traces P2.0 .|. n; traces Q1.0 .|. n = traces Q2.0 .|. n |] ==> traces (P1.0 [+] Q1.0) .|. n = traces (P2.0 [+] Q2.0) .|. n
lemma Ext_choice_distT:
PQs = {(traces P1.0, traces P2.0), (traces Q1.0, traces Q2.0)} ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (P1.0 [+] Q1.0), traces (P2.0 [+] Q2.0)) ≤ distance (fst PQ, snd PQ)
lemma map_alpha_tracesfun_Ext_choice_lm:
[| distance (traces P1.0, traces P2.0) ≤ alpha * distance (x1.0, x2.0); distance (traces Q1.0, traces Q2.0) ≤ alpha * distance (x1.0, x2.0) |] ==> distance (traces (P1.0 [+] Q1.0), traces (P2.0 [+] Q2.0)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_Ext_choice:
[| map_alpha (tracesfun Pf) alpha; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. Pf f [+] Qf f)) alpha
lemma non_expanding_tracesfun_Ext_choice:
[| non_expanding (tracesfun Pf); non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. Pf f [+] Qf f))
lemma contraction_alpha_tracesfun_Ext_choice:
[| contraction_alpha (tracesfun Pf) alpha; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. Pf f [+] Qf f)) alpha
lemma map_alpha_tracesfun_Int_choice:
[| map_alpha (tracesfun Pf) alpha; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. Pf f |~| Qf f)) alpha
lemma non_expanding_tracesfun_Int_choice:
[| non_expanding (tracesfun Pf); non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. Pf f |~| Qf f))
lemma contraction_alpha_tracesfun_Int_choice:
[| contraction_alpha (tracesfun Pf) alpha; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. Pf f |~| Qf f)) alpha
lemma Rep_int_choice_rest_domT_sub:
∀c∈C. traces (Pf c) .|. n ≤ traces (Qf c) .|. n ==> traces (!! :C .. Pf) .|. n ≤ traces (!! :C .. Qf) .|. n
lemma Rep_int_choice_rest_domT:
∀c∈C. traces (Pf c) .|. n = traces (Qf c) .|. n ==> traces (!! :C .. Pf) .|. n = traces (!! :C .. Qf) .|. n
lemma Rep_int_choice_distT_nonempty:
[| C ≠ {}; PQs = {(traces (Pf c), traces (Qf c)) |c. c ∈ C} |] ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (!! :C .. Pf), traces (!! :C .. Qf)) ≤ distance (fst PQ, snd PQ)
lemma map_alpha_tracesfun_Rep_int_choice_lm:
[| C ≠ {}; ∀c. distance (traces (Pf c), traces (Qf c)) ≤ alpha * distance (x1.0, x2.0) |] ==> distance (traces (!! :C .. Pf), traces (!! :C .. Qf)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_Rep_int_choice:
∀c. map_alpha (tracesfun (Pff c)) alpha ==> map_alpha (tracesfun (%f. !! c:C .. Pff c f)) alpha
lemma non_expanding_tracesfun_Rep_int_choice:
∀c. non_expanding (tracesfun (Pff c)) ==> non_expanding (tracesfun (%f. !! c:C .. Pff c f))
lemma contraction_alpha_tracesfun_Rep_int_choice:
∀c. contraction_alpha (tracesfun (Pff c)) alpha ==> contraction_alpha (tracesfun (%f. !! c:C .. Pff c f)) alpha
lemma IF_rest_domT_sub:
[| traces P1.0 .|. n ≤ traces P2.0 .|. n; traces Q1.0 .|. n ≤ traces Q2.0 .|. n |] ==> traces (IF b THEN P1.0 ELSE Q1.0) .|. n ≤ traces (IF b THEN P2.0 ELSE Q2.0) .|. n
lemma IF_rest_domT:
[| traces P1.0 .|. n = traces P2.0 .|. n; traces Q1.0 .|. n = traces Q2.0 .|. n |] ==> traces (IF b THEN P1.0 ELSE Q1.0) .|. n = traces (IF b THEN P2.0 ELSE Q2.0) .|. n
lemma IF_distT:
PQs = {(traces P1.0, traces P2.0), (traces Q1.0, traces Q2.0)} ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (IF b THEN P1.0 ELSE Q1.0), traces (IF b THEN P2.0 ELSE Q2.0)) ≤ distance (fst PQ, snd PQ)
lemma map_alpha_tracesfun_IF_lm:
[| distance (traces P1.0, traces P2.0) ≤ alpha * distance (x1.0, x2.0); distance (traces Q1.0, traces Q2.0) ≤ alpha * distance (x1.0, x2.0) |] ==> distance (traces (IF b THEN P1.0 ELSE Q1.0), traces (IF b THEN P2.0 ELSE Q2.0)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_IF:
[| map_alpha (tracesfun Pf) alpha; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. IF b THEN Pf f ELSE Qf f)) alpha
lemma non_expanding_tracesfun_IF:
[| non_expanding (tracesfun Pf); non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. IF b THEN Pf f ELSE Qf f))
lemma contraction_alpha_tracesfun_IF:
[| contraction_alpha (tracesfun Pf) alpha; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. IF b THEN Pf f ELSE Qf f)) alpha
lemma Parallel_rest_domT_sub:
[| traces P1.0 .|. n ≤ traces P2.0 .|. n; traces Q1.0 .|. n ≤ traces Q2.0 .|. n |] ==> traces (P1.0 |[X]| Q1.0) .|. n ≤ traces (P2.0 |[X]| Q2.0) .|. n
lemma Parallel_rest_domT:
[| traces P1.0 .|. n = traces P2.0 .|. n; traces Q1.0 .|. n = traces Q2.0 .|. n |] ==> traces (P1.0 |[X]| Q1.0) .|. n = traces (P2.0 |[X]| Q2.0) .|. n
lemma Parallel_distT:
PQs = {(traces P1.0, traces P2.0), (traces Q1.0, traces Q2.0)} ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (P1.0 |[X]| Q1.0), traces (P2.0 |[X]| Q2.0)) ≤ distance (fst PQ, snd PQ)
lemma map_alpha_tracesfun_Parallel_lm:
[| distance (traces P1.0, traces P2.0) ≤ alpha * distance (x1.0, x2.0); distance (traces Q1.0, traces Q2.0) ≤ alpha * distance (x1.0, x2.0) |] ==> distance (traces (P1.0 |[X]| Q1.0), traces (P2.0 |[X]| Q2.0)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_Parallel:
[| map_alpha (tracesfun Pf) alpha; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. Pf f |[X]| Qf f)) alpha
lemma non_expanding_tracesfun_Parallel:
[| non_expanding (tracesfun Pf); non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. Pf f |[X]| Qf f))
lemma contraction_alpha_tracesfun_Parallel:
[| contraction_alpha (tracesfun Pf) alpha; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. Pf f |[X]| Qf f)) alpha
lemma Renaming_rest_domT_sub:
traces P .|. n ≤ traces Q .|. n ==> traces (P [[r]]) .|. n ≤ traces (Q [[r]]) .|. n
lemma Renaming_rest_domT:
traces P .|. n = traces Q .|. n ==> traces (P [[r]]) .|. n = traces (Q [[r]]) .|. n
lemma Renaming_distT:
distance (traces (P [[r]]), traces (Q [[r]])) ≤ distance (traces P, traces Q)
lemma map_alpha_tracesfun_Renaming_lm:
distance (traces P, traces Q) ≤ alpha * distance (x1.0, x2.0) ==> distance (traces (P [[r]]), traces (Q [[r]])) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_Renaming:
map_alpha (tracesfun Pf) alpha ==> map_alpha (tracesfun (%f. Pf f [[r]])) alpha
lemma non_expanding_tracesfun_Renaming:
non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. Pf f [[r]]))
lemma contraction_alpha_tracesfun_Renaming:
contraction_alpha (tracesfun Pf) alpha ==> contraction_alpha (tracesfun (%f. Pf f [[r]])) alpha
lemma Seq_compo_rest_domT_sub:
[| traces P1.0 .|. n ≤ traces P2.0 .|. n; traces Q1.0 .|. n ≤ traces Q2.0 .|. n |] ==> traces (P1.0 ;; Q1.0) .|. n ≤ traces (P2.0 ;; Q2.0) .|. n
lemma Seq_compo_rest_domT:
[| traces P1.0 .|. n = traces P2.0 .|. n; traces Q1.0 .|. n = traces Q2.0 .|. n |] ==> traces (P1.0 ;; Q1.0) .|. n = traces (P2.0 ;; Q2.0) .|. n
lemma Seq_compo_distT:
PQs = {(traces P1.0, traces P2.0), (traces Q1.0, traces Q2.0)} ==> ∃PQ. PQ ∈ PQs ∧ distance (traces (P1.0 ;; Q1.0), traces (P2.0 ;; Q2.0)) ≤ distance (fst PQ, snd PQ)
lemma map_alpha_transfun_Seq_compo_lm:
[| distance (traces P1.0, traces P2.0) ≤ alpha * distance (x1.0, x2.0); distance (traces Q1.0, traces Q2.0) ≤ alpha * distance (x1.0, x2.0) |] ==> distance (traces (P1.0 ;; Q1.0), traces (P2.0 ;; Q2.0)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_transfun_Seq_compo:
[| map_alpha (tracesfun Pf) alpha; map_alpha (tracesfun Qf) alpha |] ==> map_alpha (tracesfun (%f. Pf f ;; Qf f)) alpha
lemma non_expanding_tracesfun_Seq_compo:
[| non_expanding (tracesfun Pf); non_expanding (tracesfun Qf) |] ==> non_expanding (tracesfun (%f. Pf f ;; Qf f))
lemma contraction_alpha_tracesfun_Seq_compo:
[| contraction_alpha (tracesfun Pf) alpha; contraction_alpha (tracesfun Qf) alpha |] ==> contraction_alpha (tracesfun (%f. Pf f ;; Qf f)) alpha
lemma gSKIP_Seq_compo_rest_domT_sub:
[| traces P1.0 .|. Suc n ≤ traces P2.0 .|. Suc n; traces Q1.0 .|. n ≤ traces Q2.0 .|. n; <Tick> ~:t traces P1.0; <Tick> ~:t traces P2.0 |] ==> traces (P1.0 ;; Q1.0) .|. Suc n ≤ traces (P2.0 ;; Q2.0) .|. Suc n
lemma gSKIP_Seq_compo_rest_domT:
[| traces P1.0 .|. Suc n = traces P2.0 .|. Suc n; traces Q1.0 .|. n = traces Q2.0 .|. n; <Tick> ~:t traces P1.0; <Tick> ~:t traces P2.0 |] ==> traces (P1.0 ;; Q1.0) .|. Suc n = traces (P2.0 ;; Q2.0) .|. Suc n
lemma gSKIP_map_alpha_transfun_Seq_compo_lm:
[| distance (traces P1.0, traces P2.0) * 2 ≤ (1 / 2) ^ n; distance (traces Q1.0, traces Q2.0) ≤ (1 / 2) ^ n; <Tick> ~:t traces P1.0; <Tick> ~:t traces P2.0 |] ==> distance (traces (P1.0 ;; Q1.0), traces (P2.0 ;; Q2.0)) * 2 ≤ (1 / 2) ^ n
lemma gSKIP_contraction_half_transfun_Seq_compo:
[| contraction_alpha (tracesfun Pf) (1 / 2); non_expanding (tracesfun Qf); Pf ∈ gSKIPfun |] ==> contraction_alpha (tracesfun (%f. Pf f ;; Qf f)) (1 / 2)
lemma Depth_rest_rest_domT:
traces P .|. n = traces Q .|. n ==> traces (P |. m) .|. n = traces (Q |. m) .|. n
lemma Depth_rest_distT:
distance (traces (P |. m), traces (Q |. m)) ≤ distance (traces P, traces Q)
lemma map_alpha_tracesfun_Depth_rest_lm:
distance (traces P, traces Q) ≤ alpha * distance (x1.0, x2.0) ==> distance (traces (P |. m), traces (Q |. m)) ≤ alpha * distance (x1.0, x2.0)
lemma map_alpha_tracesfun_Depth_rest:
map_alpha (tracesfun Pf) alpha ==> map_alpha (tracesfun (%f. Pf f |. m)) alpha
lemma non_expanding_tracesfun_Depth_rest:
non_expanding (tracesfun Pf) ==> non_expanding (tracesfun (%f. Pf f |. m))
lemma contraction_alpha_tracesfun_Depth_rest:
contraction_alpha (tracesfun Pf) alpha ==> contraction_alpha (tracesfun (%f. Pf f |. m)) alpha
lemma non_expanding_tracesfun_variable:
non_expanding (tracesfun (%f. f p))
lemma non_expanding_tracesfun:
Pf ∈ nohidefun ==> non_expanding (tracesfun Pf)
lemma non_expanding_semTfun:
Pf ∈ nohidefun ==> non_expanding [[Pf]]Tfun
lemma non_expanding_tracesFun:
PF ∈ nohideFun ==> non_expanding (tracesFun PF)
lemma non_expanding_semTFun:
PF ∈ nohideFun ==> non_expanding [[PF]]TFun
lemma contraction_alpha_tracesfun_lm:
Pf ∈ gProcfun ==> contraction_alpha (tracesfun Pf) (1 / 2)
lemma contraction_alpha_tracesfun:
Pf ∈ gProcfun ==> contraction_alpha (tracesfun Pf) (1 / 2)
lemma contraction_alpha_semTfun:
Pf ∈ gProcfun ==> contraction_alpha [[Pf]]Tfun (1 / 2)
lemma contraction_alpha_tracesFun:
PF ∈ gProcFun ==> contraction_alpha (tracesFun PF) (1 / 2)
lemma contraction_tracesFun:
PF ∈ gProcFun ==> contraction (tracesFun PF)
lemma contraction_alpha_semTFun:
PF ∈ gProcFun ==> contraction_alpha [[PF]]TFun (1 / 2)
lemma contraction_semTFun:
PF ∈ gProcFun ==> contraction [[PF]]TFun