# HG changeset patch
# User paulson
# Date 1057743574 -7200
# Node ID 24382760fd89f49d509d074d953f1bc46820eefb
# Parent  68da54626309a71d99ea7e13d85b932b3060ddce
converting more theories to Isar scripts, and tidying

diff -r 68da54626309 -r 24382760fd89 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/IsaMakefile	Wed Jul 09 11:39:34 2003 +0200
@@ -115,15 +115,14 @@
 ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
 
 $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
-  UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
-  UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
+  UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
+  UNITY/FP.thy UNITY/Guar.thy \
   UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.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\
-  UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
-  UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
+  UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\
+  UNITY/Monotonicity.thy\
   UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
   UNITY/WFair.ML UNITY/WFair.thy
 	@$(ISATOOL) usedir $(OUT)/ZF UNITY
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Comp.ML
--- a/src/ZF/UNITY/Comp.ML	Tue Jul 08 11:44:30 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,348 +0,0 @@
-(*  Title:      ZF/UNITY/Comp.ML
-    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
-From Chandy and Sanders, "Reasoning About Program Composition"
-
-Revised by Sidi Ehmety on January 2001
-
-*)
-
-(*** component and strict_component relations ***)
-
-Goalw [component_def]
-     "H component F | H component G ==> H component (F Join G)";
-by Auto_tac;
-by (res_inst_tac [("x", "Ga Join G")] exI 1);
-by (res_inst_tac [("x", "G Join F")] exI 2);
-by (auto_tac (claset(), simpset() addsimps Join_ac));
-qed "componentI";
-
-Goalw [component_def]
-     "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);
-by (rtac program_equalityI 1);
-by Auto_tac;
-qed "component_eq_subset";
-
-Goalw [component_def] 
-   "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 \\<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";
-
-Addsimps [component_SKIP, component_refl];
-
-Goal "F component SKIP ==> programify(F) = SKIP";
-by (rtac program_equalityI 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset])));
-by (Blast_tac 1);
-qed "SKIP_minimal";
-
-Goalw [component_def] "F component (F Join G)";
-by (Blast_tac 1);
-qed "component_Join1";
-
-Goalw [component_def] "G component (F Join G)";
-by (simp_tac (simpset() addsimps [Join_commute]) 1);
-by (Blast_tac 1);
-qed "component_Join2";
-
-Goal "F component G ==> F Join G = G";
-by (auto_tac (claset(), simpset() 
-        addsimps [component_def, Join_left_absorb]));
-qed "Join_absorb1";
-
-Goal "G component F ==> F Join G = F";
-by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
-qed "Join_absorb2";
-
-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);
-by Auto_tac;
-by (Blast_tac 1); 
-by (rename_tac "y" 1);
-by (dres_inst_tac [("c", "y"), ("A", "AllowedActs(H)")] subsetD 1);
-by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
-qed "JN_component_iff";
-
-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";
-
-Goalw [component_def] "[| F component G; G component H |] ==> F component H";
-by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
-qed "component_trans";
-
-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 \\<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 \\<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(), 
-              simpset() addsimps [constrains_def, component_eq_subset]));
-qed "component_constrains";
-
-(* Used in Guar.thy to show that programs are partially ordered*)
-(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
-
-(*** preserves ***)
-
-Goalw [preserves_def, safety_prop_def]
-  "safety_prop(preserves(f))";
-by (auto_tac (claset() addDs [ActsD], simpset() addsimps [stable_def, constrains_def]));
-by (dres_inst_tac [("c", "act")] subsetD 1);
-by Auto_tac;
-qed "preserves_is_safety_prop";
-Addsimps [preserves_is_safety_prop];
-
-
-val prems = Goalw [preserves_def] 
-"\\<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 \\<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);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by Auto_tac;
-qed "preserves_imp_eq";
-
-Goalw [preserves_def]
-"(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)) <-> (\\<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 \\<in> preserves(v)";
-by (auto_tac (claset(), simpset() addsimps [preserves_def, INT_iff]));
-qed "SKIP_preserves";
-
-AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
-
-Goalw [fun_pair_def] "fun_pair(f,g,x) = <f(x), g(x)>";
-by (Simp_tac 1);
-qed "fun_pair_apply";
-Addsimps [fun_pair_apply];
-
-Goal "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)";
-by (rtac equalityI 1);
-by (auto_tac (claset(),
-              simpset() addsimps [preserves_def, stable_def, constrains_def]));
-by (REPEAT(Blast_tac 1));
-qed "preserves_fun_pair";
-
-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];
-
-Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
-by (simp_tac (simpset() addsimps [fun_pair_def, metacomp_def]) 1);
-qed "fun_pair_comp_distrib";
-
-Goal "(f comp g)(x) = f(g(x))";
-by (simp_tac (simpset() addsimps [metacomp_def]) 1);
-qed "comp_apply";
-Addsimps [comp_apply];
-
-Goalw [preserves_def]
- "preserves(v)<=program";
-by Auto_tac;
-qed "preserves_type";
-
-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];
-
-Goal "preserves(f) <= preserves(g comp f)";
-by (auto_tac (claset(),  simpset() 
-     addsimps [preserves_def, stable_def, constrains_def]));
-by (dres_inst_tac [("x", "f(xb)")] spec 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by Auto_tac;
-qed "subset_preserves_comp";
-
-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 \\<in> state. P(f(s))})";
-by (auto_tac (claset(),
-              simpset() addsimps [preserves_def, stable_def, constrains_def]));
-by (rename_tac "s' s" 1);
-by (subgoal_tac "f(s) = f(s')" 1);
-by (ALLGOALS Force_tac);
-qed "preserves_subset_stable";
-
-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 \\<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);
-by Auto_tac;
-qed "preserves_imp_increasing";
-
-Goalw [preserves_def, stable_def, constrains_def]
- "st_set(A) ==> preserves(%x. x) <= stable(A)";
-by Auto_tac;
-by (dres_inst_tac [("x", "xb")] spec 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by (auto_tac (claset() addDs [ActsD], simpset()));
-qed "preserves_id_subset_stable";
-
-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";
-
-(** Added by Sidi **)
-(** component_of **)
-
-(*  component_of is stronger than component *)
-Goalw [component_def, component_of_def]
-"F component_of H ==> F component H";
-by (Blast_tac 1);
-qed "component_of_imp_component";
-
-(* component_of satisfies many of component's properties *)
-Goalw [component_of_def]
-"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 \\<in> program ==>SKIP component_of F";
-by Auto_tac;
-by (res_inst_tac [("x", "F")] exI 1);
-by Auto_tac;
-qed "component_of_SKIP";
-Addsimps [component_of_refl, component_of_SKIP];
-
-Goalw [component_of_def]
-"[| F component_of G; G component_of H |] ==> F component_of H";
-by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
-qed "component_of_trans";
-
-(** localize **)
-Goalw [localize_def]
- "Init(localize(v,F)) = Init(F)";
-by (Simp_tac 1);
-qed "localize_Init_eq";
-
-Goalw [localize_def]
- "Acts(localize(v,F)) = Acts(F)";
-by (Simp_tac 1);
-qed "localize_Acts_eq";
-
-Goalw [localize_def]
- "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";
-
-AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
-
-(** Theorems used in ClientImpl **)
-
-Goal
- "[| 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 \\<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 \\<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]));
-by (ALLGOALS(asm_full_simp_tac (simpset()
-        addsimps [constrains_type RS subsetD, preserves_type RS subsetD])));
-by (blast_tac (claset() addIs [constrains_weaken]) 1); 
-(*The G case remains*)
-by (auto_tac (claset() addDs [ActsD], 
-              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 "\\<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";
-
-
-(** Lemma used in AllocImpl **)
-
-Goalw [Constrains_def, constrains_def] 
-"[| \\<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 \\<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 \\<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);
-by (auto_tac (claset(), simpset() addsimps [constrains_type RS subsetD]));
-by (ALLGOALS(rtac constrains_weaken));
-by (rotate_tac ~1 4);
-by (dres_inst_tac [("x", "k")] spec 4);
-by (REPEAT(Blast_tac 1));
-qed "stable_Join_Stable";
-
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Comp.thy
--- a/src/ZF/UNITY/Comp.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Comp.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -3,7 +3,6 @@
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Composition
 From Chandy and Sanders, "Reasoning About Program Composition",
 Technical Report 2000-003, University of Florida, 2000.
 
@@ -15,14 +14,16 @@
   
 *)
 
-Comp = Union + Increasing +
+header{*Composition*}
+
+theory Comp = Union + Increasing:
 
 constdefs
 
-  component :: [i, i] => o  (infixl 65) 
+  component :: "[i,i]=>o"  (infixl "component" 65) 
   "F component H == (EX G. F Join G = H)"
 
-  strict_component :: [i, i] => o (infixl "strict'_component" 65)
+  strict_component :: "[i,i]=>o" (infixl "strict'_component" 65)
   "F strict_component H == F component H & F~=H"
 
   (* A stronger form of the component relation *)
@@ -33,15 +34,360 @@
   "F strict_component_of H  == F component_of H  & F~=H"
 
   (* Preserves a state function f, in particular a variable *)
-  preserves :: (i=>i)=>i
+  preserves :: "(i=>i)=>i"
   "preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}"
 
   fun_pair :: "[i=>i, i =>i] =>(i=>i)"
   "fun_pair(f, g) == %x. <f(x), g(x)>"
 
-localize  :: "[i=>i, i] => i"
+  localize  :: "[i=>i, i] => i"
   "localize(f,F) == mk_program(Init(F), Acts(F),
 		       AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
 
   
-  end
+(*** component and strict_component relations ***)
+
+lemma componentI: 
+     "H component F | H component G ==> H component (F Join G)"
+apply (unfold component_def, auto)
+apply (rule_tac x = "Ga Join G" in exI)
+apply (rule_tac [2] x = "G Join F" in exI)
+apply (auto simp add: Join_ac)
+done
+
+lemma component_eq_subset: 
+     "G \<in> program ==> (F component G) <->  
+   (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))"
+apply (unfold component_def, auto)
+apply (rule exI)
+apply (rule program_equalityI, auto)
+done
+
+lemma component_SKIP [simp]: "F \<in> program ==> SKIP component F"
+apply (unfold component_def)
+apply (rule_tac x = F in exI)
+apply (force intro: Join_SKIP_left)
+done
+
+lemma component_refl [simp]: "F \<in> program ==> F component F"
+apply (unfold component_def)
+apply (rule_tac x = F in exI)
+apply (force intro: Join_SKIP_right)
+done
+
+lemma SKIP_minimal: "F component SKIP ==> programify(F) = SKIP"
+apply (rule program_equalityI)
+apply (simp_all add: component_eq_subset, blast)
+done
+
+lemma component_Join1: "F component (F Join G)"
+by (unfold component_def, blast)
+
+lemma component_Join2: "G component (F Join G)"
+apply (unfold component_def)
+apply (simp (no_asm) add: Join_commute)
+apply blast
+done
+
+lemma Join_absorb1: "F component G ==> F Join G = G"
+by (auto simp add: component_def Join_left_absorb)
+
+lemma Join_absorb2: "G component F ==> F Join G = F"
+by (auto simp add: Join_ac component_def)
+
+lemma JN_component_iff:
+     "H \<in> program==>(JOIN(I,F) component H) <-> (\<forall>i \<in> I. F(i) component H)"
+apply (case_tac "I=0", force)
+apply (simp (no_asm_simp) add: component_eq_subset)
+apply auto
+apply blast
+apply (rename_tac "y")
+apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD)
+apply (blast elim!: not_emptyE)+
+done
+
+lemma component_JN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))"
+apply (unfold component_def)
+apply (blast intro: JN_absorb)
+done
+
+lemma component_trans: "[| F component G; G component H |] ==> F component H"
+apply (unfold component_def)
+apply (blast intro: Join_assoc [symmetric])
+done
+
+lemma component_antisym:
+     "[| F \<in> program; G \<in> program |] ==>(F component G & G  component F) --> F = G"
+apply (simp (no_asm_simp) add: component_eq_subset)
+apply clarify
+apply (rule program_equalityI, auto)
+done
+
+lemma Join_component_iff:
+     "H \<in> program ==> 
+      ((F Join G) component H) <-> (F component H & G component H)"
+apply (simp (no_asm_simp) add: component_eq_subset)
+apply blast
+done
+
+lemma component_constrains:
+     "[| F component G; G \<in> A co B; F \<in> program |] ==> F \<in> A co B"
+apply (frule constrainsD2)
+apply (auto simp add: constrains_def component_eq_subset)
+done
+
+(* Used in Guar.thy to show that programs are partially ordered*)
+(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
+
+(*** preserves ***)
+
+lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
+apply (unfold preserves_def safety_prop_def)
+apply (auto dest: ActsD simp add: stable_def constrains_def)
+apply (drule_tac c = act in subsetD, auto)
+done
+
+lemma preservesI [rule_format]: 
+     "\<forall>z. F \<in> stable({s \<in> state. f(s) = z})  ==> F \<in> preserves(f)"
+apply (auto simp add: preserves_def)
+apply (blast dest: stableD2)
+done
+
+lemma preserves_imp_eq: 
+     "[| F \<in> preserves(f);  act \<in> Acts(F);  <s,t> \<in> act |] ==> f(s) = f(t)"
+apply (unfold preserves_def stable_def constrains_def)
+apply (subgoal_tac "s \<in> state & t \<in> state")
+ prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 
+done
+
+lemma Join_preserves [iff]: 
+"(F Join G \<in> preserves(v)) <->   
+      (programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))"
+by (auto simp add: preserves_def INT_iff)
+ 
+lemma JN_preserves [iff]:
+     "(JOIN(I,F): preserves(v)) <-> (\<forall>i \<in> I. programify(F(i)):preserves(v))"
+by (auto simp add: JN_stable preserves_def INT_iff)
+
+lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)"
+by (auto simp add: preserves_def INT_iff)
+
+lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>"
+apply (unfold fun_pair_def)
+apply (simp (no_asm))
+done
+
+lemma preserves_fun_pair:
+     "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)"
+apply (rule equalityI)
+apply (auto simp add: preserves_def stable_def constrains_def, blast+)
+done
+
+lemma preserves_fun_pair_iff [iff]:
+     "F \<in> preserves(fun_pair(v, w))  <-> F \<in> preserves(v) Int preserves(w)"
+by (simp add: preserves_fun_pair)
+
+lemma fun_pair_comp_distrib:
+     "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)"
+by (simp add: fun_pair_def metacomp_def)
+
+lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))"
+by (simp add: metacomp_def)
+
+lemma preserves_type: "preserves(v)<=program"
+by (unfold preserves_def, auto)
+
+lemma preserves_into_program [TC]: "F \<in> preserves(f) ==> F \<in> program"
+by (blast intro: preserves_type [THEN subsetD])
+
+lemma subset_preserves_comp: "preserves(f) <= preserves(g comp f)"
+apply (auto simp add: preserves_def stable_def constrains_def)
+apply (drule_tac x = "f (xb)" in spec)
+apply (drule_tac x = act in bspec, auto)
+done
+
+lemma imp_preserves_comp: "F \<in> preserves(f) ==> F \<in> preserves(g comp f)"
+by (blast intro: subset_preserves_comp [THEN subsetD])
+
+lemma preserves_subset_stable: "preserves(f) <= stable({s \<in> state. P(f(s))})"
+apply (auto simp add: preserves_def stable_def constrains_def)
+apply (rename_tac s' s)
+apply (subgoal_tac "f (s) = f (s') ")
+apply (force+)
+done
+
+lemma preserves_imp_stable:
+     "F \<in> preserves(f) ==> F \<in> stable({s \<in> state. P(f(s))})"
+by (blast intro: preserves_subset_stable [THEN subsetD])
+
+lemma preserves_imp_increasing: 
+ "[| F \<in> preserves(f); \<forall>x \<in> state. f(x):A |] ==> F \<in> Increasing.increasing(A, r, f)"
+apply (unfold Increasing.increasing_def)
+apply (auto intro: preserves_into_program)
+apply (rule_tac P = "%x. <k, x>:r" in preserves_imp_stable, auto)
+done
+
+lemma preserves_id_subset_stable: 
+ "st_set(A) ==> preserves(%x. x) <= stable(A)"
+apply (unfold preserves_def stable_def constrains_def, auto)
+apply (drule_tac x = xb in spec)
+apply (drule_tac x = act in bspec)
+apply (auto dest: ActsD)
+done
+
+lemma preserves_id_imp_stable:
+     "[| F \<in> preserves(%x. x); st_set(A) |] ==> F \<in> stable(A)"
+by (blast intro: preserves_id_subset_stable [THEN subsetD])
+
+(** Added by Sidi **)
+(** component_of **)
+
+(*  component_of is stronger than component *)
+lemma component_of_imp_component: 
+"F component_of H ==> F component H"
+apply (unfold component_def component_of_def, blast)
+done
+
+(* component_of satisfies many of component's properties *)
+lemma component_of_refl [simp]: "F \<in> program ==> F component_of F"
+apply (unfold component_of_def)
+apply (rule_tac x = SKIP in exI, auto)
+done
+
+lemma component_of_SKIP [simp]: "F \<in> program ==>SKIP component_of F"
+apply (unfold component_of_def, auto)
+apply (rule_tac x = F in exI, auto)
+done
+
+lemma component_of_trans: 
+     "[| F component_of G; G component_of H |] ==> F component_of H"
+apply (unfold component_of_def)
+apply (blast intro: Join_assoc [symmetric])
+done
+
+(** localize **)
+lemma localize_Init_eq [simp]: "Init(localize(v,F)) = Init(F)"
+by (unfold localize_def, simp)
+
+lemma localize_Acts_eq [simp]: "Acts(localize(v,F)) = Acts(F)"
+by (unfold localize_def, simp)
+
+lemma localize_AllowedActs_eq [simp]: 
+ "AllowedActs(localize(v,F)) = AllowedActs(F) Int (\<Union>G \<in> preserves(v). Acts(G))"
+apply (unfold localize_def)
+apply (rule equalityI)
+apply (auto dest: Acts_type [THEN subsetD])
+done
+
+
+(** Theorems used in ClientImpl **)
+
+lemma stable_localTo_stable2: 
+ "[| 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))})"
+apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def)
+apply (case_tac "act \<in> Acts (F) ")
+apply auto
+apply (drule preserves_imp_eq)
+apply (drule_tac [3] preserves_imp_eq, auto)
+done
+
+lemma Increasing_preserves_Stable:
+     "[| 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})"
+apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
+apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD])
+apply (blast intro: constrains_weaken)
+(*The G case remains*)
+apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
+(*We have a G-action, so delete assumptions about F-actions*)
+apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
+apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
+apply (subgoal_tac "f (x) = f (xa) ")
+apply (auto dest!: bspec)
+done
+
+
+(** Lemma used in AllocImpl **)
+
+lemma Constrains_UN_left: 
+     "[| \<forall>x \<in> I. F \<in> A(x) Co B; F \<in> program |] ==> F:(\<Union>x \<in> I. A(x)) Co B"
+by (unfold Constrains_def constrains_def, auto)
+
+
+lemma stable_Join_Stable: 
+ "[| 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))})"
+apply (unfold stable_def Stable_def preserves_def)
+apply (rule_tac A = "(\<Union>k \<in> A. {s \<in> state. f(s)=k} Int {s \<in> state. P (f (s), g (s))})" in Constrains_weaken_L)
+prefer 2 apply blast
+apply (rule Constrains_UN_left, auto)
+apply (rule_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))}" and A' = "({s \<in> state. f(s)=k} Un {s \<in> state. P (f (s), g (s))}) Int {s \<in> state. P (k, g (s))}" in Constrains_weaken)
+ prefer 2 apply blast 
+ prefer 2 apply blast 
+apply (rule Constrains_Int)
+apply (rule constrains_imp_Constrains)
+apply (auto simp add: constrains_type [THEN subsetD])
+apply (blast intro: constrains_weaken) 
+apply (drule_tac x = k in spec)
+apply (blast intro: constrains_weaken) 
+done
+
+ML
+{*
+val component_of_def = thm "component_of_def";
+val component_def = thm "component_def";
+
+val componentI = thm "componentI";
+val component_eq_subset = thm "component_eq_subset";
+val component_SKIP = thm "component_SKIP";
+val component_refl = thm "component_refl";
+val SKIP_minimal = thm "SKIP_minimal";
+val component_Join1 = thm "component_Join1";
+val component_Join2 = thm "component_Join2";
+val Join_absorb1 = thm "Join_absorb1";
+val Join_absorb2 = thm "Join_absorb2";
+val JN_component_iff = thm "JN_component_iff";
+val component_JN = thm "component_JN";
+val component_trans = thm "component_trans";
+val component_antisym = thm "component_antisym";
+val Join_component_iff = thm "Join_component_iff";
+val component_constrains = thm "component_constrains";
+val preserves_is_safety_prop = thm "preserves_is_safety_prop";
+val preservesI = thm "preservesI";
+val preserves_imp_eq = thm "preserves_imp_eq";
+val Join_preserves = thm "Join_preserves";
+val JN_preserves = thm "JN_preserves";
+val SKIP_preserves = thm "SKIP_preserves";
+val fun_pair_apply = thm "fun_pair_apply";
+val preserves_fun_pair = thm "preserves_fun_pair";
+val preserves_fun_pair_iff = thm "preserves_fun_pair_iff";
+val fun_pair_comp_distrib = thm "fun_pair_comp_distrib";
+val comp_apply = thm "comp_apply";
+val preserves_type = thm "preserves_type";
+val preserves_into_program = thm "preserves_into_program";
+val subset_preserves_comp = thm "subset_preserves_comp";
+val imp_preserves_comp = thm "imp_preserves_comp";
+val preserves_subset_stable = thm "preserves_subset_stable";
+val preserves_imp_stable = thm "preserves_imp_stable";
+val preserves_imp_increasing = thm "preserves_imp_increasing";
+val preserves_id_subset_stable = thm "preserves_id_subset_stable";
+val preserves_id_imp_stable = thm "preserves_id_imp_stable";
+val component_of_imp_component = thm "component_of_imp_component";
+val component_of_refl = thm "component_of_refl";
+val component_of_SKIP = thm "component_of_SKIP";
+val component_of_trans = thm "component_of_trans";
+val localize_Init_eq = thm "localize_Init_eq";
+val localize_Acts_eq = thm "localize_Acts_eq";
+val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
+val stable_localTo_stable2 = thm "stable_localTo_stable2";
+val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
+val Constrains_UN_left = thm "Constrains_UN_left";
+val stable_Join_Stable = thm "stable_Join_Stable";
+*}
+
+end
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Follows.ML
--- a/src/ZF/UNITY/Follows.ML	Tue Jul 08 11:44:30 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,487 +0,0 @@
-(*  Title:      ZF/UNITY/Follows
-    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
- 
-The Follows relation of Charpentier and Sivilotte
-*)
- 
-(*Does this hold for "invariant"?*)
-
-val prems =
-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); \\<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 \\<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 \\<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); \
-\   \\<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()));
-qed "imp_Always_comp2";
-
-(* comp LeadsTo *)
-
-Goalw [mono1_def, metacomp_def]
-"[| mono1(A, r, B, s, h); refl(A,r); trans[B](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;
-by (rtac single_LeadsTo_I 1);
-by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]) 2);
-by Auto_tac;
-by (rotate_tac 5 1);
-by (dres_inst_tac [("x", "g(sa)")] bspec 1);
-by (etac LeadsTo_weaken 2);
-by (auto_tac (claset(), simpset() addsimps [part_order_def, refl_def]));
-by (res_inst_tac [("b", "h(g(sa))")] trans_onD 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "subset_LeadsTo_comp";
-
-Goal
-"[| 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); \
-\   \\<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 \\<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); \
-\ \\<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);
-by Auto_tac;
-by (dres_inst_tac [("x", "f(sa)"),("P","%j. F \\<in> ?X(j) \\<longmapsto>w ?Y(j)")] bspec 1);
-by Auto_tac;
-by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
-by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
-by (dres_inst_tac [("x", "f1(x)"), ("x1", "f(sa)"), 
-                   ("P2", "%x y. \\<forall>u\\<in>B. ?P(x,y,u)")] (bspec RS bspec) 1);
-by (dres_inst_tac [("x", "g(x)"), ("x1", "g(sa)"), 
-                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
-by Auto_tac;
-by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
-by (auto_tac (claset(), simpset() addsimps [part_order_def]));
-qed "imp_LeadsTo_comp_right";
-
-Goalw [mono2_def, Increasing_def]
-"[| 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); \
-\ \\<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);
-by Auto_tac;
-by (dres_inst_tac [("x", "g(sa)")] bspec 1);
-by Auto_tac;
-by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
-by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
-by (dres_inst_tac [("x", "f(x)"), ("x1", "f(sa)")] (bspec RS bspec) 1);
-by (dres_inst_tac [("x", "g1(x)"), ("x1", "g(sa)"), 
-                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
-by Auto_tac;
-by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
-by (auto_tac (claset(), simpset() addsimps [part_order_def]));
-qed "imp_LeadsTo_comp_left";
-
-(**  This general result is used to prove Follows Un, munion, etc. **)
-Goal
-"[| 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); \
-\ \\<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";
-
-(* Follows type *)
-Goalw [Follows_def] "Follows(A, r, f, g)<=program";
-by (blast_tac (claset() addDs [Increasing_type RS subsetD]) 1);
-qed "Follows_type";
-
-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 \\<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 \\<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";
-
-Goalw [Follows_def] 
-"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
-\  ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)";
-by (Clarify_tac 1);
-by (forw_inst_tac [("f", "g")] IncreasingD 1);
-by (forw_inst_tac [("f", "f")] IncreasingD 1);
-by (rtac IntI 1);
-by (res_inst_tac [("h", "h")] imp_LeadsTo_comp 2);
-by (assume_tac 5);
-by (auto_tac (claset() addIs  [imp_Increasing_comp, imp_Always_comp], 
-             simpset() delsimps INT_simps));
-qed "subset_Follows_comp";
-
-Goal
-"[| 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 \\<in> 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 *)
-Goalw [Follows_def] 
-"[| 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 \\<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);
-by (rtac IntI 1);
-by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 2);
-by Safe_tac;
-by (res_inst_tac [("h", "h")] imp_Always_comp2 3);
-by (assume_tac 5);
-by (res_inst_tac [("h", "h")] imp_Increasing_comp2 2);
-by (assume_tac 4);
-by (res_inst_tac [("h", "h")] imp_Increasing_comp2 1);
-by (assume_tac 3);
-by (TRYALL(assume_tac));
-by (ALLGOALS(Asm_full_simp_tac)); 
-by (blast_tac (claset() addSDs [IncreasingD]) 1);
-by (res_inst_tac [("h", "h")] imp_LeadsTo_comp2 1);
-by (assume_tac 4);
-by Auto_tac;
-by (rewrite_goal_tac [mono2_def] 3);
-by (REPEAT(blast_tac (claset() addDs [IncreasingD]) 1));
-qed "imp_Follows_comp2";
-
-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 \\<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";
-
-(** Destruction rules for Follows **)
-
-Goalw [Follows_def]
-     "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 \\<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 \\<in> Always({s \\<in> state. <f(s),g(s)> \\<in> r})";
-by (Blast_tac 1);
-qed "Follows_imp_Always";
-
-Goalw [Follows_def]
- "[| 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 \\<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 \\<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 \\<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 \\<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);
-by (assume_tac 1);
-by (eres_inst_tac [("A","{s \\<in> state . f(s) = g(s)} \\<inter> {s \\<in> state . \\<langle>f(s), h(s)\\<rangle> \\<in> r}")] Always_weaken 1); 
-by Auto_tac;
-qed "Always_Follows1";
-
-Goalw [Follows_def, Increasing_def, Stable_def]
-"[| 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 \\<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);
-by (assume_tac 1);
-by (eres_inst_tac [("A","{s \\<in> state . g(s) = h(s)} \\<inter> {s \\<in> state . \\<langle>f(s), g(s)\\<rangle> \\<in> r}")] Always_weaken 1); 
-by Auto_tac;
-qed "Always_Follows2";
-
-(** Union properties (with the subset ordering) **)
-
-Goalw [refl_def, SetLe_def] "refl(Pow(A), SetLe(A))";
-by Auto_tac;
-qed "refl_SetLe";
-Addsimps [refl_SetLe];
-
-Goalw [trans_on_def, SetLe_def] "trans[Pow(A)](SetLe(A))";
-by Auto_tac;
-qed "trans_on_SetLe";
-Addsimps [trans_on_SetLe];
-
-Goalw [antisym_def, SetLe_def] "antisym(SetLe(A))";
-by Auto_tac;
-qed "antisym_SetLe";
-Addsimps [antisym_SetLe];
-
-Goalw [part_order_def] "part_order(Pow(A), SetLe(A))";
-by Auto_tac;
-qed "part_order_SetLe";
-Addsimps [part_order_SetLe];
-
-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 \\<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 \\<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 \\<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";
-
-(** Multiset union properties (with the MultLe ordering) **)
-
-Goalw [MultLe_def, refl_def] "refl(Mult(A), MultLe(A,r))";
-by Auto_tac;
-qed "refl_MultLe";
-Addsimps [refl_MultLe];
-
-Goalw [MultLe_def, id_def, lam_def]
- "[| 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 \\<in> Mult(A) ==> <M, M> \\<in> MultLe(A, r)";
-by Auto_tac;
-qed "MultLe_refl2";
-Addsimps [MultLe_refl2];
-
-Goalw [MultLe_def, trans_on_def] "trans[Mult(A)](MultLe(A,r))";
-by (auto_tac (claset() addIs [trancl_trans], simpset() addsimps [multirel_def]));
-qed "trans_on_MultLe";
-Addsimps [trans_on_MultLe];
-
-Goalw [MultLe_def] "MultLe(A, r)<= (Mult(A) * Mult(A))";
-by Auto_tac;
-by (dtac (multirel_type RS subsetD) 1);
-by Auto_tac;
-qed "MultLe_type";
-
-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);
-by (auto_tac (claset() addDs [MultLe_type RS subsetD], simpset()));
-qed "MultLe_trans";
-
-Goalw [part_order_def, part_ord_def]
-"part_order(A, r) ==> part_ord(A, r-id(A))";
-by (rewrite_goal_tac [refl_def, id_def, lam_def, irrefl_def] 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [trans_on_def]) 1);
-by Auto_tac;
-by (blast_tac (claset() addDs [trans_onD]) 1);
-by (full_simp_tac (simpset() addsimps [antisym_def]) 1);
-by Auto_tac;
-qed "part_order_imp_part_ord";
-
-Goalw [MultLe_def, antisym_def]
-  "part_order(A, r) ==> antisym(MultLe(A,r))";
-by (dtac part_order_imp_part_ord 1);
-by Auto_tac;
-by (dtac irrefl_on_multirel 1);
-by (forward_tac [multirel_type RS subsetD] 1);
-by (dtac multirel_trans 1);
-by (auto_tac (claset(), simpset() addsimps [irrefl_def]));
-qed "antisym_MultLe";
-Addsimps [antisym_MultLe];
-
-Goal  "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))";
-by (ftac antisym_MultLe 1);
-by (auto_tac (claset(), simpset() addsimps [part_order_def]));
-qed "part_order_MultLe";
-Addsimps [part_order_MultLe];
-
-Goalw [MultLe_def]
-"[| 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> \\<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 \\<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> \\<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,
-                              multiset_into_Mult], 
-               simpset() addsimps [Mult_iff_multiset]));
-qed "munion_mono";
-
-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 \\<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 \\<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);
-by (ALLGOALS(Asm_full_simp_tac));
-qed "Always_munion";
-
-Goal
-"[| 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";
-
-(** Used in ClientImp **)
-
-Goal 
-"!!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 \\<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);
-by (dtac Finite_into_Fin 1);
-by (etac Fin_induct 1);
-by (Asm_simp_tac 1);
-by (rtac Follows_constantI 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps  (thms"FiniteFun.intros"))));
-by Auto_tac;
-by (resolve_tac [Follows_munion] 1);
-by Auto_tac;
-qed "Follows_msetsum_UN";
-
-
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Follows.thy
--- a/src/ZF/UNITY/Follows.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Follows.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -1,27 +1,28 @@
 (*  Title:      ZF/UNITY/Follows
-    ID:         $Id$
+    ID:         $Id \<in> Follows.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2002  University of Cambridge
 
-The "Follows" relation of Charpentier and Sivilotte
-
 Theory ported from HOL.
 *)
 
-Follows = SubstAx + Increasing +
+header{*The "Follows" relation of Charpentier and Sivilotte*}
+
+theory Follows = SubstAx + Increasing:
+
 constdefs
   Follows :: "[i, i, i=>i, i=>i] => i"
   "Follows(A, r, f, g) == 
             Increasing(A, r, g) Int
             Increasing(A, r,f) Int
-            Always({s:state. <f(s), g(s)>:r}) Int
-           (INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"
+            Always({s \<in> state. <f(s), g(s)>:r}) Int
+           (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})"
 consts
-  Incr :: [i=>i]=>i   
-  n_Incr :: [i=>i]=>i
-  m_Incr :: [i=>i]=>i
-  s_Incr :: [i=>i]=>i
-  n_Fols :: [i=>i, i=>i]=>i   (infixl "n'_Fols" 65)
+  Incr :: "[i=>i]=>i"   
+  n_Incr :: "[i=>i]=>i"
+  m_Incr :: "[i=>i]=>i"
+  s_Incr :: "[i=>i]=>i"
+  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)
 
 syntax
   Follows' :: "[i=>i, i=>i, i, i] => i"
@@ -37,4 +38,482 @@
   "f n_Fols g" == "Follows(nat, Le, f, g)"
 
   "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
+
+
+(*Does this hold for "invariant"?*)
+
+lemma Follows_cong: 
+     "[|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 (simp add: Increasing_def Follows_def)
+
+
+lemma subset_Always_comp: 
+"[| 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})"
+apply (unfold mono1_def metacomp_def)
+apply (auto simp add: Always_eq_includes_reachable)
+done
+
+lemma imp_Always_comp: 
+"[| 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 intro: subset_Always_comp [THEN subsetD])
+
+
+lemma imp_Always_comp2: 
+"[| 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);  
+    \<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})"
+apply (auto simp add: Always_eq_includes_reachable mono2_def)
+apply (auto dest!: subsetD)
+done
+
+(* comp LeadsTo *)
+
+lemma subset_LeadsTo_comp: 
+"[| mono1(A, r, B, s, h); refl(A,r); trans[B](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})"
+
+apply (unfold mono1_def metacomp_def, clarify)
+apply (simp_all (no_asm_use) add: INT_iff)
+apply auto
+apply (rule single_LeadsTo_I)
+prefer 2 apply (blast dest: LeadsTo_type [THEN subsetD], auto)
+apply (rotate_tac 5)
+apply (drule_tac x = "g (sa) " in bspec)
+apply (erule_tac [2] LeadsTo_weaken)
+apply (auto simp add: part_order_def refl_def)
+apply (rule_tac b = "h (g (sa))" in trans_onD)
+apply blast
+apply auto
+done
+
+lemma imp_LeadsTo_comp: 
+"[| 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);  
+    \<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})"
+apply (rule subset_LeadsTo_comp [THEN subsetD], auto)
+done
+
+lemma imp_LeadsTo_comp_right: 
+"[| 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);  
+  \<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}"
+apply (unfold mono2_def Increasing_def)
+apply (rule single_LeadsTo_I, auto)
+apply (drule_tac x = "g (sa) " and A = B in bspec)
+apply auto
+apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
+apply auto
+apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
+apply auto
+apply (force simp add: part_order_def refl_def)
+apply (force simp add: part_order_def refl_def)
+apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec])
+apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) --> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply auto
+apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
+apply (auto simp add: part_order_def)
+done
+
+lemma imp_LeadsTo_comp_left: 
+"[| 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);  
+  \<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}"
+apply (unfold mono2_def Increasing_def)
+apply (rule single_LeadsTo_I, auto)
+apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
+apply auto
+apply (drule_tac x = "g (sa) " in bspec)
+apply auto
+apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
+apply auto
+apply (force simp add: part_order_def refl_def)
+apply (force simp add: part_order_def refl_def)
+apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
+apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) --> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply auto
+apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
+apply (auto simp add: part_order_def)
+done
+
+(**  This general result is used to prove Follows Un, munion, etc. **)
+lemma imp_LeadsTo_comp2: 
+"[| 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);  
+  \<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}"
+apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans)
+apply (blast intro: imp_LeadsTo_comp_right)
+apply (blast intro: imp_LeadsTo_comp_left)
+done
+
+(* Follows type *)
+lemma Follows_type: "Follows(A, r, f, g)<=program"
+apply (unfold Follows_def)
+apply (blast dest: Increasing_type [THEN subsetD])
+done
+
+lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program"
+by (blast dest: Follows_type [THEN subsetD])
+
+lemma FollowsD: 
+"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)"
+apply (unfold Follows_def)
+apply (blast dest: IncreasingD)
+done
+
+lemma Follows_constantI: 
+ "[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)"
+apply (unfold Follows_def, auto)
+apply (auto simp add: refl_def)
+done
+
+lemma subset_Follows_comp: 
+"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]  
+   ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)"
+apply (unfold Follows_def, clarify)
+apply (frule_tac f = g in IncreasingD)
+apply (frule_tac f = f in IncreasingD)
+apply (rule IntI)
+apply (rule_tac [2] h = h in imp_LeadsTo_comp)
+prefer 5 apply assumption
+apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps)
+done
+
+lemma imp_Follows_comp: 
+"[| 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)"
+apply (blast intro: subset_Follows_comp [THEN subsetD])
+done
+
+(* 2-place monotone operation \<in> 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 *)
+lemma imp_Follows_comp2: 
+"[| 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 \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"
+apply (unfold Follows_def, clarify)
+apply (frule_tac f = g in IncreasingD)
+apply (frule_tac f = f in IncreasingD)
+apply (rule IntI, safe)
+apply (rule_tac [3] h = h in imp_Always_comp2)
+prefer 5 apply assumption
+apply (rule_tac [2] h = h in imp_Increasing_comp2)
+prefer 4 apply assumption
+apply (rule_tac h = h in imp_Increasing_comp2)
+prefer 3 apply assumption
+apply simp_all
+apply (blast dest!: IncreasingD)
+apply (rule_tac h = h in imp_LeadsTo_comp2)
+prefer 4 apply assumption
+apply auto
+  prefer 3 apply (simp add: mono2_def) 
+apply (blast dest: IncreasingD)+
+done
+
+
+lemma Follows_trans:
+     "[| F \<in> Follows(A, r, f, g);  F \<in> Follows(A,r, g, h);  
+         trans[A](r) |] ==> F \<in> Follows(A, r, f, h)"
+apply (frule_tac f = f in FollowsD)
+apply (frule_tac f = g in FollowsD)
+apply (simp add: Follows_def)
+apply (simp add: Always_eq_includes_reachable INT_iff, auto)
+apply (rule_tac [2] B = "{s \<in> state. <k, g (s) > \<in> r}" in LeadsTo_Trans)
+apply (rule_tac b = "g (x) " in trans_onD)
+apply blast+
+done
+
+(** Destruction rules for Follows **)
+
+lemma Follows_imp_Increasing_left: 
+     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)"
+by (unfold Follows_def, blast)
+
+lemma Follows_imp_Increasing_right: 
+     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)"
+by (unfold Follows_def, blast)
+
+lemma Follows_imp_Always: 
+ "F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})"
+by (unfold Follows_def, blast)
+
+lemma Follows_imp_LeadsTo: 
+ "[| 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 (unfold Follows_def, blast)
+
+lemma Follows_LeadsTo_pfixLe:
+     "[| 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 intro: Follows_imp_LeadsTo)
+
+lemma Follows_LeadsTo_pfixGe:
+     "[| 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 intro: Follows_imp_LeadsTo)
+
+lemma Always_Follows1: 
+"[| 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)"
+apply (unfold Follows_def Increasing_def Stable_def)
+apply (simp add: INT_iff, auto)
+apply (rule_tac [3] C = "{s \<in> state. f (s) =g (s) }" and A = "{s \<in> state. <ka, h (s) > \<in> r}" and A' = "{s \<in> state. <ka, f (s) > \<in> r}" in Always_LeadsTo_weaken)
+apply (erule_tac A = "{s \<in> state. <ka,f (s) > \<in> r}" and A' = "{s \<in> state. <ka,f (s) > \<in> r}" in Always_Constrains_weaken)
+apply auto
+apply (drule Always_Int_I, assumption)
+apply (erule_tac A = "{s \<in> state . f (s) = g (s) } \<inter> {s \<in> state . \<langle>f (s), h (s) \<rangle> \<in> r}" in Always_weaken)
+apply auto
+done
+
+lemma Always_Follows2: 
+"[| 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)"
+apply (unfold Follows_def Increasing_def Stable_def)
+apply (simp (no_asm_use) add: INT_iff)
+apply auto
+apply (erule_tac [3] V = "k \<in> A" in thin_rl)
+apply (rule_tac [3] C = "{s \<in> state. g (s) =h (s) }" and A = "{s \<in> state. <ka, g (s) > \<in> r}" and A' = "{s \<in> state. <ka, f (s) > \<in> r}" in Always_LeadsTo_weaken)
+apply (erule_tac A = "{s \<in> state. <ka, g (s) > \<in> r}" and A' = "{s \<in> state. <ka, g (s) > \<in> r}" in Always_Constrains_weaken)
+apply auto
+apply (drule Always_Int_I, assumption)
+apply (erule_tac A = "{s \<in> state . g (s) = h (s) } \<inter> {s \<in> state . \<langle>f (s), g (s) \<rangle> \<in> r}" in Always_weaken)
+apply auto
+done
+
+(** Union properties (with the subset ordering) **)
+
+lemma refl_SetLe [simp]: "refl(Pow(A), SetLe(A))"
+by (unfold refl_def SetLe_def, auto)
+
+lemma trans_on_SetLe [simp]: "trans[Pow(A)](SetLe(A))"
+by (unfold trans_on_def SetLe_def, auto)
+
+lemma antisym_SetLe [simp]: "antisym(SetLe(A))"
+by (unfold antisym_def SetLe_def, auto)
+
+lemma part_order_SetLe [simp]: "part_order(Pow(A), SetLe(A))"
+by (unfold part_order_def, auto)
+
+lemma increasing_Un:
+     "[| 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 (rule_tac h = "op Un" in imp_increasing_comp2, auto)
+
+lemma Increasing_Un:
+     "[| 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 (rule_tac h = "op Un" in imp_Increasing_comp2, auto)
+
+lemma Always_Un:
+     "[| 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 (simp add: Always_eq_includes_reachable, blast)
+
+lemma Follows_Un: 
+"[| 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 (rule_tac h = "op Un" in imp_Follows_comp2, auto)
+
+(** Multiset union properties (with the MultLe ordering) **)
+
+lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))"
+by (unfold MultLe_def refl_def, auto)
+
+lemma MultLe_refl1 [simp]: 
+ "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)"
+apply (unfold MultLe_def id_def lam_def)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma MultLe_refl2 [simp]: "M \<in> Mult(A) ==> <M, M> \<in> MultLe(A, r)"
+by (unfold MultLe_def id_def lam_def, auto)
+
+
+lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))"
+apply (unfold MultLe_def trans_on_def)
+apply (auto intro: trancl_trans simp add: multirel_def)
+done
+
+lemma MultLe_type: "MultLe(A, r)<= (Mult(A) * Mult(A))"
+apply (unfold MultLe_def, auto)
+apply (drule multirel_type [THEN subsetD], auto)
+done
+
+lemma MultLe_trans:
+     "[| <M,K> \<in> MultLe(A,r); <K,N> \<in> MultLe(A,r) |] ==> <M,N> \<in> MultLe(A,r)"
+apply (cut_tac A=A in trans_on_MultLe)
+apply (drule trans_onD, assumption)
+apply (auto dest: MultLe_type [THEN subsetD])
+done
+
+lemma part_order_imp_part_ord: 
+     "part_order(A, r) ==> part_ord(A, r-id(A))"
+apply (unfold part_order_def part_ord_def)
+apply (simp add: refl_def id_def lam_def irrefl_def, auto)
+apply (simp (no_asm) add: trans_on_def)
+apply auto
+apply (blast dest: trans_onD)
+apply (simp (no_asm_use) add: antisym_def)
+apply auto
+done
+
+lemma antisym_MultLe [simp]: 
+  "part_order(A, r) ==> antisym(MultLe(A,r))"
+apply (unfold MultLe_def antisym_def)
+apply (drule part_order_imp_part_ord, auto)
+apply (drule irrefl_on_multirel)
+apply (frule multirel_type [THEN subsetD])
+apply (drule multirel_trans)
+apply (auto simp add: irrefl_def)
+done
+
+lemma part_order_MultLe [simp]:
+     "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))"
+apply (frule antisym_MultLe)
+apply (auto simp add: part_order_def)
+done
+
+lemma empty_le_MultLe [simp]: 
+"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)"
+apply (unfold MultLe_def)
+apply (case_tac "M=0")
+apply (auto simp add: FiniteFun.intros)
+apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))")
+apply (rule_tac [2] one_step_implies_multirel)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)"
+by (simp add: Mult_iff_multiset)
+
+lemma munion_mono: 
+"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==> 
+  <M +# K, N +# L> \<in> MultLe(A, r)"
+apply (unfold MultLe_def)
+apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
+       munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset)
+done
+
+lemma increasing_munion:
+     "[| 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 (rule_tac h = munion in imp_increasing_comp2, auto)
+
+lemma Increasing_munion:
+     "[| 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 (rule_tac h = munion in imp_Increasing_comp2, auto)
+
+lemma Always_munion: 
+"[| 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)})"
+apply (rule_tac h = munion in imp_Always_comp2, simp_all)
+apply (blast intro: munion_mono, simp_all)
+done
+
+lemma Follows_munion: 
+"[| 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 (rule_tac h = munion in imp_Follows_comp2, auto)
+
+(** Used in ClientImp **)
+
+lemma Follows_msetsum_UN: 
+"!!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 \<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))"
+apply (erule rev_mp)
+apply (drule Finite_into_Fin)
+apply (erule Fin_induct)
+apply (simp (no_asm_simp))
+apply (rule Follows_constantI)
+apply (simp_all (no_asm_simp) add: FiniteFun.intros)
+apply auto
+apply (rule Follows_munion, auto)
+done
+
+ML
+{*
+val Follows_cong = thm "Follows_cong";
+val subset_Always_comp = thm "subset_Always_comp";
+val imp_Always_comp = thm "imp_Always_comp";
+val imp_Always_comp2 = thm "imp_Always_comp2";
+val subset_LeadsTo_comp = thm "subset_LeadsTo_comp";
+val imp_LeadsTo_comp = thm "imp_LeadsTo_comp";
+val imp_LeadsTo_comp_right = thm "imp_LeadsTo_comp_right";
+val imp_LeadsTo_comp_left = thm "imp_LeadsTo_comp_left";
+val imp_LeadsTo_comp2 = thm "imp_LeadsTo_comp2";
+val Follows_type = thm "Follows_type";
+val Follows_into_program = thm "Follows_into_program";
+val FollowsD = thm "FollowsD";
+val Follows_constantI = thm "Follows_constantI";
+val subset_Follows_comp = thm "subset_Follows_comp";
+val imp_Follows_comp = thm "imp_Follows_comp";
+val imp_Follows_comp2 = thm "imp_Follows_comp2";
+val Follows_trans = thm "Follows_trans";
+val Follows_imp_Increasing_left = thm "Follows_imp_Increasing_left";
+val Follows_imp_Increasing_right = thm "Follows_imp_Increasing_right";
+val Follows_imp_Always = thm "Follows_imp_Always";
+val Follows_imp_LeadsTo = thm "Follows_imp_LeadsTo";
+val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe";
+val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe";
+val Always_Follows1 = thm "Always_Follows1";
+val Always_Follows2 = thm "Always_Follows2";
+val refl_SetLe = thm "refl_SetLe";
+val trans_on_SetLe = thm "trans_on_SetLe";
+val antisym_SetLe = thm "antisym_SetLe";
+val part_order_SetLe = thm "part_order_SetLe";
+val increasing_Un = thm "increasing_Un";
+val Increasing_Un = thm "Increasing_Un";
+val Always_Un = thm "Always_Un";
+val Follows_Un = thm "Follows_Un";
+val refl_MultLe = thm "refl_MultLe";
+val MultLe_refl1 = thm "MultLe_refl1";
+val MultLe_refl2 = thm "MultLe_refl2";
+val trans_on_MultLe = thm "trans_on_MultLe";
+val MultLe_type = thm "MultLe_type";
+val MultLe_trans = thm "MultLe_trans";
+val part_order_imp_part_ord = thm "part_order_imp_part_ord";
+val antisym_MultLe = thm "antisym_MultLe";
+val part_order_MultLe = thm "part_order_MultLe";
+val empty_le_MultLe = thm "empty_le_MultLe";
+val empty_le_MultLe2 = thm "empty_le_MultLe2";
+val munion_mono = thm "munion_mono";
+val increasing_munion = thm "increasing_munion";
+val Increasing_munion = thm "Increasing_munion";
+val Always_munion = thm "Always_munion";
+val Follows_munion = thm "Follows_munion";
+val Follows_msetsum_UN = thm "Follows_msetsum_UN";
+*}
+
 end
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Guar.ML
--- a/src/ZF/UNITY/Guar.ML	Tue Jul 08 11:44:30 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,548 +0,0 @@
-(*  Title:      ZF/UNITY/Guar.ML
-    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
-
-Guarantees, etc.
-
-From Chandy and Sanders, "Reasoning About Program Composition"
-Revised by Sidi Ehmety on January 2001
-
-Proofs ported from HOL.
-*)
-
-Goal "OK(cons(i, 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;
-by (ALLGOALS(Clarify_tac));
-by (REPEAT(blast_tac (claset() addIs [ok_sym]) 10));
-by (REPEAT(Blast_tac 1));
-qed "OK_cons_iff";
-
-(*** existential properties ***)
-
-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 \\<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])));
-(* Auto_tac proves the goal in one step *)
-by (safe_tac (claset() addSEs [not_emptyE]));
-by (ALLGOALS(Asm_full_simp_tac));
-by (Fast_tac 1);
-qed_spec_mp "ex1";
-
-Goalw [ex_prop_def]
-"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);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_iff_ok])));
-by Safe_tac;
-by (auto_tac (claset() addIs [ok_sym], simpset()));
-qed "ex2";
-
-(*Chandy & Sanders take this as a definition*)
-
-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])));
-qed "ex_prop_finite";
-
-(* Equivalent definition of ex_prop given at the end of section 3*)
-Goalw [ex_prop_def, component_of_def]
-"ex_prop(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);
-by (dres_inst_tac [("x", "G")] bspec 4);
-by (dres_inst_tac [("x", "F")] bspec 3);
-by Safe_tac;
-by (REPEAT(Force_tac 1));
-qed "ex_prop_equiv";
-
-(*** universal properties ***)
-
-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 \\<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\\<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);
-by (dres_inst_tac [("x", "0")] spec 1);
-by (auto_tac (claset() addDs [ok_sym], 
-    simpset() addsimps [OK_iff_ok]));
-qed "uv2";
-
-(*Chandy & Sanders take this as a definition*)
-Goal 
-"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));
-qed "uv_prop_finite";
-
-(*** guarantees ***)
-val major::prems = Goal
-     "[| (!!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 \\<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\\<subseteq>H since we need to reason about G*)
-
-Goalw [guar_def]
-     "[| 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 \\<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 \\<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 \\<subseteq> Y; F \\<in> program |] \
-\  ==> F \\<in> X guarantees Y";
-by (Blast_tac 1);
-qed "subset_imp_guarantees";
-
-Goalw [component_of_def] 
-"F ok G ==> F component_of (F Join G)";
-by (Blast_tac 1);
-qed "component_of_Join1";
-
-Goal "F ok G ==> G component_of (F Join G)";
-by (stac Join_commute 1);
-by (blast_tac (claset() addIs [ok_sym, component_of_Join1]) 1);
-qed "component_of_Join2";
-
-(*Remark at end of section 4.1 *)
-Goalw [guar_def, component_of_def] 
-"ex_prop(Y) ==> (Y = (program guarantees Y))";
-by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by (Clarify_tac 1);
-by (rtac equalityI 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "x")] bspec 2);
-by (dres_inst_tac [("x", "x")] bspec 4);
-by (dtac iff_sym 5);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_Join1])));
-by (etac iffE 3);
-by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
-by Safe_tac;
-by (REPEAT(Force_tac 1));
-qed "ex_prop_imp";
-
-Goalw [guar_def] "(Y = program guarantees Y) ==> ex_prop(Y)";
-by (asm_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
-by Safe_tac;
-by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
-by (dtac sym 2);
-by (ALLGOALS(etac equalityE));
-by (REPEAT(Force_tac 1));
-qed "guarantees_imp";
-
-Goal "(ex_prop(Y)) <-> (Y = program guarantees Y)";
-by (blast_tac (claset() addIs [ex_prop_imp, guarantees_imp]) 1);
-qed "ex_prop_equiv2";
-
-(** Distributive laws.  Re-orient to perform miniscoping **)
-
-Goalw [guar_def]
-     "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);
-by (REPEAT(Blast_tac 1));
-qed "guarantees_UN_left";
-
-Goalw [guar_def]
-     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
-by (rtac equalityI 1);
-by Safe_tac;
-by (REPEAT(Blast_tac 1));
-qed "guarantees_Un_left";
-
-Goalw [guar_def]
-     "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));
-qed "guarantees_INT_right";
-
-Goalw [guar_def]
-     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
-by (Blast_tac 1);
-qed "guarantees_Int_right";
-
-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 \\<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";
-
-
-Goalw [guar_def] "(X guarantees Y) = (program guarantees ((program-X) Un Y))";
-by Auto_tac;
-qed "shunting";
-
-Goalw [guar_def] "(X guarantees Y) = (program - Y) guarantees (program -X)";
-by (Blast_tac 1);
-qed "contrapositive";
-
-(** The following two can be expressed using intersection and subset, which
-    is more faithful to the text but looks cryptic.
-**)
-
-Goalw [guar_def]
-    "[| 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 \\<in> V guarantees (X Un Y);  F \\<in> Y guarantees Z |]\
-\    ==> F \\<in> V guarantees (X Un Z)";
-by (Blast_tac 1);
-qed "combining2";
-
-
-(** The following two follow Chandy-Sanders, but the use of object-quantifiers
-    does not suit Isabelle... **)
-
-(*Premise should be (!!i. i \\<in> I ==> F \\<in> X guarantees Y i) *)
-Goalw [guar_def]
-     "[| \\<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 \\<in> X guarantees Y i; i \\<in> I |] *)
-Goalw [guar_def]
-     "\\<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";
-
-
-(*** Additional guarantees laws, by lcp ***)
-
-Goalw [guar_def]
-    "[| 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;
-by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
-by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
-by (asm_simp_tac (simpset() addsimps Join_ac) 1);
-qed "guarantees_Join_Int";
-
-Goalw [guar_def]
-    "[| 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;
-by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
-by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (rotate_tac 4 1);
-by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
-by (Simp_tac 1);
-by (force_tac (claset(), simpset() addsimps [ok_commute]) 1);
-by (asm_simp_tac (simpset() addsimps Join_ac) 1);
-qed "guarantees_Join_Un";
-
-Goalw [guar_def]
-     "[| \\<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", "(\\<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]
-    "[| \\<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));
-by Safe_tac;
-by (rotate_tac ~1 1);
-by (rename_tac "G y" 1);
-by (dres_inst_tac [("x", "JOIN(I-{y}, F) 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_UN";
-
-(*** guarantees laws for breaking down the program, by lcp ***)
-
-Goalw [guar_def]
-     "[| 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 \\<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 \\<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);
-by (auto_tac (claset() addIs [OK_imp_ok],
-              simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
-qed "guarantees_JN_I";
-
-(*** well-definedness ***)
-
-Goalw [welldef_def] "F Join G \\<in> welldef ==> programify(F): welldef";
-by Auto_tac;
-qed "Join_welldef_D1";
-
-Goalw [welldef_def] "F Join G \\<in> welldef ==> programify(G): welldef";
-by Auto_tac;
-qed "Join_welldef_D2";
-
-(*** refinement ***)
-
-Goalw [refines_def] "F refines F wrt X";
-by (Blast_tac 1);
-qed "refines_refl";
-
-(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
-
-Goalw [wg_def] "wg(F, X) \\<subseteq> program";
-by Auto_tac;
-qed "wg_type";
-
-Goalw [guar_def] "X guarantees Y \\<subseteq> program";
-by Auto_tac;
-qed "guarantees_type";
-
-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 \\<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 \\<in> (X guarantees Y); X \\<subseteq> program |] ==> X \\<subseteq> wg(F,Y)";
-by Auto_tac;
-qed "wg_weakest";
-
-Goalw [wg_def, guar_def] 
-"F \\<in> program ==> F \\<in> wg(F,Y) guarantees Y";
-by (Blast_tac 1);
-qed "wg_guarantees";
-
-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;
-by (res_inst_tac [("x", "{H}")] bexI 4);
-by (res_inst_tac [("x", "{H}")] bexI 3);
-by (REPEAT(Blast_tac 1));
-qed "wg_equiv";
-
-Goal
-"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
-"\\<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 (\\<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", "\\<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 \\<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 \\<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)\\<subseteq>X";
-by Auto_tac;
-qed "wx_subset";
-
-Goal "ex_prop(wx(X))";
-by (full_simp_tac (simpset() addsimps [ex_prop_def, wx_def]) 1);
-by Safe_tac;
-by (Blast_tac 1);
-by (ALLGOALS(res_inst_tac [("x", "x")] bexI));
-by (REPEAT(Force_tac 1));
-qed "wx_ex_prop";
-
-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 \\<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);
-by (force_tac (claset(), simpset() addsimps [Join_assoc]) 1);
-by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
-by (Simp_tac 1);
-by (Full_simp_tac 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
-by (subgoal_tac "F Join G = G Join F" 1);
-by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
-by (simp_tac (simpset() addsimps [Join_commute]) 1);
-qed "wx'_ex_prop";
-
-(* Equivalence with the other definition of wx *)
-
-Goalw [wx_def]
- "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);
-by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "x")] bspec 1);
-by (dres_inst_tac [("x", "G")] bspec 2);
-by (forw_inst_tac [("c", "x Join G")] subsetD 3);
-by Safe_tac;
-by (Blast_tac 1);
-by (Blast_tac 1);
-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);
-by (rotate_tac 2 1);
-by (dres_inst_tac [("x", "SKIP")] bspec 1);
-by Auto_tac;
-qed "wx_equiv";
-
-(* Propositions 7 to 11 are all about this second definition of wx. And
-   by equivalence between the two definition, they are the same as the ones proved *)
-
-
-(* Proposition 12 *)
-(* Main result of the paper *)
-Goalw [guar_def]  "(X guarantees Y) = wx((program-X) Un Y)";
-by (simp_tac (simpset() addsimps [wx_equiv]) 1);
-by Auto_tac;
-qed "guarantees_wx_eq";
-
-(* 
-{* Corollary, but this result has already been proved elsewhere *}
- "ex_prop(X guarantees Y)";
-  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
-  qed "guarantees_ex_prop";
-*)
-
-(* Rules given in section 7 of Chandy and Sander's
-    Reasoning About Program composition paper *)
-
-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);
-by (rtac stable_Join_Always1 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [invariant_def])));
-by (auto_tac (claset(), simpset() addsimps [programify_def, initially_def]));
-qed "stable_guarantees_Always";
-
-(* To be moved to WFair.ML *)
-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);
-by (rtac (ensuresI RS leadsTo_Basis) 3);
-by (ALLGOALS(Blast_tac));
-qed "leadsTo_Basis'";
-
-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);
-by (Blast_tac 3);
-by (dtac constrains_weaken_R 1);
-by (assume_tac 2);
-by (rtac Join_transient_I1 2);
-by (REPEAT(Blast_tac 1));
-qed "constrains_guarantees_leadsTo";
-
-
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Guar.thy
--- a/src/ZF/UNITY/Guar.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Guar.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -1,5 +1,5 @@
 (*  Title:      ZF/UNITY/Guar.thy
-    ID:         $Id$
+    ID:         $Id \<in> Guar.thy,v 1.3 2001/11/15 14:51:43 ehmety Exp $
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   2001  University of Cambridge
 
@@ -10,7 +10,7 @@
 
 Revised by Sidi Ehmety on January 2001
 
-Added: Compatibility, weakest guarantees, etc.
+Added \<in> Compatibility, weakest guarantees, etc.
 
 and Weakest existential property,
 from Charpentier and Chandy "Theorems about Composition",
@@ -18,50 +18,508 @@
 
 Theory ported from HOL.
 *)
-Guar = Comp +
+
+
+header{*The Chandy-Sanders Guarantees Operator*}
+
+theory Guar = Comp: 
+
+
+(* To be moved to theory WFair???? *)
+lemma leadsTo_Basis': "[| F \<in> A co A Un B; F \<in> transient(A); st_set(B) |] ==> F \<in> A leadsTo B"
+apply (frule constrainsD2)
+apply (drule_tac B = "A-B" in constrains_weaken_L, blast) 
+apply (drule_tac B = "A-B" in transient_strengthen, blast) 
+apply (blast intro: ensuresI [THEN leadsTo_Basis])
+done
+
+
 constdefs
 
-  (*Existential and Universal properties.  I formalize the two-program
+  (*Existential and Universal properties.  We formalize the two-program
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
-   ex_prop :: i =>o
+   ex_prop :: "i => o"
    "ex_prop(X) == X<=program &
-    (ALL F:program. ALL G:program. F ok G --> F:X | G:X --> (F Join G):X)"
+    (\<forall>F \<in> program. \<forall>G \<in> program. F ok G --> F \<in> X | G \<in> X --> (F Join G) \<in> X)"
 
-  strict_ex_prop  :: i => o
+  strict_ex_prop  :: "i => o"
   "strict_ex_prop(X) == X<=program &
-   (ALL F:program. ALL  G:program. F ok G --> (F:X | G: X) <-> (F Join G : X))"
+   (\<forall>F \<in> program. \<forall>G \<in> program. F ok G --> (F \<in> X | G \<in> X) <-> (F Join G \<in> X))"
 
-  uv_prop  :: i => o
+  uv_prop  :: "i => o"
    "uv_prop(X) == X<=program &
-    (SKIP:X & (ALL F:program. ALL G:program. F ok G --> F:X & G:X --> (F Join G):X))"
+    (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X))"
   
- strict_uv_prop  :: i => o
+ strict_uv_prop  :: "i => o"
    "strict_uv_prop(X) == X<=program &
-    (SKIP:X & (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X)))"
+    (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G -->(F \<in> X & G \<in> X) <-> (F Join G \<in> X)))"
 
-  guar :: [i, i] => i (infixl "guarantees" 55)
+  guar :: "[i, i] => i" (infixl "guarantees" 55)
               (*higher than membership, lower than Co*)
-  "X guarantees Y == {F:program. ALL G:program. F ok G --> F Join G : X --> F Join G:Y}"
+  "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
   
   (* Weakest guarantees *)
-   wg :: [i,i] => i
-  "wg(F,Y) == Union({X:Pow(program). F:(X guarantees Y)})"
+   wg :: "[i,i] => i"
+  "wg(F,Y) == Union({X \<in> Pow(program). F:(X guarantees Y)})"
 
   (* Weakest existential property stronger than X *)
    wx :: "i =>i"
-   "wx(X) == Union({Y:Pow(program). Y<=X & ex_prop(Y)})"
+   "wx(X) == Union({Y \<in> Pow(program). Y<=X & ex_prop(Y)})"
 
   (*Ill-defined programs can arise through "Join"*)
   welldef :: i
-  "welldef == {F:program. Init(F) ~= 0}"
+  "welldef == {F \<in> program. Init(F) \<noteq> 0}"
   
-  refines :: [i, i, i] => o ("(3_ refines _ wrt _)" [10,10,10] 10)
+  refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
-   ALL H:program. (F ok H  & G ok H & F Join H:welldef Int X)
-    --> (G Join H:welldef Int X)"
+   \<forall>H \<in> program. (F ok H  & G ok H & F Join H \<in> welldef Int X)
+    --> (G Join H \<in> welldef Int X)"
+
+  iso_refines :: "[i,i, i] => o"  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
+  "G iso_refines F wrt X ==  F \<in> welldef Int X --> G \<in> welldef Int X"
+
+
+(*** existential properties ***)
+
+lemma ex_imp_subset_program: "ex_prop(X) ==> X\<subseteq>program"
+by (simp add: ex_prop_def)
+
+lemma ex1 [rule_format]: 
+ "GG \<in> Fin(program) 
+  ==> ex_prop(X) --> GG Int X\<noteq>0 --> OK(GG, (%G. G)) -->(\<Squnion>G \<in> GG. G) \<in> X"
+apply (unfold ex_prop_def)
+apply (erule Fin_induct)
+apply (simp_all add: OK_cons_iff)
+apply (safe elim!: not_emptyE, auto) 
+done
+
+lemma ex2 [rule_format]: 
+"X \<subseteq> program ==>  
+ (\<forall>GG \<in> Fin(program). GG Int X \<noteq> 0 --> OK(GG,(%G. G))-->(\<Squnion>G \<in> GG. G) \<in> X) 
+   --> ex_prop(X)"
+apply (unfold ex_prop_def, clarify)
+apply (drule_tac x = "{F,G}" in bspec)
+apply (simp_all add: OK_iff_ok)
+apply (auto intro: ok_sym)
+done
+
+(*Chandy & Sanders take this as a definition*)
+
+lemma ex_prop_finite:
+     "ex_prop(X) <-> (X\<subseteq>program &  
+  (\<forall>GG \<in> Fin(program). GG Int X \<noteq> 0 & OK(GG,(%G. G))-->(\<Squnion>G \<in> GG. G) \<in> X))"
+apply auto
+apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+
+done
+
+(* Equivalent definition of ex_prop given at the end of section 3*)
+lemma ex_prop_equiv: 
+"ex_prop(X) <->  
+  X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X <-> (\<forall>H \<in> program. (G component_of H) --> H \<in> X)))"
+apply (unfold ex_prop_def component_of_def, safe, force, force, blast) 
+apply (subst Join_commute)
+apply (blast intro: ok_sym) 
+done
+
+(*** universal properties ***)
+
+lemma uv_imp_subset_program: "uv_prop(X)==> X\<subseteq>program"
+apply (unfold uv_prop_def)
+apply (simp (no_asm_simp))
+done
+
+lemma uv1 [rule_format]: 
+     "GG \<in> Fin(program) ==>  
+      (uv_prop(X)--> GG \<subseteq> X & OK(GG, (%G. G)) --> (\<Squnion>G \<in> GG. G) \<in> X)"
+apply (unfold uv_prop_def)
+apply (erule Fin_induct)
+apply (auto simp add: OK_cons_iff)
+done
+
+lemma uv2 [rule_format]: 
+     "X\<subseteq>program  ==> 
+      (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) --> (\<Squnion>G \<in> GG. G) \<in> X)
+      --> uv_prop(X)"
+apply (unfold uv_prop_def, auto)
+apply (drule_tac x = 0 in bspec, simp+) 
+apply (drule_tac x = "{F,G}" in bspec, simp) 
+apply (force dest: ok_sym simp add: OK_iff_ok) 
+done
+
+(*Chandy & Sanders take this as a definition*)
+lemma uv_prop_finite: 
+"uv_prop(X) <-> X\<subseteq>program &  
+  (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) --> (\<Squnion>G \<in> GG. G) \<in>  X)"
+apply auto
+apply (blast dest: uv_imp_subset_program)
+apply (blast intro: uv1)
+apply (blast intro!: uv2 dest:)
+done
+
+(*** guarantees ***)
+lemma guaranteesI: 
+     "[| (!!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 (simp add: guar_def component_def)
+
+lemma guaranteesD: 
+     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X; G \<in> program |]  
+      ==> F Join G \<in> Y"
+by (simp add: guar_def component_def)
+
+
+(*This version of guaranteesD matches more easily in the conclusion
+  The major premise can no longer be  F\<subseteq>H since we need to reason about G*)
+
+lemma component_guaranteesD: 
+     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G; G \<in> program |]  
+      ==> H \<in> Y"
+by (simp add: guar_def, blast)
+
+lemma guarantees_weaken: 
+     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
+by (simp add: guar_def, auto)
+
+lemma subset_imp_guarantees_program:
+     "X \<subseteq> Y ==> X guarantees Y = program"
+by (unfold guar_def, blast)
+
+(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
+lemma subset_imp_guarantees:
+     "[| X \<subseteq> Y; F \<in> program |] ==> F \<in> X guarantees Y"
+by (unfold guar_def, blast)
+
+lemma component_of_Join1: "F ok G ==> F component_of (F Join G)"
+by (unfold component_of_def, blast)
+
+lemma component_of_Join2: "F ok G ==> G component_of (F Join G)"
+apply (subst Join_commute)
+apply (blast intro: ok_sym component_of_Join1)
+done
+
+(*Remark at end of section 4.1 *)
+lemma ex_prop_imp: 
+     "ex_prop(Y) ==> (Y = (program guarantees Y))"
+apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def)
+apply clarify
+apply (rule equalityI, blast, safe)
+apply (drule_tac x = x in bspec, assumption, force) 
+done
+
+lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)"
+apply (unfold guar_def)
+apply (simp (no_asm_simp) add: ex_prop_equiv)
+apply safe
+apply (blast intro: elim: equalityE) 
+apply (simp_all (no_asm_use) add: component_of_def)
+apply (force elim: equalityE)+
+done
+
+lemma ex_prop_equiv2: "(ex_prop(Y)) <-> (Y = program guarantees Y)"
+by (blast intro: ex_prop_imp guarantees_imp)
+
+(** Distributive laws.  Re-orient to perform miniscoping **)
+
+lemma guarantees_UN_left: 
+     "i \<in> I ==>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)"
+apply (unfold guar_def)
+apply (rule equalityI, safe)
+ prefer 2 apply force
+apply blast+
+done
+
+lemma guarantees_Un_left: 
+     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
+apply (unfold guar_def)
+apply (rule equalityI, safe, blast+)
+done
+
+lemma guarantees_INT_right: 
+     "i \<in> I ==> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))"
+apply (unfold guar_def)
+apply (rule equalityI, safe, blast+)
+done
+
+lemma guarantees_Int_right: 
+     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
+by (unfold guar_def, blast)
+
+lemma guarantees_Int_right_I:
+     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
+     ==> F \<in> Z guarantees (X Int Y)"
+by (simp (no_asm_simp) add: guarantees_Int_right)
+
+lemma guarantees_INT_right_iff:
+     "i \<in> I==> (F \<in> X guarantees (\<Inter>i \<in> I. Y(i))) <->  
+      (\<forall>i \<in> I. F \<in> X guarantees Y(i))"
+by (simp add: guarantees_INT_right INT_iff, blast)
+
+
+lemma shunting: "(X guarantees Y) = (program guarantees ((program-X) Un Y))"
+by (unfold guar_def, auto)
+
+lemma contrapositive:
+     "(X guarantees Y) = (program - Y) guarantees (program -X)"
+by (unfold guar_def, blast)
+
+(** The following two can be expressed using intersection and subset, which
+    is more faithful to the text but looks cryptic.
+**)
+
+lemma combining1: 
+    "[| F \<in> V guarantees X;  F \<in> (X Int Y) guarantees Z |] 
+     ==> F \<in> (V Int Y) guarantees Z"
+by (unfold guar_def, blast)
+
+lemma combining2: 
+    "[| F \<in> V guarantees (X Un Y);  F \<in> Y guarantees Z |] 
+     ==> F \<in> V guarantees (X Un Z)"
+by (unfold guar_def, blast)
+
+
+(** The following two follow Chandy-Sanders, but the use of object-quantifiers
+    does not suit Isabelle... **)
+
+(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
+lemma all_guarantees: 
+     "[| \<forall>i \<in> I. F \<in> X guarantees Y(i); i \<in> I |]  
+    ==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))"
+by (unfold guar_def, blast)
+
+(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
+lemma ex_guarantees: 
+     "\<exists>i \<in> I. F \<in> X guarantees Y(i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y(i))"
+by (unfold guar_def, blast)
+
+
+(*** Additional guarantees laws, by lcp ***)
 
-  iso_refines :: [i,i, i] => o  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
-  "G iso_refines F wrt X ==  F:welldef Int X --> G:welldef Int X"
+lemma guarantees_Join_Int: 
+    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
+     ==> F Join G: (U Int X) guarantees (V Int Y)"
+
+apply (unfold guar_def)
+apply (simp (no_asm))
+apply safe
+apply (simp add: Join_assoc)
+apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (simp add: ok_commute)
+apply (simp (no_asm_simp) add: Join_ac)
+done
+
+lemma guarantees_Join_Un: 
+    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
+     ==> F Join G: (U Un X) guarantees (V Un Y)"
+apply (unfold guar_def)
+apply (simp (no_asm))
+apply safe
+apply (simp add: Join_assoc)
+apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (rotate_tac 4)
+apply (drule_tac x = "F Join Ga" in bspec)
+apply (simp (no_asm))
+apply (force simp add: ok_commute)
+apply (simp (no_asm_simp) add: Join_ac)
+done
+
+lemma guarantees_JN_INT: 
+     "[| \<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))"
+apply (unfold guar_def, safe)
+ prefer 2 apply blast
+apply (drule_tac x = xa in bspec)
+apply (simp_all add: INT_iff, safe)
+apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) Join G" and A=program in bspec)
+apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+done
+
+lemma guarantees_JN_UN: 
+    "[| \<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))"
+apply (unfold guar_def, auto)
+apply (drule_tac x = y in bspec, simp_all, safe)
+apply (rename_tac G y)
+apply (drule_tac x = "JOIN (I-{y}, F) Join G" and A=program in bspec)
+apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
+done
+
+(*** guarantees laws for breaking down the program, by lcp ***)
+
+lemma guarantees_Join_I1: 
+     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
+apply (simp add: guar_def, safe)
+apply (simp add: Join_assoc)
+done
+
+lemma guarantees_Join_I2:
+     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
+apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
+apply (blast intro: guarantees_Join_I1)
+done
+
+lemma guarantees_JN_I: 
+     "[| i \<in> I; F(i) \<in>  X guarantees Y;  OK(I,F) |]  
+      ==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y"
+apply (unfold guar_def, safe)
+apply (drule_tac x = "JOIN (I-{i},F) Join G" in bspec)
+apply (simp (no_asm))
+apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
+done
+
+(*** well-definedness ***)
+
+lemma Join_welldef_D1: "F Join G \<in> welldef ==> programify(F) \<in>  welldef"
+by (unfold welldef_def, auto)
+
+lemma Join_welldef_D2: "F Join G \<in> welldef ==> programify(G) \<in>  welldef"
+by (unfold welldef_def, auto)
+
+(*** refinement ***)
+
+lemma refines_refl: "F refines F wrt X"
+by (unfold refines_def, blast)
+
+(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
+
+lemma wg_type: "wg(F, X) \<subseteq> program"
+by (unfold wg_def, auto)
+
+lemma guarantees_type: "X guarantees Y \<subseteq> program"
+by (unfold guar_def, auto)
+
+lemma wgD2: "G \<in> wg(F, X) ==> G \<in> program & F \<in> program"
+apply (unfold wg_def, auto)
+apply (blast dest: guarantees_type [THEN subsetD])
+done
+
+lemma guarantees_equiv: 
+"(F \<in> X guarantees Y) <->  
+   F \<in> program & (\<forall>H \<in> program. H \<in> X --> (F component_of H --> H \<in> Y))"
+by (unfold guar_def component_of_def, force) 
+
+lemma wg_weakest:
+     "!!X. [| F \<in> (X guarantees Y); X \<subseteq> program |] ==> X \<subseteq> wg(F,Y)"
+by (unfold wg_def, auto)
+
+lemma wg_guarantees: "F \<in> program ==> F \<in> wg(F,Y) guarantees Y"
+by (unfold wg_def guar_def, blast)
+
+lemma wg_equiv:
+     "H \<in> wg(F,X) <-> 
+      ((F component_of H --> H \<in> X) & F \<in> program & H \<in> program)"
+apply (simp add: wg_def guarantees_equiv)
+apply (rule iffI, safe)
+apply (rule_tac [4] x = "{H}" in bexI)
+apply (rule_tac [3] x = "{H}" in bexI, blast+)
+done
+
+lemma component_of_wg: 
+    "F component_of H ==> H \<in> wg(F,X) <-> (H \<in> X & F \<in> program & H \<in> program)"
+by (simp (no_asm_simp) add: wg_equiv)
+
+lemma wg_finite [rule_format]: 
+"\<forall>FF \<in> Fin(program). FF Int X \<noteq> 0 --> OK(FF, %F. F)  
+   --> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in>  wg(F,X)) <-> ((\<Squnion>F \<in> FF. F) \<in> X))"
+apply clarify
+apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
+apply (drule_tac X = X in component_of_wg)
+apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])
+apply (simp_all add: component_of_def)
+apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
+apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
+done
+
+lemma wg_ex_prop:
+     "ex_prop(X) ==> (F \<in> X) <-> (\<forall>H \<in> program. H \<in> wg(F,X) & F \<in> program)"
+apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
+apply blast
+done
+
+(** From Charpentier and Chandy "Theorems About Composition" **)
+(* Proposition 2 *)
+lemma wx_subset: "wx(X)\<subseteq>X"
+by (unfold wx_def, auto)
+
+lemma wx_ex_prop: "ex_prop(wx(X))"
+apply (simp (no_asm_use) add: ex_prop_def wx_def)
+apply safe
+apply blast
+apply (rule_tac x=x in bexI, force, simp)+
+done
+
+lemma wx_weakest: "\<forall>Z. Z\<subseteq>program --> Z\<subseteq> X --> ex_prop(Z) --> Z \<subseteq> wx(X)"
+by (unfold wx_def, auto)
+
+(* Proposition 6 *)
+lemma wx'_ex_prop: 
+ "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X})"
+apply (unfold ex_prop_def, safe)
+ apply (drule_tac x = "G Join Ga" in bspec)
+  apply (simp (no_asm))
+ apply (force simp add: Join_assoc)
+apply (drule_tac x = "F Join Ga" in bspec)
+ apply (simp (no_asm))
+apply (simp (no_asm_use))
+apply safe
+ apply (simp (no_asm_simp) add: ok_commute)
+apply (subgoal_tac "F Join G = G Join F")
+ apply (simp (no_asm_simp) add: Join_assoc)
+apply (simp (no_asm) add: Join_commute)
+done
+
+(* Equivalence with the other definition of wx *)
+
+lemma wx_equiv: 
+     "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G --> (F Join G) \<in> X}"
+apply (unfold wx_def)
+apply (rule equalityI, safe, blast)
+ apply (simp (no_asm_use) add: ex_prop_def)
+apply blast 
+apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X}" 
+         in UnionI, 
+       safe)
+apply (rule_tac [2] wx'_ex_prop)
+apply (drule_tac x=SKIP in bspec, simp)+
+apply auto 
+done
+
+(* Propositions 7 to 11 are all about this second definition of wx. And
+   by equivalence between the two definition, they are the same as the ones proved *)
+
+
+(* Proposition 12 *)
+(* Main result of the paper *)
+lemma guarantees_wx_eq: "(X guarantees Y) = wx((program-X) Un Y)"
+by (auto simp add: guar_def wx_equiv)
+
+(* 
+{* Corollary, but this result has already been proved elsewhere *}
+ "ex_prop(X guarantees Y)"
+*)
+
+(* Rules given in section 7 of Chandy and Sander's
+    Reasoning About Program composition paper *)
+
+lemma stable_guarantees_Always:
+     "[| Init(F) \<subseteq> A; F \<in> program |] ==> F \<in> stable(A) guarantees Always(A)"
+apply (rule guaranteesI)
+ prefer 2 apply assumption
+apply (simp (no_asm) add: Join_commute)
+apply (rule stable_Join_Always1)
+apply (simp_all add: invariant_def)
+apply (auto simp add: programify_def initially_def)
+done
+
+lemma constrains_guarantees_leadsTo:
+     "[| F \<in> transient(A); st_set(B) |] 
+      ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
+apply (rule guaranteesI)
+ prefer 2 apply (blast dest: transient_type [THEN subsetD])
+apply (rule leadsTo_Basis')
+  apply (blast intro: constrains_weaken_R) 
+ apply (blast intro!: Join_transient_I1, blast)
+done
 
 end
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Increasing.ML
--- a/src/ZF/UNITY/Increasing.ML	Tue Jul 08 11:44:30 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-(*  Title:      ZF/UNITY/GenIncreasing
-    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
-
-A general form of the `Increasing' relation of Charpentier
-*)
-
-(** increasing **)
-
-Goalw [increasing_def] "increasing[A](r, f) <= program";
-by (Blast_tac 1);
-qed "increasing_type";
-
-Goalw [increasing_def] "F \\<in> increasing[A](r, f) ==> F \\<in> program";
-by (Blast_tac 1);
-qed "increasing_into_program";
-
-Goalw [increasing_def]
-"[| 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 \\<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 \\<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";
-Addsimps [increasing_constant];
-
-Goalw [increasing_def, stable_def, part_order_def, 
-       constrains_def, mono1_def, metacomp_def]
-"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==> \
-\  increasing[A](r, f) <= increasing[B](s, g comp f)";
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 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);
-by (rotate_tac 5 1);
-by (dres_inst_tac [("x", "f(xb)")] bspec 1);
-by (rotate_tac ~1 2);
-by (dres_inst_tac [("x", "act")] bspec 2);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
-by (Blast_tac 1);
-by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
-by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
-by (ALLGOALS(Asm_simp_tac));
-qed "subset_increasing_comp";
-
-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";
-
-Goalw [increasing_def, Lt_def]
-   "increasing[nat](Le, f) <= increasing[nat](Lt, f)";
-by Auto_tac;
-qed "strict_increasing";
-
-Goalw [increasing_def, Gt_def, Ge_def]
-   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)";
-by Auto_tac;
-by (etac natE 1);
-by (auto_tac (claset(), simpset() addsimps [stable_def]));
-qed "strict_gt_increasing";
-
-(** Increasing **)
-
-Goalw [increasing_def, Increasing_def]
-     "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";
-
-Goalw [Increasing_def] "Increasing[A](r, f) <= program";
-by Auto_tac;
-qed "Increasing_type";
-
-Goalw [Increasing_def] "F \\<in> Increasing[A](r, f) ==> F \\<in> program";
-by Auto_tac;
-qed "Increasing_into_program";
-
-Goalw [Increasing_def]
-"[| 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 \\<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 \\<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()));
-qed "Increasing_constant";
-Addsimps [Increasing_constant];
-
-Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def, 
-       constrains_def, mono1_def, metacomp_def]
-"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
-\  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 \\<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);
-by (rotate_tac 5 1);
-by (dres_inst_tac [("x", "f(xb)")] bspec 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Clarify_tac 1);
-by (rotate_tac ~2 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Blast_tac 1);
-by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
-by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
-by (ALLGOALS(Asm_full_simp_tac));
-qed "subset_Increasing_comp";
-
-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";
-  
-Goalw [Increasing_def, Lt_def]
-"Increasing[nat](Le, f) <= Increasing[nat](Lt, f)";
-by Auto_tac;
-qed "strict_Increasing";
-
-Goalw [Increasing_def, Ge_def, Gt_def] 
-"Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)";
-by Auto_tac;
-by (etac natE 1);
-by (auto_tac (claset(), simpset() addsimps [Stable_def]));
-qed "strict_gt_Increasing";
-
-(** Two-place monotone operations **)
-
-Goalw [increasing_def, stable_def, 
-       part_order_def, constrains_def, mono2_def]
-"[| 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 \\<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 \\<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);
-by (rotate_tac 6 1);
-by (dres_inst_tac [("x", "f(xb)")] bspec 1);
-by (rotate_tac 1 2);
-by (dres_inst_tac [("x", "g(xb)")] bspec 2);
-by (ALLGOALS(Asm_simp_tac));
-by (rotate_tac ~1 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by (rotate_tac ~3 2);
-by (dres_inst_tac [("x", "act")] bspec 2);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
-by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (rotate_tac ~4 1);
-by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
-by (rotate_tac ~1 3);
-by (dres_inst_tac [("x", "g(xa)"), ("x1", "g(xb)")] (bspec RS bspec) 3);
-by (ALLGOALS(Asm_full_simp_tac));
-by (res_inst_tac [("b", "h(f(xb), g(xb))"), ("A", "C")] trans_onD 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed "imp_increasing_comp2";
-
-Goalw [Increasing_def, stable_def, 
-       part_order_def, constrains_def, mono2_def, Stable_def, Constrains_def]
-"[| 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 \\<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 \\<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);
-by (rotate_tac 6 1);
-by (dres_inst_tac [("x", "f(xa)")] bspec 1);
-by (rotate_tac 1 2);
-by (dres_inst_tac [("x", "g(xa)")] bspec 2);
-by (ALLGOALS(Asm_simp_tac));
-by (Clarify_tac 1);
-by (rotate_tac ~2 1);
-by (dres_inst_tac [("x", "act")] bspec 1);
-by (rotate_tac ~3 2);
-by (dres_inst_tac [("x", "act")] bspec 2);
-by (ALLGOALS(Asm_full_simp_tac));
-by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 1);
-by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 2);
-by (Blast_tac 1);
-by (Blast_tac 1);
-by (rotate_tac ~9 1);
-by (dres_inst_tac [("x", "f(x)"), ("x1", "f(xa)")] (bspec RS bspec) 1);
-by (rotate_tac ~1 3);
-by (dres_inst_tac [("x", "g(x)"), ("x1", "g(xa)")] (bspec RS bspec) 3);
-by (ALLGOALS(Asm_full_simp_tac));
-by (res_inst_tac [("b", "h(f(xa), g(xa))"), ("A", "C")] trans_onD 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed "imp_Increasing_comp2";
-
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Increasing.thy
--- a/src/ZF/UNITY/Increasing.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Increasing.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -1,32 +1,231 @@
 (*  Title:      ZF/UNITY/Increasing
-    ID:         $Id$
+    ID:         $Id \<in> Increasing.thy,v 1.2 2003/06/02 09:17:52 paulson Exp $
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2001  University of Cambridge
 
-The "Increasing" relation of Charpentier.
-
 Increasing's parameters are a state function f, a domain A and an order
 relation r over the domain A. 
 *)
 
-Increasing = Constrains + Monotonicity +
+header{*Charpentier's "Increasing" Relation*}
+
+theory Increasing = Constrains + Monotonicity:
+
 constdefs
 
-  increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')")
+  increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')")
   "increasing[A](r, f) ==
-    {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) &
-                (ALL x:state. f(x):A)}"
+    {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) &
+                (\<forall>x \<in> state. f(x):A)}"
   
-  Increasing :: [i, i, i=>i] => i ("Increasing[_]'(_, _')")
+  Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')")
   "Increasing[A](r, f) ==
-    {F:program. (ALL k:A. F:Stable({s:state. <k, f(s)>:r})) &
-                (ALL x:state. f(x):A)}"
+    {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
+                (\<forall>x \<in> state. f(x):A)}"
 
 syntax
-  IncWrt      ::  [i=>i, i, i] => i ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
+  IncWrt ::  "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
 
 translations
   "IncWrt(f,r,A)" => "Increasing[A](r,f)"
 
+
+(** increasing **)
+
+lemma increasing_type: "increasing[A](r, f) <= program"
+by (unfold increasing_def, blast)
+
+lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program"
+by (unfold increasing_def, blast)
+
+lemma increasing_imp_stable: 
+"[| F \<in> increasing[A](r, f); x \<in> A |] ==>F \<in> stable({s \<in> state. <x, f(s)>:r})"
+by (unfold increasing_def, blast)
+
+lemma increasingD: 
+"F \<in> increasing[A](r,f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)"
+apply (unfold increasing_def)
+apply (subgoal_tac "\<exists>x. x \<in> state")
+apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
+done
+
+lemma increasing_constant [simp]: 
+ "F \<in> increasing[A](r, %s. c) <-> F \<in> program & c \<in> A"
+apply (unfold increasing_def stable_def)
+apply (subgoal_tac "\<exists>x. x \<in> state")
+apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
+done
+
+lemma subset_increasing_comp: 
+"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==>  
+   increasing[A](r, f) <= increasing[B](s, g comp f)"
+apply (unfold increasing_def stable_def part_order_def 
+       constrains_def mono1_def metacomp_def, clarify, simp)
+apply clarify
+apply (subgoal_tac "xa \<in> state")
+prefer 2 apply (blast dest!: ActsD)
+apply (subgoal_tac "<f (xb), f (xb) >:r")
+prefer 2 apply (force simp add: refl_def)
+apply (rotate_tac 5)
+apply (drule_tac x = "f (xb) " in bspec)
+apply (rotate_tac [2] -1)
+apply (drule_tac [2] x = act in bspec, simp_all)
+apply (drule_tac A = "act``?u" and c = xa in subsetD, blast)
+apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
+apply simp_all
+done
+
+lemma imp_increasing_comp:
+     "[| 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 (rule subset_increasing_comp [THEN subsetD], auto)
+
+lemma strict_increasing: 
+   "increasing[nat](Le, f) <= increasing[nat](Lt, f)"
+by (unfold increasing_def Lt_def, auto)
+
+lemma strict_gt_increasing: 
+   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)"
+apply (unfold increasing_def Gt_def Ge_def, auto)
+apply (erule natE)
+apply (auto simp add: stable_def)
+done
+
+(** Increasing **)
+
+lemma increasing_imp_Increasing: 
+     "F \<in> increasing[A](r, f) ==> F \<in> Increasing[A](r, f)"
+
+apply (unfold increasing_def Increasing_def)
+apply (auto intro: stable_imp_Stable)
+done
+
+lemma Increasing_type: "Increasing[A](r, f) <= program"
+by (unfold Increasing_def, auto)
+
+lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program"
+by (unfold Increasing_def, auto)
+
+lemma Increasing_imp_Stable: 
+"[| F \<in> Increasing[A](r, f); a \<in> A |] ==> F \<in> Stable({s \<in> state. <a,f(s)>:r})"
+by (unfold Increasing_def, blast)
+
+lemma IncreasingD: 
+"F \<in> Increasing[A](r, f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)"
+apply (unfold Increasing_def)
+apply (subgoal_tac "\<exists>x. x \<in> state")
+apply (auto intro: st0_in_state)
+done
+
+lemma Increasing_constant [simp]: 
+     "F \<in> Increasing[A](r, %s. c) <-> F \<in> program & (c \<in> A)"
+apply (subgoal_tac "\<exists>x. x \<in> state")
+apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing)
+done
+
+lemma subset_Increasing_comp: 
+"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==>  
+   Increasing[A](r, f) <= Increasing[B](s, g comp f)"
+apply (unfold Increasing_def Stable_def Constrains_def part_order_def 
+       constrains_def mono1_def metacomp_def, safe)
+apply (simp_all add: ActsD)
+apply (subgoal_tac "xb \<in> state & xa \<in> state")
+ prefer 2 apply (simp add: ActsD)
+apply (subgoal_tac "<f (xb), f (xb) >:r")
+prefer 2 apply (force simp add: refl_def)
+apply (rotate_tac 5)
+apply (drule_tac x = "f (xb) " in bspec)
+apply simp_all
+apply clarify
+apply (rotate_tac -2)
+apply (drule_tac x = act in bspec)
+apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast)
+apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
+apply simp_all
+done
+
+lemma imp_Increasing_comp:
+ "[| 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)"
+apply (rule subset_Increasing_comp [THEN subsetD], auto)
+done
+  
+lemma strict_Increasing: "Increasing[nat](Le, f) <= Increasing[nat](Lt, f)"
+by (unfold Increasing_def Lt_def, auto)
+
+lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)"
+apply (unfold Increasing_def Ge_def Gt_def, auto)
+apply (erule natE)
+apply (auto simp add: Stable_def)
+done
+
+(** Two-place monotone operations **)
+
+lemma imp_increasing_comp2: 
+"[| 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 \<in> increasing[C](t, %x. h(f(x), g(x)))"
+apply (unfold increasing_def stable_def 
+       part_order_def constrains_def mono2_def, clarify, simp)
+apply clarify
+apply (rename_tac xa xb)
+apply (subgoal_tac "xb \<in> state & xa \<in> state")
+ prefer 2 apply (blast dest!: ActsD)
+apply (subgoal_tac "<f (xb), f (xb) >:r & <g (xb), g (xb) >:s")
+prefer 2 apply (force simp add: refl_def)
+apply (rotate_tac 6)
+apply (drule_tac x = "f (xb) " in bspec)
+apply (rotate_tac [2] 1)
+apply (drule_tac [2] x = "g (xb) " in bspec)
+apply simp_all
+apply (rotate_tac -1)
+apply (drule_tac x = act in bspec)
+apply (rotate_tac [2] -3)
+apply (drule_tac [2] x = act in bspec, simp_all)
+apply (drule_tac A = "act``?u" and c = xa in subsetD)
+apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast)
+apply (rotate_tac -4)
+apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (rotate_tac [3] -1)
+apply (drule_tac [3] x = "g (xa) " and x1 = "g (xb) " in bspec [THEN bspec])
+apply simp_all
+apply (rule_tac b = "h (f (xb), g (xb))" and A = C in trans_onD)
+apply simp_all
+done
+
+lemma imp_Increasing_comp2: 
+"[| 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 \<in> Increasing[C](t, %x. h(f(x), g(x)))"
+apply (unfold Increasing_def stable_def 
+       part_order_def constrains_def mono2_def Stable_def Constrains_def, safe)
+apply (simp_all add: ActsD)
+apply (subgoal_tac "xa \<in> state & x \<in> state")
+prefer 2 apply (blast dest!: ActsD)
+apply (subgoal_tac "<f (xa), f (xa) >:r & <g (xa), g (xa) >:s")
+prefer 2 apply (force simp add: refl_def)
+apply (rotate_tac 6)
+apply (drule_tac x = "f (xa) " in bspec)
+apply (rotate_tac [2] 1)
+apply (drule_tac [2] x = "g (xa) " in bspec)
+apply simp_all
+apply clarify
+apply (rotate_tac -2)
+apply (drule_tac x = act in bspec)
+apply (rotate_tac [2] -3)
+apply (drule_tac [2] x = act in bspec, simp_all)
+apply (drule_tac A = "act``?u" and c = x in subsetD)
+apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast)
+apply (rotate_tac -9)
+apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
+apply (rotate_tac [3] -1)
+apply (drule_tac [3] x = "g (x) " and x1 = "g (xa) " in bspec [THEN bspec])
+apply simp_all
+apply (rule_tac b = "h (f (xa), g (xa))" and A = C in trans_onD)
+apply simp_all
+done
+
   
 end
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Monotonicity.ML
--- a/src/ZF/UNITY/Monotonicity.ML	Tue Jul 08 11:44:30 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(*  Title:      ZF/UNITY/Monotonicity.ML
-    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
-
-Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
-*)
-
-
-(*TOO SLOW as a default simprule????
-Addsimps [append_left_is_Nil_iff,append_left_is_Nil_iff2];
-*)
-
-Goalw [mono1_def]
-  "[| 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 \\<in> A; y \\<in> A; u \\<in> B; v \\<in> B |] ==> \
-\  <f(x, u), f(y,v)>:t";
-by Auto_tac;
-qed "mono2D";
-
-
-(** Monotonicity of take **)
-
-(*????premises too strong*)
-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);
-by (Asm_simp_tac 1);
-by (dtac not_lt_imp_le 1);
-by Auto_tac;
-by (case_tac "length(xs) le j" 1);
-by (auto_tac (claset(), simpset() addsimps [take_prefix]));
-by (dtac not_lt_imp_le 1);
-by Auto_tac;
-by (dres_inst_tac [("m", "i")] less_imp_succ_add 1);
-by Auto_tac;
-by (subgoal_tac "i #+ k le length(xs)" 1);
-by (blast_tac (claset() addIs [leI]) 2);
-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 \\<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 \\<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()));
-qed "take_mono";
-
-Goalw [mono2_def, Le_def] "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)";
-by Auto_tac;
-by (blast_tac (claset() addIs [take_mono]) 1);
-qed "mono_take";
-Addsimps [mono_take];
-AddIs [mono_take];
-
-(** Monotonicity of length **)
-
-bind_thm("length_mono", prefix_length_le);
-
-Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le, length)";
-by (auto_tac (claset() addDs [prefix_length_le],
-             simpset() addsimps [Le_def]));
-qed "mono_length";
-Addsimps [mono_length];
-AddIs [mono_length];
-
-(** Monotonicity of Un **)
-
-Goalw [mono2_def, SetLe_def]  
- "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)";
-by Auto_tac;
-qed "mono_Un";
-Addsimps [mono_Un];
-AddIs [mono_Un];
-
-(* Monotonicity of multiset union *)
-
-Goalw [mono2_def, MultLe_def]  
-   "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-by (REPEAT(blast_tac (claset() addIs [munion_multirel_mono,
-                                munion_multirel_mono1,
-                                munion_multirel_mono2,
-                                multiset_into_Mult]) 1));
-qed "mono_munion";
-Addsimps [mono_munion];
-AddIs [mono_munion];
-
-Goalw [mono1_def, Le_def] "mono1(nat, Le, nat, Le, succ)";
-by Auto_tac;
-qed "mono_succ";
-Addsimps [mono_succ];
-AddIs [mono_succ];
-
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Monotonicity.thy
--- a/src/ZF/UNITY/Monotonicity.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Monotonicity.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -1,30 +1,133 @@
 (*  Title:      ZF/UNITY/Monotonicity.thy
-    ID:         $Id$
+    ID:         $Id \<in> Monotonicity.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2002  University of Cambridge
 
 Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
 *)
 
-Monotonicity =  GenPrefix  +  MultisetSum +
+header{*Monotonicity of an Operator WRT a Relation*}
+
+theory Monotonicity = GenPrefix + MultisetSum:
+
 constdefs
-mono1 :: [i, i, i, i, i=>i] => o
-"mono1(A, r, B, s, f) ==
- (ALL x:A. ALL y:A. <x, y>:r --> <f(x), f(y)>:s) & (ALL x:A. f(x):B)"
+
+  mono1 :: "[i, i, i, i, i=>i] => o"
+  "mono1(A, r, B, s, f) ==
+    (\<forall>x \<in> A. \<forall>y \<in> A. <x,y> \<in> r --> <f(x), f(y)> \<in> s) & (\<forall>x \<in> A. f(x) \<in> B)"
 
   (* monotonicity of a 2-place meta-function f *)
 
-  mono2 :: [i, i, i, i, i, i, [i,i]=>i] => o
-  "mono2(A, r, B, s, C, t, f) == (ALL x:A. ALL y:A. ALL u:B. ALL v:B.
-    <x, y>:r & <u,v>:s --> <f(x, u), f(y,v)>:t) &
-    (ALL x:A. ALL y:B. f(x,y):C)"
+  mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o"
+  "mono2(A, r, B, s, C, t, f) == 
+    (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
+              <x,y> \<in> r & <u,v> \<in> s --> <f(x,u), f(y,v)> \<in> t) &
+    (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
 
  (* Internalized relations on sets and multisets *)
 
-  SetLe :: i =>i
-  "SetLe(A) == {<x, y>:Pow(A)*Pow(A). x <= y}"
+  SetLe :: "i =>i"
+  "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x <= y}"
 
-  MultLe :: [i,i] =>i
+  MultLe :: "[i,i] =>i"
   "MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
 
+
+
+lemma mono1D: 
+  "[| mono1(A, r, B, s, f); <x, y> \<in> r; x \<in> A; y \<in> A |] ==> <f(x), f(y)> \<in> s"
+by (unfold mono1_def, auto)
+
+lemma mono2D: 
+     "[| mono2(A, r, B, s, C, t, f);  
+         <x, y> \<in> r; <u,v> \<in> s; x \<in> A; y \<in> A; u \<in> B; v \<in> B |] 
+      ==> <f(x, u), f(y,v)> \<in> t"
+by (unfold mono2_def, auto)
+
+
+(** Monotonicity of take **)
+
+lemma take_mono_left_lemma:
+     "[| i le j; xs \<in> list(A); i \<in> nat; j \<in> nat |] 
+      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
+apply (case_tac "length (xs) le i")
+ apply (subgoal_tac "length (xs) le j")
+  apply (simp)
+ apply (blast intro: le_trans)
+apply (drule not_lt_imp_le, auto)
+apply (case_tac "length (xs) le j")
+ apply (auto simp add: take_prefix)
+apply (drule not_lt_imp_le, auto)
+apply (drule_tac m = i in less_imp_succ_add, auto)
+apply (subgoal_tac "i #+ k le length (xs) ")
+ apply (simp add: take_add prefix_iff take_type drop_type)
+apply (blast intro: leI)
+done
+
+lemma take_mono_left:
+     "[| i le j; xs \<in> list(A); j \<in> nat |]
+      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
+by (blast intro: Nat.le_in_nat take_mono_left_lemma) 
+
+lemma take_mono_right:
+     "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 
+      ==> <take(i, xs), take(i, ys)> \<in> prefix(A)"
+by (auto simp add: prefix_iff)
+
+lemma take_mono:
+     "[| i le j; <xs, ys> \<in> prefix(A); j \<in> nat |]
+      ==> <take(i, xs), take(j, ys)> \<in> prefix(A)"
+apply (rule_tac b = "take (j, xs) " in prefix_trans)
+apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
+done
+
+lemma mono_take [iff]:
+     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
+apply (unfold mono2_def Le_def, auto)
+apply (blast intro: take_mono)
+done
+
+(** Monotonicity of length **)
+
+lemmas length_mono = prefix_length_le
+
+lemma mono_length [iff]:
+     "mono1(list(A), prefix(A), nat, Le, length)"
+apply (unfold mono1_def)
+apply (auto dest: prefix_length_le simp add: Le_def)
+done
+
+(** Monotonicity of Un **)
+
+lemma mono_Un [iff]: 
+     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)"
+by (unfold mono2_def SetLe_def, auto)
+
+(* Monotonicity of multiset union *)
+
+lemma mono_munion [iff]: 
+     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
+apply (unfold mono2_def MultLe_def)
+apply (auto simp add: Mult_iff_multiset)
+apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
+done
+
+lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
+by (unfold mono1_def Le_def, auto)
+
+ML{*
+val mono1D = thm "mono1D";
+val mono2D = thm "mono2D";
+val take_mono_left_lemma = thm "take_mono_left_lemma";
+val take_mono_left = thm "take_mono_left";
+val take_mono_right = thm "take_mono_right";
+val take_mono = thm "take_mono";
+val mono_take = thm "mono_take";
+val length_mono = thm "length_mono";
+val mono_length = thm "mono_length";
+val mono_Un = thm "mono_Un";
+val mono_munion = thm "mono_munion";
+val mono_succ = thm "mono_succ";
+*}
+
 end
\ No newline at end of file
diff -r 68da54626309 -r 24382760fd89 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Tue Jul 08 11:44:30 2003 +0200
+++ b/src/ZF/UNITY/Union.thy	Wed Jul 09 11:39:34 2003 +0200
@@ -460,6 +460,17 @@
 by (auto simp add: OK_iff_ok)
 
 
+lemma OK_0 [iff]: "OK(0,F)"
+by (simp add: OK_def)
+
+lemma OK_cons_iff:
+     "OK(cons(i, I), F) <->  
+      (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
+apply (simp add: OK_iff_ok)
+apply (blast intro: ok_sym) 
+done
+
+
 subsection{*Allowed*}
 
 lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"