# HG changeset patch # User paulson # Date 1043919356 -3600 # Node ID 19f50fa807ae16653d9c3a5e74765e9e13f38e04 # Parent cfa3441c5238abd5d3bdb91f0e2a95c1fc59df52 converting more UNITY theories to new-style diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/IsaMakefile --- 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 \ diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/Comp/Priority.ML --- 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"; diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/Comp/Priority.thy --- 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" diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/Comp/PriorityAux.thy --- 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 diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/FP.ML --- 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"; - diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/FP.thy --- 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 diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/Follows.ML --- 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. \\i:I. f' i s) Fols (%s. \\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"; diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/Follows.thy --- 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. \i:I. f' i s) Fols (%s. \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 diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/SubstAx.ML --- 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 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]); diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/SubstAx.thy --- 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 " \\w " 60) + "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \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 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 diff -r cfa3441c5238 -r 19f50fa807ae src/HOL/UNITY/UNITY_tactics.ML --- 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*)