--- a/src/HOL/IsaMakefile Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/IsaMakefile Thu Jan 30 10:35:56 2003 +0100
@@ -383,11 +383,11 @@
$(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/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
+ 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.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
+ UNITY/SubstAx.thy UNITY/UNITY.ML \
UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \
UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
--- a/src/HOL/UNITY/Comp/Priority.ML Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/Comp/Priority.ML Thu Jan 30 10:35:56 2003 +0100
@@ -12,7 +12,6 @@
*)
Addsimps [Component_def RS def_prg_Init];
-program_defs_ref := [Component_def, system_def];
Addsimps [highest_def, lowest_def];
Addsimps [simp_of_act act_def];
Addsimps (map simp_of_set [Highest_def, Lowest_def]);
@@ -24,13 +23,14 @@
(* neighbors is stable *)
Goal "Component i: stable {s. neighbors k s = n}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "Component_neighbors_stable";
(* property 4 *)
-Goal
-"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
+Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "Component_waits_priority";
@@ -39,24 +39,28 @@
Goal
"Component i: {s. neighbors i s ~= {}} Int Highest i \
\ ensures - Highest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (ensures_tac "act i" 1);
by (REPEAT(Fast_tac 1));
qed "Component_yields_priority";
(* or better *)
Goal "Component i: Highest i ensures Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (ensures_tac "act i" 1);
by (REPEAT(Fast_tac 1));
qed "Component_yields_priority'";
(* property 6: Component doesn't introduce cycle *)
Goal "Component i: Highest i co Highest i Un Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
by (Fast_tac 1);
qed "Component_well_behaves";
(* property 7: local axiom *)
Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
+by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1);
by (constrains_tac 1);
qed "locality";
@@ -64,16 +68,16 @@
(**** System properties ****)
(* property 8: strictly universal *)
-Goalw [Safety_def]
- "system: stable Safety";
+Goalw [Safety_def] "system: stable Safety";
by (rtac stable_INT 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
by (constrains_tac 1);
by (Fast_tac 1);
qed "Safety";
(* property 13: universal *)
-Goal
-"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
+Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by (Blast_tac 1);
qed "p13";
@@ -84,6 +88,7 @@
"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
by (Clarify_tac 1);
by (cut_inst_tac [("i", "j")] reach_lemma 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
qed "above_not_increase";
@@ -101,6 +106,7 @@
(* p15: universal property: all Components well behave *)
Goal "ALL i. system: Highest i co Highest i Un Lowest i";
by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def]) 1);
by (constrains_tac 1);
by Auto_tac;
qed "system_well_behaves";
@@ -141,6 +147,7 @@
(* propert 5: existential property *)
Goal "system: Highest i leadsTo Lowest i";
+by (asm_full_simp_tac (simpset() addsimps [system_def]) 1);
by (ensures_tac "act i" 1);
by (auto_tac (claset(), simpset() addsimps [Component_def]));
qed "Highest_leadsTo_Lowest";
--- a/src/HOL/UNITY/Comp/Priority.thy Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jan 30 10:35:56 2003 +0100
@@ -11,7 +11,7 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
-Priority = PriorityAux + Comp + SubstAx +
+Priority = PriorityAux +
types state = "(vertex*vertex)set"
types command = "vertex=>(state*state)set"
--- a/src/HOL/UNITY/Comp/PriorityAux.thy Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Thu Jan 30 10:35:56 2003 +0100
@@ -6,7 +6,7 @@
Auxiliary definitions needed in Priority.thy
*)
-PriorityAux = Main +
+PriorityAux = UNITY_Main +
types vertex
arities vertex :: type
--- a/src/HOL/UNITY/FP.ML Wed Jan 29 17:35:11 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: HOL/UNITY/FP
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Fixed Point of a Program
-
-From Misra, "A Logic for Concurrent Programming", 1994
-*)
-
-Goalw [FP_Orig_def, stable_def] "F : stable (FP_Orig F Int B)";
-by (stac Int_Union2 1);
-by (blast_tac (claset() addIs [constrains_UN]) 1);
-qed "stable_FP_Orig_Int";
-
-
-val prems = goalw thy [FP_Orig_def, stable_def]
- "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F";
-by (blast_tac (claset() addIs prems) 1);
-qed "FP_Orig_weakest";
-
-
-Goal "F : stable (FP F Int B)";
-by (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x})" 1);
-by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
-by (rewrite_goals_tac [FP_def, stable_def]);
-by (rtac constrains_UN 1);
-by (Simp_tac 1);
-qed "stable_FP_Int";
-
-Goal "FP F <= FP_Orig F";
-by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
-val lemma1 = result();
-
-Goalw [FP_Orig_def, FP_def] "FP_Orig F <= FP F";
-by (Clarify_tac 1);
-by (dres_inst_tac [("x", "{x}")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
-val lemma2 = result();
-
-Goal "FP F = FP_Orig F";
-by (rtac ([lemma1,lemma2] MRS equalityI) 1);
-qed "FP_equivalence";
-
-val [prem] = goal thy
- "(!!B. F : stable (A Int B)) ==> A <= FP F";
-by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
-qed "FP_weakest";
-
-Goalw [FP_def, stable_def, constrains_def]
- "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})";
-by (Blast_tac 1);
-qed "Compl_FP";
-
-Goal "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})";
-by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
-qed "Diff_FP";
-
--- a/src/HOL/UNITY/FP.thy Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/FP.thy Thu Jan 30 10:35:56 2003 +0100
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-FP = UNITY +
+theory FP = UNITY:
constdefs
@@ -18,4 +18,42 @@
FP :: "'a program => 'a set"
"FP F == {s. F : stable {s}}"
+lemma stable_FP_Orig_Int: "F : stable (FP_Orig F Int B)"
+apply (unfold FP_Orig_def stable_def)
+apply (subst Int_Union2)
+apply (blast intro: constrains_UN)
+done
+
+lemma FP_Orig_weakest:
+ "(!!B. F : stable (A Int B)) ==> A <= FP_Orig F"
+by (unfold FP_Orig_def stable_def, blast)
+
+lemma stable_FP_Int: "F : stable (FP F Int B)"
+apply (subgoal_tac "FP F Int B = (UN x:B. FP F Int {x}) ")
+prefer 2 apply blast
+apply (simp (no_asm_simp) add: Int_insert_right)
+apply (unfold FP_def stable_def)
+apply (rule constrains_UN)
+apply (simp (no_asm))
+done
+
+lemma FP_equivalence: "FP F = FP_Orig F"
+apply (rule equalityI)
+ apply (rule stable_FP_Int [THEN FP_Orig_weakest])
+apply (unfold FP_Orig_def FP_def, clarify)
+apply (drule_tac x = "{x}" in spec)
+apply (simp add: Int_insert_right)
+done
+
+lemma FP_weakest:
+ "(!!B. F : stable (A Int B)) ==> A <= FP F"
+by (simp add: FP_equivalence FP_Orig_weakest)
+
+lemma Compl_FP:
+ "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})"
+by (simp add: FP_def stable_def constrains_def, blast)
+
+lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
+by (simp add: Diff_eq Compl_FP)
+
end
--- a/src/HOL/UNITY/Follows.ML Wed Jan 29 17:35:11 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(* Title: HOL/UNITY/Follows
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-The Follows relation of Charpentier and Sivilotte
-*)
-
-(*Does this hold for "invariant"?*)
-Goal "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}";
-by (asm_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset() addIs [monoD]) 1);
-qed "mono_Always_o";
-
-Goal "mono (h::'a::order => 'b::order) \
-\ ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <= \
-\ (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})";
-by Auto_tac;
-by (rtac single_LeadsTo_I 1);
-by (dres_inst_tac [("x", "g s")] spec 1);
-by (etac LeadsTo_weaken 1);
-by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
-qed "mono_LeadsTo_o";
-
-Goalw [Follows_def] "F : (%s. c) Fols (%s. c)";
-by Auto_tac;
-qed "Follows_constant";
-AddIffs [Follows_constant];
-
-Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
-by (Clarify_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [impOfSubs mono_Increasing_o,
- impOfSubs mono_Always_o,
- impOfSubs mono_LeadsTo_o RS INT_D]) 1);
-qed "mono_Follows_o";
-
-Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))";
-by (dtac mono_Follows_o 1);
-by (force_tac (claset(), simpset() addsimps [o_def]) 1);
-qed "mono_Follows_apply";
-
-Goalw [Follows_def]
- "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h";
-by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
-qed "Follows_trans";
-
-
-(** Destructiom rules **)
-
-Goalw [Follows_def]
- "F : f Fols g ==> F : Increasing f";
-by (Blast_tac 1);
-qed "Follows_Increasing1";
-
-Goalw [Follows_def]
- "F : f Fols g ==> F : Increasing g";
-by (Blast_tac 1);
-qed "Follows_Increasing2";
-
-Goalw [Follows_def]
- "F : f Fols g ==> F : Always {s. f s <= g s}";
-by (Blast_tac 1);
-qed "Follows_Bounded";
-
-Goalw [Follows_def]
- "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}";
-by (Blast_tac 1);
-qed "Follows_LeadsTo";
-
-Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}";
-by (rtac single_LeadsTo_I 1);
-by (Clarify_tac 1);
-by (dtac Follows_LeadsTo 1);
-by (etac LeadsTo_weaken 1);
-by (blast_tac set_cs 1);
-by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1);
-qed "Follows_LeadsTo_pfixLe";
-
-Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}";
-by (rtac single_LeadsTo_I 1);
-by (Clarify_tac 1);
-by (dtac Follows_LeadsTo 1);
-by (etac LeadsTo_weaken 1);
-by (blast_tac set_cs 1);
-by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1);
-qed "Follows_LeadsTo_pfixGe";
-
-
-Goalw [Follows_def, Increasing_def, Stable_def]
- "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g";
-by Auto_tac;
-by (etac Always_LeadsTo_weaken 3);
-by (eres_inst_tac [("A", "{s. z <= f s}"), ("A'", "{s. z <= f s}")]
- Always_Constrains_weaken 1);
-by Auto_tac;
-by (dtac Always_Int_I 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
-qed "Always_Follows1";
-
-Goalw [Follows_def, Increasing_def, Stable_def]
- "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'";
-by Auto_tac;
-by (etac Always_LeadsTo_weaken 3);
-by (eres_inst_tac [("A", "{s. z <= g s}"), ("A'", "{s. z <= g s}")]
- Always_Constrains_weaken 1);
-by Auto_tac;
-by (dtac Always_Int_I 1);
-by (assume_tac 1);
-by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
-qed "Always_Follows2";
-
-
-(** Union properties (with the subset ordering) **)
-
-(*Can replace "Un" by any sup. But existing max only works for linorders.*)
-Goalw [increasing_def, stable_def, constrains_def]
- "[| F : increasing f; F: increasing g |] \
-\ ==> F : increasing (%s. (f s) Un (g s))";
-by Auto_tac;
-by (dres_inst_tac [("x","f xa")] spec 1);
-by (dres_inst_tac [("x","g xa")] spec 1);
-by (blast_tac (claset() addSDs [bspec]) 1);
-qed "increasing_Un";
-
-Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
- "[| F : Increasing f; F: Increasing g |] \
-\ ==> F : Increasing (%s. (f s) Un (g s))";
-by Auto_tac;
-by (dres_inst_tac [("x","f xa")] spec 1);
-by (dres_inst_tac [("x","g xa")] spec 1);
-by (blast_tac (claset() addSDs [bspec]) 1);
-qed "Increasing_Un";
-
-
-Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
-\ ==> F : Always {s. f' s Un g' s <= f s Un g s}";
-by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (Blast_tac 1);
-qed "Always_Un";
-
-(*Lemma to re-use the argument that one variable increases (progress)
- while the other variable doesn't decrease (safety)*)
-Goal "[| F : Increasing f; F : Increasing g; \
-\ F : Increasing g'; F : Always {s. f' s <= f s};\
-\ ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
-\ ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}";
-by (rtac single_LeadsTo_I 1);
-by (dres_inst_tac [("x", "f s")] IncreasingD 1);
-by (dres_inst_tac [("x", "g s")] IncreasingD 1);
-by (rtac LeadsTo_weaken 1);
-by (rtac PSP_Stable 1);
-by (eres_inst_tac [("x", "f s")] spec 1);
-by (etac Stable_Int 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed "Follows_Un_lemma";
-
-Goalw [Follows_def]
- "[| F : f' Fols f; F: g' Fols g |] \
-\ ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))";
-by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
-by Auto_tac;
-by (rtac LeadsTo_Trans 1);
-by (blast_tac (claset() addIs [Follows_Un_lemma]) 1);
-(*Weakening is used to exchange Un's arguments*)
-by (blast_tac (claset() addIs [Follows_Un_lemma RS LeadsTo_weaken]) 1);
-qed "Follows_Un";
-
-
-(** Multiset union properties (with the multiset ordering) **)
-
-Goalw [increasing_def, stable_def, constrains_def]
- "[| F : increasing f; F: increasing g |] \
-\ ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))";
-by Auto_tac;
-by (dres_inst_tac [("x","f xa")] spec 1);
-by (dres_inst_tac [("x","g xa")] spec 1);
-by (ball_tac 1);
-by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
-qed "increasing_union";
-
-Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
- "[| F : Increasing f; F: Increasing g |] \
-\ ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))";
-by Auto_tac;
-by (dres_inst_tac [("x","f xa")] spec 1);
-by (dres_inst_tac [("x","g xa")] spec 1);
-by (ball_tac 1);
-by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
-qed "Increasing_union";
-
-Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
-\ ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
-by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset() addIs [thm "union_le_mono"]) 1);
-qed "Always_union";
-
-(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
-Goal "[| F : Increasing f; F : Increasing g; \
-\ F : Increasing g'; F : Always {s. f' s <= f s};\
-\ ALL k::('a::order) multiset. \
-\ F : {s. k <= f s} LeadsTo {s. k <= f' s} |]\
-\ ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}";
-by (rtac single_LeadsTo_I 1);
-by (dres_inst_tac [("x", "f s")] IncreasingD 1);
-by (dres_inst_tac [("x", "g s")] IncreasingD 1);
-by (rtac LeadsTo_weaken 1);
-by (rtac PSP_Stable 1);
-by (eres_inst_tac [("x", "f s")] spec 1);
-by (etac Stable_Int 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
-qed "Follows_union_lemma";
-
-(*The !! is there to influence to effect of permutative rewriting at the end*)
-Goalw [Follows_def]
- "!!g g' ::'b => ('a::order) multiset. \
-\ [| F : f' Fols f; F: g' Fols g |] \
-\ ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))";
-by (asm_full_simp_tac (simpset() addsimps [Increasing_union, Always_union]) 1);
-by Auto_tac;
-by (rtac LeadsTo_Trans 1);
-by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
-(*now exchange union's arguments*)
-by (simp_tac (simpset() addsimps [thm "union_commute"]) 1);
-by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
-qed "Follows_union";
-
-Goal "!!f ::['c,'b] => ('a::order) multiset. \
-\ [| ALL i: I. F : f' i Fols f i; finite I |] \
-\ ==> F : (%s. \\<Sum>i:I. f' i s) Fols (%s. \\<Sum>i:I. f i s)";
-by (etac rev_mp 1);
-by (etac finite_induct 1);
-by (asm_simp_tac (simpset() addsimps [Follows_union]) 2);
-by (Simp_tac 1);
-qed "Follows_setsum";
-
-
-(*Currently UNUSED, but possibly of interest*)
-Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
-by (asm_full_simp_tac
- (simpset() addsimps [Increasing_def, Stable_def, Constrains_def,
- constrains_def]) 1);
-by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
- prefix_imp_pfixGe]) 1);
-qed "Increasing_imp_Stable_pfixGe";
-
-(*Currently UNUSED, but possibly of interest*)
-Goal "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} \
-\ ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}";
-by (rtac single_LeadsTo_I 1);
-by (dres_inst_tac [("x", "f s")] spec 1);
-by (etac LeadsTo_weaken 1);
-by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
- prefix_imp_pfixGe]) 2);
-by (Blast_tac 1);
-qed "LeadsTo_le_imp_pfixGe";
--- a/src/HOL/UNITY/Follows.thy Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/Follows.thy Thu Jan 30 10:35:56 2003 +0100
@@ -6,7 +6,7 @@
The "Follows" relation of Charpentier and Sivilotte
*)
-Follows = SubstAx + ListOrder + Multiset +
+theory Follows = SubstAx + ListOrder + Multiset:
constdefs
@@ -17,4 +17,259 @@
(INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
+(*Does this hold for "invariant"?*)
+lemma mono_Always_o:
+ "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}"
+apply (simp add: Always_eq_includes_reachable)
+apply (blast intro: monoD)
+done
+
+lemma mono_LeadsTo_o:
+ "mono (h::'a::order => 'b::order)
+ ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <=
+ (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})"
+apply auto
+apply (rule single_LeadsTo_I)
+apply (drule_tac x = "g s" in spec)
+apply (erule LeadsTo_weaken)
+apply (blast intro: monoD order_trans)+
+done
+
+lemma Follows_constant: "F : (%s. c) Fols (%s. c)"
+by (unfold Follows_def, auto)
+declare Follows_constant [iff]
+
+lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)"
+apply (unfold Follows_def, clarify)
+apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD]
+ mono_Always_o [THEN [2] rev_subsetD]
+ mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
+done
+
+lemma mono_Follows_apply:
+ "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))"
+apply (drule mono_Follows_o)
+apply (force simp add: o_def)
+done
+
+lemma Follows_trans:
+ "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h"
+apply (unfold Follows_def)
+apply (simp add: Always_eq_includes_reachable)
+apply (blast intro: order_trans LeadsTo_Trans)
+done
+
+
+(** Destructiom rules **)
+
+lemma Follows_Increasing1:
+ "F : f Fols g ==> F : Increasing f"
+
+apply (unfold Follows_def, blast)
+done
+
+lemma Follows_Increasing2:
+ "F : f Fols g ==> F : Increasing g"
+apply (unfold Follows_def, blast)
+done
+
+lemma Follows_Bounded:
+ "F : f Fols g ==> F : Always {s. f s <= g s}"
+apply (unfold Follows_def, blast)
+done
+
+lemma Follows_LeadsTo:
+ "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"
+apply (unfold Follows_def, blast)
+done
+
+lemma Follows_LeadsTo_pfixLe:
+ "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
+apply (rule single_LeadsTo_I, clarify)
+apply (drule_tac k="g s" in Follows_LeadsTo)
+apply (erule LeadsTo_weaken)
+ apply blast
+apply (blast intro: pfixLe_trans prefix_imp_pfixLe)
+done
+
+lemma Follows_LeadsTo_pfixGe:
+ "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
+apply (rule single_LeadsTo_I, clarify)
+apply (drule_tac k="g s" in Follows_LeadsTo)
+apply (erule LeadsTo_weaken)
+ apply blast
+apply (blast intro: pfixGe_trans prefix_imp_pfixGe)
+done
+
+
+lemma Always_Follows1:
+ "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"
+
+apply (unfold Follows_def Increasing_def Stable_def, auto)
+apply (erule_tac [3] Always_LeadsTo_weaken)
+apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" in Always_Constrains_weaken, auto)
+apply (drule Always_Int_I, assumption)
+apply (force intro: Always_weaken)
+done
+
+lemma Always_Follows2:
+ "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"
+apply (unfold Follows_def Increasing_def Stable_def, auto)
+apply (erule_tac [3] Always_LeadsTo_weaken)
+apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}" in Always_Constrains_weaken, auto)
+apply (drule Always_Int_I, assumption)
+apply (force intro: Always_weaken)
+done
+
+
+(** Union properties (with the subset ordering) **)
+
+(*Can replace "Un" by any sup. But existing max only works for linorders.*)
+lemma increasing_Un:
+ "[| F : increasing f; F: increasing g |]
+ ==> F : increasing (%s. (f s) Un (g s))"
+apply (unfold increasing_def stable_def constrains_def, auto)
+apply (drule_tac x = "f xa" in spec)
+apply (drule_tac x = "g xa" in spec)
+apply (blast dest!: bspec)
+done
+
+lemma Increasing_Un:
+ "[| F : Increasing f; F: Increasing g |]
+ ==> F : Increasing (%s. (f s) Un (g s))"
+apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
+apply (drule_tac x = "f xa" in spec)
+apply (drule_tac x = "g xa" in spec)
+apply (blast dest!: bspec)
+done
+
+
+lemma Always_Un:
+ "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]
+ ==> F : Always {s. f' s Un g' s <= f s Un g s}"
+apply (simp add: Always_eq_includes_reachable, blast)
+done
+
+(*Lemma to re-use the argument that one variable increases (progress)
+ while the other variable doesn't decrease (safety)*)
+lemma Follows_Un_lemma:
+ "[| F : Increasing f; F : Increasing g;
+ F : Increasing g'; F : Always {s. f' s <= f s};
+ ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]
+ ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}"
+apply (rule single_LeadsTo_I)
+apply (drule_tac x = "f s" in IncreasingD)
+apply (drule_tac x = "g s" in IncreasingD)
+apply (rule LeadsTo_weaken)
+apply (rule PSP_Stable)
+apply (erule_tac x = "f s" in spec)
+apply (erule Stable_Int, assumption)
+apply blast
+apply blast
+done
+
+lemma Follows_Un:
+ "[| F : f' Fols f; F: g' Fols g |]
+ ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))"
+apply (unfold Follows_def)
+apply (simp add: Increasing_Un Always_Un, auto)
+apply (rule LeadsTo_Trans)
+apply (blast intro: Follows_Un_lemma)
+(*Weakening is used to exchange Un's arguments*)
+apply (blast intro: Follows_Un_lemma [THEN LeadsTo_weaken])
+done
+
+
+(** Multiset union properties (with the multiset ordering) **)
+
+lemma increasing_union:
+ "[| F : increasing f; F: increasing g |]
+ ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+
+apply (unfold increasing_def stable_def constrains_def, auto)
+apply (drule_tac x = "f xa" in spec)
+apply (drule_tac x = "g xa" in spec)
+apply (drule bspec, assumption)
+apply (blast intro: union_le_mono order_trans)
+done
+
+lemma Increasing_union:
+ "[| F : Increasing f; F: Increasing g |]
+ ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+apply (unfold Increasing_def Stable_def Constrains_def stable_def constrains_def, auto)
+apply (drule_tac x = "f xa" in spec)
+apply (drule_tac x = "g xa" in spec)
+apply (drule bspec, assumption)
+apply (blast intro: union_le_mono order_trans)
+done
+
+lemma Always_union:
+ "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]
+ ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}"
+apply (simp add: Always_eq_includes_reachable)
+apply (blast intro: union_le_mono)
+done
+
+(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
+lemma Follows_union_lemma:
+ "[| F : Increasing f; F : Increasing g;
+ F : Increasing g'; F : Always {s. f' s <= f s};
+ ALL k::('a::order) multiset.
+ F : {s. k <= f s} LeadsTo {s. k <= f' s} |]
+ ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}"
+apply (rule single_LeadsTo_I)
+apply (drule_tac x = "f s" in IncreasingD)
+apply (drule_tac x = "g s" in IncreasingD)
+apply (rule LeadsTo_weaken)
+apply (rule PSP_Stable)
+apply (erule_tac x = "f s" in spec)
+apply (erule Stable_Int, assumption)
+apply blast
+apply (blast intro: union_le_mono order_trans)
+done
+
+(*The !! is there to influence to effect of permutative rewriting at the end*)
+lemma Follows_union:
+ "!!g g' ::'b => ('a::order) multiset.
+ [| F : f' Fols f; F: g' Fols g |]
+ ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
+apply (unfold Follows_def)
+apply (simp add: Increasing_union Always_union, auto)
+apply (rule LeadsTo_Trans)
+apply (blast intro: Follows_union_lemma)
+(*now exchange union's arguments*)
+apply (simp add: union_commute)
+apply (blast intro: Follows_union_lemma)
+done
+
+lemma Follows_setsum:
+ "!!f ::['c,'b] => ('a::order) multiset.
+ [| ALL i: I. F : f' i Fols f i; finite I |]
+ ==> F : (%s. \<Sum>i:I. f' i s) Fols (%s. \<Sum>i:I. f i s)"
+apply (erule rev_mp)
+apply (erule finite_induct, simp)
+apply (simp add: Follows_union)
+done
+
+
+(*Currently UNUSED, but possibly of interest*)
+lemma Increasing_imp_Stable_pfixGe:
+ "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}"
+apply (simp add: Increasing_def Stable_def Constrains_def constrains_def)
+apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD]
+ prefix_imp_pfixGe)
+done
+
+(*Currently UNUSED, but possibly of interest*)
+lemma LeadsTo_le_imp_pfixGe:
+ "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s}
+ ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
+apply (rule single_LeadsTo_I)
+apply (drule_tac x = "f s" in spec)
+apply (erule LeadsTo_weaken)
+ prefer 2
+ apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD]
+ prefix_imp_pfixGe, blast)
+done
+
end
--- a/src/HOL/UNITY/SubstAx.ML Wed Jan 29 17:35:11 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,439 +0,0 @@
-(* Title: HOL/UNITY/SubstAx
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-LeadsTo relation, restricted to the set of reachable states.
-*)
-
-(*Resembles the previous definition of LeadsTo*)
-Goalw [LeadsTo_def]
- "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
-by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1);
-qed "LeadsTo_eq_leadsTo";
-
-
-(*** Specialized laws for handling invariants ***)
-
-(** Conjoining an Always property **)
-
-Goal "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')";
-by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
- Int_absorb2, Int_assoc RS sym]) 1);
-qed "Always_LeadsTo_pre";
-
-Goal "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')";
-by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable,
- Int_absorb2, Int_assoc RS sym]) 1);
-qed "Always_LeadsTo_post";
-
-(* [| F : Always C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
-bind_thm ("Always_LeadsToI", Always_LeadsTo_pre RS iffD1);
-
-(* [| F : Always INV; F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
-bind_thm ("Always_LeadsToD", Always_LeadsTo_post RS iffD2);
-
-
-(*** Introduction rules: Basis, Trans, Union ***)
-
-Goal "F : A leadsTo B ==> F : A LeadsTo B";
-by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
-qed "leadsTo_imp_LeadsTo";
-
-Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C";
-by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
-by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
-qed "LeadsTo_Trans";
-
-val prems = Goalw [LeadsTo_def]
- "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B";
-by (Simp_tac 1);
-by (stac Int_Union 1);
-by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
-qed "LeadsTo_Union";
-
-
-(*** Derived rules ***)
-
-Goal "F : A LeadsTo UNIV";
-by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-qed "LeadsTo_UNIV";
-Addsimps [LeadsTo_UNIV];
-
-(*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";
-
-val prems =
-Goal "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B";
-by (simp_tac (HOL_ss addsimps [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";
-
-(*Lets us look at the starting state*)
-val prems =
-Goal "(!!s. s : A ==> F : {s} 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";
-
-Goal "A <= B ==> F : A LeadsTo B";
-by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
-qed "subset_imp_LeadsTo";
-
-bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
-Addsimps [empty_LeadsTo];
-
-Goal "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
-qed_spec_mp "LeadsTo_weaken_R";
-
-Goal "[| F : A LeadsTo A'; B <= A |] \
-\ ==> F : B LeadsTo A'";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
-qed_spec_mp "LeadsTo_weaken_L";
-
-Goal "[| F : A LeadsTo A'; \
-\ B <= A; A' <= B' |] \
-\ ==> F : B LeadsTo B'";
-by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
- LeadsTo_Trans]) 1);
-qed "LeadsTo_weaken";
-
-Goal "[| F : Always C; F : A LeadsTo A'; \
-\ C Int B <= A; C Int A' <= B' |] \
-\ ==> F : B LeadsTo B'";
-by (blast_tac (claset() addDs [Always_LeadsToI] addIs[LeadsTo_weaken]
- addIs [Always_LeadsToD]) 1);
-qed "Always_LeadsTo_weaken";
-
-(** Two theorems for "proof lattices" **)
-
-Goal "F : A LeadsTo B ==> F : (A Un B) LeadsTo B";
-by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
-qed "LeadsTo_Un_post";
-
-Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \
-\ ==> F : (A Un B) LeadsTo C";
-by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
- LeadsTo_weaken_L, LeadsTo_Trans]) 1);
-qed "LeadsTo_Trans_Un";
-
-
-(** Distributive laws **)
-
-Goal "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
-qed "LeadsTo_Un_distrib";
-
-Goal "(F : (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";
-
-
-(** More rules using the premise "Always INV" **)
-
-Goal "F : A Ensures B ==> F : A LeadsTo B";
-by (asm_full_simp_tac
- (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
-qed "LeadsTo_Basis";
-
-Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \
-\ ==> F : A Ensures B";
-by (asm_full_simp_tac
- (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
-by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
- transient_strengthen]) 1);
-qed "EnsuresI";
-
-Goal "[| F : Always INV; \
-\ F : (INV Int (A-A')) Co (A Un A'); \
-\ F : transient (INV Int (A-A')) |] \
-\ ==> F : A LeadsTo A'";
-by (rtac Always_LeadsToI 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
- Always_ConstrainsD RS Constrains_weaken,
- transient_strengthen]) 1);
-qed "Always_LeadsTo_Basis";
-
-(*Set difference: maybe combine with leadsTo_weaken_L??
- This is the most useful form of the "disjunction" rule*)
-Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] \
-\ ==> F : A LeadsTo C";
-by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
-qed "LeadsTo_Diff";
-
-
-val prems =
-Goal "(!! 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";
-
-
-(*Version with no index set*)
-val prems =
-Goal "(!! i. F : (A i) LeadsTo (A' i)) \
-\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [LeadsTo_UN_UN]
- addIs prems) 1);
-qed "LeadsTo_UN_UN_noindex";
-
-(*Version with no index set*)
-Goal "ALL i. F : (A i) LeadsTo (A' i) \
-\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
-qed "all_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 **)
-
-(*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "F : A LeadsTo {} ==> F : Always (-A)";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def,
- Always_eq_includes_reachable]) 1);
-by (dtac leadsTo_empty 1);
-by Auto_tac;
-qed "LeadsTo_empty";
-
-
-(** PSP: Progress-Safety-Progress **)
-
-(*Special case of PSP: Misra's "stable conjunction"*)
-Goal "[| F : A LeadsTo A'; F : Stable B |] \
-\ ==> F : (A Int B) LeadsTo (A' Int B)";
-by (full_simp_tac
- (simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
-by (dtac psp_stable 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps Int_ac) 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";
-
-Goal "[| F : A LeadsTo A'; F : B Co B' |] \
-\ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))";
-by (full_simp_tac
- (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
-by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
-qed "PSP";
-
-Goal "[| F : A LeadsTo A'; F : B Co B' |] \
-\ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))";
-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_Diff, LeadsTo_weaken,
- subset_imp_LeadsTo]) 1);
-qed "PSP_Unless";
-
-
-Goal "[| F : Stable A; F : transient C; \
-\ F : Always (-A Un B Un C) |] ==> F : A LeadsTo B";
-by (etac Always_LeadsTo_weaken 1);
-by (rtac LeadsTo_Diff 1);
-by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_Stable2) 2);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
-qed "Stable_transient_Always_LeadsTo";
-
-
-(*** Induction rules ***)
-
-(** 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 (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
-by (etac leadsTo_wf_induct 1);
-by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
-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";
-
-
-val prems =
-Goal "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B)) \
-\ ==> F : A LeadsTo B";
-by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
-by (auto_tac (claset() addIs prems, simpset()));
-qed "LessThan_induct";
-
-(*Integer version. Could generalize from 0 to any lower bound*)
-val [reach, prem] =
-Goal "[| F : Always {s. (0::int) <= f s}; \
-\ !! z. F : (A Int {s. f s = z}) LeadsTo \
-\ ((A Int {s. f s < z}) Un B) |] \
-\ ==> F : A LeadsTo B";
-by (res_inst_tac [("f", "nat o f")] LessThan_induct 1);
-by (simp_tac (simpset() addsimps [vimage_def]) 1);
-by (rtac ([reach, prem] MRS Always_LeadsTo_weaken) 1);
-by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
-qed "integ_0_le_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";
-
-
-(*** Completion: Binary and General Finite versions ***)
-
-Goal "[| 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 (full_simp_tac
- (simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains,
- Int_Un_distrib]) 1);
-by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
-qed "Completion";
-
-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";
-
-
-(*proves "ensures/leadsTo" properties when the program is specified*)
-fun ensures_tac sact =
- SELECT_GOAL
- (EVERY [REPEAT (Always_Int_tac 1),
- etac Always_LeadsTo_Basis 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
- EnsuresI, ensuresI] 1),
- (*now there are two subgoals: co & transient*)
- simp_tac (simpset() addsimps !program_defs_ref) 2,
- res_inst_tac [("act", sact)] transientI 2,
- (*simplify the command's domain*)
- simp_tac (simpset() addsimps [Domain_def]) 3,
- constrains_tac 1,
- ALLGOALS Clarify_tac,
- ALLGOALS Asm_lr_simp_tac]);
--- a/src/HOL/UNITY/SubstAx.thy Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Thu Jan 30 10:35:56 2003 +0100
@@ -6,16 +6,416 @@
Weak LeadsTo relation (restricted to the set of reachable states)
*)
-SubstAx = WFair + Constrains +
+theory SubstAx = WFair + Constrains:
constdefs
- Ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
+ Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60)
"A Ensures B == {F. F : (reachable F Int A) ensures B}"
- 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. F : (reachable F Int A) leadsTo B}"
syntax (xsymbols)
- "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
+ "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
+
+
+(*Resembles the previous definition of LeadsTo*)
+lemma LeadsTo_eq_leadsTo:
+ "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
+apply (unfold LeadsTo_def)
+apply (blast dest: psp_stable2 intro: leadsTo_weaken)
+done
+
+
+(*** Specialized laws for handling invariants ***)
+
+(** Conjoining an Always property **)
+
+lemma Always_LeadsTo_pre:
+ "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
+by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+
+lemma Always_LeadsTo_post:
+ "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
+by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+
+(* [| F : Always C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
+lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
+
+(* [| F : Always INV; F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
+lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
+
+
+(*** Introduction rules: Basis, Trans, Union ***)
+
+lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
+apply (simp add: LeadsTo_def)
+apply (blast intro: leadsTo_weaken_L)
+done
+
+lemma LeadsTo_Trans:
+ "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"
+apply (simp add: LeadsTo_eq_leadsTo)
+apply (blast intro: leadsTo_Trans)
+done
+
+lemma LeadsTo_Union:
+ "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
+apply (simp add: LeadsTo_def)
+apply (subst Int_Union)
+apply (blast intro: leadsTo_UN)
+done
+
+
+(*** Derived rules ***)
+
+lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
+by (simp add: LeadsTo_def)
+
+(*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)
+
+lemma LeadsTo_UN:
+ "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
+apply (simp only: 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
+
+(*Lets us look at the starting state*)
+lemma single_LeadsTo_I:
+ "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
+by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
+
+lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
+apply (simp add: LeadsTo_def)
+apply (blast intro: subset_imp_leadsTo)
+done
+
+lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
+
+lemma LeadsTo_weaken_R [rule_format]:
+ "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'"
+apply (simp (no_asm_use) add: LeadsTo_def)
+apply (blast intro: leadsTo_weaken_R)
+done
+
+lemma LeadsTo_weaken_L [rule_format]:
+ "[| F : A LeadsTo A'; B <= A |]
+ ==> F : B LeadsTo A'"
+apply (simp (no_asm_use) add: LeadsTo_def)
+apply (blast intro: leadsTo_weaken_L)
+done
+
+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)
+
+lemma Always_LeadsTo_weaken:
+ "[| F : Always C; F : A LeadsTo A';
+ C Int B <= A; C Int A' <= B' |]
+ ==> F : B LeadsTo B'"
+by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
+
+(** Two theorems for "proof lattices" **)
+
+lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"
+by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
+
+lemma LeadsTo_Trans_Un:
+ "[| F : A LeadsTo B; F : B LeadsTo C |]
+ ==> F : (A Un B) LeadsTo C"
+by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
+
+
+(** Distributive laws **)
+
+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)
+
+
+(** More rules using the premise "Always INV" **)
+
+lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
+by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
+
+lemma EnsuresI:
+ "[| F : (A-B) Co (A Un B); F : transient (A-B) |]
+ ==> F : A Ensures B"
+apply (simp add: Ensures_def Constrains_eq_constrains)
+apply (blast intro: ensuresI constrains_weaken transient_strengthen)
+done
+
+lemma Always_LeadsTo_Basis:
+ "[| F : Always INV;
+ F : (INV Int (A-A')) Co (A Un A');
+ F : transient (INV Int (A-A')) |]
+ ==> F : A LeadsTo A'"
+apply (rule Always_LeadsToI, assumption)
+apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
+done
+
+(*Set difference: maybe combine with leadsTo_weaken_L??
+ This is the most useful form of the "disjunction" rule*)
+lemma LeadsTo_Diff:
+ "[| F : (A-B) LeadsTo C; F : (A Int 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
+
+
+(*Version with no index set*)
+lemma LeadsTo_UN_UN_noindex:
+ "(!! i. F : (A i) LeadsTo (A' i))
+ ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+by (blast intro: LeadsTo_UN_UN)
+
+(*Version with no index set*)
+lemma all_LeadsTo_UN_UN:
+ "ALL i. F : (A i) LeadsTo (A' i)
+ ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+by (blast intro: LeadsTo_UN_UN)
+
+(*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 **)
+
+(*The set "A" may be non-empty, but it contains no reachable states*)
+lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
+apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
+apply (drule leadsTo_empty, auto)
+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 (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable)
+apply (drule psp_stable, assumption)
+apply (simp add: Int_ac)
+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:
+ "[| F : A LeadsTo A'; F : B Co B' |]
+ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
+apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
+apply (blast dest: psp intro: leadsTo_weaken)
+done
+
+lemma PSP2:
+ "[| F : A LeadsTo A'; F : B Co B' |]
+ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
+by (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_Diff LeadsTo_weaken subset_imp_LeadsTo)
+done
+
+
+lemma Stable_transient_Always_LeadsTo:
+ "[| F : Stable A; F : transient C;
+ F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
+apply (erule Always_LeadsTo_weaken)
+apply (rule LeadsTo_Diff)
+ prefer 2
+ apply (erule
+ transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2])
+ apply (blast intro: subset_imp_LeadsTo)+
+done
+
+
+(*** Induction rules ***)
+
+(** 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 (simp (no_asm_use) add: LeadsTo_eq_leadsTo)
+apply (erule leadsTo_wf_induct)
+apply (blast intro: leadsTo_weaken)
+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
+
+
+lemma LessThan_induct:
+ "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))
+ ==> F : A LeadsTo B"
+apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
+done
+
+(*Integer version. Could generalize from 0 to any lower bound*)
+lemma integ_0_le_induct:
+ "[| F : Always {s. (0::int) <= f s};
+ !! z. F : (A Int {s. f s = z}) LeadsTo
+ ((A Int {s. f s < z}) Un B) |]
+ ==> F : A LeadsTo B"
+apply (rule_tac f = "nat o f" in LessThan_induct)
+apply (simp add: vimage_def)
+apply (rule Always_LeadsTo_weaken, assumption+)
+apply (auto simp add: nat_eq_iff nat_less_iff)
+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 add: inv_image_def Image_singleton, 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
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+lemma Completion:
+ "[| 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 (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
+apply (blast intro: completion leadsTo_weaken)
+done
+
+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
--- a/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 17:35:11 2003 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Jan 30 10:35:56 2003 +0100
@@ -6,6 +6,72 @@
Specialized UNITY tactics, and ML bindings of theorems
*)
+(*FP*)
+val stable_FP_Orig_Int = thm "stable_FP_Orig_Int";
+val FP_Orig_weakest = thm "FP_Orig_weakest";
+val stable_FP_Int = thm "stable_FP_Int";
+val FP_equivalence = thm "FP_equivalence";
+val FP_weakest = thm "FP_weakest";
+val Compl_FP = thm "Compl_FP";
+val Diff_FP = thm "Diff_FP";
+
+(*SubstAx*)
+val LeadsTo_eq_leadsTo = thm "LeadsTo_eq_leadsTo";
+val Always_LeadsTo_pre = thm "Always_LeadsTo_pre";
+val Always_LeadsTo_post = thm "Always_LeadsTo_post";
+val Always_LeadsToI = thm "Always_LeadsToI";
+val Always_LeadsToD = thm "Always_LeadsToD";
+val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo";
+val LeadsTo_Trans = thm "LeadsTo_Trans";
+val LeadsTo_Union = thm "LeadsTo_Union";
+val LeadsTo_UNIV = thm "LeadsTo_UNIV";
+val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate";
+val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2";
+val LeadsTo_UN = thm "LeadsTo_UN";
+val LeadsTo_Un = thm "LeadsTo_Un";
+val single_LeadsTo_I = thm "single_LeadsTo_I";
+val subset_imp_LeadsTo = thm "subset_imp_LeadsTo";
+val empty_LeadsTo = thm "empty_LeadsTo";
+val LeadsTo_weaken_R = thm "LeadsTo_weaken_R";
+val LeadsTo_weaken_L = thm "LeadsTo_weaken_L";
+val LeadsTo_weaken = thm "LeadsTo_weaken";
+val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken";
+val LeadsTo_Un_post = thm "LeadsTo_Un_post";
+val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un";
+val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib";
+val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib";
+val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib";
+val LeadsTo_Basis = thm "LeadsTo_Basis";
+val EnsuresI = thm "EnsuresI";
+val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis";
+val LeadsTo_Diff = thm "LeadsTo_Diff";
+val LeadsTo_UN_UN = thm "LeadsTo_UN_UN";
+val LeadsTo_UN_UN_noindex = thm "LeadsTo_UN_UN_noindex";
+val all_LeadsTo_UN_UN = thm "all_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 = thm "PSP";
+val PSP2 = thm "PSP2";
+val PSP_Unless = thm "PSP_Unless";
+val Stable_transient_Always_LeadsTo = thm "Stable_transient_Always_LeadsTo";
+val LeadsTo_wf_induct = thm "LeadsTo_wf_induct";
+val Bounded_induct = thm "Bounded_induct";
+val LessThan_induct = thm "LessThan_induct";
+val integ_0_le_induct = thm "integ_0_le_induct";
+val LessThan_bounded_induct = thm "LessThan_bounded_induct";
+val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct";
+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";
+
(*Union*)
val Init_SKIP = thm "Init_SKIP";
val Acts_SKIP = thm "Acts_SKIP";
@@ -377,6 +443,35 @@
val Allowed_PLam = thm "Allowed_PLam";
val PLam_preserves = thm "PLam_preserves";
+(*Follows*)
+val mono_Always_o = thm "mono_Always_o";
+val mono_LeadsTo_o = thm "mono_LeadsTo_o";
+val Follows_constant = thm "Follows_constant";
+val mono_Follows_o = thm "mono_Follows_o";
+val mono_Follows_apply = thm "mono_Follows_apply";
+val Follows_trans = thm "Follows_trans";
+val Follows_Increasing1 = thm "Follows_Increasing1";
+val Follows_Increasing2 = thm "Follows_Increasing2";
+val Follows_Bounded = thm "Follows_Bounded";
+val Follows_LeadsTo = thm "Follows_LeadsTo";
+val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe";
+val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe";
+val Always_Follows1 = thm "Always_Follows1";
+val Always_Follows2 = thm "Always_Follows2";
+val increasing_Un = thm "increasing_Un";
+val Increasing_Un = thm "Increasing_Un";
+val Always_Un = thm "Always_Un";
+val Follows_Un_lemma = thm "Follows_Un_lemma";
+val Follows_Un = thm "Follows_Un";
+val increasing_union = thm "increasing_union";
+val Increasing_union = thm "Increasing_union";
+val Always_union = thm "Always_union";
+val Follows_union_lemma = thm "Follows_union_lemma";
+val Follows_union = thm "Follows_union";
+val Follows_setsum = thm "Follows_setsum";
+val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe";
+val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe";
+
(*proves "co" properties when the program is specified*)
fun gen_constrains_tac(cs,ss) i =
@@ -409,6 +504,8 @@
ALLGOALS (clarify_tac cs),
ALLGOALS (asm_lr_simp_tac ss)]);
+fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
+
(*Composition equivalences, from Lift_prog*)