# HG changeset patch # User paulson # Date 1044716733 -3600 # Node ID 91713a1915ee8505869afe8c1466d8323bcaca6a # Parent f39f67982854815e018e07b24cdcfc13eb90aa04 converting HOL/UNITY to use unconditional fairness diff -r f39f67982854 -r 91713a1915ee src/HOL/Relation.thy --- a/src/HOL/Relation.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/Relation.thy Sat Feb 08 16:05:33 2003 +0100 @@ -86,6 +86,9 @@ subsection {* Diagonal: identity over a set *} +lemma diag_empty [simp]: "diag {} = {}" + by (simp add: diag_def) + lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A" by (simp add: diag_def) @@ -318,6 +321,9 @@ lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B" by blast +lemma Un_Image: "(R \ S) `` A = R `` A \ S `` A" + by blast + lemma Image_subset: "r \ A \ B ==> r``C \ B" by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Sat Feb 08 16:05:33 2003 +0100 @@ -185,7 +185,7 @@ "[| F \ stable {s. P (v s) (w s)}; G \ preserves v; G \ preserves w |] ==> F Join G \ stable {s. P (v s) (w s)}" -apply (simp) +apply simp apply (subgoal_tac "G \ preserves (funPair v w) ") prefer 2 apply simp apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Client.ML --- a/src/HOL/UNITY/Comp/Client.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Client.ML Sat Feb 08 16:05:33 2003 +0100 @@ -14,7 +14,7 @@ \ (G : preserves rel & G : preserves ask & G : preserves tok &\ \ Client : Allowed G)"; by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed])); + simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed])); qed "Client_ok_iff"; AddIffs [Client_ok_iff]; @@ -79,7 +79,8 @@ qed "Join_Always_rel_le_giv"; Goal "Client : transient {s. rel s = k & knrel. nrel = size (rel s) & + s' = s (| rel := rel s @ [giv s!nrel] |) & + nrel < size (giv s) & + ask s!nrel <= giv s!nrel}" (** Choose a new token requirement **) @@ -49,10 +49,11 @@ Client :: 'a state_d program "Client == - mk_program ({s. tok s : atMost NbT & - giv s = [] & ask s = [] & rel s = []}, - {rel_act, tok_act, ask_act}, - UN G: preserves rel Int preserves ask Int preserves tok. + mk_total_program + ({s. tok s : atMost NbT & + giv s = [] & ask s = [] & rel s = []}, + {rel_act, tok_act, ask_act}, + \\G \\ preserves rel Int preserves ask Int preserves tok. Acts G)" (*Maybe want a special theory section to declare such maps*) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Counter.ML --- a/src/HOL/UNITY/Comp/Counter.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counter.ML Sat Feb 08 16:05:33 2003 +0100 @@ -11,11 +11,10 @@ Spriner LNCS 1586 (1999), pages 1215-1227. *) -Addsimps [Component_def RS def_prg_Init]; -Addsimps (map simp_of_act [a_def]); +Addsimps [Component_def RS def_prg_Init, simp_of_act a_def]; (* Theorems about sum and sumj *) -Goal "ALL n. I sum I (s(c n := x)) = sum I s"; +Goal "\\n. I sum I (s(c n := x)) = sum I s"; by (induct_tac "I" 1); by Auto_tac; qed_spec_mp "sum_upd_gt"; @@ -47,7 +46,7 @@ addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1); qed "sumj_upd_C"; -Goal "ALL i. I (sumj I i s = sum I s)"; +Goal "\\i. I (sumj I i s = sum I s)"; by (induct_tac "I" 1); by Auto_tac; qed_spec_mp "sumj_sum_gt"; @@ -58,49 +57,49 @@ by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1); qed "sumj_sum_eq"; -Goal "ALL i. i(sum I s = s (c i) + sumj I i s)"; +Goal "\\i. i(sum I s = s (c i) + sumj I i s)"; by (induct_tac "I" 1); by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq])); qed_spec_mp "sum_sumj"; (* Correctness proofs for Components *) (* p2 and p3 proofs *) -Goal "Component i : stable {s. s C = s (c i) + k}"; +Goal "Component i \\ stable {s. s C = s (c i) + k}"; by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p2"; -Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}"; +Goal "Component i \\ stable {s. \\v. v~=c i & v~=C --> s v = k v}"; by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p3"; Goal -"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \ -\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \ -\ = (Component i: stable {s. s C = s (c i) + sumj I i s})"; +"(\\k. Component i \\ stable ({s. s C = s (c i) + sumj I i k} \ +\ \\ {s. \\v. v~=c i & v~=C --> s v = k v})) \ +\ = (Component i \\ stable {s. s C = s (c i) + sumj I i s})"; +by (asm_full_simp_tac (simpset() addsimps [Component_def, mk_total_program_def]) 1); by (auto_tac (claset(), simpset() - addsimps [constrains_def, stable_def,Component_def, - sumj_upd_C, sumj_upd_ci])); + addsimps [constrains_def, stable_def, sumj_upd_C, sumj_upd_ci])); qed "p2_p3_lemma1"; Goal -"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \ -\ {s. ALL v. v~=c i & v~=C --> s v = k v})"; +"\\k. Component i \\ stable ({s. s C = s (c i) + sumj I i k} Int \ +\ {s. \\v. v~=c i & v~=C --> s v = k v})"; by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); qed "p2_p3_lemma2"; Goal -"Component i: stable {s. s C = s (c i) + sumj I i s}"; +"Component i \\ stable {s. s C = s (c i) + sumj I i s}"; by (auto_tac (claset() addSIs [p2_p3_lemma2], simpset() addsimps [p2_p3_lemma1 RS sym])); qed "p2_p3"; (* Compositional Proof *) -Goal "(ALL i. i < I --> s (c i) = 0) --> sum I s = 0"; +Goal "(\\i. i < I --> s (c i) = 0) --> sum I s = 0"; by (induct_tac "I" 1); by Auto_tac; qed "sum_0'"; @@ -108,33 +107,7 @@ (* I could'nt be empty *) Goalw [invariant_def] -"!!I. 0 (JN i:{i. i (\\i \\ {i. i invariant {s. s C = sum I s}"; +by (simp_tac (simpset() addsimps [JN_stable, sum_sumj]) 1); by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1); qed "safety"; - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counter.thy Sat Feb 08 16:05:33 2003 +0100 @@ -37,6 +37,7 @@ Component :: "nat => state program" "Component i == - mk_program({s. s C = 0 & s (c i) = 0}, {a i}, - UN G: preserves (%s. s (c i)). Acts G)" + mk_total_program({s. s C = 0 & s (c i) = 0}, {a i}, + \\G \\ preserves (%s. s (c i)). Acts G)" + end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Counterc.ML --- a/src/HOL/UNITY/Comp/Counterc.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counterc.ML Sat Feb 08 16:05:33 2003 +0100 @@ -12,11 +12,11 @@ *) Addsimps [Component_def RS def_prg_Init, -Component_def RS def_prg_AllowedActs]; -Addsimps (map simp_of_act [a_def]); + Component_def RS def_prg_AllowedActs, + simp_of_act a_def]; (* Theorems about sum and sumj *) -Goal "ALL i. I (sum I s = sumj I i s)"; +Goal "\\i. I (sum I s = sumj I i s)"; by (induct_tac "I" 1); by Auto_tac; qed_spec_mp "sum_sumj_eq1"; @@ -26,18 +26,18 @@ by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1])); qed_spec_mp "sum_sumj_eq2"; -Goal "(ALL i. i c s' i = c s i) --> (sum I s' = sum I s)"; +Goal "(\\i. i c s' i = c s i) --> (sum I s' = sum I s)"; by (induct_tac "I" 1 THEN Auto_tac); qed_spec_mp "sum_ext"; -Goal "(ALL j. j c s' j = c s j) --> (sumj I i s' = sumj I i s)"; +Goal "(\\j. j c s' j = c s j) --> (sumj I i s' = sumj I i s)"; by (induct_tac "I" 1); by Safe_tac; by (auto_tac (claset() addSIs [sum_ext], simpset())); qed_spec_mp "sumj_ext"; -Goal "(ALL i. i c s i = 0) --> sum I s = 0"; +Goal "(\\i. i c s i = 0) --> sum I s = 0"; by (induct_tac "I" 1); by Auto_tac; qed "sum0"; @@ -46,22 +46,24 @@ (* Safety properties for Components *) Goal "(Component i ok G) = \ -\ (G: preserves (%s. c s i) & Component i:Allowed G)"; +\ (G \\ preserves (%s. c s i) & Component i \\ Allowed G)"; by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed])); + simpset() addsimps [ok_iff_Allowed, Component_def RS def_total_prg_Allowed])); qed "Component_ok_iff"; AddIffs [Component_ok_iff]; AddIffs [OK_iff_ok]; Addsimps [preserves_def]; -Goal "Component i: stable {s. C s = (c s) i + k}"; +Goal "Component i \\ stable {s. C s = (c s) i + k}"; by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); by (constrains_tac 1); qed "p2"; -Goal "[| OK I Component; i:I |] \ -\ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}"; +Goal "[| OK I Component; i\\I |] \ +\ ==> Component i \\ stable {s. \\j\\I. j~=i --> c s j = c k j}"; +by (asm_full_simp_tac (simpset() addsimps []) 1); +by (rewrite_goals_tac [Component_def, mk_total_program_def]); by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1); by (Blast_tac 1); qed "p3"; @@ -69,22 +71,22 @@ Goal "[| OK {i. i \ -\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \ -\ {s. ALL j:{i. i c s j = c k j})"; +\ \\k. Component i \\ stable ({s. C s = c s i + sumj I i k} Int \ +\ {s. \\j\\{i. i c s j = c k j})"; by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); qed "p2_p3_lemma1"; -Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \ -\ {s. ALL j:{i. i c s j = c k j})) \ -\ ==> (F:stable {s. C s = c s i + sumj I i s})"; +Goal "(\\k. F\\stable ({s. C s = (c s) i + sumj I i k} Int \ +\ {s. \\j\\{i. i c s j = c k j})) \ +\ ==> (F\\stable {s. C s = c s i + sumj I i s})"; by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1); by (force_tac (claset() addSIs [sumj_ext], simpset()) 1); qed "p2_p3_lemma2"; Goal "[| OK {i. i Component i: stable {s. C s = c s i + sumj I i s}"; +\ ==> Component i \\ stable {s. C s = c s i + sumj I i s}"; by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1); qed "p2_p3"; @@ -92,7 +94,7 @@ (* Compositional correctness *) Goalw [invariant_def] "[| 0 (JN i:{i. i (\\i\\{i. i invariant {s. C s = sum I s}"; by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1); by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3], simpset())); diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Counterc.thy --- a/src/HOL/UNITY/Comp/Counterc.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counterc.thy Sat Feb 08 16:05:33 2003 +0100 @@ -39,6 +39,7 @@ "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}" Component :: "nat => state program" - "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i}, - UN G: preserves (%s. (c s) i). Acts G)" + "Component i == mk_total_program({s. C s = 0 & (c s) i = 0}, + {a i}, + \\G \\ preserves (%s. (c s) i). Acts G)" end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Handshake.thy --- a/src/HOL/UNITY/Comp/Handshake.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Handshake.thy Sat Feb 08 16:05:33 2003 +0100 @@ -21,14 +21,14 @@ "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" F :: "state program" - "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" + "F == mk_total_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" (*G's program*) cmdG :: "(state*state) set" "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" G :: "state program" - "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" + "G == mk_total_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" (*the joint invariant*) invFG :: "state set" diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Priority.ML --- a/src/HOL/UNITY/Comp/Priority.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Priority.ML Sat Feb 08 16:05:33 2003 +0100 @@ -77,7 +77,7 @@ (* property 13: universal *) Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); by (constrains_tac 1); by (Blast_tac 1); qed "p13"; @@ -88,16 +88,15 @@ "ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; by (Clarify_tac 1); by (cut_inst_tac [("i", "j")] reach_lemma 1); -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); by (constrains_tac 1); by (auto_tac (claset(), simpset() addsimps [trancl_converse])); qed "above_not_increase"; -Goal -"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}"; +Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}"; by (cut_inst_tac [("i", "i")] above_not_increase 1); -by (asm_full_simp_tac (simpset() addsimps - [trancl_converse, constrains_def]) 1); +by (asm_full_simp_tac + (simpset() addsimps [trancl_converse, constrains_def]) 1); by (Blast_tac 1); qed "above_not_increase'"; @@ -106,7 +105,7 @@ (* p15: universal property: all Components well behave *) Goal "ALL i. system: Highest i co Highest i Un Lowest i"; by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); by (constrains_tac 1); by Auto_tac; qed "system_well_behaves"; @@ -147,9 +146,9 @@ (* propert 5: existential property *) Goal "system: Highest i leadsTo Lowest i"; -by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); by (ensures_tac "act i" 1); -by (auto_tac (claset(), simpset() addsimps [Component_def])); +by Auto_tac; qed "Highest_leadsTo_Lowest"; (* a lowest i can never be in any abover set *) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/Priority.thy Sat Feb 08 16:05:33 2003 +0100 @@ -35,7 +35,7 @@ (* All components start with the same initial state *) Component :: "vertex=>state program" - "Component i == mk_program({init}, {act i}, UNIV)" + "Component i == mk_total_program({init}, {act i}, UNIV)" (* Abbreviations *) Highest :: "vertex=>state set" diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Comp/TimerArray.thy --- a/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Comp/TimerArray.thy Sat Feb 08 16:05:33 2003 +0100 @@ -18,7 +18,7 @@ "decr == UN n uu. {((Suc n, uu), (n,uu))}" Timer :: "'a state program" - "Timer == mk_program (UNIV, {decr}, UNIV)" + "Timer == mk_total_program (UNIV, {decr}, UNIV)" declare Timer_def [THEN def_prg_Init, simp] @@ -61,8 +61,8 @@ apply (rename_tac "n") apply (rule PLam_leadsTo_Basis) apply (auto simp add: lessThan_Suc [symmetric]) -apply (unfold Timer_def, constrains) -apply (rule_tac act = decr in transientI, auto) +apply (unfold Timer_def mk_total_program_def, constrains) +apply (rule_tac act = decr in totalize_transientI, auto) done end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Constrains.thy Sat Feb 08 16:05:33 2003 +0100 @@ -55,7 +55,7 @@ subsection{*traces and reachable*} lemma reachable_equiv_traces: - "reachable F = {s. \evs. (s,evs): traces (Init F) (Acts F)}" + "reachable F = {s. \evs. (s,evs) \ traces (Init F) (Acts F)}" apply safe apply (erule_tac [2] traces.induct) apply (erule reachable.induct) @@ -392,4 +392,35 @@ used by Always_Int_I) *) lemmas Always_thin = thin_rl [of "F \ Always A", standard] + +subsection{*Totalize*} + +lemma reachable_imp_reachable_tot: + "s \ reachable F ==> s \ reachable (totalize F)" +apply (erule reachable.induct) + apply (rule reachable.Init) + apply simp +apply (rule_tac act = "totalize_act act" in reachable.Acts) +apply (auto simp add: totalize_act_def) +done + +lemma reachable_tot_imp_reachable: + "s \ reachable (totalize F) ==> s \ reachable F" +apply (erule reachable.induct) + apply (rule reachable.Init, simp) +apply (force simp add: totalize_act_def intro: reachable.Acts) +done + +lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F" +by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) + +lemma totalize_Constrains_iff [simp]: "(totalize F \ A Co B) = (F \ A Co B)" +by (simp add: Constrains_def) + +lemma totalize_Stable_iff [simp]: "(totalize F \ Stable A) = (F \ Stable A)" +by (simp add: Stable_def) + +lemma totalize_Always_iff [simp]: "(totalize F \ Always A) = (F \ Always A)" +by (simp add: Always_def) + end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Detects.thy --- a/src/HOL/UNITY/Detects.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Detects.thy Sat Feb 08 16:05:33 2003 +0100 @@ -21,7 +21,8 @@ (* Corollary from Sectiom 3.6.4 *) -lemma Always_at_FP: "F \ A LeadsTo B ==> F \ Always (-((FP F) \ A \ -B))" +lemma Always_at_FP: + "[|F \ A LeadsTo B; all_total F|] ==> F \ Always (-((FP F) \ A \ -B))" apply (rule LeadsTo_empty) apply (subgoal_tac "F \ (FP F \ A \ - B) LeadsTo (B \ (FP F \ -B))") apply (subgoal_tac [2] " (FP F \ A \ - B) = (A \ (FP F \ -B))") @@ -36,8 +37,7 @@ apply (unfold Detects_def Int_def) apply (simp (no_asm)) apply safe -apply (rule_tac [2] LeadsTo_Trans) -apply auto +apply (rule_tac [2] LeadsTo_Trans, auto) apply (subgoal_tac "F \ Always ((-A \ B) \ (-B \ C))") apply (blast intro: Always_weaken) apply (simp add: Always_Int_distrib) @@ -49,9 +49,7 @@ done lemma Detects_eq_Un: "(A<==>B) = (A \ B) \ (-A \ -B)" -apply (unfold Equality_def) -apply blast -done +by (unfold Equality_def, blast) (*Not quite antisymmetry: sets A and B agree in all reachable states *) lemma Detects_antisym: @@ -64,9 +62,9 @@ (* Theorem from Section 3.8 *) lemma Detects_Always: - "F \ A Detects B ==> F \ Always ((-(FP F)) \ (A <==> B))" + "[|F \ A Detects B; all_total F|] ==> F \ Always (-(FP F) \ (A <==> B))" apply (unfold Detects_def Equality_def) -apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib) +apply (simp add: Un_Int_distrib Always_Int_distrib) apply (blast dest: Always_at_FP intro: Always_weaken) done @@ -75,7 +73,7 @@ lemma Detects_Imp_LeadstoEQ: "F \ A Detects B ==> F \ UNIV LeadsTo (A <==> B)" apply (unfold Detects_def Equality_def) -apply (rule_tac B = "B" in LeadsTo_Diff) +apply (rule_tac B = B in LeadsTo_Diff) apply (blast intro: Always_LeadsToI subset_imp_LeadsTo) apply (blast intro: Always_LeadsTo_weaken) done diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/ELT.thy --- a/src/HOL/UNITY/ELT.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/ELT.thy Sat Feb 08 16:05:33 2003 +0100 @@ -281,22 +281,11 @@ "[| F : A leadsTo[CC] (B Un A'); F : (B-A') leadsTo[CC] B' |] ==> F : A leadsTo[CC] (B' Un A')" apply (rule leadsETo_cancel1) -prefer 2 apply assumption -apply (simp_all (no_asm_simp)) + prefer 2 apply assumption +apply simp_all done -(** The impossibility law **) - -lemma leadsETo_empty_lemma: "F : A leadsTo[CC] B ==> B={} --> A={}" -apply (erule leadsETo_induct) -apply (simp_all (no_asm_simp)) -apply (unfold ensures_def constrains_def transient_def, blast) -done - -lemma leadsETo_empty: "F : A leadsTo[CC] {} ==> A={}" -by (blast intro!: leadsETo_empty_lemma [THEN mp]) - (** PSP: Progress-Safety-Progress **) @@ -367,23 +356,6 @@ apply (blast intro: constrains_Int [THEN constrains_weaken])+ done -(*useful??*) -lemma Join_leadsETo_stable_imp_leadsETo: - "[| F Join G : (A leadsTo[CC] B); ALL C:CC. G : stable C |] - ==> F: (A leadsTo[CC] B)" -apply (erule leadsETo_induct) -prefer 3 apply (blast intro: leadsETo_Union) -prefer 2 apply (blast intro: leadsETo_Trans) -apply (rule leadsETo_Basis) -apply (case_tac "A <= B") -apply (erule subset_imp_ensures) -apply (auto intro: constrains_weaken simp add: stable_def ensures_def Join_transient) -apply (erule_tac V = "?F : ?A co ?B" in thin_rl)+ -apply (erule transientE) -apply (unfold constrains_def) -apply (blast dest!: bspec) -done - (**** Relationship with traditional "leadsTo", strong & weak ****) (** strong **) @@ -538,18 +510,6 @@ done - -(*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*) -lemma (in Extend) - "[| G : preserves (v o f); project h C G : transient D; - D : givenBy v |] ==> D={}" -apply (rule stable_transient_empty) - prefer 2 apply assumption -(*If addIs then PROOF FAILED at depth 2*) -apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I) -done - - (*This version's stronger in the "ensures" precondition BUT there's no ensures_weaken_L*) lemma (in Extend) Join_project_ensures_strong: @@ -563,20 +523,7 @@ apply (auto simp add: Int_Diff) done -(*Generalizes preserves_project_transient_empty*) -lemma (in Extend) preserves_o_project_transient_empty: - "[| G : preserves (v o f); - project h C G : transient (C' Int D); - project h C G : stable C'; D : givenBy v |] - ==> C' Int D = {}" -apply (rule stable_transient_empty) -prefer 2 apply assumption -(*Fragile proof. Was just a single blast call. - If just "intro" then PROOF FAILED at depth 3*) -apply (rule stable_Int) - apply (blast intro!: preserves_givenBy_imp_stable project_preserves_I)+ -done - +(*NOT WORKING. MODIFY AS IN Project.thy lemma (in Extend) pld_lemma: "[| extend h F Join G : stable C; F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B; @@ -596,7 +543,7 @@ prefer 2 apply (simp add: Int_Diff Int_extend_set_lemma extend_set_Diff_distrib [symmetric]) apply (rule Join_project_ensures_strong) -apply (auto dest: preserves_o_project_transient_empty intro: project_stable_project_set simp add: Int_left_absorb) +apply (auto intro: project_stable_project_set simp add: Int_left_absorb) apply (simp (no_asm_simp) add: stable_ensures_Int [THEN ensures_weaken_R] Int_lower2 project_stable_project_set extend_stable_project_set) done @@ -652,6 +599,7 @@ apply (unfold extending_def) apply (blast intro: project_LeadsETo_D) done +*) (*** leadsETo in the precondition ***) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Extend.thy --- a/src/HOL/UNITY/Extend.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Extend.thy Sat Feb 08 16:05:33 2003 +0100 @@ -101,9 +101,6 @@ lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \ B)" by blast -lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F" -by (blast intro: sym [THEN image_eqI]) - (*Possibly easier than reasoning about "inv h"*) lemma good_mapI: assumes surj_h: "surj h" @@ -338,9 +335,9 @@ -subsection{*extend ****) +subsection{*extend*} -(*** Basic properties*} +text{*Basic properties*} lemma Init_extend [simp]: "Init (extend h F) = extend_set h (Init F)" @@ -453,6 +450,8 @@ lemma (in Extend) project_mono: "F \ G ==> project h C F \ project h C G" by (simp add: component_eq_subset, blast) +lemma (in Extend) all_total_extend: "all_total F ==> all_total (extend h F)" +by (simp add: all_total_def Domain_extend_act) subsection{*Safety: co, stable*} @@ -611,10 +610,7 @@ lemma (in Extend) extend_transient_slice: "extend h F \ transient A ==> F \ transient (slice A y)" -apply (unfold transient_def, auto) -apply (rule bexI, auto) -apply (force simp add: extend_act_def) -done +by (unfold transient_def, auto) (*Converse?*) lemma (in Extend) extend_constrains_slice: diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/FP.thy --- a/src/HOL/UNITY/FP.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/FP.thy Sat Feb 08 16:05:33 2003 +0100 @@ -56,4 +56,7 @@ lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})" by (simp add: Diff_eq Compl_FP) +lemma totalize_FP [simp]: "FP (totalize F) = FP F" +by (simp add: FP_def) + end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Follows.thy Sat Feb 08 16:05:33 2003 +0100 @@ -62,16 +62,13 @@ subsection{*Destruction rules*} lemma Follows_Increasing1: "F \ f Fols g ==> F \ Increasing f" -apply (unfold Follows_def, blast) -done +by (unfold Follows_def, blast) lemma Follows_Increasing2: "F \ f Fols g ==> F \ Increasing g" -apply (unfold Follows_def, blast) -done +by (unfold Follows_def, blast) lemma Follows_Bounded: "F \ f Fols g ==> F \ Always {s. f s \ g s}" -apply (unfold Follows_def, blast) -done +by (unfold Follows_def, blast) lemma Follows_LeadsTo: "F \ f Fols g ==> F \ {s. k \ g s} LeadsTo {s. k \ f s}" @@ -159,8 +156,7 @@ apply (rule LeadsTo_weaken) apply (rule PSP_Stable) apply (erule_tac x = "f s" in spec) -apply (erule Stable_Int, assumption) -apply blast+ +apply (erule Stable_Int, assumption, blast+) done lemma Follows_Un: @@ -218,8 +214,7 @@ apply (rule LeadsTo_weaken) apply (rule PSP_Stable) apply (erule_tac x = "f s" in spec) -apply (erule Stable_Int, assumption) -apply blast +apply (erule Stable_Int, assumption, blast) apply (blast intro: union_le_mono order_trans) done diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Guar.thy Sat Feb 08 16:05:33 2003 +0100 @@ -109,8 +109,7 @@ lemma ex_prop_equiv: "ex_prop X = (\G. G \ X = (\H. (G component_of H) --> H \ X))" apply auto -apply (unfold ex_prop_def component_of_def, safe) -apply blast +apply (unfold ex_prop_def component_of_def, safe, blast) apply blast apply (subst Join_commute) apply (drule ok_sym, blast) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Lift_prog.thy Sat Feb 08 16:05:33 2003 +0100 @@ -47,7 +47,7 @@ apply (auto split add: nat_diff_split) done -(*** Injectiveness proof ***) +subsection{*Injectiveness proof*} lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y" by (drule_tac x = i in fun_cong, simp) @@ -80,7 +80,7 @@ apply (rule inj_onI, auto) done -(*** Surjectiveness proof ***) +subsection{*Surjectiveness proof*} lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s" apply (unfold lift_map_def drop_map_def) @@ -111,7 +111,11 @@ lemma sub_apply [simp]: "sub i f = f i" by (simp add: sub_def) -(*** lift_set ***) +lemma all_total_lift: "all_total F ==> all_total (lift i F)" +by (simp add: lift_def rename_def Extend.all_total_extend) + + +subsection{*The Operator @{term lift_set}*} lemma lift_set_empty [simp]: "lift_set i {} = {}" by (unfold lift_set_def, auto) @@ -133,9 +137,7 @@ done lemma lift_set_Un_distrib: "lift_set i (A \ B) = lift_set i A \ lift_set i B" -apply (unfold lift_set_def) -apply (simp add: image_Un) -done +by (simp add: lift_set_def image_Un) lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B" apply (unfold lift_set_def) @@ -143,7 +145,7 @@ done -(*** the lattice operations ***) +subsection{*The Lattice Operations*} lemma bij_lift [iff]: "bij (lift i)" by (simp add: lift_def) @@ -157,7 +159,7 @@ lemma lift_JN [simp]: "lift j (JOIN I F) = (\i \ I. lift j (F i))" by (simp add: lift_def) -(*** Safety: co, stable, invariant ***) +subsection{*Safety: constrains, stable, invariant*} lemma lift_constrains: "(lift i F \ (lift_set i A) co (lift_set i B)) = (F \ A co B)" @@ -169,29 +171,21 @@ lemma lift_invariant: "(lift i F \ invariant (lift_set i A)) = (F \ invariant A)" -apply (unfold lift_def lift_set_def) -apply (simp add: rename_invariant) -done +by (simp add: lift_def lift_set_def rename_invariant) lemma lift_Constrains: "(lift i F \ (lift_set i A) Co (lift_set i B)) = (F \ A Co B)" -apply (unfold lift_def lift_set_def) -apply (simp add: rename_Constrains) -done +by (simp add: lift_def lift_set_def rename_Constrains) lemma lift_Stable: "(lift i F \ Stable (lift_set i A)) = (F \ Stable A)" -apply (unfold lift_def lift_set_def) -apply (simp add: rename_Stable) -done +by (simp add: lift_def lift_set_def rename_Stable) lemma lift_Always: "(lift i F \ Always (lift_set i A)) = (F \ Always A)" -apply (unfold lift_def lift_set_def) -apply (simp add: rename_Always) -done +by (simp add: lift_def lift_set_def rename_Always) -(*** Progress: transient, ensures ***) +subsection{*Progress: transient, ensures*} lemma lift_transient: "(lift i F \ transient (lift_set i A)) = (F \ transient A)" @@ -223,16 +217,12 @@ apply (simp add: o_def) done -lemma lift_guarantees_eq_lift_inv: "(lift i F \ X guarantees Y) = +lemma lift_guarantees_eq_lift_inv: + "(lift i F \ X guarantees Y) = (F \ (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))" by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def) -(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj, - which is used only in TimerArray and perhaps isn't even essential - there! -***) - (*To preserve snd means that the second component is there just to allow guarantees properties to be stated. Converse fails, for lift i F can change function components other than i*) @@ -293,59 +283,9 @@ apply (erule constrains_imp_subset [THEN lift_set_mono]) done -(** Lemmas for the transient theorem **) - -lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f" -by (rule ext, auto) - -lemma insert_map_upd: - "(insert_map j t f)(i := s) = - (if i=j then insert_map i s f - else if ij |] - ==> \g'. insert_map i s' f = insert_map j t g'" -apply (subst insert_map_upd_same [symmetric]) -apply (erule ssubst) -apply (simp only: insert_map_upd if_False split: split_if, blast) -done - -lemma lift_map_eq_diff: - "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i\j |] - ==> \g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))" -apply (unfold lift_map_def, auto) -apply (blast dest: insert_map_eq_diff) -done - -lemma lift_transient_eq_disj: - "F \ preserves snd - ==> (lift i F \ transient (lift_set j (A <*> UNIV))) = - (i=j & F \ transient (A <*> UNIV) | A={})" -apply (case_tac "i=j") -apply (auto simp add: lift_transient) -apply (auto simp add: lift_set_def lift_def transient_def rename_def - extend_def Domain_extend_act) -apply (drule subsetD, blast, auto) -apply (rename_tac s f uu s' f' uu') -apply (subgoal_tac "f'=f & uu'=uu") - prefer 2 apply (force dest!: preserves_imp_eq, auto) -apply (drule sym) -apply (drule subsetD) -apply (rule ImageI) -apply (erule bij_lift_map [THEN good_map_bij, - THEN Extend.intro, - THEN Extend.mem_extend_act_iff [THEN iffD2]], force) -apply (erule lift_map_eq_diff [THEN exE], auto) -done - (*USELESS??*) -lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) = +lemma lift_map_image_Times: + "lift_map i ` (A <*> UNIV) = (\s \ A. \f. {insert_map i s f}) <*> UNIV" apply (auto intro!: bexI image_eqI simp add: lift_map_def) apply (rule split_conv [symmetric]) @@ -368,7 +308,7 @@ done -(*** Lemmas to handle function composition (o) more consistently ***) +subsection{*Lemmas to Handle Function Composition (o) More Consistently*} (*Lets us prove one version of a theorem and store others*) lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h" @@ -388,15 +328,18 @@ done -(*** More lemmas about extend and project - They could be moved to {Extend,Project}.ML, but DON'T need the locale ***) +subsection{*More lemmas about extend and project*} -lemma extend_act_extend_act: "extend_act h' (extend_act h act) = +text{*They could be moved to theory Extend or Project*} + +lemma extend_act_extend_act: + "extend_act h' (extend_act h act) = extend_act (%(x,(y,y')). h'(h(x,y),y')) act" apply (auto elim!: rev_bexI simp add: extend_act_def, blast) done -lemma project_act_project_act: "project_act h (project_act h' act) = +lemma project_act_project_act: + "project_act h (project_act h' act) = project_act (%(x,(y,y')). h'(h(x,y),y')) act" by (auto elim!: rev_bexI simp add: project_act_def) @@ -407,7 +350,7 @@ by (simp add: extend_act_def project_act_def, blast) -(*** OK and "lift" ***) +subsection{*OK and "lift"*} lemma act_in_UNION_preserves_fst: "act \ {(x,x'). fst x = fst x'} ==> act \ UNION (preserves fst) Acts" diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/PPROD.thy --- a/src/HOL/UNITY/PPROD.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/PPROD.thy Sat Feb 08 16:05:33 2003 +0100 @@ -27,28 +27,20 @@ (*** Basic properties ***) -lemma Init_PLam: "Init (PLam I F) = (\i \ I. lift_set i (Init (F i)))" -apply (simp (no_asm) add: PLam_def lift_def lift_set_def) -done - -declare Init_PLam [simp] +lemma Init_PLam [simp]: "Init (PLam I F) = (\i \ I. lift_set i (Init (F i)))" +by (simp add: PLam_def lift_def lift_set_def) -lemma PLam_empty: "PLam {} F = SKIP" -apply (simp (no_asm) add: PLam_def) -done +lemma PLam_empty [simp]: "PLam {} F = SKIP" +by (simp add: PLam_def) -lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP" -apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant) -done - -declare PLam_SKIP [simp] PLam_empty [simp] +lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP" +by (simp add: PLam_def lift_SKIP JN_constant) lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)" by (unfold PLam_def, auto) lemma PLam_component_iff: "((PLam I F) \ H) = (\i \ I. lift i (F i) \ H)" -apply (simp (no_asm) add: PLam_def JN_component_iff) -done +by (simp add: PLam_def JN_component_iff) lemma component_PLam: "i \ I ==> lift i (F i) \ (PLam I F)" apply (unfold PLam_def) @@ -59,87 +51,89 @@ (** Safety & Progress: but are they used anywhere? **) -lemma PLam_constrains: - "[| i \ I; \j. F j \ preserves snd |] ==> - (PLam I F \ (lift_set i (A <*> UNIV)) co - (lift_set i (B <*> UNIV))) = - (F i \ (A <*> UNIV) co (B <*> UNIV))" -apply (simp (no_asm_simp) add: PLam_def JN_constrains) +lemma PLam_constrains: + "[| i \ I; \j. F j \ preserves snd |] + ==> (PLam I F \ (lift_set i (A <*> UNIV)) co + (lift_set i (B <*> UNIV))) = + (F i \ (A <*> UNIV) co (B <*> UNIV))" +apply (simp add: PLam_def JN_constrains) apply (subst insert_Diff [symmetric], assumption) -apply (simp (no_asm_simp) add: lift_constrains) +apply (simp add: lift_constrains) apply (blast intro: constrains_imp_lift_constrains) done -lemma PLam_stable: - "[| i \ I; \j. F j \ preserves snd |] - ==> (PLam I F \ stable (lift_set i (A <*> UNIV))) = +lemma PLam_stable: + "[| i \ I; \j. F j \ preserves snd |] + ==> (PLam I F \ stable (lift_set i (A <*> UNIV))) = (F i \ stable (A <*> UNIV))" -apply (simp (no_asm_simp) add: stable_def PLam_constrains) -done +by (simp add: stable_def PLam_constrains) + +lemma PLam_transient: + "i \ I ==> + PLam I F \ transient A = (\i \ I. lift i (F i) \ transient A)" +by (simp add: JN_transient PLam_def) -lemma PLam_transient: - "i \ I ==> - PLam I F \ transient A = (\i \ I. lift i (F i) \ transient A)" -apply (simp (no_asm_simp) add: JN_transient PLam_def) +text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*} +lemma PLam_ensures: + "[| i \ I; F i \ (A <*> UNIV) ensures (B <*> UNIV); + \j. F j \ preserves snd |] + ==> PLam I F \ lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)" +apply (simp add: ensures_def PLam_constrains PLam_transient + lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] + Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) +apply (rule rev_bexI, assumption) +apply (simp add: lift_transient) done -(*This holds because the F j cannot change (lift_set i)*) -lemma PLam_ensures: - "[| i \ I; F i \ (A <*> UNIV) ensures (B <*> UNIV); - \j. F j \ preserves snd |] ==> - PLam I F \ lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)" -apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric]) -done - -lemma PLam_leadsTo_Basis: - "[| i \ I; - F i \ ((A <*> UNIV) - (B <*> UNIV)) co - ((A <*> UNIV) \ (B <*> UNIV)); - F i \ transient ((A <*> UNIV) - (B <*> UNIV)); - \j. F j \ preserves snd |] ==> - PLam I F \ lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)" +lemma PLam_leadsTo_Basis: + "[| i \ I; + F i \ ((A <*> UNIV) - (B <*> UNIV)) co + ((A <*> UNIV) \ (B <*> UNIV)); + F i \ transient ((A <*> UNIV) - (B <*> UNIV)); + \j. F j \ preserves snd |] + ==> PLam I F \ lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)" by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI) (** invariant **) -lemma invariant_imp_PLam_invariant: - "[| F i \ invariant (A <*> UNIV); i \ I; - \j. F j \ preserves snd |] +lemma invariant_imp_PLam_invariant: + "[| F i \ invariant (A <*> UNIV); i \ I; + \j. F j \ preserves snd |] ==> PLam I F \ invariant (lift_set i (A <*> UNIV))" by (auto simp add: PLam_stable invariant_def) lemma PLam_preserves_fst [simp]: - "\j. F j \ preserves snd - ==> (PLam I F \ preserves (v o sub j o fst)) = + "\j. F j \ preserves snd + ==> (PLam I F \ preserves (v o sub j o fst)) = (if j \ I then F j \ preserves (v o fst) else True)" -by (simp (no_asm_simp) add: PLam_def lift_preserves_sub) +by (simp add: PLam_def lift_preserves_sub) lemma PLam_preserves_snd [simp,intro]: "\j. F j \ preserves snd ==> PLam I F \ preserves snd" -by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I) +by (simp add: PLam_def lift_preserves_snd_I) (*** guarantees properties ***) -(*This rule looks unsatisfactory because it refers to "lift". One must use +text{*This rule looks unsatisfactory because it refers to "lift". One must use lift_guarantees_eq_lift_inv to rewrite the first subgoal and something like lift_preserves_sub to rewrite the third. However there's - no obvious way to alternative for the third premise.*) -lemma guarantees_PLam_I: - "[| lift i (F i): X guarantees Y; i \ I; - OK I (%i. lift i (F i)) |] + no obvious way to alternative for the third premise.*} +lemma guarantees_PLam_I: + "[| lift i (F i): X guarantees Y; i \ I; + OK I (%i. lift i (F i)) |] ==> (PLam I F) \ X guarantees Y" apply (unfold PLam_def) -apply (simp (no_asm_simp) add: guarantees_JN_I) +apply (simp add: guarantees_JN_I) done lemma Allowed_PLam [simp]: "Allowed (PLam I F) = (\i \ I. lift i ` Allowed(F i))" -by (simp (no_asm) add: PLam_def) +by (simp add: PLam_def) lemma PLam_preserves [simp]: @@ -149,24 +143,24 @@ (**UNUSED (*The f0 premise ensures that the product is well-defined.*) - lemma PLam_invariant_imp_invariant: - "[| PLam I F \ invariant (lift_set i A); i \ I; + lemma PLam_invariant_imp_invariant: + "[| PLam I F \ invariant (lift_set i A); i \ I; f0: Init (PLam I F) |] ==> F i \ invariant A" apply (auto simp add: invariant_def) apply (drule_tac c = "f0 (i:=x) " in subsetD) apply auto done - lemma PLam_invariant: - "[| i \ I; f0: Init (PLam I F) |] + lemma PLam_invariant: + "[| i \ I; f0: Init (PLam I F) |] ==> (PLam I F \ invariant (lift_set i A)) = (F i \ invariant A)" apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant) done (*The f0 premise isn't needed if F is a constant program because then we get an initial state by replicating that of F*) - lemma reachable_PLam: - "i \ I + lemma reachable_PLam: + "i \ I ==> ((plam x \ I. F) \ invariant (lift_set i A)) = (F \ invariant A)" apply (auto simp add: invariant_def) done @@ -185,15 +179,15 @@ lemma "{f. \i \ I. f i \ R i} = (\i \ I. lift_set i (R i))" by auto - lemma reachable_PLam_subset1: + lemma reachable_PLam_subset1: "reachable (PLam I F) \ (\i \ I. lift_set i (reachable (F i)))" apply (force dest!: reachable_PLam) done (*simplify using reachable_lift??*) lemma reachable_lift_Join_PLam [rule_format]: - "[| i \ I; A \ reachable (F i) |] - ==> \f. f \ reachable (PLam I F) + "[| i \ I; A \ reachable (F i) |] + ==> \f. f \ reachable (PLam I F) --> f(i:=A) \ reachable (lift i (F i) Join PLam I F)" apply (erule reachable.induct) apply (ALLGOALS Clarify_tac) @@ -222,16 +216,16 @@ (*The index set must be finite: otherwise infinitely many copies of F can perform actions, and PLam can never catch up in finite time.*) - lemma reachable_PLam_subset2: - "finite I + lemma reachable_PLam_subset2: + "finite I ==> (\i \ I. lift_set i (reachable (F i))) \ reachable (PLam I F)" apply (erule finite_induct) apply (simp (no_asm)) apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert) done - lemma reachable_PLam_eq: - "finite I ==> + lemma reachable_PLam_eq: + "finite I ==> reachable (PLam I F) = (\i \ I. lift_set i (reachable (F i)))" apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2])) done @@ -239,8 +233,8 @@ (** Co **) - lemma Constrains_imp_PLam_Constrains: - "[| F i \ A Co B; i \ I; finite I |] + lemma Constrains_imp_PLam_Constrains: + "[| F i \ A Co B; i \ I; finite I |] ==> PLam I F \ (lift_set i A) Co (lift_set i B)" apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq) apply (auto simp add: constrains_def PLam_def) @@ -249,37 +243,37 @@ - lemma PLam_Constrains: - "[| i \ I; finite I; f0: Init (PLam I F) |] - ==> (PLam I F \ (lift_set i A) Co (lift_set i B)) = + lemma PLam_Constrains: + "[| i \ I; finite I; f0: Init (PLam I F) |] + ==> (PLam I F \ (lift_set i A) Co (lift_set i B)) = (F i \ A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains) done - lemma PLam_Stable: - "[| i \ I; finite I; f0: Init (PLam I F) |] + lemma PLam_Stable: + "[| i \ I; finite I; f0: Init (PLam I F) |] ==> (PLam I F \ Stable (lift_set i A)) = (F i \ Stable A)" - apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains) + apply (simp del: Init_PLam add: Stable_def PLam_Constrains) done (** const_PLam (no dependence on i) doesn't require the f0 premise **) - lemma const_PLam_Constrains: - "[| i \ I; finite I |] - ==> ((plam x \ I. F) \ (lift_set i A) Co (lift_set i B)) = + lemma const_PLam_Constrains: + "[| i \ I; finite I |] + ==> ((plam x \ I. F) \ (lift_set i A) Co (lift_set i B)) = (F \ A Co B)" apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains) done - lemma const_PLam_Stable: - "[| i \ I; finite I |] + lemma const_PLam_Stable: + "[| i \ I; finite I |] ==> ((plam x \ I. F) \ Stable (lift_set i A)) = (F \ Stable A)" - apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains) + apply (simp add: Stable_def const_PLam_Constrains) done - lemma const_PLam_Increasing: - "[| i \ I; finite I |] + lemma const_PLam_Increasing: + "[| i \ I; finite I |] ==> ((plam x \ I. F) \ Increasing (f o sub i)) = (F \ Increasing f)" apply (unfold Increasing_def) apply (subgoal_tac "\z. {s. z \ (f o sub i) s} = lift_set i {s. z \ f s}") diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Project.thy --- a/src/HOL/UNITY/Project.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Project.thy Sat Feb 08 16:05:33 2003 +0100 @@ -16,20 +16,20 @@ projecting :: "['c program => 'c set, 'a*'b => 'c, 'a program, 'c program set, 'a program set] => bool" "projecting C h F X' X == - ALL G. extend h F Join G : X' --> F Join project h (C G) G : X" + \G. extend h F Join G \ X' --> F Join project h (C G) G \ X" extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 'c program set, 'a program set] => bool" "extending C h F Y' Y == - ALL G. extend h F ok G --> F Join project h (C G) G : Y - --> extend h F Join G : Y'" + \G. extend h F ok G --> F Join project h (C G) G \ Y + --> extend h F Join G \ Y'" subset_closed :: "'a set set => bool" - "subset_closed U == ALL A: U. Pow A <= U" + "subset_closed U == \A \ U. Pow A \ U" lemma (in Extend) project_extend_constrains_I: - "F : A co B ==> project h C (extend h F) : A co B" + "F \ A co B ==> project h C (extend h F) \ A co B" apply (auto simp add: extend_act_def project_act_def constrains_def) done @@ -38,8 +38,8 @@ (*used below to prove Join_project_ensures*) lemma (in Extend) project_unless [rule_format]: - "[| G : stable C; project h C G : A unless B |] - ==> G : (C Int extend_set h A) unless (extend_set h B)" + "[| G \ stable C; project h C G \ A unless B |] + ==> G \ (C \ extend_set h A) unless (extend_set h B)" apply (simp add: unless_def project_constrains) apply (blast dest: stable_constrains_Int intro: constrains_weaken) done @@ -47,21 +47,21 @@ (*Generalizes project_constrains to the program F Join project h C G useful with guarantees reasoning*) lemma (in Extend) Join_project_constrains: - "(F Join project h C G : A co B) = - (extend h F Join G : (C Int extend_set h A) co (extend_set h B) & - F : A co B)" + "(F Join project h C G \ A co B) = + (extend h F Join G \ (C \ extend_set h A) co (extend_set h B) & + F \ A co B)" apply (simp (no_asm) add: project_constrains) apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] dest: constrains_imp_subset) done (*The condition is required to prove the left-to-right direction - could weaken it to G : (C Int extend_set h A) co C*) + could weaken it to G \ (C \ extend_set h A) co C*) lemma (in Extend) Join_project_stable: - "extend h F Join G : stable C - ==> (F Join project h C G : stable A) = - (extend h F Join G : stable (C Int extend_set h A) & - F : stable A)" + "extend h F Join G \ stable C + ==> (F Join project h C G \ stable A) = + (extend h F Join G \ stable (C \ extend_set h A) & + F \ stable A)" apply (unfold stable_def) apply (simp only: Join_project_constrains) apply (blast intro: constrains_weaken dest: constrains_Int) @@ -69,23 +69,23 @@ (*For using project_guarantees in particular cases*) lemma (in Extend) project_constrains_I: - "extend h F Join G : extend_set h A co extend_set h B - ==> F Join project h C G : A co B" + "extend h F Join G \ extend_set h A co extend_set h B + ==> F Join project h C G \ A co B" apply (simp add: project_constrains extend_constrains) apply (blast intro: constrains_weaken dest: constrains_imp_subset) done lemma (in Extend) project_increasing_I: - "extend h F Join G : increasing (func o f) - ==> F Join project h C G : increasing func" + "extend h F Join G \ increasing (func o f) + ==> F Join project h C G \ increasing func" apply (unfold increasing_def stable_def) apply (simp del: Join_constrains add: project_constrains_I extend_set_eq_Collect) done lemma (in Extend) Join_project_increasing: - "(F Join project h UNIV G : increasing func) = - (extend h F Join G : increasing (func o f))" + "(F Join project h UNIV G \ increasing func) = + (extend h F Join G \ increasing (func o f))" apply (rule iffI) apply (erule_tac [2] project_increasing_I) apply (simp del: Join_stable @@ -95,8 +95,8 @@ (*The UNIV argument is essential*) lemma (in Extend) project_constrains_D: - "F Join project h UNIV G : A co B - ==> extend h F Join G : extend_set h A co extend_set h B" + "F Join project h UNIV G \ A co B + ==> extend h F Join G \ extend_set h A co extend_set h B" by (simp add: project_constrains extend_constrains) @@ -104,26 +104,26 @@ lemma projecting_Int: "[| projecting C h F XA' XA; projecting C h F XB' XB |] - ==> projecting C h F (XA' Int XB') (XA Int XB)" + ==> projecting C h F (XA' \ XB') (XA \ XB)" by (unfold projecting_def, blast) lemma projecting_Un: "[| projecting C h F XA' XA; projecting C h F XB' XB |] - ==> projecting C h F (XA' Un XB') (XA Un XB)" + ==> projecting C h F (XA' \ XB') (XA \ XB)" by (unfold projecting_def, blast) lemma projecting_INT: - "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] - ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)" + "[| !!i. i \ I ==> projecting C h F (X' i) (X i) |] + ==> projecting C h F (\i \ I. X' i) (\i \ I. X i)" by (unfold projecting_def, blast) lemma projecting_UN: - "[| !!i. i:I ==> projecting C h F (X' i) (X i) |] - ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)" + "[| !!i. i \ I ==> projecting C h F (X' i) (X i) |] + ==> projecting C h F (\i \ I. X' i) (\i \ I. X i)" by (unfold projecting_def, blast) lemma projecting_weaken: - "[| projecting C h F X' X; U'<=X'; X<=U |] ==> projecting C h F U' U" + "[| projecting C h F X' X; U'<=X'; X \ U |] ==> projecting C h F U' U" by (unfold projecting_def, auto) lemma projecting_weaken_L: @@ -132,26 +132,26 @@ lemma extending_Int: "[| extending C h F YA' YA; extending C h F YB' YB |] - ==> extending C h F (YA' Int YB') (YA Int YB)" + ==> extending C h F (YA' \ YB') (YA \ YB)" by (unfold extending_def, blast) lemma extending_Un: "[| extending C h F YA' YA; extending C h F YB' YB |] - ==> extending C h F (YA' Un YB') (YA Un YB)" + ==> extending C h F (YA' \ YB') (YA \ YB)" by (unfold extending_def, blast) lemma extending_INT: - "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] - ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)" + "[| !!i. i \ I ==> extending C h F (Y' i) (Y i) |] + ==> extending C h F (\i \ I. Y' i) (\i \ I. Y i)" by (unfold extending_def, blast) lemma extending_UN: - "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] - ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)" + "[| !!i. i \ I ==> extending C h F (Y' i) (Y i) |] + ==> extending C h F (\i \ I. Y' i) (\i \ I. Y i)" by (unfold extending_def, blast) lemma extending_weaken: - "[| extending C h F Y' Y; Y'<=V'; V<=Y |] ==> extending C h F V' V" + "[| extending C h F Y' Y; Y'<=V'; V \ Y |] ==> extending C h F V' V" by (unfold extending_def, auto) lemma extending_weaken_L: @@ -204,9 +204,9 @@ (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_imp_reachable_project: - "[| reachable (extend h F Join G) <= C; - z : reachable (extend h F Join G) |] - ==> f z : reachable (F Join project h C G)" + "[| reachable (extend h F Join G) \ C; + z \ reachable (extend h F Join G) |] + ==> f z \ reachable (F Join project h C G)" apply (erule reachable.induct) apply (force intro!: reachable.Init simp add: split_extended_all, auto) apply (rule_tac act = x in reachable.Acts) @@ -217,8 +217,8 @@ done lemma (in Extend) project_Constrains_D: - "F Join project h (reachable (extend h F Join G)) G : A Co B - ==> extend h F Join G : (extend_set h A) Co (extend_set h B)" + "F Join project h (reachable (extend h F Join G)) G \ A Co B + ==> extend h F Join G \ (extend_set h A) Co (extend_set h B)" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains, clarify) @@ -227,22 +227,22 @@ done lemma (in Extend) project_Stable_D: - "F Join project h (reachable (extend h F Join G)) G : Stable A - ==> extend h F Join G : Stable (extend_set h A)" + "F Join project h (reachable (extend h F Join G)) G \ Stable A + ==> extend h F Join G \ Stable (extend_set h A)" apply (unfold Stable_def) apply (simp (no_asm_simp) add: project_Constrains_D) done lemma (in Extend) project_Always_D: - "F Join project h (reachable (extend h F Join G)) G : Always A - ==> extend h F Join G : Always (extend_set h A)" + "F Join project h (reachable (extend h F Join G)) G \ Always A + ==> extend h F Join G \ Always (extend_set h A)" apply (unfold Always_def) apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all) done lemma (in Extend) project_Increasing_D: - "F Join project h (reachable (extend h F Join G)) G : Increasing func - ==> extend h F Join G : Increasing (func o f)" + "F Join project h (reachable (extend h F Join G)) G \ Increasing func + ==> extend h F Join G \ Increasing (func o f)" apply (unfold Increasing_def, auto) apply (subst extend_set_eq_Collect [symmetric]) apply (simp (no_asm_simp) add: project_Stable_D) @@ -253,9 +253,9 @@ (*In practice, C = reachable(...): the inclusion is equality*) lemma (in Extend) reachable_project_imp_reachable: - "[| C <= reachable(extend h F Join G); - x : reachable (F Join project h C G) |] - ==> EX y. h(x,y) : reachable (extend h F Join G)" + "[| C \ reachable(extend h F Join G); + x \ reachable (F Join project h C G) |] + ==> \y. h(x,y) \ reachable (extend h F Join G)" apply (erule reachable.induct) apply (force intro: reachable.Init) apply (auto simp add: project_act_def) @@ -270,15 +270,15 @@ (*UNUSED*) lemma (in Extend) reachable_extend_Join_subset: - "reachable (extend h F Join G) <= C - ==> reachable (extend h F Join G) <= + "reachable (extend h F Join G) \ C + ==> reachable (extend h F Join G) \ extend_set h (reachable (F Join project h C G))" apply (auto dest: reachable_imp_reachable_project) done lemma (in Extend) project_Constrains_I: - "extend h F Join G : (extend_set h A) Co (extend_set h B) - ==> F Join project h (reachable (extend h F Join G)) G : A Co B" + "extend h F Join G \ (extend_set h A) Co (extend_set h B) + ==> F Join project h (reachable (extend h F Join G)) G \ A Co B" apply (unfold Constrains_def) apply (simp del: Join_constrains add: Join_project_constrains extend_set_Int_distrib) @@ -291,43 +291,43 @@ done lemma (in Extend) project_Stable_I: - "extend h F Join G : Stable (extend_set h A) - ==> F Join project h (reachable (extend h F Join G)) G : Stable A" + "extend h F Join G \ Stable (extend_set h A) + ==> F Join project h (reachable (extend h F Join G)) G \ Stable A" apply (unfold Stable_def) apply (simp (no_asm_simp) add: project_Constrains_I) done lemma (in Extend) project_Always_I: - "extend h F Join G : Always (extend_set h A) - ==> F Join project h (reachable (extend h F Join G)) G : Always A" + "extend h F Join G \ Always (extend_set h A) + ==> F Join project h (reachable (extend h F Join G)) G \ Always A" apply (unfold Always_def) apply (auto simp add: project_Stable_I) apply (unfold extend_set_def, blast) done lemma (in Extend) project_Increasing_I: - "extend h F Join G : Increasing (func o f) - ==> F Join project h (reachable (extend h F Join G)) G : Increasing func" + "extend h F Join G \ Increasing (func o f) + ==> F Join project h (reachable (extend h F Join G)) G \ Increasing func" apply (unfold Increasing_def, auto) apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I) done lemma (in Extend) project_Constrains: - "(F Join project h (reachable (extend h F Join G)) G : A Co B) = - (extend h F Join G : (extend_set h A) Co (extend_set h B))" + "(F Join project h (reachable (extend h F Join G)) G \ A Co B) = + (extend h F Join G \ (extend_set h A) Co (extend_set h B))" apply (blast intro: project_Constrains_I project_Constrains_D) done lemma (in Extend) project_Stable: - "(F Join project h (reachable (extend h F Join G)) G : Stable A) = - (extend h F Join G : Stable (extend_set h A))" + "(F Join project h (reachable (extend h F Join G)) G \ Stable A) = + (extend h F Join G \ Stable (extend_set h A))" apply (unfold Stable_def) apply (rule project_Constrains) done lemma (in Extend) project_Increasing: - "(F Join project h (reachable (extend h F Join G)) G : Increasing func) = - (extend h F Join G : Increasing (func o f))" + "(F Join project h (reachable (extend h F Join G)) G \ Increasing func) = + (extend h F Join G \ Increasing (func o f))" apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) done @@ -397,30 +397,24 @@ subsubsection{*transient*} lemma (in Extend) transient_extend_set_imp_project_transient: - "[| G : transient (C Int extend_set h A); G : stable C |] - ==> project h C G : transient (project_set h C Int A)" - -apply (unfold transient_def) -apply (auto simp add: Domain_project_act) -apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A") -prefer 2 + "[| G \ transient (C \ extend_set h A); G \ stable C |] + ==> project h C G \ transient (project_set h C \ A)" +apply (auto simp add: transient_def Domain_project_act) +apply (subgoal_tac "act `` (C \ extend_set h A) \ - extend_set h A") + prefer 2 apply (simp add: stable_def constrains_def, blast) (*back to main goal*) -apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl) +apply (erule_tac V = "?AA \ -C \ ?BB" in thin_rl) apply (drule bspec, assumption) apply (simp add: extend_set_def project_act_def, blast) done (*converse might hold too?*) lemma (in Extend) project_extend_transient_D: - "project h C (extend h F) : transient (project_set h C Int D) - ==> F : transient (project_set h C Int D)" -apply (unfold transient_def) -apply (auto simp add: Domain_project_act) -apply (rule bexI) -prefer 2 apply assumption -apply auto -apply (unfold extend_act_def, blast) + "project h C (extend h F) \ transient (project_set h C \ D) + ==> F \ transient (project_set h C \ D)" +apply (simp add: transient_def Domain_project_act, safe) +apply blast+ done @@ -428,11 +422,12 @@ (*Used to prove project_leadsETo_I*) lemma (in Extend) ensures_extend_set_imp_project_ensures: - "[| extend h F : stable C; G : stable C; - extend h F Join G : A ensures B; A-B = C Int extend_set h D |] + "[| extend h F \ stable C; G \ stable C; + extend h F Join G \ A ensures B; A-B = C \ extend_set h D |] ==> F Join project h C G - : (project_set h C Int project_set h A) ensures (project_set h B)" -apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify) + \ (project_set h C \ project_set h A) ensures (project_set h B)" +apply (simp add: ensures_def project_constrains Join_transient extend_transient, + clarify) apply (intro conjI) (*first subgoal*) apply (blast intro: extend_stable_project_set @@ -457,19 +452,42 @@ [THEN project_extend_transient_D, THEN transient_strengthen]) done +text{*Transferring a transient property upwards*} +lemma (in Extend) project_transient_extend_set: + "project h C G \ transient (project_set h C \ A - B) + ==> G \ transient (C \ extend_set h A - extend_set h B)" +apply (simp add: transient_def project_set_def extend_set_def project_act_def) +apply (elim disjE bexE) + apply (rule_tac x=Id in bexI) + apply (blast intro!: rev_bexI )+ +done + +lemma (in Extend) project_unless2 [rule_format]: + "[| G \ stable C; project h C G \ (project_set h C \ A) unless B |] + ==> G \ (C \ extend_set h A) unless (extend_set h B)" +by (auto dest: stable_constrains_Int intro: constrains_weaken + simp add: unless_def project_constrains Diff_eq Int_assoc + Int_extend_set_lemma) + + +lemma (in Extend) extend_unless: + "[|extend h F \ stable C; F \ A unless B|] + ==> extend h F \ C \ extend_set h A unless extend_set h B" +apply (simp add: unless_def stable_def) +apply (drule constrains_Int) +apply (erule extend_constrains [THEN iffD2]) +apply (erule constrains_weaken, blast) +apply blast +done + (*Used to prove project_leadsETo_D*) lemma (in Extend) Join_project_ensures [rule_format]: - "[| project h C G ~: transient (A-B) | A<=B; - extend h F Join G : stable C; - F Join project h C G : A ensures B |] - ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)" -apply (erule disjE) -prefer 2 apply (blast intro: subset_imp_ensures) -apply (auto dest: extend_transient [THEN iffD2] - intro: transient_strengthen project_set_I - project_unless [THEN unlessD] unlessI - project_extend_constrains_I - simp add: ensures_def Join_transient) + "[| extend h F Join G \ stable C; + F Join project h C G \ A ensures B |] + ==> extend h F Join G \ (C \ extend_set h A) ensures (extend_set h B)" +apply (auto simp add: ensures_eq extend_unless project_unless) +apply (blast intro: extend_transient [THEN iffD2] transient_strengthen) +apply (blast intro: project_transient_extend_set transient_strengthen) done text{*Lemma useful for both STRONG and WEAK progress, but the transient @@ -478,11 +496,10 @@ (*The strange induction formula allows induction over the leadsTo assumption's non-atomic precondition*) lemma (in Extend) PLD_lemma: - "[| ALL D. project h C G : transient D --> D={}; - extend h F Join G : stable C; - F Join project h C G : (project_set h C Int A) leadsTo B |] - ==> extend h F Join G : - C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)" + "[| extend h F Join G \ stable C; + F Join project h C G \ (project_set h C \ A) leadsTo B |] + ==> extend h F Join G \ + C \ extend_set h (project_set h C \ A) leadsTo (extend_set h B)" apply (erule leadsTo_induct) apply (blast intro: leadsTo_Basis Join_project_ensures) apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans) @@ -490,74 +507,28 @@ done lemma (in Extend) project_leadsTo_D_lemma: - "[| ALL D. project h C G : transient D --> D={}; - extend h F Join G : stable C; - F Join project h C G : (project_set h C Int A) leadsTo B |] - ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)" + "[| extend h F Join G \ stable C; + F Join project h C G \ (project_set h C \ A) leadsTo B |] + ==> extend h F Join G \ (C \ extend_set h A) leadsTo (extend_set h B)" apply (rule PLD_lemma [THEN leadsTo_weaken]) apply (auto simp add: split_extended_all) done lemma (in Extend) Join_project_LeadsTo: "[| C = (reachable (extend h F Join G)); - ALL D. project h C G : transient D --> D={}; - F Join project h C G : A LeadsTo B |] - ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)" + F Join project h C G \ A LeadsTo B |] + ==> extend h F Join G \ (extend_set h A) LeadsTo (extend_set h B)" by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma project_set_reachable_extend_eq) subsection{*Towards the theorem @{text project_Ensures_D}*} - -lemma (in Extend) act_subset_imp_project_act_subset: - "act `` (C Int extend_set h A) <= B - ==> project_act h (Restrict C act) `` (project_set h C Int A) - <= project_set h B" -apply (unfold project_set_def extend_set_def project_act_def, blast) -done - -(*This trivial proof is the complementation part of transferring a transient - property upwards. The hard part would be to - show that G's action has a big enough domain.*) -lemma (in Extend) - "[| act: Acts G; - (project_act h (Restrict C act))`` - (project_set h C Int A - B) <= -(project_set h C Int A - B) |] - ==> act``(C Int extend_set h A - extend_set h B) - <= -(C Int extend_set h A - extend_set h B)" -by (auto simp add: project_set_def extend_set_def project_act_def) - -lemma (in Extend) stable_project_transient: - "[| G : stable ((C Int extend_set h A) - (extend_set h B)); - project h C G : transient (project_set h C Int A - B) |] - ==> (C Int extend_set h A) - extend_set h B = {}" -apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast) -apply (auto simp add: stable_def constrains_def) -apply (drule bspec, assumption) -apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric]) -apply (drule act_subset_imp_project_act_subset) -apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}") -apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+ -apply (unfold project_set_def extend_set_def project_act_def) -prefer 2 apply blast -apply (rule ccontr) -apply (drule subsetD, blast) -apply (force simp add: split_extended_all) -done - -lemma (in Extend) project_unless2 [rule_format]: - "[| G : stable C; project h C G : (project_set h C Int A) unless B |] - ==> G : (C Int extend_set h A) unless (extend_set h B)" -by (auto dest: stable_constrains_Int intro: constrains_weaken - simp add: unless_def project_constrains Diff_eq Int_assoc - Int_extend_set_lemma) - lemma (in Extend) project_ensures_D_lemma: - "[| G : stable ((C Int extend_set h A) - (extend_set h B)); - F Join project h C G : (project_set h C Int A) ensures B; - extend h F Join G : stable C |] - ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)" + "[| G \ stable ((C \ extend_set h A) - (extend_set h B)); + F Join project h C G \ (project_set h C \ A) ensures B; + extend h F Join G \ stable C |] + ==> extend h F Join G \ (C \ extend_set h A) ensures (extend_set h B)" (*unless*) apply (auto intro!: project_unless2 [unfolded unless_def] intro: project_extend_constrains_I @@ -565,26 +536,24 @@ (*transient*) (*A G-action cannot occur*) prefer 2 - apply (force dest: stable_project_transient - simp del: Diff_eq_empty_iff - simp add: Diff_eq_empty_iff [symmetric]) + apply (blast intro: project_transient_extend_set) (*An F-action*) apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen] simp add: split_extended_all) done lemma (in Extend) project_ensures_D: - "[| F Join project h UNIV G : A ensures B; - G : stable (extend_set h A - extend_set h B) |] - ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)" + "[| F Join project h UNIV G \ A ensures B; + G \ stable (extend_set h A - extend_set h B) |] + ==> extend h F Join G \ (extend_set h A) ensures (extend_set h B)" apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto) done lemma (in Extend) project_Ensures_D: - "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B; - G : stable (reachable (extend h F Join G) Int extend_set h A - + "[| F Join project h (reachable (extend h F Join G)) G \ A Ensures B; + G \ stable (reachable (extend h F Join G) \ extend_set h A - extend_set h B) |] - ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)" + ==> extend h F Join G \ (extend_set h A) Ensures (extend_set h B)" apply (unfold Ensures_def) apply (rule project_ensures_D_lemma [THEN revcut_rl]) apply (auto simp add: project_set_reachable_extend_eq [symmetric]) @@ -594,7 +563,7 @@ subsection{*Guarantees*} lemma (in Extend) project_act_Restrict_subset_project_act: - "project_act h (Restrict C act) <= project_act h act" + "project_act h (Restrict C act) \ project_act h act" apply (auto simp add: project_act_def) done @@ -616,24 +585,24 @@ Not clear that it has a converse [or that we want one!]*) (*The raw version; 3rd premise could be weakened by adding the - precondition extend h F Join G : X' *) + precondition extend h F Join G \ X' *) lemma (in Extend) project_guarantees_raw: - assumes xguary: "F : X guarantees Y" + assumes xguary: "F \ X guarantees Y" and closed: "subset_closed (AllowedActs F)" - and project: "!!G. extend h F Join G : X' - ==> F Join project h (C G) G : X" - and extend: "!!G. [| F Join project h (C G) G : Y |] - ==> extend h F Join G : Y'" - shows "extend h F : X' guarantees Y'" + and project: "!!G. extend h F Join G \ X' + ==> F Join project h (C G) G \ X" + and extend: "!!G. [| F Join project h (C G) G \ Y |] + ==> extend h F Join G \ Y'" + shows "extend h F \ X' guarantees Y'" apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI]) apply (blast intro: closed subset_closed_ok_extend_imp_ok_project) apply (erule project) done lemma (in Extend) project_guarantees: - "[| F : X guarantees Y; subset_closed (AllowedActs F); + "[| F \ X guarantees Y; subset_closed (AllowedActs F); projecting C h F X' X; extending C h F Y' Y |] - ==> extend h F : X' guarantees Y'" + ==> extend h F \ X' guarantees Y'" apply (rule guaranteesI) apply (auto simp add: guaranteesD projecting_def extending_def subset_closed_ok_extend_imp_ok_project) @@ -648,73 +617,58 @@ subsubsection{*Some could be deleted: the required versions are easy to prove*} lemma (in Extend) extend_guar_increasing: - "[| F : UNIV guarantees increasing func; + "[| F \ UNIV guarantees increasing func; subset_closed (AllowedActs F) |] - ==> extend h F : X' guarantees increasing (func o f)" + ==> extend h F \ X' guarantees increasing (func o f)" apply (erule project_guarantees) apply (rule_tac [3] extending_increasing) apply (rule_tac [2] projecting_UNIV, auto) done lemma (in Extend) extend_guar_Increasing: - "[| F : UNIV guarantees Increasing func; + "[| F \ UNIV guarantees Increasing func; subset_closed (AllowedActs F) |] - ==> extend h F : X' guarantees Increasing (func o f)" + ==> extend h F \ X' guarantees Increasing (func o f)" apply (erule project_guarantees) apply (rule_tac [3] extending_Increasing) apply (rule_tac [2] projecting_UNIV, auto) done lemma (in Extend) extend_guar_Always: - "[| F : Always A guarantees Always B; + "[| F \ Always A guarantees Always B; subset_closed (AllowedActs F) |] ==> extend h F - : Always(extend_set h A) guarantees Always(extend_set h B)" + \ Always(extend_set h A) guarantees Always(extend_set h B)" apply (erule project_guarantees) apply (rule_tac [3] extending_Always) apply (rule_tac [2] projecting_Always, auto) done -lemma (in Extend) preserves_project_transient_empty: - "[| G : preserves f; project h C G : transient D |] ==> D={}" -apply (rule stable_transient_empty) - prefer 2 apply assumption -apply (blast intro: project_preserves_id_I - preserves_id_subset_stable [THEN subsetD]) -done - -subsubsection{*Guarantees with a leadsTo postcondition - ALL TOO WEAK because G can't affect F's variables at all**) +subsubsection{*Guarantees with a leadsTo postcondition*} lemma (in Extend) project_leadsTo_D: - "[| F Join project h UNIV G : A leadsTo B; - G : preserves f |] - ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)" -apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken]) -apply (auto dest: preserves_project_transient_empty) + "F Join project h UNIV G \ A leadsTo B + ==> extend h F Join G \ (extend_set h A) leadsTo (extend_set h B)" +apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto) done lemma (in Extend) project_LeadsTo_D: - "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; - G : preserves f |] - ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)" -apply (rule refl [THEN Join_project_LeadsTo]) -apply (auto dest: preserves_project_transient_empty) + "F Join project h (reachable (extend h F Join G)) G \ A LeadsTo B + ==> extend h F Join G \ (extend_set h A) LeadsTo (extend_set h B)" +apply (rule refl [THEN Join_project_LeadsTo], auto) done lemma (in Extend) extending_leadsTo: - "(ALL G. extend h F ok G --> G : preserves f) - ==> extending (%G. UNIV) h F - (extend_set h A leadsTo extend_set h B) (A leadsTo B)" + "extending (%G. UNIV) h F + (extend_set h A leadsTo extend_set h B) (A leadsTo B)" apply (unfold extending_def) apply (blast intro: project_leadsTo_D) done lemma (in Extend) extending_LeadsTo: - "(ALL G. extend h F ok G --> G : preserves f) - ==> extending (%G. reachable (extend h F Join G)) h F - (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" + "extending (%G. reachable (extend h F Join G)) h F + (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" apply (unfold extending_def) apply (blast intro: project_LeadsTo_D) done diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/Common.thy Sat Feb 08 16:05:33 2003 +0100 @@ -54,20 +54,27 @@ by (simp add: constrains_def maxfg_def le_max_iff_disj fasc) (*This one is t := ftime t || t := gtime t*) -lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) +lemma "mk_total_program + (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \ {m} co (maxfg m)" -by (simp add: constrains_def maxfg_def le_max_iff_disj fasc) +apply (simp add: mk_total_program_def) +apply (simp add: constrains_def maxfg_def le_max_iff_disj fasc) +done (*This one is t := max (ftime t) (gtime t)*) -lemma "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) +lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \ {m} co (maxfg m)" -by (simp add: constrains_def maxfg_def max_def gasc) +apply (simp add: mk_total_program_def) +apply (simp add: constrains_def maxfg_def max_def gasc) +done (*This one is t := t+1 if t {m} co (maxfg m)" -by (simp add: constrains_def maxfg_def max_def gasc) +apply (simp add: mk_total_program_def) +apply (simp add: constrains_def maxfg_def max_def gasc) +done (*It remans to prove that they satisfy CMT3': t does not decrease, diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/Lift.thy --- a/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/Lift.thy Sat Feb 08 16:05:33 2003 +0100 @@ -120,11 +120,12 @@ Lift :: "state program" (*for the moment, we OMIT button_press*) - "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & + "Lift == mk_total_program + ({s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, - {request_act, open_act, close_act, - req_up, req_down, move_up, move_down}, - UNIV)" + {request_act, open_act, close_act, + req_up, req_down, move_up, move_down}, + UNIV)" (** Invariants **) @@ -196,7 +197,7 @@ lemma open_stop: "Lift \ Always open_stop" apply (rule AlwaysI, force) -apply (unfold Lift_def, constrains) +apply (unfold Lift_def, constrains) done lemma stop_floor: "Lift \ Always stop_floor" @@ -249,19 +250,22 @@ apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_5*) + + + lemma E_thm02: "Lift \ (Req n \ stopped - atFloor n) LeadsTo - (Req n \ opened - atFloor n)" + (Req n \ opened - atFloor n)" apply (cut_tac stop_floor) apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_1*) lemma E_thm03: "Lift \ (Req n \ opened - atFloor n) LeadsTo - (Req n \ closed - (atFloor n - queueing))" + (Req n \ closed - (atFloor n - queueing))" apply (unfold Lift_def, ensures_tac "close_act") done (*lem_lift_1_2*) lemma E_thm04: "Lift \ (Req n \ closed \ (atFloor n - queueing)) - LeadsTo (opened \ atFloor n)" + LeadsTo (opened \ atFloor n)" apply (unfold Lift_def, ensures_tac "open_act") done (*lem_lift_1_7*) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/Mutex.thy --- a/src/HOL/UNITY/Simple/Mutex.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/Mutex.thy Sat Feb 08 16:05:33 2003 +0100 @@ -54,9 +54,10 @@ "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" Mutex :: "state program" - "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, - {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, - UNIV)" + "Mutex == mk_total_program + ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, + {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, + UNIV)" (** The correct invariants **) diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/NSP_Bad.ML --- a/src/HOL/UNITY/Simple/NSP_Bad.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Sat Feb 08 16:05:33 2003 +0100 @@ -22,8 +22,7 @@ Here, it facilitates re-use of the Auth proofs.*) AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]); - -Addsimps [Nprg_def RS def_prg_simps]; +Addsimps [Nprg_def RS def_prg_Init]; (*A "possibility property": there are traces that reach the end. @@ -31,12 +30,13 @@ Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \ \ Says A B (Crypt (pubK B) (Nonce NB)) : set s"; by (REPEAT (resolve_tac [exI,bexI] 1)); -by (res_inst_tac [("act", "NS3")] reachable_Acts 2); -by (res_inst_tac [("act", "NS2")] reachable_Acts 3); -by (res_inst_tac [("act", "NS1")] reachable_Acts 4); +by (res_inst_tac [("act", "totalize_act NS3")] reachable_Acts 2); +by (res_inst_tac [("act", "totalize_act NS2")] reachable_Acts 3); +by (res_inst_tac [("act", "totalize_act NS1")] reachable_Acts 4); by (rtac reachable_Init 5); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def]))); -by (REPEAT_FIRST (rtac exI )); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def, totalize_act_def]))); + (*Now ignore the possibility of identity transitions*) +by (REPEAT_FIRST (resolve_tac [disjI1, exI])); by possibility_tac; result(); @@ -54,12 +54,23 @@ by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset())); *) +val [prem] = +Goal "(!!act s s'. [| act: {Id, Fake, NS1, NS2, NS3}; \ +\ (s,s') \\ act; s \\ A |] ==> s': A') \ +\ ==> Nprg \\ A co A'"; +by (asm_full_simp_tac (simpset() addsimps [Nprg_def, mk_total_program_def]) 1); +by (rtac constrainsI 1); +by (rtac prem 1); +by Auto_tac; +qed "ns_constrainsI"; + + fun ns_constrains_tac i = SELECT_GOAL (EVERY [REPEAT (etac Always_ConstrainsI 1), REPEAT (resolve_tac [StableI, stableI, constrains_imp_Constrains] 1), - rtac constrainsI 1, + rtac ns_constrainsI 1, Full_simp_tac 1, REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS (clarify_tac (claset() delrules [impI,impCE])), diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Feb 08 16:05:33 2003 +0100 @@ -54,6 +54,6 @@ constdefs Nprg :: state program (*Initial trace is empty*) - "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" + "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Simple/Reach.thy --- a/src/HOL/UNITY/Simple/Reach.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Simple/Reach.thy Sat Feb 08 16:05:33 2003 +0100 @@ -24,7 +24,7 @@ "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" Rprg :: "state program" - "Rprg == mk_program ({%v. v=init}, \(u,v)\edges. {asgt u v}, UNIV)" + "Rprg == mk_total_program ({%v. v=init}, \(u,v)\edges. {asgt u v}, UNIV)" reach_invariant :: "state set" "reach_invariant == {s. (\v. s v --> (init, v) \ edges^*) & s init}" @@ -81,7 +81,8 @@ lemma lemma1: "FP Rprg \ fixedpoint" -apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto) +apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def) +apply (auto simp add: stable_def constrains_def) apply (drule bspec, assumption) apply (simp add: Image_singleton image_iff) apply (drule fun_cong, auto) @@ -89,8 +90,8 @@ lemma lemma2: "fixedpoint \ FP Rprg" -apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def) -apply (auto intro!: ext) +apply (simp add: FP_def fixedpoint_def Rprg_def mk_total_program_def) +apply (auto intro!: ext simp add: stable_def constrains_def) done lemma FP_fixedpoint: "FP Rprg = fixedpoint" @@ -104,7 +105,8 @@ *) lemma Compl_fixedpoint: "- fixedpoint = (\(u,v)\edges. {s. s u & ~ s v})" -apply (auto simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def) +apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def) +apply (auto simp add: Compl_FP UN_UN_flatten) apply (rule fun_upd_idem, force) apply (force intro!: rev_bexI simp add: fun_upd_idem_iff) done diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/SubstAx.thy --- a/src/HOL/UNITY/SubstAx.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Sat Feb 08 16:05:33 2003 +0100 @@ -21,7 +21,7 @@ "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \w " 60) -(*Resembles the previous definition of LeadsTo*) +text{*Resembles the previous definition of LeadsTo*} lemma LeadsTo_eq_leadsTo: "A LeadsTo B = {F. F \ (reachable F \ A) leadsTo (reachable F \ B)}" apply (unfold LeadsTo_def) @@ -76,7 +76,7 @@ lemma LeadsTo_UNIV [simp]: "F \ A LeadsTo UNIV" by (simp add: LeadsTo_def) -(*Useful with cancellation, disjunction*) +text{*Useful with cancellation, disjunction*} lemma LeadsTo_Un_duplicate: "F \ A LeadsTo (A' \ A') ==> F \ A LeadsTo A'" by (simp add: Un_ac) @@ -91,14 +91,14 @@ apply (blast intro: LeadsTo_Union) done -(*Binary union introduction rule*) +text{*Binary union introduction rule*} lemma LeadsTo_Un: "[| F \ A LeadsTo C; F \ B LeadsTo C |] ==> F \ (A \ B) LeadsTo C" apply (subst Un_eq_Union) apply (blast intro: LeadsTo_Union) done -(*Lets us look at the starting state*) +text{*Lets us look at the starting state*} lemma single_LeadsTo_I: "(!!s. s \ A ==> F \ {s} LeadsTo B) ==> F \ A LeadsTo B" by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) @@ -182,8 +182,8 @@ apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) done -(*Set difference: maybe combine with leadsTo_weaken_L?? - This is the most useful form of the "disjunction" rule*) +text{*Set difference: maybe combine with leadsTo_weaken_L?? + This is the most useful form of the "disjunction" rule*} lemma LeadsTo_Diff: "[| F \ (A-B) LeadsTo C; F \ (A \ B) LeadsTo C |] ==> F \ A LeadsTo C" @@ -198,18 +198,18 @@ done -(*Version with no index set*) +text{*Version with no index set*} lemma LeadsTo_UN_UN_noindex: "(!!i. F \ (A i) LeadsTo (A' i)) ==> F \ (\i. A i) LeadsTo (\i. A' i)" by (blast intro: LeadsTo_UN_UN) -(*Version with no index set*) +text{*Version with no index set*} lemma all_LeadsTo_UN_UN: "\i. F \ (A i) LeadsTo (A' i) ==> F \ (\i. A i) LeadsTo (\i. A' i)" by (blast intro: LeadsTo_UN_UN) -(*Binary union version*) +text{*Binary union version*} lemma LeadsTo_Un_Un: "[| F \ A LeadsTo A'; F \ B LeadsTo B' |] ==> F \ (A \ B) LeadsTo (A' \ B')" @@ -247,18 +247,18 @@ done -(** The impossibility law **) +text{*The impossibility law*} -(*The set "A" may be non-empty, but it contains no reachable states*) -lemma LeadsTo_empty: "F \ A LeadsTo {} ==> F \ Always (-A)" +text{*The set "A" may be non-empty, but it contains no reachable states*} +lemma LeadsTo_empty: "[|F \ A LeadsTo {}; all_total F|] ==> F \ Always (-A)" apply (simp add: LeadsTo_def Always_eq_includes_reachable) apply (drule leadsTo_empty, auto) done -(** PSP: Progress-Safety-Progress **) +subsection{*PSP: Progress-Safety-Progress*} -(*Special case of PSP: Misra's "stable conjunction"*) +text{*Special case of PSP: Misra's "stable conjunction"*} lemma PSP_Stable: "[| F \ A LeadsTo A'; F \ Stable B |] ==> F \ (A \ B) LeadsTo (A' \ B)" @@ -336,7 +336,7 @@ ==> F \ A LeadsTo B" by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) -(*Integer version. Could generalize from 0 to any lower bound*) +text{*Integer version. Could generalize from 0 to any lower bound*} lemma integ_0_le_induct: "[| F \ Always {s. (0::int) \ f s}; !! z. F \ (A \ {s. f s = z}) LeadsTo diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/UNITY.thy Sat Feb 08 16:05:33 2003 +0100 @@ -50,12 +50,12 @@ invariant :: "'a set => 'a program set" "invariant A == {F. Init F \ A} \ stable A" - (*Polymorphic in both states and the meaning of \ *) increasing :: "['a => 'b::{order}] => 'a program set" + --{*Polymorphic in both states and the meaning of @{text "\"}*} "increasing f == \z. stable {s. z \ f s}" -(*Perhaps equalities.ML shouldn't add this in the first place!*) +text{*Perhaps equalities.ML shouldn't add this in the first place!*} declare image_Collect [simp del] (*** The abstract type of programs ***) @@ -83,14 +83,14 @@ (** Inspectors for type "program" **) lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init" -by (auto simp add: program_typedef) +by (simp add: program_typedef) lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts" -by (auto simp add: program_typedef) +by (simp add: program_typedef) lemma AllowedActs_eq [simp]: "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed" -by (auto simp add: program_typedef) +by (simp add: program_typedef) (** Equality for UNITY programs **) @@ -121,38 +121,6 @@ by (blast intro: program_equalityI program_equalityE) -(*** These rules allow "lazy" definition expansion - They avoid expanding the full program, which is a large expression -***) - -lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init" -by auto - -lemma def_prg_Acts: - "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts" -by auto - -lemma def_prg_AllowedActs: - "F == mk_program (init,acts,allowed) - ==> AllowedActs F = insert Id allowed" -by auto - -(*The program is not expanded, but its Init and Acts are*) -lemma def_prg_simps: - "[| F == mk_program (init,acts,allowed) |] - ==> Init F = init & Acts F = insert Id acts" -by simp - -(*An action is expanded only if a pair of states is being tested against it*) -lemma def_act_simp: - "[| act == {(s,s'). P s s'} |] ==> ((s,s') \ act) = P s s'" -by auto - -(*A set is expanded only if an element is being tested against it*) -lemma def_set_simp: "A == B ==> (x \ A) = (x \ B)" -by auto - - (*** co ***) lemma constrainsI: @@ -176,12 +144,12 @@ lemma constrains_UNIV2 [iff]: "F \ A co UNIV" by (unfold constrains_def, blast) -(*monotonic in 2nd argument*) +text{*monotonic in 2nd argument*} lemma constrains_weaken_R: "[| F \ A co A'; A'<=B' |] ==> F \ A co B'" by (unfold constrains_def, blast) -(*anti-monotonic in 1st argument*) +text{*anti-monotonic in 1st argument*} lemma constrains_weaken_L: "[| F \ A co A'; B \ A |] ==> F \ B co A'" by (unfold constrains_def, blast) @@ -227,8 +195,8 @@ lemma constrains_imp_subset: "F \ A co A' ==> A \ A'" by (unfold constrains_def, auto) -(*The reasoning is by subsets since "co" refers to single actions - only. So this rule isn't that useful.*) +text{*The reasoning is by subsets since "co" refers to single actions + only. So this rule isn't that useful.*} lemma constrains_trans: "[| F \ A co B; F \ B co C |] ==> F \ A co C" by (unfold constrains_def, blast) @@ -304,7 +272,7 @@ lemma invariantI: "[| Init F \ A; F \ stable A |] ==> F \ invariant A" by (simp add: invariant_def) -(*Could also say "invariant A \ invariant B \ invariant (A \ B)"*) +text{*Could also say "invariant A \ invariant B \ invariant (A \ B)"*} lemma invariant_Int: "[| F \ invariant A; F \ invariant B |] ==> F \ invariant (A \ B)" by (auto simp add: invariant_def stable_Int) @@ -314,7 +282,6 @@ lemma increasingD: "F \ increasing f ==> F \ stable {s. z \ f s}" - by (unfold increasing_def, blast) lemma increasing_constant [iff]: "F \ increasing (%s. c)" @@ -341,8 +308,8 @@ ==> F \ {s. s x \ M} co (\m \ M. B m)" by (unfold constrains_def, blast) -(*As above, but for the trivial case of a one-variable state, in which the - state is identified with its one variable.*) +text{*As above, but for the trivial case of a one-variable state, in which the + state is identified with its one variable.*} lemma elimination_sing: "(\m \ M. F \ {m} co (B m)) ==> F \ M co (\m \ M. B m)" by (unfold constrains_def, blast) @@ -376,4 +343,119 @@ lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k" by blast + +subsection{*Partial versus Total Transitions*} + +constdefs + totalize_act :: "('a * 'a)set => ('a * 'a)set" + "totalize_act act == act \ diag (-(Domain act))" + + totalize :: "'a program => 'a program" + "totalize F == mk_program (Init F, + totalize_act ` Acts F, + AllowedActs F)" + + mk_total_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set) + => 'a program" + "mk_total_program args == totalize (mk_program args)" + + all_total :: "'a program => bool" + "all_total F == \act \ Acts F. Domain act = UNIV" + +lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F" +by (blast intro: sym [THEN image_eqI]) + + +text{*Basic properties*} + +lemma totalize_act_Id [simp]: "totalize_act Id = Id" +by (simp add: totalize_act_def) + +lemma Domain_totalize_act [simp]: "Domain (totalize_act act) = UNIV" +by (auto simp add: totalize_act_def) + +lemma Init_totalize [simp]: "Init (totalize F) = Init F" +by (unfold totalize_def, auto) + +lemma Acts_totalize [simp]: "Acts (totalize F) = (totalize_act ` Acts F)" +by (simp add: totalize_def insert_Id_image_Acts) + +lemma AllowedActs_totalize [simp]: "AllowedActs (totalize F) = AllowedActs F" +by (simp add: totalize_def) + +lemma totalize_constrains_iff [simp]: "(totalize F \ A co B) = (F \ A co B)" +by (simp add: totalize_def totalize_act_def constrains_def, blast) + +lemma totalize_stable_iff [simp]: "(totalize F \ stable A) = (F \ stable A)" +by (simp add: stable_def) + +lemma totalize_invariant_iff [simp]: + "(totalize F \ invariant A) = (F \ invariant A)" +by (simp add: invariant_def) + +lemma all_total_totalize: "all_total (totalize F)" +by (simp add: totalize_def all_total_def) + +lemma Domain_iff_totalize_act: "(Domain act = UNIV) = (totalize_act act = act)" +by (force simp add: totalize_act_def) + +lemma all_total_imp_totalize: "all_total F ==> (totalize F = F)" +apply (simp add: all_total_def totalize_def) +apply (rule program_equalityI) + apply (simp_all add: Domain_iff_totalize_act image_def) +done + +lemma all_total_iff_totalize: "all_total F = (totalize F = F)" +apply (rule iffI) + apply (erule all_total_imp_totalize) +apply (erule subst) +apply (rule all_total_totalize) +done + +lemma mk_total_program_constrains_iff [simp]: + "(mk_total_program args \ A co B) = (mk_program args \ A co B)" +by (simp add: mk_total_program_def) + + +subsection{*Rules for Lazy Definition Expansion*} + +text{*They avoid expanding the full program, which is a large expression*} + +lemma def_prg_Init: + "F == mk_total_program (init,acts,allowed) ==> Init F = init" +by (simp add: mk_total_program_def) + +lemma def_prg_Acts: + "F == mk_total_program (init,acts,allowed) + ==> Acts F = insert Id (totalize_act ` acts)" +by (simp add: mk_total_program_def) + +lemma def_prg_AllowedActs: + "F == mk_total_program (init,acts,allowed) + ==> AllowedActs F = insert Id allowed" +by (simp add: mk_total_program_def) + +text{*An action is expanded if a pair of states is being tested against it*} +lemma def_act_simp: + "act == {(s,s'). P s s'} ==> ((s,s') \ act) = P s s'" +by (simp add: mk_total_program_def) + +text{*A set is expanded only if an element is being tested against it*} +lemma def_set_simp: "A == B ==> (x \ A) = (x \ B)" +by (simp add: mk_total_program_def) + +(** Inspectors for type "program" **) + +lemma Init_total_eq [simp]: + "Init (mk_total_program (init,acts,allowed)) = init" +by (simp add: mk_total_program_def) + +lemma Acts_total_eq [simp]: + "Acts(mk_total_program(init,acts,allowed)) = insert Id (totalize_act`acts)" +by (simp add: mk_total_program_def) + +lemma AllowedActs_total_eq [simp]: + "AllowedActs (mk_total_program (init,acts,allowed)) = insert Id allowed" +by (auto simp add: mk_total_program_def) + end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Feb 08 16:05:33 2003 +0100 @@ -72,6 +72,8 @@ (*UNITY*) +val mk_total_program_def = thm "mk_total_program_def"; +val totalize_act_def = thm "totalize_act_def"; val constrains_def = thm "constrains_def"; val stable_def = thm "stable_def"; val invariant_def = thm "invariant_def"; @@ -91,7 +93,6 @@ val def_prg_Init = thm "def_prg_Init"; val def_prg_Acts = thm "def_prg_Acts"; val def_prg_AllowedActs = thm "def_prg_AllowedActs"; -val def_prg_simps = thm "def_prg_simps"; val def_act_simp = thm "def_act_simp"; val def_set_simp = thm "def_set_simp"; val constrainsI = thm "constrainsI"; @@ -140,13 +141,14 @@ val Int_Union_Union = thm "Int_Union_Union"; val Image_less_than = thm "Image_less_than"; val Image_inverse_less_than = thm "Image_inverse_less_than"; +val totalize_constrains_iff = thm "totalize_constrains_iff"; (*WFair*) val stable_transient_empty = thm "stable_transient_empty"; val transient_strengthen = thm "transient_strengthen"; val transientI = thm "transientI"; +val totalize_transientI = thm "totalize_transientI"; val transientE = thm "transientE"; -val transient_UNIV = thm "transient_UNIV"; val transient_empty = thm "transient_empty"; val ensuresI = thm "ensuresI"; val ensuresD = thm "ensuresD"; @@ -415,12 +417,14 @@ val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; val Allowed_eq = thm "Allowed_eq"; val def_prg_Allowed = thm "def_prg_Allowed"; +val def_total_prg_Allowed = thm "def_total_prg_Allowed"; val safety_prop_constrains = thm "safety_prop_constrains"; val safety_prop_stable = thm "safety_prop_stable"; val safety_prop_Int = thm "safety_prop_Int"; val safety_prop_INTER1 = thm "safety_prop_INTER1"; val safety_prop_INTER = thm "safety_prop_INTER"; val def_UNION_ok_iff = thm "def_UNION_ok_iff"; +val totalize_JN = thm "totalize_JN"; (*Comp*) val preserves_def = thm "preserves_def"; @@ -670,11 +674,6 @@ val mem_lift_act_iff = thm "mem_lift_act_iff"; val preserves_snd_lift_stable = thm "preserves_snd_lift_stable"; val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains"; -val insert_map_upd_same = thm "insert_map_upd_same"; -val insert_map_upd = thm "insert_map_upd"; -val insert_map_eq_diff = thm "insert_map_eq_diff"; -val lift_map_eq_diff = thm "lift_map_eq_diff"; -val lift_transient_eq_disj = thm "lift_transient_eq_disj"; val lift_map_image_Times = thm "lift_map_image_Times"; val lift_preserves_eq = thm "lift_preserves_eq"; val lift_preserves_sub = thm "lift_preserves_sub"; @@ -751,14 +750,19 @@ (*Combines a list of invariance THEOREMS into one.*) val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I) -(*proves "co" properties when the program is specified*) +(*Proves "co" properties when the program is specified. Any use of invariants + (from weak constrains) must have been done already.*) fun gen_constrains_tac(cs,ss) i = SELECT_GOAL (EVERY [REPEAT (Always_Int_tac 1), + (*reduce the fancy safety properties to "constrains"*) REPEAT (etac Always_ConstrainsI 1 ORELSE resolve_tac [StableI, stableI, constrains_imp_Constrains] 1), + (*for safety, the totalize operator can be ignored*) + simp_tac (HOL_ss addsimps + [mk_total_program_def, totalize_constrains_iff]) 1, rtac constrainsI 1, full_simp_tac ss 1, REPEAT (FIRSTGOAL (etac disjE)), @@ -774,8 +778,9 @@ REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis, EnsuresI, ensuresI] 1), (*now there are two subgoals: co & transient*) - simp_tac ss 2, - res_inst_tac [("act", sact)] transientI 2, + simp_tac (ss addsimps [mk_total_program_def]) 2, + res_inst_tac [("act", sact)] totalize_transientI 2 + ORELSE res_inst_tac [("act", sact)] transientI 2, (*simplify the command's domain*) simp_tac (ss addsimps [Domain_def]) 3, gen_constrains_tac (cs,ss) 1, diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/Union.thy Sat Feb 08 16:05:33 2003 +0100 @@ -32,7 +32,7 @@ SKIP :: "'a program" "SKIP == mk_program (UNIV, {}, UNIV)" - (*Characterizes safety properties. Used with specifying AllowedActs*) + (*Characterizes safety properties. Used with specifying Allowed*) safety_prop :: "'a program set => bool" "safety_prop X == SKIP: X & (\G. Acts G \ UNION X Acts --> G \ X)" @@ -316,10 +316,10 @@ subsection{*the ok and OK relations*} lemma ok_SKIP1 [iff]: "SKIP ok F" -by (auto simp add: ok_def) +by (simp add: ok_def) lemma ok_SKIP2 [iff]: "F ok SKIP" -by (auto simp add: ok_def) +by (simp add: ok_def) lemma ok_Join_commute: "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))" @@ -332,7 +332,8 @@ lemma ok_iff_OK: "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)" -by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast) +by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb + all_conj_distrib eq_commute, blast) lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)" by (auto simp add: ok_def) @@ -374,7 +375,7 @@ lemma OK_iff_Allowed: "OK I F = (\i \ I. \j \ I-{i}. F i \ Allowed(F j))" by (auto simp add: OK_iff_ok ok_iff_Allowed) -subsection{*@{text safety_prop}, for reasoning about +subsection{*@{term safety_prop}, for reasoning about given instances of "ok"*} lemma safety_prop_Acts_iff: @@ -389,11 +390,6 @@ "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X" by (simp add: Allowed_def safety_prop_Acts_iff) -lemma def_prg_Allowed: - "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] - ==> Allowed F = X" -by (simp add: Allowed_eq) - (*For safety_prop to hold, the property must be satisfiable!*) lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \ B)" by (simp add: safety_prop_def constrains_def, blast) @@ -413,9 +409,35 @@ "(!!i. i \ I ==> safety_prop (X i)) ==> safety_prop (\i \ I. X i)" by (auto simp add: safety_prop_def, blast) +lemma def_prg_Allowed: + "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] + ==> Allowed F = X" +by (simp add: Allowed_eq) + +lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F" +by (simp add: Allowed_def) + +lemma def_total_prg_Allowed: + "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |] + ==> Allowed F = X" +by (simp add: mk_total_program_def def_prg_Allowed) + lemma def_UNION_ok_iff: "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] ==> F ok G = (G \ X & acts \ AllowedActs G)" by (auto simp add: ok_def safety_prop_Acts_iff) +text{*The union of two total programs is total.*} +lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)" +by (simp add: program_equalityI totalize_def Join_def image_Un) + +lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)" +by (simp add: all_total_def, blast) + +lemma totalize_JN: "(\i \ I. totalize (F i)) = totalize(\i \ I. F i)" +by (simp add: program_equalityI totalize_def JOIN_def image_UN) + +lemma all_total_JN: "(!!i. i\I ==> all_total (F i)) ==> all_total(\i\I. F i)" +by (simp add: all_total_iff_totalize totalize_JN [symmetric]) + end diff -r f39f67982854 -r 91713a1915ee src/HOL/UNITY/WFair.thy --- a/src/HOL/UNITY/WFair.thy Sat Feb 08 14:46:22 2003 +0100 +++ b/src/HOL/UNITY/WFair.thy Sat Feb 08 16:05:33 2003 +0100 @@ -3,21 +3,44 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge -Weak Fairness versions of transient, ensures, leadsTo. +Conditional Fairness versions of transient, ensures, leadsTo. From Misra, "A Logic for Concurrent Programming", 1994 *) -header{*Progress under Weak Fairness*} +header{*Progress*} theory WFair = UNITY: +text{*The original version of this theory was based on weak fairness. (Thus, +the entire UNITY development embodied this assumption, until February 2003.) +Weak fairness states that if a command is enabled continuously, then it is +eventually executed. Ernie Cohen suggested that I instead adopt unconditional +fairness: every command is executed infinitely often. + +In fact, Misra's paper on "Progress" seems to be ambiguous about the correct +interpretation, and says that the two forms of fairness are equivalent. They +differ only on their treatment of partial transitions, which under +unconditional fairness behave magically. That is because if there are partial +transitions then there may be no fair executions, making all leads-to +properties hold vacuously. + +Unconditional fairness has some great advantages. By distinguishing partial +transitions from total ones that are the identity on part of their domain, it +is more expressive. Also, by simplifying the definition of the transient +property, it simplifies many proofs. A drawback is that some laws only hold +under the assumption that all transitions are total. The best-known of these +is the impossibility law for leads-to. +*} + constdefs - (*This definition specifies weak fairness. The rest of the theory - is generic to all forms of fairness.*) + --{*This definition specifies conditional fairness. The rest of the theory + is generic to all forms of fairness. To get weak fairness, conjoin + the inclusion below with @{term "A \ Domain act"}, which specifies + that the action is enabled over all of @{term A}.*} transient :: "'a set => 'a program set" - "transient A == {F. \act\Acts F. A \ Domain act & act``A \ -A}" + "transient A == {F. \act\Acts F. act``A \ -A}" ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60) "A ensures B == (A-B co A \ B) \ transient (A-B)" @@ -25,8 +48,8 @@ consts - (*LEADS-TO constant for the inductive definition*) leads :: "'a program => ('a set * 'a set) set" + --{*LEADS-TO constant for the inductive definition*} inductive "leads F" @@ -41,12 +64,12 @@ constdefs - (*visible version of the LEADS-TO relation*) leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) + --{*visible version of the LEADS-TO relation*} "A leadsTo B == {F. (A,B) \ leads F}" - (*wlt F B is the largest set that leads to B*) wlt :: "['a program, 'a set] => 'a set" + --{*predicate transformer: the largest set that leads to @{term B}*} "wlt F B == Union {A. F \ A leadsTo B}" syntax (xsymbols) @@ -55,9 +78,17 @@ subsection{*transient*} +lemma stable_transient: + "[| F \ stable A; F \ transient A |] ==> \act\Acts F. A \ - (Domain act)" +apply (simp add: stable_def constrains_def transient_def, clarify) +apply (rule rev_bexI, auto) +done + lemma stable_transient_empty: - "[| F \ stable A; F \ transient A |] ==> A = {}" -by (unfold stable_def constrains_def transient_def, blast) + "[| F \ stable A; F \ transient A; all_total F |] ==> A = {}" +apply (drule stable_transient, assumption) +apply (simp add: all_total_def) +done lemma transient_strengthen: "[| F \ transient A; B \ A |] ==> F \ transient B" @@ -66,22 +97,34 @@ done lemma transientI: - "[| act: Acts F; A \ Domain act; act``A \ -A |] ==> F \ transient A" + "[| act: Acts F; act``A \ -A |] ==> F \ transient A" by (unfold transient_def, blast) lemma transientE: "[| F \ transient A; - !!act. [| act: Acts F; A \ Domain act; act``A \ -A |] ==> P |] + !!act. [| act: Acts F; act``A \ -A |] ==> P |] ==> P" by (unfold transient_def, blast) -lemma transient_UNIV [simp]: "transient UNIV = {}" -by (unfold transient_def, blast) - lemma transient_empty [simp]: "transient {} = UNIV" by (unfold transient_def, auto) +text{*This equation recovers the notion of weak fairness. A totalized + program satisfies a transient assertion just if the original program + contains a suitable action that is also enabled.*} +lemma totalize_transient_iff: + "(totalize F \ transient A) = (\act\Acts F. A \ Domain act & act``A \ -A)" +apply (simp add: totalize_def totalize_act_def transient_def + Un_Image Un_subset_iff, safe) +apply (blast intro!: rev_bexI)+ +done + +lemma totalize_transientI: + "[| act: Acts F; A \ Domain act; act``A \ -A |] + ==> totalize F \ transient A" +by (simp add: totalize_transient_iff, blast) + subsection{*ensures*} lemma ensuresI: @@ -98,7 +141,7 @@ apply (blast intro: constrains_weaken transient_strengthen) done -(*The L-version (precondition strengthening) fails, but we have this*) +text{*The L-version (precondition strengthening) fails, but we have this*} lemma stable_ensures_Int: "[| F \ stable C; F \ A ensures B |] ==> F \ (C \ A) ensures (C \ B)" @@ -134,7 +177,7 @@ lemma transient_imp_leadsTo: "F \ transient A ==> F \ A leadsTo (-A)" by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition) -(*Useful with cancellation, disjunction*) +text{*Useful with cancellation, disjunction*} lemma leadsTo_Un_duplicate: "F \ A leadsTo (A' \ A') ==> F \ A leadsTo A'" by (simp add: Un_ac) @@ -142,7 +185,7 @@ "F \ A leadsTo (A' \ C \ C) ==> F \ A leadsTo (A' \ C)" by (simp add: Un_ac) -(*The Union introduction rule as we should have liked to state it*) +text{*The Union introduction rule as we should have liked to state it*} lemma leadsTo_Union: "(!!A. A \ S ==> F \ A leadsTo B) ==> F \ (Union S) leadsTo B" apply (unfold leadsTo_def) @@ -162,7 +205,7 @@ apply (blast intro: leadsTo_Union) done -(*Binary union introduction rule*) +text{*Binary union introduction rule*} lemma leadsTo_Un: "[| F \ A leadsTo C; F \ B leadsTo C |] ==> F \ (A \ B) leadsTo C" apply (subst Un_eq_Union) @@ -174,7 +217,7 @@ by (subst UN_singleton [symmetric], rule leadsTo_UN, blast) -(*The INDUCTION rule as we should have liked to state it*) +text{*The INDUCTION rule as we should have liked to state it*} lemma leadsTo_induct: "[| F \ za leadsTo zb; !!A B. F \ A ensures B ==> P A B; @@ -203,16 +246,16 @@ (** Variant induction rule: on the preconditions for B **) -(*Lemma is the weak version: can't see how to do it in one step*) +text{*Lemma is the weak version: can't see how to do it in one step*} lemma leadsTo_induct_pre_lemma: "[| F \ za leadsTo zb; P zb; !!A B. [| F \ A ensures B; P B |] ==> P A; !!S. \A \ S. P A ==> P (Union S) |] ==> P za" -(*by induction on this formula*) +txt{*by induction on this formula*} apply (subgoal_tac "P zb --> P za") -(*now solve first subgoal: this formula is sufficient*) +txt{*now solve first subgoal: this formula is sufficient*} apply (blast intro: leadsTo_refl) apply (erule leadsTo_induct) apply (blast+) @@ -240,7 +283,7 @@ "[| F \ A leadsTo A'; B \ A |] ==> F \ B leadsTo A'" by (blast intro: leadsTo_Trans subset_imp_leadsTo) -(*Distributes over binary unions*) +text{*Distributes over binary unions*} lemma leadsTo_Un_distrib: "F \ (A \ B) leadsTo C = (F \ A leadsTo C & F \ B leadsTo C)" by (blast intro: leadsTo_Un leadsTo_weaken_L) @@ -271,7 +314,7 @@ apply (blast intro: leadsTo_Union leadsTo_weaken_R) done -(*Binary union version*) +text{*Binary union version*} lemma leadsTo_Un_Un: "[| F \ A leadsTo A'; F \ B leadsTo B' |] ==> F \ (A \ B) leadsTo (A' \ B')" @@ -309,18 +352,17 @@ done - -(** The impossibility law **) - -lemma leadsTo_empty: "F \ A leadsTo {} ==> A={}" +text{*The impossibility law*} +lemma leadsTo_empty: "[|F \ A leadsTo {}; all_total F|] ==> A={}" apply (erule leadsTo_induct_pre) -apply (simp_all add: ensures_def constrains_def transient_def, blast) +apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify) +apply (drule bspec, assumption)+ +apply blast done +subsection{*PSP: Progress-Safety-Progress*} -(** PSP: Progress-Safety-Progress **) - -(*Special case of PSP: Misra's "stable conjunction"*) +text{*Special case of PSP: Misra's "stable conjunction"*} lemma psp_stable: "[| F \ A leadsTo A'; F \ stable B |] ==> F \ (A \ B) leadsTo (A' \ B)" @@ -452,7 +494,7 @@ subsection{*wlt*} -(*Misra's property W3*) +text{*Misra's property W3*} lemma wlt_leadsTo: "F \ (wlt F B) leadsTo B" apply (unfold wlt_def) apply (blast intro!: leadsTo_Union) @@ -463,17 +505,17 @@ apply (blast intro!: leadsTo_Union) done -(*Misra's property W2*) +text{*Misra's property W2*} lemma leadsTo_eq_subset_wlt: "F \ A leadsTo B = (A \ wlt F B)" by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L]) -(*Misra's property W4*) +text{*Misra's property W4*} lemma wlt_increasing: "B \ wlt F B" apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo) done -(*Used in the Trans case below*) +text{*Used in the Trans case below*} lemma lemma1: "[| B \ A2; F \ (A1 - B) co (A1 \ B); @@ -481,18 +523,18 @@ ==> F \ (A1 \ A2 - C) co (A1 \ A2 \ C)" by (unfold constrains_def, clarify, blast) -(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) +text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*} lemma leadsTo_123: "F \ A leadsTo A' ==> \B. A \ B & F \ B leadsTo A' & F \ (B-A') co (B \ A')" apply (erule leadsTo_induct) -(*Basis*) -apply (blast dest: ensuresD) -(*Trans*) -apply clarify -apply (rule_tac x = "Ba \ Bb" in exI) -apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) -(*Union*) + txt{*Basis*} + apply (blast dest: ensuresD) + txt{*Trans*} + apply clarify + apply (rule_tac x = "Ba \ Bb" in exI) + apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate) +txt{*Union*} apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice) apply (rule_tac x = "\A \ S. f A" in exI) apply (auto intro: leadsTo_UN) @@ -502,7 +544,7 @@ done -(*Misra's property W5*) +text{*Misra's property W5*} lemma wlt_constrains_wlt: "F \ (wlt F B - B) co (wlt F B)" proof - from wlt_leadsTo [of F B, THEN leadsTo_123]