--- 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); <s,t> : 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];
+
--- 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
--- 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. <s,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. <s,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); <s,s'>: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); <s,s'>: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. <a,f`s>: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. <a,f`s>: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, {<m,n>: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)),
--- 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. <z, f`s>:r}))}"
-
+ (* Increasing is the weak from of increasing *)
+ Increasing :: [i,i, i] => i
+ "Increasing(A, r, f) == INT a:A. Stable({s:state. <a, f`s>:r})"
end
--- 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";
--- 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})}"
--- 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";
--- 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*)
--- 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";
--- 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 **)
--- 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=<c,c>)";
-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];
--- 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
--- 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)]);
--- 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 " \\<longmapsto>w " 60)
--- 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); <s,s'>: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. <z, f`s>: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. <a, f`s>: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, {<m,n>: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";
--- 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 == {<init, acts, allowed>:condition*actionSet*actionSet.
- Id:acts & Id:allowed}"
+ "program == {<init, acts, allowed>:
+ 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) ==
- <init Int state, cons(Id, acts Int action), cons(Id, allowed Int action)>"
+ <init Int state, cons(id(state), acts Int Pow(state*state)),
+ cons(id(state), allowed Int Pow(state*state))>"
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. <a, f`s>: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 == {<i,j>: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. <z, f`s>: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
--- 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";
+
--- 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 ("\\<bottom>")
"op Join" :: [i, i] => i (infixl "\\<squnion>" 65)
"@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10)
--- 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";
--- 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 |] ==> <A,B>:leads(F)"
- Trans "[| <A,B> : leads(F); <B,C> : leads(F) |] ==> <A,C>:leads(F)"
- Union "[| S:Pow({A:S. <A, B>:leads(F)});
- B:condition; S:Pow(condition) |] ==>
- <Union(S),B>:leads(F)"
+ Basis "[| F:A ensures B; A:Pow(D); B:Pow(D) |] ==> <A,B>:leads(D, F)"
+ Trans "[| <A,B> : leads(D, F); <B,C> : leads(D, F) |] ==> <A,C>:leads(D, F)"
+ Union "[| S:Pow({A:S. <A, B>:leads(D, F)}); B:Pow(D); S:Pow(Pow(D)) |] ==>
+ <Union(S),B>: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. <A,B>:leads(F)}"
+ "A leadsTo B == {F:program. <A,B>: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 "\\<longmapsto>" 60)