# HG changeset patch # User ehmety # Date 1005833236 -3600 # Node ID ed2893765a08b282e14d68836120400ad3de831b # Parent 13909cb72129938f2333fc4f2575f0c0abec0e19 *** empty log message *** diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Comp.ML --- a/src/ZF/UNITY/Comp.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Comp.ML Thu Nov 15 15:07:16 2001 +0100 @@ -28,14 +28,12 @@ by Auto_tac; qed "component_eq_subset"; - Goalw [component_def] "F:program ==> SKIP component F"; by (res_inst_tac [("x", "F")] exI 1); by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); qed "component_SKIP"; - Goalw [component_def] "F:program ==> F component F"; by (res_inst_tac [("x", "F")] exI 1); @@ -50,12 +48,10 @@ by (Blast_tac 1); qed "SKIP_minimal"; - Goalw [component_def] "F component (F Join G)"; by (Blast_tac 1); qed "component_Join1"; - Goalw [component_def] "G component (F Join G)"; by (simp_tac (simpset() addsimps [Join_commute]) 1); by (Blast_tac 1); @@ -70,10 +66,8 @@ by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); qed "Join_absorb2"; - - -Goal "H:program ==> \ -\ (JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; +Goal +"H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; by (case_tac "I=0" 1); by (Force_tac 1); by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); @@ -82,18 +76,15 @@ by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1)); qed "JN_component_iff"; - -Goalw [component_def] "i : I ==> F(i) component (JN i:I. (F(i)))"; +Goalw [component_def] "i:I ==> F(i) component (JN i:I. (F(i)))"; by (blast_tac (claset() addIs [JN_absorb]) 1); qed "component_JN"; - Goalw [component_def] "[| F component G; G component H |] ==> F component H"; by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); qed "component_trans"; -Goal "[| F:program; G:program |] ==> \ -\ (F component G & G component F) --> F = G"; +Goal "[| F:program; G:program |] ==>(F component G & G component F) --> F = G"; by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); by (Clarify_tac 1); by (rtac program_equalityI 1); @@ -105,7 +96,6 @@ by (Blast_tac 1); qed "Join_component_iff"; - Goal "[| F component G; G:A co B; F:program |] ==> F : A co B"; by (forward_tac [constrainsD2] 1); by (rotate_tac ~1 1); @@ -113,23 +103,22 @@ simpset() addsimps [constrains_def, component_eq_subset])); qed "component_constrains"; -(*Used in Guar.thy to show that programs are partially ordered*) +(* Used in Guar.thy to show that programs are partially ordered*) (* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*) - (*** preserves ***) -val prems = -Goalw [preserves_def] +val prems = Goalw [preserves_def] "ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)"; by Auto_tac; by (blast_tac (claset() addDs [stableD2]) 1); -bind_thm("preservesI", allI RS result()); +qed "preserves_aux"; +bind_thm("preservesI", allI RS preserves_aux); Goalw [preserves_def, stable_def, constrains_def] "[| F:preserves(f); act : Acts(F); : act |] ==> f(s) = f(t)"; by (subgoal_tac "s:state & t:state" 1); -by (blast_tac (claset() addSDs [ActsD]) 2); +by (blast_tac (claset() addSDs [Acts_type RS subsetD]) 2); by Auto_tac; by (dres_inst_tac [("x", "f(s)")] spec 1); by (dres_inst_tac [("x", "act")] bspec 1); @@ -141,23 +130,18 @@ \ (programify(F) : preserves(v) & programify(G) : preserves(v))"; by (auto_tac (claset(), simpset() addsimps [INT_iff])); qed "Join_preserves"; - Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))"; -by (auto_tac (claset(), simpset() addsimps - [JN_stable, preserves_def, INT_iff]@state_simps)); +by (auto_tac (claset(), simpset() addsimps [JN_stable, preserves_def, INT_iff])); qed "JN_preserves"; Goal "SKIP : preserves(v)"; -by (auto_tac (claset(), simpset() - addsimps [preserves_def, INT_iff]@state_simps)); +by (auto_tac (claset(), simpset() addsimps [preserves_def, INT_iff])); qed "SKIP_preserves"; AddIffs [Join_preserves, JN_preserves, SKIP_preserves]; - - - +(** Added by Sidi **) (** component_of **) (* component_of is stronger than component *) @@ -166,49 +150,42 @@ by (Blast_tac 1); qed "component_of_imp_component"; - - -(* component_of satisfies many of the <='s properties *) +(* component_of satisfies many of component's properties *) Goalw [component_of_def] "F:program ==> F component_of F"; by (res_inst_tac [("x", "SKIP")] exI 1); by Auto_tac; qed "component_of_refl"; - - Goalw [component_of_def] "F:program ==>SKIP component_of F"; by Auto_tac; by (res_inst_tac [("x", "F")] exI 1); by Auto_tac; qed "component_of_SKIP"; - Addsimps [component_of_refl, component_of_SKIP]; - - Goalw [component_of_def] "[| F component_of G; G component_of H |] ==> F component_of H"; by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); qed "component_of_trans"; - (** localize **) Goalw [localize_def] "Init(localize(v,F)) = Init(F)"; by (Simp_tac 1); qed "localize_Init_eq"; - Goalw [localize_def] "Acts(localize(v,F)) = Acts(F)"; by (Simp_tac 1); qed "localize_Acts_eq"; Goalw [localize_def] - "AllowedActs(localize(v,F)) = AllowedActs(F Int (UN G:preserves(v). Acts(G)))"; -by Auto_tac; + "AllowedActs(localize(v,F)) = AllowedActs(F) Int (UN G:preserves(v). Acts(G))"; +by (rtac equalityI 1); +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "localize_AllowedActs_eq"; -Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; +AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; + diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Comp.thy --- a/src/ZF/UNITY/Comp.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Comp.thy Thu Nov 15 15:07:16 2001 +0100 @@ -32,13 +32,13 @@ strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) "F strict_component_of H == F component_of H & F~=H" - (* preserves any state function f, in particular a variable *) + (* Preserves a state function f, in particular a variable *) preserves :: (i=>i)=>i "preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}" localize :: "[i=>i, i] => i" "localize(f,F) == mk_program(Init(F), Acts(F), - AllowedActs(F Int (UN G:preserves(f). Acts(G))))" + AllowedActs(F) Int (UN G:preserves(f). Acts(G)))" end diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Constrains.ML --- a/src/ZF/UNITY/Constrains.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Constrains.ML Thu Nov 15 15:07:16 2001 +0100 @@ -10,24 +10,35 @@ (*** traces and reachable ***) -Goalw [condition_def] - "reachable(F):condition"; -by (auto_tac (claset() addSDs [reachable.dom_subset RS subsetD] - addDs [InitD, ActsD], simpset())); +Goal "reachable(F) <= state"; +by (cut_inst_tac [("F", "F")] Init_type 1); +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (cut_inst_tac [("F", "F")] reachable.dom_subset 1); +by (Blast_tac 1); qed "reachable_type"; -Addsimps [reachable_type]; -AddIs [reachable_type]; + +Goalw [st_set_def] "st_set(reachable(F))"; +by (resolve_tac [reachable_type] 1); +qed "st_set_reachable"; +AddIffs [st_set_reachable]; -Goal "x:reachable(F) ==> x:state"; -by (cut_inst_tac [("F", "F")] reachable_type 1); -by (auto_tac (claset(), simpset() addsimps [condition_def])); -qed "reachableD"; +Goal "reachable(F) Int state = reachable(F)"; +by (cut_facts_tac [reachable_type] 1); +by Auto_tac; +qed "reachable_Int_state"; +AddIffs [reachable_Int_state]; -Goal "F:program ==> \ -\ reachable(F) = {s:state. EX evs. : traces(Init(F), Acts(F))}"; +Goal "state Int reachable(F) = reachable(F)"; +by (cut_facts_tac [reachable_type] 1); +by Auto_tac; +qed "state_Int_reachable"; +AddIffs [state_Int_reachable]; + +Goal +"F:program ==> reachable(F)={s:state. EX evs. :traces(Init(F), Acts(F))}"; by (rtac equalityI 1); by Safe_tac; -by (blast_tac (claset() addDs [reachableD]) 1); +by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1); by (etac traces.induct 2); by (etac reachable.induct 1); by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs))); @@ -40,7 +51,8 @@ Goal "[| F:program; G:program; \ \ Acts(G) <= Acts(F) |] ==> G:stable(reachable(F))"; by (blast_tac (claset() - addIs [stableI, constrainsI, reachable_type] @ reachable.intrs) 1); + addIs [stableI, constrainsI, st_setI, + reachable_type RS subsetD] @ reachable.intrs) 1); qed "stable_reachable"; AddSIs [stable_reachable]; @@ -49,13 +61,16 @@ (*The set of all reachable states is an invariant...*) Goalw [invariant_def, initially_def] "F:program ==> F:invariant(reachable(F))"; -by (blast_tac (claset() addIs [reachable_type]@reachable.intrs) 1); +by (blast_tac (claset() addIs [reachable_type RS subsetD]@reachable.intrs) 1); qed "invariant_reachable"; (*...in fact the strongest invariant!*) -Goal "F : invariant(A) ==> reachable(F) <= A"; -by (full_simp_tac - (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1); +Goal "F:invariant(A) ==> reachable(F) <= A"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (cut_inst_tac [("F", "F")] Init_type 1); +by (cut_inst_tac [("F", "F")] reachable_type 1); +by (full_simp_tac (simpset() addsimps [stable_def, constrains_def, + invariant_def, initially_def]) 1); by (rtac subsetI 1); by (etac reachable.induct 1); by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); @@ -63,186 +78,139 @@ (*** Co ***) -(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) -val lemma = subset_refl RSN (3, rewrite_rule - [stable_def] stable_reachable RS constrains_Int); -Goal "F:B co B' ==> F: (reachable(F) Int B) co (reachable(F) Int B')"; -by (blast_tac (claset() addSIs [lemma] - addDs [constrainsD2]) 1); +Goal "F:B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')"; +by (forward_tac [constrains_type RS subsetD] 1); +by (forward_tac [[asm_rl, asm_rl, subset_refl] MRS stable_reachable] 1); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [stable_def, constrains_Int]))); qed "constrains_reachable_Int"; (*Resembles the previous definition of Constrains*) Goalw [Constrains_def] - "A Co B = \ -\ {F:program. F : (reachable(F) Int A) co (reachable(F) Int B) & \ -\ A:condition & B:condition}"; -by (rtac equalityI 1); -by (ALLGOALS(Clarify_tac)); -by (subgoal_tac "reachable(x) Int B:condition" 2); -by (blast_tac (claset() addDs [constrains_reachable_Int] - addIs [constrains_weaken]) 2); -by (subgoal_tac "reachable(x) Int B:condition" 1); -by (blast_tac (claset() addDs [constrains_reachable_Int] +"A Co B = {F:program. F:(reachable(F) Int A) co (reachable(F) Int B)}"; +by (blast_tac (claset() addDs [constrains_reachable_Int, + constrains_type RS subsetD] addIs [constrains_weaken]) 1); -by (REPEAT(blast_tac (claset() addIs [reachable_type]) 1)); qed "Constrains_eq_constrains"; +val Constrains_def2 = Constrains_eq_constrains RS eq_reflection; + +Goalw [Constrains_def] + "F:A co A' ==> F:A Co A'"; +by (blast_tac (claset() addIs [constrains_weaken_L] addDs [constrainsD2]) 1); +qed "constrains_imp_Constrains"; + +val prems = Goalw [Constrains_def, constrains_def, st_set_def] +"[|(!!act s s'. [| act: Acts(F); :act; s:A |] ==> s':A'); F:program|]==>F:A Co A'"; +by (auto_tac (claset(), simpset() addsimps prems)); +by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1); +qed "ConstrainsI"; Goalw [Constrains_def] - "F : A co A' ==> F : A Co A'"; -by (blast_tac (claset() addIs [constrains_weaken_L] - addDs [constrainsD2]) 1); -qed "constrains_imp_Constrains"; + "A Co B <= program"; +by (Blast_tac 1); +qed "Constrains_type"; + +Goal "F : 0 Co B <-> F:program"; +by (auto_tac (claset() addDs [Constrains_type RS subsetD] + addIs [constrains_imp_Constrains], simpset())); +qed "Constrains_empty"; +AddIffs [Constrains_empty]; + +Goalw [Constrains_def] "F : A Co state <-> F:program"; +by (auto_tac (claset() addDs [Constrains_type RS subsetD] + addIs [constrains_imp_Constrains], simpset())); +qed "Constrains_state"; +AddIffs [Constrains_state]; + +Goalw [Constrains_def2] + "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"; +by (blast_tac (claset() addIs [constrains_weaken_R]) 1); +qed "Constrains_weaken_R"; + +Goalw [Constrains_def2] + "[| F : A Co A'; B<=A |] ==> F : B Co A'"; +by (blast_tac (claset() addIs [constrains_weaken_L, st_set_subset]) 1); +qed "Constrains_weaken_L"; + +Goalw [Constrains_def2] + "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"; +by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1); +qed "Constrains_weaken"; + +(** Union **) +Goalw [Constrains_def2] +"[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"; +by Auto_tac; +by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1); +by (blast_tac (claset() addIs [constrains_Un]) 1); +qed "Constrains_Un"; + +val [major, minor] = Goalw [Constrains_def2] +"[|(!!i. i:I==>F:A(i) Co A'(i)); F:program|] ==> F:(UN i:I. A(i)) Co (UN i:I. A'(i))"; +by (cut_facts_tac [minor] 1); +by (auto_tac (claset() addDs [major] + addIs [constrains_UN], + simpset() addsimps [Int_UN_distrib])); +qed "Constrains_UN"; + +(** Intersection **) + +Goalw [Constrains_def] +"[| F : A Co A'; F : B Co B'|]==> F:(A Int B) Co (A' Int B')"; +by (subgoal_tac "reachable(F) Int (A Int B) = \ + \ (reachable(F) Int A) Int (reachable(F) Int B)" 1); +by (ALLGOALS(force_tac (claset() addIs [constrains_Int], simpset()))); +qed "Constrains_Int"; + +val [major,minor] = Goal +"[| (!!i. i:I ==>F: A(i) Co A'(i)); F:program |] \ +\ ==> F:(INT i:I. A(i)) Co (INT i:I. A'(i))"; +by (cut_facts_tac [minor] 1); +by (case_tac "I=0" 1); +by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1); +by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1); +by (force_tac (claset(), simpset() addsimps [Inter_def]) 2); +by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); +by (rtac constrains_INT 1); +by (etac not_emptyE 1); +by (dresolve_tac [major] 1); +by (rewrite_goal_tac [Constrains_def] 1); +by (ALLGOALS(Asm_full_simp_tac)); +qed "Constrains_INT"; + +Goalw [Constrains_def] "F : A Co A' ==> reachable(F) Int A <= A'"; +by (blast_tac (claset() addDs [constrains_imp_subset]) 1); +qed "Constrains_imp_subset"; + +Goalw [Constrains_def2] + "[| F : A Co B; F : B Co C |] ==> F : A Co C"; +by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); +qed "Constrains_trans"; + +Goalw [Constrains_def2] +"[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"; +by (full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1); +by (blast_tac (claset() addIs [constrains_cancel]) 1); +qed "Constrains_cancel"; + +(*** Stable ***) +(* Useful because there's no Stable_weaken. [Tanja Vos] *) Goalw [stable_def, Stable_def] "F : stable(A) ==> F : Stable(A)"; by (etac constrains_imp_Constrains 1); qed "stable_imp_Stable"; - -val prems = Goal - "[|(!!act s s'. [| act: Acts(F); :act; s:A |] \ -\ ==> s':A'); F:program; A:condition; A':condition |] ==> F:A Co A'"; -by (rtac constrains_imp_Constrains 1); -by (blast_tac (claset() addIs (constrainsI::prems)) 1); -qed "ConstrainsI"; - -Goalw [Constrains_def] - "F:A Co B ==> F:program & A:condition & B:condition"; -by (Blast_tac 1); -qed "ConstrainsD"; - -Goal "[| F:program; B:condition |] ==> F : 0 Co B"; -by (blast_tac (claset() addIs - [constrains_imp_Constrains, constrains_empty]) 1); -qed "Constrains_empty"; - -Goal "[| F:program; A:condition |] ==> F : A Co state"; -by (blast_tac (claset() addIs - [constrains_imp_Constrains, constrains_state2]) 1); -qed "Constrains_state"; -Addsimps [Constrains_empty, Constrains_state]; - -val Constrains_def2 = Constrains_eq_constrains RS eq_reflection; - -Goalw [Constrains_def2] - "[| F : A Co A'; A'<=B'; B':condition |] ==> F : A Co B'"; -by (Clarify_tac 1); -by (blast_tac (claset() - addIs [reachable_type, constrains_weaken_R]) 1); -qed "Constrains_weaken_R"; - - -Goalw [condition_def] - "[| A<=B; B:condition |] ==>A:condition"; -by (Blast_tac 1); -qed "condition_subset_mono"; - - -Goalw [Constrains_def2] - "[| F : A Co A'; B<=A |] ==> F : B Co A'"; -by (Clarify_tac 1); -by (forward_tac [condition_subset_mono] 1); -by (assume_tac 1); -by (blast_tac (claset() - addIs [reachable_type, constrains_weaken_L]) 1); -qed "Constrains_weaken_L"; - -Goalw [Constrains_def] - "[| F : A Co A'; B<=A; A'<=B'; B':condition |] ==> F : B Co B'"; -by (Clarify_tac 1); -by (forward_tac [condition_subset_mono] 1); -by (assume_tac 1); -by (blast_tac (claset() addIs [reachable_type, constrains_weaken]) 1); -qed "Constrains_weaken"; - -(** Union **) - -Goalw [Constrains_def2] - "[| F : A Co A'; F : B Co B' |] \ -\ ==> F : (A Un B) Co (A' Un B')"; -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1); -by (blast_tac (claset() addIs [constrains_Un]) 1); -qed "Constrains_Un"; - -Goalw [Constrains_def2] - "[| F:program; \ -\ ALL i:I. F : A(i) Co A'(i) |] \ -\ ==> F : (UN i:I. A(i)) Co (UN i:I. A'(i))"; -by (rtac CollectI 1); -by Safe_tac; -by (simp_tac (simpset() addsimps [Int_UN_distrib]) 1); -by (blast_tac (claset() addIs [constrains_UN, CollectD2 RS conjunct1]) 1); -by (rewrite_goals_tac [condition_def]); -by (ALLGOALS(Blast_tac)); -qed "Constrains_UN"; - -(** Intersection **) - -Goal "A Int (B Int C) = (A Int B) Int (A Int C)"; -by (Blast_tac 1); -qed "Int_duplicate"; - -Goalw [Constrains_def] - "[| F : A Co A'; F : B Co B' |] \ -\ ==> F : (A Int B) Co (A' Int B')"; -by (Step_tac 1); -by (subgoal_tac "reachable(F) Int (A Int B) = \ - \ (reachable(F) Int A) Int (reachable(F) Int B)" 1); -by (Blast_tac 2); -by (Asm_simp_tac 1); -by (rtac constrains_Int 1); -by (ALLGOALS(Asm_simp_tac)); -qed "Constrains_Int"; - -Goal - "[| F:program; \ -\ ALL i:I. F: A(i) Co A'(i) |] \ -\ ==> F : (INT i:I. A(i)) Co (INT i:I. A'(i))"; -by (case_tac "I=0" 1); -by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1); -by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1); -by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 2); -by (Blast_tac 2); -by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1); -by (Step_tac 1); -by (rtac constrains_INT 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(Blast_tac)); -qed "Constrains_INT"; - -Goal "F : A Co A' ==> reachable(F) Int A <= A'"; -by (asm_full_simp_tac (simpset() addsimps - [Constrains_def, reachable_type]) 1); -by (blast_tac (claset() addDs [constrains_imp_subset]) 1); -qed "Constrains_imp_subset"; - -Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C"; -by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1); -by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); -qed "Constrains_trans"; - -Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"; -by (full_simp_tac (simpset() - addsimps [Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1); -by (Step_tac 1); -by (blast_tac (claset() addIs [constrains_cancel]) 1); -qed "Constrains_cancel"; - -(*** Stable ***) - -(*Useful because there's no Stable_weaken. [Tanja Vos]*) Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)"; by (Blast_tac 1); qed "Stable_eq"; -Goal "A:condition ==> F : Stable(A) <-> (F : stable(reachable(F) Int A))"; -by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains, - stable_def]) 1); -by (blast_tac (claset() addDs [constrainsD2]) 1); +Goal +"F : Stable(A) <-> (F:stable(reachable(F) Int A))"; +by (auto_tac (claset() addDs [constrainsD2], + simpset() addsimps [Stable_def, stable_def, Constrains_def2])); qed "Stable_eq_stable"; -Goalw [Stable_def] "F : A Co A ==> F : Stable(A)"; +Goalw [Stable_def] "F:A Co A ==> F : Stable(A)"; by (assume_tac 1); qed "StableI"; @@ -263,66 +231,50 @@ Goalw [Stable_def] "[| F : Stable(C); F : A Co (C Un A') |] \ \ ==> F : (C Un A) Co (C Un A')"; -by (subgoal_tac "C Un A' :condition & C Un A:condition" 1); by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1); -by (blast_tac (claset() addDs [ConstrainsD]) 1); qed "Stable_Constrains_Un"; - Goalw [Stable_def] "[| F : Stable(C); F : (C Int A) Co A' |] \ \ ==> F : (C Int A) Co (C Int A')"; -by (blast_tac (claset() addDs [ConstrainsD] - addIs [Constrains_Int RS Constrains_weaken]) 1); +by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); qed "Stable_Constrains_Int"; -val [major, prem] = Goalw [Stable_def] - "[| F:program; \ -\ (!!i. i:I ==> F : Stable(A(i))) |]==> F : Stable (UN i:I. A(i))"; -by (cut_facts_tac [major] 1); -by (blast_tac (claset() addIs [major, Constrains_UN, prem]) 1); +val [major,minor] = Goalw [Stable_def] +"[| (!!i. i:I ==> F : Stable(A(i))); F:program |]==> F : Stable (UN i:I. A(i))"; +by (cut_facts_tac [minor] 1); +by (blast_tac (claset() addIs [Constrains_UN,major]) 1); qed "Stable_UN"; -val [major, prem] = Goalw [Stable_def] - "[| F:program; \ -\ (!!i. i:I ==> F:Stable(A(i))) |]==> F : Stable (INT i:I. A(i))"; -by (cut_facts_tac [major] 1); -by (blast_tac (claset() addIs [major, Constrains_INT, prem]) 1); +val [major,minor] = Goalw [Stable_def] +"[|(!!i. i:I ==> F:Stable(A(i))); F:program |]==> F : Stable (INT i:I. A(i))"; +by (cut_facts_tac [minor] 1); +by (blast_tac (claset() addIs [Constrains_INT, major]) 1); qed "Stable_INT"; Goal "F:program ==>F : Stable (reachable(F))"; by (asm_simp_tac (simpset() - addsimps [Stable_eq_stable, Int_absorb, subset_refl]) 1); + addsimps [Stable_eq_stable, Int_absorb]) 1); qed "Stable_reachable"; Goalw [Stable_def] -"F:Stable(A) ==> F:program & A:condition"; -by (blast_tac (claset() addDs [ConstrainsD]) 1); -qed "StableD2"; +"Stable(A) <= program"; +by (rtac Constrains_type 1); +qed "Stable_type"; (*** The Elimination Theorem. The "free" m has become universally quantified! Should the premise be !!m instead of ALL m ? Would make it harder to use in forward proof. ***) -Goalw [condition_def] - "Collect(state,P):condition"; +Goalw [Constrains_def] +"[| ALL m:M. F : ({s:A. x(s) = m}) Co (B(m)); F:program |] \ +\ ==> F : ({s:A. x(s):M}) Co (UN m:M. B(m))"; by Auto_tac; -qed "Collect_in_condition"; -AddIffs [Collect_in_condition]; - -Goalw [Constrains_def] - "[| ALL m:M. F : {s:S. x(s) = m} Co B(m); F:program |] \ -\ ==> F : {s:S. x(s):M} Co (UN m:M. B(m))"; -by Safe_tac; -by (res_inst_tac [("S1", "reachable(F) Int S")] - (elimination RS constrains_weaken_L) 1); -by Auto_tac; -by (rtac constrains_weaken_L 1); -by (auto_tac (claset(), simpset() addsimps [condition_def])); +by (res_inst_tac [("A1","reachable(F)Int A")] (elimination RS constrains_weaken_L) 1); +by (auto_tac (claset() addIs [constrains_weaken_L], simpset())); qed "Elimination"; -(* As above, but for the special case of S=state *) - +(* As above, but for the special case of A=state *) Goal "[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \ \ ==> F : {s:state. x(s):M} Co (UN m:M. B(m))"; @@ -331,62 +283,53 @@ (** Unless **) -Goalw [Unless_def] -"F:A Unless B ==> F:program & A:condition & B:condition"; -by (blast_tac (claset() addDs [ConstrainsD]) 1); -qed "UnlessD"; +Goalw [Unless_def] "A Unless B <=program"; +by (rtac Constrains_type 1); +qed "Unless_type"; (*** Specialized laws for handling Always ***) (** Natural deduction rules for "Always A" **) + Goalw [Always_def, initially_def] - "Always(A) = initially(A) Int Stable(A)"; -by (blast_tac (claset() addDs [StableD2]) 1); -qed "Always_eq"; - -val Always_def2 = Always_eq RS eq_reflection; - -Goalw [Always_def] "[| Init(F)<=A; F : Stable(A) |] ==> F : Always(A)"; -by (asm_simp_tac (simpset() addsimps [StableD2]) 1); +by (forward_tac [Stable_type RS subsetD] 1); +by Auto_tac; qed "AlwaysI"; Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)"; -by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1); +by (asm_full_simp_tac (simpset() addsimps [Always_def, initially_def]) 1); qed "AlwaysD"; bind_thm ("AlwaysE", AlwaysD RS conjE); bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2); - (*The set of all reachable states is Always*) Goal "F : Always(A) ==> reachable(F) <= A"; -by (full_simp_tac - (simpset() addsimps [Stable_def, Constrains_def, constrains_def, - Always_def]) 1); +by (full_simp_tac (simpset() addsimps + [Stable_def, Constrains_def, constrains_def, Always_def, initially_def]) 1); by (rtac subsetI 1); by (etac reachable.induct 1); by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1)); qed "Always_includes_reachable"; -Goalw [Always_def2, invariant_def2, Stable_def, stable_def] +Goalw [Always_def, invariant_def, Stable_def, stable_def] "F : invariant(A) ==> F : Always(A)"; by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1); qed "invariant_imp_Always"; bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always); -Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A) & A:condition}"; +Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A)}"; by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, - Constrains_eq_constrains, stable_def]) 1); + Constrains_def2, stable_def, initially_def]) 1); by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); -by (REPEAT(blast_tac (claset() addDs [constrainsD] - addIs reachable.intrs@[reachable_type]) 1)); +by (REPEAT(blast_tac (claset() addIs reachable.intrs@[reachable_type]) 1)); qed "Always_eq_invariant_reachable"; (*the RHS is the traditional definition of the "always" operator*) -Goal "Always(A) = {F:program. reachable(F) <= A & A:condition}"; +Goal "Always(A) = {F:program. reachable(F) <= A}"; br equalityI 1; by (ALLGOALS(Clarify_tac)); by (auto_tac (claset() addDs [invariant_includes_reachable], @@ -394,38 +337,34 @@ Always_eq_invariant_reachable])); qed "Always_eq_includes_reachable"; -Goalw [Always_def] -"F:Always(A)==> F:program & A:condition"; -by (blast_tac (claset() addDs [StableD2]) 1); -qed "AlwaysD2"; +Goalw [Always_def, initially_def] "Always(A) <= program"; +by Auto_tac; +qed "Always_type"; Goal "Always(state) = program"; br equalityI 1; -by (ALLGOALS(Clarify_tac)); -by (blast_tac (claset() addDs [AlwaysD2]) 1); -by (auto_tac (claset() addDs [reachableD], - simpset() addsimps [Always_eq_includes_reachable])); +by (auto_tac (claset() addDs [Always_type RS subsetD, + reachable_type RS subsetD], + simpset() addsimps [Always_eq_includes_reachable])); qed "Always_state_eq"; Addsimps [Always_state_eq]; -Goal "[| state <= A; F:program; A:condition |] ==> F : Always(A)"; -by (auto_tac (claset(), simpset() +Goal "F:program ==> F : Always(state)"; +by (auto_tac (claset() addDs [reachable_type RS subsetD], simpset() addsimps [Always_eq_includes_reachable])); -by (auto_tac (claset() addSDs [reachableD], - simpset() addsimps [condition_def])); qed "state_AlwaysI"; -Goal "A:condition ==> Always(A) = (UN I: Pow(A). invariant(I))"; +Goal "st_set(A) ==> Always(A) = (UN I: Pow(A). invariant(I))"; by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); by (REPEAT(blast_tac (claset() addIs [invariantI, impOfSubs Init_into_reachable, impOfSubs invariant_includes_reachable] - addDs [invariantD2]) 1)); + addDs [invariant_type RS subsetD]) 1)); qed "Always_eq_UN_invariant"; -Goal "[| F : Always(A); A <= B; B:condition |] ==> F : Always(B)"; +Goal "[| F : Always(A); A <= B |] ==> F : Always(B)"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "Always_weaken"; @@ -433,66 +372,55 @@ (*** "Co" rules involving Always ***) val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp; -Goal "[| F:Always(INV); A:condition |] \ - \ ==> (F:(INV Int A) Co A') <-> (F : A Co A')"; +Goal "F:Always(I) ==> (F:(I Int A) Co A') <-> (F : A Co A')"; by (asm_simp_tac (simpset() addsimps [Always_includes_reachable RS Int_absorb2, Constrains_def, Int_assoc RS sym]) 1); -by (blast_tac (claset() addDs [AlwaysD2]) 1); qed "Always_Constrains_pre"; -Goal "[| F : Always(INV); A':condition |] \ -\ ==> (F : A Co (INV Int A')) <->(F : A Co A')"; +Goal "F:Always(I) ==> (F : A Co (I Int A')) <->(F : A Co A')"; by (asm_simp_tac (simpset() addsimps [Always_includes_reachable RS Int_absorb2, Constrains_eq_constrains, Int_assoc RS sym]) 1); -by (blast_tac (claset() addDs [AlwaysD2]) 1); qed "Always_Constrains_post"; -(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *) -bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1); +Goal "[| F : Always(I); F : (I Int A) Co A' |] ==> F : A Co A'"; +by (blast_tac (claset() addIs [Always_Constrains_pre RS iffD1]) 1); +qed "Always_ConstrainsI"; -(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *) +(* [| F : Always(I); F : A Co A' |] ==> F : A Co (I Int A') *) bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2); (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) -Goal "[| F : Always(C); F : A Co A'; \ -\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \ -\ ==> F : B Co B'"; +Goal +"[|F:Always(C); F:A Co A'; C Int B<=A; C Int A'<=B'|]==>F:B Co B'"; by (rtac Always_ConstrainsI 1); -by (assume_tac 1); -by (assume_tac 1); -by (dtac Always_ConstrainsD 1); -by (assume_tac 2); -by (blast_tac (claset() addDs [ConstrainsD]) 1); +by (dtac Always_ConstrainsD 2); +by (ALLGOALS(Asm_simp_tac)); by (blast_tac (claset() addIs [Constrains_weaken]) 1); qed "Always_Constrains_weaken"; - (** Conjoining Always properties **) - -Goal "[| A:condition; B:condition |] ==> \ -\ Always(A Int B) = Always(A) Int Always(B)"; +Goal "Always(A Int B) = Always(A) Int Always(B)"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "Always_Int_distrib"; (* the premise i:I is need since INT is formally not defined for I=0 *) -Goal "[| i:I; ALL i:I. A(i):condition |] \ -\ ==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))"; +Goal "i:I==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))"; by (rtac equalityI 1); -by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); +by (auto_tac (claset(), simpset() addsimps + [Inter_iff, Always_eq_includes_reachable])); qed "Always_INT_distrib"; -Goal "[| F : Always(A); F : Always(B) |] ==> F : Always(A Int B)"; -by (asm_simp_tac (simpset() addsimps - [Always_Int_distrib,AlwaysD2]) 1); +Goal "[| F:Always(A); F:Always(B) |] ==> F:Always(A Int B)"; +by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1); qed "Always_Int_I"; (*Allows a kind of "implication introduction"*) -Goal "F : Always(A) ==> (F : Always (state-A Un B)) <-> (F : Always(B))"; +Goal "[| F:Always(A) |] ==> (F : Always(C-A Un B)) <-> (F : Always(B))"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); -qed "Always_Compl_Un_eq"; +qed "Always_Diff_Un_eq"; (*Delete the nearest invariance assumption (which will be the second one used by Always_Int_I) *) @@ -508,65 +436,75 @@ (*** Increasing ***) -Goalw [Increasing_on_def] -"[| F:Increasing_on(A, f, r); a:A |] ==> F: Stable({s:state. :r})"; +Goalw [Increasing_def] "Increasing(A,r,f) <= program"; +by (auto_tac (claset() addDs [Stable_type RS subsetD] + addSDs [bspec], simpset() addsimps [INT_iff])); +qed "Increasing_type"; + +Goalw [Increasing_def] +"[| F:Increasing(A, r, f); a:A |] ==> F: Stable({s:state. :r})"; by (Blast_tac 1); -qed "Increasing_onD"; +qed "IncreasingD"; -Goalw [Increasing_on_def] -"F:Increasing_on(A, f, r) ==> F:program & f:state->A & part_order(A,r)"; +Goalw [Increasing_def] +"F:Increasing(A, r, f) ==> F:program & (EX a. a:A)"; by (auto_tac (claset(), simpset() addsimps [INT_iff])); -qed "Increasing_onD2"; +by (blast_tac (claset() addDs [Stable_type RS subsetD]) 1); +qed "IncreasingD2"; + +Goalw [increasing_def, Increasing_def] + "F : increasing(A, r, f) ==> F : Increasing(A, r, f)"; +by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); +by (blast_tac (claset() addIs [stable_imp_Stable]) 1); +qed "increasing_imp_Increasing"; -Goalw [Increasing_on_def, Stable_def, Constrains_def, stable_def, constrains_def, part_order_def] - "!!f. g:mono_map(A,r,A,r) \ -\ ==> Increasing_on(A, f, r) <= Increasing_on(A, g O f, r)"; -by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1); -by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def])); -by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1); -by (subgoal_tac "xc:state" 1); -by (blast_tac (claset() addSDs [ActsD]) 2); -by (subgoal_tac "f`xd:A & f`xc:A" 1); -by (blast_tac (claset() addDs [apply_type]) 2); -by (rotate_tac 3 1); -by (dres_inst_tac [("x", "f`xd")] bspec 1); -by (Asm_simp_tac 1); -by (REPEAT(etac conjE 1)); -by (rotate_tac ~3 1); +Goal +"F:Increasing(A, r, lam x:state. c) <-> F:program & (EX a. a:A)"; +by (auto_tac (claset() addDs [IncreasingD2] + addIs [increasing_imp_Increasing], simpset())); +qed "Increasing_constant"; +AddIffs [Increasing_constant]; + +Goalw [Increasing_def, Stable_def, stable_def, Constrains_def, + constrains_def, part_order_def, st_set_def] +"[| g:mono_map(A,r,A,r); part_order(A, r); f:state->A |] \ +\ ==> Increasing(A, r,f) <= Increasing(A, r,g O f)"; +by (case_tac "A=0" 1); +by (Asm_full_simp_tac 1); +by (etac not_emptyE 1); +by (Clarify_tac 1); +by (cut_inst_tac [("F", "xa")] Acts_type 1); +by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1); +by Auto_tac; +by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); +by (dres_inst_tac [("x", "f`xf")] bspec 1); +by Auto_tac; +by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); by (dres_inst_tac [("x", "act")] bspec 1); -by (Asm_simp_tac 1); -by (dres_inst_tac [("c", "xc")] subsetD 1); +by Auto_tac; +by (dres_inst_tac [("psi", "Acts(?u) <= ?v")] asm_rl 1); +by (dres_inst_tac [("psi", "?u <= state")] asm_rl 1); +by (dres_inst_tac [("c", "xe")] subsetD 1); by (rtac imageI 1); by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1); -by (dres_inst_tac [("x", "f`xd")] bspec 1); -by (dres_inst_tac [("x", "f`xc")] bspec 2); -by (ALLGOALS(Asm_simp_tac)); -by (dres_inst_tac [("b", "g`(f`xd)")] trans_onD 1); -by Auto_tac; -qed "mono_Increasing_on_comp"; +by (asm_full_simp_tac (simpset() addsimps [refl_def, apply_type]) 1); +by (dres_inst_tac [("x1", "f`xf"), ("x", "f`xe")] (bspec RS bspec) 1); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type]))); +by (res_inst_tac [("b", "g ` (f ` xf)")] trans_onD 1); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type]))); +qed "mono_Increasing_comp"; -Goalw [increasing_on_def, Increasing_on_def] - "F : increasing_on(A, f,r) ==> F : Increasing_on(A, f,r)"; -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); -by (blast_tac (claset() addIs [stable_imp_Stable]) 1); -qed "increasing_on_imp_Increasing_on"; - -bind_thm("Increasing_on_constant", increasing_on_constant RS increasing_on_imp_Increasing_on); -Addsimps [Increasing_on_constant]; - -Goalw [Increasing_on_def, nat_order_def] - "[| F:Increasing_on(nat,f, nat_order); z:nat |] \ -\ ==> F: Stable({s:state. z < f`s})"; +Goalw [Increasing_def] + "[| F:Increasing(nat, {:nat*nat. m le n}, f); f:state->nat; k:nat |] \ +\ ==> F: Stable({s:state. k < f`s})"; by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); by Safe_tac; -by (dres_inst_tac [("x", "succ(z)")] bspec 1); +by (dres_inst_tac [("x", "succ(k)")] bspec 1); by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq])); -by (subgoal_tac "{x: state . f ` x : nat} = state" 1); +by (subgoal_tac "{x: state . f`x : nat} = state" 1); by Auto_tac; -qed "strict_Increasing_onD"; +qed "strict_IncreasingD"; (*To allow expansion of the program's definition when appropriate*) val program_defs_ref = ref ([] : thm list); @@ -581,6 +519,9 @@ resolve_tac [StableI, stableI, constrains_imp_Constrains] 1), rtac constrainsI 1, + (* Three subgoals *) + rewrite_goal_tac [st_set_def] 3, + REPEAT (Force_tac 2), full_simp_tac (simpset() addsimps !program_defs_ref) 1, ALLGOALS Clarify_tac, REPEAT (FIRSTGOAL (etac disjE)), diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Constrains.thy Thu Nov 15 15:07:16 2001 +0100 @@ -11,7 +11,7 @@ Constrains = UNITY + consts traces :: "[i, i] => i" (* Initial states and program => (final state, reversed trace to it)... - the domain might also be state*list(state) *) + the domain may also be state*list(state) *) inductive domains "traces(init, acts)" <= @@ -45,8 +45,7 @@ defs Constrains_def - "A Co B == {F:program. F:(reachable(F) Int A) co B & - A:condition & B:condition}" + "A Co B == {F:program. F:(reachable(F) Int A) co B}" Unless_def "A Unless B == (A-B) Co (A Un B)" @@ -56,20 +55,10 @@ "Stable(A) == A Co A" (*Always is the weak form of "invariant"*) Always :: "i => i" - "Always(A) == {F:program. Init(F) <= A} Int Stable(A)" + "Always(A) == initially(A) Int Stable(A)" - (* - The constant Increasing_on defines a weak form of the Charpentier's - increasing notion. It should not be confused with the ZF's - increasing constant which have a different meaning. - Increasing's parameters: a state function f, - a domain A and a order relation r over the domain A. - Should f be a meta function instead ? - *) - Increasing_on :: [i,i, i] => i ("Increasing[_]'(_,_')") - "Increasing[A](f, r) == {F:program. f:state->A & - part_order(A,r) & - F: (INT z:A. Stable({s:state. :r}))}" - + (* Increasing is the weak from of increasing *) + Increasing :: [i,i, i] => i + "Increasing(A, r, f) == INT a:A. Stable({s:state. :r})" end diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/FP.ML --- a/src/ZF/UNITY/FP.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/FP.ML Thu Nov 15 15:07:16 2001 +0100 @@ -10,55 +10,46 @@ Theory ported form HOL. *) - -Goalw [FP_Orig_def] - "FP_Orig(F):condition"; +Goalw [FP_Orig_def] "FP_Orig(F)<=state"; by (Blast_tac 1); qed "FP_Orig_type"; -AddIffs [FP_Orig_type]; -AddTCs [FP_Orig_type]; -Goalw [FP_Orig_def, condition_def] - "x:FP_Orig(F) ==> x:state"; -by Auto_tac; -qed "FP_OrigD"; +Goalw [st_set_def] "st_set(FP_Orig(F))"; +by (rtac FP_Orig_type 1); +qed "st_set_FP_Orig"; +AddIffs [st_set_FP_Orig]; -Goalw [FP_def, condition_def] - "FP(F):condition"; +Goalw [FP_def] "FP(F)<=state"; by (Blast_tac 1); qed "FP_type"; -AddIffs [FP_type]; -AddTCs [FP_type]; -Goalw [FP_def, condition_def] - "x:FP(F) ==> x:state"; -by Auto_tac; -qed "FP_D"; +Goalw [st_set_def] "st_set(FP(F))"; +by (rtac FP_type 1); +qed "st_set_FP"; +AddIffs [st_set_FP]; Goal "Union(B) Int A = (UN C:B. C Int A)"; by (Blast_tac 1); qed "Int_Union2"; -Goalw [FP_Orig_def, stable_def] -"[| F:program; B:condition |] \ -\ ==> F:stable(FP_Orig(F) Int B)"; +Goalw [FP_Orig_def, stable_def] "F:program ==> F:stable(FP_Orig(F) Int B)"; by (stac Int_Union2 1); by (blast_tac (claset() addIs [constrains_UN]) 1); qed "stable_FP_Orig_Int"; -Goalw [FP_Orig_def, stable_def] - "[| ALL B:condition. F : stable (A Int B); A:condition |] \ -\ ==> A <= FP_Orig(F)"; +Goalw [FP_Orig_def, stable_def, st_set_def] + "[| ALL B. F: stable (A Int B); st_set(A) |] ==> A <= FP_Orig(F)"; by (Blast_tac 1); -bind_thm("FP_Orig_weakest", ballI RS result()); +qed "FP_Orig_weakest2"; + +bind_thm("FP_Orig_weakest", allI RS FP_Orig_weakest2); Goal "A Int cons(a, B) = \ \ (if a : A then cons(a, cons(a, (A Int B))) else A Int B)"; by Auto_tac; qed "Int_cons_right"; - -Goal "[| F:program; B:condition |] ==> F : stable (FP(F) Int B)"; +Goal "F:program ==> F : stable (FP(F) Int B)"; by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1); by (Blast_tac 2); by (asm_simp_tac (simpset() addsimps [Int_cons_right]) 1); @@ -67,38 +58,33 @@ by (auto_tac (claset(), simpset() addsimps [cons_absorb])); qed "stable_FP_Int"; - Goal "F:program ==> FP(F) <= FP_Orig(F)"; by (rtac (stable_FP_Int RS FP_Orig_weakest) 1); by Auto_tac; -val lemma1 = result(); - +qed "FP_subset_FP_Orig"; -Goalw [FP_Orig_def, FP_def] -"F:program ==> FP_Orig(F) <= FP(F)"; +Goalw [FP_Orig_def, FP_def] "F:program ==> FP_Orig(F) <= FP(F)"; by (Clarify_tac 1); -by (dres_inst_tac [("x", "{x}")] bspec 1); -by (force_tac (claset(), simpset() addsimps [condition_def]) 1); +by (dres_inst_tac [("x", "{x}")] spec 1); by (asm_full_simp_tac (simpset() addsimps [Int_cons_right]) 1); -by (auto_tac (claset(), simpset() addsimps [cons_absorb])); -by (force_tac (claset(), simpset() addsimps [condition_def]) 1); -val lemma2 = result(); +by (forward_tac [stableD2] 1); +by (auto_tac (claset(), simpset() addsimps [cons_absorb, st_set_def])); +qed "FP_Orig_subset_FP"; Goal "F:program ==> FP(F) = FP_Orig(F)"; -by (rtac ([lemma1,lemma2] MRS equalityI) 1); +by (rtac ([FP_subset_FP_Orig,FP_Orig_subset_FP] MRS equalityI) 1); by (ALLGOALS(assume_tac)); qed "FP_equivalence"; -Goal "[| ALL B:condition. F : stable(A Int B); A:condition; F:program |] \ -\ ==> A <= FP(F)"; +Goal "[| ALL B. F : stable(A Int B); F:program; st_set(A) |] ==> A <= FP(F)"; by (asm_simp_tac (simpset() addsimps [FP_equivalence, FP_Orig_weakest]) 1); -bind_thm("FP_weakest", result() RS ballI); +qed "FP_weakest2"; +bind_thm("FP_weakest", allI RS FP_weakest2); -Goalw [FP_def, stable_def, constrains_def, condition_def] - "[| F:program; A:condition |] ==> \ -\ A - FP(F) = (UN act: Acts(F). A -{s:state. act``{s} <= {s}})"; +Goalw [FP_def, stable_def, constrains_def, st_set_def] +"[| F:program; st_set(A) |] ==> A-FP(F) = (UN act:Acts(F). A-{s:state. act``{s} <= {s}})"; by (Blast_tac 1); qed "Diff_FP"; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/FP.thy --- a/src/ZF/UNITY/FP.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/FP.thy Thu Nov 15 15:07:16 2001 +0100 @@ -14,7 +14,7 @@ constdefs FP_Orig :: i=>i - "FP_Orig(F) == Union({A:condition. ALL B:condition. F : stable(A Int B)})" + "FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})" FP :: i=>i "FP(F) == {s:state. F : stable({s})}" diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Guar.ML --- a/src/ZF/UNITY/Guar.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Guar.ML Thu Nov 15 15:07:16 2001 +0100 @@ -11,51 +11,10 @@ Proofs ported from HOL. *) - -Goal -"F~:program ==> F Join G = programify(G)"; -by (rtac program_equalityI 1); -by Auto_tac; -by (auto_tac (claset(), - simpset() addsimps [Join_def, programify_def, SKIP_def, - Acts_def, Init_def, AllowedActs_def, - RawInit_eq, RawActs_eq, RawAllowedActs_eq, - Int_absorb, Int_assoc, Un_absorb])); -by (forward_tac [Id_in_RawActs] 2); -by (forward_tac [Id_in_RawAllowedActs] 3); -by (dtac RawInit_type 1); -by (dtac RawActs_type 2); -by (dtac RawAllowedActs_type 3); -by (auto_tac (claset(), simpset() - addsimps [condition_def, actionSet_def, cons_absorb])); -qed "not_program_Join1"; - -Goal -"G~:program ==> F Join G = programify(F)"; -by (stac Join_commute 1); -by (blast_tac (claset() addIs [not_program_Join1]) 1); -qed "not_program_Join2"; - -Goal "F~:program ==> F ok G"; -by (auto_tac (claset(), - simpset() addsimps [ok_def, programify_def, SKIP_def, mk_program_def, - Acts_def, Init_def, AllowedActs_def, - RawInit_def, RawActs_def, RawAllowedActs_def, - Int_absorb, Int_assoc, Un_absorb])); -by (auto_tac (claset(), simpset() - addsimps [condition_def, actionSet_def, program_def, cons_absorb])); -qed "not_program_ok1"; - -Goal "G~:program ==> F ok G"; -by (rtac ok_sym 1); -by (blast_tac (claset() addIs [not_program_ok1]) 1); -qed "not_program_ok2"; - - Goal "OK(cons(i, I), F) <-> \ \ (i:I & OK(I, F)) | (i~:I & OK(I, F) & F(i) ok JOIN(I,F))"; by (asm_full_simp_tac (simpset() addsimps [OK_iff_ok]) 1); -(** Auto_tac proves the goal in one step, but take more time **) +(** Auto_tac proves the goal in one-step, but takes more time **) by Safe_tac; by (ALLGOALS(Clarify_tac)); by (REPEAT(blast_tac (claset() addIs [ok_sym]) 10)); @@ -64,6 +23,10 @@ (*** existential properties ***) +Goalw [ex_prop_def] "ex_prop(X) ==> X<=program"; +by (Asm_simp_tac 1); +qed "ex_imp_subset_program"; + Goalw [ex_prop_def] "GG:Fin(program) ==> (ex_prop(X) \ \ --> GG Int X~=0 --> OK(GG, (%G. G)) -->(JN G:GG. G):X)"; @@ -77,8 +40,9 @@ qed_spec_mp "ex1"; Goalw [ex_prop_def] - "X<=program ==> (ALL GG. GG:Fin(program) & GG Int X ~= 0\ -\ --> OK(GG,(%G. G)) -->(JN G:GG. G):X) --> ex_prop(X)"; +"X<=program ==> \ +\(ALL GG. GG:Fin(program) & GG Int X ~= 0 --> OK(GG,(%G. G))-->(JN G:GG. G):X)\ +\ --> ex_prop(X)"; by (Clarify_tac 1); by (dres_inst_tac [("x", "{F,G}")] spec 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_iff_ok]))); @@ -88,37 +52,35 @@ (*Chandy & Sanders take this as a definition*) -Goal "X<=program ==> ex_prop(X) <-> \ -\ (ALL GG. GG:Fin(program) & GG Int X ~= 0 &\ -\ OK(GG,( %G. G)) --> (JN G:GG. G):X)"; -by (blast_tac (claset() addIs [ex1, ex2 RS mp]) 1); +Goal "ex_prop(X) <-> (X<=program & \ +\ (ALL GG. GG:Fin(program) & GG Int X ~= 0& OK(GG,( %G. G))-->(JN G:GG. G):X))"; +by Auto_tac; +by (ALLGOALS(blast_tac (claset() addIs [ex1, ex2 RS mp] + addDs [ex_imp_subset_program]))); qed "ex_prop_finite"; - -(*Their "equivalent definition" given at the end of section 3*) -Goalw [ex_prop2_def] - "ex_prop(X) <-> ex_prop2(X)"; -by (Asm_full_simp_tac 1); -by (rewrite_goals_tac - [ex_prop_def, component_of_def]); +(* Equivalent definition of ex_prop given at the end of section 3*) +Goalw [ex_prop_def, component_of_def] +"ex_prop(X) <-> \ +\ X<=program & (ALL G:program. (G:X <-> (ALL H:program. (G component_of H) --> H:X)))"; by Safe_tac; by (stac Join_commute 4); by (dtac ok_sym 4); -by (case_tac "G:program" 1); -by (dres_inst_tac [("x", "G")] bspec 5); -by (dres_inst_tac [("x", "F")] bspec 4); +by (dres_inst_tac [("x", "G")] bspec 4); +by (dres_inst_tac [("x", "F")] bspec 3); by Safe_tac; -by (force_tac (claset(), - simpset() addsimps [not_program_Join1]) 2); by (REPEAT(Force_tac 1)); qed "ex_prop_equiv"; (*** universal properties ***) +Goalw [uv_prop_def] "uv_prop(X)==> X<=program"; +by (Asm_simp_tac 1); +qed "uv_imp_subset_program"; + Goalw [uv_prop_def] "GG:Fin(program) ==> \ -\ (uv_prop(X)--> \ -\ GG <= X & OK(GG, (%G. G)) --> (JN G:GG. G):X)"; +\ (uv_prop(X)--> GG <= X & OK(GG, (%G. G)) --> (JN G:GG. G):X)"; by (etac Fin_induct 1); by (auto_tac (claset(), simpset() addsimps [OK_cons_iff])); @@ -137,14 +99,14 @@ (*Chandy & Sanders take this as a definition*) Goal -"X<=program ==> \ -\ uv_prop(X) <-> (ALL GG. GG:Fin(program) & GG <= X &\ -\ OK(GG, %G. G) --> (JN G:GG. G): X)"; -by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp]) 1)); +"uv_prop(X) <-> X<=program & \ +\ (ALL GG. GG:Fin(program) & GG <= X & OK(GG, %G. G) --> (JN G:GG. G): X)"; +by Auto_tac; +by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp] + addDs [uv_imp_subset_program]) 1)); qed "uv_prop_finite"; (*** guarantees ***) -(* The premise G:program is needed later *) val major::prems = Goal "[| (!!G. [| F ok G; F Join G:X; G:program |] ==> F Join G : Y); F:program |] \ \ ==> F : X guarantees Y"; @@ -184,31 +146,35 @@ by (Blast_tac 1); qed "subset_imp_guarantees"; +Goalw [component_of_def] +"F ok G ==> F component_of (F Join G)"; +by (Blast_tac 1); +qed "component_of_Join1"; + +Goal "F ok G ==> G component_of (F Join G)"; +by (stac Join_commute 1); +by (blast_tac (claset() addIs [ok_sym, component_of_Join1]) 1); +qed "component_of_Join2"; + (*Remark at end of section 4.1 *) Goalw [guar_def, component_of_def] -"Y<=program ==>ex_prop(Y) --> (Y = (program guarantees Y))"; -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); -(* Simplification tactics with ex_prop2_def loops *) -by (rewrite_goals_tac [ex_prop2_def]); +"ex_prop(Y) ==> (Y = (program guarantees Y))"; +by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1); by (Clarify_tac 1); by (rtac equalityI 1); by Safe_tac; -by (Blast_tac 1); -by (dres_inst_tac [("x", "x")] bspec 1); -by (dres_inst_tac [("x", "x")] bspec 3); -by (dtac iff_sym 4); -by (Blast_tac 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (etac iffE 2); +by (dres_inst_tac [("x", "x")] bspec 2); +by (dres_inst_tac [("x", "x")] bspec 4); +by (dtac iff_sym 5); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_Join1]))); +by (etac iffE 3); by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); by Safe_tac; by (REPEAT(Force_tac 1)); qed "ex_prop_imp"; -Goalw [guar_def] - "(Y = program guarantees Y) ==> ex_prop(Y)"; +Goalw [guar_def] "(Y = program guarantees Y) ==> ex_prop(Y)"; by (asm_simp_tac (simpset() addsimps [ex_prop_equiv]) 1); -by (rewrite_goals_tac [ex_prop2_def]); by Safe_tac; by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); by (dtac sym 2); @@ -216,11 +182,8 @@ by (REPEAT(Force_tac 1)); qed "guarantees_imp"; -Goal "Y<=program ==>(ex_prop(Y)) <-> (Y = program guarantees Y)"; -by (rtac iffI 1); -by (rtac (ex_prop_imp RS mp) 1); -by (rtac guarantees_imp 3); -by (ALLGOALS(Asm_simp_tac)); +Goal "(ex_prop(Y)) <-> (Y = program guarantees Y)"; +by (blast_tac (claset() addIs [ex_prop_imp, guarantees_imp]) 1); qed "ex_prop_equiv2"; (** Distributive laws. Re-orient to perform miniscoping **) @@ -403,7 +366,20 @@ by (Blast_tac 1); qed "refines_refl"; -(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) +(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *) + +Goalw [wg_def] "wg(F, X) <= program"; +by Auto_tac; +qed "wg_type"; + +Goalw [guar_def] "X guarantees Y <= program"; +by Auto_tac; +qed "guarantees_type"; + +Goalw [wg_def] "G:wg(F, X) ==> G:program & F:program"; +by Auto_tac; +by (blast_tac (claset() addDs [guarantees_type RS subsetD]) 1); +qed "wgD2"; Goalw [guar_def, component_of_def] "(F:X guarantees Y) <-> \ @@ -421,21 +397,18 @@ by (Blast_tac 1); qed "wg_guarantees"; -Goalw [wg_def] - "[| F:program; H:program |] ==> \ -\ (H: wg(F,X)) <-> H:program & (F component_of H --> H:X)"; +Goalw [wg_def] "(H: wg(F,X)) <-> ((F component_of H --> H:X) & F:program & H:program)"; by (simp_tac (simpset() addsimps [guarantees_equiv]) 1); by (rtac iffI 1); by Safe_tac; +by (res_inst_tac [("x", "{H}")] bexI 4); by (res_inst_tac [("x", "{H}")] bexI 3); -by (res_inst_tac [("x", "{H}")] bexI 2); by (REPEAT(Blast_tac 1)); qed "wg_equiv"; Goal -"[| F component_of H; F:program; H:program |] ==> \ -\ H:wg(F,X) <-> H:X"; -by (asm_full_simp_tac (simpset() addsimps [wg_equiv]) 1); +"F component_of H ==> H:wg(F,X) <-> (H:X & F:program & H:program)"; +by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1); qed "component_of_wg"; Goal @@ -457,10 +430,8 @@ ==> JOIN(FF, %F. F):wg(G, X) <-> JOIN(FF, %F. F):X" *) val wg_finite2 = wg_finite RS bspec RS mp RS mp RS bspec; - -Goal "[| ex_prop(X); F:program |] ==> (F:X) <-> (ALL H:program. H : wg(F,X))"; -by (asm_full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); -by (rewrite_goals_tac [ex_prop2_def]); +Goal "ex_prop(X) ==> (F:X) <-> (ALL H:program. H : wg(F,X) & F:program)"; +by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); by (Blast_tac 1); qed "wg_ex_prop"; @@ -470,15 +441,12 @@ by Auto_tac; qed "wx_subset"; -Goalw [wx_def] "wx(X)<=program"; -by Auto_tac; -qed "wx_into_program"; - Goal "ex_prop(wx(X))"; by (full_simp_tac (simpset() addsimps [ex_prop_def, wx_def]) 1); by Safe_tac; +by (Blast_tac 1); by (ALLGOALS(res_inst_tac [("x", "xb")] bexI)); by (REPEAT(Force_tac 1)); qed "wx_ex_prop"; @@ -494,10 +462,10 @@ by Safe_tac; by (dres_inst_tac [("x", "G Join Ga")] bspec 1); by (Simp_tac 1); -by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1); +by (force_tac (claset(), simpset() addsimps [Join_assoc]) 1); by (dres_inst_tac [("x", "F Join Ga")] bspec 1); by (Simp_tac 1); -by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1); +by (Full_simp_tac 1); by Safe_tac; by (asm_simp_tac (simpset() addsimps [ok_commute]) 1); by (subgoal_tac "F Join G = G Join F" 1); @@ -513,6 +481,7 @@ by Safe_tac; by (Blast_tac 1); by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1); +by Safe_tac; by (dres_inst_tac [("x", "x")] bspec 1); by (dres_inst_tac [("x", "G")] bspec 2); by (forw_inst_tac [("c", "x Join G")] subsetD 3); @@ -534,13 +503,13 @@ (* Proposition 12 *) (* Main result of the paper *) -Goalw [guar_def] - "(X guarantees Y) = wx((program-X) Un Y)"; +Goalw [guar_def] "(X guarantees Y) = wx((program-X) Un Y)"; by (simp_tac (simpset() addsimps [wx_equiv]) 1); by Auto_tac; qed "guarantees_wx_eq"; -(* {* Corollary, but this result has already been proved elsewhere *} +(* +{* Corollary, but this result has already been proved elsewhere *} "ex_prop(X guarantees Y)"; by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); qed "guarantees_ex_prop"; @@ -549,33 +518,33 @@ (* Rules given in section 7 of Chandy and Sander's Reasoning About Program composition paper *) -Goal "[| Init(F) <= A; F:program |] \ -\ ==> F:(stable(A)) guarantees (Always(A))"; +Goal "[| Init(F) <= A; F:program |] ==> F:(stable(A)) guarantees (Always(A))"; by (rtac guaranteesI 1); by (assume_tac 2); by (simp_tac (simpset() addsimps [Join_commute]) 1); by (rtac stable_Join_Always1 1); -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [invariant_def, Join_stable]))); -by (auto_tac (claset(), simpset() addsimps [programify_def])); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [invariant_def]))); +by (auto_tac (claset(), simpset() addsimps [programify_def, initially_def])); qed "stable_guarantees_Always"; (* To be moved to WFair.ML *) -Goal "[| F:A co A Un B; F:transient(A) |] ==> F:A leadsTo B"; +Goal "[| F:A co A Un B; F:transient(A); st_set(B) |] ==> F:A leadsTo B"; +by (forward_tac [constrainsD2] 1); by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); by (rtac (ensuresI RS leadsTo_Basis) 3); by (ALLGOALS(Blast_tac)); qed "leadsTo_Basis'"; -Goal "[| F:transient(A); B:condition |] \ -\ ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; +Goal "[| F:transient(A); st_set(B) |] ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; by (rtac guaranteesI 1); +by (blast_tac (claset() addDs [transient_type RS subsetD]) 2); by (rtac leadsTo_Basis' 1); +by (Blast_tac 3); by (dtac constrains_weaken_R 1); -by (assume_tac 3); -by (blast_tac (claset() addIs [Join_transient_I1]) 3); -by (REPEAT(blast_tac (claset() addDs [transientD]) 1)); +by (assume_tac 2); +by (rtac Join_transient_I1 2); +by (REPEAT(Blast_tac 1)); qed "constrains_guarantees_leadsTo"; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Guar.thy --- a/src/ZF/UNITY/Guar.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Guar.thy Thu Nov 15 15:07:16 2001 +0100 @@ -25,25 +25,20 @@ case, proving equivalence with Chandy and Sanders's n-ary definitions*) ex_prop :: i =>o - "ex_prop(X) == ALL F:program. ALL G:program. - F ok G --> F:X | G:X --> (F Join G):X" + "ex_prop(X) == X<=program & + (ALL F:program. ALL G:program. F ok G --> F:X | G:X --> (F Join G):X)" - (* Equivalent definition of ex_prop given at the end of section 3*) - ex_prop2 :: i =>o - "ex_prop2(X) == ALL G:program. (G:X <-> (ALL H:program. (G component_of H) --> H:X))" - strict_ex_prop :: i => o - "strict_ex_prop(X) == ALL F:program. ALL G:program. - F ok G --> (F:X | G: X) <-> (F Join G : X)" - + "strict_ex_prop(X) == X<=program & + (ALL F:program. ALL G:program. F ok G --> (F:X | G: X) <-> (F Join G : X))" uv_prop :: i => o - "uv_prop(X) == SKIP:X & (ALL F:program. ALL G:program. - F ok G --> F:X & G:X --> (F Join G):X)" + "uv_prop(X) == X<=program & + (SKIP:X & (ALL F:program. ALL G:program. F ok G --> F:X & G:X --> (F Join G):X))" strict_uv_prop :: i => o - "strict_uv_prop(X) == SKIP:X & - (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X))" + "strict_uv_prop(X) == X<=program & + (SKIP:X & (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X)))" guar :: [i, i] => i (infixl "guarantees" 55) (*higher than membership, lower than Co*) diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Mutex.ML --- a/src/ZF/UNITY/Mutex.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Mutex.ML Thu Nov 15 15:07:16 2001 +0100 @@ -5,6 +5,10 @@ Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra +Variables' types are introduced globally so that type verification +reduces to the usual ZF typechecking: an ill-tyed expression will +reduce to the empty set. + *) (** Variables' types **) @@ -12,43 +16,35 @@ AddIffs [p_type, u_type, v_type, m_type, n_type]; Goal "!!s. s:state ==> s`u:bool"; -by (dres_inst_tac [("a", "u"), ("A", "variable")] - apply_type 1); -by (auto_tac (claset(), simpset() addsimps [u_type])); +by (dres_inst_tac [("a", "u"), ("A", "var")] apply_type 1); +by Auto_tac; qed "u_apply_type"; Goal "!!s. s:state ==> s`v:bool"; -by (dres_inst_tac [("a", "v"), ("A", "variable")] - apply_type 1); -by (auto_tac (claset(), simpset() addsimps [v_type])); +by (dres_inst_tac [("a", "v"), ("A", "var")] apply_type 1); +by Auto_tac; qed "v_apply_type"; - Goal "!!s. s:state ==> s`p:bool"; -by (dres_inst_tac [("a", "p"), ("A", "variable")] - apply_type 1); -by (auto_tac (claset(), simpset() addsimps [p_type])); +by (dres_inst_tac [("a", "p"), ("A", "var")] apply_type 1); +by Auto_tac; qed "p_apply_type"; Goal "!!s. s:state ==> s`m:int"; -by (dres_inst_tac [("a", "m"), ("A", "variable")] - apply_type 1); -by (auto_tac (claset(), simpset() addsimps [m_type])); +by (dres_inst_tac [("a", "m"), ("A", "var")] apply_type 1); +by Auto_tac; qed "m_apply_type"; Goal "!!s. s:state ==> s`n:int"; -by (dres_inst_tac [("a", "n"), ("A", "variable")] - apply_type 1); -by (auto_tac (claset(), simpset() addsimps [n_type])); +by (dres_inst_tac [("a", "n"), ("A", "var")] apply_type 1); +by Auto_tac; qed "n_apply_type"; - -Addsimps [p_apply_type, u_apply_type, v_apply_type, m_apply_type, n_apply_type]; - +Addsimps [p_apply_type, u_apply_type, v_apply_type, + m_apply_type, n_apply_type]; (** Mutex is a program **) -Goalw [Mutex_def] -"Mutex:program"; +Goalw [Mutex_def] "Mutex:program"; by Auto_tac; qed "Mutex_in_program"; AddIffs [Mutex_in_program]; @@ -65,17 +61,9 @@ Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]); -Addsimps [condition_def, actionSet_def]; - - -Addsimps variable.intrs; -AddIs variable.intrs; - (** In case one wants to be sure that the initial state is not empty **) Goal "some(u:=0,v:=0, m:= #0,n:= #0):Init(Mutex)"; -by Auto_tac; -by (REPEAT(rtac update_type2 1)); -by (auto_tac (claset(), simpset() addsimps [lam_type])); +by (auto_tac (claset() addSIs [update_type2], simpset())); qed "Mutex_Init_not_empty"; Goal "Mutex : Always(IU)"; @@ -85,7 +73,6 @@ Goal "Mutex : Always(IV)"; by (always_tac 1); -by Auto_tac; qed "IV"; @@ -124,25 +111,21 @@ Goalw [Unless_def] "Mutex : {s:state. s`m=#2} Unless {s:state. s`m=#3}"; by (constrains_tac 1); -by Auto_tac; qed "U_F0"; Goal "Mutex : {s:state. s`m=#1} LeadsTo {s:state. s`p = s`v & s`m = #2}"; by (ensures_tac "U1" 1); -by Auto_tac; qed "U_F1"; Goal "Mutex : {s:state. s`p =0 & s`m = #2} LeadsTo {s:state. s`m = #3}"; by (cut_facts_tac [IU] 1); by (ensures_tac "U2" 1); -by Auto_tac; qed "U_F2"; Goal "Mutex : {s:state. s`m = #3} LeadsTo {s:state. s`p=1}"; by (res_inst_tac [("B", "{s:state. s`m = #4}")] LeadsTo_Trans 1); by (ensures_tac "U4" 2); by (ensures_tac "U3" 1); -by Auto_tac; qed "U_F3"; @@ -191,7 +174,6 @@ Goalw [Unless_def] "Mutex : {s:state. s`n=#2} Unless {s:state. s`n=#3}"; by (constrains_tac 1); -by Auto_tac; qed "V_F0"; Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}"; @@ -202,14 +184,12 @@ Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}"; by (cut_facts_tac [IV] 1); by (ensures_tac "V2" 1); -by Auto_tac; qed "V_F2"; Goal "Mutex : {s:state. s`n = #3} LeadsTo {s:state. s`p=0}"; by (res_inst_tac [("B", "{s:state. s`n = #4}")] LeadsTo_Trans 1); by (ensures_tac "V4" 2); by (ensures_tac "V3" 1); -by Auto_tac; qed "V_F3"; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Mutex.thy --- a/src/ZF/UNITY/Mutex.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Mutex.thy Thu Nov 15 15:07:16 2001 +0100 @@ -5,9 +5,8 @@ Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra -Variables' types are introduced globally so that type verification of -UNITY programs/specifications reduce to the usual ZF typechecking. -An ill-tyed expression will reduce to the empty set. +Variables' types are introduced globally so that type verification +reduces to the usual ZF typechecking: an ill-tyed expressions reduce to the empty set. *) Mutex = SubstAx + @@ -65,7 +64,7 @@ Mutex :: i "Mutex == mk_program({s:state. s`u=0 & s`v=0 & s`m = #0 & s`n = #0}, - {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, action)" + {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, Pow(state*state))" (** The correct invariants **) diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/State.ML --- a/src/ZF/UNITY/State.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/State.ML Thu Nov 15 15:07:16 2001 +0100 @@ -5,160 +5,60 @@ Formalizes UNITY-program states. *) - -AddIffs [some_in_state]; - +AddIffs [some_assume]; -Goal "!!A. state<=A ==> EX x. x:A"; -by (res_inst_tac [("x", "some")] exI 1); -by Auto_tac; -qed "state_subset_not_empty"; - -(** condition **) -Goalw [condition_def] - "A:condition ==>A<=state"; -by (Blast_tac 1); -qed "conditionD"; +AddIs var.intrs; +Addsimps var.intrs; -Goalw [condition_def] - "A<=state ==> A:condition"; -by (Blast_tac 1); -qed "conditionI"; - -(** actionSet **) -Goalw [actionSet_def] -"acts:actionSet ==> acts<=action"; -by (Blast_tac 1); -qed "actionSetD"; - -Goalw [actionSet_def] -"acts<=action ==>acts:actionSet"; -by (Blast_tac 1); -qed "actionSetI"; - -(** Identity **) -Goalw [condition_def, Identity_def] -"A:condition ==> Id``A = A"; -by (Blast_tac 1); -qed "Id_image"; +Goalw [st_set_def] "st_set({x:state. P(x)})"; +by Auto_tac; +qed "st_set_Collect"; +AddIffs [st_set_Collect]; -Goalw [Identity_def] -"A<=state ==> Id``A = A"; -by (Blast_tac 1); -qed "Id_image2"; - -Addsimps [Id_image, Id_image2]; - -Goalw [Identity_def] - "Id:action"; -by (Blast_tac 1); -qed "Id_in_action"; -AddIffs [Id_in_action]; -AddTCs [Id_in_action]; +Goalw [st_set_def] "st_set(0)"; +by (Simp_tac 1); +qed "st_set_0"; +AddIffs [st_set_0]; -Goalw [Identity_def] - "(x:Id) <-> (EX c:state. x=)"; -by (Blast_tac 1); -qed "Id_member_simp"; -Addsimps [Id_member_simp]; - -Goalw [Identity_def] -"Id``0 = 0"; -by (Blast_tac 1); -qed "Id_0"; -Addsimps [Id_0]; +Goalw [st_set_def] "st_set(state)"; +by (Simp_tac 1); +qed "st_set_state"; +AddIffs [st_set_state]; - -Goalw [Identity_def] -"Id``state = state"; -by (Blast_tac 1); -qed "Id_image_state"; -Addsimps [Id_image_state]; - -Goalw [condition_def] -"0:condition"; -by (Blast_tac 1); -qed "condition_0"; +(* Union *) -Goalw [condition_def] -"state:condition"; -by (Blast_tac 1); -qed "condition_state"; - -Goalw [actionSet_def] -"0:actionSet"; +Goalw [st_set_def] +"st_set(A Un B) <-> st_set(A) & st_set(B)"; by Auto_tac; -qed "actionSet_0"; - -Goalw [actionSet_def] -"action:actionSet"; -by Auto_tac; -qed "actionSet_Prod"; - -AddIffs [condition_0, condition_state, actionSet_0, actionSet_Prod]; -AddTCs [condition_0, condition_state, actionSet_0, actionSet_Prod]; +qed "st_set_Un_iff"; +AddIffs [st_set_Un_iff]; -(** Simplification rules for condition **) - - -(** Union and Un **) - -Goalw [condition_def] - "A Un B:condition <-> A:condition & B:condition"; -by (Blast_tac 1); -qed "condition_Un"; +Goalw [st_set_def] +"st_set(Union(S)) <-> (ALL A:S. st_set(A))"; +by Auto_tac; +qed "st_set_Union_iff"; +AddIffs [st_set_Union_iff]; -Goalw [condition_def] - "Union(S):condition <-> (ALL A:S. A:condition)"; -by (Blast_tac 1); -qed "condition_Union"; - -AddIffs [condition_Un, condition_Union]; -AddIs [condition_Un RS iffD2, condition_Union RS iffD2]; - -(** Intersection **) +(* Intersection *) -Goalw [condition_def] - "[| A:condition; B:condition |] ==> A Int B: condition"; -by (Blast_tac 1); -qed "condition_IntI"; - -Goalw [condition_def, Inter_def] - "(ALL A:S. A:condition) ==> Inter(S): condition"; -by (Blast_tac 1); -bind_thm("condition_InterI", ballI RS result()); - -AddIs [condition_IntI, condition_InterI]; -Addsimps [condition_IntI, condition_InterI]; - -Goalw [condition_def] -"A:condition ==> A - B :condition"; -by (Blast_tac 1); -qed "condition_DiffI"; -AddIs [condition_DiffI]; -Addsimps [condition_DiffI]; - +Goalw [st_set_def] +"st_set(A) | st_set(B) ==> st_set(A Int B)"; +by Auto_tac; +qed "st_set_Int"; +AddSIs [st_set_Int]; -(** Needed in WFair.thy **) -Goalw [condition_def] -"S:Pow(condition) ==> Union(S):condition"; -by (Blast_tac 1); -qed "Union_in_conditionI"; - -(** Simplification rules **) +Goalw [st_set_def, Inter_def] + "(S=0) | (EX A:S. st_set(A)) ==> st_set(Inter(S))"; +by Auto_tac; +qed "st_set_Inter"; +AddSIs [st_set_Inter]; -Goalw [condition_def] - "{s:state. P(s)}:condition"; +(* Diff *) +Goalw [st_set_def] +"st_set(A) ==> st_set(A - B)"; by Auto_tac; -qed "Collect_in_condition"; - -Goal "{s:state. P(s)}:Pow(state)"; -by Auto_tac; -qed "Collect_condition2"; - -Goal "{s:state. P(s)}<=state"; -by Auto_tac; -qed "Collect_condition3"; +qed "st_set_DiffI"; +AddSIs [st_set_DiffI]; Goal "{s:state. P(s)} Int state = {s:state. P(s)}"; by Auto_tac; @@ -166,45 +66,25 @@ Goal "state Int {s:state. P(s)} = {s:state. P(s)}"; by Auto_tac; -qed "Collect_Int_state2"; +qed "state_Int_Collect"; +AddIffs [Collect_Int_state, state_Int_Collect]; + +(* Introduction and destruction rules for st_set *) + +Goalw [st_set_def] + "A <= state ==> st_set(A)"; +by (assume_tac 1); +qed "st_setI"; -val state_simps = [Collect_in_condition, Collect_condition2, -Collect_condition3, Collect_Int_state, Collect_Int_state2]; +Goalw [st_set_def] + "st_set(A) ==> A<=state"; +by (assume_tac 1); +qed "st_setD"; + +Goalw [st_set_def] +"[| st_set(A); B<=A |] ==> st_set(B)"; +by Auto_tac; +qed "st_set_subset"; -(* actionSet *) -Goalw [actionSet_def] - "(A Un B):actionSet <-> (A:actionSet&B:actionSet)"; -by Auto_tac; -qed "actionSet_Un"; - -Goalw [actionSet_def] - "(UN i:I. A(i)):actionSet <-> (ALL i:I. A(i):actionSet)"; -by Auto_tac; -qed "actionSet_UN"; - -AddIffs [actionSet_Un, actionSet_UN]; -AddIs [actionSet_Un RS iffD2, actionSet_UN RS iffD2]; - -Goalw [actionSet_def] -"[| A:actionSet; B:actionSet |] ==> (A Int B):actionSet"; -by Auto_tac; -qed "actionSet_Int"; - -Goalw [actionSet_def] -"(ALL i:I. A(i):actionSet) ==> (INT i:I. A(i)):actionSet"; -by (auto_tac (claset(), simpset() addsimps [Inter_def])); -qed "actionSet_INT"; - -Addsimps [actionSet_INT]; -AddIs [actionSet_INT]; -Addsimps [Inter_0]; - -Goalw [condition_def] - "(PROD x:variable. type_of(x)):condition"; -by Auto_tac; -qed "PROD_condition"; - -Addsimps [PROD_condition]; -AddIs [PROD_condition]; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/State.thy --- a/src/ZF/UNITY/State.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/State.thy Thu Nov 15 15:07:16 2001 +0100 @@ -3,58 +3,47 @@ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge -Formalizes UNITY-program states using dependent types: +Formalizes UNITY-program states using dependent types so that: - variables are typed. - the state space is uniform, common to all defined programs. - variables can be quantified over. - *) State = UNITYMisc + -consts - variable :: i - -(** - Variables are better represented using integers, but at the moment - there is a problem with integer translations like "uu" == "Var(#0)", which - are needed to give names to variables. - So for the time being we are using lists of naturals to index variables. - **) +consts var::i +datatype var = Var("i:list(nat)") + type_intrs "[list_nat_into_univ]" -datatype variable = Var("i:list(nat)") - type_intrs "[list_nat_into_univ]" - consts - state, action, some ::i type_of :: i=>i + some :: i + state :: i + st_set :: i =>o +translations + "state" == "Pi(var, type_of)" -translations - (* The state space is a dependent type *) - "state" == "Pi(variable, type_of)" - - (* Commands are relations over states *) - "action" == "Pow(state*state)" +defs + (* To prevent typing conditions (like `A<=state') from + being used in combination with the rules `constrains_weaken', etc. *) + st_set_def "st_set(A) == A<=state" rules - (** We might have defined the state space in a such way that it is already - not empty by formation: for example "state==PROD x:variable. type_of(x) Un {0}" - which contains the function (lam x:variable. 0) is a possible choice. - However, we prefer the following way for simpler proofs by avoiding - case splitting resulting from type_of(x) Un {0}. **) + some_assume "some:state" - some_in_state "some:state" +(*** +REMARKS: + 1. The reason of indexing variables by lists instead of integers is that, +at the time I was writing this theory, translations like `foo == Var(#1)' +mysteriously provoke a syntactical error. Such translations are used +for introducing variable names when specifying programs. -constdefs - (* State conditions/predicates are sets of states *) - condition :: i - "condition == Pow(state)" - - actionSet :: i - "actionSet == Pow(action)" - -consts - Id :: i -translations - "Id" == "Identity(state)" + 2. State space `state' is required to be not empty. This requirement +can be achieved by definition: the space "PROD x:var. type_of(x) Un {0}" +includes the state `lam x:state. 0'. However, such definition leads to +complications later during program type-chinking. For example, to prove +that the assignment `foo:=#1' is well typed, for `foo' an integer +variable, we would have to show two things: (a) that #1 is an integer +but also (b) that #1 is different from 0. Hence axiom `some_assume'. +***) end \ No newline at end of file diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/SubstAx.ML --- a/src/ZF/UNITY/SubstAx.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/SubstAx.ML Thu Nov 15 15:07:16 2001 +0100 @@ -10,78 +10,71 @@ (*Resembles the previous definition of LeadsTo*) +(* Equivalence with the HOL-like definition *) Goalw [LeadsTo_def] - "A LeadsTo B = \ -\ {F:program. F : (reachable(F) Int A) leadsTo (reachable(F) Int B) & \ -\ A:condition & B:condition}"; -by (blast_tac (claset() addDs [psp_stable2, leadsToD, constrainsD2] +"st_set(B)==> A LeadsTo B = {F:program. F:(reachable(F) Int A) leadsTo B}"; +by (blast_tac (claset() addDs [psp_stable2, leadsToD2, constrainsD2] addIs [leadsTo_weaken]) 1); -qed "LeadsTo_eq_leadsTo"; +qed "LeadsTo_eq"; -Goalw [LeadsTo_def] -"F: A LeadsTo B ==> F:program & A:condition & B:condition"; -by (Blast_tac 1); -qed "LeadsToD"; +Goalw [LeadsTo_def] "A LeadsTo B <=program"; +by Auto_tac; +qed "LeadsTo_type"; (*** Specialized laws for handling invariants ***) (** Conjoining an Always property **) -Goal "[| F : Always(INV); A:condition |] ==> \ -\ (F : (INV Int A) LeadsTo A') <-> (F : A LeadsTo A')"; +Goal "F : Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F: A LeadsTo A')"; by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable, - Int_absorb2, Int_assoc RS sym, leadsToD]) 1); + Int_absorb2, Int_assoc RS sym, leadsToD2]) 1); qed "Always_LeadsTo_pre"; -Goal "[| F : Always(INV); A':condition |] \ - \ ==> (F : A LeadsTo (INV Int A')) <-> (F : A LeadsTo A')"; -by (asm_full_simp_tac - (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable, - Int_absorb2, Int_assoc RS sym,leadsToD]) 1); +Goalw [LeadsTo_def] "F:Always(I) ==> (F : A LeadsTo (I Int A')) <-> (F : A LeadsTo A')"; +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable, + Int_absorb2, Int_assoc RS sym,leadsToD2]) 1); qed "Always_LeadsTo_post"; (* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *) -Goal "[| F:Always(C); F : (C Int A) LeadsTo A'; A:condition |] \ -\ ==> F: A LeadsTo A'"; +Goal "[| F:Always(C); F : (C Int A) LeadsTo A' |] ==> F: A LeadsTo A'"; by (blast_tac (claset() addIs [Always_LeadsTo_pre RS iffD1]) 1); qed "Always_LeadsToI"; (* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *) -Goal -"[| F : Always(C); F : A LeadsTo A'; A':condition |] \ -\ ==> F : A LeadsTo (C Int A')"; +Goal "[| F:Always(C); F:A LeadsTo A' |] ==> F : A LeadsTo (C Int A')"; by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1); qed "Always_LeadsToD"; (*** Introduction rules: Basis, Trans, Union ***) -Goal "F : A leadsTo B ==> F : A LeadsTo B"; -by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); -by (blast_tac (claset() addIs [leadsTo_weaken_L] - addDs [leadsToD]) 1); -qed "leadsTo_imp_LeadsTo"; +Goal "F : A Ensures B ==> F : A LeadsTo B"; +by (auto_tac (claset(), simpset() addsimps + [Ensures_def, LeadsTo_def])); +qed "LeadsTo_Basis"; Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"; -by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1); +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_Trans]) 1); qed "LeadsTo_Trans"; -Goalw [LeadsTo_def] - "[| ALL A:S. F : A LeadsTo B; F:program; B:condition |] \ -\ ==> F : Union(S) LeadsTo B"; +val [major, program] = Goalw [LeadsTo_def] +"[|(!!A. A:S ==> F : A LeadsTo B); F:program|]==>F:Union(S) LeadsTo B"; +by (cut_facts_tac [program] 1); by Auto_tac; by (stac Int_Union_Union2 1); -by (blast_tac (claset() addIs [leadsTo_UN]) 1); -bind_thm("LeadsTo_Union", ballI RS result()); - +by (rtac leadsTo_UN 1); +by (dtac major 1); +by Auto_tac; +qed "LeadsTo_Union"; (*** Derived rules ***) -Goalw [LeadsTo_def] -"[| F:program; A:condition |] ==>F : A LeadsTo state"; -by (blast_tac (claset() addIs [leadsTo_state]) 1); -qed "LeadsTo_state"; -Addsimps [LeadsTo_state]; +Goal "F : A leadsTo B ==> F : A LeadsTo B"; +by (forward_tac [leadsToD2] 1); +by (Clarify_tac 1); +by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1); +by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); +qed "leadsTo_imp_LeadsTo"; (*Useful with cancellation, disjunction*) Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"; @@ -92,108 +85,102 @@ by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "LeadsTo_Un_duplicate2"; -Goal "[| ALL i:I. F : A(i) LeadsTo B; F:program; B:condition |] \ +val [major, program] = Goalw [LeadsTo_def] +"[|(!!i. i:I ==> F : A(i) LeadsTo B); F:program|] \ \ ==> F : (UN i:I. A(i)) LeadsTo B"; -by (simp_tac (simpset() addsimps [Int_Union_Union]) 1); -by (blast_tac (claset() addIs [LeadsTo_Union]) 1); -bind_thm("LeadsTo_UN", ballI RS result()); +by (cut_facts_tac [program] 1); +by (asm_simp_tac (simpset() addsimps [Int_Union_Union2]) 1); +by (rtac leadsTo_UN 1); +by (dtac major 1); +by Auto_tac; +qed "LeadsTo_UN"; (*Binary union introduction rule*) Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"; by (stac Un_eq_Union 1); -by (blast_tac (claset() addIs [LeadsTo_Union] - addDs [LeadsToD]) 1); +by (rtac LeadsTo_Union 1); +by (auto_tac (claset() addDs [LeadsTo_type RS subsetD], simpset())); qed "LeadsTo_Un"; (*Lets us look at the starting state*) -Goal "[| ALL s:A. F : {s} LeadsTo B; F:program; B:condition |]\ -\ ==> F : A LeadsTo B"; +val [major, program] = Goal +"[|(!!s. s:A ==> F:{s} LeadsTo B); F:program|]==>F:A LeadsTo B"; +by (cut_facts_tac [program] 1); by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1); -by (REPEAT(Blast_tac 1)); -bind_thm("single_LeadsTo_I", ballI RS result()); +by (forward_tac [major] 1); +by Auto_tac; +qed "single_LeadsTo_I"; -Goal "[| A <= B; B:condition; F:program |] ==> F : A LeadsTo B"; -by (subgoal_tac "A:condition" 1); -by (force_tac (claset(), - simpset() addsimps [condition_def]) 2); -by (simp_tac (simpset() addsimps [LeadsTo_def]) 1); +Goal "[| A <= B; F:program |] ==> F : A LeadsTo B"; +by (asm_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "subset_imp_LeadsTo"; -bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo); -Addsimps [empty_LeadsTo]; +Goal "F:0 LeadsTo A <-> F:program"; +by (auto_tac (claset() addDs [LeadsTo_type RS subsetD] + addIs [empty_subsetI RS subset_imp_LeadsTo], simpset())); +qed "empty_LeadsTo"; +AddIffs [empty_LeadsTo]; -Goal "[| F : A LeadsTo A'; A' <= B'; B':condition |] ==> F : A LeadsTo B'"; -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); -by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1); +Goal "F : A LeadsTo state <-> F:program"; +by (auto_tac (claset() addDs [LeadsTo_type RS subsetD], + simpset() addsimps [LeadsTo_eq])); +qed "LeadsTo_state"; +AddIffs [LeadsTo_state]; + +Goalw [LeadsTo_def] + "[| F:A LeadsTo A'; A'<=B'|] ==> F : A LeadsTo B'"; +by (auto_tac (claset() addIs[leadsTo_weaken_R], simpset())); qed_spec_mp "LeadsTo_weaken_R"; - -Goal "[| F : A LeadsTo A'; B <= A |] \ -\ ==> F : B LeadsTo A'"; -by (subgoal_tac "B:condition" 1); -by (force_tac (claset() addSDs [LeadsToD], - simpset() addsimps [condition_def]) 2); -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); -by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); +Goalw [LeadsTo_def] "[| F : A LeadsTo A'; B <= A |] ==> F : B LeadsTo A'"; +by (auto_tac (claset() addIs[leadsTo_weaken_L], simpset())); qed_spec_mp "LeadsTo_weaken_L"; -Goal "[| F : A LeadsTo A'; \ -\ B <= A; A' <= B'; B':condition |] \ -\ ==> F : B LeadsTo B'"; +Goal "[| F : A LeadsTo A'; B<=A; A'<=B' |] ==> F : B LeadsTo B'"; by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L, LeadsTo_Trans]) 1); qed "LeadsTo_weaken"; -Goal "[| F : Always(C); F : A LeadsTo A'; \ -\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \ +Goal +"[| F:Always(C); F:A LeadsTo A'; C Int B <= A; C Int A' <= B' |] \ \ ==> F : B LeadsTo B'"; -by (blast_tac (claset() - addDs [AlwaysD2, LeadsToD, Always_LeadsToI] - addIs [LeadsTo_weaken, Always_LeadsToD]) 1); +by (blast_tac (claset() addDs [Always_LeadsToI] + addIs [LeadsTo_weaken, Always_LeadsToD]) 1); qed "Always_LeadsTo_weaken"; (** Two theorems for "proof lattices" **) Goal "F : A LeadsTo B ==> F:(A Un B) LeadsTo B"; -by (blast_tac (claset() - addIs [LeadsTo_Un, subset_imp_LeadsTo] - addDs [LeadsToD]) 1); +by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] + addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); qed "LeadsTo_Un_post"; Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \ \ ==> F : (A Un B) LeadsTo C"; by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, LeadsTo_weaken_L, LeadsTo_Trans] - addDs [LeadsToD]) 1); + addDs [LeadsTo_type RS subsetD]) 1); qed "LeadsTo_Trans_Un"; - (** Distributive laws **) - Goal "(F : (A Un B) LeadsTo C) <-> (F : A LeadsTo C & F : B LeadsTo C)"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); qed "LeadsTo_Un_distrib"; -Goal "[| F:program; B:condition |] ==> \ -\ (F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B)"; -by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); +Goal "(F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B) & F:program"; +by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] + addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); qed "LeadsTo_UN_distrib"; -Goal "[| F:program; B:condition |] ==> \ -\ (F : Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B)"; -by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); +Goal "(F:Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B) & F:program"; +by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] + addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); qed "LeadsTo_Union_distrib"; -(** More rules using the premise "Always INV" **) +(** More rules using the premise "Always(I)" **) -Goal "F : A Ensures B ==> F : A LeadsTo B"; -by (asm_full_simp_tac - (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1); -qed "LeadsTo_Basis"; - -Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \ -\ ==> F : A Ensures B"; +Goal "[| F:(A-B) Co (A Un B); F:transient (A-B) |] ==> F : A Ensures B"; by (asm_full_simp_tac (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1); by (blast_tac (claset() addIs [ensuresI, constrains_weaken, @@ -201,150 +188,108 @@ addDs [constrainsD2]) 1); qed "EnsuresI"; -Goal "[| F : Always(INV); \ -\ F : (INV Int (A-A')) Co (A Un A'); \ -\ F : transient (INV Int (A-A')) |] \ +Goal "[| F : Always(I); F : (I Int (A-A')) Co (A Un A'); \ +\ F : transient (I Int (A-A')) |] \ \ ==> F : A LeadsTo A'"; by (rtac Always_LeadsToI 1); by (assume_tac 1); -by (blast_tac (claset() addDs [ConstrainsD]) 2); by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis, Always_ConstrainsD RS Constrains_weaken, - transient_strengthen] - addDs [AlwaysD2, ConstrainsD]) 1); + transient_strengthen]) 1); qed "Always_LeadsTo_Basis"; (*Set difference: maybe combine with leadsTo_weaken_L?? This is the most useful form of the "disjunction" rule*) -Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C; \ -\ A:condition; B:condition |] \ -\ ==> F : A LeadsTo C"; -by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken] - addDs [LeadsToD]) 1); +Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] ==> F : A LeadsTo C"; +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1); qed "LeadsTo_Diff"; - -Goal "[| ALL i:I. F: A(i) LeadsTo A'(i); F:program |] \ +val [major, minor] = Goal +"[|(!!i. i:I ==> F: A(i) LeadsTo A'(i)); F:program |] \ \ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))"; +by (cut_facts_tac [minor] 1); by (rtac LeadsTo_Union 1); by (ALLGOALS(Clarify_tac)); -by (blast_tac (claset() addDs [LeadsToD]) 2); -by (blast_tac (claset() addIs [LeadsTo_weaken_R] - addDs [LeadsToD]) 1); -bind_thm ("LeadsTo_UN_UN", ballI RS result()); - - -(*Version with no index set*) -Goal "[| ALL i. F: A(i) LeadsTo A'(i); F:program |] \ -\ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))"; -by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1); -qed "all_LeadsTo_UN_UN"; - -bind_thm ("LeadsTo_UN_UN_noindex", allI RS all_LeadsTo_UN_UN); +by (forward_tac [major] 1); +by (blast_tac (claset() addIs [LeadsTo_weaken_R]) 1); +qed "LeadsTo_UN_UN"; (*Binary union version*) -Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \ -\ ==> F : (A Un B) LeadsTo (A' Un B')"; -by (blast_tac (claset() - addIs [LeadsTo_Un, LeadsTo_weaken_R] - addDs [LeadsToD]) 1); +Goal "[| F:A LeadsTo A'; F:B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')"; +by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_R]) 1); qed "LeadsTo_Un_Un"; (** The cancellation law **) -Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] \ -\ ==> F : A LeadsTo (A' Un B')"; -by (blast_tac (claset() addIs [LeadsTo_Un_Un, - subset_imp_LeadsTo, LeadsTo_Trans] - addDs [LeadsToD]) 1); +Goal "[| F: A LeadsTo(A' Un B); F: B LeadsTo B' |] ==> F:A LeadsTo (A' Un B')"; +by (blast_tac (claset() addIs [LeadsTo_Un_Un, subset_imp_LeadsTo, LeadsTo_Trans] + addDs [LeadsTo_type RS subsetD]) 1); qed "LeadsTo_cancel2"; Goal "A Un (B - A) = A Un B"; by Auto_tac; qed "Un_Diff"; -Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \ -\ ==> F : A LeadsTo (A' Un B')"; +Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] ==> F : A LeadsTo (A' Un B')"; by (rtac LeadsTo_cancel2 1); by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [Un_Diff]) 1); qed "LeadsTo_cancel_Diff2"; -Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \ -\ ==> F : A LeadsTo (B' Un A')"; +Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] ==> F : A LeadsTo (B' Un A')"; by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); qed "LeadsTo_cancel1"; - Goal "(B - A) Un A = B Un A"; by Auto_tac; qed "Diff_Un2"; -Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \ -\ ==> F : A LeadsTo (B' Un A')"; +Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] ==> F : A LeadsTo (B' Un A')"; by (rtac LeadsTo_cancel1 1); by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [Diff_Un2]) 1); qed "LeadsTo_cancel_Diff1"; - (** The impossibility law **) (*The set "A" may be non-empty, but it contains no reachable states*) Goal "F : A LeadsTo 0 ==> F : Always (state -A)"; by (full_simp_tac (simpset() addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1); -by (Clarify_tac 1); -by (forward_tac [reachableD] 1); -by (auto_tac (claset() addSDs [leadsTo_empty], - simpset() addsimps [condition_def])); +by (cut_facts_tac [reachable_type] 1); +by (auto_tac (claset() addSDs [leadsTo_empty], simpset())); qed "LeadsTo_empty"; (** PSP: Progress-Safety-Progress **) (*Special case of PSP: Misra's "stable conjunction"*) -Goal "[| F : A LeadsTo A'; F : Stable(B) |] \ -\ ==> F : (A Int B) LeadsTo (A' Int B)"; -by (forward_tac [StableD2] 1); -by (rotate_tac ~1 1); -by (asm_full_simp_tac - (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1); +Goal "[| F : A LeadsTo A'; F : Stable(B) |]==> F:(A Int B) LeadsTo (A' Int B)"; +by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); by (Clarify_tac 1); by (dtac psp_stable 1); -by (assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1); +by (REPEAT(asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1)); qed "PSP_Stable"; -Goal "[| F : A LeadsTo A'; F : Stable(B) |] \ -\ ==> F : (B Int A) LeadsTo (B Int A')"; +Goal "[| F : A LeadsTo A'; F : Stable(B) |] ==> F : (B Int A) LeadsTo (B Int A')"; by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1); qed "PSP_Stable2"; -Goal "[| F : A LeadsTo A'; F : B Co B' |] \ -\ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"; -by (full_simp_tac - (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1); +Goal "[| F:A LeadsTo A'; F:B Co B'|]==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"; +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1); by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); qed "PSP"; -Goal "[| F : A LeadsTo A'; F : B Co B' |] \ -\ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"; +Goal "[| F : A LeadsTo A'; F : B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); qed "PSP2"; - Goal -"[| F : A LeadsTo A'; F : B Unless B' |] \ -\ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"; -by (forward_tac [LeadsToD] 1); -by (forward_tac [UnlessD] 1); +"[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"; by (rewrite_goals_tac [Unless_def]); by (dtac PSP 1); by (assume_tac 1); -by (blast_tac (claset() - addIs [LeadsTo_Diff, - LeadsTo_weaken, subset_imp_LeadsTo]) 1); +by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, subset_imp_LeadsTo]) 1); qed "PSP_Unless"; (*** Induction rules ***) @@ -353,27 +298,25 @@ Goal "[| wf(r); \ \ ALL m:I. F : (A Int f-``{m}) LeadsTo \ \ ((A Int f-``(converse(r) `` {m})) Un B); \ -\ field(r)<=I; A<=f-``I; F:program; A:condition; B:condition |] \ +\ field(r)<=I; A<=f-``I; F:program |] \ \ ==> F : A LeadsTo B"; -by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1); +by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by Safe_tac; by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1); by (ALLGOALS(Clarify_tac)); -by (dres_inst_tac [("x", "m")] bspec 4); +by (dres_inst_tac [("x", "m")] bspec 2); by Safe_tac; -by (res_inst_tac [("A'", - "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")] - leadsTo_weaken_R 4); -by (asm_simp_tac (simpset() addsimps [Int_assoc]) 4); -by (asm_simp_tac (simpset() addsimps [Int_assoc]) 5); +by (res_inst_tac +[("A'", "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]leadsTo_weaken_R 2); +by (asm_simp_tac (simpset() addsimps [Int_assoc]) 2); +by (asm_simp_tac (simpset() addsimps [Int_assoc]) 3); by (REPEAT(Blast_tac 1)); qed "LeadsTo_wf_induct"; Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \ -\ A<=f-``nat; F:program; A:condition; B:condition |] \ -\ ==> F : A LeadsTo B"; +\ A<=f-``nat; F:program |] ==> F : A LeadsTo B"; by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_less_than_field]))); @@ -398,20 +341,19 @@ \ F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |] \ \ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"; by (full_simp_tac - (simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains, + (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1); by Safe_tac; by (REPEAT(Blast_tac 2)); by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1); qed "Completion"; - -Goal "[| I:Fin(X);F:program; C:condition |] \ +Goal "[| I:Fin(X);F:program |] \ \ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \ \ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \ \ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; by (etac Fin_induct 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [Inter_0])); by (case_tac "y=0" 1); by Auto_tac; by (etac not_emptyE 1); @@ -421,17 +363,15 @@ by (Asm_simp_tac 1); by (rtac Completion 1); by (subgoal_tac "Inter(RepFun(y, A')) Un C = (INT x:RepFun(y, A'). x Un C)" 4); -by (Blast_tac 5); by (Asm_simp_tac 4); by (rtac Constrains_INT 4); by (REPEAT(Blast_tac 1)); val lemma = result(); - val prems = Goal "[| I:Fin(X); !!i. i:I ==> F : A(i) LeadsTo (A'(i) Un C); \ \ !!i. i:I ==> F : A'(i) Co (A'(i) Un C); \ -\ F:program; C:condition |] \ +\ F:program |] \ \ ==> F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); qed "Finite_completion"; @@ -441,22 +381,20 @@ \ F : B LeadsTo B'; F : Stable(B') |] \ \ ==> F : (A Int B) LeadsTo (A' Int B')"; by (res_inst_tac [("C1", "0")] (Completion RS LeadsTo_weaken_R) 1); -by (REPEAT(blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 5)); -by (ALLGOALS(Asm_full_simp_tac)); +by (Asm_full_simp_tac 5); +by (rtac subset_refl 5); +by Auto_tac; qed "Stable_completion"; - val prems = Goalw [Stable_def] "[| I:Fin(X); \ -\ ALL i:I. F : A(i) LeadsTo A'(i); \ -\ ALL i:I. F: Stable(A'(i)); F:program |] \ +\ (!!i. i:I ==> F : A(i) LeadsTo A'(i)); \ +\ (!!i. i:I ==>F: Stable(A'(i))); F:program |] \ \ ==> F : (INT i:I. A(i)) LeadsTo (INT i:I. A'(i))"; -by (subgoal_tac "(INT i:I. A'(i)):condition" 1); -by (blast_tac (claset() addDs [LeadsToD,ConstrainsD]) 2); by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1); -by (assume_tac 7); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS (Blast_tac)); +by (ALLGOALS(Simp_tac)); +by (rtac subset_refl 5); +by (REPEAT(blast_tac (claset() addIs prems) 1)); qed "Finite_stable_completion"; @@ -481,6 +419,7 @@ constrains_tac 1, ALLGOALS Clarify_tac, ALLGOALS (asm_full_simp_tac - (simpset() addsimps [condition_def])), - ALLGOALS Clarify_tac]); + (simpset() addsimps [st_set_def])), + ALLGOALS Clarify_tac, + ALLGOALS (Asm_full_simp_tac)]); diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/SubstAx.thy Thu Nov 15 15:07:16 2001 +0100 @@ -11,13 +11,12 @@ SubstAx = WFair + Constrains + constdefs + (* The definitions below are not `conventional', but yields simpler rules *) Ensures :: "[i,i] => i" (infixl 60) - "A Ensures B == {F:program. F : (reachable(F) Int A) ensures B & - A:condition & B:condition}" + "A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }" - LeadsTo :: "[i, i] => i" (infixl 60) - "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo B & - A:condition & B:condition}" + LeadsTo :: "[i, i] => i" (infixl 60) + "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo (reachable(F) Int B)}" syntax (xsymbols) "op LeadsTo" :: "[i, i] => i" (infixl " \\w " 60) diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/UNITY.ML --- a/src/ZF/UNITY/UNITY.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/UNITY.ML Thu Nov 15 15:07:16 2001 +0100 @@ -10,12 +10,12 @@ *) (** SKIP **) -Goal "SKIP:program"; -by (auto_tac (claset(), simpset() addsimps - [SKIP_def, program_def, mk_program_def, actionSet_def, cons_absorb])); -qed "SKIP_type"; -AddIffs [SKIP_type]; -AddTCs [SKIP_type]; +Goalw [SKIP_def] "SKIP:program"; +by (rewrite_goal_tac [program_def, mk_program_def] 1); +by Auto_tac; +qed "SKIP_in_program"; +AddIffs [SKIP_in_program]; +AddTCs [SKIP_in_program]; (** programify: coersion from anything to program **) @@ -37,288 +37,253 @@ "programify(programify(F))=programify(F)"; by Auto_tac; qed "programify_idem"; -Addsimps [programify_idem]; +AddIffs [programify_idem]; Goal "Init(programify(F)) = Init(F)"; by (simp_tac (simpset() addsimps [Init_def]) 1); qed "Init_programify"; +AddIffs [Init_programify]; Goal "Acts(programify(F)) = Acts(F)"; by (simp_tac (simpset() addsimps [Acts_def]) 1); qed "Acts_programify"; +AddIffs [Acts_programify]; Goal "AllowedActs(programify(F)) = AllowedActs(F)"; by (simp_tac (simpset() addsimps [AllowedActs_def]) 1); qed "AllowedActs_programify"; - -Addsimps [Init_programify,Acts_programify,AllowedActs_programify]; +AddIffs [AllowedActs_programify]; -(** program inspectors **) +(** program's inspectors **) -Goal "F:program ==>Id:RawActs(F)"; +Goal "F:program ==>id(state):RawActs(F)"; by (auto_tac (claset(), simpset() addsimps [program_def, RawActs_def])); -qed "Id_in_RawActs"; +qed "id_in_RawActs"; -Goal "Id:Acts(F)"; +Goal "id(state):Acts(F)"; by (simp_tac (simpset() - addsimps [Id_in_RawActs, Acts_def]) 1); -qed "Id_in_Acts"; + addsimps [id_in_RawActs, Acts_def]) 1); +qed "id_in_Acts"; -Goal "F:program ==>Id:RawAllowedActs(F)"; +Goal "F:program ==>id(state):RawAllowedActs(F)"; by (auto_tac (claset(), simpset() addsimps [program_def, RawAllowedActs_def])); -qed "Id_in_RawAllowedActs"; +qed "id_in_RawAllowedActs"; -Goal "Id:AllowedActs(F)"; +Goal "id(state):AllowedActs(F)"; by (simp_tac (simpset() - addsimps [Id_in_RawAllowedActs, AllowedActs_def]) 1); -qed "Id_in_AllowedActs"; + addsimps [id_in_RawAllowedActs, AllowedActs_def]) 1); +qed "id_in_AllowedActs"; -AddIffs [Id_in_Acts, Id_in_AllowedActs]; -AddTCs [Id_in_Acts, Id_in_AllowedActs]; +AddIffs [id_in_Acts, id_in_AllowedActs]; +AddTCs [id_in_Acts, id_in_AllowedActs]; -Goal "cons(Id, Acts(F)) = Acts(F)"; +Goal "cons(id(state), Acts(F)) = Acts(F)"; by (simp_tac (simpset() addsimps [cons_absorb]) 1); -qed "cons_Id_Acts"; +qed "cons_id_Acts"; -Goal "cons(Id, AllowedActs(F)) = AllowedActs(F)"; +Goal "cons(id(state), AllowedActs(F)) = AllowedActs(F)"; by (simp_tac (simpset() addsimps [cons_absorb]) 1); -qed "cons_Id_AllowedActs"; +qed "cons_id_AllowedActs"; -Addsimps [cons_Id_Acts, cons_Id_AllowedActs]; +AddIffs [cons_id_Acts, cons_id_AllowedActs]; (** inspectors's types **) Goal -"F:program ==> RawInit(F):condition"; +"F:program ==> RawInit(F)<=state"; by (auto_tac (claset(), simpset() addsimps [program_def, RawInit_def])); qed "RawInit_type"; -Goal "Init(F):condition"; +Goal +"F:program ==> RawActs(F)<=Pow(state*state)"; +by (auto_tac (claset(), simpset() + addsimps [program_def, RawActs_def])); +qed "RawActs_type"; + +Goal +"F:program ==> RawAllowedActs(F)<=Pow(state*state)"; +by (auto_tac (claset(), simpset() + addsimps [program_def, RawAllowedActs_def])); +qed "RawAllowedActs_type"; + +Goal "Init(F)<=state"; by (simp_tac (simpset() addsimps [RawInit_type, Init_def]) 1); qed "Init_type"; -Goal -"F:program ==> RawActs(F):actionSet"; -by (auto_tac (claset(), simpset() - addsimps [program_def, RawActs_def, actionSet_def])); -qed "RawActs_type"; +Goalw [st_set_def] "st_set(Init(F))"; +by (resolve_tac [Init_type] 1); +qed "st_set_Init"; +AddIffs [st_set_Init]; Goal -"Acts(F):actionSet"; +"Acts(F)<=Pow(state*state)"; by (simp_tac (simpset() addsimps [RawActs_type, Acts_def]) 1); qed "Acts_type"; Goal -"F:program ==> RawAllowedActs(F):actionSet"; -by (auto_tac (claset(), simpset() - addsimps [program_def, RawAllowedActs_def, actionSet_def])); -qed "RawAllowedActs_type"; - -Goal -"AllowedActs(F): actionSet"; +"AllowedActs(F)<=Pow(state*state)"; by (simp_tac (simpset() addsimps [RawAllowedActs_type, AllowedActs_def]) 1); qed "AllowedActs_type"; -AddIffs [Init_type, Acts_type, AllowedActs_type]; -AddTCs [Init_type, Acts_type, AllowedActs_type]; - -Goal "x:Init(F) ==> x:state"; -by (cut_inst_tac [("F", "F")] Init_type 1); -by (auto_tac (claset(), simpset() addsimps [condition_def])); -qed "InitD"; - -Goal "act:Acts(F) ==> act<=state*state"; -by (cut_inst_tac [("F", "F")] Acts_type 1); -by (rewrite_goals_tac [actionSet_def]); -by Auto_tac; -qed "ActsD"; - - -Goal "act:AllowedActs(F) ==> act<=state*state"; -by (cut_inst_tac [("F", "F")] AllowedActs_type 1); -by (rewrite_goals_tac [actionSet_def]); -by Auto_tac; -qed "AllowedActsD"; - (** More simplification rules involving state and Init, Acts, and AllowedActs **) Goal "state <= Init(F) <-> Init(F)=state"; by (cut_inst_tac [("F", "F")] Init_type 1); -by (auto_tac (claset(), - simpset() addsimps [condition_def])); -qed "Init_state_eq"; +by Auto_tac; +qed "state_subset_is_Init_iff"; +AddIffs [state_subset_is_Init_iff]; -Goal "action <= Acts(F) <-> Acts(F)=action"; +Goal "Pow(state*state) <= Acts(F) <-> Acts(F)=Pow(state*state)"; by (cut_inst_tac [("F", "F")] Acts_type 1); -by (auto_tac (claset(), - simpset() addsimps [actionSet_def])); -qed "Acts_action_eq"; +by Auto_tac; +qed "Pow_state_times_state_is_subset_Acts_iff"; +AddIffs [Pow_state_times_state_is_subset_Acts_iff]; -Goal "action <= AllowedActs(F) <-> AllowedActs(F)=action"; +Goal "Pow(state*state) <= AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)"; by (cut_inst_tac [("F", "F")] AllowedActs_type 1); -by (auto_tac (claset(), - simpset() addsimps [actionSet_def])); -qed "AllowedActs_action_eq"; +by Auto_tac; +qed "Pow_state_times_state_is_subset_AllowedActs_iff"; +AddIffs [Pow_state_times_state_is_subset_AllowedActs_iff]; (** Eliminating `Int state' from expressions **) -Goal -"Init(F) Int state = Init(F)"; +Goal "Init(F) Int state = Init(F)"; by (cut_inst_tac [("F", "F")] Init_type 1); -by (auto_tac (claset(), - simpset() addsimps [condition_def])); +by (Blast_tac 1); qed "Init_Int_state"; +AddIffs [Init_Int_state]; -Goal -"state Int Init(F) = Init(F)"; -by (stac (Int_commute) 1); -by (simp_tac (simpset() - addsimps [Init_Int_state]) 1); -qed "Init_Int_state2"; +Goal "state Int Init(F) = Init(F)"; +by (cut_inst_tac [("F", "F")] Init_type 1); +by (Blast_tac 1); +qed "state_Int_Init"; +AddIffs [state_Int_Init]; -Goal -"Acts(F) Int action = Acts(F)"; +Goal "Acts(F) Int Pow(state*state) = Acts(F)"; by (cut_inst_tac [("F", "F")] Acts_type 1); -by (auto_tac (claset(), - simpset() addsimps [actionSet_def])); -qed "Acts_Int_action"; +by (Blast_tac 1); +qed "Acts_Int_Pow_state_times_state"; +AddIffs [Acts_Int_Pow_state_times_state]; -Goal -"action Int Acts(F) = Acts(F)"; -by (simp_tac (simpset() addsimps - [Int_commute, Acts_Int_action]) 1); -qed "Acts_Int_action2"; +Goal "Pow(state*state) Int Acts(F) = Acts(F)"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (Blast_tac 1); +qed "state_times_state_Int_Acts"; +AddIffs [state_times_state_Int_Acts]; -Goal -"AllowedActs(F) Int action = AllowedActs(F)"; +Goal "AllowedActs(F) Int Pow(state*state) = AllowedActs(F)"; by (cut_inst_tac [("F", "F")] AllowedActs_type 1); -by (auto_tac (claset(), - simpset() addsimps [actionSet_def])); -qed "AllowedActs_Int_action"; +by (Blast_tac 1); +qed "AllowedActs_Int_Pow_state_times_state"; +AddIffs [AllowedActs_Int_Pow_state_times_state]; -Goal -"action Int AllowedActs(F) = AllowedActs(F)"; -by (simp_tac (simpset() addsimps - [Int_commute, AllowedActs_Int_action]) 1); -qed "AllowedActs_Int_action2"; - -Addsimps -[Init_state_eq, Acts_action_eq, AllowedActs_action_eq, - Init_Int_state, Init_Int_state2, Acts_Int_action, Acts_Int_action2, - AllowedActs_Int_action,AllowedActs_Int_action2]; +Goal "Pow(state*state) Int AllowedActs(F) = AllowedActs(F)"; +by (cut_inst_tac [("F", "F")] AllowedActs_type 1); +by (Blast_tac 1); +qed "state_times_state_Int_AllowedActs"; +AddIffs [state_times_state_Int_AllowedActs]; (** mk_program **) -Goal "mk_program(init, acts, allowed):program"; -by (auto_tac (claset(), simpset() - addsimps [program_def, mk_program_def, condition_def, actionSet_def])); -qed "mk_program_type"; -AddIffs [mk_program_type]; -AddTCs [mk_program_type]; +Goalw [mk_program_def, program_def] "mk_program(init, acts, allowed):program"; +by Auto_tac; +qed "mk_program_in_program"; +AddIffs [mk_program_in_program]; +AddTCs [mk_program_in_program]; -Goal "RawInit(mk_program(init, acts, allowed)) = init Int state"; -by (auto_tac (claset(), simpset() - addsimps [RawInit_def, mk_program_def])); +Goalw [RawInit_def, mk_program_def] + "RawInit(mk_program(init, acts, allowed)) = init Int state"; +by Auto_tac; qed "RawInit_eq"; +AddIffs [RawInit_eq]; -Goal "Init(mk_program(init, acts, allowed)) = init Int state"; -by (auto_tac (claset(), simpset() - addsimps [Init_def, RawInit_eq])); -qed "Init_eq"; -Addsimps [Init_eq]; +Goalw [RawActs_def, mk_program_def] +"RawActs(mk_program(init, acts, allowed)) = cons(id(state), acts Int Pow(state*state))"; +by Auto_tac; +qed "RawActs_eq"; +AddIffs [RawActs_eq]; -Goalw [RawActs_def] -"RawActs(mk_program(init, acts, allowed)) \ -\ = cons(Id, acts Int Pow(state*state))"; -by (auto_tac (claset(), simpset() - addsimps [mk_program_def])); -qed "RawActs_eq"; +Goalw [RawAllowedActs_def, mk_program_def] +"RawAllowedActs(mk_program(init, acts, allowed)) = \ +\ cons(id(state), allowed Int Pow(state*state))"; +by Auto_tac; +qed "RawAllowedActs_eq"; +AddIffs [RawAllowedActs_eq]; -Goalw [Acts_def] -"Acts(mk_program(init, acts, allowed)) \ - \ = cons(Id, acts Int Pow(state*state))"; -by (auto_tac (claset(), - simpset() addsimps [RawActs_eq])); +Goalw [Init_def] "Init(mk_program(init, acts, allowed)) = init Int state"; +by (Simp_tac 1); +qed "Init_eq"; +AddIffs [Init_eq]; + +Goalw [Acts_def] +"Acts(mk_program(init, acts, allowed)) = cons(id(state), acts Int Pow(state*state))"; +by (Simp_tac 1); qed "Acts_eq"; -Addsimps [Acts_eq]; - -Goalw [RawAllowedActs_def] -"RawAllowedActs(mk_program(init, acts, allowed)) \ -\ = cons(Id, allowed Int action)"; -by (auto_tac (claset(), - simpset() addsimps [mk_program_def])); -qed "RawAllowedActs_eq"; +AddIffs [Acts_eq]; Goalw [AllowedActs_def] -"AllowedActs(mk_program(init, acts, allowed)) \ -\ = cons(Id, allowed Int action)"; -by (auto_tac (claset(), - simpset() addsimps [RawAllowedActs_eq])); +"AllowedActs(mk_program(init, acts, allowed))= \ +\ cons(id(state), allowed Int Pow(state*state))"; +by (Simp_tac 1); qed "AllowedActs_eq"; -Addsimps [AllowedActs_eq]; - +AddIffs [AllowedActs_eq]; (**Init, Acts, and AlowedActs of SKIP **) -Goal "RawInit(SKIP) = state"; -by (auto_tac (claset(), simpset() - addsimps [SKIP_def, RawInit_eq])); +Goalw [SKIP_def] "RawInit(SKIP) = state"; +by Auto_tac; qed "RawInit_SKIP"; +AddIffs [RawInit_SKIP]; -Goal "Init(SKIP) = state"; -by (simp_tac (simpset() - addsimps [Init_def, RawInit_SKIP]) 1); -qed "Init_SKIP"; -Addsimps [Init_SKIP]; +Goalw [SKIP_def] "RawAllowedActs(SKIP) = Pow(state*state)"; +by Auto_tac; +qed "RawAllowedActs_SKIP"; +AddIffs [RawAllowedActs_SKIP]; -Goal "RawActs(SKIP) = {Id}"; -by (auto_tac (claset(), simpset() - addsimps [SKIP_def, RawActs_eq])); +Goalw [SKIP_def] "RawActs(SKIP) = {id(state)}"; +by Auto_tac; qed "RawActs_SKIP"; - +AddIffs [RawActs_SKIP]; -Goal "Acts(SKIP) = {Id}"; -by (simp_tac (simpset() - addsimps [Acts_def, RawActs_SKIP]) 1); -qed "Acts_SKIP"; -Addsimps [Acts_SKIP]; +Goalw [Init_def] "Init(SKIP) = state"; +by Auto_tac; +qed "Init_SKIP"; +AddIffs [Init_SKIP]; -Goal "RawAllowedActs(SKIP) = action"; -by (auto_tac (claset(), simpset() - addsimps [SKIP_def, RawAllowedActs_eq])); -qed "RawAllowedActs_SKIP"; +Goalw [Acts_def] "Acts(SKIP) = {id(state)}"; +by Auto_tac; +qed "Acts_SKIP"; +AddIffs [Acts_SKIP]; -Goal "AllowedActs(SKIP) = action"; -by (simp_tac (simpset() - addsimps [AllowedActs_def, RawAllowedActs_SKIP]) 1); +Goalw [AllowedActs_def] "AllowedActs(SKIP) = Pow(state*state)"; +by Auto_tac; qed "AllowedActs_SKIP"; -Addsimps [AllowedActs_SKIP]; +AddIffs [AllowedActs_SKIP]; -(** Equality for UNITY programs **) +(** Equality of UNITY programs **) Goal "F:program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"; -by (auto_tac (claset(), simpset() addsimps - [program_def, mk_program_def, RawInit_def, - RawActs_def, RawAllowedActs_def, actionSet_def, condition_def])); +by (rewrite_goal_tac [program_def, mk_program_def,RawInit_def, + RawActs_def, RawAllowedActs_def] 1); +by Auto_tac; by (REPEAT(Blast_tac 1)); qed "raw_surjective_mk_program"; +Addsimps [raw_surjective_mk_program]; -Goal +Goalw [Init_def, Acts_def, AllowedActs_def] "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"; -by (auto_tac (claset(), simpset() addsimps - [Init_def, Acts_def, AllowedActs_def, - raw_surjective_mk_program])); +by Auto_tac; qed "surjective_mk_program"; - +AddIffs [surjective_mk_program]; Goal "[|Init(F) = Init(G); Acts(F) = Acts(G); \ \ AllowedActs(F) = AllowedActs(G); F:program; G:program |] ==> F = G"; @@ -344,8 +309,6 @@ by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1); qed "program_equality_iff"; -Addsimps [surjective_mk_program]; - (*** These rules allow "lazy" definition expansion ...skipping 1 line @@ -357,20 +320,22 @@ qed "def_prg_Init"; -Goal "F == mk_program (init,acts,allowed) ==> Acts(F) = cons(Id, acts Int action)"; +Goal "F == mk_program (init,acts,allowed) ==> \ +\ Acts(F) = cons(id(state), acts Int Pow(state*state))"; by Auto_tac; qed "def_prg_Acts"; Goal "F == mk_program (init,acts,allowed) ==> \ -\ AllowedActs(F) = cons(Id, allowed Int action)"; +\ AllowedActs(F) = cons(id(state), allowed Int Pow(state*state))"; by Auto_tac; qed "def_prg_AllowedActs"; val [rew] = goal thy "[| F == mk_program (init,acts,allowed) |] \ -\ ==> Init(F) = init Int state & Acts(F) = cons(Id, acts Int action)"; +\ ==> Init(F) = init Int state & Acts(F) = cons(id(state), acts Int Pow(state*state)) & \ +\ AllowedActs(F) = cons(id(state), allowed Int Pow(state*state)) "; by (rewtac rew); by Auto_tac; qed "def_prg_simps"; @@ -393,9 +358,18 @@ (*** co ***) +Goalw [constrains_def] +"A co B <= program"; +by Auto_tac; +qed "constrains_type"; + + val prems = Goalw [constrains_def] "[|(!!act s s'. [| act: Acts(F); :act; s:A|] ==> s':A'); \ - \ F:program; A:condition; A':condition |] ==> F:A co A'"; + \ F:program; st_set(A) |] ==> F:A co A'"; +by (auto_tac (claset() delrules [subsetI], simpset())); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems))); +by (Clarify_tac 1); by (blast_tac(claset() addIs prems) 1); qed "constrainsI"; @@ -405,184 +379,169 @@ qed "constrainsD"; Goalw [constrains_def] - "F:A co B ==> F:program & A:condition & B:condition"; + "F:A co B ==> F:program & st_set(A)"; by (Blast_tac 1); -qed "constrainsD2"; +qed "constrainsD2"; -Goalw [constrains_def] - "[| F:program; B:condition |] ==> F : 0 co B"; +Goalw [constrains_def, st_set_def] "F : 0 co B <-> F:program"; by (Blast_tac 1); qed "constrains_empty"; -Goalw [constrains_def] - "[| F:program; A:condition |] ==>(F : A co 0) <-> (A=0)"; -by (auto_tac (claset() addSDs [bspec], - simpset() addsimps [condition_def])); +Goalw [constrains_def, st_set_def] + "(F : A co 0) <-> (A=0 & F:program)"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by Auto_tac; +by (Blast_tac 1); qed "constrains_empty2"; -Goalw [constrains_def] -"[| F:program; B:condition |] ==> (F: state co B) <-> (B = state)"; -by (auto_tac (claset() addSDs [bspec] addDs [ActsD], - simpset() addsimps [condition_def])); +Goalw [constrains_def, st_set_def] +"(F: state co B) <-> (state<=B & F:program)"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (Blast_tac 1); qed "constrains_state"; - -Goalw [constrains_def] - "[| F:program; A:condition |] ==> F : A co state"; -by (auto_tac (claset() addDs [ActsD], simpset())); +Goalw [constrains_def, st_set_def] "F:A co state <-> (F:program & st_set(A))"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (Blast_tac 1); qed "constrains_state2"; -Addsimps [constrains_empty, constrains_empty2, +AddIffs [constrains_empty, constrains_empty2, constrains_state, constrains_state2]; (*monotonic in 2nd argument*) Goalw [constrains_def] - "[| F:A co A'; A'<=B'; B':condition |] ==> F : A co B'"; + "[| F:A co A'; A'<=B' |] ==> F : A co B'"; by (Blast_tac 1); qed "constrains_weaken_R"; (*anti-monotonic in 1st argument*) -Goalw [constrains_def, condition_def] +Goalw [constrains_def, st_set_def] "[| F : A co A'; B<=A |] ==> F : B co A'"; by (Blast_tac 1); qed "constrains_weaken_L"; Goal - "[| F : A co A'; B<=A; A'<=B'; B':condition |] ==> F : B co B'"; + "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"; by (dtac constrains_weaken_R 1); -by (dtac constrains_weaken_L 3); +by (dtac constrains_weaken_L 2); by (REPEAT(Blast_tac 1)); qed "constrains_weaken"; (** Union **) -Goalw [constrains_def] - "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')"; -by (Asm_full_simp_tac 1); -by (Blast_tac 1); -qed "constrains_Un"; - -Goalw [constrains_def] +Goalw [constrains_def, st_set_def] "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')"; by Auto_tac; -by (asm_full_simp_tac - (simpset() addsimps [condition_def]) 1); -by (Blast_tac 1); +by (Force_tac 1); qed "constrains_Un"; -Goalw [constrains_def] - "[| ALL i:I. F:A(i) co A'(i); F:program |] ==> \ -\ F:(UN i:I. A(i)) co (UN i:I. A'(i))"; -by (Clarify_tac 1); -by (Blast_tac 1); -bind_thm ("constrains_UN", ballI RS result()); +val major::minor::_ = Goalw [constrains_def, st_set_def] +"[|(!!i. i:I ==> F:A(i) co A'(i)); F:program |]==> F:(UN i:I. A(i)) co (UN i:I. A'(i))"; +by (cut_facts_tac [minor] 1); +by Safe_tac; +by (ALLGOALS(forward_tac [major])); +by (ALLGOALS(Asm_full_simp_tac)); +by (REPEAT(Blast_tac 1)); +qed "constrains_UN"; - -Goalw [constrains_def] +Goalw [constrains_def, st_set_def] "(A Un B) co C = (A co C) Int (B co C)"; -by (rtac equalityI 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(Blast_tac)); +by Auto_tac; +by (Force_tac 1); qed "constrains_Un_distrib"; +Goalw [constrains_def, st_set_def] + "i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)"; +by (rtac equalityI 1); +by (REPEAT(Force_tac 1)); +qed "constrains_UN_distrib"; -Goalw [constrains_def] - "i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)"; +(** Intersection **) +Goalw [constrains_def, st_set_def] + "C co (A Int B) = (C co A) Int (C co B)"; +by (rtac equalityI 1); +by (ALLGOALS(Clarify_tac)); (* to speed up the proof *) +by (REPEAT(Blast_tac 1)); +qed "constrains_Int_distrib"; + +Goalw [constrains_def, st_set_def] +"x:I ==> A co (INT i:I. B(i)) = (INT i:I. A co B(i))"; by (rtac equalityI 1); by Safe_tac; -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(Blast_tac)); -qed "constrains_UN_distrib"; - -Goalw [constrains_def] - "[| A:condition; B:condition |] \ -\ ==> C co (A Int B) = (C co A) Int (C co B)"; -by (rtac equalityI 1); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(Blast_tac)); -qed "constrains_Int_distrib"; - -Goalw [constrains_def] "[| i:I; ALL i:I. B(i):condition |] ==> \ -\ A co (INT i:I. B(i)) = (INT i:I. A co B(i))"; -by (rtac equalityI 1); -by Safe_tac; -by (ALLGOALS(Blast_tac)); +by (REPEAT(Blast_tac 1)); qed "constrains_INT_distrib"; -(** Intersection **) - -Goalw [constrains_def] +Goalw [constrains_def, st_set_def] "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"; by (Clarify_tac 1); by (Blast_tac 1); qed "constrains_Int"; -Goalw [constrains_def] - "[| ALL i:I. F : A(i) co A'(i); F:program |] \ -\ ==> F : (INT i:I. A(i)) co (INT i:I. A'(i))"; +val major::minor::_ = Goalw [constrains_def, st_set_def] +"[| (!!i. i:I==>F:A(i) co A'(i)); F:program|]==> F:(INT i:I. A(i)) co (INT i:I. A'(i))"; +by (cut_facts_tac [minor] 1); +by (cut_inst_tac [("F", "F")] Acts_type 1); by (case_tac "I=0" 1); by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1); by (etac not_emptyE 1); -by Safe_tac; -by (dres_inst_tac [("x", "xd")] bspec 1); -by (ALLGOALS(Blast_tac)); -bind_thm ("constrains_INT", ballI RS result()); - - -(* This rule simulates the HOL's one for (INT z. A i) co (INT z. B i) *) +by Safe_tac; +by (forw_inst_tac [("i", "xd")] major 1); +by (forward_tac [major] 2); +by (forward_tac [major] 3); +by (REPEAT(Force_tac 1)); +qed "constrains_INT"; -Goalw [constrains_def, condition_def] - "[| ALL z. F: {s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |] ==> \ -\ F: {s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}"; -by (auto_tac (claset() addSDs [bspec] addDs [ActsD], - simpset() addsimps [condition_def])); +(* The rule below simulates the HOL's one for (INT z. A i) co (INT z. B i) *) +Goalw [constrains_def] +"[| ALL z. F:{s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |]==>\ +\ F:{s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}"; by (Blast_tac 1); -bind_thm ("constrains_All", allI RS result()); +qed "constrains_All"; -Goalw [constrains_def] - "F : A co A' ==> A <= A'"; -by (auto_tac (claset() addSDs [bspec], simpset())); +Goalw [constrains_def, st_set_def] + "[| F:A co A' |] ==> A <= A'"; +by Auto_tac; +by (Blast_tac 1); qed "constrains_imp_subset"; - (*The reasoning is by subsets since "co" refers to single actions only. So this rule isn't that useful.*) -Goalw [constrains_def] +Goalw [constrains_def, st_set_def] "[| F : A co B; F : B co C |] ==> F : A co C"; by Auto_tac; -by (dres_inst_tac [("x", "act")] bspec 1); -by (dres_inst_tac [("x", "Id")] bspec 2); -by (auto_tac (claset() addDs [ActsD], - simpset() addsimps [condition_def])); +by (Blast_tac 1); qed "constrains_trans"; -Goalw [constrains_def] - "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"; -by Auto_tac; -by (dres_inst_tac [("x", "Id")] bspec 1); -by (dres_inst_tac [("x", "act")] bspec 2); -by (auto_tac (claset(), simpset() addsimps [condition_def])); +Goal +"[| F : A co (A' Un B); F : B co B' |] ==> F:A co (A' Un B')"; +by (dres_inst_tac [("A", "B")] constrains_imp_subset 1); +by (blast_tac (claset() addIs [constrains_weaken_R]) 1); qed "constrains_cancel"; (*** unless ***) -Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B"; -by (assume_tac 1); +Goalw [unless_def, constrains_def] + "A unless B <= program"; +by Auto_tac; +qed "unless_type"; + +Goalw [unless_def] "[| F:(A-B) co (A Un B) |] ==> F : A unless B"; +by (blast_tac (claset() addDs [constrainsD2]) 1); qed "unlessI"; Goalw [unless_def] "F :A unless B ==> F : (A-B) co (A Un B)"; -by (assume_tac 1); +by Auto_tac; qed "unlessD"; -Goalw [unless_def, constrains_def] - "F: A unless B ==> F:program & A:condition & B:condition"; -by Auto_tac; -qed "unlessD2"; - (*** initially ***) Goalw [initially_def] -"[| Init(F)<=A; F:program; A:condition |] ==> F:initially(A)"; +"initially(A) <= program"; +by (Blast_tac 1); +qed "initially_type"; + +Goalw [initially_def] +"[| F:program; Init(F)<=A |] ==> F:initially(A)"; by (Blast_tac 1); qed "initiallyI"; @@ -591,42 +550,40 @@ by (Blast_tac 1); qed "initiallyD"; -Goalw [initially_def] -"F:initially(A) ==> F:program & A:condition"; +(*** stable ***) + +Goalw [stable_def, constrains_def] + "stable(A)<=program"; by (Blast_tac 1); -qed "initiallyD2"; - -(*** stable ***) +qed "stable_type"; Goalw [stable_def] "F : A co A ==> F : stable(A)"; by (assume_tac 1); qed "stableI"; -Goalw [stable_def] "F : stable(A) ==> F : A co A"; +Goalw [stable_def] "F:stable(A) ==> F : A co A"; by (assume_tac 1); qed "stableD"; -Goalw [stable_def, constrains_def] - "F:stable(A)==> F:program & A:condition"; -by (Blast_tac 1); +Goalw [stable_def, constrains_def] "F:stable(A) ==> F:program & st_set(A)"; +by Auto_tac; qed "stableD2"; -Goalw [stable_def, constrains_def] - "stable(state) = program"; -by (auto_tac (claset() addDs [ActsD], simpset())); +Goalw [stable_def, constrains_def] "stable(state) = program"; +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "stable_state"; -Addsimps [stable_state]; +AddIffs [stable_state]; (** Union **) Goalw [stable_def] - "[| F : stable(A); F : stable(A') |] ==> F : stable(A Un A')"; + "[| F : stable(A); F:stable(A') |] ==> F : stable(A Un A')"; by (blast_tac (claset() addIs [constrains_Un]) 1); qed "stable_Un"; val [major, minor] = Goalw [stable_def] - "[| (!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))"; +"[|(!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))"; by (cut_facts_tac [minor] 1); by (blast_tac (claset() addIs [constrains_UN, major]) 1); qed "stable_UN"; @@ -637,156 +594,169 @@ qed "stable_Int"; val [major, minor] = Goalw [stable_def] - "[| (!!i. i:I ==> F : stable(A(i))); F:program |] \ -\ ==> F : stable (INT i:I. A(i))"; +"[| (!!i. i:I ==> F:stable(A(i))); F:program |] ==> F : stable (INT i:I. A(i))"; by (cut_facts_tac [minor] 1); by (blast_tac (claset() addIs [constrains_INT, major]) 1); qed "stable_INT"; Goalw [stable_def] - "[| ALL z. F: stable({s:state. P(s, z)}); F:program |] ==> \ -\ F: stable({s:state. ALL z. P(s, z)})"; +"[|ALL z. F:stable({s:state. P(s, z)}); F:program|]==>F:stable({s:state. ALL z. P(s, z)})"; by (rtac constrains_All 1); by Auto_tac; -bind_thm("stable_All", allI RS result()); - +qed "stable_All"; -Goalw [stable_def, constrains_def] - "[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; -by (Clarify_tac 1); -by (Blast_tac 1); +Goalw [stable_def, constrains_def, st_set_def] +"[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; +by (cut_inst_tac [("F", "F")] Acts_type 1); +by Auto_tac; +by (Force_tac 1); qed "stable_constrains_Un"; - -Goalw [stable_def, constrains_def] +Goalw [stable_def, constrains_def, st_set_def] "[| F : stable(C); F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"; by (Clarify_tac 1); by (Blast_tac 1); qed "stable_constrains_Int"; -(*[| F : stable(C); F : (C Int A) co A |] ==> F : stable (C Int A) *) +(* [| F:stable(C); F :(C Int A) co A |] ==> F:stable(C Int A) *) bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); (** invariant **) -Goalw [invariant_def, initially_def] -"invariant(A) = initially(A) Int stable(A)"; -by (blast_tac (claset() addDs [stableD2]) 1); -qed "invariant_eq"; +Goalw [invariant_def] + "invariant(A) <= program"; +by (blast_tac (claset() addDs [stable_type RS subsetD]) 1); +qed "invariant_type"; -val invariant_def2 = invariant_eq RS eq_reflection; - -Goalw [invariant_def] +Goalw [invariant_def, initially_def] "[| Init(F)<=A; F:stable(A) |] ==> F : invariant(A)"; -by (blast_tac (claset() addDs [stableD2]) 1); +by (forward_tac [stable_type RS subsetD] 1); +by Auto_tac; qed "invariantI"; -Goalw [invariant_def] +Goalw [invariant_def, initially_def] "F:invariant(A) ==> Init(F)<=A & F:stable(A)"; by Auto_tac; qed "invariantD"; -Goalw [invariant_def] - "F:invariant(A) ==> F:program & A:condition"; +Goalw [invariant_def] + "F:invariant(A) ==> F:program & st_set(A)"; by (blast_tac (claset() addDs [stableD2]) 1); qed "invariantD2"; (*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) -Goalw [invariant_def] +Goalw [invariant_def, initially_def] "[| F : invariant(A); F : invariant(B) |] ==> F : invariant(A Int B)"; by (asm_full_simp_tac (simpset() addsimps [stable_Int]) 1); by (Blast_tac 1); qed "invariant_Int"; (** The Elimination Theorem. The "free" m has become universally quantified! - Should the premise be !!m instead of ALL m ? Would make it harder to use - in forward proof. **) + Should the premise be !!m instead of ALL m ? Would make it harder + to use in forward proof. **) -Goalw [constrains_def] - "[| ALL m:M. F : {s:S. x(s) = m} co B(m); F:program |] \ -\ ==> F:{s:S. x(s):M} co (UN m:M. B(m))"; +(* The general case easier to prove that le special case! *) +Goalw [constrains_def, st_set_def] + "[| ALL m:M. F : {s:A. x(s) = m} co B(m); F:program |] \ +\ ==> F:{s:A. x(s):M} co (UN m:M. B(m))"; by Safe_tac; +by Auto_tac; by (Blast_tac 1); -by (auto_tac (claset(), simpset() addsimps [condition_def])); qed "elimination"; -(* As above, but for the special case of S=state *) +(* As above, but for the special case of A=state *) Goal "[| ALL m:M. F : {s:state. x(s) = m} co B(m); F:program |] \ \ ==> F:{s:state. x(s):M} co (UN m:M. B(m))"; by (rtac elimination 1); by (ALLGOALS(Clarify_tac)); qed "eliminiation2"; +(** strongest_rhs **) -Goalw [constrains_def, strongest_rhs_def] - "[| F:program; A:condition |] ==>F : A co (strongest_rhs(F,A))"; -by (auto_tac (claset() addDs [ActsD], simpset())); +Goalw [constrains_def, strongest_rhs_def, st_set_def] + "[| F:program; st_set(A) |] ==> F:A co (strongest_rhs(F,A))"; +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "constrains_strongest_rhs"; -Goalw [constrains_def, strongest_rhs_def] - "F : A co B ==> strongest_rhs(F,A) <=B"; +Goalw [constrains_def, strongest_rhs_def, st_set_def] +"[| F:A co B; st_set(B) |] ==> strongest_rhs(F,A) <= B"; by Safe_tac; by (dtac InterD 1); -by (auto_tac (claset(), - simpset() addsimps [condition_def])); +by Auto_tac; qed "strongest_rhs_is_strongest"; (*** increasing ***) -Goalw [increasing_on_def] - "[| F:increasing[A](f, r); z:A |] ==> F:stable({s:state. :r})"; -by (Blast_tac 1); -qed "increasing_onD"; +Goalw [increasing_def] "increasing(A, r, f) <= program"; +by (case_tac "A=0" 1); +by (etac not_emptyE 2); +by (Clarify_tac 2); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Inter_iff, Inter_0]))); +by (blast_tac (claset() addDs [stable_type RS subsetD]) 1); +qed "increasing_type"; -Goalw [increasing_on_def] -"F:increasing[A](f, r) ==> F:program & f:state->A & part_order(A,r)"; -by (auto_tac (claset(), simpset() addsimps [INT_iff])); -qed "increasing_onD2"; +Goalw [increasing_def] + "[| F:increasing(A, r, f); a:A |] ==> F:stable({s:state. :r})"; +by (Blast_tac 1); +qed "increasingD"; -Goalw [increasing_on_def, stable_def] -"[| part_order(A,r); c:A; F:program |] ==> F : increasing[A](lam s:state. c, r)"; -by (auto_tac (claset(), simpset() addsimps [INT_iff])); -by (force_tac (claset() addSDs [bspec, ActsD], - simpset() addsimps [constrains_def, condition_def]) 1); -qed "increasing_on_constant"; -Addsimps [increasing_on_constant]; +Goalw [increasing_def] +"F:increasing(A, r, f) ==> F:program & (EX a. a:A)"; +by (auto_tac (claset() addDs [stable_type RS subsetD], + simpset() addsimps [INT_iff])); +qed "increasingD2"; -Goalw [increasing_on_def, stable_def, constrains_def, part_order_def] - "!!f. g:mono_map(A,r,A,r) \ -\ ==> increasing[A](f, r) <= increasing[A](g O f, r)"; -by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1); -by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def])); -by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1); -by (subgoal_tac "xc:state" 1); -by (force_tac (claset() addSDs [ActsD], simpset()) 2); -by (subgoal_tac "f`xd:A & f`xc:A" 1); -by (blast_tac (claset() addDs [apply_type]) 2); -by (rotate_tac 3 1); -by (dres_inst_tac [("x", "f`xd")] bspec 1); -by (Asm_simp_tac 1); -by (REPEAT(etac conjE 1)); -by (rotate_tac ~2 1); +Goalw [increasing_def, stable_def] + "F:increasing(A, r, lam s:state. c) <-> F:program & (EX a. a:A)"; +by (auto_tac (claset() addDs [constrains_type RS subsetD], + simpset() addsimps [INT_iff])); +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (auto_tac (claset(), simpset() addsimps [constrains_def])); +qed "increasing_constant"; +AddIffs [increasing_constant]; + +Goalw [increasing_def, stable_def, constrains_def, st_set_def, part_order_def] +"[| g:mono_map(A,r,A,r); part_order(A, r); f:state->A |] \ +\ ==> increasing(A, r,f) <= increasing(A, r,g O f)"; +by (case_tac "A=0" 1); +by (Asm_full_simp_tac 1); +by (etac not_emptyE 1); +by (Clarify_tac 1); +by (cut_inst_tac [("F", "xa")] Acts_type 1); +by (asm_full_simp_tac (simpset() addsimps [Inter_iff, mono_map_def]) 1); +by Auto_tac; +by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); +by (dres_inst_tac [("x", "f`xf")] bspec 1); +by Auto_tac; +by (dres_inst_tac [("psi", "ALL x:A. ALL xa:A. ?u(x,xa)")] asm_rl 1); by (dres_inst_tac [("x", "act")] bspec 1); -by (Asm_simp_tac 1); -by (dres_inst_tac [("c", "xc")] subsetD 1); +by Auto_tac; +by (dres_inst_tac [("psi", "Acts(?u) <= ?v")] asm_rl 1); +by (dres_inst_tac [("psi", "?u <= state")] asm_rl 1); +by (dres_inst_tac [("c", "xe")] subsetD 1); by (rtac imageI 1); by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1); -by (dres_inst_tac [("x", "f`xd")] bspec 1); -by (dres_inst_tac [("x", "f`xc")] bspec 2); -by (ALLGOALS(Asm_simp_tac)); -by (dres_inst_tac [("b", "g`(f`xd)")] trans_onD 1); -by Auto_tac; -qed "mono_increasing_on_comp"; +by (asm_full_simp_tac (simpset() addsimps [refl_def, apply_type]) 1); +by (dres_inst_tac [("x1", "f`xf"), ("x", "f`xe")] (bspec RS bspec) 1); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type]))); +by (res_inst_tac [("b", "g ` (f ` xf)")] trans_onD 1); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [apply_type]))); +qed "mono_increasing_comp"; (*Holds by the theorem (succ(m) le n) = (m < n) *) -Goalw [increasing_on_def, nat_order_def] - "[| F:increasing[nat](f, nat_order); z:nat |] \ -\ ==> F: stable({s:state. z < f`s})"; +Goalw [increasing_def] + "[| F:increasing(nat, {:nat*nat. m le n}, f); f:state->nat; k:nat |] \ +\ ==> F: stable({s:state. k < f`s})"; by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); by Safe_tac; -by (dres_inst_tac [("x", "succ(z)")] bspec 1); +by (dres_inst_tac [("x", "succ(k)")] bspec 1); by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq])); -by (subgoal_tac "{x: state . f ` x : nat} = state" 1); +by (subgoal_tac "{x: state . f`x : nat} = state" 1); by Auto_tac; -qed "strict_increasing_onD"; \ No newline at end of file +qed "strict_increasingD"; + + +(* Used in WFair.thy *) +Goal "A:Pow(Pow(B)) ==> Union(A):Pow(B)"; +by Auto_tac; +qed "Union_PowI"; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/UNITY.thy --- a/src/ZF/UNITY/UNITY.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/UNITY.thy Thu Nov 15 15:07:16 2001 +0100 @@ -9,27 +9,31 @@ Theory ported from HOL. *) -UNITY = State + UNITYMisc + +UNITY = State + consts constrains :: "[i, i] => i" (infixl "co" 60) op_unless :: "[i, i] => i" (infixl "unless" 60) constdefs program :: i - "program == {:condition*actionSet*actionSet. - Id:acts & Id:allowed}" + "program == {: + Pow(state)*Pow(Pow(state*state))*Pow(Pow(state*state)). + id(state):acts & id(state):allowed}" + (* The definition below yields a program thanks to the coercions + init Int state, acts Int Pow(state*state), etc. *) mk_program :: [i,i,i]=>i "mk_program(init, acts, allowed) == - " + " SKIP :: i - "SKIP == mk_program(state, 0, action)" + "SKIP == mk_program(state, 0, Pow(state*state))" - (** Coercion from anything to program **) + (* Coercion from anything to program *) programify :: i=>i "programify(F) == if F:program then F else SKIP" - + RawInit :: i=>i "RawInit(F) == fst(F)" @@ -37,13 +41,13 @@ "Init(F) == RawInit(programify(F))" RawActs :: i=>i - "RawActs(F) == cons(Id, fst(snd(F)))" + "RawActs(F) == cons(id(state), fst(snd(F)))" Acts :: i=>i "Acts(F) == RawActs(programify(F))" RawAllowedActs :: i=>i - "RawAllowedActs(F) == cons(Id, snd(snd(F)))" + "RawAllowedActs(F) == cons(id(state), snd(snd(F)))" AllowedActs :: i=>i "AllowedActs(F) == RawAllowedActs(programify(F))" @@ -52,9 +56,8 @@ Allowed :: i =>i "Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}" - (* initially property, used by some UNITY authors *) - initially :: i => i - "initially(A) == {F:program. Init(F)<= A & A:condition}" + initially :: i=>i + "initially(A) == {F:program. Init(F)<=A}" stable :: i=>i "stable(A) == A co A" @@ -63,36 +66,24 @@ "strongest_rhs(F, A) == Inter({B:Pow(state). F:A co B})" invariant :: i => i - "invariant(A) == {F:program. Init(F)<=A} Int stable(A)" + "invariant(A) == initially(A) Int stable(A)" + + (* The `increasing' relation of Charpentier. Increasing's parameters are: + a state function f, a domain A and an order relation r over the domain A. *) + + increasing :: [i,i, i] => i + "increasing(A, r, f) == INT a:A. stable({s:state. :r})" + (* The definition of a partial order in ZF (predicate part_ord in theory Order) + describes a strict order: irreflexive and transitive. + However, the order used in association with Charpentier's increasing + relation is not, hence the definition below: *) part_order :: [i, i] => o "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)" - nat_order :: i - "nat_order == {:nat*nat. i le j}" - - (* - The constant increasing_on defines the Charpentier's increasing notion. - It should not be confused with the ZF's increasing constant - which have a different meaning. - Increasing_on's parameters: a state function f, a domain A and - a order relation r over the domain A - Should f be a meta function instead ? - *) - increasing_on :: [i,i, i] => i ("increasing[_]'(_,_')") - "increasing[A](f, r) == - {F:program. f:state->A & part_order(A,r) & F: - (INT z:A. stable({s:state. :r}))}" - defs - (* The typing requirements `A:condition & B:condition' - make the definition stronger than the original ones in HOL. *) - - constrains_def "A co B == - {F:program. (ALL act:Acts(F). act``A <= B) - & A:condition & B:condition}" - + (* Condition `st_set(A)' makes the definition slightly stronger than the HOL one *) + constrains_def "A co B == {F:program. (ALL act:Acts(F). act``A<=B) & st_set(A)}" unless_def "A unless B == (A - B) co (A Un B)" - end diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Union.ML Thu Nov 15 15:07:16 2001 +0100 @@ -17,8 +17,7 @@ by (force_tac (claset() addEs [reachable.induct] addIs reachable.intrs, simpset()) 1); qed "reachable_SKIP"; - -Addsimps [reachable_SKIP]; +AddIffs [reachable_SKIP]; (* Elimination programify from ok and Join *) @@ -38,44 +37,42 @@ by (simp_tac (simpset() addsimps [Join_def]) 1); qed "Join_programify_right"; -Addsimps [ok_programify_left, ok_programify_right, +AddIffs [ok_programify_left, ok_programify_right, Join_programify_left, Join_programify_right]; (** SKIP and safety properties **) -Goalw [constrains_def] -"[| A:condition; B:condition |] ==> (SKIP: A co B) <-> (A<=B)"; +Goalw [constrains_def, st_set_def] +"(SKIP: A co B) <-> (A<=B & st_set(A))"; by Auto_tac; qed "SKIP_in_constrains_iff"; -Addsimps [SKIP_in_constrains_iff]; - +AddIffs [SKIP_in_constrains_iff]; -Goalw [Constrains_def] -"[| A:condition; B:condition |] ==> (SKIP : A Co B)<-> (A<=B)"; -by (Asm_simp_tac 1); -by (auto_tac (claset(), - simpset() addsimps [condition_def])); +Goalw [Constrains_def]"(SKIP : A Co B)<-> (state Int A<=B)"; +by Auto_tac; qed "SKIP_in_Constrains_iff"; -Addsimps [SKIP_in_Constrains_iff]; +AddIffs [SKIP_in_Constrains_iff]; -Goal "A:condition ==>SKIP : stable(A)"; +Goal "SKIP:stable(A) <-> st_set(A)"; by (auto_tac (claset(), simpset() addsimps [stable_def])); qed "SKIP_in_stable"; -Addsimps [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable]; +AddIffs [SKIP_in_stable]; +Goalw [Stable_def] "SKIP:Stable(A)"; +by Auto_tac; +qed "SKIP_in_Stable"; +AddIffs [SKIP_in_Stable]; (** Join and JOIN types **) -Goalw [Join_def] - "F Join G : program"; +Goalw [Join_def] "F Join G : program"; by Auto_tac; qed "Join_in_program"; AddIffs [Join_in_program]; AddTCs [Join_in_program]; -Goalw [JOIN_def] -"JOIN(I,F):program"; +Goalw [JOIN_def] "JOIN(I,F):program"; by Auto_tac; qed "JOIN_in_program"; AddIffs [JOIN_in_program]; @@ -99,7 +96,6 @@ qed "AllowedActs_Join"; Addsimps [Init_Join, Acts_Join, AllowedActs_Join]; - (** Join's algebraic laws **) Goal "F Join G = G Join F"; @@ -107,21 +103,25 @@ [Join_def, Un_commute, Int_commute]) 1); qed "Join_commute"; - Goal "A Join (B Join C) = B Join (A Join C)"; -by (asm_simp_tac (simpset() addsimps - Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1); +by (asm_simp_tac (simpset() addsimps + Un_ac@Int_ac@[Join_def,Int_Un_distrib, cons_absorb]) 1); qed "Join_left_commute"; - Goal "(F Join G) Join H = F Join (G Join H)"; by (asm_simp_tac (simpset() addsimps Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib]) 1); qed "Join_assoc"; +(* Needed below *) +Goal "cons(id(state), Pow(state * state)) = Pow(state*state)"; +by Auto_tac; +qed "cons_id"; +AddIffs [cons_id]; + Goalw [Join_def, SKIP_def] "SKIP Join F = programify(F)"; -by (simp_tac (simpset() addsimps [Int_absorb, cons_absorb,cons_eq]) 1); +by (auto_tac (claset(), simpset() addsimps [Int_absorb,cons_eq])); qed "Join_SKIP_left"; Goal "F Join SKIP = programify(F)"; @@ -129,9 +129,7 @@ by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1); qed "Join_SKIP_right"; - -Addsimps [Join_SKIP_left, Join_SKIP_right]; - +AddIffs [Join_SKIP_left, Join_SKIP_right]; Goal "F Join F = programify(F)"; by (rtac program_equalityI 1); @@ -144,11 +142,10 @@ by (asm_simp_tac (simpset() addsimps [Join_assoc RS sym]) 1); qed "Join_left_absorb"; - (*Join is an AC-operator*) val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute]; -(** Eliminating programify in JN and OK expressions **) +(** Eliminating programify form JN and OK expressions **) Goal "OK(I, %x. programify(F(x))) <-> OK(I, F)"; by (simp_tac (simpset() addsimps [OK_def]) 1); @@ -158,46 +155,40 @@ by (simp_tac (simpset() addsimps [JOIN_def]) 1); qed "JN_programify"; -Addsimps [OK_programify, JN_programify]; +AddIffs [OK_programify, JN_programify]; (* JN *) -Goalw [JOIN_def] -"JOIN(0, F) = SKIP"; +Goalw [JOIN_def] "JOIN(0, F) = SKIP"; by Auto_tac; qed "JN_empty"; -Addsimps [JN_empty]; +AddIffs [JN_empty]; AddSEs [not_emptyE]; Addsimps [Inter_0]; -Goal +Goalw [JOIN_def] "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))"; -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (auto_tac (claset(), simpset() - addsimps [JOIN_def,INT_Int_distrib2])); +by (auto_tac (claset(), simpset() addsimps [INT_Int_distrib2])); qed "Init_JN"; -Goal -"Acts(JOIN(I,F)) = cons(Id, UN i:I. Acts(F(i)))"; -by (auto_tac (claset(), - simpset() addsimps [JOIN_def, UN_Int_distrib])); +Goalw [JOIN_def] +"Acts(JOIN(I,F)) = cons(id(state), UN i:I. Acts(F(i)))"; +by (auto_tac (claset(), simpset() addsimps [ UN_Int_distrib])); qed "Acts_JN"; -Goal -"AllowedActs(JN i:I. F(i)) = (if I=0 then action else (INT i:I. AllowedActs(F(i))))"; -by (auto_tac (claset(), simpset() - addsimps [JOIN_def, INT_cons RS sym, INT_Int_distrib2])); +Goalw [JOIN_def] +"AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))"; +by (auto_tac (claset(), + simpset() addsimps [INT_cons RS sym, INT_Int_distrib2])); qed "AllowedActs_JN"; - -Addsimps [Init_JN, Acts_JN, AllowedActs_JN]; +AddIffs [Init_JN, Acts_JN, AllowedActs_JN]; Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))"; by (rtac program_equalityI 1); by Auto_tac; qed "JN_cons"; -Addsimps[JN_cons]; +AddIffs[JN_cons]; val prems = Goalw [JOIN_def] @@ -208,7 +199,6 @@ Addcongs [JN_cong]; - (*** JN laws ***) Goal "k:I ==>F(k) Join (JN i:I. F(i)) = (JN i:I. F(i))"; by (stac (JN_cons RS sym) 1); @@ -268,14 +258,16 @@ alternative precondition is A<=B, but most proofs using this rule require I to be nonempty for other reasons anyway.*) -Goalw [constrains_def, JOIN_def] +Goalw [constrains_def, JOIN_def,st_set_def] "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)"; by Auto_tac; -by (blast_tac (claset() addDs [ActsD]) 1); +by (cut_inst_tac [("F","F(xa)")] Acts_type 1); +by (Blast_tac 2); +by (dres_inst_tac [("x", "xb")] bspec 1); +by Auto_tac; qed "JN_constrains"; -Goal "(F Join G : A co B) <-> \ -\ (programify(F):A co B & programify(G):A co B)"; +Goal "(F Join G : A co B) <-> (programify(F):A co B & programify(G):A co B)"; by (auto_tac (claset(), simpset() addsimps [constrains_def])); qed "Join_constrains"; @@ -285,7 +277,7 @@ by (asm_simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1); qed "Join_unless"; -Addsimps [Join_constrains, Join_unless]; +AddIffs [Join_constrains, Join_unless]; (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. reachable (F Join G) could be much bigger than reachable F, reachable G @@ -293,52 +285,67 @@ Goal "[| F : A co A'; G:B co B' |] \ \ ==> F Join G : (A Int B) co (A' Un B')"; -by (subgoal_tac "A:condition&A':condition & B: condition& \ - \ B': condition & F:program & G:program" 1); +by (subgoal_tac "st_set(A) & st_set(B) & F:program & G:program" 1); by (blast_tac (claset() addDs [constrainsD2]) 2); by (Asm_simp_tac 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "Join_constrains_weaken"; -(*If I=0, it degenerates to SKIP : UNIV co 0, which is false.*) -Goal "[| ALL i:I. F(i) : A(i) co A'(i); i: I |] \ +(*If I=0, it degenerates to SKIP : state co 0, which is false.*) +val [major, minor] = Goal +"[| (!!i. i:I ==> F(i) : A(i) co A'(i)); i: I |] \ \ ==> (JN i:I. F(i)) : (INT i:I. A(i)) co (UN i:I. A'(i))"; +by (cut_facts_tac [minor] 1); by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); by (Clarify_tac 1); -by (subgoal_tac "(ALL i:I. F(i):program & A(i):condition)&\ - \ (Union(RepFun(I, A')):condition)&\ - \ (Inter(RepFun(I, A)):condition)" 1); -by (blast_tac (claset() addDs [constrainsD2]) 2); -by (Asm_simp_tac 1); +by (forw_inst_tac [("i", "x")] major 1); +by (forward_tac [constrainsD2] 1); +by (Asm_full_simp_tac 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "JN_constrains_weaken"; - -Goal "A:condition ==> (JN i:I. F(i)) : stable(A) <-> \ -\ (ALL i:I. programify(F(i)):stable(A))"; +Goal "(JN i:I. F(i)): stable(A) <-> ((ALL i:I. programify(F(i)):stable(A)) & st_set(A))"; by (asm_simp_tac (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1); by Auto_tac; -by (blast_tac (claset() addDs [ActsD]) 1); +by (cut_inst_tac [("F", "F(xa)")] Acts_type 1); +by (dres_inst_tac [("x","xb")] bspec 1); +by Auto_tac; qed "JN_stable"; +val [major, minor] = Goalw [initially_def] + "[| (!!i. i:I ==>F(i):initially(A)); i:I |] ==> (JN i:I. F(i)):initially(A)"; +by (cut_facts_tac [minor] 1); +by (Asm_full_simp_tac 1); +by Safe_tac; +by (asm_full_simp_tac (simpset() addsimps [Inter_iff]) 1); +by (forw_inst_tac [("i", "x")] major 1); +by Auto_tac; +qed "initially_JN_I"; -Goal "[| ALL i:I. F(i) : invariant(A); i : I |] \ -\ ==> (JN i:I. F(i)) : invariant(A)"; -by (subgoal_tac "A:condition" 1); -by (blast_tac (claset() addDs [invariantD2]) 2); -by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1); -by (Blast_tac 1); -bind_thm ("invariant_JN_I", ballI RS result()); +val [major, minor] = Goal +"[|(!!i. i:I ==> F(i) : invariant(A)); i:I|]==> (JN i:I. F(i)):invariant(A)"; +by (cut_facts_tac [minor] 1); +by (auto_tac (claset() addSIs [initially_JN_I] addDs [major], + simpset() addsimps [invariant_def, JN_stable])); +by (thin_tac "i:I" 1); +by (forward_tac [major] 1); +by (dtac major 2); +by (auto_tac (claset(), simpset() addsimps [invariant_def])); +by (ALLGOALS(forward_tac [stableD2])); +by Auto_tac; +qed "invariant_JN_I"; + Goal " (F Join G : stable(A)) <-> \ \ (programify(F) : stable(A) & programify(G): stable(A))"; by (asm_simp_tac (simpset() addsimps [stable_def]) 1); qed "Join_stable"; - +AddIffs [Join_stable]; -(* TO BE DONE: stable_increasing *) - -Addsimps [Join_stable]; +Goalw [initially_def] "[| F:initially(A); G:initially(A) |] ==> F Join G: initially(A)"; +by Auto_tac; +qed "initially_JoinI"; +AddSIs [initially_JoinI]; Goal "[| F : invariant(A); G : invariant(A) |] \ \ ==> F Join G : invariant(A)"; @@ -354,11 +361,11 @@ by (asm_simp_tac (simpset() addsimps [FP_def, Inter_def]) 1); by (rtac equalityI 1); by Safe_tac; -by (ALLGOALS(subgoal_tac "{x}:condition")); +by (ALLGOALS(subgoal_tac "st_set({x})")); by (rotate_tac ~1 3); by (rotate_tac ~1 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable]))); -by (rewrite_goals_tac [condition_def]); +by (rewrite_goals_tac [st_set_def]); by (REPEAT(Blast_tac 1)); qed "FP_JN"; @@ -369,7 +376,7 @@ by (auto_tac (claset(), simpset() addsimps [transient_def, JOIN_def])); by (auto_tac (claset(), simpset() addsimps - [condition_def,UN_Int_distrib, INT_Int_distrib])); + [st_set_def,UN_Int_distrib, INT_Int_distrib])); qed "JN_transient"; Goal "F Join G : transient(A) <-> \ @@ -379,18 +386,18 @@ Join_def, Int_Un_distrib])); qed "Join_transient"; -Addsimps [Join_transient]; +AddIffs [Join_transient]; Goal "F : transient(A) ==> F Join G : transient(A)"; by (asm_full_simp_tac (simpset() - addsimps [Join_transient, transientD]) 1); + addsimps [Join_transient, transientD2]) 1); qed "Join_transient_I1"; Goal "G : transient(A) ==> F Join G : transient(A)"; by (asm_full_simp_tac (simpset() - addsimps [Join_transient, transientD]) 1); + addsimps [Join_transient, transientD2]) 1); qed "Join_transient_I2"; (*If I=0 it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) @@ -410,34 +417,25 @@ by (auto_tac (claset(), simpset() addsimps [Join_transient])); qed "Join_ensures"; - - -Goalw [stable_def, constrains_def, Join_def] +Goalw [stable_def, constrains_def, Join_def, st_set_def] "[| F : stable(A); G : A co A' |] \ \ ==> F Join G : A co A'"; -by Auto_tac; -by (rewrite_goals_tac [condition_def]); +by (cut_inst_tac [("F", "F")] Acts_type 1); +by (cut_inst_tac [("F", "G")] Acts_type 1); by Auto_tac; -by (blast_tac (claset() addDs [ActsD]) 3); -by (dres_inst_tac [("x", "Id")] bspec 1); -by (dres_inst_tac [("x", "Id")] bspec 2); -by (dres_inst_tac [("x", "x")] bspec 4); -by (dres_inst_tac [("x", "Id")] bspec 5); -by Auto_tac; +by (REPEAT(Blast_tac 1)); qed "stable_Join_constrains"; (*Premise for G cannot use Always because F: Stable A is weaker than G : stable A *) Goal "[| F : stable(A); G : invariant(A) |] ==> F Join G : Always(A)"; -by (subgoal_tac "A:condition & F:program" 1); -by (blast_tac (claset() addDs [stableD2]) 2); -by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def, +by (subgoal_tac "F:program & G:program & st_set(A)" 1); +by (blast_tac (claset() addDs [invariantD2, stableD2]) 2); +by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def,initially_def , Stable_eq_stable]) 1); by (force_tac(claset() addIs [stable_Int], simpset()) 1); qed "stable_Join_Always1"; - - (*As above, but exchanging the roles of F and G*) Goal "[| F : invariant(A); G : stable(A) |] ==> F Join G : Always(A)"; by (stac Join_commute 1); @@ -447,8 +445,8 @@ Goal "[| F : stable(A); G : A ensures B |] ==> F Join G : A ensures B"; -by (subgoal_tac "F:program&G:program&A:condition&B:condition" 1); -by (blast_tac (claset() addDs [stableD2, ensuresD2]) 2); +by (subgoal_tac "F:program & G:program & st_set(A)" 1); +by (blast_tac (claset() addDs [stableD2, ensures_type RS subsetD]) 2); by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1); by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); by (etac constrains_weaken 1); @@ -462,19 +460,16 @@ by (blast_tac (claset() addIs [stable_Join_ensures1]) 1); qed "stable_Join_ensures2"; - -(*** the ok and OK relations ***) +(*** The ok and OK relations ***) Goal "SKIP ok F"; -by (auto_tac (claset() addDs [ActsD], - simpset() addsimps [ok_def])); +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset() addsimps [ok_def])); qed "ok_SKIP1"; Goal "F ok SKIP"; -by (auto_tac (claset() addDs [ActsD], +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset() addsimps [ok_def])); qed "ok_SKIP2"; - AddIffs [ok_SKIP1, ok_SKIP2]; Goal "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))"; @@ -513,14 +508,13 @@ Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))"; by (auto_tac (claset(), simpset() addsimps [ok_def])); -by (blast_tac (claset() addDs [ActsD]) 1); -by (REPEAT(Force_tac 1)); +by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1); qed "ok_JN_iff1"; Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)"; by (auto_tac (claset(), simpset() addsimps [ok_def])); -by (blast_tac (claset() addDs [ActsD]) 1); +by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1); qed "ok_JN_iff2"; AddIffs [ok_JN_iff1, ok_JN_iff2]; @@ -528,7 +522,6 @@ by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def])); qed "OK_iff_ok"; - Goal "[| OK(I,F); i: I; j: I; i~=j|] ==> F(i) ok F(j)"; by (auto_tac (claset(), simpset() addsimps [OK_iff_ok])); qed "OK_imp_ok"; @@ -537,7 +530,7 @@ (*** Allowed ***) Goal "Allowed(SKIP) = program"; -by (auto_tac (claset() addDs [ActsD], +by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset() addsimps [Allowed_def])); qed "Allowed_SKIP"; @@ -549,10 +542,7 @@ Goal "i:I ==> \ \ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))"; by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -br equalityI 1; -by Auto_tac; qed "Allowed_JN"; - Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN]; Goal @@ -569,7 +559,7 @@ (*** safety_prop, for reasoning about given instances of "ok" ***) -Goal "safety_prop(X) ==> (Acts(G) <= cons(Id, (UN F:X. Acts(F)))) <-> (programify(G):X)"; +Goal "safety_prop(X) ==> (Acts(G) <= cons(id(state), (UN F:X. Acts(F)))) <-> (programify(G):X)"; by (full_simp_tac( simpset() addsimps [safety_prop_def]) 1); by (Clarify_tac 1); by (case_tac "G:program" 1); @@ -581,19 +571,20 @@ addsimps [programify_def]) 1); qed "safety_prop_Acts_iff"; -Goal "X:property ==> \ -\ (safety_prop(X) --> \ -\ ((UN G:X. Acts(G)) <= AllowedActs(F)) <-> (X <= Allowed(programify(F))))"; +Goal "safety_prop(X) ==> \ +\ (UN G:X. Acts(G)) <= AllowedActs(F) <-> (X <= Allowed(programify(F)))"; by (auto_tac (claset(), simpset() addsimps [Allowed_def, - safety_prop_Acts_iff RS iff_sym, property_def])); + safety_prop_Acts_iff RS iff_sym])); +by (rewrite_goals_tac [safety_prop_def]); +by Auto_tac; qed "safety_prop_AllowedActs_iff_Allowed"; -Goal "X:property ==> \ -\ safety_prop(X) --> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X"; +Goal "safety_prop(X) ==> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X"; by (asm_full_simp_tac (simpset() addsimps [Allowed_def, - UN_Int_distrib,safety_prop_Acts_iff, property_def]) 1); + UN_Int_distrib, safety_prop_Acts_iff]) 1); +by (rewrite_goals_tac [safety_prop_def]); by Auto_tac; qed "Allowed_eq"; @@ -603,26 +594,30 @@ qed "def_prg_Allowed"; (*For safety_prop to hold, the property must be satisfiable!*) -Goal "B:condition ==> safety_prop(A co B) <-> (A <= B)"; -by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1); +Goal "safety_prop(A co B) <-> (A <= B & st_set(A))"; +by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1); by Auto_tac; -by (Blast_tac 2); -by (force_tac (claset(), simpset() addsimps [condition_def]) 1); +by (REPEAT(Blast_tac 1)); qed "safety_prop_constrains"; -Addsimps [safety_prop_constrains]; - +AddIffs [safety_prop_constrains]; +(* To be used with resolution *) +Goal "[| A<=B; st_set(A) |] ==>safety_prop(A co B)"; +by Auto_tac; +qed "safety_prop_constrainsI"; -Goal "A:condition ==>safety_prop(stable(A))"; +Goal "safety_prop(stable(A)) <-> st_set(A)"; by (asm_simp_tac (simpset() addsimps [stable_def]) 1); qed "safety_prop_stable"; -Addsimps [safety_prop_stable]; +AddIffs [safety_prop_stable]; -Goal "[| X:property; Y:property |] ==> \ -\ safety_prop(X) --> safety_prop(Y) --> safety_prop(X Int Y)"; -by (asm_full_simp_tac (simpset() - addsimps [safety_prop_def, property_def]) 1); -by Safe_tac; +Goal "st_set(A) ==> safety_prop(stable(A))"; +by Auto_tac; +qed "safety_prop_stableI"; + +Goal "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)"; +by (asm_full_simp_tac (simpset() addsimps [safety_prop_def]) 1); +by Auto_tac; by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), ("C", "Union(RepFun(Y, Acts))")] subset_trans 2); by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), @@ -632,18 +627,26 @@ Addsimps [safety_prop_Int]; (* If I=0 the conclusion becomes safety_prop(0) which is false *) -Goal "[| ALL i:I. X(i):property; i:I |] ==> \ -\ (ALL i:I. safety_prop(X(i))) --> safety_prop(INT i:I. X(i))"; -by (asm_full_simp_tac (simpset() addsimps [safety_prop_def, property_def]) 1); +val [major, minor] = Goalw [safety_prop_def] +"[| (!!i. i:I ==>safety_prop(X(i))); i:I |] ==> safety_prop(INT i:I. X(i))"; +by (cut_facts_tac [minor] 1); by Safe_tac; +by (full_simp_tac (simpset() addsimps [Inter_iff]) 1); +by (Clarify_tac 1); +by (forward_tac [major] 1); +by (dres_inst_tac [("i", "xa")] major 2); +by (forw_inst_tac [("i", "xa")] major 4); +by (ALLGOALS(Asm_full_simp_tac)); +by Auto_tac; by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"), - ("C", "Union(RepFun(X(xb), Acts))")] subset_trans 3); + ("C", "Union(RepFun(X(xa), Acts))")] subset_trans 1); by (REPEAT(Blast_tac 1)); -bind_thm ("safety_prop_Inter", ballI RS result()); +qed "safety_prop_Inter"; -Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X); X:property |] \ -\ ==> F ok G <-> (programify(G):X & acts Int action <= AllowedActs(G))"; +Goal "[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X) |] \ +\ ==> F ok G <-> (programify(G):X & acts Int Pow(state*state) <= AllowedActs(G))"; by (auto_tac (claset(), - simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib, property_def])); + simpset() addsimps [ok_def, safety_prop_Acts_iff, UN_Int_distrib])); qed "def_UNION_ok_iff"; + diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/Union.thy Thu Nov 15 15:07:16 2001 +0100 @@ -34,12 +34,8 @@ AllowedActs(F) Int AllowedActs(G))" (*Characterizes safety properties. Used with specifying AllowedActs*) safety_prop :: "i => o" - "safety_prop(X) == SKIP:X & - (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)" - - property :: i - "property == Pow(program)" - + "safety_prop(X) == X<=program & + SKIP:X & (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)" syntax "@JOIN1" :: [pttrns, i] => i ("(3JN _./ _)" 10) @@ -50,7 +46,7 @@ "JN x y. B" == "JN x. JN y. B" "JN x. B" == "JOIN(state,(%x. B))" -syntax (xsymbols) +syntax (symbols) SKIP :: i ("\\") "op Join" :: [i, i] => i (infixl "\\" 65) "@JOIN1" :: [pttrns, i] => i ("(3\\ _./ _)" 10) diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/WFair.ML Thu Nov 15 15:07:16 2001 +0100 @@ -10,10 +10,14 @@ (*** transient ***) -Goalw [transient_def] -"F:transient(A) ==> F:program & A:condition"; +Goalw [transient_def] "transient(A)<=program"; by Auto_tac; -qed "transientD"; +qed "transient_type"; + +Goalw [transient_def] +"F:transient(A) ==> F:program & st_set(A)"; +by Auto_tac; +qed "transientD2"; Goalw [stable_def, constrains_def, transient_def] "[| F : stable(A); F : transient(A) |] ==> A = 0"; @@ -21,27 +25,24 @@ by (Blast_tac 1); qed "stable_transient_empty"; -Goalw [transient_def] - "[| F : transient(A); B<=A |] ==> F : transient(B)"; +Goalw [transient_def, st_set_def] +"[|F:transient(A); B<=A|] ==> F:transient(B)"; by Safe_tac; by (res_inst_tac [("x", "act")] bexI 1); by (ALLGOALS(Asm_full_simp_tac)); by (Blast_tac 1); -by (auto_tac (claset(), - simpset() addsimps [condition_def])); +by Auto_tac; qed "transient_strengthen"; -Goalw [transient_def] -"[| act:Acts(F); A <= domain(act); act``A <= state-A; \ -\ F:program; A:condition |] ==> F : transient(A)"; +Goalw [transient_def] +"[|act:Acts(F); A <= domain(act); act``A <= state-A; \ +\ F:program; st_set(A)|] ==> F:transient(A)"; by (Blast_tac 1); qed "transientI"; val major::prems = -Goalw [transient_def] - "[| F:transient(A); \ -\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A |] ==> P |] \ -\ ==> P"; +Goalw [transient_def] "[| F:transient(A); \ +\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P"; by (rtac (major RS CollectE) 1); by (blast_tac (claset() addIs prems) 1); qed "transientE"; @@ -49,121 +50,114 @@ Goalw [transient_def] "transient(state) = 0"; by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); -by (dtac ActsD 1); +by (cut_inst_tac [("F", "x")] Acts_type 1); by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); -by (blast_tac (claset() addSDs [state_subset_not_empty]) 1); +by (subgoal_tac "EX x. x:state" 1); +by Auto_tac; qed "transient_state"; +Goalw [transient_def,st_set_def] "state<=B ==> transient(B) = 0"; +by (rtac equalityI 1); +by (ALLGOALS(Clarify_tac)); +by (cut_inst_tac [("F", "x")] Acts_type 1); +by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); +by (subgoal_tac "EX x. x:state" 1); +by (subgoal_tac "B=state" 1); +by Auto_tac; +qed "transient_state2"; + Goalw [transient_def] "transient(0) = program"; by (rtac equalityI 1); -by Safe_tac; -by (subgoal_tac "Id:Acts(x)" 1); -by (Asm_simp_tac 2); -by (res_inst_tac [("x", "Id")] bexI 1); -by (ALLGOALS(Blast_tac)); +by Auto_tac; qed "transient_empty"; -Addsimps [transient_empty, transient_state]; +Addsimps [transient_empty, transient_state, transient_state2]; (*** ensures ***) +Goalw [ensures_def, constrains_def] "A ensures B <=program"; +by Auto_tac; +qed "ensures_type"; + Goalw [ensures_def] - "[| F : (A-B) co (A Un B); F : transient(A-B) |] \ -\ ==> F : A ensures B"; -by (Blast_tac 1); +"[|F:(A-B) co (A Un B); F:transient(A-B)|]==>F:A ensures B"; +by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD])); qed "ensuresI"; -(** From Misra's notes, Progress chapter, exercise number 4 **) +(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *) Goal "[| F:A co A Un B; F: transient(A) |] ==> F: A ensures B"; by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); -by (auto_tac (claset(), simpset() addsimps [ensures_def])); +by (auto_tac (claset(), simpset() addsimps [ensures_def, transient_type RS subsetD])); qed "ensuresI2"; - -Goalw [ensures_def] - "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"; -by (Blast_tac 1); +Goalw [ensures_def] "F:A ensures B ==> F:(A-B) co (A Un B) & F:transient (A-B)"; +by Auto_tac; qed "ensuresD"; -Goalw [ensures_def, constrains_def] - "F : A ensures B ==> F:program & A:condition & B:condition"; -by Auto_tac; -qed "ensuresD2"; - -Goalw [ensures_def] - "[| F : A ensures A'; A'<=B'; B':condition |] ==> F : A ensures B'"; -by (Clarify_tac 1); +Goalw [ensures_def] "[|F:A ensures A'; A'<=B' |] ==> F:A ensures B'"; by (blast_tac (claset() - addIs [transient_strengthen, constrains_weaken] - addDs [constrainsD2]) 1); + addIs [transient_strengthen, constrains_weaken]) 1); qed "ensures_weaken_R"; (*The L-version (precondition strengthening) fails, but we have this*) -Goalw [ensures_def] - "[| F : stable(C); F : A ensures B |] \ -\ ==> F : (C Int A) ensures (C Int B)"; +Goalw [ensures_def] "[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)"; by (asm_full_simp_tac (simpset() addsimps [ensures_def, Int_Un_distrib2, Diff_Int_distrib RS sym]) 1); by (Clarify_tac 1); by (blast_tac (claset() addIs [transient_strengthen, - stable_constrains_Int, constrains_weaken] - addDs [constrainsD2]) 1); + stable_constrains_Int, constrains_weaken]) 1); qed "stable_ensures_Int"; -Goal "[| F : stable(A); F : transient(C); \ -\ A <= B Un C; B:condition|] ==> F : A ensures B"; -by (asm_full_simp_tac (simpset() - addsimps [ensures_def, stable_def]) 1); +Goal "[|F:stable(A); F:transient(C); A<=B Un C|] ==> F : A ensures B"; +by (forward_tac [stable_type RS subsetD] 1); +by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); by (Clarify_tac 1); by (blast_tac (claset() addIs [transient_strengthen, - constrains_weaken] - addDs [constrainsD2]) 1); + constrains_weaken]) 1); qed "stable_transient_ensures"; Goal "(A ensures B) = (A unless B) Int transient (A-B)"; -by (simp_tac (simpset() - addsimps [ensures_def, unless_def]) 1); +by (auto_tac (claset(), simpset() addsimps [ensures_def, unless_def])); qed "ensures_eq"; +Goal "[| F:program; A<=B |] ==> F : A ensures B"; +by (rewrite_goal_tac [ensures_def,constrains_def,transient_def, st_set_def] 1); +by Auto_tac; +qed "subset_imp_ensures"; + (*** leadsTo ***) - -val leads_lhs_subset = leads.dom_subset RS subsetD RS SigmaD1; -val leads_rhs_subset = leads.dom_subset RS subsetD RS SigmaD2; +val leads_left = leads.dom_subset RS subsetD RS SigmaD1; +val leads_right = leads.dom_subset RS subsetD RS SigmaD2; -Goalw [leadsTo_def] - "F: A leadsTo B ==> F:program & A:condition & B:condition"; -by (blast_tac (claset() addDs [leads_lhs_subset, - leads_rhs_subset]) 1); -qed "leadsToD"; +Goalw [leadsTo_def] "A leadsTo B <= program"; +by Auto_tac; +qed "leadsTo_type"; + +Goalw [leadsTo_def, st_set_def] +"F: A leadsTo B ==> F:program & st_set(A) & st_set(B)"; +by (blast_tac (claset() addDs [leads_left, leads_right]) 1); +qed "leadsToD2"; -Goalw [leadsTo_def] - "F : A ensures B ==> F : A leadsTo B"; -by (blast_tac (claset() addDs [ensuresD2] - addIs [leads.Basis]) 1); +Goalw [leadsTo_def, st_set_def] + "[|F:A ensures B; st_set(A); st_set(B)|] ==> F:A leadsTo B"; +by (cut_facts_tac [ensures_type] 1); +by (auto_tac (claset() addIs [leads.Basis], simpset())); qed "leadsTo_Basis"; +AddIs [leadsTo_Basis]; -AddIs [leadsTo_Basis]; -Addsimps [leadsTo_Basis]; +(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) +(* [| F:program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) +bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); -Goalw [leadsTo_def] - "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C"; -by (blast_tac (claset() addIs [leads.Trans]) 1); +Goalw [leadsTo_def] "[|F: A leadsTo B; F: B leadsTo C |]==>F: A leadsTo C"; +by (auto_tac (claset() addIs [leads.Trans], simpset())); qed "leadsTo_Trans"; -(* To be move to State.thy *) - -Goalw [condition_def] - "A:condition ==> state<=A <-> A=state"; -by Auto_tac; -qed "state_upper"; -Addsimps [state_upper]; - - -Goalw [transient_def] - "F : transient(A) ==> F : A leadsTo (state - A )"; +(* Better when used in association with leadsTo_weaken_R *) +Goalw [transient_def] "F:transient(A) ==> F : A leadsTo (state-A )"; by (rtac (ensuresI RS leadsTo_Basis) 1); by (ALLGOALS(Clarify_tac)); by (blast_tac (claset() addIs [transientI]) 2); @@ -172,7 +166,6 @@ qed "transient_imp_leadsTo"; (*Useful with cancellation, disjunction*) - Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate"; @@ -181,126 +174,214 @@ by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate2"; -(*The Union introduction rule as we should have liked to state it*) -Goalw [leadsTo_def] - "[| ALL A:S. F : A leadsTo B; F:program; B:condition |]\ -\ ==> F : Union(S) leadsTo B"; -by (Clarify_tac 1); -by (blast_tac (claset() addIs [leads.Union] - addDs [leads_lhs_subset]) 1); -bind_thm ("leadsTo_Union", ballI RS result()); +(* The Union introduction rule as we should have liked to state it *) +val [major, program,B]= Goalw [leadsTo_def, st_set_def] +"[|(!!A. A:S ==> F:A leadsTo B); F:program; st_set(B)|]==>F:Union(S) leadsTo B"; +by (cut_facts_tac [program, B] 1); +by Auto_tac; +by (rtac leads.Union 1); +by Auto_tac; +by (ALLGOALS(dtac major)); +by (auto_tac (claset() addDs [leads_left], simpset())); +qed "leadsTo_Union"; -Goalw [leadsTo_def] - "[| ALL A:S. F: (A Int C) leadsTo B; F:program; B:condition |] \ - \ ==> F : (Union(S) Int C) leadsTo B"; -by (Clarify_tac 1); -by (simp_tac (simpset() addsimps [Int_Union_Union]) 1); -by (blast_tac (claset() addIs [leads.Union] - addDs [leads_lhs_subset, leads_rhs_subset]) 1); -bind_thm ("leadsTo_Union_Int", ballI RS result()); +val [major,program,B] = Goalw [leadsTo_def, st_set_def] +"[|(!!A. A:S ==>F:(A Int C) leadsTo B); F:program; st_set(B)|]==>F:(Union(S)Int C)leadsTo B"; +by (cut_facts_tac [program, B] 1); +by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); +by (rtac leads.Union 1); +by Auto_tac; +by (ALLGOALS(dtac major)); +by (auto_tac (claset() addDs [leads_left], simpset())); +qed "leadsTo_Union_Int"; -Goalw [leadsTo_def] -"[| ALL i:I. F : (A(i)) leadsTo B; F:program; B:condition |] \ -\ ==> F:(UN i:I. A(i)) leadsTo B"; -by (Clarify_tac 1); -by (simp_tac (simpset() addsimps [Int_Union_Union]) 1); -by (blast_tac (claset() addIs [leads.Union] - addDs [leads_lhs_subset, leads_rhs_subset]) 1); -bind_thm ("leadsTo_UN", ballI RS result()); +val [major,program,B] = Goalw [leadsTo_def, st_set_def] +"[|(!!i. i:I ==> F : A(i) leadsTo B); F:program; st_set(B)|]==>F:(UN i:I. A(i)) leadsTo B"; +by (cut_facts_tac [program, B] 1); +by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); +by (rtac leads.Union 1); +by Auto_tac; +by (ALLGOALS(dtac major)); +by (auto_tac (claset() addDs [leads_left], simpset())); +qed "leadsTo_UN"; -(*Binary union introduction rule*) +(* Binary union introduction rule *) Goal "[| F: A leadsTo C; F: B leadsTo C |] ==> F : (A Un B) leadsTo C"; by (stac Un_eq_Union 1); -by (blast_tac (claset() addIs [leadsTo_Union] - addDs [leadsToD]) 1); +by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1); qed "leadsTo_Un"; +val [major, program, B] = Goal +"[|(!!x. x:A==> F:{x} leadsTo B); F:program; st_set(B) |] ==> F:A leadsTo B"; +by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1); +by (rtac leadsTo_UN 1); +by (auto_tac (claset() addDs prems, simpset() addsimps [major, program, B])); +qed "single_leadsTo_I"; + +Goal "[| F:program; st_set(A) |] ==> F: A leadsTo A"; +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); +qed "leadsTo_refl"; + +Goal "F: A leadsTo A <-> F:program & st_set(A)"; +by (auto_tac (claset() addIs [leadsTo_refl] + addDs [leadsToD2], simpset())); +qed "leadsTo_refl_iff"; + +Goal "F: 0 leadsTo B <-> (F:program & st_set(B))"; +by (auto_tac (claset() addIs [subset_imp_leadsTo] + addDs [leadsToD2], simpset())); +qed "empty_leadsTo"; +AddIffs [empty_leadsTo]; + +Goal "F: A leadsTo state <-> (F:program & st_set(A))"; +by (auto_tac (claset() addIs [subset_imp_leadsTo] + addDs [leadsToD2, st_setD], simpset())); +qed "leadsTo_state"; +AddIffs [leadsTo_state]; + +Goal "[| F:A leadsTo A'; A'<=B'; st_set(B') |] ==> F : A leadsTo B'"; +by (blast_tac (claset() addDs [leadsToD2] + addIs [subset_imp_leadsTo,leadsTo_Trans]) 1); +qed "leadsTo_weaken_R"; + +Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; +by (forward_tac [leadsToD2] 1); +by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1); +qed_spec_mp "leadsTo_weaken_L"; + +Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'"; +by (forward_tac [leadsToD2] 1); +by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, + leadsTo_Trans, leadsTo_refl]) 1); +qed "leadsTo_weaken"; + +(* This rule has a nicer conclusion *) +Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B"; +by (forward_tac [transientD2] 1); +by (rtac leadsTo_weaken_R 1); +by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo])); +qed "transient_imp_leadsTo2"; + +(*Distributes over binary unions*) +Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)"; +by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); +qed "leadsTo_Un_distrib"; + +Goal +"(F:(UN i:I. A(i)) leadsTo B)<-> ((ALL i : I. F: A(i) leadsTo B) & F:program & st_set(B))"; +by (blast_tac (claset() addDs [leadsToD2] + addIs [leadsTo_UN, leadsTo_weaken_L]) 1); +qed "leadsTo_UN_distrib"; + +Goal "(F: Union(S) leadsTo B) <-> (ALL A:S. F : A leadsTo B) & F:program & st_set(B)"; +by (blast_tac (claset() addDs [leadsToD2] + addIs [leadsTo_Union, leadsTo_weaken_L]) 1); +qed "leadsTo_Union_distrib"; + +(*Set difference: maybe combine with leadsTo_weaken_L?*) +Goal "[| F: (A-B) leadsTo C; F: B leadsTo C; st_set(C) |] ==> F: A leadsTo C"; +by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken] + addDs [leadsToD2]) 1); +qed "leadsTo_Diff"; + +val [major,minor] = Goal +"[|(!!i. i:I ==> F: A(i) leadsTo A'(i)); F:program |] \ +\ ==> F: (UN i:I. A(i)) leadsTo (UN i:I. A'(i))"; +by (rtac leadsTo_Union 1); +by (ALLGOALS(Asm_simp_tac)); +by Safe_tac; +by (simp_tac (simpset() addsimps [minor]) 2); +by (blast_tac (claset() addDs [leadsToD2, major])2); +by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [major, leadsToD2]) 1); +qed "leadsTo_UN_UN"; + +(*Binary union version*) +Goal "[| F: A leadsTo A'; F:B leadsTo B' |] ==> F : (A Un B) leadsTo (A' Un B')"; +by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B')" 1); +by (blast_tac (claset() addDs [leadsToD2]) 2); +by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); +qed "leadsTo_Un_Un"; + +(** The cancellation law **) +Goal "[|F: A leadsTo (A' Un B); F: B leadsTo B'|] ==> F: A leadsTo (A' Un B')"; +by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F:program" 1); +by (blast_tac (claset() addDs [leadsToD2]) 2); +by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]) 1); +qed "leadsTo_cancel2"; + +Goal "[|F: A leadsTo (A' Un B); F : (B-A') leadsTo B'|]==> F: A leadsTo (A' Un B')"; +by (rtac leadsTo_cancel2 1); +by (assume_tac 2); +by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_weaken_R]) 1); +qed "leadsTo_cancel_Diff2"; + -Goal "[| ALL x:A. F:{x} leadsTo B; \ -\ F:program; B:condition |] ==> F : A leadsTo B"; -by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1); -by (blast_tac (claset() addIs [leadsTo_UN]) 1); -bind_thm("single_leadsTo_I", ballI RS result()); +Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] ==> F:A leadsTo (B' Un A')"; +by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); +by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); +qed "leadsTo_cancel1"; +Goal "[|F: A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F : A leadsTo (B' Un A')"; +by (rtac leadsTo_cancel1 1); +by (assume_tac 2); +by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [leadsToD2]) 1); +qed "leadsTo_cancel_Diff1"; (*The INDUCTION rule as we should have liked to state it*) -val major::prems = Goalw [leadsTo_def] +val [major, basis_prem, trans_prem, union_prem] = Goalw [leadsTo_def, st_set_def] "[| F: za leadsTo zb; \ -\ !!A B. F : A ensures B ==> P(A, B); \ +\ !!A B. [| F: A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \ \ !!A B C. [| F: A leadsTo B; P(A, B); \ \ F: B leadsTo C; P(B, C) |] \ \ ==> P(A, C); \ -\ !!B S. [| ALL A:S. F:A leadsTo B & P(A, B); B:condition |] \ +\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A)|] \ \ ==> P(Union(S), B) \ \ |] ==> P(za, zb)"; by (cut_facts_tac [major] 1); by (rtac (major RS CollectD2 RS leads.induct) 1); -by (auto_tac (claset() addIs prems, simpset())); +by (rtac union_prem 3); +by (rtac trans_prem 2); +by (rtac basis_prem 1); +by Auto_tac; qed "leadsTo_induct"; -Goal -"[| A<=B; F:program; B:condition |] \ -\ ==> F : A ensures B"; -by (rewrite_goals_tac [ensures_def, constrains_def, - transient_def, condition_def]); -by (Clarify_tac 1); -by Safe_tac; -by (res_inst_tac [("x", "Id")] bexI 5); -by (REPEAT(blast_tac (claset() addDs [Id_in_Acts]) 1)); -qed "subset_imp_ensures"; - -bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); -bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo); - -bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); - -Addsimps [empty_leadsTo]; - -Goalw [condition_def] - "[| F:program; A:condition |] ==> F: A leadsTo state"; -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); -qed "leadsTo_state"; -Addsimps [leadsTo_state]; - -(* A nicer induction rule; without ensures *) -val [major,impl,basis,trans,unionp] = Goal +(* Added by Sidi, an induction rule without ensures *) +val [major,imp_prem,basis_prem,trans_prem,union_prem] = Goal "[| F: za leadsTo zb; \ -\ !!A B. [| A<=B; B:condition |] ==> P(A, B); \ -\ !!A B. [| F:A co A Un B; F:transient(A) |] ==> P(A, B); \ +\ !!A B. [| A<=B; st_set(B) |] ==> P(A, B); \ +\ !!A B. [| F:A co A Un B; F:transient(A); st_set(B) |] ==> P(A, B); \ \ !!A B C. [| F: A leadsTo B; P(A, B); \ \ F: B leadsTo C; P(B, C) |] \ \ ==> P(A, C); \ -\ !!B S. [| ALL A:S. F:A leadsTo B & P(A, B); B:condition |] \ +\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A) |] \ \ ==> P(Union(S), B) \ \ |] ==> P(za, zb)"; by (cut_facts_tac [major] 1); by (etac leadsTo_induct 1); -by (auto_tac (claset() addIs [trans,unionp], simpset())); +by (auto_tac (claset() addIs [trans_prem,union_prem], simpset())); by (rewrite_goal_tac [ensures_def] 1); -by Auto_tac; +by (Clarify_tac 1); by (forward_tac [constrainsD2] 1); by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1); -by Auto_tac; +by (Blast_tac 1); by (forward_tac [ensuresI2 RS leadsTo_Basis] 1); -by (dtac basis 2); -by (subgoal_tac "A Int B <= B " 3); -by Auto_tac; -by (dtac impl 1); -by Auto_tac; -by (res_inst_tac [("a", "Union({A - B, A Int B})"), ("P", "%x. P(x, ?u)")] subst 1); -by (rtac unionp 2); +by (dtac basis_prem 4); +by (ALLGOALS(Asm_full_simp_tac)); +by (forw_inst_tac [("A1", "A"), ("B", "B")] (Int_lower2 RS imp_prem) 1); +by (subgoal_tac "A=Union({A - B, A Int B})" 1); +by (Blast_tac 2); +by (etac ssubst 1); +by (rtac union_prem 1); by (auto_tac (claset() addIs [subset_imp_leadsTo], simpset())); qed "leadsTo_induct2"; - - (** Variant induction rule: on the preconditions for B **) (*Lemma is the weak version: can't see how to do it in one step*) val major::prems = Goal "[| F : za leadsTo zb; \ \ P(zb); \ -\ !!A B. [| F : A ensures B; P(B) |] ==> P(A); \ -\ !!S. [| ALL A:S. P(A) |] ==> P(Union(S)) \ +\ !!A B. [| F : A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \ +\ !!S. [| ALL A:S. P(A); ALL A:S. st_set(A) |] ==> P(Union(S)) \ \ |] ==> P(za)"; (*by induction on this formula*) by (subgoal_tac "P(zb) --> P(za)" 1); @@ -311,145 +392,43 @@ qed "lemma"; -val [major, cond, ensuresp, unionp] = Goal +val [major, zb_prem, basis_prem, union_prem] = Goal "[| F : za leadsTo zb; \ \ P(zb); \ -\ !!A B. [| F : A ensures B; F : B leadsTo zb; P(B) |] ==> P(A); \ -\ !!S. ALL A:S. F : A leadsTo zb & P(A) ==> P(Union(S)) \ +\ !!A B. [| F : A ensures B; F : B leadsTo zb; P(B); st_set(A) |] ==> P(A); \ +\ !!S. ALL A:S. F : A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \ \ |] ==> P(za)"; by (cut_facts_tac [major] 1); by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1); by (etac conjunct2 1); by (rtac (major RS lemma) 1); -by (blast_tac (claset() addDs [leadsToD] - addIs [leadsTo_Union,unionp]) 3); -by (blast_tac (claset() addIs [leadsTo_Trans,ensuresp]) 2); -by (blast_tac (claset() addIs [conjI,leadsTo_refl,cond] - addDs [leadsToD]) 1); +by (blast_tac (claset() addDs [leadsToD2] + addIs [leadsTo_Union,union_prem]) 3); +by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2); +by (blast_tac (claset() addIs [leadsTo_refl,zb_prem] + addDs [leadsToD2]) 1); qed "leadsTo_induct_pre"; - -Goal -"[| F : A leadsTo A'; A'<=B'; B':condition |]\ -\ ==> F : A leadsTo B'"; -by (blast_tac (claset() addIs [subset_imp_leadsTo, - leadsTo_Trans] - addDs [leadsToD]) 1); -qed "leadsTo_weaken_R"; - - -Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; -by (blast_tac (claset() - addIs [leadsTo_Trans, subset_imp_leadsTo] - addDs [leadsToD]) 1); -qed_spec_mp "leadsTo_weaken_L"; - -(*Distributes over binary unions*) -Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)"; -by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); -qed "leadsTo_Un_distrib"; - -Goal "[| F:program; B:condition |] \ -\==> F : (UN i:I. A(i)) leadsTo B <-> (ALL i : I. F : (A(i)) leadsTo B)"; -by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); -qed "leadsTo_UN_distrib"; - -Goal "[| F:program; B:condition |] \ -\==> F : (Union(S)) leadsTo B <-> (ALL A:S. F : A leadsTo B)"; -by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); -qed "leadsTo_Union_distrib"; - -Goal -"[| F : A leadsTo A'; B<=A; A'<=B'; B':condition |] \ -\ ==> F : B leadsTo B'"; -by (subgoal_tac "B:condition & A':condition" 1); -by (force_tac (claset() addSDs [leadsToD], - simpset() addsimps [condition_def]) 2); -by (blast_tac (claset() - addIs [leadsTo_weaken_R, leadsTo_weaken_L, leadsTo_Trans]) 1); -qed "leadsTo_weaken"; - -(*Set difference: maybe combine with leadsTo_weaken_L?*) -Goal "[| F : (A-B) leadsTo C; F : B leadsTo C|] ==> F : A leadsTo C"; -by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken] - addDs [leadsToD]) 1); -qed "leadsTo_Diff"; - - -Goal "[| ALL i:I. F : (A(i)) leadsTo (A'(i)); F:program |] \ -\ ==> F:(UN i:I. A(i)) leadsTo (UN i:I. A'(i))"; -by (rtac leadsTo_Union 1); -by (ALLGOALS(Clarify_tac)); -by (REPEAT(blast_tac (claset() - addIs [leadsTo_weaken_R] addDs [leadsToD]) 1)); -qed "leadsTo_UN_UN"; - -(*Binary union version*) -Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \ -\ ==> F : (A Un B) leadsTo (A' Un B')"; -by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R] - addDs [leadsToD]) 1); -qed "leadsTo_Un_Un"; - - -(** The cancellation law **) - -Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \ -\ ==> F : A leadsTo (A' Un B')"; -by (blast_tac (claset() - addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl] - addDs [leadsToD]) 1); -qed "leadsTo_cancel2"; - -Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \ -\ ==> F : A leadsTo (A' Un B')"; -by (rtac leadsTo_cancel2 1); -by (assume_tac 2); -by (blast_tac (claset() addIs [leadsTo_weaken_R] - addDs [leadsToD]) 1); -qed "leadsTo_cancel_Diff2"; - - -Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \ -\ ==> F : A leadsTo (B' Un A')"; -by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); -by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); -qed "leadsTo_cancel1"; - -Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \ -\ ==> F : A leadsTo (B' Un A')"; -by (rtac leadsTo_cancel1 1); -by (assume_tac 2); -by (blast_tac (claset() - addIs [leadsTo_weaken_R] - addDs [leadsToD]) 1); -qed "leadsTo_cancel_Diff1"; - (** The impossibility law **) - Goal "F : A leadsTo 0 ==> A=0"; by (etac leadsTo_induct_pre 1); -by (rewrite_goals_tac - [ensures_def, constrains_def, transient_def]); -by Auto_tac; -by (auto_tac (claset() addSDs [Acts_type], - simpset() addsimps - [actionSet_def, condition_def])); -by (blast_tac (claset() addSDs [bspec]) 1); +by (auto_tac (claset(), simpset() addsimps + [ensures_def, constrains_def, transient_def, st_set_def])); +by (dtac bspec 1); +by (REPEAT(Blast_tac 1)); qed "leadsTo_empty"; - - +Addsimps [leadsTo_empty]; (** PSP: Progress-Safety-Progress **) (*Special case of PSP: Misra's "stable conjunction"*) Goalw [stable_def] - "[| F : A leadsTo A'; F : stable(B) |] ==> \ -\ F:(A Int B) leadsTo (A' Int B)"; + "[| F : A leadsTo A'; F : stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"; by (etac leadsTo_induct 1); by (rtac leadsTo_Union_Int 3); -by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); +by (ALLGOALS(Asm_simp_tac)); +by (REPEAT(blast_tac (claset() addDs [constrainsD2]) 3)); by (blast_tac (claset() addIs [leadsTo_Trans]) 2); by (rtac leadsTo_Basis 1); by (asm_full_simp_tac (simpset() @@ -461,27 +440,22 @@ qed "psp_stable"; -Goal - "[| F : A leadsTo A'; F : stable(B) |] \ -\ ==> F : (B Int A) leadsTo (B Int A')"; +Goal "[|F: A leadsTo A'; F : stable(B) |]==>F: (B Int A) leadsTo (B Int A')"; by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); qed "psp_stable2"; - -Goalw [ensures_def, constrains_def] - "[| F : A ensures A'; F : B co B' |] \ -\ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"; +Goalw [ensures_def, constrains_def, st_set_def] +"[| F: A ensures A'; F: B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"; (*speeds up the proof*) by (Clarify_tac 1); by (blast_tac (claset() addIs [transient_strengthen]) 1); qed "psp_ensures"; -Goal "[| F : A leadsTo A'; F : B co B' |] \ -\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"; -by (subgoal_tac "F:program & A:condition & \ - \ A':condition & B:condition & B':condition" 1); -by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2); +Goal +"[|F:A leadsTo A'; F: B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"; +by (subgoal_tac "F:program & st_set(A) & st_set(A')& st_set(B)" 1); +by (blast_tac (claset() addSDs [constrainsD2, leadsToD2]) 2); by (etac leadsTo_induct 1); by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); (*Transitivity case has a delicate argument involving "cancellation"*) @@ -491,34 +465,32 @@ by (blast_tac (claset() addIs [leadsTo_weaken_L] addDs [constrains_imp_subset]) 2); (*Basis case*) -by (blast_tac (claset() addIs [psp_ensures]) 1); +by (blast_tac (claset() addIs [psp_ensures, leadsTo_Basis]) 1); qed "psp"; -Goal "[| F : A leadsTo A'; F : B co B' |] \ +Goal "[| F : A leadsTo A'; F : B co B'; st_set(B') |] \ \ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); qed "psp2"; - - Goalw [unless_def] - "[| F : A leadsTo A'; F : B unless B' |] \ + "[| F : A leadsTo A'; F : B unless B'; st_set(B); st_set(B') |] \ \ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; -by (subgoal_tac "F:program & A:condition & A':condition &\ - \ B:condition & B':condition" 1); -by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2); +by (subgoal_tac "st_set(A)&st_set(A')" 1); +by (blast_tac (claset() addDs [leadsToD2]) 2); by (dtac psp 1); by (assume_tac 1); -by (blast_tac (claset() addIs [leadsTo_weaken]) 1); +by (Blast_tac 1); +by (REPEAT(blast_tac (claset() addIs [leadsTo_weaken]) 1)); qed "psp_unless"; -(*** Proving the induction rules ***) +(*** Proving the wf induction rules ***) (** The most general rule: r is any wf relation; f is any variant function **) Goal "[| wf(r); \ \ m:I; \ \ field(r)<=I; \ -\ F:program; B:condition;\ +\ F:program; st_set(B);\ \ ALL m:I. F : (A Int f-``{m}) leadsTo \ \ ((A Int f-``(converse(r)``{m})) Un B) |] \ \ ==> F : (A Int f-``{m}) leadsTo B"; @@ -528,15 +500,14 @@ by (stac vimage_eq_UN 2); by (asm_simp_tac (simpset() addsimps [Int_UN_distrib]) 2); by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); -by (case_tac "converse(r)``{x}=0" 1); -by (auto_tac (claset() addSEs [not_emptyE] addSIs [leadsTo_UN], simpset())); +by (auto_tac (claset() addIs [leadsTo_UN], simpset())); qed "lemma1"; (** Meta or object quantifier ? **) Goal "[| wf(r); \ \ field(r)<=I; \ \ A<=f-``I;\ -\ F:program; A:condition; B:condition; \ +\ F:program; st_set(A); st_set(B); \ \ ALL m:I. F : (A Int f-``{m}) leadsTo \ \ ((A Int f-``(converse(r)``{m})) Un B) |] \ \ ==> F : A leadsTo B"; @@ -558,7 +529,7 @@ Goalw [field_def] "field(less_than(nat)) = nat"; by (simp_tac (simpset() addsimps [less_than_equals]) 1); by (rtac equalityI 1); -by (force_tac (claset() addSEs [rangeE], simpset()) 1); +by (force_tac (claset(), simpset()) 1); by (Clarify_tac 1); by (thin_tac "x~:range(?y)" 1); by (etac nat_induct 1); @@ -571,7 +542,7 @@ (*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) Goal "[| A<=f-``nat;\ -\ F:program; A:condition; B:condition; \ +\ F:program; st_set(A); st_set(B); \ \ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f-``lessThan(m,nat)) Un B) |] \ \ ==> F : A leadsTo B"; by (res_inst_tac [("A1", "nat")] @@ -584,36 +555,47 @@ (simpset() addsimps [rewrite_rule [vimage_def] Image_inverse_less_than]))); qed "lessThan_induct"; - (*** wlt ****) (*Misra's property W3*) -Goalw [wlt_def] -"[| F:program; B:condition |] ==> F:wlt(F, B) leadsTo B"; -by (blast_tac (claset() addSIs [leadsTo_Union]) 1); -qed "wlt_leadsTo"; +Goalw [wlt_def] "wlt(F,B) <=state"; +by Auto_tac; +qed "wlt_type"; + +Goalw [st_set_def] "st_set(wlt(F, B))"; +by (resolve_tac [wlt_type] 1); +qed "wlt_st_set"; +AddIffs [wlt_st_set]; + +Goalw [wlt_def] "F:wlt(F, B) leadsTo B <-> (F:program & st_set(B))"; +by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1); +qed "wlt_leadsTo_iff"; + +(* [| F:program; st_set(B) |] ==> F:wlt(F, B) leadsTo B *) +bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2)); Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)"; -by (blast_tac (claset() addSIs [leadsTo_Union] - addDs [leadsToD]) 1); +by (forward_tac [leadsToD2] 1); +by (auto_tac (claset(), simpset() addsimps [st_set_def])); qed "leadsTo_subset"; (*Misra's property W2*) -Goal "[| F:program; B:condition |] ==> \ -\ F : A leadsTo B <-> (A <= wlt(F,B))"; -by (blast_tac (claset() - addSIs [leadsTo_subset, wlt_leadsTo RS leadsTo_weaken_L]) 1); +Goal "F : A leadsTo B <-> (A <= wlt(F,B) & F:program & st_set(B))"; +by Auto_tac; +by (REPEAT(blast_tac (claset() addDs [leadsToD2,leadsTo_subset] + addIs [leadsTo_weaken_L, wlt_leadsTo]) 1)); qed "leadsTo_eq_subset_wlt"; (*Misra's property W4*) -Goal "[| F:program; B:condition |] ==> B <= wlt(F,B)"; +Goal "[| F:program; st_set(B) |] ==> B <= wlt(F,B)"; +by (rtac leadsTo_subset 1); by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS iff_sym, subset_imp_leadsTo]) 1); qed "wlt_increasing"; (*Used in the Trans case below*) -Goalw [constrains_def] +Goalw [constrains_def, st_set_def] "[| B <= A2; \ \ F : (A1 - B) co (A1 Un B); \ \ F : (A2 - C) co (A2 Un C) |] \ @@ -622,16 +604,14 @@ by (Blast_tac 1); qed "lemma1"; - - (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) (* slightly different from the HOL one: B here is bounded *) Goal "F : A leadsTo A' \ -\ ==> EX B:condition. A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')"; -by (forward_tac [leadsToD] 1); +\ ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')"; +by (forward_tac [leadsToD2] 1); by (etac leadsTo_induct 1); (*Basis*) -by (blast_tac (claset() addDs [ensuresD, constrainsD2]) 1); +by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1); (*Trans*) by (Clarify_tac 1); by (res_inst_tac [("x", "Ba Un Bb")] bexI 1); @@ -640,29 +620,28 @@ by (Blast_tac 1); (*Union*) by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1); -by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:condition. A<=Ba & \ +by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:Pow(state). A<=Ba & \ \ F:Ba leadsTo B & F:Ba - B co Ba Un B})" 1); by (rtac AC_ball_Pi 2); -by (Clarify_tac 2); -by (rotate_tac 3 2); -by (blast_tac (claset() addSDs [bspec]) 2); -by (Clarify_tac 1); +by (ALLGOALS(Clarify_tac)); +by (rotate_tac 1 2); +by (dres_inst_tac [("x", "x")] bspec 2); +by (REPEAT(Blast_tac 2)); by (res_inst_tac [("x", "UN A:S. y`A")] bexI 1); by Safe_tac; by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3); by (rtac leadsTo_Union 2); -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [condition_def]) 7); -by (asm_full_simp_tac (simpset() addsimps [condition_def]) 6); -by (REPEAT(blast_tac (claset() addDs [apply_type]) 1)); +by (blast_tac (claset() addSDs [apply_type]) 5); +by (ALLGOALS(Asm_full_simp_tac)); +by (REPEAT(force_tac (claset() addSDs [apply_type], simpset()) 1)); qed "leadsTo_123"; (*Misra's property W5*) -Goal "[| F:program; B:condition |] ==>F : (wlt(F, B) - B) co (wlt(F,B))"; +Goal "[| F:program; st_set(B) |] ==>F : (wlt(F, B) - B) co (wlt(F,B))"; by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); by (assume_tac 1); -by (assume_tac 1); +by (Blast_tac 1); by (Clarify_tac 1); by (subgoal_tac "Ba = wlt(F,B)" 1); by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); @@ -671,63 +650,49 @@ addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1); qed "wlt_constrains_wlt"; -Goalw [wlt_def, condition_def] - "wlt(F,B):condition"; -by Auto_tac; -qed "wlt_in_condition"; - (*** Completion: Binary and General Finite versions ***) Goal "[| W = wlt(F, (B' Un C)); \ \ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ \ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \ \ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; -by (subgoal_tac "W:condition" 1); -by (blast_tac (claset() addIs [wlt_in_condition]) 2); +by (subgoal_tac "st_set(C)&st_set(W)&st_set(W-C)&st_set(A')&st_set(A)\ +\ & st_set(B) & st_set(B') & F:program" 1); +by (Asm_simp_tac 2); +by (blast_tac (claset() addSDs [leadsToD2]) 2); by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1); by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] - MRS constrains_Un RS constrains_weaken] - addDs [leadsToD, constrainsD2]) 2); + MRS constrains_Un RS constrains_weaken]) 2); by (subgoal_tac "F : (W-C) co W" 1); -by (subgoals_tac ["F:program", "(B' Un C):condition"] 2); -by (rotate_tac ~2 2); -by (asm_full_simp_tac - (simpset() addsimps - [wlt_increasing RS (subset_Un_iff2 RS iffD1), Un_assoc]) 2); -by (REPEAT(blast_tac (claset() addDs [leadsToD, constrainsD]) 2)); +by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS + (subset_Un_iff2 RS iffD1), Un_assoc]) 2); by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1); -by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken] - addDs [leadsToD, constrainsD2]) 2); -(** LEVEL 6 **) +by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); +(** LEVEL 9 **) by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); -by (subgoal_tac "A' Int W Un C:condition & A' Int B' Un C:condition" 2); by (rtac leadsTo_Un_duplicate2 2); -by (blast_tac (claset() - addIs [leadsTo_Un_Un, wlt_leadsTo RS - psp2 RS leadsTo_weaken,leadsTo_refl] - addDs [leadsToD, constrainsD]) 2); -by (thin_tac "W=wlt(F, B' Un C)" 2); -by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2); +by (rtac leadsTo_Un_Un 2); +by (blast_tac (claset() addIs [leadsTo_refl]) 3); +by (res_inst_tac [("A'1", "B' Un C")] (wlt_leadsTo RS psp2 RS leadsTo_weaken) 2); +by (REPEAT(Blast_tac 2)); +(** LEVEL 17 **) by (dtac leadsTo_Diff 1); -by (blast_tac (claset() addIs [subset_imp_leadsTo] - addDs [leadsToD, constrainsD2]) 1); +by (blast_tac (claset() addIs [subset_imp_leadsTo] + addDs [leadsToD2, constrainsD2]) 1); +by (force_tac (claset(), simpset() addsimps [st_set_def]) 1); by (subgoal_tac "A Int B <= A Int W" 1); by (blast_tac (claset() addSDs [leadsTo_subset] addSIs [subset_refl RS Int_mono]) 2); -(** To speed the proof **) -by (subgoal_tac "A Int B :condition & A \ - \ Int W :condition & A' Int B' Un C:condition" 1); -by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo] - addDs [leadsToD, constrainsD2]) 1); -by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 1); -bind_thm("completion", refl RS result()); +by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); +qed "completion_aux"; +bind_thm("completion", refl RS completion_aux); -Goal "[| I:Fin(X); F:program; C:condition |] ==> \ +Goal "[| I:Fin(X); F:program; st_set(C) |] ==> \ \(ALL i:I. F : (A(i)) leadsTo (A'(i) Un C)) --> \ \ (ALL i:I. F : (A'(i)) co (A'(i) Un C)) --> \ \ F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; by (etac Fin_induct 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [Inter_0])); by (case_tac "y=0" 1); by Auto_tac; by (etac not_emptyE 1); @@ -746,9 +711,11 @@ val prems = Goal "[| I:Fin(X); \ \ !!i. i:I ==> F : A(i) leadsTo (A'(i) Un C); \ -\ !!i. i:I ==> F : A'(i) co (A'(i) Un C); F:program; C:condition |] \ +\ !!i. i:I ==> F : A'(i) co (A'(i) Un C); F:program; st_set(C)|] \ \ ==> F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; -by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); +by (resolve_tac [lemma RS mp RS mp] 1); +by (resolve_tac prems 3); +by (REPEAT(blast_tac (claset() addIs prems) 1)); qed "finite_completion"; Goalw [stable_def] @@ -756,21 +723,25 @@ \ F : B leadsTo B'; F : stable(B') |] \ \ ==> F : (A Int B) leadsTo (A' Int B')"; by (res_inst_tac [("C1", "0")] (completion RS leadsTo_weaken_R) 1); -by (REPEAT(blast_tac (claset() addDs [leadsToD, constrainsD2]) 5)); +by (REPEAT(blast_tac (claset() addDs [leadsToD2, constrainsD2]) 5)); by (ALLGOALS(Asm_full_simp_tac)); qed "stable_completion"; -val prems = Goalw [stable_def] +val major::prems = Goalw [stable_def] "[| I:Fin(X); \ -\ ALL i:I. F : A(i) leadsTo A'(i); \ -\ ALL i:I. F: stable(A'(i)); F:program |] \ +\ (!!i. i:I ==> F : A(i) leadsTo A'(i)); \ +\ (!!i. i:I ==> F: stable(A'(i))); F:program |] \ \ ==> F : (INT i:I. A(i)) leadsTo (INT i:I. A'(i))"; -by (subgoal_tac "(INT i:I. A'(i)):condition" 1); -by (blast_tac (claset() addDs [leadsToD, constrainsD2]) 2); +by (cut_facts_tac [major] 1); +by (subgoal_tac "st_set(INT i:I. A'(i))" 1); +by (blast_tac (claset() addDs [leadsToD2]@prems) 2); by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1); -by (assume_tac 7); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS (Blast_tac)); +by (Asm_simp_tac 1); +by (assume_tac 6); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems))); +by (resolve_tac prems 2); +by (resolve_tac prems 1); +by Auto_tac; qed "finite_stable_completion"; diff -r 13909cb72129 -r ed2893765a08 src/ZF/UNITY/WFair.thy --- a/src/ZF/UNITY/WFair.thy Wed Nov 14 23:22:43 2001 +0100 +++ b/src/ZF/UNITY/WFair.thy Thu Nov 15 15:07:16 2001 +0100 @@ -13,11 +13,11 @@ WFair = UNITY + constdefs - (*This definition specifies weak fairness. The rest of the theory + (* This definition specifies weak fairness. The rest of the theory is generic to all forms of fairness.*) transient :: "i=>i" - "transient(A) =={F:program. (EX act: Acts(F). - A<= domain(act) & act``A <= state-A) & A:condition}" + "transient(A) =={F:program. (EX act: Acts(F). A<=domain(act) & + act``A <= state-A) & st_set(A)}" ensures :: "[i,i] => i" (infixl 60) "A ensures B == ((A-B) co (A Un B)) Int transient(A-B)" @@ -25,31 +25,29 @@ consts (*LEADS-TO constant for the inductive definition*) - leads :: "i=>i" + leads :: "[i, i]=>i" -inductive (* All typing conidition `A:condition' will desapear - in the dervied rules *) +inductive domains - "leads(F)" <= "condition*condition" + "leads(D, F)" <= "Pow(D)*Pow(D)" intrs - Basis "[| F:A ensures B; A:condition; B:condition |] ==> :leads(F)" - Trans "[| : leads(F); : leads(F) |] ==> :leads(F)" - Union "[| S:Pow({A:S. :leads(F)}); - B:condition; S:Pow(condition) |] ==> - :leads(F)" + Basis "[| F:A ensures B; A:Pow(D); B:Pow(D) |] ==> :leads(D, F)" + Trans "[| : leads(D, F); : leads(D, F) |] ==> :leads(D, F)" + Union "[| S:Pow({A:S. :leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==> + :leads(D, F)" monos Pow_mono - type_intrs "[UnionI, Union_in_conditionI, PowI]" + type_intrs "[Union_PowI, UnionI, PowI]" constdefs - (*visible version of the LEADS-TO relation*) + (* The Visible version of the LEADS-TO relation*) leadsTo :: "[i, i] => i" (infixl 60) - "A leadsTo B == {F:program. :leads(F)}" + "A leadsTo B == {F:program. :leads(state, F)}" - (*wlt F B is the largest set that leads to B*) + (* wlt(F, B) is the largest set that leads to B*) wlt :: "[i, i] => i" - "wlt(F, B) == Union({A:condition. F: A leadsTo B})" + "wlt(F, B) == Union({A:Pow(state). F: A leadsTo B})" syntax (xsymbols) "op leadsTo" :: "[i, i] => i" (infixl "\\" 60)