converting more theories to Isar scripts, and tidying
authorpaulson
Wed Jul 09 11:39:34 2003 +0200 (2003-07-09)
changeset 1409324382760fd89
parent 14092 68da54626309
child 14094 33147ecac5f9
converting more theories to Isar scripts, and tidying
src/ZF/IsaMakefile
src/ZF/UNITY/Comp.ML
src/ZF/UNITY/Comp.thy
src/ZF/UNITY/Follows.ML
src/ZF/UNITY/Follows.thy
src/ZF/UNITY/Guar.ML
src/ZF/UNITY/Guar.thy
src/ZF/UNITY/Increasing.ML
src/ZF/UNITY/Increasing.thy
src/ZF/UNITY/Monotonicity.ML
src/ZF/UNITY/Monotonicity.thy
src/ZF/UNITY/Union.thy
     1.1 --- a/src/ZF/IsaMakefile	Tue Jul 08 11:44:30 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Jul 09 11:39:34 2003 +0200
     1.3 @@ -115,15 +115,14 @@
     1.4  ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
     1.5  
     1.6  $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
     1.7 -  UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
     1.8 -  UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
     1.9 +  UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
    1.10 +  UNITY/FP.thy UNITY/Guar.thy \
    1.11    UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.thy \
    1.12    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \
    1.13    UNITY/AllocBase.thy UNITY/AllocImpl.thy\
    1.14    UNITY/ClientImpl.thy UNITY/Distributor.thy\
    1.15 -  UNITY/Follows.ML UNITY/Follows.thy\
    1.16 -  UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
    1.17 -  UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
    1.18 +  UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\
    1.19 +  UNITY/Monotonicity.thy\
    1.20    UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
    1.21    UNITY/WFair.ML UNITY/WFair.thy
    1.22  	@$(ISATOOL) usedir $(OUT)/ZF UNITY
     2.1 --- a/src/ZF/UNITY/Comp.ML	Tue Jul 08 11:44:30 2003 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,348 +0,0 @@
     2.4 -(*  Title:      ZF/UNITY/Comp.ML
     2.5 -    ID:         $Id \\<in> Comp.ML,v 1.8 2003/06/27 16:40:25 paulson Exp $
     2.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     2.7 -    Copyright   1998  University of Cambridge
     2.8 -Composition
     2.9 -From Chandy and Sanders, "Reasoning About Program Composition"
    2.10 -
    2.11 -Revised by Sidi Ehmety on January 2001
    2.12 -
    2.13 -*)
    2.14 -
    2.15 -(*** component and strict_component relations ***)
    2.16 -
    2.17 -Goalw [component_def]
    2.18 -     "H component F | H component G ==> H component (F Join G)";
    2.19 -by Auto_tac;
    2.20 -by (res_inst_tac [("x", "Ga Join G")] exI 1);
    2.21 -by (res_inst_tac [("x", "G Join F")] exI 2);
    2.22 -by (auto_tac (claset(), simpset() addsimps Join_ac));
    2.23 -qed "componentI";
    2.24 -
    2.25 -Goalw [component_def]
    2.26 -     "G \\<in> program ==> (F component G) <-> \
    2.27 -\  (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))";
    2.28 -by Auto_tac;
    2.29 -by (rtac exI 1);
    2.30 -by (rtac program_equalityI 1);
    2.31 -by Auto_tac;
    2.32 -qed "component_eq_subset";
    2.33 -
    2.34 -Goalw [component_def] 
    2.35 -   "F \\<in> program ==> SKIP component F";
    2.36 -by (res_inst_tac [("x", "F")] exI 1);
    2.37 -by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    2.38 -qed "component_SKIP";
    2.39 -
    2.40 -Goalw [component_def] 
    2.41 -"F \\<in> program ==> F component F";
    2.42 -by (res_inst_tac  [("x", "F")] exI 1);
    2.43 -by (force_tac (claset() addIs [Join_SKIP_right], simpset()) 1);
    2.44 -qed "component_refl";
    2.45 -
    2.46 -Addsimps [component_SKIP, component_refl];
    2.47 -
    2.48 -Goal "F component SKIP ==> programify(F) = SKIP";
    2.49 -by (rtac program_equalityI 1);
    2.50 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_eq_subset])));
    2.51 -by (Blast_tac 1);
    2.52 -qed "SKIP_minimal";
    2.53 -
    2.54 -Goalw [component_def] "F component (F Join G)";
    2.55 -by (Blast_tac 1);
    2.56 -qed "component_Join1";
    2.57 -
    2.58 -Goalw [component_def] "G component (F Join G)";
    2.59 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
    2.60 -by (Blast_tac 1);
    2.61 -qed "component_Join2";
    2.62 -
    2.63 -Goal "F component G ==> F Join G = G";
    2.64 -by (auto_tac (claset(), simpset() 
    2.65 -        addsimps [component_def, Join_left_absorb]));
    2.66 -qed "Join_absorb1";
    2.67 -
    2.68 -Goal "G component F ==> F Join G = F";
    2.69 -by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
    2.70 -qed "Join_absorb2";
    2.71 -
    2.72 -Goal "H \\<in> program==>(JOIN(I,F) component H) <-> (\\<forall>i \\<in> I. F(i) component H)";
    2.73 -by (case_tac "I=0" 1);
    2.74 -by (Force_tac 1);
    2.75 -by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.76 -by Auto_tac;
    2.77 -by (Blast_tac 1); 
    2.78 -by (rename_tac "y" 1);
    2.79 -by (dres_inst_tac [("c", "y"), ("A", "AllowedActs(H)")] subsetD 1);
    2.80 -by (REPEAT(blast_tac (claset() addSEs [not_emptyE]) 1));
    2.81 -qed "JN_component_iff";
    2.82 -
    2.83 -Goalw [component_def] "i \\<in> I ==> F(i) component (\\<Squnion>i \\<in> I. (F(i)))";
    2.84 -by (blast_tac (claset() addIs [JN_absorb]) 1);
    2.85 -qed "component_JN";
    2.86 -
    2.87 -Goalw [component_def] "[| F component G; G component H |] ==> F component H";
    2.88 -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    2.89 -qed "component_trans";
    2.90 -
    2.91 -Goal "[| F \\<in> program; G \\<in> program |] ==>(F component G & G  component F) --> F = G";
    2.92 -by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.93 -by (Clarify_tac 1);
    2.94 -by (rtac program_equalityI 1);
    2.95 -by Auto_tac;
    2.96 -qed "component_antisym";
    2.97 -
    2.98 -Goal "H \\<in> program ==> ((F Join G) component H) <-> (F component H & G component H)";
    2.99 -by (asm_simp_tac (simpset() addsimps [component_eq_subset]) 1);
   2.100 -by (Blast_tac 1);
   2.101 -qed "Join_component_iff";
   2.102 -
   2.103 -Goal "[| F component G; G \\<in> A co B; F \\<in> program |] ==> F \\<in> A co B";
   2.104 -by (ftac constrainsD2 1);
   2.105 -by (rotate_tac ~1 1);
   2.106 -by (auto_tac (claset(), 
   2.107 -              simpset() addsimps [constrains_def, component_eq_subset]));
   2.108 -qed "component_constrains";
   2.109 -
   2.110 -(* Used in Guar.thy to show that programs are partially ordered*)
   2.111 -(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
   2.112 -
   2.113 -(*** preserves ***)
   2.114 -
   2.115 -Goalw [preserves_def, safety_prop_def]
   2.116 -  "safety_prop(preserves(f))";
   2.117 -by (auto_tac (claset() addDs [ActsD], simpset() addsimps [stable_def, constrains_def]));
   2.118 -by (dres_inst_tac [("c", "act")] subsetD 1);
   2.119 -by Auto_tac;
   2.120 -qed "preserves_is_safety_prop";
   2.121 -Addsimps [preserves_is_safety_prop];
   2.122 -
   2.123 -
   2.124 -val prems = Goalw [preserves_def] 
   2.125 -"\\<forall>z. F \\<in> stable({s \\<in> state. f(s) = z})  ==> F \\<in> preserves(f)";
   2.126 -by Auto_tac;
   2.127 -by (blast_tac (claset() addDs [stableD2]) 1);
   2.128 -qed "preserves_aux";
   2.129 -bind_thm("preservesI", allI RS preserves_aux);
   2.130 -
   2.131 -Goalw [preserves_def, stable_def, constrains_def]
   2.132 -     "[| F \\<in> preserves(f);  act \\<in> Acts(F);  <s,t> \\<in> act |] ==> f(s) = f(t)";
   2.133 -by (subgoal_tac "s \\<in> state & t \\<in> state" 1);
   2.134 -by (blast_tac (claset() addSDs [Acts_type RS subsetD]) 2);
   2.135 -by Auto_tac;
   2.136 -by (dres_inst_tac [("x", "f(s)")] spec 1);
   2.137 -by (dres_inst_tac [("x", "act")] bspec 1);
   2.138 -by Auto_tac;
   2.139 -qed "preserves_imp_eq";
   2.140 -
   2.141 -Goalw [preserves_def]
   2.142 -"(F Join G \\<in> preserves(v)) <->  \
   2.143 -\     (programify(F) \\<in> preserves(v) & programify(G) \\<in> preserves(v))";
   2.144 -by (auto_tac (claset(), simpset() addsimps [INT_iff]));
   2.145 -qed "Join_preserves";
   2.146 - 
   2.147 -Goal "(JOIN(I,F): preserves(v)) <-> (\\<forall>i \\<in> I. programify(F(i)):preserves(v))";
   2.148 -by (auto_tac (claset(), simpset() addsimps [JN_stable, preserves_def, INT_iff]));
   2.149 -qed "JN_preserves";
   2.150 -
   2.151 -Goal "SKIP \\<in> preserves(v)";
   2.152 -by (auto_tac (claset(), simpset() addsimps [preserves_def, INT_iff]));
   2.153 -qed "SKIP_preserves";
   2.154 -
   2.155 -AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
   2.156 -
   2.157 -Goalw [fun_pair_def] "fun_pair(f,g,x) = <f(x), g(x)>";
   2.158 -by (Simp_tac 1);
   2.159 -qed "fun_pair_apply";
   2.160 -Addsimps [fun_pair_apply];
   2.161 -
   2.162 -Goal "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)";
   2.163 -by (rtac equalityI 1);
   2.164 -by (auto_tac (claset(),
   2.165 -              simpset() addsimps [preserves_def, stable_def, constrains_def]));
   2.166 -by (REPEAT(Blast_tac 1));
   2.167 -qed "preserves_fun_pair";
   2.168 -
   2.169 -Goal "F \\<in> preserves(fun_pair(v, w))  <-> F \\<in> preserves(v) Int preserves(w)";
   2.170 -by (simp_tac (simpset() addsimps [preserves_fun_pair]) 1);
   2.171 -qed "preserves_fun_pair_iff";
   2.172 -AddIffs [preserves_fun_pair_iff];
   2.173 -
   2.174 -Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
   2.175 -by (simp_tac (simpset() addsimps [fun_pair_def, metacomp_def]) 1);
   2.176 -qed "fun_pair_comp_distrib";
   2.177 -
   2.178 -Goal "(f comp g)(x) = f(g(x))";
   2.179 -by (simp_tac (simpset() addsimps [metacomp_def]) 1);
   2.180 -qed "comp_apply";
   2.181 -Addsimps [comp_apply];
   2.182 -
   2.183 -Goalw [preserves_def]
   2.184 - "preserves(v)<=program";
   2.185 -by Auto_tac;
   2.186 -qed "preserves_type";
   2.187 -
   2.188 -Goal "F \\<in> preserves(f) ==> F \\<in> program";
   2.189 -by (blast_tac (claset() addIs [preserves_type RS subsetD]) 1);
   2.190 -qed "preserves_into_program";
   2.191 -AddTCs [preserves_into_program];
   2.192 -
   2.193 -Goal "preserves(f) <= preserves(g comp f)";
   2.194 -by (auto_tac (claset(),  simpset() 
   2.195 -     addsimps [preserves_def, stable_def, constrains_def]));
   2.196 -by (dres_inst_tac [("x", "f(xb)")] spec 1);
   2.197 -by (dres_inst_tac [("x", "act")] bspec 1);
   2.198 -by Auto_tac;
   2.199 -qed "subset_preserves_comp";
   2.200 -
   2.201 -Goal "F \\<in> preserves(f) ==> F \\<in> preserves(g comp f)";
   2.202 -by (blast_tac (claset() addIs [subset_preserves_comp RS subsetD]) 1);
   2.203 -qed "imp_preserves_comp";
   2.204 -
   2.205 -Goal "preserves(f) <= stable({s \\<in> state. P(f(s))})";
   2.206 -by (auto_tac (claset(),
   2.207 -              simpset() addsimps [preserves_def, stable_def, constrains_def]));
   2.208 -by (rename_tac "s' s" 1);
   2.209 -by (subgoal_tac "f(s) = f(s')" 1);
   2.210 -by (ALLGOALS Force_tac);
   2.211 -qed "preserves_subset_stable";
   2.212 -
   2.213 -Goal "F \\<in> preserves(f) ==> F \\<in> stable({s \\<in> state. P(f(s))})";
   2.214 -by (blast_tac (claset() addIs [preserves_subset_stable RS subsetD]) 1);
   2.215 -qed "preserves_imp_stable";
   2.216 -
   2.217 -Goalw  [increasing_def]
   2.218 - "[| F \\<in> preserves(f); \\<forall>x \\<in> state. f(x):A |] ==> F \\<in> Increasing.increasing(A, r, f)";
   2.219 -by (auto_tac (claset() addIs [preserves_into_program],
   2.220 -              simpset()));
   2.221 -by (res_inst_tac [("P", "%x. <k, x>:r")]  preserves_imp_stable 1);
   2.222 -by Auto_tac;
   2.223 -qed "preserves_imp_increasing";
   2.224 -
   2.225 -Goalw [preserves_def, stable_def, constrains_def]
   2.226 - "st_set(A) ==> preserves(%x. x) <= stable(A)";
   2.227 -by Auto_tac;
   2.228 -by (dres_inst_tac [("x", "xb")] spec 1);
   2.229 -by (dres_inst_tac [("x", "act")] bspec 1);
   2.230 -by (auto_tac (claset() addDs [ActsD], simpset()));
   2.231 -qed "preserves_id_subset_stable";
   2.232 -
   2.233 -Goal "[| F \\<in> preserves(%x. x); st_set(A) |] ==> F \\<in> stable(A)";
   2.234 -by (blast_tac (claset() addIs [preserves_id_subset_stable RS subsetD]) 1);
   2.235 -qed "preserves_id_imp_stable";
   2.236 -
   2.237 -(** Added by Sidi **)
   2.238 -(** component_of **)
   2.239 -
   2.240 -(*  component_of is stronger than component *)
   2.241 -Goalw [component_def, component_of_def]
   2.242 -"F component_of H ==> F component H";
   2.243 -by (Blast_tac 1);
   2.244 -qed "component_of_imp_component";
   2.245 -
   2.246 -(* component_of satisfies many of component's properties *)
   2.247 -Goalw [component_of_def]
   2.248 -"F \\<in> program ==> F component_of F";
   2.249 -by (res_inst_tac [("x", "SKIP")] exI 1);
   2.250 -by Auto_tac;
   2.251 -qed "component_of_refl";
   2.252 -
   2.253 -Goalw [component_of_def]
   2.254 -"F \\<in> program ==>SKIP component_of F";
   2.255 -by Auto_tac;
   2.256 -by (res_inst_tac [("x", "F")] exI 1);
   2.257 -by Auto_tac;
   2.258 -qed "component_of_SKIP";
   2.259 -Addsimps [component_of_refl, component_of_SKIP];
   2.260 -
   2.261 -Goalw [component_of_def]
   2.262 -"[| F component_of G; G component_of H |] ==> F component_of H";
   2.263 -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
   2.264 -qed "component_of_trans";
   2.265 -
   2.266 -(** localize **)
   2.267 -Goalw [localize_def]
   2.268 - "Init(localize(v,F)) = Init(F)";
   2.269 -by (Simp_tac 1);
   2.270 -qed "localize_Init_eq";
   2.271 -
   2.272 -Goalw [localize_def]
   2.273 - "Acts(localize(v,F)) = Acts(F)";
   2.274 -by (Simp_tac 1);
   2.275 -qed "localize_Acts_eq";
   2.276 -
   2.277 -Goalw [localize_def]
   2.278 - "AllowedActs(localize(v,F)) = AllowedActs(F) Int (\\<Union>G \\<in> preserves(v). Acts(G))";
   2.279 -by (rtac equalityI 1);
   2.280 -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
   2.281 -qed "localize_AllowedActs_eq";
   2.282 -
   2.283 -AddIffs [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
   2.284 -
   2.285 -(** Theorems used in ClientImpl **)
   2.286 -
   2.287 -Goal
   2.288 - "[| F \\<in> stable({s \\<in> state. P(f(s), g(s))});  G \\<in> preserves(f);  G \\<in> preserves(g) |] \
   2.289 -\     ==> F Join G \\<in> stable({s \\<in> state. P(f(s), g(s))})";
   2.290 -by (auto_tac (claset() addDs [ActsD, preserves_into_program], 
   2.291 -              simpset() addsimps [stable_def, constrains_def]));
   2.292 -by (case_tac "act \\<in> Acts(F)" 1);
   2.293 -by Auto_tac;
   2.294 -by (dtac preserves_imp_eq 1);
   2.295 -by (dtac preserves_imp_eq 3);
   2.296 -by Auto_tac;
   2.297 -qed "stable_localTo_stable2";
   2.298 -
   2.299 -Goal "[| F \\<in> stable({s \\<in> state. <f(s), g(s)>:r});  G \\<in> preserves(f);   \
   2.300 -\        F Join G \\<in> Increasing(A, r, g); \
   2.301 -\        \\<forall>x \\<in> state. f(x):A & g(x):A |]     \
   2.302 -\     ==> F Join G \\<in> Stable({s \\<in> state. <f(s), g(s)>:r})";
   2.303 -by (auto_tac (claset(), 
   2.304 -              simpset() addsimps [stable_def, Stable_def, Increasing_def, 
   2.305 -                                  Constrains_def, all_conj_distrib]));
   2.306 -by (ALLGOALS(asm_full_simp_tac (simpset()
   2.307 -        addsimps [constrains_type RS subsetD, preserves_type RS subsetD])));
   2.308 -by (blast_tac (claset() addIs [constrains_weaken]) 1); 
   2.309 -(*The G case remains*)
   2.310 -by (auto_tac (claset() addDs [ActsD], 
   2.311 -              simpset() addsimps [preserves_def, stable_def, constrains_def,
   2.312 -                                  ball_conj_distrib, all_conj_distrib]));
   2.313 -(*We have a G-action, so delete assumptions about F-actions*)
   2.314 -by (thin_tac "\\<forall>act \\<in> Acts(F). ?P(act)" 1);
   2.315 -by (thin_tac "\\<forall>k\\<in>A. \\<forall>act \\<in> Acts(F). ?P(k,act)" 1);
   2.316 -by (subgoal_tac "f(x) = f(xa)" 1);
   2.317 -by (auto_tac (claset() addSDs [bspec], simpset())); 
   2.318 -qed "Increasing_preserves_Stable";
   2.319 -
   2.320 -
   2.321 -(** Lemma used in AllocImpl **)
   2.322 -
   2.323 -Goalw [Constrains_def, constrains_def] 
   2.324 -"[| \\<forall>x \\<in> I. F \\<in> A(x) Co B; F \\<in> program |] ==> F:(\\<Union>x \\<in> I. A(x)) Co B";
   2.325 -by Auto_tac;
   2.326 -qed "Constrains_UN_left";
   2.327 -
   2.328 -Goalw [stable_def, Stable_def, preserves_def]
   2.329 - "[| F \\<in> stable({s \\<in> state. P(f(s), g(s))}); \
   2.330 -\    \\<forall>k \\<in> A. F Join G \\<in> Stable({s \\<in> state. P(k, g(s))}); \
   2.331 -\   G \\<in> preserves(f); \\<forall>s \\<in> state. f(s):A|] ==> \
   2.332 -\   F Join G \\<in> Stable({s \\<in> state. P(f(s), g(s))})";
   2.333 -by (res_inst_tac [("A", "(\\<Union>k \\<in> A. {s \\<in> state. f(s)=k} Int {s \\<in> state. P(f(s), g(s))})")]
   2.334 -               Constrains_weaken_L 1);
   2.335 -by (Blast_tac 2);
   2.336 -by (rtac Constrains_UN_left 1);
   2.337 -by Auto_tac;
   2.338 -by (res_inst_tac [("A", "{s \\<in> state. f(s)=k} Int {s \\<in> state. P(f(s), g(s))} Int \
   2.339 -\                        {s \\<in> state. P(k, g(s))}"),
   2.340 -                  ("A'", "({s \\<in> state. f(s)=k} Un {s \\<in> state. P(f(s), g(s))}) \
   2.341 -\                           Int {s \\<in> state. P(k, g(s))}")] Constrains_weaken 1);
   2.342 -by (REPEAT(Blast_tac 2));
   2.343 -by (rtac Constrains_Int 1);
   2.344 -by (rtac constrains_imp_Constrains 1);
   2.345 -by (auto_tac (claset(), simpset() addsimps [constrains_type RS subsetD]));
   2.346 -by (ALLGOALS(rtac constrains_weaken));
   2.347 -by (rotate_tac ~1 4);
   2.348 -by (dres_inst_tac [("x", "k")] spec 4);
   2.349 -by (REPEAT(Blast_tac 1));
   2.350 -qed "stable_Join_Stable";
   2.351 -
     3.1 --- a/src/ZF/UNITY/Comp.thy	Tue Jul 08 11:44:30 2003 +0200
     3.2 +++ b/src/ZF/UNITY/Comp.thy	Wed Jul 09 11:39:34 2003 +0200
     3.3 @@ -3,7 +3,6 @@
     3.4      Author:     Sidi O Ehmety, Computer Laboratory
     3.5      Copyright   1998  University of Cambridge
     3.6  
     3.7 -Composition
     3.8  From Chandy and Sanders, "Reasoning About Program Composition",
     3.9  Technical Report 2000-003, University of Florida, 2000.
    3.10  
    3.11 @@ -15,14 +14,16 @@
    3.12    
    3.13  *)
    3.14  
    3.15 -Comp = Union + Increasing +
    3.16 +header{*Composition*}
    3.17 +
    3.18 +theory Comp = Union + Increasing:
    3.19  
    3.20  constdefs
    3.21  
    3.22 -  component :: [i, i] => o  (infixl 65) 
    3.23 +  component :: "[i,i]=>o"  (infixl "component" 65) 
    3.24    "F component H == (EX G. F Join G = H)"
    3.25  
    3.26 -  strict_component :: [i, i] => o (infixl "strict'_component" 65)
    3.27 +  strict_component :: "[i,i]=>o" (infixl "strict'_component" 65)
    3.28    "F strict_component H == F component H & F~=H"
    3.29  
    3.30    (* A stronger form of the component relation *)
    3.31 @@ -33,15 +34,360 @@
    3.32    "F strict_component_of H  == F component_of H  & F~=H"
    3.33  
    3.34    (* Preserves a state function f, in particular a variable *)
    3.35 -  preserves :: (i=>i)=>i
    3.36 +  preserves :: "(i=>i)=>i"
    3.37    "preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}"
    3.38  
    3.39    fun_pair :: "[i=>i, i =>i] =>(i=>i)"
    3.40    "fun_pair(f, g) == %x. <f(x), g(x)>"
    3.41  
    3.42 -localize  :: "[i=>i, i] => i"
    3.43 +  localize  :: "[i=>i, i] => i"
    3.44    "localize(f,F) == mk_program(Init(F), Acts(F),
    3.45  		       AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
    3.46  
    3.47    
    3.48 -  end
    3.49 +(*** component and strict_component relations ***)
    3.50 +
    3.51 +lemma componentI: 
    3.52 +     "H component F | H component G ==> H component (F Join G)"
    3.53 +apply (unfold component_def, auto)
    3.54 +apply (rule_tac x = "Ga Join G" in exI)
    3.55 +apply (rule_tac [2] x = "G Join F" in exI)
    3.56 +apply (auto simp add: Join_ac)
    3.57 +done
    3.58 +
    3.59 +lemma component_eq_subset: 
    3.60 +     "G \<in> program ==> (F component G) <->  
    3.61 +   (Init(G) <= Init(F) & Acts(F) <= Acts(G) & AllowedActs(G) <= AllowedActs(F))"
    3.62 +apply (unfold component_def, auto)
    3.63 +apply (rule exI)
    3.64 +apply (rule program_equalityI, auto)
    3.65 +done
    3.66 +
    3.67 +lemma component_SKIP [simp]: "F \<in> program ==> SKIP component F"
    3.68 +apply (unfold component_def)
    3.69 +apply (rule_tac x = F in exI)
    3.70 +apply (force intro: Join_SKIP_left)
    3.71 +done
    3.72 +
    3.73 +lemma component_refl [simp]: "F \<in> program ==> F component F"
    3.74 +apply (unfold component_def)
    3.75 +apply (rule_tac x = F in exI)
    3.76 +apply (force intro: Join_SKIP_right)
    3.77 +done
    3.78 +
    3.79 +lemma SKIP_minimal: "F component SKIP ==> programify(F) = SKIP"
    3.80 +apply (rule program_equalityI)
    3.81 +apply (simp_all add: component_eq_subset, blast)
    3.82 +done
    3.83 +
    3.84 +lemma component_Join1: "F component (F Join G)"
    3.85 +by (unfold component_def, blast)
    3.86 +
    3.87 +lemma component_Join2: "G component (F Join G)"
    3.88 +apply (unfold component_def)
    3.89 +apply (simp (no_asm) add: Join_commute)
    3.90 +apply blast
    3.91 +done
    3.92 +
    3.93 +lemma Join_absorb1: "F component G ==> F Join G = G"
    3.94 +by (auto simp add: component_def Join_left_absorb)
    3.95 +
    3.96 +lemma Join_absorb2: "G component F ==> F Join G = F"
    3.97 +by (auto simp add: Join_ac component_def)
    3.98 +
    3.99 +lemma JN_component_iff:
   3.100 +     "H \<in> program==>(JOIN(I,F) component H) <-> (\<forall>i \<in> I. F(i) component H)"
   3.101 +apply (case_tac "I=0", force)
   3.102 +apply (simp (no_asm_simp) add: component_eq_subset)
   3.103 +apply auto
   3.104 +apply blast
   3.105 +apply (rename_tac "y")
   3.106 +apply (drule_tac c = y and A = "AllowedActs (H)" in subsetD)
   3.107 +apply (blast elim!: not_emptyE)+
   3.108 +done
   3.109 +
   3.110 +lemma component_JN: "i \<in> I ==> F(i) component (\<Squnion>i \<in> I. (F(i)))"
   3.111 +apply (unfold component_def)
   3.112 +apply (blast intro: JN_absorb)
   3.113 +done
   3.114 +
   3.115 +lemma component_trans: "[| F component G; G component H |] ==> F component H"
   3.116 +apply (unfold component_def)
   3.117 +apply (blast intro: Join_assoc [symmetric])
   3.118 +done
   3.119 +
   3.120 +lemma component_antisym:
   3.121 +     "[| F \<in> program; G \<in> program |] ==>(F component G & G  component F) --> F = G"
   3.122 +apply (simp (no_asm_simp) add: component_eq_subset)
   3.123 +apply clarify
   3.124 +apply (rule program_equalityI, auto)
   3.125 +done
   3.126 +
   3.127 +lemma Join_component_iff:
   3.128 +     "H \<in> program ==> 
   3.129 +      ((F Join G) component H) <-> (F component H & G component H)"
   3.130 +apply (simp (no_asm_simp) add: component_eq_subset)
   3.131 +apply blast
   3.132 +done
   3.133 +
   3.134 +lemma component_constrains:
   3.135 +     "[| F component G; G \<in> A co B; F \<in> program |] ==> F \<in> A co B"
   3.136 +apply (frule constrainsD2)
   3.137 +apply (auto simp add: constrains_def component_eq_subset)
   3.138 +done
   3.139 +
   3.140 +(* Used in Guar.thy to show that programs are partially ordered*)
   3.141 +(* bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);*)
   3.142 +
   3.143 +(*** preserves ***)
   3.144 +
   3.145 +lemma preserves_is_safety_prop [simp]: "safety_prop(preserves(f))"
   3.146 +apply (unfold preserves_def safety_prop_def)
   3.147 +apply (auto dest: ActsD simp add: stable_def constrains_def)
   3.148 +apply (drule_tac c = act in subsetD, auto)
   3.149 +done
   3.150 +
   3.151 +lemma preservesI [rule_format]: 
   3.152 +     "\<forall>z. F \<in> stable({s \<in> state. f(s) = z})  ==> F \<in> preserves(f)"
   3.153 +apply (auto simp add: preserves_def)
   3.154 +apply (blast dest: stableD2)
   3.155 +done
   3.156 +
   3.157 +lemma preserves_imp_eq: 
   3.158 +     "[| F \<in> preserves(f);  act \<in> Acts(F);  <s,t> \<in> act |] ==> f(s) = f(t)"
   3.159 +apply (unfold preserves_def stable_def constrains_def)
   3.160 +apply (subgoal_tac "s \<in> state & t \<in> state")
   3.161 + prefer 2 apply (blast dest!: Acts_type [THEN subsetD], force) 
   3.162 +done
   3.163 +
   3.164 +lemma Join_preserves [iff]: 
   3.165 +"(F Join G \<in> preserves(v)) <->   
   3.166 +      (programify(F) \<in> preserves(v) & programify(G) \<in> preserves(v))"
   3.167 +by (auto simp add: preserves_def INT_iff)
   3.168 + 
   3.169 +lemma JN_preserves [iff]:
   3.170 +     "(JOIN(I,F): preserves(v)) <-> (\<forall>i \<in> I. programify(F(i)):preserves(v))"
   3.171 +by (auto simp add: JN_stable preserves_def INT_iff)
   3.172 +
   3.173 +lemma SKIP_preserves [iff]: "SKIP \<in> preserves(v)"
   3.174 +by (auto simp add: preserves_def INT_iff)
   3.175 +
   3.176 +lemma fun_pair_apply [simp]: "fun_pair(f,g,x) = <f(x), g(x)>"
   3.177 +apply (unfold fun_pair_def)
   3.178 +apply (simp (no_asm))
   3.179 +done
   3.180 +
   3.181 +lemma preserves_fun_pair:
   3.182 +     "preserves(fun_pair(v,w)) = preserves(v) Int preserves(w)"
   3.183 +apply (rule equalityI)
   3.184 +apply (auto simp add: preserves_def stable_def constrains_def, blast+)
   3.185 +done
   3.186 +
   3.187 +lemma preserves_fun_pair_iff [iff]:
   3.188 +     "F \<in> preserves(fun_pair(v, w))  <-> F \<in> preserves(v) Int preserves(w)"
   3.189 +by (simp add: preserves_fun_pair)
   3.190 +
   3.191 +lemma fun_pair_comp_distrib:
   3.192 +     "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)"
   3.193 +by (simp add: fun_pair_def metacomp_def)
   3.194 +
   3.195 +lemma comp_apply [simp]: "(f comp g)(x) = f(g(x))"
   3.196 +by (simp add: metacomp_def)
   3.197 +
   3.198 +lemma preserves_type: "preserves(v)<=program"
   3.199 +by (unfold preserves_def, auto)
   3.200 +
   3.201 +lemma preserves_into_program [TC]: "F \<in> preserves(f) ==> F \<in> program"
   3.202 +by (blast intro: preserves_type [THEN subsetD])
   3.203 +
   3.204 +lemma subset_preserves_comp: "preserves(f) <= preserves(g comp f)"
   3.205 +apply (auto simp add: preserves_def stable_def constrains_def)
   3.206 +apply (drule_tac x = "f (xb)" in spec)
   3.207 +apply (drule_tac x = act in bspec, auto)
   3.208 +done
   3.209 +
   3.210 +lemma imp_preserves_comp: "F \<in> preserves(f) ==> F \<in> preserves(g comp f)"
   3.211 +by (blast intro: subset_preserves_comp [THEN subsetD])
   3.212 +
   3.213 +lemma preserves_subset_stable: "preserves(f) <= stable({s \<in> state. P(f(s))})"
   3.214 +apply (auto simp add: preserves_def stable_def constrains_def)
   3.215 +apply (rename_tac s' s)
   3.216 +apply (subgoal_tac "f (s) = f (s') ")
   3.217 +apply (force+)
   3.218 +done
   3.219 +
   3.220 +lemma preserves_imp_stable:
   3.221 +     "F \<in> preserves(f) ==> F \<in> stable({s \<in> state. P(f(s))})"
   3.222 +by (blast intro: preserves_subset_stable [THEN subsetD])
   3.223 +
   3.224 +lemma preserves_imp_increasing: 
   3.225 + "[| F \<in> preserves(f); \<forall>x \<in> state. f(x):A |] ==> F \<in> Increasing.increasing(A, r, f)"
   3.226 +apply (unfold Increasing.increasing_def)
   3.227 +apply (auto intro: preserves_into_program)
   3.228 +apply (rule_tac P = "%x. <k, x>:r" in preserves_imp_stable, auto)
   3.229 +done
   3.230 +
   3.231 +lemma preserves_id_subset_stable: 
   3.232 + "st_set(A) ==> preserves(%x. x) <= stable(A)"
   3.233 +apply (unfold preserves_def stable_def constrains_def, auto)
   3.234 +apply (drule_tac x = xb in spec)
   3.235 +apply (drule_tac x = act in bspec)
   3.236 +apply (auto dest: ActsD)
   3.237 +done
   3.238 +
   3.239 +lemma preserves_id_imp_stable:
   3.240 +     "[| F \<in> preserves(%x. x); st_set(A) |] ==> F \<in> stable(A)"
   3.241 +by (blast intro: preserves_id_subset_stable [THEN subsetD])
   3.242 +
   3.243 +(** Added by Sidi **)
   3.244 +(** component_of **)
   3.245 +
   3.246 +(*  component_of is stronger than component *)
   3.247 +lemma component_of_imp_component: 
   3.248 +"F component_of H ==> F component H"
   3.249 +apply (unfold component_def component_of_def, blast)
   3.250 +done
   3.251 +
   3.252 +(* component_of satisfies many of component's properties *)
   3.253 +lemma component_of_refl [simp]: "F \<in> program ==> F component_of F"
   3.254 +apply (unfold component_of_def)
   3.255 +apply (rule_tac x = SKIP in exI, auto)
   3.256 +done
   3.257 +
   3.258 +lemma component_of_SKIP [simp]: "F \<in> program ==>SKIP component_of F"
   3.259 +apply (unfold component_of_def, auto)
   3.260 +apply (rule_tac x = F in exI, auto)
   3.261 +done
   3.262 +
   3.263 +lemma component_of_trans: 
   3.264 +     "[| F component_of G; G component_of H |] ==> F component_of H"
   3.265 +apply (unfold component_of_def)
   3.266 +apply (blast intro: Join_assoc [symmetric])
   3.267 +done
   3.268 +
   3.269 +(** localize **)
   3.270 +lemma localize_Init_eq [simp]: "Init(localize(v,F)) = Init(F)"
   3.271 +by (unfold localize_def, simp)
   3.272 +
   3.273 +lemma localize_Acts_eq [simp]: "Acts(localize(v,F)) = Acts(F)"
   3.274 +by (unfold localize_def, simp)
   3.275 +
   3.276 +lemma localize_AllowedActs_eq [simp]: 
   3.277 + "AllowedActs(localize(v,F)) = AllowedActs(F) Int (\<Union>G \<in> preserves(v). Acts(G))"
   3.278 +apply (unfold localize_def)
   3.279 +apply (rule equalityI)
   3.280 +apply (auto dest: Acts_type [THEN subsetD])
   3.281 +done
   3.282 +
   3.283 +
   3.284 +(** Theorems used in ClientImpl **)
   3.285 +
   3.286 +lemma stable_localTo_stable2: 
   3.287 + "[| F \<in> stable({s \<in> state. P(f(s), g(s))});  G \<in> preserves(f);  G \<in> preserves(g) |]  
   3.288 +      ==> F Join G \<in> stable({s \<in> state. P(f(s), g(s))})"
   3.289 +apply (auto dest: ActsD preserves_into_program simp add: stable_def constrains_def)
   3.290 +apply (case_tac "act \<in> Acts (F) ")
   3.291 +apply auto
   3.292 +apply (drule preserves_imp_eq)
   3.293 +apply (drule_tac [3] preserves_imp_eq, auto)
   3.294 +done
   3.295 +
   3.296 +lemma Increasing_preserves_Stable:
   3.297 +     "[| F \<in> stable({s \<in> state. <f(s), g(s)>:r});  G \<in> preserves(f);    
   3.298 +         F Join G \<in> Increasing(A, r, g);  
   3.299 +         \<forall>x \<in> state. f(x):A & g(x):A |]      
   3.300 +      ==> F Join G \<in> Stable({s \<in> state. <f(s), g(s)>:r})"
   3.301 +apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
   3.302 +apply (simp_all add: constrains_type [THEN subsetD] preserves_type [THEN subsetD])
   3.303 +apply (blast intro: constrains_weaken)
   3.304 +(*The G case remains*)
   3.305 +apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
   3.306 +(*We have a G-action, so delete assumptions about F-actions*)
   3.307 +apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
   3.308 +apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
   3.309 +apply (subgoal_tac "f (x) = f (xa) ")
   3.310 +apply (auto dest!: bspec)
   3.311 +done
   3.312 +
   3.313 +
   3.314 +(** Lemma used in AllocImpl **)
   3.315 +
   3.316 +lemma Constrains_UN_left: 
   3.317 +     "[| \<forall>x \<in> I. F \<in> A(x) Co B; F \<in> program |] ==> F:(\<Union>x \<in> I. A(x)) Co B"
   3.318 +by (unfold Constrains_def constrains_def, auto)
   3.319 +
   3.320 +
   3.321 +lemma stable_Join_Stable: 
   3.322 + "[| F \<in> stable({s \<in> state. P(f(s), g(s))});  
   3.323 +     \<forall>k \<in> A. F Join G \<in> Stable({s \<in> state. P(k, g(s))});  
   3.324 +     G \<in> preserves(f); \<forall>s \<in> state. f(s):A|]
   3.325 +  ==> F Join G \<in> Stable({s \<in> state. P(f(s), g(s))})"
   3.326 +apply (unfold stable_def Stable_def preserves_def)
   3.327 +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)
   3.328 +prefer 2 apply blast
   3.329 +apply (rule Constrains_UN_left, auto)
   3.330 +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)
   3.331 + prefer 2 apply blast 
   3.332 + prefer 2 apply blast 
   3.333 +apply (rule Constrains_Int)
   3.334 +apply (rule constrains_imp_Constrains)
   3.335 +apply (auto simp add: constrains_type [THEN subsetD])
   3.336 +apply (blast intro: constrains_weaken) 
   3.337 +apply (drule_tac x = k in spec)
   3.338 +apply (blast intro: constrains_weaken) 
   3.339 +done
   3.340 +
   3.341 +ML
   3.342 +{*
   3.343 +val component_of_def = thm "component_of_def";
   3.344 +val component_def = thm "component_def";
   3.345 +
   3.346 +val componentI = thm "componentI";
   3.347 +val component_eq_subset = thm "component_eq_subset";
   3.348 +val component_SKIP = thm "component_SKIP";
   3.349 +val component_refl = thm "component_refl";
   3.350 +val SKIP_minimal = thm "SKIP_minimal";
   3.351 +val component_Join1 = thm "component_Join1";
   3.352 +val component_Join2 = thm "component_Join2";
   3.353 +val Join_absorb1 = thm "Join_absorb1";
   3.354 +val Join_absorb2 = thm "Join_absorb2";
   3.355 +val JN_component_iff = thm "JN_component_iff";
   3.356 +val component_JN = thm "component_JN";
   3.357 +val component_trans = thm "component_trans";
   3.358 +val component_antisym = thm "component_antisym";
   3.359 +val Join_component_iff = thm "Join_component_iff";
   3.360 +val component_constrains = thm "component_constrains";
   3.361 +val preserves_is_safety_prop = thm "preserves_is_safety_prop";
   3.362 +val preservesI = thm "preservesI";
   3.363 +val preserves_imp_eq = thm "preserves_imp_eq";
   3.364 +val Join_preserves = thm "Join_preserves";
   3.365 +val JN_preserves = thm "JN_preserves";
   3.366 +val SKIP_preserves = thm "SKIP_preserves";
   3.367 +val fun_pair_apply = thm "fun_pair_apply";
   3.368 +val preserves_fun_pair = thm "preserves_fun_pair";
   3.369 +val preserves_fun_pair_iff = thm "preserves_fun_pair_iff";
   3.370 +val fun_pair_comp_distrib = thm "fun_pair_comp_distrib";
   3.371 +val comp_apply = thm "comp_apply";
   3.372 +val preserves_type = thm "preserves_type";
   3.373 +val preserves_into_program = thm "preserves_into_program";
   3.374 +val subset_preserves_comp = thm "subset_preserves_comp";
   3.375 +val imp_preserves_comp = thm "imp_preserves_comp";
   3.376 +val preserves_subset_stable = thm "preserves_subset_stable";
   3.377 +val preserves_imp_stable = thm "preserves_imp_stable";
   3.378 +val preserves_imp_increasing = thm "preserves_imp_increasing";
   3.379 +val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   3.380 +val preserves_id_imp_stable = thm "preserves_id_imp_stable";
   3.381 +val component_of_imp_component = thm "component_of_imp_component";
   3.382 +val component_of_refl = thm "component_of_refl";
   3.383 +val component_of_SKIP = thm "component_of_SKIP";
   3.384 +val component_of_trans = thm "component_of_trans";
   3.385 +val localize_Init_eq = thm "localize_Init_eq";
   3.386 +val localize_Acts_eq = thm "localize_Acts_eq";
   3.387 +val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   3.388 +val stable_localTo_stable2 = thm "stable_localTo_stable2";
   3.389 +val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   3.390 +val Constrains_UN_left = thm "Constrains_UN_left";
   3.391 +val stable_Join_Stable = thm "stable_Join_Stable";
   3.392 +*}
   3.393 +
   3.394 +end
     4.1 --- a/src/ZF/UNITY/Follows.ML	Tue Jul 08 11:44:30 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,487 +0,0 @@
     4.4 -(*  Title:      ZF/UNITY/Follows
     4.5 -    ID:         $Id \\<in> Follows.ML,v 1.4 2003/06/27 16:40:25 paulson Exp $
     4.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 -    Copyright   2001  University of Cambridge
     4.8 - 
     4.9 -The Follows relation of Charpentier and Sivilotte
    4.10 -*)
    4.11 - 
    4.12 -(*Does this hold for "invariant"?*)
    4.13 -
    4.14 -val prems =
    4.15 -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')";
    4.16 -by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
    4.17 -qed "Follows_cong";
    4.18 -
    4.19 -Goalw [mono1_def, metacomp_def] 
    4.20 -"[| mono1(A, r, B, s, h); \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
    4.21 -\  Always({x \\<in> state. <f(x), g(x)> \\<in> r})<=Always({x \\<in> state. <(h comp f)(x), (h comp g)(x)> \\<in> s})";
    4.22 -by (auto_tac (claset(), simpset() addsimps 
    4.23 -         [Always_eq_includes_reachable]));
    4.24 -qed "subset_Always_comp";
    4.25 -
    4.26 -Goal 
    4.27 -"[| F \\<in> Always({x \\<in> state. <f(x), g(x)> \\<in> r}); \
    4.28 -\   mono1(A, r, B, s, h); \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
    4.29 -\   F \\<in> Always({x \\<in> state. <(h comp f)(x), (h comp g)(x)> \\<in> s})";
    4.30 -by (blast_tac (claset() addIs [subset_Always_comp RS subsetD]) 1);
    4.31 -qed "imp_Always_comp";
    4.32 -
    4.33 -Goal 
    4.34 -"[| F \\<in> Always({x \\<in> state. <f1(x), f(x)> \\<in> r});  \
    4.35 -\   F \\<in> Always({x \\<in> state. <g1(x), g(x)> \\<in> s}); \
    4.36 -\   mono2(A, r, B, s, C, t, h); \
    4.37 -\   \\<forall>x \\<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \
    4.38 -\ ==> F \\<in> Always({x \\<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \\<in> t})";
    4.39 -by (auto_tac (claset(), simpset() addsimps 
    4.40 -         [Always_eq_includes_reachable, mono2_def]));
    4.41 -by (auto_tac (claset() addSDs [subsetD], simpset()));
    4.42 -qed "imp_Always_comp2";
    4.43 -
    4.44 -(* comp LeadsTo *)
    4.45 -
    4.46 -Goalw [mono1_def, metacomp_def]
    4.47 -"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
    4.48 -\       \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
    4.49 -\ (\\<Inter>j \\<in> A. {s \\<in> state. <j, g(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f(s)> \\<in> r}) <= \
    4.50 -\(\\<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})";
    4.51 -by (Clarify_tac 1);
    4.52 -by (ALLGOALS(full_simp_tac (simpset() addsimps [INT_iff])));
    4.53 -by Auto_tac;
    4.54 -by (rtac single_LeadsTo_I 1);
    4.55 -by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]) 2);
    4.56 -by Auto_tac;
    4.57 -by (rotate_tac 5 1);
    4.58 -by (dres_inst_tac [("x", "g(sa)")] bspec 1);
    4.59 -by (etac LeadsTo_weaken 2);
    4.60 -by (auto_tac (claset(), simpset() addsimps [part_order_def, refl_def]));
    4.61 -by (res_inst_tac [("b", "h(g(sa))")] trans_onD 1);
    4.62 -by (Blast_tac 1);
    4.63 -by Auto_tac;
    4.64 -qed "subset_LeadsTo_comp";
    4.65 -
    4.66 -Goal
    4.67 -"[| F:(\\<Inter>j \\<in> A. {s \\<in> state. <j, g(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f(s)> \\<in> r}); \
    4.68 -\   mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
    4.69 -\   \\<forall>x \\<in> state. f(x):A & g(x):A |] ==> \
    4.70 -\  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})";
    4.71 -by (rtac (subset_LeadsTo_comp RS subsetD) 1);
    4.72 -by Auto_tac;
    4.73 -qed "imp_LeadsTo_comp";
    4.74 -
    4.75 -Goalw [mono2_def, Increasing_def]
    4.76 -"[| F \\<in> Increasing(B, s, g); \
    4.77 -\ \\<forall>j \\<in> A. F: {s \\<in> state. <j, f(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f1(s)> \\<in> r}; \
    4.78 -\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t); \
    4.79 -\ \\<forall>x \\<in> state. f1(x):A & f(x):A & g(x):B; k \\<in> C |] ==> \
    4.80 -\ F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f1(x), g(x))> \\<in> t}";
    4.81 -by (rtac single_LeadsTo_I 1);
    4.82 -by Auto_tac;
    4.83 -by (dres_inst_tac [("x", "g(sa)"), ("A","B")] bspec 1);
    4.84 -by Auto_tac;
    4.85 -by (dres_inst_tac [("x", "f(sa)"),("P","%j. F \\<in> ?X(j) \\<longmapsto>w ?Y(j)")] bspec 1);
    4.86 -by Auto_tac;
    4.87 -by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
    4.88 -by (Blast_tac 1);
    4.89 -by (Blast_tac 1);
    4.90 -by Auto_tac;
    4.91 -by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
    4.92 -by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
    4.93 -by (dres_inst_tac [("x", "f1(x)"), ("x1", "f(sa)"), 
    4.94 -                   ("P2", "%x y. \\<forall>u\\<in>B. ?P(x,y,u)")] (bspec RS bspec) 1);
    4.95 -by (dres_inst_tac [("x", "g(x)"), ("x1", "g(sa)"), 
    4.96 -                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
    4.97 -by Auto_tac;
    4.98 -by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
    4.99 -by (auto_tac (claset(), simpset() addsimps [part_order_def]));
   4.100 -qed "imp_LeadsTo_comp_right";
   4.101 -
   4.102 -Goalw [mono2_def, Increasing_def]
   4.103 -"[| F \\<in> Increasing(A, r, f); \
   4.104 -\ \\<forall>j \\<in> B. F: {x \\<in> state. <j, g(x)> \\<in> s} LeadsTo {x \\<in> state. <j,g1(x)> \\<in> s}; \
   4.105 -\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
   4.106 -\ \\<forall>x \\<in> state. f(x):A & g1(x):B & g(x):B; k \\<in> C |] ==> \
   4.107 -\ F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f(x), g1(x))> \\<in> t}";
   4.108 -by (rtac single_LeadsTo_I 1);
   4.109 -by Auto_tac;
   4.110 -by (dres_inst_tac [("x", "f(sa)"),("P","%k. F \\<in> Stable(?X(k))")] bspec 1);
   4.111 -by Auto_tac;
   4.112 -by (dres_inst_tac [("x", "g(sa)")] bspec 1);
   4.113 -by Auto_tac;
   4.114 -by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
   4.115 -by (Blast_tac 1);
   4.116 -by (Blast_tac 1);
   4.117 -by Auto_tac;
   4.118 -by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
   4.119 -by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
   4.120 -by (dres_inst_tac [("x", "f(x)"), ("x1", "f(sa)")] (bspec RS bspec) 1);
   4.121 -by (dres_inst_tac [("x", "g1(x)"), ("x1", "g(sa)"), 
   4.122 -                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
   4.123 -by Auto_tac;
   4.124 -by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
   4.125 -by (auto_tac (claset(), simpset() addsimps [part_order_def]));
   4.126 -qed "imp_LeadsTo_comp_left";
   4.127 -
   4.128 -(**  This general result is used to prove Follows Un, munion, etc. **)
   4.129 -Goal
   4.130 -"[| F \\<in> Increasing(A, r, f1) Int  Increasing(B, s, g); \
   4.131 -\ \\<forall>j \\<in> A. F: {s \\<in> state. <j, f(s)> \\<in> r} LeadsTo {s \\<in> state. <j,f1(s)> \\<in> r}; \
   4.132 -\ \\<forall>j \\<in> B. F: {x \\<in> state. <j, g(x)> \\<in> s} LeadsTo {x \\<in> state. <j,g1(x)> \\<in> s}; \
   4.133 -\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
   4.134 -\ \\<forall>x \\<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \\<in> C |]\
   4.135 -\ ==> F:{x \\<in> state. <k, h(f(x), g(x))> \\<in> t} LeadsTo {x \\<in> state. <k, h(f1(x), g1(x))> \\<in> t}";
   4.136 -by (res_inst_tac [("B", "{x \\<in> state. <k, h(f1(x), g(x))> \\<in> t}")] LeadsTo_Trans 1);
   4.137 -by (blast_tac (claset() addIs [imp_LeadsTo_comp_right]) 1);
   4.138 -by (blast_tac (claset() addIs [imp_LeadsTo_comp_left]) 1);
   4.139 -qed "imp_LeadsTo_comp2";
   4.140 -
   4.141 -(* Follows type *)
   4.142 -Goalw [Follows_def] "Follows(A, r, f, g)<=program";
   4.143 -by (blast_tac (claset() addDs [Increasing_type RS subsetD]) 1);
   4.144 -qed "Follows_type";
   4.145 -
   4.146 -Goal "F \\<in> Follows(A, r, f, g) ==> F \\<in> program";
   4.147 -by (blast_tac (claset() addDs [Follows_type RS subsetD]) 1);
   4.148 -qed "Follows_into_program";
   4.149 -AddTCs [Follows_into_program];
   4.150 -
   4.151 -Goalw [Follows_def] 
   4.152 -"F \\<in> Follows(A, r, f, g)==> \
   4.153 -\ F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>x \\<in> state. f(x):A & g(x):A)";
   4.154 -by (blast_tac (claset() addDs [IncreasingD]) 1);
   4.155 -qed "FollowsD";
   4.156 -
   4.157 -Goalw [Follows_def]
   4.158 - "[| F \\<in> program; c \\<in> A; refl(A, r) |] ==> F \\<in> Follows(A, r, %x. c, %x. c)";
   4.159 -by Auto_tac;
   4.160 -by (auto_tac (claset(), simpset() addsimps [refl_def]));
   4.161 -qed "Follows_constantI";
   4.162 -
   4.163 -Goalw [Follows_def] 
   4.164 -"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
   4.165 -\  ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)";
   4.166 -by (Clarify_tac 1);
   4.167 -by (forw_inst_tac [("f", "g")] IncreasingD 1);
   4.168 -by (forw_inst_tac [("f", "f")] IncreasingD 1);
   4.169 -by (rtac IntI 1);
   4.170 -by (res_inst_tac [("h", "h")] imp_LeadsTo_comp 2);
   4.171 -by (assume_tac 5);
   4.172 -by (auto_tac (claset() addIs  [imp_Increasing_comp, imp_Always_comp], 
   4.173 -             simpset() delsimps INT_simps));
   4.174 -qed "subset_Follows_comp";
   4.175 -
   4.176 -Goal
   4.177 -"[| F \\<in> Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
   4.178 -\ ==>  F \\<in> Follows(B, s,  h comp f, h comp g)";
   4.179 -by (blast_tac (claset() addIs [subset_Follows_comp RS subsetD]) 1);
   4.180 -qed "imp_Follows_comp";
   4.181 -
   4.182 -(* 2-place monotone operation \\<in> this general result is used to prove Follows_Un, Follows_munion *)
   4.183 -
   4.184 -(* 2-place monotone operation \\<in> this general result is 
   4.185 -   used to prove Follows_Un, Follows_munion *)
   4.186 -Goalw [Follows_def] 
   4.187 -"[| F \\<in> Follows(A, r, f1, f);  F \\<in> Follows(B, s, g1, g); \
   4.188 -\  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |] \
   4.189 -\  ==> F \\<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))";
   4.190 -by (Clarify_tac 1);
   4.191 -by (forw_inst_tac [("f", "g")] IncreasingD 1);
   4.192 -by (forw_inst_tac [("f", "f")] IncreasingD 1);
   4.193 -by (rtac IntI 1);
   4.194 -by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 2);
   4.195 -by Safe_tac;
   4.196 -by (res_inst_tac [("h", "h")] imp_Always_comp2 3);
   4.197 -by (assume_tac 5);
   4.198 -by (res_inst_tac [("h", "h")] imp_Increasing_comp2 2);
   4.199 -by (assume_tac 4);
   4.200 -by (res_inst_tac [("h", "h")] imp_Increasing_comp2 1);
   4.201 -by (assume_tac 3);
   4.202 -by (TRYALL(assume_tac));
   4.203 -by (ALLGOALS(Asm_full_simp_tac)); 
   4.204 -by (blast_tac (claset() addSDs [IncreasingD]) 1);
   4.205 -by (res_inst_tac [("h", "h")] imp_LeadsTo_comp2 1);
   4.206 -by (assume_tac 4);
   4.207 -by Auto_tac;
   4.208 -by (rewrite_goal_tac [mono2_def] 3);
   4.209 -by (REPEAT(blast_tac (claset() addDs [IncreasingD]) 1));
   4.210 -qed "imp_Follows_comp2";
   4.211 -
   4.212 -Goal "[| F \\<in> Follows(A, r, f, g);  F \\<in> Follows(A,r, g, h); \
   4.213 -\        trans[A](r) |] ==> F \\<in> Follows(A, r, f, h)";
   4.214 -by (forw_inst_tac [("f", "f")] FollowsD 1);
   4.215 -by (forw_inst_tac [("f", "g")] FollowsD 1);
   4.216 -by (rewrite_goal_tac [Follows_def] 1);
   4.217 -by (asm_full_simp_tac (simpset() 
   4.218 -                 addsimps [Always_eq_includes_reachable, INT_iff]) 1);
   4.219 -by Auto_tac;
   4.220 -by (res_inst_tac [("B", "{s \\<in> state. <k, g(s)> \\<in> r}")] LeadsTo_Trans 2);
   4.221 -by (res_inst_tac [("b", "g(x)")] trans_onD 1);
   4.222 -by (REPEAT(Blast_tac 1));
   4.223 -qed "Follows_trans";
   4.224 -
   4.225 -(** Destruction rules for Follows **)
   4.226 -
   4.227 -Goalw [Follows_def]
   4.228 -     "F \\<in> Follows(A, r, f,g) ==> F \\<in> Increasing(A, r, f)";
   4.229 -by (Blast_tac 1);
   4.230 -qed "Follows_imp_Increasing_left";
   4.231 -
   4.232 -Goalw [Follows_def]
   4.233 -     "F \\<in> Follows(A, r, f,g) ==> F \\<in> Increasing(A, r, g)";
   4.234 -by (Blast_tac 1);
   4.235 -qed "Follows_imp_Increasing_right";
   4.236 -
   4.237 -Goalw [Follows_def]
   4.238 - "F :Follows(A, r, f, g) ==> F \\<in> Always({s \\<in> state. <f(s),g(s)> \\<in> r})";
   4.239 -by (Blast_tac 1);
   4.240 -qed "Follows_imp_Always";
   4.241 -
   4.242 -Goalw [Follows_def]
   4.243 - "[| F \\<in> Follows(A, r, f, g); k \\<in> A |]  ==> \
   4.244 -\ F: {s \\<in> state. <k,g(s)> \\<in> r } LeadsTo {s \\<in> state. <k,f(s)> \\<in> r}";
   4.245 -by (Blast_tac 1);
   4.246 -qed "Follows_imp_LeadsTo";
   4.247 -
   4.248 -Goal "[| F \\<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \\<in> list(nat) |] \
   4.249 -\  ==> F \\<in> {s \\<in> state. k pfixLe g(s)} LeadsTo {s \\<in> state. k pfixLe f(s)}";
   4.250 -by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
   4.251 -qed "Follows_LeadsTo_pfixLe";
   4.252 -
   4.253 -Goal "[| F \\<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \\<in> list(nat) |] \
   4.254 -\  ==> F \\<in> {s \\<in> state. k pfixGe g(s)} LeadsTo {s \\<in> state. k pfixGe f(s)}";
   4.255 -by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
   4.256 -qed "Follows_LeadsTo_pfixGe";
   4.257 -
   4.258 -Goalw  [Follows_def, Increasing_def, Stable_def]
   4.259 -"[| F \\<in> Always({s \\<in> state. f(s) = g(s)}); F \\<in> Follows(A, r, f, h);  \
   4.260 -\   \\<forall>x \\<in> state. g(x):A |] ==> F \\<in> Follows(A, r, g, h)";
   4.261 -by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
   4.262 -by Auto_tac;
   4.263 -by (res_inst_tac [("C", "{s \\<in> state. f(s)=g(s)}"),
   4.264 -                 ("A", "{s \\<in> state. <ka, h(s)> \\<in> r}"),
   4.265 -                 ("A'", "{s \\<in> state. <ka, f(s)> \\<in> r}")] Always_LeadsTo_weaken 3);
   4.266 -by (eres_inst_tac [("A", "{s \\<in> state. <ka,f(s)> \\<in> r}"), 
   4.267 -                   ("A'", "{s \\<in> state. <ka,f(s)> \\<in> r}")] 
   4.268 -                  Always_Constrains_weaken 1);
   4.269 -by Auto_tac;
   4.270 -by (dtac Always_Int_I 1);
   4.271 -by (assume_tac 1);
   4.272 -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); 
   4.273 -by Auto_tac;
   4.274 -qed "Always_Follows1";
   4.275 -
   4.276 -Goalw [Follows_def, Increasing_def, Stable_def]
   4.277 -"[| F \\<in> Always({s \\<in> state. g(s) = h(s)}); \
   4.278 -\ F \\<in> Follows(A, r, f, g); \\<forall>x \\<in> state. h(x):A |] ==> F \\<in> Follows(A, r, f, h)";
   4.279 -by (full_simp_tac (simpset() addsimps [INT_iff]) 1);
   4.280 -by Auto_tac;
   4.281 -by (thin_tac "k \\<in> A" 3);
   4.282 -by (res_inst_tac [("C", "{s \\<in> state. g(s)=h(s)}"),
   4.283 -                  ("A", "{s \\<in> state. <ka, g(s)> \\<in> r}"),
   4.284 -                  ("A'", "{s \\<in> state. <ka, f(s)> \\<in> r}")] Always_LeadsTo_weaken 3);
   4.285 -by (eres_inst_tac [("A", "{s \\<in> state. <ka, g(s)> \\<in> r}"), 
   4.286 -                   ("A'", "{s \\<in> state. <ka, g(s)> \\<in> r}")] 
   4.287 -                  Always_Constrains_weaken 1);
   4.288 -by Auto_tac;
   4.289 -by (dtac Always_Int_I 1);
   4.290 -by (assume_tac 1);
   4.291 -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); 
   4.292 -by Auto_tac;
   4.293 -qed "Always_Follows2";
   4.294 -
   4.295 -(** Union properties (with the subset ordering) **)
   4.296 -
   4.297 -Goalw [refl_def, SetLe_def] "refl(Pow(A), SetLe(A))";
   4.298 -by Auto_tac;
   4.299 -qed "refl_SetLe";
   4.300 -Addsimps [refl_SetLe];
   4.301 -
   4.302 -Goalw [trans_on_def, SetLe_def] "trans[Pow(A)](SetLe(A))";
   4.303 -by Auto_tac;
   4.304 -qed "trans_on_SetLe";
   4.305 -Addsimps [trans_on_SetLe];
   4.306 -
   4.307 -Goalw [antisym_def, SetLe_def] "antisym(SetLe(A))";
   4.308 -by Auto_tac;
   4.309 -qed "antisym_SetLe";
   4.310 -Addsimps [antisym_SetLe];
   4.311 -
   4.312 -Goalw [part_order_def] "part_order(Pow(A), SetLe(A))";
   4.313 -by Auto_tac;
   4.314 -qed "part_order_SetLe";
   4.315 -Addsimps [part_order_SetLe];
   4.316 -
   4.317 -Goal "[| F \\<in> Increasing.increasing(Pow(A), SetLe(A), f);  \
   4.318 -\        F \\<in> Increasing.increasing(Pow(A), SetLe(A), g) |] \
   4.319 -\    ==> F \\<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
   4.320 -by (res_inst_tac [("h", "op Un")] imp_increasing_comp2 1);
   4.321 -by Auto_tac;
   4.322 -qed "increasing_Un";
   4.323 -
   4.324 -Goal "[| F \\<in> Increasing(Pow(A), SetLe(A), f);  \
   4.325 -\        F \\<in> Increasing(Pow(A), SetLe(A), g) |] \
   4.326 -\    ==> F \\<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
   4.327 -by (res_inst_tac [("h", "op Un")] imp_Increasing_comp2 1);
   4.328 -by Auto_tac;
   4.329 -qed "Increasing_Un";
   4.330 -
   4.331 -Goal "[| F \\<in> Always({s \\<in> state. f1(s) <= f(s)}); \
   4.332 -\    F \\<in> Always({s \\<in> state. g1(s) <= g(s)}) |] \
   4.333 -\     ==> F \\<in> Always({s \\<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})";
   4.334 -by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
   4.335 -by (Blast_tac 1);
   4.336 -qed "Always_Un";
   4.337 -
   4.338 -Goal
   4.339 -"[| F \\<in> Follows(Pow(A), SetLe(A), f1, f); \
   4.340 -\    F \\<in> Follows(Pow(A), SetLe(A), g1, g) |] \
   4.341 -\    ==> F \\<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))";
   4.342 -by (res_inst_tac [("h", "op Un")] imp_Follows_comp2 1);
   4.343 -by Auto_tac;
   4.344 -qed "Follows_Un";
   4.345 -
   4.346 -(** Multiset union properties (with the MultLe ordering) **)
   4.347 -
   4.348 -Goalw [MultLe_def, refl_def] "refl(Mult(A), MultLe(A,r))";
   4.349 -by Auto_tac;
   4.350 -qed "refl_MultLe";
   4.351 -Addsimps [refl_MultLe];
   4.352 -
   4.353 -Goalw [MultLe_def, id_def, lam_def]
   4.354 - "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \\<in> MultLe(A, r)";
   4.355 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   4.356 -qed "MultLe_refl1";
   4.357 -Addsimps [MultLe_refl1];
   4.358 -
   4.359 -Goalw [MultLe_def, id_def, lam_def]
   4.360 - "M \\<in> Mult(A) ==> <M, M> \\<in> MultLe(A, r)";
   4.361 -by Auto_tac;
   4.362 -qed "MultLe_refl2";
   4.363 -Addsimps [MultLe_refl2];
   4.364 -
   4.365 -Goalw [MultLe_def, trans_on_def] "trans[Mult(A)](MultLe(A,r))";
   4.366 -by (auto_tac (claset() addIs [trancl_trans], simpset() addsimps [multirel_def]));
   4.367 -qed "trans_on_MultLe";
   4.368 -Addsimps [trans_on_MultLe];
   4.369 -
   4.370 -Goalw [MultLe_def] "MultLe(A, r)<= (Mult(A) * Mult(A))";
   4.371 -by Auto_tac;
   4.372 -by (dtac (multirel_type RS subsetD) 1);
   4.373 -by Auto_tac;
   4.374 -qed "MultLe_type";
   4.375 -
   4.376 -Goal "[| <M, K> \\<in> MultLe(A, r); <K, N> \\<in> MultLe(A, r) |] ==> <M, N> \\<in> MultLe(A,r)";
   4.377 -by (cut_facts_tac [inst "A" "A" trans_on_MultLe] 1);
   4.378 -by (dtac trans_onD 1);
   4.379 -by (assume_tac 1);
   4.380 -by (auto_tac (claset() addDs [MultLe_type RS subsetD], simpset()));
   4.381 -qed "MultLe_trans";
   4.382 -
   4.383 -Goalw [part_order_def, part_ord_def]
   4.384 -"part_order(A, r) ==> part_ord(A, r-id(A))";
   4.385 -by (rewrite_goal_tac [refl_def, id_def, lam_def, irrefl_def] 1);
   4.386 -by Auto_tac;
   4.387 -by (simp_tac (simpset() addsimps [trans_on_def]) 1);
   4.388 -by Auto_tac;
   4.389 -by (blast_tac (claset() addDs [trans_onD]) 1);
   4.390 -by (full_simp_tac (simpset() addsimps [antisym_def]) 1);
   4.391 -by Auto_tac;
   4.392 -qed "part_order_imp_part_ord";
   4.393 -
   4.394 -Goalw [MultLe_def, antisym_def]
   4.395 -  "part_order(A, r) ==> antisym(MultLe(A,r))";
   4.396 -by (dtac part_order_imp_part_ord 1);
   4.397 -by Auto_tac;
   4.398 -by (dtac irrefl_on_multirel 1);
   4.399 -by (forward_tac [multirel_type RS subsetD] 1);
   4.400 -by (dtac multirel_trans 1);
   4.401 -by (auto_tac (claset(), simpset() addsimps [irrefl_def]));
   4.402 -qed "antisym_MultLe";
   4.403 -Addsimps [antisym_MultLe];
   4.404 -
   4.405 -Goal  "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))";
   4.406 -by (ftac antisym_MultLe 1);
   4.407 -by (auto_tac (claset(), simpset() addsimps [part_order_def]));
   4.408 -qed "part_order_MultLe";
   4.409 -Addsimps [part_order_MultLe];
   4.410 -
   4.411 -Goalw [MultLe_def]
   4.412 -"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \\<in> MultLe(A, r)";
   4.413 -by (case_tac "M=0" 1);
   4.414 -by (auto_tac (claset(), simpset() addsimps (thms"FiniteFun.intros")));
   4.415 -by (subgoal_tac "<0 +# 0, 0 +# M> \\<in> multirel(A, r - id(A))" 1);
   4.416 -by (rtac one_step_implies_multirel 2);
   4.417 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   4.418 -qed "empty_le_MultLe";
   4.419 -Addsimps [empty_le_MultLe];
   4.420 -
   4.421 -Goal "M \\<in> Mult(A) ==> <0, M> \\<in> MultLe(A, r)";
   4.422 -by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
   4.423 -qed "empty_le_MultLe2";
   4.424 -Addsimps [empty_le_MultLe2];
   4.425 -
   4.426 -Goalw [MultLe_def] 
   4.427 -"[| <M, N> \\<in> MultLe(A, r); <K, L> \\<in> MultLe(A, r) |] ==>\
   4.428 -\ <M +# K, N +# L> \\<in> MultLe(A, r)";
   4.429 -by (auto_tac (claset() addIs [munion_multirel_mono1, 
   4.430 -                              munion_multirel_mono2,
   4.431 -                              munion_multirel_mono,
   4.432 -                              multiset_into_Mult], 
   4.433 -               simpset() addsimps [Mult_iff_multiset]));
   4.434 -qed "munion_mono";
   4.435 -
   4.436 -Goal "[| F \\<in> Increasing.increasing(Mult(A), MultLe(A,r), f);  \
   4.437 -\        F \\<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |] \
   4.438 -\    ==> F \\<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
   4.439 -by (res_inst_tac [("h", "munion")] imp_increasing_comp2 1);
   4.440 -by Auto_tac;
   4.441 -qed "increasing_munion";
   4.442 -
   4.443 -Goal "[| F \\<in> Increasing(Mult(A), MultLe(A,r), f);  \
   4.444 -\        F \\<in> Increasing(Mult(A), MultLe(A,r), g)|] \
   4.445 -\    ==> F \\<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
   4.446 -by (res_inst_tac [("h", "munion")] imp_Increasing_comp2 1);
   4.447 -by Auto_tac;
   4.448 -qed "Increasing_munion";
   4.449 -
   4.450 -Goal
   4.451 -"[| F \\<in> Always({s \\<in> state. <f1(s),f(s)> \\<in> MultLe(A,r)}); \
   4.452 -\         F \\<in> Always({s \\<in> state. <g1(s), g(s)> \\<in> MultLe(A,r)});\
   4.453 -\ \\<forall>x \\<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \
   4.454 -\     ==> F \\<in> Always({s \\<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \\<in> MultLe(A,r)})";
   4.455 -by (res_inst_tac [("h", "munion")] imp_Always_comp2 1);
   4.456 -by (ALLGOALS(Asm_full_simp_tac));
   4.457 -by (blast_tac (claset() addIs [munion_mono]) 1);
   4.458 -by (ALLGOALS(Asm_full_simp_tac));
   4.459 -qed "Always_munion";
   4.460 -
   4.461 -Goal
   4.462 -"[| F \\<in> Follows(Mult(A), MultLe(A, r), f1, f); \
   4.463 -\   F \\<in> Follows(Mult(A), MultLe(A, r), g1, g) |] \
   4.464 -\ ==> F \\<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))";
   4.465 -by (res_inst_tac [("h", "munion")] imp_Follows_comp2 1);
   4.466 -by Auto_tac;
   4.467 -qed "Follows_munion";
   4.468 -
   4.469 -(** Used in ClientImp **)
   4.470 -
   4.471 -Goal 
   4.472 -"!!f. [| \\<forall>i \\<in> I. F \\<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \
   4.473 -\ \\<forall>s. \\<forall>i \\<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & \
   4.474 -\                       multiset(f(i, s)) & mset_of(f(i, s))<=A ; \
   4.475 -\  Finite(I); F \\<in> program |] \
   4.476 -\       ==> F \\<in> Follows(Mult(A), \
   4.477 -\                       MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A), \
   4.478 -\                                     %x. msetsum(%i. f(i,  x), I, A))";
   4.479 -by (etac rev_mp 1);
   4.480 -by (dtac Finite_into_Fin 1);
   4.481 -by (etac Fin_induct 1);
   4.482 -by (Asm_simp_tac 1);
   4.483 -by (rtac Follows_constantI 1);
   4.484 -by (ALLGOALS(asm_simp_tac (simpset() addsimps  (thms"FiniteFun.intros"))));
   4.485 -by Auto_tac;
   4.486 -by (resolve_tac [Follows_munion] 1);
   4.487 -by Auto_tac;
   4.488 -qed "Follows_msetsum_UN";
   4.489 -
   4.490 -
     5.1 --- a/src/ZF/UNITY/Follows.thy	Tue Jul 08 11:44:30 2003 +0200
     5.2 +++ b/src/ZF/UNITY/Follows.thy	Wed Jul 09 11:39:34 2003 +0200
     5.3 @@ -1,27 +1,28 @@
     5.4  (*  Title:      ZF/UNITY/Follows
     5.5 -    ID:         $Id$
     5.6 +    ID:         $Id \<in> Follows.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $
     5.7      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     5.8      Copyright   2002  University of Cambridge
     5.9  
    5.10 -The "Follows" relation of Charpentier and Sivilotte
    5.11 -
    5.12  Theory ported from HOL.
    5.13  *)
    5.14  
    5.15 -Follows = SubstAx + Increasing +
    5.16 +header{*The "Follows" relation of Charpentier and Sivilotte*}
    5.17 +
    5.18 +theory Follows = SubstAx + Increasing:
    5.19 +
    5.20  constdefs
    5.21    Follows :: "[i, i, i=>i, i=>i] => i"
    5.22    "Follows(A, r, f, g) == 
    5.23              Increasing(A, r, g) Int
    5.24              Increasing(A, r,f) Int
    5.25 -            Always({s:state. <f(s), g(s)>:r}) Int
    5.26 -           (INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"
    5.27 +            Always({s \<in> state. <f(s), g(s)>:r}) Int
    5.28 +           (\<Inter>k \<in> A. {s \<in> state. <k, g(s)>:r} LeadsTo {s \<in> state. <k,f(s)>:r})"
    5.29  consts
    5.30 -  Incr :: [i=>i]=>i   
    5.31 -  n_Incr :: [i=>i]=>i
    5.32 -  m_Incr :: [i=>i]=>i
    5.33 -  s_Incr :: [i=>i]=>i
    5.34 -  n_Fols :: [i=>i, i=>i]=>i   (infixl "n'_Fols" 65)
    5.35 +  Incr :: "[i=>i]=>i"   
    5.36 +  n_Incr :: "[i=>i]=>i"
    5.37 +  m_Incr :: "[i=>i]=>i"
    5.38 +  s_Incr :: "[i=>i]=>i"
    5.39 +  n_Fols :: "[i=>i, i=>i]=>i"   (infixl "n'_Fols" 65)
    5.40  
    5.41  syntax
    5.42    Follows' :: "[i=>i, i=>i, i, i] => i"
    5.43 @@ -37,4 +38,482 @@
    5.44    "f n_Fols g" == "Follows(nat, Le, f, g)"
    5.45  
    5.46    "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
    5.47 +
    5.48 +
    5.49 +(*Does this hold for "invariant"?*)
    5.50 +
    5.51 +lemma Follows_cong: 
    5.52 +     "[|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')"
    5.53 +by (simp add: Increasing_def Follows_def)
    5.54 +
    5.55 +
    5.56 +lemma subset_Always_comp: 
    5.57 +"[| mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
    5.58 +   Always({x \<in> state. <f(x), g(x)> \<in> r})<=Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
    5.59 +apply (unfold mono1_def metacomp_def)
    5.60 +apply (auto simp add: Always_eq_includes_reachable)
    5.61 +done
    5.62 +
    5.63 +lemma imp_Always_comp: 
    5.64 +"[| F \<in> Always({x \<in> state. <f(x), g(x)> \<in> r});  
    5.65 +    mono1(A, r, B, s, h); \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
    5.66 +    F \<in> Always({x \<in> state. <(h comp f)(x), (h comp g)(x)> \<in> s})"
    5.67 +by (blast intro: subset_Always_comp [THEN subsetD])
    5.68 +
    5.69 +
    5.70 +lemma imp_Always_comp2: 
    5.71 +"[| F \<in> Always({x \<in> state. <f1(x), f(x)> \<in> r});   
    5.72 +    F \<in> Always({x \<in> state. <g1(x), g(x)> \<in> s});  
    5.73 +    mono2(A, r, B, s, C, t, h);  
    5.74 +    \<forall>x \<in> state. f1(x):A & f(x):A & g1(x):B & g(x):B |]  
    5.75 +  ==> F \<in> Always({x \<in> state. <h(f1(x), g1(x)), h(f(x), g(x))> \<in> t})"
    5.76 +apply (auto simp add: Always_eq_includes_reachable mono2_def)
    5.77 +apply (auto dest!: subsetD)
    5.78 +done
    5.79 +
    5.80 +(* comp LeadsTo *)
    5.81 +
    5.82 +lemma subset_LeadsTo_comp: 
    5.83 +"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s);  
    5.84 +        \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
    5.85 +  (\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r}) <=  
    5.86 + (\<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})"
    5.87 +
    5.88 +apply (unfold mono1_def metacomp_def, clarify)
    5.89 +apply (simp_all (no_asm_use) add: INT_iff)
    5.90 +apply auto
    5.91 +apply (rule single_LeadsTo_I)
    5.92 +prefer 2 apply (blast dest: LeadsTo_type [THEN subsetD], auto)
    5.93 +apply (rotate_tac 5)
    5.94 +apply (drule_tac x = "g (sa) " in bspec)
    5.95 +apply (erule_tac [2] LeadsTo_weaken)
    5.96 +apply (auto simp add: part_order_def refl_def)
    5.97 +apply (rule_tac b = "h (g (sa))" in trans_onD)
    5.98 +apply blast
    5.99 +apply auto
   5.100 +done
   5.101 +
   5.102 +lemma imp_LeadsTo_comp: 
   5.103 +"[| F:(\<Inter>j \<in> A. {s \<in> state. <j, g(s)> \<in> r} LeadsTo {s \<in> state. <j,f(s)> \<in> r});  
   5.104 +    mono1(A, r, B, s, h); refl(A,r); trans[B](s);  
   5.105 +    \<forall>x \<in> state. f(x):A & g(x):A |] ==>  
   5.106 +   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})"
   5.107 +apply (rule subset_LeadsTo_comp [THEN subsetD], auto)
   5.108 +done
   5.109 +
   5.110 +lemma imp_LeadsTo_comp_right: 
   5.111 +"[| F \<in> Increasing(B, s, g);  
   5.112 +  \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};  
   5.113 +  mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t);  
   5.114 +  \<forall>x \<in> state. f1(x):A & f(x):A & g(x):B; k \<in> C |] ==>  
   5.115 +  F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g(x))> \<in> t}"
   5.116 +apply (unfold mono2_def Increasing_def)
   5.117 +apply (rule single_LeadsTo_I, auto)
   5.118 +apply (drule_tac x = "g (sa) " and A = B in bspec)
   5.119 +apply auto
   5.120 +apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
   5.121 +apply auto
   5.122 +apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
   5.123 +apply auto
   5.124 +apply (force simp add: part_order_def refl_def)
   5.125 +apply (force simp add: part_order_def refl_def)
   5.126 +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])
   5.127 +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])
   5.128 +apply auto
   5.129 +apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
   5.130 +apply (auto simp add: part_order_def)
   5.131 +done
   5.132 +
   5.133 +lemma imp_LeadsTo_comp_left: 
   5.134 +"[| F \<in> Increasing(A, r, f);  
   5.135 +  \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};  
   5.136 +  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);  
   5.137 +  \<forall>x \<in> state. f(x):A & g1(x):B & g(x):B; k \<in> C |] ==>  
   5.138 +  F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
   5.139 +apply (unfold mono2_def Increasing_def)
   5.140 +apply (rule single_LeadsTo_I, auto)
   5.141 +apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
   5.142 +apply auto
   5.143 +apply (drule_tac x = "g (sa) " in bspec)
   5.144 +apply auto
   5.145 +apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
   5.146 +apply auto
   5.147 +apply (force simp add: part_order_def refl_def)
   5.148 +apply (force simp add: part_order_def refl_def)
   5.149 +apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
   5.150 +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])
   5.151 +apply auto
   5.152 +apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
   5.153 +apply (auto simp add: part_order_def)
   5.154 +done
   5.155 +
   5.156 +(**  This general result is used to prove Follows Un, munion, etc. **)
   5.157 +lemma imp_LeadsTo_comp2: 
   5.158 +"[| F \<in> Increasing(A, r, f1) Int  Increasing(B, s, g);  
   5.159 +  \<forall>j \<in> A. F: {s \<in> state. <j, f(s)> \<in> r} LeadsTo {s \<in> state. <j,f1(s)> \<in> r};  
   5.160 +  \<forall>j \<in> B. F: {x \<in> state. <j, g(x)> \<in> s} LeadsTo {x \<in> state. <j,g1(x)> \<in> s};  
   5.161 +  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t);  
   5.162 +  \<forall>x \<in> state. f(x):A & g1(x):B & f1(x):A &g(x):B; k \<in> C |] 
   5.163 +  ==> F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f1(x), g1(x))> \<in> t}"
   5.164 +apply (rule_tac B = "{x \<in> state. <k, h (f1 (x), g (x))> \<in> t}" in LeadsTo_Trans)
   5.165 +apply (blast intro: imp_LeadsTo_comp_right)
   5.166 +apply (blast intro: imp_LeadsTo_comp_left)
   5.167 +done
   5.168 +
   5.169 +(* Follows type *)
   5.170 +lemma Follows_type: "Follows(A, r, f, g)<=program"
   5.171 +apply (unfold Follows_def)
   5.172 +apply (blast dest: Increasing_type [THEN subsetD])
   5.173 +done
   5.174 +
   5.175 +lemma Follows_into_program [TC]: "F \<in> Follows(A, r, f, g) ==> F \<in> program"
   5.176 +by (blast dest: Follows_type [THEN subsetD])
   5.177 +
   5.178 +lemma FollowsD: 
   5.179 +"F \<in> Follows(A, r, f, g)==>  
   5.180 +  F \<in> program & (\<exists>a. a \<in> A) & (\<forall>x \<in> state. f(x):A & g(x):A)"
   5.181 +apply (unfold Follows_def)
   5.182 +apply (blast dest: IncreasingD)
   5.183 +done
   5.184 +
   5.185 +lemma Follows_constantI: 
   5.186 + "[| F \<in> program; c \<in> A; refl(A, r) |] ==> F \<in> Follows(A, r, %x. c, %x. c)"
   5.187 +apply (unfold Follows_def, auto)
   5.188 +apply (auto simp add: refl_def)
   5.189 +done
   5.190 +
   5.191 +lemma subset_Follows_comp: 
   5.192 +"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]  
   5.193 +   ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)"
   5.194 +apply (unfold Follows_def, clarify)
   5.195 +apply (frule_tac f = g in IncreasingD)
   5.196 +apply (frule_tac f = f in IncreasingD)
   5.197 +apply (rule IntI)
   5.198 +apply (rule_tac [2] h = h in imp_LeadsTo_comp)
   5.199 +prefer 5 apply assumption
   5.200 +apply (auto intro: imp_Increasing_comp imp_Always_comp simp del: INT_simps)
   5.201 +done
   5.202 +
   5.203 +lemma imp_Follows_comp: 
   5.204 +"[| F \<in> Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |]  
   5.205 +  ==>  F \<in> Follows(B, s,  h comp f, h comp g)"
   5.206 +apply (blast intro: subset_Follows_comp [THEN subsetD])
   5.207 +done
   5.208 +
   5.209 +(* 2-place monotone operation \<in> this general result is used to prove Follows_Un, Follows_munion *)
   5.210 +
   5.211 +(* 2-place monotone operation \<in> this general result is 
   5.212 +   used to prove Follows_Un, Follows_munion *)
   5.213 +lemma imp_Follows_comp2: 
   5.214 +"[| F \<in> Follows(A, r, f1, f);  F \<in> Follows(B, s, g1, g);  
   5.215 +   mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |]  
   5.216 +   ==> F \<in> Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))"
   5.217 +apply (unfold Follows_def, clarify)
   5.218 +apply (frule_tac f = g in IncreasingD)
   5.219 +apply (frule_tac f = f in IncreasingD)
   5.220 +apply (rule IntI, safe)
   5.221 +apply (rule_tac [3] h = h in imp_Always_comp2)
   5.222 +prefer 5 apply assumption
   5.223 +apply (rule_tac [2] h = h in imp_Increasing_comp2)
   5.224 +prefer 4 apply assumption
   5.225 +apply (rule_tac h = h in imp_Increasing_comp2)
   5.226 +prefer 3 apply assumption
   5.227 +apply simp_all
   5.228 +apply (blast dest!: IncreasingD)
   5.229 +apply (rule_tac h = h in imp_LeadsTo_comp2)
   5.230 +prefer 4 apply assumption
   5.231 +apply auto
   5.232 +  prefer 3 apply (simp add: mono2_def) 
   5.233 +apply (blast dest: IncreasingD)+
   5.234 +done
   5.235 +
   5.236 +
   5.237 +lemma Follows_trans:
   5.238 +     "[| F \<in> Follows(A, r, f, g);  F \<in> Follows(A,r, g, h);  
   5.239 +         trans[A](r) |] ==> F \<in> Follows(A, r, f, h)"
   5.240 +apply (frule_tac f = f in FollowsD)
   5.241 +apply (frule_tac f = g in FollowsD)
   5.242 +apply (simp add: Follows_def)
   5.243 +apply (simp add: Always_eq_includes_reachable INT_iff, auto)
   5.244 +apply (rule_tac [2] B = "{s \<in> state. <k, g (s) > \<in> r}" in LeadsTo_Trans)
   5.245 +apply (rule_tac b = "g (x) " in trans_onD)
   5.246 +apply blast+
   5.247 +done
   5.248 +
   5.249 +(** Destruction rules for Follows **)
   5.250 +
   5.251 +lemma Follows_imp_Increasing_left: 
   5.252 +     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, f)"
   5.253 +by (unfold Follows_def, blast)
   5.254 +
   5.255 +lemma Follows_imp_Increasing_right: 
   5.256 +     "F \<in> Follows(A, r, f,g) ==> F \<in> Increasing(A, r, g)"
   5.257 +by (unfold Follows_def, blast)
   5.258 +
   5.259 +lemma Follows_imp_Always: 
   5.260 + "F :Follows(A, r, f, g) ==> F \<in> Always({s \<in> state. <f(s),g(s)> \<in> r})"
   5.261 +by (unfold Follows_def, blast)
   5.262 +
   5.263 +lemma Follows_imp_LeadsTo: 
   5.264 + "[| F \<in> Follows(A, r, f, g); k \<in> A |]  ==>  
   5.265 +  F: {s \<in> state. <k,g(s)> \<in> r } LeadsTo {s \<in> state. <k,f(s)> \<in> r}"
   5.266 +by (unfold Follows_def, blast)
   5.267 +
   5.268 +lemma Follows_LeadsTo_pfixLe:
   5.269 +     "[| F \<in> Follows(list(nat), gen_prefix(nat, Le), f, g); k \<in> list(nat) |]  
   5.270 +   ==> F \<in> {s \<in> state. k pfixLe g(s)} LeadsTo {s \<in> state. k pfixLe f(s)}"
   5.271 +by (blast intro: Follows_imp_LeadsTo)
   5.272 +
   5.273 +lemma Follows_LeadsTo_pfixGe:
   5.274 +     "[| F \<in> Follows(list(nat), gen_prefix(nat, Ge), f, g); k \<in> list(nat) |]  
   5.275 +   ==> F \<in> {s \<in> state. k pfixGe g(s)} LeadsTo {s \<in> state. k pfixGe f(s)}"
   5.276 +by (blast intro: Follows_imp_LeadsTo)
   5.277 +
   5.278 +lemma Always_Follows1: 
   5.279 +"[| F \<in> Always({s \<in> state. f(s) = g(s)}); F \<in> Follows(A, r, f, h);   
   5.280 +    \<forall>x \<in> state. g(x):A |] ==> F \<in> Follows(A, r, g, h)"
   5.281 +apply (unfold Follows_def Increasing_def Stable_def)
   5.282 +apply (simp add: INT_iff, auto)
   5.283 +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)
   5.284 +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)
   5.285 +apply auto
   5.286 +apply (drule Always_Int_I, assumption)
   5.287 +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)
   5.288 +apply auto
   5.289 +done
   5.290 +
   5.291 +lemma Always_Follows2: 
   5.292 +"[| F \<in> Always({s \<in> state. g(s) = h(s)});  
   5.293 +  F \<in> Follows(A, r, f, g); \<forall>x \<in> state. h(x):A |] ==> F \<in> Follows(A, r, f, h)"
   5.294 +apply (unfold Follows_def Increasing_def Stable_def)
   5.295 +apply (simp (no_asm_use) add: INT_iff)
   5.296 +apply auto
   5.297 +apply (erule_tac [3] V = "k \<in> A" in thin_rl)
   5.298 +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)
   5.299 +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)
   5.300 +apply auto
   5.301 +apply (drule Always_Int_I, assumption)
   5.302 +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)
   5.303 +apply auto
   5.304 +done
   5.305 +
   5.306 +(** Union properties (with the subset ordering) **)
   5.307 +
   5.308 +lemma refl_SetLe [simp]: "refl(Pow(A), SetLe(A))"
   5.309 +by (unfold refl_def SetLe_def, auto)
   5.310 +
   5.311 +lemma trans_on_SetLe [simp]: "trans[Pow(A)](SetLe(A))"
   5.312 +by (unfold trans_on_def SetLe_def, auto)
   5.313 +
   5.314 +lemma antisym_SetLe [simp]: "antisym(SetLe(A))"
   5.315 +by (unfold antisym_def SetLe_def, auto)
   5.316 +
   5.317 +lemma part_order_SetLe [simp]: "part_order(Pow(A), SetLe(A))"
   5.318 +by (unfold part_order_def, auto)
   5.319 +
   5.320 +lemma increasing_Un:
   5.321 +     "[| F \<in> Increasing.increasing(Pow(A), SetLe(A), f);   
   5.322 +         F \<in> Increasing.increasing(Pow(A), SetLe(A), g) |]  
   5.323 +     ==> F \<in> Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
   5.324 +by (rule_tac h = "op Un" in imp_increasing_comp2, auto)
   5.325 +
   5.326 +lemma Increasing_Un:
   5.327 +     "[| F \<in> Increasing(Pow(A), SetLe(A), f);   
   5.328 +         F \<in> Increasing(Pow(A), SetLe(A), g) |]  
   5.329 +     ==> F \<in> Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))"
   5.330 +by (rule_tac h = "op Un" in imp_Increasing_comp2, auto)
   5.331 +
   5.332 +lemma Always_Un:
   5.333 +     "[| F \<in> Always({s \<in> state. f1(s) <= f(s)});  
   5.334 +     F \<in> Always({s \<in> state. g1(s) <= g(s)}) |]  
   5.335 +      ==> F \<in> Always({s \<in> state. f1(s) Un g1(s) <= f(s) Un g(s)})"
   5.336 +by (simp add: Always_eq_includes_reachable, blast)
   5.337 +
   5.338 +lemma Follows_Un: 
   5.339 +"[| F \<in> Follows(Pow(A), SetLe(A), f1, f);  
   5.340 +     F \<in> Follows(Pow(A), SetLe(A), g1, g) |]  
   5.341 +     ==> F \<in> Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))"
   5.342 +by (rule_tac h = "op Un" in imp_Follows_comp2, auto)
   5.343 +
   5.344 +(** Multiset union properties (with the MultLe ordering) **)
   5.345 +
   5.346 +lemma refl_MultLe [simp]: "refl(Mult(A), MultLe(A,r))"
   5.347 +by (unfold MultLe_def refl_def, auto)
   5.348 +
   5.349 +lemma MultLe_refl1 [simp]: 
   5.350 + "[| multiset(M); mset_of(M)<=A |] ==> <M, M> \<in> MultLe(A, r)"
   5.351 +apply (unfold MultLe_def id_def lam_def)
   5.352 +apply (auto simp add: Mult_iff_multiset)
   5.353 +done
   5.354 +
   5.355 +lemma MultLe_refl2 [simp]: "M \<in> Mult(A) ==> <M, M> \<in> MultLe(A, r)"
   5.356 +by (unfold MultLe_def id_def lam_def, auto)
   5.357 +
   5.358 +
   5.359 +lemma trans_on_MultLe [simp]: "trans[Mult(A)](MultLe(A,r))"
   5.360 +apply (unfold MultLe_def trans_on_def)
   5.361 +apply (auto intro: trancl_trans simp add: multirel_def)
   5.362 +done
   5.363 +
   5.364 +lemma MultLe_type: "MultLe(A, r)<= (Mult(A) * Mult(A))"
   5.365 +apply (unfold MultLe_def, auto)
   5.366 +apply (drule multirel_type [THEN subsetD], auto)
   5.367 +done
   5.368 +
   5.369 +lemma MultLe_trans:
   5.370 +     "[| <M,K> \<in> MultLe(A,r); <K,N> \<in> MultLe(A,r) |] ==> <M,N> \<in> MultLe(A,r)"
   5.371 +apply (cut_tac A=A in trans_on_MultLe)
   5.372 +apply (drule trans_onD, assumption)
   5.373 +apply (auto dest: MultLe_type [THEN subsetD])
   5.374 +done
   5.375 +
   5.376 +lemma part_order_imp_part_ord: 
   5.377 +     "part_order(A, r) ==> part_ord(A, r-id(A))"
   5.378 +apply (unfold part_order_def part_ord_def)
   5.379 +apply (simp add: refl_def id_def lam_def irrefl_def, auto)
   5.380 +apply (simp (no_asm) add: trans_on_def)
   5.381 +apply auto
   5.382 +apply (blast dest: trans_onD)
   5.383 +apply (simp (no_asm_use) add: antisym_def)
   5.384 +apply auto
   5.385 +done
   5.386 +
   5.387 +lemma antisym_MultLe [simp]: 
   5.388 +  "part_order(A, r) ==> antisym(MultLe(A,r))"
   5.389 +apply (unfold MultLe_def antisym_def)
   5.390 +apply (drule part_order_imp_part_ord, auto)
   5.391 +apply (drule irrefl_on_multirel)
   5.392 +apply (frule multirel_type [THEN subsetD])
   5.393 +apply (drule multirel_trans)
   5.394 +apply (auto simp add: irrefl_def)
   5.395 +done
   5.396 +
   5.397 +lemma part_order_MultLe [simp]:
   5.398 +     "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))"
   5.399 +apply (frule antisym_MultLe)
   5.400 +apply (auto simp add: part_order_def)
   5.401 +done
   5.402 +
   5.403 +lemma empty_le_MultLe [simp]: 
   5.404 +"[| multiset(M); mset_of(M)<= A|] ==> <0, M> \<in> MultLe(A, r)"
   5.405 +apply (unfold MultLe_def)
   5.406 +apply (case_tac "M=0")
   5.407 +apply (auto simp add: FiniteFun.intros)
   5.408 +apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (A, r - id (A))")
   5.409 +apply (rule_tac [2] one_step_implies_multirel)
   5.410 +apply (auto simp add: Mult_iff_multiset)
   5.411 +done
   5.412 +
   5.413 +lemma empty_le_MultLe2 [simp]: "M \<in> Mult(A) ==> <0, M> \<in> MultLe(A, r)"
   5.414 +by (simp add: Mult_iff_multiset)
   5.415 +
   5.416 +lemma munion_mono: 
   5.417 +"[| <M, N> \<in> MultLe(A, r); <K, L> \<in> MultLe(A, r) |] ==> 
   5.418 +  <M +# K, N +# L> \<in> MultLe(A, r)"
   5.419 +apply (unfold MultLe_def)
   5.420 +apply (auto intro: munion_multirel_mono1 munion_multirel_mono2
   5.421 +       munion_multirel_mono multiset_into_Mult simp add: Mult_iff_multiset)
   5.422 +done
   5.423 +
   5.424 +lemma increasing_munion:
   5.425 +     "[| F \<in> Increasing.increasing(Mult(A), MultLe(A,r), f);   
   5.426 +         F \<in> Increasing.increasing(Mult(A), MultLe(A,r), g) |]  
   5.427 +     ==> F \<in> Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
   5.428 +by (rule_tac h = munion in imp_increasing_comp2, auto)
   5.429 +
   5.430 +lemma Increasing_munion:
   5.431 +     "[| F \<in> Increasing(Mult(A), MultLe(A,r), f);   
   5.432 +         F \<in> Increasing(Mult(A), MultLe(A,r), g)|]  
   5.433 +     ==> F \<in> Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))"
   5.434 +by (rule_tac h = munion in imp_Increasing_comp2, auto)
   5.435 +
   5.436 +lemma Always_munion: 
   5.437 +"[| F \<in> Always({s \<in> state. <f1(s),f(s)> \<in> MultLe(A,r)});  
   5.438 +          F \<in> Always({s \<in> state. <g1(s), g(s)> \<in> MultLe(A,r)}); 
   5.439 +  \<forall>x \<in> state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|]  
   5.440 +      ==> F \<in> Always({s \<in> state. <f1(s) +# g1(s), f(s) +# g(s)> \<in> MultLe(A,r)})"
   5.441 +apply (rule_tac h = munion in imp_Always_comp2, simp_all)
   5.442 +apply (blast intro: munion_mono, simp_all)
   5.443 +done
   5.444 +
   5.445 +lemma Follows_munion: 
   5.446 +"[| F \<in> Follows(Mult(A), MultLe(A, r), f1, f);  
   5.447 +    F \<in> Follows(Mult(A), MultLe(A, r), g1, g) |]  
   5.448 +  ==> F \<in> Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))"
   5.449 +by (rule_tac h = munion in imp_Follows_comp2, auto)
   5.450 +
   5.451 +(** Used in ClientImp **)
   5.452 +
   5.453 +lemma Follows_msetsum_UN: 
   5.454 +"!!f. [| \<forall>i \<in> I. F \<in> Follows(Mult(A), MultLe(A, r), f'(i), f(i));  
   5.455 +  \<forall>s. \<forall>i \<in> I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A &  
   5.456 +                        multiset(f(i, s)) & mset_of(f(i, s))<=A ;  
   5.457 +   Finite(I); F \<in> program |]  
   5.458 +        ==> F \<in> Follows(Mult(A),  
   5.459 +                        MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A),  
   5.460 +                                      %x. msetsum(%i. f(i,  x), I, A))"
   5.461 +apply (erule rev_mp)
   5.462 +apply (drule Finite_into_Fin)
   5.463 +apply (erule Fin_induct)
   5.464 +apply (simp (no_asm_simp))
   5.465 +apply (rule Follows_constantI)
   5.466 +apply (simp_all (no_asm_simp) add: FiniteFun.intros)
   5.467 +apply auto
   5.468 +apply (rule Follows_munion, auto)
   5.469 +done
   5.470 +
   5.471 +ML
   5.472 +{*
   5.473 +val Follows_cong = thm "Follows_cong";
   5.474 +val subset_Always_comp = thm "subset_Always_comp";
   5.475 +val imp_Always_comp = thm "imp_Always_comp";
   5.476 +val imp_Always_comp2 = thm "imp_Always_comp2";
   5.477 +val subset_LeadsTo_comp = thm "subset_LeadsTo_comp";
   5.478 +val imp_LeadsTo_comp = thm "imp_LeadsTo_comp";
   5.479 +val imp_LeadsTo_comp_right = thm "imp_LeadsTo_comp_right";
   5.480 +val imp_LeadsTo_comp_left = thm "imp_LeadsTo_comp_left";
   5.481 +val imp_LeadsTo_comp2 = thm "imp_LeadsTo_comp2";
   5.482 +val Follows_type = thm "Follows_type";
   5.483 +val Follows_into_program = thm "Follows_into_program";
   5.484 +val FollowsD = thm "FollowsD";
   5.485 +val Follows_constantI = thm "Follows_constantI";
   5.486 +val subset_Follows_comp = thm "subset_Follows_comp";
   5.487 +val imp_Follows_comp = thm "imp_Follows_comp";
   5.488 +val imp_Follows_comp2 = thm "imp_Follows_comp2";
   5.489 +val Follows_trans = thm "Follows_trans";
   5.490 +val Follows_imp_Increasing_left = thm "Follows_imp_Increasing_left";
   5.491 +val Follows_imp_Increasing_right = thm "Follows_imp_Increasing_right";
   5.492 +val Follows_imp_Always = thm "Follows_imp_Always";
   5.493 +val Follows_imp_LeadsTo = thm "Follows_imp_LeadsTo";
   5.494 +val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe";
   5.495 +val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe";
   5.496 +val Always_Follows1 = thm "Always_Follows1";
   5.497 +val Always_Follows2 = thm "Always_Follows2";
   5.498 +val refl_SetLe = thm "refl_SetLe";
   5.499 +val trans_on_SetLe = thm "trans_on_SetLe";
   5.500 +val antisym_SetLe = thm "antisym_SetLe";
   5.501 +val part_order_SetLe = thm "part_order_SetLe";
   5.502 +val increasing_Un = thm "increasing_Un";
   5.503 +val Increasing_Un = thm "Increasing_Un";
   5.504 +val Always_Un = thm "Always_Un";
   5.505 +val Follows_Un = thm "Follows_Un";
   5.506 +val refl_MultLe = thm "refl_MultLe";
   5.507 +val MultLe_refl1 = thm "MultLe_refl1";
   5.508 +val MultLe_refl2 = thm "MultLe_refl2";
   5.509 +val trans_on_MultLe = thm "trans_on_MultLe";
   5.510 +val MultLe_type = thm "MultLe_type";
   5.511 +val MultLe_trans = thm "MultLe_trans";
   5.512 +val part_order_imp_part_ord = thm "part_order_imp_part_ord";
   5.513 +val antisym_MultLe = thm "antisym_MultLe";
   5.514 +val part_order_MultLe = thm "part_order_MultLe";
   5.515 +val empty_le_MultLe = thm "empty_le_MultLe";
   5.516 +val empty_le_MultLe2 = thm "empty_le_MultLe2";
   5.517 +val munion_mono = thm "munion_mono";
   5.518 +val increasing_munion = thm "increasing_munion";
   5.519 +val Increasing_munion = thm "Increasing_munion";
   5.520 +val Always_munion = thm "Always_munion";
   5.521 +val Follows_munion = thm "Follows_munion";
   5.522 +val Follows_msetsum_UN = thm "Follows_msetsum_UN";
   5.523 +*}
   5.524 +
   5.525  end
     6.1 --- a/src/ZF/UNITY/Guar.ML	Tue Jul 08 11:44:30 2003 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,548 +0,0 @@
     6.4 -(*  Title:      ZF/UNITY/Guar.ML
     6.5 -    ID:         $Id \\<in> Guar.ML,v 1.8 2003/06/27 11:15:41 paulson Exp $
     6.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     6.7 -    Copyright   2001  University of Cambridge
     6.8 -
     6.9 -Guarantees, etc.
    6.10 -
    6.11 -From Chandy and Sanders, "Reasoning About Program Composition"
    6.12 -Revised by Sidi Ehmety on January 2001
    6.13 -
    6.14 -Proofs ported from HOL.
    6.15 -*)
    6.16 -
    6.17 -Goal "OK(cons(i, I), F) <-> \
    6.18 -\ (i \\<in> I & OK(I, F)) | (i\\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))";
    6.19 -by (asm_full_simp_tac (simpset() addsimps [OK_iff_ok]) 1);
    6.20 -(** Auto_tac proves the goal in one-step, but takes more time **)
    6.21 -by Safe_tac;
    6.22 -by (ALLGOALS(Clarify_tac));
    6.23 -by (REPEAT(blast_tac (claset() addIs [ok_sym]) 10));
    6.24 -by (REPEAT(Blast_tac 1));
    6.25 -qed "OK_cons_iff";
    6.26 -
    6.27 -(*** existential properties ***)
    6.28 -
    6.29 -Goalw [ex_prop_def] "ex_prop(X) ==> X\\<subseteq>program";
    6.30 -by (Asm_simp_tac 1);
    6.31 -qed "ex_imp_subset_program";
    6.32 -
    6.33 -Goalw [ex_prop_def]
    6.34 - "GG \\<in> Fin(program) ==> (ex_prop(X) \
    6.35 -\ --> GG Int X\\<noteq>0 --> OK(GG, (%G. G)) -->(\\<Squnion>G \\<in> GG. G):X)";
    6.36 -by (etac Fin_induct 1);
    6.37 -by (ALLGOALS(asm_full_simp_tac 
    6.38 -         (simpset() addsimps [OK_cons_iff])));
    6.39 -(* Auto_tac proves the goal in one step *)
    6.40 -by (safe_tac (claset() addSEs [not_emptyE]));
    6.41 -by (ALLGOALS(Asm_full_simp_tac));
    6.42 -by (Fast_tac 1);
    6.43 -qed_spec_mp "ex1";
    6.44 -
    6.45 -Goalw [ex_prop_def]
    6.46 -"X\\<subseteq>program ==> \
    6.47 -\(\\<forall>GG. GG \\<in> Fin(program) & GG Int X \\<noteq> 0 --> OK(GG,(%G. G))-->(\\<Squnion>G \\<in> GG. G):X)\
    6.48 -\  --> ex_prop(X)";
    6.49 -by (Clarify_tac 1);
    6.50 -by (dres_inst_tac [("x", "{F,G}")] spec 1);
    6.51 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [OK_iff_ok])));
    6.52 -by Safe_tac;
    6.53 -by (auto_tac (claset() addIs [ok_sym], simpset()));
    6.54 -qed "ex2";
    6.55 -
    6.56 -(*Chandy & Sanders take this as a definition*)
    6.57 -
    6.58 -Goal "ex_prop(X) <-> (X\\<subseteq>program & \
    6.59 -\ (\\<forall>GG. GG \\<in> Fin(program) & GG Int X \\<noteq> 0& OK(GG,( %G. G))-->(\\<Squnion>G \\<in> GG. G):X))";
    6.60 -by Auto_tac;
    6.61 -by (ALLGOALS(blast_tac (claset() addIs [ex1, ex2 RS mp] 
    6.62 -                                 addDs [ex_imp_subset_program])));
    6.63 -qed "ex_prop_finite";
    6.64 -
    6.65 -(* Equivalent definition of ex_prop given at the end of section 3*)
    6.66 -Goalw [ex_prop_def, component_of_def]
    6.67 -"ex_prop(X) <-> \
    6.68 -\ X\\<subseteq>program & (\\<forall>G \\<in> program. (G \\<in> X <-> (\\<forall>H \\<in> program. (G component_of H) --> H \\<in> X)))";
    6.69 -by Safe_tac;
    6.70 -by (stac Join_commute 4);
    6.71 -by (dtac  ok_sym 4);
    6.72 -by (dres_inst_tac [("x", "G")] bspec 4);
    6.73 -by (dres_inst_tac [("x", "F")] bspec 3);
    6.74 -by Safe_tac;
    6.75 -by (REPEAT(Force_tac 1));
    6.76 -qed "ex_prop_equiv";
    6.77 -
    6.78 -(*** universal properties ***)
    6.79 -
    6.80 -Goalw [uv_prop_def] "uv_prop(X)==> X\\<subseteq>program";
    6.81 -by (Asm_simp_tac 1);
    6.82 -qed "uv_imp_subset_program";
    6.83 -
    6.84 -Goalw [uv_prop_def]
    6.85 -     "GG \\<in> Fin(program) ==> \
    6.86 -\ (uv_prop(X)--> GG \\<subseteq> X & OK(GG, (%G. G)) --> (\\<Squnion>G \\<in> GG. G):X)";
    6.87 -by (etac Fin_induct 1);
    6.88 -by (auto_tac (claset(), simpset() addsimps 
    6.89 -           [OK_cons_iff]));
    6.90 -qed_spec_mp "uv1";
    6.91 -
    6.92 -Goalw [uv_prop_def]
    6.93 -"X\\<subseteq>program  ==> (\\<forall>GG. GG \\<in> Fin(program) & GG \\<subseteq> X & OK(GG,(%G. G)) \
    6.94 -\ --> (\\<Squnion>G \\<in> GG. G):X)  --> uv_prop(X)";
    6.95 -by Auto_tac;
    6.96 -by (Clarify_tac 2);
    6.97 -by (dres_inst_tac [("x", "{F,G}")] spec 2);
    6.98 -by (dres_inst_tac [("x", "0")] spec 1);
    6.99 -by (auto_tac (claset() addDs [ok_sym], 
   6.100 -    simpset() addsimps [OK_iff_ok]));
   6.101 -qed "uv2";
   6.102 -
   6.103 -(*Chandy & Sanders take this as a definition*)
   6.104 -Goal 
   6.105 -"uv_prop(X) <-> X\\<subseteq>program & \
   6.106 -\ (\\<forall>GG. GG \\<in> Fin(program) & GG \\<subseteq> X & OK(GG, %G. G) --> (\\<Squnion>G \\<in> GG. G): X)";
   6.107 -by Auto_tac;
   6.108 -by (REPEAT(blast_tac (claset() addIs [uv1,uv2 RS mp]
   6.109 -                               addDs [uv_imp_subset_program]) 1));
   6.110 -qed "uv_prop_finite";
   6.111 -
   6.112 -(*** guarantees ***)
   6.113 -val major::prems = Goal
   6.114 -     "[| (!!G. [| F ok G; F Join G \\<in> X; G \\<in> program |] ==> F Join G \\<in> Y); F \\<in> program |]  \
   6.115 -\   ==> F \\<in> X guarantees Y";
   6.116 -by (cut_facts_tac prems 1);
   6.117 -by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
   6.118 -by (blast_tac (claset() addIs [major]) 1);
   6.119 -qed "guaranteesI";
   6.120 -
   6.121 -Goalw [guar_def, component_def]
   6.122 -     "[| F \\<in> X guarantees Y;  F ok G;  F Join G \\<in> X; G \\<in> program |] \
   6.123 -\     ==> F Join G \\<in> Y";
   6.124 -by (Asm_full_simp_tac 1);
   6.125 -qed "guaranteesD";
   6.126 -
   6.127 -(*This version of guaranteesD matches more easily in the conclusion
   6.128 -  The major premise can no longer be  F\\<subseteq>H since we need to reason about G*)
   6.129 -
   6.130 -Goalw [guar_def]
   6.131 -     "[| F \\<in> X guarantees Y;  F Join G = H;  H \\<in> X;  F ok G; G \\<in> program |] \
   6.132 -\     ==> H \\<in> Y";
   6.133 -by (Blast_tac 1);
   6.134 -qed "component_guaranteesD";
   6.135 -
   6.136 -Goalw [guar_def]
   6.137 -     "[| F \\<in> X guarantees X'; Y \\<subseteq> X; X' \\<subseteq> Y' |] ==> F \\<in> Y guarantees Y'";
   6.138 -by Auto_tac;
   6.139 -qed "guarantees_weaken";
   6.140 -
   6.141 -Goalw [guar_def] "X \\<subseteq> Y \
   6.142 -\  ==> X guarantees Y = program";
   6.143 -by (Blast_tac 1);
   6.144 -qed "subset_imp_guarantees_program";
   6.145 -
   6.146 -(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   6.147 -Goalw [guar_def] "[| X \\<subseteq> Y; F \\<in> program |] \
   6.148 -\  ==> F \\<in> X guarantees Y";
   6.149 -by (Blast_tac 1);
   6.150 -qed "subset_imp_guarantees";
   6.151 -
   6.152 -Goalw [component_of_def] 
   6.153 -"F ok G ==> F component_of (F Join G)";
   6.154 -by (Blast_tac 1);
   6.155 -qed "component_of_Join1";
   6.156 -
   6.157 -Goal "F ok G ==> G component_of (F Join G)";
   6.158 -by (stac Join_commute 1);
   6.159 -by (blast_tac (claset() addIs [ok_sym, component_of_Join1]) 1);
   6.160 -qed "component_of_Join2";
   6.161 -
   6.162 -(*Remark at end of section 4.1 *)
   6.163 -Goalw [guar_def, component_of_def] 
   6.164 -"ex_prop(Y) ==> (Y = (program guarantees Y))";
   6.165 -by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   6.166 -by (Clarify_tac 1);
   6.167 -by (rtac equalityI 1);
   6.168 -by Safe_tac;
   6.169 -by (dres_inst_tac [("x", "x")] bspec 2);
   6.170 -by (dres_inst_tac [("x", "x")] bspec 4);
   6.171 -by (dtac iff_sym 5);
   6.172 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_Join1])));
   6.173 -by (etac iffE 3);
   6.174 -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   6.175 -by Safe_tac;
   6.176 -by (REPEAT(Force_tac 1));
   6.177 -qed "ex_prop_imp";
   6.178 -
   6.179 -Goalw [guar_def] "(Y = program guarantees Y) ==> ex_prop(Y)";
   6.180 -by (asm_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   6.181 -by Safe_tac;
   6.182 -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   6.183 -by (dtac sym 2);
   6.184 -by (ALLGOALS(etac equalityE));
   6.185 -by (REPEAT(Force_tac 1));
   6.186 -qed "guarantees_imp";
   6.187 -
   6.188 -Goal "(ex_prop(Y)) <-> (Y = program guarantees Y)";
   6.189 -by (blast_tac (claset() addIs [ex_prop_imp, guarantees_imp]) 1);
   6.190 -qed "ex_prop_equiv2";
   6.191 -
   6.192 -(** Distributive laws.  Re-orient to perform miniscoping **)
   6.193 -
   6.194 -Goalw [guar_def]
   6.195 -     "i \\<in> I ==>(\\<Union>i \\<in> I. X(i)) guarantees Y = (\\<Inter>i \\<in> I. X(i) guarantees Y)";
   6.196 -by (rtac equalityI 1);
   6.197 -by Safe_tac;
   6.198 -by (Force_tac 2);
   6.199 -by (REPEAT(Blast_tac 1));
   6.200 -qed "guarantees_UN_left";
   6.201 -
   6.202 -Goalw [guar_def]
   6.203 -     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
   6.204 -by (rtac equalityI 1);
   6.205 -by Safe_tac;
   6.206 -by (REPEAT(Blast_tac 1));
   6.207 -qed "guarantees_Un_left";
   6.208 -
   6.209 -Goalw [guar_def]
   6.210 -     "i \\<in> I ==> X guarantees (\\<Inter>i \\<in> I. Y(i)) = (\\<Inter>i \\<in> I. X guarantees Y(i))";
   6.211 -by (rtac equalityI 1);
   6.212 -by Safe_tac;
   6.213 -by (REPEAT(Blast_tac 1));
   6.214 -qed "guarantees_INT_right";
   6.215 -
   6.216 -Goalw [guar_def]
   6.217 -     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
   6.218 -by (Blast_tac 1);
   6.219 -qed "guarantees_Int_right";
   6.220 -
   6.221 -Goal "[| F \\<in> Z guarantees X;  F \\<in> Z guarantees Y |] \
   6.222 -\    ==> F \\<in> Z guarantees (X Int Y)";
   6.223 -by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
   6.224 -qed "guarantees_Int_right_I";
   6.225 -
   6.226 -Goal "i \\<in> I==> (F \\<in> X guarantees (\\<Inter>i \\<in> I. Y(i))) <-> \
   6.227 -\     (\\<forall>i \\<in> I. F \\<in> X guarantees Y(i))";
   6.228 -by (asm_simp_tac (simpset() addsimps [guarantees_INT_right, INT_iff]) 1);
   6.229 -by (Blast_tac 1);
   6.230 -qed "guarantees_INT_right_iff";
   6.231 -
   6.232 -
   6.233 -Goalw [guar_def] "(X guarantees Y) = (program guarantees ((program-X) Un Y))";
   6.234 -by Auto_tac;
   6.235 -qed "shunting";
   6.236 -
   6.237 -Goalw [guar_def] "(X guarantees Y) = (program - Y) guarantees (program -X)";
   6.238 -by (Blast_tac 1);
   6.239 -qed "contrapositive";
   6.240 -
   6.241 -(** The following two can be expressed using intersection and subset, which
   6.242 -    is more faithful to the text but looks cryptic.
   6.243 -**)
   6.244 -
   6.245 -Goalw [guar_def]
   6.246 -    "[| F \\<in> V guarantees X;  F \\<in> (X Int Y) guarantees Z |]\
   6.247 -\    ==> F \\<in> (V Int Y) guarantees Z";
   6.248 -by (Blast_tac 1);
   6.249 -qed "combining1";
   6.250 -
   6.251 -Goalw [guar_def]
   6.252 -    "[| F \\<in> V guarantees (X Un Y);  F \\<in> Y guarantees Z |]\
   6.253 -\    ==> F \\<in> V guarantees (X Un Z)";
   6.254 -by (Blast_tac 1);
   6.255 -qed "combining2";
   6.256 -
   6.257 -
   6.258 -(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   6.259 -    does not suit Isabelle... **)
   6.260 -
   6.261 -(*Premise should be (!!i. i \\<in> I ==> F \\<in> X guarantees Y i) *)
   6.262 -Goalw [guar_def]
   6.263 -     "[| \\<forall>i \\<in> I. F \\<in> X guarantees Y(i); i \\<in> I |] \
   6.264 -\   ==> F \\<in> X guarantees (\\<Inter>i \\<in> I. Y(i))";
   6.265 -by (Blast_tac 1);
   6.266 -qed "all_guarantees";
   6.267 -
   6.268 -(*Premises should be [| F \\<in> X guarantees Y i; i \\<in> I |] *)
   6.269 -Goalw [guar_def]
   6.270 -     "\\<exists>i \\<in> I. F \\<in> X guarantees Y(i) ==> F \\<in> X guarantees (\\<Union>i \\<in> I. Y(i))";
   6.271 -by (Blast_tac 1);
   6.272 -qed "ex_guarantees";
   6.273 -
   6.274 -
   6.275 -(*** Additional guarantees laws, by lcp ***)
   6.276 -
   6.277 -Goalw [guar_def]
   6.278 -    "[| F \\<in> U guarantees V;  G \\<in> X guarantees Y; F ok G |] \
   6.279 -\    ==> F Join G: (U Int X) guarantees (V Int Y)"; 
   6.280 -by (Simp_tac 1);
   6.281 -by Safe_tac;
   6.282 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.283 -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   6.284 -by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
   6.285 -by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   6.286 -qed "guarantees_Join_Int";
   6.287 -
   6.288 -Goalw [guar_def]
   6.289 -    "[| F \\<in> U guarantees V;  G \\<in> X guarantees Y; F ok G |]  \
   6.290 -\    ==> F Join G: (U Un X) guarantees (V Un Y)";
   6.291 -by (Simp_tac 1);
   6.292 -by Safe_tac;
   6.293 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.294 -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   6.295 -by (rotate_tac 4 1);
   6.296 -by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
   6.297 -by (Simp_tac 1);
   6.298 -by (force_tac (claset(), simpset() addsimps [ok_commute]) 1);
   6.299 -by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   6.300 -qed "guarantees_Join_Un";
   6.301 -
   6.302 -Goalw [guar_def]
   6.303 -     "[| \\<forall>i \\<in> I. F(i) \\<in> X(i) guarantees Y(i);  OK(I,F); i \\<in> I |] \
   6.304 -\     ==> (\\<Squnion>i \\<in> I. F(i)) \\<in> (\\<Inter>i \\<in> I. X(i)) guarantees (\\<Inter>i \\<in> I. Y(i))";
   6.305 -by Safe_tac;
   6.306 -by (Blast_tac 2);
   6.307 -by (dres_inst_tac [("x", "xa")] bspec 1);
   6.308 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [INT_iff])));
   6.309 -by Safe_tac;
   6.310 -by (rotate_tac ~1 1);
   6.311 -by (dres_inst_tac [("x", "(\\<Squnion>x \\<in> (I-{xa}). F(x)) Join G")] bspec 1);
   6.312 -by (auto_tac
   6.313 -    (claset() addIs [OK_imp_ok],
   6.314 -     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
   6.315 -qed "guarantees_JN_INT";
   6.316 -
   6.317 -Goalw [guar_def]
   6.318 -    "[| \\<forall>i \\<in> I. F(i) \\<in> X(i) guarantees Y(i);  OK(I,F) |] \
   6.319 -\    ==> JOIN(I,F) \\<in> (\\<Union>i \\<in> I. X(i)) guarantees (\\<Union>i \\<in> I. Y(i))";
   6.320 -by Auto_tac;
   6.321 -by (dres_inst_tac [("x", "y")] bspec 1);
   6.322 -by (ALLGOALS(Asm_full_simp_tac));
   6.323 -by Safe_tac;
   6.324 -by (rotate_tac ~1 1);
   6.325 -by (rename_tac "G y" 1);
   6.326 -by (dres_inst_tac [("x", "JOIN(I-{y}, F) Join G")] bspec 1);
   6.327 -by (auto_tac
   6.328 -    (claset() addIs [OK_imp_ok],
   6.329 -     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
   6.330 -qed "guarantees_JN_UN";
   6.331 -
   6.332 -(*** guarantees laws for breaking down the program, by lcp ***)
   6.333 -
   6.334 -Goalw [guar_def]
   6.335 -     "[| F \\<in> X guarantees Y;  F ok G |] ==> F Join G \\<in> X guarantees Y";
   6.336 -by (Simp_tac 1);
   6.337 -by Safe_tac;
   6.338 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.339 -qed "guarantees_Join_I1";
   6.340 -
   6.341 -Goal "[| G \\<in> X guarantees Y;  F ok G |] ==> F Join G \\<in> X guarantees Y";
   6.342 -by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, 
   6.343 -                                           inst "G" "G" ok_commute]) 1);
   6.344 -by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
   6.345 -qed "guarantees_Join_I2";
   6.346 -
   6.347 -Goalw [guar_def]
   6.348 -     "[| i \\<in> I; F(i): X guarantees Y;  OK(I,F) |] \
   6.349 -\     ==> (\\<Squnion>i \\<in> I. F(i)) \\<in> X guarantees Y";
   6.350 -by Safe_tac;
   6.351 -by (dres_inst_tac [("x", "JOIN(I-{i},F) Join G")] bspec 1);
   6.352 -by (Simp_tac 1);
   6.353 -by (auto_tac (claset() addIs [OK_imp_ok],
   6.354 -              simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
   6.355 -qed "guarantees_JN_I";
   6.356 -
   6.357 -(*** well-definedness ***)
   6.358 -
   6.359 -Goalw [welldef_def] "F Join G \\<in> welldef ==> programify(F): welldef";
   6.360 -by Auto_tac;
   6.361 -qed "Join_welldef_D1";
   6.362 -
   6.363 -Goalw [welldef_def] "F Join G \\<in> welldef ==> programify(G): welldef";
   6.364 -by Auto_tac;
   6.365 -qed "Join_welldef_D2";
   6.366 -
   6.367 -(*** refinement ***)
   6.368 -
   6.369 -Goalw [refines_def] "F refines F wrt X";
   6.370 -by (Blast_tac 1);
   6.371 -qed "refines_refl";
   6.372 -
   6.373 -(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
   6.374 -
   6.375 -Goalw [wg_def] "wg(F, X) \\<subseteq> program";
   6.376 -by Auto_tac;
   6.377 -qed "wg_type";
   6.378 -
   6.379 -Goalw [guar_def] "X guarantees Y \\<subseteq> program";
   6.380 -by Auto_tac;
   6.381 -qed "guarantees_type";
   6.382 -
   6.383 -Goalw [wg_def] "G \\<in> wg(F, X) ==> G \\<in> program & F \\<in> program";
   6.384 -by Auto_tac;
   6.385 -by (blast_tac (claset() addDs [guarantees_type RS subsetD]) 1);
   6.386 -qed "wgD2";
   6.387 -
   6.388 -Goalw [guar_def, component_of_def]
   6.389 -"(F \\<in> X guarantees Y) <-> \
   6.390 -\  F \\<in> program & (\\<forall>H \\<in> program. H \\<in> X --> (F component_of H --> H \\<in> Y))";
   6.391 -by Safe_tac;
   6.392 -by (REPEAT(Force_tac 1));
   6.393 -qed "guarantees_equiv";
   6.394 -
   6.395 -Goalw [wg_def] "!!X. [| F \\<in> (X guarantees Y); X \\<subseteq> program |] ==> X \\<subseteq> wg(F,Y)";
   6.396 -by Auto_tac;
   6.397 -qed "wg_weakest";
   6.398 -
   6.399 -Goalw [wg_def, guar_def] 
   6.400 -"F \\<in> program ==> F \\<in> wg(F,Y) guarantees Y";
   6.401 -by (Blast_tac 1);
   6.402 -qed "wg_guarantees";
   6.403 -
   6.404 -Goalw [wg_def] "(H \\<in> wg(F,X)) <-> ((F component_of H --> H \\<in> X) & F \\<in> program & H \\<in> program)";
   6.405 -by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
   6.406 -by (rtac iffI 1);
   6.407 -by Safe_tac;
   6.408 -by (res_inst_tac [("x", "{H}")] bexI 4);
   6.409 -by (res_inst_tac [("x", "{H}")] bexI 3);
   6.410 -by (REPEAT(Blast_tac 1));
   6.411 -qed "wg_equiv";
   6.412 -
   6.413 -Goal
   6.414 -"F component_of H ==> H \\<in> wg(F,X) <-> (H \\<in> X & F \\<in> program & H \\<in> program)";
   6.415 -by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
   6.416 -qed "component_of_wg";
   6.417 -
   6.418 -Goal
   6.419 -"\\<forall>FF \\<in> Fin(program). FF Int X \\<noteq> 0 --> OK(FF, %F. F) \
   6.420 -\  --> (\\<forall>F \\<in> FF. ((\\<Squnion>F \\<in> FF. F): wg(F,X)) <-> ((\\<Squnion>F \\<in> FF. F):X))";
   6.421 -by (Clarify_tac 1);
   6.422 -by (subgoal_tac "F component_of (\\<Squnion>F \\<in> FF. F)" 1);
   6.423 -by (dres_inst_tac [("X", "X")] component_of_wg 1);
   6.424 -by (force_tac (claset() addSDs [thm"Fin.dom_subset" RS subsetD RS PowD],
   6.425 -               simpset()) 1);
   6.426 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [component_of_def])));
   6.427 -by (res_inst_tac [("x", "\\<Squnion>F \\<in> (FF-{F}). F")] exI 1);
   6.428 -by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], 
   6.429 -              simpset() addsimps [OK_iff_ok]));
   6.430 -qed "wg_finite";
   6.431 -
   6.432 -
   6.433 -(* "!!FF. [| FF \\<in> Fin(program); FF Int X \\<noteq>0; OK(FF, %F. F); G \\<in> FF |] 
   6.434 -   ==> JOIN(FF, %F. F):wg(G, X) <-> JOIN(FF, %F. F):X"  *)
   6.435 -val wg_finite2 = wg_finite RS bspec RS mp RS mp RS bspec;
   6.436 -
   6.437 -Goal "ex_prop(X) ==> (F \\<in> X) <-> (\\<forall>H \\<in> program. H \\<in> wg(F,X) & F \\<in> program)";
   6.438 -by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
   6.439 -by (Blast_tac 1);
   6.440 -qed "wg_ex_prop";
   6.441 -
   6.442 -(** From Charpentier and Chandy "Theorems About Composition" **)
   6.443 -(* Proposition 2 *)
   6.444 -Goalw [wx_def] "wx(X)\\<subseteq>X";
   6.445 -by Auto_tac;
   6.446 -qed "wx_subset";
   6.447 -
   6.448 -Goal "ex_prop(wx(X))";
   6.449 -by (full_simp_tac (simpset() addsimps [ex_prop_def, wx_def]) 1);
   6.450 -by Safe_tac;
   6.451 -by (Blast_tac 1);
   6.452 -by (ALLGOALS(res_inst_tac [("x", "x")] bexI));
   6.453 -by (REPEAT(Force_tac 1));
   6.454 -qed "wx_ex_prop";
   6.455 -
   6.456 -Goalw [wx_def] "\\<forall>Z. Z\\<subseteq>program --> Z\\<subseteq> X --> ex_prop(Z) --> Z \\<subseteq> wx(X)";
   6.457 -by Auto_tac;
   6.458 -qed "wx_weakest";
   6.459 -
   6.460 -(* Proposition 6 *)
   6.461 -Goalw [ex_prop_def]
   6.462 - "ex_prop({F \\<in> program. \\<forall>G \\<in> program. F ok G --> F Join G \\<in> X})";
   6.463 -by Safe_tac;
   6.464 -by (dres_inst_tac [("x", "G Join Ga")] bspec 1);
   6.465 -by (Simp_tac 1);
   6.466 -by (force_tac (claset(), simpset() addsimps [Join_assoc]) 1);
   6.467 -by (dres_inst_tac [("x", "F Join Ga")] bspec 1);
   6.468 -by (Simp_tac 1);
   6.469 -by (Full_simp_tac 1);
   6.470 -by Safe_tac;
   6.471 -by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
   6.472 -by (subgoal_tac "F Join G = G Join F" 1);
   6.473 -by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.474 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
   6.475 -qed "wx'_ex_prop";
   6.476 -
   6.477 -(* Equivalence with the other definition of wx *)
   6.478 -
   6.479 -Goalw [wx_def]
   6.480 - "wx(X) = {F \\<in> program. \\<forall>G \\<in> program. F ok G --> (F Join G):X}";
   6.481 -by (rtac equalityI 1);
   6.482 -by Safe_tac;
   6.483 -by (Blast_tac 1);
   6.484 -by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
   6.485 -by Safe_tac;
   6.486 -by (dres_inst_tac [("x", "x")] bspec 1);
   6.487 -by (dres_inst_tac [("x", "G")] bspec 2);
   6.488 -by (forw_inst_tac [("c", "x Join G")] subsetD 3);
   6.489 -by Safe_tac;
   6.490 -by (Blast_tac 1);
   6.491 -by (Blast_tac 1);
   6.492 -by (res_inst_tac [("B", "{F \\<in> program. \\<forall>G \\<in> program. F ok G --> F Join G \\<in> X}")] 
   6.493 -                   UnionI 1);
   6.494 -by Safe_tac;
   6.495 -by (rtac wx'_ex_prop 2);
   6.496 -by (rotate_tac 2 1);
   6.497 -by (dres_inst_tac [("x", "SKIP")] bspec 1);
   6.498 -by Auto_tac;
   6.499 -qed "wx_equiv";
   6.500 -
   6.501 -(* Propositions 7 to 11 are all about this second definition of wx. And
   6.502 -   by equivalence between the two definition, they are the same as the ones proved *)
   6.503 -
   6.504 -
   6.505 -(* Proposition 12 *)
   6.506 -(* Main result of the paper *)
   6.507 -Goalw [guar_def]  "(X guarantees Y) = wx((program-X) Un Y)";
   6.508 -by (simp_tac (simpset() addsimps [wx_equiv]) 1);
   6.509 -by Auto_tac;
   6.510 -qed "guarantees_wx_eq";
   6.511 -
   6.512 -(* 
   6.513 -{* Corollary, but this result has already been proved elsewhere *}
   6.514 - "ex_prop(X guarantees Y)";
   6.515 -  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
   6.516 -  qed "guarantees_ex_prop";
   6.517 -*)
   6.518 -
   6.519 -(* Rules given in section 7 of Chandy and Sander's
   6.520 -    Reasoning About Program composition paper *)
   6.521 -
   6.522 -Goal "[| Init(F) \\<subseteq> A; F \\<in> program |] ==> F \\<in> stable(A) guarantees Always(A)";
   6.523 -by (rtac guaranteesI 1);
   6.524 -by (assume_tac 2);
   6.525 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
   6.526 -by (rtac stable_Join_Always1 1);
   6.527 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [invariant_def])));
   6.528 -by (auto_tac (claset(), simpset() addsimps [programify_def, initially_def]));
   6.529 -qed "stable_guarantees_Always";
   6.530 -
   6.531 -(* To be moved to WFair.ML *)
   6.532 -Goal "[| F \\<in> A co A Un B; F \\<in> transient(A); st_set(B) |] ==> F \\<in> A leadsTo B";
   6.533 -by (ftac constrainsD2 1);
   6.534 -by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
   6.535 -by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
   6.536 -by (rtac (ensuresI RS leadsTo_Basis) 3);
   6.537 -by (ALLGOALS(Blast_tac));
   6.538 -qed "leadsTo_Basis'";
   6.539 -
   6.540 -Goal "[| F \\<in> transient(A); st_set(B) |] ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
   6.541 -by (rtac guaranteesI 1);
   6.542 -by (blast_tac (claset() addDs [transient_type RS subsetD]) 2);
   6.543 -by (rtac leadsTo_Basis' 1);
   6.544 -by (Blast_tac 3);
   6.545 -by (dtac constrains_weaken_R 1);
   6.546 -by (assume_tac 2);
   6.547 -by (rtac Join_transient_I1 2);
   6.548 -by (REPEAT(Blast_tac 1));
   6.549 -qed "constrains_guarantees_leadsTo";
   6.550 -
   6.551 -
     7.1 --- a/src/ZF/UNITY/Guar.thy	Tue Jul 08 11:44:30 2003 +0200
     7.2 +++ b/src/ZF/UNITY/Guar.thy	Wed Jul 09 11:39:34 2003 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4  (*  Title:      ZF/UNITY/Guar.thy
     7.5 -    ID:         $Id$
     7.6 +    ID:         $Id \<in> Guar.thy,v 1.3 2001/11/15 14:51:43 ehmety Exp $
     7.7      Author:     Sidi O Ehmety, Computer Laboratory
     7.8      Copyright   2001  University of Cambridge
     7.9  
    7.10 @@ -10,7 +10,7 @@
    7.11  
    7.12  Revised by Sidi Ehmety on January 2001
    7.13  
    7.14 -Added: Compatibility, weakest guarantees, etc.
    7.15 +Added \<in> Compatibility, weakest guarantees, etc.
    7.16  
    7.17  and Weakest existential property,
    7.18  from Charpentier and Chandy "Theorems about Composition",
    7.19 @@ -18,50 +18,508 @@
    7.20  
    7.21  Theory ported from HOL.
    7.22  *)
    7.23 -Guar = Comp +
    7.24 +
    7.25 +
    7.26 +header{*The Chandy-Sanders Guarantees Operator*}
    7.27 +
    7.28 +theory Guar = Comp: 
    7.29 +
    7.30 +
    7.31 +(* To be moved to theory WFair???? *)
    7.32 +lemma leadsTo_Basis': "[| F \<in> A co A Un B; F \<in> transient(A); st_set(B) |] ==> F \<in> A leadsTo B"
    7.33 +apply (frule constrainsD2)
    7.34 +apply (drule_tac B = "A-B" in constrains_weaken_L, blast) 
    7.35 +apply (drule_tac B = "A-B" in transient_strengthen, blast) 
    7.36 +apply (blast intro: ensuresI [THEN leadsTo_Basis])
    7.37 +done
    7.38 +
    7.39 +
    7.40  constdefs
    7.41  
    7.42 -  (*Existential and Universal properties.  I formalize the two-program
    7.43 +  (*Existential and Universal properties.  We formalize the two-program
    7.44      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    7.45  
    7.46 -   ex_prop :: i =>o
    7.47 +   ex_prop :: "i => o"
    7.48     "ex_prop(X) == X<=program &
    7.49 -    (ALL F:program. ALL G:program. F ok G --> F:X | G:X --> (F Join G):X)"
    7.50 +    (\<forall>F \<in> program. \<forall>G \<in> program. F ok G --> F \<in> X | G \<in> X --> (F Join G) \<in> X)"
    7.51  
    7.52 -  strict_ex_prop  :: i => o
    7.53 +  strict_ex_prop  :: "i => o"
    7.54    "strict_ex_prop(X) == X<=program &
    7.55 -   (ALL F:program. ALL  G:program. F ok G --> (F:X | G: X) <-> (F Join G : X))"
    7.56 +   (\<forall>F \<in> program. \<forall>G \<in> program. F ok G --> (F \<in> X | G \<in> X) <-> (F Join G \<in> X))"
    7.57  
    7.58 -  uv_prop  :: i => o
    7.59 +  uv_prop  :: "i => o"
    7.60     "uv_prop(X) == X<=program &
    7.61 -    (SKIP:X & (ALL F:program. ALL G:program. F ok G --> F:X & G:X --> (F Join G):X))"
    7.62 +    (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))"
    7.63    
    7.64 - strict_uv_prop  :: i => o
    7.65 + strict_uv_prop  :: "i => o"
    7.66     "strict_uv_prop(X) == X<=program &
    7.67 -    (SKIP:X & (ALL F:program. ALL G:program. F ok G -->(F:X & G:X) <-> (F Join G:X)))"
    7.68 +    (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)))"
    7.69  
    7.70 -  guar :: [i, i] => i (infixl "guarantees" 55)
    7.71 +  guar :: "[i, i] => i" (infixl "guarantees" 55)
    7.72                (*higher than membership, lower than Co*)
    7.73 -  "X guarantees Y == {F:program. ALL G:program. F ok G --> F Join G : X --> F Join G:Y}"
    7.74 +  "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
    7.75    
    7.76    (* Weakest guarantees *)
    7.77 -   wg :: [i,i] => i
    7.78 -  "wg(F,Y) == Union({X:Pow(program). F:(X guarantees Y)})"
    7.79 +   wg :: "[i,i] => i"
    7.80 +  "wg(F,Y) == Union({X \<in> Pow(program). F:(X guarantees Y)})"
    7.81  
    7.82    (* Weakest existential property stronger than X *)
    7.83     wx :: "i =>i"
    7.84 -   "wx(X) == Union({Y:Pow(program). Y<=X & ex_prop(Y)})"
    7.85 +   "wx(X) == Union({Y \<in> Pow(program). Y<=X & ex_prop(Y)})"
    7.86  
    7.87    (*Ill-defined programs can arise through "Join"*)
    7.88    welldef :: i
    7.89 -  "welldef == {F:program. Init(F) ~= 0}"
    7.90 +  "welldef == {F \<in> program. Init(F) \<noteq> 0}"
    7.91    
    7.92 -  refines :: [i, i, i] => o ("(3_ refines _ wrt _)" [10,10,10] 10)
    7.93 +  refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10)
    7.94    "G refines F wrt X ==
    7.95 -   ALL H:program. (F ok H  & G ok H & F Join H:welldef Int X)
    7.96 -    --> (G Join H:welldef Int X)"
    7.97 +   \<forall>H \<in> program. (F ok H  & G ok H & F Join H \<in> welldef Int X)
    7.98 +    --> (G Join H \<in> welldef Int X)"
    7.99 +
   7.100 +  iso_refines :: "[i,i, i] => o"  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
   7.101 +  "G iso_refines F wrt X ==  F \<in> welldef Int X --> G \<in> welldef Int X"
   7.102 +
   7.103 +
   7.104 +(*** existential properties ***)
   7.105 +
   7.106 +lemma ex_imp_subset_program: "ex_prop(X) ==> X\<subseteq>program"
   7.107 +by (simp add: ex_prop_def)
   7.108 +
   7.109 +lemma ex1 [rule_format]: 
   7.110 + "GG \<in> Fin(program) 
   7.111 +  ==> ex_prop(X) --> GG Int X\<noteq>0 --> OK(GG, (%G. G)) -->(\<Squnion>G \<in> GG. G) \<in> X"
   7.112 +apply (unfold ex_prop_def)
   7.113 +apply (erule Fin_induct)
   7.114 +apply (simp_all add: OK_cons_iff)
   7.115 +apply (safe elim!: not_emptyE, auto) 
   7.116 +done
   7.117 +
   7.118 +lemma ex2 [rule_format]: 
   7.119 +"X \<subseteq> program ==>  
   7.120 + (\<forall>GG \<in> Fin(program). GG Int X \<noteq> 0 --> OK(GG,(%G. G))-->(\<Squnion>G \<in> GG. G) \<in> X) 
   7.121 +   --> ex_prop(X)"
   7.122 +apply (unfold ex_prop_def, clarify)
   7.123 +apply (drule_tac x = "{F,G}" in bspec)
   7.124 +apply (simp_all add: OK_iff_ok)
   7.125 +apply (auto intro: ok_sym)
   7.126 +done
   7.127 +
   7.128 +(*Chandy & Sanders take this as a definition*)
   7.129 +
   7.130 +lemma ex_prop_finite:
   7.131 +     "ex_prop(X) <-> (X\<subseteq>program &  
   7.132 +  (\<forall>GG \<in> Fin(program). GG Int X \<noteq> 0 & OK(GG,(%G. G))-->(\<Squnion>G \<in> GG. G) \<in> X))"
   7.133 +apply auto
   7.134 +apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+
   7.135 +done
   7.136 +
   7.137 +(* Equivalent definition of ex_prop given at the end of section 3*)
   7.138 +lemma ex_prop_equiv: 
   7.139 +"ex_prop(X) <->  
   7.140 +  X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X <-> (\<forall>H \<in> program. (G component_of H) --> H \<in> X)))"
   7.141 +apply (unfold ex_prop_def component_of_def, safe, force, force, blast) 
   7.142 +apply (subst Join_commute)
   7.143 +apply (blast intro: ok_sym) 
   7.144 +done
   7.145 +
   7.146 +(*** universal properties ***)
   7.147 +
   7.148 +lemma uv_imp_subset_program: "uv_prop(X)==> X\<subseteq>program"
   7.149 +apply (unfold uv_prop_def)
   7.150 +apply (simp (no_asm_simp))
   7.151 +done
   7.152 +
   7.153 +lemma uv1 [rule_format]: 
   7.154 +     "GG \<in> Fin(program) ==>  
   7.155 +      (uv_prop(X)--> GG \<subseteq> X & OK(GG, (%G. G)) --> (\<Squnion>G \<in> GG. G) \<in> X)"
   7.156 +apply (unfold uv_prop_def)
   7.157 +apply (erule Fin_induct)
   7.158 +apply (auto simp add: OK_cons_iff)
   7.159 +done
   7.160 +
   7.161 +lemma uv2 [rule_format]: 
   7.162 +     "X\<subseteq>program  ==> 
   7.163 +      (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) --> (\<Squnion>G \<in> GG. G) \<in> X)
   7.164 +      --> uv_prop(X)"
   7.165 +apply (unfold uv_prop_def, auto)
   7.166 +apply (drule_tac x = 0 in bspec, simp+) 
   7.167 +apply (drule_tac x = "{F,G}" in bspec, simp) 
   7.168 +apply (force dest: ok_sym simp add: OK_iff_ok) 
   7.169 +done
   7.170 +
   7.171 +(*Chandy & Sanders take this as a definition*)
   7.172 +lemma uv_prop_finite: 
   7.173 +"uv_prop(X) <-> X\<subseteq>program &  
   7.174 +  (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) --> (\<Squnion>G \<in> GG. G) \<in>  X)"
   7.175 +apply auto
   7.176 +apply (blast dest: uv_imp_subset_program)
   7.177 +apply (blast intro: uv1)
   7.178 +apply (blast intro!: uv2 dest:)
   7.179 +done
   7.180 +
   7.181 +(*** guarantees ***)
   7.182 +lemma guaranteesI: 
   7.183 +     "[| (!!G. [| F ok G; F Join G \<in> X; G \<in> program |] ==> F Join G \<in> Y); 
   7.184 +         F \<in> program |]   
   7.185 +    ==> F \<in> X guarantees Y"
   7.186 +by (simp add: guar_def component_def)
   7.187 +
   7.188 +lemma guaranteesD: 
   7.189 +     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X; G \<in> program |]  
   7.190 +      ==> F Join G \<in> Y"
   7.191 +by (simp add: guar_def component_def)
   7.192 +
   7.193 +
   7.194 +(*This version of guaranteesD matches more easily in the conclusion
   7.195 +  The major premise can no longer be  F\<subseteq>H since we need to reason about G*)
   7.196 +
   7.197 +lemma component_guaranteesD: 
   7.198 +     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G; G \<in> program |]  
   7.199 +      ==> H \<in> Y"
   7.200 +by (simp add: guar_def, blast)
   7.201 +
   7.202 +lemma guarantees_weaken: 
   7.203 +     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
   7.204 +by (simp add: guar_def, auto)
   7.205 +
   7.206 +lemma subset_imp_guarantees_program:
   7.207 +     "X \<subseteq> Y ==> X guarantees Y = program"
   7.208 +by (unfold guar_def, blast)
   7.209 +
   7.210 +(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   7.211 +lemma subset_imp_guarantees:
   7.212 +     "[| X \<subseteq> Y; F \<in> program |] ==> F \<in> X guarantees Y"
   7.213 +by (unfold guar_def, blast)
   7.214 +
   7.215 +lemma component_of_Join1: "F ok G ==> F component_of (F Join G)"
   7.216 +by (unfold component_of_def, blast)
   7.217 +
   7.218 +lemma component_of_Join2: "F ok G ==> G component_of (F Join G)"
   7.219 +apply (subst Join_commute)
   7.220 +apply (blast intro: ok_sym component_of_Join1)
   7.221 +done
   7.222 +
   7.223 +(*Remark at end of section 4.1 *)
   7.224 +lemma ex_prop_imp: 
   7.225 +     "ex_prop(Y) ==> (Y = (program guarantees Y))"
   7.226 +apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def)
   7.227 +apply clarify
   7.228 +apply (rule equalityI, blast, safe)
   7.229 +apply (drule_tac x = x in bspec, assumption, force) 
   7.230 +done
   7.231 +
   7.232 +lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)"
   7.233 +apply (unfold guar_def)
   7.234 +apply (simp (no_asm_simp) add: ex_prop_equiv)
   7.235 +apply safe
   7.236 +apply (blast intro: elim: equalityE) 
   7.237 +apply (simp_all (no_asm_use) add: component_of_def)
   7.238 +apply (force elim: equalityE)+
   7.239 +done
   7.240 +
   7.241 +lemma ex_prop_equiv2: "(ex_prop(Y)) <-> (Y = program guarantees Y)"
   7.242 +by (blast intro: ex_prop_imp guarantees_imp)
   7.243 +
   7.244 +(** Distributive laws.  Re-orient to perform miniscoping **)
   7.245 +
   7.246 +lemma guarantees_UN_left: 
   7.247 +     "i \<in> I ==>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)"
   7.248 +apply (unfold guar_def)
   7.249 +apply (rule equalityI, safe)
   7.250 + prefer 2 apply force
   7.251 +apply blast+
   7.252 +done
   7.253 +
   7.254 +lemma guarantees_Un_left: 
   7.255 +     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
   7.256 +apply (unfold guar_def)
   7.257 +apply (rule equalityI, safe, blast+)
   7.258 +done
   7.259 +
   7.260 +lemma guarantees_INT_right: 
   7.261 +     "i \<in> I ==> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))"
   7.262 +apply (unfold guar_def)
   7.263 +apply (rule equalityI, safe, blast+)
   7.264 +done
   7.265 +
   7.266 +lemma guarantees_Int_right: 
   7.267 +     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
   7.268 +by (unfold guar_def, blast)
   7.269 +
   7.270 +lemma guarantees_Int_right_I:
   7.271 +     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
   7.272 +     ==> F \<in> Z guarantees (X Int Y)"
   7.273 +by (simp (no_asm_simp) add: guarantees_Int_right)
   7.274 +
   7.275 +lemma guarantees_INT_right_iff:
   7.276 +     "i \<in> I==> (F \<in> X guarantees (\<Inter>i \<in> I. Y(i))) <->  
   7.277 +      (\<forall>i \<in> I. F \<in> X guarantees Y(i))"
   7.278 +by (simp add: guarantees_INT_right INT_iff, blast)
   7.279 +
   7.280 +
   7.281 +lemma shunting: "(X guarantees Y) = (program guarantees ((program-X) Un Y))"
   7.282 +by (unfold guar_def, auto)
   7.283 +
   7.284 +lemma contrapositive:
   7.285 +     "(X guarantees Y) = (program - Y) guarantees (program -X)"
   7.286 +by (unfold guar_def, blast)
   7.287 +
   7.288 +(** The following two can be expressed using intersection and subset, which
   7.289 +    is more faithful to the text but looks cryptic.
   7.290 +**)
   7.291 +
   7.292 +lemma combining1: 
   7.293 +    "[| F \<in> V guarantees X;  F \<in> (X Int Y) guarantees Z |] 
   7.294 +     ==> F \<in> (V Int Y) guarantees Z"
   7.295 +by (unfold guar_def, blast)
   7.296 +
   7.297 +lemma combining2: 
   7.298 +    "[| F \<in> V guarantees (X Un Y);  F \<in> Y guarantees Z |] 
   7.299 +     ==> F \<in> V guarantees (X Un Z)"
   7.300 +by (unfold guar_def, blast)
   7.301 +
   7.302 +
   7.303 +(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   7.304 +    does not suit Isabelle... **)
   7.305 +
   7.306 +(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
   7.307 +lemma all_guarantees: 
   7.308 +     "[| \<forall>i \<in> I. F \<in> X guarantees Y(i); i \<in> I |]  
   7.309 +    ==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))"
   7.310 +by (unfold guar_def, blast)
   7.311 +
   7.312 +(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
   7.313 +lemma ex_guarantees: 
   7.314 +     "\<exists>i \<in> I. F \<in> X guarantees Y(i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y(i))"
   7.315 +by (unfold guar_def, blast)
   7.316 +
   7.317 +
   7.318 +(*** Additional guarantees laws, by lcp ***)
   7.319  
   7.320 -  iso_refines :: [i,i, i] => o  ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
   7.321 -  "G iso_refines F wrt X ==  F:welldef Int X --> G:welldef Int X"
   7.322 +lemma guarantees_Join_Int: 
   7.323 +    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
   7.324 +     ==> F Join G: (U Int X) guarantees (V Int Y)"
   7.325 +
   7.326 +apply (unfold guar_def)
   7.327 +apply (simp (no_asm))
   7.328 +apply safe
   7.329 +apply (simp add: Join_assoc)
   7.330 +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
   7.331 +apply (simp add: ok_commute)
   7.332 +apply (simp (no_asm_simp) add: Join_ac)
   7.333 +done
   7.334 +
   7.335 +lemma guarantees_Join_Un: 
   7.336 +    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
   7.337 +     ==> F Join G: (U Un X) guarantees (V Un Y)"
   7.338 +apply (unfold guar_def)
   7.339 +apply (simp (no_asm))
   7.340 +apply safe
   7.341 +apply (simp add: Join_assoc)
   7.342 +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
   7.343 +apply (rotate_tac 4)
   7.344 +apply (drule_tac x = "F Join Ga" in bspec)
   7.345 +apply (simp (no_asm))
   7.346 +apply (force simp add: ok_commute)
   7.347 +apply (simp (no_asm_simp) add: Join_ac)
   7.348 +done
   7.349 +
   7.350 +lemma guarantees_JN_INT: 
   7.351 +     "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i);  OK(I,F); i \<in> I |]  
   7.352 +      ==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))"
   7.353 +apply (unfold guar_def, safe)
   7.354 + prefer 2 apply blast
   7.355 +apply (drule_tac x = xa in bspec)
   7.356 +apply (simp_all add: INT_iff, safe)
   7.357 +apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) Join G" and A=program in bspec)
   7.358 +apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   7.359 +done
   7.360 +
   7.361 +lemma guarantees_JN_UN: 
   7.362 +    "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i);  OK(I,F) |]  
   7.363 +     ==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))"
   7.364 +apply (unfold guar_def, auto)
   7.365 +apply (drule_tac x = y in bspec, simp_all, safe)
   7.366 +apply (rename_tac G y)
   7.367 +apply (drule_tac x = "JOIN (I-{y}, F) Join G" and A=program in bspec)
   7.368 +apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   7.369 +done
   7.370 +
   7.371 +(*** guarantees laws for breaking down the program, by lcp ***)
   7.372 +
   7.373 +lemma guarantees_Join_I1: 
   7.374 +     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
   7.375 +apply (simp add: guar_def, safe)
   7.376 +apply (simp add: Join_assoc)
   7.377 +done
   7.378 +
   7.379 +lemma guarantees_Join_I2:
   7.380 +     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
   7.381 +apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
   7.382 +apply (blast intro: guarantees_Join_I1)
   7.383 +done
   7.384 +
   7.385 +lemma guarantees_JN_I: 
   7.386 +     "[| i \<in> I; F(i) \<in>  X guarantees Y;  OK(I,F) |]  
   7.387 +      ==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y"
   7.388 +apply (unfold guar_def, safe)
   7.389 +apply (drule_tac x = "JOIN (I-{i},F) Join G" in bspec)
   7.390 +apply (simp (no_asm))
   7.391 +apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
   7.392 +done
   7.393 +
   7.394 +(*** well-definedness ***)
   7.395 +
   7.396 +lemma Join_welldef_D1: "F Join G \<in> welldef ==> programify(F) \<in>  welldef"
   7.397 +by (unfold welldef_def, auto)
   7.398 +
   7.399 +lemma Join_welldef_D2: "F Join G \<in> welldef ==> programify(G) \<in>  welldef"
   7.400 +by (unfold welldef_def, auto)
   7.401 +
   7.402 +(*** refinement ***)
   7.403 +
   7.404 +lemma refines_refl: "F refines F wrt X"
   7.405 +by (unfold refines_def, blast)
   7.406 +
   7.407 +(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *)
   7.408 +
   7.409 +lemma wg_type: "wg(F, X) \<subseteq> program"
   7.410 +by (unfold wg_def, auto)
   7.411 +
   7.412 +lemma guarantees_type: "X guarantees Y \<subseteq> program"
   7.413 +by (unfold guar_def, auto)
   7.414 +
   7.415 +lemma wgD2: "G \<in> wg(F, X) ==> G \<in> program & F \<in> program"
   7.416 +apply (unfold wg_def, auto)
   7.417 +apply (blast dest: guarantees_type [THEN subsetD])
   7.418 +done
   7.419 +
   7.420 +lemma guarantees_equiv: 
   7.421 +"(F \<in> X guarantees Y) <->  
   7.422 +   F \<in> program & (\<forall>H \<in> program. H \<in> X --> (F component_of H --> H \<in> Y))"
   7.423 +by (unfold guar_def component_of_def, force) 
   7.424 +
   7.425 +lemma wg_weakest:
   7.426 +     "!!X. [| F \<in> (X guarantees Y); X \<subseteq> program |] ==> X \<subseteq> wg(F,Y)"
   7.427 +by (unfold wg_def, auto)
   7.428 +
   7.429 +lemma wg_guarantees: "F \<in> program ==> F \<in> wg(F,Y) guarantees Y"
   7.430 +by (unfold wg_def guar_def, blast)
   7.431 +
   7.432 +lemma wg_equiv:
   7.433 +     "H \<in> wg(F,X) <-> 
   7.434 +      ((F component_of H --> H \<in> X) & F \<in> program & H \<in> program)"
   7.435 +apply (simp add: wg_def guarantees_equiv)
   7.436 +apply (rule iffI, safe)
   7.437 +apply (rule_tac [4] x = "{H}" in bexI)
   7.438 +apply (rule_tac [3] x = "{H}" in bexI, blast+)
   7.439 +done
   7.440 +
   7.441 +lemma component_of_wg: 
   7.442 +    "F component_of H ==> H \<in> wg(F,X) <-> (H \<in> X & F \<in> program & H \<in> program)"
   7.443 +by (simp (no_asm_simp) add: wg_equiv)
   7.444 +
   7.445 +lemma wg_finite [rule_format]: 
   7.446 +"\<forall>FF \<in> Fin(program). FF Int X \<noteq> 0 --> OK(FF, %F. F)  
   7.447 +   --> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in>  wg(F,X)) <-> ((\<Squnion>F \<in> FF. F) \<in> X))"
   7.448 +apply clarify
   7.449 +apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
   7.450 +apply (drule_tac X = X in component_of_wg)
   7.451 +apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD])
   7.452 +apply (simp_all add: component_of_def)
   7.453 +apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
   7.454 +apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
   7.455 +done
   7.456 +
   7.457 +lemma wg_ex_prop:
   7.458 +     "ex_prop(X) ==> (F \<in> X) <-> (\<forall>H \<in> program. H \<in> wg(F,X) & F \<in> program)"
   7.459 +apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
   7.460 +apply blast
   7.461 +done
   7.462 +
   7.463 +(** From Charpentier and Chandy "Theorems About Composition" **)
   7.464 +(* Proposition 2 *)
   7.465 +lemma wx_subset: "wx(X)\<subseteq>X"
   7.466 +by (unfold wx_def, auto)
   7.467 +
   7.468 +lemma wx_ex_prop: "ex_prop(wx(X))"
   7.469 +apply (simp (no_asm_use) add: ex_prop_def wx_def)
   7.470 +apply safe
   7.471 +apply blast
   7.472 +apply (rule_tac x=x in bexI, force, simp)+
   7.473 +done
   7.474 +
   7.475 +lemma wx_weakest: "\<forall>Z. Z\<subseteq>program --> Z\<subseteq> X --> ex_prop(Z) --> Z \<subseteq> wx(X)"
   7.476 +by (unfold wx_def, auto)
   7.477 +
   7.478 +(* Proposition 6 *)
   7.479 +lemma wx'_ex_prop: 
   7.480 + "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X})"
   7.481 +apply (unfold ex_prop_def, safe)
   7.482 + apply (drule_tac x = "G Join Ga" in bspec)
   7.483 +  apply (simp (no_asm))
   7.484 + apply (force simp add: Join_assoc)
   7.485 +apply (drule_tac x = "F Join Ga" in bspec)
   7.486 + apply (simp (no_asm))
   7.487 +apply (simp (no_asm_use))
   7.488 +apply safe
   7.489 + apply (simp (no_asm_simp) add: ok_commute)
   7.490 +apply (subgoal_tac "F Join G = G Join F")
   7.491 + apply (simp (no_asm_simp) add: Join_assoc)
   7.492 +apply (simp (no_asm) add: Join_commute)
   7.493 +done
   7.494 +
   7.495 +(* Equivalence with the other definition of wx *)
   7.496 +
   7.497 +lemma wx_equiv: 
   7.498 +     "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G --> (F Join G) \<in> X}"
   7.499 +apply (unfold wx_def)
   7.500 +apply (rule equalityI, safe, blast)
   7.501 + apply (simp (no_asm_use) add: ex_prop_def)
   7.502 +apply blast 
   7.503 +apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G --> F Join G \<in> X}" 
   7.504 +         in UnionI, 
   7.505 +       safe)
   7.506 +apply (rule_tac [2] wx'_ex_prop)
   7.507 +apply (drule_tac x=SKIP in bspec, simp)+
   7.508 +apply auto 
   7.509 +done
   7.510 +
   7.511 +(* Propositions 7 to 11 are all about this second definition of wx. And
   7.512 +   by equivalence between the two definition, they are the same as the ones proved *)
   7.513 +
   7.514 +
   7.515 +(* Proposition 12 *)
   7.516 +(* Main result of the paper *)
   7.517 +lemma guarantees_wx_eq: "(X guarantees Y) = wx((program-X) Un Y)"
   7.518 +by (auto simp add: guar_def wx_equiv)
   7.519 +
   7.520 +(* 
   7.521 +{* Corollary, but this result has already been proved elsewhere *}
   7.522 + "ex_prop(X guarantees Y)"
   7.523 +*)
   7.524 +
   7.525 +(* Rules given in section 7 of Chandy and Sander's
   7.526 +    Reasoning About Program composition paper *)
   7.527 +
   7.528 +lemma stable_guarantees_Always:
   7.529 +     "[| Init(F) \<subseteq> A; F \<in> program |] ==> F \<in> stable(A) guarantees Always(A)"
   7.530 +apply (rule guaranteesI)
   7.531 + prefer 2 apply assumption
   7.532 +apply (simp (no_asm) add: Join_commute)
   7.533 +apply (rule stable_Join_Always1)
   7.534 +apply (simp_all add: invariant_def)
   7.535 +apply (auto simp add: programify_def initially_def)
   7.536 +done
   7.537 +
   7.538 +lemma constrains_guarantees_leadsTo:
   7.539 +     "[| F \<in> transient(A); st_set(B) |] 
   7.540 +      ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
   7.541 +apply (rule guaranteesI)
   7.542 + prefer 2 apply (blast dest: transient_type [THEN subsetD])
   7.543 +apply (rule leadsTo_Basis')
   7.544 +  apply (blast intro: constrains_weaken_R) 
   7.545 + apply (blast intro!: Join_transient_I1, blast)
   7.546 +done
   7.547  
   7.548  end
     8.1 --- a/src/ZF/UNITY/Increasing.ML	Tue Jul 08 11:44:30 2003 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,229 +0,0 @@
     8.4 -(*  Title:      ZF/UNITY/GenIncreasing
     8.5 -    ID:         $Id \\<in> Increasing.ML,v 1.3 2003/06/27 16:40:25 paulson Exp $
     8.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     8.7 -    Copyright   1998  University of Cambridge
     8.8 -
     8.9 -A general form of the `Increasing' relation of Charpentier
    8.10 -*)
    8.11 -
    8.12 -(** increasing **)
    8.13 -
    8.14 -Goalw [increasing_def] "increasing[A](r, f) <= program";
    8.15 -by (Blast_tac 1);
    8.16 -qed "increasing_type";
    8.17 -
    8.18 -Goalw [increasing_def] "F \\<in> increasing[A](r, f) ==> F \\<in> program";
    8.19 -by (Blast_tac 1);
    8.20 -qed "increasing_into_program";
    8.21 -
    8.22 -Goalw [increasing_def]
    8.23 -"[| F \\<in> increasing[A](r, f); x \\<in> A |] ==>F \\<in> stable({s \\<in> state. <x, f(s)>:r})";
    8.24 -by (Blast_tac 1);
    8.25 -qed "increasing_imp_stable";
    8.26 -
    8.27 -Goalw [increasing_def]
    8.28 -"F \\<in> increasing[A](r,f) ==> F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>s \\<in> state. f(s):A)";
    8.29 -by (subgoal_tac "\\<exists>x. x \\<in> state" 1);
    8.30 -by (auto_tac (claset() addDs [stable_type RS subsetD]
    8.31 -                       addIs [st0_in_state], simpset()));
    8.32 -qed "increasingD";
    8.33 -
    8.34 -Goalw [increasing_def, stable_def]
    8.35 - "F \\<in> increasing[A](r, %s. c) <-> F \\<in> program & c \\<in> A";
    8.36 -by (subgoal_tac "\\<exists>x. x \\<in> state" 1);
    8.37 -by (auto_tac (claset() addDs [stable_type RS subsetD]
    8.38 -                       addIs [st0_in_state], simpset()));
    8.39 -qed "increasing_constant";
    8.40 -Addsimps [increasing_constant];
    8.41 -
    8.42 -Goalw [increasing_def, stable_def, part_order_def, 
    8.43 -       constrains_def, mono1_def, metacomp_def]
    8.44 -"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==> \
    8.45 -\  increasing[A](r, f) <= increasing[B](s, g comp f)";
    8.46 -by (Clarify_tac 1);
    8.47 -by (Asm_full_simp_tac 1);
    8.48 -by (Clarify_tac 1);
    8.49 -by (subgoal_tac "xa \\<in> state" 1);
    8.50 -by (blast_tac (claset() addSDs [ActsD]) 2);
    8.51 -by (subgoal_tac "<f(xb), f(xb)>:r" 1);
    8.52 -by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
    8.53 -by (rotate_tac 5 1);
    8.54 -by (dres_inst_tac [("x", "f(xb)")] bspec 1);
    8.55 -by (rotate_tac ~1 2);
    8.56 -by (dres_inst_tac [("x", "act")] bspec 2);
    8.57 -by (ALLGOALS(Asm_full_simp_tac));
    8.58 -by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
    8.59 -by (Blast_tac 1);
    8.60 -by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
    8.61 -by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
    8.62 -by (ALLGOALS(Asm_simp_tac));
    8.63 -qed "subset_increasing_comp";
    8.64 -
    8.65 -Goal "[| F \\<in> increasing[A](r, f); mono1(A, r, B, s, g); \
    8.66 -\        refl(A, r); trans[B](s) |] ==> F \\<in> increasing[B](s, g comp f)";
    8.67 -by (rtac (subset_increasing_comp RS subsetD) 1);
    8.68 -by Auto_tac;
    8.69 -qed "imp_increasing_comp";
    8.70 -
    8.71 -Goalw [increasing_def, Lt_def]
    8.72 -   "increasing[nat](Le, f) <= increasing[nat](Lt, f)";
    8.73 -by Auto_tac;
    8.74 -qed "strict_increasing";
    8.75 -
    8.76 -Goalw [increasing_def, Gt_def, Ge_def]
    8.77 -   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)";
    8.78 -by Auto_tac;
    8.79 -by (etac natE 1);
    8.80 -by (auto_tac (claset(), simpset() addsimps [stable_def]));
    8.81 -qed "strict_gt_increasing";
    8.82 -
    8.83 -(** Increasing **)
    8.84 -
    8.85 -Goalw [increasing_def, Increasing_def]
    8.86 -     "F \\<in> increasing[A](r, f) ==> F \\<in> Increasing[A](r, f)";
    8.87 -by (auto_tac (claset() addIs [stable_imp_Stable], simpset())); 
    8.88 -qed "increasing_imp_Increasing";
    8.89 -
    8.90 -Goalw [Increasing_def] "Increasing[A](r, f) <= program";
    8.91 -by Auto_tac;
    8.92 -qed "Increasing_type";
    8.93 -
    8.94 -Goalw [Increasing_def] "F \\<in> Increasing[A](r, f) ==> F \\<in> program";
    8.95 -by Auto_tac;
    8.96 -qed "Increasing_into_program";
    8.97 -
    8.98 -Goalw [Increasing_def]
    8.99 -"[| F \\<in> Increasing[A](r, f); a \\<in> A |] ==> F \\<in> Stable({s \\<in> state. <a,f(s)>:r})";
   8.100 -by (Blast_tac 1);
   8.101 -qed "Increasing_imp_Stable";
   8.102 -
   8.103 -Goalw [Increasing_def]
   8.104 -"F \\<in> Increasing[A](r, f) ==> F \\<in> program & (\\<exists>a. a \\<in> A) & (\\<forall>s \\<in> state. f(s):A)";
   8.105 -by (subgoal_tac "\\<exists>x. x \\<in> state" 1);
   8.106 -by (auto_tac (claset() addIs [st0_in_state], simpset()));
   8.107 -qed "IncreasingD";
   8.108 -
   8.109 -Goal
   8.110 -"F \\<in> Increasing[A](r, %s. c) <-> F \\<in> program & (c \\<in> A)";
   8.111 -by (subgoal_tac "\\<exists>x. x \\<in> state" 1);
   8.112 -by (auto_tac (claset() addSDs [IncreasingD]
   8.113 -                       addIs [st0_in_state,
   8.114 -                   increasing_imp_Increasing], simpset()));
   8.115 -qed "Increasing_constant";
   8.116 -Addsimps [Increasing_constant];
   8.117 -
   8.118 -Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def, 
   8.119 -       constrains_def, mono1_def, metacomp_def]
   8.120 -"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
   8.121 -\  Increasing[A](r, f) <= Increasing[B](s, g comp f)";
   8.122 -by Safe_tac;
   8.123 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
   8.124 -by (subgoal_tac "xb \\<in> state & xa \\<in> state" 1);
   8.125 -by (asm_simp_tac (simpset() addsimps [ActsD]) 2);
   8.126 -by (subgoal_tac "<f(xb), f(xb)>:r" 1);
   8.127 -by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   8.128 -by (rotate_tac 5 1);
   8.129 -by (dres_inst_tac [("x", "f(xb)")] bspec 1);
   8.130 -by (ALLGOALS(Asm_full_simp_tac));
   8.131 -by (Clarify_tac 1);
   8.132 -by (rotate_tac ~2 1);
   8.133 -by (dres_inst_tac [("x", "act")] bspec 1);
   8.134 -by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
   8.135 -by (ALLGOALS(Asm_full_simp_tac));
   8.136 -by (Blast_tac 1);
   8.137 -by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
   8.138 -by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
   8.139 -by (ALLGOALS(Asm_full_simp_tac));
   8.140 -qed "subset_Increasing_comp";
   8.141 -
   8.142 -Goal "[| F \\<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |]  \
   8.143 -\ ==> F \\<in> Increasing[B](s, g comp f)";
   8.144 -by (rtac (subset_Increasing_comp RS subsetD) 1);
   8.145 -by Auto_tac;
   8.146 -qed "imp_Increasing_comp";
   8.147 -  
   8.148 -Goalw [Increasing_def, Lt_def]
   8.149 -"Increasing[nat](Le, f) <= Increasing[nat](Lt, f)";
   8.150 -by Auto_tac;
   8.151 -qed "strict_Increasing";
   8.152 -
   8.153 -Goalw [Increasing_def, Ge_def, Gt_def] 
   8.154 -"Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)";
   8.155 -by Auto_tac;
   8.156 -by (etac natE 1);
   8.157 -by (auto_tac (claset(), simpset() addsimps [Stable_def]));
   8.158 -qed "strict_gt_Increasing";
   8.159 -
   8.160 -(** Two-place monotone operations **)
   8.161 -
   8.162 -Goalw [increasing_def, stable_def, 
   8.163 -       part_order_def, constrains_def, mono2_def]
   8.164 -"[| F \\<in> increasing[A](r, f); F \\<in> increasing[B](s, g); \
   8.165 -\   mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
   8.166 -\  F \\<in> increasing[C](t, %x. h(f(x), g(x)))";
   8.167 -by (Clarify_tac 1);
   8.168 -by (Asm_full_simp_tac 1);
   8.169 -by (Clarify_tac 1);
   8.170 -by (rename_tac "xa xb" 1);
   8.171 -by (subgoal_tac "xb \\<in> state & xa \\<in> state" 1);
   8.172 -by (blast_tac (claset() addSDs [ActsD]) 2);
   8.173 -by (subgoal_tac "<f(xb), f(xb)>:r & <g(xb), g(xb)>:s" 1);
   8.174 -by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   8.175 -by (rotate_tac 6 1);
   8.176 -by (dres_inst_tac [("x", "f(xb)")] bspec 1);
   8.177 -by (rotate_tac 1 2);
   8.178 -by (dres_inst_tac [("x", "g(xb)")] bspec 2);
   8.179 -by (ALLGOALS(Asm_simp_tac));
   8.180 -by (rotate_tac ~1 1);
   8.181 -by (dres_inst_tac [("x", "act")] bspec 1);
   8.182 -by (rotate_tac ~3 2);
   8.183 -by (dres_inst_tac [("x", "act")] bspec 2);
   8.184 -by (ALLGOALS(Asm_full_simp_tac));
   8.185 -by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
   8.186 -by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
   8.187 -by (Blast_tac 1);
   8.188 -by (Blast_tac 1);
   8.189 -by (rotate_tac ~4 1);
   8.190 -by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
   8.191 -by (rotate_tac ~1 3);
   8.192 -by (dres_inst_tac [("x", "g(xa)"), ("x1", "g(xb)")] (bspec RS bspec) 3);
   8.193 -by (ALLGOALS(Asm_full_simp_tac));
   8.194 -by (res_inst_tac [("b", "h(f(xb), g(xb))"), ("A", "C")] trans_onD 1);
   8.195 -by (ALLGOALS(Asm_full_simp_tac));
   8.196 -qed "imp_increasing_comp2";
   8.197 -
   8.198 -Goalw [Increasing_def, stable_def, 
   8.199 -       part_order_def, constrains_def, mono2_def, Stable_def, Constrains_def]
   8.200 -"[| F \\<in> Increasing[A](r, f); F \\<in> Increasing[B](s, g); \
   8.201 -\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
   8.202 -\ F \\<in> Increasing[C](t, %x. h(f(x), g(x)))";
   8.203 -by Safe_tac;
   8.204 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
   8.205 -by (subgoal_tac "xa \\<in> state & x \\<in> state" 1);
   8.206 -by (blast_tac (claset() addSDs [ActsD]) 2);
   8.207 -by (subgoal_tac "<f(xa), f(xa)>:r & <g(xa), g(xa)>:s" 1);
   8.208 -by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   8.209 -by (rotate_tac 6 1);
   8.210 -by (dres_inst_tac [("x", "f(xa)")] bspec 1);
   8.211 -by (rotate_tac 1 2);
   8.212 -by (dres_inst_tac [("x", "g(xa)")] bspec 2);
   8.213 -by (ALLGOALS(Asm_simp_tac));
   8.214 -by (Clarify_tac 1);
   8.215 -by (rotate_tac ~2 1);
   8.216 -by (dres_inst_tac [("x", "act")] bspec 1);
   8.217 -by (rotate_tac ~3 2);
   8.218 -by (dres_inst_tac [("x", "act")] bspec 2);
   8.219 -by (ALLGOALS(Asm_full_simp_tac));
   8.220 -by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 1);
   8.221 -by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 2);
   8.222 -by (Blast_tac 1);
   8.223 -by (Blast_tac 1);
   8.224 -by (rotate_tac ~9 1);
   8.225 -by (dres_inst_tac [("x", "f(x)"), ("x1", "f(xa)")] (bspec RS bspec) 1);
   8.226 -by (rotate_tac ~1 3);
   8.227 -by (dres_inst_tac [("x", "g(x)"), ("x1", "g(xa)")] (bspec RS bspec) 3);
   8.228 -by (ALLGOALS(Asm_full_simp_tac));
   8.229 -by (res_inst_tac [("b", "h(f(xa), g(xa))"), ("A", "C")] trans_onD 1);
   8.230 -by (ALLGOALS(Asm_full_simp_tac));
   8.231 -qed "imp_Increasing_comp2";
   8.232 -
     9.1 --- a/src/ZF/UNITY/Increasing.thy	Tue Jul 08 11:44:30 2003 +0200
     9.2 +++ b/src/ZF/UNITY/Increasing.thy	Wed Jul 09 11:39:34 2003 +0200
     9.3 @@ -1,32 +1,231 @@
     9.4  (*  Title:      ZF/UNITY/Increasing
     9.5 -    ID:         $Id$
     9.6 +    ID:         $Id \<in> Increasing.thy,v 1.2 2003/06/02 09:17:52 paulson Exp $
     9.7      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     9.8      Copyright   2001  University of Cambridge
     9.9  
    9.10 -The "Increasing" relation of Charpentier.
    9.11 -
    9.12  Increasing's parameters are a state function f, a domain A and an order
    9.13  relation r over the domain A. 
    9.14  *)
    9.15  
    9.16 -Increasing = Constrains + Monotonicity +
    9.17 +header{*Charpentier's "Increasing" Relation*}
    9.18 +
    9.19 +theory Increasing = Constrains + Monotonicity:
    9.20 +
    9.21  constdefs
    9.22  
    9.23 -  increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')")
    9.24 +  increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')")
    9.25    "increasing[A](r, f) ==
    9.26 -    {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) &
    9.27 -                (ALL x:state. f(x):A)}"
    9.28 +    {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) &
    9.29 +                (\<forall>x \<in> state. f(x):A)}"
    9.30    
    9.31 -  Increasing :: [i, i, i=>i] => i ("Increasing[_]'(_, _')")
    9.32 +  Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')")
    9.33    "Increasing[A](r, f) ==
    9.34 -    {F:program. (ALL k:A. F:Stable({s:state. <k, f(s)>:r})) &
    9.35 -                (ALL x:state. f(x):A)}"
    9.36 +    {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
    9.37 +                (\<forall>x \<in> state. f(x):A)}"
    9.38  
    9.39  syntax
    9.40 -  IncWrt      ::  [i=>i, i, i] => i ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
    9.41 +  IncWrt ::  "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
    9.42  
    9.43  translations
    9.44    "IncWrt(f,r,A)" => "Increasing[A](r,f)"
    9.45  
    9.46 +
    9.47 +(** increasing **)
    9.48 +
    9.49 +lemma increasing_type: "increasing[A](r, f) <= program"
    9.50 +by (unfold increasing_def, blast)
    9.51 +
    9.52 +lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program"
    9.53 +by (unfold increasing_def, blast)
    9.54 +
    9.55 +lemma increasing_imp_stable: 
    9.56 +"[| F \<in> increasing[A](r, f); x \<in> A |] ==>F \<in> stable({s \<in> state. <x, f(s)>:r})"
    9.57 +by (unfold increasing_def, blast)
    9.58 +
    9.59 +lemma increasingD: 
    9.60 +"F \<in> increasing[A](r,f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)"
    9.61 +apply (unfold increasing_def)
    9.62 +apply (subgoal_tac "\<exists>x. x \<in> state")
    9.63 +apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
    9.64 +done
    9.65 +
    9.66 +lemma increasing_constant [simp]: 
    9.67 + "F \<in> increasing[A](r, %s. c) <-> F \<in> program & c \<in> A"
    9.68 +apply (unfold increasing_def stable_def)
    9.69 +apply (subgoal_tac "\<exists>x. x \<in> state")
    9.70 +apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state)
    9.71 +done
    9.72 +
    9.73 +lemma subset_increasing_comp: 
    9.74 +"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==>  
    9.75 +   increasing[A](r, f) <= increasing[B](s, g comp f)"
    9.76 +apply (unfold increasing_def stable_def part_order_def 
    9.77 +       constrains_def mono1_def metacomp_def, clarify, simp)
    9.78 +apply clarify
    9.79 +apply (subgoal_tac "xa \<in> state")
    9.80 +prefer 2 apply (blast dest!: ActsD)
    9.81 +apply (subgoal_tac "<f (xb), f (xb) >:r")
    9.82 +prefer 2 apply (force simp add: refl_def)
    9.83 +apply (rotate_tac 5)
    9.84 +apply (drule_tac x = "f (xb) " in bspec)
    9.85 +apply (rotate_tac [2] -1)
    9.86 +apply (drule_tac [2] x = act in bspec, simp_all)
    9.87 +apply (drule_tac A = "act``?u" and c = xa in subsetD, blast)
    9.88 +apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
    9.89 +apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
    9.90 +apply simp_all
    9.91 +done
    9.92 +
    9.93 +lemma imp_increasing_comp:
    9.94 +     "[| F \<in> increasing[A](r, f); mono1(A, r, B, s, g);  
    9.95 +         refl(A, r); trans[B](s) |] ==> F \<in> increasing[B](s, g comp f)"
    9.96 +by (rule subset_increasing_comp [THEN subsetD], auto)
    9.97 +
    9.98 +lemma strict_increasing: 
    9.99 +   "increasing[nat](Le, f) <= increasing[nat](Lt, f)"
   9.100 +by (unfold increasing_def Lt_def, auto)
   9.101 +
   9.102 +lemma strict_gt_increasing: 
   9.103 +   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)"
   9.104 +apply (unfold increasing_def Gt_def Ge_def, auto)
   9.105 +apply (erule natE)
   9.106 +apply (auto simp add: stable_def)
   9.107 +done
   9.108 +
   9.109 +(** Increasing **)
   9.110 +
   9.111 +lemma increasing_imp_Increasing: 
   9.112 +     "F \<in> increasing[A](r, f) ==> F \<in> Increasing[A](r, f)"
   9.113 +
   9.114 +apply (unfold increasing_def Increasing_def)
   9.115 +apply (auto intro: stable_imp_Stable)
   9.116 +done
   9.117 +
   9.118 +lemma Increasing_type: "Increasing[A](r, f) <= program"
   9.119 +by (unfold Increasing_def, auto)
   9.120 +
   9.121 +lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program"
   9.122 +by (unfold Increasing_def, auto)
   9.123 +
   9.124 +lemma Increasing_imp_Stable: 
   9.125 +"[| F \<in> Increasing[A](r, f); a \<in> A |] ==> F \<in> Stable({s \<in> state. <a,f(s)>:r})"
   9.126 +by (unfold Increasing_def, blast)
   9.127 +
   9.128 +lemma IncreasingD: 
   9.129 +"F \<in> Increasing[A](r, f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)"
   9.130 +apply (unfold Increasing_def)
   9.131 +apply (subgoal_tac "\<exists>x. x \<in> state")
   9.132 +apply (auto intro: st0_in_state)
   9.133 +done
   9.134 +
   9.135 +lemma Increasing_constant [simp]: 
   9.136 +     "F \<in> Increasing[A](r, %s. c) <-> F \<in> program & (c \<in> A)"
   9.137 +apply (subgoal_tac "\<exists>x. x \<in> state")
   9.138 +apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing)
   9.139 +done
   9.140 +
   9.141 +lemma subset_Increasing_comp: 
   9.142 +"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==>  
   9.143 +   Increasing[A](r, f) <= Increasing[B](s, g comp f)"
   9.144 +apply (unfold Increasing_def Stable_def Constrains_def part_order_def 
   9.145 +       constrains_def mono1_def metacomp_def, safe)
   9.146 +apply (simp_all add: ActsD)
   9.147 +apply (subgoal_tac "xb \<in> state & xa \<in> state")
   9.148 + prefer 2 apply (simp add: ActsD)
   9.149 +apply (subgoal_tac "<f (xb), f (xb) >:r")
   9.150 +prefer 2 apply (force simp add: refl_def)
   9.151 +apply (rotate_tac 5)
   9.152 +apply (drule_tac x = "f (xb) " in bspec)
   9.153 +apply simp_all
   9.154 +apply clarify
   9.155 +apply (rotate_tac -2)
   9.156 +apply (drule_tac x = act in bspec)
   9.157 +apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast)
   9.158 +apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
   9.159 +apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
   9.160 +apply simp_all
   9.161 +done
   9.162 +
   9.163 +lemma imp_Increasing_comp:
   9.164 + "[| F \<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] 
   9.165 +  ==> F \<in> Increasing[B](s, g comp f)"
   9.166 +apply (rule subset_Increasing_comp [THEN subsetD], auto)
   9.167 +done
   9.168 +  
   9.169 +lemma strict_Increasing: "Increasing[nat](Le, f) <= Increasing[nat](Lt, f)"
   9.170 +by (unfold Increasing_def Lt_def, auto)
   9.171 +
   9.172 +lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)"
   9.173 +apply (unfold Increasing_def Ge_def Gt_def, auto)
   9.174 +apply (erule natE)
   9.175 +apply (auto simp add: Stable_def)
   9.176 +done
   9.177 +
   9.178 +(** Two-place monotone operations **)
   9.179 +
   9.180 +lemma imp_increasing_comp2: 
   9.181 +"[| F \<in> increasing[A](r, f); F \<in> increasing[B](s, g);  
   9.182 +    mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |]
   9.183 + ==> F \<in> increasing[C](t, %x. h(f(x), g(x)))"
   9.184 +apply (unfold increasing_def stable_def 
   9.185 +       part_order_def constrains_def mono2_def, clarify, simp)
   9.186 +apply clarify
   9.187 +apply (rename_tac xa xb)
   9.188 +apply (subgoal_tac "xb \<in> state & xa \<in> state")
   9.189 + prefer 2 apply (blast dest!: ActsD)
   9.190 +apply (subgoal_tac "<f (xb), f (xb) >:r & <g (xb), g (xb) >:s")
   9.191 +prefer 2 apply (force simp add: refl_def)
   9.192 +apply (rotate_tac 6)
   9.193 +apply (drule_tac x = "f (xb) " in bspec)
   9.194 +apply (rotate_tac [2] 1)
   9.195 +apply (drule_tac [2] x = "g (xb) " in bspec)
   9.196 +apply simp_all
   9.197 +apply (rotate_tac -1)
   9.198 +apply (drule_tac x = act in bspec)
   9.199 +apply (rotate_tac [2] -3)
   9.200 +apply (drule_tac [2] x = act in bspec, simp_all)
   9.201 +apply (drule_tac A = "act``?u" and c = xa in subsetD)
   9.202 +apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast)
   9.203 +apply (rotate_tac -4)
   9.204 +apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
   9.205 +apply (rotate_tac [3] -1)
   9.206 +apply (drule_tac [3] x = "g (xa) " and x1 = "g (xb) " in bspec [THEN bspec])
   9.207 +apply simp_all
   9.208 +apply (rule_tac b = "h (f (xb), g (xb))" and A = C in trans_onD)
   9.209 +apply simp_all
   9.210 +done
   9.211 +
   9.212 +lemma imp_Increasing_comp2: 
   9.213 +"[| F \<in> Increasing[A](r, f); F \<in> Increasing[B](s, g);  
   9.214 +  mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==>  
   9.215 +  F \<in> Increasing[C](t, %x. h(f(x), g(x)))"
   9.216 +apply (unfold Increasing_def stable_def 
   9.217 +       part_order_def constrains_def mono2_def Stable_def Constrains_def, safe)
   9.218 +apply (simp_all add: ActsD)
   9.219 +apply (subgoal_tac "xa \<in> state & x \<in> state")
   9.220 +prefer 2 apply (blast dest!: ActsD)
   9.221 +apply (subgoal_tac "<f (xa), f (xa) >:r & <g (xa), g (xa) >:s")
   9.222 +prefer 2 apply (force simp add: refl_def)
   9.223 +apply (rotate_tac 6)
   9.224 +apply (drule_tac x = "f (xa) " in bspec)
   9.225 +apply (rotate_tac [2] 1)
   9.226 +apply (drule_tac [2] x = "g (xa) " in bspec)
   9.227 +apply simp_all
   9.228 +apply clarify
   9.229 +apply (rotate_tac -2)
   9.230 +apply (drule_tac x = act in bspec)
   9.231 +apply (rotate_tac [2] -3)
   9.232 +apply (drule_tac [2] x = act in bspec, simp_all)
   9.233 +apply (drule_tac A = "act``?u" and c = x in subsetD)
   9.234 +apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast)
   9.235 +apply (rotate_tac -9)
   9.236 +apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
   9.237 +apply (rotate_tac [3] -1)
   9.238 +apply (drule_tac [3] x = "g (x) " and x1 = "g (xa) " in bspec [THEN bspec])
   9.239 +apply simp_all
   9.240 +apply (rule_tac b = "h (f (xa), g (xa))" and A = C in trans_onD)
   9.241 +apply simp_all
   9.242 +done
   9.243 +
   9.244    
   9.245  end
    10.1 --- a/src/ZF/UNITY/Monotonicity.ML	Tue Jul 08 11:44:30 2003 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,102 +0,0 @@
    10.4 -(*  Title:      ZF/UNITY/Monotonicity.ML
    10.5 -    ID:         $Id \\<in> Monotonicity.ML,v 1.2 2003/06/26 13:48:33 paulson Exp $
    10.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    10.7 -    Copyright   2002  University of Cambridge
    10.8 -
    10.9 -Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
   10.10 -*)
   10.11 -
   10.12 -
   10.13 -(*TOO SLOW as a default simprule????
   10.14 -Addsimps [append_left_is_Nil_iff,append_left_is_Nil_iff2];
   10.15 -*)
   10.16 -
   10.17 -Goalw [mono1_def]
   10.18 -  "[| mono1(A, r, B, s, f); <x, y>:r; x \\<in> A; y \\<in> A |] ==> <f(x), f(y)>:s";
   10.19 -by Auto_tac;
   10.20 -qed "mono1D";
   10.21 -
   10.22 -Goalw [mono2_def]
   10.23 -"[| 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 |] ==> \
   10.24 -\  <f(x, u), f(y,v)>:t";
   10.25 -by Auto_tac;
   10.26 -qed "mono2D";
   10.27 -
   10.28 -
   10.29 -(** Monotonicity of take **)
   10.30 -
   10.31 -(*????premises too strong*)
   10.32 -Goal "[| i le j; xs \\<in> list(A); i \\<in> nat; j \\<in> nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
   10.33 -by (case_tac "length(xs) le i" 1);
   10.34 -by (subgoal_tac "length(xs) le j" 1);
   10.35 -by (blast_tac (claset() addIs [le_trans]) 2);
   10.36 -by (Asm_simp_tac 1);
   10.37 -by (dtac not_lt_imp_le 1);
   10.38 -by Auto_tac;
   10.39 -by (case_tac "length(xs) le j" 1);
   10.40 -by (auto_tac (claset(), simpset() addsimps [take_prefix]));
   10.41 -by (dtac not_lt_imp_le 1);
   10.42 -by Auto_tac;
   10.43 -by (dres_inst_tac [("m", "i")] less_imp_succ_add 1);
   10.44 -by Auto_tac;
   10.45 -by (subgoal_tac "i #+ k le length(xs)" 1);
   10.46 -by (blast_tac (claset() addIs [leI]) 2);
   10.47 -by (asm_full_simp_tac (simpset() addsimps [take_add, prefix_iff, take_type, drop_type]) 1);
   10.48 -qed "take_mono_left";
   10.49 -
   10.50 -Goal "[| <xs, ys>:prefix(A); i \\<in> nat |] ==> <take(i, xs), take(i, ys)>:prefix(A)"; 
   10.51 -by (auto_tac (claset(), simpset() addsimps [prefix_iff]));
   10.52 -qed "take_mono_right";
   10.53 -
   10.54 -Goal "[| i le j; <xs, ys>:prefix(A); i \\<in> nat; j \\<in> nat |] ==> <take(i, xs), take(j, ys)>:prefix(A)";
   10.55 -by (res_inst_tac [("b", "take(j, xs)")] prefix_trans 1);
   10.56 -by (auto_tac (claset() addDs [prefix_type RS subsetD]
   10.57 -                       addIs [take_mono_left, take_mono_right], simpset()));
   10.58 -qed "take_mono";
   10.59 -
   10.60 -Goalw [mono2_def, Le_def] "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)";
   10.61 -by Auto_tac;
   10.62 -by (blast_tac (claset() addIs [take_mono]) 1);
   10.63 -qed "mono_take";
   10.64 -Addsimps [mono_take];
   10.65 -AddIs [mono_take];
   10.66 -
   10.67 -(** Monotonicity of length **)
   10.68 -
   10.69 -bind_thm("length_mono", prefix_length_le);
   10.70 -
   10.71 -Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le, length)";
   10.72 -by (auto_tac (claset() addDs [prefix_length_le],
   10.73 -             simpset() addsimps [Le_def]));
   10.74 -qed "mono_length";
   10.75 -Addsimps [mono_length];
   10.76 -AddIs [mono_length];
   10.77 -
   10.78 -(** Monotonicity of Un **)
   10.79 -
   10.80 -Goalw [mono2_def, SetLe_def]  
   10.81 - "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)";
   10.82 -by Auto_tac;
   10.83 -qed "mono_Un";
   10.84 -Addsimps [mono_Un];
   10.85 -AddIs [mono_Un];
   10.86 -
   10.87 -(* Monotonicity of multiset union *)
   10.88 -
   10.89 -Goalw [mono2_def, MultLe_def]  
   10.90 -   "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)";
   10.91 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   10.92 -by (REPEAT(blast_tac (claset() addIs [munion_multirel_mono,
   10.93 -                                munion_multirel_mono1,
   10.94 -                                munion_multirel_mono2,
   10.95 -                                multiset_into_Mult]) 1));
   10.96 -qed "mono_munion";
   10.97 -Addsimps [mono_munion];
   10.98 -AddIs [mono_munion];
   10.99 -
  10.100 -Goalw [mono1_def, Le_def] "mono1(nat, Le, nat, Le, succ)";
  10.101 -by Auto_tac;
  10.102 -qed "mono_succ";
  10.103 -Addsimps [mono_succ];
  10.104 -AddIs [mono_succ];
  10.105 -
    11.1 --- a/src/ZF/UNITY/Monotonicity.thy	Tue Jul 08 11:44:30 2003 +0200
    11.2 +++ b/src/ZF/UNITY/Monotonicity.thy	Wed Jul 09 11:39:34 2003 +0200
    11.3 @@ -1,30 +1,133 @@
    11.4  (*  Title:      ZF/UNITY/Monotonicity.thy
    11.5 -    ID:         $Id$
    11.6 +    ID:         $Id \<in> Monotonicity.thy,v 1.1 2003/05/28 16:13:42 paulson Exp $
    11.7      Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    11.8      Copyright   2002  University of Cambridge
    11.9  
   11.10  Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
   11.11  *)
   11.12  
   11.13 -Monotonicity =  GenPrefix  +  MultisetSum +
   11.14 +header{*Monotonicity of an Operator WRT a Relation*}
   11.15 +
   11.16 +theory Monotonicity = GenPrefix + MultisetSum:
   11.17 +
   11.18  constdefs
   11.19 -mono1 :: [i, i, i, i, i=>i] => o
   11.20 -"mono1(A, r, B, s, f) ==
   11.21 - (ALL x:A. ALL y:A. <x, y>:r --> <f(x), f(y)>:s) & (ALL x:A. f(x):B)"
   11.22 +
   11.23 +  mono1 :: "[i, i, i, i, i=>i] => o"
   11.24 +  "mono1(A, r, B, s, f) ==
   11.25 +    (\<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)"
   11.26  
   11.27    (* monotonicity of a 2-place meta-function f *)
   11.28  
   11.29 -  mono2 :: [i, i, i, i, i, i, [i,i]=>i] => o
   11.30 -  "mono2(A, r, B, s, C, t, f) == (ALL x:A. ALL y:A. ALL u:B. ALL v:B.
   11.31 -    <x, y>:r & <u,v>:s --> <f(x, u), f(y,v)>:t) &
   11.32 -    (ALL x:A. ALL y:B. f(x,y):C)"
   11.33 +  mono2 :: "[i, i, i, i, i, i, [i,i]=>i] => o"
   11.34 +  "mono2(A, r, B, s, C, t, f) == 
   11.35 +    (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>u \<in> B. \<forall>v \<in> B.
   11.36 +              <x,y> \<in> r & <u,v> \<in> s --> <f(x,u), f(y,v)> \<in> t) &
   11.37 +    (\<forall>x \<in> A. \<forall>y \<in> B. f(x,y) \<in> C)"
   11.38  
   11.39   (* Internalized relations on sets and multisets *)
   11.40  
   11.41 -  SetLe :: i =>i
   11.42 -  "SetLe(A) == {<x, y>:Pow(A)*Pow(A). x <= y}"
   11.43 +  SetLe :: "i =>i"
   11.44 +  "SetLe(A) == {<x,y> \<in> Pow(A)*Pow(A). x <= y}"
   11.45  
   11.46 -  MultLe :: [i,i] =>i
   11.47 +  MultLe :: "[i,i] =>i"
   11.48    "MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
   11.49  
   11.50 +
   11.51 +
   11.52 +lemma mono1D: 
   11.53 +  "[| mono1(A, r, B, s, f); <x, y> \<in> r; x \<in> A; y \<in> A |] ==> <f(x), f(y)> \<in> s"
   11.54 +by (unfold mono1_def, auto)
   11.55 +
   11.56 +lemma mono2D: 
   11.57 +     "[| mono2(A, r, B, s, C, t, f);  
   11.58 +         <x, y> \<in> r; <u,v> \<in> s; x \<in> A; y \<in> A; u \<in> B; v \<in> B |] 
   11.59 +      ==> <f(x, u), f(y,v)> \<in> t"
   11.60 +by (unfold mono2_def, auto)
   11.61 +
   11.62 +
   11.63 +(** Monotonicity of take **)
   11.64 +
   11.65 +lemma take_mono_left_lemma:
   11.66 +     "[| i le j; xs \<in> list(A); i \<in> nat; j \<in> nat |] 
   11.67 +      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
   11.68 +apply (case_tac "length (xs) le i")
   11.69 + apply (subgoal_tac "length (xs) le j")
   11.70 +  apply (simp)
   11.71 + apply (blast intro: le_trans)
   11.72 +apply (drule not_lt_imp_le, auto)
   11.73 +apply (case_tac "length (xs) le j")
   11.74 + apply (auto simp add: take_prefix)
   11.75 +apply (drule not_lt_imp_le, auto)
   11.76 +apply (drule_tac m = i in less_imp_succ_add, auto)
   11.77 +apply (subgoal_tac "i #+ k le length (xs) ")
   11.78 + apply (simp add: take_add prefix_iff take_type drop_type)
   11.79 +apply (blast intro: leI)
   11.80 +done
   11.81 +
   11.82 +lemma take_mono_left:
   11.83 +     "[| i le j; xs \<in> list(A); j \<in> nat |]
   11.84 +      ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
   11.85 +by (blast intro: Nat.le_in_nat take_mono_left_lemma) 
   11.86 +
   11.87 +lemma take_mono_right:
   11.88 +     "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 
   11.89 +      ==> <take(i, xs), take(i, ys)> \<in> prefix(A)"
   11.90 +by (auto simp add: prefix_iff)
   11.91 +
   11.92 +lemma take_mono:
   11.93 +     "[| i le j; <xs, ys> \<in> prefix(A); j \<in> nat |]
   11.94 +      ==> <take(i, xs), take(j, ys)> \<in> prefix(A)"
   11.95 +apply (rule_tac b = "take (j, xs) " in prefix_trans)
   11.96 +apply (auto dest: prefix_type [THEN subsetD] intro: take_mono_left take_mono_right)
   11.97 +done
   11.98 +
   11.99 +lemma mono_take [iff]:
  11.100 +     "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)"
  11.101 +apply (unfold mono2_def Le_def, auto)
  11.102 +apply (blast intro: take_mono)
  11.103 +done
  11.104 +
  11.105 +(** Monotonicity of length **)
  11.106 +
  11.107 +lemmas length_mono = prefix_length_le
  11.108 +
  11.109 +lemma mono_length [iff]:
  11.110 +     "mono1(list(A), prefix(A), nat, Le, length)"
  11.111 +apply (unfold mono1_def)
  11.112 +apply (auto dest: prefix_length_le simp add: Le_def)
  11.113 +done
  11.114 +
  11.115 +(** Monotonicity of Un **)
  11.116 +
  11.117 +lemma mono_Un [iff]: 
  11.118 +     "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)"
  11.119 +by (unfold mono2_def SetLe_def, auto)
  11.120 +
  11.121 +(* Monotonicity of multiset union *)
  11.122 +
  11.123 +lemma mono_munion [iff]: 
  11.124 +     "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
  11.125 +apply (unfold mono2_def MultLe_def)
  11.126 +apply (auto simp add: Mult_iff_multiset)
  11.127 +apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
  11.128 +done
  11.129 +
  11.130 +lemma mono_succ [iff]: "mono1(nat, Le, nat, Le, succ)"
  11.131 +by (unfold mono1_def Le_def, auto)
  11.132 +
  11.133 +ML{*
  11.134 +val mono1D = thm "mono1D";
  11.135 +val mono2D = thm "mono2D";
  11.136 +val take_mono_left_lemma = thm "take_mono_left_lemma";
  11.137 +val take_mono_left = thm "take_mono_left";
  11.138 +val take_mono_right = thm "take_mono_right";
  11.139 +val take_mono = thm "take_mono";
  11.140 +val mono_take = thm "mono_take";
  11.141 +val length_mono = thm "length_mono";
  11.142 +val mono_length = thm "mono_length";
  11.143 +val mono_Un = thm "mono_Un";
  11.144 +val mono_munion = thm "mono_munion";
  11.145 +val mono_succ = thm "mono_succ";
  11.146 +*}
  11.147 +
  11.148  end
  11.149 \ No newline at end of file
    12.1 --- a/src/ZF/UNITY/Union.thy	Tue Jul 08 11:44:30 2003 +0200
    12.2 +++ b/src/ZF/UNITY/Union.thy	Wed Jul 09 11:39:34 2003 +0200
    12.3 @@ -460,6 +460,17 @@
    12.4  by (auto simp add: OK_iff_ok)
    12.5  
    12.6  
    12.7 +lemma OK_0 [iff]: "OK(0,F)"
    12.8 +by (simp add: OK_def)
    12.9 +
   12.10 +lemma OK_cons_iff:
   12.11 +     "OK(cons(i, I), F) <->  
   12.12 +      (i \<in> I & OK(I, F)) | (i\<notin>I & OK(I, F) & F(i) ok JOIN(I,F))"
   12.13 +apply (simp add: OK_iff_ok)
   12.14 +apply (blast intro: ok_sym) 
   12.15 +done
   12.16 +
   12.17 +
   12.18  subsection{*Allowed*}
   12.19  
   12.20  lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program"