# HG changeset patch # User paulson # Date 1057657470 -7200 # Node ID 68da54626309a71d99ea7e13d85b932b3060ddce # Parent ad6ba9c55190f6edf4ff4d0baaed7785ee13e4ee Conversion of ZF/UNITY/{FP,Union} to Isar script. Introduction of X-symbols to the ML files. diff -r ad6ba9c55190 -r 68da54626309 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/IsaMakefile Tue Jul 08 11:44:30 2003 +0200 @@ -116,10 +116,9 @@ $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \ UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \ - UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \ + UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \ UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.thy \ - UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy \ - UNITY/Union.ML UNITY/Union.thy \ + UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \ UNITY/AllocBase.thy UNITY/AllocImpl.thy\ UNITY/ClientImpl.thy UNITY/Distributor.thy\ UNITY/Follows.ML UNITY/Follows.thy\ diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Comp.ML --- a/src/ZF/UNITY/Comp.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Comp.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/Comp.ML - ID: $Id$ + ID: $Id \\ Comp.ML,v 1.8 2003/06/27 16:40:25 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 1998 University of Cambridge Composition @@ -20,7 +20,7 @@ qed "componentI"; Goalw [component_def] - "G:program ==> (F component G) <-> \ + "G \\ program ==> (F component G) <-> \ \ (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))"; by Auto_tac; by (rtac exI 1); @@ -29,13 +29,13 @@ qed "component_eq_subset"; Goalw [component_def] - "F:program ==> SKIP component F"; + "F \\ program ==> SKIP component F"; by (res_inst_tac [("x", "F")] exI 1); by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); qed "component_SKIP"; Goalw [component_def] -"F:program ==> F component F"; +"F \\ program ==> F component F"; by (res_inst_tac [("x", "F")] exI 1); by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1); qed "component_refl"; @@ -66,7 +66,7 @@ by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); qed "Join_absorb2"; -Goal "H:program==>(JOIN(I,F) component H) <-> (ALL i:I. F(i) component H)"; +Goal "H \\ program==>(JOIN(I,F) component H) <-> (\\i \\ I. F(i) component H)"; by (case_tac "I=0" 1); by (Force_tac 1); by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); @@ -77,7 +77,7 @@ by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1)); qed "JN_component_iff"; -Goalw [component_def] "i:I ==> F(i) component (JN i:I. (F(i)))"; +Goalw [component_def] "i \\ I ==> F(i) component (\\i \\ I. (F(i)))"; by (blast_tac (claset() addIs [JN_absorb]) 1); qed "component_JN"; @@ -85,19 +85,19 @@ by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); qed "component_trans"; -Goal "[| F:program; G:program |] ==>(F component G & G component F) --> F = G"; +Goal "[| F \\ program; G \\ program |] ==>(F component G & G component F) --> F = G"; by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); by (Clarify_tac 1); by (rtac program_equalityI 1); by Auto_tac; qed "component_antisym"; -Goal "H:program ==> ((F Join G) component H) <-> (F component H & G component H)"; +Goal "H \\ program ==> ((F Join G) component H) <-> (F component H & G component H)"; by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1); by (Blast_tac 1); qed "Join_component_iff"; -Goal "[| F component G; G:A co B; F:program |] ==> F : A co B"; +Goal "[| F component G; G \\ A co B; F \\ program |] ==> F \\ A co B"; by (ftac constrainsD2 1); by (rotate_tac ~1 1); by (auto_tac (claset(), @@ -119,15 +119,15 @@ val prems = Goalw [preserves_def] -"ALL z. F:stable({s:state. f(s) = z}) ==> F:preserves(f)"; +"\\z. F \\ stable({s \\ state. f(s) = z}) ==> F \\ preserves(f)"; by Auto_tac; by (blast_tac (claset() addDs [stableD2]) 1); qed "preserves_aux"; bind_thm("preservesI", allI RS preserves_aux); Goalw [preserves_def, stable_def, constrains_def] - "[| F:preserves(f); act : Acts(F); : act |] ==> f(s) = f(t)"; -by (subgoal_tac "s:state & t:state" 1); + "[| F \\ preserves(f); act \\ Acts(F); \\ act |] ==> f(s) = f(t)"; +by (subgoal_tac "s \\ state & t \\ state" 1); by (blast_tac (claset() addSDs [Acts_type RS subsetD]) 2); by Auto_tac; by (dres_inst_tac [("x", "f(s)")] spec 1); @@ -136,16 +136,16 @@ qed "preserves_imp_eq"; Goalw [preserves_def] -"(F Join G : preserves(v)) <-> \ -\ (programify(F) : preserves(v) & programify(G) : preserves(v))"; +"(F Join G \\ preserves(v)) <-> \ +\ (programify(F) \\ preserves(v) & programify(G) \\ preserves(v))"; by (auto_tac (claset(), simpset() addsimps [INT_iff])); qed "Join_preserves"; -Goal "(JOIN(I,F): preserves(v)) <-> (ALL i:I. programify(F(i)):preserves(v))"; +Goal "(JOIN(I,F): preserves(v)) <-> (\\i \\ I. programify(F(i)):preserves(v))"; by (auto_tac (claset(), simpset() addsimps [JN_stable, preserves_def, INT_iff])); qed "JN_preserves"; -Goal "SKIP : preserves(v)"; +Goal "SKIP \\ preserves(v)"; by (auto_tac (claset(), simpset() addsimps [preserves_def, INT_iff])); qed "SKIP_preserves"; @@ -163,7 +163,7 @@ by (REPEAT(Blast_tac 1)); qed "preserves_fun_pair"; -Goal "F:preserves(fun_pair(v, w)) <-> F:preserves(v) Int preserves(w)"; +Goal "F \\ preserves(fun_pair(v, w)) <-> F \\ preserves(v) Int preserves(w)"; by (simp_tac (simpset() addsimps [preserves_fun_pair]) 1); qed "preserves_fun_pair_iff"; AddIffs [preserves_fun_pair_iff]; @@ -182,7 +182,7 @@ by Auto_tac; qed "preserves_type"; -Goal "F:preserves(f) ==> F:program"; +Goal "F \\ preserves(f) ==> F \\ program"; by (blast_tac (claset() addIs [preserves_type RS subsetD]) 1); qed "preserves_into_program"; AddTCs [preserves_into_program]; @@ -195,11 +195,11 @@ by Auto_tac; qed "subset_preserves_comp"; -Goal "F:preserves(f) ==> F:preserves(g comp f)"; +Goal "F \\ preserves(f) ==> F \\ preserves(g comp f)"; by (blast_tac (claset() addIs [subset_preserves_comp RS subsetD]) 1); qed "imp_preserves_comp"; -Goal "preserves(f) <= stable({s:state. P(f(s))})"; +Goal "preserves(f) <= stable({s \\ state. P(f(s))})"; by (auto_tac (claset(), simpset() addsimps [preserves_def, stable_def, constrains_def])); by (rename_tac "s' s" 1); @@ -207,12 +207,12 @@ by (ALLGOALS Force_tac); qed "preserves_subset_stable"; -Goal "F:preserves(f) ==> F:stable({s:state. P(f(s))})"; +Goal "F \\ preserves(f) ==> F \\ stable({s \\ state. P(f(s))})"; by (blast_tac (claset() addIs [preserves_subset_stable RS subsetD]) 1); qed "preserves_imp_stable"; Goalw [increasing_def] - "[| F:preserves(f); ALL x:state. f(x):A |] ==> F:Increasing.increasing(A, r, f)"; + "[| F \\ preserves(f); \\x \\ state. f(x):A |] ==> F \\ Increasing.increasing(A, r, f)"; by (auto_tac (claset() addIs [preserves_into_program], simpset())); by (res_inst_tac [("P", "%x. :r")] preserves_imp_stable 1); @@ -227,7 +227,7 @@ by (auto_tac (claset() addDs [ActsD], simpset())); qed "preserves_id_subset_stable"; -Goal "[| F:preserves(%x. x); st_set(A) |] ==> F:stable(A)"; +Goal "[| F \\ preserves(%x. x); st_set(A) |] ==> F \\ stable(A)"; by (blast_tac (claset() addIs [preserves_id_subset_stable RS subsetD]) 1); qed "preserves_id_imp_stable"; @@ -242,13 +242,13 @@ (* component_of satisfies many of component's properties *) Goalw [component_of_def] -"F:program ==> F component_of F"; +"F \\ program ==> F component_of F"; by (res_inst_tac [("x", "SKIP")] exI 1); by Auto_tac; qed "component_of_refl"; Goalw [component_of_def] -"F:program ==>SKIP component_of F"; +"F \\ program ==>SKIP component_of F"; by Auto_tac; by (res_inst_tac [("x", "F")] exI 1); by Auto_tac; @@ -272,7 +272,7 @@ qed "localize_Acts_eq"; Goalw [localize_def] - "AllowedActs(localize(v,F)) = AllowedActs(F) Int (UN G:preserves(v). Acts(G))"; + "AllowedActs(localize(v,F)) = AllowedActs(F) Int (\\G \\ preserves(v). Acts(G))"; by (rtac equalityI 1); by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "localize_AllowedActs_eq"; @@ -282,21 +282,21 @@ (** Theorems used in ClientImpl **) Goal - "[| F:stable({s:state. P(f(s), g(s))}); G:preserves(f); G:preserves(g) |] \ -\ ==> F Join G : stable({s:state. P(f(s), g(s))})"; + "[| F \\ stable({s \\ state. P(f(s), g(s))}); G \\ preserves(f); G \\ preserves(g) |] \ +\ ==> F Join G \\ stable({s \\ state. P(f(s), g(s))})"; by (auto_tac (claset() addDs [ActsD, preserves_into_program], simpset() addsimps [stable_def, constrains_def])); -by (case_tac "act:Acts(F)" 1); +by (case_tac "act \\ Acts(F)" 1); by Auto_tac; by (dtac preserves_imp_eq 1); by (dtac preserves_imp_eq 3); by Auto_tac; qed "stable_localTo_stable2"; -Goal "[| F : stable({s:state. :r}); G:preserves(f); \ -\ F Join G : Increasing(A, r, g); \ -\ ALL x:state. f(x):A & g(x):A |] \ -\ ==> F Join G : Stable({s:state. :r})"; +Goal "[| F \\ stable({s \\ state. :r}); G \\ preserves(f); \ +\ F Join G \\ Increasing(A, r, g); \ +\ \\x \\ state. f(x):A & g(x):A |] \ +\ ==> F Join G \\ Stable({s \\ state. :r})"; by (auto_tac (claset(), simpset() addsimps [stable_def, Stable_def, Increasing_def, Constrains_def, all_conj_distrib])); @@ -308,8 +308,8 @@ simpset() addsimps [preserves_def, stable_def, constrains_def, ball_conj_distrib, all_conj_distrib])); (*We have a G-action, so delete assumptions about F-actions*) -by (thin_tac "ALL act:Acts(F). ?P(act)" 1); -by (thin_tac "\\k\\A. ALL act:Acts(F). ?P(k,act)" 1); +by (thin_tac "\\act \\ Acts(F). ?P(act)" 1); +by (thin_tac "\\k\\A. \\act \\ Acts(F). ?P(k,act)" 1); by (subgoal_tac "f(x) = f(xa)" 1); by (auto_tac (claset() addSDs [bspec], simpset())); qed "Increasing_preserves_Stable"; @@ -318,24 +318,24 @@ (** Lemma used in AllocImpl **) Goalw [Constrains_def, constrains_def] -"[| ALL x:I. F: A(x) Co B; F:program |] ==> F:(UN x:I. A(x)) Co B"; +"[| \\x \\ I. F \\ A(x) Co B; F \\ program |] ==> F:(\\x \\ I. A(x)) Co B"; by Auto_tac; qed "Constrains_UN_left"; Goalw [stable_def, Stable_def, preserves_def] - "[| F:stable({s:state. P(f(s), g(s))}); \ -\ ALL k:A. F Join G: Stable({s:state. P(k, g(s))}); \ -\ G:preserves(f); ALL s:state. f(s):A|] ==> \ -\ F Join G : Stable({s:state. P(f(s), g(s))})"; -by (res_inst_tac [("A", "(UN k:A. {s:state. f(s)=k} Int {s:state. P(f(s), g(s))})")] + "[| F \\ stable({s \\ state. P(f(s), g(s))}); \ +\ \\k \\ A. F Join G \\ Stable({s \\ state. P(k, g(s))}); \ +\ G \\ preserves(f); \\s \\ state. f(s):A|] ==> \ +\ F Join G \\ Stable({s \\ state. P(f(s), g(s))})"; +by (res_inst_tac [("A", "(\\k \\ A. {s \\ state. f(s)=k} Int {s \\ state. P(f(s), g(s))})")] Constrains_weaken_L 1); by (Blast_tac 2); by (rtac Constrains_UN_left 1); by Auto_tac; -by (res_inst_tac [("A", "{s:state. f(s)=k} Int {s:state. P(f(s), g(s))} Int \ -\ {s:state. P(k, g(s))}"), - ("A'", "({s:state. f(s)=k} Un {s:state. P(f(s), g(s))}) \ -\ Int {s:state. P(k, g(s))}")] Constrains_weaken 1); +by (res_inst_tac [("A", "{s \\ state. f(s)=k} Int {s \\ state. P(f(s), g(s))} Int \ +\ {s \\ state. P(k, g(s))}"), + ("A'", "({s \\ state. f(s)=k} Un {s \\ state. P(f(s), g(s))}) \ +\ Int {s \\ state. P(k, g(s))}")] Constrains_weaken 1); by (REPEAT(Blast_tac 2)); by (rtac Constrains_Int 1); by (rtac constrains_imp_Constrains 1); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Constrains.ML --- a/src/ZF/UNITY/Constrains.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Constrains.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,9 +1,9 @@ (* Title: ZF/UNITY/Constrains.ML - ID: $Id$ + ID: $Id \\ Constrains.ML,v 1.10 2003/06/20 10:10:45 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge -Safety relations: restricted to the set of reachable states. +Safety relations \\ restricted to the set of reachable states. Proofs ported from HOL. *) @@ -35,7 +35,7 @@ AddIffs [state_Int_reachable]; Goal -"F:program ==> reachable(F)={s:state. EX evs. :traces(Init(F), Acts(F))}"; +"F \\ program ==> reachable(F)={s \\ state. \\evs. :traces(Init(F), Acts(F))}"; by (rtac equalityI 1); by Safe_tac; by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1); @@ -48,8 +48,8 @@ by (blast_tac (claset() addIs reachable.intrs) 1); qed "Init_into_reachable"; -Goal "[| F:program; G:program; \ -\ Acts(G) <= Acts(F) |] ==> G:stable(reachable(F))"; +Goal "[| F \\ program; G \\ program; \ +\ Acts(G) <= Acts(F) |] ==> G \\ stable(reachable(F))"; by (blast_tac (claset() addIs [stableI, constrainsI, st_setI, reachable_type RS subsetD] @ reachable.intrs) 1); @@ -60,12 +60,12 @@ (*The set of all reachable states is an invariant...*) Goalw [invariant_def, initially_def] - "F:program ==> F:invariant(reachable(F))"; + "F \\ program ==> F \\ invariant(reachable(F))"; by (blast_tac (claset() addIs [reachable_type RS subsetD]@reachable.intrs) 1); qed "invariant_reachable"; (*...in fact the strongest invariant!*) -Goal "F:invariant(A) ==> reachable(F) <= A"; +Goal "F \\ invariant(A) ==> reachable(F) <= A"; by (cut_inst_tac [("F", "F")] Acts_type 1); by (cut_inst_tac [("F", "F")] Init_type 1); by (cut_inst_tac [("F", "F")] reachable_type 1); @@ -78,7 +78,7 @@ (*** Co ***) -Goal "F:B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')"; +Goal "F \\ B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')"; by (forward_tac [constrains_type RS subsetD] 1); by (forward_tac [[asm_rl, asm_rl, subset_refl] MRS stable_reachable] 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [stable_def, constrains_Int]))); @@ -86,7 +86,7 @@ (*Resembles the previous definition of Constrains*) Goalw [Constrains_def] -"A Co B = {F:program. F:(reachable(F) Int A) co (reachable(F) Int B)}"; +"A Co B = {F \\ program. F:(reachable(F) Int A) co (reachable(F) Int B)}"; by (blast_tac (claset() addDs [constrains_reachable_Int, constrains_type RS subsetD] addIs [constrains_weaken]) 1); @@ -94,12 +94,12 @@ val Constrains_def2 = Constrains_eq_constrains RS eq_reflection; Goalw [Constrains_def] - "F:A co A' ==> F:A Co A'"; + "F \\ A co A' ==> F \\ A Co A'"; by (blast_tac (claset() addIs [constrains_weaken_L] addDs [constrainsD2]) 1); qed "constrains_imp_Constrains"; val prems = Goalw [Constrains_def, constrains_def, st_set_def] -"[|(!!act s s'. [| act: Acts(F); :act; s:A |] ==> s':A'); F:program|]==>F:A Co A'"; +"[|(!!act s s'. [| act \\ Acts(F); :act; s \\ A |] ==> s':A'); F \\ program|]==>F \\ A Co A'"; by (auto_tac (claset(), simpset() addsimps prems)); by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1); qed "ConstrainsI"; @@ -109,43 +109,43 @@ by (Blast_tac 1); qed "Constrains_type"; -Goal "F : 0 Co B <-> F:program"; +Goal "F \\ 0 Co B <-> F \\ program"; by (auto_tac (claset() addDs [Constrains_type RS subsetD] addIs [constrains_imp_Constrains], simpset())); qed "Constrains_empty"; AddIffs [Constrains_empty]; -Goalw [Constrains_def] "F : A Co state <-> F:program"; +Goalw [Constrains_def] "F \\ A Co state <-> F \\ program"; by (auto_tac (claset() addDs [Constrains_type RS subsetD] addIs [constrains_imp_Constrains], simpset())); qed "Constrains_state"; AddIffs [Constrains_state]; Goalw [Constrains_def2] - "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"; + "[| F \\ A Co A'; A'<=B' |] ==> F \\ A Co B'"; by (blast_tac (claset() addIs [constrains_weaken_R]) 1); qed "Constrains_weaken_R"; Goalw [Constrains_def2] - "[| F : A Co A'; B<=A |] ==> F : B Co A'"; + "[| F \\ A Co A'; B<=A |] ==> F \\ B Co A'"; by (blast_tac (claset() addIs [constrains_weaken_L, st_set_subset]) 1); qed "Constrains_weaken_L"; Goalw [Constrains_def2] - "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"; + "[| F \\ A Co A'; B<=A; A'<=B' |] ==> F \\ B Co B'"; by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1); qed "Constrains_weaken"; (** Union **) Goalw [Constrains_def2] -"[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"; +"[| F \\ A Co A'; F \\ B Co B' |] ==> F \\ (A Un B) Co (A' Un B')"; by Auto_tac; by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1); by (blast_tac (claset() addIs [constrains_Un]) 1); qed "Constrains_Un"; val [major, minor] = Goalw [Constrains_def2] -"[|(!!i. i:I==>F:A(i) Co A'(i)); F:program|] ==> F:(UN i:I. A(i)) Co (UN i:I. A'(i))"; +"[|(!!i. i \\ I==>F \\ A(i) Co A'(i)); F \\ program|] ==> F:(\\i \\ I. A(i)) Co (\\i \\ I. A'(i))"; by (cut_facts_tac [minor] 1); by (auto_tac (claset() addDs [major] addIs [constrains_UN], @@ -155,15 +155,15 @@ (** Intersection **) Goalw [Constrains_def] -"[| F : A Co A'; F : B Co B'|]==> F:(A Int B) Co (A' Int B')"; +"[| F \\ A Co A'; F \\ B Co B'|]==> F:(A Int B) Co (A' Int B')"; by (subgoal_tac "reachable(F) Int (A Int B) = \ \ (reachable(F) Int A) Int (reachable(F) Int B)" 1); by (ALLGOALS(force_tac (claset() addIs [constrains_Int], simpset()))); qed "Constrains_Int"; val [major,minor] = Goal -"[| (!!i. i:I ==>F: A(i) Co A'(i)); F:program |] \ -\ ==> F:(INT i:I. A(i)) Co (INT i:I. A'(i))"; +"[| (!!i. i \\ I ==>F \\ A(i) Co A'(i)); F \\ program |] \ +\ ==> F:(\\i \\ I. A(i)) Co (\\i \\ I. A'(i))"; by (cut_facts_tac [minor] 1); by (asm_simp_tac (simpset() delsimps INT_simps addsimps [Constrains_def]@INT_extend_simps) 1); @@ -172,17 +172,17 @@ by (auto_tac (claset(), simpset() addsimps [Constrains_def])); qed "Constrains_INT"; -Goalw [Constrains_def] "F : A Co A' ==> reachable(F) Int A <= A'"; +Goalw [Constrains_def] "F \\ A Co A' ==> reachable(F) Int A <= A'"; by (blast_tac (claset() addDs [constrains_imp_subset]) 1); qed "Constrains_imp_subset"; Goalw [Constrains_def2] - "[| F : A Co B; F : B Co C |] ==> F : A Co C"; + "[| F \\ A Co B; F \\ B Co C |] ==> F \\ A Co C"; by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1); qed "Constrains_trans"; Goalw [Constrains_def2] -"[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"; +"[| F \\ A Co (A' Un B); F \\ B Co B' |] ==> F \\ A Co (A' Un B')"; by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1); by (blast_tac (claset() addIs [constrains_cancel]) 1); qed "Constrains_cancel"; @@ -191,63 +191,63 @@ (* Useful because there's no Stable_weaken. [Tanja Vos] *) Goalw [stable_def, Stable_def] -"F : stable(A) ==> F : Stable(A)"; +"F \\ stable(A) ==> F \\ Stable(A)"; by (etac constrains_imp_Constrains 1); qed "stable_imp_Stable"; -Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)"; +Goal "[| F \\ Stable(A); A = B |] ==> F \\ Stable(B)"; by (Blast_tac 1); qed "Stable_eq"; Goal -"F : Stable(A) <-> (F:stable(reachable(F) Int A))"; +"F \\ Stable(A) <-> (F \\ stable(reachable(F) Int A))"; by (auto_tac (claset() addDs [constrainsD2], simpset() addsimps [Stable_def, stable_def, Constrains_def2])); qed "Stable_eq_stable"; -Goalw [Stable_def] "F:A Co A ==> F : Stable(A)"; +Goalw [Stable_def] "F \\ A Co A ==> F \\ Stable(A)"; by (assume_tac 1); qed "StableI"; -Goalw [Stable_def] "F : Stable(A) ==> F : A Co A"; +Goalw [Stable_def] "F \\ Stable(A) ==> F \\ A Co A"; by (assume_tac 1); qed "StableD"; Goalw [Stable_def] - "[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')"; + "[| F \\ Stable(A); F \\ Stable(A') |] ==> F \\ Stable(A Un A')"; by (blast_tac (claset() addIs [Constrains_Un]) 1); qed "Stable_Un"; Goalw [Stable_def] - "[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')"; + "[| F \\ Stable(A); F \\ Stable(A') |] ==> F \\ Stable (A Int A')"; by (blast_tac (claset() addIs [Constrains_Int]) 1); qed "Stable_Int"; Goalw [Stable_def] - "[| F : Stable(C); F : A Co (C Un A') |] \ -\ ==> F : (C Un A) Co (C Un A')"; + "[| F \\ Stable(C); F \\ A Co (C Un A') |] \ +\ ==> F \\ (C Un A) Co (C Un A')"; by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1); qed "Stable_Constrains_Un"; Goalw [Stable_def] - "[| F : Stable(C); F : (C Int A) Co A' |] \ -\ ==> F : (C Int A) Co (C Int A')"; + "[| F \\ Stable(C); F \\ (C Int A) Co A' |] \ +\ ==> F \\ (C Int A) Co (C Int A')"; by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1); qed "Stable_Constrains_Int"; val [major,minor] = Goalw [Stable_def] -"[| (!!i. i:I ==> F : Stable(A(i))); F:program |]==> F : Stable (UN i:I. A(i))"; +"[| (!!i. i \\ I ==> F \\ Stable(A(i))); F \\ program |]==> F \\ Stable (\\i \\ I. A(i))"; by (cut_facts_tac [minor] 1); by (blast_tac (claset() addIs [Constrains_UN,major]) 1); qed "Stable_UN"; val [major,minor] = Goalw [Stable_def] -"[|(!!i. i:I ==> F:Stable(A(i))); F:program |]==> F : Stable (INT i:I. A(i))"; +"[|(!!i. i \\ I ==> F \\ Stable(A(i))); F \\ program |]==> F \\ Stable (\\i \\ I. A(i))"; by (cut_facts_tac [minor] 1); by (blast_tac (claset() addIs [Constrains_INT, major]) 1); qed "Stable_INT"; -Goal "F:program ==>F : Stable (reachable(F))"; +Goal "F \\ program ==>F \\ Stable (reachable(F))"; by (asm_simp_tac (simpset() addsimps [Stable_eq_stable, Int_absorb]) 1); qed "Stable_reachable"; @@ -258,12 +258,12 @@ qed "Stable_type"; (*** The Elimination Theorem. The "free" m has become universally quantified! - Should the premise be !!m instead of ALL m ? Would make it harder to use + Should the premise be !!m instead of \\m ? Would make it harder to use in forward proof. ***) Goalw [Constrains_def] -"[| ALL m:M. F : ({s:A. x(s) = m}) Co (B(m)); F:program |] \ -\ ==> F : ({s:A. x(s):M}) Co (UN m:M. B(m))"; +"[| \\m \\ M. F \\ ({s \\ A. x(s) = m}) Co (B(m)); F \\ program |] \ +\ ==> F \\ ({s \\ A. x(s):M}) Co (\\m \\ M. B(m))"; by Auto_tac; by (res_inst_tac [("A1","reachable(F)Int A")] (elimination RS constrains_weaken_L) 1); by (auto_tac (claset() addIs [constrains_weaken_L], simpset())); @@ -271,8 +271,8 @@ (* As above, but for the special case of A=state *) Goal - "[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \ -\ ==> F : {s:state. x(s):M} Co (UN m:M. B(m))"; + "[| \\m \\ M. F \\ {s \\ state. x(s) = m} Co B(m); F \\ program |] \ +\ ==> F \\ {s \\ state. x(s):M} Co (\\m \\ M. B(m))"; by (blast_tac (claset() addIs [Elimination]) 1); qed "Elimination2"; @@ -287,12 +287,12 @@ (** Natural deduction rules for "Always A" **) Goalw [Always_def, initially_def] -"[| Init(F)<=A; F : Stable(A) |] ==> F : Always(A)"; +"[| Init(F)<=A; F \\ Stable(A) |] ==> F \\ Always(A)"; by (forward_tac [Stable_type RS subsetD] 1); by Auto_tac; qed "AlwaysI"; -Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)"; +Goal "F \\ Always(A) ==> Init(F)<=A & F \\ Stable(A)"; by (asm_full_simp_tac (simpset() addsimps [Always_def, initially_def]) 1); qed "AlwaysD"; @@ -300,7 +300,7 @@ bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2); (*The set of all reachable states is Always*) -Goal "F : Always(A) ==> reachable(F) <= A"; +Goal "F \\ Always(A) ==> reachable(F) <= A"; by (full_simp_tac (simpset() addsimps [Stable_def, Constrains_def, constrains_def, Always_def, initially_def]) 1); by (rtac subsetI 1); @@ -309,13 +309,13 @@ qed "Always_includes_reachable"; Goalw [Always_def, invariant_def, Stable_def, stable_def] - "F : invariant(A) ==> F : Always(A)"; + "F \\ invariant(A) ==> F \\ Always(A)"; by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1); qed "invariant_imp_Always"; bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always); -Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A)}"; +Goal "Always(A) = {F \\ program. F \\ invariant(reachable(F) Int A)}"; by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, Constrains_def2, stable_def, initially_def]) 1); by (rtac equalityI 1); @@ -324,7 +324,7 @@ qed "Always_eq_invariant_reachable"; (*the RHS is the traditional definition of the "always" operator*) -Goal "Always(A) = {F:program. reachable(F) <= A}"; +Goal "Always(A) = {F \\ program. reachable(F) <= A}"; by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); by (auto_tac (claset() addDs [invariant_includes_reachable], @@ -344,12 +344,12 @@ qed "Always_state_eq"; Addsimps [Always_state_eq]; -Goal "F:program ==> F : Always(state)"; +Goal "F \\ program ==> F \\ Always(state)"; by (auto_tac (claset() addDs [reachable_type RS subsetD], simpset() addsimps [Always_eq_includes_reachable])); qed "state_AlwaysI"; -Goal "st_set(A) ==> Always(A) = (UN I: Pow(A). invariant(I))"; +Goal "st_set(A) ==> Always(A) = (\\I \\ Pow(A). invariant(I))"; by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); @@ -359,7 +359,7 @@ addDs [invariant_type RS subsetD]) 1)); qed "Always_eq_UN_invariant"; -Goal "[| F : Always(A); A <= B |] ==> F : Always(B)"; +Goal "[| F \\ Always(A); A <= B |] ==> F \\ Always(B)"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "Always_weaken"; @@ -367,28 +367,28 @@ (*** "Co" rules involving Always ***) val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp; -Goal "F:Always(I) ==> (F:(I Int A) Co A') <-> (F : A Co A')"; +Goal "F \\ Always(I) ==> (F:(I Int A) Co A') <-> (F \\ A Co A')"; by (asm_simp_tac (simpset() addsimps [Always_includes_reachable RS Int_absorb2, Constrains_def, Int_assoc RS sym]) 1); qed "Always_Constrains_pre"; -Goal "F:Always(I) ==> (F : A Co (I Int A')) <->(F : A Co A')"; +Goal "F \\ Always(I) ==> (F \\ A Co (I Int A')) <->(F \\ A Co A')"; by (asm_simp_tac (simpset() addsimps [Always_includes_reachable RS Int_absorb2, Constrains_eq_constrains, Int_assoc RS sym]) 1); qed "Always_Constrains_post"; -Goal "[| F : Always(I); F : (I Int A) Co A' |] ==> F : A Co A'"; +Goal "[| F \\ Always(I); F \\ (I Int A) Co A' |] ==> F \\ A Co A'"; by (blast_tac (claset() addIs [Always_Constrains_pre RS iffD1]) 1); qed "Always_ConstrainsI"; -(* [| F : Always(I); F : A Co A' |] ==> F : A Co (I Int A') *) +(* [| F \\ Always(I); F \\ A Co A' |] ==> F \\ A Co (I Int A') *) bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2); (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) Goal -"[|F:Always(C); F:A Co A'; C Int B<=A; C Int A'<=B'|]==>F:B Co B'"; +"[|F \\ Always(C); F \\ A Co A'; C Int B<=A; C Int A'<=B'|]==>F \\ B Co B'"; by (rtac Always_ConstrainsI 1); by (dtac Always_ConstrainsD 2); by (ALLGOALS(Asm_simp_tac)); @@ -400,20 +400,20 @@ by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "Always_Int_distrib"; -(* the premise i:I is need since INT is formally not defined for I=0 *) -Goal "i:I==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))"; +(* the premise i \\ I is need since \\is formally not defined for I=0 *) +Goal "i \\ I==>Always(\\i \\ I. A(i)) = (\\i \\ I. Always(A(i)))"; by (rtac equalityI 1); by (auto_tac (claset(), simpset() addsimps [Inter_iff, Always_eq_includes_reachable])); qed "Always_INT_distrib"; -Goal "[| F:Always(A); F:Always(B) |] ==> F:Always(A Int B)"; +Goal "[| F \\ Always(A); F \\ Always(B) |] ==> F \\ Always(A Int B)"; by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1); qed "Always_Int_I"; (*Allows a kind of "implication introduction"*) -Goal "[| F:Always(A) |] ==> (F : Always(C-A Un B)) <-> (F : Always(B))"; +Goal "[| F \\ Always(A) |] ==> (F \\ Always(C-A Un B)) <-> (F \\ Always(B))"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "Always_Diff_Un_eq"; @@ -421,7 +421,7 @@ used by Always_Int_I) *) val Always_thin = read_instantiate_sg (sign_of thy) - [("V", "?F : Always(?A)")] thin_rl; + [("V", "?F \\ Always(?A)")] thin_rl; (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin; @@ -430,7 +430,7 @@ val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I); (*To allow expansion of the program's definition when appropriate*) -val program_defs_ref = ref ([] : thm list); +val program_defs_ref = ref ([]: thm list); (*proves "co" properties when the program is specified*) diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/FP.ML --- a/src/ZF/UNITY/FP.ML Mon Jul 07 17:58:21 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,81 +0,0 @@ -(* Title: ZF/UNITY/FP.ML - ID: $Id$ - Author: Sidi O Ehmety, Computer Laboratory - Copyright 2001 University of Cambridge - -Fixed Point of a Program - -From Misra, "A Logic for Concurrent Programming", 1994 - -Theory ported form HOL. -*) - -Goalw [FP_Orig_def] "FP_Orig(F)<=state"; -by (Blast_tac 1); -qed "FP_Orig_type"; - -Goalw [st_set_def] "st_set(FP_Orig(F))"; -by (rtac FP_Orig_type 1); -qed "st_set_FP_Orig"; -AddIffs [st_set_FP_Orig]; - -Goalw [FP_def] "FP(F)<=state"; -by (Blast_tac 1); -qed "FP_type"; - -Goalw [st_set_def] "st_set(FP(F))"; -by (rtac FP_type 1); -qed "st_set_FP"; -AddIffs [st_set_FP]; - -Goalw [FP_Orig_def, stable_def] "F:program ==> F:stable(FP_Orig(F) Int B)"; -by (stac Int_Union2 1); -by (blast_tac (claset() addIs [constrains_UN]) 1); -qed "stable_FP_Orig_Int"; - -Goalw [FP_Orig_def, stable_def, st_set_def] - "[| ALL B. F: stable (A Int B); st_set(A) |] ==> A <= FP_Orig(F)"; -by (Blast_tac 1); -qed "FP_Orig_weakest2"; - -bind_thm("FP_Orig_weakest", allI RS FP_Orig_weakest2); - -Goal "F:program ==> F : stable (FP(F) Int B)"; -by (subgoal_tac "FP(F) Int B = (UN x:B. FP(F) Int {x})" 1); -by (Blast_tac 2); -by (asm_simp_tac (simpset() addsimps [Int_cons_right]) 1); -by (rewrite_goals_tac [FP_def, stable_def]); -by (rtac constrains_UN 1); -by (auto_tac (claset(), simpset() addsimps [cons_absorb])); -qed "stable_FP_Int"; - -Goal "F:program ==> FP(F) <= FP_Orig(F)"; -by (rtac (stable_FP_Int RS FP_Orig_weakest) 1); -by Auto_tac; -qed "FP_subset_FP_Orig"; - -Goalw [FP_Orig_def, FP_def] "F:program ==> 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_cons_right]) 1); -by (ftac stableD2 1); -by (auto_tac (claset(), simpset() addsimps [cons_absorb, st_set_def])); -qed "FP_Orig_subset_FP"; - - -Goal "F:program ==> FP(F) = FP_Orig(F)"; -by (rtac ([FP_subset_FP_Orig,FP_Orig_subset_FP] MRS equalityI) 1); -by (ALLGOALS(assume_tac)); -qed "FP_equivalence"; - - -Goal "[| ALL B. F : stable(A Int B); F:program; st_set(A) |] ==> A <= FP(F)"; -by (asm_simp_tac (simpset() addsimps [FP_equivalence, FP_Orig_weakest]) 1); -qed "FP_weakest2"; -bind_thm("FP_weakest", allI RS FP_weakest2); - -Goalw [FP_def, stable_def, constrains_def, st_set_def] -"[| F:program; st_set(A) |] ==> A-FP(F) = (UN act:Acts(F). A-{s:state. act``{s} <= {s}})"; -by (Blast_tac 1); -qed "Diff_FP"; - diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/FP.thy --- a/src/ZF/UNITY/FP.thy Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/FP.thy Tue Jul 08 11:44:30 2003 +0200 @@ -3,20 +3,99 @@ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge -Fixed Point of a Program - From Misra, "A Logic for Concurrent Programming", 1994 Theory ported from HOL. *) -FP = UNITY + +header{*Fixed Point of a Program*} + +theory FP = UNITY: constdefs - FP_Orig :: i=>i - "FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})" + FP_Orig :: "i=>i" + "FP_Orig(F) == Union({A \ Pow(state). \B. F \ stable(A Int B)})" + + FP :: "i=>i" + "FP(F) == {s\state. F \ stable({s})}" + + +lemma FP_Orig_type: "FP_Orig(F) \ state" +by (unfold FP_Orig_def, blast) + +lemma st_set_FP_Orig [iff]: "st_set(FP_Orig(F))" +apply (unfold st_set_def) +apply (rule FP_Orig_type) +done + +lemma FP_type: "FP(F) \ state" +by (unfold FP_def, blast) + +lemma st_set_FP [iff]: "st_set(FP(F))" +apply (unfold st_set_def) +apply (rule FP_type) +done + +lemma stable_FP_Orig_Int: "F \ program ==> 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_weakest2: + "[| \B. F \ stable (A Int B); st_set(A) |] ==> A \ FP_Orig(F)" +apply (unfold FP_Orig_def stable_def st_set_def, blast) +done + +lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard] - FP :: i=>i - "FP(F) == {s:state. F : stable({s})}" +lemma stable_FP_Int: "F \ program ==> F \ stable (FP(F) Int B)" +apply (subgoal_tac "FP (F) Int B = (\x\B. FP (F) Int {x}) ") + prefer 2 apply blast +apply (simp (no_asm_simp) add: Int_cons_right) +apply (unfold FP_def stable_def) +apply (rule constrains_UN) +apply (auto simp add: cons_absorb) +done + +lemma FP_subset_FP_Orig: "F \ program ==> FP(F) \ FP_Orig(F)" +by (rule stable_FP_Int [THEN FP_Orig_weakest], auto) + +lemma FP_Orig_subset_FP: "F \ program ==> FP_Orig(F) \ FP(F)" +apply (unfold FP_Orig_def FP_def, clarify) +apply (drule_tac x = "{x}" in spec) +apply (simp add: Int_cons_right) +apply (frule stableD2) +apply (auto simp add: cons_absorb st_set_def) +done + +lemma FP_equivalence: "F \ program ==> FP(F) = FP_Orig(F)" +by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig) + +lemma FP_weakest [rule_format]: + "[| \B. F \ stable(A Int B); F \ program; st_set(A) |] ==> A \ FP(F)" +by (simp add: FP_equivalence FP_Orig_weakest) + + +lemma Diff_FP: + "[| F \ program; st_set(A) |] + ==> A-FP(F) = (\act \ Acts(F). A - {s \ state. act``{s} \ {s}})" +by (unfold FP_def stable_def constrains_def st_set_def, blast) + +ML +{* +val FP_Orig_type = thm "FP_Orig_type"; +val st_set_FP_Orig = thm "st_set_FP_Orig"; +val FP_type = thm "FP_type"; +val st_set_FP = thm "st_set_FP"; +val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; +val FP_Orig_weakest2 = thm "FP_Orig_weakest2"; +val stable_FP_Int = thm "stable_FP_Int"; +val FP_subset_FP_Orig = thm "FP_subset_FP_Orig"; +val FP_Orig_subset_FP = thm "FP_Orig_subset_FP"; +val FP_equivalence = thm "FP_equivalence"; +val FP_weakest = thm "FP_weakest"; +val Diff_FP = thm "Diff_FP"; +*} end diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Follows.ML --- a/src/ZF/UNITY/Follows.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Follows.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/Follows - ID: $Id$ + ID: $Id \\ Follows.ML,v 1.4 2003/06/27 16:40:25 paulson Exp $ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge @@ -9,30 +9,30 @@ (*Does this hold for "invariant"?*) val prems = -Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')"; +Goal "[|A=A'; r=r'; !!x. x \\ state ==> f(x)=f'(x); !!x. x \\ state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')"; by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1); qed "Follows_cong"; Goalw [mono1_def, metacomp_def] -"[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \ -\ Always({x:state. :r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})"; +"[| mono1(A, r, B, s, h); \\x \\ state. f(x):A & g(x):A |] ==> \ +\ Always({x \\ state. \\ r})<=Always({x \\ state. <(h comp f)(x), (h comp g)(x)> \\ s})"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable])); qed "subset_Always_comp"; Goal -"[| F:Always({x:state. :r}); \ -\ mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \ -\ F:Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})"; +"[| F \\ Always({x \\ state. \\ r}); \ +\ mono1(A, r, B, s, h); \\x \\ state. f(x):A & g(x):A |] ==> \ +\ F \\ Always({x \\ state. <(h comp f)(x), (h comp g)(x)> \\ s})"; by (blast_tac (claset() addIs [subset_Always_comp RS subsetD]) 1); qed "imp_Always_comp"; Goal -"[| F:Always({x:state. :r}); \ -\ F:Always({x:state. :s}); \ +"[| F \\ Always({x \\ state. \\ r}); \ +\ F \\ Always({x \\ state. \\ s}); \ \ mono2(A, r, B, s, C, t, h); \ -\ ALL x:state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \ -\ ==> F:Always({x:state. :t})"; +\ \\x \\ state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \ +\ ==> F \\ Always({x \\ state. \\ t})"; by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable, mono2_def])); by (auto_tac (claset() addSDs [subsetD], simpset())); @@ -42,9 +42,9 @@ Goalw [mono1_def, metacomp_def] "[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \ -\ ALL x:state. f(x):A & g(x):A |] ==> \ -\ (INT j:A. {s:state. :r} LeadsTo {s:state. :r}) <= \ -\(INT k:B. {x:state. :s} LeadsTo {x:state. :s})"; +\ \\x \\ state. f(x):A & g(x):A |] ==> \ +\ (\\j \\ A. {s \\ state. \\ r} LeadsTo {s \\ state. \\ r}) <= \ +\(\\k \\ B. {x \\ state. \\ s} LeadsTo {x \\ state. \\ s})"; by (Clarify_tac 1); by (ALLGOALS(full_simp_tac (simpset() addsimps [INT_iff]))); by Auto_tac; @@ -61,20 +61,20 @@ qed "subset_LeadsTo_comp"; Goal -"[| F:(INT j:A. {s:state. :r} LeadsTo {s:state. :r}); \ +"[| F:(\\j \\ A. {s \\ state. \\ r} LeadsTo {s \\ state. \\ r}); \ \ mono1(A, r, B, s, h); refl(A,r); trans[B](s); \ -\ ALL x:state. f(x):A & g(x):A |] ==> \ -\ F:(INT k:B. {x:state. :s} LeadsTo {x:state. :s})"; +\ \\x \\ state. f(x):A & g(x):A |] ==> \ +\ F:(\\k \\ B. {x \\ state. \\ s} LeadsTo {x \\ state. \\ s})"; by (rtac (subset_LeadsTo_comp RS subsetD) 1); by Auto_tac; qed "imp_LeadsTo_comp"; Goalw [mono2_def, Increasing_def] -"[| F:Increasing(B, s, g); \ -\ ALL j:A. F: {s:state. :r} LeadsTo {s:state. :r}; \ +"[| F \\ Increasing(B, s, g); \ +\ \\j \\ A. F: {s \\ state. \\ r} LeadsTo {s \\ state. \\ r}; \ \ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t); \ -\ ALL x:state. f1(x):A & f(x):A & g(x):B; k:C |] ==> \ -\ F:{x:state. :t} LeadsTo {x:state. :t}"; +\ \\x \\ state. f1(x):A & f(x):A & g(x):B; k \\ C |] ==> \ +\ F:{x \\ state. \\ t} LeadsTo {x \\ state. \\ t}"; by (rtac single_LeadsTo_I 1); by Auto_tac; by (dres_inst_tac [("x", "g(sa)"), ("A","B")] bspec 1); @@ -97,11 +97,11 @@ qed "imp_LeadsTo_comp_right"; Goalw [mono2_def, Increasing_def] -"[| F:Increasing(A, r, f); \ -\ ALL j:B. F: {x:state. :s} LeadsTo {x:state. :s}; \ +"[| F \\ Increasing(A, r, f); \ +\ \\j \\ B. F: {x \\ state. \\ s} LeadsTo {x \\ state. \\ s}; \ \ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \ -\ ALL x:state. f(x):A & g1(x):B & g(x):B; k:C |] ==> \ -\ F:{x:state. :t} LeadsTo {x:state. :t}"; +\ \\x \\ state. f(x):A & g1(x):B & g(x):B; k \\ C |] ==> \ +\ F:{x \\ state. \\ t} LeadsTo {x \\ state. \\ t}"; by (rtac single_LeadsTo_I 1); by Auto_tac; by (dres_inst_tac [("x", "f(sa)"),("P","%k. F \\ Stable(?X(k))")] bspec 1); @@ -124,13 +124,13 @@ (** This general result is used to prove Follows Un, munion, etc. **) Goal -"[| F:Increasing(A, r, f1) Int Increasing(B, s, g); \ -\ ALL j:A. F: {s:state. :r} LeadsTo {s:state. :r}; \ -\ ALL j:B. F: {x:state. :s} LeadsTo {x:state. :s}; \ +"[| F \\ Increasing(A, r, f1) Int Increasing(B, s, g); \ +\ \\j \\ A. F: {s \\ state. \\ r} LeadsTo {s \\ state. \\ r}; \ +\ \\j \\ B. F: {x \\ state. \\ s} LeadsTo {x \\ state. \\ s}; \ \ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \ -\ ALL x:state. f(x):A & g1(x):B & f1(x):A &g(x):B; k:C |]\ -\ ==> F:{x:state. :t} LeadsTo {x:state. :t}"; -by (res_inst_tac [("B", "{x:state. :t}")] LeadsTo_Trans 1); +\ \\x \\ state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \\ C |]\ +\ ==> F:{x \\ state. \\ t} LeadsTo {x \\ state. \\ t}"; +by (res_inst_tac [("B", "{x \\ state. \\ t}")] LeadsTo_Trans 1); by (blast_tac (claset() addIs [imp_LeadsTo_comp_right]) 1); by (blast_tac (claset() addIs [imp_LeadsTo_comp_left]) 1); qed "imp_LeadsTo_comp2"; @@ -140,19 +140,19 @@ by (blast_tac (claset() addDs [Increasing_type RS subsetD]) 1); qed "Follows_type"; -Goal "F:Follows(A, r, f, g) ==> F:program"; +Goal "F \\ Follows(A, r, f, g) ==> F \\ program"; by (blast_tac (claset() addDs [Follows_type RS subsetD]) 1); qed "Follows_into_program"; AddTCs [Follows_into_program]; Goalw [Follows_def] -"F:Follows(A, r, f, g)==> \ -\ F:program & (EX a. a:A) & (ALL x:state. f(x):A & g(x):A)"; +"F \\ Follows(A, r, f, g)==> \ +\ F \\ program & (\\a. a \\ A) & (\\x \\ state. f(x):A & g(x):A)"; by (blast_tac (claset() addDs [IncreasingD]) 1); qed "FollowsD"; Goalw [Follows_def] - "[| F:program; c:A; refl(A, r) |] ==> F:Follows(A, r, %x. c, %x. c)"; + "[| F \\ program; c \\ A; refl(A, r) |] ==> F \\ Follows(A, r, %x. c, %x. c)"; by Auto_tac; by (auto_tac (claset(), simpset() addsimps [refl_def])); qed "Follows_constantI"; @@ -171,19 +171,19 @@ qed "subset_Follows_comp"; Goal -"[| F:Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \ -\ ==> F:Follows(B, s, h comp f, h comp g)"; +"[| F \\ Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \ +\ ==> F \\ Follows(B, s, h comp f, h comp g)"; by (blast_tac (claset() addIs [subset_Follows_comp RS subsetD]) 1); qed "imp_Follows_comp"; -(* 2-place monotone operation: this general result is used to prove Follows_Un, Follows_munion *) +(* 2-place monotone operation \\ this general result is used to prove Follows_Un, Follows_munion *) -(* 2-place monotone operation: this general result is +(* 2-place monotone operation \\ this general result is used to prove Follows_Un, Follows_munion *) Goalw [Follows_def] -"[| F:Follows(A, r, f1, f); F:Follows(B, s, g1, g); \ +"[| F \\ Follows(A, r, f1, f); F \\ Follows(B, s, g1, g); \ \ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |] \ -\ ==> F:Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"; +\ ==> F \\ Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"; by (Clarify_tac 1); by (forw_inst_tac [("f", "g")] IncreasingD 1); by (forw_inst_tac [("f", "f")] IncreasingD 1); @@ -206,15 +206,15 @@ by (REPEAT(blast_tac (claset() addDs [IncreasingD]) 1)); qed "imp_Follows_comp2"; -Goal "[| F : Follows(A, r, f, g); F: Follows(A,r, g, h); \ -\ trans[A](r) |] ==> F : Follows(A, r, f, h)"; +Goal "[| F \\ Follows(A, r, f, g); F \\ Follows(A,r, g, h); \ +\ trans[A](r) |] ==> F \\ Follows(A, r, f, h)"; by (forw_inst_tac [("f", "f")] FollowsD 1); by (forw_inst_tac [("f", "g")] FollowsD 1); by (rewrite_goal_tac [Follows_def] 1); by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable, INT_iff]) 1); by Auto_tac; -by (res_inst_tac [("B", "{s:state. :r}")] LeadsTo_Trans 2); +by (res_inst_tac [("B", "{s \\ state. \\ r}")] LeadsTo_Trans 2); by (res_inst_tac [("b", "g(x)")] trans_onD 1); by (REPEAT(Blast_tac 1)); qed "Follows_trans"; @@ -222,46 +222,46 @@ (** Destruction rules for Follows **) Goalw [Follows_def] - "F : Follows(A, r, f,g) ==> F:Increasing(A, r, f)"; + "F \\ Follows(A, r, f,g) ==> F \\ Increasing(A, r, f)"; by (Blast_tac 1); qed "Follows_imp_Increasing_left"; Goalw [Follows_def] - "F : Follows(A, r, f,g) ==> F:Increasing(A, r, g)"; + "F \\ Follows(A, r, f,g) ==> F \\ Increasing(A, r, g)"; by (Blast_tac 1); qed "Follows_imp_Increasing_right"; Goalw [Follows_def] - "F :Follows(A, r, f, g) ==> F:Always({s:state. :r})"; + "F :Follows(A, r, f, g) ==> F \\ Always({s \\ state. \\ r})"; by (Blast_tac 1); qed "Follows_imp_Always"; Goalw [Follows_def] - "[| F:Follows(A, r, f, g); k:A |] ==> \ -\ F: {s:state. :r } LeadsTo {s:state. :r}"; + "[| F \\ Follows(A, r, f, g); k \\ A |] ==> \ +\ F: {s \\ state. \\ r } LeadsTo {s \\ state. \\ r}"; by (Blast_tac 1); qed "Follows_imp_LeadsTo"; -Goal "[| F : Follows(list(nat), gen_prefix(nat, Le), f, g); k:list(nat) |] \ -\ ==> F : {s:state. k pfixLe g(s)} LeadsTo {s:state. k pfixLe f(s)}"; +Goal "[| F \\ Follows(list(nat), gen_prefix(nat, Le), f, g); k \\ list(nat) |] \ +\ ==> F \\ {s \\ state. k pfixLe g(s)} LeadsTo {s \\ state. k pfixLe f(s)}"; by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1); qed "Follows_LeadsTo_pfixLe"; -Goal "[| F : Follows(list(nat), gen_prefix(nat, Ge), f, g); k:list(nat) |] \ -\ ==> F : {s:state. k pfixGe g(s)} LeadsTo {s:state. k pfixGe f(s)}"; +Goal "[| F \\ Follows(list(nat), gen_prefix(nat, Ge), f, g); k \\ list(nat) |] \ +\ ==> F \\ {s \\ state. k pfixGe g(s)} LeadsTo {s \\ state. k pfixGe f(s)}"; by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1); qed "Follows_LeadsTo_pfixGe"; Goalw [Follows_def, Increasing_def, Stable_def] -"[| F:Always({s:state. f(s) = g(s)}); F:Follows(A, r, f, h); \ -\ ALL x:state. g(x):A |] ==> F : Follows(A, r, g, h)"; +"[| F \\ Always({s \\ state. f(s) = g(s)}); F \\ Follows(A, r, f, h); \ +\ \\x \\ state. g(x):A |] ==> F \\ Follows(A, r, g, h)"; by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); by Auto_tac; -by (res_inst_tac [("C", "{s:state. f(s)=g(s)}"), - ("A", "{s:state. :r}"), - ("A'", "{s:state. :r}")] Always_LeadsTo_weaken 3); -by (eres_inst_tac [("A", "{s:state. :r}"), - ("A'", "{s:state. :r}")] +by (res_inst_tac [("C", "{s \\ state. f(s)=g(s)}"), + ("A", "{s \\ state. \\ r}"), + ("A'", "{s \\ state. \\ r}")] Always_LeadsTo_weaken 3); +by (eres_inst_tac [("A", "{s \\ state. \\ r}"), + ("A'", "{s \\ state. \\ r}")] Always_Constrains_weaken 1); by Auto_tac; by (dtac Always_Int_I 1); @@ -271,16 +271,16 @@ qed "Always_Follows1"; Goalw [Follows_def, Increasing_def, Stable_def] -"[| F : Always({s:state. g(s) = h(s)}); \ -\ F: Follows(A, r, f, g); ALL x:state. h(x):A |] ==> F : Follows(A, r, f, h)"; +"[| F \\ Always({s \\ state. g(s) = h(s)}); \ +\ F \\ Follows(A, r, f, g); \\x \\ state. h(x):A |] ==> F \\ Follows(A, r, f, h)"; by (full_simp_tac (simpset() addsimps [INT_iff]) 1); by Auto_tac; -by (thin_tac "k:A" 3); -by (res_inst_tac [("C", "{s:state. g(s)=h(s)}"), - ("A", "{s:state. :r}"), - ("A'", "{s:state. :r}")] Always_LeadsTo_weaken 3); -by (eres_inst_tac [("A", "{s:state. :r}"), - ("A'", "{s:state. :r}")] +by (thin_tac "k \\ A" 3); +by (res_inst_tac [("C", "{s \\ state. g(s)=h(s)}"), + ("A", "{s \\ state. \\ r}"), + ("A'", "{s \\ state. \\ r}")] Always_LeadsTo_weaken 3); +by (eres_inst_tac [("A", "{s \\ state. \\ r}"), + ("A'", "{s \\ state. \\ r}")] Always_Constrains_weaken 1); by Auto_tac; by (dtac Always_Int_I 1); @@ -311,31 +311,31 @@ qed "part_order_SetLe"; Addsimps [part_order_SetLe]; -Goal "[| F: Increasing.increasing(Pow(A), SetLe(A), f); \ -\ F: Increasing.increasing(Pow(A), SetLe(A), g) |] \ -\ ==> F : Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"; +Goal "[| F \\ Increasing.increasing(Pow(A), SetLe(A), f); \ +\ F \\ Increasing.increasing(Pow(A), SetLe(A), g) |] \ +\ ==> F \\ Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"; by (res_inst_tac [("h", "op Un")] imp_increasing_comp2 1); by Auto_tac; qed "increasing_Un"; -Goal "[| F: Increasing(Pow(A), SetLe(A), f); \ -\ F: Increasing(Pow(A), SetLe(A), g) |] \ -\ ==> F : Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"; +Goal "[| F \\ Increasing(Pow(A), SetLe(A), f); \ +\ F \\ Increasing(Pow(A), SetLe(A), g) |] \ +\ ==> F \\ Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"; by (res_inst_tac [("h", "op Un")] imp_Increasing_comp2 1); by Auto_tac; qed "Increasing_Un"; -Goal "[| F:Always({s:state. f1(s) <= f(s)}); \ -\ F : Always({s:state. g1(s) <= g(s)}) |] \ -\ ==> F : Always({s:state. f1(s) Un g1(s) <= f(s) Un g(s)})"; +Goal "[| F \\ Always({s \\ state. f1(s) <= f(s)}); \ +\ F \\ Always({s \\ state. g1(s) <= g(s)}) |] \ +\ ==> F \\ Always({s \\ state. f1(s) Un g1(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"; Goal -"[| F:Follows(Pow(A), SetLe(A), f1, f); \ -\ F:Follows(Pow(A), SetLe(A), g1, g) |] \ -\ ==> F:Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"; +"[| F \\ Follows(Pow(A), SetLe(A), f1, f); \ +\ F \\ Follows(Pow(A), SetLe(A), g1, g) |] \ +\ ==> F \\ Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"; by (res_inst_tac [("h", "op Un")] imp_Follows_comp2 1); by Auto_tac; qed "Follows_Un"; @@ -348,13 +348,13 @@ Addsimps [refl_MultLe]; Goalw [MultLe_def, id_def, lam_def] - "[| multiset(M); mset_of(M)<=A |] ==> :MultLe(A, r)"; + "[| multiset(M); mset_of(M)<=A |] ==> \\ MultLe(A, r)"; by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "MultLe_refl1"; Addsimps [MultLe_refl1]; Goalw [MultLe_def, id_def, lam_def] - "M:Mult(A) ==> :MultLe(A, r)"; + "M \\ Mult(A) ==> \\ MultLe(A, r)"; by Auto_tac; qed "MultLe_refl2"; Addsimps [MultLe_refl2]; @@ -370,7 +370,7 @@ by Auto_tac; qed "MultLe_type"; -Goal "[| :MultLe(A, r); :MultLe(A, r) |] ==> :MultLe(A,r)"; +Goal "[| \\ MultLe(A, r); \\ MultLe(A, r) |] ==> \\ MultLe(A,r)"; by (cut_facts_tac [inst "A" "A" trans_on_MultLe] 1); by (dtac trans_onD 1); by (assume_tac 1); @@ -406,23 +406,23 @@ Addsimps [part_order_MultLe]; Goalw [MultLe_def] -"[| multiset(M); mset_of(M)<= A|] ==> <0, M>:MultLe(A, r)"; +"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \\ MultLe(A, r)"; by (case_tac "M=0" 1); by (auto_tac (claset(), simpset() addsimps (thms"FiniteFun.intros"))); -by (subgoal_tac "<0 +# 0, 0 +# M>:multirel(A, r - id(A))" 1); +by (subgoal_tac "<0 +# 0, 0 +# M> \\ multirel(A, r - id(A))" 1); by (rtac one_step_implies_multirel 2); by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset])); qed "empty_le_MultLe"; Addsimps [empty_le_MultLe]; -Goal "M:Mult(A) ==> <0, M>:MultLe(A, r)"; +Goal "M \\ Mult(A) ==> <0, M> \\ MultLe(A, r)"; by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1); qed "empty_le_MultLe2"; Addsimps [empty_le_MultLe2]; Goalw [MultLe_def] -"[| :MultLe(A, r); :MultLe(A, r) |] ==>\ -\ :MultLe(A, r)"; +"[| \\ MultLe(A, r); \\ MultLe(A, r) |] ==>\ +\ \\ MultLe(A, r)"; by (auto_tac (claset() addIs [munion_multirel_mono1, munion_multirel_mono2, munion_multirel_mono, @@ -430,25 +430,25 @@ simpset() addsimps [Mult_iff_multiset])); qed "munion_mono"; -Goal "[| F:Increasing.increasing(Mult(A), MultLe(A,r), f); \ -\ F:Increasing.increasing(Mult(A), MultLe(A,r), g) |] \ -\ ==> F : Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"; +Goal "[| F \\ Increasing.increasing(Mult(A), MultLe(A,r), f); \ +\ F \\ Increasing.increasing(Mult(A), MultLe(A,r), g) |] \ +\ ==> F \\ Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"; by (res_inst_tac [("h", "munion")] imp_increasing_comp2 1); by Auto_tac; qed "increasing_munion"; -Goal "[| F:Increasing(Mult(A), MultLe(A,r), f); \ -\ F:Increasing(Mult(A), MultLe(A,r), g)|] \ -\ ==> F : Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"; +Goal "[| F \\ Increasing(Mult(A), MultLe(A,r), f); \ +\ F \\ Increasing(Mult(A), MultLe(A,r), g)|] \ +\ ==> F \\ Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"; by (res_inst_tac [("h", "munion")] imp_Increasing_comp2 1); by Auto_tac; qed "Increasing_munion"; Goal -"[| F:Always({s:state. :MultLe(A,r)}); \ -\ F:Always({s:state. :MultLe(A,r)});\ -\ ALL x:state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \ -\ ==> F : Always({s:state. :MultLe(A,r)})"; +"[| F \\ Always({s \\ state. \\ MultLe(A,r)}); \ +\ F \\ Always({s \\ state. \\ MultLe(A,r)});\ +\ \\x \\ state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \ +\ ==> F \\ Always({s \\ state. \\ MultLe(A,r)})"; by (res_inst_tac [("h", "munion")] imp_Always_comp2 1); by (ALLGOALS(Asm_full_simp_tac)); by (blast_tac (claset() addIs [munion_mono]) 1); @@ -456,9 +456,9 @@ qed "Always_munion"; Goal -"[| F:Follows(Mult(A), MultLe(A, r), f1, f); \ -\ F:Follows(Mult(A), MultLe(A, r), g1, g) |] \ -\ ==> F:Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"; +"[| F \\ Follows(Mult(A), MultLe(A, r), f1, f); \ +\ F \\ Follows(Mult(A), MultLe(A, r), g1, g) |] \ +\ ==> F \\ Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"; by (res_inst_tac [("h", "munion")] imp_Follows_comp2 1); by Auto_tac; qed "Follows_munion"; @@ -466,11 +466,11 @@ (** Used in ClientImp **) Goal -"!!f. [| ALL i:I. F : Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \ -\ ALL s. ALL i:I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & \ +"!!f. [| \\i \\ I. F \\ Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \ +\ \\s. \\i \\ I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & \ \ multiset(f(i, s)) & mset_of(f(i, s))<=A ; \ -\ Finite(I); F:program |] \ -\ ==> F : Follows(Mult(A), \ +\ Finite(I); F \\ program |] \ +\ ==> F \\ Follows(Mult(A), \ \ MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A), \ \ %x. msetsum(%i. f(i, x), I, A))"; by (etac rev_mp 1); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/GenPrefix.ML --- a/src/ZF/UNITY/GenPrefix.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/GenPrefix.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/GenPrefix.ML - ID: $Id$ + ID: $Id \\ GenPrefix.ML,v 1.8 2003/06/20 16:13:16 paulson Exp $ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge @@ -224,14 +224,14 @@ Addsimps [same_gen_prefix_gen_prefix]; Goal "[| xs \\ list(A); ys \\ list(A); y \\ A |] ==> \ -\ : gen_prefix(A,r) <-> \ +\ \\ gen_prefix(A,r) <-> \ \ (xs=[] | (\\z zs. xs=Cons(z,zs) & z \\ A & :r & \\ gen_prefix(A,r)))"; by (induct_tac "xs" 1); by Auto_tac; qed "gen_prefix_Cons"; Goal "[| refl(A,r); \\ gen_prefix(A, r); zs \\ list(A) |] \ -\ ==> : gen_prefix(A, r)"; +\ ==> \\ gen_prefix(A, r)"; by (etac gen_prefix.induct 1); by (Asm_simp_tac 1); by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD])); @@ -244,7 +244,7 @@ Goal "[| refl(A, r); \\ gen_prefix(A,r); \ \ length(xs) = length(ys); zs \\ list(A) |] \ -\ ==> : gen_prefix(A, r)"; +\ ==> \\ gen_prefix(A, r)"; by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1); by (REPEAT(assume_tac 1)); by (subgoal_tac "take(length(xs), ys)=ys" 1); @@ -326,7 +326,7 @@ by (force_tac (claset() addSIs [nat_0_le], simpset() addsimps [lt_nat_in_nat]) 1); qed_spec_mp "nth_imp_gen_prefix"; -Goal "( : gen_prefix(A,r)) <-> \ +Goal "( \\ gen_prefix(A,r)) <-> \ \ (xs \\ list(A) & ys \\ list(A) & length(xs) \\ length(ys) & \ \ (\\i. i < length(xs) --> : r))"; by (rtac iffI 1); @@ -436,7 +436,7 @@ qed "prefix_length_le"; Goalw [prefix_def] -" \\ prefix(A) ==> xs~=ys --> length(xs) < length(ys)"; +" \\ prefix(A) ==> xs\\ys --> length(xs) < length(ys)"; by (etac gen_prefix.induct 1); by (Clarify_tac 1); by (ALLGOALS(subgoal_tac "ys \\ list(A)&xs \\ list(A)")); @@ -532,7 +532,7 @@ qed "common_prefix_linear"; -(*** pfixLe, pfixGe: properties inherited from the translations ***) +(*** pfixLe, pfixGe \\ properties inherited from the translations ***) @@ -618,7 +618,7 @@ by (rtac (gen_prefix_mono RS subsetD) 1); by Auto_tac; qed "prefix_imp_pfixGe"; -(* Added by Sidi: prefix and take *) +(* Added by Sidi \\ prefix and take *) Goalw [prefix_def] " \\ prefix(A) ==> xs = take(length(xs), ys)"; diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Guar.ML --- a/src/ZF/UNITY/Guar.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Guar.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/Guar.ML - ID: $Id$ + ID: $Id \\ Guar.ML,v 1.8 2003/06/27 11:15:41 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge @@ -12,7 +12,7 @@ *) Goal "OK(cons(i, I), F) <-> \ -\ (i:I & OK(I, F)) | (i~:I & OK(I, F) & F(i) ok JOIN(I,F))"; +\ (i \\ I & OK(I, F)) | (i\\I & OK(I, F) & F(i) ok JOIN(I,F))"; by (asm_full_simp_tac (simpset() addsimps [OK_iff_ok]) 1); (** Auto_tac proves the goal in one-step, but takes more time **) by Safe_tac; @@ -23,13 +23,13 @@ (*** existential properties ***) -Goalw [ex_prop_def] "ex_prop(X) ==> X<=program"; +Goalw [ex_prop_def] "ex_prop(X) ==> X\\program"; by (Asm_simp_tac 1); qed "ex_imp_subset_program"; Goalw [ex_prop_def] - "GG:Fin(program) ==> (ex_prop(X) \ -\ --> GG Int X~=0 --> OK(GG, (%G. G)) -->(JN G:GG. G):X)"; + "GG \\ Fin(program) ==> (ex_prop(X) \ +\ --> GG Int X\\0 --> OK(GG, (%G. G)) -->(\\G \\ GG. G):X)"; by (etac Fin_induct 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_cons_iff]))); @@ -40,8 +40,8 @@ qed_spec_mp "ex1"; Goalw [ex_prop_def] -"X<=program ==> \ -\(ALL GG. GG:Fin(program) & GG Int X ~= 0 --> OK(GG,(%G. G))-->(JN G:GG. G):X)\ +"X\\program ==> \ +\(\\GG. GG \\ Fin(program) & GG Int X \\ 0 --> OK(GG,(%G. G))-->(\\G \\ GG. G):X)\ \ --> ex_prop(X)"; by (Clarify_tac 1); by (dres_inst_tac [("x", "{F,G}")] spec 1); @@ -52,8 +52,8 @@ (*Chandy & Sanders take this as a definition*) -Goal "ex_prop(X) <-> (X<=program & \ -\ (ALL GG. GG:Fin(program) & GG Int X ~= 0& OK(GG,( %G. G))-->(JN G:GG. G):X))"; +Goal "ex_prop(X) <-> (X\\program & \ +\ (\\GG. GG \\ Fin(program) & GG Int X \\ 0& OK(GG,( %G. G))-->(\\G \\ GG. G):X))"; by Auto_tac; by (ALLGOALS(blast_tac (claset() addIs [ex1, ex2 RS mp] addDs [ex_imp_subset_program]))); @@ -62,7 +62,7 @@ (* Equivalent definition of ex_prop given at the end of section 3*) Goalw [ex_prop_def, component_of_def] "ex_prop(X) <-> \ -\ X<=program & (ALL G:program. (G:X <-> (ALL H:program. (G component_of H) --> H:X)))"; +\ X\\program & (\\G \\ program. (G \\ X <-> (\\H \\ program. (G component_of H) --> H \\ X)))"; by Safe_tac; by (stac Join_commute 4); by (dtac ok_sym 4); @@ -74,21 +74,21 @@ (*** universal properties ***) -Goalw [uv_prop_def] "uv_prop(X)==> X<=program"; +Goalw [uv_prop_def] "uv_prop(X)==> X\\program"; by (Asm_simp_tac 1); qed "uv_imp_subset_program"; Goalw [uv_prop_def] - "GG:Fin(program) ==> \ -\ (uv_prop(X)--> GG <= X & OK(GG, (%G. G)) --> (JN G:GG. G):X)"; + "GG \\ Fin(program) ==> \ +\ (uv_prop(X)--> GG \\ X & OK(GG, (%G. G)) --> (\\G \\ GG. G):X)"; by (etac Fin_induct 1); by (auto_tac (claset(), simpset() addsimps [OK_cons_iff])); qed_spec_mp "uv1"; Goalw [uv_prop_def] -"X<=program ==> (ALL GG. GG:Fin(program) & GG <= X & OK(GG,(%G. G)) \ -\ --> (JN G:GG. G):X) --> uv_prop(X)"; +"X\\program ==> (\\GG. GG \\ Fin(program) & GG \\ X & OK(GG,(%G. G)) \ +\ --> (\\G \\ GG. G):X) --> uv_prop(X)"; by Auto_tac; by (Clarify_tac 2); by (dres_inst_tac [("x", "{F,G}")] spec 2); @@ -99,8 +99,8 @@ (*Chandy & Sanders take this as a definition*) Goal -"uv_prop(X) <-> X<=program & \ -\ (ALL GG. GG:Fin(program) & GG <= X & OK(GG, %G. G) --> (JN G:GG. G): X)"; +"uv_prop(X) <-> X\\program & \ +\ (\\GG. GG \\ Fin(program) & GG \\ X & OK(GG, %G. G) --> (\\G \\ GG. G): X)"; by Auto_tac; by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp] addDs [uv_imp_subset_program]) 1)); @@ -108,41 +108,41 @@ (*** guarantees ***) val major::prems = Goal - "[| (!!G. [| F ok G; F Join G:X; G:program |] ==> F Join G : Y); F:program |] \ -\ ==> F : X guarantees Y"; + "[| (!!G. [| F ok G; F Join G \\ X; G \\ program |] ==> F Join G \\ Y); F \\ program |] \ +\ ==> F \\ X guarantees Y"; by (cut_facts_tac prems 1); by (simp_tac (simpset() addsimps [guar_def, component_def]) 1); by (blast_tac (claset() addIs [major]) 1); qed "guaranteesI"; Goalw [guar_def, component_def] - "[| F : X guarantees Y; F ok G; F Join G:X; G:program |] \ -\ ==> F Join G : Y"; + "[| F \\ X guarantees Y; F ok G; F Join G \\ X; G \\ program |] \ +\ ==> F Join G \\ Y"; by (Asm_full_simp_tac 1); qed "guaranteesD"; (*This version of guaranteesD matches more easily in the conclusion - The major premise can no longer be F<=H since we need to reason about G*) + The major premise can no longer be F\\H since we need to reason about G*) Goalw [guar_def] - "[| F : X guarantees Y; F Join G = H; H : X; F ok G; G:program |] \ -\ ==> H : Y"; + "[| F \\ X guarantees Y; F Join G = H; H \\ X; F ok G; G \\ program |] \ +\ ==> H \\ Y"; by (Blast_tac 1); qed "component_guaranteesD"; Goalw [guar_def] - "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; + "[| F \\ X guarantees X'; Y \\ X; X' \\ Y' |] ==> F \\ Y guarantees Y'"; by Auto_tac; qed "guarantees_weaken"; -Goalw [guar_def] "X <= Y \ +Goalw [guar_def] "X \\ Y \ \ ==> X guarantees Y = program"; by (Blast_tac 1); qed "subset_imp_guarantees_program"; (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) -Goalw [guar_def] "[| X <= Y; F:program |] \ -\ ==> F : X guarantees Y"; +Goalw [guar_def] "[| X \\ Y; F \\ program |] \ +\ ==> F \\ X guarantees Y"; by (Blast_tac 1); qed "subset_imp_guarantees"; @@ -189,7 +189,7 @@ (** Distributive laws. Re-orient to perform miniscoping **) Goalw [guar_def] - "i:I ==>(UN i:I. X(i)) guarantees Y = (INT i:I. X(i) guarantees Y)"; + "i \\ I ==>(\\i \\ I. X(i)) guarantees Y = (\\i \\ I. X(i) guarantees Y)"; by (rtac equalityI 1); by Safe_tac; by (Force_tac 2); @@ -204,7 +204,7 @@ qed "guarantees_Un_left"; Goalw [guar_def] - "i:I ==> X guarantees (INT i:I. Y(i)) = (INT i:I. X guarantees Y(i))"; + "i \\ I ==> X guarantees (\\i \\ I. Y(i)) = (\\i \\ I. X guarantees Y(i))"; by (rtac equalityI 1); by Safe_tac; by (REPEAT(Blast_tac 1)); @@ -215,13 +215,13 @@ by (Blast_tac 1); qed "guarantees_Int_right"; -Goal "[| F : Z guarantees X; F : Z guarantees Y |] \ -\ ==> F : Z guarantees (X Int Y)"; +Goal "[| F \\ Z guarantees X; F \\ Z guarantees Y |] \ +\ ==> F \\ Z guarantees (X Int Y)"; by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); qed "guarantees_Int_right_I"; -Goal "i:I==> (F : X guarantees (INT i:I. Y(i))) <-> \ -\ (ALL i:I. F : X guarantees Y(i))"; +Goal "i \\ I==> (F \\ X guarantees (\\i \\ I. Y(i))) <-> \ +\ (\\i \\ I. F \\ X guarantees Y(i))"; by (asm_simp_tac (simpset() addsimps [guarantees_INT_right, INT_iff]) 1); by (Blast_tac 1); qed "guarantees_INT_right_iff"; @@ -240,14 +240,14 @@ **) Goalw [guar_def] - "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ -\ ==> F : (V Int Y) guarantees Z"; + "[| F \\ V guarantees X; F \\ (X Int Y) guarantees Z |]\ +\ ==> F \\ (V Int Y) guarantees Z"; by (Blast_tac 1); qed "combining1"; Goalw [guar_def] - "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ -\ ==> F : V guarantees (X Un Z)"; + "[| F \\ V guarantees (X Un Y); F \\ Y guarantees Z |]\ +\ ==> F \\ V guarantees (X Un Z)"; by (Blast_tac 1); qed "combining2"; @@ -255,16 +255,16 @@ (** The following two follow Chandy-Sanders, but the use of object-quantifiers does not suit Isabelle... **) -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) +(*Premise should be (!!i. i \\ I ==> F \\ X guarantees Y i) *) Goalw [guar_def] - "[| ALL i:I. F : X guarantees Y(i); i:I |] \ -\ ==> F : X guarantees (INT i:I. Y(i))"; + "[| \\i \\ I. F \\ X guarantees Y(i); i \\ I |] \ +\ ==> F \\ X guarantees (\\i \\ I. Y(i))"; by (Blast_tac 1); qed "all_guarantees"; -(*Premises should be [| F: X guarantees Y i; i: I |] *) +(*Premises should be [| F \\ X guarantees Y i; i \\ I |] *) Goalw [guar_def] - "EX i:I. F : X guarantees Y(i) ==> F : X guarantees (UN i:I. Y(i))"; + "\\i \\ I. F \\ X guarantees Y(i) ==> F \\ X guarantees (\\i \\ I. Y(i))"; by (Blast_tac 1); qed "ex_guarantees"; @@ -272,7 +272,7 @@ (*** Additional guarantees laws, by lcp ***) Goalw [guar_def] - "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ + "[| F \\ U guarantees V; G \\ X guarantees Y; F ok G |] \ \ ==> F Join G: (U Int X) guarantees (V Int Y)"; by (Simp_tac 1); by Safe_tac; @@ -283,7 +283,7 @@ qed "guarantees_Join_Int"; Goalw [guar_def] - "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ + "[| F \\ U guarantees V; G \\ X guarantees Y; F ok G |] \ \ ==> F Join G: (U Un X) guarantees (V Un Y)"; by (Simp_tac 1); by Safe_tac; @@ -297,23 +297,23 @@ qed "guarantees_Join_Un"; Goalw [guar_def] - "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F); i:I |] \ -\ ==> (JN i:I. F(i)) : (INT i:I. X(i)) guarantees (INT i:I. Y(i))"; + "[| \\i \\ I. F(i) \\ X(i) guarantees Y(i); OK(I,F); i \\ I |] \ +\ ==> (\\i \\ I. F(i)) \\ (\\i \\ I. X(i)) guarantees (\\i \\ I. Y(i))"; by Safe_tac; by (Blast_tac 2); by (dres_inst_tac [("x", "xa")] bspec 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [INT_iff]))); by Safe_tac; by (rotate_tac ~1 1); -by (dres_inst_tac [("x", "(JN x:(I-{xa}). F(x)) Join G")] bspec 1); +by (dres_inst_tac [("x", "(\\x \\ (I-{xa}). F(x)) Join G")] bspec 1); by (auto_tac (claset() addIs [OK_imp_ok], simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); qed "guarantees_JN_INT"; Goalw [guar_def] - "[| ALL i:I. F(i) : X(i) guarantees Y(i); OK(I,F) |] \ -\ ==> JOIN(I,F) : (UN i:I. X(i)) guarantees (UN i:I. Y(i))"; + "[| \\i \\ I. F(i) \\ X(i) guarantees Y(i); OK(I,F) |] \ +\ ==> JOIN(I,F) \\ (\\i \\ I. X(i)) guarantees (\\i \\ I. Y(i))"; by Auto_tac; by (dres_inst_tac [("x", "y")] bspec 1); by (ALLGOALS(Asm_full_simp_tac)); @@ -329,21 +329,21 @@ (*** guarantees laws for breaking down the program, by lcp ***) Goalw [guar_def] - "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; + "[| F \\ X guarantees Y; F ok G |] ==> F Join G \\ X guarantees Y"; by (Simp_tac 1); by Safe_tac; by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); qed "guarantees_Join_I1"; -Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; +Goal "[| G \\ X guarantees Y; F ok G |] ==> F Join G \\ X guarantees Y"; by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, inst "G" "G" ok_commute]) 1); by (blast_tac (claset() addIs [guarantees_Join_I1]) 1); qed "guarantees_Join_I2"; Goalw [guar_def] - "[| i:I; F(i): X guarantees Y; OK(I,F) |] \ -\ ==> (JN i:I. F(i)) : X guarantees Y"; + "[| i \\ I; F(i): X guarantees Y; OK(I,F) |] \ +\ ==> (\\i \\ I. F(i)) \\ X guarantees Y"; by Safe_tac; by (dres_inst_tac [("x", "JOIN(I-{i},F) Join G")] bspec 1); by (Simp_tac 1); @@ -353,11 +353,11 @@ (*** well-definedness ***) -Goalw [welldef_def] "F Join G: welldef ==> programify(F): welldef"; +Goalw [welldef_def] "F Join G \\ welldef ==> programify(F): welldef"; by Auto_tac; qed "Join_welldef_D1"; -Goalw [welldef_def] "F Join G: welldef ==> programify(G): welldef"; +Goalw [welldef_def] "F Join G \\ welldef ==> programify(G): welldef"; by Auto_tac; qed "Join_welldef_D2"; @@ -369,36 +369,36 @@ (* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *) -Goalw [wg_def] "wg(F, X) <= program"; +Goalw [wg_def] "wg(F, X) \\ program"; by Auto_tac; qed "wg_type"; -Goalw [guar_def] "X guarantees Y <= program"; +Goalw [guar_def] "X guarantees Y \\ program"; by Auto_tac; qed "guarantees_type"; -Goalw [wg_def] "G:wg(F, X) ==> G:program & F:program"; +Goalw [wg_def] "G \\ wg(F, X) ==> G \\ program & F \\ program"; by Auto_tac; by (blast_tac (claset() addDs [guarantees_type RS subsetD]) 1); qed "wgD2"; Goalw [guar_def, component_of_def] -"(F:X guarantees Y) <-> \ -\ F:program & (ALL H:program. H:X --> (F component_of H --> H:Y))"; +"(F \\ X guarantees Y) <-> \ +\ F \\ program & (\\H \\ program. H \\ X --> (F component_of H --> H \\ Y))"; by Safe_tac; by (REPEAT(Force_tac 1)); qed "guarantees_equiv"; -Goalw [wg_def] "!!X. [| F:(X guarantees Y); X <= program |] ==> X <= wg(F,Y)"; +Goalw [wg_def] "!!X. [| F \\ (X guarantees Y); X \\ program |] ==> X \\ wg(F,Y)"; by Auto_tac; qed "wg_weakest"; Goalw [wg_def, guar_def] -"F:program ==> F:wg(F,Y) guarantees Y"; +"F \\ program ==> F \\ wg(F,Y) guarantees Y"; by (Blast_tac 1); qed "wg_guarantees"; -Goalw [wg_def] "(H: wg(F,X)) <-> ((F component_of H --> H:X) & F:program & H:program)"; +Goalw [wg_def] "(H \\ wg(F,X)) <-> ((F component_of H --> H \\ X) & F \\ program & H \\ program)"; by (simp_tac (simpset() addsimps [guarantees_equiv]) 1); by (rtac iffI 1); by Safe_tac; @@ -408,37 +408,37 @@ qed "wg_equiv"; Goal -"F component_of H ==> H:wg(F,X) <-> (H:X & F:program & H:program)"; +"F component_of H ==> H \\ wg(F,X) <-> (H \\ X & F \\ program & H \\ program)"; by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1); qed "component_of_wg"; Goal -"ALL FF:Fin(program). FF Int X ~= 0 --> OK(FF, %F. F) \ -\ --> (ALL F:FF. ((JN F:FF. F): wg(F,X)) <-> ((JN F:FF. F):X))"; +"\\FF \\ Fin(program). FF Int X \\ 0 --> OK(FF, %F. F) \ +\ --> (\\F \\ FF. ((\\F \\ FF. F): wg(F,X)) <-> ((\\F \\ FF. F):X))"; by (Clarify_tac 1); -by (subgoal_tac "F component_of (JN F:FF. F)" 1); +by (subgoal_tac "F component_of (\\F \\ FF. F)" 1); by (dres_inst_tac [("X", "X")] component_of_wg 1); by (force_tac (claset() addSDs [thm"Fin.dom_subset" RS subsetD RS PowD], simpset()) 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def]))); -by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1); +by (res_inst_tac [("x", "\\F \\ (FF-{F}). F")] exI 1); by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], simpset() addsimps [OK_iff_ok])); qed "wg_finite"; -(* "!!FF. [| FF:Fin(program); FF Int X ~=0; OK(FF, %F. F); G:FF |] +(* "!!FF. [| FF \\ Fin(program); FF Int X \\0; OK(FF, %F. F); G \\ FF |] ==> JOIN(FF, %F. F):wg(G, X) <-> JOIN(FF, %F. F):X" *) val wg_finite2 = wg_finite RS bspec RS mp RS mp RS bspec; -Goal "ex_prop(X) ==> (F:X) <-> (ALL H:program. H : wg(F,X) & F:program)"; +Goal "ex_prop(X) ==> (F \\ X) <-> (\\H \\ program. H \\ wg(F,X) & F \\ program)"; by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); by (Blast_tac 1); qed "wg_ex_prop"; (** From Charpentier and Chandy "Theorems About Composition" **) (* Proposition 2 *) -Goalw [wx_def] "wx(X)<=X"; +Goalw [wx_def] "wx(X)\\X"; by Auto_tac; qed "wx_subset"; @@ -450,13 +450,13 @@ by (REPEAT(Force_tac 1)); qed "wx_ex_prop"; -Goalw [wx_def] "ALL Z. Z<=program --> Z<= X --> ex_prop(Z) --> Z <= wx(X)"; +Goalw [wx_def] "\\Z. Z\\program --> Z\\ X --> ex_prop(Z) --> Z \\ wx(X)"; by Auto_tac; qed "wx_weakest"; (* Proposition 6 *) Goalw [ex_prop_def] - "ex_prop({F:program. ALL G:program. F ok G --> F Join G:X})"; + "ex_prop({F \\ program. \\G \\ program. F ok G --> F Join G \\ X})"; by Safe_tac; by (dres_inst_tac [("x", "G Join Ga")] bspec 1); by (Simp_tac 1); @@ -474,7 +474,7 @@ (* Equivalence with the other definition of wx *) Goalw [wx_def] - "wx(X) = {F:program. ALL G:program. F ok G --> (F Join G):X}"; + "wx(X) = {F \\ program. \\G \\ program. F ok G --> (F Join G):X}"; by (rtac equalityI 1); by Safe_tac; by (Blast_tac 1); @@ -486,7 +486,7 @@ by Safe_tac; by (Blast_tac 1); by (Blast_tac 1); -by (res_inst_tac [("B", "{F:program. ALL G:program. F ok G --> F Join G:X}")] +by (res_inst_tac [("B", "{F \\ program. \\G \\ program. F ok G --> F Join G \\ X}")] UnionI 1); by Safe_tac; by (rtac wx'_ex_prop 2); @@ -516,7 +516,7 @@ (* Rules given in section 7 of Chandy and Sander's Reasoning About Program composition paper *) -Goal "[| Init(F) <= A; F:program |] ==> F:(stable(A)) guarantees (Always(A))"; +Goal "[| Init(F) \\ A; F \\ program |] ==> F \\ stable(A) guarantees Always(A)"; by (rtac guaranteesI 1); by (assume_tac 2); by (simp_tac (simpset() addsimps [Join_commute]) 1); @@ -526,7 +526,7 @@ qed "stable_guarantees_Always"; (* To be moved to WFair.ML *) -Goal "[| F:A co A Un B; F:transient(A); st_set(B) |] ==> F:A leadsTo B"; +Goal "[| F \\ A co A Un B; F \\ transient(A); st_set(B) |] ==> F \\ A leadsTo B"; by (ftac constrainsD2 1); by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); @@ -534,7 +534,7 @@ by (ALLGOALS(Blast_tac)); qed "leadsTo_Basis'"; -Goal "[| F:transient(A); st_set(B) |] ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; +Goal "[| F \\ transient(A); st_set(B) |] ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; by (rtac guaranteesI 1); by (blast_tac (claset() addDs [transient_type RS subsetD]) 2); by (rtac leadsTo_Basis' 1); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Increasing.ML --- a/src/ZF/UNITY/Increasing.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Increasing.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/GenIncreasing - ID: $Id$ + ID: $Id \\ Increasing.ML,v 1.3 2003/06/27 16:40:25 paulson Exp $ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge @@ -12,25 +12,25 @@ by (Blast_tac 1); qed "increasing_type"; -Goalw [increasing_def] "F:increasing[A](r, f) ==> F:program"; +Goalw [increasing_def] "F \\ increasing[A](r, f) ==> F \\ program"; by (Blast_tac 1); qed "increasing_into_program"; Goalw [increasing_def] -"[| F:increasing[A](r, f); x:A |] ==>F:stable({s:state. :r})"; +"[| F \\ increasing[A](r, f); x \\ A |] ==>F \\ stable({s \\ state. :r})"; by (Blast_tac 1); qed "increasing_imp_stable"; Goalw [increasing_def] -"F:increasing[A](r,f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)"; -by (subgoal_tac "EX x. x:state" 1); +"F \\ increasing[A](r,f) ==> F \\ program & (\\a. a \\ A) & (\\s \\ state. f(s):A)"; +by (subgoal_tac "\\x. x \\ state" 1); by (auto_tac (claset() addDs [stable_type RS subsetD] addIs [st0_in_state], simpset())); qed "increasingD"; Goalw [increasing_def, stable_def] - "F:increasing[A](r, %s. c) <-> F:program & c:A"; -by (subgoal_tac "EX x. x:state" 1); + "F \\ increasing[A](r, %s. c) <-> F \\ program & c \\ A"; +by (subgoal_tac "\\x. x \\ state" 1); by (auto_tac (claset() addDs [stable_type RS subsetD] addIs [st0_in_state], simpset())); qed "increasing_constant"; @@ -43,7 +43,7 @@ by (Clarify_tac 1); by (Asm_full_simp_tac 1); by (Clarify_tac 1); -by (subgoal_tac "xa:state" 1); +by (subgoal_tac "xa \\ state" 1); by (blast_tac (claset() addSDs [ActsD]) 2); by (subgoal_tac ":r" 1); by (force_tac (claset(), simpset() addsimps [refl_def]) 2); @@ -59,8 +59,8 @@ by (ALLGOALS(Asm_simp_tac)); qed "subset_increasing_comp"; -Goal "[| F:increasing[A](r, f); mono1(A, r, B, s, g); \ -\ refl(A, r); trans[B](s) |] ==> F:increasing[B](s, g comp f)"; +Goal "[| F \\ increasing[A](r, f); mono1(A, r, B, s, g); \ +\ refl(A, r); trans[B](s) |] ==> F \\ increasing[B](s, g comp f)"; by (rtac (subset_increasing_comp RS subsetD) 1); by Auto_tac; qed "imp_increasing_comp"; @@ -80,7 +80,7 @@ (** Increasing **) Goalw [increasing_def, Increasing_def] - "F : increasing[A](r, f) ==> F : Increasing[A](r, f)"; + "F \\ increasing[A](r, f) ==> F \\ Increasing[A](r, f)"; by (auto_tac (claset() addIs [stable_imp_Stable], simpset())); qed "increasing_imp_Increasing"; @@ -88,24 +88,24 @@ by Auto_tac; qed "Increasing_type"; -Goalw [Increasing_def] "F:Increasing[A](r, f) ==> F:program"; +Goalw [Increasing_def] "F \\ Increasing[A](r, f) ==> F \\ program"; by Auto_tac; qed "Increasing_into_program"; Goalw [Increasing_def] -"[| F:Increasing[A](r, f); a:A |] ==> F: Stable({s:state. :r})"; +"[| F \\ Increasing[A](r, f); a \\ A |] ==> F \\ Stable({s \\ state. :r})"; by (Blast_tac 1); qed "Increasing_imp_Stable"; Goalw [Increasing_def] -"F:Increasing[A](r, f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)"; -by (subgoal_tac "EX x. x:state" 1); +"F \\ Increasing[A](r, f) ==> F \\ program & (\\a. a \\ A) & (\\s \\ state. f(s):A)"; +by (subgoal_tac "\\x. x \\ state" 1); by (auto_tac (claset() addIs [st0_in_state], simpset())); qed "IncreasingD"; Goal -"F:Increasing[A](r, %s. c) <-> F:program & (c:A)"; -by (subgoal_tac "EX x. x:state" 1); +"F \\ Increasing[A](r, %s. c) <-> F \\ program & (c \\ A)"; +by (subgoal_tac "\\x. x \\ state" 1); by (auto_tac (claset() addSDs [IncreasingD] addIs [st0_in_state, increasing_imp_Increasing], simpset())); @@ -118,7 +118,7 @@ \ Increasing[A](r, f) <= Increasing[B](s, g comp f)"; by Safe_tac; by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD]))); -by (subgoal_tac "xb:state & xa:state" 1); +by (subgoal_tac "xb \\ state & xa \\ state" 1); by (asm_simp_tac (simpset() addsimps [ActsD]) 2); by (subgoal_tac ":r" 1); by (force_tac (claset(), simpset() addsimps [refl_def]) 2); @@ -136,8 +136,8 @@ by (ALLGOALS(Asm_full_simp_tac)); qed "subset_Increasing_comp"; -Goal "[| F:Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] \ -\ ==> F:Increasing[B](s, g comp f)"; +Goal "[| F \\ Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] \ +\ ==> F \\ Increasing[B](s, g comp f)"; by (rtac (subset_Increasing_comp RS subsetD) 1); by Auto_tac; qed "imp_Increasing_comp"; @@ -158,14 +158,14 @@ Goalw [increasing_def, stable_def, part_order_def, constrains_def, mono2_def] -"[| F:increasing[A](r, f); F:increasing[B](s, g); \ +"[| F \\ increasing[A](r, f); F \\ increasing[B](s, g); \ \ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \ -\ F:increasing[C](t, %x. h(f(x), g(x)))"; +\ F \\ increasing[C](t, %x. h(f(x), g(x)))"; by (Clarify_tac 1); by (Asm_full_simp_tac 1); by (Clarify_tac 1); by (rename_tac "xa xb" 1); -by (subgoal_tac "xb:state & xa:state" 1); +by (subgoal_tac "xb \\ state & xa \\ state" 1); by (blast_tac (claset() addSDs [ActsD]) 2); by (subgoal_tac ":r & :s" 1); by (force_tac (claset(), simpset() addsimps [refl_def]) 2); @@ -194,12 +194,12 @@ Goalw [Increasing_def, stable_def, part_order_def, constrains_def, mono2_def, Stable_def, Constrains_def] -"[| F:Increasing[A](r, f); F:Increasing[B](s, g); \ +"[| F \\ Increasing[A](r, f); F \\ Increasing[B](s, g); \ \ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \ -\ F:Increasing[C](t, %x. h(f(x), g(x)))"; +\ F \\ Increasing[C](t, %x. h(f(x), g(x)))"; by Safe_tac; by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD]))); -by (subgoal_tac "xa:state & x:state" 1); +by (subgoal_tac "xa \\ state & x \\ state" 1); by (blast_tac (claset() addSDs [ActsD]) 2); by (subgoal_tac ":r & :s" 1); by (force_tac (claset(), simpset() addsimps [refl_def]) 2); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Monotonicity.ML --- a/src/ZF/UNITY/Monotonicity.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Monotonicity.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/Monotonicity.ML - ID: $Id$ + ID: $Id \\ Monotonicity.ML,v 1.2 2003/06/26 13:48:33 paulson Exp $ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2002 University of Cambridge @@ -12,12 +12,12 @@ *) Goalw [mono1_def] - "[| mono1(A, r, B, s, f); :r; x:A; y:A |] ==> :s"; + "[| mono1(A, r, B, s, f); :r; x \\ A; y \\ A |] ==> :s"; by Auto_tac; qed "mono1D"; Goalw [mono2_def] -"[| mono2(A, r, B, s, C, t, f); :r; :s; x:A; y:A; u:B; v:B |] ==> \ +"[| mono2(A, r, B, s, C, t, f); :r; :s; x \\ A; y \\ A; u \\ B; v \\ B |] ==> \ \ :t"; by Auto_tac; qed "mono2D"; @@ -26,7 +26,7 @@ (** Monotonicity of take **) (*????premises too strong*) -Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> :prefix(A)"; +Goal "[| i le j; xs \\ list(A); i \\ nat; j \\ nat |] ==> :prefix(A)"; by (case_tac "length(xs) le i" 1); by (subgoal_tac "length(xs) le j" 1); by (blast_tac (claset() addIs [le_trans]) 2); @@ -44,11 +44,11 @@ by (asm_full_simp_tac (simpset() addsimps [take_add, prefix_iff, take_type, drop_type]) 1); qed "take_mono_left"; -Goal "[| :prefix(A); i:nat |] ==> :prefix(A)"; +Goal "[| :prefix(A); i \\ nat |] ==> :prefix(A)"; by (auto_tac (claset(), simpset() addsimps [prefix_iff])); qed "take_mono_right"; -Goal "[| i le j; :prefix(A); i:nat; j:nat |] ==> :prefix(A)"; +Goal "[| i le j; :prefix(A); i \\ nat; j \\ nat |] ==> :prefix(A)"; by (res_inst_tac [("b", "take(j, xs)")] prefix_trans 1); by (auto_tac (claset() addDs [prefix_type RS subsetD] addIs [take_mono_left, take_mono_right], simpset())); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/MultisetSum.ML --- a/src/ZF/UNITY/MultisetSum.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/MultisetSum.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/MultusetSum.thy - ID: $Id$ + ID: $Id \\ MultisetSum.ML,v 1.2 2003/06/24 14:33:00 paulson Exp $ Author: Sidi O Ehmety Copyright: 2002 University of Cambridge Setsum for multisets. @@ -16,7 +16,7 @@ Addsimps [general_setsum_0]; Goalw [general_setsum_def] -"[| C:Fin(A); a:A; a~:C; e:B; ALL x:A. g(x):B; lcomm(B, B, f) |] ==> \ +"[| C \\ Fin(A); a \\ A; a\\C; e \\ B; \\x \\ A. g(x):B; lcomm(B, B, f) |] ==> \ \ general_setsum(cons(a, C), B, e, f, g) = \ \ f(g(a), general_setsum(C, B, e, f,g))"; by (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, @@ -45,7 +45,7 @@ (** msetsum **) Goal -"[| C:Fin(A); ALL x:A. multiset(g(x))& mset_of(g(x))<=B |] \ +"[| C \\ Fin(A); \\x \\ A. multiset(g(x))& mset_of(g(x))<=B |] \ \ ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\u v. u +# v, g))"; by (etac Fin_induct 1); by Auto_tac; @@ -59,7 +59,7 @@ Addsimps [msetsum_0]; Goalw [msetsum_def] -"[| C:Fin(A); a~:C; a:A; ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ +"[| C \\ Fin(A); a\\C; a \\ A; \\x \\ A. multiset(g(x)) & mset_of(g(x))<=B |] \ \ ==> msetsum(g, cons(a, C), B) = g(a) +# msetsum(g, C, B)"; by (stac general_setsum_cons 1); by (auto_tac (claset(), simpset() addsimps [multiset_general_setsum, Mult_iff_multiset])); @@ -73,7 +73,7 @@ qed "msetsum_multiset"; Goal -"[| C:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ +"[| C \\ Fin(A); \\x \\ A. multiset(g(x)) & mset_of(g(x))<=B |] \ \ ==> mset_of(msetsum(g, C, B))<=B"; by (etac Fin_induct 1); by Auto_tac; @@ -83,15 +83,15 @@ (*The reversed orientation looks more natural, but LOOPS as a simprule!*) Goal -"[| C:Fin(A); D:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ +"[| C \\ Fin(A); D \\ Fin(A); \\x \\ A. multiset(g(x)) & mset_of(g(x))<=B |] \ \ ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) \ \ = msetsum(g, C, B) +# msetsum(g, D, B)"; by (etac Fin_induct 1); by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 2); by (auto_tac (claset(), simpset() addsimps [msetsum_multiset])); -by (subgoal_tac "y Un D:Fin(A) & y Int D : Fin(A)" 1); +by (subgoal_tac "y Un D \\ Fin(A) & y Int D \\ Fin(A)" 1); by (Clarify_tac 1); -by (case_tac "x:D" 1); +by (case_tac "x \\ D" 1); by (subgoal_tac "cons(x, y) Int D = y Int D" 2); by (subgoal_tac "cons(x, y) Int D = cons(x, y Int D)" 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_absorb, @@ -101,34 +101,34 @@ qed "msetsum_Un_Int"; -Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; \ -\ ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ +Goal "[| C \\ Fin(A); D \\ Fin(A); C Int D = 0; \ +\ \\x \\ A. multiset(g(x)) & mset_of(g(x))<=B |] \ \ ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)"; by (stac (msetsum_Un_Int RS sym) 1); by (auto_tac (claset(), simpset() addsimps [msetsum_multiset])); qed "msetsum_Un_disjoint"; -Goal "I:Fin(A) ==> (ALL i:I. C(i):Fin(B)) --> (UN i:I. C(i)):Fin(B)"; +Goal "I \\ Fin(A) ==> (\\i \\ I. C(i):Fin(B)) --> (\\i \\ I. C(i)):Fin(B)"; by (etac Fin_induct 1); by Auto_tac; qed_spec_mp "UN_Fin_lemma"; -Goal "!!I. [| I:Fin(K); ALL i:K. C(i):Fin(A) |] ==> \ -\ (ALL x:A. multiset(f(x)) & mset_of(f(x))<=B) --> \ -\ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \ -\ msetsum(f, UN i:I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; +Goal "!!I. [| I \\ Fin(K); \\i \\ K. C(i):Fin(A) |] ==> \ +\ (\\x \\ A. multiset(f(x)) & mset_of(f(x))<=B) --> \ +\ (\\i \\ I. \\j \\ I. i\\j --> C(i) Int C(j) = 0) --> \ +\ msetsum(f, \\i \\ I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; by (etac Fin_induct 1); by (ALLGOALS(Clarify_tac)); by Auto_tac; -by (subgoal_tac "ALL i:y. x ~= i" 1); +by (subgoal_tac "\\i \\ y. x \\ i" 1); by (Blast_tac 2); -by (subgoal_tac "C(x) Int (UN i:y. C(i)) = 0" 1); +by (subgoal_tac "C(x) Int (\\i \\ y. C(i)) = 0" 1); by (Blast_tac 2); -by (subgoal_tac " (UN i:y. C(i)):Fin(A) & C(x):Fin(A)" 1); +by (subgoal_tac " (\\i \\ y. C(i)):Fin(A) & C(x):Fin(A)" 1); by (blast_tac (claset() addIs [UN_Fin_lemma] addDs [FinD]) 2); by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [msetsum_Un_disjoint]) 1); -by (subgoal_tac "ALL x:K. multiset(msetsum(f, C(x), B)) &\ +by (subgoal_tac "\\x \\ K. multiset(msetsum(f, C(x), B)) &\ \ mset_of(msetsum(f, C(x), B)) <= B" 1); by (Asm_simp_tac 1); by (Clarify_tac 1); @@ -137,11 +137,11 @@ qed_spec_mp "msetsum_UN_disjoint"; Goal -"[| C:Fin(A); \ -\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B; \ -\ ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\ +"[| C \\ Fin(A); \ +\ \\x \\ A. multiset(f(x)) & mset_of(f(x))<=B; \ +\ \\x \\ A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\ \ msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)"; -by (subgoal_tac "ALL x:A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1); +by (subgoal_tac "\\x \\ A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1); by (etac Fin_induct 1); by (ALLGOALS(Asm_simp_tac)); by (resolve_tac [trans] 1); @@ -153,7 +153,7 @@ val prems = Goal - "[| C=D; !!x. x:D ==> f(x) = g(x) |] ==> \ + "[| C=D; !!x. x \\ D ==> f(x) = g(x) |] ==> \ \ msetsum(f, C, B) = msetsum(g, D, B)"; by (asm_full_simp_tac (simpset() addsimps [msetsum_def, general_setsum_def]@prems addcongs [fold_cong]) 1); qed "msetsum_cong"; @@ -163,11 +163,11 @@ qed "multiset_union_diff"; -Goal "[| C:Fin(A); D:Fin(A); \ -\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B |] \ +Goal "[| C \\ Fin(A); D \\ Fin(A); \ +\ \\x \\ A. multiset(f(x)) & mset_of(f(x))<=B |] \ \ ==> msetsum(f, C Un D, B) = \ \ msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)"; -by (subgoal_tac "C Un D:Fin(A) & C Int D:Fin(A)" 1); +by (subgoal_tac "C Un D \\ Fin(A) & C Int D \\ Fin(A)" 1); by (Clarify_tac 1); by (stac (msetsum_Un_Int RS sym) 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps @@ -182,7 +182,7 @@ Addsimps [nsetsum_0]; Goalw [nsetsum_def, general_setsum_def] -"[| Finite(C); x~:C |] \ +"[| Finite(C); x\\C |] \ \ ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)"; by (auto_tac (claset(), simpset() addsimps [Finite_cons])); by (res_inst_tac [("A", "cons(x, C)")] (thm"fold_typing.fold_cons") 1); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Mutex.ML --- a/src/ZF/UNITY/Mutex.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Mutex.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,12 +1,12 @@ (* Title: ZF/UNITY/Mutex.ML - ID: $Id$ + ID: $Id \\ Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra Variables' types are introduced globally so that type verification -reduces to the usual ZF typechecking: an ill-tyed expression will +reduces to the usual ZF typechecking \\ an ill-tyed expression will reduce to the empty set. *) @@ -15,27 +15,27 @@ Addsimps [p_type, u_type, v_type, m_type, n_type]; -Goalw [state_def] "s:state ==>s`u:bool"; +Goalw [state_def] "s \\ state ==>s`u \\ bool"; by (dres_inst_tac [("a", "u")] apply_type 1); by Auto_tac; qed "u_value_type"; -Goalw [state_def] "s:state ==> s`v:bool"; +Goalw [state_def] "s \\ state ==> s`v \\ bool"; by (dres_inst_tac [("a", "v")] apply_type 1); by Auto_tac; qed "v_value_type"; -Goalw [state_def] "s:state ==> s`p:bool"; +Goalw [state_def] "s \\ state ==> s`p \\ bool"; by (dres_inst_tac [("a", "p")] apply_type 1); by Auto_tac; qed "p_value_type"; -Goalw [state_def] "s:state ==> s`m:int"; +Goalw [state_def] "s \\ state ==> s`m \\ int"; by (dres_inst_tac [("a", "m")] apply_type 1); by Auto_tac; qed "m_value_type"; -Goalw [state_def] "s:state ==>s`n:int"; +Goalw [state_def] "s \\ state ==>s`n \\ int"; by (dres_inst_tac [("a", "n")] apply_type 1); by Auto_tac; qed "n_value_type"; @@ -46,7 +46,7 @@ m_value_type, n_value_type]; (** Mutex is a program **) -Goalw [Mutex_def] "Mutex:program"; +Goalw [Mutex_def] "Mutex \\ program"; by Auto_tac; qed "Mutex_in_program"; Addsimps [Mutex_in_program]; @@ -64,17 +64,17 @@ Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]); -Goal "Mutex : Always(IU)"; +Goal "Mutex \\ Always(IU)"; by (always_tac 1); by Auto_tac; qed "IU"; -Goal "Mutex : Always(IV)"; +Goal "Mutex \\ Always(IV)"; by (always_tac 1); qed "IV"; -(*The safety property: mutual exclusion*) -Goal "Mutex : Always({s:state. ~(s`m = #3 & s`n = #3)})"; +(*The safety property \\ mutual exclusion*) +Goal "Mutex \\ Always({s \\ state. ~(s`m = #3 & s`n = #3)})"; by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1); by Auto_tac; qed "mutual_exclusion"; @@ -87,7 +87,7 @@ by Auto_tac; qed "less_lemma"; -Goal "Mutex : Always(bad_IU)"; +Goal "Mutex \\ Always(bad_IU)"; by (always_tac 1); by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless])); by (auto_tac (claset(), simpset() addsimps [bool_def])); @@ -96,37 +96,37 @@ by Auto_tac; by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1); by Auto_tac; -(*Resulting state: n=1, p=false, m=4, u=false. +(*Resulting state \\ n=1, p=false, m=4, u=false. Execution of V1 (the command of process v guarded by n=1) sets p:=true, violating the invariant!*) -(*Check that subgoals remain: proof failed.*) +(*Check that subgoals remain \\ proof failed.*) getgoal 1; (*** Progress for U ***) Goalw [Unless_def] -"Mutex : {s:state. s`m=#2} Unless {s:state. s`m=#3}"; +"Mutex \\ {s \\ state. s`m=#2} Unless {s \\ state. s`m=#3}"; by (constrains_tac 1); qed "U_F0"; -Goal "Mutex : {s:state. s`m=#1} LeadsTo {s:state. s`p = s`v & s`m = #2}"; +Goal "Mutex \\ {s \\ state. s`m=#1} LeadsTo {s \\ state. s`p = s`v & s`m = #2}"; by (ensures_tac "U1" 1); qed "U_F1"; -Goal "Mutex : {s:state. s`p =0 & s`m = #2} LeadsTo {s:state. s`m = #3}"; +Goal "Mutex \\ {s \\ state. s`p =0 & s`m = #2} LeadsTo {s \\ state. s`m = #3}"; by (cut_facts_tac [IU] 1); by (ensures_tac "U2" 1); qed "U_F2"; -Goal "Mutex : {s:state. s`m = #3} LeadsTo {s:state. s`p=1}"; -by (res_inst_tac [("B", "{s:state. s`m = #4}")] LeadsTo_Trans 1); +Goal "Mutex \\ {s \\ state. s`m = #3} LeadsTo {s \\ state. s`p=1}"; +by (res_inst_tac [("B", "{s \\ state. s`m = #4}")] LeadsTo_Trans 1); by (ensures_tac "U4" 2); by (ensures_tac "U3" 1); qed "U_F3"; -Goal "Mutex : {s:state. s`m = #2} LeadsTo {s:state. s`p=1}"; +Goal "Mutex \\ {s \\ state. s`m = #2} LeadsTo {s \\ state. s`p=1}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); @@ -134,12 +134,12 @@ by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def])); val U_lemma2 = result(); -Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`p =1}"; +Goal "Mutex \\ {s \\ state. s`m = #1} LeadsTo {s \\ state. s`p =1}"; by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); by Auto_tac; val U_lemma1 = result(); -Goal "i:int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"; +Goal "i \\ int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)"; by Auto_tac; by (auto_tac (claset(), simpset() addsimps [neq_iff_zless])); by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4); @@ -152,7 +152,7 @@ qed "eq_123"; -Goal "Mutex : {s:state. #1 $<= s`m & s`m $<= #3} LeadsTo {s:state. s`p=1}"; +Goal "Mutex \\ {s \\ state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \\ state. s`p=1}"; by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib, U_lemma1, U_lemma2, U_F3] ) 1); @@ -160,7 +160,7 @@ (*Misra's F4*) -Goal "Mutex : {s:state. s`u = 1} LeadsTo {s:state. s`p=1}"; +Goal "Mutex \\ {s \\ state. s`u = 1} LeadsTo {s \\ state. s`p=1}"; by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1); by Auto_tac; qed "u_Leadsto_p"; @@ -169,26 +169,26 @@ (*** Progress for V ***) Goalw [Unless_def] -"Mutex : {s:state. s`n=#2} Unless {s:state. s`n=#3}"; +"Mutex \\ {s \\ state. s`n=#2} Unless {s \\ state. s`n=#3}"; by (constrains_tac 1); qed "V_F0"; -Goal "Mutex : {s:state. s`n=#1} LeadsTo {s:state. s`p = not(s`u) & s`n = #2}"; +Goal "Mutex \\ {s \\ state. s`n=#1} LeadsTo {s \\ state. s`p = not(s`u) & s`n = #2}"; by (ensures_tac "V1" 1); qed "V_F1"; -Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}"; +Goal "Mutex \\ {s \\ state. s`p=1 & s`n = #2} LeadsTo {s \\ state. s`n = #3}"; by (cut_facts_tac [IV] 1); by (ensures_tac "V2" 1); qed "V_F2"; -Goal "Mutex : {s:state. s`n = #3} LeadsTo {s:state. s`p=0}"; -by (res_inst_tac [("B", "{s:state. s`n = #4}")] LeadsTo_Trans 1); +Goal "Mutex \\ {s \\ state. s`n = #3} LeadsTo {s \\ state. s`p=0}"; +by (res_inst_tac [("B", "{s \\ state. s`n = #4}")] LeadsTo_Trans 1); by (ensures_tac "V4" 2); by (ensures_tac "V3" 1); qed "V_F3"; -Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}"; +Goal "Mutex \\ {s \\ state. s`n = #2} LeadsTo {s \\ state. s`p=0}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); @@ -196,19 +196,19 @@ by (auto_tac (claset() addSDs [p_value_type], simpset() addsimps [bool_def])); val V_lemma2 = result(); -Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`p = 0}"; +Goal "Mutex \\ {s \\ state. s`n = #1} LeadsTo {s \\ state. s`p = 0}"; by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); by Auto_tac; val V_lemma1 = result(); -Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}"; +Goal "Mutex \\ {s \\ state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \\ state. s`p = 0}"; by (simp_tac (simpset() addsimps [n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib, V_lemma1, V_lemma2, V_F3] ) 1); val V_lemma123 = result(); (*Misra's F4*) -Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}"; +Goal "Mutex \\ {s \\ state. s`v = 1} LeadsTo {s \\ state. s`p = 0}"; by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1); by Auto_tac; qed "v_Leadsto_not_p"; @@ -216,7 +216,7 @@ (** Absence of starvation **) (*Misra's F6*) -Goal "Mutex : {s:state. s`m = #1} LeadsTo {s:state. s`m = #3}"; +Goal "Mutex \\ {s \\ state. s`m = #1} LeadsTo {s \\ state. s`m = #3}"; by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); by (rtac U_F2 2); by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); @@ -230,7 +230,7 @@ (*The same for V*) -Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`n = #3}"; +Goal "Mutex \\ {s \\ state. s`n = #1} LeadsTo {s \\ state. s`n = #3}"; by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); by (rtac V_F2 2); by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/SubstAx.ML --- a/src/ZF/UNITY/SubstAx.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/SubstAx.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: ZF/UNITY/SubstAx.ML - ID: $Id$ + ID: $Id \\ SubstAx.ML,v 1.8 2003/05/27 09:39:06 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge @@ -12,7 +12,7 @@ (* Equivalence with the HOL-like definition *) Goalw [LeadsTo_def] -"st_set(B)==> A LeadsTo B = {F:program. F:(reachable(F) Int A) leadsTo B}"; +"st_set(B)==> A LeadsTo B = {F \\ program. F:(reachable(F) Int A) leadsTo B}"; by (blast_tac (claset() addDs [psp_stable2, leadsToD2, constrainsD2] addIs [leadsTo_weaken]) 1); qed "LeadsTo_eq"; @@ -24,41 +24,41 @@ (*** Specialized laws for handling invariants ***) (** Conjoining an Always property **) -Goal "F : Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F: A LeadsTo A')"; +Goal "F \\ Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \\ A LeadsTo A')"; by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable, Int_absorb2, Int_assoc RS sym, leadsToD2]) 1); qed "Always_LeadsTo_pre"; -Goalw [LeadsTo_def] "F:Always(I) ==> (F : A LeadsTo (I Int A')) <-> (F : A LeadsTo A')"; +Goalw [LeadsTo_def] "F \\ Always(I) ==> (F \\ A LeadsTo (I Int A')) <-> (F \\ A LeadsTo A')"; by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable, Int_absorb2, Int_assoc RS sym,leadsToD2]) 1); qed "Always_LeadsTo_post"; (* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *) -Goal "[| F:Always(C); F : (C Int A) LeadsTo A' |] ==> F: A LeadsTo A'"; +Goal "[| F \\ Always(C); F \\ (C Int A) LeadsTo A' |] ==> F \\ A LeadsTo A'"; by (blast_tac (claset() addIs [Always_LeadsTo_pre RS iffD1]) 1); qed "Always_LeadsToI"; (* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *) -Goal "[| F:Always(C); F:A LeadsTo A' |] ==> F : A LeadsTo (C Int A')"; +Goal "[| F \\ Always(C); F \\ A LeadsTo A' |] ==> F \\ A LeadsTo (C Int A')"; by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1); qed "Always_LeadsToD"; -(*** Introduction rules: Basis, Trans, Union ***) +(*** Introduction rules \\ Basis, Trans, Union ***) -Goal "F : A Ensures B ==> F : A LeadsTo B"; +Goal "F \\ A Ensures B ==> F \\ A LeadsTo B"; by (auto_tac (claset(), simpset() addsimps [Ensures_def, LeadsTo_def])); qed "LeadsTo_Basis"; -Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"; +Goal "[| F \\ A LeadsTo B; F \\ B LeadsTo C |] ==> F \\ A LeadsTo C"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [leadsTo_Trans]) 1); qed "LeadsTo_Trans"; val [major, program] = Goalw [LeadsTo_def] -"[|(!!A. A:S ==> F : A LeadsTo B); F:program|]==>F:Union(S) LeadsTo B"; +"[|(!!A. A \\ S ==> F \\ A LeadsTo B); F \\ program|]==>F \\ Union(S) LeadsTo B"; by (cut_facts_tac [program] 1); by Auto_tac; by (stac Int_Union_Union2 1); @@ -69,7 +69,7 @@ (*** Derived rules ***) -Goal "F : A leadsTo B ==> F : A LeadsTo B"; +Goal "F \\ A leadsTo B ==> F \\ A LeadsTo B"; by (ftac leadsToD2 1); by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1); @@ -77,16 +77,16 @@ qed "leadsTo_imp_LeadsTo"; (*Useful with cancellation, disjunction*) -Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"; +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)"; +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 [major, program] = Goalw [LeadsTo_def] -"[|(!!i. i:I ==> F : A(i) LeadsTo B); F:program|]==>F:(UN i:I. A(i)) LeadsTo B"; +"[|(!!i. i \\ I ==> F \\ A(i) LeadsTo B); F \\ program|]==>F:(\\i \\ I. A(i)) LeadsTo B"; by (cut_facts_tac [program] 1); by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 1); by (rtac leadsTo_UN 1); @@ -95,7 +95,7 @@ qed "LeadsTo_UN"; (*Binary union introduction rule*) -Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"; +Goal "[| F \\ A LeadsTo C; F \\ B LeadsTo C |] ==> F \\ (A Un B) LeadsTo C"; by (stac Un_eq_Union 1); by (rtac LeadsTo_Union 1); by (auto_tac (claset() addDs [LeadsTo_type RS subsetD], simpset())); @@ -103,83 +103,83 @@ (*Lets us look at the starting state*) val [major, program] = Goal -"[|(!!s. s:A ==> F:{s} LeadsTo B); F:program|]==>F:A LeadsTo B"; +"[|(!!s. s \\ A ==> F:{s} LeadsTo B); F \\ program|]==>F \\ A LeadsTo B"; by (cut_facts_tac [program] 1); by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1); by (ftac major 1); by Auto_tac; qed "single_LeadsTo_I"; -Goal "[| A <= B; F:program |] ==> F : A LeadsTo B"; +Goal "[| A <= B; F \\ program |] ==> F \\ A LeadsTo B"; by (asm_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "subset_imp_LeadsTo"; -Goal "F:0 LeadsTo A <-> F:program"; +Goal "F:0 LeadsTo A <-> F \\ program"; by (auto_tac (claset() addDs [LeadsTo_type RS subsetD] addIs [empty_subsetI RS subset_imp_LeadsTo], simpset())); qed "empty_LeadsTo"; AddIffs [empty_LeadsTo]; -Goal "F : A LeadsTo state <-> F:program"; +Goal "F \\ A LeadsTo state <-> F \\ program"; by (auto_tac (claset() addDs [LeadsTo_type RS subsetD], simpset() addsimps [LeadsTo_eq])); qed "LeadsTo_state"; AddIffs [LeadsTo_state]; Goalw [LeadsTo_def] - "[| F:A LeadsTo A'; A'<=B'|] ==> F : A LeadsTo B'"; + "[| F \\ A LeadsTo A'; A'<=B'|] ==> F \\ A LeadsTo B'"; by (auto_tac (claset() addIs[leadsTo_weaken_R], simpset())); qed_spec_mp "LeadsTo_weaken_R"; -Goalw [LeadsTo_def] "[| F : A LeadsTo A'; B <= A |] ==> F : B LeadsTo A'"; +Goalw [LeadsTo_def] "[| F \\ A LeadsTo A'; B <= A |] ==> F \\ B LeadsTo A'"; by (auto_tac (claset() addIs[leadsTo_weaken_L], simpset())); qed_spec_mp "LeadsTo_weaken_L"; -Goal "[| F : A LeadsTo A'; B<=A; A'<=B' |] ==> F : B LeadsTo B'"; +Goal "[| F \\ A LeadsTo A'; B<=A; A'<=B' |] ==> F \\ B LeadsTo B'"; by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L, LeadsTo_Trans]) 1); qed "LeadsTo_weaken"; Goal -"[| F:Always(C); F:A LeadsTo A'; C Int B <= A; C Int A' <= B' |] \ -\ ==> F : B LeadsTo B'"; +"[| 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, Always_LeadsToD]) 1); qed "Always_LeadsTo_weaken"; (** Two theorems for "proof lattices" **) -Goal "F : A LeadsTo B ==> F:(A Un B) LeadsTo B"; +Goal "F \\ A LeadsTo B ==> F:(A Un B) LeadsTo B"; by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); qed "LeadsTo_Un_post"; -Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \ -\ ==> F : (A Un B) LeadsTo C"; +Goal "[| F \\ A LeadsTo B; F \\ B LeadsTo C |] \ +\ ==> F \\ (A Un B) LeadsTo C"; by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo, LeadsTo_weaken_L, LeadsTo_Trans] addDs [LeadsTo_type RS subsetD]) 1); qed "LeadsTo_Trans_Un"; (** Distributive laws **) -Goal "(F : (A Un B) LeadsTo C) <-> (F : A LeadsTo C & F : B LeadsTo C)"; +Goal "(F \\ (A Un B) LeadsTo C) <-> (F \\ A LeadsTo C & F \\ B LeadsTo C)"; by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1); qed "LeadsTo_Un_distrib"; -Goal "(F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B) & F:program"; +Goal "(F \\ (\\i \\ I. A(i)) LeadsTo B) <-> (\\i \\ I. F \\ A(i) LeadsTo B) & F \\ program"; by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1); qed "LeadsTo_UN_distrib"; -Goal "(F:Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B) & F:program"; +Goal "(F \\ Union(S) LeadsTo B) <-> (\\A \\ S. F \\ A LeadsTo B) & F \\ program"; by (blast_tac (claset() addDs [LeadsTo_type RS subsetD] addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1); qed "LeadsTo_Union_distrib"; (** More rules using the premise "Always(I)" **) -Goal "[| F:(A-B) Co (A Un B); F:transient (A-B) |] ==> F : A Ensures B"; +Goal "[| F:(A-B) Co (A Un B); F \\ transient (A-B) |] ==> F \\ A Ensures B"; by (asm_full_simp_tac (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1); by (blast_tac (claset() addIs [ensuresI, constrains_weaken, @@ -187,9 +187,9 @@ addDs [constrainsD2]) 1); qed "EnsuresI"; -Goal "[| F : Always(I); F : (I Int (A-A')) Co (A Un A'); \ -\ F : transient (I Int (A-A')) |] \ -\ ==> F : A LeadsTo A'"; +Goal "[| F \\ Always(I); F \\ (I Int (A-A')) Co (A Un A'); \ +\ F \\ transient (I Int (A-A')) |] \ +\ ==> F \\ A LeadsTo A'"; by (rtac Always_LeadsToI 1); by (assume_tac 1); by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis, @@ -197,15 +197,15 @@ transient_strengthen]) 1); qed "Always_LeadsTo_Basis"; -(*Set difference: maybe combine with leadsTo_weaken_L?? +(*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"; +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 [major, minor] = Goal -"[|(!!i. i:I ==> F: A(i) LeadsTo A'(i)); F:program |] \ -\ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))"; +"[|(!!i. i \\ I ==> F \\ A(i) LeadsTo A'(i)); F \\ program |] \ +\ ==> F \\ (\\i \\ I. A(i)) LeadsTo (\\i \\ I. A'(i))"; by (cut_facts_tac [minor] 1); by (rtac LeadsTo_Union 1); by (ALLGOALS(Clarify_tac)); @@ -214,13 +214,13 @@ qed "LeadsTo_UN_UN"; (*Binary union version*) -Goal "[| F:A LeadsTo A'; F:B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')"; +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')"; +Goal "[| F \\ A LeadsTo(A' Un B); F \\ B LeadsTo B' |] ==> F \\ A LeadsTo (A' Un B')"; by (blast_tac (claset() addIs [LeadsTo_Un_Un, subset_imp_LeadsTo, LeadsTo_Trans] addDs [LeadsTo_type RS subsetD]) 1); qed "LeadsTo_cancel2"; @@ -229,13 +229,13 @@ by Auto_tac; qed "Un_Diff"; -Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] ==> F : A LeadsTo (A' Un B')"; +Goal "[| F \\ A LeadsTo (A' Un B); F \\ (B-A') LeadsTo B' |] ==> F \\ A LeadsTo (A' Un B')"; by (rtac LeadsTo_cancel2 1); by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [Un_Diff]) 1); qed "LeadsTo_cancel_Diff2"; -Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] ==> F : A LeadsTo (B' Un A')"; +Goal "[| F \\ A LeadsTo (B Un A'); F \\ B LeadsTo B' |] ==> F \\ A LeadsTo (B' Un A')"; by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1); qed "LeadsTo_cancel1"; @@ -244,7 +244,7 @@ by Auto_tac; qed "Diff_Un2"; -Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] ==> F : A LeadsTo (B' Un A')"; +Goal "[| F \\ A LeadsTo (B Un A'); F \\ (B-A') LeadsTo B' |] ==> F \\ A LeadsTo (B' Un A')"; by (rtac LeadsTo_cancel1 1); by (assume_tac 2); by (asm_simp_tac (simpset() addsimps [Diff_Un2]) 1); @@ -253,38 +253,38 @@ (** The impossibility law **) (*The set "A" may be non-empty, but it contains no reachable states*) -Goal "F : A LeadsTo 0 ==> F : Always (state -A)"; +Goal "F \\ A LeadsTo 0 ==> F \\ Always (state -A)"; by (full_simp_tac (simpset() addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1); by (cut_facts_tac [reachable_type] 1); by (auto_tac (claset() addSDs [leadsTo_empty], simpset())); qed "LeadsTo_empty"; -(** PSP: Progress-Safety-Progress **) +(** 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)"; +(*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 (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1); by (Clarify_tac 1); by (dtac psp_stable 1); by (REPEAT(asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1)); qed "PSP_Stable"; -Goal "[| F : A LeadsTo A'; F : Stable(B) |] ==> F : (B Int A) LeadsTo (B Int A')"; +Goal "[| F \\ A LeadsTo A'; F \\ Stable(B) |] ==> F \\ (B Int A) LeadsTo (B Int A')"; by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1); qed "PSP_Stable2"; -Goal "[| F:A LeadsTo A'; F:B Co B'|]==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"; +Goal "[| F \\ A LeadsTo A'; F \\ B Co B'|]==> F \\ (A Int B') LeadsTo ((A' Int B) Un (B' - B))"; by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1); by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1); qed "PSP"; -Goal "[| F : A LeadsTo A'; F : B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"; +Goal "[| F \\ A LeadsTo A'; F \\ B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1); qed "PSP2"; Goal -"[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"; +"[| F \\ A LeadsTo A'; F \\ B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"; by (rewtac Unless_def); by (dtac PSP 1); by (assume_tac 1); @@ -295,10 +295,10 @@ (** Meta or object quantifier ????? **) Goal "[| wf(r); \ -\ ALL m:I. F : (A Int f-``{m}) LeadsTo \ +\ \\m \\ I. F \\ (A Int f-``{m}) LeadsTo \ \ ((A Int f-``(converse(r) `` {m})) Un B); \ -\ field(r)<=I; A<=f-``I; F:program |] \ -\ ==> F : A LeadsTo B"; +\ field(r)<=I; A<=f-``I; F \\ program |] \ +\ ==> F \\ A LeadsTo B"; by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1); by Auto_tac; by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1); @@ -314,8 +314,8 @@ qed "LeadsTo_wf_induct"; -Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B); \ -\ A<=f-``nat; F:program |] ==> F : A LeadsTo B"; +Goal "[| \\m \\ nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B); \ +\ A<=f-``nat; F \\ program |] ==> F \\ A LeadsTo B"; by (res_inst_tac [("A1", "nat"),("f1", "%x. x")] (wf_measure RS LeadsTo_wf_induct) 1); by (ALLGOALS(asm_full_simp_tac @@ -333,11 +333,11 @@ *****) -(*** Completion: Binary and General Finite versions ***) +(*** 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)"; +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_def, Constrains_eq_constrains, Int_Un_distrib]) 1); @@ -346,10 +346,10 @@ by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1); qed "Completion"; -Goal "[| I:Fin(X);F:program |] \ -\ ==> (ALL i:I. F : (A(i)) LeadsTo (A'(i) Un C)) --> \ -\ (ALL i:I. F : (A'(i)) Co (A'(i) Un C)) --> \ -\ F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; +Goal "[| I \\ Fin(X);F \\ program |] \ +\ ==> (\\i \\ I. F \\ (A(i)) LeadsTo (A'(i) Un C)) --> \ +\ (\\i \\ I. F \\ (A'(i)) Co (A'(i) Un C)) --> \ +\ F \\ (\\i \\ I. A(i)) LeadsTo ((\\i \\ I. A'(i)) Un C)"; by (etac Fin_induct 1); by (auto_tac (claset(), simpset() delsimps INT_simps addsimps [Inter_0])); @@ -360,17 +360,17 @@ val lemma = result(); val prems = Goal - "[| I:Fin(X); !!i. i:I ==> F : A(i) LeadsTo (A'(i) Un C); \ -\ !!i. i:I ==> F : A'(i) Co (A'(i) Un C); \ -\ F:program |] \ -\ ==> F : (INT i:I. A(i)) LeadsTo ((INT i:I. A'(i)) Un C)"; + "[| I \\ Fin(X); !!i. i \\ I ==> F \\ A(i) LeadsTo (A'(i) Un C); \ +\ !!i. i \\ I ==> F \\ A'(i) Co (A'(i) Un C); \ +\ F \\ program |] \ +\ ==> F \\ (\\i \\ I. A(i)) LeadsTo ((\\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')"; + "[| 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", "0")] (Completion RS LeadsTo_weaken_R) 1); by (Asm_full_simp_tac 5); by (rtac subset_refl 5); @@ -378,10 +378,10 @@ qed "Stable_completion"; val prems = Goalw [Stable_def] - "[| I:Fin(X); \ -\ (!!i. i:I ==> F : A(i) LeadsTo A'(i)); \ -\ (!!i. i:I ==>F: Stable(A'(i))); F:program |] \ -\ ==> F : (INT i:I. A(i)) LeadsTo (INT i:I. A'(i))"; + "[| I \\ Fin(X); \ +\ (!!i. i \\ I ==> F \\ A(i) LeadsTo A'(i)); \ +\ (!!i. i \\ I ==>F \\ Stable(A'(i))); F \\ program |] \ +\ ==> F \\ (\\i \\ I. A(i)) LeadsTo (\\i \\ I. A'(i))"; by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1); by (ALLGOALS(Simp_tac)); by (rtac subset_refl 5); @@ -397,7 +397,7 @@ 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*) + (*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*) diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Mon Jul 07 17:58:21 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,652 +0,0 @@ -(* Title: ZF/UNITY/Union.ML - ID: $Id$ - Author: Sidi O Ehmety, Computer Laboratory - Copyright 2001 University of Cambridge - -Unions of programs - -From Misra's Chapter 5: Asynchronous Compositions of Programs - -Proofs ported from HOL. - -*) - -(** SKIP **) - -Goal "reachable(SKIP) = state"; -by (force_tac (claset() addEs [reachable.induct] - addIs reachable.intrs, simpset()) 1); -qed "reachable_SKIP"; -AddIffs [reachable_SKIP]; - -(* Elimination programify from ok and Join *) - -Goal "programify(F) ok G <-> F ok G"; -by (simp_tac (simpset() addsimps [ok_def]) 1); -qed "ok_programify_left"; - -Goal "F ok programify(G) <-> F ok G"; -by (simp_tac (simpset() addsimps [ok_def]) 1); -qed "ok_programify_right"; - -Goal "programify(F) Join G = F Join G"; -by (simp_tac (simpset() addsimps [Join_def]) 1); -qed "Join_programify_left"; - -Goal "F Join programify(G) = F Join G"; -by (simp_tac (simpset() addsimps [Join_def]) 1); -qed "Join_programify_right"; - -AddIffs [ok_programify_left, ok_programify_right, - Join_programify_left, Join_programify_right]; - -(** SKIP and safety properties **) - -Goalw [constrains_def, st_set_def] -"(SKIP: A co B) <-> (A<=B & st_set(A))"; -by Auto_tac; -qed "SKIP_in_constrains_iff"; -AddIffs [SKIP_in_constrains_iff]; - -Goalw [Constrains_def]"(SKIP : A Co B)<-> (state Int A<=B)"; -by Auto_tac; -qed "SKIP_in_Constrains_iff"; -AddIffs [SKIP_in_Constrains_iff]; - -Goal "SKIP:stable(A) <-> st_set(A)"; -by (auto_tac (claset(), - simpset() addsimps [stable_def])); -qed "SKIP_in_stable"; -AddIffs [SKIP_in_stable]; - -Goalw [Stable_def] "SKIP:Stable(A)"; -by Auto_tac; -qed "SKIP_in_Stable"; -AddIffs [SKIP_in_Stable]; - -(** Join and JOIN types **) - -Goalw [Join_def] "F Join G : program"; -by Auto_tac; -qed "Join_in_program"; -AddIffs [Join_in_program]; -AddTCs [Join_in_program]; - -Goalw [JOIN_def] "JOIN(I,F):program"; -by Auto_tac; -qed "JOIN_in_program"; -AddIffs [JOIN_in_program]; -AddTCs [JOIN_in_program]; - -(* Init, Acts, and AllowedActs of Join and JOIN *) -Goal "Init(F Join G) = Init(F) Int Init(G)"; -by (simp_tac (simpset() - addsimps [Int_assoc, Join_def]) 1); -qed "Init_Join"; - -Goal "Acts(F Join G) = Acts(F) Un Acts(G)"; -by (simp_tac (simpset() addsimps [Int_Un_distrib2, cons_absorb, Join_def]) 1); -qed "Acts_Join"; - -Goal "AllowedActs(F Join G) = \ -\ AllowedActs(F) Int AllowedActs(G)"; -by (simp_tac (simpset() - addsimps [Int_assoc,cons_absorb,Join_def]) 1); -qed "AllowedActs_Join"; -Addsimps [Init_Join, Acts_Join, AllowedActs_Join]; - -(** Join's algebraic laws **) - -Goal "F Join G = G Join F"; -by (simp_tac (simpset() addsimps - [Join_def, Un_commute, Int_commute]) 1); -qed "Join_commute"; - -Goal "A Join (B Join C) = B Join (A Join C)"; -by (simp_tac (simpset() addsimps - [Join_def,Int_Un_distrib2, cons_absorb]) 1); -by (simp_tac (simpset() addsimps - Un_ac@Int_ac@[Int_Un_distrib2, cons_absorb]) 1); -qed "Join_left_commute"; - -Goal "(F Join G) Join H = F Join (G Join H)"; -by (asm_simp_tac (simpset() addsimps - Un_ac@[Join_def, cons_absorb, Int_assoc, Int_Un_distrib2]) 1); -qed "Join_assoc"; - -(* Needed below *) -Goal "cons(id(state), Pow(state * state)) = Pow(state*state)"; -by Auto_tac; -qed "cons_id"; -AddIffs [cons_id]; - -Goalw [Join_def, SKIP_def] - "SKIP Join F = programify(F)"; -by (auto_tac (claset(), simpset() addsimps [Int_absorb,cons_eq])); -qed "Join_SKIP_left"; - -Goal "F Join SKIP = programify(F)"; -by (stac Join_commute 1); -by (asm_simp_tac (simpset() addsimps [Join_SKIP_left]) 1); -qed "Join_SKIP_right"; - -AddIffs [Join_SKIP_left, Join_SKIP_right]; - -Goal "F Join F = programify(F)"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "Join_absorb"; - -Addsimps [Join_absorb]; - -Goal "F Join (F Join G) = F Join G"; -by (asm_simp_tac (simpset() addsimps [Join_assoc RS sym]) 1); -qed "Join_left_absorb"; - -(*Join is an AC-operator*) -val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute]; - -(** Eliminating programify form JN and OK expressions **) - -Goal "OK(I, %x. programify(F(x))) <-> OK(I, F)"; -by (simp_tac (simpset() addsimps [OK_def]) 1); -qed "OK_programify"; - -Goal "JOIN(I, %x. programify(F(x))) = JOIN(I, F)"; -by (simp_tac (simpset() addsimps [JOIN_def]) 1); -qed "JN_programify"; - -AddIffs [OK_programify, JN_programify]; - -(* JN *) - -Goalw [JOIN_def] "JOIN(0, F) = SKIP"; -by Auto_tac; -qed "JN_empty"; -AddIffs [JN_empty]; -Addsimps [Inter_0]; - -Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))"; -by (simp_tac (simpset() addsimps [JOIN_def]) 1); -by (auto_tac (claset() addSEs [not_emptyE], - simpset() addsimps INT_extend_simps - delsimps INT_simps)); -qed "Init_JN"; - -Goalw [JOIN_def] - "Acts(JOIN(I,F)) = cons(id(state), UN i:I. Acts(F(i)))"; -by (auto_tac (claset(), simpset() delsimps (INT_simps@UN_simps))); -by (rtac equalityI 1); -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); -qed "Acts_JN"; - -Goalw [JOIN_def] -"AllowedActs(JN i:I. F(i)) = (if I=0 then Pow(state*state) else (INT i:I. AllowedActs(F(i))))"; -by Auto_tac; -by (rtac equalityI 1); -by (auto_tac (claset() addSEs [not_emptyE] addDs [AllowedActs_type RS subsetD], simpset())); -qed "AllowedActs_JN"; -AddIffs [Init_JN, Acts_JN, AllowedActs_JN]; - -Goal "(JN i:cons(a,I). F(i)) = F(a) Join (JN i:I. F(i))"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "JN_cons"; -AddIffs[JN_cons]; - - -val prems = Goalw [JOIN_def] - "[| I=J; !!i. i:J ==> F(i) = G(i) |] ==> \ -\ (JN i:I. F(i)) = (JN i:J. G(i))"; -by (asm_simp_tac (simpset() addsimps prems) 1); -qed "JN_cong"; - -Addcongs [JN_cong]; - -(*** JN laws ***) -Goal "k:I ==>F(k) Join (JN i:I. F(i)) = (JN i:I. F(i))"; -by (stac (JN_cons RS sym) 1); -by (auto_tac (claset(), - simpset() addsimps [cons_absorb])); -qed "JN_absorb"; - -Goal "(JN i: I Un J. F(i)) = ((JN i: I. F(i)) Join (JN i:J. F(i)))"; -by (rtac program_equalityI 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [UN_Un,INT_Un]))); -by (ALLGOALS(asm_full_simp_tac (simpset() delsimps INT_simps - addsimps INT_extend_simps))); -by (Blast_tac 1); -qed "JN_Un"; - -Goal "(JN i:I. c) = (if I=0 then SKIP else programify(c))"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "JN_constant"; - -Goal "(JN i:I. F(i) Join G(i)) = (JN i:I. F(i)) Join (JN i:I. G(i))"; -by (rtac program_equalityI 1); -by (ALLGOALS(simp_tac (simpset() addsimps [Int_absorb]))); -by (safe_tac (claset() addSEs [not_emptyE])); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps - [INT_Int_distrib, Int_absorb]))); -by (Force_tac 1); -qed "JN_Join_distrib"; - -Goal "(JN i:I. F(i) Join G) = ((JN i:I. F(i) Join G))"; -by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1); -qed "JN_Join_miniscope"; - -(*Used to prove guarantees_JN_I*) - -Goal "i:I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)"; -by (rtac program_equalityI 1); -by (auto_tac (claset() addSEs [not_emptyE], simpset())); -qed "JN_Join_diff"; - -(*** Safety: co, stable, FP ***) - - -(*Fails if I=0 because it collapses to SKIP : A co B, i.e. to A<=B. So an - alternative precondition is A<=B, but most proofs using this rule require - I to be nonempty for other reasons anyway.*) - -Goalw [constrains_def, JOIN_def,st_set_def] - "i:I==>(JN i:I. F(i)):A co B <-> (ALL i:I. programify(F(i)):A co B)"; -by Auto_tac; -by (Blast_tac 2); -by (rename_tac "j act y z" 1); -by (cut_inst_tac [("F","F(j)")] Acts_type 1); -by (dres_inst_tac [("x", "act")] bspec 1); -by Auto_tac; -qed "JN_constrains"; - -Goal "(F Join G : A co B) <-> (programify(F):A co B & programify(G):A co B)"; -by (auto_tac (claset(), simpset() addsimps [constrains_def])); -qed "Join_constrains"; - -Goal "(F Join G : A unless B) <-> \ -\ (programify(F) : A unless B & programify(G):A unless B)"; -by (asm_simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1); -qed "Join_unless"; - -AddIffs [Join_constrains, Join_unless]; - -(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. - reachable (F Join G) could be much bigger than reachable F, reachable G -*) - -Goal "[| F : A co A'; G:B co B' |] \ -\ ==> F Join G : (A Int B) co (A' Un B')"; -by (subgoal_tac "st_set(A) & st_set(B) & F:program & G:program" 1); -by (blast_tac (claset() addDs [constrainsD2]) 2); -by (Asm_simp_tac 1); -by (blast_tac (claset() addIs [constrains_weaken]) 1); -qed "Join_constrains_weaken"; - -(*If I=0, it degenerates to SKIP : state co 0, which is false.*) -val [major, minor] = Goal -"[| (!!i. i:I ==> F(i) : A(i) co A'(i)); i: I |] \ -\ ==> (JN i:I. F(i)) : (INT i:I. A(i)) co (UN i:I. A'(i))"; -by (cut_facts_tac [minor] 1); -by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); -by (Clarify_tac 1); -by (rename_tac "j" 1); -by (forw_inst_tac [("i", "j")] major 1); -by (ftac constrainsD2 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [constrains_weaken]) 1); -qed "JN_constrains_weaken"; - -Goal "(JN i:I. F(i)): stable(A) <-> ((ALL i:I. programify(F(i)):stable(A)) & st_set(A))"; -by (asm_simp_tac - (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1); -by Auto_tac; -by (cut_inst_tac [("F", "F(i)")] Acts_type 1); -by (dres_inst_tac [("x","act")] bspec 1); -by Auto_tac; -qed "JN_stable"; - -val [major, minor] = Goalw [initially_def] - "[| (!!i. i:I ==>F(i):initially(A)); i:I |] ==> (JN i:I. F(i)):initially(A)"; -by (cut_facts_tac [minor] 1); -by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [Inter_iff])); -by (forw_inst_tac [("i", "x")] major 1); -by Auto_tac; -qed "initially_JN_I"; - -val [major, minor] = Goal -"[|(!!i. i:I ==> F(i) : invariant(A)); i:I|]==> (JN i:I. F(i)):invariant(A)"; -by (cut_facts_tac [minor] 1); -by (auto_tac (claset() addSIs [initially_JN_I] addDs [major], - simpset() addsimps [invariant_def, JN_stable])); -by (thin_tac "i:I" 1); -by (ftac major 1); -by (dtac major 2); -by (auto_tac (claset(), simpset() addsimps [invariant_def])); -by (ALLGOALS(ftac stableD2 )); -by Auto_tac; -qed "invariant_JN_I"; - -Goal " (F Join G : stable(A)) <-> \ -\ (programify(F) : stable(A) & programify(G): stable(A))"; -by (asm_simp_tac (simpset() addsimps [stable_def]) 1); -qed "Join_stable"; -AddIffs [Join_stable]; - -Goalw [initially_def] "[| F:initially(A); G:initially(A) |] ==> F Join G: initially(A)"; -by Auto_tac; -qed "initially_JoinI"; -AddSIs [initially_JoinI]; - -Goal "[| F : invariant(A); G : invariant(A) |] \ -\ ==> F Join G : invariant(A)"; -by (subgoal_tac "F:program&G:program" 1); -by (blast_tac (claset() addDs [invariantD2]) 2); -by (full_simp_tac (simpset() addsimps [invariant_def]) 1); -by (auto_tac (claset() addIs [Join_in_program], simpset())); -qed "invariant_JoinI"; - - -(* Fails if I=0 because INT i:0. A(i) = 0 *) -Goal "i:I ==> FP(JN i:I. F(i)) = (INT i:I. FP (programify(F(i))))"; -by (asm_simp_tac (simpset() addsimps [FP_def, Inter_def]) 1); -by (rtac equalityI 1); -by Safe_tac; -by (ALLGOALS(subgoal_tac "st_set({x})")); -by (rotate_tac ~1 3); -by (rotate_tac ~1 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable]))); -by (rewtac st_set_def); -by (REPEAT(Blast_tac 1)); -qed "FP_JN"; - -(*** Progress: transient, ensures ***) - -Goal "i:I==>(JN i:I. F(i)) : transient(A) <-> \ -\ (EX i:I. programify(F(i)) : transient(A))"; -by (auto_tac (claset(), - simpset() addsimps [transient_def, JOIN_def])); -by (rewtac st_set_def); -by (dres_inst_tac [("x", "act")] bspec 2); -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); -qed "JN_transient"; - -Goal "F Join G : transient(A) <-> \ -\ (programify(F) : transient(A) | programify(G):transient(A))"; -by (auto_tac (claset(), - simpset() addsimps [transient_def, Join_def, Int_Un_distrib2])); -qed "Join_transient"; - -AddIffs [Join_transient]; - - -Goal "F : transient(A) ==> F Join G : transient(A)"; -by (asm_full_simp_tac (simpset() - addsimps [Join_transient, transientD2]) 1); -qed "Join_transient_I1"; - - -Goal "G : transient(A) ==> F Join G : transient(A)"; -by (asm_full_simp_tac (simpset() - addsimps [Join_transient, transientD2]) 1); -qed "Join_transient_I2"; - -(*If I=0 it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) -Goal "i : I ==> \ -\ (JN i:I. F(i)) : A ensures B <-> \ -\ ((ALL i:I. programify(F(i)) : (A-B) co (A Un B)) & \ -\ (EX i:I. programify(F(i)) : A ensures B))"; -by (auto_tac (claset(), - simpset() addsimps [ensures_def, JN_constrains, JN_transient])); -qed "JN_ensures"; - - -Goalw [ensures_def] - "F Join G : A ensures B <-> \ -\ (programify(F) : (A-B) co (A Un B) & programify(G) : (A-B) co (A Un B) & \ -\ (programify(F): transient (A-B) | programify(G) : transient (A-B)))"; -by (auto_tac (claset(), simpset() addsimps [Join_transient])); -qed "Join_ensures"; - -Goalw [stable_def, constrains_def, Join_def, st_set_def] - "[| F : stable(A); G : A co A' |] \ -\ ==> F Join G : A co A'"; -by (cut_inst_tac [("F", "F")] Acts_type 1); -by (cut_inst_tac [("F", "G")] Acts_type 1); -by Auto_tac; -by (REPEAT(Blast_tac 1)); -qed "stable_Join_constrains"; - -(*Premise for G cannot use Always because F: Stable A is - weaker than G : stable A *) -Goal "[| F : stable(A); G : invariant(A) |] ==> F Join G : Always(A)"; -by (subgoal_tac "F:program & G:program & st_set(A)" 1); -by (blast_tac (claset() addDs [invariantD2, stableD2]) 2); -by (asm_full_simp_tac (simpset() addsimps [Always_def, invariant_def,initially_def , - Stable_eq_stable]) 1); -by (force_tac(claset() addIs [stable_Int], simpset()) 1); -qed "stable_Join_Always1"; - -(*As above, but exchanging the roles of F and G*) -Goal "[| F : invariant(A); G : stable(A) |] ==> F Join G : Always(A)"; -by (stac Join_commute 1); -by (blast_tac (claset() addIs [stable_Join_Always1]) 1); -qed "stable_Join_Always2"; - - - -Goal "[| F : stable(A); G : A ensures B |] ==> F Join G : A ensures B"; -by (subgoal_tac "F:program & G:program & st_set(A)" 1); -by (blast_tac (claset() addDs [stableD2, ensures_type RS subsetD]) 2); -by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1); -by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); -by (etac constrains_weaken 1); -by Auto_tac; -qed "stable_Join_ensures1"; - - -(*As above, but exchanging the roles of F and G*) -Goal "[| F : A ensures B; G : stable(A) |] ==> F Join G : A ensures B"; -by (stac Join_commute 1); -by (blast_tac (claset() addIs [stable_Join_ensures1]) 1); -qed "stable_Join_ensures2"; - -(*** The ok and OK relations ***) - -Goal "SKIP ok F"; -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset() addsimps [ok_def])); -qed "ok_SKIP1"; - -Goal "F ok SKIP"; -by (auto_tac (claset() addDs [Acts_type RS subsetD], - simpset() addsimps [ok_def])); -qed "ok_SKIP2"; -AddIffs [ok_SKIP1, ok_SKIP2]; - -Goal "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_commute"; - -Goal "(F ok G) <->(G ok F)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_commute"; - -bind_thm ("ok_sym", ok_commute RS iffD1); - -Goal "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"; -by (asm_full_simp_tac - (simpset() addsimps [ok_def, Join_def, OK_def, - Int_assoc, cons_absorb, Int_Un_distrib2, Ball_def]) 1); -by (rtac iffI 1); -by Safe_tac; -by (REPEAT(Force_tac 1)); -qed "ok_iff_OK"; - -Goal "F ok (G Join H) <-> (F ok G & F ok H)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_iff1"; - - -Goal "(G Join H) ok F <-> (G ok F & H ok F)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_iff2"; -AddIffs [ok_Join_iff1, ok_Join_iff2]; - -(*useful? Not with the previous two around*) -Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_commute_I"; - -Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))"; -by (force_tac (claset() addDs [Acts_type RS subsetD] addSEs [not_emptyE], - simpset() addsimps [ok_def]) 1); -qed "ok_JN_iff1"; - -Goal "JOIN(I,G) ok F <-> (ALL i:I. G(i) ok F)"; -by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def])); -by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1); -qed "ok_JN_iff2"; -AddIffs [ok_JN_iff1, ok_JN_iff2]; - -Goal "OK(I,F) <-> (ALL i: I. ALL j: I-{i}. F(i) ok (F(j)))"; -by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def])); -qed "OK_iff_ok"; - -Goal "[| OK(I,F); i: I; j: I; i~=j|] ==> F(i) ok F(j)"; -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok])); -qed "OK_imp_ok"; - - -(*** Allowed ***) - -Goal "Allowed(SKIP) = program"; -by (auto_tac (claset() addDs [Acts_type RS subsetD], - simpset() addsimps [Allowed_def])); -qed "Allowed_SKIP"; - -Goal "Allowed(F Join G) = \ -\ Allowed(programify(F)) Int Allowed(programify(G))"; -by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -qed "Allowed_Join"; - -Goal "i:I ==> \ -\ Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))"; -by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -by (Blast_tac 1); -qed "Allowed_JN"; -Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN]; - -Goal "F ok G <-> (programify(F):Allowed(programify(G)) & \ -\ programify(G):Allowed(programify(F)))"; -by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1); -qed "ok_iff_Allowed"; - - -Goal "OK(I,F) <-> \ -\ (ALL i: I. ALL j: I-{i}. programify(F(i)) : Allowed(programify(F(j))))"; -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed])); -qed "OK_iff_Allowed"; - -(*** safety_prop, for reasoning about given instances of "ok" ***) - -Goal "safety_prop(X) ==> (Acts(G) <= cons(id(state), (UN F:X. Acts(F)))) <-> (programify(G):X)"; -by (full_simp_tac( simpset() addsimps [safety_prop_def]) 1); -by (Clarify_tac 1); -by (case_tac "G:program" 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (Blast_tac 1); -by Safe_tac; -by (Force_tac 2); -by (force_tac (claset(), simpset() - addsimps [programify_def]) 1); -qed "safety_prop_Acts_iff"; - -Goal "safety_prop(X) ==> \ -\ (UN G:X. Acts(G)) <= AllowedActs(F) <-> (X <= Allowed(programify(F)))"; -by (asm_full_simp_tac (simpset() addsimps [Allowed_def, - safety_prop_Acts_iff RS iff_sym]) 1); -by Safe_tac; -by (REPEAT (Blast_tac 2)); -by (rewtac safety_prop_def); -by (Blast_tac 1); -qed "safety_prop_AllowedActs_iff_Allowed"; - - -Goal "safety_prop(X) ==> Allowed(mk_program(init, acts, UN F:X. Acts(F))) = X"; -by (subgoal_tac "cons(id(state), Union(RepFun(X, Acts)) Int Pow(state * state)) = \ -\ Union(RepFun(X, Acts))" 1); -by (rtac equalityI 2); -by (REPEAT(force_tac (claset() addDs [Acts_type RS subsetD], - simpset() addsimps [safety_prop_def]) 2)); -by (asm_full_simp_tac (simpset() delsimps UN_simps - addsimps [Allowed_def, safety_prop_Acts_iff]) 1); -by (rewtac safety_prop_def); -by Auto_tac; -qed "Allowed_eq"; - -Goal "[| F == mk_program (init, acts, UN F:X. Acts(F)); safety_prop(X) |] \ -\ ==> Allowed(F) = X"; -by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); -qed "def_prg_Allowed"; - -(*For safety_prop to hold, the property must be satisfiable!*) -Goal "safety_prop(A co B) <-> (A <= B & st_set(A))"; -by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def, st_set_def]) 1); -by (Blast_tac 1); -qed "safety_prop_constrains"; -AddIffs [safety_prop_constrains]; - -(* To be used with resolution *) -Goal "[| A<=B; st_set(A) |] ==>safety_prop(A co B)"; -by Auto_tac; -qed "safety_prop_constrainsI"; - -Goal "safety_prop(stable(A)) <-> st_set(A)"; -by (asm_simp_tac (simpset() addsimps [stable_def]) 1); -qed "safety_prop_stable"; -AddIffs [safety_prop_stable]; - -Goal "st_set(A) ==> safety_prop(stable(A))"; -by Auto_tac; -qed "safety_prop_stableI"; - -Goal "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)"; -by (asm_full_simp_tac (simpset() addsimps [safety_prop_def]) 1); -by Safe_tac; -by (Blast_tac 1); -by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), - ("C", "Union(RepFun(Y, Acts))")] subset_trans 2); -by (dres_inst_tac [("B", "Union(RepFun(X Int Y, Acts))"), - ("C", "Union(RepFun(X, Acts))")] subset_trans 1); -by (REPEAT(Blast_tac 1)); -qed "safety_prop_Int"; -Addsimps [safety_prop_Int]; - -(* If I=0 the conclusion becomes safety_prop(0) which is false *) -val [major, minor] = Goalw [safety_prop_def] -"[| (!!i. i:I ==>safety_prop(X(i))); i:I |] ==> safety_prop(INT i:I. X(i))"; -by (cut_facts_tac [minor] 1); -by Safe_tac; -by (full_simp_tac (simpset() addsimps [Inter_iff]) 1); -by (Clarify_tac 1); -by (ftac major 1); -by (dres_inst_tac [("i", "xa")] major 2); -by (forw_inst_tac [("i", "xa")] major 4); -by (ALLGOALS(Asm_full_simp_tac)); -by Auto_tac; -by (dres_inst_tac [("B", "Union(RepFun(Inter(RepFun(I, X)), Acts))"), - ("C", "Union(RepFun(X(xa), Acts))")] subset_trans 1); -by (REPEAT(Blast_tac 1)); -qed "safety_prop_Inter"; - -Goalw [ok_def] -"[| F == mk_program(init,acts, UN G:X. Acts(G)); safety_prop(X) |] \ -\ ==> F ok G <-> (programify(G):X & acts Int Pow(state*state) <= AllowedActs(G))"; -by (dres_inst_tac [("G", "G")] safety_prop_Acts_iff 1); -by Safe_tac; -by (ALLGOALS(cut_inst_tac [("F", "G")] AllowedActs_type)); -by (ALLGOALS(cut_inst_tac [("F", "G")] Acts_type)); -by Auto_tac; -qed "def_UNION_ok_iff"; - - diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/Union.thy Tue Jul 08 11:44:30 2003 +0200 @@ -11,35 +11,37 @@ *) -Union = SubstAx + FP + +theory Union = SubstAx + FP: + +declare Inter_0 [simp] constdefs - (*FIXME: conjoin Init(F) Int Init(G) ~= 0 *) - ok :: [i, i] => o (infixl 65) - "F ok G == Acts(F) <= AllowedActs(G) & - Acts(G) <= AllowedActs(F)" + (*FIXME: conjoin Init(F) Int Init(G) \ 0 *) + ok :: "[i, i] => o" (infixl "ok" 65) + "F ok G == Acts(F) \ AllowedActs(G) & + Acts(G) \ AllowedActs(F)" - (*FIXME: conjoin (INT i:I. Init(F(i))) ~= 0 *) - OK :: [i, i=>i] => o - "OK(I,F) == (ALL i:I. ALL j: I-{i}. Acts(F(i)) <= AllowedActs(F(j)))" + (*FIXME: conjoin (\i \ I. Init(F(i))) \ 0 *) + OK :: "[i, i=>i] => o" + "OK(I,F) == (\i \ I. \j \ I-{i}. Acts(F(i)) \ AllowedActs(F(j)))" - JOIN :: [i, i=>i] => i + JOIN :: "[i, i=>i] => i" "JOIN(I,F) == if I = 0 then SKIP else - mk_program(INT i:I. Init(F(i)), UN i:I. Acts(F(i)), - INT i:I. AllowedActs(F(i)))" + mk_program(\i \ I. Init(F(i)), \i \ I. Acts(F(i)), + \i \ I. AllowedActs(F(i)))" - Join :: [i, i] => i (infixl 65) + Join :: "[i, i] => i" (infixl "Join" 65) "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G), AllowedActs(F) Int AllowedActs(G))" (*Characterizes safety properties. Used with specifying AllowedActs*) safety_prop :: "i => o" - "safety_prop(X) == X<=program & - SKIP:X & (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)" + "safety_prop(X) == X\program & + SKIP \ X & (\G \ program. Acts(G) \ (\F \ X. Acts(F)) --> G \ X)" syntax - "@JOIN1" :: [pttrns, i] => i ("(3JN _./ _)" 10) - "@JOIN" :: [pttrn, i, i] => i ("(3JN _:_./ _)" 10) + "@JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) + "@JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) translations "JN x:A. B" == "JOIN(A, (%x. B))" @@ -47,9 +49,624 @@ "JN x. B" == "JOIN(state,(%x. B))" syntax (symbols) - SKIP :: i ("\\") - "op Join" :: [i, i] => i (infixl "\\" 65) - "@JOIN1" :: [pttrns, i] => i ("(3\\ _./ _)" 10) - "@JOIN" :: [pttrn, i, i] => i ("(3\\ _:_./ _)" 10) + SKIP :: i ("\") + Join :: "[i, i] => i" (infixl "\" 65) + "@JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) + "@JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 10) + + +subsection{*SKIP*} + +lemma reachable_SKIP [simp]: "reachable(SKIP) = state" +by (force elim: reachable.induct intro: reachable.intros) + +text{*Elimination programify from ok and Join*} + +lemma ok_programify_left [iff]: "programify(F) ok G <-> F ok G" +by (simp add: ok_def) + +lemma ok_programify_right [iff]: "F ok programify(G) <-> F ok G" +by (simp add: ok_def) + +lemma Join_programify_left [simp]: "programify(F) Join G = F Join G" +by (simp add: Join_def) + +lemma Join_programify_right [simp]: "F Join programify(G) = F Join G" +by (simp add: Join_def) + +subsection{*SKIP and safety properties*} + +lemma SKIP_in_constrains_iff [iff]: "(SKIP \ A co B) <-> (A\B & st_set(A))" +by (unfold constrains_def st_set_def, auto) + +lemma SKIP_in_Constrains_iff [iff]: "(SKIP \ A Co B)<-> (state Int A\B)" +by (unfold Constrains_def, auto) + +lemma SKIP_in_stable [iff]: "SKIP \ stable(A) <-> st_set(A)" +by (auto simp add: stable_def) + +lemma SKIP_in_Stable [iff]: "SKIP \ Stable(A)" +by (unfold Stable_def, auto) + +subsection{*Join and JOIN types*} + +lemma Join_in_program [iff,TC]: "F Join G \ program" +by (unfold Join_def, auto) + +lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \ program" +by (unfold JOIN_def, auto) + +subsection{*Init, Acts, and AllowedActs of Join and JOIN*} +lemma Init_Join [simp]: "Init(F Join G) = Init(F) Int Init(G)" +by (simp add: Int_assoc Join_def) + +lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) Un Acts(G)" +by (simp add: Int_Un_distrib2 cons_absorb Join_def) + +lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) = + AllowedActs(F) Int AllowedActs(G)" +apply (simp add: Int_assoc cons_absorb Join_def) +done + +subsection{*Join's algebraic laws*} + +lemma Join_commute: "F Join G = G Join F" +by (simp add: Join_def Un_commute Int_commute) + +lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)" +apply (simp add: Join_def Int_Un_distrib2 cons_absorb) +apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb) +done + +lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)" +by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2) + +subsection{*Needed below*} +lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)" +by auto + +lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)" +apply (unfold Join_def SKIP_def) +apply (auto simp add: Int_absorb cons_eq) +done + +lemma Join_SKIP_right [simp]: "F Join SKIP = programify(F)" +apply (subst Join_commute) +apply (simp add: Join_SKIP_left) +done + +lemma Join_absorb [simp]: "F Join F = programify(F)" +by (rule program_equalityI, auto) + +lemma Join_left_absorb: "F Join (F Join G) = F Join G" +by (simp add: Join_assoc [symmetric]) + +subsection{*Join is an AC-operator*} +lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute + +subsection{*Eliminating programify form JN and OK expressions*} + +lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) <-> OK(I, F)" +by (simp add: OK_def) + +lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)" +by (simp add: JOIN_def) + + +subsection{*JN*} + +lemma JN_empty [simp]: "JOIN(0, F) = SKIP" +by (unfold JOIN_def, auto) + +lemma Init_JN [simp]: + "Init(\i \ I. F(i)) = (if I=0 then state else (\i \ I. Init(F(i))))" +apply (simp add: JOIN_def) +apply (auto elim!: not_emptyE simp add: INT_extend_simps simp del: INT_simps) +done + +lemma Acts_JN [simp]: + "Acts(JOIN(I,F)) = cons(id(state), \i \ I. Acts(F(i)))" +apply (unfold JOIN_def) +apply (auto simp del: INT_simps UN_simps) +apply (rule equalityI) +apply (auto dest: Acts_type [THEN subsetD]) +done + +lemma AllowedActs_JN [simp]: + "AllowedActs(\i \ I. F(i)) = + (if I=0 then Pow(state*state) else (\i \ I. AllowedActs(F(i))))" +apply (unfold JOIN_def, auto) +apply (rule equalityI) +apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD]) +done + +lemma JN_cons [simp]: "(\i \ cons(a,I). F(i)) = F(a) Join (\i \ I. F(i))" +by (rule program_equalityI, auto) + +lemma JN_cong [cong]: + "[| I=J; !!i. i \ J ==> F(i) = G(i) |] ==> + (\i \ I. F(i)) = (\i \ J. G(i))" +by (simp add: JOIN_def) + + + +subsection{*JN laws*} +lemma JN_absorb: "k \ I ==>F(k) Join (\i \ I. F(i)) = (\i \ I. F(i))" +apply (subst JN_cons [symmetric]) +apply (auto simp add: cons_absorb) +done + +lemma JN_Un: "(\i \ I Un J. F(i)) = ((\i \ I. F(i)) Join (\i \ J. F(i)))" +apply (rule program_equalityI) +apply (simp_all add: UN_Un INT_Un) +apply (simp_all del: INT_simps add: INT_extend_simps, blast) +done + +lemma JN_constant: "(\i \ I. c) = (if I=0 then SKIP else programify(c))" +by (rule program_equalityI, auto) + +lemma JN_Join_distrib: + "(\i \ I. F(i) Join G(i)) = (\i \ I. F(i)) Join (\i \ I. G(i))" +apply (rule program_equalityI) +apply (simp_all add: Int_absorb) +apply (safe elim!: not_emptyE) +apply (simp_all add: INT_Int_distrib Int_absorb, force) +done + +lemma JN_Join_miniscope: "(\i \ I. F(i) Join G) = ((\i \ I. F(i) Join G))" +by (simp add: JN_Join_distrib JN_constant) + +text{*Used to prove guarantees_JN_I*} +lemma JN_Join_diff: "i \ I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)" +apply (rule program_equalityI) +apply (auto elim!: not_emptyE) +done + +subsection{*Safety: co, stable, FP*} + + +(*Fails if I=0 because it collapses to SKIP \ A co B, i.e. to A\B. So an + alternative precondition is A\B, but most proofs using this rule require + I to be nonempty for other reasons anyway.*) + +lemma JN_constrains: + "i \ I==>(\i \ I. F(i)) \ A co B <-> (\i \ I. programify(F(i)) \ A co B)" + +apply (unfold constrains_def JOIN_def st_set_def, auto) +prefer 2 apply blast +apply (rename_tac j act y z) +apply (cut_tac F = "F (j) " in Acts_type) +apply (drule_tac x = act in bspec, auto) +done + +lemma Join_constrains [iff]: + "(F Join G \ A co B) <-> (programify(F) \ A co B & programify(G) \ A co B)" +by (auto simp add: constrains_def) + +lemma Join_unless [iff]: + "(F Join G \ A unless B) <-> + (programify(F) \ A unless B & programify(G) \ A unless B)" +by (simp add: Join_constrains unless_def) + + +(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. + reachable (F Join G) could be much bigger than reachable F, reachable G +*) + +lemma Join_constrains_weaken: + "[| F \ A co A'; G \ B co B' |] + ==> F Join G \ (A Int B) co (A' Un B')" +apply (subgoal_tac "st_set (A) & st_set (B) & F \ program & G \ program") +prefer 2 apply (blast dest: constrainsD2, simp) +apply (blast intro: constrains_weaken) +done + +(*If I=0, it degenerates to SKIP \ state co 0, which is false.*) +lemma JN_constrains_weaken: + assumes major: "(!!i. i \ I ==> F(i) \ A(i) co A'(i))" + and minor: "i \ I" + shows "(\i \ I. F(i)) \ (\i \ I. A(i)) co (\i \ I. A'(i))" +apply (cut_tac minor) +apply (simp (no_asm_simp) add: JN_constrains) +apply clarify +apply (rename_tac "j") +apply (frule_tac i = j in major) +apply (frule constrainsD2, simp) +apply (blast intro: constrains_weaken) +done + +lemma JN_stable: + "(\i \ I. F(i)) \ stable(A) <-> ((\i \ I. programify(F(i)) \ stable(A)) & st_set(A))" +apply (auto simp add: stable_def constrains_def JOIN_def) +apply (cut_tac F = "F (i) " in Acts_type) +apply (drule_tac x = act in bspec, auto) +done + +lemma initially_JN_I: + assumes major: "(!!i. i \ I ==>F(i) \ initially(A))" + and minor: "i \ I" + shows "(\i \ I. F(i)) \ initially(A)" +apply (cut_tac minor) +apply (auto elim!: not_emptyE simp add: Inter_iff initially_def) +apply (frule_tac i = x in major) +apply (auto simp add: initially_def) +done + +lemma invariant_JN_I: + assumes major: "(!!i. i \ I ==> F(i) \ invariant(A))" + and minor: "i \ I" + shows "(\i \ I. F(i)) \ invariant(A)" +apply (cut_tac minor) +apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable) +apply (erule_tac V = "i \ I" in thin_rl) +apply (frule major) +apply (drule_tac [2] major) +apply (auto simp add: invariant_def) +apply (frule stableD2, force)+ +done + +lemma Join_stable [iff]: + " (F Join G \ stable(A)) <-> + (programify(F) \ stable(A) & programify(G) \ stable(A))" +by (simp add: stable_def) + +lemma initially_JoinI [intro!]: + "[| F \ initially(A); G \ initially(A) |] ==> F Join G \ initially(A)" +by (unfold initially_def, auto) + +lemma invariant_JoinI: + "[| F \ invariant(A); G \ invariant(A) |] + ==> F Join G \ invariant(A)" +apply (subgoal_tac "F \ program&G \ program") +prefer 2 apply (blast dest: invariantD2) +apply (simp add: invariant_def) +apply (auto intro: Join_in_program) +done + + +(* Fails if I=0 because \i \ 0. A(i) = 0 *) +lemma FP_JN: "i \ I ==> FP(\i \ I. F(i)) = (\i \ I. FP (programify(F(i))))" +by (auto simp add: FP_def Inter_def st_set_def JN_stable) + +subsection{*Progress: transient, ensures*} + +lemma JN_transient: + "i \ I ==> + (\i \ I. F(i)) \ transient(A) <-> (\i \ I. programify(F(i)) \ transient(A))" +apply (auto simp add: transient_def JOIN_def) +apply (unfold st_set_def) +apply (drule_tac [2] x = act in bspec) +apply (auto dest: Acts_type [THEN subsetD]) +done + +lemma Join_transient [iff]: + "F Join G \ transient(A) <-> + (programify(F) \ transient(A) | programify(G) \ transient(A))" +apply (auto simp add: transient_def Join_def Int_Un_distrib2) +done + +lemma Join_transient_I1: "F \ transient(A) ==> F Join G \ transient(A)" +by (simp add: Join_transient transientD2) + + +lemma Join_transient_I2: "G \ transient(A) ==> F Join G \ transient(A)" +by (simp add: Join_transient transientD2) + +(*If I=0 it degenerates to (SKIP \ A ensures B) = False, i.e. to ~(A\B) *) +lemma JN_ensures: + "i \ I ==> + (\i \ I. F(i)) \ A ensures B <-> + ((\i \ I. programify(F(i)) \ (A-B) co (A Un B)) & + (\i \ I. programify(F(i)) \ A ensures B))" +by (auto simp add: ensures_def JN_constrains JN_transient) + + +lemma Join_ensures: + "F Join G \ A ensures B <-> + (programify(F) \ (A-B) co (A Un B) & programify(G) \ (A-B) co (A Un B) & + (programify(F) \ transient (A-B) | programify(G) \ transient (A-B)))" + +apply (unfold ensures_def) +apply (auto simp add: Join_transient) +done + +lemma stable_Join_constrains: + "[| F \ stable(A); G \ A co A' |] + ==> F Join G \ A co A'" +apply (unfold stable_def constrains_def Join_def st_set_def) +apply (cut_tac F = F in Acts_type) +apply (cut_tac F = G in Acts_type, force) +done + +(*Premise for G cannot use Always because F \ Stable A is + weaker than G \ stable A *) +lemma stable_Join_Always1: + "[| F \ stable(A); G \ invariant(A) |] ==> F Join G \ Always(A)" +apply (subgoal_tac "F \ program & G \ program & st_set (A) ") +prefer 2 apply (blast dest: invariantD2 stableD2) +apply (simp add: Always_def invariant_def initially_def Stable_eq_stable) +apply (force intro: stable_Int) +done + +(*As above, but exchanging the roles of F and G*) +lemma stable_Join_Always2: + "[| F \ invariant(A); G \ stable(A) |] ==> F Join G \ Always(A)" +apply (subst Join_commute) +apply (blast intro: stable_Join_Always1) +done + + + +lemma stable_Join_ensures1: + "[| F \ stable(A); G \ A ensures B |] ==> F Join G \ A ensures B" +apply (subgoal_tac "F \ program & G \ program & st_set (A) ") +prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD]) +apply (simp (no_asm_simp) add: Join_ensures) +apply (simp add: stable_def ensures_def) +apply (erule constrains_weaken, auto) +done + + +(*As above, but exchanging the roles of F and G*) +lemma stable_Join_ensures2: + "[| F \ A ensures B; G \ stable(A) |] ==> F Join G \ A ensures B" +apply (subst Join_commute) +apply (blast intro: stable_Join_ensures1) +done + +subsection{*The ok and OK relations*} + +lemma ok_SKIP1 [iff]: "SKIP ok F" +by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) + +lemma ok_SKIP2 [iff]: "F ok SKIP" +by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) + +lemma ok_Join_commute: + "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))" +by (auto simp add: ok_def) + +lemma ok_commute: "(F ok G) <->(G ok F)" +by (auto simp add: ok_def) + +lemmas ok_sym = ok_commute [THEN iffD1, standard] + +lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)" +by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb + Int_Un_distrib2 Ball_def, safe, force+) + +lemma ok_Join_iff1 [iff]: "F ok (G Join H) <-> (F ok G & F ok H)" +by (auto simp add: ok_def) + +lemma ok_Join_iff2 [iff]: "(G Join H) ok F <-> (G ok F & H ok F)" +by (auto simp add: ok_def) + +(*useful? Not with the previous two around*) +lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" +by (auto simp add: ok_def) + +lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) <-> (\i \ I. F ok G(i))" +by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def) + +lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F <-> (\i \ I. G(i) ok F)" +apply (auto elim!: not_emptyE simp add: ok_def) +apply (blast dest: Acts_type [THEN subsetD]) +done + +lemma OK_iff_ok: "OK(I,F) <-> (\i \ I. \j \ I-{i}. F(i) ok (F(j)))" +by (auto simp add: ok_def OK_def) + +lemma OK_imp_ok: "[| OK(I,F); i \ I; j \ I; i\j|] ==> F(i) ok F(j)" +by (auto simp add: OK_iff_ok) + + +subsection{*Allowed*} + +lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program" +by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def) + +lemma Allowed_Join [simp]: + "Allowed(F Join G) = + Allowed(programify(F)) Int Allowed(programify(G))" +apply (auto simp add: Allowed_def) +done + +lemma Allowed_JN [simp]: + "i \ I ==> + Allowed(JOIN(I,F)) = (\i \ I. Allowed(programify(F(i))))" +apply (auto simp add: Allowed_def, blast) +done + +lemma ok_iff_Allowed: + "F ok G <-> (programify(F) \ Allowed(programify(G)) & + programify(G) \ Allowed(programify(F)))" +by (simp add: ok_def Allowed_def) + + +lemma OK_iff_Allowed: + "OK(I,F) <-> + (\i \ I. \j \ I-{i}. programify(F(i)) \ Allowed(programify(F(j))))" +apply (auto simp add: OK_iff_ok ok_iff_Allowed) +done + +subsection{*safety_prop, for reasoning about given instances of "ok"*} + +lemma safety_prop_Acts_iff: + "safety_prop(X) ==> (Acts(G) \ cons(id(state), (\F \ X. Acts(F)))) <-> (programify(G) \ X)" +apply (simp (no_asm_use) add: safety_prop_def) +apply clarify +apply (case_tac "G \ program", simp_all, blast, safe) +prefer 2 apply force +apply (force simp add: programify_def) +done + +lemma safety_prop_AllowedActs_iff_Allowed: + "safety_prop(X) ==> + (\G \ X. Acts(G)) \ AllowedActs(F) <-> (X \ Allowed(programify(F)))" +apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym] + safety_prop_def, blast) +done + + +lemma Allowed_eq: + "safety_prop(X) ==> Allowed(mk_program(init, acts, \F \ X. Acts(F))) = X" +apply (subgoal_tac "cons (id (state), Union (RepFun (X, Acts)) Int Pow (state * state)) = Union (RepFun (X, Acts))") +apply (rule_tac [2] equalityI) + apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto) +apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+ +done + +lemma def_prg_Allowed: + "[| F == mk_program (init, acts, \F \ X. Acts(F)); safety_prop(X) |] + ==> Allowed(F) = X" +by (simp add: Allowed_eq) + +(*For safety_prop to hold, the property must be satisfiable!*) +lemma safety_prop_constrains [iff]: + "safety_prop(A co B) <-> (A \ B & st_set(A))" +by (simp add: safety_prop_def constrains_def st_set_def, blast) + +(* To be used with resolution *) +lemma safety_prop_constrainsI [iff]: + "[| A\B; st_set(A) |] ==>safety_prop(A co B)" +by auto + +lemma safety_prop_stable [iff]: "safety_prop(stable(A)) <-> st_set(A)" +by (simp add: stable_def) + +lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))" +by auto + +lemma safety_prop_Int [simp]: + "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)" +apply (simp add: safety_prop_def, safe, blast) +apply (drule_tac [2] B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (Y, Acts))" in subset_trans) +apply (drule_tac B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (X, Acts))" in subset_trans) +apply blast+ +done + +(* If I=0 the conclusion becomes safety_prop(0) which is false *) +lemma safety_prop_Inter: + assumes major: "(!!i. i \ I ==>safety_prop(X(i)))" + and minor: "i \ I" + shows "safety_prop(\i \ I. X(i))" +apply (simp add: safety_prop_def) +apply (cut_tac minor, safe) +apply (simp (no_asm_use) add: Inter_iff) +apply clarify +apply (frule major) +apply (drule_tac [2] i = xa in major) +apply (frule_tac [4] i = xa in major) +apply (auto simp add: safety_prop_def) +apply (drule_tac B = "Union (RepFun (Inter (RepFun (I, X)), Acts))" and C = "Union (RepFun (X (xa), Acts))" in subset_trans) +apply blast+ +done + +lemma def_UNION_ok_iff: +"[| F == mk_program(init,acts, \G \ X. Acts(G)); safety_prop(X) |] + ==> F ok G <-> (programify(G) \ X & acts Int Pow(state*state) \ AllowedActs(G))" +apply (unfold ok_def) +apply (drule_tac G = G in safety_prop_Acts_iff) +apply (cut_tac F = G in AllowedActs_type) +apply (cut_tac F = G in Acts_type, auto) +done + + +ML +{* +val safety_prop_def = thm "safety_prop_def"; + +val reachable_SKIP = thm "reachable_SKIP"; +val ok_programify_left = thm "ok_programify_left"; +val ok_programify_right = thm "ok_programify_right"; +val Join_programify_left = thm "Join_programify_left"; +val Join_programify_right = thm "Join_programify_right"; +val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; +val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; +val SKIP_in_stable = thm "SKIP_in_stable"; +val SKIP_in_Stable = thm "SKIP_in_Stable"; +val Join_in_program = thm "Join_in_program"; +val JOIN_in_program = thm "JOIN_in_program"; +val Init_Join = thm "Init_Join"; +val Acts_Join = thm "Acts_Join"; +val AllowedActs_Join = thm "AllowedActs_Join"; +val Join_commute = thm "Join_commute"; +val Join_left_commute = thm "Join_left_commute"; +val Join_assoc = thm "Join_assoc"; +val cons_id = thm "cons_id"; +val Join_SKIP_left = thm "Join_SKIP_left"; +val Join_SKIP_right = thm "Join_SKIP_right"; +val Join_absorb = thm "Join_absorb"; +val Join_left_absorb = thm "Join_left_absorb"; +val OK_programify = thm "OK_programify"; +val JN_programify = thm "JN_programify"; +val JN_empty = thm "JN_empty"; +val Init_JN = thm "Init_JN"; +val Acts_JN = thm "Acts_JN"; +val AllowedActs_JN = thm "AllowedActs_JN"; +val JN_cons = thm "JN_cons"; +val JN_cong = thm "JN_cong"; +val JN_absorb = thm "JN_absorb"; +val JN_Un = thm "JN_Un"; +val JN_constant = thm "JN_constant"; +val JN_Join_distrib = thm "JN_Join_distrib"; +val JN_Join_miniscope = thm "JN_Join_miniscope"; +val JN_Join_diff = thm "JN_Join_diff"; +val JN_constrains = thm "JN_constrains"; +val Join_constrains = thm "Join_constrains"; +val Join_unless = thm "Join_unless"; +val Join_constrains_weaken = thm "Join_constrains_weaken"; +val JN_constrains_weaken = thm "JN_constrains_weaken"; +val JN_stable = thm "JN_stable"; +val initially_JN_I = thm "initially_JN_I"; +val invariant_JN_I = thm "invariant_JN_I"; +val Join_stable = thm "Join_stable"; +val initially_JoinI = thm "initially_JoinI"; +val invariant_JoinI = thm "invariant_JoinI"; +val FP_JN = thm "FP_JN"; +val JN_transient = thm "JN_transient"; +val Join_transient = thm "Join_transient"; +val Join_transient_I1 = thm "Join_transient_I1"; +val Join_transient_I2 = thm "Join_transient_I2"; +val JN_ensures = thm "JN_ensures"; +val Join_ensures = thm "Join_ensures"; +val stable_Join_constrains = thm "stable_Join_constrains"; +val stable_Join_Always1 = thm "stable_Join_Always1"; +val stable_Join_Always2 = thm "stable_Join_Always2"; +val stable_Join_ensures1 = thm "stable_Join_ensures1"; +val stable_Join_ensures2 = thm "stable_Join_ensures2"; +val ok_SKIP1 = thm "ok_SKIP1"; +val ok_SKIP2 = thm "ok_SKIP2"; +val ok_Join_commute = thm "ok_Join_commute"; +val ok_commute = thm "ok_commute"; +val ok_sym = thm "ok_sym"; +val ok_iff_OK = thm "ok_iff_OK"; +val ok_Join_iff1 = thm "ok_Join_iff1"; +val ok_Join_iff2 = thm "ok_Join_iff2"; +val ok_Join_commute_I = thm "ok_Join_commute_I"; +val ok_JN_iff1 = thm "ok_JN_iff1"; +val ok_JN_iff2 = thm "ok_JN_iff2"; +val OK_iff_ok = thm "OK_iff_ok"; +val OK_imp_ok = thm "OK_imp_ok"; +val Allowed_SKIP = thm "Allowed_SKIP"; +val Allowed_Join = thm "Allowed_Join"; +val Allowed_JN = thm "Allowed_JN"; +val ok_iff_Allowed = thm "ok_iff_Allowed"; +val OK_iff_Allowed = thm "OK_iff_Allowed"; +val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; +val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; +val Allowed_eq = thm "Allowed_eq"; +val def_prg_Allowed = thm "def_prg_Allowed"; +val safety_prop_constrains = thm "safety_prop_constrains"; +val safety_prop_constrainsI = thm "safety_prop_constrainsI"; +val safety_prop_stable = thm "safety_prop_stable"; +val safety_prop_stableI = thm "safety_prop_stableI"; +val safety_prop_Int = thm "safety_prop_Int"; +val safety_prop_Inter = thm "safety_prop_Inter"; +val def_UNION_ok_iff = thm "def_UNION_ok_iff"; + +val Join_ac = thms "Join_ac"; +*} + end diff -r ad6ba9c55190 -r 68da54626309 src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Mon Jul 07 17:58:21 2003 +0200 +++ b/src/ZF/UNITY/WFair.ML Tue Jul 08 11:44:30 2003 +0200 @@ -1,5 +1,5 @@ (* Title: HOL/UNITY/WFair.ML - ID: $Id$ + ID: $Id \\ WFair.ML,v 1.13 2003/06/30 16:15:52 paulson Exp $ Author: Sidi O Ehmety, Computer Laboratory Copyright 2001 University of Cambridge @@ -10,11 +10,11 @@ (** Ad-hoc set-theory rules **) -Goal "Union(B) Int A = (UN b:B. b Int A)"; +Goal "Union(B) Int A = (\\b \\ B. b Int A)"; by Auto_tac; qed "Int_Union_Union"; -Goal "A Int Union(B) = (UN b:B. A Int b)"; +Goal "A Int Union(B) = (\\b \\ B. A Int b)"; by Auto_tac; qed "Int_Union_Union2"; @@ -25,16 +25,16 @@ qed "transient_type"; Goalw [transient_def] -"F:transient(A) ==> F:program & st_set(A)"; +"F \\ transient(A) ==> F \\ program & st_set(A)"; by Auto_tac; qed "transientD2"; -Goal "[| F : stable(A); F : transient(A) |] ==> A = 0"; +Goal "[| F \\ stable(A); F \\ transient(A) |] ==> A = 0"; by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1); by (Fast_tac 1); qed "stable_transient_empty"; -Goalw [transient_def, st_set_def] "[|F:transient(A); B<=A|] ==> F:transient(B)"; +Goalw [transient_def, st_set_def] "[|F \\ transient(A); B<=A|] ==> F \\ transient(B)"; by Safe_tac; by (res_inst_tac [("x", "act")] bexI 1); by (ALLGOALS(Asm_full_simp_tac)); @@ -43,14 +43,14 @@ qed "transient_strengthen"; Goalw [transient_def] -"[|act:Acts(F); A <= domain(act); act``A <= state-A; \ -\ F:program; st_set(A)|] ==> F:transient(A)"; +"[|act \\ Acts(F); A <= domain(act); act``A <= state-A; \ +\ F \\ program; st_set(A)|] ==> F \\ transient(A)"; by (Blast_tac 1); qed "transientI"; val major::prems = -Goalw [transient_def] "[| F:transient(A); \ -\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P"; +Goalw [transient_def] "[| F \\ transient(A); \ +\ !!act. [| act \\ Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P"; by (rtac (major RS CollectE) 1); by (blast_tac (claset() addIs prems) 1); qed "transientE"; @@ -86,29 +86,29 @@ qed "ensures_type"; Goalw [ensures_def] -"[|F:(A-B) co (A Un B); F:transient(A-B)|]==>F:A ensures B"; +"[|F:(A-B) co (A Un B); F \\ transient(A-B)|]==>F \\ A ensures B"; by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD])); qed "ensuresI"; (* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *) -Goal "[| F:A co A Un B; F: transient(A) |] ==> F: A ensures B"; +Goal "[| F \\ A co A Un B; F \\ transient(A) |] ==> F \\ A ensures B"; by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); by (auto_tac (claset(), simpset() addsimps [ensures_def, transient_type RS subsetD])); qed "ensuresI2"; -Goalw [ensures_def] "F:A ensures B ==> F:(A-B) co (A Un B) & F:transient (A-B)"; +Goalw [ensures_def] "F \\ A ensures B ==> F:(A-B) co (A Un B) & F \\ transient (A-B)"; by Auto_tac; qed "ensuresD"; -Goalw [ensures_def] "[|F:A ensures A'; A'<=B' |] ==> F:A ensures B'"; +Goalw [ensures_def] "[|F \\ A ensures A'; A'<=B' |] ==> F \\ A ensures B'"; by (blast_tac (claset() addIs [transient_strengthen, constrains_weaken]) 1); qed "ensures_weaken_R"; (*The L-version (precondition strengthening) fails, but we have this*) Goalw [ensures_def] - "[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)"; + "[| F \\ stable(C); F \\ A ensures B |] ==> F:(C Int A) ensures (C Int B)"; by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym]) 1); by (blast_tac (claset() @@ -116,7 +116,7 @@ stable_constrains_Int, constrains_weaken]) 1); qed "stable_ensures_Int"; -Goal "[|F:stable(A); F:transient(C); A<=B Un C|] ==> F : A ensures B"; +Goal "[|F \\ stable(A); F \\ transient(C); A<=B Un C|] ==> F \\ A ensures B"; by (forward_tac [stable_type RS subsetD] 1); by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); by (Clarify_tac 1); @@ -128,7 +128,7 @@ by (auto_tac (claset(), simpset() addsimps [ensures_def, unless_def])); qed "ensures_eq"; -Goal "[| F:program; A<=B |] ==> F : A ensures B"; +Goal "[| F \\ program; A<=B |] ==> F \\ A ensures B"; by (rewrite_goal_tac [ensures_def,constrains_def,transient_def, st_set_def] 1); by Auto_tac; qed "subset_imp_ensures"; @@ -142,27 +142,27 @@ qed "leadsTo_type"; Goalw [leadsTo_def, st_set_def] -"F: A leadsTo B ==> F:program & st_set(A) & st_set(B)"; +"F \\ A leadsTo B ==> F \\ program & st_set(A) & st_set(B)"; by (blast_tac (claset() addDs [leads_left, leads_right]) 1); qed "leadsToD2"; Goalw [leadsTo_def, st_set_def] - "[|F:A ensures B; st_set(A); st_set(B)|] ==> F:A leadsTo B"; + "[|F \\ A ensures B; st_set(A); st_set(B)|] ==> F \\ A leadsTo B"; by (cut_facts_tac [ensures_type] 1); by (auto_tac (claset() addIs [leads.Basis], simpset())); qed "leadsTo_Basis"; AddIs [leadsTo_Basis]; (* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) -(* [| F:program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) +(* [| F \\ program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); -Goalw [leadsTo_def] "[|F: A leadsTo B; F: B leadsTo C |]==>F: A leadsTo C"; +Goalw [leadsTo_def] "[|F \\ A leadsTo B; F \\ B leadsTo C |]==>F \\ A leadsTo C"; by (auto_tac (claset() addIs [leads.Trans], simpset())); qed "leadsTo_Trans"; (* Better when used in association with leadsTo_weaken_R *) -Goalw [transient_def] "F:transient(A) ==> F : A leadsTo (state-A )"; +Goalw [transient_def] "F \\ transient(A) ==> F \\ A leadsTo (state-A )"; by (rtac (ensuresI RS leadsTo_Basis) 1); by (ALLGOALS(Clarify_tac)); by (blast_tac (claset() addIs [transientI]) 2); @@ -171,17 +171,17 @@ qed "transient_imp_leadsTo"; (*Useful with cancellation, disjunction*) -Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; +Goal "F \\ A leadsTo (A' Un A') ==> F \\ A leadsTo A'"; by (Asm_full_simp_tac 1); qed "leadsTo_Un_duplicate"; -Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; +Goal "F \\ A leadsTo (A' Un C Un C) ==> F \\ A leadsTo (A' Un C)"; by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); qed "leadsTo_Un_duplicate2"; (*The Union introduction rule as we should have liked to state it*) val [major, program,B]= Goalw [leadsTo_def, st_set_def] -"[|(!!A. A:S ==> F:A leadsTo B); F:program; st_set(B)|]==>F:Union(S) leadsTo B"; +"[|(!!A. A \\ S ==> F \\ A leadsTo B); F \\ program; st_set(B)|]==>F \\ Union(S) leadsTo B"; by (cut_facts_tac [program, B] 1); by Auto_tac; by (rtac leads.Union 1); @@ -191,7 +191,7 @@ qed "leadsTo_Union"; val [major,program,B] = Goalw [leadsTo_def, st_set_def] -"[|(!!A. A:S ==>F:(A Int C) leadsTo B); F:program; st_set(B)|] \ +"[|(!!A. A \\ S ==>F:(A Int C) leadsTo B); F \\ program; st_set(B)|] \ \ ==>F:(Union(S)Int C)leadsTo B"; by (cut_facts_tac [program, B] 1); by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1); @@ -202,7 +202,7 @@ qed "leadsTo_Union_Int"; val [major,program,B] = Goalw [leadsTo_def, st_set_def] -"[|(!!i. i:I ==> F : A(i) leadsTo B); F:program; st_set(B)|]==>F:(UN i:I. A(i)) leadsTo B"; +"[|(!!i. i \\ I ==> F \\ A(i) leadsTo B); F \\ program; st_set(B)|]==>F:(\\i \\ I. A(i)) leadsTo B"; by (cut_facts_tac [program, B] 1); by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); by (rtac leads.Union 1); @@ -212,87 +212,87 @@ qed "leadsTo_UN"; (* Binary union introduction rule *) -Goal "[| F: A leadsTo C; F: B leadsTo C |] ==> F : (A Un B) leadsTo C"; +Goal "[| F \\ A leadsTo C; F \\ B leadsTo C |] ==> F \\ (A Un B) leadsTo C"; by (stac Un_eq_Union 1); by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1); qed "leadsTo_Un"; val [major, program, B] = Goal -"[|(!!x. x:A==> F:{x} leadsTo B); F:program; st_set(B) |] ==> F:A leadsTo B"; +"[|(!!x. x \\ A==> F:{x} leadsTo B); F \\ program; st_set(B) |] ==> F \\ A leadsTo B"; by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1); by (rtac leadsTo_UN 1); by (auto_tac (claset() addDs prems, simpset() addsimps [major, program, B])); qed "single_leadsTo_I"; -Goal "[| F:program; st_set(A) |] ==> F: A leadsTo A"; +Goal "[| F \\ program; st_set(A) |] ==> F \\ A leadsTo A"; by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); qed "leadsTo_refl"; -Goal "F: A leadsTo A <-> F:program & st_set(A)"; +Goal "F \\ A leadsTo A <-> F \\ program & st_set(A)"; by (auto_tac (claset() addIs [leadsTo_refl] addDs [leadsToD2], simpset())); qed "leadsTo_refl_iff"; -Goal "F: 0 leadsTo B <-> (F:program & st_set(B))"; +Goal "F \\ 0 leadsTo B <-> (F \\ program & st_set(B))"; by (auto_tac (claset() addIs [subset_imp_leadsTo] addDs [leadsToD2], simpset())); qed "empty_leadsTo"; AddIffs [empty_leadsTo]; -Goal "F: A leadsTo state <-> (F:program & st_set(A))"; +Goal "F \\ A leadsTo state <-> (F \\ program & st_set(A))"; by (auto_tac (claset() addIs [subset_imp_leadsTo] addDs [leadsToD2, st_setD], simpset())); qed "leadsTo_state"; AddIffs [leadsTo_state]; -Goal "[| F:A leadsTo A'; A'<=B'; st_set(B') |] ==> F : A leadsTo B'"; +Goal "[| F \\ A leadsTo A'; A'<=B'; st_set(B') |] ==> F \\ A leadsTo B'"; by (blast_tac (claset() addDs [leadsToD2] addIs [subset_imp_leadsTo,leadsTo_Trans]) 1); qed "leadsTo_weaken_R"; -Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; +Goal "[| F \\ A leadsTo A'; B<=A |] ==> F \\ B leadsTo A'"; by (ftac leadsToD2 1); by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1); qed_spec_mp "leadsTo_weaken_L"; -Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'"; +Goal "[| F \\ A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \\ B leadsTo B'"; by (ftac leadsToD2 1); by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, leadsTo_Trans, leadsTo_refl]) 1); qed "leadsTo_weaken"; (* This rule has a nicer conclusion *) -Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B"; +Goal "[| F \\ transient(A); state-A<=B; st_set(B)|] ==> F \\ A leadsTo B"; by (ftac transientD2 1); by (rtac leadsTo_weaken_R 1); by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo])); qed "transient_imp_leadsTo2"; (*Distributes over binary unions*) -Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)"; +Goal "F:(A Un B) leadsTo C <-> (F \\ A leadsTo C & F \\ B leadsTo C)"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); qed "leadsTo_Un_distrib"; Goal -"(F:(UN i:I. A(i)) leadsTo B)<-> ((ALL i : I. F: A(i) leadsTo B) & F:program & st_set(B))"; +"(F:(\\i \\ I. A(i)) leadsTo B)<-> ((\\i \\ I. F \\ A(i) leadsTo B) & F \\ program & st_set(B))"; by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_UN, leadsTo_weaken_L]) 1); qed "leadsTo_UN_distrib"; -Goal "(F: Union(S) leadsTo B) <-> (ALL A:S. F : A leadsTo B) & F:program & st_set(B)"; +Goal "(F \\ Union(S) leadsTo B) <-> (\\A \\ S. F \\ A leadsTo B) & F \\ program & st_set(B)"; by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_Union, leadsTo_weaken_L]) 1); qed "leadsTo_Union_distrib"; -(*Set difference: maybe combine with leadsTo_weaken_L?*) -Goal "[| F: (A-B) leadsTo C; F: B leadsTo C; st_set(C) |] ==> F: A leadsTo C"; +(*Set difference \\ maybe combine with leadsTo_weaken_L?*) +Goal "[| F: (A-B) leadsTo C; F \\ B leadsTo C; st_set(C) |] ==> F \\ A leadsTo C"; by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken] addDs [leadsToD2]) 1); qed "leadsTo_Diff"; val [major,minor] = Goal -"[|(!!i. i:I ==> F: A(i) leadsTo A'(i)); F:program |] \ -\ ==> F: (UN i:I. A(i)) leadsTo (UN i:I. A'(i))"; +"[|(!!i. i \\ I ==> F \\ A(i) leadsTo A'(i)); F \\ program |] \ +\ ==> F: (\\i \\ I. A(i)) leadsTo (\\i \\ I. A'(i))"; by (rtac leadsTo_Union 1); by (ALLGOALS(Asm_simp_tac)); by Safe_tac; @@ -302,32 +302,32 @@ qed "leadsTo_UN_UN"; (*Binary union version*) -Goal "[| F: A leadsTo A'; F:B leadsTo B' |] ==> F : (A Un B) leadsTo (A' Un B')"; +Goal "[| F \\ A leadsTo A'; F \\ B leadsTo B' |] ==> F \\ (A Un B) leadsTo (A' Un B')"; by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B')" 1); by (blast_tac (claset() addDs [leadsToD2]) 2); by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); qed "leadsTo_Un_Un"; (** The cancellation law **) -Goal "[|F: A leadsTo (A' Un B); F: B leadsTo B'|] ==> F: A leadsTo (A' Un B')"; -by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F:program" 1); +Goal "[|F \\ A leadsTo (A' Un B); F \\ B leadsTo B'|] ==> F \\ A leadsTo (A' Un B')"; +by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F \\ program" 1); by (blast_tac (claset() addDs [leadsToD2]) 2); by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]) 1); qed "leadsTo_cancel2"; -Goal "[|F: A leadsTo (A' Un B); F : (B-A') leadsTo B'|]==> F: A leadsTo (A' Un B')"; +Goal "[|F \\ A leadsTo (A' Un B); F \\ (B-A') leadsTo B'|]==> F \\ A leadsTo (A' Un B')"; by (rtac leadsTo_cancel2 1); by (assume_tac 2); by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_weaken_R]) 1); qed "leadsTo_cancel_Diff2"; -Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] ==> F:A leadsTo (B' Un A')"; +Goal "[| F \\ A leadsTo (B Un A'); F \\ B leadsTo B' |] ==> F \\ A leadsTo (B' Un A')"; by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); qed "leadsTo_cancel1"; -Goal "[|F: A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F : A leadsTo (B' Un A')"; +Goal "[|F \\ A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F \\ A leadsTo (B' Un A')"; by (rtac leadsTo_cancel1 1); by (assume_tac 2); by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [leadsToD2]) 1); @@ -335,12 +335,12 @@ (*The INDUCTION rule as we should have liked to state it*) val [major, basis_prem, trans_prem, union_prem] = Goalw [leadsTo_def, st_set_def] - "[| F: za leadsTo zb; \ -\ !!A B. [| F: A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \ -\ !!A B C. [| F: A leadsTo B; P(A, B); \ -\ F: B leadsTo C; P(B, C) |] \ + "[| F \\ za leadsTo zb; \ +\ !!A B. [| F \\ A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \ +\ !!A B C. [| F \\ A leadsTo B; P(A, B); \ +\ F \\ B leadsTo C; P(B, C) |] \ \ ==> P(A, C); \ -\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A)|] \ +\ !!B S. [| \\A \\ S. F \\ A leadsTo B; \\A \\ S. P(A, B); st_set(B); \\A \\ S. st_set(A)|] \ \ ==> P(Union(S), B) \ \ |] ==> P(za, zb)"; by (cut_facts_tac [major] 1); @@ -353,13 +353,13 @@ (* Added by Sidi, an induction rule without ensures *) val [major,imp_prem,basis_prem,trans_prem,union_prem] = Goal - "[| F: za leadsTo zb; \ + "[| F \\ za leadsTo zb; \ \ !!A B. [| A<=B; st_set(B) |] ==> P(A, B); \ -\ !!A B. [| F:A co A Un B; F:transient(A); st_set(B) |] ==> P(A, B); \ -\ !!A B C. [| F: A leadsTo B; P(A, B); \ -\ F: B leadsTo C; P(B, C) |] \ +\ !!A B. [| F \\ A co A Un B; F \\ transient(A); st_set(B) |] ==> P(A, B); \ +\ !!A B C. [| F \\ A leadsTo B; P(A, B); \ +\ F \\ B leadsTo C; P(B, C) |] \ \ ==> P(A, C); \ -\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A) |] \ +\ !!B S. [| \\A \\ S. F \\ A leadsTo B; \\A \\ S. P(A, B); st_set(B); \\A \\ S. st_set(A) |] \ \ ==> P(Union(S), B) \ \ |] ==> P(za, zb)"; by (cut_facts_tac [major] 1); @@ -381,17 +381,17 @@ by (auto_tac (claset() addIs [subset_imp_leadsTo], simpset())); qed "leadsTo_induct2"; -(** Variant induction rule: on the preconditions for B **) -(*Lemma is the weak version: can't see how to do it in one step*) +(** Variant induction rule \\ on the preconditions for B **) +(*Lemma is the weak version \\ can't see how to do it in one step*) val major::prems = Goal - "[| F : za leadsTo zb; \ + "[| F \\ za leadsTo zb; \ \ P(zb); \ -\ !!A B. [| F : A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \ -\ !!S. [| ALL A:S. P(A); ALL A:S. st_set(A) |] ==> P(Union(S)) \ +\ !!A B. [| F \\ A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \ +\ !!S. [| \\A \\ S. P(A); \\A \\ S. st_set(A) |] ==> P(Union(S)) \ \ |] ==> P(za)"; (*by induction on this formula*) by (subgoal_tac "P(zb) --> P(za)" 1); -(*now solve first subgoal: this formula is sufficient*) +(*now solve first subgoal \\ this formula is sufficient*) by (blast_tac (claset() addIs leadsTo_refl::prems) 1); by (rtac (major RS leadsTo_induct) 1); by (REPEAT (blast_tac (claset() addIs prems) 1)); @@ -399,13 +399,13 @@ val [major, zb_prem, basis_prem, union_prem] = Goal - "[| F : za leadsTo zb; \ + "[| F \\ za leadsTo zb; \ \ P(zb); \ -\ !!A B. [| F : A ensures B; F : B leadsTo zb; P(B); st_set(A) |] ==> P(A); \ -\ !!S. ALL A:S. F : A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \ +\ !!A B. [| F \\ A ensures B; F \\ B leadsTo zb; P(B); st_set(A) |] ==> P(A); \ +\ !!S. \\A \\ S. F \\ A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \ \ |] ==> P(za)"; by (cut_facts_tac [major] 1); -by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1); +by (subgoal_tac "(F \\ za leadsTo zb) & P(za)" 1); by (etac conjunct2 1); by (rtac (major RS leadsTo_induct_pre_aux) 1); by (blast_tac (claset() addDs [leadsToD2] @@ -417,7 +417,7 @@ (** The impossibility law **) Goal - "F : A leadsTo 0 ==> A=0"; + "F \\ A leadsTo 0 ==> A=0"; by (etac leadsTo_induct_pre 1); by (auto_tac (claset(), simpset() addsimps [ensures_def, constrains_def, transient_def, st_set_def])); @@ -426,11 +426,11 @@ qed "leadsTo_empty"; Addsimps [leadsTo_empty]; -(** PSP: Progress-Safety-Progress **) +(** PSP \\ Progress-Safety-Progress **) -(*Special case of PSP: Misra's "stable conjunction"*) +(*Special case of PSP \\ Misra's "stable conjunction"*) Goalw [stable_def] - "[| F : A leadsTo A'; F : stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"; + "[| F \\ A leadsTo A'; F \\ stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"; by (etac leadsTo_induct 1); by (rtac leadsTo_Union_Int 3); by (ALLGOALS(Asm_simp_tac)); @@ -446,21 +446,21 @@ qed "psp_stable"; -Goal "[|F: A leadsTo A'; F : stable(B) |]==>F: (B Int A) leadsTo (B Int A')"; +Goal "[|F \\ A leadsTo A'; F \\ stable(B) |]==>F: (B Int A) leadsTo (B Int A')"; by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); qed "psp_stable2"; Goalw [ensures_def, constrains_def, st_set_def] -"[| F: A ensures A'; F: B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"; +"[| F \\ A ensures A'; F \\ B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"; (*speeds up the proof*) by (Clarify_tac 1); by (blast_tac (claset() addIs [transient_strengthen]) 1); qed "psp_ensures"; Goal -"[|F:A leadsTo A'; F: B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"; -by (subgoal_tac "F:program & st_set(A) & st_set(A')& st_set(B)" 1); +"[|F \\ A leadsTo A'; F \\ B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"; +by (subgoal_tac "F \\ program & st_set(A) & st_set(A')& st_set(B)" 1); by (blast_tac (claset() addSDs [constrainsD2, leadsToD2]) 2); by (etac leadsTo_induct 1); by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); @@ -475,14 +475,14 @@ qed "psp"; -Goal "[| F : A leadsTo A'; F : B co B'; st_set(B') |] \ -\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"; +Goal "[| F \\ A leadsTo A'; F \\ B co B'; st_set(B') |] \ +\ ==> F \\ (B' Int A) leadsTo ((B Int A') Un (B' - B))"; by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); qed "psp2"; Goalw [unless_def] - "[| F : A leadsTo A'; F : B unless B'; st_set(B); st_set(B') |] \ -\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; + "[| F \\ A leadsTo A'; F \\ B unless B'; st_set(B); st_set(B') |] \ +\ ==> F \\ (A Int B) leadsTo ((A' Int B) Un B')"; by (subgoal_tac "st_set(A)&st_set(A')" 1); by (blast_tac (claset() addDs [leadsToD2]) 2); by (dtac psp 1); @@ -492,17 +492,17 @@ qed "psp_unless"; (*** Proving the wf induction rules ***) -(** The most general rule: r is any wf relation; f is any variant function **) +(** The most general rule \\ r is any wf relation; f is any variant function **) Goal "[| wf(r); \ -\ m:I; \ +\ m \\ I; \ \ field(r)<=I; \ -\ F:program; st_set(B);\ -\ ALL m:I. F : (A Int f-``{m}) leadsTo \ +\ F \\ program; st_set(B);\ +\ \\m \\ I. F \\ (A Int f-``{m}) leadsTo \ \ ((A Int f-``(converse(r)``{m})) Un B) |] \ -\ ==> F : (A Int f-``{m}) leadsTo B"; +\ ==> F \\ (A Int f-``{m}) leadsTo B"; by (eres_inst_tac [("a","m")] wf_induct2 1); by (ALLGOALS(Asm_simp_tac)); -by (subgoal_tac "F : (A Int (f-``(converse(r)``{x}))) leadsTo B" 1); +by (subgoal_tac "F \\ (A Int (f-``(converse(r)``{x}))) leadsTo B" 1); by (stac vimage_eq_UN 2); by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 2); @@ -515,10 +515,10 @@ Goal "[| wf(r); \ \ field(r)<=I; \ \ A<=f-``I;\ -\ F:program; st_set(A); st_set(B); \ -\ ALL m:I. F : (A Int f-``{m}) leadsTo \ +\ F \\ program; st_set(A); st_set(B); \ +\ \\m \\ I. F \\ (A Int f-``{m}) leadsTo \ \ ((A Int f-``(converse(r)``{m})) Un B) |] \ -\ ==> F : A leadsTo B"; +\ ==> F \\ A leadsTo B"; by (res_inst_tac [("b", "A")] subst 1); by (res_inst_tac [("I", "I")] leadsTo_UN 2); by (REPEAT (assume_tac 2)); @@ -539,7 +539,7 @@ by (rtac equalityI 1); by (force_tac (claset(), simpset()) 1); by (Clarify_tac 1); -by (thin_tac "x~:range(?y)" 1); +by (thin_tac "x\\range(?y)" 1); by (etac nat_induct 1); by (res_inst_tac [("b", "succ(succ(xa))")] domainI 2); by (res_inst_tac [("b","succ(0)")] domainI 1); @@ -557,12 +557,12 @@ by (blast_tac (claset() addIs [lt_trans]) 1); qed "Image_inverse_lessThan"; -(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*) +(*Alternative proof is via the lemma F \\ (A Int f-`(lessThan m)) leadsTo B*) Goal "[| A<=f-``nat;\ -\ F:program; st_set(A); st_set(B); \ -\ ALL m:nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \ -\ ==> F : A leadsTo B"; +\ F \\ program; st_set(A); st_set(B); \ +\ \\m \\ nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \ +\ ==> F \\ A leadsTo B"; by (res_inst_tac [("A1", "nat"),("f1", "%x. x")] (wf_measure RS leadsTo_wf_induct) 1); by (Clarify_tac 6); @@ -584,27 +584,27 @@ qed "wlt_st_set"; AddIffs [wlt_st_set]; -Goalw [wlt_def] "F:wlt(F, B) leadsTo B <-> (F:program & st_set(B))"; +Goalw [wlt_def] "F \\ wlt(F, B) leadsTo B <-> (F \\ program & st_set(B))"; by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1); qed "wlt_leadsTo_iff"; -(* [| F:program; st_set(B) |] ==> F:wlt(F, B) leadsTo B *) +(* [| F \\ program; st_set(B) |] ==> F \\ wlt(F, B) leadsTo B *) bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2)); -Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)"; +Goalw [wlt_def] "F \\ A leadsTo B ==> A <= wlt(F, B)"; by (ftac leadsToD2 1); by (auto_tac (claset(), simpset() addsimps [st_set_def])); qed "leadsTo_subset"; (*Misra's property W2*) -Goal "F : A leadsTo B <-> (A <= wlt(F,B) & F:program & st_set(B))"; +Goal "F \\ A leadsTo B <-> (A <= wlt(F,B) & F \\ program & st_set(B))"; by Auto_tac; by (REPEAT(blast_tac (claset() addDs [leadsToD2,leadsTo_subset] addIs [leadsTo_weaken_L, wlt_leadsTo]) 1)); qed "leadsTo_eq_subset_wlt"; (*Misra's property W4*) -Goal "[| F:program; st_set(B) |] ==> B <= wlt(F,B)"; +Goal "[| F \\ program; st_set(B) |] ==> B <= wlt(F,B)"; by (rtac leadsTo_subset 1); by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS iff_sym, @@ -614,16 +614,16 @@ (*Used in the Trans case below*) Goalw [constrains_def, st_set_def] "[| B <= A2; \ -\ F : (A1 - B) co (A1 Un B); \ -\ F : (A2 - C) co (A2 Un C) |] \ -\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; +\ F \\ (A1 - B) co (A1 Un B); \ +\ F \\ (A2 - C) co (A2 Un C) |] \ +\ ==> F \\ (A1 Un A2 - C) co (A1 Un A2 Un C)"; by (Blast_tac 1); qed "leadsTo_123_aux"; (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) -(* slightly different from the HOL one: B here is bounded *) -Goal "F : A leadsTo A' \ -\ ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')"; +(* slightly different from the HOL one \\ B here is bounded *) +Goal "F \\ A leadsTo A' \ +\ ==> \\B \\ Pow(state). A<=B & F \\ B leadsTo A' & F \\ (B-A') co (B Un A')"; by (ftac leadsToD2 1); by (etac leadsTo_induct 1); (*Basis*) @@ -636,14 +636,14 @@ by (Blast_tac 1); (*Union*) by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1); -by (subgoal_tac "EX y. y:Pi(S, %A. {Ba:Pow(state). A<=Ba & \ - \ F:Ba leadsTo B & F:Ba - B co Ba Un B})" 1); +by (subgoal_tac "\\y. y \\ Pi(S, %A. {Ba \\ Pow(state). A<=Ba & \ + \ F \\ Ba leadsTo B & F \\ Ba - B co Ba Un B})" 1); by (rtac AC_ball_Pi 2); by (ALLGOALS(Clarify_tac)); by (rotate_tac 1 2); by (dres_inst_tac [("x", "x")] bspec 2); by (REPEAT(Blast_tac 2)); -by (res_inst_tac [("x", "UN A:S. y`A")] bexI 1); +by (res_inst_tac [("x", "\\A \\ S. y`A")] bexI 1); by Safe_tac; by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3); by (rtac leadsTo_Union 2); @@ -654,7 +654,7 @@ (*Misra's property W5*) -Goal "[| F:program; st_set(B) |] ==>F : (wlt(F, B) - B) co (wlt(F,B))"; +Goal "[| F \\ program; st_set(B) |] ==>F \\ (wlt(F, B) - B) co (wlt(F,B))"; by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); by (assume_tac 1); by (Blast_tac 1); @@ -666,26 +666,26 @@ addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1); qed "wlt_constrains_wlt"; -(*** Completion: Binary and General Finite versions ***) +(*** Completion \\ Binary and General Finite versions ***) Goal "[| W = wlt(F, (B' Un C)); \ -\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ -\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \ -\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; +\ F \\ A leadsTo (A' Un C); F \\ A' co (A' Un C); \ +\ F \\ B leadsTo (B' Un C); F \\ B' co (B' Un C) |] \ +\ ==> F \\ (A Int B) leadsTo ((A' Int B') Un C)"; by (subgoal_tac "st_set(C)&st_set(W)&st_set(W-C)&st_set(A')&st_set(A)\ -\ & st_set(B) & st_set(B') & F:program" 1); +\ & st_set(B) & st_set(B') & F \\ program" 1); by (Asm_simp_tac 2); by (blast_tac (claset() addSDs [leadsToD2]) 2); -by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1); +by (subgoal_tac "F \\ (W-C) co (W Un B' Un C)" 1); by (blast_tac (claset() addSIs [[asm_rl, wlt_constrains_wlt] MRS constrains_Un RS constrains_weaken]) 2); -by (subgoal_tac "F : (W-C) co W" 1); +by (subgoal_tac "F \\ (W-C) co W" 1); by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1), Un_assoc]) 2); -by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1); +by (subgoal_tac "F \\ (A Int W - C) leadsTo (A' Int W Un C)" 1); by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); (** LEVEL 9 **) -by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); +by (subgoal_tac "F \\ (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); by (rtac leadsTo_Un_duplicate2 2); by (rtac leadsTo_Un_Un 2); by (blast_tac (claset() addIs [leadsTo_refl]) 3); @@ -703,10 +703,10 @@ qed "completion_aux"; bind_thm("completion", refl RS completion_aux); -Goal "[| I:Fin(X); F:program; st_set(C) |] ==> \ -\(ALL i:I. F : (A(i)) leadsTo (A'(i) Un C)) --> \ -\ (ALL i:I. F : (A'(i)) co (A'(i) Un C)) --> \ -\ F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; +Goal "[| I \\ Fin(X); F \\ program; st_set(C) |] ==> \ +\(\\i \\ I. F \\ (A(i)) leadsTo (A'(i) Un C)) --> \ +\ (\\i \\ I. F \\ (A'(i)) co (A'(i) Un C)) --> \ +\ F \\ (\\i \\ I. A(i)) leadsTo ((\\i \\ I. A'(i)) Un C)"; by (etac Fin_induct 1); by (auto_tac (claset(), simpset() addsimps [Inter_0])); by (rtac completion 1); @@ -717,19 +717,19 @@ qed "lemma"; val prems = Goal - "[| I:Fin(X); \ -\ !!i. i:I ==> F : A(i) leadsTo (A'(i) Un C); \ -\ !!i. i:I ==> F : A'(i) co (A'(i) Un C); F:program; st_set(C)|] \ -\ ==> F : (INT i:I. A(i)) leadsTo ((INT i:I. A'(i)) Un C)"; + "[| I \\ Fin(X); \ +\ !!i. i \\ I ==> F \\ A(i) leadsTo (A'(i) Un C); \ +\ !!i. i \\ I ==> F \\ A'(i) co (A'(i) Un C); F \\ program; st_set(C)|] \ +\ ==> F \\ (\\i \\ I. A(i)) leadsTo ((\\i \\ I. A'(i)) Un C)"; by (resolve_tac [lemma RS mp RS mp] 1); by (resolve_tac prems 3); by (REPEAT(blast_tac (claset() addIs prems) 1)); qed "finite_completion"; Goalw [stable_def] - "[| F : A leadsTo A'; F : stable(A'); \ -\ F : B leadsTo B'; F : stable(B') |] \ -\ ==> F : (A Int B) leadsTo (A' Int B')"; + "[| 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", "0")] (completion RS leadsTo_weaken_R) 1); by (REPEAT(blast_tac (claset() addDs [leadsToD2, constrainsD2]) 5)); by (ALLGOALS(Asm_full_simp_tac)); @@ -737,12 +737,12 @@ val major::prems = Goalw [stable_def] - "[| I:Fin(X); \ -\ (!!i. i:I ==> F : A(i) leadsTo A'(i)); \ -\ (!!i. i:I ==> F: stable(A'(i))); F:program |] \ -\ ==> F : (INT i:I. A(i)) leadsTo (INT i:I. A'(i))"; + "[| I \\ Fin(X); \ +\ (!!i. i \\ I ==> F \\ A(i) leadsTo A'(i)); \ +\ (!!i. i \\ I ==> F \\ stable(A'(i))); F \\ program |] \ +\ ==> F \\ (\\i \\ I. A(i)) leadsTo (\\i \\ I. A'(i))"; by (cut_facts_tac [major] 1); -by (subgoal_tac "st_set(INT i:I. A'(i))" 1); +by (subgoal_tac "st_set(\\i \\ I. A'(i))" 1); by (blast_tac (claset() addDs [leadsToD2]@prems) 2); by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1); by (Asm_simp_tac 1);