--- a/src/HOL/IsaMakefile Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/IsaMakefile Thu Jan 30 18:08:09 2003 +0100
@@ -382,13 +382,12 @@
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
- UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \
+ UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
UNITY/Extend.thy UNITY/FP.thy \
UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
- UNITY/SubstAx.thy UNITY/UNITY.ML \
- UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \
+ UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \
--- a/src/HOL/UNITY/Comp/Client.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Comp/Client.ML Thu Jan 30 18:08:09 2003 +0100
@@ -8,8 +8,6 @@
Addsimps [Client_def RS def_prg_Init,
Client_def RS def_prg_AllowedActs];
-program_defs_ref := [Client_def];
-
Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
Goal "(Client ok G) = \
@@ -26,7 +24,7 @@
by (auto_tac
(claset() addSIs [increasing_imp_Increasing],
simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
-by (auto_tac (claset(), simpset() addsimps [increasing_def]));
+by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def]));
by (ALLGOALS constrains_tac);
by Auto_tac;
qed "increasing_ask_rel";
@@ -46,6 +44,7 @@
by (rtac (invariantI RS stable_Join_Always2) 1);
by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
addSIs [stable_Int]) 3);
+by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2);
by (constrains_tac 2);
by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
by Auto_tac;
@@ -63,6 +62,7 @@
(*** Towards proving the liveness property ***)
Goal "Client: stable {s. rel s <= giv s}";
+by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "stable_rel_le_giv";
@@ -150,8 +150,8 @@
(*This shows that the Client won't alter other variables in any state
that it is combined with*)
Goal "Client : preserves dummy";
-by (rewtac preserves_def);
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1);
+by (Clarify_tac 1);
by (constrains_tac 1);
by Auto_tac;
qed "client_preserves_dummy";
@@ -160,6 +160,7 @@
(** Obsolete lemmas from first version of the Client **)
Goal "Client: stable {s. size (rel s) <= size (giv s)}";
+by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "stable_size_rel_le_giv";
--- a/src/HOL/UNITY/Comp/Counter.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counter.ML Thu Jan 30 18:08:09 2003 +0100
@@ -12,7 +12,6 @@
*)
Addsimps [Component_def RS def_prg_Init];
-program_defs_ref := [Component_def];
Addsimps (map simp_of_act [a_def]);
(* Theorems about sum and sumj *)
@@ -67,11 +66,12 @@
(* Correctness proofs for Components *)
(* p2 and p3 proofs *)
Goal "Component i : stable {s. s C = s (c i) + k}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p2";
-Goal
-"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
+Goal "Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p3";
--- a/src/HOL/UNITY/Comp/Counterc.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.ML Thu Jan 30 18:08:09 2003 +0100
@@ -13,7 +13,6 @@
Addsimps [Component_def RS def_prg_Init,
Component_def RS def_prg_AllowedActs];
-program_defs_ref := [Component_def];
Addsimps (map simp_of_act [a_def]);
(* Theorems about sum and sumj *)
@@ -57,6 +56,7 @@
Goal "Component i: stable {s. C s = (c s) i + k}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "p2";
--- a/src/HOL/UNITY/Constrains.ML Thu Jan 30 10:35:56 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,407 +0,0 @@
-(* Title: HOL/UNITY/Constrains
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Safety relations: restricted to the set of reachable states.
-*)
-
-
-(*** traces and reachable ***)
-
-Goal "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}";
-by Safe_tac;
-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_subset_reachable";
-
-Goal "Acts G <= Acts F ==> G : stable (reachable F)";
-by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
-qed "stable_reachable";
-
-AddSIs [stable_reachable];
-Addsimps [stable_reachable];
-
-(*The set of all reachable states is an invariant...*)
-Goal "F : invariant (reachable F)";
-by (simp_tac (simpset() addsimps [invariant_def]) 1);
-by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "invariant_reachable";
-
-(*...in fact the strongest invariant!*)
-Goal "F : invariant A ==> reachable F <= A";
-by (full_simp_tac
- (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
-by (rtac subsetI 1);
-by (etac reachable.induct 1);
-by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "invariant_includes_reachable";
-
-
-(*** Co ***)
-
-(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
-bind_thm ("constrains_reachable_Int",
- subset_refl RS
- rewrite_rule [stable_def] stable_reachable RS
- constrains_Int);
-
-(*Resembles the previous definition of Constrains*)
-Goalw [Constrains_def]
- "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}";
-by (blast_tac (claset() addDs [constrains_reachable_Int]
- addIs [constrains_weaken]) 1);
-qed "Constrains_eq_constrains";
-
-Goalw [Constrains_def] "F : A co A' ==> F : A Co A'";
-by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
-qed "constrains_imp_Constrains";
-
-Goalw [stable_def, Stable_def] "F : stable A ==> F : Stable A";
-by (etac constrains_imp_Constrains 1);
-qed "stable_imp_Stable";
-
-val prems = Goal
- "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
-\ ==> F : A Co A'";
-by (rtac constrains_imp_Constrains 1);
-by (blast_tac (claset() addIs (constrainsI::prems)) 1);
-qed "ConstrainsI";
-
-Goalw [Constrains_def, constrains_def] "F : {} Co B";
-by (Blast_tac 1);
-qed "Constrains_empty";
-
-Goal "F : A Co UNIV";
-by (blast_tac (claset() addIs [ConstrainsI]) 1);
-qed "Constrains_UNIV";
-AddIffs [Constrains_empty, Constrains_UNIV];
-
-Goalw [Constrains_def]
- "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
-by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
-qed "Constrains_weaken_R";
-
-Goalw [Constrains_def]
- "[| F : A Co A'; B<=A |] ==> F : B Co A'";
-by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
-qed "Constrains_weaken_L";
-
-Goalw [Constrains_def]
- "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "Constrains_weaken";
-
-(** Union **)
-
-Goalw [Constrains_def]
- "[| F : A Co A'; F : B Co B' |] \
-\ ==> F : (A Un B) Co (A' Un B')";
-by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
-qed "Constrains_Un";
-
-val [prem] = Goalw [Constrains_def]
- "(!!i. i:I ==> F : (A i) Co (A' i)) \
-\ ==> F : (UN i:I. A i) Co (UN i:I. A' i)";
-by (rtac CollectI 1);
-by (rtac (prem RS CollectD RS constrains_UN RS constrains_weaken) 1);
-by Auto_tac;
-qed "Constrains_UN";
-
-(** Intersection **)
-
-Goalw [Constrains_def]
- "[| F : A Co A'; F : B Co B' |] \
-\ ==> F : (A Int B) Co (A' Int B')";
-by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
-qed "Constrains_Int";
-
-val [prem] = Goalw [Constrains_def]
- "(!!i. i:I ==> F : (A i) Co (A' i)) \
-\ ==> F : (INT i:I. A i) Co (INT i:I. A' i)";
-by (rtac CollectI 1);
-by (rtac (prem RS CollectD RS constrains_INT RS constrains_weaken) 1);
-by Auto_tac;
-qed "Constrains_INT";
-
-Goal "F : A Co A' ==> reachable F Int A <= A'";
-by (asm_full_simp_tac (simpset() addsimps [constrains_imp_subset,
- Constrains_def]) 1);
-qed "Constrains_imp_subset";
-
-Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
-by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
-qed "Constrains_trans";
-
-Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
-by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains,
- constrains_def]) 1);
-by (Blast_tac 1);
-qed "Constrains_cancel";
-
-
-(*** Stable ***)
-
-(*Useful because there's no Stable_weaken. [Tanja Vos]*)
-Goal "[| F: Stable A; A = B |] ==> F : Stable B";
-by (Blast_tac 1);
-qed "Stable_eq";
-
-Goal "(F : Stable A) = (F : stable (reachable F Int A))";
-by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains,
- stable_def]) 1);
-qed "Stable_eq_stable";
-
-Goalw [Stable_def] "F : A Co A ==> F : Stable A";
-by (assume_tac 1);
-qed "StableI";
-
-Goalw [Stable_def] "F : Stable A ==> F : A Co A";
-by (assume_tac 1);
-qed "StableD";
-
-Goalw [Stable_def]
- "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')";
-by (blast_tac (claset() addIs [Constrains_Un]) 1);
-qed "Stable_Un";
-
-Goalw [Stable_def]
- "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')";
-by (blast_tac (claset() addIs [Constrains_Int]) 1);
-qed "Stable_Int";
-
-Goalw [Stable_def]
- "[| F : Stable C; F : A Co (C Un A') |] \
-\ ==> F : (C Un A) Co (C Un A')";
-by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
-qed "Stable_Constrains_Un";
-
-Goalw [Stable_def]
- "[| F : Stable C; F : (C Int A) Co A' |] \
-\ ==> F : (C Int A) Co (C Int A')";
-by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
-qed "Stable_Constrains_Int";
-
-val [prem] = Goalw [Stable_def]
- "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)";
-by (rtac (prem RS Constrains_UN) 1);
-by (assume_tac 1);
-qed "Stable_UN";
-
-val [prem] = Goalw [Stable_def]
- "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)";
-by (rtac (prem RS Constrains_INT) 1);
-by (assume_tac 1);
-qed "Stable_INT";
-
-Goal "F : Stable (reachable F)";
-by (simp_tac (simpset() addsimps [Stable_eq_stable]) 1);
-qed "Stable_reachable";
-
-
-
-(*** Increasing ***)
-
-Goalw [Increasing_def]
- "F : Increasing f ==> F : Stable {s. x <= f s}";
-by (Blast_tac 1);
-qed "IncreasingD";
-
-Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
- "mono g ==> Increasing f <= Increasing (g o f)";
-by Auto_tac;
-by (blast_tac (claset() addIs [monoD, order_trans]) 1);
-qed "mono_Increasing_o";
-
-Goalw [Increasing_def]
- "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}";
-by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
-by (Blast_tac 1);
-qed "strict_IncreasingD";
-
-Goalw [increasing_def, Increasing_def]
- "F : increasing f ==> F : Increasing f";
-by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
-qed "increasing_imp_Increasing";
-
-bind_thm ("Increasing_constant",
- increasing_constant RS increasing_imp_Increasing);
-AddIffs [Increasing_constant];
-
-
-(*** The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder to use
- in forward proof. ***)
-
-Goalw [Constrains_def, constrains_def]
- "[| ALL m. F : {s. s x = m} Co (B m) |] \
-\ ==> F : {s. s x : M} Co (UN m:M. B m)";
-by (Blast_tac 1);
-qed "Elimination";
-
-(*As above, but for the trivial case of a one-variable state, in which the
- state is identified with its one variable.*)
-Goalw [Constrains_def, constrains_def]
- "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)";
-by (Blast_tac 1);
-qed "Elimination_sing";
-
-
-(*** Specialized laws for handling Always ***)
-
-(** Natural deduction rules for "Always A" **)
-
-Goal "[| Init F<=A; F : Stable A |] ==> F : Always A";
-by (asm_simp_tac (simpset() addsimps [Always_def]) 1);
-qed "AlwaysI";
-
-Goal "F : Always A ==> Init F<=A & F : Stable A";
-by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
-qed "AlwaysD";
-
-bind_thm ("AlwaysE", AlwaysD RS conjE);
-bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);
-
-
-(*The set of all reachable states is Always*)
-Goal "F : Always A ==> reachable F <= A";
-by (full_simp_tac
- (simpset() addsimps [Stable_def, Constrains_def, constrains_def,
- Always_def]) 1);
-by (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 : invariant A ==> F : Always A";
-by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
-qed "invariant_imp_Always";
-
-bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
-
-Goal "Always A = {F. F : invariant (reachable F Int A)}";
-by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
- Constrains_eq_constrains, stable_def]) 1);
-by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "Always_eq_invariant_reachable";
-
-(*the RHS is the traditional definition of the "always" operator*)
-Goal "Always A = {F. reachable F <= A}";
-by (auto_tac (claset() addDs [invariant_includes_reachable],
- simpset() addsimps [Int_absorb2, invariant_reachable,
- Always_eq_invariant_reachable]));
-qed "Always_eq_includes_reachable";
-
-Goal "Always UNIV = UNIV";
-by (auto_tac (claset(),
- simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_UNIV_eq";
-Addsimps [Always_UNIV_eq];
-
-Goal "UNIV <= A ==> F : Always A";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "UNIV_AlwaysI";
-
-Goal "Always A = (UN I: Pow A. invariant I)";
-by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
- impOfSubs invariant_includes_reachable]) 1);
-qed "Always_eq_UN_invariant";
-
-Goal "[| F : Always A; A <= B |] ==> F : Always B";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_weaken";
-
-
-(*** "Co" rules involving Always ***)
-
-Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')";
-by (asm_simp_tac
- (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
- Constrains_def, Int_assoc RS sym]) 1);
-qed "Always_Constrains_pre";
-
-Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')";
-by (asm_simp_tac
- (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
- Constrains_eq_constrains, Int_assoc RS sym]) 1);
-qed "Always_Constrains_post";
-
-(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
-bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
-
-(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *)
-bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
-
-(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
-Goal "[| F : Always C; F : A Co A'; \
-\ C Int B <= A; C Int A' <= B' |] \
-\ ==> F : B Co B'";
-by (rtac Always_ConstrainsI 1);
-by (assume_tac 1);
-by (dtac Always_ConstrainsD 1);
-by (assume_tac 1);
-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";
-
-Goal "Always (INTER I A) = (INT i:I. Always (A i))";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_INT_distrib";
-
-Goal "[| F : Always A; F : Always B |] ==> F : Always (A Int B)";
-by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1);
-qed "Always_Int_I";
-
-(*Allows a kind of "implication introduction"*)
-Goal "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)";
-by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_Compl_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 : 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 constrains_tac 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,
- full_simp_tac (simpset() addsimps !program_defs_ref) 1,
- REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS Clarify_tac,
- ALLGOALS Asm_lr_simp_tac]) i;
-
-
-(*For proving invariants*)
-fun always_tac i =
- rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
--- a/src/HOL/UNITY/Constrains.thy Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy Thu Jan 30 18:08:09 2003 +0100
@@ -3,10 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Safety relations: restricted to the set of reachable states.
+Weak safety relations: restricted to the set of reachable states.
*)
-Constrains = UNITY +
+theory Constrains = UNITY:
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
@@ -14,36 +14,30 @@
Arguments MUST be curried in an inductive definition*)
inductive "traces init acts"
- 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 |]
- ==> (s', s#evs) : traces init acts"
+ Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |]
+ ==> (s', s#evs) : traces init acts"
consts reachable :: "'a program => 'a set"
inductive "reachable F"
- intrs
- Init "s: Init F ==> s : reachable F"
-
- Acts "[| act: Acts F; s : reachable F; (s,s'): act |]
- ==> s' : reachable F"
+ intros
+ Init: "s: Init F ==> s : reachable F"
-consts
- Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60)
- op_Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60)
+ Acts: "[| act: Acts F; s : reachable F; (s,s'): act |]
+ ==> s' : reachable F"
-defs
- Constrains_def
+constdefs
+ Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60)
"A Co B == {F. F : (reachable F Int A) co B}"
- Unless_def
+ Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60)
"A Unless B == (A-B) Co (A Un B)"
-constdefs
-
Stable :: "'a set => 'a program set"
"Stable A == A Co A"
@@ -55,4 +49,345 @@
Increasing :: "['a => 'b::{order}] => 'a program set"
"Increasing f == INT z. Stable {s. z <= f s}"
+
+(*** traces and reachable ***)
+
+lemma reachable_equiv_traces:
+ "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
+apply safe
+apply (erule_tac [2] traces.induct)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros traces.intros)+
+done
+
+lemma Init_subset_reachable: "Init F <= reachable F"
+by (blast intro: reachable.intros)
+
+lemma stable_reachable [intro!,simp]:
+ "Acts G <= Acts F ==> G : stable (reachable F)"
+by (blast intro: stableI constrainsI reachable.intros)
+
+(*The set of all reachable states is an invariant...*)
+lemma invariant_reachable: "F : invariant (reachable F)"
+apply (simp add: invariant_def)
+apply (blast intro: reachable.intros)
+done
+
+(*...in fact the strongest invariant!*)
+lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
+apply (simp add: stable_def constrains_def invariant_def)
+apply (rule subsetI)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros)+
+done
+
+
+(*** Co ***)
+
+(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+lemmas constrains_reachable_Int =
+ subset_refl [THEN stable_reachable [unfolded stable_def],
+ THEN constrains_Int, standard]
+
+(*Resembles the previous definition of Constrains*)
+lemma Constrains_eq_constrains:
+ "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}"
+apply (unfold Constrains_def)
+apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
+done
+
+lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_weaken_L)
+done
+
+lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
+apply (unfold stable_def Stable_def)
+apply (erule constrains_imp_Constrains)
+done
+
+lemma ConstrainsI:
+ "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A')
+ ==> F : A Co A'"
+apply (rule constrains_imp_Constrains)
+apply (blast intro: constrainsI)
+done
+
+lemma Constrains_empty [iff]: "F : {} Co B"
+by (unfold Constrains_def constrains_def, blast)
+
+lemma Constrains_UNIV [iff]: "F : A Co UNIV"
+by (blast intro: ConstrainsI)
+
+lemma Constrains_weaken_R:
+ "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_weaken_R)
+done
+
+lemma Constrains_weaken_L:
+ "[| F : A Co A'; B<=A |] ==> F : B Co A'"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_weaken_L)
+done
+
+lemma Constrains_weaken:
+ "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_weaken)
+done
+
+(** Union **)
+
+lemma Constrains_Un:
+ "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_Un [THEN constrains_weaken])
+done
+
+lemma Constrains_UN:
+ assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
+ shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
+apply (unfold Constrains_def)
+apply (rule CollectI)
+apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN,
+ THEN constrains_weaken], auto)
+done
+
+(** Intersection **)
+
+lemma Constrains_Int:
+ "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
+apply (unfold Constrains_def)
+apply (blast intro: constrains_Int [THEN constrains_weaken])
+done
+
+lemma Constrains_INT:
+ assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
+ shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
+apply (unfold Constrains_def)
+apply (rule CollectI)
+apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT,
+ THEN constrains_weaken], auto)
+done
+
+lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
+by (simp add: constrains_imp_subset Constrains_def)
+
+lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
+apply (simp add: Constrains_eq_constrains)
+apply (blast intro: constrains_trans constrains_weaken)
+done
+
+lemma Constrains_cancel:
+ "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
+by (simp add: Constrains_eq_constrains constrains_def, blast)
+
+
+(*** Stable ***)
+
+(*Useful because there's no Stable_weaken. [Tanja Vos]*)
+lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
+by blast
+
+lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
+by (simp add: Stable_def Constrains_eq_constrains stable_def)
+
+lemma StableI: "F : A Co A ==> F : Stable A"
+by (unfold Stable_def, assumption)
+
+lemma StableD: "F : Stable A ==> F : A Co A"
+by (unfold Stable_def, assumption)
+
+lemma Stable_Un:
+ "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Un)
+done
+
+lemma Stable_Int:
+ "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Int)
+done
+
+lemma Stable_Constrains_Un:
+ "[| F : Stable C; F : A Co (C Un A') |]
+ ==> F : (C Un A) Co (C Un A')"
+apply (unfold Stable_def)
+apply (blast intro: Constrains_Un [THEN Constrains_weaken])
+done
+
+lemma Stable_Constrains_Int:
+ "[| F : Stable C; F : (C Int A) Co A' |]
+ ==> F : (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:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
+by (simp add: Stable_def Constrains_UN)
+
+lemma Stable_INT:
+ "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
+by (simp add: Stable_def Constrains_INT)
+
+lemma Stable_reachable: "F : Stable (reachable F)"
+by (simp add: Stable_eq_stable)
+
+
+
+(*** Increasing ***)
+
+lemma IncreasingD:
+ "F : Increasing f ==> F : Stable {s. x <= f s}"
+by (unfold Increasing_def, blast)
+
+lemma mono_Increasing_o:
+ "mono g ==> Increasing f <= Increasing (g o f)"
+apply (simp add: Increasing_def Stable_def Constrains_def stable_def
+ constrains_def)
+apply (blast intro: monoD order_trans)
+done
+
+lemma strict_IncreasingD:
+ "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
+by (simp add: Increasing_def Suc_le_eq [symmetric])
+
+lemma increasing_imp_Increasing:
+ "F : increasing f ==> F : Increasing f"
+apply (unfold increasing_def Increasing_def)
+apply (blast intro: stable_imp_Stable)
+done
+
+lemmas Increasing_constant =
+ increasing_constant [THEN increasing_imp_Increasing, standard, iff]
+
+
+(*** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. ***)
+
+lemma Elimination:
+ "[| ALL m. F : {s. s x = m} Co (B m) |]
+ ==> F : {s. s x : M} Co (UN m:M. B m)"
+
+by (unfold Constrains_def constrains_def, blast)
+
+(*As above, but for the trivial case of a one-variable state, in which the
+ state is identified with its one variable.*)
+lemma Elimination_sing:
+ "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
+by (unfold Constrains_def constrains_def, blast)
+
+
+(*** Specialized laws for handling Always ***)
+
+(** Natural deduction rules for "Always A" **)
+
+lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A"
+by (simp add: Always_def)
+
+lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
+by (simp add: Always_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 : Always A ==> reachable F <= A"
+apply (simp add: Stable_def Constrains_def constrains_def Always_def)
+apply (rule subsetI)
+apply (erule reachable.induct)
+apply (blast intro: reachable.intros)+
+done
+
+lemma invariant_imp_Always:
+ "F : invariant A ==> F : 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. F : invariant (reachable F Int A)}"
+apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
+ stable_def)
+apply (blast intro: reachable.intros)
+done
+
+(*the RHS is the traditional definition of the "always" operator*)
+lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
+by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
+
+lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
+by (auto simp add: Always_eq_includes_reachable)
+
+lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
+by (auto simp add: Always_eq_includes_reachable)
+
+lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
+apply (simp add: Always_eq_includes_reachable)
+apply (blast intro: invariantI Init_subset_reachable [THEN subsetD]
+ invariant_includes_reachable [THEN subsetD])
+done
+
+lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
+by (auto simp add: Always_eq_includes_reachable)
+
+
+(*** "Co" rules involving Always ***)
+
+lemma Always_Constrains_pre:
+ "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
+by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def
+ Int_assoc [symmetric])
+
+lemma Always_Constrains_post:
+ "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
+by (simp add: Always_includes_reachable [THEN Int_absorb2]
+ Constrains_eq_constrains Int_assoc [symmetric])
+
+(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
+lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
+
+(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV 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 : Always C; F : A Co A';
+ C Int B <= A; C Int A' <= B' |]
+ ==> F : B Co B'"
+apply (rule Always_ConstrainsI, assumption)
+apply (drule Always_ConstrainsD, assumption)
+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)
+
+lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
+by (auto simp add: Always_eq_includes_reachable)
+
+lemma Always_Int_I:
+ "[| F : Always A; F : Always B |] ==> F : Always (A Int B)"
+by (simp add: Always_Int_distrib)
+
+(*Allows a kind of "implication introduction"*)
+lemma Always_Compl_Un_eq:
+ "F : Always A ==> (F : Always (-A Un B)) = (F : 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 : Always A", standard]
+
end
--- a/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Thu Jan 30 18:08:09 2003 +0100
@@ -31,10 +31,10 @@
Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
by (REPEAT (resolve_tac [exI,bexI] 1));
-by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
-by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
-by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
-by (rtac reachable.Init 5);
+by (res_inst_tac [("act", "NS3")] reachable_Acts 2);
+by (res_inst_tac [("act", "NS2")] reachable_Acts 3);
+by (res_inst_tac [("act", "NS1")] reachable_Acts 4);
+by (rtac reachable_Init 5);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
by (REPEAT_FIRST (rtac exI ));
by possibility_tac;
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jan 30 18:08:09 2003 +0100
@@ -10,7 +10,7 @@
Original file is ../Auth/NS_Public_Bad
*)
-NSP_Bad = Public + Constrains +
+NSP_Bad = Public + UNITY_Main +
types state = event list
--- a/src/HOL/UNITY/UNITY.ML Thu Jan 30 10:35:56 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-(* Title: HOL/UNITY/UNITY
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-The basic UNITY theory (revised version, based upon the "co" operator)
-
-From Misra, "A Logic for Concurrent Programming", 1994
-*)
-
-(*Perhaps equalities.ML shouldn't add this in the first place!*)
-Delsimps [image_Collect];
-
-(*** The abstract type of programs ***)
-
-val rep_ss = simpset() addsimps
- [Init_def, Acts_def, AllowedActs_def,
- mk_program_def, Program_def, Rep_Program,
- Rep_Program_inverse, Abs_Program_inverse];
-
-
-Goal "Id : Acts F";
-by (cut_inst_tac [("x", "F")] Rep_Program 1);
-by (auto_tac (claset(), rep_ss));
-qed "Id_in_Acts";
-AddIffs [Id_in_Acts];
-
-Goal "insert Id (Acts F) = Acts F";
-by (simp_tac (simpset() addsimps [insert_absorb, Id_in_Acts]) 1);
-qed "insert_Id_Acts";
-AddIffs [insert_Id_Acts];
-
-Goal "Id : AllowedActs F";
-by (cut_inst_tac [("x", "F")] Rep_Program 1);
-by (auto_tac (claset(), rep_ss));
-qed "Id_in_AllowedActs";
-AddIffs [Id_in_AllowedActs];
-
-Goal "insert Id (AllowedActs F) = AllowedActs F";
-by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1);
-qed "insert_Id_AllowedActs";
-AddIffs [insert_Id_AllowedActs];
-
-(** Inspectors for type "program" **)
-
-Goal "Init (mk_program (init,acts,allowed)) = init";
-by (auto_tac (claset(), rep_ss));
-qed "Init_eq";
-
-Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts";
-by (auto_tac (claset(), rep_ss));
-qed "Acts_eq";
-
-Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed";
-by (auto_tac (claset(), rep_ss));
-qed "AllowedActs_eq";
-
-Addsimps [Init_eq, Acts_eq, AllowedActs_eq];
-
-(** Equality for UNITY programs **)
-
-Goal "mk_program (Init F, Acts F, AllowedActs F) = F";
-by (cut_inst_tac [("x", "F")] Rep_Program 1);
-by (auto_tac (claset(), rep_ss));
-by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
-by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
-qed "surjective_mk_program";
-
-Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \
-\ ==> F = G";
-by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
-by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
-by (Asm_simp_tac 1);
-qed "program_equalityI";
-
-val [major,minor] =
-Goal "[| F = G; \
-\ [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\
-\ ==> P |] ==> P";
-by (rtac minor 1);
-by (auto_tac (claset(), simpset() addsimps [major]));
-qed "program_equalityE";
-
-Goal "(F=G) = \
-\ (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)";
-by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
-qed "program_equality_iff";
-
-Addsimps [surjective_mk_program];
-
-
-(*** These rules allow "lazy" definition expansion
- They avoid expanding the full program, which is a large expression
-***)
-
-Goal "F == mk_program (init,acts,allowed) ==> Init F = init";
-by Auto_tac;
-qed "def_prg_Init";
-
-Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts";
-by Auto_tac;
-qed "def_prg_Acts";
-
-Goal "F == mk_program (init,acts,allowed) \
-\ ==> AllowedActs F = insert Id allowed";
-by Auto_tac;
-qed "def_prg_AllowedActs";
-
-(*The program is not expanded, but its Init and Acts are*)
-val [rew] = goal thy
- "[| F == mk_program (init,acts,allowed) |] \
-\ ==> Init F = init & Acts F = insert Id acts";
-by (rewtac rew);
-by Auto_tac;
-qed "def_prg_simps";
-
-(*An action is expanded only if a pair of states is being tested against it*)
-Goal "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'";
-by Auto_tac;
-qed "def_act_simp";
-
-fun simp_of_act def = def RS def_act_simp;
-
-(*A set is expanded only if an element is being tested against it*)
-Goal "A == B ==> (x : A) = (x : B)";
-by Auto_tac;
-qed "def_set_simp";
-
-fun simp_of_set def = def RS def_set_simp;
-
-
-(*** co ***)
-
-val prems = Goalw [constrains_def]
- "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') \
-\ ==> F : A co A'";
-by (blast_tac (claset() addIs prems) 1);
-qed "constrainsI";
-
-Goalw [constrains_def]
- "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'";
-by (Blast_tac 1);
-qed "constrainsD";
-
-Goalw [constrains_def] "F : {} co B";
-by (Blast_tac 1);
-qed "constrains_empty";
-
-Goalw [constrains_def] "(F : A co {}) = (A={})";
-by (Blast_tac 1);
-qed "constrains_empty2";
-
-Goalw [constrains_def] "(F : UNIV co B) = (B = UNIV)";
-by (Blast_tac 1);
-qed "constrains_UNIV";
-
-Goalw [constrains_def] "F : A co UNIV";
-by (Blast_tac 1);
-qed "constrains_UNIV2";
-
-AddIffs [constrains_empty, constrains_empty2,
- constrains_UNIV, constrains_UNIV2];
-
-(*monotonic in 2nd argument*)
-Goalw [constrains_def]
- "[| F : A co A'; A'<=B' |] ==> F : A co B'";
-by (Blast_tac 1);
-qed "constrains_weaken_R";
-
-(*anti-monotonic in 1st argument*)
-Goalw [constrains_def]
- "[| F : A co A'; B<=A |] ==> F : B co A'";
-by (Blast_tac 1);
-qed "constrains_weaken_L";
-
-Goalw [constrains_def]
- "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
-by (Blast_tac 1);
-qed "constrains_weaken";
-
-(** Union **)
-
-Goalw [constrains_def]
- "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')";
-by (Blast_tac 1);
-qed "constrains_Un";
-
-Goalw [constrains_def]
- "ALL i:I. F : (A i) co (A' i) ==> F : (UN i:I. A i) co (UN i:I. A' i)";
-by (Blast_tac 1);
-bind_thm ("constrains_UN", ballI RS result());
-
-Goalw [constrains_def] "(A Un B) co C = (A co C) Int (B co C)";
-by (Blast_tac 1);
-qed "constrains_Un_distrib";
-
-Goalw [constrains_def] "(UN i:I. A i) co B = (INT i:I. A i co B)";
-by (Blast_tac 1);
-qed "constrains_UN_distrib";
-
-Goalw [constrains_def] "C co (A Int B) = (C co A) Int (C co B)";
-by (Blast_tac 1);
-qed "constrains_Int_distrib";
-
-Goalw [constrains_def] "A co (INT i:I. B i) = (INT i:I. A co B i)";
-by (Blast_tac 1);
-qed "constrains_INT_distrib";
-
-(** Intersection **)
-
-Goalw [constrains_def]
- "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')";
-by (Blast_tac 1);
-qed "constrains_Int";
-
-Goalw [constrains_def]
- "ALL i:I. F : (A i) co (A' i) ==> F : (INT i:I. A i) co (INT i:I. A' i)";
-by (Blast_tac 1);
-bind_thm ("constrains_INT", ballI RS result());
-
-Goalw [constrains_def] "F : A co A' ==> A <= A'";
-by Auto_tac;
-qed "constrains_imp_subset";
-
-(*The reasoning is by subsets since "co" refers to single actions
- only. So this rule isn't that useful.*)
-Goalw [constrains_def]
- "[| F : A co B; F : B co C |] ==> F : A co C";
-by (Blast_tac 1);
-qed "constrains_trans";
-
-Goalw [constrains_def]
- "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')";
-by (Clarify_tac 1);
-by (Blast_tac 1);
-qed "constrains_cancel";
-
-
-(*** unless ***)
-
-Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B";
-by (assume_tac 1);
-qed "unlessI";
-
-Goalw [unless_def] "F : A unless B ==> F : (A-B) co (A Un B)";
-by (assume_tac 1);
-qed "unlessD";
-
-
-(*** stable ***)
-
-Goalw [stable_def] "F : A co A ==> F : stable A";
-by (assume_tac 1);
-qed "stableI";
-
-Goalw [stable_def] "F : stable A ==> F : A co A";
-by (assume_tac 1);
-qed "stableD";
-
-Goalw [stable_def, constrains_def] "stable UNIV = UNIV";
-by Auto_tac;
-qed "stable_UNIV";
-Addsimps [stable_UNIV];
-
-(** Union **)
-
-Goalw [stable_def]
- "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')";
-by (blast_tac (claset() addIs [constrains_Un]) 1);
-qed "stable_Un";
-
-Goalw [stable_def]
- "ALL i:I. F : stable (A i) ==> F : stable (UN i:I. A i)";
-by (blast_tac (claset() addIs [constrains_UN]) 1);
-bind_thm ("stable_UN", ballI RS result());
-
-(** Intersection **)
-
-Goalw [stable_def]
- "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
-by (blast_tac (claset() addIs [constrains_Int]) 1);
-qed "stable_Int";
-
-Goalw [stable_def]
- "ALL i:I. F : stable (A i) ==> F : stable (INT i:I. A i)";
-by (blast_tac (claset() addIs [constrains_INT]) 1);
-bind_thm ("stable_INT", ballI RS result());
-
-Goalw [stable_def, constrains_def]
- "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
-by (Blast_tac 1);
-qed "stable_constrains_Un";
-
-Goalw [stable_def, constrains_def]
- "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
-by (Blast_tac 1);
-qed "stable_constrains_Int";
-
-(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *)
-bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
-
-
-(*** invariant ***)
-
-Goal "[| Init F<=A; F: stable A |] ==> F : invariant A";
-by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantI";
-
-(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
-Goal "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)";
-by (auto_tac (claset(), simpset() addsimps [invariant_def, stable_Int]));
-qed "invariant_Int";
-
-
-(*** increasing ***)
-
-Goalw [increasing_def]
- "F : increasing f ==> F : stable {s. z <= f s}";
-by (Blast_tac 1);
-qed "increasingD";
-
-Goalw [increasing_def, stable_def] "F : increasing (%s. c)";
-by Auto_tac;
-qed "increasing_constant";
-AddIffs [increasing_constant];
-
-Goalw [increasing_def, stable_def, constrains_def]
- "mono g ==> increasing f <= increasing (g o f)";
-by Auto_tac;
-by (blast_tac (claset() addIs [monoD, order_trans]) 1);
-qed "mono_increasing_o";
-
-(*Holds by the theorem (Suc m <= n) = (m < n) *)
-Goalw [increasing_def]
- "!!z::nat. F : increasing f ==> F: stable {s. z < f s}";
-by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1);
-by (Blast_tac 1);
-qed "strict_increasingD";
-
-
-(** The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder to use
- in forward proof. **)
-
-Goalw [constrains_def]
- "[| ALL m:M. F : {s. s x = m} co (B m) |] \
-\ ==> F : {s. s x : M} co (UN m:M. B m)";
-by (Blast_tac 1);
-qed "elimination";
-
-(*As above, but for the trivial case of a one-variable state, in which the
- state is identified with its one variable.*)
-Goalw [constrains_def]
- "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)";
-by (Blast_tac 1);
-qed "elimination_sing";
-
-
-
-(*** Theoretical Results from Section 6 ***)
-
-Goalw [constrains_def, strongest_rhs_def]
- "F : A co (strongest_rhs F A )";
-by (Blast_tac 1);
-qed "constrains_strongest_rhs";
-
-Goalw [constrains_def, strongest_rhs_def]
- "F : A co B ==> strongest_rhs F A <= B";
-by (Blast_tac 1);
-qed "strongest_rhs_is_strongest";
-
-
-(** Ad-hoc set-theory rules **)
-
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-Addsimps [Un_Diff_Diff];
-
-Goal "Union(B) Int A = Union((%C. C Int A)`B)";
-by (Blast_tac 1);
-qed "Int_Union_Union";
-
-(** Needed for WF reasoning in WFair.ML **)
-
-Goal "less_than `` {k} = greaterThan k";
-by (Blast_tac 1);
-qed "Image_less_than";
-
-Goal "less_than^-1 `` {k} = lessThan k";
-by (Blast_tac 1);
-qed "Image_inverse_less_than";
-
-Addsimps [Image_less_than, Image_inverse_less_than];
--- a/src/HOL/UNITY/UNITY.thy Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy Thu Jan 30 18:08:09 2003 +0100
@@ -8,18 +8,21 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-UNITY = Main +
+theory UNITY = Main:
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
- allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
-
-consts
- constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
- op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
+ allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
+ by blast
constdefs
- mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
+ constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
+ "A co B == {F. ALL act: Acts F. act``A <= B}"
+
+ unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
+ "A unless B == (A-B) co (A Un B)"
+
+ mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
=> 'a program"
"mk_program == %(init, acts, allowed).
Abs_Program (init, insert Id acts, insert Id allowed)"
@@ -50,9 +53,325 @@
"increasing f == INT z. stable {s. z <= f s}"
-defs
- constrains_def "A co B == {F. ALL act: Acts F. act``A <= B}"
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+declare image_Collect [simp del]
+
+(*** The abstract type of programs ***)
+
+lemmas program_typedef =
+ Rep_Program Rep_Program_inverse Abs_Program_inverse
+ Program_def Init_def Acts_def AllowedActs_def mk_program_def
+
+lemma Id_in_Acts [iff]: "Id : Acts F"
+apply (cut_tac x = F in Rep_Program)
+apply (auto simp add: program_typedef)
+done
+
+lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
+by (simp add: insert_absorb Id_in_Acts)
+
+lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F"
+apply (cut_tac x = F in Rep_Program)
+apply (auto simp add: program_typedef)
+done
+
+lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
+by (simp add: insert_absorb Id_in_AllowedActs)
+
+(** Inspectors for type "program" **)
+
+lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
+by (auto simp add: program_typedef)
+
+lemma Acts_eq [simp]: "Acts (mk_program (init,acts,allowed)) = insert Id acts"
+by (auto simp add: program_typedef)
+
+lemma AllowedActs_eq [simp]:
+ "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
+by (auto simp add: program_typedef)
+
+(** Equality for UNITY programs **)
+
+lemma surjective_mk_program [simp]:
+ "mk_program (Init F, Acts F, AllowedActs F) = F"
+apply (cut_tac x = F in Rep_Program)
+apply (auto simp add: program_typedef)
+apply (drule_tac f = Abs_Program in arg_cong)+
+apply (simp add: program_typedef insert_absorb)
+done
+
+lemma program_equalityI:
+ "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]
+ ==> F = G"
+apply (rule_tac t = F in surjective_mk_program [THEN subst])
+apply (rule_tac t = G in surjective_mk_program [THEN subst], simp)
+done
+
+lemma program_equalityE:
+ "[| F = G;
+ [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]
+ ==> P |] ==> P"
+by simp
+
+lemma program_equality_iff:
+ "(F=G) =
+ (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)"
+by (blast intro: program_equalityI program_equalityE)
+
+
+(*** These rules allow "lazy" definition expansion
+ They avoid expanding the full program, which is a large expression
+***)
+
+lemma def_prg_Init: "F == mk_program (init,acts,allowed) ==> Init F = init"
+by auto
+
+lemma def_prg_Acts:
+ "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts"
+by auto
+
+lemma def_prg_AllowedActs:
+ "F == mk_program (init,acts,allowed)
+ ==> AllowedActs F = insert Id allowed"
+by auto
+
+(*The program is not expanded, but its Init and Acts are*)
+lemma def_prg_simps:
+ "[| F == mk_program (init,acts,allowed) |]
+ ==> Init F = init & Acts F = insert Id acts"
+by simp
+
+(*An action is expanded only if a pair of states is being tested against it*)
+lemma def_act_simp:
+ "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"
+by auto
+
+(*A set is expanded only if an element is being tested against it*)
+lemma def_set_simp: "A == B ==> (x : A) = (x : B)"
+by auto
+
+
+(*** co ***)
+
+lemma constrainsI:
+ "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A')
+ ==> F : A co A'"
+by (simp add: constrains_def, blast)
+
+lemma constrainsD:
+ "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"
+by (unfold constrains_def, blast)
+
+lemma constrains_empty [iff]: "F : {} co B"
+by (unfold constrains_def, blast)
+
+lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})"
+by (unfold constrains_def, blast)
+
+lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)"
+by (unfold constrains_def, blast)
+
+lemma constrains_UNIV2 [iff]: "F : A co UNIV"
+by (unfold constrains_def, blast)
+
+(*monotonic in 2nd argument*)
+lemma constrains_weaken_R:
+ "[| F : A co A'; A'<=B' |] ==> F : A co B'"
+by (unfold constrains_def, blast)
+
+(*anti-monotonic in 1st argument*)
+lemma constrains_weaken_L:
+ "[| F : A co A'; B<=A |] ==> F : B co A'"
+by (unfold constrains_def, blast)
+
+lemma constrains_weaken:
+ "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"
+by (unfold constrains_def, blast)
+
+(** Union **)
+
+lemma constrains_Un:
+ "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"
+by (unfold constrains_def, blast)
+
+lemma constrains_UN:
+ "(!!i. i:I ==> F : (A i) co (A' i))
+ ==> F : (UN i:I. A i) co (UN i:I. A' i)"
+by (unfold constrains_def, blast)
+
+lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)"
+by (unfold constrains_def, blast)
+
+lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)"
+by (unfold constrains_def, blast)
+
+lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)"
+by (unfold constrains_def, blast)
+
+lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)"
+by (unfold constrains_def, blast)
+
+(** Intersection **)
- unless_def "A unless B == (A-B) co (A Un B)"
+lemma constrains_Int:
+ "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"
+by (unfold constrains_def, blast)
+
+lemma constrains_INT:
+ "(!!i. i:I ==> F : (A i) co (A' i))
+ ==> F : (INT i:I. A i) co (INT i:I. A' i)"
+by (unfold constrains_def, blast)
+
+lemma constrains_imp_subset: "F : A co A' ==> A <= A'"
+by (unfold constrains_def, auto)
+
+(*The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.*)
+lemma constrains_trans:
+ "[| F : A co B; F : B co C |] ==> F : A co C"
+by (unfold constrains_def, blast)
+
+lemma constrains_cancel:
+ "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"
+by (unfold constrains_def, clarify, blast)
+
+
+(*** unless ***)
+
+lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B"
+by (unfold unless_def, assumption)
+
+lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)"
+by (unfold unless_def, assumption)
+
+
+(*** stable ***)
+
+lemma stableI: "F : A co A ==> F : stable A"
+by (unfold stable_def, assumption)
+
+lemma stableD: "F : stable A ==> F : A co A"
+by (unfold stable_def, assumption)
+
+lemma stable_UNIV [simp]: "stable UNIV = UNIV"
+by (unfold stable_def constrains_def, auto)
+
+(** Union **)
+
+lemma stable_Un:
+ "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"
+
+apply (unfold stable_def)
+apply (blast intro: constrains_Un)
+done
+
+lemma stable_UN:
+ "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)"
+apply (unfold stable_def)
+apply (blast intro: constrains_UN)
+done
+
+(** Intersection **)
+
+lemma stable_Int:
+ "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"
+apply (unfold stable_def)
+apply (blast intro: constrains_Int)
+done
+
+lemma stable_INT:
+ "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)"
+apply (unfold stable_def)
+apply (blast intro: constrains_INT)
+done
+
+lemma stable_constrains_Un:
+ "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"
+by (unfold stable_def constrains_def, blast)
+
+lemma stable_constrains_Int:
+ "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"
+by (unfold stable_def constrains_def, blast)
+
+(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *)
+lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
+
+
+(*** invariant ***)
+
+lemma invariantI: "[| Init F<=A; F: stable A |] ==> F : invariant A"
+by (simp add: invariant_def)
+
+(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+lemma invariant_Int:
+ "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"
+by (auto simp add: invariant_def stable_Int)
+
+
+(*** increasing ***)
+
+lemma increasingD:
+ "F : increasing f ==> F : stable {s. z <= f s}"
+
+by (unfold increasing_def, blast)
+
+lemma increasing_constant [iff]: "F : increasing (%s. c)"
+by (unfold increasing_def stable_def, auto)
+
+lemma mono_increasing_o:
+ "mono g ==> increasing f <= increasing (g o f)"
+apply (unfold increasing_def stable_def constrains_def, auto)
+apply (blast intro: monoD order_trans)
+done
+
+(*Holds by the theorem (Suc m <= n) = (m < n) *)
+lemma strict_increasingD:
+ "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"
+by (simp add: increasing_def Suc_le_eq [symmetric])
+
+
+(** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. **)
+
+lemma elimination:
+ "[| ALL m:M. F : {s. s x = m} co (B m) |]
+ ==> F : {s. s x : M} co (UN m:M. B m)"
+by (unfold constrains_def, blast)
+
+(*As above, but for the trivial case of a one-variable state, in which the
+ state is identified with its one variable.*)
+lemma elimination_sing:
+ "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"
+by (unfold constrains_def, blast)
+
+
+
+(*** Theoretical Results from Section 6 ***)
+
+lemma constrains_strongest_rhs:
+ "F : A co (strongest_rhs F A )"
+by (unfold constrains_def strongest_rhs_def, blast)
+
+lemma strongest_rhs_is_strongest:
+ "F : A co B ==> strongest_rhs F A <= B"
+by (unfold constrains_def strongest_rhs_def, blast)
+
+
+(** Ad-hoc set-theory rules **)
+
+lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B"
+by blast
+
+lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)"
+by blast
+
+(** Needed for WF reasoning in WFair.ML **)
+
+lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
+by blast
+
+lemma Image_inverse_less_than [simp]: "less_than^-1 `` {k} = lessThan k"
+by blast
end
--- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 18:08:09 2003 +0100
@@ -6,6 +6,215 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*UNITY*)
+val constrains_def = thm "constrains_def";
+val stable_def = thm "stable_def";
+val invariant_def = thm "invariant_def";
+val increasing_def = thm "increasing_def";
+val Allowed_def = thm "Allowed_def";
+val Id_in_Acts = thm "Id_in_Acts";
+val insert_Id_Acts = thm "insert_Id_Acts";
+val Id_in_AllowedActs = thm "Id_in_AllowedActs";
+val insert_Id_AllowedActs = thm "insert_Id_AllowedActs";
+val Init_eq = thm "Init_eq";
+val Acts_eq = thm "Acts_eq";
+val AllowedActs_eq = thm "AllowedActs_eq";
+val surjective_mk_program = thm "surjective_mk_program";
+val program_equalityI = thm "program_equalityI";
+val program_equalityE = thm "program_equalityE";
+val program_equality_iff = thm "program_equality_iff";
+val def_prg_Init = thm "def_prg_Init";
+val def_prg_Acts = thm "def_prg_Acts";
+val def_prg_AllowedActs = thm "def_prg_AllowedActs";
+val def_prg_simps = thm "def_prg_simps";
+val def_act_simp = thm "def_act_simp";
+val def_set_simp = thm "def_set_simp";
+val constrainsI = thm "constrainsI";
+val constrainsD = thm "constrainsD";
+val constrains_empty = thm "constrains_empty";
+val constrains_empty2 = thm "constrains_empty2";
+val constrains_UNIV = thm "constrains_UNIV";
+val constrains_UNIV2 = thm "constrains_UNIV2";
+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_Un_distrib = thm "constrains_Un_distrib";
+val constrains_UN_distrib = thm "constrains_UN_distrib";
+val constrains_Int_distrib = thm "constrains_Int_distrib";
+val constrains_INT_distrib = thm "constrains_INT_distrib";
+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 unlessI = thm "unlessI";
+val unlessD = thm "unlessD";
+val stableI = thm "stableI";
+val stableD = thm "stableD";
+val stable_UNIV = thm "stable_UNIV";
+val stable_Un = thm "stable_Un";
+val stable_UN = thm "stable_UN";
+val stable_Int = thm "stable_Int";
+val stable_INT = thm "stable_INT";
+val stable_constrains_Un = thm "stable_constrains_Un";
+val stable_constrains_Int = thm "stable_constrains_Int";
+val stable_constrains_stable = thm "stable_constrains_stable";
+val invariantI = thm "invariantI";
+val invariant_Int = thm "invariant_Int";
+val increasingD = thm "increasingD";
+val increasing_constant = thm "increasing_constant";
+val mono_increasing_o = thm "mono_increasing_o";
+val strict_increasingD = thm "strict_increasingD";
+val elimination = thm "elimination";
+val elimination_sing = thm "elimination_sing";
+val constrains_strongest_rhs = thm "constrains_strongest_rhs";
+val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
+val Un_Diff_Diff = thm "Un_Diff_Diff";
+val Int_Union_Union = thm "Int_Union_Union";
+val Image_less_than = thm "Image_less_than";
+val Image_inverse_less_than = thm "Image_inverse_less_than";
+
+(*WFair*)
+val stable_transient_empty = thm "stable_transient_empty";
+val transient_strengthen = thm "transient_strengthen";
+val transientI = thm "transientI";
+val transientE = thm "transientE";
+val transient_UNIV = thm "transient_UNIV";
+val transient_empty = thm "transient_empty";
+val ensuresI = thm "ensuresI";
+val ensuresD = thm "ensuresD";
+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 leadsTo_Basis = thm "leadsTo_Basis";
+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_induct = thm "leadsTo_induct";
+val subset_imp_ensures = thm "subset_imp_ensures";
+val subset_imp_leadsTo = thm "subset_imp_leadsTo";
+val leadsTo_refl = thm "leadsTo_refl";
+val empty_leadsTo = thm "empty_leadsTo";
+val leadsTo_UNIV = thm "leadsTo_UNIV";
+val leadsTo_induct_pre_lemma = thm "leadsTo_induct_pre_lemma";
+val leadsTo_induct_pre = thm "leadsTo_induct_pre";
+val leadsTo_weaken_R = thm "leadsTo_weaken_R";
+val leadsTo_weaken_L = thm "leadsTo_weaken_L";
+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_weaken = thm "leadsTo_weaken";
+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_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_lemma = thm "leadsTo_wf_induct_lemma";
+val leadsTo_wf_induct = thm "leadsTo_wf_induct";
+val bounded_induct = thm "bounded_induct";
+val lessThan_induct = thm "lessThan_induct";
+val lessThan_bounded_induct = thm "lessThan_bounded_induct";
+val greaterThan_bounded_induct = thm "greaterThan_bounded_induct";
+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 lemma1 = thm "lemma1";
+val leadsTo_123 = thm "leadsTo_123";
+val wlt_constrains_wlt = thm "wlt_constrains_wlt";
+val completion_lemma = thm "completion_lemma";
+val completion = thm "completion";
+val finite_completion_lemma = thm "finite_completion_lemma";
+val finite_completion = thm "finite_completion";
+val stable_completion = thm "stable_completion";
+val finite_stable_completion = thm "finite_stable_completion";
+
+(*Constrains*)
+val Increasing_def = thm "Increasing_def";
+val reachable_Init = thm "reachable.Init";
+val reachable_Acts = thm "reachable.Acts";
+val reachable_equiv_traces = thm "reachable_equiv_traces";
+val Init_subset_reachable = thm "Init_subset_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_imp_Constrains = thm "constrains_imp_Constrains";
+val stable_imp_Stable = thm "stable_imp_Stable";
+val ConstrainsI = thm "ConstrainsI";
+val Constrains_empty = thm "Constrains_empty";
+val Constrains_UNIV = thm "Constrains_UNIV";
+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_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 IncreasingD = thm "IncreasingD";
+val mono_Increasing_o = thm "mono_Increasing_o";
+val strict_IncreasingD = thm "strict_IncreasingD";
+val increasing_imp_Increasing = thm "increasing_imp_Increasing";
+val Increasing_constant = thm "Increasing_constant";
+val Elimination = thm "Elimination";
+val Elimination_sing = thm "Elimination_sing";
+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_UNIV_eq = thm "Always_UNIV_eq";
+val UNIV_AlwaysI = thm "UNIV_AlwaysI";
+val Always_eq_UN_invariant = thm "Always_eq_UN_invariant";
+val Always_weaken = thm "Always_weaken";
+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_Compl_Un_eq = thm "Always_Compl_Un_eq";
+val Always_thin = thm "Always_thin";
+
(*FP*)
val stable_FP_Orig_Int = thm "stable_FP_Orig_Int";
val FP_Orig_weakest = thm "FP_Orig_weakest";
@@ -473,6 +682,18 @@
val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe";
+(*Lazy unfolding of actions or of sets*)
+fun simp_of_act def = def RS def_act_simp;
+
+fun simp_of_set def = def RS def_set_simp;
+
+
+(*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)
+
(*proves "co" properties when the program is specified*)
fun gen_constrains_tac(cs,ss) i =
SELECT_GOAL
@@ -504,6 +725,8 @@
ALLGOALS (clarify_tac cs),
ALLGOALS (asm_lr_simp_tac ss)]);
+fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
+
fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
--- a/src/HOL/UNITY/WFair.ML Thu Jan 30 10:35:56 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,560 +0,0 @@
-(* Title: HOL/UNITY/WFair
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Weak Fairness versions of transient, ensures, leadsTo.
-
-From Misra, "A Logic for Concurrent Programming", 1994
-*)
-
-
-(*** transient ***)
-
-Goalw [stable_def, constrains_def, transient_def]
- "[| F : stable A; F : transient A |] ==> A = {}";
-by (Blast_tac 1);
-qed "stable_transient_empty";
-
-Goalw [transient_def]
- "[| F : transient A; B<=A |] ==> F : transient B";
-by (Clarify_tac 1);
-by (blast_tac (claset() addSIs [rev_bexI]) 1);
-qed "transient_strengthen";
-
-Goalw [transient_def]
- "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A";
-by (Blast_tac 1);
-qed "transientI";
-
-val major::prems =
-Goalw [transient_def]
- "[| F : transient A; \
-\ !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |] \
-\ ==> P";
-by (rtac (major RS CollectD RS bexE) 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "transientE";
-
-Goalw [transient_def] "transient UNIV = {}";
-by (Blast_tac 1);
-qed "transient_UNIV";
-
-Goalw [transient_def] "transient {} = UNIV";
-by Auto_tac;
-qed "transient_empty";
-Addsimps [transient_UNIV, transient_empty];
-
-
-(*** ensures ***)
-
-Goalw [ensures_def]
- "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B";
-by (Blast_tac 1);
-qed "ensuresI";
-
-Goalw [ensures_def]
- "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)";
-by (Blast_tac 1);
-qed "ensuresD";
-
-Goalw [ensures_def]
- "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
-by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
-qed "ensures_weaken_R";
-
-(*The L-version (precondition strengthening) fails, but we have this*)
-Goalw [ensures_def]
- "[| F : stable C; F : A ensures B |] \
-\ ==> F : (C Int A) ensures (C Int B)";
-by (auto_tac (claset(),
- simpset() addsimps [ensures_def,
- Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym]));
-by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
-qed "stable_ensures_Int";
-
-Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B";
-by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
-by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
-qed "stable_transient_ensures";
-
-Goal "(A ensures B) = (A unless B) Int transient (A-B)";
-by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1);
-qed "ensures_eq";
-
-
-(*** leadsTo ***)
-
-Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
-by (blast_tac (claset() addIs [leads.Basis]) 1);
-qed "leadsTo_Basis";
-
-AddIs [leadsTo_Basis];
-
-Goalw [leadsTo_def]
- "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C";
-by (blast_tac (claset() addIs [leads.Trans]) 1);
-qed "leadsTo_Trans";
-
-Goal "F : transient A ==> F : A leadsTo (-A)";
-by (asm_simp_tac
- (simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
-qed "transient_imp_leadsTo";
-
-(*Useful with cancellation, disjunction*)
-Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
-by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
-qed "leadsTo_Un_duplicate";
-
-Goal "F : A leadsTo (A' Un C Un C) ==> F : 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 prems = Goalw [leadsTo_def]
- "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
-by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
-qed "leadsTo_Union";
-
-val prems = Goalw [leadsTo_def]
- "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B";
-by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
-by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
-qed "leadsTo_Union_Int";
-
-val prems = Goal
- "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B";
-by (stac (Union_image_eq RS sym) 1);
-by (blast_tac (claset() addIs leadsTo_Union::prems) 1);
-qed "leadsTo_UN";
-
-(*Binary union introduction rule*)
-Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C";
-by (stac Un_eq_Union 1);
-by (blast_tac (claset() addIs [leadsTo_Union]) 1);
-qed "leadsTo_Un";
-
-val prems =
-Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B";
-by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "single_leadsTo_I";
-
-
-(*The INDUCTION rule as we should have liked to state it*)
-val major::prems = Goalw [leadsTo_def]
- "[| F : za leadsTo zb; \
-\ !!A B. F : A ensures B ==> P A B; \
-\ !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \
-\ ==> P A C; \
-\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
-\ |] ==> P za zb";
-by (rtac (major RS CollectD RS leads.induct) 1);
-by (REPEAT (blast_tac (claset() addIs prems) 1));
-qed "leadsTo_induct";
-
-
-Goal "A<=B ==> F : A ensures B";
-by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
-by (Blast_tac 1);
-qed "subset_imp_ensures";
-
-bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
-
-bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo);
-
-bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
-Addsimps [empty_leadsTo];
-
-bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo);
-Addsimps [leadsTo_UNIV];
-
-
-
-(** Variant induction rule: on the preconditions for B **)
-
-(*Lemma is the weak version: can't see how to do it in one step*)
-val major::prems = Goal
- "[| F : za leadsTo zb; \
-\ P zb; \
-\ !!A B. [| F : A ensures B; P B |] ==> P A; \
-\ !!S. ALL A:S. P A ==> P (Union S) \
-\ |] ==> P za";
-(*by induction on this formula*)
-by (subgoal_tac "P zb --> P za" 1);
-(*now solve first subgoal: 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));
-val lemma = result();
-
-val major::prems = Goal
- "[| F : za leadsTo zb; \
-\ P zb; \
-\ !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A; \
-\ !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) \
-\ |] ==> P za";
-by (subgoal_tac "F : za leadsTo zb & P za" 1);
-by (etac conjunct2 1);
-by (rtac (major RS lemma) 1);
-by (blast_tac (claset() addIs [leadsTo_Union]@prems) 3);
-by (blast_tac (claset() addIs [leadsTo_Trans]@prems) 2);
-by (blast_tac (claset() addIs [leadsTo_refl]@prems) 1);
-qed "leadsTo_induct_pre";
-
-
-Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
-by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
-qed "leadsTo_weaken_R";
-
-Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
-by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
-qed_spec_mp "leadsTo_weaken_L";
-
-(*Distributes over binary unions*)
-Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)";
-by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
-qed "leadsTo_Un_distrib";
-
-Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)";
-by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
-qed "leadsTo_UN_distrib";
-
-Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)";
-by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
-qed "leadsTo_Union_distrib";
-
-
-Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'";
-by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
- leadsTo_Trans]) 1);
-qed "leadsTo_weaken";
-
-
-(*Set difference: maybe combine with leadsTo_weaken_L?*)
-Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C";
-by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
-qed "leadsTo_Diff";
-
-val prems = goal thy
- "(!! i. i:I ==> F : (A i) leadsTo (A' i)) \
-\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)";
-by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
-by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R]
- addIs prems) 1);
-qed "leadsTo_UN_UN";
-
-(*Binary union version*)
-Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
-\ ==> F : (A Un B) leadsTo (A' Un B')";
-by (blast_tac (claset() addIs [leadsTo_Un,
- leadsTo_weaken_R]) 1);
-qed "leadsTo_Un_Un";
-
-
-(** The cancellation law **)
-
-Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \
-\ ==> F : A leadsTo (A' Un B')";
-by (blast_tac (claset() addIs [leadsTo_Un_Un,
- subset_imp_leadsTo, leadsTo_Trans]) 1);
-qed "leadsTo_cancel2";
-
-Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \
-\ ==> F : A leadsTo (A' Un B')";
-by (rtac leadsTo_cancel2 1);
-by (assume_tac 2);
-by (ALLGOALS Asm_simp_tac);
-qed "leadsTo_cancel_Diff2";
-
-Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \
-\ ==> F : A leadsTo (B' Un A')";
-by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
-by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
-qed "leadsTo_cancel1";
-
-Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \
-\ ==> F : A leadsTo (B' Un A')";
-by (rtac leadsTo_cancel1 1);
-by (assume_tac 2);
-by (ALLGOALS Asm_simp_tac);
-qed "leadsTo_cancel_Diff1";
-
-
-
-(** The impossibility law **)
-
-Goal "F : A leadsTo {} ==> A={}";
-by (etac leadsTo_induct_pre 1);
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [ensures_def, constrains_def, transient_def])));
-by (Blast_tac 1);
-qed "leadsTo_empty";
-
-
-(** PSP: Progress-Safety-Progress **)
-
-(*Special case of PSP: Misra's "stable conjunction"*)
-Goalw [stable_def]
- "[| F : A leadsTo A'; F : stable B |] \
-\ ==> F : (A Int B) leadsTo (A' Int B)";
-by (etac leadsTo_induct 1);
-by (blast_tac (claset() addIs [leadsTo_Union_Int]) 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_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
-by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
-qed "psp_stable";
-
-Goal
- "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')";
-by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1);
-qed "psp_stable2";
-
-Goalw [ensures_def, constrains_def]
- "[| F : A ensures A'; F : B co B' |] \
-\ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))";
-by (Clarify_tac 1); (*speeds up the proof*)
-by (blast_tac (claset() addIs [transient_strengthen]) 1);
-qed "psp_ensures";
-
-Goal "[| F : A leadsTo A'; F : B co B' |] \
-\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))";
-by (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]) 1);
-qed "psp";
-
-Goal "[| F : A leadsTo A'; F : B co B' |] \
-\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
-qed "psp2";
-
-
-Goalw [unless_def]
- "[| F : A leadsTo A'; F : B unless B' |] \
-\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
-by (dtac psp 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
-qed "psp_unless";
-
-
-(*** Proving the induction rules ***)
-
-(** The most general rule: r is any wf relation; f is any variant function **)
-
-Goal "[| wf r; \
-\ ALL m. F : (A Int f-`{m}) leadsTo \
-\ ((A Int f-`(r^-1 `` {m})) Un B) |] \
-\ ==> F : (A Int f-`{m}) leadsTo B";
-by (eres_inst_tac [("a","m")] wf_induct 1);
-by (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B" 1);
-by (stac vimage_eq_UN 2);
-by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
-by (blast_tac (claset() addIs [leadsTo_UN]) 2);
-by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
-val lemma = result();
-
-
-(** Meta or object quantifier ? **)
-Goal "[| wf r; \
-\ ALL m. F : (A Int f-`{m}) leadsTo \
-\ ((A Int f-`(r^-1 `` {m})) Un B) |] \
-\ ==> F : A leadsTo B";
-by (res_inst_tac [("t", "A")] subst 1);
-by (rtac leadsTo_UN 2);
-by (etac lemma 2);
-by (REPEAT (assume_tac 2));
-by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*)
-qed "leadsTo_wf_induct";
-
-
-Goal "[| wf r; \
-\ ALL m:I. F : (A Int f-`{m}) leadsTo \
-\ ((A Int f-`(r^-1 `` {m})) Un B) |] \
-\ ==> F : A leadsTo ((A - (f-`I)) Un B)";
-by (etac leadsTo_wf_induct 1);
-by Safe_tac;
-by (case_tac "m:I" 1);
-by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
-qed "bounded_induct";
-
-
-(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
-val prems =
-Goal "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |] \
-\ ==> F : A leadsTo B";
-by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "lessThan_induct";
-
-Goal "!!l::nat. [| ALL m:(greaterThan l). \
-\ F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |] \
-\ ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)";
-by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl,
- Compl_greaterThan RS sym]) 1);
-by (rtac (wf_less_than RS bounded_induct) 1);
-by (Asm_simp_tac 1);
-qed "lessThan_bounded_induct";
-
-Goal "!!l::nat. [| ALL m:(lessThan l). \
-\ F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |] \
-\ ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)";
-by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
- (wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1);
-by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
-by (Clarify_tac 1);
-by (case_tac "m<l" 1);
-by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2);
-by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1);
-qed "greaterThan_bounded_induct";
-
-
-(*** wlt ****)
-
-(*Misra's property W3*)
-Goalw [wlt_def] "F : (wlt F B) leadsTo B";
-by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
-qed "wlt_leadsTo";
-
-Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B";
-by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
-qed "leadsTo_subset";
-
-(*Misra's property W2*)
-Goal "F : A leadsTo B = (A <= wlt F B)";
-by (blast_tac (claset() addSIs [leadsTo_subset,
- wlt_leadsTo RS leadsTo_weaken_L]) 1);
-qed "leadsTo_eq_subset_wlt";
-
-(*Misra's property W4*)
-Goal "B <= wlt F B";
-by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
- subset_imp_leadsTo]) 1);
-qed "wlt_increasing";
-
-
-(*Used in the Trans case below*)
-Goalw [constrains_def]
- "[| B <= A2; \
-\ F : (A1 - B) co (A1 Un B); \
-\ F : (A2 - C) co (A2 Un C) |] \
-\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)";
-by (Clarify_tac 1);
-by (Blast_tac 1);
-val lemma1 = result();
-
-
-(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-Goal "F : A leadsTo A' \
-\ ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')";
-by (etac leadsTo_induct 1);
-(*Basis*)
-by (blast_tac (claset() addDs [ensuresD]) 1);
-(*Trans*)
-by (Clarify_tac 1);
-by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
-by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
- leadsTo_Un_duplicate]) 1);
-(*Union*)
-by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);;
-by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
-by (auto_tac (claset() addIs [leadsTo_UN], simpset()));
-(*Blast_tac says PROOF FAILED*)
-by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1);
-qed "leadsTo_123";
-
-
-(*Misra's property W5*)
-Goal "F : (wlt F B - B) co (wlt F B)";
-by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 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, Un_absorb2]) 1);
-qed "wlt_constrains_wlt";
-
-
-(*** Completion: Binary and General Finite versions ***)
-
-Goal "[| W = wlt F (B' Un C); \
-\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \
-\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \
-\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)";
-by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
-by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt]
- MRS constrains_Un RS constrains_weaken]) 2);
-by (subgoal_tac "F : (W-C) co W" 1);
-by (asm_full_simp_tac
- (simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
-by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
-by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
-(** LEVEL 6 **)
-by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
-by (rtac leadsTo_Un_duplicate2 2);
-by (blast_tac (claset() addIs [leadsTo_Un_Un,
- wlt_leadsTo RS psp2 RS leadsTo_weaken,
- leadsTo_refl]) 2);
-by (dtac leadsTo_Diff 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 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);
-bind_thm("completion", refl RS result());
-
-
-Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> \
-\ (ALL i:I. F : (A' i) co (A' i Un C)) --> \
-\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
-by (etac finite_induct 1);
-by Auto_tac;
-by (rtac completion 1);
-by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4);
-by (rtac constrains_INT 4);
-by Auto_tac;
-val lemma = result();
-
-val prems = Goal
- "[| finite I; \
-\ !!i. i:I ==> F : (A i) leadsTo (A' i Un C); \
-\ !!i. i:I ==> F : (A' i) co (A' i Un C) |] \
-\ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)";
-by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
-qed "finite_completion";
-
-Goalw [stable_def]
- "[| F : A leadsTo A'; F : stable A'; \
-\ F : B leadsTo B'; F : stable B' |] \
-\ ==> F : (A Int B) leadsTo (A' Int B')";
-by (res_inst_tac [("C1", "{}")] (completion RS leadsTo_weaken_R) 1);
-by (REPEAT (Force_tac 1));
-qed "stable_completion";
-
-val prems = Goalw [stable_def]
- "[| finite I; \
-\ !!i. i:I ==> F : (A i) leadsTo (A' i); \
-\ !!i. i:I ==> F : stable (A' i) |] \
-\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)";
-by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (blast_tac (claset() addIs prems)));
-qed "finite_stable_completion";
-
-
--- a/src/HOL/UNITY/WFair.thy Thu Jan 30 10:35:56 2003 +0100
+++ b/src/HOL/UNITY/WFair.thy Thu Jan 30 18:08:09 2003 +0100
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-WFair = UNITY +
+theory WFair = UNITY:
constdefs
@@ -17,7 +17,7 @@
transient :: "'a set => 'a program set"
"transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
- ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
+ ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60)
"A ensures B == (A-B co A Un B) Int transient (A-B)"
@@ -28,19 +28,19 @@
inductive "leads F"
- intrs
+ intros
- Basis "F : A ensures B ==> (A,B) : leads F"
+ Basis: "F : A ensures B ==> (A,B) : leads F"
- Trans "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F"
+ Trans: "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F"
- Union "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
+ Union: "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
constdefs
(*visible version of the LEADS-TO relation*)
- leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
+ leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60)
"A leadsTo B == {F. (A,B) : leads F}"
(*wlt F B is the largest set that leads to B*)
@@ -48,6 +48,537 @@
"wlt F B == Union {A. F: A leadsTo B}"
syntax (xsymbols)
- "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\\<longmapsto>" 60)
+ "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
+
+
+(*** transient ***)
+
+lemma stable_transient_empty:
+ "[| F : stable A; F : transient A |] ==> A = {}"
+
+by (unfold stable_def constrains_def transient_def, blast)
+
+lemma transient_strengthen:
+ "[| F : transient A; B<=A |] ==> F : transient B"
+apply (unfold transient_def, clarify)
+apply (blast intro!: rev_bexI)
+done
+
+lemma transientI:
+ "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A"
+by (unfold transient_def, blast)
+
+lemma transientE:
+ "[| F : transient A;
+ !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |]
+ ==> P"
+by (unfold transient_def, blast)
+
+lemma transient_UNIV [simp]: "transient UNIV = {}"
+by (unfold transient_def, blast)
+
+lemma transient_empty [simp]: "transient {} = UNIV"
+by (unfold transient_def, auto)
+
+
+(*** ensures ***)
+
+lemma ensuresI:
+ "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
+by (unfold ensures_def, blast)
+
+lemma ensuresD:
+ "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
+by (unfold ensures_def, blast)
+
+lemma ensures_weaken_R:
+ "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
+apply (unfold ensures_def)
+apply (blast intro: constrains_weaken transient_strengthen)
+done
+
+(*The L-version (precondition strengthening) fails, but we have this*)
+lemma stable_ensures_Int:
+ "[| F : stable C; F : A ensures B |]
+ ==> F : (C Int A) ensures (C Int B)"
+apply (unfold ensures_def)
+apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
+prefer 2 apply (blast intro: transient_strengthen)
+apply (blast intro: stable_constrains_Int constrains_weaken)
+done
+
+lemma stable_transient_ensures:
+ "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"
+apply (simp add: ensures_def stable_def)
+apply (blast intro: constrains_weaken transient_strengthen)
+done
+
+lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
+by (simp (no_asm) add: ensures_def unless_def)
+
+
+(*** leadsTo ***)
+
+lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
+apply (unfold leadsTo_def)
+apply (blast intro: leads.Basis)
+done
+
+lemma leadsTo_Trans:
+ "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C"
+apply (unfold leadsTo_def)
+apply (blast intro: leads.Trans)
+done
+
+lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"
+by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
+
+(*Useful with cancellation, disjunction*)
+lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"
+by (simp add: Un_ac)
+
+lemma leadsTo_Un_duplicate2:
+ "F : A leadsTo (A' Un C Un C) ==> F : 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 : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
+apply (unfold leadsTo_def)
+apply (blast intro: leads.Union)
+done
+
+lemma leadsTo_Union_Int:
+ "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
+apply (unfold leadsTo_def)
+apply (simp only: Int_Union_Union)
+apply (blast intro: leads.Union)
+done
+
+lemma leadsTo_UN:
+ "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
+apply (subst Union_image_eq [symmetric])
+apply (blast intro: leadsTo_Union)
+done
+
+(*Binary union introduction rule*)
+lemma leadsTo_Un:
+ "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
+apply (subst Un_eq_Union)
+apply (blast intro: leadsTo_Union)
+done
+
+lemma single_leadsTo_I:
+ "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
+by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
+
+
+(*The INDUCTION rule as we should have liked to state it*)
+lemma leadsTo_induct:
+ "[| F : za leadsTo zb;
+ !!A B. F : A ensures B ==> P A B;
+ !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]
+ ==> P A C;
+ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B
+ |] ==> P za zb"
+apply (unfold leadsTo_def)
+apply (drule CollectD, erule leads.induct)
+apply (blast+)
+done
+
+
+lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
+by (unfold ensures_def constrains_def transient_def, blast)
+
+lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
+
+lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
+
+lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
+
+lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
+
+
+
+(** 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_lemma:
+ "[| F : za leadsTo zb;
+ P zb;
+ !!A B. [| F : A ensures B; P B |] ==> P A;
+ !!S. ALL A:S. P A ==> P (Union S)
+ |] ==> P za"
+(*by induction on this formula*)
+apply (subgoal_tac "P zb --> P za")
+(*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 : za leadsTo zb;
+ P zb;
+ !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A;
+ !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)
+ |] ==> P za"
+apply (subgoal_tac "F : za leadsTo zb & P za")
+apply (erule conjunct2)
+apply (erule leadsTo_induct_pre_lemma)
+prefer 3 apply (blast intro: leadsTo_Union)
+prefer 2 apply (blast intro: leadsTo_Trans)
+apply (blast intro: leadsTo_refl)
+done
+
+
+lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
+by (blast intro: subset_imp_leadsTo leadsTo_Trans)
+
+lemma leadsTo_weaken_L [rule_format (no_asm)]:
+ "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
+by (blast intro: leadsTo_Trans subset_imp_leadsTo)
+
+(*Distributes over binary unions*)
+lemma leadsTo_Un_distrib:
+ "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"
+by (blast intro: leadsTo_Un leadsTo_weaken_L)
+
+lemma leadsTo_UN_distrib:
+ "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"
+by (blast intro: leadsTo_UN leadsTo_weaken_L)
+
+lemma leadsTo_Union_distrib:
+ "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"
+by (blast intro: leadsTo_Union leadsTo_weaken_L)
+
+
+lemma leadsTo_weaken:
+ "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"
+by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
+
+
+(*Set difference: maybe combine with leadsTo_weaken_L?*)
+lemma leadsTo_Diff:
+ "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C"
+by (blast intro: leadsTo_Un leadsTo_weaken)
+
+lemma leadsTo_UN_UN:
+ "(!! i. i:I ==> F : (A i) leadsTo (A' i))
+ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
+apply (simp only: Union_image_eq [symmetric])
+apply (blast intro: leadsTo_Union leadsTo_weaken_R)
+done
+
+(*Binary union version*)
+lemma leadsTo_Un_Un:
+ "[| F : A leadsTo A'; F : 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 : A leadsTo (A' Un B); F : B leadsTo B' |]
+ ==> F : A leadsTo (A' Un B')"
+by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
+
+lemma leadsTo_cancel_Diff2:
+ "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]
+ ==> F : A leadsTo (A' Un B')"
+apply (rule leadsTo_cancel2)
+prefer 2 apply assumption
+apply (simp_all (no_asm_simp))
+done
+
+lemma leadsTo_cancel1:
+ "[| F : A leadsTo (B Un A'); F : B leadsTo B' |]
+ ==> F : A leadsTo (B' Un A')"
+apply (simp add: Un_commute)
+apply (blast intro!: leadsTo_cancel2)
+done
+
+lemma leadsTo_cancel_Diff1:
+ "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]
+ ==> F : A leadsTo (B' Un A')"
+apply (rule leadsTo_cancel1)
+prefer 2 apply assumption
+apply (simp_all (no_asm_simp))
+done
+
+
+
+(** The impossibility law **)
+
+lemma leadsTo_empty: "F : A leadsTo {} ==> A={}"
+apply (erule leadsTo_induct_pre)
+apply (simp_all add: ensures_def constrains_def transient_def, blast)
+done
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction"*)
+lemma psp_stable:
+ "[| F : A leadsTo A'; F : stable B |]
+ ==> F : (A Int B) leadsTo (A' Int B)"
+apply (unfold stable_def)
+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 (blast intro: transient_strengthen constrains_Int)
+done
+
+lemma psp_stable2:
+ "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"
+by (simp add: psp_stable Int_ac)
+
+lemma psp_ensures:
+ "[| F : A ensures A'; F : B co B' |]
+ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
+apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
+apply (blast intro: transient_strengthen)
+done
+
+lemma psp:
+ "[| F : A leadsTo A'; F : B co B' |]
+ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
+apply (erule leadsTo_induct)
+ prefer 3 apply (blast intro: leadsTo_Union_Int)
+ txt{*Basis case*}
+ apply (blast intro: psp_ensures)
+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 : A leadsTo A'; F : 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 : A leadsTo A'; F : 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_weaken)
+done
+
+
+(*** Proving the induction rules ***)
+
+(** The most general rule: r is any wf relation; f is any variant function **)
+
+lemma leadsTo_wf_induct_lemma:
+ "[| wf r;
+ ALL m. F : (A Int f-`{m}) leadsTo
+ ((A Int f-`(r^-1 `` {m})) Un B) |]
+ ==> F : (A Int f-`{m}) leadsTo B"
+apply (erule_tac a = m in wf_induct)
+apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
+ apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
+apply (subst vimage_eq_UN)
+apply (simp only: UN_simps [symmetric])
+apply (blast intro: leadsTo_UN)
+done
+
+
+(** Meta or object quantifier ? **)
+lemma leadsTo_wf_induct:
+ "[| wf r;
+ ALL m. F : (A Int f-`{m}) leadsTo
+ ((A Int f-`(r^-1 `` {m})) Un B) |]
+ ==> F : A leadsTo B"
+apply (rule_tac t = A in subst)
+ defer 1
+ apply (rule leadsTo_UN)
+ apply (erule leadsTo_wf_induct_lemma)
+ apply assumption
+apply fast (*Blast_tac: Function unknown's argument not a parameter*)
+done
+
+
+lemma bounded_induct:
+ "[| wf r;
+ ALL m:I. F : (A Int f-`{m}) leadsTo
+ ((A Int f-`(r^-1 `` {m})) Un B) |]
+ ==> F : A leadsTo ((A - (f-`I)) Un B)"
+apply (erule leadsTo_wf_induct, safe)
+apply (case_tac "m:I")
+apply (blast intro: leadsTo_weaken)
+apply (blast intro: subset_imp_leadsTo)
+done
+
+
+(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
+lemma lessThan_induct:
+ "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]
+ ==> F : A leadsTo B"
+apply (rule wf_less_than [THEN leadsTo_wf_induct])
+apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma lessThan_bounded_induct:
+ "!!l::nat. [| ALL m:(greaterThan l).
+ F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]
+ ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
+apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
+apply (rule wf_less_than [THEN bounded_induct])
+apply (simp (no_asm_simp))
+done
+
+lemma greaterThan_bounded_induct:
+ "!!l::nat. [| ALL m:(lessThan l).
+ F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]
+ ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
+apply (rule_tac f = f and f1 = "%k. l - k"
+ in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
+apply (simp (no_asm) add: inv_image_def Image_singleton)
+apply clarify
+apply (case_tac "m<l")
+prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
+apply (blast intro: leadsTo_weaken_R diff_less_mono2)
+done
+
+
+(*** wlt ****)
+
+(*Misra's property W3*)
+lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
+apply (unfold wlt_def)
+apply (blast intro!: leadsTo_Union)
+done
+
+lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
+apply (unfold wlt_def)
+apply (blast intro!: leadsTo_Union)
+done
+
+(*Misra's property W2*)
+lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"
+by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
+
+(*Misra's property W4*)
+lemma wlt_increasing: "B <= wlt F B"
+apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
+done
+
+
+(*Used in the Trans case below*)
+lemma lemma1:
+ "[| B <= A2;
+ F : (A1 - B) co (A1 Un B);
+ F : (A2 - C) co (A2 Un C) |]
+ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
+by (unfold constrains_def, clarify, blast)
+
+(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+lemma leadsTo_123:
+ "F : A leadsTo A'
+ ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
+apply (erule leadsTo_induct)
+(*Basis*)
+apply (blast dest: ensuresD)
+(*Trans*)
+apply clarify
+apply (rule_tac x = "Ba Un Bb" in exI)
+apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
+(*Union*)
+apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
+apply (rule_tac x = "UN A:S. f A" in exI)
+apply (auto intro: leadsTo_UN)
+(*Blast_tac says PROOF FAILED*)
+apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B"
+ in constrains_UN [THEN constrains_weaken])
+apply (auto );
+done
+
+
+(*Misra's property W5*)
+lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
+apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], 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 Un_absorb2)
+done
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+lemma completion_lemma :
+ "[| W = wlt F (B' Un C);
+ F : A leadsTo (A' Un C); F : A' co (A' Un C);
+ F : B leadsTo (B' Un C); F : B' co (B' Un C) |]
+ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"
+apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
+ prefer 2
+ apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un,
+ THEN constrains_weaken])
+apply (subgoal_tac "F : (W-C) co W")
+ prefer 2
+ apply (simp add: wlt_increasing Un_assoc Un_absorb2)
+apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
+ prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
+(** LEVEL 6 **)
+apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
+ prefer 2
+ apply (rule leadsTo_Un_duplicate2)
+ apply (blast intro: leadsTo_Un_Un wlt_leadsTo
+ [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
+apply (drule leadsTo_Diff)
+apply (blast intro: subset_imp_leadsTo)
+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)
+done
+
+lemmas completion = completion_lemma [OF refl]
+
+lemma finite_completion_lemma:
+ "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->
+ (ALL i:I. F : (A' i) co (A' i Un C)) -->
+ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+apply (erule finite_induct, auto)
+apply (rule completion)
+ prefer 4
+ apply (simp only: INT_simps [symmetric])
+ apply (rule constrains_INT, auto)
+done
+
+lemma finite_completion:
+ "[| finite I;
+ !!i. i:I ==> F : (A i) leadsTo (A' i Un C);
+ !!i. i:I ==> F : (A' i) co (A' i Un C) |]
+ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
+
+lemma stable_completion:
+ "[| F : A leadsTo A'; F : stable A';
+ F : B leadsTo B'; F : stable B' |]
+ ==> F : (A Int B) leadsTo (A' Int B')"
+apply (unfold stable_def)
+apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
+apply (force+)
+done
+
+lemma finite_stable_completion:
+ "[| finite I;
+ !!i. i:I ==> F : (A i) leadsTo (A' i);
+ !!i. i:I ==> F : stable (A' i) |]
+ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
+apply (unfold stable_def)
+apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
+apply (simp_all (no_asm_simp))
+apply blast+
+done
end