--- a/src/ZF/IsaMakefile Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/IsaMakefile Mon Mar 28 16:19:56 2005 +0200
@@ -115,15 +115,13 @@
ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
- UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
- UNITY/FP.thy UNITY/Guar.thy \
- UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.thy \
- UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \
+ UNITY/Comp.thy UNITY/Constrains.thy UNITY/FP.thy\
+ UNITY/GenPrefix.thy UNITY/Guar.thy UNITY/Mutex.thy UNITY/State.thy \
+ UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \
UNITY/AllocBase.thy UNITY/AllocImpl.thy\
UNITY/ClientImpl.thy UNITY/Distributor.thy\
UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\
- UNITY/Monotonicity.thy UNITY/MultisetSum.thy\
- UNITY/WFair.ML UNITY/WFair.thy
+ UNITY/Monotonicity.thy UNITY/MultisetSum.thy UNITY/WFair.thy
@$(ISATOOL) usedir $(OUT)/ZF UNITY
--- a/src/ZF/UNITY/ClientImpl.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Mon Mar 28 16:19:56 2005 +0200
@@ -9,13 +9,6 @@
theory ClientImpl = AllocBase + Guar:
-(*move to Constrains.thy when the latter is converted to Isar format*)
-method_setup constrains = {*
- Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
- "for proving safety properties"
-
consts
ask :: i (* input history: tokens requested *)
giv :: i (* output history: tokens granted *)
--- a/src/ZF/UNITY/Constrains.ML Sat Mar 26 18:20:29 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,461 +0,0 @@
-(* Title: ZF/UNITY/Constrains.ML
- ID: $Id \\<in> Constrains.ML,v 1.10 2003/06/20 10:10:45 paulson Exp $
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-Safety relations \\<in> restricted to the set of reachable states.
-
-Proofs ported from HOL.
-*)
-
-(*** traces and reachable ***)
-
-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";
-
-Goalw [st_set_def] "st_set(reachable(F))";
-by (rtac reachable_type 1);
-qed "st_set_reachable";
-AddIffs [st_set_reachable];
-
-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 "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 \\<in> program ==> reachable(F)={s \\<in> state. \\<exists>evs. <s,evs>:traces(Init(F), Acts(F))}";
-by (rtac equalityI 1);
-by Safe_tac;
-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)));
-qed "reachable_equiv_traces";
-
-Goal "Init(F) <= reachable(F)";
-by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "Init_into_reachable";
-
-Goal "[| F \\<in> program; G \\<in> program; \
-\ Acts(G) <= Acts(F) |] ==> G \\<in> stable(reachable(F))";
-by (blast_tac (claset()
- addIs [stableI, constrainsI, st_setI,
- reachable_type RS subsetD] @ reachable.intrs) 1);
-qed "stable_reachable";
-
-AddSIs [stable_reachable];
-Addsimps [stable_reachable];
-
-(*The set of all reachable states is an invariant...*)
-Goalw [invariant_def, initially_def]
- "F \\<in> program ==> F \\<in> invariant(reachable(F))";
-by (blast_tac (claset() addIs [reachable_type RS subsetD]@reachable.intrs) 1);
-qed "invariant_reachable";
-
-(*...in fact the strongest invariant!*)
-Goal "F \\<in> 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));
-qed "invariant_includes_reachable";
-
-(*** Co ***)
-
-Goal "F \\<in> 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 \\<in> 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);
-qed "Constrains_eq_constrains";
-val Constrains_def2 = Constrains_eq_constrains RS eq_reflection;
-
-Goalw [Constrains_def]
- "F \\<in> A co A' ==> F \\<in> 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 \\<in> Acts(F); <s,s'>:act; s \\<in> A |] ==> s':A'); F \\<in> program|]==>F \\<in> 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]
- "A Co B <= program";
-by (Blast_tac 1);
-qed "Constrains_type";
-
-Goal "F \\<in> 0 Co B <-> F \\<in> 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 \\<in> A Co state <-> F \\<in> 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 \\<in> A Co A'; A'<=B' |] ==> F \\<in> A Co B'";
-by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
-qed "Constrains_weaken_R";
-
-Goalw [Constrains_def2]
- "[| F \\<in> A Co A'; B<=A |] ==> F \\<in> B Co A'";
-by (blast_tac (claset() addIs [constrains_weaken_L, st_set_subset]) 1);
-qed "Constrains_weaken_L";
-
-Goalw [Constrains_def2]
- "[| F \\<in> A Co A'; B<=A; A'<=B' |] ==> F \\<in> B Co B'";
-by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1);
-qed "Constrains_weaken";
-
-(** Union **)
-Goalw [Constrains_def2]
-"[| F \\<in> A Co A'; F \\<in> B Co B' |] ==> F \\<in> (A Un B) Co (A' Un B')";
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
-by (blast_tac (claset() addIs [constrains_Un]) 1);
-qed "Constrains_Un";
-
-val [major, minor] = Goalw [Constrains_def2]
-"[|(!!i. i \\<in> I==>F \\<in> A(i) Co A'(i)); F \\<in> program|] ==> F:(\\<Union>i \\<in> I. A(i)) Co (\\<Union>i \\<in> I. A'(i))";
-by (cut_facts_tac [minor] 1);
-by (auto_tac (claset() addDs [major]
- addIs [constrains_UN],
- simpset() delsimps UN_simps addsimps [Int_UN_distrib]));
-qed "Constrains_UN";
-
-(** Intersection **)
-
-Goalw [Constrains_def]
-"[| F \\<in> A Co A'; F \\<in> 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 \\<in> I ==>F \\<in> A(i) Co A'(i)); F \\<in> program |] \
-\ ==> F:(\\<Inter>i \\<in> I. A(i)) Co (\\<Inter>i \\<in> I. A'(i))";
-by (cut_facts_tac [minor] 1);
-by (asm_simp_tac (simpset() delsimps INT_simps
- addsimps [Constrains_def]@INT_extend_simps) 1);
-by (rtac constrains_INT 1);
-by (dtac major 1);
-by (auto_tac (claset(), simpset() addsimps [Constrains_def]));
-qed "Constrains_INT";
-
-Goalw [Constrains_def] "F \\<in> 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 \\<in> A Co B; F \\<in> B Co C |] ==> F \\<in> A Co C";
-by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
-qed "Constrains_trans";
-
-Goalw [Constrains_def2]
-"[| F \\<in> A Co (A' Un B); F \\<in> B Co B' |] ==> F \\<in> A Co (A' Un B')";
-by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 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 \\<in> stable(A) ==> F \\<in> Stable(A)";
-by (etac constrains_imp_Constrains 1);
-qed "stable_imp_Stable";
-
-Goal "[| F \\<in> Stable(A); A = B |] ==> F \\<in> Stable(B)";
-by (Blast_tac 1);
-qed "Stable_eq";
-
-Goal
-"F \\<in> Stable(A) <-> (F \\<in> 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 \\<in> A Co A ==> F \\<in> Stable(A)";
-by (assume_tac 1);
-qed "StableI";
-
-Goalw [Stable_def] "F \\<in> Stable(A) ==> F \\<in> A Co A";
-by (assume_tac 1);
-qed "StableD";
-
-Goalw [Stable_def]
- "[| F \\<in> Stable(A); F \\<in> Stable(A') |] ==> F \\<in> Stable(A Un A')";
-by (blast_tac (claset() addIs [Constrains_Un]) 1);
-qed "Stable_Un";
-
-Goalw [Stable_def]
- "[| F \\<in> Stable(A); F \\<in> Stable(A') |] ==> F \\<in> Stable (A Int A')";
-by (blast_tac (claset() addIs [Constrains_Int]) 1);
-qed "Stable_Int";
-
-Goalw [Stable_def]
- "[| F \\<in> Stable(C); F \\<in> A Co (C Un A') |] \
-\ ==> F \\<in> (C Un A) Co (C Un A')";
-by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
-qed "Stable_Constrains_Un";
-
-Goalw [Stable_def]
- "[| F \\<in> Stable(C); F \\<in> (C Int A) Co A' |] \
-\ ==> F \\<in> (C Int A) Co (C Int A')";
-by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
-qed "Stable_Constrains_Int";
-
-val [major,minor] = Goalw [Stable_def]
-"[| (!!i. i \\<in> I ==> F \\<in> Stable(A(i))); F \\<in> program |]==> F \\<in> Stable (\\<Union>i \\<in> I. A(i))";
-by (cut_facts_tac [minor] 1);
-by (blast_tac (claset() addIs [Constrains_UN,major]) 1);
-qed "Stable_UN";
-
-val [major,minor] = Goalw [Stable_def]
-"[|(!!i. i \\<in> I ==> F \\<in> Stable(A(i))); F \\<in> program |]==> F \\<in> Stable (\\<Inter>i \\<in> I. A(i))";
-by (cut_facts_tac [minor] 1);
-by (blast_tac (claset() addIs [Constrains_INT, major]) 1);
-qed "Stable_INT";
-
-Goal "F \\<in> program ==>F \\<in> Stable (reachable(F))";
-by (asm_simp_tac (simpset()
- addsimps [Stable_eq_stable, Int_absorb]) 1);
-qed "Stable_reachable";
-
-Goalw [Stable_def]
-"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 \\<forall>m ? Would make it harder to use
- in forward proof. ***)
-
-Goalw [Constrains_def]
-"[| \\<forall>m \\<in> M. F \\<in> ({s \\<in> A. x(s) = m}) Co (B(m)); F \\<in> program |] \
-\ ==> F \\<in> ({s \\<in> A. x(s):M}) Co (\\<Union>m \\<in> M. B(m))";
-by Auto_tac;
-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 A=state *)
-Goal
- "[| \\<forall>m \\<in> M. F \\<in> {s \\<in> state. x(s) = m} Co B(m); F \\<in> program |] \
-\ ==> F \\<in> {s \\<in> state. x(s):M} Co (\\<Union>m \\<in> M. B(m))";
-by (blast_tac (claset() addIs [Elimination]) 1);
-qed "Elimination2";
-
-(** Unless **)
-
-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]
-"[| Init(F)<=A; F \\<in> Stable(A) |] ==> F \\<in> Always(A)";
-by (forward_tac [Stable_type RS subsetD] 1);
-by Auto_tac;
-qed "AlwaysI";
-
-Goal "F \\<in> Always(A) ==> Init(F)<=A & F \\<in> Stable(A)";
-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 \\<in> Always(A) ==> reachable(F) <= A";
-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_def, invariant_def, Stable_def, stable_def]
- "F \\<in> invariant(A) ==> F \\<in> 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 \\<in> program. F \\<in> invariant(reachable(F) Int A)}";
-by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
- Constrains_def2, stable_def, initially_def]) 1);
-by (rtac equalityI 1);
-by (ALLGOALS(Clarify_tac));
-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 \\<in> program. reachable(F) <= A}";
-by (rtac equalityI 1);
-by (ALLGOALS(Clarify_tac));
-by (auto_tac (claset() addDs [invariant_includes_reachable],
- simpset() addsimps [subset_Int_iff, invariant_reachable,
- Always_eq_invariant_reachable]));
-qed "Always_eq_includes_reachable";
-
-Goalw [Always_def, initially_def] "Always(A) <= program";
-by Auto_tac;
-qed "Always_type";
-
-Goal "Always(state) = program";
-by (rtac equalityI 1);
-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 "F \\<in> program ==> F \\<in> Always(state)";
-by (auto_tac (claset() addDs [reachable_type RS subsetD], simpset()
- addsimps [Always_eq_includes_reachable]));
-qed "state_AlwaysI";
-
-Goal "st_set(A) ==> Always(A) = (\\<Union>I \\<in> 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 [invariant_type RS subsetD]) 1));
-qed "Always_eq_UN_invariant";
-
-Goal "[| F \\<in> Always(A); A <= B |] ==> F \\<in> Always(B)";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_weaken";
-
-
-(*** "Co" rules involving Always ***)
-val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp;
-
-Goal "F \\<in> Always(I) ==> (F:(I Int A) Co A') <-> (F \\<in> A Co A')";
-by (asm_simp_tac
- (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
- Constrains_def, Int_assoc RS sym]) 1);
-qed "Always_Constrains_pre";
-
-Goal "F \\<in> Always(I) ==> (F \\<in> A Co (I Int A')) <->(F \\<in> A Co A')";
-by (asm_simp_tac
- (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
- Constrains_eq_constrains, Int_assoc RS sym]) 1);
-qed "Always_Constrains_post";
-
-Goal "[| F \\<in> Always(I); F \\<in> (I Int A) Co A' |] ==> F \\<in> A Co A'";
-by (blast_tac (claset() addIs [Always_Constrains_pre RS iffD1]) 1);
-qed "Always_ConstrainsI";
-
-(* [| F \\<in> Always(I); F \\<in> A Co A' |] ==> F \\<in> 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 \\<in> Always(C); F \\<in> A Co A'; C Int B<=A; C Int A'<=B'|]==>F \\<in> B Co B'";
-by (rtac Always_ConstrainsI 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 "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 \\<in> I is need since \\<Inter>is formally not defined for I=0 *)
-Goal "i \\<in> I==>Always(\\<Inter>i \\<in> I. A(i)) = (\\<Inter>i \\<in> I. Always(A(i)))";
-by (rtac equalityI 1);
-by (auto_tac (claset(), simpset() addsimps
- [Inter_iff, Always_eq_includes_reachable]));
-qed "Always_INT_distrib";
-
-
-Goal "[| F \\<in> Always(A); F \\<in> Always(B) |] ==> F \\<in> 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 \\<in> Always(A) |] ==> (F \\<in> Always(C-A Un B)) <-> (F \\<in> Always(B))";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_Diff_Un_eq";
-
-(*Delete the nearest invariance assumption (which will be the second one
- used by Always_Int_I) *)
-val Always_thin =
- read_instantiate_sg (sign_of thy)
- [("V", "?F \\<in> Always(?A)")] thin_rl;
-
-(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
-val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
-
-(*Combines a list of invariance THEOREMS into one.*)
-val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
-
-(*To allow expansion of the program's definition when appropriate*)
-val program_defs_ref = ref ([]: thm list);
-
-(*proves "co" properties when the program is specified*)
-
-fun gen_constrains_tac(cs,ss) i =
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- REPEAT (etac Always_ConstrainsI 1
- ORELSE
- 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 (ss addsimps !program_defs_ref) 1,
- ALLGOALS (clarify_tac cs),
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS Clarify_tac,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_full_simp_tac ss),
- ALLGOALS (clarify_tac cs)]) i;
-
-fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
-
-(*For proving invariants*)
-fun always_tac i =
- rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
--- a/src/ZF/UNITY/Constrains.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/Constrains.thy Mon Mar 28 16:19:56 2005 +0200
@@ -1,14 +1,14 @@
-(* Title: ZF/UNITY/Constrains.thy
- ID: $Id$
+(* ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
-
-Safety relations: restricted to the set of reachable states.
-
-Theory ported from HOL.
*)
-Constrains = UNITY +
+header{*Weak Safety Properties*}
+
+theory Constrains
+imports UNITY
+
+begin
consts traces :: "[i, i] => i"
(* Initial states and program => (final state, reversed trace to it)...
the domain may also be state*list(state) *)
@@ -16,27 +16,27 @@
domains
"traces(init, acts)" <=
"(init Un (UN act:acts. field(act)))*list(UN act:acts. field(act))"
- intrs
+ intros
(*Initial trace is empty*)
- Init "s: init ==> <s,[]> : traces(init,acts)"
+ Init: "s: init ==> <s,[]> : traces(init,acts)"
- Acts "[| act:acts; <s,evs> : traces(init,acts); <s,s'>: act |]
+ Acts: "[| act:acts; <s,evs> : traces(init,acts); <s,s'>: act |]
==> <s', Cons(s,evs)> : traces(init, acts)"
- type_intrs "list.intrs@[UnI1, UnI2, UN_I, fieldI2, fieldI1]"
+ type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1
- consts reachable :: "i=>i"
+consts reachable :: "i=>i"
inductive
domains
"reachable(F)" <= "Init(F) Un (UN act:Acts(F). field(act))"
- intrs
- Init "s:Init(F) ==> s:reachable(F)"
+ intros
+ Init: "s:Init(F) ==> s:reachable(F)"
- Acts "[| act: Acts(F); s:reachable(F); <s,s'>: act |]
+ Acts: "[| act: Acts(F); s:reachable(F); <s,s'>: act |]
==> s':reachable(F)"
- type_intrs "[UnI1, UnI2, fieldI2, UN_I]"
+ type_intros UnI1 UnI2 fieldI2 UN_I
consts
@@ -44,10 +44,10 @@
op_Unless :: "[i, i] => i" (infixl "Unless" 60)
defs
- Constrains_def
+ Constrains_def:
"A Co B == {F:program. F:(reachable(F) Int A) co B}"
- Unless_def
+ Unless_def:
"A Unless B == (A-B) Co (A Un B)"
constdefs
@@ -57,5 +57,519 @@
Always :: "i => i"
"Always(A) == initially(A) Int Stable(A)"
+
+(*** traces and reachable ***)
+
+lemma reachable_type: "reachable(F) <= state"
+apply (cut_tac F = F in Init_type)
+apply (cut_tac F = F in Acts_type)
+apply (cut_tac F = F in reachable.dom_subset, blast)
+done
+
+lemma st_set_reachable: "st_set(reachable(F))"
+apply (unfold st_set_def)
+apply (rule reachable_type)
+done
+declare st_set_reachable [iff]
+
+lemma reachable_Int_state: "reachable(F) Int state = reachable(F)"
+by (cut_tac reachable_type, auto)
+declare reachable_Int_state [iff]
+
+lemma state_Int_reachable: "state Int reachable(F) = reachable(F)"
+by (cut_tac reachable_type, auto)
+declare state_Int_reachable [iff]
+
+lemma reachable_equiv_traces:
+"F \<in> program ==> reachable(F)={s \<in> state. \<exists>evs. <s,evs>:traces(Init(F), Acts(F))}"
+apply (rule equalityI, safe)
+apply (blast dest: reachable_type [THEN subsetD])
+apply (erule_tac [2] traces.induct)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros traces.intros)+
+done
+
+lemma Init_into_reachable: "Init(F) <= reachable(F)"
+by (blast intro: reachable.intros)
+
+lemma stable_reachable: "[| F \<in> program; G \<in> program;
+ Acts(G) <= Acts(F) |] ==> G \<in> stable(reachable(F))"
+apply (blast intro: stableI constrainsI st_setI
+ reachable_type [THEN subsetD] reachable.intros)
+done
+
+declare stable_reachable [intro!]
+declare stable_reachable [simp]
+
+(*The set of all reachable states is an invariant...*)
+lemma invariant_reachable:
+ "F \<in> program ==> F \<in> invariant(reachable(F))"
+apply (unfold invariant_def initially_def)
+apply (blast intro: reachable_type [THEN subsetD] reachable.intros)
+done
+
+(*...in fact the strongest invariant!*)
+lemma invariant_includes_reachable: "F \<in> invariant(A) ==> reachable(F) <= A"
+apply (cut_tac F = F in Acts_type)
+apply (cut_tac F = F in Init_type)
+apply (cut_tac F = F in reachable_type)
+apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def)
+apply (rule subsetI)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros)+
+done
+
+(*** Co ***)
+
+lemma constrains_reachable_Int: "F \<in> B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')"
+apply (frule constrains_type [THEN subsetD])
+apply (frule stable_reachable [OF _ _ subset_refl])
+apply (simp_all add: stable_def constrains_Int)
+done
+
+(*Resembles the previous definition of Constrains*)
+lemma Constrains_eq_constrains:
+"A Co B = {F \<in> program. F:(reachable(F) Int A) co (reachable(F) Int B)}"
+apply (unfold Constrains_def)
+apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD]
+ intro: constrains_weaken)
+done
+
+lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection]
+
+lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_weaken_L dest: constrainsD2)
+done
+
+lemma ConstrainsI:
+ "[|!!act s s'. [| act \<in> Acts(F); <s,s'>:act; s \<in> A |] ==> s':A';
+ F \<in> program|]
+ ==> F \<in> A Co A'"
+apply (auto simp add: Constrains_def constrains_def st_set_def)
+apply (blast dest: reachable_type [THEN subsetD])
+done
+
+lemma Constrains_type:
+ "A Co B <= program"
+apply (unfold Constrains_def, blast)
+done
+
+lemma Constrains_empty: "F \<in> 0 Co B <-> F \<in> program"
+by (auto dest: Constrains_type [THEN subsetD]
+ intro: constrains_imp_Constrains)
+declare Constrains_empty [iff]
+
+lemma Constrains_state: "F \<in> A Co state <-> F \<in> program"
+apply (unfold Constrains_def)
+apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains)
+done
+declare Constrains_state [iff]
+
+lemma Constrains_weaken_R:
+ "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
+apply (unfold Constrains_def2)
+apply (blast intro: constrains_weaken_R)
+done
+
+lemma Constrains_weaken_L:
+ "[| F \<in> A Co A'; B<=A |] ==> F \<in> B Co A'"
+apply (unfold Constrains_def2)
+apply (blast intro: constrains_weaken_L st_set_subset)
+done
+
+lemma Constrains_weaken:
+ "[| F \<in> A Co A'; B<=A; A'<=B' |] ==> F \<in> B Co B'"
+apply (unfold Constrains_def2)
+apply (blast intro: constrains_weaken st_set_subset)
+done
+
+(** Union **)
+lemma Constrains_Un:
+ "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A Un B) Co (A' Un B')"
+apply (unfold Constrains_def2, auto)
+apply (simp add: Int_Un_distrib)
+apply (blast intro: constrains_Un)
+done
+
+lemma Constrains_UN:
+ "[|(!!i. i \<in> I==>F \<in> A(i) Co A'(i)); F \<in> program|]
+ ==> F:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> I. A'(i))"
+by (auto intro: constrains_UN simp del: UN_simps
+ simp add: Constrains_def2 Int_UN_distrib)
+
+
+(** Intersection **)
+
+lemma Constrains_Int:
+ "[| F \<in> A Co A'; F \<in> B Co B'|]==> F:(A Int B) Co (A' Int B')"
+apply (unfold Constrains_def)
+apply (subgoal_tac "reachable (F) Int (A Int B) = (reachable (F) Int A) Int (reachable (F) Int B) ")
+apply (auto intro: constrains_Int)
+done
+
+lemma Constrains_INT:
+ "[| (!!i. i \<in> I ==>F \<in> A(i) Co A'(i)); F \<in> program |]
+ ==> F:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> I. A'(i))"
+apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps)
+apply (rule constrains_INT)
+apply (auto simp add: Constrains_def)
+done
+
+lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable(F) Int A <= A'"
+apply (unfold Constrains_def)
+apply (blast dest: constrains_imp_subset)
+done
+
+lemma Constrains_trans:
+ "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
+apply (unfold Constrains_def2)
+apply (blast intro: constrains_trans constrains_weaken)
+done
+
+lemma Constrains_cancel:
+"[| F \<in> A Co (A' Un B); F \<in> B Co B' |] ==> F \<in> A Co (A' Un B')"
+apply (unfold Constrains_def2)
+apply (simp (no_asm_use) add: Int_Un_distrib)
+apply (blast intro: constrains_cancel)
+done
+
+(*** Stable ***)
+(* Useful because there's no Stable_weaken. [Tanja Vos] *)
+
+lemma stable_imp_Stable:
+"F \<in> stable(A) ==> F \<in> Stable(A)"
+
+apply (unfold stable_def Stable_def)
+apply (erule constrains_imp_Constrains)
+done
+
+lemma Stable_eq: "[| F \<in> Stable(A); A = B |] ==> F \<in> Stable(B)"
+by blast
+
+lemma Stable_eq_stable:
+"F \<in> Stable(A) <-> (F \<in> stable(reachable(F) Int A))"
+apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2)
+done
+
+lemma StableI: "F \<in> A Co A ==> F \<in> Stable(A)"
+by (unfold Stable_def, assumption)
+
+lemma StableD: "F \<in> Stable(A) ==> F \<in> A Co A"
+by (unfold Stable_def, assumption)
+
+lemma Stable_Un:
+ "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable(A Un A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Un)
+done
+
+lemma Stable_Int:
+ "[| F \<in> Stable(A); F \<in> Stable(A') |] ==> F \<in> Stable (A Int A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Int)
+done
+
+lemma Stable_Constrains_Un:
+ "[| F \<in> Stable(C); F \<in> A Co (C Un A') |]
+ ==> F \<in> (C Un A) Co (C Un A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Un [THEN Constrains_weaken_R])
+done
+
+lemma Stable_Constrains_Int:
+ "[| F \<in> Stable(C); F \<in> (C Int A) Co A' |]
+ ==> F \<in> (C Int A) Co (C Int A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Int [THEN Constrains_weaken])
+done
+
+lemma Stable_UN:
+ "[| (!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
+ ==> F \<in> Stable (\<Union>i \<in> I. A(i))"
+apply (simp add: Stable_def)
+apply (blast intro: Constrains_UN)
+done
+
+lemma Stable_INT:
+ "[|(!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program |]
+ ==> F \<in> Stable (\<Inter>i \<in> I. A(i))"
+apply (simp add: Stable_def)
+apply (blast intro: Constrains_INT)
+done
+
+lemma Stable_reachable: "F \<in> program ==>F \<in> Stable (reachable(F))"
+apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb)
+done
+
+lemma Stable_type: "Stable(A) <= program"
+apply (unfold Stable_def)
+apply (rule Constrains_type)
+done
+
+(*** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of \<forall>m ? Would make it harder to use
+ in forward proof. ***)
+
+lemma Elimination:
+ "[| \<forall>m \<in> M. F \<in> ({s \<in> A. x(s) = m}) Co (B(m)); F \<in> program |]
+ ==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> M. B(m))"
+apply (unfold Constrains_def, auto)
+apply (rule_tac A1 = "reachable (F) Int A"
+ in UNITY.elimination [THEN constrains_weaken_L])
+apply (auto intro: constrains_weaken_L)
+done
+
+(* As above, but for the special case of A=state *)
+lemma Elimination2:
+ "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} Co B(m); F \<in> program |]
+ ==> F \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))"
+apply (blast intro: Elimination)
+done
+
+(** Unless **)
+
+lemma Unless_type: "A Unless B <=program"
+
+apply (unfold Unless_def)
+apply (rule Constrains_type)
+done
+
+(*** Specialized laws for handling Always ***)
+
+(** Natural deduction rules for "Always A" **)
+
+lemma AlwaysI:
+"[| Init(F)<=A; F \<in> Stable(A) |] ==> F \<in> Always(A)"
+
+apply (unfold Always_def initially_def)
+apply (frule Stable_type [THEN subsetD], auto)
+done
+
+lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)"
+by (simp add: Always_def initially_def)
+
+lemmas AlwaysE = AlwaysD [THEN conjE, standard]
+lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
+
+(*The set of all reachable states is Always*)
+lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) <= A"
+apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def)
+apply (rule subsetI)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros)+
+done
+
+lemma invariant_imp_Always:
+ "F \<in> invariant(A) ==> F \<in> Always(A)"
+apply (unfold Always_def invariant_def Stable_def stable_def)
+apply (blast intro: constrains_imp_Constrains)
+done
+
+lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always, standard]
+
+lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) Int A)}"
+apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
+apply (rule equalityI, auto)
+apply (blast intro: reachable.intros reachable_type)
+done
+
+(*the RHS is the traditional definition of the "always" operator*)
+lemma Always_eq_includes_reachable: "Always(A) = {F \<in> program. reachable(F) <= A}"
+apply (rule equalityI, safe)
+apply (auto dest: invariant_includes_reachable
+ simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable)
+done
+
+lemma Always_type: "Always(A) <= program"
+by (unfold Always_def initially_def, auto)
+
+lemma Always_state_eq: "Always(state) = program"
+apply (rule equalityI)
+apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD]
+ simp add: Always_eq_includes_reachable)
+done
+declare Always_state_eq [simp]
+
+lemma state_AlwaysI: "F \<in> program ==> F \<in> Always(state)"
+by (auto dest: reachable_type [THEN subsetD]
+ simp add: Always_eq_includes_reachable)
+
+lemma Always_eq_UN_invariant: "st_set(A) ==> Always(A) = (\<Union>I \<in> Pow(A). invariant(I))"
+apply (simp (no_asm) add: Always_eq_includes_reachable)
+apply (rule equalityI, auto)
+apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable]
+ rev_subsetD [OF _ invariant_includes_reachable]
+ dest: invariant_type [THEN subsetD])+
+done
+
+lemma Always_weaken: "[| F \<in> Always(A); A <= B |] ==> F \<in> Always(B)"
+by (auto simp add: Always_eq_includes_reachable)
+
+
+(*** "Co" rules involving Always ***)
+lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp]
+
+lemma Always_Constrains_pre: "F \<in> Always(I) ==> (F:(I Int A) Co A') <-> (F \<in> A Co A')"
+apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric])
+done
+
+lemma Always_Constrains_post: "F \<in> Always(I) ==> (F \<in> A Co (I Int A')) <->(F \<in> A Co A')"
+apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric])
+done
+
+lemma Always_ConstrainsI: "[| F \<in> Always(I); F \<in> (I Int A) Co A' |] ==> F \<in> A Co A'"
+by (blast intro: Always_Constrains_pre [THEN iffD1])
+
+(* [| F \<in> Always(I); F \<in> A Co A' |] ==> F \<in> A Co (I Int A') *)
+lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
+
+(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
+lemma Always_Constrains_weaken:
+"[|F \<in> Always(C); F \<in> A Co A'; C Int B<=A; C Int A'<=B'|]==>F \<in> B Co B'"
+apply (rule Always_ConstrainsI)
+apply (drule_tac [2] Always_ConstrainsD, simp_all)
+apply (blast intro: Constrains_weaken)
+done
+
+(** Conjoining Always properties **)
+lemma Always_Int_distrib: "Always(A Int B) = Always(A) Int Always(B)"
+by (auto simp add: Always_eq_includes_reachable)
+
+(* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *)
+lemma Always_INT_distrib: "i \<in> I==>Always(\<Inter>i \<in> I. A(i)) = (\<Inter>i \<in> I. Always(A(i)))"
+apply (rule equalityI)
+apply (auto simp add: Inter_iff Always_eq_includes_reachable)
+done
+
+
+lemma Always_Int_I: "[| F \<in> Always(A); F \<in> Always(B) |] ==> F \<in> Always(A Int B)"
+apply (simp (no_asm_simp) add: Always_Int_distrib)
+done
+
+(*Allows a kind of "implication introduction"*)
+lemma Always_Diff_Un_eq: "[| F \<in> Always(A) |] ==> (F \<in> Always(C-A Un B)) <-> (F \<in> Always(B))"
+by (auto simp add: Always_eq_includes_reachable)
+
+(*Delete the nearest invariance assumption (which will be the second one
+ used by Always_Int_I) *)
+lemmas Always_thin = thin_rl [of "F \<in> Always(A)", standard]
+
+ML
+{*
+val reachable_type = thm "reachable_type";
+val st_set_reachable = thm "st_set_reachable";
+val reachable_Int_state = thm "reachable_Int_state";
+val state_Int_reachable = thm "state_Int_reachable";
+val reachable_equiv_traces = thm "reachable_equiv_traces";
+val Init_into_reachable = thm "Init_into_reachable";
+val stable_reachable = thm "stable_reachable";
+val invariant_reachable = thm "invariant_reachable";
+val invariant_includes_reachable = thm "invariant_includes_reachable";
+val constrains_reachable_Int = thm "constrains_reachable_Int";
+val Constrains_eq_constrains = thm "Constrains_eq_constrains";
+val Constrains_def2 = thm "Constrains_def2";
+val constrains_imp_Constrains = thm "constrains_imp_Constrains";
+val ConstrainsI = thm "ConstrainsI";
+val Constrains_type = thm "Constrains_type";
+val Constrains_empty = thm "Constrains_empty";
+val Constrains_state = thm "Constrains_state";
+val Constrains_weaken_R = thm "Constrains_weaken_R";
+val Constrains_weaken_L = thm "Constrains_weaken_L";
+val Constrains_weaken = thm "Constrains_weaken";
+val Constrains_Un = thm "Constrains_Un";
+val Constrains_UN = thm "Constrains_UN";
+val Constrains_Int = thm "Constrains_Int";
+val Constrains_INT = thm "Constrains_INT";
+val Constrains_imp_subset = thm "Constrains_imp_subset";
+val Constrains_trans = thm "Constrains_trans";
+val Constrains_cancel = thm "Constrains_cancel";
+val stable_imp_Stable = thm "stable_imp_Stable";
+val Stable_eq = thm "Stable_eq";
+val Stable_eq_stable = thm "Stable_eq_stable";
+val StableI = thm "StableI";
+val StableD = thm "StableD";
+val Stable_Un = thm "Stable_Un";
+val Stable_Int = thm "Stable_Int";
+val Stable_Constrains_Un = thm "Stable_Constrains_Un";
+val Stable_Constrains_Int = thm "Stable_Constrains_Int";
+val Stable_UN = thm "Stable_UN";
+val Stable_INT = thm "Stable_INT";
+val Stable_reachable = thm "Stable_reachable";
+val Stable_type = thm "Stable_type";
+val Elimination = thm "Elimination";
+val Elimination2 = thm "Elimination2";
+val Unless_type = thm "Unless_type";
+val AlwaysI = thm "AlwaysI";
+val AlwaysD = thm "AlwaysD";
+val AlwaysE = thm "AlwaysE";
+val Always_imp_Stable = thm "Always_imp_Stable";
+val Always_includes_reachable = thm "Always_includes_reachable";
+val invariant_imp_Always = thm "invariant_imp_Always";
+val Always_reachable = thm "Always_reachable";
+val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable";
+val Always_eq_includes_reachable = thm "Always_eq_includes_reachable";
+val Always_type = thm "Always_type";
+val Always_state_eq = thm "Always_state_eq";
+val state_AlwaysI = thm "state_AlwaysI";
+val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
+val Always_weaken = thm "Always_weaken";
+val Int_absorb2 = thm "Int_absorb2";
+val Always_Constrains_pre = thm "Always_Constrains_pre";
+val Always_Constrains_post = thm "Always_Constrains_post";
+val Always_ConstrainsI = thm "Always_ConstrainsI";
+val Always_ConstrainsD = thm "Always_ConstrainsD";
+val Always_Constrains_weaken = thm "Always_Constrains_weaken";
+val Always_Int_distrib = thm "Always_Int_distrib";
+val Always_INT_distrib = thm "Always_INT_distrib";
+val Always_Int_I = thm "Always_Int_I";
+val Always_Diff_Un_eq = thm "Always_Diff_Un_eq";
+val Always_thin = thm "Always_thin";
+
+(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
+val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
+
+(*Combines a list of invariance THEOREMS into one.*)
+val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
+
+(*To allow expansion of the program's definition when appropriate*)
+val program_defs_ref = ref ([]: thm list);
+
+(*proves "co" properties when the program is specified*)
+
+fun gen_constrains_tac(cs,ss) i =
+ SELECT_GOAL
+ (EVERY [REPEAT (Always_Int_tac 1),
+ REPEAT (etac Always_ConstrainsI 1
+ ORELSE
+ 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 (ss addsimps !program_defs_ref) 1,
+ ALLGOALS (clarify_tac cs),
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS Clarify_tac,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_full_simp_tac ss),
+ ALLGOALS (clarify_tac cs)]) i;
+
+fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
+
+(*For proving invariants*)
+fun always_tac i =
+ rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
+*}
+
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
+ "for proving safety properties"
+
+
end
--- a/src/ZF/UNITY/GenPrefix.ML Sat Mar 26 18:20:29 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,690 +0,0 @@
-(* Title: ZF/UNITY/GenPrefix.ML
- ID: $Id \\<in> GenPrefix.ML,v 1.8 2003/06/20 16:13:16 paulson Exp $
- Author: Sidi O Ehmety, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-
-Charpentier's Generalized Prefix Relation
- <xs,ys>:gen_prefix(r)
- if ys = xs' @ zs where length(xs) = length(xs')
- and corresponding elements of xs, xs' are pairwise related by r
-
-Based on Lex/Prefix
-*)
-
-Goalw [refl_def]
- "[| refl(A, r); x \\<in> A |] ==> <x,x>:r";
-by Auto_tac;
-qed "reflD";
-
-(*** preliminary lemmas ***)
-
-Goal "xs \\<in> list(A) ==> <[], xs> \\<in> gen_prefix(A, r)";
-by (dtac (rotate_prems 1 gen_prefix.append) 1);
-by (rtac gen_prefix.Nil 1);
-by Auto_tac;
-qed "Nil_gen_prefix";
-Addsimps [Nil_gen_prefix];
-
-
-Goal "<xs,ys> \\<in> gen_prefix(A, r) ==> length(xs) \\<le> length(ys)";
-by (etac gen_prefix.induct 1);
-by (subgoal_tac "ys \\<in> list(A)" 3);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
- addIs [le_trans],
- simpset() addsimps [length_app]));
-qed "gen_prefix_length_le";
-
-
-Goal "[| <xs', ys'> \\<in> gen_prefix(A, r) |] \
-\ ==> (\\<forall>x xs. x \\<in> A --> xs'= Cons(x,xs) --> \
-\ (\\<exists>y ys. y \\<in> A & ys' = Cons(y,ys) &\
-\ <x,y>:r & <xs, ys> \\<in> gen_prefix(A, r)))";
-by (etac gen_prefix.induct 1);
-by (force_tac (claset() addIs [gen_prefix.append],
- simpset()) 3);
-by (REPEAT(Asm_simp_tac 1));
-val lemma = result();
-
-(*As usual converting it to an elimination rule is tiresome*)
-val major::prems =
-Goal "[| <Cons(x,xs), zs> \\<in> gen_prefix(A, r); \
-\ !!y ys. [|zs = Cons(y, ys); y \\<in> A; x \\<in> A; <x,y>:r; \
-\ <xs,ys> \\<in> gen_prefix(A, r) |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac [major] 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (etac ConsE 1);
-by (cut_facts_tac [major RS lemma] 1);
-by (Full_simp_tac 1);
-by (dtac mp 1);
-by (Asm_simp_tac 1);
-by (REPEAT (eresolve_tac [exE, conjE] 1));
-by (REPEAT (ares_tac prems 1));
-qed "Cons_gen_prefixE";
-AddSEs [Cons_gen_prefixE];
-
-Goal
-"(<Cons(x,xs),Cons(y,ys)> \\<in> gen_prefix(A, r)) \
-\ <-> (x \\<in> A & y \\<in> A & <x,y>:r & <xs,ys> \\<in> gen_prefix(A, r))";
-by (auto_tac (claset() addIs [gen_prefix.prepend], simpset()));
-qed"Cons_gen_prefix_Cons";
-AddIffs [Cons_gen_prefix_Cons];
-
-(** Monotonicity of gen_prefix **)
-
-Goal "r<=s ==> gen_prefix(A, r) <= gen_prefix(A, s)";
-by (Clarify_tac 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (etac rev_mp 1);
-by (etac gen_prefix.induct 1);
-by (auto_tac (claset() addIs
- [gen_prefix.append], simpset()));
-qed "gen_prefix_mono2";
-
-Goal "A<=B ==>gen_prefix(A, r) <= gen_prefix(B, r)";
-by (Clarify_tac 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (etac rev_mp 1);
-by (eres_inst_tac [("P", "y \\<in> list(A)")] rev_mp 1);
-by (eres_inst_tac [("P", "xa \\<in> list(A)")] rev_mp 1);
-by (etac gen_prefix.induct 1);
-by (Asm_simp_tac 1);
-by (Clarify_tac 1);
-by (REPEAT(etac ConsE 1));
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
- addIs [gen_prefix.append, list_mono RS subsetD],
- simpset()));
-qed "gen_prefix_mono1";
-
-Goal "[| A <= B; r <= s |] ==> gen_prefix(A, r) <= gen_prefix(B, s)";
-by (rtac subset_trans 1);
-by (rtac gen_prefix_mono1 1);
-by (rtac gen_prefix_mono2 2);
-by Auto_tac;
-qed "gen_prefix_mono";
-
-(*** gen_prefix order ***)
-
-(* reflexivity *)
-Goalw [refl_def] "refl(A, r) ==> refl(list(A), gen_prefix(A, r))";
-by Auto_tac;
-by (induct_tac "x" 1);
-by Auto_tac;
-qed "refl_gen_prefix";
-Addsimps [refl_gen_prefix RS reflD];
-
-(* Transitivity *)
-(* A lemma for proving gen_prefix_trans_comp *)
-
-Goal "xs \\<in> list(A) ==> \
-\ \\<forall>zs. <xs @ ys, zs> \\<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
-by (etac list.induct 1);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
-qed_spec_mp "append_gen_prefix";
-
-(* Lemma proving transitivity and more*)
-
-Goal "<x, y>: gen_prefix(A, r) ==> \
-\ (\\<forall>z \\<in> list(A). <y,z> \\<in> gen_prefix(A, s)--><x, z> \\<in> gen_prefix(A, s O r))";
-by (etac gen_prefix.induct 1);
-by (auto_tac (claset() addEs [ConsE], simpset() addsimps [Nil_gen_prefix]));
-by (subgoal_tac "ys \\<in> list(A)" 1);
-by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
-by (dres_inst_tac [("xs", "ys"), ("r", "s")] append_gen_prefix 1);
-by Auto_tac;
-qed_spec_mp "gen_prefix_trans_comp";
-
-Goal "trans(r) ==> r O r <= r";
-by (auto_tac (claset() addDs [transD], simpset()));
-qed "trans_comp_subset";
-
-Goal "trans(r) ==> trans(gen_prefix(A,r))";
-by (simp_tac (simpset() addsimps [trans_def]) 1);
-by (Clarify_tac 1);
-by (rtac (impOfSubs (trans_comp_subset RS gen_prefix_mono2)) 1);
- by (assume_tac 2);
-by (rtac gen_prefix_trans_comp 1);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
-qed_spec_mp "trans_gen_prefix";
-
-Goal
- "trans(r) ==> trans[list(A)](gen_prefix(A, r))";
-by (dres_inst_tac [("A", "A")] trans_gen_prefix 1);
-by (rewrite_goal_tac [trans_def, trans_on_def] 1);
-by (Blast_tac 1);
-qed "trans_on_gen_prefix";
-
-Goalw [prefix_def]
-"[| <x,y> \\<in> prefix(A); <y, z> \\<in> gen_prefix(A, r); r<=A*A |] \
-\ ==> <x, z> \\<in> gen_prefix(A, r)";
-by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")]
- (right_comp_id RS subst) 1);
-by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
- gen_prefix.dom_subset RS subsetD]) 1));
-qed_spec_mp "prefix_gen_prefix_trans";
-
-
-Goalw [prefix_def]
-"[| <x,y> \\<in> gen_prefix(A,r); <y, z> \\<in> prefix(A); r<=A*A |] \
-\ ==> <x, z> \\<in> gen_prefix(A, r)";
-by (res_inst_tac [("P", "%r. <x,z> \\<in> gen_prefix(A, r)")] (left_comp_id RS subst) 1);
-by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
- gen_prefix.dom_subset RS subsetD]) 1));
-qed_spec_mp "gen_prefix_prefix_trans";
-
-(** Antisymmetry **)
-
-Goal "n \\<in> nat ==> \\<forall>b \\<in> nat. n #+ b \\<le> n --> b = 0";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "nat_le_lemma";
-
-Goal "antisym(r) ==> antisym(gen_prefix(A, r))";
-by (simp_tac (simpset() addsimps [antisym_def]) 1);
-by (rtac (impI RS allI RS allI) 1);
-by (etac gen_prefix.induct 1);
-by (full_simp_tac (simpset() addsimps [antisym_def]) 2);
-by (Blast_tac 2);
-by (Blast_tac 1);
-(*append case is hardest*)
-by (Clarify_tac 1);
-by (subgoal_tac "length(zs) = 0" 1);
-by (subgoal_tac "ys \\<in> list(A)" 1);
-by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
-by (dres_inst_tac [("psi", "<ys @ zs, xs> \\<in> gen_prefix(A,r)")] asm_rl 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "length(ys @ zs) = length(ys) #+ length(zs) &ys \\<in> list(A)&xs \\<in> list(A)" 1);
-by (blast_tac (claset() addIs [length_app]
- addDs [gen_prefix.dom_subset RS subsetD]) 2);
-by (REPEAT (dtac gen_prefix_length_le 1));
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("j", "length(xs)")] le_trans 1);
-by (Blast_tac 1);
-by (auto_tac (claset() addIs [nat_le_lemma], simpset()));
-qed_spec_mp "antisym_gen_prefix";
-
-(*** recursion equations ***)
-
-Goal "xs \\<in> list(A) ==> <xs, []> \\<in> gen_prefix(A,r) <-> (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "gen_prefix_Nil";
-Addsimps [gen_prefix_Nil];
-
-Goalw [refl_def]
- "[| refl(A, r); xs \\<in> list(A) |] ==> \
-\ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \\<in> gen_prefix(A, r)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "same_gen_prefix_gen_prefix";
-Addsimps [same_gen_prefix_gen_prefix];
-
-Goal "[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
-\ <xs, Cons(y,ys)> \\<in> gen_prefix(A,r) <-> \
-\ (xs=[] | (\\<exists>z zs. xs=Cons(z,zs) & z \\<in> A & <z,y>:r & <zs,ys> \\<in> gen_prefix(A,r)))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "gen_prefix_Cons";
-
-Goal "[| refl(A,r); <xs,ys> \\<in> gen_prefix(A, r); zs \\<in> list(A) |] \
-\ ==> <xs@zs, take(length(xs), ys) @ zs> \\<in> gen_prefix(A, r)";
-by (etac gen_prefix.induct 1);
-by (Asm_simp_tac 1);
-by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD]));
-by Auto_tac;
-by (ftac gen_prefix_length_le 1);
-by (subgoal_tac "take(length(xs), ys) \\<in> list(A)" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps
- [diff_is_0_iff RS iffD2, take_type ])));
-qed "gen_prefix_take_append";
-
-Goal "[| refl(A, r); <xs,ys> \\<in> gen_prefix(A,r); \
-\ length(xs) = length(ys); zs \\<in> list(A) |] \
-\ ==> <xs@zs, ys @ zs> \\<in> gen_prefix(A, r)";
-by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1);
-by (REPEAT(assume_tac 1));
-by (subgoal_tac "take(length(xs), ys)=ys" 1);
-by (auto_tac (claset() addSIs [take_all]
- addDs [gen_prefix.dom_subset RS subsetD],
- simpset()));
-qed "gen_prefix_append_both";
-
-(*NOT suitable for rewriting since [y] has the form y#ys*)
-Goal "xs \\<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
-by (auto_tac (claset(), simpset() addsimps [app_assoc]));
-qed "append_cons_conv";
-
-Goal "[| <xs,ys> \\<in> gen_prefix(A, r); refl(A, r) |] \
-\ ==> length(xs) < length(ys) --> \
-\ <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
-by (etac gen_prefix.induct 1);
-by (Blast_tac 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type])));
-(* Append case is hardest *)
-by (forward_tac [gen_prefix_length_le RS (le_iff RS iffD1) ] 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (Clarify_tac 1);
-by (subgoal_tac "length(xs):nat&length(ys):nat &length(zs):nat" 1);
-by (blast_tac (claset() addIs [length_type]) 2);
-by (Clarify_tac 1);
-by (ALLGOALS (asm_full_simp_tac (simpset()
- addsimps [nth_append, length_type, length_app])));
-by (Clarify_tac 1);
-by (rtac conjI 1);
-by (blast_tac (claset() addIs [gen_prefix.append]) 1);
-by (thin_tac "length(xs) < length(ys) -->?u" 1);
-by (eres_inst_tac [("a","zs")] list.elim 1);
-by Auto_tac;
-by (res_inst_tac [("P1", "%x. <?u(x), ?v>:?w")] (nat_diff_split RS iffD2) 1);
-by Auto_tac;
-by (stac append_cons_conv 1);
-by (rtac gen_prefix.append 2);
-by (auto_tac (claset() addEs [ConsE],
- simpset() addsimps [gen_prefix_append_both]));
-val append_one_gen_prefix_lemma = result() RS mp;
-
-Goal "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] \
-\ ==> <xs @ [nth(length(xs), ys)], ys> \\<in> gen_prefix(A, r)";
-by (blast_tac (claset() addIs [append_one_gen_prefix_lemma]) 1);
-qed "append_one_gen_prefix";
-
-
-(** Proving the equivalence with Charpentier's definition **)
-
-Goal "xs \\<in> list(A) ==> \
-\ \\<forall>ys \\<in> list(A). \\<forall>i \\<in> nat. i < length(xs) \
-\ --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r";
-by (induct_tac "xs" 1);
-by (ALLGOALS(Clarify_tac));
-by (ALLGOALS(Asm_full_simp_tac));
-by (etac natE 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "gen_prefix_imp_nth_lemma";
-
-Goal "[| <xs,ys> \\<in> gen_prefix(A,r); i < length(xs)|] \
-\ ==> <nth(i, xs), nth(i, ys)>:r";
-by (cut_inst_tac [("A","A")] gen_prefix.dom_subset 1);
-by (rtac gen_prefix_imp_nth_lemma 1);
-by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat]));
-qed "gen_prefix_imp_nth";
-
-Goal "xs \\<in> list(A) ==> \
-\ \\<forall>ys \\<in> list(A). length(xs) \\<le> length(ys) \
-\ --> (\\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r) \
-\ --> <xs, ys> \\<in> gen_prefix(A, r)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-by (Clarify_tac 1);
-by (eres_inst_tac [("a","ys")] list.elim 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (force_tac (claset() addSIs [nat_0_le], simpset() addsimps [lt_nat_in_nat]) 1);
-qed_spec_mp "nth_imp_gen_prefix";
-
-Goal "(<xs,ys> \\<in> gen_prefix(A,r)) <-> \
-\ (xs \\<in> list(A) & ys \\<in> list(A) & length(xs) \\<le> length(ys) & \
-\ (\\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
-by (rtac iffI 1);
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (ftac gen_prefix_length_le 1);
-by (ALLGOALS(Clarify_tac));
-by (rtac nth_imp_gen_prefix 2);
-by (dtac gen_prefix_imp_nth 1);
-by (auto_tac (claset(), simpset() addsimps [lt_nat_in_nat]));
-qed "gen_prefix_iff_nth";
-
-(** prefix is a partial order: **)
-
-Goalw [prefix_def]
- "refl(list(A), prefix(A))";
-by (rtac refl_gen_prefix 1);
-by (auto_tac (claset(), simpset() addsimps [refl_def]));
-qed "refl_prefix";
-Addsimps [refl_prefix RS reflD];
-
-Goalw [prefix_def] "trans(prefix(A))";
-by (rtac trans_gen_prefix 1);
-by (auto_tac (claset(), simpset() addsimps [trans_def]));
-qed "trans_prefix";
-
-bind_thm("prefix_trans", trans_prefix RS transD);
-
-Goalw [prefix_def] "trans[list(A)](prefix(A))";
-by (rtac trans_on_gen_prefix 1);
-by (auto_tac (claset(), simpset() addsimps [trans_def]));
-qed "trans_on_prefix";
-
-bind_thm("prefix_trans_on", trans_on_prefix RS trans_onD);
-
-(* Monotonicity of "set" operator WRT prefix *)
-
-Goalw [prefix_def]
-"<xs,ys> \\<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
-by (etac gen_prefix.induct 1);
-by (subgoal_tac "xs \\<in> list(A)&ys \\<in> list(A)" 3);
-by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 4);
-by (auto_tac (claset(), simpset() addsimps [set_of_list_append]));
-qed "set_of_list_prefix_mono";
-
-(** recursion equations **)
-
-Goalw [prefix_def] "xs \\<in> list(A) ==> <[],xs> \\<in> prefix(A)";
-by (asm_simp_tac (simpset() addsimps [Nil_gen_prefix]) 1);
-qed "Nil_prefix";
-Addsimps[Nil_prefix];
-
-
-Goalw [prefix_def] "<xs, []> \\<in> prefix(A) <-> (xs = [])";
-by Auto_tac;
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (dres_inst_tac [("psi", "<xs, []> \\<in> gen_prefix(A, id(A))")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [gen_prefix_Nil]) 1);
-qed "prefix_Nil";
-AddIffs [prefix_Nil];
-
-Goalw [prefix_def]
-"<Cons(x,xs), Cons(y,ys)> \\<in> prefix(A) <-> (x=y & <xs,ys> \\<in> prefix(A) & y \\<in> A)";
-by Auto_tac;
-qed"Cons_prefix_Cons";
-AddIffs [Cons_prefix_Cons];
-
-Goalw [prefix_def]
-"xs \\<in> list(A)==> <xs@ys,xs@zs> \\<in> prefix(A) <-> (<ys,zs> \\<in> prefix(A))";
-by (subgoal_tac "refl(A,id(A))" 1);
-by (Asm_simp_tac 1);
-by (auto_tac (claset(), simpset() addsimps[refl_def]));
-qed "same_prefix_prefix";
-Addsimps [same_prefix_prefix];
-
-Goal "xs \\<in> list(A) ==> <xs@ys,xs> \\<in> prefix(A) <-> (<ys,[]> \\<in> prefix(A))";
-by (res_inst_tac [("P", "%x. <?u, x>:?v <-> ?w(x)")] (app_right_Nil RS subst) 1);
-by (rtac same_prefix_prefix 2);
-by Auto_tac;
-qed "same_prefix_prefix_Nil";
-Addsimps [same_prefix_prefix_Nil];
-
-Goalw [prefix_def]
-"[| <xs,ys> \\<in> prefix(A); zs \\<in> list(A) |] ==> <xs,ys@zs> \\<in> prefix(A)";
-by (etac gen_prefix.append 1);
-by (assume_tac 1);
-qed "prefix_appendI";
-Addsimps [prefix_appendI];
-
-Goalw [prefix_def]
-"[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
-\ <xs,Cons(y,ys)> \\<in> prefix(A) <-> \
-\ (xs=[] | (\\<exists>zs. xs=Cons(y,zs) & <zs,ys> \\<in> prefix(A)))";
-by (auto_tac (claset(), simpset() addsimps [gen_prefix_Cons]));
-qed "prefix_Cons";
-
-Goalw [prefix_def]
- "[| <xs,ys> \\<in> prefix(A); length(xs) < length(ys) |] \
-\ ==> <xs @ [nth(length(xs),ys)], ys> \\<in> prefix(A)";
-by (subgoal_tac "refl(A, id(A))" 1);
-by (asm_simp_tac (simpset() addsimps [append_one_gen_prefix]) 1);
-by (auto_tac (claset(), simpset() addsimps [refl_def]));
-qed "append_one_prefix";
-
-Goalw [prefix_def]
-"<xs,ys> \\<in> prefix(A) ==> length(xs) \\<le> length(ys)";
-by (blast_tac (claset() addDs [gen_prefix_length_le]) 1);
-qed "prefix_length_le";
-
-Goalw [prefix_def]
-"<xs,ys> \\<in> prefix(A) ==> xs\\<noteq>ys --> length(xs) < length(ys)";
-by (etac gen_prefix.induct 1);
-by (Clarify_tac 1);
-by (ALLGOALS(subgoal_tac "ys \\<in> list(A)&xs \\<in> list(A)"));
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
- simpset() addsimps [length_app, length_type]));
-by (subgoal_tac "length(zs)=0" 1);
-by (dtac not_lt_imp_le 2);
-by (res_inst_tac [("j", "length(ys)")] lt_trans2 5);
-by Auto_tac;
-val lemma = result();
-
-Goalw [prefix_def]
-"prefix(A)<=list(A)*list(A)";
-by (blast_tac (claset() addSIs [gen_prefix.dom_subset]) 1);
-qed "prefix_type";
-
-Goalw [strict_prefix_def]
-"strict_prefix(A) <= list(A)*list(A)";
-by (blast_tac (claset() addSIs [prefix_type RS subsetD]) 1);
-qed "strict_prefix_type";
-
-Goalw [strict_prefix_def]
- "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)";
-by (resolve_tac [lemma RS mp] 1);
-by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset()));
-qed "strict_prefix_length_lt";
-
-(*Equivalence to the definition used in Lex/Prefix.thy*)
-Goalw [prefix_def]
- "<xs,zs> \\<in> prefix(A) <-> (\\<exists>ys \\<in> list(A). zs = xs@ys) & xs \\<in> list(A)";
-by (auto_tac (claset(),
- simpset() addsimps [gen_prefix_iff_nth, lt_nat_in_nat,
- nth_append, nth_type, app_type, length_app]));
-by (subgoal_tac "drop(length(xs), zs) \\<in> list(A)" 1);
-by (res_inst_tac [("x", "drop(length(xs), zs)")] bexI 1);
-by (ALLGOALS(Clarify_tac));
-by (asm_simp_tac (simpset() addsimps [length_type, drop_type]) 2);
-by (rtac nth_equalityI 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps
- [nth_append, app_type, drop_type, length_app, length_drop])));
-by (rtac (nat_diff_split RS iffD2) 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Clarify_tac 1);
-by (dres_inst_tac [("i", "length(zs)")] leI 1);
-by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1);
-by Safe_tac;
-by (subgoal_tac "length(xs) #+ (i #- length(xs)) = i" 1);
-by (stac nth_drop 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI] addsplits [nat_diff_split])));
-qed "prefix_iff";
-
-Goal
-"[|xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
-\ <xs, ys@[y]> \\<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \\<in> prefix(A))";
-by (simp_tac (simpset() addsimps [prefix_iff]) 1);
-by (rtac iffI 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("xs", "ysa")] rev_list_elim 1);
-by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [app_type, app_assoc RS sym]) 1);
-by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
-qed "prefix_snoc";
-Addsimps [prefix_snoc];
-
-Goal "zs \\<in> list(A) ==> \\<forall>xs \\<in> list(A). \\<forall>ys \\<in> list(A). \
-\ (<xs, ys@zs> \\<in> prefix(A)) <-> \
-\ (<xs,ys> \\<in> prefix(A) | (\\<exists>us. xs = ys@us & <us,zs> \\<in> prefix(A)))";
-by (etac list_append_induct 1);
-by (Clarify_tac 2);
-by (rtac iffI 2);
-by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2);
-by (etac disjE 2 THEN etac disjE 3);
-by (rtac disjI2 2);
-by (res_inst_tac [("x", "y @ [x]")] exI 2);
-by (asm_full_simp_tac (simpset() addsimps [app_assoc RS sym]) 2);
-by (REPEAT(Force_tac 1));
-qed_spec_mp "prefix_append_iff";
-
-
-(*Although the prefix ordering is not linear, the prefixes of a list
- are linearly ordered.*)
-Goal "[| zs \\<in> list(A); xs \\<in> list(A); ys \\<in> list(A) |] \
-\ ==> <xs, zs> \\<in> prefix(A) --> <ys,zs> \\<in> prefix(A) \
-\ --><xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
-by (etac list_append_induct 1);
-by Auto_tac;
-qed_spec_mp "common_prefix_linear_lemma";
-
-Goal "[|<xs, zs> \\<in> prefix(A); <ys,zs> \\<in> prefix(A) |] \
-\ ==> <xs,ys> \\<in> prefix(A) | <ys,xs> \\<in> prefix(A)";
-by (cut_facts_tac [prefix_type] 1);
-by (blast_tac (claset() delrules [disjCI] addIs [common_prefix_linear_lemma]) 1);
-qed "common_prefix_linear";
-
-
-(*** pfixLe, pfixGe \\<in> properties inherited from the translations ***)
-
-
-
-(** pfixLe **)
-
-Goalw [refl_def] "refl(nat,Le)";
-by Auto_tac;
-qed "refl_Le";
-Addsimps [refl_Le];
-
-Goalw [antisym_def] "antisym(Le)";
-by (auto_tac (claset() addIs [le_anti_sym], simpset()));
-qed "antisym_Le";
-Addsimps [antisym_Le];
-
-Goalw [trans_on_def] "trans[nat](Le)";
-by Auto_tac;
-by (blast_tac (claset() addIs [le_trans]) 1);
-qed "trans_on_Le";
-Addsimps [trans_on_Le];
-
-Goalw [trans_def] "trans(Le)";
-by Auto_tac;
-by (blast_tac (claset() addIs [le_trans]) 1);
-qed "trans_Le";
-Addsimps [trans_Le];
-
-Goalw [part_order_def] "part_order(nat,Le)";
-by Auto_tac;
-qed "part_order_Le";
-Addsimps [part_order_Le];
-
-Goal "x \\<in> list(nat) ==> x pfixLe x";
-by (blast_tac (claset() addIs [refl_gen_prefix RS reflD, refl_Le]) 1);
-qed "pfixLe_refl";
-Addsimps[pfixLe_refl];
-
-Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
-by (blast_tac (claset() addIs [trans_gen_prefix RS transD, trans_Le]) 1);
-qed "pfixLe_trans";
-
-Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
-by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE, antisym_Le]) 1);
-qed "pfixLe_antisym";
-
-
-Goalw [prefix_def]
-"<xs,ys>:prefix(nat)==> xs pfixLe ys";
-by (rtac (gen_prefix_mono RS subsetD) 1);
-by Auto_tac;
-qed "prefix_imp_pfixLe";
-
-Goalw [refl_def, Ge_def] "refl(nat, Ge)";
-by Auto_tac;
-qed "refl_Ge";
-AddIffs [refl_Ge];
-
-Goalw [antisym_def, Ge_def] "antisym(Ge)";
-by (auto_tac (claset() addIs [le_anti_sym], simpset()));
-qed "antisym_Ge";
-AddIffs [antisym_Ge];
-
-Goalw [trans_def, Ge_def] "trans(Ge)";
-by (auto_tac (claset() addIs [le_trans], simpset()));
-qed "trans_Ge";
-AddIffs [trans_Ge];
-
-Goal "x \\<in> list(nat) ==> x pfixGe x";
-by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1);
-qed "pfixGe_refl";
-Addsimps[pfixGe_refl];
-
-Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
-by (blast_tac (claset() addIs [trans_gen_prefix RS transD]) 1);
-qed "pfixGe_trans";
-
-Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
-by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE]) 1);
-qed "pfixGe_antisym";
-
-Goalw [prefix_def, Ge_def]
- "<xs,ys>:prefix(nat) ==> xs pfixGe ys";
-by (rtac (gen_prefix_mono RS subsetD) 1);
-by Auto_tac;
-qed "prefix_imp_pfixGe";
-(* Added by Sidi \\<in> prefix and take *)
-
-Goalw [prefix_def]
-"<xs, ys> \\<in> prefix(A) ==> xs = take(length(xs), ys)";
-by (etac gen_prefix.induct 1);
-by (subgoal_tac "length(xs):nat" 3);
-by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
- simpset() addsimps [length_type]));
-by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
-by (forward_tac [gen_prefix_length_le] 1);
-by (auto_tac (claset(), simpset() addsimps [take_append]));
-by (subgoal_tac "length(xs) #- length(ys)=0" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_is_0_iff])));
-qed "prefix_imp_take";
-
-Goal "[|<xs,ys> \\<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys";
-by (cut_inst_tac [("A","A")] prefix_type 1);
-by (dtac subsetD 1);
-by Auto_tac;
-by (dtac prefix_imp_take 1);
-by (etac trans 1);
-by (Asm_full_simp_tac 1);
-qed "prefix_length_equal";
-
-Goal "[|<xs,ys> \\<in> prefix(A); length(ys) \\<le> length(xs)|] ==> xs = ys";
-by (blast_tac (claset() addIs [prefix_length_equal, le_anti_sym, prefix_length_le]) 1);
-qed "prefix_length_le_equal";
-
-Goalw [prefix_def] "xs \\<in> list(A) ==> \\<forall>n \\<in> nat. <take(n, xs), xs> \\<in> prefix(A)";
-by (etac list.induct 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (etac natE 1);
-by Auto_tac;
-qed_spec_mp "take_prefix";
-
-Goal "<xs,ys> \\<in> prefix(A) <-> (xs=take(length(xs), ys) & xs \\<in> list(A) & ys \\<in> list(A))";
-by (rtac iffI 1);
-by (forward_tac [prefix_type RS subsetD] 1);
-by (blast_tac (claset() addIs [prefix_imp_take]) 1);
-by (Clarify_tac 1);
-by (etac ssubst 1);
-by (blast_tac (claset() addIs [take_prefix, length_type]) 1);
-qed "prefix_take_iff";
-
-Goal "[| <xs,ys> \\<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)";
-by (auto_tac (claset() addSDs [gen_prefix_imp_nth],
- simpset() addsimps [prefix_def]));
-qed "prefix_imp_nth";
-
-val prems = Goal "[|xs \\<in> list(A); ys \\<in> list(A); length(xs) \\<le> length(ys); \
-\ !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|] \
-\ ==> <xs,ys> \\<in> prefix(A)";
-by (auto_tac (claset(), simpset() addsimps prems@[prefix_def, nth_imp_gen_prefix]));
-by (auto_tac (claset() addSIs [nth_imp_gen_prefix], simpset() addsimps prems@[prefix_def]));
-by (blast_tac (claset() addIs prems@[nth_type, lt_trans2]) 1);
-qed "nth_imp_prefix";
-
-
-Goal "[|length(xs) \\<le> length(ys); \
-\ <xs,zs> \\<in> prefix(A); <ys,zs> \\<in> prefix(A)|] ==> <xs,ys> \\<in> prefix(A)";
-by (cut_inst_tac [("A","A")] prefix_type 1);
-by (rtac nth_imp_prefix 1);
- by (blast_tac (claset() addIs []) 1);
- by (blast_tac (claset() addIs []) 1);
- by (assume_tac 1);
-by (res_inst_tac [("b","nth(i,zs)")] trans 1);
- by (blast_tac (claset() addIs [prefix_imp_nth]) 1);
-by (blast_tac (claset() addIs [sym, prefix_imp_nth, prefix_length_le, lt_trans2]) 1);
-qed "length_le_prefix_imp_prefix";
\ No newline at end of file
--- a/src/ZF/UNITY/GenPrefix.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Mon Mar 28 16:19:56 2005 +0200
@@ -1,9 +1,7 @@
-(* Title: ZF/UNITY/GenPrefix.thy
- ID: $Id$
+(* ID: $Id$
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
-Charpentier's Generalized Prefix Relation
<xs,ys>:gen_prefix(r)
if ys = xs' @ zs where length(xs) = length(xs')
and corresponding elements of xs, xs' are pairwise related by r
@@ -11,10 +9,15 @@
Based on Lex/Prefix
*)
-GenPrefix = Main +
+header{*Charpentier's Generalized Prefix Relation*}
+
+theory GenPrefix
+imports Main
+
+begin
constdefs (*really belongs in ZF/Trancl*)
- part_order :: [i, i] => o
+ part_order :: "[i, i] => o"
"part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
consts
@@ -25,31 +28,651 @@
domains "gen_prefix(A, r)" <= "list(A)*list(A)"
- intrs
- Nil "<[],[]>:gen_prefix(A, r)"
+ intros
+ Nil: "<[],[]>:gen_prefix(A, r)"
- prepend "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x:A; y:A |]
+ prepend: "[| <xs,ys>:gen_prefix(A, r); <x,y>:r; x:A; y:A |]
==> <Cons(x,xs), Cons(y,ys)>: gen_prefix(A, r)"
- append "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
- ==> <xs, ys@zs>:gen_prefix(A, r)"
- type_intrs "list.intrs@[app_type]"
+ append: "[| <xs,ys>:gen_prefix(A, r); zs:list(A) |]
+ ==> <xs, ys@zs>:gen_prefix(A, r)"
+ type_intros app_type list.Nil list.Cons
constdefs
- prefix :: i=>i
+ prefix :: "i=>i"
"prefix(A) == gen_prefix(A, id(A))"
- strict_prefix :: i=>i
+ strict_prefix :: "i=>i"
"strict_prefix(A) == prefix(A) - id(list(A))"
syntax
(* less or equal and greater or equal over prefixes *)
- pfixLe :: [i, i] => o (infixl "pfixLe" 50)
- pfixGe :: [i, i] => o (infixl "pfixGe" 50)
+ pfixLe :: "[i, i] => o" (infixl "pfixLe" 50)
+ pfixGe :: "[i, i] => o" (infixl "pfixGe" 50)
translations
"xs pfixLe ys" == "<xs, ys>:gen_prefix(nat, Le)"
"xs pfixGe ys" == "<xs, ys>:gen_prefix(nat, Ge)"
+lemma reflD:
+ "[| refl(A, r); x \<in> A |] ==> <x,x>:r"
+apply (unfold refl_def, auto)
+done
+
+(*** preliminary lemmas ***)
+
+lemma Nil_gen_prefix: "xs \<in> list(A) ==> <[], xs> \<in> gen_prefix(A, r)"
+by (drule gen_prefix.append [OF gen_prefix.Nil], simp)
+declare Nil_gen_prefix [simp]
+
+
+lemma gen_prefix_length_le: "<xs,ys> \<in> gen_prefix(A, r) ==> length(xs) \<le> length(ys)"
+apply (erule gen_prefix.induct)
+apply (subgoal_tac [3] "ys \<in> list (A) ")
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
+ intro: le_trans simp add: length_app)
+done
+
+
+lemma Cons_gen_prefix_aux:
+ "[| <xs', ys'> \<in> gen_prefix(A, r) |]
+ ==> (\<forall>x xs. x \<in> A --> xs'= Cons(x,xs) -->
+ (\<exists>y ys. y \<in> A & ys' = Cons(y,ys) &
+ <x,y>:r & <xs, ys> \<in> gen_prefix(A, r)))"
+apply (erule gen_prefix.induct)
+prefer 3 apply (force intro: gen_prefix.append, auto)
+done
+
+lemma Cons_gen_prefixE:
+ "[| <Cons(x,xs), zs> \<in> gen_prefix(A, r);
+ !!y ys. [|zs = Cons(y, ys); y \<in> A; x \<in> A; <x,y>:r;
+ <xs,ys> \<in> gen_prefix(A, r) |] ==> P |] ==> P"
+apply (frule gen_prefix.dom_subset [THEN subsetD], auto)
+apply (blast dest: Cons_gen_prefix_aux)
+done
+declare Cons_gen_prefixE [elim!]
+
+lemma Cons_gen_prefix_Cons:
+"(<Cons(x,xs),Cons(y,ys)> \<in> gen_prefix(A, r))
+ <-> (x \<in> A & y \<in> A & <x,y>:r & <xs,ys> \<in> gen_prefix(A, r))"
+apply (auto intro: gen_prefix.prepend)
+done
+declare Cons_gen_prefix_Cons [iff]
+
+(** Monotonicity of gen_prefix **)
+
+lemma gen_prefix_mono2: "r<=s ==> gen_prefix(A, r) <= gen_prefix(A, s)"
+apply clarify
+apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
+apply (erule rev_mp)
+apply (erule gen_prefix.induct)
+apply (auto intro: gen_prefix.append)
+done
+
+lemma gen_prefix_mono1: "A<=B ==>gen_prefix(A, r) <= gen_prefix(B, r)"
+apply clarify
+apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
+apply (erule rev_mp)
+apply (erule_tac P = "y \<in> list (A) " in rev_mp)
+apply (erule_tac P = "xa \<in> list (A) " in rev_mp)
+apply (erule gen_prefix.induct)
+apply (simp (no_asm_simp))
+apply clarify
+apply (erule ConsE)+
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
+ intro: gen_prefix.append list_mono [THEN subsetD])
+done
+
+lemma gen_prefix_mono: "[| A <= B; r <= s |] ==> gen_prefix(A, r) <= gen_prefix(B, s)"
+apply (rule subset_trans)
+apply (rule gen_prefix_mono1)
+apply (rule_tac [2] gen_prefix_mono2, auto)
+done
+
+(*** gen_prefix order ***)
+
+(* reflexivity *)
+lemma refl_gen_prefix: "refl(A, r) ==> refl(list(A), gen_prefix(A, r))"
+apply (unfold refl_def, auto)
+apply (induct_tac "x", auto)
+done
+declare refl_gen_prefix [THEN reflD, simp]
+
+(* Transitivity *)
+(* A lemma for proving gen_prefix_trans_comp *)
+
+lemma append_gen_prefix [rule_format (no_asm)]: "xs \<in> list(A) ==>
+ \<forall>zs. <xs @ ys, zs> \<in> gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)"
+apply (erule list.induct)
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
+done
+
+(* Lemma proving transitivity and more*)
+
+lemma gen_prefix_trans_comp [rule_format (no_asm)]:
+ "<x, y>: gen_prefix(A, r) ==>
+ (\<forall>z \<in> list(A). <y,z> \<in> gen_prefix(A, s)--><x, z> \<in> gen_prefix(A, s O r))"
+apply (erule gen_prefix.induct)
+apply (auto elim: ConsE simp add: Nil_gen_prefix)
+apply (subgoal_tac "ys \<in> list (A) ")
+prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
+apply (drule_tac xs = ys and r = s in append_gen_prefix, auto)
+done
+
+lemma trans_comp_subset: "trans(r) ==> r O r <= r"
+by (auto dest: transD)
+
+lemma trans_gen_prefix: "trans(r) ==> trans(gen_prefix(A,r))"
+apply (simp (no_asm) add: trans_def)
+apply clarify
+apply (rule trans_comp_subset [THEN gen_prefix_mono2, THEN subsetD], assumption)
+apply (rule gen_prefix_trans_comp)
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD])
+done
+
+lemma trans_on_gen_prefix:
+ "trans(r) ==> trans[list(A)](gen_prefix(A, r))"
+apply (drule_tac A = A in trans_gen_prefix)
+apply (unfold trans_def trans_on_def, blast)
+done
+
+lemma prefix_gen_prefix_trans:
+ "[| <x,y> \<in> prefix(A); <y, z> \<in> gen_prefix(A, r); r<=A*A |]
+ ==> <x, z> \<in> gen_prefix(A, r)"
+apply (unfold prefix_def)
+apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in right_comp_id [THEN subst])
+apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
+done
+
+
+lemma gen_prefix_prefix_trans:
+"[| <x,y> \<in> gen_prefix(A,r); <y, z> \<in> prefix(A); r<=A*A |]
+ ==> <x, z> \<in> gen_prefix(A, r)"
+apply (unfold prefix_def)
+apply (rule_tac P = "%r. <x,z> \<in> gen_prefix (A, r) " in left_comp_id [THEN subst])
+apply (blast dest: gen_prefix_trans_comp gen_prefix.dom_subset [THEN subsetD])+
+done
+
+(** Antisymmetry **)
+
+lemma nat_le_lemma [rule_format]: "n \<in> nat ==> \<forall>b \<in> nat. n #+ b \<le> n --> b = 0"
+by (induct_tac "n", auto)
+
+lemma antisym_gen_prefix: "antisym(r) ==> antisym(gen_prefix(A, r))"
+apply (simp (no_asm) add: antisym_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule gen_prefix.induct, blast)
+apply (simp add: antisym_def, blast)
+txt{*append case is hardest*}
+apply clarify
+apply (subgoal_tac "length (zs) = 0")
+apply (subgoal_tac "ys \<in> list (A) ")
+prefer 2 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
+apply (drule_tac psi = "<ys @ zs, xs> \<in> gen_prefix (A,r) " in asm_rl)
+apply simp
+apply (subgoal_tac "length (ys @ zs) = length (ys) #+ length (zs) &ys \<in> list (A) &xs \<in> list (A) ")
+prefer 2 apply (blast intro: length_app dest: gen_prefix.dom_subset [THEN subsetD])
+apply (drule gen_prefix_length_le)+
+apply clarify
+apply simp
+apply (drule_tac j = "length (xs) " in le_trans)
+apply blast
+apply (auto intro: nat_le_lemma)
+done
+
+(*** recursion equations ***)
+
+lemma gen_prefix_Nil: "xs \<in> list(A) ==> <xs, []> \<in> gen_prefix(A,r) <-> (xs = [])"
+by (induct_tac "xs", auto)
+declare gen_prefix_Nil [simp]
+
+lemma same_gen_prefix_gen_prefix:
+ "[| refl(A, r); xs \<in> list(A) |] ==>
+ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs> \<in> gen_prefix(A, r)"
+apply (unfold refl_def)
+apply (induct_tac "xs")
+apply (simp_all (no_asm_simp))
+done
+declare same_gen_prefix_gen_prefix [simp]
+
+lemma gen_prefix_Cons: "[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+ <xs, Cons(y,ys)> \<in> gen_prefix(A,r) <->
+ (xs=[] | (\<exists>z zs. xs=Cons(z,zs) & z \<in> A & <z,y>:r & <zs,ys> \<in> gen_prefix(A,r)))"
+apply (induct_tac "xs", auto)
+done
+
+lemma gen_prefix_take_append: "[| refl(A,r); <xs,ys> \<in> gen_prefix(A, r); zs \<in> list(A) |]
+ ==> <xs@zs, take(length(xs), ys) @ zs> \<in> gen_prefix(A, r)"
+apply (erule gen_prefix.induct)
+apply (simp (no_asm_simp))
+apply (frule_tac [!] gen_prefix.dom_subset [THEN subsetD], auto)
+apply (frule gen_prefix_length_le)
+apply (subgoal_tac "take (length (xs), ys) \<in> list (A) ")
+apply (simp_all (no_asm_simp) add: diff_is_0_iff [THEN iffD2] take_type)
+done
+
+lemma gen_prefix_append_both: "[| refl(A, r); <xs,ys> \<in> gen_prefix(A,r);
+ length(xs) = length(ys); zs \<in> list(A) |]
+ ==> <xs@zs, ys @ zs> \<in> gen_prefix(A, r)"
+apply (drule_tac zs = zs in gen_prefix_take_append, assumption+)
+apply (subgoal_tac "take (length (xs), ys) =ys")
+apply (auto intro!: take_all dest: gen_prefix.dom_subset [THEN subsetD])
+done
+
+(*NOT suitable for rewriting since [y] has the form y#ys*)
+lemma append_cons_conv: "xs \<in> list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys"
+by (auto simp add: app_assoc)
+
+lemma append_one_gen_prefix_lemma [rule_format]:
+ "[| <xs,ys> \<in> gen_prefix(A, r); refl(A, r) |]
+ ==> length(xs) < length(ys) -->
+ <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
+apply (erule gen_prefix.induct, blast)
+apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
+apply (simp_all add: length_type)
+(* Append case is hardest *)
+apply (frule gen_prefix_length_le [THEN le_iff [THEN iffD1]])
+apply (frule gen_prefix.dom_subset [THEN subsetD], clarify)
+apply (subgoal_tac "length (xs) :nat&length (ys) :nat &length (zs) :nat")
+prefer 2 apply (blast intro: length_type, clarify)
+apply (simp_all add: nth_append length_type length_app)
+apply (rule conjI)
+apply (blast intro: gen_prefix.append)
+apply (erule_tac V = "length (xs) < length (ys) -->?u" in thin_rl)
+apply (erule_tac a = zs in list.cases, auto)
+apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2])
+apply auto
+apply (simplesubst append_cons_conv)
+apply (rule_tac [2] gen_prefix.append)
+apply (auto elim: ConsE simp add: gen_prefix_append_both)
+done
+
+lemma append_one_gen_prefix: "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |]
+ ==> <xs @ [nth(length(xs), ys)], ys> \<in> gen_prefix(A, r)"
+apply (blast intro: append_one_gen_prefix_lemma)
+done
+
+
+(** Proving the equivalence with Charpentier's definition **)
+
+lemma gen_prefix_imp_nth_lemma [rule_format]: "xs \<in> list(A) ==>
+ \<forall>ys \<in> list(A). \<forall>i \<in> nat. i < length(xs)
+ --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r"
+apply (induct_tac "xs", simp, clarify)
+apply simp
+apply (erule natE, auto)
+done
+
+lemma gen_prefix_imp_nth: "[| <xs,ys> \<in> gen_prefix(A,r); i < length(xs)|]
+ ==> <nth(i, xs), nth(i, ys)>:r"
+apply (cut_tac A = A in gen_prefix.dom_subset)
+apply (rule gen_prefix_imp_nth_lemma)
+apply (auto simp add: lt_nat_in_nat)
+done
+
+lemma nth_imp_gen_prefix [rule_format]: "xs \<in> list(A) ==>
+ \<forall>ys \<in> list(A). length(xs) \<le> length(ys)
+ --> (\<forall>i. i < length(xs) --> <nth(i, xs), nth(i,ys)>:r)
+ --> <xs, ys> \<in> gen_prefix(A, r)"
+apply (induct_tac "xs")
+apply (simp_all (no_asm_simp))
+apply clarify
+apply (erule_tac a = ys in list.cases, simp)
+apply (force intro!: nat_0_le simp add: lt_nat_in_nat)
+done
+
+lemma gen_prefix_iff_nth: "(<xs,ys> \<in> gen_prefix(A,r)) <->
+ (xs \<in> list(A) & ys \<in> list(A) & length(xs) \<le> length(ys) &
+ (\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))"
+apply (rule iffI)
+apply (frule gen_prefix.dom_subset [THEN subsetD])
+apply (frule gen_prefix_length_le, auto)
+apply (rule_tac [2] nth_imp_gen_prefix)
+apply (drule gen_prefix_imp_nth)
+apply (auto simp add: lt_nat_in_nat)
+done
+
+(** prefix is a partial order: **)
+
+lemma refl_prefix: "refl(list(A), prefix(A))"
+apply (unfold prefix_def)
+apply (rule refl_gen_prefix)
+apply (auto simp add: refl_def)
+done
+declare refl_prefix [THEN reflD, simp]
+
+lemma trans_prefix: "trans(prefix(A))"
+apply (unfold prefix_def)
+apply (rule trans_gen_prefix)
+apply (auto simp add: trans_def)
+done
+
+lemmas prefix_trans = trans_prefix [THEN transD, standard]
+
+lemma trans_on_prefix: "trans[list(A)](prefix(A))"
+apply (unfold prefix_def)
+apply (rule trans_on_gen_prefix)
+apply (auto simp add: trans_def)
+done
+
+lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard]
+
+(* Monotonicity of "set" operator WRT prefix *)
+
+lemma set_of_list_prefix_mono:
+"<xs,ys> \<in> prefix(A) ==> set_of_list(xs) <= set_of_list(ys)"
+
+apply (unfold prefix_def)
+apply (erule gen_prefix.induct)
+apply (subgoal_tac [3] "xs \<in> list (A) &ys \<in> list (A) ")
+prefer 4 apply (blast dest: gen_prefix.dom_subset [THEN subsetD])
+apply (auto simp add: set_of_list_append)
+done
+
+(** recursion equations **)
+
+lemma Nil_prefix: "xs \<in> list(A) ==> <[],xs> \<in> prefix(A)"
+
+apply (unfold prefix_def)
+apply (simp (no_asm_simp) add: Nil_gen_prefix)
+done
+declare Nil_prefix [simp]
+
+
+lemma prefix_Nil: "<xs, []> \<in> prefix(A) <-> (xs = [])"
+
+apply (unfold prefix_def, auto)
+apply (frule gen_prefix.dom_subset [THEN subsetD])
+apply (drule_tac psi = "<xs, []> \<in> gen_prefix (A, id (A))" in asm_rl)
+apply (simp add: gen_prefix_Nil)
+done
+declare prefix_Nil [iff]
+
+lemma Cons_prefix_Cons:
+"<Cons(x,xs), Cons(y,ys)> \<in> prefix(A) <-> (x=y & <xs,ys> \<in> prefix(A) & y \<in> A)"
+apply (unfold prefix_def, auto)
+done
+declare Cons_prefix_Cons [iff]
+
+lemma same_prefix_prefix:
+"xs \<in> list(A)==> <xs@ys,xs@zs> \<in> prefix(A) <-> (<ys,zs> \<in> prefix(A))"
+apply (unfold prefix_def)
+apply (subgoal_tac "refl (A,id (A))")
+apply (simp (no_asm_simp))
+apply (auto simp add: refl_def)
+done
+declare same_prefix_prefix [simp]
+
+lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) <-> (<ys,[]> \<in> prefix(A))"
+apply (rule_tac P = "%x. <?u, x>:?v <-> ?w (x) " in app_right_Nil [THEN subst])
+apply (rule_tac [2] same_prefix_prefix, auto)
+done
+declare same_prefix_prefix_Nil [simp]
+
+lemma prefix_appendI:
+"[| <xs,ys> \<in> prefix(A); zs \<in> list(A) |] ==> <xs,ys@zs> \<in> prefix(A)"
+apply (unfold prefix_def)
+apply (erule gen_prefix.append, assumption)
+done
+declare prefix_appendI [simp]
+
+lemma prefix_Cons:
+"[| xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+ <xs,Cons(y,ys)> \<in> prefix(A) <->
+ (xs=[] | (\<exists>zs. xs=Cons(y,zs) & <zs,ys> \<in> prefix(A)))"
+apply (unfold prefix_def)
+apply (auto simp add: gen_prefix_Cons)
+done
+
+lemma append_one_prefix:
+ "[| <xs,ys> \<in> prefix(A); length(xs) < length(ys) |]
+ ==> <xs @ [nth(length(xs),ys)], ys> \<in> prefix(A)"
+apply (unfold prefix_def)
+apply (subgoal_tac "refl (A, id (A))")
+apply (simp (no_asm_simp) add: append_one_gen_prefix)
+apply (auto simp add: refl_def)
+done
+
+lemma prefix_length_le:
+"<xs,ys> \<in> prefix(A) ==> length(xs) \<le> length(ys)"
+apply (unfold prefix_def)
+apply (blast dest: gen_prefix_length_le)
+done
+
+lemma prefix_type: "prefix(A)<=list(A)*list(A)"
+apply (unfold prefix_def)
+apply (blast intro!: gen_prefix.dom_subset)
+done
+
+lemma strict_prefix_type:
+"strict_prefix(A) <= list(A)*list(A)"
+apply (unfold strict_prefix_def)
+apply (blast intro!: prefix_type [THEN subsetD])
+done
+
+lemma strict_prefix_length_lt_aux:
+ "<xs,ys> \<in> prefix(A) ==> xs\<noteq>ys --> length(xs) < length(ys)"
+apply (unfold prefix_def)
+apply (erule gen_prefix.induct, clarify)
+apply (subgoal_tac [!] "ys \<in> list(A) & xs \<in> list(A)")
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD]
+ simp add: length_type)
+apply (subgoal_tac "length (zs) =0")
+apply (drule_tac [2] not_lt_imp_le)
+apply (rule_tac [5] j = "length (ys) " in lt_trans2)
+apply auto
+done
+
+lemma strict_prefix_length_lt:
+ "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)"
+apply (unfold strict_prefix_def)
+apply (rule strict_prefix_length_lt_aux [THEN mp])
+apply (auto dest: prefix_type [THEN subsetD])
+done
+
+(*Equivalence to the definition used in Lex/Prefix.thy*)
+lemma prefix_iff:
+ "<xs,zs> \<in> prefix(A) <-> (\<exists>ys \<in> list(A). zs = xs@ys) & xs \<in> list(A)"
+apply (unfold prefix_def)
+apply (auto simp add: gen_prefix_iff_nth lt_nat_in_nat nth_append nth_type app_type length_app)
+apply (subgoal_tac "drop (length (xs), zs) \<in> list (A) ")
+apply (rule_tac x = "drop (length (xs), zs) " in bexI)
+apply safe
+ prefer 2 apply (simp add: length_type drop_type)
+apply (rule nth_equalityI)
+apply (simp_all (no_asm_simp) add: nth_append app_type drop_type length_app length_drop)
+apply (rule nat_diff_split [THEN iffD2], simp_all, clarify)
+apply (drule_tac i = "length (zs) " in leI)
+apply (force simp add: le_subset_iff, safe)
+apply (subgoal_tac "length (xs) #+ (i #- length (xs)) = i")
+apply (subst nth_drop)
+apply (simp_all (no_asm_simp) add: leI split add: nat_diff_split)
+done
+
+lemma prefix_snoc:
+"[|xs \<in> list(A); ys \<in> list(A); y \<in> A |] ==>
+ <xs, ys@[y]> \<in> prefix(A) <-> (xs = ys@[y] | <xs,ys> \<in> prefix(A))"
+apply (simp (no_asm) add: prefix_iff)
+apply (rule iffI, clarify)
+apply (erule_tac xs = ysa in rev_list_elim, simp)
+apply (simp add: app_type app_assoc [symmetric])
+apply (auto simp add: app_assoc app_type)
+done
+declare prefix_snoc [simp]
+
+lemma prefix_append_iff [rule_format]: "zs \<in> list(A) ==> \<forall>xs \<in> list(A). \<forall>ys \<in> list(A).
+ (<xs, ys@zs> \<in> prefix(A)) <->
+ (<xs,ys> \<in> prefix(A) | (\<exists>us. xs = ys@us & <us,zs> \<in> prefix(A)))"
+apply (erule list_append_induct, force, clarify)
+apply (rule iffI)
+apply (simp add: add: app_assoc [symmetric])
+apply (erule disjE)
+apply (rule disjI2)
+apply (rule_tac x = "y @ [x]" in exI)
+apply (simp add: add: app_assoc [symmetric], force+)
+done
+
+
+(*Although the prefix ordering is not linear, the prefixes of a list
+ are linearly ordered.*)
+lemma common_prefix_linear_lemma [rule_format]: "[| zs \<in> list(A); xs \<in> list(A); ys \<in> list(A) |]
+ ==> <xs, zs> \<in> prefix(A) --> <ys,zs> \<in> prefix(A)
+ --><xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
+apply (erule list_append_induct, auto)
+done
+
+lemma common_prefix_linear: "[|<xs, zs> \<in> prefix(A); <ys,zs> \<in> prefix(A) |]
+ ==> <xs,ys> \<in> prefix(A) | <ys,xs> \<in> prefix(A)"
+apply (cut_tac prefix_type)
+apply (blast del: disjCI intro: common_prefix_linear_lemma)
+done
+
+
+(*** pfixLe, pfixGe \<in> properties inherited from the translations ***)
+
+
+
+(** pfixLe **)
+
+lemma refl_Le: "refl(nat,Le)"
+
+apply (unfold refl_def, auto)
+done
+declare refl_Le [simp]
+
+lemma antisym_Le: "antisym(Le)"
+apply (unfold antisym_def)
+apply (auto intro: le_anti_sym)
+done
+declare antisym_Le [simp]
+
+lemma trans_on_Le: "trans[nat](Le)"
+apply (unfold trans_on_def, auto)
+apply (blast intro: le_trans)
+done
+declare trans_on_Le [simp]
+
+lemma trans_Le: "trans(Le)"
+apply (unfold trans_def, auto)
+apply (blast intro: le_trans)
+done
+declare trans_Le [simp]
+
+lemma part_order_Le: "part_order(nat,Le)"
+by (unfold part_order_def, auto)
+declare part_order_Le [simp]
+
+lemma pfixLe_refl: "x \<in> list(nat) ==> x pfixLe x"
+by (blast intro: refl_gen_prefix [THEN reflD] refl_Le)
+declare pfixLe_refl [simp]
+
+lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"
+by (blast intro: trans_gen_prefix [THEN transD] trans_Le)
+
+lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y"
+by (blast intro: antisym_gen_prefix [THEN antisymE] antisym_Le)
+
+
+lemma prefix_imp_pfixLe:
+"<xs,ys>:prefix(nat)==> xs pfixLe ys"
+
+apply (unfold prefix_def)
+apply (rule gen_prefix_mono [THEN subsetD], auto)
+done
+
+lemma refl_Ge: "refl(nat, Ge)"
+by (unfold refl_def Ge_def, auto)
+declare refl_Ge [iff]
+
+lemma antisym_Ge: "antisym(Ge)"
+apply (unfold antisym_def Ge_def)
+apply (auto intro: le_anti_sym)
+done
+declare antisym_Ge [iff]
+
+lemma trans_Ge: "trans(Ge)"
+apply (unfold trans_def Ge_def)
+apply (auto intro: le_trans)
+done
+declare trans_Ge [iff]
+
+lemma pfixGe_refl: "x \<in> list(nat) ==> x pfixGe x"
+by (blast intro: refl_gen_prefix [THEN reflD])
+declare pfixGe_refl [simp]
+
+lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"
+by (blast intro: trans_gen_prefix [THEN transD])
+
+lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y"
+by (blast intro: antisym_gen_prefix [THEN antisymE])
+
+lemma prefix_imp_pfixGe:
+ "<xs,ys>:prefix(nat) ==> xs pfixGe ys"
+apply (unfold prefix_def Ge_def)
+apply (rule gen_prefix_mono [THEN subsetD], auto)
+done
+(* Added by Sidi \<in> prefix and take *)
+
+lemma prefix_imp_take:
+"<xs, ys> \<in> prefix(A) ==> xs = take(length(xs), ys)"
+
+apply (unfold prefix_def)
+apply (erule gen_prefix.induct)
+apply (subgoal_tac [3] "length (xs) :nat")
+apply (auto dest: gen_prefix.dom_subset [THEN subsetD] simp add: length_type)
+apply (frule gen_prefix.dom_subset [THEN subsetD])
+apply (frule gen_prefix_length_le)
+apply (auto simp add: take_append)
+apply (subgoal_tac "length (xs) #- length (ys) =0")
+apply (simp_all (no_asm_simp) add: diff_is_0_iff)
+done
+
+lemma prefix_length_equal: "[|<xs,ys> \<in> prefix(A); length(xs)=length(ys)|] ==> xs = ys"
+apply (cut_tac A = A in prefix_type)
+apply (drule subsetD, auto)
+apply (drule prefix_imp_take)
+apply (erule trans, simp)
+done
+
+lemma prefix_length_le_equal: "[|<xs,ys> \<in> prefix(A); length(ys) \<le> length(xs)|] ==> xs = ys"
+by (blast intro: prefix_length_equal le_anti_sym prefix_length_le)
+
+lemma take_prefix [rule_format]: "xs \<in> list(A) ==> \<forall>n \<in> nat. <take(n, xs), xs> \<in> prefix(A)"
+apply (unfold prefix_def)
+apply (erule list.induct, simp, clarify)
+apply (erule natE, auto)
+done
+
+lemma prefix_take_iff: "<xs,ys> \<in> prefix(A) <-> (xs=take(length(xs), ys) & xs \<in> list(A) & ys \<in> list(A))"
+apply (rule iffI)
+apply (frule prefix_type [THEN subsetD])
+apply (blast intro: prefix_imp_take, clarify)
+apply (erule ssubst)
+apply (blast intro: take_prefix length_type)
+done
+
+lemma prefix_imp_nth: "[| <xs,ys> \<in> prefix(A); i < length(xs)|] ==> nth(i,xs) = nth(i,ys)"
+by (auto dest!: gen_prefix_imp_nth simp add: prefix_def)
+
+lemma nth_imp_prefix:
+ "[|xs \<in> list(A); ys \<in> list(A); length(xs) \<le> length(ys);
+ !!i. i < length(xs) ==> nth(i, xs) = nth(i,ys)|]
+ ==> <xs,ys> \<in> prefix(A)"
+apply (auto simp add: prefix_def nth_imp_gen_prefix)
+apply (auto intro!: nth_imp_gen_prefix simp add: prefix_def)
+apply (blast intro: nth_type lt_trans2)
+done
+
+
+lemma length_le_prefix_imp_prefix: "[|length(xs) \<le> length(ys);
+ <xs,zs> \<in> prefix(A); <ys,zs> \<in> prefix(A)|] ==> <xs,ys> \<in> prefix(A)"
+apply (cut_tac A = A in prefix_type)
+apply (rule nth_imp_prefix, blast, blast)
+ apply assumption
+apply (rule_tac b = "nth (i,zs)" in trans)
+ apply (blast intro: prefix_imp_nth)
+apply (blast intro: sym prefix_imp_nth prefix_length_le lt_trans2)
+done
+
end
--- a/src/ZF/UNITY/Mutex.ML Sat Mar 26 18:20:29 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(* Title: ZF/UNITY/Mutex.ML
- ID: $Id \\<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-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 \\<in> an ill-tyed expression will
-reduce to the empty set.
-
-*)
-
-(** Variables' types **)
-
-Addsimps [p_type, u_type, v_type, m_type, n_type];
-
-Goalw [state_def] "s \\<in> state ==>s`u \\<in> bool";
-by (dres_inst_tac [("a", "u")] apply_type 1);
-by Auto_tac;
-qed "u_value_type";
-
-Goalw [state_def] "s \\<in> state ==> s`v \\<in> bool";
-by (dres_inst_tac [("a", "v")] apply_type 1);
-by Auto_tac;
-qed "v_value_type";
-
-Goalw [state_def] "s \\<in> state ==> s`p \\<in> bool";
-by (dres_inst_tac [("a", "p")] apply_type 1);
-by Auto_tac;
-qed "p_value_type";
-
-Goalw [state_def] "s \\<in> state ==> s`m \\<in> int";
-by (dres_inst_tac [("a", "m")] apply_type 1);
-by Auto_tac;
-qed "m_value_type";
-
-Goalw [state_def] "s \\<in> state ==>s`n \\<in> int";
-by (dres_inst_tac [("a", "n")] apply_type 1);
-by Auto_tac;
-qed "n_value_type";
-
-Addsimps [p_value_type, u_value_type, v_value_type,
- m_value_type, n_value_type];
-AddTCs [p_value_type, u_value_type, v_value_type,
- m_value_type, n_value_type];
-(** Mutex is a program **)
-
-Goalw [Mutex_def] "Mutex \\<in> program";
-by Auto_tac;
-qed "Mutex_in_program";
-Addsimps [Mutex_in_program];
-AddTCs [Mutex_in_program];
-
-Addsimps [Mutex_def RS def_prg_Init];
-program_defs_ref := [Mutex_def];
-
-Addsimps (map simp_of_act
- [U0_def, U1_def, U2_def, U3_def, U4_def,
- V0_def, V1_def, V2_def, V3_def, V4_def]);
-
-Addsimps (map simp_of_set [U0_def, U1_def, U2_def, U3_def, U4_def,
- V0_def, V1_def, V2_def, V3_def, V4_def]);
-
-Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
-
-Goal "Mutex \\<in> Always(IU)";
-by (always_tac 1);
-by Auto_tac;
-qed "IU";
-
-Goal "Mutex \\<in> Always(IV)";
-by (always_tac 1);
-qed "IV";
-
-(*The safety property \\<in> mutual exclusion*)
-Goal "Mutex \\<in> Always({s \\<in> state. ~(s`m = #3 & s`n = #3)})";
-by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
-by Auto_tac;
-qed "mutual_exclusion";
-
-(*The bad invariant FAILS in V1*)
-
-Goal "[| x$<#1; #3 $<= x |] ==> P";
-by (dres_inst_tac [("j", "#1"), ("k", "#3")] zless_zle_trans 1);
-by (dres_inst_tac [("j", "x")] zle_zless_trans 2);
-by Auto_tac;
-qed "less_lemma";
-
-Goal "Mutex \\<in> Always(bad_IU)";
-by (always_tac 1);
-by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
-by (auto_tac (claset(), simpset() addsimps [bool_def]));
-by (subgoal_tac "#1 $<= #3" 1);
-by (dres_inst_tac [("x", "#1"), ("y", "#3")] zle_trans 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-by Auto_tac;
-(*Resulting state \\<in> n=1, p=false, m=4, u=false.
- Execution of V1 (the command of process v guarded by n=1) sets p:=true,
- violating the invariant!*)
-(*Check that subgoals remain: proof failed.*)
-getgoal 1;
-
-
-(*** Progress for U ***)
-
-Goalw [Unless_def]
-"Mutex \\<in> {s \\<in> state. s`m=#2} Unless {s \\<in> state. s`m=#3}";
-by (constrains_tac 1);
-qed "U_F0";
-
-Goal "Mutex \\<in> {s \\<in> state. s`m=#1} LeadsTo {s \\<in> state. s`p = s`v & s`m = #2}";
-by (ensures_tac "U1" 1);
-qed "U_F1";
-
-Goal "Mutex \\<in> {s \\<in> state. s`p =0 & s`m = #2} LeadsTo {s \\<in> state. s`m = #3}";
-by (cut_facts_tac [IU] 1);
-by (ensures_tac "U2" 1);
-qed "U_F2";
-
-Goal "Mutex \\<in> {s \\<in> state. s`m = #3} LeadsTo {s \\<in> state. s`p=1}";
-by (res_inst_tac [("B", "{s \\<in> state. s`m = #4}")] LeadsTo_Trans 1);
-by (ensures_tac "U4" 2);
-by (ensures_tac "U3" 1);
-qed "U_F3";
-
-
-Goal "Mutex \\<in> {s \\<in> state. s`m = #2} LeadsTo {s \\<in> state. s`p=1}";
-by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
- MRS LeadsTo_Diff) 1);
-by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
-by Auto_tac;
-by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
-val U_lemma2 = result();
-
-Goal "Mutex \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`p =1}";
-by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
-by Auto_tac;
-val U_lemma1 = result();
-
-Goal "i \\<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)";
-by Auto_tac;
-by (auto_tac (claset(), simpset() addsimps [neq_iff_zless]));
-by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4);
-by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 2);
-by (dres_inst_tac [("j", "i"), ("i", "#1")] zle_zless_trans 1);
-by Auto_tac;
-by (rtac zle_anti_sym 1);
-by (ALLGOALS(asm_simp_tac (simpset()
- addsimps [zless_add1_iff_zle RS iff_sym])));
-qed "eq_123";
-
-
-Goal "Mutex \\<in> {s \\<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \\<in> state. s`p=1}";
-by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq,
- LeadsTo_Un_distrib,
- U_lemma1, U_lemma2, U_F3] ) 1);
-val U_lemma123 = result();
-
-
-(*Misra's F4*)
-Goal "Mutex \\<in> {s \\<in> state. s`u = 1} LeadsTo {s \\<in> state. s`p=1}";
-by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
-by Auto_tac;
-qed "u_Leadsto_p";
-
-
-(*** Progress for V ***)
-
-Goalw [Unless_def]
-"Mutex \\<in> {s \\<in> state. s`n=#2} Unless {s \\<in> state. s`n=#3}";
-by (constrains_tac 1);
-qed "V_F0";
-
-Goal "Mutex \\<in> {s \\<in> state. s`n=#1} LeadsTo {s \\<in> state. s`p = not(s`u) & s`n = #2}";
-by (ensures_tac "V1" 1);
-qed "V_F1";
-
-Goal "Mutex \\<in> {s \\<in> state. s`p=1 & s`n = #2} LeadsTo {s \\<in> state. s`n = #3}";
-by (cut_facts_tac [IV] 1);
-by (ensures_tac "V2" 1);
-qed "V_F2";
-
-Goal "Mutex \\<in> {s \\<in> state. s`n = #3} LeadsTo {s \\<in> state. s`p=0}";
-by (res_inst_tac [("B", "{s \\<in> state. s`n = #4}")] LeadsTo_Trans 1);
-by (ensures_tac "V4" 2);
-by (ensures_tac "V3" 1);
-qed "V_F3";
-
-Goal "Mutex \\<in> {s \\<in> state. s`n = #2} LeadsTo {s \\<in> state. s`p=0}";
-by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
- MRS LeadsTo_Diff) 1);
-by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
-by Auto_tac;
-by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def]));
-val V_lemma2 = result();
-
-Goal "Mutex \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`p = 0}";
-by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
-by Auto_tac;
-val V_lemma1 = result();
-
-Goal "Mutex \\<in> {s \\<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \\<in> state. s`p = 0}";
-by (simp_tac (simpset() addsimps
- [n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
- V_lemma1, V_lemma2, V_F3] ) 1);
-val V_lemma123 = result();
-
-(*Misra's F4*)
-Goal "Mutex \\<in> {s \\<in> state. s`v = 1} LeadsTo {s \\<in> state. s`p = 0}";
-by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
-by Auto_tac;
-qed "v_Leadsto_not_p";
-
-(** Absence of starvation **)
-
-(*Misra's F6*)
-Goal "Mutex \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`m = #3}";
-by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
-by (rtac U_F2 2);
-by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
-by (stac Un_commute 1);
-by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
-by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
-by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
-by Auto_tac;
-by (auto_tac (claset() addSDs [v_value_type], simpset() addsimps [bool_def]));
-qed "m1_Leadsto_3";
-
-
-(*The same for V*)
-Goal "Mutex \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`n = #3}";
-by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
-by (rtac V_F2 2);
-by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
-by (stac Un_commute 1);
-by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
-by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
-by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
-by Auto_tac;
-by (auto_tac (claset() addSDs [u_value_type], simpset() addsimps [bool_def]));
-qed "n1_Leadsto_3";
--- a/src/ZF/UNITY/Mutex.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/Mutex.thy Mon Mar 28 16:19:56 2005 +0200
@@ -1,17 +1,26 @@
-(* Title: ZF/UNITY/Mutex.thy
- ID: $Id$
+(* ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
-
-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 expressions reduce to the empty set.
*)
-Mutex = SubstAx +
+header{*Mutual Exclusion*}
+
+theory Mutex
+imports SubstAx
+begin
+
+text{*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 expressions reduce to the empty set.
+*}
+
consts
- p, m, n, u, v :: i
+ p :: i
+ m :: i
+ n :: i
+ u :: i
+ v :: i
translations
"p" == "Var([0])"
@@ -20,12 +29,12 @@
"u" == "Var([0,1])"
"v" == "Var([1,0])"
-rules (** Type declarations **)
- p_type "type_of(p)=bool & default_val(p)=0"
- m_type "type_of(m)=int & default_val(m)=#0"
- n_type "type_of(n)=int & default_val(n)=#0"
- u_type "type_of(u)=bool & default_val(u)=0"
- v_type "type_of(v)=bool & default_val(v)=0"
+axioms --{** Type declarations **}
+ p_type: "type_of(p)=bool & default_val(p)=0"
+ m_type: "type_of(m)=int & default_val(m)=#0"
+ n_type: "type_of(n)=int & default_val(n)=#0"
+ u_type: "type_of(u)=bool & default_val(u)=0"
+ v_type: "type_of(v)=bool & default_val(v)=0"
constdefs
(** The program for process U **)
@@ -82,4 +91,256 @@
"bad_IU == {s:state. (s`u = 1 <-> (#1 $<= s`m & s`m $<= #3))&
(#3 $<= s`m & s`m $<= #4 --> s`p=0)}"
+
+(* Title: ZF/UNITY/Mutex.ML
+ ID: $Id \<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
+ Author: Sidi O Ehmety, Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+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 \<in> an ill-tyed expression will
+reduce to the empty set.
+
+*)
+
+(** Variables' types **)
+
+declare p_type [simp] u_type [simp] v_type [simp] m_type [simp] n_type [simp]
+
+lemma u_value_type: "s \<in> state ==>s`u \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = u in apply_type, auto)
+done
+
+lemma v_value_type: "s \<in> state ==> s`v \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = v in apply_type, auto)
+done
+
+lemma p_value_type: "s \<in> state ==> s`p \<in> bool"
+apply (unfold state_def)
+apply (drule_tac a = p in apply_type, auto)
+done
+
+lemma m_value_type: "s \<in> state ==> s`m \<in> int"
+apply (unfold state_def)
+apply (drule_tac a = m in apply_type, auto)
+done
+
+lemma n_value_type: "s \<in> state ==>s`n \<in> int"
+apply (unfold state_def)
+apply (drule_tac a = n in apply_type, auto)
+done
+
+declare p_value_type [simp] u_value_type [simp] v_value_type [simp]
+ m_value_type [simp] n_value_type [simp]
+
+declare p_value_type [TC] u_value_type [TC] v_value_type [TC]
+ m_value_type [TC] n_value_type [TC]
+
+
+
+text{*Mutex is a program*}
+
+lemma Mutex_in_program [simp,TC]: "Mutex \<in> program"
+by (simp add: Mutex_def)
+
+
+method_setup constrains = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.METHOD (fn facts =>
+ gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
+ "for proving safety properties"
+
+
+declare Mutex_def [THEN def_prg_Init, simp]
+ML
+{*
+program_defs_ref := [thm"Mutex_def"]
+*}
+
+declare U0_def [THEN def_act_simp, simp]
+declare U1_def [THEN def_act_simp, simp]
+declare U2_def [THEN def_act_simp, simp]
+declare U3_def [THEN def_act_simp, simp]
+declare U4_def [THEN def_act_simp, simp]
+
+declare V0_def [THEN def_act_simp, simp]
+declare V1_def [THEN def_act_simp, simp]
+declare V2_def [THEN def_act_simp, simp]
+declare V3_def [THEN def_act_simp, simp]
+declare V4_def [THEN def_act_simp, simp]
+
+declare U0_def [THEN def_set_simp, simp]
+declare U1_def [THEN def_set_simp, simp]
+declare U2_def [THEN def_set_simp, simp]
+declare U3_def [THEN def_set_simp, simp]
+declare U4_def [THEN def_set_simp, simp]
+
+declare V0_def [THEN def_set_simp, simp]
+declare V1_def [THEN def_set_simp, simp]
+declare V2_def [THEN def_set_simp, simp]
+declare V3_def [THEN def_set_simp, simp]
+declare V4_def [THEN def_set_simp, simp]
+
+declare IU_def [THEN def_set_simp, simp]
+declare IV_def [THEN def_set_simp, simp]
+declare bad_IU_def [THEN def_set_simp, simp]
+
+lemma IU: "Mutex \<in> Always(IU)"
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, constrains, auto)
+done
+
+lemma IV: "Mutex \<in> Always(IV)"
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, constrains)
+done
+
+(*The safety property: mutual exclusion*)
+lemma mutual_exclusion: "Mutex \<in> Always({s \<in> state. ~(s`m = #3 & s`n = #3)})"
+apply (rule Always_weaken)
+apply (rule Always_Int_I [OF IU IV], auto)
+done
+
+(*The bad invariant FAILS in V1*)
+
+lemma less_lemma: "[| x$<#1; #3 $<= x |] ==> P"
+apply (drule_tac j = "#1" and k = "#3" in zless_zle_trans)
+apply (drule_tac [2] j = x in zle_zless_trans, auto)
+done
+
+lemma "Mutex \<in> Always(bad_IU)"
+apply (rule AlwaysI, force)
+apply (unfold Mutex_def, constrains, auto)
+apply (subgoal_tac "#1 $<= #3")
+apply (drule_tac x = "#1" and y = "#3" in zle_trans, auto)
+apply (simp (no_asm) add: not_zless_iff_zle [THEN iff_sym])
+apply auto
+(*Resulting state: n=1, p=false, m=4, u=false.
+ Execution of V1 (the command of process v guarded by n=1) sets p:=true,
+ violating the invariant!*)
+oops
+
+
+
+(*** Progress for U ***)
+
+lemma U_F0: "Mutex \<in> {s \<in> state. s`m=#2} Unless {s \<in> state. s`m=#3}"
+by (unfold Unless_def Mutex_def, constrains)
+
+lemma U_F1:
+ "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
+by (unfold Mutex_def, ensures_tac U1)
+
+lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
+apply (cut_tac IU)
+apply (unfold Mutex_def, ensures_tac U2)
+done
+
+lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
+apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
+ apply (unfold Mutex_def)
+ apply (ensures_tac U3)
+apply (ensures_tac U4)
+done
+
+
+lemma U_lemma2: "Mutex \<in> {s \<in> state. s`m = #2} LeadsTo {s \<in> state. s`p=1}"
+apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
+ Int_lower2 [THEN subset_imp_LeadsTo]])
+apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
+apply (auto dest!: p_value_type simp add: bool_def)
+done
+
+lemma U_lemma1: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`p =1}"
+by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
+
+lemma eq_123: "i \<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"
+apply auto
+apply (auto simp add: neq_iff_zless)
+apply (drule_tac [4] j = "#3" and i = i in zle_zless_trans)
+apply (drule_tac [2] j = i and i = "#1" in zle_zless_trans)
+apply (drule_tac j = i and i = "#1" in zle_zless_trans, auto)
+apply (rule zle_anti_sym)
+apply (simp_all (no_asm_simp) add: zless_add1_iff_zle [THEN iff_sym])
+done
+
+
+lemma U_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \<in> state. s`p=1}"
+by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
+
+
+(*Misra's F4*)
+lemma u_Leadsto_p: "Mutex \<in> {s \<in> state. s`u = 1} LeadsTo {s \<in> state. s`p=1}"
+by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
+
+
+(*** Progress for V ***)
+
+lemma V_F0: "Mutex \<in> {s \<in> state. s`n=#2} Unless {s \<in> state. s`n=#3}"
+by (unfold Unless_def Mutex_def, constrains)
+
+lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
+by (unfold Mutex_def, ensures_tac "V1")
+
+lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
+apply (cut_tac IV)
+apply (unfold Mutex_def, ensures_tac "V2")
+done
+
+lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
+apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
+ apply (unfold Mutex_def)
+ apply (ensures_tac V3)
+apply (ensures_tac V4)
+done
+
+lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
+apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
+ Int_lower2 [THEN subset_imp_LeadsTo]])
+apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto)
+apply (auto dest!: p_value_type simp add: bool_def)
+done
+
+lemma V_lemma1: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`p = 0}"
+by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
+
+lemma V_lemma123: "Mutex \<in> {s \<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \<in> state. s`p = 0}"
+by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
+
+(*Misra's F4*)
+lemma v_Leadsto_not_p: "Mutex \<in> {s \<in> state. s`v = 1} LeadsTo {s \<in> state. s`p = 0}"
+by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
+
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+lemma m1_Leadsto_3: "Mutex \<in> {s \<in> state. s`m = #1} LeadsTo {s \<in> state. s`m = #3}"
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+apply (rule_tac [2] U_F2)
+apply (simp add: Collect_conj_eq)
+apply (subst Un_commute)
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+ apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0])
+apply (rule U_F1 [THEN LeadsTo_weaken_R], auto)
+apply (auto dest!: v_value_type simp add: bool_def)
+done
+
+
+(*The same for V*)
+lemma n1_Leadsto_3: "Mutex \<in> {s \<in> state. s`n = #1} LeadsTo {s \<in> state. s`n = #3}"
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+apply (rule_tac [2] V_F2)
+apply (simp add: Collect_conj_eq)
+apply (subst Un_commute)
+apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
+ apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0])
+apply (rule V_F1 [THEN LeadsTo_weaken_R], auto)
+apply (auto dest!: u_value_type simp add: bool_def)
+done
+
end
\ No newline at end of file
--- a/src/ZF/UNITY/SubstAx.ML Sat Mar 26 18:20:29 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,416 +0,0 @@
-(* Title: ZF/UNITY/SubstAx.ML
- ID: $Id \\<in> SubstAx.ML,v 1.8 2003/05/27 09:39:06 paulson Exp $
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-LeadsTo relation, restricted to the set of reachable states.
-
-*)
-
-
-(*Resembles the previous definition of LeadsTo*)
-
-(* Equivalence with the HOL-like definition *)
-Goalw [LeadsTo_def]
-"st_set(B)==> A LeadsTo B = {F \\<in> program. F:(reachable(F) Int A) leadsTo B}";
-by (blast_tac (claset() addDs [psp_stable2, leadsToD2, constrainsD2]
- addIs [leadsTo_weaken]) 1);
-qed "LeadsTo_eq";
-
-Goalw [LeadsTo_def] "A LeadsTo B <=program";
-by Auto_tac;
-qed "LeadsTo_type";
-
-(*** Specialized laws for handling invariants ***)
-
-(** Conjoining an Always property **)
-Goal "F \\<in> Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \\<in> A LeadsTo A')";
-by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
- Int_absorb2, Int_assoc RS sym, leadsToD2]) 1);
-qed "Always_LeadsTo_pre";
-
-Goalw [LeadsTo_def] "F \\<in> Always(I) ==> (F \\<in> A LeadsTo (I Int A')) <-> (F \\<in> 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 \\<in> Always(C); F \\<in> (C Int A) LeadsTo A' |] ==> F \\<in> 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 \\<in> Always(C); F \\<in> A LeadsTo A' |] ==> F \\<in> A LeadsTo (C Int A')";
-by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1);
-qed "Always_LeadsToD";
-
-(*** Introduction rules \\<in> Basis, Trans, Union ***)
-
-Goal "F \\<in> A Ensures B ==> F \\<in> A LeadsTo B";
-by (auto_tac (claset(), simpset() addsimps
- [Ensures_def, LeadsTo_def]));
-qed "LeadsTo_Basis";
-
-Goal "[| F \\<in> A LeadsTo B; F \\<in> B LeadsTo C |] ==> F \\<in> A LeadsTo C";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
-qed "LeadsTo_Trans";
-
-val [major, program] = Goalw [LeadsTo_def]
-"[|(!!A. A \\<in> S ==> F \\<in> A LeadsTo B); F \\<in> program|]==>F \\<in> Union(S) LeadsTo B";
-by (cut_facts_tac [program] 1);
-by Auto_tac;
-by (stac Int_Union_Union2 1);
-by (rtac leadsTo_UN 1);
-by (dtac major 1);
-by Auto_tac;
-qed "LeadsTo_Union";
-
-(*** Derived rules ***)
-
-Goal "F \\<in> A leadsTo B ==> F \\<in> A LeadsTo B";
-by (ftac 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 \\<in> A LeadsTo (A' Un A') ==> F \\<in> A LeadsTo A'";
-by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
-qed "LeadsTo_Un_duplicate";
-
-Goal "F \\<in> A LeadsTo (A' Un C Un C) ==> F \\<in> A LeadsTo (A' Un C)";
-by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
-qed "LeadsTo_Un_duplicate2";
-
-val [major, program] = Goalw [LeadsTo_def]
-"[|(!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo B); F \\<in> program|]==>F:(\\<Union>i \\<in> I. A(i)) LeadsTo B";
-by (cut_facts_tac [program] 1);
-by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 1);
-by (rtac leadsTo_UN 1);
-by (dtac major 1);
-by Auto_tac;
-qed "LeadsTo_UN";
-
-(*Binary union introduction rule*)
-Goal "[| F \\<in> A LeadsTo C; F \\<in> B LeadsTo C |] ==> F \\<in> (A Un B) LeadsTo C";
-by (stac Un_eq_Union 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*)
-val [major, program] = Goal
-"[|(!!s. s \\<in> A ==> F:{s} LeadsTo B); F \\<in> program|]==>F \\<in> A LeadsTo B";
-by (cut_facts_tac [program] 1);
-by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
-by (ftac major 1);
-by Auto_tac;
-qed "single_LeadsTo_I";
-
-Goal "[| A <= B; F \\<in> program |] ==> F \\<in> 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";
-
-Goal "F:0 LeadsTo A <-> F \\<in> 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 \\<in> A LeadsTo state <-> F \\<in> program";
-by (auto_tac (claset() addDs [LeadsTo_type RS subsetD],
- simpset() addsimps [LeadsTo_eq]));
-qed "LeadsTo_state";
-AddIffs [LeadsTo_state];
-
-Goalw [LeadsTo_def]
- "[| F \\<in> A LeadsTo A'; A'<=B'|] ==> F \\<in> A LeadsTo B'";
-by (auto_tac (claset() addIs[leadsTo_weaken_R], simpset()));
-qed_spec_mp "LeadsTo_weaken_R";
-
-Goalw [LeadsTo_def] "[| F \\<in> A LeadsTo A'; B <= A |] ==> F \\<in> B LeadsTo A'";
-by (auto_tac (claset() addIs[leadsTo_weaken_L], simpset()));
-qed_spec_mp "LeadsTo_weaken_L";
-
-Goal "[| F \\<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \\<in> B LeadsTo B'";
-by (blast_tac (claset() addIs [LeadsTo_weaken_R,
- LeadsTo_weaken_L, LeadsTo_Trans]) 1);
-qed "LeadsTo_weaken";
-
-Goal
-"[| F \\<in> Always(C); F \\<in> A LeadsTo A'; C Int B <= A; C Int A' <= B' |] \
-\ ==> F \\<in> B LeadsTo B'";
-by (blast_tac (claset() addDs [Always_LeadsToI]
- addIs [LeadsTo_weaken, Always_LeadsToD]) 1);
-qed "Always_LeadsTo_weaken";
-
-(** Two theorems for "proof lattices" **)
-
-Goal "F \\<in> A LeadsTo B ==> F:(A Un B) LeadsTo B";
-by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]
- addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
-qed "LeadsTo_Un_post";
-
-Goal "[| F \\<in> A LeadsTo B; F \\<in> B LeadsTo C |] \
-\ ==> F \\<in> (A Un B) LeadsTo C";
-by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
- LeadsTo_weaken_L, LeadsTo_Trans]
- addDs [LeadsTo_type RS subsetD]) 1);
-qed "LeadsTo_Trans_Un";
-
-(** Distributive laws **)
-Goal "(F \\<in> (A Un B) LeadsTo C) <-> (F \\<in> A LeadsTo C & F \\<in> B LeadsTo C)";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
-qed "LeadsTo_Un_distrib";
-
-Goal "(F \\<in> (\\<Union>i \\<in> I. A(i)) LeadsTo B) <-> (\\<forall>i \\<in> I. F \\<in> A(i) LeadsTo B) & F \\<in> program";
-by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]
- addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
-qed "LeadsTo_UN_distrib";
-
-Goal "(F \\<in> Union(S) LeadsTo B) <-> (\\<forall>A \\<in> S. F \\<in> A LeadsTo B) & F \\<in> 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(I)" **)
-
-Goal "[| F:(A-B) Co (A Un B); F \\<in> transient (A-B) |] ==> F \\<in> A Ensures B";
-by (asm_full_simp_tac
- (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
-by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
- transient_strengthen]
- addDs [constrainsD2]) 1);
-qed "EnsuresI";
-
-Goal "[| F \\<in> Always(I); F \\<in> (I Int (A-A')) Co (A Un A'); \
-\ F \\<in> transient (I Int (A-A')) |] \
-\ ==> F \\<in> A LeadsTo A'";
-by (rtac Always_LeadsToI 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
- Always_ConstrainsD RS Constrains_weaken,
- transient_strengthen]) 1);
-qed "Always_LeadsTo_Basis";
-
-(*Set difference \\<in> maybe combine with leadsTo_weaken_L??
- This is the most useful form of the "disjunction" rule*)
-Goal "[| F \\<in> (A-B) LeadsTo C; F \\<in> (A Int B) LeadsTo C |] ==> F \\<in> A LeadsTo C";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
-qed "LeadsTo_Diff";
-
-val [major, minor] = Goal
-"[|(!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo A'(i)); F \\<in> program |] \
-\ ==> F \\<in> (\\<Union>i \\<in> I. A(i)) LeadsTo (\\<Union>i \\<in> I. A'(i))";
-by (cut_facts_tac [minor] 1);
-by (rtac LeadsTo_Union 1);
-by (ALLGOALS(Clarify_tac));
-by (ftac major 1);
-by (blast_tac (claset() addIs [LeadsTo_weaken_R]) 1);
-qed "LeadsTo_UN_UN";
-
-(*Binary union version*)
-Goal "[| F \\<in> A LeadsTo A'; F \\<in> 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 \\<in> A LeadsTo(A' Un B); F \\<in> B LeadsTo B' |] ==> F \\<in> 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 \\<in> A LeadsTo (A' Un B); F \\<in> (B-A') LeadsTo B' |] ==> F \\<in> 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 \\<in> A LeadsTo (B Un A'); F \\<in> B LeadsTo B' |] ==> F \\<in> 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 \\<in> A LeadsTo (B Un A'); F \\<in> (B-A') LeadsTo B' |] ==> F \\<in> 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 \\<in> A LeadsTo 0 ==> F \\<in> Always (state -A)";
-by (full_simp_tac (simpset()
- addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1);
-by (cut_facts_tac [reachable_type] 1);
-by (auto_tac (claset() addSDs [leadsTo_empty], simpset()));
-qed "LeadsTo_empty";
-
-(** PSP \\<in> Progress-Safety-Progress **)
-
-(*Special case of PSP \\<in> Misra's "stable conjunction"*)
-Goal "[| F \\<in> A LeadsTo A'; F \\<in> 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 (REPEAT(asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1));
-qed "PSP_Stable";
-
-Goal "[| F \\<in> A LeadsTo A'; F \\<in> Stable(B) |] ==> F \\<in> (B Int A) LeadsTo (B Int A')";
-by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1);
-qed "PSP_Stable2";
-
-Goal "[| F \\<in> A LeadsTo A'; F \\<in> B Co B'|]==> F \\<in> (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 \\<in> A LeadsTo A'; F \\<in> 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 \\<in> A LeadsTo A'; F \\<in> B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')";
-by (rewtac Unless_def);
-by (dtac PSP 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, subset_imp_LeadsTo]) 1);
-qed "PSP_Unless";
-
-(*** Induction rules ***)
-
-(** Meta or object quantifier ????? **)
-Goal "[| wf(r); \
-\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) LeadsTo \
-\ ((A Int f-``(converse(r) `` {m})) Un B); \
-\ field(r)<=I; A<=f-``I; F \\<in> program |] \
-\ ==> F \\<in> A LeadsTo B";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by Auto_tac;
-by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1);
-by (ALLGOALS(Clarify_tac));
-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 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 "[| \\<forall>m \\<in> nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B); \
-\ A<=f-``nat; F \\<in> program |] ==> F \\<in> A LeadsTo B";
-by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
- (wf_measure RS LeadsTo_wf_induct) 1);
-by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [nat_measure_field])));
-by (asm_simp_tac (simpset() addsimps [ltI, Image_inverse_lessThan, symmetric vimage_def]) 1);
-qed "LessThan_induct";
-
-
-(******
- To be ported ??? I am not sure.
-
- integ_0_le_induct
- LessThan_bounded_induct
- GreaterThan_bounded_induct
-
-*****)
-
-(*** Completion \\<in> Binary and General Finite versions ***)
-
-Goal "[| F \\<in> A LeadsTo (A' Un C); F \\<in> A' Co (A' Un C); \
-\ F \\<in> B LeadsTo (B' Un C); F \\<in> B' Co (B' Un C) |] \
-\ ==> F \\<in> (A Int B) LeadsTo ((A' Int B') Un C)";
-by (full_simp_tac
- (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains,
- Int_Un_distrib]) 1);
-by Safe_tac;
-by (REPEAT(Blast_tac 2));
-by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
-qed "Completion";
-
-Goal "[| I \\<in> Fin(X);F \\<in> program |] \
-\ ==> (\\<forall>i \\<in> I. F \\<in> (A(i)) LeadsTo (A'(i) Un C)) --> \
-\ (\\<forall>i \\<in> I. F \\<in> (A'(i)) Co (A'(i) Un C)) --> \
-\ F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
-by (etac Fin_induct 1);
-by (auto_tac (claset(), simpset() delsimps INT_simps
- addsimps [Inter_0]));
-by (rtac Completion 1);
-by (asm_simp_tac (simpset() delsimps INT_simps addsimps INT_extend_simps) 4);
-by (rtac Constrains_INT 4);
-by (REPEAT(Blast_tac 1));
-val lemma = result();
-
-val prems = Goal
- "[| I \\<in> Fin(X); !!i. i \\<in> I ==> F \\<in> A(i) LeadsTo (A'(i) Un C); \
-\ !!i. i \\<in> I ==> F \\<in> A'(i) Co (A'(i) Un C); \
-\ F \\<in> program |] \
-\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
-by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
-qed "Finite_completion";
-
-Goalw [Stable_def]
- "[| F \\<in> A LeadsTo A'; F \\<in> Stable(A'); \
-\ F \\<in> B LeadsTo B'; F \\<in> Stable(B') |] \
-\ ==> F \\<in> (A Int B) LeadsTo (A' Int B')";
-by (res_inst_tac [("C1", "0")] (Completion RS LeadsTo_weaken_R) 1);
-by (Asm_full_simp_tac 5);
-by (rtac subset_refl 5);
-by Auto_tac;
-qed "Stable_completion";
-
-val prems = Goalw [Stable_def]
- "[| I \\<in> Fin(X); \
-\ (!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo A'(i)); \
-\ (!!i. i \\<in> I ==>F \\<in> Stable(A'(i))); F \\<in> program |] \
-\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo (\\<Inter>i \\<in> I. A'(i))";
-by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1);
-by (ALLGOALS(Simp_tac));
-by (rtac subset_refl 5);
-by (REPEAT(blast_tac (claset() addIs prems) 1));
-qed "Finite_stable_completion";
-
-
-(*proves "ensures/leadsTo" properties when the program is specified*)
-fun ensures_tac sact =
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- etac Always_LeadsTo_Basis 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
- EnsuresI, ensuresI] 1),
- (*now there are two subgoals \\<in> co & transient*)
- simp_tac (simpset() addsimps !program_defs_ref) 2,
- res_inst_tac [("act", sact)] transientI 2,
- (*simplify the command's domain*)
- simp_tac (simpset() addsimps [domain_def]) 3,
- (* proving the domain part *)
- Clarify_tac 3, dtac swap 3, Force_tac 4,
- rtac ReplaceI 3, Force_tac 3, Force_tac 4,
- Asm_full_simp_tac 3, rtac conjI 3, Simp_tac 4,
- REPEAT (rtac state_update_type 3),
- constrains_tac 1,
- ALLGOALS Clarify_tac,
- ALLGOALS (asm_full_simp_tac
- (simpset() addsimps [st_set_def])),
- ALLGOALS Clarify_tac,
- ALLGOALS (Asm_full_simp_tac)]);
-
--- a/src/ZF/UNITY/SubstAx.thy Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Mon Mar 28 16:19:56 2005 +0200
@@ -1,24 +1,441 @@
-(* Title: ZF/UNITY/SubstAx.thy
- ID: $Id$
+(* ID: $Id$
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
-Weak LeadsTo relation (restricted to the set of reachable states)
-
Theory ported from HOL.
*)
-SubstAx = WFair + Constrains +
+header{*Weak LeadsTo relation (restricted to the set of reachable states)*}
+
+theory SubstAx
+imports WFair Constrains
+
+begin
constdefs
(* The definitions below are not `conventional', but yields simpler rules *)
- Ensures :: "[i,i] => i" (infixl 60)
+ Ensures :: "[i,i] => i" (infixl "Ensures" 60)
"A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }"
- LeadsTo :: "[i, i] => i" (infixl 60)
+ LeadsTo :: "[i, i] => i" (infixl "LeadsTo" 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)
+ "LeadsTo" :: "[i, i] => i" (infixl " \<longmapsto>w " 60)
+
+
+
+(*Resembles the previous definition of LeadsTo*)
+
+(* Equivalence with the HOL-like definition *)
+lemma LeadsTo_eq:
+"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) Int A) leadsTo B}"
+apply (unfold LeadsTo_def)
+apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
+done
+
+lemma LeadsTo_type: "A LeadsTo B <=program"
+by (unfold LeadsTo_def, auto)
+
+(*** Specialized laws for handling invariants ***)
+
+(** Conjoining an Always property **)
+lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \<in> A LeadsTo A')"
+by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
+
+lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I Int A')) <-> (F \<in> A LeadsTo A')"
+apply (unfold LeadsTo_def)
+apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
+done
+
+(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
+lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C Int A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"
+by (blast intro: Always_LeadsTo_pre [THEN iffD1])
+
+(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
+lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C Int A')"
+by (blast intro: Always_LeadsTo_post [THEN iffD2])
+
+(*** Introduction rules \<in> Basis, Trans, Union ***)
+
+lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
+by (auto simp add: Ensures_def LeadsTo_def)
+
+lemma LeadsTo_Trans:
+ "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
+apply (simp (no_asm_use) add: LeadsTo_def)
+apply (blast intro: leadsTo_Trans)
+done
+
+lemma LeadsTo_Union:
+"[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> Union(S) LeadsTo B"
+apply (simp add: LeadsTo_def)
+apply (subst Int_Union_Union2)
+apply (rule leadsTo_UN, auto)
+done
+
+(*** Derived rules ***)
+
+lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
+apply (frule leadsToD2, clarify)
+apply (simp (no_asm_simp) add: LeadsTo_eq)
+apply (blast intro: leadsTo_weaken_L)
+done
+
+(*Useful with cancellation, disjunction*)
+lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' Un A') ==> F \<in> A LeadsTo A'"
+by (simp add: Un_ac)
+
+lemma LeadsTo_Un_duplicate2:
+ "F \<in> A LeadsTo (A' Un C Un C) ==> F \<in> A LeadsTo (A' Un C)"
+by (simp add: Un_ac)
+
+lemma LeadsTo_UN:
+ "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]
+ ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"
+apply (simp add: LeadsTo_def)
+apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
+apply (rule leadsTo_UN, auto)
+done
+
+(*Binary union introduction rule*)
+lemma LeadsTo_Un:
+ "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A Un B) LeadsTo C"
+apply (subst Un_eq_Union)
+apply (rule LeadsTo_Union)
+apply (auto dest: LeadsTo_type [THEN subsetD])
+done
+
+(*Lets us look at the starting state*)
+lemma single_LeadsTo_I:
+ "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"
+apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
+done
+
+lemma subset_imp_LeadsTo: "[| A <= B; F \<in> program |] ==> F \<in> A LeadsTo B"
+apply (simp (no_asm_simp) add: LeadsTo_def)
+apply (blast intro: subset_imp_leadsTo)
+done
+
+lemma empty_LeadsTo: "F:0 LeadsTo A <-> F \<in> program"
+by (auto dest: LeadsTo_type [THEN subsetD]
+ intro: empty_subsetI [THEN subset_imp_LeadsTo])
+declare empty_LeadsTo [iff]
+
+lemma LeadsTo_state: "F \<in> A LeadsTo state <-> F \<in> program"
+by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
+declare LeadsTo_state [iff]
+
+lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A'; A'<=B'|] ==> F \<in> A LeadsTo B'"
+apply (unfold LeadsTo_def)
+apply (auto intro: leadsTo_weaken_R)
+done
+
+lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B <= A |] ==> F \<in> B LeadsTo A'"
+apply (unfold LeadsTo_def)
+apply (auto intro: leadsTo_weaken_L)
+done
+
+lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"
+by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
+
+lemma Always_LeadsTo_weaken:
+"[| F \<in> Always(C); F \<in> A LeadsTo A'; C Int B <= A; C Int A' <= B' |]
+ ==> F \<in> B LeadsTo B'"
+apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
+done
+
+(** Two theorems for "proof lattices" **)
+
+lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A Un B) LeadsTo B"
+by (blast dest: LeadsTo_type [THEN subsetD]
+ intro: LeadsTo_Un subset_imp_LeadsTo)
+
+lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |]
+ ==> F \<in> (A Un B) LeadsTo C"
+apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
+done
+
+(** Distributive laws **)
+lemma LeadsTo_Un_distrib: "(F \<in> (A Un B) LeadsTo C) <-> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
+by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
+
+lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) <-> (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"
+by (blast dest: LeadsTo_type [THEN subsetD]
+ intro: LeadsTo_UN LeadsTo_weaken_L)
+
+lemma LeadsTo_Union_distrib: "(F \<in> Union(S) LeadsTo B) <-> (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"
+by (blast dest: LeadsTo_type [THEN subsetD]
+ intro: LeadsTo_Union LeadsTo_weaken_L)
+
+(** More rules using the premise "Always(I)" **)
+
+lemma EnsuresI: "[| F:(A-B) Co (A Un B); F \<in> transient (A-B) |] ==> F \<in> A Ensures B"
+apply (simp add: Ensures_def Constrains_eq_constrains)
+apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)
+done
+
+lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I Int (A-A')) Co (A Un A');
+ F \<in> transient (I Int (A-A')) |]
+ ==> F \<in> A LeadsTo A'"
+apply (rule Always_LeadsToI, assumption)
+apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
+done
+
+(*Set difference: maybe combine with leadsTo_weaken_L??
+ This is the most useful form of the "disjunction" rule*)
+lemma LeadsTo_Diff:
+ "[| F \<in> (A-B) LeadsTo C; F \<in> (A Int B) LeadsTo C |] ==> F \<in> A LeadsTo C"
+by (blast intro: LeadsTo_Un LeadsTo_weaken)
+
+lemma LeadsTo_UN_UN:
+ "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]
+ ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"
+apply (rule LeadsTo_Union, auto)
+apply (blast intro: LeadsTo_weaken_R)
+done
+
+(*Binary union version*)
+lemma LeadsTo_Un_Un:
+ "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')"
+by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
+
+(** The cancellation law **)
+
+lemma LeadsTo_cancel2: "[| F \<in> A LeadsTo(A' Un B); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"
+by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
+
+lemma Un_Diff: "A Un (B - A) = A Un B"
+by auto
+
+lemma LeadsTo_cancel_Diff2: "[| F \<in> A LeadsTo (A' Un B); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"
+apply (rule LeadsTo_cancel2)
+prefer 2 apply assumption
+apply (simp (no_asm_simp) add: Un_Diff)
+done
+
+lemma LeadsTo_cancel1: "[| F \<in> A LeadsTo (B Un A'); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"
+apply (simp add: Un_commute)
+apply (blast intro!: LeadsTo_cancel2)
+done
+
+lemma Diff_Un2: "(B - A) Un A = B Un A"
+by auto
+
+lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B Un A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"
+apply (rule LeadsTo_cancel1)
+prefer 2 apply assumption
+apply (simp (no_asm_simp) add: Diff_Un2)
+done
+
+(** The impossibility law **)
+
+(*The set "A" may be non-empty, but it contains no reachable states*)
+lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"
+apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
+apply (cut_tac reachable_type)
+apply (auto dest!: leadsTo_empty)
+done
+
+(** PSP \<in> Progress-Safety-Progress **)
+
+(*Special case of PSP \<in> Misra's "stable conjunction"*)
+lemma PSP_Stable: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |]==> F:(A Int B) LeadsTo (A' Int B)"
+apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
+apply (drule psp_stable, assumption)
+apply (simp add: Int_ac)
+done
+
+lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B Int A) LeadsTo (B Int A')"
+apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
+done
+
+lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
+apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
+apply (blast dest: psp intro: leadsTo_weaken)
+done
+
+lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"
+by (simp (no_asm_simp) add: PSP Int_ac)
+
+lemma PSP_Unless:
+"[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"
+apply (unfold Unless_def)
+apply (drule PSP, assumption)
+apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
+done
+
+(*** Induction rules ***)
+
+(** Meta or object quantifier ????? **)
+lemma LeadsTo_wf_induct: "[| wf(r);
+ \<forall>m \<in> I. F \<in> (A Int f-``{m}) LeadsTo
+ ((A Int f-``(converse(r) `` {m})) Un B);
+ field(r)<=I; A<=f-``I; F \<in> program |]
+ ==> F \<in> A LeadsTo B"
+apply (simp (no_asm_use) add: LeadsTo_def)
+apply auto
+apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
+apply (drule_tac [2] x = m in bspec, safe)
+apply (rule_tac [2] A' = "reachable (F) Int (A Int f -`` (converse (r) ``{m}) Un B) " in leadsTo_weaken_R)
+apply (auto simp add: Int_assoc)
+done
+
+
+lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B);
+ A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"
+apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])
+apply (simp_all add: nat_measure_field)
+apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
+done
+
+
+(******
+ To be ported ??? I am not sure.
+
+ integ_0_le_induct
+ LessThan_bounded_induct
+ GreaterThan_bounded_induct
+
+*****)
+
+(*** Completion \<in> Binary and General Finite versions ***)
+
+lemma Completion: "[| F \<in> A LeadsTo (A' Un C); F \<in> A' Co (A' Un C);
+ F \<in> B LeadsTo (B' Un C); F \<in> B' Co (B' Un C) |]
+ ==> F \<in> (A Int B) LeadsTo ((A' Int B') Un C)"
+apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
+apply (blast intro: completion leadsTo_weaken)
+done
+
+lemma Finite_completion_aux:
+ "[| I \<in> Fin(X);F \<in> program |]
+ ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) Un C)) -->
+ (\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) Un C)) -->
+ F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
+apply (erule Fin_induct)
+apply (auto simp del: INT_simps simp add: Inter_0)
+apply (rule Completion, auto)
+apply (simp del: INT_simps add: INT_extend_simps)
+apply (blast intro: Constrains_INT)
+done
+
+lemma Finite_completion:
+ "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) Un C);
+ !!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) Un C);
+ F \<in> program |]
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
+by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
+
+lemma Stable_completion:
+ "[| F \<in> A LeadsTo A'; F \<in> Stable(A');
+ F \<in> B LeadsTo B'; F \<in> Stable(B') |]
+ ==> F \<in> (A Int B) LeadsTo (A' Int B')"
+apply (unfold Stable_def)
+apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
+ prefer 5
+ apply blast
+apply auto
+done
+
+lemma Finite_stable_completion:
+ "[| I \<in> Fin(X);
+ (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));
+ (!!i. i \<in> I ==>F \<in> Stable(A'(i))); F \<in> program |]
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"
+apply (unfold Stable_def)
+apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
+apply (rule_tac [3] subset_refl, auto)
+done
+
+ML
+{*
+val LeadsTo_eq = thm "LeadsTo_eq";
+val LeadsTo_type = thm "LeadsTo_type";
+val Always_LeadsTo_pre = thm "Always_LeadsTo_pre";
+val Always_LeadsTo_post = thm "Always_LeadsTo_post";
+val Always_LeadsToI = thm "Always_LeadsToI";
+val Always_LeadsToD = thm "Always_LeadsToD";
+val LeadsTo_Basis = thm "LeadsTo_Basis";
+val LeadsTo_Trans = thm "LeadsTo_Trans";
+val LeadsTo_Union = thm "LeadsTo_Union";
+val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo";
+val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate";
+val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2";
+val LeadsTo_UN = thm "LeadsTo_UN";
+val LeadsTo_Un = thm "LeadsTo_Un";
+val single_LeadsTo_I = thm "single_LeadsTo_I";
+val subset_imp_LeadsTo = thm "subset_imp_LeadsTo";
+val empty_LeadsTo = thm "empty_LeadsTo";
+val LeadsTo_state = thm "LeadsTo_state";
+val LeadsTo_weaken_R = thm "LeadsTo_weaken_R";
+val LeadsTo_weaken_L = thm "LeadsTo_weaken_L";
+val LeadsTo_weaken = thm "LeadsTo_weaken";
+val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken";
+val LeadsTo_Un_post = thm "LeadsTo_Un_post";
+val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un";
+val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib";
+val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib";
+val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib";
+val EnsuresI = thm "EnsuresI";
+val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis";
+val LeadsTo_Diff = thm "LeadsTo_Diff";
+val LeadsTo_UN_UN = thm "LeadsTo_UN_UN";
+val LeadsTo_Un_Un = thm "LeadsTo_Un_Un";
+val LeadsTo_cancel2 = thm "LeadsTo_cancel2";
+val Un_Diff = thm "Un_Diff";
+val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2";
+val LeadsTo_cancel1 = thm "LeadsTo_cancel1";
+val Diff_Un2 = thm "Diff_Un2";
+val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1";
+val LeadsTo_empty = thm "LeadsTo_empty";
+val PSP_Stable = thm "PSP_Stable";
+val PSP_Stable2 = thm "PSP_Stable2";
+val PSP = thm "PSP";
+val PSP2 = thm "PSP2";
+val PSP_Unless = thm "PSP_Unless";
+val LeadsTo_wf_induct = thm "LeadsTo_wf_induct";
+val LessThan_induct = thm "LessThan_induct";
+val Completion = thm "Completion";
+val Finite_completion = thm "Finite_completion";
+val Stable_completion = thm "Stable_completion";
+val Finite_stable_completion = thm "Finite_stable_completion";
+
+
+(*proves "ensures/leadsTo" properties when the program is specified*)
+fun gen_ensures_tac(cs,ss) sact =
+ SELECT_GOAL
+ (EVERY [REPEAT (Always_Int_tac 1),
+ etac Always_LeadsTo_Basis 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
+ EnsuresI, ensuresI] 1),
+ (*now there are two subgoals: co & transient*)
+ simp_tac (ss addsimps !program_defs_ref) 2,
+ res_inst_tac [("act", sact)] transientI 2,
+ (*simplify the command's domain*)
+ simp_tac (ss addsimps [domain_def]) 3,
+ (* proving the domain part *)
+ clarify_tac cs 3, dtac swap 3, force_tac (cs,ss) 4,
+ rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
+ asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
+ REPEAT (rtac state_update_type 3),
+ gen_constrains_tac (cs,ss) 1,
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_full_simp_tac (ss addsimps [st_set_def])),
+ ALLGOALS (clarify_tac cs),
+ ALLGOALS (asm_lr_simp_tac ss)]);
+
+fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
+*}
+
+
+method_setup ensures_tac = {*
+ fn args => fn ctxt =>
+ Method.goal_args' (Scan.lift Args.name)
+ (gen_ensures_tac (local_clasimpset_of ctxt))
+ args ctxt *}
+ "for proving progress properties"
+
end
--- a/src/ZF/UNITY/WFair.ML Sat Mar 26 18:20:29 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,755 +0,0 @@
-(* Title: HOL/UNITY/WFair.ML
- ID: $Id \\<in> WFair.ML,v 1.13 2003/06/30 16:15:52 paulson Exp $
- Author: Sidi O Ehmety, Computer Laboratory
- Copyright 2001 University of Cambridge
-
-Weak Fairness versions of transient, ensures, leadsTo.
-
-From Misra, "A Logic for Concurrent Programming", 1994
-*)
-
-(** Ad-hoc set-theory rules **)
-
-Goal "Union(B) Int A = (\\<Union>b \\<in> B. b Int A)";
-by Auto_tac;
-qed "Int_Union_Union";
-
-Goal "A Int Union(B) = (\\<Union>b \\<in> B. A Int b)";
-by Auto_tac;
-qed "Int_Union_Union2";
-
-(*** transient ***)
-
-Goalw [transient_def] "transient(A)<=program";
-by Auto_tac;
-qed "transient_type";
-
-Goalw [transient_def]
-"F \\<in> transient(A) ==> F \\<in> program & st_set(A)";
-by Auto_tac;
-qed "transientD2";
-
-Goal "[| F \\<in> stable(A); F \\<in> transient(A) |] ==> A = 0";
-by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1);
-by (Fast_tac 1);
-qed "stable_transient_empty";
-
-Goalw [transient_def, st_set_def] "[|F \\<in> transient(A); B<=A|] ==> F \\<in> 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;
-qed "transient_strengthen";
-
-Goalw [transient_def]
-"[|act \\<in> Acts(F); A <= domain(act); act``A <= state-A; \
-\ F \\<in> program; st_set(A)|] ==> F \\<in> transient(A)";
-by (Blast_tac 1);
-qed "transientI";
-
-val major::prems =
-Goalw [transient_def] "[| F \\<in> transient(A); \
-\ !!act. [| act \\<in> 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";
-
-Goalw [transient_def] "transient(state) = 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 (auto_tac (claset() addIs [st0_in_state], simpset()));
-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 "B=state" 1);
-by (auto_tac (claset() addIs [st0_in_state], simpset()));
-qed "transient_state2";
-
-Goalw [transient_def] "transient(0) = program";
-by (rtac equalityI 1);
-by Auto_tac;
-qed "transient_empty";
-
-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 \\<in> transient(A-B)|]==>F \\<in> A ensures B";
-by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD]));
-qed "ensuresI";
-
-(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)
-Goal "[| F \\<in> A co A Un B; F \\<in> transient(A) |] ==> F \\<in> 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, transient_type RS subsetD]));
-qed "ensuresI2";
-
-Goalw [ensures_def] "F \\<in> A ensures B ==> F:(A-B) co (A Un B) & F \\<in> transient (A-B)";
-by Auto_tac;
-qed "ensuresD";
-
-Goalw [ensures_def] "[|F \\<in> A ensures A'; A'<=B' |] ==> F \\<in> A ensures B'";
-by (blast_tac (claset()
- addIs [transient_strengthen, constrains_weaken]) 1);
-qed "ensures_weaken_R";
-
-(*The L-version (precondition strengthening) fails, but we have this*)
-Goalw [ensures_def]
- "[| F \\<in> stable(C); F \\<in> A ensures B |] ==> F:(C Int A) ensures (C Int B)";
-by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym]) 1);
-by (blast_tac (claset()
- addIs [transient_strengthen,
- stable_constrains_Int, constrains_weaken]) 1);
-qed "stable_ensures_Int";
-
-Goal "[|F \\<in> stable(A); F \\<in> transient(C); A<=B Un C|] ==> F \\<in> 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]) 1);
-qed "stable_transient_ensures";
-
-Goal "(A ensures B) = (A unless B) Int transient (A-B)";
-by (auto_tac (claset(), simpset() addsimps [ensures_def, unless_def]));
-qed "ensures_eq";
-
-Goal "[| F \\<in> program; A<=B |] ==> F \\<in> 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_left = leads.dom_subset RS subsetD RS SigmaD1;
-val leads_right = leads.dom_subset RS subsetD RS SigmaD2;
-
-Goalw [leadsTo_def] "A leadsTo B <= program";
-by Auto_tac;
-qed "leadsTo_type";
-
-Goalw [leadsTo_def, st_set_def]
-"F \\<in> A leadsTo B ==> F \\<in> program & st_set(A) & st_set(B)";
-by (blast_tac (claset() addDs [leads_left, leads_right]) 1);
-qed "leadsToD2";
-
-Goalw [leadsTo_def, st_set_def]
- "[|F \\<in> A ensures B; st_set(A); st_set(B)|] ==> F \\<in> A leadsTo B";
-by (cut_facts_tac [ensures_type] 1);
-by (auto_tac (claset() addIs [leads.Basis], simpset()));
-qed "leadsTo_Basis";
-AddIs [leadsTo_Basis];
-
-(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
-(* [| F \\<in> 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 \\<in> A leadsTo B; F \\<in> B leadsTo C |]==>F \\<in> A leadsTo C";
-by (auto_tac (claset() addIs [leads.Trans], simpset()));
-qed "leadsTo_Trans";
-
-(* Better when used in association with leadsTo_weaken_R *)
-Goalw [transient_def] "F \\<in> transient(A) ==> F \\<in> A leadsTo (state-A )";
-by (rtac (ensuresI RS leadsTo_Basis) 1);
-by (ALLGOALS(Clarify_tac));
-by (blast_tac (claset() addIs [transientI]) 2);
-by (rtac constrains_weaken 1);
-by Auto_tac;
-qed "transient_imp_leadsTo";
-
-(*Useful with cancellation, disjunction*)
-Goal "F \\<in> A leadsTo (A' Un A') ==> F \\<in> A leadsTo A'";
-by (Asm_full_simp_tac 1);
-qed "leadsTo_Un_duplicate";
-
-Goal "F \\<in> A leadsTo (A' Un C Un C) ==> F \\<in> A leadsTo (A' Un C)";
-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*)
-val [major, program,B]= Goalw [leadsTo_def, st_set_def]
-"[|(!!A. A \\<in> S ==> F \\<in> A leadsTo B); F \\<in> program; st_set(B)|]==>F \\<in> 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";
-
-val [major,program,B] = Goalw [leadsTo_def, st_set_def]
-"[|(!!A. A \\<in> S ==>F:(A Int C) leadsTo B); F \\<in> program; st_set(B)|] \
-\ ==>F:(Union(S)Int C)leadsTo B";
-by (cut_facts_tac [program, B] 1);
-by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1);
-by (resolve_tac [leads.Union] 1);
-by Auto_tac;
-by (ALLGOALS(dtac major));
-by (auto_tac (claset() addDs [leads_left], simpset()));
-qed "leadsTo_Union_Int";
-
-val [major,program,B] = Goalw [leadsTo_def, st_set_def]
-"[|(!!i. i \\<in> I ==> F \\<in> A(i) leadsTo B); F \\<in> program; st_set(B)|]==>F:(\\<Union>i \\<in> 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 *)
-Goal "[| F \\<in> A leadsTo C; F \\<in> B leadsTo C |] ==> F \\<in> (A Un B) leadsTo C";
-by (stac Un_eq_Union 1);
-by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1);
-qed "leadsTo_Un";
-
-val [major, program, B] = Goal
-"[|(!!x. x \\<in> A==> F:{x} leadsTo B); F \\<in> program; st_set(B) |] ==> F \\<in> 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 \\<in> program; st_set(A) |] ==> F \\<in> A leadsTo A";
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
-qed "leadsTo_refl";
-
-Goal "F \\<in> A leadsTo A <-> F \\<in> program & st_set(A)";
-by (auto_tac (claset() addIs [leadsTo_refl]
- addDs [leadsToD2], simpset()));
-qed "leadsTo_refl_iff";
-
-Goal "F \\<in> 0 leadsTo B <-> (F \\<in> program & st_set(B))";
-by (auto_tac (claset() addIs [subset_imp_leadsTo]
- addDs [leadsToD2], simpset()));
-qed "empty_leadsTo";
-AddIffs [empty_leadsTo];
-
-Goal "F \\<in> A leadsTo state <-> (F \\<in> 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 \\<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \\<in> A leadsTo B'";
-by (blast_tac (claset() addDs [leadsToD2]
- addIs [subset_imp_leadsTo,leadsTo_Trans]) 1);
-qed "leadsTo_weaken_R";
-
-Goal "[| F \\<in> A leadsTo A'; B<=A |] ==> F \\<in> B leadsTo A'";
-by (ftac leadsToD2 1);
-by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1);
-qed_spec_mp "leadsTo_weaken_L";
-
-Goal "[| F \\<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \\<in> B leadsTo B'";
-by (ftac 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 \\<in> transient(A); state-A<=B; st_set(B)|] ==> F \\<in> A leadsTo B";
-by (ftac 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 \\<in> A leadsTo C & F \\<in> B leadsTo C)";
-by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
-qed "leadsTo_Un_distrib";
-
-Goal
-"(F:(\\<Union>i \\<in> I. A(i)) leadsTo B)<-> ((\\<forall>i \\<in> I. F \\<in> A(i) leadsTo B) & F \\<in> program & st_set(B))";
-by (blast_tac (claset() addDs [leadsToD2]
- addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
-qed "leadsTo_UN_distrib";
-
-Goal "(F \\<in> Union(S) leadsTo B) <-> (\\<forall>A \\<in> S. F \\<in> A leadsTo B) & F \\<in> program & st_set(B)";
-by (blast_tac (claset() addDs [leadsToD2]
- addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
-qed "leadsTo_Union_distrib";
-
-(*Set difference \\<in> maybe combine with leadsTo_weaken_L?*)
-Goal "[| F: (A-B) leadsTo C; F \\<in> B leadsTo C; st_set(C) |] ==> F \\<in> A leadsTo C";
-by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]
- addDs [leadsToD2]) 1);
-qed "leadsTo_Diff";
-
-val [major,minor] = Goal
-"[|(!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); F \\<in> program |] \
-\ ==> F: (\\<Union>i \\<in> I. A(i)) leadsTo (\\<Union>i \\<in> 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 \\<in> A leadsTo A'; F \\<in> B leadsTo B' |] ==> F \\<in> (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 \\<in> A leadsTo (A' Un B); F \\<in> B leadsTo B'|] ==> F \\<in> A leadsTo (A' Un B')";
-by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F \\<in> 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 \\<in> A leadsTo (A' Un B); F \\<in> (B-A') leadsTo B'|]==> F \\<in> 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 "[| F \\<in> A leadsTo (B Un A'); F \\<in> B leadsTo B' |] ==> F \\<in> 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 \\<in> A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F \\<in> 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, basis_prem, trans_prem, union_prem] = Goalw [leadsTo_def, st_set_def]
- "[| F \\<in> za leadsTo zb; \
-\ !!A B. [| F \\<in> A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \
-\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \
-\ F \\<in> B leadsTo C; P(B, C) |] \
-\ ==> P(A, C); \
-\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> 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 (rtac union_prem 3);
-by (rtac trans_prem 2);
-by (rtac basis_prem 1);
-by Auto_tac;
-qed "leadsTo_induct";
-
-(* Added by Sidi, an induction rule without ensures *)
-val [major,imp_prem,basis_prem,trans_prem,union_prem] = Goal
- "[| F \\<in> za leadsTo zb; \
-\ !!A B. [| A<=B; st_set(B) |] ==> P(A, B); \
-\ !!A B. [| F \\<in> A co A Un B; F \\<in> transient(A); st_set(B) |] ==> P(A, B); \
-\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \
-\ F \\<in> B leadsTo C; P(B, C) |] \
-\ ==> P(A, C); \
-\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> 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_prem,union_prem], simpset()));
-by (rewrite_goal_tac [ensures_def] 1);
-by (Clarify_tac 1);
-by (ftac constrainsD2 1);
-by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1);
-by (Blast_tac 1);
-by (forward_tac [ensuresI2 RS leadsTo_Basis] 1);
-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 \\<in> on the preconditions for B **)
-(*Lemma is the weak version \\<in> can't see how to do it in one step*)
-val major::prems = Goal
- "[| F \\<in> za leadsTo zb; \
-\ P(zb); \
-\ !!A B. [| F \\<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \
-\ !!S. [| \\<forall>A \\<in> S. P(A); \\<forall>A \\<in> S. st_set(A) |] ==> P(Union(S)) \
-\ |] ==> P(za)";
-(*by induction on this formula*)
-by (subgoal_tac "P(zb) --> P(za)" 1);
-(*now solve first subgoal \\<in> this formula is sufficient*)
-by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
-by (rtac (major RS leadsTo_induct) 1);
-by (REPEAT (blast_tac (claset() addIs prems) 1));
-qed "leadsTo_induct_pre_aux";
-
-
-val [major, zb_prem, basis_prem, union_prem] = Goal
- "[| F \\<in> za leadsTo zb; \
-\ P(zb); \
-\ !!A B. [| F \\<in> A ensures B; F \\<in> B leadsTo zb; P(B); st_set(A) |] ==> P(A); \
-\ !!S. \\<forall>A \\<in> S. F \\<in> A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \
-\ |] ==> P(za)";
-by (cut_facts_tac [major] 1);
-by (subgoal_tac "(F \\<in> za leadsTo zb) & P(za)" 1);
-by (etac conjunct2 1);
-by (rtac (major RS leadsTo_induct_pre_aux) 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";
-
-(** The impossibility law **)
-Goal
- "F \\<in> A leadsTo 0 ==> A=0";
-by (etac leadsTo_induct_pre 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 \\<in> Progress-Safety-Progress **)
-
-(*Special case of PSP \\<in> Misra's "stable conjunction"*)
-Goalw [stable_def]
- "[| F \\<in> A leadsTo A'; F \\<in> stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)";
-by (etac leadsTo_induct 1);
-by (rtac 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()
- addsimps [ensures_def, Diff_Int_distrib RS sym,
- Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
-by (REPEAT(blast_tac (claset()
- addIs [transient_strengthen,constrains_Int]
- addDs [constrainsD2]) 1));
-qed "psp_stable";
-
-
-Goal "[|F \\<in> A leadsTo A'; F \\<in> 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, st_set_def]
-"[| F \\<in> A ensures A'; F \\<in> 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 \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))";
-by (subgoal_tac "F \\<in> 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"*)
-by (rtac leadsTo_Un_duplicate2 2);
-by (etac leadsTo_cancel_Diff1 2);
-by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
-by (blast_tac (claset() addIs [leadsTo_weaken_L]
- addDs [constrains_imp_subset]) 2);
-(*Basis case*)
-by (blast_tac (claset() addIs [psp_ensures, leadsTo_Basis]) 1);
-qed "psp";
-
-
-Goal "[| F \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B') |] \
-\ ==> F \\<in> (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 \\<in> A leadsTo A'; F \\<in> B unless B'; st_set(B); st_set(B') |] \
-\ ==> F \\<in> (A Int B) leadsTo ((A' Int B) Un B')";
-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 1);
-by (REPEAT(blast_tac (claset() addIs [leadsTo_weaken]) 1));
-qed "psp_unless";
-
-(*** Proving the wf induction rules ***)
-(** The most general rule \\<in> r is any wf relation; f is any variant function **)
-Goal "[| wf(r); \
-\ m \\<in> I; \
-\ field(r)<=I; \
-\ F \\<in> program; st_set(B);\
-\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(converse(r)``{m})) Un B) |] \
-\ ==> F \\<in> (A Int f-``{m}) leadsTo B";
-by (eres_inst_tac [("a","m")] wf_induct2 1);
-by (ALLGOALS(Asm_simp_tac));
-by (subgoal_tac "F \\<in> (A Int (f-``(converse(r)``{x}))) leadsTo B" 1);
-by (stac vimage_eq_UN 2);
-by (asm_simp_tac (simpset() delsimps UN_simps
- addsimps [Int_UN_distrib]) 2);
-by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
-by (auto_tac (claset() addIs [leadsTo_UN],
- simpset() delsimps UN_simps addsimps [Int_UN_distrib]));
-qed "leadsTo_wf_induct_aux";
-
-(** Meta or object quantifier ? **)
-Goal "[| wf(r); \
-\ field(r)<=I; \
-\ A<=f-``I;\
-\ F \\<in> program; st_set(A); st_set(B); \
-\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \
-\ ((A Int f-``(converse(r)``{m})) Un B) |] \
-\ ==> F \\<in> A leadsTo B";
-by (res_inst_tac [("b", "A")] subst 1);
-by (res_inst_tac [("I", "I")] leadsTo_UN 2);
-by (REPEAT (assume_tac 2));
-by (Clarify_tac 2);
-by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2);
-by (REPEAT (assume_tac 2));
-by (rtac equalityI 1);
-by Safe_tac;
-by (thin_tac "field(r)<=I" 1);
-by (dres_inst_tac [("c", "x")] subsetD 1);
-by Safe_tac;
-by (res_inst_tac [("b", "x")] UN_I 1);
-by Auto_tac;
-qed "leadsTo_wf_induct";
-
-Goalw [field_def] "field(measure(nat, %x. x)) = nat";
-by (asm_full_simp_tac (simpset() addsimps [measure_def]) 1) ;
-by (rtac equalityI 1);
-by (force_tac (claset(), simpset()) 1);
-by (Clarify_tac 1);
-by (thin_tac "x\\<notin>range(?y)" 1);
-by (etac nat_induct 1);
-by (res_inst_tac [("b", "succ(succ(xa))")] domainI 2);
-by (res_inst_tac [("b","succ(0)")] domainI 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "nat_measure_field";
-
-
-Goal "k<A ==> measure(A, %x. x) -`` {k} = k";
-by (rtac equalityI 1);
-by (auto_tac (claset(), simpset() addsimps [measure_def]));
-by (blast_tac (claset() addIs [ltD]) 1);
-by (rtac vimageI 1);
-by (Blast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1);
-by (blast_tac (claset() addIs [lt_trans]) 1);
-qed "Image_inverse_lessThan";
-
-(*Alternative proof is via the lemma F \\<in> (A Int f-`(lessThan m)) leadsTo B*)
-Goal
- "[| A<=f-``nat;\
-\ F \\<in> program; st_set(A); st_set(B); \
-\ \\<forall>m \\<in> nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \
-\ ==> F \\<in> A leadsTo B";
-by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
- (wf_measure RS leadsTo_wf_induct) 1);
-by (Clarify_tac 6);
-by (ALLGOALS(asm_full_simp_tac
- (simpset() addsimps [nat_measure_field])));
-by (asm_simp_tac (simpset() addsimps [ltI, Image_inverse_lessThan, symmetric vimage_def]) 1);
-qed "lessThan_induct";
-
-
-(*** wlt ****)
-
-(*Misra's property W3*)
-Goalw [wlt_def] "wlt(F,B) <=state";
-by Auto_tac;
-qed "wlt_type";
-
-Goalw [st_set_def] "st_set(wlt(F, B))";
-by (rtac wlt_type 1);
-qed "wlt_st_set";
-AddIffs [wlt_st_set];
-
-Goalw [wlt_def] "F \\<in> wlt(F, B) leadsTo B <-> (F \\<in> program & st_set(B))";
-by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1);
-qed "wlt_leadsTo_iff";
-
-(* [| F \\<in> program; st_set(B) |] ==> F \\<in> wlt(F, B) leadsTo B *)
-bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2));
-
-Goalw [wlt_def] "F \\<in> A leadsTo B ==> A <= wlt(F, B)";
-by (ftac leadsToD2 1);
-by (auto_tac (claset(), simpset() addsimps [st_set_def]));
-qed "leadsTo_subset";
-
-(*Misra's property W2*)
-Goal "F \\<in> A leadsTo B <-> (A <= wlt(F,B) & F \\<in> 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 \\<in> 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, st_set_def]
- "[| B <= A2; \
-\ F \\<in> (A1 - B) co (A1 Un B); \
-\ F \\<in> (A2 - C) co (A2 Un C) |] \
-\ ==> F \\<in> (A1 Un A2 - C) co (A1 Un A2 Un C)";
-by (Blast_tac 1);
-qed "leadsTo_123_aux";
-
-(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-(* slightly different from the HOL one \\<in> B here is bounded *)
-Goal "F \\<in> A leadsTo A' \
-\ ==> \\<exists>B \\<in> Pow(state). A<=B & F \\<in> B leadsTo A' & F \\<in> (B-A') co (B Un A')";
-by (ftac leadsToD2 1);
-by (etac leadsTo_induct 1);
-(*Basis*)
-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);
-by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1,
- leadsTo_Un_duplicate]) 1);
-by (Blast_tac 1);
-(*Union*)
-by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1);
-by (subgoal_tac "\\<exists>y. y \\<in> Pi(S, %A. {Ba \\<in> Pow(state). A<=Ba & \
- \ F \\<in> Ba leadsTo B & F \\<in> Ba - B co Ba Un B})" 1);
-by (rtac AC_ball_Pi 2);
-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", "\\<Union>A \\<in> 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 (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 \\<in> program; st_set(B) |] ==>F \\<in> (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 (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);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset()
- addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1);
-qed "wlt_constrains_wlt";
-
-(*** Completion \\<in> Binary and General Finite versions ***)
-
-Goal "[| W = wlt(F, (B' Un C)); \
-\ F \\<in> A leadsTo (A' Un C); F \\<in> A' co (A' Un C); \
-\ F \\<in> B leadsTo (B' Un C); F \\<in> B' co (B' Un C) |] \
-\ ==> F \\<in> (A Int B) leadsTo ((A' Int B') Un C)";
-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 \\<in> program" 1);
-by (Asm_simp_tac 2);
-by (blast_tac (claset() addSDs [leadsToD2]) 2);
-by (subgoal_tac "F \\<in> (W-C) co (W Un B' Un C)" 1);
-by (blast_tac (claset() addSIs [[asm_rl, wlt_constrains_wlt]
- MRS constrains_Un RS constrains_weaken]) 2);
-by (subgoal_tac "F \\<in> (W-C) co W" 1);
-by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS
- (subset_Un_iff2 RS iffD1), Un_assoc]) 2);
-by (subgoal_tac "F \\<in> (A Int W - C) leadsTo (A' Int W Un C)" 1);
-by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
-(** LEVEL 9 **)
-by (subgoal_tac "F \\<in> (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
-by (rtac leadsTo_Un_duplicate2 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 [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);
-by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
-qed "completion_aux";
-bind_thm("completion", refl RS completion_aux);
-
-Goal "[| I \\<in> Fin(X); F \\<in> program; st_set(C) |] ==> \
-\(\\<forall>i \\<in> I. F \\<in> (A(i)) leadsTo (A'(i) Un C)) --> \
-\ (\\<forall>i \\<in> I. F \\<in> (A'(i)) co (A'(i) Un C)) --> \
-\ F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
-by (etac Fin_induct 1);
-by (auto_tac (claset(), simpset() addsimps [Inter_0]));
-by (rtac completion 1);
-by (auto_tac (claset(),
- simpset() delsimps INT_simps addsimps INT_extend_simps));
-by (rtac constrains_INT 1);
-by (REPEAT(Blast_tac 1));
-qed "lemma";
-
-val prems = Goal
- "[| I \\<in> Fin(X); \
-\ !!i. i \\<in> I ==> F \\<in> A(i) leadsTo (A'(i) Un C); \
-\ !!i. i \\<in> I ==> F \\<in> A'(i) co (A'(i) Un C); F \\<in> program; st_set(C)|] \
-\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
-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]
- "[| F \\<in> A leadsTo A'; F \\<in> stable(A'); \
-\ F \\<in> B leadsTo B'; F \\<in> stable(B') |] \
-\ ==> F \\<in> (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 [leadsToD2, constrainsD2]) 5));
-by (ALLGOALS(Asm_full_simp_tac));
-qed "stable_completion";
-
-
-val major::prems = Goalw [stable_def]
- "[| I \\<in> Fin(X); \
-\ (!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); \
-\ (!!i. i \\<in> I ==> F \\<in> stable(A'(i))); F \\<in> program |] \
-\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo (\\<Inter>i \\<in> I. A'(i))";
-by (cut_facts_tac [major] 1);
-by (subgoal_tac "st_set(\\<Inter>i \\<in> 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 (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 Sat Mar 26 18:20:29 2005 +0100
+++ b/src/ZF/UNITY/WFair.thy Mon Mar 28 16:19:56 2005 +0200
@@ -2,15 +2,18 @@
ID: $Id$
Author: Sidi Ehmety, Computer Laboratory
Copyright 1998 University of Cambridge
-
-Weak Fairness versions of transient, ensures, leadsTo.
-
-From Misra, "A Logic for Concurrent Programming", 1994
-
-Theory ported from HOL.
*)
-WFair = UNITY + Main_ZFC +
+header{*Progress under Weak Fairness*}
+
+theory WFair
+imports UNITY Main_ZFC
+begin
+
+text{*This theory defines the operators transient, ensures and leadsTo,
+assuming weak fairness. From Misra, "A Logic for Concurrent Programming",
+1994.*}
+
constdefs
(* This definition specifies weak fairness. The rest of the theory
@@ -19,7 +22,7 @@
"transient(A) =={F:program. (EX act: Acts(F). A<=domain(act) &
act``A <= state-A) & st_set(A)}"
- ensures :: "[i,i] => i" (infixl 60)
+ ensures :: "[i,i] => i" (infixl "ensures" 60)
"A ensures B == ((A-B) co (A Un B)) Int transient(A-B)"
consts
@@ -30,19 +33,19 @@
inductive
domains
"leads(D, F)" <= "Pow(D)*Pow(D)"
- intrs
- 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)) |] ==>
+ intros
+ 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 "[Union_Pow_iff RS iffD2, UnionI, PowI]"
+ type_intros Union_Pow_iff [THEN iffD2] UnionI PowI
constdefs
(* The Visible version of the LEADS-TO relation*)
- leadsTo :: "[i, i] => i" (infixl 60)
+ leadsTo :: "[i, i] => i" (infixl "leadsTo" 60)
"A leadsTo B == {F:program. <A,B>:leads(state, F)}"
(* wlt(F, B) is the largest set that leads to B*)
@@ -50,6 +53,748 @@
"wlt(F, B) == Union({A:Pow(state). F: A leadsTo B})"
syntax (xsymbols)
- "op leadsTo" :: "[i, i] => i" (infixl "\\<longmapsto>" 60)
+ "leadsTo" :: "[i, i] => i" (infixl "\<longmapsto>" 60)
+
+(** Ad-hoc set-theory rules **)
+
+lemma Int_Union_Union: "Union(B) Int A = (\<Union>b \<in> B. b Int A)"
+by auto
+
+lemma Int_Union_Union2: "A Int Union(B) = (\<Union>b \<in> B. A Int b)"
+by auto
+
+(*** transient ***)
+
+lemma transient_type: "transient(A)<=program"
+by (unfold transient_def, auto)
+
+lemma transientD2:
+"F \<in> transient(A) ==> F \<in> program & st_set(A)"
+apply (unfold transient_def, auto)
+done
+
+lemma stable_transient_empty: "[| F \<in> stable(A); F \<in> transient(A) |] ==> A = 0"
+by (simp add: stable_def constrains_def transient_def, fast)
+
+lemma transient_strengthen: "[|F \<in> transient(A); B<=A|] ==> F \<in> transient(B)"
+apply (simp add: transient_def st_set_def, clarify)
+apply (blast intro!: rev_bexI)
+done
+
+lemma transientI:
+"[|act \<in> Acts(F); A <= domain(act); act``A <= state-A;
+ F \<in> program; st_set(A)|] ==> F \<in> transient(A)"
+by (simp add: transient_def, blast)
+
+lemma transientE:
+ "[| F \<in> transient(A);
+ !!act. [| act \<in> Acts(F); A <= domain(act); act``A <= state-A|]==>P|]
+ ==>P"
+by (simp add: transient_def, blast)
+
+lemma transient_state: "transient(state) = 0"
+apply (simp add: transient_def)
+apply (rule equalityI, auto)
+apply (cut_tac F = x in Acts_type)
+apply (simp add: Diff_cancel)
+apply (auto intro: st0_in_state)
+done
+
+lemma transient_state2: "state<=B ==> transient(B) = 0"
+apply (simp add: transient_def st_set_def)
+apply (rule equalityI, auto)
+apply (cut_tac F = x in Acts_type)
+apply (subgoal_tac "B=state")
+apply (auto intro: st0_in_state)
+done
+
+lemma transient_empty: "transient(0) = program"
+by (auto simp add: transient_def)
+
+declare transient_empty [simp] transient_state [simp] transient_state2 [simp]
+
+(*** ensures ***)
+
+lemma ensures_type: "A ensures B <=program"
+by (simp add: ensures_def constrains_def, auto)
+
+lemma ensuresI:
+"[|F:(A-B) co (A Un B); F \<in> transient(A-B)|]==>F \<in> A ensures B"
+apply (unfold ensures_def)
+apply (auto simp add: transient_type [THEN subsetD])
+done
+
+(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)
+lemma ensuresI2: "[| F \<in> A co A Un B; F \<in> transient(A) |] ==> F \<in> A ensures B"
+apply (drule_tac B = "A-B" in constrains_weaken_L)
+apply (drule_tac [2] B = "A-B" in transient_strengthen)
+apply (auto simp add: ensures_def transient_type [THEN subsetD])
+done
+
+lemma ensuresD: "F \<in> A ensures B ==> F:(A-B) co (A Un B) & F \<in> transient (A-B)"
+by (unfold ensures_def, auto)
+
+lemma ensures_weaken_R: "[|F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'"
+apply (unfold ensures_def)
+apply (blast intro: transient_strengthen constrains_weaken)
+done
+
+(*The L-version (precondition strengthening) fails, but we have this*)
+lemma stable_ensures_Int:
+ "[| F \<in> stable(C); F \<in> A ensures B |] ==> F:(C Int A) ensures (C Int B)"
+
+apply (unfold ensures_def)
+apply (simp (no_asm) add: Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
+apply (blast intro: transient_strengthen stable_constrains_Int constrains_weaken)
+done
+
+lemma stable_transient_ensures: "[|F \<in> stable(A); F \<in> transient(C); A<=B Un C|] ==> F \<in> A ensures B"
+apply (frule stable_type [THEN subsetD])
+apply (simp add: ensures_def stable_def)
+apply (blast intro: transient_strengthen constrains_weaken)
+done
+
+lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
+by (auto simp add: ensures_def unless_def)
+
+lemma subset_imp_ensures: "[| F \<in> program; A<=B |] ==> F \<in> A ensures B"
+by (auto simp add: ensures_def constrains_def transient_def st_set_def)
+
+(*** leadsTo ***)
+lemmas leads_left = leads.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas leads_right = leads.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemma leadsTo_type: "A leadsTo B <= program"
+by (unfold leadsTo_def, auto)
+
+lemma leadsToD2:
+"F \<in> A leadsTo B ==> F \<in> program & st_set(A) & st_set(B)"
+apply (unfold leadsTo_def st_set_def)
+apply (blast dest: leads_left leads_right)
+done
+
+lemma leadsTo_Basis:
+ "[|F \<in> A ensures B; st_set(A); st_set(B)|] ==> F \<in> A leadsTo B"
+apply (unfold leadsTo_def st_set_def)
+apply (cut_tac ensures_type)
+apply (auto intro: leads.Basis)
+done
+declare leadsTo_Basis [intro]
+
+(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
+(* [| F \<in> program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *)
+lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
+
+lemma leadsTo_Trans: "[|F \<in> A leadsTo B; F \<in> B leadsTo C |]==>F \<in> A leadsTo C"
+apply (unfold leadsTo_def)
+apply (auto intro: leads.Trans)
+done
+
+(* Better when used in association with leadsTo_weaken_R *)
+lemma transient_imp_leadsTo: "F \<in> transient(A) ==> F \<in> A leadsTo (state-A)"
+apply (unfold transient_def)
+apply (blast intro: ensuresI [THEN leadsTo_Basis] constrains_weaken transientI)
+done
+
+(*Useful with cancellation, disjunction*)
+lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' Un A') ==> F \<in> A leadsTo A'"
+by simp
+
+lemma leadsTo_Un_duplicate2:
+ "F \<in> A leadsTo (A' Un C Un C) ==> F \<in> A leadsTo (A' Un C)"
+by (simp add: Un_ac)
+
+(*The Union introduction rule as we should have liked to state it*)
+lemma leadsTo_Union:
+ "[|!!A. A \<in> S ==> F \<in> A leadsTo B; F \<in> program; st_set(B)|]
+ ==> F \<in> Union(S) leadsTo B"
+apply (unfold leadsTo_def st_set_def)
+apply (blast intro: leads.Union dest: leads_left)
+done
+
+lemma leadsTo_Union_Int:
+ "[|!!A. A \<in> S ==>F : (A Int C) leadsTo B; F \<in> program; st_set(B)|]
+ ==> F : (Union(S)Int C)leadsTo B"
+apply (unfold leadsTo_def st_set_def)
+apply (simp only: Int_Union_Union)
+apply (blast dest: leads_left intro: leads.Union)
+done
+
+lemma leadsTo_UN:
+ "[| !!i. i \<in> I ==> F \<in> A(i) leadsTo B; F \<in> program; st_set(B)|]
+ ==> F:(\<Union>i \<in> I. A(i)) leadsTo B"
+apply (simp add: Int_Union_Union leadsTo_def st_set_def)
+apply (blast dest: leads_left intro: leads.Union)
+done
+
+(* Binary union introduction rule *)
+lemma leadsTo_Un:
+ "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A Un B) leadsTo C"
+apply (subst Un_eq_Union)
+apply (blast intro: leadsTo_Union dest: leadsToD2)
+done
+
+lemma single_leadsTo_I:
+ "[|!!x. x \<in> A==> F:{x} leadsTo B; F \<in> program; st_set(B) |]
+ ==> F \<in> A leadsTo B"
+apply (rule_tac b = A in UN_singleton [THEN subst])
+apply (rule leadsTo_UN, auto)
+done
+
+lemma leadsTo_refl: "[| F \<in> program; st_set(A) |] ==> F \<in> A leadsTo A"
+by (blast intro: subset_imp_leadsTo)
+
+lemma leadsTo_refl_iff: "F \<in> A leadsTo A <-> F \<in> program & st_set(A)"
+by (auto intro: leadsTo_refl dest: leadsToD2)
+
+lemma empty_leadsTo: "F \<in> 0 leadsTo B <-> (F \<in> program & st_set(B))"
+by (auto intro: subset_imp_leadsTo dest: leadsToD2)
+declare empty_leadsTo [iff]
+
+lemma leadsTo_state: "F \<in> A leadsTo state <-> (F \<in> program & st_set(A))"
+by (auto intro: subset_imp_leadsTo dest: leadsToD2 st_setD)
+declare leadsTo_state [iff]
+
+lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \<in> A leadsTo B'"
+by (blast dest: leadsToD2 intro: subset_imp_leadsTo leadsTo_Trans)
+
+lemma leadsTo_weaken_L: "[| F \<in> A leadsTo A'; B<=A |] ==> F \<in> B leadsTo A'"
+apply (frule leadsToD2)
+apply (blast intro: leadsTo_Trans subset_imp_leadsTo st_set_subset)
+done
+
+lemma leadsTo_weaken: "[| F \<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \<in> B leadsTo B'"
+apply (frule leadsToD2)
+apply (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans leadsTo_refl)
+done
+
+(* This rule has a nicer conclusion *)
+lemma transient_imp_leadsTo2: "[| F \<in> transient(A); state-A<=B; st_set(B)|] ==> F \<in> A leadsTo B"
+apply (frule transientD2)
+apply (rule leadsTo_weaken_R)
+apply (auto simp add: transient_imp_leadsTo)
+done
+
+(*Distributes over binary unions*)
+lemma leadsTo_Un_distrib: "F:(A Un B) leadsTo C <-> (F \<in> A leadsTo C & F \<in> B leadsTo C)"
+by (blast intro: leadsTo_Un leadsTo_weaken_L)
+
+lemma leadsTo_UN_distrib:
+"(F:(\<Union>i \<in> I. A(i)) leadsTo B)<-> ((\<forall>i \<in> I. F \<in> A(i) leadsTo B) & F \<in> program & st_set(B))"
+apply (blast dest: leadsToD2 intro: leadsTo_UN leadsTo_weaken_L)
+done
+
+lemma leadsTo_Union_distrib: "(F \<in> Union(S) leadsTo B) <-> (\<forall>A \<in> S. F \<in> A leadsTo B) & F \<in> program & st_set(B)"
+by (blast dest: leadsToD2 intro: leadsTo_Union leadsTo_weaken_L)
+
+text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
+lemma leadsTo_Diff:
+ "[| F: (A-B) leadsTo C; F \<in> B leadsTo C; st_set(C) |]
+ ==> F \<in> A leadsTo C"
+by (blast intro: leadsTo_Un leadsTo_weaken dest: leadsToD2)
+
+lemma leadsTo_UN_UN:
+ "[|!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i); F \<in> program |]
+ ==> F: (\<Union>i \<in> I. A(i)) leadsTo (\<Union>i \<in> I. A'(i))"
+apply (rule leadsTo_Union)
+apply (auto intro: leadsTo_weaken_R dest: leadsToD2)
+done
+
+(*Binary union version*)
+lemma leadsTo_Un_Un: "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |] ==> F \<in> (A Un B) leadsTo (A' Un B')"
+apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') ")
+prefer 2 apply (blast dest: leadsToD2)
+apply (blast intro: leadsTo_Un leadsTo_weaken_R)
+done
+
+(** The cancellation law **)
+lemma leadsTo_cancel2: "[|F \<in> A leadsTo (A' Un B); F \<in> B leadsTo B'|] ==> F \<in> A leadsTo (A' Un B')"
+apply (subgoal_tac "st_set (A) & st_set (A') & st_set (B) & st_set (B') &F \<in> program")
+prefer 2 apply (blast dest: leadsToD2)
+apply (blast intro: leadsTo_Trans leadsTo_Un_Un leadsTo_refl)
+done
+
+lemma leadsTo_cancel_Diff2: "[|F \<in> A leadsTo (A' Un B); F \<in> (B-A') leadsTo B'|]==> F \<in> A leadsTo (A' Un B')"
+apply (rule leadsTo_cancel2)
+prefer 2 apply assumption
+apply (blast dest: leadsToD2 intro: leadsTo_weaken_R)
+done
+
+
+lemma leadsTo_cancel1: "[| F \<in> A leadsTo (B Un A'); F \<in> B leadsTo B' |] ==> F \<in> A leadsTo (B' Un A')"
+apply (simp add: Un_commute)
+apply (blast intro!: leadsTo_cancel2)
+done
+
+lemma leadsTo_cancel_Diff1:
+ "[|F \<in> A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F \<in> A leadsTo (B' Un A')"
+apply (rule leadsTo_cancel1)
+prefer 2 apply assumption
+apply (blast intro: leadsTo_weaken_R dest: leadsToD2)
+done
+
+(*The INDUCTION rule as we should have liked to state it*)
+lemma leadsTo_induct:
+ assumes major: "F \<in> za leadsTo zb"
+ and basis: "!!A B. [|F \<in> A ensures B; st_set(A); st_set(B)|] ==> P(A,B)"
+ and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
+ F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
+ and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
+ st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(Union(S), B)"
+ shows "P(za, zb)"
+apply (cut_tac major)
+apply (unfold leadsTo_def, clarify)
+apply (erule leads.induct)
+ apply (blast intro: basis [unfolded st_set_def])
+ apply (blast intro: trans [unfolded leadsTo_def])
+apply (force intro: union [unfolded st_set_def leadsTo_def])
+done
+
+
+(* Added by Sidi, an induction rule without ensures *)
+lemma leadsTo_induct2:
+ assumes major: "F \<in> za leadsTo zb"
+ and basis1: "!!A B. [| A<=B; st_set(B) |] ==> P(A, B)"
+ and basis2: "!!A B. [| F \<in> A co A Un B; F \<in> transient(A); st_set(B) |]
+ ==> P(A, B)"
+ and trans: "!!A B C. [| F \<in> A leadsTo B; P(A, B);
+ F \<in> B leadsTo C; P(B, C) |] ==> P(A,C)"
+ and union: "!!B S. [| \<forall>A \<in> S. F \<in> A leadsTo B; \<forall>A \<in> S. P(A,B);
+ st_set(B); \<forall>A \<in> S. st_set(A)|] ==> P(Union(S), B)"
+ shows "P(za, zb)"
+apply (cut_tac major)
+apply (erule leadsTo_induct)
+apply (auto intro: trans union)
+apply (simp add: ensures_def, clarify)
+apply (frule constrainsD2)
+apply (drule_tac B' = " (A-B) Un B" in constrains_weaken_R)
+apply blast
+apply (frule ensuresI2 [THEN leadsTo_Basis])
+apply (drule_tac [4] basis2, simp_all)
+apply (frule_tac A1 = A and B = B in Int_lower2 [THEN basis1])
+apply (subgoal_tac "A=Union ({A - B, A Int B}) ")
+prefer 2 apply blast
+apply (erule ssubst)
+apply (rule union)
+apply (auto intro: subset_imp_leadsTo)
+done
+
+
+(** Variant induction rule: on the preconditions for B **)
+(*Lemma is the weak version: can't see how to do it in one step*)
+lemma leadsTo_induct_pre_aux:
+ "[| F \<in> za leadsTo zb;
+ P(zb);
+ !!A B. [| F \<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A);
+ !!S. [| \<forall>A \<in> S. P(A); \<forall>A \<in> S. st_set(A) |] ==> P(Union(S))
+ |] ==> P(za)"
+txt{*by induction on this formula*}
+apply (subgoal_tac "P (zb) --> P (za) ")
+txt{*now solve first subgoal: this formula is sufficient*}
+apply (blast intro: leadsTo_refl)
+apply (erule leadsTo_induct)
+apply (blast+)
+done
+
+
+lemma leadsTo_induct_pre:
+ "[| F \<in> za leadsTo zb;
+ P(zb);
+ !!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P(B); st_set(A) |] ==> P(A);
+ !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P(A) & st_set(A) ==> P(Union(S))
+ |] ==> P(za)"
+apply (subgoal_tac " (F \<in> za leadsTo zb) & P (za) ")
+apply (erule conjunct2)
+apply (frule leadsToD2)
+apply (erule leadsTo_induct_pre_aux)
+prefer 3 apply (blast dest: leadsToD2 intro: leadsTo_Union)
+prefer 2 apply (blast intro: leadsTo_Trans leadsTo_Basis)
+apply (blast intro: leadsTo_refl)
+done
+
+(** The impossibility law **)
+lemma leadsTo_empty:
+ "F \<in> A leadsTo 0 ==> A=0"
+apply (erule leadsTo_induct_pre)
+apply (auto simp add: ensures_def constrains_def transient_def st_set_def)
+apply (drule bspec, assumption)+
+apply blast
+done
+declare leadsTo_empty [simp]
+
+subsection{*PSP: Progress-Safety-Progress*}
+
+text{*Special case of PSP: Misra's "stable conjunction"*}
+
+lemma psp_stable:
+ "[| F \<in> A leadsTo A'; F \<in> stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"
+apply (unfold stable_def)
+apply (frule leadsToD2)
+apply (erule leadsTo_induct)
+prefer 3 apply (blast intro: leadsTo_Union_Int)
+prefer 2 apply (blast intro: leadsTo_Trans)
+apply (rule leadsTo_Basis)
+apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
+apply (auto intro: transient_strengthen constrains_Int)
+done
+
+
+lemma psp_stable2: "[|F \<in> A leadsTo A'; F \<in> stable(B) |]==>F: (B Int A) leadsTo (B Int A')"
+apply (simp (no_asm_simp) add: psp_stable Int_ac)
+done
+
+lemma psp_ensures:
+"[| F \<in> A ensures A'; F \<in> B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"
+apply (unfold ensures_def constrains_def st_set_def)
+(*speeds up the proof*)
+apply clarify
+apply (blast intro: transient_strengthen)
+done
+
+lemma psp:
+"[|F \<in> A leadsTo A'; F \<in> B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"
+apply (subgoal_tac "F \<in> program & st_set (A) & st_set (A') & st_set (B) ")
+prefer 2 apply (blast dest!: constrainsD2 leadsToD2)
+apply (erule leadsTo_induct)
+prefer 3 apply (blast intro: leadsTo_Union_Int)
+ txt{*Basis case*}
+ apply (blast intro: psp_ensures leadsTo_Basis)
+txt{*Transitivity case has a delicate argument involving "cancellation"*}
+apply (rule leadsTo_Un_duplicate2)
+apply (erule leadsTo_cancel_Diff1)
+apply (simp add: Int_Diff Diff_triv)
+apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
+done
+
+
+lemma psp2: "[| F \<in> A leadsTo A'; F \<in> B co B'; st_set(B') |]
+ ==> F \<in> (B' Int A) leadsTo ((B Int A') Un (B' - B))"
+by (simp (no_asm_simp) add: psp Int_ac)
+
+lemma psp_unless:
+ "[| F \<in> A leadsTo A'; F \<in> B unless B'; st_set(B); st_set(B') |]
+ ==> F \<in> (A Int B) leadsTo ((A' Int B) Un B')"
+apply (unfold unless_def)
+apply (subgoal_tac "st_set (A) &st_set (A') ")
+prefer 2 apply (blast dest: leadsToD2)
+apply (drule psp, assumption, blast)
+apply (blast intro: leadsTo_weaken)
+done
+
+
+subsection{*Proving the induction rules*}
+
+(** The most general rule \<in> r is any wf relation; f is any variant function **)
+lemma leadsTo_wf_induct_aux: "[| wf(r);
+ m \<in> I;
+ field(r)<=I;
+ F \<in> program; st_set(B);
+ \<forall>m \<in> I. F \<in> (A Int f-``{m}) leadsTo
+ ((A Int f-``(converse(r)``{m})) Un B) |]
+ ==> F \<in> (A Int f-``{m}) leadsTo B"
+apply (erule_tac a = m in wf_induct2, simp_all)
+apply (subgoal_tac "F \<in> (A Int (f-`` (converse (r) ``{x}))) leadsTo B")
+ apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
+apply (subst vimage_eq_UN)
+apply (simp del: UN_simps add: Int_UN_distrib)
+apply (auto intro: leadsTo_UN simp del: UN_simps simp add: Int_UN_distrib)
+done
+
+(** Meta or object quantifier ? **)
+lemma leadsTo_wf_induct: "[| wf(r);
+ field(r)<=I;
+ A<=f-``I;
+ F \<in> program; st_set(A); st_set(B);
+ \<forall>m \<in> I. F \<in> (A Int f-``{m}) leadsTo
+ ((A Int f-``(converse(r)``{m})) Un B) |]
+ ==> F \<in> A leadsTo B"
+apply (rule_tac b = A in subst)
+ defer 1
+ apply (rule_tac I = I in leadsTo_UN)
+ apply (erule_tac I = I in leadsTo_wf_induct_aux, assumption+, best)
+done
+
+lemma nat_measure_field: "field(measure(nat, %x. x)) = nat"
+apply (unfold field_def)
+apply (simp add: measure_def)
+apply (rule equalityI, force, clarify)
+apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)
+apply (erule nat_induct)
+apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
+apply (rule_tac b = "succ (0) " in domainI)
+apply simp_all
+done
+
+
+lemma Image_inverse_lessThan: "k<A ==> measure(A, %x. x) -`` {k} = k"
+apply (rule equalityI)
+apply (auto simp add: measure_def)
+apply (blast intro: ltD)
+apply (rule vimageI)
+prefer 2 apply blast
+apply (simp add: lt_Ord lt_Ord2 Ord_mem_iff_lt)
+apply (blast intro: lt_trans)
+done
+
+(*Alternative proof is via the lemma F \<in> (A Int f-`(lessThan m)) leadsTo B*)
+lemma lessThan_induct:
+ "[| A<=f-``nat;
+ F \<in> program; st_set(A); st_set(B);
+ \<forall>m \<in> nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |]
+ ==> F \<in> A leadsTo B"
+apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN leadsTo_wf_induct])
+apply (simp_all add: nat_measure_field)
+apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
+done
+
+
+(*** wlt ****)
+
+(*Misra's property W3*)
+lemma wlt_type: "wlt(F,B) <=state"
+by (unfold wlt_def, auto)
+
+lemma wlt_st_set: "st_set(wlt(F, B))"
+apply (unfold st_set_def)
+apply (rule wlt_type)
+done
+declare wlt_st_set [iff]
+
+lemma wlt_leadsTo_iff: "F \<in> wlt(F, B) leadsTo B <-> (F \<in> program & st_set(B))"
+apply (unfold wlt_def)
+apply (blast dest: leadsToD2 intro!: leadsTo_Union)
+done
+
+(* [| F \<in> program; st_set(B) |] ==> F \<in> wlt(F, B) leadsTo B *)
+lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2], standard]
+
+lemma leadsTo_subset: "F \<in> A leadsTo B ==> A <= wlt(F, B)"
+apply (unfold wlt_def)
+apply (frule leadsToD2)
+apply (auto simp add: st_set_def)
+done
+
+(*Misra's property W2*)
+lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B <-> (A <= wlt(F,B) & F \<in> program & st_set(B))"
+apply auto
+apply (blast dest: leadsToD2 leadsTo_subset intro: leadsTo_weaken_L wlt_leadsTo)+
+done
+
+(*Misra's property W4*)
+lemma wlt_increasing: "[| F \<in> program; st_set(B) |] ==> B <= wlt(F,B)"
+apply (rule leadsTo_subset)
+apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [THEN iff_sym] subset_imp_leadsTo)
+done
+
+(*Used in the Trans case below*)
+lemma leadsTo_123_aux:
+ "[| B <= A2;
+ F \<in> (A1 - B) co (A1 Un B);
+ F \<in> (A2 - C) co (A2 Un C) |]
+ ==> F \<in> (A1 Un A2 - C) co (A1 Un A2 Un C)"
+apply (unfold constrains_def st_set_def, blast)
+done
+
+(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+(* slightly different from the HOL one \<in> B here is bounded *)
+lemma leadsTo_123: "F \<in> A leadsTo A'
+ ==> \<exists>B \<in> Pow(state). A<=B & F \<in> B leadsTo A' & F \<in> (B-A') co (B Un A')"
+apply (frule leadsToD2)
+apply (erule leadsTo_induct)
+ txt{*Basis*}
+ apply (blast dest: ensuresD constrainsD2 st_setD)
+ txt{*Trans*}
+ apply clarify
+ apply (rule_tac x = "Ba Un Bb" in bexI)
+ apply (blast intro: leadsTo_123_aux leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate, blast)
+txt{*Union*}
+apply (clarify dest!: ball_conj_distrib [THEN iffD1])
+apply (subgoal_tac "\<exists>y. y \<in> Pi (S, %A. {Ba \<in> Pow (state) . A<=Ba & F \<in> Ba leadsTo B & F \<in> Ba - B co Ba Un B}) ")
+defer 1
+apply (rule AC_ball_Pi, safe)
+apply (rotate_tac 1)
+apply (drule_tac x = x in bspec, blast, blast)
+apply (rule_tac x = "\<Union>A \<in> S. y`A" in bexI, safe)
+apply (rule_tac [3] I1 = S in constrains_UN [THEN constrains_weaken])
+apply (rule_tac [2] leadsTo_Union)
+prefer 5 apply (blast dest!: apply_type, simp_all)
+apply (force dest!: apply_type)+
+done
+
+
+(*Misra's property W5*)
+lemma wlt_constrains_wlt: "[| F \<in> program; st_set(B) |] ==>F \<in> (wlt(F, B) - B) co (wlt(F,B))"
+apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], assumption, blast)
+apply clarify
+apply (subgoal_tac "Ba = wlt (F,B) ")
+prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
+apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]])
+done
+
+
+subsection{*Completion: Binary and General Finite versions*}
+
+lemma completion_aux: "[| W = wlt(F, (B' Un C));
+ F \<in> A leadsTo (A' Un C); F \<in> A' co (A' Un C);
+ F \<in> B leadsTo (B' Un C); F \<in> B' co (B' Un C) |]
+ ==> F \<in> (A Int B) leadsTo ((A' Int B') Un C)"
+apply (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 \<in> program")
+ prefer 2
+ apply simp
+ apply (blast dest!: leadsToD2)
+apply (subgoal_tac "F \<in> (W-C) co (W Un B' Un C) ")
+ prefer 2
+ apply (blast intro!: constrains_weaken [OF constrains_Un [OF _ wlt_constrains_wlt]])
+apply (subgoal_tac "F \<in> (W-C) co W")
+ prefer 2
+ apply (simp add: wlt_increasing [THEN subset_Un_iff2 [THEN iffD1]] Un_assoc)
+apply (subgoal_tac "F \<in> (A Int W - C) leadsTo (A' Int W Un C) ")
+ prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
+(** step 13 **)
+apply (subgoal_tac "F \<in> (A' Int W Un C) leadsTo (A' Int B' Un C) ")
+apply (drule leadsTo_Diff)
+apply (blast intro: subset_imp_leadsTo dest: leadsToD2 constrainsD2)
+apply (force simp add: st_set_def)
+apply (subgoal_tac "A Int B <= A Int W")
+prefer 2 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
+apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
+txt{*last subgoal*}
+apply (rule_tac leadsTo_Un_duplicate2)
+apply (rule_tac leadsTo_Un_Un)
+ prefer 2 apply (blast intro: leadsTo_refl)
+apply (rule_tac A'1 = "B' Un C" in wlt_leadsTo[THEN psp2, THEN leadsTo_weaken])
+apply blast+
+done
+
+lemmas completion = refl [THEN completion_aux, standard]
+
+lemma finite_completion_aux:
+ "[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==>
+ (\<forall>i \<in> I. F \<in> (A(i)) leadsTo (A'(i) Un C)) -->
+ (\<forall>i \<in> I. F \<in> (A'(i)) co (A'(i) Un C)) -->
+ F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
+apply (erule Fin_induct)
+apply (auto simp add: Inter_0)
+apply (rule completion)
+apply (auto simp del: INT_simps simp add: INT_extend_simps)
+apply (blast intro: constrains_INT)
+done
+
+lemma finite_completion:
+ "[| I \<in> Fin(X);
+ !!i. i \<in> I ==> F \<in> A(i) leadsTo (A'(i) Un C);
+ !!i. i \<in> I ==> F \<in> A'(i) co (A'(i) Un C); F \<in> program; st_set(C)|]
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
+by (blast intro: finite_completion_aux [THEN mp, THEN mp])
+
+lemma stable_completion:
+ "[| F \<in> A leadsTo A'; F \<in> stable(A');
+ F \<in> B leadsTo B'; F \<in> stable(B') |]
+ ==> F \<in> (A Int B) leadsTo (A' Int B')"
+apply (unfold stable_def)
+apply (rule_tac C1 = 0 in completion [THEN leadsTo_weaken_R], simp+)
+apply (blast dest: leadsToD2)
+done
+
+
+lemma finite_stable_completion:
+ "[| I \<in> Fin(X);
+ (!!i. i \<in> I ==> F \<in> A(i) leadsTo A'(i));
+ (!!i. i \<in> I ==> F \<in> stable(A'(i))); F \<in> program |]
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) leadsTo (\<Inter>i \<in> I. A'(i))"
+apply (unfold stable_def)
+apply (subgoal_tac "st_set (\<Inter>i \<in> I. A' (i))")
+prefer 2 apply (blast dest: leadsToD2)
+apply (rule_tac C1 = 0 in finite_completion [THEN leadsTo_weaken_R], auto)
+done
+
+ML
+{*
+val Int_Union_Union = thm "Int_Union_Union";
+val Int_Union_Union2 = thm "Int_Union_Union2";
+val transient_type = thm "transient_type";
+val transientD2 = thm "transientD2";
+val stable_transient_empty = thm "stable_transient_empty";
+val transient_strengthen = thm "transient_strengthen";
+val transientI = thm "transientI";
+val transientE = thm "transientE";
+val transient_state = thm "transient_state";
+val transient_state2 = thm "transient_state2";
+val transient_empty = thm "transient_empty";
+val ensures_type = thm "ensures_type";
+val ensuresI = thm "ensuresI";
+val ensuresI2 = thm "ensuresI2";
+val ensuresD = thm "ensuresD";
+val ensures_weaken_R = thm "ensures_weaken_R";
+val stable_ensures_Int = thm "stable_ensures_Int";
+val stable_transient_ensures = thm "stable_transient_ensures";
+val ensures_eq = thm "ensures_eq";
+val subset_imp_ensures = thm "subset_imp_ensures";
+val leads_left = thm "leads_left";
+val leads_right = thm "leads_right";
+val leadsTo_type = thm "leadsTo_type";
+val leadsToD2 = thm "leadsToD2";
+val leadsTo_Basis = thm "leadsTo_Basis";
+val subset_imp_leadsTo = thm "subset_imp_leadsTo";
+val leadsTo_Trans = thm "leadsTo_Trans";
+val transient_imp_leadsTo = thm "transient_imp_leadsTo";
+val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate";
+val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2";
+val leadsTo_Union = thm "leadsTo_Union";
+val leadsTo_Union_Int = thm "leadsTo_Union_Int";
+val leadsTo_UN = thm "leadsTo_UN";
+val leadsTo_Un = thm "leadsTo_Un";
+val single_leadsTo_I = thm "single_leadsTo_I";
+val leadsTo_refl = thm "leadsTo_refl";
+val leadsTo_refl_iff = thm "leadsTo_refl_iff";
+val empty_leadsTo = thm "empty_leadsTo";
+val leadsTo_state = thm "leadsTo_state";
+val leadsTo_weaken_R = thm "leadsTo_weaken_R";
+val leadsTo_weaken_L = thm "leadsTo_weaken_L";
+val leadsTo_weaken = thm "leadsTo_weaken";
+val transient_imp_leadsTo2 = thm "transient_imp_leadsTo2";
+val leadsTo_Un_distrib = thm "leadsTo_Un_distrib";
+val leadsTo_UN_distrib = thm "leadsTo_UN_distrib";
+val leadsTo_Union_distrib = thm "leadsTo_Union_distrib";
+val leadsTo_Diff = thm "leadsTo_Diff";
+val leadsTo_UN_UN = thm "leadsTo_UN_UN";
+val leadsTo_Un_Un = thm "leadsTo_Un_Un";
+val leadsTo_cancel2 = thm "leadsTo_cancel2";
+val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2";
+val leadsTo_cancel1 = thm "leadsTo_cancel1";
+val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1";
+val leadsTo_induct = thm "leadsTo_induct";
+val leadsTo_induct2 = thm "leadsTo_induct2";
+val leadsTo_induct_pre_aux = thm "leadsTo_induct_pre_aux";
+val leadsTo_induct_pre = thm "leadsTo_induct_pre";
+val leadsTo_empty = thm "leadsTo_empty";
+val psp_stable = thm "psp_stable";
+val psp_stable2 = thm "psp_stable2";
+val psp_ensures = thm "psp_ensures";
+val psp = thm "psp";
+val psp2 = thm "psp2";
+val psp_unless = thm "psp_unless";
+val leadsTo_wf_induct_aux = thm "leadsTo_wf_induct_aux";
+val leadsTo_wf_induct = thm "leadsTo_wf_induct";
+val nat_measure_field = thm "nat_measure_field";
+val Image_inverse_lessThan = thm "Image_inverse_lessThan";
+val lessThan_induct = thm "lessThan_induct";
+val wlt_type = thm "wlt_type";
+val wlt_st_set = thm "wlt_st_set";
+val wlt_leadsTo_iff = thm "wlt_leadsTo_iff";
+val wlt_leadsTo = thm "wlt_leadsTo";
+val leadsTo_subset = thm "leadsTo_subset";
+val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt";
+val wlt_increasing = thm "wlt_increasing";
+val leadsTo_123_aux = thm "leadsTo_123_aux";
+val leadsTo_123 = thm "leadsTo_123";
+val wlt_constrains_wlt = thm "wlt_constrains_wlt";
+val completion_aux = thm "completion_aux";
+val completion = thm "completion";
+val finite_completion_aux = thm "finite_completion_aux";
+val finite_completion = thm "finite_completion";
+val stable_completion = thm "stable_completion";
+val finite_stable_completion = thm "finite_stable_completion";
+*}
end