converted more UNITY theories to new-style
authorpaulson
Wed Jan 29 16:34:51 2003 +0100 (2003-01-29)
changeset 13792d1811693899c
parent 13791 3b6ff7ceaf27
child 13793 c02c81fd11b8
converted more UNITY theories to new-style
src/HOL/IsaMakefile
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/Comp/Counter.thy
src/HOL/UNITY/Comp/Counterc.thy
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/UNITY/Union.ML
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Jan 29 16:29:38 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jan 29 16:34:51 2003 +0100
     1.3 @@ -382,13 +382,13 @@
     1.4  
     1.5  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
     1.6    UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
     1.7 -  UNITY/Comp.ML UNITY/Comp.thy UNITY/Detects.thy  UNITY/ELT.thy \
     1.8 +  UNITY/Comp.thy UNITY/Detects.thy  UNITY/ELT.thy \
     1.9    UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \
    1.10    UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \
    1.11 -  UNITY/Guar.ML UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
    1.12 +  UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
    1.13    UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy \
    1.14    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \
    1.15 -  UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML  UNITY/WFair.thy \
    1.16 +  UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML  UNITY/WFair.thy \
    1.17    UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
    1.18    UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
    1.19    UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy  \
     2.1 --- a/src/HOL/UNITY/Comp.ML	Wed Jan 29 16:29:38 2003 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,263 +0,0 @@
     2.4 -(*  Title:      HOL/UNITY/Comp.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1998  University of Cambridge
     2.8 -
     2.9 -Composition
    2.10 -From Chandy and Sanders, "Reasoning About Program Composition"
    2.11 -
    2.12 -Revised by Sidi Ehmety on January 2001
    2.13 -
    2.14 -*)
    2.15 -(*** component <= ***)
    2.16 -Goalw [component_def]
    2.17 -     "H <= F | H <= G ==> H <= (F Join G)";
    2.18 -by Auto_tac;
    2.19 -by (res_inst_tac [("x", "G Join Ga")] exI 1);
    2.20 -by (res_inst_tac [("x", "G Join F")] exI 2);
    2.21 -by (auto_tac (claset(), simpset() addsimps Join_ac));
    2.22 -qed "componentI";
    2.23 -
    2.24 -Goalw [component_def]
    2.25 -     "(F <= G) = \
    2.26 -\     (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)";
    2.27 -by (force_tac (claset() addSIs [exI, program_equalityI], 
    2.28 -	       simpset()) 1);
    2.29 -qed "component_eq_subset";
    2.30 -
    2.31 -Goalw [component_def] "SKIP <= F";
    2.32 -by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1);
    2.33 -qed "component_SKIP";
    2.34 -
    2.35 -Goalw [component_def] "F <= (F :: 'a program)";
    2.36 -by (blast_tac (claset() addIs [Join_SKIP_right]) 1);
    2.37 -qed "component_refl";
    2.38 -
    2.39 -AddIffs [component_SKIP, component_refl];
    2.40 -
    2.41 -Goal "F <= SKIP ==> F = SKIP";
    2.42 -by (auto_tac (claset() addSIs [program_equalityI],
    2.43 -	      simpset() addsimps [component_eq_subset]));
    2.44 -qed "SKIP_minimal";
    2.45 -
    2.46 -Goalw [component_def] "F <= (F Join G)";
    2.47 -by (Blast_tac 1);
    2.48 -qed "component_Join1";
    2.49 -
    2.50 -Goalw [component_def] "G <= (F Join G)";
    2.51 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
    2.52 -by (Blast_tac 1);
    2.53 -qed "component_Join2";
    2.54 -
    2.55 -Goal "F<=G ==> F Join G = G";
    2.56 -by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb]));
    2.57 -qed "Join_absorb1";
    2.58 -
    2.59 -Goal "G<=F ==> F Join G = F";
    2.60 -by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
    2.61 -qed "Join_absorb2";
    2.62 -
    2.63 -Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
    2.64 -by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.65 -by (Blast_tac 1);
    2.66 -qed "JN_component_iff";
    2.67 -
    2.68 -Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
    2.69 -by (blast_tac (claset() addIs [JN_absorb]) 1);
    2.70 -qed "component_JN";
    2.71 -
    2.72 -Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)";
    2.73 -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
    2.74 -qed "component_trans";
    2.75 -
    2.76 -Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)";
    2.77 -by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.78 -by (blast_tac (claset() addSIs [program_equalityI]) 1);
    2.79 -qed "component_antisym";
    2.80 -
    2.81 -Goal "((F Join G) <= H) = (F <= H & G <= H)";
    2.82 -by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
    2.83 -by (Blast_tac 1);
    2.84 -qed "Join_component_iff";
    2.85 -
    2.86 -Goal "[| F <= G; G : A co B |] ==> F : A co B";
    2.87 -by (auto_tac (claset(), 
    2.88 -	      simpset() addsimps [constrains_def, component_eq_subset]));
    2.89 -qed "component_constrains";
    2.90 -
    2.91 -(*Used in Guar.thy to show that programs are partially ordered*)
    2.92 -bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
    2.93 -
    2.94 -
    2.95 -(*** preserves ***)
    2.96 -
    2.97 -val prems = 
    2.98 -Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v";
    2.99 -by (blast_tac (claset() addIs prems) 1);
   2.100 -qed "preservesI";
   2.101 -
   2.102 -Goalw [preserves_def, stable_def, constrains_def]
   2.103 -     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'";
   2.104 -by (Force_tac 1);
   2.105 -qed "preserves_imp_eq";
   2.106 -
   2.107 -Goalw [preserves_def]
   2.108 -     "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
   2.109 -by Auto_tac;
   2.110 -qed "Join_preserves";
   2.111 -
   2.112 -Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
   2.113 -by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1);
   2.114 -by (Blast_tac 1);
   2.115 -qed "JN_preserves";
   2.116 -
   2.117 -Goal "SKIP : preserves v";
   2.118 -by (auto_tac (claset(), simpset() addsimps [preserves_def]));
   2.119 -qed "SKIP_preserves";
   2.120 -
   2.121 -AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
   2.122 -
   2.123 -Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
   2.124 -by (Simp_tac 1);
   2.125 -qed "funPair_apply";
   2.126 -Addsimps [funPair_apply];
   2.127 -
   2.128 -Goal "preserves (funPair v w) = preserves v Int preserves w";
   2.129 -by (auto_tac (claset(),
   2.130 -	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
   2.131 -by (Blast_tac 1);
   2.132 -qed "preserves_funPair";
   2.133 -
   2.134 -(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
   2.135 -AddIffs [preserves_funPair RS eqset_imp_iff];
   2.136 -
   2.137 -
   2.138 -Goal "(funPair f g) o h = funPair (f o h) (g o h)";
   2.139 -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
   2.140 -qed "funPair_o_distrib";
   2.141 -
   2.142 -Goal "fst o (funPair f g) = f";
   2.143 -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
   2.144 -qed "fst_o_funPair";
   2.145 -
   2.146 -Goal "snd o (funPair f g) = g";
   2.147 -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
   2.148 -qed "snd_o_funPair";
   2.149 -Addsimps [fst_o_funPair, snd_o_funPair];
   2.150 -
   2.151 -Goal "preserves v <= preserves (w o v)";
   2.152 -by (force_tac (claset(),
   2.153 -      simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
   2.154 -qed "subset_preserves_o";
   2.155 -
   2.156 -Goal "preserves v <= stable {s. P (v s)}";
   2.157 -by (auto_tac (claset(),
   2.158 -	      simpset() addsimps [preserves_def, stable_def, constrains_def]));
   2.159 -by (rename_tac "s' s" 1);
   2.160 -by (subgoal_tac "v s = v s'" 1);
   2.161 -by (ALLGOALS Force_tac);
   2.162 -qed "preserves_subset_stable";
   2.163 -
   2.164 -Goal "preserves v <= increasing v";
   2.165 -by (auto_tac (claset(),
   2.166 -	      simpset() addsimps [impOfSubs preserves_subset_stable, 
   2.167 -				  increasing_def]));
   2.168 -qed "preserves_subset_increasing";
   2.169 -
   2.170 -Goal "preserves id <= stable A";
   2.171 -by (force_tac (claset(), 
   2.172 -	   simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
   2.173 -qed "preserves_id_subset_stable";
   2.174 -
   2.175 -
   2.176 -(** For use with def_UNION_ok_iff **)
   2.177 -
   2.178 -Goal "safety_prop (preserves v)";
   2.179 -by (auto_tac (claset() addIs [safety_prop_INTER1], 
   2.180 -              simpset() addsimps [preserves_def]));
   2.181 -qed "safety_prop_preserves";
   2.182 -AddIffs [safety_prop_preserves];
   2.183 -
   2.184 -
   2.185 -(** Some lemmas used only in Client.ML **)
   2.186 -
   2.187 -Goal "[| F : stable {s. P (v s) (w s)};   \
   2.188 -\        G : preserves v;  G : preserves w |]               \
   2.189 -\     ==> F Join G : stable {s. P (v s) (w s)}";
   2.190 -by (Asm_simp_tac 1);
   2.191 -by (subgoal_tac "G: preserves (funPair v w)" 1);
   2.192 -by (Asm_simp_tac 2);
   2.193 -by (dres_inst_tac [("P1", "split ?Q")]  
   2.194 -    (impOfSubs preserves_subset_stable) 1);
   2.195 -by Auto_tac;
   2.196 -qed "stable_localTo_stable2";
   2.197 -
   2.198 -Goal "[| F : stable {s. v s <= w s};  G : preserves v;       \
   2.199 -\        F Join G : Increasing w |]               \
   2.200 -\     ==> F Join G : Stable {s. v s <= w s}";
   2.201 -by (auto_tac (claset(), 
   2.202 -	      simpset() addsimps [stable_def, Stable_def, Increasing_def, 
   2.203 -				  Constrains_def, all_conj_distrib]));
   2.204 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
   2.205 -(*The G case remains*)
   2.206 -by (auto_tac (claset(), 
   2.207 -              simpset() addsimps [preserves_def, stable_def, constrains_def]));
   2.208 -by (case_tac "act: Acts F" 1);
   2.209 -by (Blast_tac 1);
   2.210 -(*We have a G-action, so delete assumptions about F-actions*)
   2.211 -by (thin_tac "ALL act:Acts F. ?P act" 1);
   2.212 -by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1);
   2.213 -by (subgoal_tac "v x = v xa" 1);
   2.214 -by (Blast_tac 2);
   2.215 -by Auto_tac;
   2.216 -by (etac order_trans 1);
   2.217 -by (Blast_tac 1);
   2.218 -qed "Increasing_preserves_Stable";
   2.219 -
   2.220 -(** component_of **)
   2.221 -
   2.222 -(*  component_of is stronger than <= *)
   2.223 -Goalw [component_def, component_of_def]
   2.224 -"F component_of H ==> F <= H";
   2.225 -by (Blast_tac 1);
   2.226 -qed "component_of_imp_component";
   2.227 -
   2.228 -
   2.229 -(* component_of satisfies many of the <='s properties *)
   2.230 -Goalw [component_of_def]
   2.231 -"F component_of F";
   2.232 -by (res_inst_tac [("x", "SKIP")] exI 1);
   2.233 -by Auto_tac;
   2.234 -qed "component_of_refl";
   2.235 -
   2.236 -Goalw [component_of_def]
   2.237 -"SKIP component_of F";
   2.238 -by Auto_tac;
   2.239 -qed "component_of_SKIP";
   2.240 -
   2.241 -Addsimps [component_of_refl, component_of_SKIP];
   2.242 -
   2.243 -Goalw [component_of_def]
   2.244 -"[| F component_of G; G component_of H |] ==> F component_of H";
   2.245 -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
   2.246 -qed "component_of_trans";
   2.247 -
   2.248 -bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq);
   2.249 -
   2.250 -(** localize **)
   2.251 -Goalw [localize_def]
   2.252 - "Init (localize v F) = Init F";
   2.253 -by (Simp_tac 1);
   2.254 -qed "localize_Init_eq";
   2.255 -
   2.256 -Goalw [localize_def]
   2.257 - "Acts (localize v F) = Acts F";
   2.258 -by (Simp_tac 1);
   2.259 -qed "localize_Acts_eq";
   2.260 -
   2.261 -Goalw [localize_def]
   2.262 - "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)";
   2.263 -by Auto_tac;
   2.264 -qed "localize_AllowedActs_eq";
   2.265 -
   2.266 -Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq];
     3.1 --- a/src/HOL/UNITY/Comp.thy	Wed Jan 29 16:29:38 2003 +0100
     3.2 +++ b/src/HOL/UNITY/Comp.thy	Wed Jan 29 16:34:51 2003 +0100
     3.3 @@ -13,14 +13,13 @@
     3.4  
     3.5  *)
     3.6  
     3.7 -Comp = Union +
     3.8 +theory Comp = Union:
     3.9  
    3.10 -instance
    3.11 -  program :: (type) ord
    3.12 +instance program :: (type) ord ..
    3.13  
    3.14  defs
    3.15 -  component_def   "F <= H == EX G. F Join G = H"
    3.16 -  strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    3.17 +  component_def:          "F <= H == EX G. F Join G = H"
    3.18 +  strict_component_def:   "(F < (H::'a program)) == (F <= H & F ~= H)"
    3.19  
    3.20  
    3.21  constdefs
    3.22 @@ -28,7 +27,7 @@
    3.23                                      (infixl "component'_of" 50)
    3.24    "F component_of H == EX G. F ok G & F Join G = H"
    3.25  
    3.26 -  strict_component_of :: "'a program\\<Rightarrow>'a program=> bool"
    3.27 +  strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
    3.28                                      (infixl "strict'_component'_of" 50)
    3.29    "F strict_component_of H == F component_of H & F~=H"
    3.30    
    3.31 @@ -41,4 +40,222 @@
    3.32  
    3.33    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    3.34    "funPair f g == %x. (f x, g x)"
    3.35 +
    3.36 +
    3.37 +(*** component <= ***)
    3.38 +lemma componentI: 
    3.39 +     "H <= F | H <= G ==> H <= (F Join G)"
    3.40 +apply (unfold component_def, auto)
    3.41 +apply (rule_tac x = "G Join Ga" in exI)
    3.42 +apply (rule_tac [2] x = "G Join F" in exI)
    3.43 +apply (auto simp add: Join_ac)
    3.44 +done
    3.45 +
    3.46 +lemma component_eq_subset: 
    3.47 +     "(F <= G) =  
    3.48 +      (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
    3.49 +apply (unfold component_def)
    3.50 +apply (force intro!: exI program_equalityI)
    3.51 +done
    3.52 +
    3.53 +lemma component_SKIP [iff]: "SKIP <= F"
    3.54 +apply (unfold component_def)
    3.55 +apply (force intro: Join_SKIP_left)
    3.56 +done
    3.57 +
    3.58 +lemma component_refl [iff]: "F <= (F :: 'a program)"
    3.59 +apply (unfold component_def)
    3.60 +apply (blast intro: Join_SKIP_right)
    3.61 +done
    3.62 +
    3.63 +lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
    3.64 +by (auto intro!: program_equalityI simp add: component_eq_subset)
    3.65 +
    3.66 +lemma component_Join1: "F <= (F Join G)"
    3.67 +by (unfold component_def, blast)
    3.68 +
    3.69 +lemma component_Join2: "G <= (F Join G)"
    3.70 +apply (unfold component_def)
    3.71 +apply (simp (no_asm) add: Join_commute)
    3.72 +apply blast
    3.73 +done
    3.74 +
    3.75 +lemma Join_absorb1: "F<=G ==> F Join G = G"
    3.76 +by (auto simp add: component_def Join_left_absorb)
    3.77 +
    3.78 +lemma Join_absorb2: "G<=F ==> F Join G = F"
    3.79 +by (auto simp add: Join_ac component_def)
    3.80 +
    3.81 +lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
    3.82 +apply (simp (no_asm) add: component_eq_subset)
    3.83 +apply blast
    3.84 +done
    3.85 +
    3.86 +lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
    3.87 +apply (unfold component_def)
    3.88 +apply (blast intro: JN_absorb)
    3.89 +done
    3.90 +
    3.91 +lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
    3.92 +apply (unfold component_def)
    3.93 +apply (blast intro: Join_assoc [symmetric])
    3.94 +done
    3.95 +
    3.96 +lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
    3.97 +apply (simp (no_asm_use) add: component_eq_subset)
    3.98 +apply (blast intro!: program_equalityI)
    3.99 +done
   3.100 +
   3.101 +lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
   3.102 +apply (simp (no_asm) add: component_eq_subset)
   3.103 +apply blast
   3.104 +done
   3.105 +
   3.106 +lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
   3.107 +by (auto simp add: constrains_def component_eq_subset)
   3.108 +
   3.109 +(*Used in Guar.thy to show that programs are partially ordered*)
   3.110 +lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq]
   3.111 +
   3.112 +
   3.113 +(*** preserves ***)
   3.114 +
   3.115 +lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
   3.116 +by (unfold preserves_def, blast)
   3.117 +
   3.118 +lemma preserves_imp_eq: 
   3.119 +     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'"
   3.120 +apply (unfold preserves_def stable_def constrains_def, force)
   3.121 +done
   3.122 +
   3.123 +lemma Join_preserves [iff]: 
   3.124 +     "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
   3.125 +apply (unfold preserves_def, auto)
   3.126 +done
   3.127 +
   3.128 +lemma JN_preserves [iff]:
   3.129 +     "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
   3.130 +apply (simp (no_asm) add: JN_stable preserves_def)
   3.131 +apply blast
   3.132 +done
   3.133 +
   3.134 +lemma SKIP_preserves [iff]: "SKIP : preserves v"
   3.135 +by (auto simp add: preserves_def)
   3.136 +
   3.137 +lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
   3.138 +by (simp add:  funPair_def)
   3.139 +
   3.140 +lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
   3.141 +by (auto simp add: preserves_def stable_def constrains_def, blast)
   3.142 +
   3.143 +(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
   3.144 +declare preserves_funPair [THEN eqset_imp_iff, iff]
   3.145 +
   3.146 +
   3.147 +lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)"
   3.148 +apply (simp (no_asm) add: funPair_def o_def)
   3.149 +done
   3.150 +
   3.151 +lemma fst_o_funPair [simp]: "fst o (funPair f g) = f"
   3.152 +apply (simp (no_asm) add: funPair_def o_def)
   3.153 +done
   3.154 +
   3.155 +lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
   3.156 +apply (simp (no_asm) add: funPair_def o_def)
   3.157 +done
   3.158 +
   3.159 +lemma subset_preserves_o: "preserves v <= preserves (w o v)"
   3.160 +by (force simp add: preserves_def stable_def constrains_def)
   3.161 +
   3.162 +lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
   3.163 +apply (auto simp add: preserves_def stable_def constrains_def)
   3.164 +apply (rename_tac s' s)
   3.165 +apply (subgoal_tac "v s = v s'")
   3.166 +apply (force+)
   3.167 +done
   3.168 +
   3.169 +lemma preserves_subset_increasing: "preserves v <= increasing v"
   3.170 +by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
   3.171 +
   3.172 +lemma preserves_id_subset_stable: "preserves id <= stable A"
   3.173 +by (force simp add: preserves_def stable_def constrains_def)
   3.174 +
   3.175 +
   3.176 +(** For use with def_UNION_ok_iff **)
   3.177 +
   3.178 +lemma safety_prop_preserves [iff]: "safety_prop (preserves v)"
   3.179 +by (auto intro: safety_prop_INTER1 simp add: preserves_def)
   3.180 +
   3.181 +
   3.182 +(** Some lemmas used only in Client.ML **)
   3.183 +
   3.184 +lemma stable_localTo_stable2:
   3.185 +     "[| F : stable {s. P (v s) (w s)};    
   3.186 +         G : preserves v;  G : preserves w |]                
   3.187 +      ==> F Join G : stable {s. P (v s) (w s)}"
   3.188 +apply (simp (no_asm_simp))
   3.189 +apply (subgoal_tac "G: preserves (funPair v w) ")
   3.190 + prefer 2 apply simp 
   3.191 +apply (drule_tac P1 = "split ?Q" in  preserves_subset_stable [THEN subsetD], auto)
   3.192 +done
   3.193 +
   3.194 +lemma Increasing_preserves_Stable:
   3.195 +     "[| F : stable {s. v s <= w s};  G : preserves v;        
   3.196 +         F Join G : Increasing w |]                
   3.197 +      ==> F Join G : Stable {s. v s <= w s}"
   3.198 +apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
   3.199 +apply (blast intro: constrains_weaken)
   3.200 +(*The G case remains*)
   3.201 +apply (auto simp add: preserves_def stable_def constrains_def)
   3.202 +apply (case_tac "act: Acts F", blast)
   3.203 +(*We have a G-action, so delete assumptions about F-actions*)
   3.204 +apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
   3.205 +apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
   3.206 +apply (subgoal_tac "v x = v xa")
   3.207 +prefer 2 apply blast
   3.208 +apply auto
   3.209 +apply (erule order_trans, blast)
   3.210 +done
   3.211 +
   3.212 +(** component_of **)
   3.213 +
   3.214 +(*  component_of is stronger than <= *)
   3.215 +lemma component_of_imp_component: "F component_of H ==> F <= H"
   3.216 +by (unfold component_def component_of_def, blast)
   3.217 +
   3.218 +
   3.219 +(* component_of satisfies many of the <='s properties *)
   3.220 +lemma component_of_refl [simp]: "F component_of F"
   3.221 +apply (unfold component_of_def)
   3.222 +apply (rule_tac x = SKIP in exI, auto)
   3.223 +done
   3.224 +
   3.225 +lemma component_of_SKIP [simp]: "SKIP component_of F"
   3.226 +by (unfold component_of_def, auto)
   3.227 +
   3.228 +lemma component_of_trans: 
   3.229 +     "[| F component_of G; G component_of H |] ==> F component_of H"
   3.230 +apply (unfold component_of_def)
   3.231 +apply (blast intro: Join_assoc [symmetric])
   3.232 +done
   3.233 +
   3.234 +lemmas strict_component_of_eq =
   3.235 +    strict_component_of_def [THEN meta_eq_to_obj_eq, standard]
   3.236 +
   3.237 +(** localize **)
   3.238 +lemma localize_Init_eq [simp]: "Init (localize v F) = Init F"
   3.239 +apply (unfold localize_def)
   3.240 +apply (simp (no_asm))
   3.241 +done
   3.242 +
   3.243 +lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
   3.244 +apply (unfold localize_def)
   3.245 +apply (simp (no_asm))
   3.246 +done
   3.247 +
   3.248 +lemma localize_AllowedActs_eq [simp]: 
   3.249 + "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
   3.250 +apply (unfold localize_def, auto)
   3.251 +done
   3.252 +
   3.253  end
     4.1 --- a/src/HOL/UNITY/Comp/Counter.thy	Wed Jan 29 16:29:38 2003 +0100
     4.2 +++ b/src/HOL/UNITY/Comp/Counter.thy	Wed Jan 29 16:34:51 2003 +0100
     4.3 @@ -11,7 +11,8 @@
     4.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     4.5  *)
     4.6  
     4.7 -Counter =  Comp +
     4.8 +Counter = UNITY_Main +
     4.9 +
    4.10  (* Variables are names *)
    4.11  datatype name = C | c nat
    4.12  types state = name=>int
     5.1 --- a/src/HOL/UNITY/Comp/Counterc.thy	Wed Jan 29 16:29:38 2003 +0100
     5.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy	Wed Jan 29 16:34:51 2003 +0100
     5.3 @@ -11,7 +11,8 @@
     5.4     Spriner LNCS 1586 (1999), pages 1215-1227.
     5.5  *)
     5.6  
     5.7 -Counterc =  Comp +
     5.8 +Counterc =  UNITY_Main +
     5.9 +
    5.10  types state
    5.11  arities state :: type
    5.12  
     6.1 --- a/src/HOL/UNITY/Guar.ML	Wed Jan 29 16:29:38 2003 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,520 +0,0 @@
     6.4 -(*  Title:      HOL/UNITY/Guar.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1999  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 -
    6.15 -Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))";
    6.16 -by (auto_tac (claset() addIs [ok_sym], 
    6.17 -              simpset() addsimps [OK_iff_ok]));
    6.18 -qed "OK_insert_iff";
    6.19 -
    6.20 -
    6.21 -
    6.22 -(*** existential properties ***)
    6.23 -Goalw [ex_prop_def]
    6.24 - "[| ex_prop X; finite GG |] ==> \
    6.25 -\    GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X";
    6.26 -by (etac finite_induct 1);
    6.27 -by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left]));
    6.28 -qed_spec_mp "ex1";
    6.29 -
    6.30 -
    6.31 -Goalw [ex_prop_def]
    6.32 -     "ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X";
    6.33 -by (Clarify_tac 1);
    6.34 -by (dres_inst_tac [("x", "{F,G}")] spec 1);
    6.35 -by (auto_tac (claset() addDs [ok_sym], 
    6.36 -              simpset() addsimps [OK_iff_ok]));
    6.37 -qed "ex2";
    6.38 -
    6.39 -
    6.40 -(*Chandy & Sanders take this as a definition*)
    6.41 -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)";
    6.42 -by (blast_tac (claset() addIs [ex1,ex2]) 1);
    6.43 -qed "ex_prop_finite";
    6.44 -
    6.45 -
    6.46 -(*Their "equivalent definition" given at the end of section 3*)
    6.47 -Goal
    6.48 - "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))";
    6.49 -by Auto_tac;
    6.50 -by (rewrite_goals_tac 
    6.51 -          [ex_prop_def, component_of_def]);
    6.52 -by Safe_tac;
    6.53 -by (stac Join_commute 3);
    6.54 -by (dtac  ok_sym 3);
    6.55 -by (REPEAT(Blast_tac 1));
    6.56 -qed "ex_prop_equiv";
    6.57 -
    6.58 -
    6.59 -(*** universal properties ***)
    6.60 -Goalw [uv_prop_def]
    6.61 -     "[| uv_prop X; finite GG |] ==>  \
    6.62 -\  GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X";
    6.63 -by (etac finite_induct 1);
    6.64 -by (auto_tac (claset(), simpset() addsimps 
    6.65 -           [Int_insert_left, OK_insert_iff]));
    6.66 -qed_spec_mp "uv1";
    6.67 -
    6.68 -Goalw [uv_prop_def]
    6.69 -     "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X  ==> uv_prop X";
    6.70 -by (rtac conjI 1);
    6.71 -by (Clarify_tac 2);
    6.72 -by (dres_inst_tac [("x", "{F,G}")] spec 2);
    6.73 -by (dres_inst_tac [("x", "{}")] spec 1);
    6.74 -by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok]));
    6.75 -qed "uv2";
    6.76 -
    6.77 -(*Chandy & Sanders take this as a definition*)
    6.78 -Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)";
    6.79 -by (blast_tac (claset() addIs [uv1,uv2]) 1);
    6.80 -qed "uv_prop_finite";
    6.81 -
    6.82 -(*** guarantees ***)
    6.83 -
    6.84 -val prems = Goal
    6.85 -     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \
    6.86 -\     ==> F : X guarantees Y";
    6.87 -by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
    6.88 -by (blast_tac (claset() addIs prems) 1);
    6.89 -qed "guaranteesI";
    6.90 -
    6.91 -Goalw [guar_def, component_def]
    6.92 -     "[| F : X guarantees Y;  F ok G;  F Join G : X |] \
    6.93 -\     ==> F Join G : Y";
    6.94 -by (Blast_tac 1);
    6.95 -qed "guaranteesD";
    6.96 -
    6.97 -(*This version of guaranteesD matches more easily in the conclusion
    6.98 -  The major premise can no longer be  F<=H since we need to reason about G*)
    6.99 -Goalw [guar_def]
   6.100 -     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |] \
   6.101 -\     ==> H : Y";
   6.102 -by (Blast_tac 1);
   6.103 -qed "component_guaranteesD";
   6.104 -
   6.105 -Goalw [guar_def]
   6.106 -     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
   6.107 -by (Blast_tac 1);
   6.108 -qed "guarantees_weaken";
   6.109 -
   6.110 -Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
   6.111 -by (Blast_tac 1);
   6.112 -qed "subset_imp_guarantees_UNIV";
   6.113 -
   6.114 -(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   6.115 -Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
   6.116 -by (Blast_tac 1);
   6.117 -qed "subset_imp_guarantees";
   6.118 -
   6.119 -(*Remark at end of section 4.1 *)
   6.120 -
   6.121 -Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)";
   6.122 -by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   6.123 -by Safe_tac;
   6.124 -by (dres_inst_tac [("x", "x")] spec 1);
   6.125 -by (dres_inst_tac [("x", "x")] spec 2);
   6.126 -by (dtac sym 2);
   6.127 -by (ALLGOALS(etac iffE));
   6.128 -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   6.129 -by (REPEAT(Blast_tac 1));
   6.130 -qed "ex_prop_imp";
   6.131 -
   6.132 -Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)";
   6.133 -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   6.134 -by Safe_tac;
   6.135 -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def])));
   6.136 -by (dtac sym 2);
   6.137 -by (ALLGOALS(etac equalityE));
   6.138 -by (REPEAT(Blast_tac 1));
   6.139 -qed "guarantees_imp";
   6.140 -
   6.141 -Goal "(ex_prop Y) = (Y = UNIV guarantees Y)";
   6.142 -by (rtac iffI 1);
   6.143 -by (rtac ex_prop_imp 1);
   6.144 -by (rtac guarantees_imp 2);
   6.145 -by (ALLGOALS(Asm_simp_tac));
   6.146 -qed "ex_prop_equiv2";
   6.147 -
   6.148 -
   6.149 -(** Distributive laws.  Re-orient to perform miniscoping **)
   6.150 -
   6.151 -Goalw [guar_def]
   6.152 -     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
   6.153 -by (Blast_tac 1);
   6.154 -qed "guarantees_UN_left";
   6.155 -
   6.156 -Goalw [guar_def]
   6.157 -     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
   6.158 -by (Blast_tac 1);
   6.159 -qed "guarantees_Un_left";
   6.160 -
   6.161 -Goalw [guar_def]
   6.162 -     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
   6.163 -by (Blast_tac 1);
   6.164 -qed "guarantees_INT_right";
   6.165 -
   6.166 -Goalw [guar_def]
   6.167 -     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
   6.168 -by (Blast_tac 1);
   6.169 -qed "guarantees_Int_right";
   6.170 -
   6.171 -Goal "[| F : Z guarantees X;  F : Z guarantees Y |] \
   6.172 -\    ==> F : Z guarantees (X Int Y)";
   6.173 -by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
   6.174 -qed "guarantees_Int_right_I";
   6.175 -
   6.176 -Goal "(F : X guarantees (INTER I Y)) = \
   6.177 -\     (ALL i:I. F : X guarantees (Y i))";
   6.178 -by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
   6.179 -qed "guarantees_INT_right_iff";
   6.180 -
   6.181 -Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
   6.182 -by (Blast_tac 1);
   6.183 -qed "shunting";
   6.184 -
   6.185 -Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
   6.186 -by (Blast_tac 1);
   6.187 -qed "contrapositive";
   6.188 -
   6.189 -(** The following two can be expressed using intersection and subset, which
   6.190 -    is more faithful to the text but looks cryptic.
   6.191 -**)
   6.192 -
   6.193 -Goalw [guar_def]
   6.194 -    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
   6.195 -\    ==> F : (V Int Y) guarantees Z";
   6.196 -by (Blast_tac 1);
   6.197 -qed "combining1";
   6.198 -
   6.199 -Goalw [guar_def]
   6.200 -    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
   6.201 -\    ==> F : V guarantees (X Un Z)";
   6.202 -by (Blast_tac 1);
   6.203 -qed "combining2";
   6.204 -
   6.205 -(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   6.206 -    does not suit Isabelle... **)
   6.207 -
   6.208 -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   6.209 -Goalw [guar_def]
   6.210 -     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
   6.211 -by (Blast_tac 1);
   6.212 -qed "all_guarantees";
   6.213 -
   6.214 -(*Premises should be [| F: X guarantees Y i; i: I |] *)
   6.215 -Goalw [guar_def]
   6.216 -     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
   6.217 -by (Blast_tac 1);
   6.218 -qed "ex_guarantees";
   6.219 -
   6.220 -
   6.221 -(*** Additional guarantees laws, by lcp ***)
   6.222 -
   6.223 -Goalw [guar_def]
   6.224 -    "[| F: U guarantees V;  G: X guarantees Y; F ok G |] \
   6.225 -\    ==> F Join G: (U Int X) guarantees (V Int Y)"; 
   6.226 -by (Simp_tac 1);
   6.227 -by Safe_tac;
   6.228 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.229 -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   6.230 -by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
   6.231 -by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   6.232 -qed "guarantees_Join_Int";
   6.233 -
   6.234 -Goalw [guar_def]
   6.235 -    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]  \
   6.236 -\    ==> F Join G: (U Un X) guarantees (V Un Y)";
   6.237 -by (Simp_tac 1);
   6.238 -by Safe_tac;
   6.239 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.240 -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
   6.241 -by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1);
   6.242 -by (asm_simp_tac (simpset() addsimps Join_ac) 1);
   6.243 -qed "guarantees_Join_Un";
   6.244 -
   6.245 -Goalw [guar_def]
   6.246 -     "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
   6.247 -\     ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
   6.248 -by Auto_tac;
   6.249 -by (ball_tac 1);
   6.250 -by (rename_tac "i" 1);
   6.251 -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
   6.252 -by (auto_tac
   6.253 -    (claset() addIs [OK_imp_ok],
   6.254 -     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
   6.255 -qed "guarantees_JN_INT";
   6.256 -
   6.257 -Goalw [guar_def]
   6.258 -    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
   6.259 -\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
   6.260 -by Auto_tac;
   6.261 -by (ball_tac 1);
   6.262 -by (rename_tac "i" 1);
   6.263 -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
   6.264 -by (auto_tac
   6.265 -    (claset() addIs [OK_imp_ok],
   6.266 -     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
   6.267 -qed "guarantees_JN_UN";
   6.268 -
   6.269 -
   6.270 -(*** guarantees laws for breaking down the program, by lcp ***)
   6.271 -
   6.272 -Goalw [guar_def]
   6.273 -     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
   6.274 -by (Simp_tac 1);
   6.275 -by Safe_tac;
   6.276 -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.277 -qed "guarantees_Join_I1";
   6.278 -
   6.279 -Goal "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
   6.280 -by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, 
   6.281 -                                           inst "G" "G" ok_commute]) 1);
   6.282 -by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
   6.283 -qed "guarantees_Join_I2";
   6.284 -
   6.285 -Goalw [guar_def]
   6.286 -     "[| i : I;  F i: X guarantees Y;  OK I F |] \
   6.287 -\     ==> (JN i:I. (F i)) : X guarantees Y";
   6.288 -by (Clarify_tac 1);
   6.289 -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
   6.290 -by (auto_tac (claset() addIs [OK_imp_ok],
   6.291 -	      simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym]));
   6.292 -qed "guarantees_JN_I";
   6.293 -
   6.294 -
   6.295 -(*** well-definedness ***)
   6.296 -
   6.297 -Goalw [welldef_def] "F Join G: welldef ==> F: welldef";
   6.298 -by Auto_tac;
   6.299 -qed "Join_welldef_D1";
   6.300 -
   6.301 -Goalw [welldef_def] "F Join G: welldef ==> G: welldef";
   6.302 -by Auto_tac;
   6.303 -qed "Join_welldef_D2";
   6.304 -
   6.305 -(*** refinement ***)
   6.306 -
   6.307 -Goalw [refines_def] "F refines F wrt X";
   6.308 -by (Blast_tac 1);
   6.309 -qed "refines_refl";
   6.310 -
   6.311 -(* Goalw [refines_def]
   6.312 -     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"; 
   6.313 -by Auto_tac;
   6.314 -qed "refines_trans"; *)
   6.315 -
   6.316 -
   6.317 -
   6.318 -Goalw [strict_ex_prop_def]
   6.319 -     "strict_ex_prop X \
   6.320 -\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \
   6.321 -\             = (F:X --> G:X)";
   6.322 -by Auto_tac;
   6.323 -qed "strict_ex_refine_lemma";
   6.324 -
   6.325 -Goalw [strict_ex_prop_def]
   6.326 -     "strict_ex_prop X \
   6.327 -\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
   6.328 -\         (F: welldef Int X --> G:X)";
   6.329 -by Safe_tac;
   6.330 -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   6.331 -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset()));
   6.332 -qed "strict_ex_refine_lemma_v";
   6.333 -
   6.334 -Goal "[| strict_ex_prop X;  \
   6.335 -\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
   6.336 -\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   6.337 -by (res_inst_tac [("x","SKIP")] allE 1
   6.338 -    THEN assume_tac 1);
   6.339 -by (asm_full_simp_tac
   6.340 -    (simpset() addsimps [refines_def, iso_refines_def,
   6.341 -			 strict_ex_refine_lemma_v]) 1);
   6.342 -qed "ex_refinement_thm";
   6.343 -
   6.344 -
   6.345 -Goalw [strict_uv_prop_def]
   6.346 -     "strict_uv_prop X \
   6.347 -\     ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)";
   6.348 -by (Blast_tac 1);
   6.349 -qed "strict_uv_refine_lemma";
   6.350 -
   6.351 -Goalw [strict_uv_prop_def]
   6.352 -     "strict_uv_prop X \
   6.353 -\     ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \
   6.354 -\         (F: welldef Int X --> G:X)";
   6.355 -by Safe_tac;
   6.356 -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1);
   6.357 -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2],
   6.358 -	      simpset()));
   6.359 -qed "strict_uv_refine_lemma_v";
   6.360 -
   6.361 -Goal "[| strict_uv_prop X;  \
   6.362 -\        ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \
   6.363 -\     ==> (G refines F wrt X) = (G iso_refines F wrt X)";
   6.364 -by (res_inst_tac [("x","SKIP")] allE 1
   6.365 -    THEN assume_tac 1);
   6.366 -by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def,
   6.367 -					   strict_uv_refine_lemma_v]) 1);
   6.368 -qed "uv_refinement_thm";
   6.369 -
   6.370 -(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
   6.371 -Goalw [guar_def, component_of_def]
   6.372 -"(F:X guarantees Y) = (ALL H. H:X \\<longrightarrow> (F component_of H \\<longrightarrow> H:Y))";
   6.373 -by Auto_tac;
   6.374 -qed "guarantees_equiv";
   6.375 -
   6.376 -Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)";
   6.377 -by Auto_tac;
   6.378 -qed "wg_weakest";
   6.379 -
   6.380 -Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)";
   6.381 -by (Blast_tac 1);
   6.382 -qed "wg_guarantees";
   6.383 -
   6.384 -Goalw [wg_def]
   6.385 -  "(H: wg F X) = (F component_of H --> H:X)";
   6.386 -by (simp_tac (simpset() addsimps [guarantees_equiv]) 1);
   6.387 -by (rtac iffI 1);
   6.388 -by (res_inst_tac [("x", "{H}")] exI 2);
   6.389 -by (REPEAT(Blast_tac 1));
   6.390 -qed "wg_equiv";
   6.391 -
   6.392 -
   6.393 -Goal
   6.394 -"F component_of H ==> (H:wg F X) = (H:X)";
   6.395 -by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1);
   6.396 -qed "component_of_wg";
   6.397 -
   6.398 -
   6.399 -Goal
   6.400 -"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \
   6.401 -\  --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))";
   6.402 -by (Clarify_tac 1);
   6.403 -by (subgoal_tac "F component_of (JN F:FF. F)" 1);
   6.404 -by (dres_inst_tac [("X", "X")] component_of_wg 1);
   6.405 -by (Asm_full_simp_tac 1);
   6.406 -by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1);
   6.407 -by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1);
   6.408 -by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], 
   6.409 -              simpset() addsimps [OK_iff_ok]));
   6.410 -qed "wg_finite";
   6.411 -
   6.412 -Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)";
   6.413 -by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1);
   6.414 -by (Blast_tac 1);
   6.415 -qed "wg_ex_prop";
   6.416 -
   6.417 -(** From Charpentier and Chandy "Theorems About Composition" **)
   6.418 -(* Proposition 2 *)
   6.419 -Goalw [wx_def] "(wx X)<=X";
   6.420 -by Auto_tac;
   6.421 -qed "wx_subset";
   6.422 -
   6.423 -Goalw [wx_def]
   6.424 -"ex_prop (wx X)";
   6.425 -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
   6.426 -by Safe_tac;
   6.427 -by (Blast_tac 1);
   6.428 -by Auto_tac;
   6.429 -qed "wx_ex_prop";
   6.430 -
   6.431 -Goalw [wx_def]
   6.432 -"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X";
   6.433 -by Auto_tac;
   6.434 -qed "wx_weakest";
   6.435 -
   6.436 -
   6.437 -(* Proposition 6 *)
   6.438 -Goalw [ex_prop_def]
   6.439 - "ex_prop({F. ALL G. F ok G --> F Join G:X})";
   6.440 -by Safe_tac;
   6.441 -by (dres_inst_tac [("x", "G Join Ga")] spec 1);
   6.442 -by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1);
   6.443 -by (dres_inst_tac [("x", "F Join Ga")] spec 1);
   6.444 -by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1);
   6.445 -by Safe_tac;
   6.446 -by (asm_simp_tac (simpset() addsimps [ok_commute]) 1);
   6.447 -by (subgoal_tac "F Join G = G Join F" 1);
   6.448 -by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1);
   6.449 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
   6.450 -qed "wx'_ex_prop";
   6.451 -
   6.452 -(* Equivalence with the other definition of wx *)
   6.453 -
   6.454 -Goalw [wx_def]
   6.455 - "wx X = {F. ALL G. F ok G --> (F Join G):X}";
   6.456 -by Safe_tac;
   6.457 -by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1);
   6.458 -by (dres_inst_tac [("x", "x")] spec 1);
   6.459 -by (dres_inst_tac [("x", "G")] spec 1);
   6.460 -by (forw_inst_tac [("c", "x Join G")] subsetD 1);
   6.461 -by Safe_tac;
   6.462 -by (Simp_tac 1);
   6.463 -by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1);
   6.464 -by Safe_tac;
   6.465 -by (rtac wx'_ex_prop 2);
   6.466 -by (rotate_tac 1 1);
   6.467 -by (dres_inst_tac [("x", "SKIP")] spec 1);
   6.468 -by Auto_tac;
   6.469 -qed "wx_equiv";
   6.470 -
   6.471 -
   6.472 -(* Propositions 7 to 11 are about this second definition of wx. And
   6.473 -   they are the same as the ones proved for the first definition of wx by equivalence *)
   6.474 -   
   6.475 -(* Proposition 12 *)
   6.476 -(* Main result of the paper *)
   6.477 -Goalw [guar_def] 
   6.478 -   "(X guarantees Y) = wx(-X Un Y)";
   6.479 -by (simp_tac (simpset() addsimps [wx_equiv]) 1);
   6.480 -qed "guarantees_wx_eq";
   6.481 -
   6.482 -(* {* Corollary, but this result has already been proved elsewhere *}
   6.483 - "ex_prop(X guarantees Y)";
   6.484 -  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
   6.485 -  qed "guarantees_ex_prop";
   6.486 -*)
   6.487 -
   6.488 -(* Rules given in section 7 of Chandy and Sander's
   6.489 -    Reasoning About Program composition paper *)
   6.490 -
   6.491 -Goal "Init F <= A ==> F:(stable A) guarantees (Always A)";
   6.492 -by (rtac guaranteesI 1);
   6.493 -by (simp_tac (simpset() addsimps [Join_commute]) 1);
   6.494 -by (rtac stable_Join_Always1 1);
   6.495 -by (ALLGOALS(asm_full_simp_tac (simpset() 
   6.496 -     addsimps [invariant_def, Join_stable])));
   6.497 -qed "stable_guarantees_Always";
   6.498 -
   6.499 -(* To be moved to WFair.ML *)
   6.500 -Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B";
   6.501 -by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1);
   6.502 -by (dres_inst_tac [("B", "A-B")] transient_strengthen 2);
   6.503 -by (rtac (ensuresI RS leadsTo_Basis) 3);
   6.504 -by (ALLGOALS(Blast_tac));
   6.505 -qed "leadsTo_Basis'";
   6.506 -
   6.507 -
   6.508 -
   6.509 -Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))";
   6.510 -by (rtac guaranteesI 1);
   6.511 -by (rtac leadsTo_Basis' 1);
   6.512 -by (dtac constrains_weaken_R 1);
   6.513 -by (assume_tac 2);
   6.514 -by (Blast_tac 1);
   6.515 -by (blast_tac (claset() addIs [Join_transient_I1]) 1);
   6.516 -qed "constrains_guarantees_leadsTo";
   6.517 -
   6.518 -
   6.519 -
   6.520 -
   6.521 -
   6.522 -
   6.523 -
     7.1 --- a/src/HOL/UNITY/Guar.thy	Wed Jan 29 16:29:38 2003 +0100
     7.2 +++ b/src/HOL/UNITY/Guar.thy	Wed Jan 29 16:34:51 2003 +0100
     7.3 @@ -18,36 +18,39 @@
     7.4  
     7.5  *)
     7.6  
     7.7 -Guar = Comp +
     7.8 +theory Guar = Comp:
     7.9  
    7.10  instance program :: (type) order
    7.11 -                    (component_refl, component_trans, component_antisym,
    7.12 -                     program_less_le)
    7.13 +  by (intro_classes,
    7.14 +      (assumption | rule component_refl component_trans component_antisym
    7.15 +                     program_less_le)+)
    7.16 +
    7.17  
    7.18  constdefs
    7.19  
    7.20    (*Existential and Universal properties.  I formalize the two-program
    7.21      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
    7.22  
    7.23 -  ex_prop  :: 'a program set => bool
    7.24 -   "ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X"
    7.25 +  ex_prop  :: "'a program set => bool"
    7.26 +   "ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X"
    7.27  
    7.28 -  strict_ex_prop  :: 'a program set => bool
    7.29 -   "strict_ex_prop X == ALL F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
    7.30 +  strict_ex_prop  :: "'a program set => bool"
    7.31 +   "strict_ex_prop X == \<forall>F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
    7.32  
    7.33 -  uv_prop  :: 'a program set => bool
    7.34 -   "uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)"
    7.35 +  uv_prop  :: "'a program set => bool"
    7.36 +   "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
    7.37  
    7.38 -  strict_uv_prop  :: 'a program set => bool
    7.39 -   "strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))"
    7.40 +  strict_uv_prop  :: "'a program set => bool"
    7.41 +   "strict_uv_prop X == 
    7.42 +      SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
    7.43  
    7.44 -  guar :: ['a program set, 'a program set] => 'a program set
    7.45 +  guar :: "['a program set, 'a program set] => 'a program set"
    7.46            (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
    7.47 -   "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
    7.48 +   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}"
    7.49    
    7.50  
    7.51    (* Weakest guarantees *)
    7.52 -   wg :: ['a program, 'a program set] =>  'a program set
    7.53 +   wg :: "['a program, 'a program set] =>  'a program set"
    7.54    "wg F Y == Union({X. F:X guarantees Y})"
    7.55  
    7.56     (* Weakest existential property stronger than X *)
    7.57 @@ -55,17 +58,484 @@
    7.58     "wx X == Union({Y. Y<=X & ex_prop Y})"
    7.59    
    7.60    (*Ill-defined programs can arise through "Join"*)
    7.61 -  welldef :: 'a program set  
    7.62 +  welldef :: "'a program set"
    7.63    "welldef == {F. Init F ~= {}}"
    7.64    
    7.65 -  refines :: ['a program, 'a program, 'a program set] => bool
    7.66 +  refines :: "['a program, 'a program, 'a program set] => bool"
    7.67  			("(3_ refines _ wrt _)" [10,10,10] 10)
    7.68    "G refines F wrt X ==
    7.69 -   ALL H. (F ok H  & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)"
    7.70 +     \<forall>H. (F ok H  & G ok H & F Join H : welldef Int X) --> 
    7.71 +         (G Join H : welldef Int X)"
    7.72  
    7.73 -  iso_refines :: ['a program, 'a program, 'a program set] => bool
    7.74 +  iso_refines :: "['a program, 'a program, 'a program set] => bool"
    7.75                                ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    7.76    "G iso_refines F wrt X ==
    7.77     F : welldef Int X --> G : welldef Int X"
    7.78  
    7.79 +
    7.80 +lemma OK_insert_iff:
    7.81 +     "(OK (insert i I) F) = 
    7.82 +      (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
    7.83 +by (auto intro: ok_sym simp add: OK_iff_ok)
    7.84 +
    7.85 +
    7.86 +(*** existential properties ***)
    7.87 +lemma ex1 [rule_format (no_asm)]: 
    7.88 + "[| ex_prop X; finite GG |] ==>  
    7.89 +     GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
    7.90 +apply (unfold ex_prop_def)
    7.91 +apply (erule finite_induct)
    7.92 +apply (auto simp add: OK_insert_iff Int_insert_left)
    7.93 +done
    7.94 +
    7.95 +
    7.96 +lemma ex2: 
    7.97 +     "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X 
    7.98 +      ==> ex_prop X"
    7.99 +apply (unfold ex_prop_def, clarify)
   7.100 +apply (drule_tac x = "{F,G}" in spec)
   7.101 +apply (auto dest: ok_sym simp add: OK_iff_ok)
   7.102 +done
   7.103 +
   7.104 +
   7.105 +(*Chandy & Sanders take this as a definition*)
   7.106 +lemma ex_prop_finite:
   7.107 +     "ex_prop X = 
   7.108 +      (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
   7.109 +by (blast intro: ex1 ex2)
   7.110 +
   7.111 +
   7.112 +(*Their "equivalent definition" given at the end of section 3*)
   7.113 +lemma ex_prop_equiv: 
   7.114 +     "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
   7.115 +apply auto
   7.116 +apply (unfold ex_prop_def component_of_def, safe)
   7.117 +apply blast 
   7.118 +apply blast 
   7.119 +apply (subst Join_commute) 
   7.120 +apply (drule ok_sym, blast) 
   7.121 +done
   7.122 +
   7.123 +
   7.124 +(*** universal properties ***)
   7.125 +lemma uv1 [rule_format]: 
   7.126 +     "[| uv_prop X; finite GG |] 
   7.127 +      ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
   7.128 +apply (unfold uv_prop_def)
   7.129 +apply (erule finite_induct)
   7.130 +apply (auto simp add: Int_insert_left OK_insert_iff)
   7.131 +done
   7.132 +
   7.133 +lemma uv2: 
   7.134 +     "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X  
   7.135 +      ==> uv_prop X"
   7.136 +apply (unfold uv_prop_def)
   7.137 +apply (rule conjI)
   7.138 + apply (drule_tac x = "{}" in spec)
   7.139 + prefer 2
   7.140 + apply clarify 
   7.141 + apply (drule_tac x = "{F,G}" in spec)
   7.142 +apply (auto dest: ok_sym simp add: OK_iff_ok)
   7.143 +done
   7.144 +
   7.145 +(*Chandy & Sanders take this as a definition*)
   7.146 +lemma uv_prop_finite:
   7.147 +     "uv_prop X = 
   7.148 +      (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
   7.149 +by (blast intro: uv1 uv2)
   7.150 +
   7.151 +(*** guarantees ***)
   7.152 +
   7.153 +lemma guaranteesI:
   7.154 +     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)  
   7.155 +      ==> F : X guarantees Y"
   7.156 +by (simp add: guar_def component_def)
   7.157 +
   7.158 +lemma guaranteesD: 
   7.159 +     "[| F : X guarantees Y;  F ok G;  F Join G : X |]  
   7.160 +      ==> F Join G : Y"
   7.161 +by (unfold guar_def component_def, blast)
   7.162 +
   7.163 +(*This version of guaranteesD matches more easily in the conclusion
   7.164 +  The major premise can no longer be  F<=H since we need to reason about G*)
   7.165 +lemma component_guaranteesD: 
   7.166 +     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |]  
   7.167 +      ==> H : Y"
   7.168 +by (unfold guar_def, blast)
   7.169 +
   7.170 +lemma guarantees_weaken: 
   7.171 +     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
   7.172 +by (unfold guar_def, blast)
   7.173 +
   7.174 +lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
   7.175 +by (unfold guar_def, blast)
   7.176 +
   7.177 +(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   7.178 +lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
   7.179 +by (unfold guar_def, blast)
   7.180 +
   7.181 +(*Remark at end of section 4.1 *)
   7.182 +
   7.183 +lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
   7.184 +apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
   7.185 +apply safe
   7.186 + apply (drule_tac x = x in spec)
   7.187 + apply (drule_tac [2] x = x in spec)
   7.188 + apply (drule_tac [2] sym)
   7.189 +apply (auto simp add: component_of_def)
   7.190 +done
   7.191 +
   7.192 +lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
   7.193 +apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
   7.194 +apply safe
   7.195 +apply (auto simp add: component_of_def dest: sym)
   7.196 +done
   7.197 +
   7.198 +lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
   7.199 +apply (rule iffI)
   7.200 +apply (rule ex_prop_imp)
   7.201 +apply (auto simp add: guarantees_imp) 
   7.202 +done
   7.203 +
   7.204 +
   7.205 +(** Distributive laws.  Re-orient to perform miniscoping **)
   7.206 +
   7.207 +lemma guarantees_UN_left: 
   7.208 +     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
   7.209 +by (unfold guar_def, blast)
   7.210 +
   7.211 +lemma guarantees_Un_left: 
   7.212 +     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
   7.213 +by (unfold guar_def, blast)
   7.214 +
   7.215 +lemma guarantees_INT_right: 
   7.216 +     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
   7.217 +by (unfold guar_def, blast)
   7.218 +
   7.219 +lemma guarantees_Int_right: 
   7.220 +     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
   7.221 +by (unfold guar_def, blast)
   7.222 +
   7.223 +lemma guarantees_Int_right_I:
   7.224 +     "[| F : Z guarantees X;  F : Z guarantees Y |]  
   7.225 +     ==> F : Z guarantees (X Int Y)"
   7.226 +by (simp add: guarantees_Int_right)
   7.227 +
   7.228 +lemma guarantees_INT_right_iff:
   7.229 +     "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
   7.230 +by (simp add: guarantees_INT_right)
   7.231 +
   7.232 +lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
   7.233 +by (unfold guar_def, blast)
   7.234 +
   7.235 +lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
   7.236 +by (unfold guar_def, blast)
   7.237 +
   7.238 +(** The following two can be expressed using intersection and subset, which
   7.239 +    is more faithful to the text but looks cryptic.
   7.240 +**)
   7.241 +
   7.242 +lemma combining1: 
   7.243 +    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |] 
   7.244 +     ==> F : (V Int Y) guarantees Z"
   7.245 +
   7.246 +by (unfold guar_def, blast)
   7.247 +
   7.248 +lemma combining2: 
   7.249 +    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |] 
   7.250 +     ==> F : V guarantees (X Un Z)"
   7.251 +by (unfold guar_def, blast)
   7.252 +
   7.253 +(** The following two follow Chandy-Sanders, but the use of object-quantifiers
   7.254 +    does not suit Isabelle... **)
   7.255 +
   7.256 +(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
   7.257 +lemma all_guarantees: 
   7.258 +     "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
   7.259 +by (unfold guar_def, blast)
   7.260 +
   7.261 +(*Premises should be [| F: X guarantees Y i; i: I |] *)
   7.262 +lemma ex_guarantees: 
   7.263 +     "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
   7.264 +by (unfold guar_def, blast)
   7.265 +
   7.266 +
   7.267 +(*** Additional guarantees laws, by lcp ***)
   7.268 +
   7.269 +lemma guarantees_Join_Int: 
   7.270 +    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]  
   7.271 +     ==> F Join G: (U Int X) guarantees (V Int Y)"
   7.272 +apply (unfold guar_def)
   7.273 +apply (simp (no_asm))
   7.274 +apply safe
   7.275 +apply (simp add: Join_assoc)
   7.276 +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
   7.277 +apply (simp add: ok_commute)
   7.278 +apply (simp (no_asm_simp) add: Join_ac)
   7.279 +done
   7.280 +
   7.281 +lemma guarantees_Join_Un: 
   7.282 +    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]   
   7.283 +     ==> F Join G: (U Un X) guarantees (V Un Y)"
   7.284 +apply (unfold guar_def)
   7.285 +apply (simp (no_asm))
   7.286 +apply safe
   7.287 +apply (simp add: Join_assoc)
   7.288 +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
   7.289 +apply (simp add: ok_commute)
   7.290 +apply (simp (no_asm_simp) add: Join_ac)
   7.291 +done
   7.292 +
   7.293 +lemma guarantees_JN_INT: 
   7.294 +     "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]  
   7.295 +      ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
   7.296 +apply (unfold guar_def, auto)
   7.297 +apply (drule bspec, assumption)
   7.298 +apply (rename_tac "i")
   7.299 +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
   7.300 +apply (auto intro: OK_imp_ok
   7.301 +            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   7.302 +done
   7.303 +
   7.304 +lemma guarantees_JN_UN: 
   7.305 +    "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]  
   7.306 +     ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
   7.307 +apply (unfold guar_def, auto)
   7.308 +apply (drule bspec, assumption)
   7.309 +apply (rename_tac "i")
   7.310 +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
   7.311 +apply (auto intro: OK_imp_ok
   7.312 +            simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   7.313 +done
   7.314 +
   7.315 +
   7.316 +(*** guarantees laws for breaking down the program, by lcp ***)
   7.317 +
   7.318 +lemma guarantees_Join_I1: 
   7.319 +     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
   7.320 +apply (unfold guar_def)
   7.321 +apply (simp (no_asm))
   7.322 +apply safe
   7.323 +apply (simp add: Join_assoc)
   7.324 +done
   7.325 +
   7.326 +lemma guarantees_Join_I2:
   7.327 +     "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
   7.328 +apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
   7.329 +apply (blast intro: guarantees_Join_I1)
   7.330 +done
   7.331 +
   7.332 +lemma guarantees_JN_I: 
   7.333 +     "[| i : I;  F i: X guarantees Y;  OK I F |]  
   7.334 +      ==> (JN i:I. (F i)) : X guarantees Y"
   7.335 +apply (unfold guar_def, clarify)
   7.336 +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
   7.337 +apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
   7.338 +done
   7.339 +
   7.340 +
   7.341 +(*** well-definedness ***)
   7.342 +
   7.343 +lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
   7.344 +by (unfold welldef_def, auto)
   7.345 +
   7.346 +lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
   7.347 +by (unfold welldef_def, auto)
   7.348 +
   7.349 +(*** refinement ***)
   7.350 +
   7.351 +lemma refines_refl: "F refines F wrt X"
   7.352 +by (unfold refines_def, blast)
   7.353 +
   7.354 +
   7.355 +(* Goalw [refines_def]
   7.356 +     "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
   7.357 +by Auto_tac
   7.358 +qed "refines_trans"; *)
   7.359 +
   7.360 +
   7.361 +
   7.362 +lemma strict_ex_refine_lemma: 
   7.363 +     "strict_ex_prop X  
   7.364 +      ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)  
   7.365 +              = (F:X --> G:X)"
   7.366 +by (unfold strict_ex_prop_def, auto)
   7.367 +
   7.368 +lemma strict_ex_refine_lemma_v: 
   7.369 +     "strict_ex_prop X  
   7.370 +      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =  
   7.371 +          (F: welldef Int X --> G:X)"
   7.372 +apply (unfold strict_ex_prop_def, safe)
   7.373 +apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   7.374 +apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   7.375 +done
   7.376 +
   7.377 +lemma ex_refinement_thm:
   7.378 +     "[| strict_ex_prop X;   
   7.379 +         \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]  
   7.380 +      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   7.381 +apply (rule_tac x = SKIP in allE, assumption)
   7.382 +apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
   7.383 +done
   7.384 +
   7.385 +
   7.386 +lemma strict_uv_refine_lemma: 
   7.387 +     "strict_uv_prop X ==> 
   7.388 +      (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"
   7.389 +by (unfold strict_uv_prop_def, blast)
   7.390 +
   7.391 +lemma strict_uv_refine_lemma_v: 
   7.392 +     "strict_uv_prop X  
   7.393 +      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =  
   7.394 +          (F: welldef Int X --> G:X)"
   7.395 +apply (unfold strict_uv_prop_def, safe)
   7.396 +apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   7.397 +apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   7.398 +done
   7.399 +
   7.400 +lemma uv_refinement_thm:
   7.401 +     "[| strict_uv_prop X;   
   7.402 +         \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> 
   7.403 +             G Join H : welldef |]  
   7.404 +      ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   7.405 +apply (rule_tac x = SKIP in allE, assumption)
   7.406 +apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
   7.407 +done
   7.408 +
   7.409 +(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
   7.410 +lemma guarantees_equiv: 
   7.411 +    "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
   7.412 +by (unfold guar_def component_of_def, auto)
   7.413 +
   7.414 +lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
   7.415 +by (unfold wg_def, auto)
   7.416 +
   7.417 +lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
   7.418 +by (unfold wg_def guar_def, blast)
   7.419 +
   7.420 +lemma wg_equiv: 
   7.421 +  "(H: wg F X) = (F component_of H --> H:X)"
   7.422 +apply (unfold wg_def)
   7.423 +apply (simp (no_asm) add: guarantees_equiv)
   7.424 +apply (rule iffI)
   7.425 +apply (rule_tac [2] x = "{H}" in exI)
   7.426 +apply (blast+)
   7.427 +done
   7.428 +
   7.429 +
   7.430 +lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
   7.431 +by (simp add: wg_equiv)
   7.432 +
   7.433 +lemma wg_finite: 
   7.434 +    "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)  
   7.435 +          --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
   7.436 +apply clarify
   7.437 +apply (subgoal_tac "F component_of (JN F:FF. F) ")
   7.438 +apply (drule_tac X = X in component_of_wg, simp)
   7.439 +apply (simp add: component_of_def)
   7.440 +apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
   7.441 +apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
   7.442 +done
   7.443 +
   7.444 +lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
   7.445 +apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
   7.446 +apply blast
   7.447 +done
   7.448 +
   7.449 +(** From Charpentier and Chandy "Theorems About Composition" **)
   7.450 +(* Proposition 2 *)
   7.451 +lemma wx_subset: "(wx X)<=X"
   7.452 +by (unfold wx_def, auto)
   7.453 +
   7.454 +lemma wx_ex_prop: "ex_prop (wx X)"
   7.455 +apply (unfold wx_def)
   7.456 +apply (simp (no_asm) add: ex_prop_equiv)
   7.457 +apply safe
   7.458 +apply blast
   7.459 +apply auto
   7.460 +done
   7.461 +
   7.462 +lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
   7.463 +by (unfold wx_def, auto)
   7.464 +
   7.465 +(* Proposition 6 *)
   7.466 +lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
   7.467 +apply (unfold ex_prop_def, safe)
   7.468 +apply (drule_tac x = "G Join Ga" in spec)
   7.469 +apply (force simp add: ok_Join_iff1 Join_assoc)
   7.470 +apply (drule_tac x = "F Join Ga" in spec)
   7.471 +apply (simp (no_asm_use) add: ok_Join_iff1)
   7.472 +apply safe
   7.473 +apply (simp (no_asm_simp) add: ok_commute)
   7.474 +apply (subgoal_tac "F Join G = G Join F")
   7.475 +apply (simp (no_asm_simp) add: Join_assoc)
   7.476 +apply (simp (no_asm) add: Join_commute)
   7.477 +done
   7.478 +
   7.479 +(* Equivalence with the other definition of wx *)
   7.480 +
   7.481 +lemma wx_equiv: 
   7.482 + "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
   7.483 +
   7.484 +apply (unfold wx_def, safe)
   7.485 +apply (simp (no_asm_use) add: ex_prop_def)
   7.486 +apply (drule_tac x = x in spec)
   7.487 +apply (drule_tac x = G in spec)
   7.488 +apply (frule_tac c = "x Join G" in subsetD, safe)
   7.489 +apply (simp (no_asm))
   7.490 +apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
   7.491 +apply (rule_tac [2] wx'_ex_prop)
   7.492 +apply (rotate_tac 1)
   7.493 +apply (drule_tac x = SKIP in spec, auto)
   7.494 +done
   7.495 +
   7.496 +
   7.497 +(* Propositions 7 to 11 are about this second definition of wx. And
   7.498 +   they are the same as the ones proved for the first definition of wx by equivalence *)
   7.499 +   
   7.500 +(* Proposition 12 *)
   7.501 +(* Main result of the paper *)
   7.502 +lemma guarantees_wx_eq: 
   7.503 +   "(X guarantees Y) = wx(-X Un Y)"
   7.504 +apply (unfold guar_def)
   7.505 +apply (simp (no_asm) add: wx_equiv)
   7.506 +done
   7.507 +
   7.508 +(* {* Corollary, but this result has already been proved elsewhere *}
   7.509 + "ex_prop(X guarantees Y)"
   7.510 +  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
   7.511 +  qed "guarantees_ex_prop";
   7.512 +*)
   7.513 +
   7.514 +(* Rules given in section 7 of Chandy and Sander's
   7.515 +    Reasoning About Program composition paper *)
   7.516 +
   7.517 +lemma stable_guarantees_Always:
   7.518 +     "Init F <= A ==> F:(stable A) guarantees (Always A)"
   7.519 +apply (rule guaranteesI)
   7.520 +apply (simp (no_asm) add: Join_commute)
   7.521 +apply (rule stable_Join_Always1)
   7.522 +apply (simp_all add: invariant_def Join_stable)
   7.523 +done
   7.524 +
   7.525 +(* To be moved to WFair.ML *)
   7.526 +lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
   7.527 +apply (drule_tac B = "A-B" in constrains_weaken_L)
   7.528 +apply (drule_tac [2] B = "A-B" in transient_strengthen)
   7.529 +apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
   7.530 +apply (blast+)
   7.531 +done
   7.532 +
   7.533 +
   7.534 +
   7.535 +lemma constrains_guarantees_leadsTo:
   7.536 +     "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
   7.537 +apply (rule guaranteesI)
   7.538 +apply (rule leadsTo_Basis')
   7.539 +apply (drule constrains_weaken_R)
   7.540 +prefer 2 apply assumption
   7.541 +apply blast
   7.542 +apply (blast intro: Join_transient_I1)
   7.543 +done
   7.544 +
   7.545  end
     8.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Wed Jan 29 16:29:38 2003 +0100
     8.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Wed Jan 29 16:34:51 2003 +0100
     8.3 @@ -6,6 +6,193 @@
     8.4  Specialized UNITY tactics, and ML bindings of theorems
     8.5  *)
     8.6  
     8.7 +(*Union*)
     8.8 +val Init_SKIP = thm "Init_SKIP";
     8.9 +val Acts_SKIP = thm "Acts_SKIP";
    8.10 +val AllowedActs_SKIP = thm "AllowedActs_SKIP";
    8.11 +val reachable_SKIP = thm "reachable_SKIP";
    8.12 +val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff";
    8.13 +val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff";
    8.14 +val SKIP_in_stable = thm "SKIP_in_stable";
    8.15 +val Init_Join = thm "Init_Join";
    8.16 +val Acts_Join = thm "Acts_Join";
    8.17 +val AllowedActs_Join = thm "AllowedActs_Join";
    8.18 +val JN_empty = thm "JN_empty";
    8.19 +val JN_insert = thm "JN_insert";
    8.20 +val Init_JN = thm "Init_JN";
    8.21 +val Acts_JN = thm "Acts_JN";
    8.22 +val AllowedActs_JN = thm "AllowedActs_JN";
    8.23 +val JN_cong = thm "JN_cong";
    8.24 +val Join_commute = thm "Join_commute";
    8.25 +val Join_assoc = thm "Join_assoc";
    8.26 +val Join_left_commute = thm "Join_left_commute";
    8.27 +val Join_SKIP_left = thm "Join_SKIP_left";
    8.28 +val Join_SKIP_right = thm "Join_SKIP_right";
    8.29 +val Join_absorb = thm "Join_absorb";
    8.30 +val Join_left_absorb = thm "Join_left_absorb";
    8.31 +val Join_ac = thms "Join_ac";
    8.32 +val JN_absorb = thm "JN_absorb";
    8.33 +val JN_Un = thm "JN_Un";
    8.34 +val JN_constant = thm "JN_constant";
    8.35 +val JN_Join_distrib = thm "JN_Join_distrib";
    8.36 +val JN_Join_miniscope = thm "JN_Join_miniscope";
    8.37 +val JN_Join_diff = thm "JN_Join_diff";
    8.38 +val JN_constrains = thm "JN_constrains";
    8.39 +val Join_constrains = thm "Join_constrains";
    8.40 +val Join_unless = thm "Join_unless";
    8.41 +val Join_constrains_weaken = thm "Join_constrains_weaken";
    8.42 +val JN_constrains_weaken = thm "JN_constrains_weaken";
    8.43 +val JN_stable = thm "JN_stable";
    8.44 +val invariant_JN_I = thm "invariant_JN_I";
    8.45 +val Join_stable = thm "Join_stable";
    8.46 +val Join_increasing = thm "Join_increasing";
    8.47 +val invariant_JoinI = thm "invariant_JoinI";
    8.48 +val FP_JN = thm "FP_JN";
    8.49 +val JN_transient = thm "JN_transient";
    8.50 +val Join_transient = thm "Join_transient";
    8.51 +val Join_transient_I1 = thm "Join_transient_I1";
    8.52 +val Join_transient_I2 = thm "Join_transient_I2";
    8.53 +val JN_ensures = thm "JN_ensures";
    8.54 +val Join_ensures = thm "Join_ensures";
    8.55 +val stable_Join_constrains = thm "stable_Join_constrains";
    8.56 +val stable_Join_Always1 = thm "stable_Join_Always1";
    8.57 +val stable_Join_Always2 = thm "stable_Join_Always2";
    8.58 +val stable_Join_ensures1 = thm "stable_Join_ensures1";
    8.59 +val stable_Join_ensures2 = thm "stable_Join_ensures2";
    8.60 +val ok_SKIP1 = thm "ok_SKIP1";
    8.61 +val ok_SKIP2 = thm "ok_SKIP2";
    8.62 +val ok_Join_commute = thm "ok_Join_commute";
    8.63 +val ok_commute = thm "ok_commute";
    8.64 +val ok_sym = thm "ok_sym";
    8.65 +val ok_iff_OK = thm "ok_iff_OK";
    8.66 +val ok_Join_iff1 = thm "ok_Join_iff1";
    8.67 +val ok_Join_iff2 = thm "ok_Join_iff2";
    8.68 +val ok_Join_commute_I = thm "ok_Join_commute_I";
    8.69 +val ok_JN_iff1 = thm "ok_JN_iff1";
    8.70 +val ok_JN_iff2 = thm "ok_JN_iff2";
    8.71 +val OK_iff_ok = thm "OK_iff_ok";
    8.72 +val OK_imp_ok = thm "OK_imp_ok";
    8.73 +val Allowed_SKIP = thm "Allowed_SKIP";
    8.74 +val Allowed_Join = thm "Allowed_Join";
    8.75 +val Allowed_JN = thm "Allowed_JN";
    8.76 +val ok_iff_Allowed = thm "ok_iff_Allowed";
    8.77 +val OK_iff_Allowed = thm "OK_iff_Allowed";
    8.78 +val safety_prop_Acts_iff = thm "safety_prop_Acts_iff";
    8.79 +val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed";
    8.80 +val Allowed_eq = thm "Allowed_eq";
    8.81 +val def_prg_Allowed = thm "def_prg_Allowed";
    8.82 +val safety_prop_constrains = thm "safety_prop_constrains";
    8.83 +val safety_prop_stable = thm "safety_prop_stable";
    8.84 +val safety_prop_Int = thm "safety_prop_Int";
    8.85 +val safety_prop_INTER1 = thm "safety_prop_INTER1";
    8.86 +val safety_prop_INTER = thm "safety_prop_INTER";
    8.87 +val def_UNION_ok_iff = thm "def_UNION_ok_iff";
    8.88 +
    8.89 +(*Comp*)
    8.90 +val preserves_def = thm "preserves_def";
    8.91 +val funPair_def = thm "funPair_def";
    8.92 +val componentI = thm "componentI";
    8.93 +val component_eq_subset = thm "component_eq_subset";
    8.94 +val component_SKIP = thm "component_SKIP";
    8.95 +val component_refl = thm "component_refl";
    8.96 +val SKIP_minimal = thm "SKIP_minimal";
    8.97 +val component_Join1 = thm "component_Join1";
    8.98 +val component_Join2 = thm "component_Join2";
    8.99 +val Join_absorb1 = thm "Join_absorb1";
   8.100 +val Join_absorb2 = thm "Join_absorb2";
   8.101 +val JN_component_iff = thm "JN_component_iff";
   8.102 +val component_JN = thm "component_JN";
   8.103 +val component_trans = thm "component_trans";
   8.104 +val component_antisym = thm "component_antisym";
   8.105 +val Join_component_iff = thm "Join_component_iff";
   8.106 +val component_constrains = thm "component_constrains";
   8.107 +val program_less_le = thm "program_less_le";
   8.108 +val preservesI = thm "preservesI";
   8.109 +val preserves_imp_eq = thm "preserves_imp_eq";
   8.110 +val Join_preserves = thm "Join_preserves";
   8.111 +val JN_preserves = thm "JN_preserves";
   8.112 +val SKIP_preserves = thm "SKIP_preserves";
   8.113 +val funPair_apply = thm "funPair_apply";
   8.114 +val preserves_funPair = thm "preserves_funPair";
   8.115 +val funPair_o_distrib = thm "funPair_o_distrib";
   8.116 +val fst_o_funPair = thm "fst_o_funPair";
   8.117 +val snd_o_funPair = thm "snd_o_funPair";
   8.118 +val subset_preserves_o = thm "subset_preserves_o";
   8.119 +val preserves_subset_stable = thm "preserves_subset_stable";
   8.120 +val preserves_subset_increasing = thm "preserves_subset_increasing";
   8.121 +val preserves_id_subset_stable = thm "preserves_id_subset_stable";
   8.122 +val safety_prop_preserves = thm "safety_prop_preserves";
   8.123 +val stable_localTo_stable2 = thm "stable_localTo_stable2";
   8.124 +val Increasing_preserves_Stable = thm "Increasing_preserves_Stable";
   8.125 +val component_of_imp_component = thm "component_of_imp_component";
   8.126 +val component_of_refl = thm "component_of_refl";
   8.127 +val component_of_SKIP = thm "component_of_SKIP";
   8.128 +val component_of_trans = thm "component_of_trans";
   8.129 +val strict_component_of_eq = thm "strict_component_of_eq";
   8.130 +val localize_Init_eq = thm "localize_Init_eq";
   8.131 +val localize_Acts_eq = thm "localize_Acts_eq";
   8.132 +val localize_AllowedActs_eq = thm "localize_AllowedActs_eq";
   8.133 +
   8.134 +(*Guar*)
   8.135 +val guar_def = thm "guar_def";
   8.136 +val OK_insert_iff = thm "OK_insert_iff";
   8.137 +val ex1 = thm "ex1";
   8.138 +val ex2 = thm "ex2";
   8.139 +val ex_prop_finite = thm "ex_prop_finite";
   8.140 +val ex_prop_equiv = thm "ex_prop_equiv";
   8.141 +val uv1 = thm "uv1";
   8.142 +val uv2 = thm "uv2";
   8.143 +val uv_prop_finite = thm "uv_prop_finite";
   8.144 +val guaranteesI = thm "guaranteesI";
   8.145 +val guaranteesD = thm "guaranteesD";
   8.146 +val component_guaranteesD = thm "component_guaranteesD";
   8.147 +val guarantees_weaken = thm "guarantees_weaken";
   8.148 +val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV";
   8.149 +val subset_imp_guarantees = thm "subset_imp_guarantees";
   8.150 +val ex_prop_imp = thm "ex_prop_imp";
   8.151 +val guarantees_imp = thm "guarantees_imp";
   8.152 +val ex_prop_equiv2 = thm "ex_prop_equiv2";
   8.153 +val guarantees_UN_left = thm "guarantees_UN_left";
   8.154 +val guarantees_Un_left = thm "guarantees_Un_left";
   8.155 +val guarantees_INT_right = thm "guarantees_INT_right";
   8.156 +val guarantees_Int_right = thm "guarantees_Int_right";
   8.157 +val guarantees_Int_right_I = thm "guarantees_Int_right_I";
   8.158 +val guarantees_INT_right_iff = thm "guarantees_INT_right_iff";
   8.159 +val shunting = thm "shunting";
   8.160 +val contrapositive = thm "contrapositive";
   8.161 +val combining1 = thm "combining1";
   8.162 +val combining2 = thm "combining2";
   8.163 +val all_guarantees = thm "all_guarantees";
   8.164 +val ex_guarantees = thm "ex_guarantees";
   8.165 +val guarantees_Join_Int = thm "guarantees_Join_Int";
   8.166 +val guarantees_Join_Un = thm "guarantees_Join_Un";
   8.167 +val guarantees_JN_INT = thm "guarantees_JN_INT";
   8.168 +val guarantees_JN_UN = thm "guarantees_JN_UN";
   8.169 +val guarantees_Join_I1 = thm "guarantees_Join_I1";
   8.170 +val guarantees_Join_I2 = thm "guarantees_Join_I2";
   8.171 +val guarantees_JN_I = thm "guarantees_JN_I";
   8.172 +val Join_welldef_D1 = thm "Join_welldef_D1";
   8.173 +val Join_welldef_D2 = thm "Join_welldef_D2";
   8.174 +val refines_refl = thm "refines_refl";
   8.175 +val ex_refinement_thm = thm "ex_refinement_thm";
   8.176 +val uv_refinement_thm = thm "uv_refinement_thm";
   8.177 +val guarantees_equiv = thm "guarantees_equiv";
   8.178 +val wg_weakest = thm "wg_weakest";
   8.179 +val wg_guarantees = thm "wg_guarantees";
   8.180 +val wg_equiv = thm "wg_equiv";
   8.181 +val component_of_wg = thm "component_of_wg";
   8.182 +val wg_finite = thm "wg_finite";
   8.183 +val wg_ex_prop = thm "wg_ex_prop";
   8.184 +val wx_subset = thm "wx_subset";
   8.185 +val wx_ex_prop = thm "wx_ex_prop";
   8.186 +val wx_weakest = thm "wx_weakest";
   8.187 +val wx'_ex_prop = thm "wx'_ex_prop";
   8.188 +val wx_equiv = thm "wx_equiv";
   8.189 +val guarantees_wx_eq = thm "guarantees_wx_eq";
   8.190 +val stable_guarantees_Always = thm "stable_guarantees_Always";
   8.191 +val leadsTo_Basis = thm "leadsTo_Basis";
   8.192 +val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo";
   8.193 +
   8.194  (*Extend*)
   8.195  val Restrict_iff = thm "Restrict_iff";
   8.196  val Restrict_UNIV = thm "Restrict_UNIV";
     9.1 --- a/src/HOL/UNITY/Union.ML	Wed Jan 29 16:29:38 2003 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,471 +0,0 @@
     9.4 -(*  Title:      HOL/UNITY/Union.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1998  University of Cambridge
     9.8 -
     9.9 -Unions of programs
    9.10 -
    9.11 -From Misra's Chapter 5: Asynchronous Compositions of Programs
    9.12 -*)
    9.13 -
    9.14 -
    9.15 -(** SKIP **)
    9.16 -
    9.17 -Goal "Init SKIP = UNIV";
    9.18 -by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    9.19 -qed "Init_SKIP";
    9.20 -
    9.21 -Goal "Acts SKIP = {Id}";
    9.22 -by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    9.23 -qed "Acts_SKIP";
    9.24 -
    9.25 -Goal "AllowedActs SKIP = UNIV";
    9.26 -by (auto_tac (claset(), simpset() addsimps [SKIP_def]));  
    9.27 -qed "AllowedActs_SKIP";
    9.28 -
    9.29 -Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP];
    9.30 -
    9.31 -Goal "reachable SKIP = UNIV";
    9.32 -by (force_tac (claset() addEs [reachable.induct]
    9.33 -			addIs reachable.intrs, simpset()) 1);
    9.34 -qed "reachable_SKIP";
    9.35 -
    9.36 -Addsimps [reachable_SKIP];
    9.37 -
    9.38 -(** SKIP and safety properties **)
    9.39 -
    9.40 -Goalw [constrains_def] "(SKIP : A co B) = (A<=B)";
    9.41 -by Auto_tac;
    9.42 -qed "SKIP_in_constrains_iff";
    9.43 -AddIffs [SKIP_in_constrains_iff];
    9.44 -
    9.45 -Goalw [Constrains_def] "(SKIP : A Co B) = (A<=B)";
    9.46 -by Auto_tac;
    9.47 -qed "SKIP_in_Constrains_iff";
    9.48 -AddIffs [SKIP_in_Constrains_iff];
    9.49 -
    9.50 -Goalw [stable_def] "SKIP : stable A";
    9.51 -by Auto_tac;
    9.52 -qed "SKIP_in_stable";
    9.53 -AddIffs [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable];
    9.54 -
    9.55 -
    9.56 -(** Join **)
    9.57 -
    9.58 -Goal "Init (F Join G) = Init F Int Init G";
    9.59 -by (simp_tac (simpset() addsimps [Join_def]) 1);
    9.60 -qed "Init_Join";
    9.61 -
    9.62 -Goal "Acts (F Join G) = Acts F Un Acts G";
    9.63 -by (auto_tac (claset(), simpset() addsimps [Join_def]));
    9.64 -qed "Acts_Join";
    9.65 -
    9.66 -Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G";
    9.67 -by (auto_tac (claset(), simpset() addsimps [Join_def]));
    9.68 -qed "AllowedActs_Join";
    9.69 -
    9.70 -Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
    9.71 -
    9.72 -
    9.73 -(** JN **)
    9.74 -
    9.75 -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
    9.76 -by Auto_tac;
    9.77 -qed "JN_empty";
    9.78 -Addsimps [JN_empty];
    9.79 -
    9.80 -Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)";
    9.81 -by (rtac program_equalityI 1);
    9.82 -by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def]));  
    9.83 -qed "JN_insert";
    9.84 -Addsimps[JN_empty, JN_insert];
    9.85 -
    9.86 -Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))";
    9.87 -by (simp_tac (simpset() addsimps [JOIN_def]) 1);
    9.88 -qed "Init_JN";
    9.89 -
    9.90 -Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))";
    9.91 -by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
    9.92 -qed "Acts_JN";
    9.93 -
    9.94 -Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))";
    9.95 -by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
    9.96 -qed "AllowedActs_JN";
    9.97 -
    9.98 -Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
    9.99 -
   9.100 -val prems = Goalw [JOIN_def]
   9.101 -    "[| I=J;  !!i. i:J ==> F i = G i |] ==> \
   9.102 -\    (JN i:I. F i) = (JN i:J. G i)";
   9.103 -by (asm_simp_tac (simpset() addsimps prems) 1);
   9.104 -qed "JN_cong";
   9.105 -
   9.106 -Addcongs [JN_cong];
   9.107 -
   9.108 -
   9.109 -(** Algebraic laws **)
   9.110 -
   9.111 -Goal "F Join G = G Join F";
   9.112 -by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
   9.113 -qed "Join_commute";
   9.114 -
   9.115 -Goal "(F Join G) Join H = F Join (G Join H)";
   9.116 -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
   9.117 -qed "Join_assoc";
   9.118 - 
   9.119 -Goal "A Join (B Join C) = B Join (A Join C)";
   9.120 -by(rtac ([Join_assoc,Join_commute] MRS
   9.121 -         read_instantiate[("f","op Join")](thm"mk_left_commute")) 1);
   9.122 -qed "Join_left_commute";
   9.123 -
   9.124 -
   9.125 -Goalw [Join_def, SKIP_def] "SKIP Join F = F";
   9.126 -by (rtac program_equalityI 1);
   9.127 -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
   9.128 -qed "Join_SKIP_left";
   9.129 -
   9.130 -Goalw [Join_def, SKIP_def] "F Join SKIP = F";
   9.131 -by (rtac program_equalityI 1);
   9.132 -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb])));
   9.133 -qed "Join_SKIP_right";
   9.134 -
   9.135 -Addsimps [Join_SKIP_left, Join_SKIP_right];
   9.136 -
   9.137 -Goalw [Join_def] "F Join F = F";
   9.138 -by (rtac program_equalityI 1);
   9.139 -by Auto_tac;
   9.140 -qed "Join_absorb";
   9.141 -
   9.142 -Addsimps [Join_absorb];
   9.143 -
   9.144 -Goalw [Join_def] "F Join (F Join G) = F Join G";
   9.145 -by (rtac program_equalityI 1);
   9.146 -by Auto_tac;
   9.147 -qed "Join_left_absorb";
   9.148 -
   9.149 -(*Join is an AC-operator*)
   9.150 -val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute];
   9.151 -
   9.152 -
   9.153 -(*** JN laws ***)
   9.154 -
   9.155 -(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
   9.156 -Goal "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)";
   9.157 -by (auto_tac (claset() addSIs [program_equalityI], simpset()));
   9.158 -qed "JN_absorb";
   9.159 -
   9.160 -Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))";
   9.161 -by (auto_tac (claset() addSIs [program_equalityI], simpset()));
   9.162 -qed "JN_Un";
   9.163 -
   9.164 -Goal "(JN i:I. c) = (if I={} then SKIP else c)";
   9.165 -by (rtac program_equalityI 1);
   9.166 -by Auto_tac;
   9.167 -qed "JN_constant";
   9.168 -
   9.169 -Goal "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)";
   9.170 -by (auto_tac (claset() addSIs [program_equalityI], simpset()));
   9.171 -qed "JN_Join_distrib";
   9.172 -
   9.173 -Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)";
   9.174 -by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1);
   9.175 -by Auto_tac;
   9.176 -qed "JN_Join_miniscope";
   9.177 -
   9.178 -(*Used to prove guarantees_JN_I*)
   9.179 -Goalw  [JOIN_def, Join_def] "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F";
   9.180 -by (rtac program_equalityI 1);
   9.181 -by Auto_tac;
   9.182 -qed "JN_Join_diff";
   9.183 -
   9.184 -
   9.185 -(*** Safety: co, stable, FP ***)
   9.186 -
   9.187 -(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
   9.188 -  alternative precondition is A<=B, but most proofs using this rule require
   9.189 -  I to be nonempty for other reasons anyway.*)
   9.190 -Goalw [constrains_def, JOIN_def]
   9.191 -    "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)";
   9.192 -by (Simp_tac 1);
   9.193 -by (Blast_tac 1);
   9.194 -qed "JN_constrains";
   9.195 -
   9.196 -Goal "(F Join G : A co B) = (F : A co B & G : A co B)";
   9.197 -by (auto_tac
   9.198 -    (claset(),
   9.199 -     simpset() addsimps [constrains_def, Join_def]));
   9.200 -qed "Join_constrains";
   9.201 -
   9.202 -Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)";
   9.203 -by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
   9.204 -qed "Join_unless";
   9.205 -
   9.206 -Addsimps [Join_constrains, Join_unless];
   9.207 -
   9.208 -(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   9.209 -  reachable (F Join G) could be much bigger than reachable F, reachable G
   9.210 -*)
   9.211 -
   9.212 -
   9.213 -Goal "[| F : A co A';  G : B co B' |] \
   9.214 -\     ==> F Join G : (A Int B) co (A' Un B')";
   9.215 -by (Simp_tac 1);
   9.216 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
   9.217 -qed "Join_constrains_weaken";
   9.218 -
   9.219 -(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
   9.220 -Goal "[| ALL i:I. F i : A i co A' i;  i: I |] \
   9.221 -\     ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)";
   9.222 -by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1);
   9.223 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
   9.224 -qed "JN_constrains_weaken";
   9.225 -
   9.226 -Goal "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)";
   9.227 -by (asm_simp_tac 
   9.228 -    (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1);
   9.229 -qed "JN_stable";
   9.230 -
   9.231 -Goal "[| ALL i:I. F i : invariant A;  i : I |]  \
   9.232 -\      ==> (JN i:I. F i) : invariant A";
   9.233 -by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1);
   9.234 -by (Blast_tac 1);
   9.235 -bind_thm ("invariant_JN_I", ballI RS result());
   9.236 -
   9.237 -Goal "(F Join G : stable A) = \
   9.238 -\     (F : stable A & G : stable A)";
   9.239 -by (simp_tac (simpset() addsimps [stable_def]) 1);
   9.240 -qed "Join_stable";
   9.241 -
   9.242 -Goal "(F Join G : increasing f) = \
   9.243 -\     (F : increasing f & G : increasing f)";
   9.244 -by (simp_tac (simpset() addsimps [increasing_def, Join_stable]) 1);
   9.245 -by (Blast_tac 1);
   9.246 -qed "Join_increasing";
   9.247 -
   9.248 -Addsimps [Join_stable, Join_increasing];
   9.249 -
   9.250 -Goal "[| F : invariant A; G : invariant A |]  \
   9.251 -\     ==> F Join G : invariant A";
   9.252 -by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
   9.253 -by (Blast_tac 1);
   9.254 -qed "invariant_JoinI";
   9.255 -
   9.256 -Goal "FP (JN i:I. F i) = (INT i:I. FP (F i))";
   9.257 -by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1);
   9.258 -qed "FP_JN";
   9.259 -
   9.260 -
   9.261 -(*** Progress: transient, ensures ***)
   9.262 -
   9.263 -Goal "i : I ==> \
   9.264 -\   (JN i:I. F i) : transient A = (EX i:I. F i : transient A)";
   9.265 -by (auto_tac (claset(),
   9.266 -	      simpset() addsimps [transient_def, JOIN_def]));
   9.267 -qed "JN_transient";
   9.268 -
   9.269 -Goal "F Join G : transient A = \
   9.270 -\     (F : transient A | G : transient A)";
   9.271 -by (auto_tac (claset(),
   9.272 -	      simpset() addsimps [bex_Un, transient_def,
   9.273 -				  Join_def]));
   9.274 -qed "Join_transient";
   9.275 -
   9.276 -Addsimps [Join_transient];
   9.277 -
   9.278 -Goal "F : transient A ==> F Join G : transient A";
   9.279 -by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
   9.280 -qed "Join_transient_I1";
   9.281 -
   9.282 -Goal "G : transient A ==> F Join G : transient A";
   9.283 -by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
   9.284 -qed "Join_transient_I2";
   9.285 -
   9.286 -(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
   9.287 -Goal "i : I ==> \
   9.288 -\     (JN i:I. F i) : A ensures B = \
   9.289 -\     ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))";
   9.290 -by (auto_tac (claset(),
   9.291 -	      simpset() addsimps [ensures_def, JN_constrains, JN_transient]));
   9.292 -qed "JN_ensures";
   9.293 -
   9.294 -Goalw [ensures_def]
   9.295 -     "F Join G : A ensures B =     \
   9.296 -\     (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \
   9.297 -\      (F : transient (A-B) | G : transient (A-B)))";
   9.298 -by (auto_tac (claset(), simpset() addsimps [Join_transient]));
   9.299 -qed "Join_ensures";
   9.300 -
   9.301 -Goalw [stable_def, constrains_def, Join_def]
   9.302 -    "[| F : stable A;  G : A co A' |] \
   9.303 -\    ==> F Join G : A co A'";
   9.304 -by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
   9.305 -by (Blast_tac 1);
   9.306 -qed "stable_Join_constrains";
   9.307 -
   9.308 -(*Premise for G cannot use Always because  F: Stable A  is weaker than
   9.309 -  G : stable A *)
   9.310 -Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Always A";
   9.311 -by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, 
   9.312 -				       Stable_eq_stable]) 1);
   9.313 -by (force_tac(claset() addIs [stable_Int], simpset()) 1);
   9.314 -qed "stable_Join_Always1";
   9.315 -
   9.316 -(*As above, but exchanging the roles of F and G*)
   9.317 -Goal "[| F : invariant A;  G : stable A |] ==> F Join G : Always A";
   9.318 -by (stac Join_commute 1);
   9.319 -by (blast_tac (claset() addIs [stable_Join_Always1]) 1);
   9.320 -qed "stable_Join_Always2";
   9.321 -
   9.322 -Goal "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B";
   9.323 -by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);
   9.324 -by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
   9.325 -by (etac constrains_weaken 1);
   9.326 -by Auto_tac;
   9.327 -qed "stable_Join_ensures1";
   9.328 -
   9.329 -(*As above, but exchanging the roles of F and G*)
   9.330 -Goal "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B";
   9.331 -by (stac Join_commute 1);
   9.332 -by (blast_tac (claset() addIs [stable_Join_ensures1]) 1);
   9.333 -qed "stable_Join_ensures2";
   9.334 -
   9.335 -
   9.336 -(*** the ok and OK relations ***)
   9.337 -
   9.338 -Goal "SKIP ok F";
   9.339 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.340 -qed "ok_SKIP1";  
   9.341 -
   9.342 -Goal "F ok SKIP";
   9.343 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.344 -qed "ok_SKIP2";
   9.345 -
   9.346 -AddIffs [ok_SKIP1, ok_SKIP2];  
   9.347 -
   9.348 -Goal "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))";
   9.349 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.350 -qed "ok_Join_commute";
   9.351 -
   9.352 -Goal "(F ok G) = (G ok F)";
   9.353 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.354 -qed "ok_commute";
   9.355 -
   9.356 -bind_thm ("ok_sym", ok_commute RS iffD1);
   9.357 -
   9.358 -Goal "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
   9.359 -by (asm_full_simp_tac
   9.360 -    (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
   9.361 -                   OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); 
   9.362 -by (Blast_tac 1); 
   9.363 -qed "ok_iff_OK";
   9.364 -
   9.365 -Goal "F ok (G Join H) = (F ok G & F ok H)";
   9.366 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.367 -qed "ok_Join_iff1";
   9.368 -
   9.369 -Goal "(G Join H) ok F = (G ok F & H ok F)";
   9.370 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.371 -qed "ok_Join_iff2";
   9.372 -AddIffs [ok_Join_iff1, ok_Join_iff2];
   9.373 -
   9.374 -(*useful?  Not with the previous two around*)
   9.375 -Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
   9.376 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.377 -qed "ok_Join_commute_I";
   9.378 -
   9.379 -Goal "F ok (JOIN I G) = (ALL i:I. F ok G i)";
   9.380 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.381 -qed "ok_JN_iff1";
   9.382 -
   9.383 -Goal "(JOIN I G) ok F =  (ALL i:I. G i ok F)";
   9.384 -by (auto_tac (claset(), simpset() addsimps [ok_def]));
   9.385 -qed "ok_JN_iff2";
   9.386 -AddIffs [ok_JN_iff1, ok_JN_iff2];
   9.387 -
   9.388 -Goal "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"; 
   9.389 -by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));  
   9.390 -qed "OK_iff_ok";
   9.391 -
   9.392 -Goal "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"; 
   9.393 -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));  
   9.394 -qed "OK_imp_ok";
   9.395 -
   9.396 -
   9.397 -(*** Allowed ***)
   9.398 -
   9.399 -Goal "Allowed SKIP = UNIV";
   9.400 -by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
   9.401 -qed "Allowed_SKIP";
   9.402 -
   9.403 -Goal "Allowed (F Join G) = Allowed F Int Allowed G";
   9.404 -by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
   9.405 -qed "Allowed_Join";
   9.406 -
   9.407 -Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))";
   9.408 -by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
   9.409 -qed "Allowed_JN";
   9.410 -
   9.411 -Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
   9.412 -
   9.413 -Goal "F ok G = (F : Allowed G & G : Allowed F)";
   9.414 -by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
   9.415 -qed "ok_iff_Allowed";
   9.416 -
   9.417 -Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"; 
   9.418 -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));  
   9.419 -qed "OK_iff_Allowed";
   9.420 -
   9.421 -(*** safety_prop, for reasoning about given instances of "ok" ***)
   9.422 -
   9.423 -Goal "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)";
   9.424 -by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
   9.425 -qed "safety_prop_Acts_iff";
   9.426 -
   9.427 -Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)";
   9.428 -by (auto_tac (claset(), 
   9.429 -      simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym]));  
   9.430 -qed "safety_prop_AllowedActs_iff_Allowed";
   9.431 -
   9.432 -Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X";
   9.433 -by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1); 
   9.434 -qed "Allowed_eq";
   9.435 -
   9.436 -Goal "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] \
   9.437 -\     ==> Allowed F = X";
   9.438 -by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); 
   9.439 -qed "def_prg_Allowed";
   9.440 -
   9.441 -(*For safety_prop to hold, the property must be satisfiable!*)
   9.442 -Goal "safety_prop (A co B) = (A <= B)";
   9.443 -by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
   9.444 -by (Blast_tac 1); 
   9.445 -qed "safety_prop_constrains";
   9.446 -AddIffs [safety_prop_constrains];
   9.447 -
   9.448 -Goal "safety_prop (stable A)";
   9.449 -by (simp_tac (simpset() addsimps [stable_def]) 1);
   9.450 -qed "safety_prop_stable";
   9.451 -AddIffs [safety_prop_stable];
   9.452 -
   9.453 -Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)";
   9.454 -by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1); 
   9.455 -by (Blast_tac 1); 
   9.456 -qed "safety_prop_Int";
   9.457 -Addsimps [safety_prop_Int];
   9.458 -
   9.459 -Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)";
   9.460 -by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
   9.461 -by (Blast_tac 1); 
   9.462 -bind_thm ("safety_prop_INTER1", allI RS result());
   9.463 -Addsimps [safety_prop_INTER1];
   9.464 -							       
   9.465 -Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)";
   9.466 -by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
   9.467 -by (Blast_tac 1); 
   9.468 -bind_thm ("safety_prop_INTER", ballI RS result());
   9.469 -Addsimps [safety_prop_INTER];
   9.470 -
   9.471 -Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \
   9.472 -\     ==> F ok G = (G : X & acts <= AllowedActs G)";
   9.473 -by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff]));  
   9.474 -qed "def_UNION_ok_iff";
    10.1 --- a/src/HOL/UNITY/Union.thy	Wed Jan 29 16:29:38 2003 +0100
    10.2 +++ b/src/HOL/UNITY/Union.thy	Wed Jan 29 16:34:51 2003 +0100
    10.3 @@ -8,28 +8,28 @@
    10.4  Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
    10.5  *)
    10.6  
    10.7 -Union = SubstAx + FP +
    10.8 +theory Union = SubstAx + FP:
    10.9  
   10.10  constdefs
   10.11  
   10.12    (*FIXME: conjoin Init F Int Init G ~= {} *) 
   10.13 -  ok :: ['a program, 'a program] => bool      (infixl 65)
   10.14 +  ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
   10.15      "F ok G == Acts F <= AllowedActs G &
   10.16                 Acts G <= AllowedActs F"
   10.17  
   10.18    (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
   10.19 -  OK  :: ['a set, 'a => 'b program] => bool
   10.20 +  OK  :: "['a set, 'a => 'b program] => bool"
   10.21      "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
   10.22  
   10.23 -  JOIN  :: ['a set, 'a => 'b program] => 'b program
   10.24 +  JOIN  :: "['a set, 'a => 'b program] => 'b program"
   10.25      "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
   10.26  			     INT i:I. AllowedActs (F i))"
   10.27  
   10.28 -  Join :: ['a program, 'a program] => 'a program      (infixl 65)
   10.29 +  Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
   10.30      "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
   10.31  			     AllowedActs F Int AllowedActs G)"
   10.32  
   10.33 -  SKIP :: 'a program
   10.34 +  SKIP :: "'a program"
   10.35      "SKIP == mk_program (UNIV, {}, UNIV)"
   10.36  
   10.37    (*Characterizes safety properties.  Used with specifying AllowedActs*)
   10.38 @@ -37,8 +37,8 @@
   10.39      "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
   10.40  
   10.41  syntax
   10.42 -  "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
   10.43 -  "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
   10.44 +  "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   10.45 +  "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
   10.46  
   10.47  translations
   10.48    "JN x:A. B"   == "JOIN A (%x. B)"
   10.49 @@ -46,9 +46,375 @@
   10.50    "JN x. B"     == "JOIN UNIV (%x. B)"
   10.51  
   10.52  syntax (xsymbols)
   10.53 -  SKIP      :: 'a program                              ("\\<bottom>")
   10.54 -  "op Join" :: ['a program, 'a program] => 'a program  (infixl "\\<squnion>" 65)
   10.55 -  "@JOIN1"  :: [pttrns, 'b set] => 'b set              ("(3\\<Squnion> _./ _)" 10)
   10.56 -  "@JOIN"   :: [pttrn, 'a set, 'b set] => 'b set       ("(3\\<Squnion> _:_./ _)" 10)
   10.57 +  SKIP      :: "'a program"                              ("\<bottom>")
   10.58 +  "op Join" :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
   10.59 +  "@JOIN1"  :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
   10.60 +  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _:_./ _)" 10)
   10.61 +
   10.62 +
   10.63 +(** SKIP **)
   10.64 +
   10.65 +lemma Init_SKIP [simp]: "Init SKIP = UNIV"
   10.66 +by (simp add: SKIP_def)
   10.67 +
   10.68 +lemma Acts_SKIP [simp]: "Acts SKIP = {Id}"
   10.69 +by (simp add: SKIP_def)
   10.70 +
   10.71 +lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV"
   10.72 +by (auto simp add: SKIP_def)
   10.73 +
   10.74 +lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
   10.75 +by (force elim: reachable.induct intro: reachable.intros)
   10.76 +
   10.77 +(** SKIP and safety properties **)
   10.78 +
   10.79 +lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
   10.80 +by (unfold constrains_def, auto)
   10.81 +
   10.82 +lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
   10.83 +by (unfold Constrains_def, auto)
   10.84 +
   10.85 +lemma SKIP_in_stable [iff]: "SKIP : stable A"
   10.86 +by (unfold stable_def, auto)
   10.87 +
   10.88 +declare SKIP_in_stable [THEN stable_imp_Stable, iff]
   10.89 +
   10.90 +
   10.91 +(** Join **)
   10.92 +
   10.93 +lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
   10.94 +by (simp add: Join_def)
   10.95 +
   10.96 +lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
   10.97 +by (auto simp add: Join_def)
   10.98 +
   10.99 +lemma AllowedActs_Join [simp]:
  10.100 +     "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
  10.101 +by (auto simp add: Join_def)
  10.102 +
  10.103 +
  10.104 +(** JN **)
  10.105 +
  10.106 +lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
  10.107 +by (unfold JOIN_def SKIP_def, auto)
  10.108 +
  10.109 +lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
  10.110 +apply (rule program_equalityI)
  10.111 +apply (auto simp add: JOIN_def Join_def)
  10.112 +done
  10.113 +
  10.114 +lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
  10.115 +by (simp add: JOIN_def)
  10.116 +
  10.117 +lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
  10.118 +by (auto simp add: JOIN_def)
  10.119 +
  10.120 +lemma AllowedActs_JN [simp]:
  10.121 +     "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
  10.122 +by (auto simp add: JOIN_def)
  10.123 +
  10.124 +
  10.125 +lemma JN_cong [cong]: 
  10.126 +    "[| I=J;  !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
  10.127 +by (simp add: JOIN_def)
  10.128 +
  10.129 +
  10.130 +(** Algebraic laws **)
  10.131 +
  10.132 +lemma Join_commute: "F Join G = G Join F"
  10.133 +by (simp add: Join_def Un_commute Int_commute)
  10.134 +
  10.135 +lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
  10.136 +by (simp add: Un_ac Join_def Int_assoc insert_absorb)
  10.137 + 
  10.138 +lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
  10.139 +by (simp add: Un_ac Int_ac Join_def insert_absorb)
  10.140 +
  10.141 +lemma Join_SKIP_left [simp]: "SKIP Join F = F"
  10.142 +apply (unfold Join_def SKIP_def)
  10.143 +apply (rule program_equalityI)
  10.144 +apply (simp_all (no_asm) add: insert_absorb)
  10.145 +done
  10.146 +
  10.147 +lemma Join_SKIP_right [simp]: "F Join SKIP = F"
  10.148 +apply (unfold Join_def SKIP_def)
  10.149 +apply (rule program_equalityI)
  10.150 +apply (simp_all (no_asm) add: insert_absorb)
  10.151 +done
  10.152 +
  10.153 +lemma Join_absorb [simp]: "F Join F = F"
  10.154 +apply (unfold Join_def)
  10.155 +apply (rule program_equalityI, auto)
  10.156 +done
  10.157 +
  10.158 +lemma Join_left_absorb: "F Join (F Join G) = F Join G"
  10.159 +apply (unfold Join_def)
  10.160 +apply (rule program_equalityI, auto)
  10.161 +done
  10.162 +
  10.163 +(*Join is an AC-operator*)
  10.164 +lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
  10.165 +
  10.166 +
  10.167 +(*** JN laws ***)
  10.168 +
  10.169 +(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
  10.170 +lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
  10.171 +by (auto intro!: program_equalityI)
  10.172 +
  10.173 +lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
  10.174 +by (auto intro!: program_equalityI)
  10.175 +
  10.176 +lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
  10.177 +by (rule program_equalityI, auto)
  10.178 +
  10.179 +lemma JN_Join_distrib:
  10.180 +     "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)"
  10.181 +by (auto intro!: program_equalityI)
  10.182 +
  10.183 +lemma JN_Join_miniscope:
  10.184 +     "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
  10.185 +by (auto simp add: JN_Join_distrib JN_constant)
  10.186 +
  10.187 +(*Used to prove guarantees_JN_I*)
  10.188 +lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
  10.189 +apply (unfold JOIN_def Join_def)
  10.190 +apply (rule program_equalityI, auto)
  10.191 +done
  10.192 +
  10.193 +
  10.194 +(*** Safety: co, stable, FP ***)
  10.195 +
  10.196 +(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
  10.197 +  alternative precondition is A<=B, but most proofs using this rule require
  10.198 +  I to be nonempty for other reasons anyway.*)
  10.199 +lemma JN_constrains: 
  10.200 +    "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
  10.201 +by (simp add: constrains_def JOIN_def, blast)
  10.202 +
  10.203 +lemma Join_constrains [simp]:
  10.204 +     "(F Join G : A co B) = (F : A co B & G : A co B)"
  10.205 +by (auto simp add: constrains_def Join_def)
  10.206 +
  10.207 +lemma Join_unless [simp]:
  10.208 +     "(F Join G : A unless B) = (F : A unless B & G : A unless B)"
  10.209 +by (simp add: Join_constrains unless_def)
  10.210 +
  10.211 +(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
  10.212 +  reachable (F Join G) could be much bigger than reachable F, reachable G
  10.213 +*)
  10.214 +
  10.215 +
  10.216 +lemma Join_constrains_weaken:
  10.217 +     "[| F : A co A';  G : B co B' |]  
  10.218 +      ==> F Join G : (A Int B) co (A' Un B')"
  10.219 +by (simp, blast intro: constrains_weaken)
  10.220 +
  10.221 +(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
  10.222 +lemma JN_constrains_weaken:
  10.223 +     "[| ALL i:I. F i : A i co A' i;  i: I |]  
  10.224 +      ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"
  10.225 +apply (simp (no_asm_simp) add: JN_constrains)
  10.226 +apply (blast intro: constrains_weaken)
  10.227 +done
  10.228 +
  10.229 +lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
  10.230 +by (simp add: stable_def constrains_def JOIN_def)
  10.231 +
  10.232 +lemma invariant_JN_I:
  10.233 +     "[| !!i. i:I ==> F i : invariant A;  i : I |]   
  10.234 +       ==> (JN i:I. F i) : invariant A"
  10.235 +by (simp add: invariant_def JN_stable, blast)
  10.236 +
  10.237 +lemma Join_stable [simp]:
  10.238 +     "(F Join G : stable A) =  
  10.239 +      (F : stable A & G : stable A)"
  10.240 +by (simp add: stable_def)
  10.241 +
  10.242 +lemma Join_increasing [simp]:
  10.243 +     "(F Join G : increasing f) =  
  10.244 +      (F : increasing f & G : increasing f)"
  10.245 +by (simp add: increasing_def Join_stable, blast)
  10.246 +
  10.247 +lemma invariant_JoinI:
  10.248 +     "[| F : invariant A; G : invariant A |]   
  10.249 +      ==> F Join G : invariant A"
  10.250 +by (simp add: invariant_def, blast)
  10.251 +
  10.252 +lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
  10.253 +by (simp add: FP_def JN_stable INTER_def)
  10.254 +
  10.255 +
  10.256 +(*** Progress: transient, ensures ***)
  10.257 +
  10.258 +lemma JN_transient:
  10.259 +     "i : I ==>  
  10.260 +    (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
  10.261 +by (auto simp add: transient_def JOIN_def)
  10.262 +
  10.263 +lemma Join_transient [simp]:
  10.264 +     "F Join G : transient A =  
  10.265 +      (F : transient A | G : transient A)"
  10.266 +by (auto simp add: bex_Un transient_def Join_def)
  10.267 +
  10.268 +lemma Join_transient_I1: "F : transient A ==> F Join G : transient A"
  10.269 +by (simp add: Join_transient)
  10.270 +
  10.271 +lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
  10.272 +by (simp add: Join_transient)
  10.273 +
  10.274 +(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
  10.275 +lemma JN_ensures:
  10.276 +     "i : I ==>  
  10.277 +      (JN i:I. F i) : A ensures B =  
  10.278 +      ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
  10.279 +by (auto simp add: ensures_def JN_constrains JN_transient)
  10.280 +
  10.281 +lemma Join_ensures: 
  10.282 +     "F Join G : A ensures B =      
  10.283 +      (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &  
  10.284 +       (F : transient (A-B) | G : transient (A-B)))"
  10.285 +by (auto simp add: ensures_def Join_transient)
  10.286 +
  10.287 +lemma stable_Join_constrains: 
  10.288 +    "[| F : stable A;  G : A co A' |]  
  10.289 +     ==> F Join G : A co A'"
  10.290 +apply (unfold stable_def constrains_def Join_def)
  10.291 +apply (simp add: ball_Un, blast)
  10.292 +done
  10.293 +
  10.294 +(*Premise for G cannot use Always because  F: Stable A  is weaker than
  10.295 +  G : stable A *)
  10.296 +lemma stable_Join_Always1:
  10.297 +     "[| F : stable A;  G : invariant A |] ==> F Join G : Always A"
  10.298 +apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
  10.299 +apply (force intro: stable_Int)
  10.300 +done
  10.301 +
  10.302 +(*As above, but exchanging the roles of F and G*)
  10.303 +lemma stable_Join_Always2:
  10.304 +     "[| F : invariant A;  G : stable A |] ==> F Join G : Always A"
  10.305 +apply (subst Join_commute)
  10.306 +apply (blast intro: stable_Join_Always1)
  10.307 +done
  10.308 +
  10.309 +lemma stable_Join_ensures1:
  10.310 +     "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B"
  10.311 +apply (simp (no_asm_simp) add: Join_ensures)
  10.312 +apply (simp add: stable_def ensures_def)
  10.313 +apply (erule constrains_weaken, auto)
  10.314 +done
  10.315 +
  10.316 +(*As above, but exchanging the roles of F and G*)
  10.317 +lemma stable_Join_ensures2:
  10.318 +     "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B"
  10.319 +apply (subst Join_commute)
  10.320 +apply (blast intro: stable_Join_ensures1)
  10.321 +done
  10.322 +
  10.323 +
  10.324 +(*** the ok and OK relations ***)
  10.325 +
  10.326 +lemma ok_SKIP1 [iff]: "SKIP ok F"
  10.327 +by (auto simp add: ok_def)
  10.328 +
  10.329 +lemma ok_SKIP2 [iff]: "F ok SKIP"
  10.330 +by (auto simp add: ok_def)
  10.331 +
  10.332 +lemma ok_Join_commute:
  10.333 +     "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
  10.334 +by (auto simp add: ok_def)
  10.335 +
  10.336 +lemma ok_commute: "(F ok G) = (G ok F)"
  10.337 +by (auto simp add: ok_def)
  10.338 +
  10.339 +lemmas ok_sym = ok_commute [THEN iffD1, standard]
  10.340 +
  10.341 +lemma ok_iff_OK:
  10.342 +     "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
  10.343 +by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast)
  10.344 +
  10.345 +lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
  10.346 +by (auto simp add: ok_def)
  10.347 +
  10.348 +lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)"
  10.349 +by (auto simp add: ok_def)
  10.350 +
  10.351 +(*useful?  Not with the previous two around*)
  10.352 +lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
  10.353 +by (auto simp add: ok_def)
  10.354 +
  10.355 +lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
  10.356 +by (auto simp add: ok_def)
  10.357 +
  10.358 +lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (ALL i:I. G i ok F)"
  10.359 +by (auto simp add: ok_def)
  10.360 +
  10.361 +lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
  10.362 +by (auto simp add: ok_def OK_def)
  10.363 +
  10.364 +lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
  10.365 +by (auto simp add: OK_iff_ok)
  10.366 +
  10.367 +
  10.368 +(*** Allowed ***)
  10.369 +
  10.370 +lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
  10.371 +by (auto simp add: Allowed_def)
  10.372 +
  10.373 +lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
  10.374 +by (auto simp add: Allowed_def)
  10.375 +
  10.376 +lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
  10.377 +by (auto simp add: Allowed_def)
  10.378 +
  10.379 +lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
  10.380 +by (simp add: ok_def Allowed_def)
  10.381 +
  10.382 +lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
  10.383 +by (auto simp add: OK_iff_ok ok_iff_Allowed)
  10.384 +
  10.385 +(*** safety_prop, for reasoning about given instances of "ok" ***)
  10.386 +
  10.387 +lemma safety_prop_Acts_iff:
  10.388 +     "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
  10.389 +by (auto simp add: safety_prop_def)
  10.390 +
  10.391 +lemma safety_prop_AllowedActs_iff_Allowed:
  10.392 +     "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
  10.393 +by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
  10.394 +
  10.395 +lemma Allowed_eq:
  10.396 +     "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
  10.397 +by (simp add: Allowed_def safety_prop_Acts_iff)
  10.398 +
  10.399 +lemma def_prg_Allowed:
  10.400 +     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
  10.401 +      ==> Allowed F = X"
  10.402 +by (simp add: Allowed_eq)
  10.403 +
  10.404 +(*For safety_prop to hold, the property must be satisfiable!*)
  10.405 +lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
  10.406 +by (simp add: safety_prop_def constrains_def, blast)
  10.407 +
  10.408 +lemma safety_prop_stable [iff]: "safety_prop (stable A)"
  10.409 +by (simp add: stable_def)
  10.410 +
  10.411 +lemma safety_prop_Int [simp]:
  10.412 +     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
  10.413 +by (simp add: safety_prop_def, blast)
  10.414 +
  10.415 +lemma safety_prop_INTER1 [simp]:
  10.416 +     "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
  10.417 +by (auto simp add: safety_prop_def, blast)
  10.418 +							       
  10.419 +lemma safety_prop_INTER [simp]:
  10.420 +     "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
  10.421 +by (auto simp add: safety_prop_def, blast)
  10.422 +
  10.423 +lemma def_UNION_ok_iff:
  10.424 +     "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
  10.425 +      ==> F ok G = (G : X & acts <= AllowedActs G)"
  10.426 +by (auto simp add: ok_def safety_prop_Acts_iff)
  10.427  
  10.428  end