Conversion of ZF/UNITY/{FP,Union} to Isar script.
Introduction of X-symbols to the ML files.
--- 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\
--- 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> program==>(JOIN(I,F) component H) <-> (\\<forall>i \\<in> 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 \\<in> I ==> F(i) component (\\<Squnion>i \\<in> 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 \\<in> program; G \\<in> 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 \\<in> 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 \\<in> A co B; F \\<in> program |] ==> F \\<in> 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)";
+"\\<forall>z. F \\<in> stable({s \\<in> state. f(s) = z}) ==> F \\<in> 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); <s,t> : act |] ==> f(s) = f(t)";
-by (subgoal_tac "s:state & t:state" 1);
+ "[| F \\<in> preserves(f); act \\<in> Acts(F); <s,t> \\<in> act |] ==> f(s) = f(t)";
+by (subgoal_tac "s \\<in> state & t \\<in> 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 \\<in> preserves(v)) <-> \
+\ (programify(F) \\<in> preserves(v) & programify(G) \\<in> 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)) <-> (\\<forall>i \\<in> 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 \\<in> 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 \\<in> preserves(fun_pair(v, w)) <-> F \\<in> 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 \\<in> preserves(f) ==> F \\<in> 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 \\<in> preserves(f) ==> F \\<in> 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 \\<in> 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 \\<in> preserves(f) ==> F \\<in> stable({s \\<in> 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 \\<in> preserves(f); \\<forall>x \\<in> state. f(x):A |] ==> F \\<in> Increasing.increasing(A, r, f)";
by (auto_tac (claset() addIs [preserves_into_program],
simpset()));
by (res_inst_tac [("P", "%x. <k, 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 \\<in> preserves(%x. x); st_set(A) |] ==> F \\<in> 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 \\<in> 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 \\<in> 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 (\\<Union>G \\<in> 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 \\<in> stable({s \\<in> state. P(f(s), g(s))}); G \\<in> preserves(f); G \\<in> preserves(g) |] \
+\ ==> F Join G \\<in> stable({s \\<in> 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 \\<in> 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. <f(s), g(s)>: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. <f(s), g(s)>:r})";
+Goal "[| F \\<in> stable({s \\<in> state. <f(s), g(s)>:r}); G \\<in> preserves(f); \
+\ F Join G \\<in> Increasing(A, r, g); \
+\ \\<forall>x \\<in> state. f(x):A & g(x):A |] \
+\ ==> F Join G \\<in> Stable({s \\<in> state. <f(s), g(s)>: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 "\\<forall>k\\<in>A. ALL act:Acts(F). ?P(k,act)" 1);
+by (thin_tac "\\<forall>act \\<in> Acts(F). ?P(act)" 1);
+by (thin_tac "\\<forall>k\\<in>A. \\<forall>act \\<in> 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";
+"[| \\<forall>x \\<in> I. F \\<in> A(x) Co B; F \\<in> program |] ==> F:(\\<Union>x \\<in> 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 \\<in> stable({s \\<in> state. P(f(s), g(s))}); \
+\ \\<forall>k \\<in> A. F Join G \\<in> Stable({s \\<in> state. P(k, g(s))}); \
+\ G \\<in> preserves(f); \\<forall>s \\<in> state. f(s):A|] ==> \
+\ F Join G \\<in> Stable({s \\<in> state. P(f(s), g(s))})";
+by (res_inst_tac [("A", "(\\<Union>k \\<in> A. {s \\<in> state. f(s)=k} Int {s \\<in> 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 \\<in> state. f(s)=k} Int {s \\<in> state. P(f(s), g(s))} Int \
+\ {s \\<in> state. P(k, g(s))}"),
+ ("A'", "({s \\<in> state. f(s)=k} Un {s \\<in> state. P(f(s), g(s))}) \
+\ Int {s \\<in> state. P(k, g(s))}")] Constrains_weaken 1);
by (REPEAT(Blast_tac 2));
by (rtac Constrains_Int 1);
by (rtac constrains_imp_Constrains 1);
--- 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 \\<in> Constrains.ML,v 1.10 2003/06/20 10:10:45 paulson Exp $
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
-Safety relations: restricted to the set of reachable states.
+Safety relations \\<in> 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. <s,evs>:traces(Init(F), Acts(F))}";
+"F \\<in> program ==> reachable(F)={s \\<in> state. \\<exists>evs. <s,evs>:traces(Init(F), Acts(F))}";
by (rtac equalityI 1);
by Safe_tac;
by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1);
@@ -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 \\<in> program; G \\<in> program; \
+\ Acts(G) <= Acts(F) |] ==> G \\<in> stable(reachable(F))";
by (blast_tac (claset()
addIs [stableI, constrainsI, st_setI,
reachable_type RS subsetD] @ reachable.intrs) 1);
@@ -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 \\<in> program ==> F \\<in> invariant(reachable(F))";
by (blast_tac (claset() addIs [reachable_type RS subsetD]@reachable.intrs) 1);
qed "invariant_reachable";
(*...in fact the strongest invariant!*)
-Goal "F:invariant(A) ==> reachable(F) <= A";
+Goal "F \\<in> invariant(A) ==> reachable(F) <= A";
by (cut_inst_tac [("F", "F")] Acts_type 1);
by (cut_inst_tac [("F", "F")] Init_type 1);
by (cut_inst_tac [("F", "F")] reachable_type 1);
@@ -78,7 +78,7 @@
(*** Co ***)
-Goal "F:B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')";
+Goal "F \\<in> B co B'==>F:(reachable(F) Int B) co (reachable(F) Int B')";
by (forward_tac [constrains_type RS subsetD] 1);
by (forward_tac [[asm_rl, asm_rl, subset_refl] MRS stable_reachable] 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [stable_def, constrains_Int])));
@@ -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 \\<in> program. F:(reachable(F) Int A) co (reachable(F) Int B)}";
by (blast_tac (claset() addDs [constrains_reachable_Int,
constrains_type RS subsetD]
addIs [constrains_weaken]) 1);
@@ -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 \\<in> A co A' ==> F \\<in> A Co A'";
by (blast_tac (claset() addIs [constrains_weaken_L] addDs [constrainsD2]) 1);
qed "constrains_imp_Constrains";
val prems = Goalw [Constrains_def, constrains_def, st_set_def]
-"[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A |] ==> s':A'); F:program|]==>F:A Co A'";
+"[|(!!act s s'. [| act \\<in> Acts(F); <s,s'>:act; s \\<in> A |] ==> s':A'); F \\<in> program|]==>F \\<in> A Co A'";
by (auto_tac (claset(), simpset() addsimps prems));
by (blast_tac (claset() addDs [reachable_type RS subsetD]) 1);
qed "ConstrainsI";
@@ -109,43 +109,43 @@
by (Blast_tac 1);
qed "Constrains_type";
-Goal "F : 0 Co B <-> F:program";
+Goal "F \\<in> 0 Co B <-> F \\<in> program";
by (auto_tac (claset() addDs [Constrains_type RS subsetD]
addIs [constrains_imp_Constrains], simpset()));
qed "Constrains_empty";
AddIffs [Constrains_empty];
-Goalw [Constrains_def] "F : A Co state <-> F:program";
+Goalw [Constrains_def] "F \\<in> A Co state <-> F \\<in> program";
by (auto_tac (claset() addDs [Constrains_type RS subsetD]
addIs [constrains_imp_Constrains], simpset()));
qed "Constrains_state";
AddIffs [Constrains_state];
Goalw [Constrains_def2]
- "[| F : A Co A'; A'<=B' |] ==> F : A Co B'";
+ "[| F \\<in> A Co A'; A'<=B' |] ==> F \\<in> A Co B'";
by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
qed "Constrains_weaken_R";
Goalw [Constrains_def2]
- "[| F : A Co A'; B<=A |] ==> F : B Co A'";
+ "[| F \\<in> A Co A'; B<=A |] ==> F \\<in> B Co A'";
by (blast_tac (claset() addIs [constrains_weaken_L, st_set_subset]) 1);
qed "Constrains_weaken_L";
Goalw [Constrains_def2]
- "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
+ "[| F \\<in> A Co A'; B<=A; A'<=B' |] ==> F \\<in> B Co B'";
by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1);
qed "Constrains_weaken";
(** Union **)
Goalw [Constrains_def2]
-"[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')";
+"[| F \\<in> A Co A'; F \\<in> B Co B' |] ==> F \\<in> (A Un B) Co (A' Un B')";
by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "Constrains_Un";
val [major, minor] = Goalw [Constrains_def2]
-"[|(!!i. i:I==>F:A(i) Co A'(i)); F:program|] ==> F:(UN i:I. A(i)) Co (UN i:I. A'(i))";
+"[|(!!i. i \\<in> I==>F \\<in> A(i) Co A'(i)); F \\<in> program|] ==> F:(\\<Union>i \\<in> I. A(i)) Co (\\<Union>i \\<in> I. A'(i))";
by (cut_facts_tac [minor] 1);
by (auto_tac (claset() addDs [major]
addIs [constrains_UN],
@@ -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 \\<in> A Co A'; F \\<in> B Co B'|]==> F:(A Int B) Co (A' Int B')";
by (subgoal_tac "reachable(F) Int (A Int B) = \
\ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
by (ALLGOALS(force_tac (claset() addIs [constrains_Int], simpset())));
qed "Constrains_Int";
val [major,minor] = Goal
-"[| (!!i. i:I ==>F: A(i) Co A'(i)); F:program |] \
-\ ==> F:(INT i:I. A(i)) Co (INT i:I. A'(i))";
+"[| (!!i. i \\<in> I ==>F \\<in> A(i) Co A'(i)); F \\<in> program |] \
+\ ==> F:(\\<Inter>i \\<in> I. A(i)) Co (\\<Inter>i \\<in> I. A'(i))";
by (cut_facts_tac [minor] 1);
by (asm_simp_tac (simpset() delsimps INT_simps
addsimps [Constrains_def]@INT_extend_simps) 1);
@@ -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 \\<in> A Co A' ==> reachable(F) Int A <= A'";
by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
qed "Constrains_imp_subset";
Goalw [Constrains_def2]
- "[| F : A Co B; F : B Co C |] ==> F : A Co C";
+ "[| F \\<in> A Co B; F \\<in> B Co C |] ==> F \\<in> A Co C";
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
Goalw [Constrains_def2]
-"[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
+"[| F \\<in> A Co (A' Un B); F \\<in> B Co B' |] ==> F \\<in> A Co (A' Un B')";
by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
by (blast_tac (claset() addIs [constrains_cancel]) 1);
qed "Constrains_cancel";
@@ -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 \\<in> stable(A) ==> F \\<in> Stable(A)";
by (etac constrains_imp_Constrains 1);
qed "stable_imp_Stable";
-Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)";
+Goal "[| F \\<in> Stable(A); A = B |] ==> F \\<in> Stable(B)";
by (Blast_tac 1);
qed "Stable_eq";
Goal
-"F : Stable(A) <-> (F:stable(reachable(F) Int A))";
+"F \\<in> Stable(A) <-> (F \\<in> stable(reachable(F) Int A))";
by (auto_tac (claset() addDs [constrainsD2],
simpset() addsimps [Stable_def, stable_def, Constrains_def2]));
qed "Stable_eq_stable";
-Goalw [Stable_def] "F:A Co A ==> F : Stable(A)";
+Goalw [Stable_def] "F \\<in> A Co A ==> F \\<in> Stable(A)";
by (assume_tac 1);
qed "StableI";
-Goalw [Stable_def] "F : Stable(A) ==> F : A Co A";
+Goalw [Stable_def] "F \\<in> Stable(A) ==> F \\<in> A Co A";
by (assume_tac 1);
qed "StableD";
Goalw [Stable_def]
- "[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')";
+ "[| F \\<in> Stable(A); F \\<in> Stable(A') |] ==> F \\<in> Stable(A Un A')";
by (blast_tac (claset() addIs [Constrains_Un]) 1);
qed "Stable_Un";
Goalw [Stable_def]
- "[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')";
+ "[| F \\<in> Stable(A); F \\<in> Stable(A') |] ==> F \\<in> Stable (A Int A')";
by (blast_tac (claset() addIs [Constrains_Int]) 1);
qed "Stable_Int";
Goalw [Stable_def]
- "[| F : Stable(C); F : A Co (C Un A') |] \
-\ ==> F : (C Un A) Co (C Un A')";
+ "[| F \\<in> Stable(C); F \\<in> A Co (C Un A') |] \
+\ ==> F \\<in> (C Un A) Co (C Un A')";
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
qed "Stable_Constrains_Un";
Goalw [Stable_def]
- "[| F : Stable(C); F : (C Int A) Co A' |] \
-\ ==> F : (C Int A) Co (C Int A')";
+ "[| F \\<in> Stable(C); F \\<in> (C Int A) Co A' |] \
+\ ==> F \\<in> (C Int A) Co (C Int A')";
by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
qed "Stable_Constrains_Int";
val [major,minor] = Goalw [Stable_def]
-"[| (!!i. i:I ==> F : Stable(A(i))); F:program |]==> F : Stable (UN i:I. A(i))";
+"[| (!!i. i \\<in> I ==> F \\<in> Stable(A(i))); F \\<in> program |]==> F \\<in> Stable (\\<Union>i \\<in> I. A(i))";
by (cut_facts_tac [minor] 1);
by (blast_tac (claset() addIs [Constrains_UN,major]) 1);
qed "Stable_UN";
val [major,minor] = Goalw [Stable_def]
-"[|(!!i. i:I ==> F:Stable(A(i))); F:program |]==> F : Stable (INT i:I. A(i))";
+"[|(!!i. i \\<in> I ==> F \\<in> Stable(A(i))); F \\<in> program |]==> F \\<in> Stable (\\<Inter>i \\<in> I. A(i))";
by (cut_facts_tac [minor] 1);
by (blast_tac (claset() addIs [Constrains_INT, major]) 1);
qed "Stable_INT";
-Goal "F:program ==>F : Stable (reachable(F))";
+Goal "F \\<in> program ==>F \\<in> 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 \\<forall>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))";
+"[| \\<forall>m \\<in> M. F \\<in> ({s \\<in> A. x(s) = m}) Co (B(m)); F \\<in> program |] \
+\ ==> F \\<in> ({s \\<in> A. x(s):M}) Co (\\<Union>m \\<in> M. B(m))";
by Auto_tac;
by (res_inst_tac [("A1","reachable(F)Int A")] (elimination RS constrains_weaken_L) 1);
by (auto_tac (claset() addIs [constrains_weaken_L], simpset()));
@@ -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))";
+ "[| \\<forall>m \\<in> M. F \\<in> {s \\<in> state. x(s) = m} Co B(m); F \\<in> program |] \
+\ ==> F \\<in> {s \\<in> state. x(s):M} Co (\\<Union>m \\<in> M. B(m))";
by (blast_tac (claset() addIs [Elimination]) 1);
qed "Elimination2";
@@ -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 \\<in> Stable(A) |] ==> F \\<in> 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 \\<in> Always(A) ==> Init(F)<=A & F \\<in> 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 \\<in> Always(A) ==> reachable(F) <= A";
by (full_simp_tac (simpset() addsimps
[Stable_def, Constrains_def, constrains_def, Always_def, initially_def]) 1);
by (rtac subsetI 1);
@@ -309,13 +309,13 @@
qed "Always_includes_reachable";
Goalw [Always_def, invariant_def, Stable_def, stable_def]
- "F : invariant(A) ==> F : Always(A)";
+ "F \\<in> invariant(A) ==> F \\<in> Always(A)";
by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
qed "invariant_imp_Always";
bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
-Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A)}";
+Goal "Always(A) = {F \\<in> program. F \\<in> invariant(reachable(F) Int A)}";
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
Constrains_def2, stable_def, initially_def]) 1);
by (rtac equalityI 1);
@@ -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 \\<in> 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 \\<in> program ==> F \\<in> Always(state)";
by (auto_tac (claset() addDs [reachable_type RS subsetD], simpset()
addsimps [Always_eq_includes_reachable]));
qed "state_AlwaysI";
-Goal "st_set(A) ==> Always(A) = (UN I: Pow(A). invariant(I))";
+Goal "st_set(A) ==> Always(A) = (\\<Union>I \\<in> Pow(A). invariant(I))";
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
by (rtac equalityI 1);
by (ALLGOALS(Clarify_tac));
@@ -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 \\<in> Always(A); A <= B |] ==> F \\<in> 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 \\<in> Always(I) ==> (F:(I Int A) Co A') <-> (F \\<in> A Co A')";
by (asm_simp_tac
(simpset() addsimps [Always_includes_reachable RS Int_absorb2,
Constrains_def, Int_assoc RS sym]) 1);
qed "Always_Constrains_pre";
-Goal "F:Always(I) ==> (F : A Co (I Int A')) <->(F : A Co A')";
+Goal "F \\<in> Always(I) ==> (F \\<in> A Co (I Int A')) <->(F \\<in> A Co A')";
by (asm_simp_tac
(simpset() addsimps [Always_includes_reachable RS Int_absorb2,
Constrains_eq_constrains, Int_assoc RS sym]) 1);
qed "Always_Constrains_post";
-Goal "[| F : Always(I); F : (I Int A) Co A' |] ==> F : A Co A'";
+Goal "[| F \\<in> Always(I); F \\<in> (I Int A) Co A' |] ==> F \\<in> A Co A'";
by (blast_tac (claset() addIs [Always_Constrains_pre RS iffD1]) 1);
qed "Always_ConstrainsI";
-(* [| F : Always(I); F : A Co A' |] ==> F : A Co (I Int A') *)
+(* [| F \\<in> Always(I); F \\<in> A Co A' |] ==> F \\<in> A Co (I Int A') *)
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
Goal
-"[|F:Always(C); F:A Co A'; C Int B<=A; C Int A'<=B'|]==>F:B Co B'";
+"[|F \\<in> Always(C); F \\<in> A Co A'; C Int B<=A; C Int A'<=B'|]==>F \\<in> B Co B'";
by (rtac Always_ConstrainsI 1);
by (dtac Always_ConstrainsD 2);
by (ALLGOALS(Asm_simp_tac));
@@ -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 \\<in> I is need since \\<Inter>is formally not defined for I=0 *)
+Goal "i \\<in> I==>Always(\\<Inter>i \\<in> I. A(i)) = (\\<Inter>i \\<in> I. Always(A(i)))";
by (rtac equalityI 1);
by (auto_tac (claset(), simpset() addsimps
[Inter_iff, Always_eq_includes_reachable]));
qed "Always_INT_distrib";
-Goal "[| F:Always(A); F:Always(B) |] ==> F:Always(A Int B)";
+Goal "[| F \\<in> Always(A); F \\<in> Always(B) |] ==> F \\<in> Always(A Int B)";
by (asm_simp_tac (simpset() addsimps [Always_Int_distrib]) 1);
qed "Always_Int_I";
(*Allows a kind of "implication introduction"*)
-Goal "[| F:Always(A) |] ==> (F : Always(C-A Un B)) <-> (F : Always(B))";
+Goal "[| F \\<in> Always(A) |] ==> (F \\<in> Always(C-A Un B)) <-> (F \\<in> Always(B))";
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
qed "Always_Diff_Un_eq";
@@ -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 \\<in> Always(?A)")] thin_rl;
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
@@ -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*)
--- 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";
-
--- 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 \<in> Pow(state). \<forall>B. F \<in> stable(A Int B)})"
+
+ FP :: "i=>i"
+ "FP(F) == {s\<in>state. F \<in> stable({s})}"
+
+
+lemma FP_Orig_type: "FP_Orig(F) \<subseteq> 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) \<subseteq> 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 \<in> program ==> F \<in> 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:
+ "[| \<forall>B. F \<in> stable (A Int B); st_set(A) |] ==> A \<subseteq> 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 \<in> program ==> F \<in> stable (FP(F) Int B)"
+apply (subgoal_tac "FP (F) Int B = (\<Union>x\<in>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 \<in> program ==> FP(F) \<subseteq> FP_Orig(F)"
+by (rule stable_FP_Int [THEN FP_Orig_weakest], auto)
+
+lemma FP_Orig_subset_FP: "F \<in> program ==> FP_Orig(F) \<subseteq> 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 \<in> program ==> FP(F) = FP_Orig(F)"
+by (blast intro!: FP_Orig_subset_FP FP_subset_FP_Orig)
+
+lemma FP_weakest [rule_format]:
+ "[| \<forall>B. F \<in> stable(A Int B); F \<in> program; st_set(A) |] ==> A \<subseteq> FP(F)"
+by (simp add: FP_equivalence FP_Orig_weakest)
+
+
+lemma Diff_FP:
+ "[| F \<in> program; st_set(A) |]
+ ==> A-FP(F) = (\<Union>act \<in> Acts(F). A - {s \<in> state. act``{s} \<subseteq> {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
--- 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 \\<in> 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 \\<in> state ==> f(x)=f'(x); !!x. x \\<in> 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. <f(x), g(x)>:r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
+"[| mono1(A, r, B, s, h); \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
+\ Always({x \\<in> state. <f(x), g(x)> \\<in> r})<=Always({x \\<in> state. <(h comp f)(x), (h comp g)(x)> \\<in> s})";
by (auto_tac (claset(), simpset() addsimps
[Always_eq_includes_reachable]));
qed "subset_Always_comp";
Goal
-"[| F:Always({x:state. <f(x), g(x)>: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 \\<in> Always({x \\<in> state. <f(x), g(x)> \\<in> r}); \
+\ mono1(A, r, B, s, h); \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
+\ F \\<in> Always({x \\<in> state. <(h comp f)(x), (h comp g)(x)> \\<in> s})";
by (blast_tac (claset() addIs [subset_Always_comp RS subsetD]) 1);
qed "imp_Always_comp";
Goal
-"[| F:Always({x:state. <f1(x), f(x)>:r}); \
-\ F:Always({x:state. <g1(x), g(x)>:s}); \
+"[| F \\<in> Always({x \\<in> state. <f1(x), f(x)> \\<in> r}); \
+\ F \\<in> Always({x \\<in> state. <g1(x), g(x)> \\<in> 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. <h(f1(x), g1(x)), h(f(x), g(x))>:t})";
+\ \\<forall>x \\<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \
+\ ==> F \\<in> Always({x \\<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \\<in> 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. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}) <= \
-\(INT k:B. {x:state. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
+\ \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
+\ (\\<Inter>j \\<in> A. {s \\<in> state. <j, g(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f(s)> \\<in> r}) <= \
+\(\\<Inter>k \\<in> B. {x \\<in> state. <k, (h comp g)(x)> \\<in> s} LeadsTo {x \\<in> state. <k, (h comp f)(x)> \\<in> 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. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}); \
+"[| F:(\\<Inter>j \\<in> A. {s \\<in> state. <j, g(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f(s)> \\<in> 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. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
+\ \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
+\ F:(\\<Inter>k \\<in> B. {x \\<in> state. <k, (h comp g)(x)> \\<in> s} LeadsTo {x \\<in> state. <k, (h comp f)(x)> \\<in> 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. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
+"[| F \\<in> Increasing(B, s, g); \
+\ \\<forall>j \\<in> A. F: {s \\<in> state. <j, f(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f1(s)> \\<in> 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. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g(x))>:t}";
+\ \\<forall>x \\<in> state. f1(x):A & f(x):A & g(x):B; k \\<in> C |] ==> \
+\ F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f1(x), g(x))> \\<in> 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. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
+"[| F \\<in> Increasing(A, r, f); \
+\ \\<forall>j \\<in> B. F: {x \\<in> state. <j, g(x)> \\<in> s} LeadsTo {x \\<in> state. <j,g1(x)> \\<in> 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. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f(x), g1(x))>:t}";
+\ \\<forall>x \\<in> state. f(x):A & g1(x):B & g(x):B; k \\<in> C |] ==> \
+\ F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f(x), g1(x))> \\<in> t}";
by (rtac single_LeadsTo_I 1);
by Auto_tac;
by (dres_inst_tac [("x", "f(sa)"),("P","%k. F \\<in> 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. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
-\ ALL j:B. F: {x:state. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
+"[| F \\<in> Increasing(A, r, f1) Int Increasing(B, s, g); \
+\ \\<forall>j \\<in> A. F: {s \\<in> state. <j, f(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f1(s)> \\<in> r}; \
+\ \\<forall>j \\<in> B. F: {x \\<in> state. <j, g(x)> \\<in> s} LeadsTo {x \\<in> state. <j,g1(x)> \\<in> 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. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g1(x))>:t}";
-by (res_inst_tac [("B", "{x:state. <k, h(f1(x), g(x))>:t}")] LeadsTo_Trans 1);
+\ \\<forall>x \\<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \\<in> C |]\
+\ ==> F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f1(x), g1(x))> \\<in> t}";
+by (res_inst_tac [("B", "{x \\<in> state. <k, h(f1(x), g(x))> \\<in> 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 \\<in> Follows(A, r, f, g) ==> F \\<in> 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 \\<in> Follows(A, r, f, g)==> \
+\ F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>x \\<in> 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 \\<in> program; c \\<in> A; refl(A, r) |] ==> F \\<in> 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 \\<in> Follows(A, r, f, g); mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
+\ ==> F \\<in> 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 \\<in> this general result is used to prove Follows_Un, Follows_munion *)
-(* 2-place monotone operation: this general result is
+(* 2-place monotone operation \\<in> 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 \\<in> Follows(A, r, f1, f); F \\<in> 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 \\<in> 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 \\<in> Follows(A, r, f, g); F \\<in> Follows(A,r, g, h); \
+\ trans[A](r) |] ==> F \\<in> 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. <k, g(s)>:r}")] LeadsTo_Trans 2);
+by (res_inst_tac [("B", "{s \\<in> state. <k, g(s)> \\<in> 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 \\<in> Follows(A, r, f,g) ==> F \\<in> 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 \\<in> Follows(A, r, f,g) ==> F \\<in> 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. <f(s),g(s)>:r})";
+ "F :Follows(A, r, f, g) ==> F \\<in> Always({s \\<in> state. <f(s),g(s)> \\<in> r})";
by (Blast_tac 1);
qed "Follows_imp_Always";
Goalw [Follows_def]
- "[| F:Follows(A, r, f, g); k:A |] ==> \
-\ F: {s:state. <k,g(s)>:r } LeadsTo {s:state. <k,f(s)>:r}";
+ "[| F \\<in> Follows(A, r, f, g); k \\<in> A |] ==> \
+\ F: {s \\<in> state. <k,g(s)> \\<in> r } LeadsTo {s \\<in> state. <k,f(s)> \\<in> 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 \\<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \\<in> list(nat) |] \
+\ ==> F \\<in> {s \\<in> state. k pfixLe g(s)} LeadsTo {s \\<in> 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 \\<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \\<in> list(nat) |] \
+\ ==> F \\<in> {s \\<in> state. k pfixGe g(s)} LeadsTo {s \\<in> 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 \\<in> Always({s \\<in> state. f(s) = g(s)}); F \\<in> Follows(A, r, f, h); \
+\ \\<forall>x \\<in> state. g(x):A |] ==> F \\<in> 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. <ka, h(s)>:r}"),
- ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
-by (eres_inst_tac [("A", "{s:state. <ka,f(s)>:r}"),
- ("A'", "{s:state. <ka,f(s)>:r}")]
+by (res_inst_tac [("C", "{s \\<in> state. f(s)=g(s)}"),
+ ("A", "{s \\<in> state. <ka, h(s)> \\<in> r}"),
+ ("A'", "{s \\<in> state. <ka, f(s)> \\<in> r}")] Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s \\<in> state. <ka,f(s)> \\<in> r}"),
+ ("A'", "{s \\<in> state. <ka,f(s)> \\<in> 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 \\<in> Always({s \\<in> state. g(s) = h(s)}); \
+\ F \\<in> Follows(A, r, f, g); \\<forall>x \\<in> state. h(x):A |] ==> F \\<in> 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. <ka, g(s)>:r}"),
- ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
-by (eres_inst_tac [("A", "{s:state. <ka, g(s)>:r}"),
- ("A'", "{s:state. <ka, g(s)>:r}")]
+by (thin_tac "k \\<in> A" 3);
+by (res_inst_tac [("C", "{s \\<in> state. g(s)=h(s)}"),
+ ("A", "{s \\<in> state. <ka, g(s)> \\<in> r}"),
+ ("A'", "{s \\<in> state. <ka, f(s)> \\<in> r}")] Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s \\<in> state. <ka, g(s)> \\<in> r}"),
+ ("A'", "{s \\<in> state. <ka, g(s)> \\<in> 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 \\<in> Increasing.increasing(Pow(A), SetLe(A), f); \
+\ F \\<in> Increasing.increasing(Pow(A), SetLe(A), g) |] \
+\ ==> F \\<in> 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 \\<in> Increasing(Pow(A), SetLe(A), f); \
+\ F \\<in> Increasing(Pow(A), SetLe(A), g) |] \
+\ ==> F \\<in> 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 \\<in> Always({s \\<in> state. f1(s) <= f(s)}); \
+\ F \\<in> Always({s \\<in> state. g1(s) <= g(s)}) |] \
+\ ==> F \\<in> Always({s \\<in> 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 \\<in> Follows(Pow(A), SetLe(A), f1, f); \
+\ F \\<in> Follows(Pow(A), SetLe(A), g1, g) |] \
+\ ==> F \\<in> 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 |] ==> <M, M>:MultLe(A, r)";
+ "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \\<in> 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) ==> <M, M>:MultLe(A, r)";
+ "M \\<in> Mult(A) ==> <M, M> \\<in> MultLe(A, r)";
by Auto_tac;
qed "MultLe_refl2";
Addsimps [MultLe_refl2];
@@ -370,7 +370,7 @@
by Auto_tac;
qed "MultLe_type";
-Goal "[| <M, K>:MultLe(A, r); <K, N>:MultLe(A, r) |] ==> <M, N>:MultLe(A,r)";
+Goal "[| <M, K> \\<in> MultLe(A, r); <K, N> \\<in> MultLe(A, r) |] ==> <M, N> \\<in> 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> \\<in> 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> \\<in> 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 \\<in> Mult(A) ==> <0, M> \\<in> 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]
-"[| <M, N>:MultLe(A, r); <K, L>:MultLe(A, r) |] ==>\
-\ <M +# K, N +# L>:MultLe(A, r)";
+"[| <M, N> \\<in> MultLe(A, r); <K, L> \\<in> MultLe(A, r) |] ==>\
+\ <M +# K, N +# L> \\<in> 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 \\<in> Increasing.increasing(Mult(A), MultLe(A,r), f); \
+\ F \\<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |] \
+\ ==> F \\<in> 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 \\<in> Increasing(Mult(A), MultLe(A,r), f); \
+\ F \\<in> Increasing(Mult(A), MultLe(A,r), g)|] \
+\ ==> F \\<in> 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. <f1(s),f(s)>:MultLe(A,r)}); \
-\ F:Always({s:state. <g1(s), g(s)>: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. <f1(s) +# g1(s), f(s) +# g(s)>:MultLe(A,r)})";
+"[| F \\<in> Always({s \\<in> state. <f1(s),f(s)> \\<in> MultLe(A,r)}); \
+\ F \\<in> Always({s \\<in> state. <g1(s), g(s)> \\<in> MultLe(A,r)});\
+\ \\<forall>x \\<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \
+\ ==> F \\<in> Always({s \\<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \\<in> 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 \\<in> Follows(Mult(A), MultLe(A, r), f1, f); \
+\ F \\<in> Follows(Mult(A), MultLe(A, r), g1, g) |] \
+\ ==> F \\<in> 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. [| \\<forall>i \\<in> I. F \\<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \
+\ \\<forall>s. \\<forall>i \\<in> 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 \\<in> program |] \
+\ ==> F \\<in> 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);
--- 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 \\<in> GenPrefix.ML,v 1.8 2003/06/20 16:13:16 paulson Exp $
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
@@ -224,14 +224,14 @@
Addsimps [same_gen_prefix_gen_prefix];
Goal "[| xs \\<in> list(A); ys \\<in> list(A); y \\<in> A |] ==> \
-\ <xs, Cons(y,ys)> : gen_prefix(A,r) <-> \
+\ <xs, Cons(y,ys)> \\<in> gen_prefix(A,r) <-> \
\ (xs=[] | (\\<exists>z zs. xs=Cons(z,zs) & z \\<in> A & <z,y>:r & <zs,ys> \\<in> gen_prefix(A,r)))";
by (induct_tac "xs" 1);
by Auto_tac;
qed "gen_prefix_Cons";
Goal "[| refl(A,r); <xs,ys> \\<in> gen_prefix(A, r); zs \\<in> list(A) |] \
-\ ==> <xs@zs, take(length(xs), ys) @ zs> : gen_prefix(A, r)";
+\ ==> <xs@zs, take(length(xs), ys) @ zs> \\<in> gen_prefix(A, r)";
by (etac gen_prefix.induct 1);
by (Asm_simp_tac 1);
by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD]));
@@ -244,7 +244,7 @@
Goal "[| refl(A, r); <xs,ys> \\<in> gen_prefix(A,r); \
\ length(xs) = length(ys); zs \\<in> list(A) |] \
-\ ==> <xs@zs, ys @ zs> : gen_prefix(A, r)";
+\ ==> <xs@zs, ys @ zs> \\<in> gen_prefix(A, r)";
by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1);
by (REPEAT(assume_tac 1));
by (subgoal_tac "take(length(xs), ys)=ys" 1);
@@ -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 "(<xs,ys> : gen_prefix(A,r)) <-> \
+Goal "(<xs,ys> \\<in> gen_prefix(A,r)) <-> \
\ (xs \\<in> list(A) & ys \\<in> list(A) & length(xs) \\<le> length(ys) & \
\ (\\<forall>i. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
by (rtac iffI 1);
@@ -436,7 +436,7 @@
qed "prefix_length_le";
Goalw [prefix_def]
-"<xs,ys> \\<in> prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
+"<xs,ys> \\<in> prefix(A) ==> xs\\<noteq>ys --> length(xs) < length(ys)";
by (etac gen_prefix.induct 1);
by (Clarify_tac 1);
by (ALLGOALS(subgoal_tac "ys \\<in> list(A)&xs \\<in> list(A)"));
@@ -532,7 +532,7 @@
qed "common_prefix_linear";
-(*** pfixLe, pfixGe: properties inherited from the translations ***)
+(*** pfixLe, pfixGe \\<in> 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 \\<in> prefix and take *)
Goalw [prefix_def]
"<xs, ys> \\<in> prefix(A) ==> xs = take(length(xs), ys)";
--- 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 \\<in> 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 \\<in> I & OK(I, F)) | (i\\<notin>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\\<subseteq>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 \\<in> Fin(program) ==> (ex_prop(X) \
+\ --> GG Int X\\<noteq>0 --> OK(GG, (%G. G)) -->(\\<Squnion>G \\<in> 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\\<subseteq>program ==> \
+\(\\<forall>GG. GG \\<in> Fin(program) & GG Int X \\<noteq> 0 --> OK(GG,(%G. G))-->(\\<Squnion>G \\<in> 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\\<subseteq>program & \
+\ (\\<forall>GG. GG \\<in> Fin(program) & GG Int X \\<noteq> 0& OK(GG,( %G. G))-->(\\<Squnion>G \\<in> 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\\<subseteq>program & (\\<forall>G \\<in> program. (G \\<in> X <-> (\\<forall>H \\<in> program. (G component_of H) --> H \\<in> 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\\<subseteq>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 \\<in> Fin(program) ==> \
+\ (uv_prop(X)--> GG \\<subseteq> X & OK(GG, (%G. G)) --> (\\<Squnion>G \\<in> 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\\<subseteq>program ==> (\\<forall>GG. GG \\<in> Fin(program) & GG \\<subseteq> X & OK(GG,(%G. G)) \
+\ --> (\\<Squnion>G \\<in> 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\\<subseteq>program & \
+\ (\\<forall>GG. GG \\<in> Fin(program) & GG \\<subseteq> X & OK(GG, %G. G) --> (\\<Squnion>G \\<in> 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 \\<in> X; G \\<in> program |] ==> F Join G \\<in> Y); F \\<in> program |] \
+\ ==> F \\<in> 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 \\<in> X guarantees Y; F ok G; F Join G \\<in> X; G \\<in> program |] \
+\ ==> F Join G \\<in> 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\\<subseteq>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 \\<in> X guarantees Y; F Join G = H; H \\<in> X; F ok G; G \\<in> program |] \
+\ ==> H \\<in> Y";
by (Blast_tac 1);
qed "component_guaranteesD";
Goalw [guar_def]
- "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
+ "[| F \\<in> X guarantees X'; Y \\<subseteq> X; X' \\<subseteq> Y' |] ==> F \\<in> Y guarantees Y'";
by Auto_tac;
qed "guarantees_weaken";
-Goalw [guar_def] "X <= Y \
+Goalw [guar_def] "X \\<subseteq> 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 \\<subseteq> Y; F \\<in> program |] \
+\ ==> F \\<in> 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 \\<in> I ==>(\\<Union>i \\<in> I. X(i)) guarantees Y = (\\<Inter>i \\<in> 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 \\<in> I ==> X guarantees (\\<Inter>i \\<in> I. Y(i)) = (\\<Inter>i \\<in> 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 \\<in> Z guarantees X; F \\<in> Z guarantees Y |] \
+\ ==> F \\<in> 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 \\<in> I==> (F \\<in> X guarantees (\\<Inter>i \\<in> I. Y(i))) <-> \
+\ (\\<forall>i \\<in> I. F \\<in> 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 \\<in> V guarantees X; F \\<in> (X Int Y) guarantees Z |]\
+\ ==> F \\<in> (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 \\<in> V guarantees (X Un Y); F \\<in> Y guarantees Z |]\
+\ ==> F \\<in> 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 \\<in> I ==> F \\<in> 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))";
+ "[| \\<forall>i \\<in> I. F \\<in> X guarantees Y(i); i \\<in> I |] \
+\ ==> F \\<in> X guarantees (\\<Inter>i \\<in> I. Y(i))";
by (Blast_tac 1);
qed "all_guarantees";
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F \\<in> X guarantees Y i; i \\<in> I |] *)
Goalw [guar_def]
- "EX i:I. F : X guarantees Y(i) ==> F : X guarantees (UN i:I. Y(i))";
+ "\\<exists>i \\<in> I. F \\<in> X guarantees Y(i) ==> F \\<in> X guarantees (\\<Union>i \\<in> 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 \\<in> U guarantees V; G \\<in> 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 \\<in> U guarantees V; G \\<in> 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))";
+ "[| \\<forall>i \\<in> I. F(i) \\<in> X(i) guarantees Y(i); OK(I,F); i \\<in> I |] \
+\ ==> (\\<Squnion>i \\<in> I. F(i)) \\<in> (\\<Inter>i \\<in> I. X(i)) guarantees (\\<Inter>i \\<in> 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", "(\\<Squnion>x \\<in> (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))";
+ "[| \\<forall>i \\<in> I. F(i) \\<in> X(i) guarantees Y(i); OK(I,F) |] \
+\ ==> JOIN(I,F) \\<in> (\\<Union>i \\<in> I. X(i)) guarantees (\\<Union>i \\<in> 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 \\<in> X guarantees Y; F ok G |] ==> F Join G \\<in> 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 \\<in> X guarantees Y; F ok G |] ==> F Join G \\<in> 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 \\<in> I; F(i): X guarantees Y; OK(I,F) |] \
+\ ==> (\\<Squnion>i \\<in> I. F(i)) \\<in> 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 \\<in> 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 \\<in> 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) \\<subseteq> program";
by Auto_tac;
qed "wg_type";
-Goalw [guar_def] "X guarantees Y <= program";
+Goalw [guar_def] "X guarantees Y \\<subseteq> program";
by Auto_tac;
qed "guarantees_type";
-Goalw [wg_def] "G:wg(F, X) ==> G:program & F:program";
+Goalw [wg_def] "G \\<in> wg(F, X) ==> G \\<in> program & F \\<in> 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 \\<in> X guarantees Y) <-> \
+\ F \\<in> program & (\\<forall>H \\<in> program. H \\<in> X --> (F component_of H --> H \\<in> 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 \\<in> (X guarantees Y); X \\<subseteq> program |] ==> X \\<subseteq> wg(F,Y)";
by Auto_tac;
qed "wg_weakest";
Goalw [wg_def, guar_def]
-"F:program ==> F:wg(F,Y) guarantees Y";
+"F \\<in> program ==> F \\<in> 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 \\<in> wg(F,X)) <-> ((F component_of H --> H \\<in> X) & F \\<in> program & H \\<in> 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 \\<in> wg(F,X) <-> (H \\<in> X & F \\<in> program & H \\<in> 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))";
+"\\<forall>FF \\<in> Fin(program). FF Int X \\<noteq> 0 --> OK(FF, %F. F) \
+\ --> (\\<forall>F \\<in> FF. ((\\<Squnion>F \\<in> FF. F): wg(F,X)) <-> ((\\<Squnion>F \\<in> FF. F):X))";
by (Clarify_tac 1);
-by (subgoal_tac "F component_of (JN F:FF. F)" 1);
+by (subgoal_tac "F component_of (\\<Squnion>F \\<in> 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", "\\<Squnion>F \\<in> (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 \\<in> Fin(program); FF Int X \\<noteq>0; OK(FF, %F. F); G \\<in> 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 \\<in> X) <-> (\\<forall>H \\<in> program. H \\<in> wg(F,X) & F \\<in> 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)\\<subseteq>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] "\\<forall>Z. Z\\<subseteq>program --> Z\\<subseteq> X --> ex_prop(Z) --> Z \\<subseteq> 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 \\<in> program. \\<forall>G \\<in> program. F ok G --> F Join G \\<in> 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 \\<in> program. \\<forall>G \\<in> 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 \\<in> program. \\<forall>G \\<in> program. F ok G --> F Join G \\<in> 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) \\<subseteq> A; F \\<in> program |] ==> F \\<in> 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 \\<in> A co A Un B; F \\<in> transient(A); st_set(B) |] ==> F \\<in> 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 \\<in> 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);
--- 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 \\<in> 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 \\<in> increasing[A](r, f) ==> F \\<in> program";
by (Blast_tac 1);
qed "increasing_into_program";
Goalw [increasing_def]
-"[| F:increasing[A](r, f); x:A |] ==>F:stable({s:state. <x, f(s)>:r})";
+"[| F \\<in> increasing[A](r, f); x \\<in> A |] ==>F \\<in> stable({s \\<in> state. <x, f(s)>: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 \\<in> increasing[A](r,f) ==> F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>s \\<in> state. f(s):A)";
+by (subgoal_tac "\\<exists>x. x \\<in> 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 \\<in> increasing[A](r, %s. c) <-> F \\<in> program & c \\<in> A";
+by (subgoal_tac "\\<exists>x. x \\<in> 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 \\<in> state" 1);
by (blast_tac (claset() addSDs [ActsD]) 2);
by (subgoal_tac "<f(xb), f(xb)>: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 \\<in> increasing[A](r, f); mono1(A, r, B, s, g); \
+\ refl(A, r); trans[B](s) |] ==> F \\<in> 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 \\<in> increasing[A](r, f) ==> F \\<in> 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 \\<in> Increasing[A](r, f) ==> F \\<in> program";
by Auto_tac;
qed "Increasing_into_program";
Goalw [Increasing_def]
-"[| F:Increasing[A](r, f); a:A |] ==> F: Stable({s:state. <a,f(s)>:r})";
+"[| F \\<in> Increasing[A](r, f); a \\<in> A |] ==> F \\<in> Stable({s \\<in> state. <a,f(s)>: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 \\<in> Increasing[A](r, f) ==> F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>s \\<in> state. f(s):A)";
+by (subgoal_tac "\\<exists>x. x \\<in> 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 \\<in> Increasing[A](r, %s. c) <-> F \\<in> program & (c \\<in> A)";
+by (subgoal_tac "\\<exists>x. x \\<in> 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 \\<in> state & xa \\<in> state" 1);
by (asm_simp_tac (simpset() addsimps [ActsD]) 2);
by (subgoal_tac "<f(xb), f(xb)>: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 \\<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] \
+\ ==> F \\<in> 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 \\<in> increasing[A](r, f); F \\<in> 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 \\<in> 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 \\<in> state & xa \\<in> state" 1);
by (blast_tac (claset() addSDs [ActsD]) 2);
by (subgoal_tac "<f(xb), f(xb)>:r & <g(xb), g(xb)>: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 \\<in> Increasing[A](r, f); F \\<in> 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 \\<in> 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 \\<in> state & x \\<in> state" 1);
by (blast_tac (claset() addSDs [ActsD]) 2);
by (subgoal_tac "<f(xa), f(xa)>:r & <g(xa), g(xa)>:s" 1);
by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
--- 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 \\<in> 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); <x, y>:r; x:A; y:A |] ==> <f(x), f(y)>:s";
+ "[| mono1(A, r, B, s, f); <x, y>:r; x \\<in> A; y \\<in> A |] ==> <f(x), f(y)>:s";
by Auto_tac;
qed "mono1D";
Goalw [mono2_def]
-"[| mono2(A, r, B, s, C, t, f); <x, y>:r; <u,v>:s; x:A; y:A; u:B; v:B |] ==> \
+"[| mono2(A, r, B, s, C, t, f); <x, y>:r; <u,v>:s; x \\<in> A; y \\<in> A; u \\<in> B; v \\<in> B |] ==> \
\ <f(x, u), f(y,v)>: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 |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
+Goal "[| i le j; xs \\<in> list(A); i \\<in> nat; j \\<in> nat |] ==> <take(i, xs), take(j, xs)>: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 "[| <xs, ys>:prefix(A); i:nat |] ==> <take(i, xs), take(i, ys)>:prefix(A)";
+Goal "[| <xs, ys>:prefix(A); i \\<in> nat |] ==> <take(i, xs), take(i, ys)>:prefix(A)";
by (auto_tac (claset(), simpset() addsimps [prefix_iff]));
qed "take_mono_right";
-Goal "[| i le j; <xs, ys>:prefix(A); i:nat; j:nat |] ==> <take(i, xs), take(j, ys)>:prefix(A)";
+Goal "[| i le j; <xs, ys>:prefix(A); i \\<in> nat; j \\<in> nat |] ==> <take(i, xs), take(j, ys)>: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()));
--- 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 \\<in> 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 \\<in> Fin(A); a \\<in> A; a\\<notin>C; e \\<in> B; \\<forall>x \\<in> 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 \\<in> Fin(A); \\<forall>x \\<in> A. multiset(g(x))& mset_of(g(x))<=B |] \
\ ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\<lambda>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 \\<in> Fin(A); a\\<notin>C; a \\<in> A; \\<forall>x \\<in> 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 \\<in> Fin(A); \\<forall>x \\<in> 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 \\<in> Fin(A); D \\<in> Fin(A); \\<forall>x \\<in> 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 \\<in> Fin(A) & y Int D \\<in> Fin(A)" 1);
by (Clarify_tac 1);
-by (case_tac "x:D" 1);
+by (case_tac "x \\<in> 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 \\<in> Fin(A); D \\<in> Fin(A); C Int D = 0; \
+\ \\<forall>x \\<in> 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 \\<in> Fin(A) ==> (\\<forall>i \\<in> I. C(i):Fin(B)) --> (\\<Union>i \\<in> 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 \\<in> Fin(K); \\<forall>i \\<in> K. C(i):Fin(A) |] ==> \
+\ (\\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B) --> \
+\ (\\<forall>i \\<in> I. \\<forall>j \\<in> I. i\\<noteq>j --> C(i) Int C(j) = 0) --> \
+\ msetsum(f, \\<Union>i \\<in> 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 "\\<forall>i \\<in> y. x \\<noteq> 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 (\\<Union>i \\<in> 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 " (\\<Union>i \\<in> 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 "\\<forall>x \\<in> 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 \\<in> Fin(A); \
+\ \\<forall>x \\<in> A. multiset(f(x)) & mset_of(f(x))<=B; \
+\ \\<forall>x \\<in> 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 "\\<forall>x \\<in> 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 \\<in> 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 \\<in> Fin(A); D \\<in> Fin(A); \
+\ \\<forall>x \\<in> 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 \\<in> Fin(A) & C Int D \\<in> 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\\<notin>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);
--- 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 \\<in> Mutex.ML,v 1.4 2003/05/27 09:39:05 paulson Exp $
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
Variables' types are introduced globally so that type verification
-reduces to the usual ZF typechecking: an ill-tyed expression will
+reduces to the usual ZF typechecking \\<in> 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 \\<in> state ==>s`u \\<in> bool";
by (dres_inst_tac [("a", "u")] apply_type 1);
by Auto_tac;
qed "u_value_type";
-Goalw [state_def] "s:state ==> s`v:bool";
+Goalw [state_def] "s \\<in> state ==> s`v \\<in> bool";
by (dres_inst_tac [("a", "v")] apply_type 1);
by Auto_tac;
qed "v_value_type";
-Goalw [state_def] "s:state ==> s`p:bool";
+Goalw [state_def] "s \\<in> state ==> s`p \\<in> bool";
by (dres_inst_tac [("a", "p")] apply_type 1);
by Auto_tac;
qed "p_value_type";
-Goalw [state_def] "s:state ==> s`m:int";
+Goalw [state_def] "s \\<in> state ==> s`m \\<in> int";
by (dres_inst_tac [("a", "m")] apply_type 1);
by Auto_tac;
qed "m_value_type";
-Goalw [state_def] "s:state ==>s`n:int";
+Goalw [state_def] "s \\<in> state ==>s`n \\<in> int";
by (dres_inst_tac [("a", "n")] apply_type 1);
by Auto_tac;
qed "n_value_type";
@@ -46,7 +46,7 @@
m_value_type, n_value_type];
(** Mutex is a program **)
-Goalw [Mutex_def] "Mutex:program";
+Goalw [Mutex_def] "Mutex \\<in> 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 \\<in> Always(IU)";
by (always_tac 1);
by Auto_tac;
qed "IU";
-Goal "Mutex : Always(IV)";
+Goal "Mutex \\<in> 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 \\<in> mutual exclusion*)
+Goal "Mutex \\<in> Always({s \\<in> state. ~(s`m = #3 & s`n = #3)})";
by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
by Auto_tac;
qed "mutual_exclusion";
@@ -87,7 +87,7 @@
by Auto_tac;
qed "less_lemma";
-Goal "Mutex : Always(bad_IU)";
+Goal "Mutex \\<in> Always(bad_IU)";
by (always_tac 1);
by (auto_tac (claset(), simpset() addsimps [not_zle_iff_zless]));
by (auto_tac (claset(), simpset() addsimps [bool_def]));
@@ -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 \\<in> n=1, p=false, m=4, u=false.
Execution of V1 (the command of process v guarded by n=1) sets p:=true,
violating the invariant!*)
-(*Check that subgoals remain: proof failed.*)
+(*Check that subgoals remain \\<in> proof failed.*)
getgoal 1;
(*** Progress for U ***)
Goalw [Unless_def]
-"Mutex : {s:state. s`m=#2} Unless {s:state. s`m=#3}";
+"Mutex \\<in> {s \\<in> state. s`m=#2} Unless {s \\<in> 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 \\<in> {s \\<in> state. s`m=#1} LeadsTo {s \\<in> state. s`p = s`v & s`m = #2}";
by (ensures_tac "U1" 1);
qed "U_F1";
-Goal "Mutex : {s:state. s`p =0 & s`m = #2} LeadsTo {s:state. s`m = #3}";
+Goal "Mutex \\<in> {s \\<in> state. s`p =0 & s`m = #2} LeadsTo {s \\<in> state. s`m = #3}";
by (cut_facts_tac [IU] 1);
by (ensures_tac "U2" 1);
qed "U_F2";
-Goal "Mutex : {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 \\<in> {s \\<in> state. s`m = #3} LeadsTo {s \\<in> state. s`p=1}";
+by (res_inst_tac [("B", "{s \\<in> state. s`m = #4}")] LeadsTo_Trans 1);
by (ensures_tac "U4" 2);
by (ensures_tac "U3" 1);
qed "U_F3";
-Goal "Mutex : {s:state. s`m = #2} LeadsTo {s:state. s`p=1}";
+Goal "Mutex \\<in> {s \\<in> state. s`m = #2} LeadsTo {s \\<in> state. s`p=1}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
@@ -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 \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`p =1}";
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
by Auto_tac;
val U_lemma1 = result();
-Goal "i:int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)";
+Goal "i \\<in> int ==> (#1 $<= i & i $<= #3) <-> (i=#1 | i=#2 | i=#3)";
by Auto_tac;
by (auto_tac (claset(), simpset() addsimps [neq_iff_zless]));
by (dres_inst_tac [("j", "#3"), ("i", "i")] zle_zless_trans 4);
@@ -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 \\<in> {s \\<in> state. #1 $<= s`m & s`m $<= #3} LeadsTo {s \\<in> state. s`p=1}";
by (simp_tac (simpset() addsimps [m_value_type RS eq_123, Collect_disj_eq,
LeadsTo_Un_distrib,
U_lemma1, U_lemma2, U_F3] ) 1);
@@ -160,7 +160,7 @@
(*Misra's F4*)
-Goal "Mutex : {s:state. s`u = 1} LeadsTo {s:state. s`p=1}";
+Goal "Mutex \\<in> {s \\<in> state. s`u = 1} LeadsTo {s \\<in> state. s`p=1}";
by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
by Auto_tac;
qed "u_Leadsto_p";
@@ -169,26 +169,26 @@
(*** Progress for V ***)
Goalw [Unless_def]
-"Mutex : {s:state. s`n=#2} Unless {s:state. s`n=#3}";
+"Mutex \\<in> {s \\<in> state. s`n=#2} Unless {s \\<in> 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 \\<in> {s \\<in> state. s`n=#1} LeadsTo {s \\<in> state. s`p = not(s`u) & s`n = #2}";
by (ensures_tac "V1" 1);
qed "V_F1";
-Goal "Mutex : {s:state. s`p=1 & s`n = #2} LeadsTo {s:state. s`n = #3}";
+Goal "Mutex \\<in> {s \\<in> state. s`p=1 & s`n = #2} LeadsTo {s \\<in> state. s`n = #3}";
by (cut_facts_tac [IV] 1);
by (ensures_tac "V2" 1);
qed "V_F2";
-Goal "Mutex : {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 \\<in> {s \\<in> state. s`n = #3} LeadsTo {s \\<in> state. s`p=0}";
+by (res_inst_tac [("B", "{s \\<in> state. s`n = #4}")] LeadsTo_Trans 1);
by (ensures_tac "V4" 2);
by (ensures_tac "V3" 1);
qed "V_F3";
-Goal "Mutex : {s:state. s`n = #2} LeadsTo {s:state. s`p=0}";
+Goal "Mutex \\<in> {s \\<in> state. s`n = #2} LeadsTo {s \\<in> state. s`p=0}";
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
@@ -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 \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`p = 0}";
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
by Auto_tac;
val V_lemma1 = result();
-Goal "Mutex : {s:state. #1 $<= s`n & s`n $<= #3} LeadsTo {s:state. s`p = 0}";
+Goal "Mutex \\<in> {s \\<in> state. #1 $<= s`n & s`n $<= #3} LeadsTo {s \\<in> state. s`p = 0}";
by (simp_tac (simpset() addsimps
[n_value_type RS eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
V_lemma1, V_lemma2, V_F3] ) 1);
val V_lemma123 = result();
(*Misra's F4*)
-Goal "Mutex : {s:state. s`v = 1} LeadsTo {s:state. s`p = 0}";
+Goal "Mutex \\<in> {s \\<in> state. s`v = 1} LeadsTo {s \\<in> state. s`p = 0}";
by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
by Auto_tac;
qed "v_Leadsto_not_p";
@@ -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 \\<in> {s \\<in> state. s`m = #1} LeadsTo {s \\<in> state. s`m = #3}";
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
by (rtac U_F2 2);
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
@@ -230,7 +230,7 @@
(*The same for V*)
-Goal "Mutex : {s:state. s`n = #1} LeadsTo {s:state. s`n = #3}";
+Goal "Mutex \\<in> {s \\<in> state. s`n = #1} LeadsTo {s \\<in> state. s`n = #3}";
by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
by (rtac V_F2 2);
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
--- 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 \\<in> SubstAx.ML,v 1.8 2003/05/27 09:39:06 paulson Exp $
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
@@ -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 \\<in> program. F:(reachable(F) Int A) leadsTo B}";
by (blast_tac (claset() addDs [psp_stable2, leadsToD2, constrainsD2]
addIs [leadsTo_weaken]) 1);
qed "LeadsTo_eq";
@@ -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 \\<in> Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \\<in> A LeadsTo A')";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
Int_absorb2, Int_assoc RS sym, leadsToD2]) 1);
qed "Always_LeadsTo_pre";
-Goalw [LeadsTo_def] "F:Always(I) ==> (F : A LeadsTo (I Int A')) <-> (F : A LeadsTo A')";
+Goalw [LeadsTo_def] "F \\<in> Always(I) ==> (F \\<in> A LeadsTo (I Int A')) <-> (F \\<in> A LeadsTo A')";
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable,
Int_absorb2, Int_assoc RS sym,leadsToD2]) 1);
qed "Always_LeadsTo_post";
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
-Goal "[| F:Always(C); F : (C Int A) LeadsTo A' |] ==> F: A LeadsTo A'";
+Goal "[| F \\<in> Always(C); F \\<in> (C Int A) LeadsTo A' |] ==> F \\<in> A LeadsTo A'";
by (blast_tac (claset() addIs [Always_LeadsTo_pre RS iffD1]) 1);
qed "Always_LeadsToI";
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
-Goal "[| F:Always(C); F:A LeadsTo A' |] ==> F : A LeadsTo (C Int A')";
+Goal "[| F \\<in> Always(C); F \\<in> A LeadsTo A' |] ==> F \\<in> A LeadsTo (C Int A')";
by (blast_tac (claset() addIs [Always_LeadsTo_post RS iffD2]) 1);
qed "Always_LeadsToD";
-(*** Introduction rules: Basis, Trans, Union ***)
+(*** Introduction rules \\<in> Basis, Trans, Union ***)
-Goal "F : A Ensures B ==> F : A LeadsTo B";
+Goal "F \\<in> A Ensures B ==> F \\<in> A LeadsTo B";
by (auto_tac (claset(), simpset() addsimps
[Ensures_def, LeadsTo_def]));
qed "LeadsTo_Basis";
-Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C";
+Goal "[| F \\<in> A LeadsTo B; F \\<in> B LeadsTo C |] ==> F \\<in> A LeadsTo C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "LeadsTo_Trans";
val [major, program] = Goalw [LeadsTo_def]
-"[|(!!A. A:S ==> F : A LeadsTo B); F:program|]==>F:Union(S) LeadsTo B";
+"[|(!!A. A \\<in> S ==> F \\<in> A LeadsTo B); F \\<in> program|]==>F \\<in> Union(S) LeadsTo B";
by (cut_facts_tac [program] 1);
by Auto_tac;
by (stac Int_Union_Union2 1);
@@ -69,7 +69,7 @@
(*** Derived rules ***)
-Goal "F : A leadsTo B ==> F : A LeadsTo B";
+Goal "F \\<in> A leadsTo B ==> F \\<in> A LeadsTo B";
by (ftac leadsToD2 1);
by (Clarify_tac 1);
by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1);
@@ -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 \\<in> A LeadsTo (A' Un A') ==> F \\<in> A LeadsTo A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate";
-Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)";
+Goal "F \\<in> A LeadsTo (A' Un C Un C) ==> F \\<in> A LeadsTo (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate2";
val [major, program] = Goalw [LeadsTo_def]
-"[|(!!i. i:I ==> F : A(i) LeadsTo B); F:program|]==>F:(UN i:I. A(i)) LeadsTo B";
+"[|(!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo B); F \\<in> program|]==>F:(\\<Union>i \\<in> I. A(i)) LeadsTo B";
by (cut_facts_tac [program] 1);
by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_UN_distrib]) 1);
by (rtac leadsTo_UN 1);
@@ -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 \\<in> A LeadsTo C; F \\<in> B LeadsTo C |] ==> F \\<in> (A Un B) LeadsTo C";
by (stac Un_eq_Union 1);
by (rtac LeadsTo_Union 1);
by (auto_tac (claset() addDs [LeadsTo_type RS subsetD], simpset()));
@@ -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 \\<in> A ==> F:{s} LeadsTo B); F \\<in> program|]==>F \\<in> A LeadsTo B";
by (cut_facts_tac [program] 1);
by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
by (ftac major 1);
by Auto_tac;
qed "single_LeadsTo_I";
-Goal "[| A <= B; F:program |] ==> F : A LeadsTo B";
+Goal "[| A <= B; F \\<in> program |] ==> F \\<in> A LeadsTo B";
by (asm_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
-Goal "F:0 LeadsTo A <-> F:program";
+Goal "F:0 LeadsTo A <-> F \\<in> program";
by (auto_tac (claset() addDs [LeadsTo_type RS subsetD]
addIs [empty_subsetI RS subset_imp_LeadsTo], simpset()));
qed "empty_LeadsTo";
AddIffs [empty_LeadsTo];
-Goal "F : A LeadsTo state <-> F:program";
+Goal "F \\<in> A LeadsTo state <-> F \\<in> program";
by (auto_tac (claset() addDs [LeadsTo_type RS subsetD],
simpset() addsimps [LeadsTo_eq]));
qed "LeadsTo_state";
AddIffs [LeadsTo_state];
Goalw [LeadsTo_def]
- "[| F:A LeadsTo A'; A'<=B'|] ==> F : A LeadsTo B'";
+ "[| F \\<in> A LeadsTo A'; A'<=B'|] ==> F \\<in> A LeadsTo B'";
by (auto_tac (claset() addIs[leadsTo_weaken_R], simpset()));
qed_spec_mp "LeadsTo_weaken_R";
-Goalw [LeadsTo_def] "[| F : A LeadsTo A'; B <= A |] ==> F : B LeadsTo A'";
+Goalw [LeadsTo_def] "[| F \\<in> A LeadsTo A'; B <= A |] ==> F \\<in> B LeadsTo A'";
by (auto_tac (claset() addIs[leadsTo_weaken_L], simpset()));
qed_spec_mp "LeadsTo_weaken_L";
-Goal "[| F : A LeadsTo A'; B<=A; A'<=B' |] ==> F : B LeadsTo B'";
+Goal "[| F \\<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \\<in> B LeadsTo B'";
by (blast_tac (claset() addIs [LeadsTo_weaken_R,
LeadsTo_weaken_L, LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
Goal
-"[| F:Always(C); F:A LeadsTo A'; C Int B <= A; C Int A' <= B' |] \
-\ ==> F : B LeadsTo B'";
+"[| F \\<in> Always(C); F \\<in> A LeadsTo A'; C Int B <= A; C Int A' <= B' |] \
+\ ==> F \\<in> B LeadsTo B'";
by (blast_tac (claset() addDs [Always_LeadsToI]
addIs [LeadsTo_weaken, Always_LeadsToD]) 1);
qed "Always_LeadsTo_weaken";
(** Two theorems for "proof lattices" **)
-Goal "F : A LeadsTo B ==> F:(A Un B) LeadsTo B";
+Goal "F \\<in> A LeadsTo B ==> F:(A Un B) LeadsTo B";
by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]
addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
qed "LeadsTo_Un_post";
-Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \
-\ ==> F : (A Un B) LeadsTo C";
+Goal "[| F \\<in> A LeadsTo B; F \\<in> B LeadsTo C |] \
+\ ==> F \\<in> (A Un B) LeadsTo C";
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
LeadsTo_weaken_L, LeadsTo_Trans]
addDs [LeadsTo_type RS subsetD]) 1);
qed "LeadsTo_Trans_Un";
(** Distributive laws **)
-Goal "(F : (A Un B) LeadsTo C) <-> (F : A LeadsTo C & F : B LeadsTo C)";
+Goal "(F \\<in> (A Un B) LeadsTo C) <-> (F \\<in> A LeadsTo C & F \\<in> B LeadsTo C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "(F : (UN i:I. A(i)) LeadsTo B) <-> (ALL i : I. F : A(i) LeadsTo B) & F:program";
+Goal "(F \\<in> (\\<Union>i \\<in> I. A(i)) LeadsTo B) <-> (\\<forall>i \\<in> I. F \\<in> A(i) LeadsTo B) & F \\<in> program";
by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]
addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "(F:Union(S) LeadsTo B) <-> (ALL A : S. F : A LeadsTo B) & F:program";
+Goal "(F \\<in> Union(S) LeadsTo B) <-> (\\<forall>A \\<in> S. F \\<in> A LeadsTo B) & F \\<in> program";
by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]
addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
(** More rules using the premise "Always(I)" **)
-Goal "[| F:(A-B) Co (A Un B); F:transient (A-B) |] ==> F : A Ensures B";
+Goal "[| F:(A-B) Co (A Un B); F \\<in> transient (A-B) |] ==> F \\<in> A Ensures B";
by (asm_full_simp_tac
(simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
@@ -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 \\<in> Always(I); F \\<in> (I Int (A-A')) Co (A Un A'); \
+\ F \\<in> transient (I Int (A-A')) |] \
+\ ==> F \\<in> A LeadsTo A'";
by (rtac Always_LeadsToI 1);
by (assume_tac 1);
by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
@@ -197,15 +197,15 @@
transient_strengthen]) 1);
qed "Always_LeadsTo_Basis";
-(*Set difference: maybe combine with leadsTo_weaken_L??
+(*Set difference \\<in> 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 \\<in> (A-B) LeadsTo C; F \\<in> (A Int B) LeadsTo C |] ==> F \\<in> A LeadsTo C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
val [major, minor] = Goal
-"[|(!!i. i:I ==> F: A(i) LeadsTo A'(i)); F:program |] \
-\ ==> F : (UN i:I. A(i)) LeadsTo (UN i:I. A'(i))";
+"[|(!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo A'(i)); F \\<in> program |] \
+\ ==> F \\<in> (\\<Union>i \\<in> I. A(i)) LeadsTo (\\<Union>i \\<in> I. A'(i))";
by (cut_facts_tac [minor] 1);
by (rtac LeadsTo_Union 1);
by (ALLGOALS(Clarify_tac));
@@ -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 \\<in> A LeadsTo A'; F \\<in> B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_R]) 1);
qed "LeadsTo_Un_Un";
(** The cancellation law **)
-Goal "[| F: A LeadsTo(A' Un B); F: B LeadsTo B' |] ==> F:A LeadsTo (A' Un B')";
+Goal "[| F \\<in> A LeadsTo(A' Un B); F \\<in> B LeadsTo B' |] ==> F \\<in> A LeadsTo (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un, subset_imp_LeadsTo, LeadsTo_Trans]
addDs [LeadsTo_type RS subsetD]) 1);
qed "LeadsTo_cancel2";
@@ -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 \\<in> A LeadsTo (A' Un B); F \\<in> (B-A') LeadsTo B' |] ==> F \\<in> A LeadsTo (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (asm_simp_tac (simpset() addsimps [Un_Diff]) 1);
qed "LeadsTo_cancel_Diff2";
-Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] ==> F : A LeadsTo (B' Un A')";
+Goal "[| F \\<in> A LeadsTo (B Un A'); F \\<in> B LeadsTo B' |] ==> F \\<in> A LeadsTo (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
qed "LeadsTo_cancel1";
@@ -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 \\<in> A LeadsTo (B Un A'); F \\<in> (B-A') LeadsTo B' |] ==> F \\<in> A LeadsTo (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
by (asm_simp_tac (simpset() addsimps [Diff_Un2]) 1);
@@ -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 \\<in> A LeadsTo 0 ==> F \\<in> Always (state -A)";
by (full_simp_tac (simpset()
addsimps [LeadsTo_def,Always_eq_includes_reachable]) 1);
by (cut_facts_tac [reachable_type] 1);
by (auto_tac (claset() addSDs [leadsTo_empty], simpset()));
qed "LeadsTo_empty";
-(** PSP: Progress-Safety-Progress **)
+(** PSP \\<in> 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 \\<in> Misra's "stable conjunction"*)
+Goal "[| F \\<in> A LeadsTo A'; F \\<in> Stable(B) |]==> F:(A Int B) LeadsTo (A' Int B)";
by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
by (Clarify_tac 1);
by (dtac psp_stable 1);
by (REPEAT(asm_full_simp_tac (simpset() addsimps (Int_absorb::Int_ac)) 1));
qed "PSP_Stable";
-Goal "[| F : A LeadsTo A'; F : Stable(B) |] ==> F : (B Int A) LeadsTo (B Int A')";
+Goal "[| F \\<in> A LeadsTo A'; F \\<in> Stable(B) |] ==> F \\<in> (B Int A) LeadsTo (B Int A')";
by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1);
qed "PSP_Stable2";
-Goal "[| F:A LeadsTo A'; F:B Co B'|]==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))";
+Goal "[| F \\<in> A LeadsTo A'; F \\<in> B Co B'|]==> F \\<in> (A Int B') LeadsTo ((A' Int B) Un (B' - B))";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| F : A LeadsTo A'; F : B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))";
+Goal "[| F \\<in> A LeadsTo A'; F \\<in> B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
qed "PSP2";
Goal
-"[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')";
+"[| F \\<in> A LeadsTo A'; F \\<in> B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')";
by (rewtac Unless_def);
by (dtac PSP 1);
by (assume_tac 1);
@@ -295,10 +295,10 @@
(** Meta or object quantifier ????? **)
Goal "[| wf(r); \
-\ ALL m:I. F : (A Int f-``{m}) LeadsTo \
+\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) LeadsTo \
\ ((A Int f-``(converse(r) `` {m})) Un B); \
-\ field(r)<=I; A<=f-``I; F:program |] \
-\ ==> F : A LeadsTo B";
+\ field(r)<=I; A<=f-``I; F \\<in> program |] \
+\ ==> F \\<in> A LeadsTo B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by Auto_tac;
by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1);
@@ -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 "[| \\<forall>m \\<in> nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B); \
+\ A<=f-``nat; F \\<in> program |] ==> F \\<in> A LeadsTo B";
by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
(wf_measure RS LeadsTo_wf_induct) 1);
by (ALLGOALS(asm_full_simp_tac
@@ -333,11 +333,11 @@
*****)
-(*** Completion: Binary and General Finite versions ***)
+(*** Completion \\<in> 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 \\<in> A LeadsTo (A' Un C); F \\<in> A' Co (A' Un C); \
+\ F \\<in> B LeadsTo (B' Un C); F \\<in> B' Co (B' Un C) |] \
+\ ==> F \\<in> (A Int B) LeadsTo ((A' Int B') Un C)";
by (full_simp_tac
(simpset() addsimps [LeadsTo_def, Constrains_eq_constrains,
Int_Un_distrib]) 1);
@@ -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 \\<in> Fin(X);F \\<in> program |] \
+\ ==> (\\<forall>i \\<in> I. F \\<in> (A(i)) LeadsTo (A'(i) Un C)) --> \
+\ (\\<forall>i \\<in> I. F \\<in> (A'(i)) Co (A'(i) Un C)) --> \
+\ F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
by (etac Fin_induct 1);
by (auto_tac (claset(), simpset() delsimps INT_simps
addsimps [Inter_0]));
@@ -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 \\<in> Fin(X); !!i. i \\<in> I ==> F \\<in> A(i) LeadsTo (A'(i) Un C); \
+\ !!i. i \\<in> I ==> F \\<in> A'(i) Co (A'(i) Un C); \
+\ F \\<in> program |] \
+\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
qed "Finite_completion";
Goalw [Stable_def]
- "[| F : A LeadsTo A'; F : Stable(A'); \
-\ F : B LeadsTo B'; F : Stable(B') |] \
-\ ==> F : (A Int B) LeadsTo (A' Int B')";
+ "[| F \\<in> A LeadsTo A'; F \\<in> Stable(A'); \
+\ F \\<in> B LeadsTo B'; F \\<in> Stable(B') |] \
+\ ==> F \\<in> (A Int B) LeadsTo (A' Int B')";
by (res_inst_tac [("C1", "0")] (Completion RS LeadsTo_weaken_R) 1);
by (Asm_full_simp_tac 5);
by (rtac subset_refl 5);
@@ -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 \\<in> Fin(X); \
+\ (!!i. i \\<in> I ==> F \\<in> A(i) LeadsTo A'(i)); \
+\ (!!i. i \\<in> I ==>F \\<in> Stable(A'(i))); F \\<in> program |] \
+\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) LeadsTo (\\<Inter>i \\<in> I. A'(i))";
by (res_inst_tac [("C1", "0")] (Finite_completion RS LeadsTo_weaken_R) 1);
by (ALLGOALS(Simp_tac));
by (rtac subset_refl 5);
@@ -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 \\<in> co & transient*)
simp_tac (simpset() addsimps !program_defs_ref) 2,
res_inst_tac [("act", sact)] transientI 2,
(*simplify the command's domain*)
--- 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";
-
-
--- 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) \<noteq> 0 *)
+ ok :: "[i, i] => o" (infixl "ok" 65)
+ "F ok G == Acts(F) \<subseteq> AllowedActs(G) &
+ Acts(G) \<subseteq> 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 (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *)
+ OK :: "[i, i=>i] => o"
+ "OK(I,F) == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts(F(i)) \<subseteq> 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(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)),
+ \<Inter>i \<in> 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\<subseteq>program &
+ SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> 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 ("\\<bottom>")
- "op Join" :: [i, i] => i (infixl "\\<squnion>" 65)
- "@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10)
- "@JOIN" :: [pttrn, i, i] => i ("(3\\<Squnion> _:_./ _)" 10)
+ SKIP :: i ("\<bottom>")
+ Join :: "[i, i] => i" (infixl "\<squnion>" 65)
+ "@JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
+ "@JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 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 \<in> A co B) <-> (A\<subseteq>B & st_set(A))"
+by (unfold constrains_def st_set_def, auto)
+
+lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B)<-> (state Int A\<subseteq>B)"
+by (unfold Constrains_def, auto)
+
+lemma SKIP_in_stable [iff]: "SKIP \<in> stable(A) <-> st_set(A)"
+by (auto simp add: stable_def)
+
+lemma SKIP_in_Stable [iff]: "SKIP \<in> Stable(A)"
+by (unfold Stable_def, auto)
+
+subsection{*Join and JOIN types*}
+
+lemma Join_in_program [iff,TC]: "F Join G \<in> program"
+by (unfold Join_def, auto)
+
+lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> 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(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> 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), \<Union>i \<in> 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(\<Squnion>i \<in> I. F(i)) =
+ (if I=0 then Pow(state*state) else (\<Inter>i \<in> 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]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) Join (\<Squnion>i \<in> I. F(i))"
+by (rule program_equalityI, auto)
+
+lemma JN_cong [cong]:
+ "[| I=J; !!i. i \<in> J ==> F(i) = G(i) |] ==>
+ (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))"
+by (simp add: JOIN_def)
+
+
+
+subsection{*JN laws*}
+lemma JN_absorb: "k \<in> I ==>F(k) Join (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))"
+apply (subst JN_cons [symmetric])
+apply (auto simp add: cons_absorb)
+done
+
+lemma JN_Un: "(\<Squnion>i \<in> I Un J. F(i)) = ((\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> 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: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))"
+by (rule program_equalityI, auto)
+
+lemma JN_Join_distrib:
+ "(\<Squnion>i \<in> I. F(i) Join G(i)) = (\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> 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: "(\<Squnion>i \<in> I. F(i) Join G) = ((\<Squnion>i \<in> 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 \<in> 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 \<in> A co B, i.e. to A\<subseteq>B. So an
+ alternative precondition is A\<subseteq>B, but most proofs using this rule require
+ I to be nonempty for other reasons anyway.*)
+
+lemma JN_constrains:
+ "i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B <-> (\<forall>i \<in> I. programify(F(i)) \<in> 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 \<in> A co B) <-> (programify(F) \<in> A co B & programify(G) \<in> A co B)"
+by (auto simp add: constrains_def)
+
+lemma Join_unless [iff]:
+ "(F Join G \<in> A unless B) <->
+ (programify(F) \<in> A unless B & programify(G) \<in> 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 \<in> A co A'; G \<in> B co B' |]
+ ==> F Join G \<in> (A Int B) co (A' Un B')"
+apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program")
+prefer 2 apply (blast dest: constrainsD2, simp)
+apply (blast intro: constrains_weaken)
+done
+
+(*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*)
+lemma JN_constrains_weaken:
+ assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))"
+ and minor: "i \<in> I"
+ shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> 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:
+ "(\<Squnion>i \<in> I. F(i)) \<in> stable(A) <-> ((\<forall>i \<in> I. programify(F(i)) \<in> 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 \<in> I ==>F(i) \<in> initially(A))"
+ and minor: "i \<in> I"
+ shows "(\<Squnion>i \<in> I. F(i)) \<in> 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 \<in> I ==> F(i) \<in> invariant(A))"
+ and minor: "i \<in> I"
+ shows "(\<Squnion>i \<in> I. F(i)) \<in> 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 \<in> 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 \<in> stable(A)) <->
+ (programify(F) \<in> stable(A) & programify(G) \<in> stable(A))"
+by (simp add: stable_def)
+
+lemma initially_JoinI [intro!]:
+ "[| F \<in> initially(A); G \<in> initially(A) |] ==> F Join G \<in> initially(A)"
+by (unfold initially_def, auto)
+
+lemma invariant_JoinI:
+ "[| F \<in> invariant(A); G \<in> invariant(A) |]
+ ==> F Join G \<in> invariant(A)"
+apply (subgoal_tac "F \<in> program&G \<in> program")
+prefer 2 apply (blast dest: invariantD2)
+apply (simp add: invariant_def)
+apply (auto intro: Join_in_program)
+done
+
+
+(* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *)
+lemma FP_JN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> 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 \<in> I ==>
+ (\<Squnion>i \<in> I. F(i)) \<in> transient(A) <-> (\<exists>i \<in> I. programify(F(i)) \<in> 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 \<in> transient(A) <->
+ (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))"
+apply (auto simp add: transient_def Join_def Int_Un_distrib2)
+done
+
+lemma Join_transient_I1: "F \<in> transient(A) ==> F Join G \<in> transient(A)"
+by (simp add: Join_transient transientD2)
+
+
+lemma Join_transient_I2: "G \<in> transient(A) ==> F Join G \<in> transient(A)"
+by (simp add: Join_transient transientD2)
+
+(*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *)
+lemma JN_ensures:
+ "i \<in> I ==>
+ (\<Squnion>i \<in> I. F(i)) \<in> A ensures B <->
+ ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A Un B)) &
+ (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))"
+by (auto simp add: ensures_def JN_constrains JN_transient)
+
+
+lemma Join_ensures:
+ "F Join G \<in> A ensures B <->
+ (programify(F) \<in> (A-B) co (A Un B) & programify(G) \<in> (A-B) co (A Un B) &
+ (programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))"
+
+apply (unfold ensures_def)
+apply (auto simp add: Join_transient)
+done
+
+lemma stable_Join_constrains:
+ "[| F \<in> stable(A); G \<in> A co A' |]
+ ==> F Join G \<in> 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 \<in> Stable A is
+ weaker than G \<in> stable A *)
+lemma stable_Join_Always1:
+ "[| F \<in> stable(A); G \<in> invariant(A) |] ==> F Join G \<in> Always(A)"
+apply (subgoal_tac "F \<in> program & G \<in> 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 \<in> invariant(A); G \<in> stable(A) |] ==> F Join G \<in> Always(A)"
+apply (subst Join_commute)
+apply (blast intro: stable_Join_Always1)
+done
+
+
+
+lemma stable_Join_ensures1:
+ "[| F \<in> stable(A); G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
+apply (subgoal_tac "F \<in> program & G \<in> 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 \<in> A ensures B; G \<in> stable(A) |] ==> F Join G \<in> 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) <-> (\<forall>i \<in> 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 <-> (\<forall>i \<in> 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) <-> (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F(i) ok (F(j)))"
+by (auto simp add: ok_def OK_def)
+
+lemma OK_imp_ok: "[| OK(I,F); i \<in> I; j \<in> I; i\<noteq>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 \<in> I ==>
+ Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))"
+apply (auto simp add: Allowed_def, blast)
+done
+
+lemma ok_iff_Allowed:
+ "F ok G <-> (programify(F) \<in> Allowed(programify(G)) &
+ programify(G) \<in> Allowed(programify(F)))"
+by (simp add: ok_def Allowed_def)
+
+
+lemma OK_iff_Allowed:
+ "OK(I,F) <->
+ (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> 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) \<subseteq> cons(id(state), (\<Union>F \<in> X. Acts(F)))) <-> (programify(G) \<in> X)"
+apply (simp (no_asm_use) add: safety_prop_def)
+apply clarify
+apply (case_tac "G \<in> 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) ==>
+ (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) <-> (X \<subseteq> 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, \<Union>F \<in> 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, \<Union>F \<in> 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 \<subseteq> 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\<subseteq>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 \<in> I ==>safety_prop(X(i)))"
+ and minor: "i \<in> I"
+ shows "safety_prop(\<Inter>i \<in> 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, \<Union>G \<in> X. Acts(G)); safety_prop(X) |]
+ ==> F ok G <-> (programify(G) \<in> X & acts Int Pow(state*state) \<subseteq> 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
--- 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 \\<in> WFair.ML,v 1.13 2003/06/30 16:15:52 paulson Exp $
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
@@ -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 = (\\<Union>b \\<in> 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) = (\\<Union>b \\<in> 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 \\<in> transient(A) ==> F \\<in> program & st_set(A)";
by Auto_tac;
qed "transientD2";
-Goal "[| F : stable(A); F : transient(A) |] ==> A = 0";
+Goal "[| F \\<in> stable(A); F \\<in> transient(A) |] ==> A = 0";
by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1);
by (Fast_tac 1);
qed "stable_transient_empty";
-Goalw [transient_def, st_set_def] "[|F:transient(A); B<=A|] ==> F:transient(B)";
+Goalw [transient_def, st_set_def] "[|F \\<in> transient(A); B<=A|] ==> F \\<in> transient(B)";
by Safe_tac;
by (res_inst_tac [("x", "act")] bexI 1);
by (ALLGOALS(Asm_full_simp_tac));
@@ -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 \\<in> Acts(F); A <= domain(act); act``A <= state-A; \
+\ F \\<in> program; st_set(A)|] ==> F \\<in> transient(A)";
by (Blast_tac 1);
qed "transientI";
val major::prems =
-Goalw [transient_def] "[| F:transient(A); \
-\ !!act. [| act:Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P";
+Goalw [transient_def] "[| F \\<in> transient(A); \
+\ !!act. [| act \\<in> Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P";
by (rtac (major RS CollectE) 1);
by (blast_tac (claset() addIs prems) 1);
qed "transientE";
@@ -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 \\<in> transient(A-B)|]==>F \\<in> A ensures B";
by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD]));
qed "ensuresI";
(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *)
-Goal "[| F:A co A Un B; F: transient(A) |] ==> F: A ensures B";
+Goal "[| F \\<in> A co A Un B; F \\<in> transient(A) |] ==> F \\<in> A ensures B";
by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
by (auto_tac (claset(), simpset() addsimps [ensures_def, transient_type RS subsetD]));
qed "ensuresI2";
-Goalw [ensures_def] "F:A ensures B ==> F:(A-B) co (A Un B) & F:transient (A-B)";
+Goalw [ensures_def] "F \\<in> A ensures B ==> F:(A-B) co (A Un B) & F \\<in> transient (A-B)";
by Auto_tac;
qed "ensuresD";
-Goalw [ensures_def] "[|F:A ensures A'; A'<=B' |] ==> F:A ensures B'";
+Goalw [ensures_def] "[|F \\<in> A ensures A'; A'<=B' |] ==> F \\<in> A ensures B'";
by (blast_tac (claset()
addIs [transient_strengthen, constrains_weaken]) 1);
qed "ensures_weaken_R";
(*The L-version (precondition strengthening) fails, but we have this*)
Goalw [ensures_def]
- "[| F:stable(C); F:A ensures B |] ==> F:(C Int A) ensures (C Int B)";
+ "[| F \\<in> stable(C); F \\<in> A ensures B |] ==> F:(C Int A) ensures (C Int B)";
by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
Diff_Int_distrib RS sym]) 1);
by (blast_tac (claset()
@@ -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 \\<in> stable(A); F \\<in> transient(C); A<=B Un C|] ==> F \\<in> A ensures B";
by (forward_tac [stable_type RS subsetD] 1);
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
by (Clarify_tac 1);
@@ -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 \\<in> program; A<=B |] ==> F \\<in> A ensures B";
by (rewrite_goal_tac [ensures_def,constrains_def,transient_def, st_set_def] 1);
by Auto_tac;
qed "subset_imp_ensures";
@@ -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 \\<in> A leadsTo B ==> F \\<in> program & st_set(A) & st_set(B)";
by (blast_tac (claset() addDs [leads_left, leads_right]) 1);
qed "leadsToD2";
Goalw [leadsTo_def, st_set_def]
- "[|F:A ensures B; st_set(A); st_set(B)|] ==> F:A leadsTo B";
+ "[|F \\<in> A ensures B; st_set(A); st_set(B)|] ==> F \\<in> A leadsTo B";
by (cut_facts_tac [ensures_type] 1);
by (auto_tac (claset() addIs [leads.Basis], simpset()));
qed "leadsTo_Basis";
AddIs [leadsTo_Basis];
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
-(* [| F:program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *)
+(* [| F \\<in> program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *)
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis);
-Goalw [leadsTo_def] "[|F: A leadsTo B; F: B leadsTo C |]==>F: A leadsTo C";
+Goalw [leadsTo_def] "[|F \\<in> A leadsTo B; F \\<in> B leadsTo C |]==>F \\<in> A leadsTo C";
by (auto_tac (claset() addIs [leads.Trans], simpset()));
qed "leadsTo_Trans";
(* Better when used in association with leadsTo_weaken_R *)
-Goalw [transient_def] "F:transient(A) ==> F : A leadsTo (state-A )";
+Goalw [transient_def] "F \\<in> transient(A) ==> F \\<in> A leadsTo (state-A )";
by (rtac (ensuresI RS leadsTo_Basis) 1);
by (ALLGOALS(Clarify_tac));
by (blast_tac (claset() addIs [transientI]) 2);
@@ -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 \\<in> A leadsTo (A' Un A') ==> F \\<in> 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 \\<in> A leadsTo (A' Un C Un C) ==> F \\<in> A leadsTo (A' Un C)";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "leadsTo_Un_duplicate2";
(*The Union introduction rule as we should have liked to state it*)
val [major, program,B]= Goalw [leadsTo_def, st_set_def]
-"[|(!!A. A:S ==> F:A leadsTo B); F:program; st_set(B)|]==>F:Union(S) leadsTo B";
+"[|(!!A. A \\<in> S ==> F \\<in> A leadsTo B); F \\<in> program; st_set(B)|]==>F \\<in> Union(S) leadsTo B";
by (cut_facts_tac [program, B] 1);
by Auto_tac;
by (rtac leads.Union 1);
@@ -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 \\<in> S ==>F:(A Int C) leadsTo B); F \\<in> program; st_set(B)|] \
\ ==>F:(Union(S)Int C)leadsTo B";
by (cut_facts_tac [program, B] 1);
by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1);
@@ -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 \\<in> I ==> F \\<in> A(i) leadsTo B); F \\<in> program; st_set(B)|]==>F:(\\<Union>i \\<in> I. A(i)) leadsTo B";
by (cut_facts_tac [program, B] 1);
by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1);
by (rtac leads.Union 1);
@@ -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 \\<in> A leadsTo C; F \\<in> B leadsTo C |] ==> F \\<in> (A Un B) leadsTo C";
by (stac Un_eq_Union 1);
by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1);
qed "leadsTo_Un";
val [major, program, B] = Goal
-"[|(!!x. x:A==> F:{x} leadsTo B); F:program; st_set(B) |] ==> F:A leadsTo B";
+"[|(!!x. x \\<in> A==> F:{x} leadsTo B); F \\<in> program; st_set(B) |] ==> F \\<in> A leadsTo B";
by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1);
by (rtac leadsTo_UN 1);
by (auto_tac (claset() addDs prems, simpset() addsimps [major, program, B]));
qed "single_leadsTo_I";
-Goal "[| F:program; st_set(A) |] ==> F: A leadsTo A";
+Goal "[| F \\<in> program; st_set(A) |] ==> F \\<in> A leadsTo A";
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "leadsTo_refl";
-Goal "F: A leadsTo A <-> F:program & st_set(A)";
+Goal "F \\<in> A leadsTo A <-> F \\<in> program & st_set(A)";
by (auto_tac (claset() addIs [leadsTo_refl]
addDs [leadsToD2], simpset()));
qed "leadsTo_refl_iff";
-Goal "F: 0 leadsTo B <-> (F:program & st_set(B))";
+Goal "F \\<in> 0 leadsTo B <-> (F \\<in> program & st_set(B))";
by (auto_tac (claset() addIs [subset_imp_leadsTo]
addDs [leadsToD2], simpset()));
qed "empty_leadsTo";
AddIffs [empty_leadsTo];
-Goal "F: A leadsTo state <-> (F:program & st_set(A))";
+Goal "F \\<in> A leadsTo state <-> (F \\<in> program & st_set(A))";
by (auto_tac (claset() addIs [subset_imp_leadsTo]
addDs [leadsToD2, st_setD], simpset()));
qed "leadsTo_state";
AddIffs [leadsTo_state];
-Goal "[| F:A leadsTo A'; A'<=B'; st_set(B') |] ==> F : A leadsTo B'";
+Goal "[| F \\<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \\<in> A leadsTo B'";
by (blast_tac (claset() addDs [leadsToD2]
addIs [subset_imp_leadsTo,leadsTo_Trans]) 1);
qed "leadsTo_weaken_R";
-Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'";
+Goal "[| F \\<in> A leadsTo A'; B<=A |] ==> F \\<in> B leadsTo A'";
by (ftac leadsToD2 1);
by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1);
qed_spec_mp "leadsTo_weaken_L";
-Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'";
+Goal "[| F \\<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \\<in> B leadsTo B'";
by (ftac leadsToD2 1);
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L,
leadsTo_Trans, leadsTo_refl]) 1);
qed "leadsTo_weaken";
(* This rule has a nicer conclusion *)
-Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B";
+Goal "[| F \\<in> transient(A); state-A<=B; st_set(B)|] ==> F \\<in> A leadsTo B";
by (ftac transientD2 1);
by (rtac leadsTo_weaken_R 1);
by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo]));
qed "transient_imp_leadsTo2";
(*Distributes over binary unions*)
-Goal "F:(A Un B) leadsTo C <-> (F:A leadsTo C & F : B leadsTo C)";
+Goal "F:(A Un B) leadsTo C <-> (F \\<in> A leadsTo C & F \\<in> B leadsTo C)";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
qed "leadsTo_Un_distrib";
Goal
-"(F:(UN i:I. A(i)) leadsTo B)<-> ((ALL i : I. F: A(i) leadsTo B) & F:program & st_set(B))";
+"(F:(\\<Union>i \\<in> I. A(i)) leadsTo B)<-> ((\\<forall>i \\<in> I. F \\<in> A(i) leadsTo B) & F \\<in> program & st_set(B))";
by (blast_tac (claset() addDs [leadsToD2]
addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
qed "leadsTo_UN_distrib";
-Goal "(F: Union(S) leadsTo B) <-> (ALL A:S. F : A leadsTo B) & F:program & st_set(B)";
+Goal "(F \\<in> Union(S) leadsTo B) <-> (\\<forall>A \\<in> S. F \\<in> A leadsTo B) & F \\<in> program & st_set(B)";
by (blast_tac (claset() addDs [leadsToD2]
addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
qed "leadsTo_Union_distrib";
-(*Set difference: 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 \\<in> maybe combine with leadsTo_weaken_L?*)
+Goal "[| F: (A-B) leadsTo C; F \\<in> B leadsTo C; st_set(C) |] ==> F \\<in> A leadsTo C";
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]
addDs [leadsToD2]) 1);
qed "leadsTo_Diff";
val [major,minor] = Goal
-"[|(!!i. i:I ==> F: A(i) leadsTo A'(i)); F:program |] \
-\ ==> F: (UN i:I. A(i)) leadsTo (UN i:I. A'(i))";
+"[|(!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); F \\<in> program |] \
+\ ==> F: (\\<Union>i \\<in> I. A(i)) leadsTo (\\<Union>i \\<in> I. A'(i))";
by (rtac leadsTo_Union 1);
by (ALLGOALS(Asm_simp_tac));
by Safe_tac;
@@ -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 \\<in> A leadsTo A'; F \\<in> B leadsTo B' |] ==> F \\<in> (A Un B) leadsTo (A' Un B')";
by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B')" 1);
by (blast_tac (claset() addDs [leadsToD2]) 2);
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1);
qed "leadsTo_Un_Un";
(** The cancellation law **)
-Goal "[|F: 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 \\<in> A leadsTo (A' Un B); F \\<in> B leadsTo B'|] ==> F \\<in> A leadsTo (A' Un B')";
+by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F \\<in> program" 1);
by (blast_tac (claset() addDs [leadsToD2]) 2);
by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]) 1);
qed "leadsTo_cancel2";
-Goal "[|F: A leadsTo (A' Un B); F : (B-A') leadsTo B'|]==> F: A leadsTo (A' Un B')";
+Goal "[|F \\<in> A leadsTo (A' Un B); F \\<in> (B-A') leadsTo B'|]==> F \\<in> A leadsTo (A' Un B')";
by (rtac leadsTo_cancel2 1);
by (assume_tac 2);
by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_weaken_R]) 1);
qed "leadsTo_cancel_Diff2";
-Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] ==> F:A leadsTo (B' Un A')";
+Goal "[| F \\<in> A leadsTo (B Un A'); F \\<in> B leadsTo B' |] ==> F \\<in> A leadsTo (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1);
qed "leadsTo_cancel1";
-Goal "[|F: A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F : A leadsTo (B' Un A')";
+Goal "[|F \\<in> A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F \\<in> A leadsTo (B' Un A')";
by (rtac leadsTo_cancel1 1);
by (assume_tac 2);
by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [leadsToD2]) 1);
@@ -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 \\<in> za leadsTo zb; \
+\ !!A B. [| F \\<in> A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \
+\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \
+\ F \\<in> B leadsTo C; P(B, C) |] \
\ ==> P(A, C); \
-\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A)|] \
+\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> S. st_set(A)|] \
\ ==> P(Union(S), B) \
\ |] ==> P(za, zb)";
by (cut_facts_tac [major] 1);
@@ -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 \\<in> 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 \\<in> A co A Un B; F \\<in> transient(A); st_set(B) |] ==> P(A, B); \
+\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \
+\ F \\<in> B leadsTo C; P(B, C) |] \
\ ==> P(A, C); \
-\ !!B S. [| ALL A:S. F:A leadsTo B; ALL A:S. P(A, B); st_set(B); ALL A:S. st_set(A) |] \
+\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> S. st_set(A) |] \
\ ==> P(Union(S), B) \
\ |] ==> P(za, zb)";
by (cut_facts_tac [major] 1);
@@ -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 \\<in> on the preconditions for B **)
+(*Lemma is the weak version \\<in> can't see how to do it in one step*)
val major::prems = Goal
- "[| F : za leadsTo zb; \
+ "[| F \\<in> 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 \\<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \
+\ !!S. [| \\<forall>A \\<in> S. P(A); \\<forall>A \\<in> S. st_set(A) |] ==> P(Union(S)) \
\ |] ==> P(za)";
(*by induction on this formula*)
by (subgoal_tac "P(zb) --> P(za)" 1);
-(*now solve first subgoal: this formula is sufficient*)
+(*now solve first subgoal \\<in> this formula is sufficient*)
by (blast_tac (claset() addIs leadsTo_refl::prems) 1);
by (rtac (major RS leadsTo_induct) 1);
by (REPEAT (blast_tac (claset() addIs prems) 1));
@@ -399,13 +399,13 @@
val [major, zb_prem, basis_prem, union_prem] = Goal
- "[| F : za leadsTo zb; \
+ "[| F \\<in> 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 \\<in> A ensures B; F \\<in> B leadsTo zb; P(B); st_set(A) |] ==> P(A); \
+\ !!S. \\<forall>A \\<in> S. F \\<in> A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \
\ |] ==> P(za)";
by (cut_facts_tac [major] 1);
-by (subgoal_tac "(F : za leadsTo zb) & P(za)" 1);
+by (subgoal_tac "(F \\<in> za leadsTo zb) & P(za)" 1);
by (etac conjunct2 1);
by (rtac (major RS leadsTo_induct_pre_aux) 1);
by (blast_tac (claset() addDs [leadsToD2]
@@ -417,7 +417,7 @@
(** The impossibility law **)
Goal
- "F : A leadsTo 0 ==> A=0";
+ "F \\<in> A leadsTo 0 ==> A=0";
by (etac leadsTo_induct_pre 1);
by (auto_tac (claset(), simpset() addsimps
[ensures_def, constrains_def, transient_def, st_set_def]));
@@ -426,11 +426,11 @@
qed "leadsTo_empty";
Addsimps [leadsTo_empty];
-(** PSP: Progress-Safety-Progress **)
+(** PSP \\<in> Progress-Safety-Progress **)
-(*Special case of PSP: Misra's "stable conjunction"*)
+(*Special case of PSP \\<in> Misra's "stable conjunction"*)
Goalw [stable_def]
- "[| F : A leadsTo A'; F : stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)";
+ "[| F \\<in> A leadsTo A'; F \\<in> stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)";
by (etac leadsTo_induct 1);
by (rtac leadsTo_Union_Int 3);
by (ALLGOALS(Asm_simp_tac));
@@ -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 \\<in> A leadsTo A'; F \\<in> stable(B) |]==>F: (B Int A) leadsTo (B Int A')";
by (asm_simp_tac (simpset()
addsimps psp_stable::Int_ac) 1);
qed "psp_stable2";
Goalw [ensures_def, constrains_def, st_set_def]
-"[| F: A ensures A'; F: B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))";
+"[| F \\<in> A ensures A'; F \\<in> B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))";
(*speeds up the proof*)
by (Clarify_tac 1);
by (blast_tac (claset() addIs [transient_strengthen]) 1);
qed "psp_ensures";
Goal
-"[|F: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 \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))";
+by (subgoal_tac "F \\<in> program & st_set(A) & st_set(A')& st_set(B)" 1);
by (blast_tac (claset() addSDs [constrainsD2, leadsToD2]) 2);
by (etac leadsTo_induct 1);
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3);
@@ -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 \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B') |] \
+\ ==> F \\<in> (B' Int A) leadsTo ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1);
qed "psp2";
Goalw [unless_def]
- "[| F : A leadsTo A'; F : B unless B'; st_set(B); st_set(B') |] \
-\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')";
+ "[| F \\<in> A leadsTo A'; F \\<in> B unless B'; st_set(B); st_set(B') |] \
+\ ==> F \\<in> (A Int B) leadsTo ((A' Int B) Un B')";
by (subgoal_tac "st_set(A)&st_set(A')" 1);
by (blast_tac (claset() addDs [leadsToD2]) 2);
by (dtac psp 1);
@@ -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 \\<in> r is any wf relation; f is any variant function **)
Goal "[| wf(r); \
-\ m:I; \
+\ m \\<in> I; \
\ field(r)<=I; \
-\ F:program; st_set(B);\
-\ ALL m:I. F : (A Int f-``{m}) leadsTo \
+\ F \\<in> program; st_set(B);\
+\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \
\ ((A Int f-``(converse(r)``{m})) Un B) |] \
-\ ==> F : (A Int f-``{m}) leadsTo B";
+\ ==> F \\<in> (A Int f-``{m}) leadsTo B";
by (eres_inst_tac [("a","m")] wf_induct2 1);
by (ALLGOALS(Asm_simp_tac));
-by (subgoal_tac "F : (A Int (f-``(converse(r)``{x}))) leadsTo B" 1);
+by (subgoal_tac "F \\<in> (A Int (f-``(converse(r)``{x}))) leadsTo B" 1);
by (stac vimage_eq_UN 2);
by (asm_simp_tac (simpset() delsimps UN_simps
addsimps [Int_UN_distrib]) 2);
@@ -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 \\<in> program; st_set(A); st_set(B); \
+\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \
\ ((A Int f-``(converse(r)``{m})) Un B) |] \
-\ ==> F : A leadsTo B";
+\ ==> F \\<in> A leadsTo B";
by (res_inst_tac [("b", "A")] subst 1);
by (res_inst_tac [("I", "I")] leadsTo_UN 2);
by (REPEAT (assume_tac 2));
@@ -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\\<notin>range(?y)" 1);
by (etac nat_induct 1);
by (res_inst_tac [("b", "succ(succ(xa))")] domainI 2);
by (res_inst_tac [("b","succ(0)")] domainI 1);
@@ -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 \\<in> (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 \\<in> program; st_set(A); st_set(B); \
+\ \\<forall>m \\<in> nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \
+\ ==> F \\<in> A leadsTo B";
by (res_inst_tac [("A1", "nat"),("f1", "%x. x")]
(wf_measure RS leadsTo_wf_induct) 1);
by (Clarify_tac 6);
@@ -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 \\<in> wlt(F, B) leadsTo B <-> (F \\<in> program & st_set(B))";
by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1);
qed "wlt_leadsTo_iff";
-(* [| F:program; st_set(B) |] ==> F:wlt(F, B) leadsTo B *)
+(* [| F \\<in> program; st_set(B) |] ==> F \\<in> wlt(F, B) leadsTo B *)
bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2));
-Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)";
+Goalw [wlt_def] "F \\<in> A leadsTo B ==> A <= wlt(F, B)";
by (ftac leadsToD2 1);
by (auto_tac (claset(), simpset() addsimps [st_set_def]));
qed "leadsTo_subset";
(*Misra's property W2*)
-Goal "F : A leadsTo B <-> (A <= wlt(F,B) & F:program & st_set(B))";
+Goal "F \\<in> A leadsTo B <-> (A <= wlt(F,B) & F \\<in> program & st_set(B))";
by Auto_tac;
by (REPEAT(blast_tac (claset() addDs [leadsToD2,leadsTo_subset]
addIs [leadsTo_weaken_L, wlt_leadsTo]) 1));
qed "leadsTo_eq_subset_wlt";
(*Misra's property W4*)
-Goal "[| F:program; st_set(B) |] ==> B <= wlt(F,B)";
+Goal "[| F \\<in> program; st_set(B) |] ==> B <= wlt(F,B)";
by (rtac leadsTo_subset 1);
by (asm_simp_tac (simpset()
addsimps [leadsTo_eq_subset_wlt RS iff_sym,
@@ -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 \\<in> (A1 - B) co (A1 Un B); \
+\ F \\<in> (A2 - C) co (A2 Un C) |] \
+\ ==> F \\<in> (A1 Un A2 - C) co (A1 Un A2 Un C)";
by (Blast_tac 1);
qed "leadsTo_123_aux";
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
-(* slightly different from the HOL one: 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 \\<in> B here is bounded *)
+Goal "F \\<in> A leadsTo A' \
+\ ==> \\<exists>B \\<in> Pow(state). A<=B & F \\<in> B leadsTo A' & F \\<in> (B-A') co (B Un A')";
by (ftac leadsToD2 1);
by (etac leadsTo_induct 1);
(*Basis*)
@@ -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 "\\<exists>y. y \\<in> Pi(S, %A. {Ba \\<in> Pow(state). A<=Ba & \
+ \ F \\<in> Ba leadsTo B & F \\<in> Ba - B co Ba Un B})" 1);
by (rtac AC_ball_Pi 2);
by (ALLGOALS(Clarify_tac));
by (rotate_tac 1 2);
by (dres_inst_tac [("x", "x")] bspec 2);
by (REPEAT(Blast_tac 2));
-by (res_inst_tac [("x", "UN A:S. y`A")] bexI 1);
+by (res_inst_tac [("x", "\\<Union>A \\<in> S. y`A")] bexI 1);
by Safe_tac;
by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3);
by (rtac leadsTo_Union 2);
@@ -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 \\<in> program; st_set(B) |] ==>F \\<in> (wlt(F, B) - B) co (wlt(F,B))";
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1);
by (assume_tac 1);
by (Blast_tac 1);
@@ -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 \\<in> 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 \\<in> A leadsTo (A' Un C); F \\<in> A' co (A' Un C); \
+\ F \\<in> B leadsTo (B' Un C); F \\<in> B' co (B' Un C) |] \
+\ ==> F \\<in> (A Int B) leadsTo ((A' Int B') Un C)";
by (subgoal_tac "st_set(C)&st_set(W)&st_set(W-C)&st_set(A')&st_set(A)\
-\ & st_set(B) & st_set(B') & F:program" 1);
+\ & st_set(B) & st_set(B') & F \\<in> program" 1);
by (Asm_simp_tac 2);
by (blast_tac (claset() addSDs [leadsToD2]) 2);
-by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1);
+by (subgoal_tac "F \\<in> (W-C) co (W Un B' Un C)" 1);
by (blast_tac (claset() addSIs [[asm_rl, wlt_constrains_wlt]
MRS constrains_Un RS constrains_weaken]) 2);
-by (subgoal_tac "F : (W-C) co W" 1);
+by (subgoal_tac "F \\<in> (W-C) co W" 1);
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS
(subset_Un_iff2 RS iffD1), Un_assoc]) 2);
-by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1);
+by (subgoal_tac "F \\<in> (A Int W - C) leadsTo (A' Int W Un C)" 1);
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2);
(** LEVEL 9 **)
-by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
+by (subgoal_tac "F \\<in> (A' Int W Un C) leadsTo (A' Int B' Un C)" 1);
by (rtac leadsTo_Un_duplicate2 2);
by (rtac leadsTo_Un_Un 2);
by (blast_tac (claset() addIs [leadsTo_refl]) 3);
@@ -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 \\<in> Fin(X); F \\<in> program; st_set(C) |] ==> \
+\(\\<forall>i \\<in> I. F \\<in> (A(i)) leadsTo (A'(i) Un C)) --> \
+\ (\\<forall>i \\<in> I. F \\<in> (A'(i)) co (A'(i) Un C)) --> \
+\ F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
by (etac Fin_induct 1);
by (auto_tac (claset(), simpset() addsimps [Inter_0]));
by (rtac completion 1);
@@ -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 \\<in> Fin(X); \
+\ !!i. i \\<in> I ==> F \\<in> A(i) leadsTo (A'(i) Un C); \
+\ !!i. i \\<in> I ==> F \\<in> A'(i) co (A'(i) Un C); F \\<in> program; st_set(C)|] \
+\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)";
by (resolve_tac [lemma RS mp RS mp] 1);
by (resolve_tac prems 3);
by (REPEAT(blast_tac (claset() addIs prems) 1));
qed "finite_completion";
Goalw [stable_def]
- "[| F : A leadsTo A'; F : stable(A'); \
-\ F : B leadsTo B'; F : stable(B') |] \
-\ ==> F : (A Int B) leadsTo (A' Int B')";
+ "[| F \\<in> A leadsTo A'; F \\<in> stable(A'); \
+\ F \\<in> B leadsTo B'; F \\<in> stable(B') |] \
+\ ==> F \\<in> (A Int B) leadsTo (A' Int B')";
by (res_inst_tac [("C1", "0")] (completion RS leadsTo_weaken_R) 1);
by (REPEAT(blast_tac (claset() addDs [leadsToD2, constrainsD2]) 5));
by (ALLGOALS(Asm_full_simp_tac));
@@ -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 \\<in> Fin(X); \
+\ (!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); \
+\ (!!i. i \\<in> I ==> F \\<in> stable(A'(i))); F \\<in> program |] \
+\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo (\\<Inter>i \\<in> I. A'(i))";
by (cut_facts_tac [major] 1);
-by (subgoal_tac "st_set(INT i:I. A'(i))" 1);
+by (subgoal_tac "st_set(\\<Inter>i \\<in> I. A'(i))" 1);
by (blast_tac (claset() addDs [leadsToD2]@prems) 2);
by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1);
by (Asm_simp_tac 1);