Conversion of theory UNITY to Isar script
authorpaulson
Fri Jun 27 18:40:25 2003 +0200 (2003-06-27)
changeset 1407737c964462747
parent 14076 5cfc8b9fb880
child 14078 cddad2aa025b
Conversion of theory UNITY to Isar script
src/ZF/IsaMakefile
src/ZF/UNITY/Comp.ML
src/ZF/UNITY/Distributor.thy
src/ZF/UNITY/Follows.ML
src/ZF/UNITY/Increasing.ML
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/UNITY.ML
src/ZF/UNITY/UNITY.thy
src/ZF/UNITY/Union.ML
src/ZF/UNITY/WFair.thy
src/ZF/equalities.thy
     1.1 --- a/src/ZF/IsaMakefile	Fri Jun 27 13:15:40 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Fri Jun 27 18:40:25 2003 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4    UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
     1.5    UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
     1.6    UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
     1.7 -  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     1.8 +  UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy \
     1.9    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
    1.10    UNITY/AllocBase.thy UNITY/AllocImpl.thy\
    1.11    UNITY/ClientImpl.thy UNITY/Distributor.thy\
     2.1 --- a/src/ZF/UNITY/Comp.ML	Fri Jun 27 13:15:40 2003 +0200
     2.2 +++ b/src/ZF/UNITY/Comp.ML	Fri Jun 27 18:40:25 2003 +0200
     2.3 @@ -169,11 +169,11 @@
     2.4  AddIffs [preserves_fun_pair_iff];
     2.5  
     2.6  Goal "(fun_pair(f, g) comp h)(x) = fun_pair(f comp h, g comp h, x)";
     2.7 -by (simp_tac (simpset() addsimps [fun_pair_def, comp_def]) 1);
     2.8 +by (simp_tac (simpset() addsimps [fun_pair_def, metacomp_def]) 1);
     2.9  qed "fun_pair_comp_distrib";
    2.10  
    2.11  Goal "(f comp g)(x) = f(g(x))";
    2.12 -by (simp_tac (simpset() addsimps [comp_def]) 1);
    2.13 +by (simp_tac (simpset() addsimps [metacomp_def]) 1);
    2.14  qed "comp_apply";
    2.15  Addsimps [comp_apply];
    2.16  
     3.1 --- a/src/ZF/UNITY/Distributor.thy	Fri Jun 27 13:15:40 2003 +0200
     3.2 +++ b/src/ZF/UNITY/Distributor.thy	Fri Jun 27 18:40:25 2003 +0200
     3.3 @@ -158,8 +158,9 @@
     3.4  apply (auto simp add: distr_spec_def distr_follows_def)
     3.5  apply (drule guaranteesD, assumption)
     3.6  apply (simp_all cong add: Follows_cong
     3.7 -    add: refl_prefix
     3.8 -       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
     3.9 +		add: refl_prefix
    3.10 +		   mono_bag_of [THEN subset_Follows_comp, THEN subsetD, 
    3.11 +				unfolded metacomp_def])
    3.12  done
    3.13  
    3.14  end
     4.1 --- a/src/ZF/UNITY/Follows.ML	Fri Jun 27 13:15:40 2003 +0200
     4.2 +++ b/src/ZF/UNITY/Follows.ML	Fri Jun 27 18:40:25 2003 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
     4.5  qed "Follows_cong";
     4.6  
     4.7 -Goalw [mono1_def, comp_def] 
     4.8 +Goalw [mono1_def, metacomp_def] 
     4.9  "[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
    4.10  \  Always({x:state. <f(x), g(x)>:r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
    4.11  by (auto_tac (claset(), simpset() addsimps 
    4.12 @@ -40,7 +40,7 @@
    4.13  
    4.14  (* comp LeadsTo *)
    4.15  
    4.16 -Goalw [mono1_def, comp_def]
    4.17 +Goalw [mono1_def, metacomp_def]
    4.18  "[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
    4.19  \       ALL x:state. f(x):A & g(x):A |] ==> \
    4.20  \ (INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}) <= \
     5.1 --- a/src/ZF/UNITY/Increasing.ML	Fri Jun 27 13:15:40 2003 +0200
     5.2 +++ b/src/ZF/UNITY/Increasing.ML	Fri Jun 27 18:40:25 2003 +0200
     5.3 @@ -37,7 +37,7 @@
     5.4  Addsimps [increasing_constant];
     5.5  
     5.6  Goalw [increasing_def, stable_def, part_order_def, 
     5.7 -       constrains_def, mono1_def, comp_def]
     5.8 +       constrains_def, mono1_def, metacomp_def]
     5.9  "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==> \
    5.10  \  increasing[A](r, f) <= increasing[B](s, g comp f)";
    5.11  by (Clarify_tac 1);
    5.12 @@ -113,7 +113,7 @@
    5.13  Addsimps [Increasing_constant];
    5.14  
    5.15  Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def, 
    5.16 -       constrains_def, mono1_def, comp_def]
    5.17 +       constrains_def, mono1_def, metacomp_def]
    5.18  "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
    5.19  \  Increasing[A](r, f) <= Increasing[B](s, g comp f)";
    5.20  by Safe_tac;
     6.1 --- a/src/ZF/UNITY/Merge.thy	Fri Jun 27 13:15:40 2003 +0200
     6.2 +++ b/src/ZF/UNITY/Merge.thy	Fri Jun 27 18:40:25 2003 +0200
     6.3 @@ -183,8 +183,9 @@
     6.4  apply (drule guaranteesD, assumption)
     6.5    apply (simp add: merge_spec_def merge_follows_def, blast)
     6.6  apply (simp cong add: Follows_cong
     6.7 -    add: refl_prefix
     6.8 -       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
     6.9 +	    add: refl_prefix
    6.10 +	       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, 
    6.11 +			    unfolded metacomp_def])
    6.12  done
    6.13  
    6.14  end
     7.1 --- a/src/ZF/UNITY/UNITY.ML	Fri Jun 27 13:15:40 2003 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,707 +0,0 @@
     7.4 -(*  Title:      ZF/UNITY/UNITY.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     7.7 -    Copyright   2001  University of Cambridge
     7.8 -
     7.9 -The basic UNITY theory (revised version, based upon the "co" operator)
    7.10 -From Misra, "A Logic for Concurrent Programming", 1994
    7.11 -
    7.12 -Proofs ported from HOL
    7.13 -*)
    7.14 -
    7.15 -(** SKIP **)
    7.16 -Goalw [SKIP_def]  "SKIP:program";
    7.17 -by (rewrite_goal_tac [program_def, mk_program_def] 1);
    7.18 -by Auto_tac;
    7.19 -qed "SKIP_in_program";
    7.20 -AddIffs [SKIP_in_program];
    7.21 -AddTCs  [SKIP_in_program];
    7.22 -
    7.23 -(** programify: coersion from anything to program **)
    7.24 -
    7.25 -Goalw [programify_def]
    7.26 -"F:program ==> programify(F)=F";
    7.27 -by Auto_tac;
    7.28 -qed "programify_program";
    7.29 -Addsimps [programify_program];
    7.30 -
    7.31 -Goalw [programify_def]
    7.32 -"programify(F):program";
    7.33 -by Auto_tac;
    7.34 -qed "programify_in_program";
    7.35 -AddIffs [programify_in_program];
    7.36 -AddTCs  [programify_in_program];
    7.37 -
    7.38 -(** Collapsing rules: to remove programify from expressions **)
    7.39 -Goalw [programify_def]
    7.40 -"programify(programify(F))=programify(F)";
    7.41 -by Auto_tac;
    7.42 -qed "programify_idem";
    7.43 -AddIffs [programify_idem];
    7.44 -
    7.45 -Goal
    7.46 -"Init(programify(F)) = Init(F)";
    7.47 -by (simp_tac (simpset() addsimps [Init_def]) 1);
    7.48 -qed "Init_programify";
    7.49 -AddIffs [Init_programify];
    7.50 -
    7.51 -Goal
    7.52 -"Acts(programify(F)) = Acts(F)";
    7.53 -by (simp_tac (simpset() addsimps [Acts_def]) 1);
    7.54 -qed "Acts_programify";
    7.55 -AddIffs [Acts_programify];
    7.56 -
    7.57 -Goal
    7.58 -"AllowedActs(programify(F)) = AllowedActs(F)";
    7.59 -by (simp_tac (simpset() addsimps [AllowedActs_def]) 1);
    7.60 -qed "AllowedActs_programify";
    7.61 -AddIffs [AllowedActs_programify];
    7.62 -
    7.63 -(** program's inspectors **)
    7.64 -
    7.65 -Goal  "F:program ==>id(state):RawActs(F)";
    7.66 -by (auto_tac (claset(), simpset() 
    7.67 -        addsimps [program_def, RawActs_def]));
    7.68 -qed "id_in_RawActs";
    7.69 -
    7.70 -Goal "id(state):Acts(F)";
    7.71 -by (simp_tac (simpset() 
    7.72 -      addsimps [id_in_RawActs, Acts_def]) 1);
    7.73 -qed "id_in_Acts";
    7.74 -
    7.75 -Goal  "F:program ==>id(state):RawAllowedActs(F)";
    7.76 -by (auto_tac (claset(), simpset() 
    7.77 -         addsimps [program_def, RawAllowedActs_def]));
    7.78 -qed "id_in_RawAllowedActs";
    7.79 -
    7.80 -Goal   "id(state):AllowedActs(F)";
    7.81 -by (simp_tac (simpset() 
    7.82 -     addsimps [id_in_RawAllowedActs, AllowedActs_def]) 1);
    7.83 -qed "id_in_AllowedActs";
    7.84 -
    7.85 -AddIffs [id_in_Acts, id_in_AllowedActs];
    7.86 -AddTCs [id_in_Acts, id_in_AllowedActs];
    7.87 -
    7.88 -Goal "cons(id(state), Acts(F)) = Acts(F)";
    7.89 -by (simp_tac (simpset() addsimps [cons_absorb]) 1);
    7.90 -qed "cons_id_Acts";
    7.91 -
    7.92 -Goal "cons(id(state), AllowedActs(F)) = AllowedActs(F)";
    7.93 -by (simp_tac (simpset() addsimps [cons_absorb]) 1);
    7.94 -qed "cons_id_AllowedActs";
    7.95 -
    7.96 -AddIffs [cons_id_Acts, cons_id_AllowedActs];
    7.97 -
    7.98 -(** inspectors's types **)
    7.99 -Goal
   7.100 -"F:program ==> RawInit(F)<=state";
   7.101 -by (auto_tac (claset(), simpset() 
   7.102 -        addsimps [program_def, RawInit_def]));
   7.103 -qed "RawInit_type";
   7.104 -
   7.105 -Goal
   7.106 -"F:program ==> RawActs(F)<=Pow(state*state)";
   7.107 -by (auto_tac (claset(), simpset() 
   7.108 -       addsimps [program_def, RawActs_def]));
   7.109 -qed "RawActs_type";
   7.110 -
   7.111 -Goal
   7.112 -"F:program ==> RawAllowedActs(F)<=Pow(state*state)";
   7.113 -by (auto_tac (claset(), simpset() 
   7.114 -         addsimps [program_def, RawAllowedActs_def]));
   7.115 -qed "RawAllowedActs_type";
   7.116 -
   7.117 -Goal "Init(F)<=state";
   7.118 -by (simp_tac (simpset() 
   7.119 -    addsimps [RawInit_type, Init_def]) 1);
   7.120 -qed "Init_type";
   7.121 -
   7.122 -bind_thm("InitD", Init_type RS subsetD);
   7.123 -
   7.124 -Goalw [st_set_def] "st_set(Init(F))";
   7.125 -by (rtac Init_type 1);
   7.126 -qed "st_set_Init";
   7.127 -AddIffs [st_set_Init];
   7.128 -
   7.129 -Goal
   7.130 -"Acts(F)<=Pow(state*state)";
   7.131 -by (simp_tac (simpset() 
   7.132 -    addsimps [RawActs_type, Acts_def]) 1);
   7.133 -qed "Acts_type";
   7.134 -
   7.135 -Goal
   7.136 -"AllowedActs(F)<=Pow(state*state)";
   7.137 -by (simp_tac (simpset() 
   7.138 -     addsimps [RawAllowedActs_type, AllowedActs_def]) 1);
   7.139 -qed "AllowedActs_type";
   7.140 -
   7.141 -(* Needed in Behaviors *)
   7.142 -Goal "[| act:Acts(F); <s,s'>:act |] ==> s:state & s':state";
   7.143 -by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
   7.144 -qed "ActsD";
   7.145 -
   7.146 -Goal "[| act:AllowedActs(F); <s,s'>:act |] ==> s:state & s':state";
   7.147 -by (blast_tac (claset() addDs [AllowedActs_type RS subsetD]) 1);
   7.148 -qed "AllowedActsD";
   7.149 -
   7.150 -(** More simplification rules involving state 
   7.151 -    and Init, Acts, and AllowedActs **)
   7.152 -
   7.153 -Goal "state <= Init(F) <-> Init(F)=state";
   7.154 -by (cut_inst_tac [("F", "F")] Init_type 1);
   7.155 -by Auto_tac;
   7.156 -qed "state_subset_is_Init_iff";
   7.157 -AddIffs [state_subset_is_Init_iff];
   7.158 -
   7.159 -Goal "Pow(state*state) <= Acts(F) <-> Acts(F)=Pow(state*state)";
   7.160 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.161 -by Auto_tac;
   7.162 -qed "Pow_state_times_state_is_subset_Acts_iff";
   7.163 -AddIffs [Pow_state_times_state_is_subset_Acts_iff];
   7.164 -
   7.165 -Goal "Pow(state*state) <= AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)";
   7.166 -by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
   7.167 -by Auto_tac;
   7.168 -qed "Pow_state_times_state_is_subset_AllowedActs_iff";
   7.169 -AddIffs [Pow_state_times_state_is_subset_AllowedActs_iff];
   7.170 -
   7.171 -(** Eliminating `Int state' from expressions  **)
   7.172 -Goal "Init(F) Int state = Init(F)";
   7.173 -by (cut_inst_tac [("F", "F")] Init_type 1);
   7.174 -by (Blast_tac 1);
   7.175 -qed "Init_Int_state";
   7.176 -AddIffs [Init_Int_state];
   7.177 -
   7.178 -Goal "state Int Init(F) = Init(F)";
   7.179 -by (cut_inst_tac [("F", "F")] Init_type 1);
   7.180 -by (Blast_tac 1);
   7.181 -qed "state_Int_Init";
   7.182 -AddIffs [state_Int_Init];
   7.183 -
   7.184 -Goal "Acts(F) Int Pow(state*state) = Acts(F)";
   7.185 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.186 -by (Blast_tac 1);
   7.187 -qed "Acts_Int_Pow_state_times_state";
   7.188 -AddIffs [Acts_Int_Pow_state_times_state];
   7.189 -
   7.190 -Goal "Pow(state*state) Int Acts(F) = Acts(F)";
   7.191 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.192 -by (Blast_tac 1);
   7.193 -qed "state_times_state_Int_Acts";
   7.194 -AddIffs [state_times_state_Int_Acts];
   7.195 -
   7.196 -Goal "AllowedActs(F) Int Pow(state*state) = AllowedActs(F)";
   7.197 -by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
   7.198 -by (Blast_tac 1);
   7.199 -qed "AllowedActs_Int_Pow_state_times_state";
   7.200 -AddIffs [AllowedActs_Int_Pow_state_times_state];
   7.201 -
   7.202 -Goal "Pow(state*state) Int AllowedActs(F) = AllowedActs(F)";
   7.203 -by (cut_inst_tac [("F", "F")] AllowedActs_type 1);
   7.204 -by (Blast_tac 1);
   7.205 -qed "state_times_state_Int_AllowedActs";
   7.206 -AddIffs [state_times_state_Int_AllowedActs];
   7.207 -
   7.208 -(** mk_program **)
   7.209 -
   7.210 -Goalw [mk_program_def, program_def] "mk_program(init, acts, allowed):program";
   7.211 -by Auto_tac;
   7.212 -qed "mk_program_in_program";
   7.213 -AddIffs [mk_program_in_program];
   7.214 -AddTCs [mk_program_in_program];
   7.215 -
   7.216 -Goalw [RawInit_def, mk_program_def]
   7.217 -  "RawInit(mk_program(init, acts, allowed)) = init Int state";
   7.218 -by Auto_tac;
   7.219 -qed "RawInit_eq";
   7.220 -AddIffs [RawInit_eq];
   7.221 -
   7.222 -Goalw [RawActs_def, mk_program_def] 
   7.223 -"RawActs(mk_program(init, acts, allowed)) = cons(id(state), acts Int Pow(state*state))";
   7.224 -by Auto_tac;
   7.225 -qed "RawActs_eq";
   7.226 -AddIffs [RawActs_eq];
   7.227 -
   7.228 -Goalw [RawAllowedActs_def, mk_program_def]
   7.229 -"RawAllowedActs(mk_program(init, acts, allowed)) = \
   7.230 -\ cons(id(state), allowed Int Pow(state*state))";
   7.231 -by Auto_tac;
   7.232 -qed "RawAllowedActs_eq";
   7.233 -AddIffs [RawAllowedActs_eq];
   7.234 -
   7.235 -Goalw [Init_def]  "Init(mk_program(init, acts, allowed)) = init Int state";
   7.236 -by (Simp_tac 1);
   7.237 -qed "Init_eq";
   7.238 -AddIffs [Init_eq];
   7.239 -
   7.240 -Goalw [Acts_def] 
   7.241 -"Acts(mk_program(init, acts, allowed)) = cons(id(state), acts  Int Pow(state*state))";
   7.242 -by (Simp_tac 1);
   7.243 -qed "Acts_eq";
   7.244 -AddIffs [Acts_eq];
   7.245 -
   7.246 -Goalw [AllowedActs_def]
   7.247 -"AllowedActs(mk_program(init, acts, allowed))= \
   7.248 -\ cons(id(state), allowed Int Pow(state*state))";
   7.249 -by (Simp_tac 1);
   7.250 -qed "AllowedActs_eq";
   7.251 -AddIffs [AllowedActs_eq];
   7.252 -
   7.253 -(**Init, Acts, and AlowedActs  of SKIP **)
   7.254 -
   7.255 -Goalw [SKIP_def] "RawInit(SKIP) = state";
   7.256 -by Auto_tac;
   7.257 -qed "RawInit_SKIP";
   7.258 -AddIffs [RawInit_SKIP];
   7.259 -
   7.260 -Goalw [SKIP_def] "RawAllowedActs(SKIP) = Pow(state*state)";
   7.261 -by Auto_tac;
   7.262 -qed "RawAllowedActs_SKIP";
   7.263 -AddIffs [RawAllowedActs_SKIP];
   7.264 -
   7.265 -Goalw [SKIP_def] "RawActs(SKIP) = {id(state)}";
   7.266 -by Auto_tac;
   7.267 -qed "RawActs_SKIP";
   7.268 -AddIffs [RawActs_SKIP];
   7.269 -
   7.270 -Goalw [Init_def] "Init(SKIP) = state";
   7.271 -by Auto_tac;
   7.272 -qed "Init_SKIP";
   7.273 -AddIffs [Init_SKIP];
   7.274 -
   7.275 -Goalw [Acts_def] "Acts(SKIP) = {id(state)}";
   7.276 -by Auto_tac;
   7.277 -qed "Acts_SKIP";
   7.278 -AddIffs [Acts_SKIP];
   7.279 -
   7.280 -Goalw [AllowedActs_def] "AllowedActs(SKIP) = Pow(state*state)";
   7.281 -by Auto_tac;
   7.282 -qed "AllowedActs_SKIP";
   7.283 -AddIffs [AllowedActs_SKIP];
   7.284 -
   7.285 -(** Equality of UNITY programs **)
   7.286 -
   7.287 -Goal 
   7.288 -"F:program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F";
   7.289 -by (rewrite_goal_tac [program_def, mk_program_def,RawInit_def,
   7.290 -                      RawActs_def, RawAllowedActs_def] 1);
   7.291 -by Auto_tac;
   7.292 -by (REPEAT(Blast_tac 1));
   7.293 -qed "raw_surjective_mk_program";
   7.294 -Addsimps [raw_surjective_mk_program];
   7.295 -
   7.296 -Goalw [Init_def, Acts_def, AllowedActs_def]
   7.297 -  "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)";
   7.298 -by Auto_tac;
   7.299 -qed "surjective_mk_program";
   7.300 -AddIffs [surjective_mk_program];
   7.301 -
   7.302 -Goal "[|Init(F) = Init(G); Acts(F) = Acts(G); \
   7.303 -\ AllowedActs(F) = AllowedActs(G); F:program; G:program |] ==> F = G";
   7.304 -by (stac (programify_program RS sym) 1);
   7.305 -by (rtac sym 2);
   7.306 -by (stac  (programify_program RS sym) 2);
   7.307 -by (stac (surjective_mk_program RS sym) 3);
   7.308 -by (stac (surjective_mk_program RS sym) 3);
   7.309 -by (ALLGOALS(Asm_simp_tac));
   7.310 -qed "program_equalityI";
   7.311 -
   7.312 -val [major,minor] =
   7.313 -Goal "[| F = G; \
   7.314 -\        [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]\
   7.315 -\        ==> P |] ==> P";
   7.316 -by (rtac minor 1);
   7.317 -by (auto_tac (claset(), simpset() addsimps [major]));
   7.318 -qed "program_equalityE";
   7.319 -
   7.320 -
   7.321 -Goal "[| F:program; G:program |] ==>(F=G)  <->  \
   7.322 -\     (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))";
   7.323 -by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
   7.324 -qed "program_equality_iff";
   7.325 -
   7.326 -(*** These rules allow "lazy" definition expansion 
   7.327 -
   7.328 -...skipping 1 line
   7.329 -
   7.330 -***)
   7.331 -
   7.332 -Goal "F == mk_program (init,acts,allowed) ==> Init(F) = init Int state";
   7.333 -by Auto_tac;
   7.334 -qed "def_prg_Init";
   7.335 -
   7.336 -
   7.337 -Goal "F == mk_program (init,acts,allowed) ==> \
   7.338 -\ Acts(F) = cons(id(state), acts Int Pow(state*state))";
   7.339 -by Auto_tac;
   7.340 -qed "def_prg_Acts";
   7.341 -
   7.342 -
   7.343 -Goal "F == mk_program (init,acts,allowed) ==> \
   7.344 -\    AllowedActs(F) = cons(id(state), allowed Int Pow(state*state))";
   7.345 -by Auto_tac;
   7.346 -qed "def_prg_AllowedActs";
   7.347 -
   7.348 -
   7.349 -val [rew] = goal thy
   7.350 -    "[| F == mk_program (init,acts,allowed) |] \
   7.351 -\ ==> Init(F) = init Int state & Acts(F) = cons(id(state), acts Int Pow(state*state)) & \
   7.352 -\     AllowedActs(F) = cons(id(state), allowed Int Pow(state*state)) ";
   7.353 -by (rewtac rew);
   7.354 -by Auto_tac;
   7.355 -qed "def_prg_simps";
   7.356 -
   7.357 -
   7.358 -(*An action is expanded only if a pair of states is being tested against it*)
   7.359 -Goal "[| act == {<s,s'>:A*B. P(s, s')} |] ==> \
   7.360 -\ (<s,s'>:act) <-> (<s,s'>:A*B & P(s, s'))";
   7.361 -by Auto_tac;
   7.362 -qed "def_act_simp";
   7.363 -
   7.364 -fun simp_of_act def = def RS def_act_simp;
   7.365 -
   7.366 -(*A set is expanded only if an element is being tested against it*)
   7.367 -Goal "A == B ==> (x : A) <-> (x : B)";
   7.368 -by Auto_tac;
   7.369 -qed "def_set_simp";
   7.370 -
   7.371 -fun simp_of_set def = def RS def_set_simp;
   7.372 -
   7.373 -(*** co ***)
   7.374 -
   7.375 -Goalw [constrains_def]
   7.376 -"A co B <= program";
   7.377 -by Auto_tac;
   7.378 -qed "constrains_type";
   7.379 -
   7.380 -
   7.381 -val prems = Goalw [constrains_def]
   7.382 -    "[|(!!act s s'. [| act: Acts(F);  <s,s'>:act; s:A|] ==> s':A'); \
   7.383 -    \   F:program; st_set(A) |]  ==> F:A co A'";
   7.384 -by (auto_tac (claset() delrules [subsetI], simpset()));
   7.385 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems)));
   7.386 -by (Clarify_tac 1);
   7.387 -by (blast_tac(claset() addIs prems) 1);
   7.388 -qed "constrainsI";
   7.389 -
   7.390 -Goalw [constrains_def]
   7.391 -   "F:A co B ==> ALL act:Acts(F). act``A<=B";
   7.392 -by (Blast_tac 1);
   7.393 -qed "constrainsD";
   7.394 -
   7.395 -Goalw [constrains_def]
   7.396 -   "F:A co B ==> F:program & st_set(A)";
   7.397 -by (Blast_tac 1);
   7.398 -qed "constrainsD2"; 
   7.399 -
   7.400 -Goalw [constrains_def, st_set_def] "F : 0 co B <-> F:program";
   7.401 -by (Blast_tac 1);
   7.402 -qed "constrains_empty";
   7.403 -
   7.404 -Goalw [constrains_def, st_set_def]
   7.405 -    "(F : A co 0) <-> (A=0 & F:program)";
   7.406 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.407 -by Auto_tac;
   7.408 -by (Blast_tac 1);
   7.409 -qed "constrains_empty2";
   7.410 -
   7.411 -Goalw [constrains_def, st_set_def]
   7.412 -"(F: state co B) <-> (state<=B & F:program)";
   7.413 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.414 -by (Blast_tac 1);
   7.415 -qed "constrains_state";
   7.416 -
   7.417 -Goalw [constrains_def, st_set_def] "F:A co state <-> (F:program & st_set(A))";
   7.418 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.419 -by (Blast_tac 1);
   7.420 -qed "constrains_state2";
   7.421 -
   7.422 -AddIffs [constrains_empty, constrains_empty2, 
   7.423 -         constrains_state, constrains_state2];
   7.424 -
   7.425 -(*monotonic in 2nd argument*)
   7.426 -Goalw [constrains_def]
   7.427 -    "[| F:A co A'; A'<=B' |] ==> F : A co B'";
   7.428 -by (Blast_tac 1);
   7.429 -qed "constrains_weaken_R";
   7.430 -
   7.431 -(*anti-monotonic in 1st argument*)
   7.432 -Goalw [constrains_def, st_set_def]
   7.433 -    "[| F : A co A'; B<=A |] ==> F : B co A'";
   7.434 -by (Blast_tac 1);
   7.435 -qed "constrains_weaken_L";
   7.436 -
   7.437 -Goal
   7.438 -   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'";
   7.439 -by (dtac constrains_weaken_R 1);
   7.440 -by (dtac constrains_weaken_L 2);
   7.441 -by (REPEAT(Blast_tac 1));
   7.442 -qed "constrains_weaken";
   7.443 -
   7.444 -(** Union **)
   7.445 -
   7.446 -Goalw [constrains_def, st_set_def]
   7.447 -    "[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')";
   7.448 -by Auto_tac;
   7.449 -by (Force_tac 1);
   7.450 -qed "constrains_Un";
   7.451 -
   7.452 -val major::minor::_ = Goalw [constrains_def, st_set_def]
   7.453 -"[|(!!i. i:I ==> F:A(i) co A'(i)); F:program |]==> F:(UN i:I. A(i)) co (UN i:I. A'(i))";
   7.454 -by (cut_facts_tac [minor] 1);
   7.455 -by Safe_tac;
   7.456 -by (ALLGOALS(ftac major ));
   7.457 -by (ALLGOALS(Asm_full_simp_tac));
   7.458 -by (REPEAT(Blast_tac 1));
   7.459 -qed "constrains_UN";
   7.460 -
   7.461 -Goalw [constrains_def, st_set_def]
   7.462 -     "(A Un B) co C = (A co C) Int (B co C)";
   7.463 -by Auto_tac;
   7.464 -by (Force_tac 1);
   7.465 -qed "constrains_Un_distrib";
   7.466 -
   7.467 -Goalw [constrains_def, st_set_def]
   7.468 -   "i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)";
   7.469 -by (rtac equalityI 1);
   7.470 -by (REPEAT(Force_tac 1));
   7.471 -qed "constrains_UN_distrib";
   7.472 -
   7.473 -(** Intersection **)
   7.474 -Goalw [constrains_def, st_set_def]
   7.475 - "C co (A Int B) = (C co A) Int (C co B)";
   7.476 -by (rtac equalityI 1);
   7.477 -by (ALLGOALS(Clarify_tac)); (* to speed up the proof *)
   7.478 -by (REPEAT(Blast_tac 1));
   7.479 -qed "constrains_Int_distrib";
   7.480 -
   7.481 -Goalw [constrains_def, st_set_def] 
   7.482 -"x:I ==> A co (INT i:I. B(i)) = (INT i:I. A co B(i))";
   7.483 -by (rtac equalityI 1);
   7.484 -by Safe_tac;
   7.485 -by (REPEAT(Blast_tac 1));
   7.486 -qed "constrains_INT_distrib";
   7.487 -
   7.488 -Goalw [constrains_def, st_set_def]
   7.489 -    "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')";
   7.490 -by (Clarify_tac 1);
   7.491 -by (Blast_tac 1);
   7.492 -qed "constrains_Int";
   7.493 -
   7.494 -val major::minor::_ = Goalw [constrains_def, st_set_def]
   7.495 -"[| (!!i. i:I==>F:A(i) co A'(i)); F:program|]==> F:(INT i:I. A(i)) co (INT i:I. A'(i))";
   7.496 -by (cut_facts_tac [minor] 1);
   7.497 -by (cut_inst_tac [("F", "F")] Acts_type 1);
   7.498 -by (case_tac "I=0" 1);
   7.499 -by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
   7.500 -by (etac not_emptyE 1);
   7.501 -by Safe_tac;
   7.502 -by (forw_inst_tac [("i", "xd")] major 1);
   7.503 -by (ftac major 2);
   7.504 -by (ftac major 3);
   7.505 -by (REPEAT(Force_tac 1));
   7.506 -qed "constrains_INT";
   7.507 -
   7.508 -(* The rule below simulates the HOL's one for (INT z. A i) co (INT z. B i) *)
   7.509 -Goalw [constrains_def]
   7.510 -"[| ALL z. F:{s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |]==>\
   7.511 -\   F:{s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}";
   7.512 -by (Blast_tac 1);
   7.513 -qed "constrains_All";
   7.514 -
   7.515 -Goalw [constrains_def, st_set_def] 
   7.516 -  "[| F:A co A' |] ==> A <= A'";
   7.517 -by (Force_tac 1); 
   7.518 -qed "constrains_imp_subset";
   7.519 -
   7.520 -(*The reasoning is by subsets since "co" refers to single actions
   7.521 -  only.  So this rule isn't that useful.*)
   7.522 -
   7.523 -Goalw [constrains_def, st_set_def]
   7.524 -    "[| F : A co B; F : B co C |] ==> F : A co C";
   7.525 -by Auto_tac;
   7.526 -by (Blast_tac 1);
   7.527 -qed "constrains_trans";
   7.528 -
   7.529 -Goal
   7.530 -"[| F : A co (A' Un B); F : B co B' |] ==> F:A co (A' Un B')";
   7.531 -by (dres_inst_tac [("A", "B")] constrains_imp_subset 1);
   7.532 -by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
   7.533 -qed "constrains_cancel";
   7.534 -
   7.535 -(*** unless ***)
   7.536 -
   7.537 -Goalw [unless_def, constrains_def] 
   7.538 -     "A unless B <= program";
   7.539 -by Auto_tac;
   7.540 -qed "unless_type";
   7.541 -
   7.542 -Goalw [unless_def] "[| F:(A-B) co (A Un B) |] ==> F : A unless B";
   7.543 -by (blast_tac (claset() addDs [constrainsD2]) 1);
   7.544 -qed "unlessI";
   7.545 -
   7.546 -Goalw [unless_def] "F :A unless B ==> F : (A-B) co (A Un B)";
   7.547 -by Auto_tac;
   7.548 -qed "unlessD";
   7.549 -
   7.550 -(*** initially ***)
   7.551 -
   7.552 -Goalw [initially_def]
   7.553 -"initially(A) <= program";
   7.554 -by (Blast_tac 1);
   7.555 -qed "initially_type";
   7.556 -
   7.557 -Goalw [initially_def]
   7.558 -"[| F:program; Init(F)<=A |] ==> F:initially(A)";
   7.559 -by (Blast_tac 1);
   7.560 -qed "initiallyI";
   7.561 -
   7.562 -Goalw [initially_def]
   7.563 -"F:initially(A) ==> Init(F)<=A";
   7.564 -by (Blast_tac 1);
   7.565 -qed "initiallyD";
   7.566 -
   7.567 -(*** stable ***)
   7.568 -
   7.569 -Goalw [stable_def, constrains_def]
   7.570 -   "stable(A)<=program";
   7.571 -by (Blast_tac 1);
   7.572 -qed "stable_type";
   7.573 -
   7.574 -Goalw [stable_def] 
   7.575 -    "F : A co A ==> F : stable(A)";
   7.576 -by (assume_tac 1);
   7.577 -qed "stableI";
   7.578 -
   7.579 -Goalw [stable_def] "F:stable(A) ==> F : A co A";
   7.580 -by (assume_tac 1);
   7.581 -qed "stableD";
   7.582 -
   7.583 -Goalw [stable_def, constrains_def] "F:stable(A) ==> F:program & st_set(A)";
   7.584 -by Auto_tac;
   7.585 -qed "stableD2";
   7.586 -
   7.587 -Goalw [stable_def, constrains_def] "stable(state) = program";
   7.588 -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
   7.589 -qed "stable_state";
   7.590 -AddIffs [stable_state];
   7.591 -
   7.592 -Goalw [unless_def, stable_def]
   7.593 - "stable(A)= A unless 0"; 
   7.594 -by Auto_tac;
   7.595 -qed "stable_unless";
   7.596 -
   7.597 -
   7.598 -(** Union **)
   7.599 -
   7.600 -Goalw [stable_def]
   7.601 -    "[| F : stable(A); F:stable(A') |] ==> F : stable(A Un A')";
   7.602 -by (blast_tac (claset() addIs [constrains_Un]) 1);
   7.603 -qed "stable_Un";
   7.604 -
   7.605 -val [major, minor] = Goalw [stable_def]
   7.606 -"[|(!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))";
   7.607 -by (cut_facts_tac [minor] 1);
   7.608 -by (blast_tac (claset() addIs [constrains_UN, major]) 1);
   7.609 -qed "stable_UN";
   7.610 -
   7.611 -Goalw [stable_def]
   7.612 -    "[| F : stable(A);  F : stable(A') |] ==> F : stable (A Int A')";
   7.613 -by (blast_tac (claset() addIs [constrains_Int]) 1);
   7.614 -qed "stable_Int";
   7.615 -
   7.616 -val [major, minor] = Goalw [stable_def]
   7.617 -"[| (!!i. i:I ==> F:stable(A(i))); F:program |] ==> F : stable (INT i:I. A(i))";
   7.618 -by (cut_facts_tac [minor] 1);
   7.619 -by (blast_tac (claset() addIs [constrains_INT, major]) 1);
   7.620 -qed "stable_INT";
   7.621 -
   7.622 -Goalw [stable_def]
   7.623 -"[|ALL z. F:stable({s:state. P(s, z)}); F:program|]==>F:stable({s:state. ALL z. P(s, z)})";
   7.624 -by (rtac constrains_All 1);
   7.625 -by Auto_tac;
   7.626 -qed "stable_All";
   7.627 -
   7.628 -Goalw [stable_def, constrains_def, st_set_def]
   7.629 -"[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')";
   7.630 -by Auto_tac;
   7.631 -by (blast_tac (claset() addSDs [bspec]) 1); 
   7.632 -qed "stable_constrains_Un";
   7.633 -
   7.634 -Goalw [stable_def, constrains_def, st_set_def]
   7.635 -  "[| F : stable(C); F :  (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
   7.636 -by (Clarify_tac 1);
   7.637 -by (Blast_tac 1);
   7.638 -qed "stable_constrains_Int";
   7.639 -
   7.640 -(* [| F:stable(C); F :(C Int A) co A |] ==> F:stable(C Int A) *)
   7.641 -bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
   7.642 -
   7.643 -(** invariant **)
   7.644 -
   7.645 -Goalw [invariant_def] 
   7.646 -  "invariant(A) <= program";
   7.647 -by (blast_tac (claset() addDs [stable_type RS subsetD]) 1);
   7.648 -qed "invariant_type";
   7.649 -
   7.650 -Goalw [invariant_def, initially_def]
   7.651 - "[| Init(F)<=A;  F:stable(A) |] ==> F : invariant(A)";
   7.652 -by (forward_tac [stable_type RS subsetD] 1);
   7.653 -by Auto_tac;
   7.654 -qed "invariantI";
   7.655 -
   7.656 -Goalw [invariant_def, initially_def]
   7.657 -"F:invariant(A) ==> Init(F)<=A & F:stable(A)";
   7.658 -by Auto_tac;
   7.659 -qed "invariantD";
   7.660 -
   7.661 -Goalw [invariant_def]
   7.662 - "F:invariant(A) ==> F:program & st_set(A)";
   7.663 -by (blast_tac (claset() addDs [stableD2]) 1);
   7.664 -qed "invariantD2";
   7.665 -
   7.666 -(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
   7.667 -Goalw [invariant_def, initially_def]
   7.668 -  "[| F : invariant(A);  F : invariant(B) |] ==> F : invariant(A Int B)";
   7.669 -by (asm_full_simp_tac (simpset() addsimps [stable_Int]) 1);
   7.670 -by (Blast_tac 1);
   7.671 -qed "invariant_Int";
   7.672 -
   7.673 -(** The Elimination Theorem.  The "free" m has become universally quantified!
   7.674 - Should the premise be !!m instead of ALL m ? Would make it harder 
   7.675 - to use in forward proof. **)
   7.676 -
   7.677 -(* The general case easier to prove that le special case! *)
   7.678 -Goalw [constrains_def, st_set_def]
   7.679 -    "[| ALL m:M. F : {s:A. x(s) = m} co B(m); F:program  |] \
   7.680 -\    ==> F:{s:A. x(s):M} co (UN m:M. B(m))";
   7.681 -by Safe_tac;
   7.682 -by Auto_tac;
   7.683 -by (Blast_tac 1);
   7.684 -qed "elimination";
   7.685 -
   7.686 -(* As above, but for the special case of A=state *)
   7.687 -Goal "[| ALL m:M. F : {s:state. x(s) = m} co B(m); F:program  |] \
   7.688 -\    ==> F:{s:state. x(s):M} co (UN m:M. B(m))";
   7.689 -by (rtac elimination  1);
   7.690 -by (ALLGOALS(Clarify_tac));
   7.691 -qed "eliminiation2";
   7.692 -
   7.693 -(** strongest_rhs **)
   7.694 -
   7.695 -Goalw [constrains_def, strongest_rhs_def, st_set_def]
   7.696 -    "[| F:program; st_set(A) |] ==> F:A co (strongest_rhs(F,A))";
   7.697 -by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset()));
   7.698 -qed "constrains_strongest_rhs";
   7.699 -
   7.700 -Goalw [constrains_def, strongest_rhs_def, st_set_def]
   7.701 -"[| F:A co B; st_set(B) |] ==> strongest_rhs(F,A) <= B";
   7.702 -by Safe_tac;
   7.703 -by (dtac InterD 1);
   7.704 -by Auto_tac;
   7.705 -qed "strongest_rhs_is_strongest";
   7.706 -
   7.707 -(* Used in WFair.thy *)
   7.708 -Goal "A:Pow(Pow(B)) ==> Union(A):Pow(B)";
   7.709 -by Auto_tac;
   7.710 -qed "Union_PowI";
     8.1 --- a/src/ZF/UNITY/UNITY.thy	Fri Jun 27 13:15:40 2003 +0200
     8.2 +++ b/src/ZF/UNITY/UNITY.thy	Fri Jun 27 18:40:25 2003 +0200
     8.3 @@ -9,75 +9,698 @@
     8.4  Theory ported from HOL.
     8.5  *)
     8.6  
     8.7 -UNITY = State +
     8.8 +header {*The Basic UNITY Theory*}
     8.9 +
    8.10 +theory UNITY = State:
    8.11  consts
    8.12    constrains :: "[i, i] => i"  (infixl "co"     60)
    8.13    op_unless  :: "[i, i] => i"  (infixl "unless" 60)
    8.14  
    8.15  constdefs
    8.16 -   program  :: i 
    8.17 +   program  :: i
    8.18    "program == {<init, acts, allowed>:
    8.19 -	       Pow(state)*Pow(Pow(state*state))*Pow(Pow(state*state)).
    8.20 -	       id(state):acts & id(state):allowed}"
    8.21 +	       Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)).
    8.22 +	       id(state) \<in> acts & id(state) \<in> allowed}"
    8.23  
    8.24 -  (* The definition below yields a program thanks to the coercions
    8.25 -  init Int state, acts Int Pow(state*state), etc. *)
    8.26 -  mk_program :: [i,i,i]=>i 
    8.27 +  mk_program :: "[i,i,i]=>i"
    8.28 +  --{* The definition yields a program thanks to the coercions
    8.29 +       init \<inter> state, acts \<inter> Pow(state*state), etc. *}
    8.30    "mk_program(init, acts, allowed) ==
    8.31 -    <init Int state, cons(id(state), acts Int Pow(state*state)),
    8.32 -              cons(id(state), allowed Int Pow(state*state))>"
    8.33 +    <init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)),
    8.34 +              cons(id(state), allowed \<inter> Pow(state*state))>"
    8.35  
    8.36    SKIP :: i
    8.37    "SKIP == mk_program(state, 0, Pow(state*state))"
    8.38  
    8.39    (* Coercion from anything to program *)
    8.40 -  programify :: i=>i
    8.41 -  "programify(F) == if F:program then F else SKIP"
    8.42 +  programify :: "i=>i"
    8.43 +  "programify(F) == if F \<in> program then F else SKIP"
    8.44  
    8.45 -  RawInit :: i=>i
    8.46 +  RawInit :: "i=>i"
    8.47    "RawInit(F) == fst(F)"
    8.48 -  
    8.49 -  Init :: i=>i
    8.50 +
    8.51 +  Init :: "i=>i"
    8.52    "Init(F) == RawInit(programify(F))"
    8.53  
    8.54 -  RawActs :: i=>i
    8.55 +  RawActs :: "i=>i"
    8.56    "RawActs(F) == cons(id(state), fst(snd(F)))"
    8.57  
    8.58 -  Acts :: i=>i
    8.59 +  Acts :: "i=>i"
    8.60    "Acts(F) == RawActs(programify(F))"
    8.61  
    8.62 -  RawAllowedActs :: i=>i
    8.63 +  RawAllowedActs :: "i=>i"
    8.64    "RawAllowedActs(F) == cons(id(state), snd(snd(F)))"
    8.65  
    8.66 -  AllowedActs :: i=>i
    8.67 +  AllowedActs :: "i=>i"
    8.68    "AllowedActs(F) == RawAllowedActs(programify(F))"
    8.69  
    8.70 -  
    8.71 -  Allowed :: i =>i
    8.72 -  "Allowed(F) == {G:program. Acts(G) <= AllowedActs(F)}"
    8.73 +
    8.74 +  Allowed :: "i =>i"
    8.75 +  "Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}"
    8.76  
    8.77 -  initially :: i=>i
    8.78 -  "initially(A) == {F:program. Init(F)<=A}"
    8.79 -  
    8.80 -  stable     :: i=>i
    8.81 +  initially :: "i=>i"
    8.82 +  "initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
    8.83 +
    8.84 +  stable     :: "i=>i"
    8.85     "stable(A) == A co A"
    8.86  
    8.87 -  strongest_rhs :: [i, i] => i
    8.88 -  "strongest_rhs(F, A) == Inter({B:Pow(state). F:A co B})"
    8.89 +  strongest_rhs :: "[i, i] => i"
    8.90 +  "strongest_rhs(F, A) == Inter({B \<in> Pow(state). F \<in> A co B})"
    8.91  
    8.92 -  invariant :: i => i
    8.93 -  "invariant(A) == initially(A) Int stable(A)"
    8.94 -    
    8.95 +  invariant :: "i => i"
    8.96 +  "invariant(A) == initially(A) \<inter> stable(A)"
    8.97 +
    8.98    (* meta-function composition *)
    8.99 -  comp :: "[i=>i, i=>i] => (i=>i)" (infixl 65)
   8.100 +  metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65)
   8.101    "f comp g == %x. f(g(x))"
   8.102  
   8.103    pg_compl :: "i=>i"
   8.104    "pg_compl(X)== program - X"
   8.105 -    
   8.106 +
   8.107  defs
   8.108 -  (* Condition `st_set(A)' makes the definition slightly stronger than the HOL one *)
   8.109 -  constrains_def "A co B == {F:program. (ALL act:Acts(F). act``A<=B) & st_set(A)}"
   8.110 -  unless_def     "A unless B == (A - B) co (A Un B)"
   8.111 +  constrains_def:
   8.112 +     "A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
   8.113 +    --{* the condition @{term "st_set(A)"} makes the definition slightly
   8.114 +         stronger than the HOL one *}
   8.115 +
   8.116 +  unless_def:    "A unless B == (A - B) co (A Un B)"
   8.117 +
   8.118 +
   8.119 +(** SKIP **)
   8.120 +lemma SKIP_in_program [iff,TC]: "SKIP \<in> program"
   8.121 +by (force simp add: SKIP_def program_def mk_program_def)
   8.122 +
   8.123 +
   8.124 +subsection{*The function @{term programify}, the coercion from anything to
   8.125 + program*}
   8.126 +
   8.127 +lemma programify_program [simp]: "F \<in> program ==> programify(F)=F"
   8.128 +by (force simp add: programify_def) 
   8.129 +
   8.130 +lemma programify_in_program [iff,TC]: "programify(F) \<in> program"
   8.131 +by (force simp add: programify_def) 
   8.132 +
   8.133 +(** Collapsing rules: to remove programify from expressions **)
   8.134 +lemma programify_idem [simp]: "programify(programify(F))=programify(F)"
   8.135 +by (force simp add: programify_def) 
   8.136 +
   8.137 +lemma Init_programify [simp]: "Init(programify(F)) = Init(F)"
   8.138 +by (simp add: Init_def)
   8.139 +
   8.140 +lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)"
   8.141 +by (simp add: Acts_def)
   8.142 +
   8.143 +lemma AllowedActs_programify [simp]:
   8.144 +     "AllowedActs(programify(F)) = AllowedActs(F)"
   8.145 +by (simp add: AllowedActs_def)
   8.146 +
   8.147 +subsection{*The Inspectors for Programs*}
   8.148 +
   8.149 +lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)"
   8.150 +by (auto simp add: program_def RawActs_def)
   8.151 +
   8.152 +lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)"
   8.153 +by (simp add: id_in_RawActs Acts_def)
   8.154 +
   8.155 +lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)"
   8.156 +by (auto simp add: program_def RawAllowedActs_def)
   8.157 +
   8.158 +lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)"
   8.159 +by (simp add: id_in_RawAllowedActs AllowedActs_def)
   8.160 +
   8.161 +lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)"
   8.162 +by (simp add: cons_absorb)
   8.163 +
   8.164 +lemma cons_id_AllowedActs [simp]:
   8.165 +     "cons(id(state), AllowedActs(F)) = AllowedActs(F)"
   8.166 +by (simp add: cons_absorb)
   8.167 +
   8.168 +
   8.169 +subsection{*Types of the Inspectors*}
   8.170 +
   8.171 +lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state"
   8.172 +by (auto simp add: program_def RawInit_def)
   8.173 +
   8.174 +lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)"
   8.175 +by (auto simp add: program_def RawActs_def)
   8.176 +
   8.177 +lemma RawAllowedActs_type:
   8.178 +     "F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)"
   8.179 +by (auto simp add: program_def RawAllowedActs_def)
   8.180 +
   8.181 +lemma Init_type: "Init(F)\<subseteq>state"
   8.182 +by (simp add: RawInit_type Init_def)
   8.183 +
   8.184 +lemmas InitD = Init_type [THEN subsetD, standard]
   8.185 +
   8.186 +lemma st_set_Init [iff]: "st_set(Init(F))"
   8.187 +apply (unfold st_set_def)
   8.188 +apply (rule Init_type)
   8.189 +done
   8.190 +
   8.191 +lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)"
   8.192 +by (simp add: RawActs_type Acts_def)
   8.193 +
   8.194 +lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)"
   8.195 +by (simp add: RawAllowedActs_type AllowedActs_def)
   8.196 +
   8.197 +(* Needed in Behaviors *)
   8.198 +lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
   8.199 +by (blast dest: Acts_type [THEN subsetD])
   8.200 +
   8.201 +lemma AllowedActsD:
   8.202 +     "[| act \<in> AllowedActs(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state"
   8.203 +by (blast dest: AllowedActs_type [THEN subsetD])
   8.204 +
   8.205 +subsection{*Simplification rules involving @{term state}, @{term Init}, 
   8.206 +  @{term Acts}, and @{term AllowedActs}*}
   8.207 +
   8.208 +text{*But are they really needed?*}
   8.209 +
   8.210 +lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) <-> Init(F)=state"
   8.211 +by (cut_tac F = F in Init_type, auto)
   8.212 +
   8.213 +lemma Pow_state_times_state_is_subset_Acts_iff [iff]:
   8.214 +     "Pow(state*state) \<subseteq> Acts(F) <-> Acts(F)=Pow(state*state)"
   8.215 +by (cut_tac F = F in Acts_type, auto)
   8.216 +
   8.217 +lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]:
   8.218 +     "Pow(state*state) \<subseteq> AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)"
   8.219 +by (cut_tac F = F in AllowedActs_type, auto)
   8.220 +
   8.221 +subsubsection{*Eliminating @{text "\<inter> state"} from expressions*}
   8.222 +
   8.223 +lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)"
   8.224 +by (cut_tac F = F in Init_type, blast)
   8.225 +
   8.226 +lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)"
   8.227 +by (cut_tac F = F in Init_type, blast)
   8.228 +
   8.229 +lemma Acts_Int_Pow_state_times_state [simp]:
   8.230 +     "Acts(F) \<inter> Pow(state*state) = Acts(F)"
   8.231 +by (cut_tac F = F in Acts_type, blast)
   8.232 +
   8.233 +lemma state_times_state_Int_Acts [simp]:
   8.234 +     "Pow(state*state) \<inter> Acts(F) = Acts(F)"
   8.235 +by (cut_tac F = F in Acts_type, blast)
   8.236 +
   8.237 +lemma AllowedActs_Int_Pow_state_times_state [simp]:
   8.238 +     "AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)"
   8.239 +by (cut_tac F = F in AllowedActs_type, blast)
   8.240 +
   8.241 +lemma state_times_state_Int_AllowedActs [simp]:
   8.242 +     "Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)"
   8.243 +by (cut_tac F = F in AllowedActs_type, blast)
   8.244 +
   8.245 +
   8.246 +subsubsection{*The Opoerator @{term mk_program}*}
   8.247 +
   8.248 +lemma mk_program_in_program [iff,TC]:
   8.249 +     "mk_program(init, acts, allowed) \<in> program"
   8.250 +by (auto simp add: mk_program_def program_def)
   8.251 +
   8.252 +lemma RawInit_eq [simp]:
   8.253 +     "RawInit(mk_program(init, acts, allowed)) = init \<inter> state"
   8.254 +by (auto simp add: mk_program_def RawInit_def)
   8.255 +
   8.256 +lemma RawActs_eq [simp]:
   8.257 +     "RawActs(mk_program(init, acts, allowed)) = 
   8.258 +      cons(id(state), acts \<inter> Pow(state*state))"
   8.259 +by (auto simp add: mk_program_def RawActs_def)
   8.260 +
   8.261 +lemma RawAllowedActs_eq [simp]:
   8.262 +     "RawAllowedActs(mk_program(init, acts, allowed)) =
   8.263 +      cons(id(state), allowed \<inter> Pow(state*state))"
   8.264 +by (auto simp add: mk_program_def RawAllowedActs_def)
   8.265 +
   8.266 +lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state"
   8.267 +by (simp add: Init_def)
   8.268 +
   8.269 +lemma Acts_eq [simp]:
   8.270 +     "Acts(mk_program(init, acts, allowed)) = 
   8.271 +      cons(id(state), acts  \<inter> Pow(state*state))"
   8.272 +by (simp add: Acts_def)
   8.273 +
   8.274 +lemma AllowedActs_eq [simp]:
   8.275 +     "AllowedActs(mk_program(init, acts, allowed))=
   8.276 +      cons(id(state), allowed \<inter> Pow(state*state))"
   8.277 +by (simp add: AllowedActs_def)
   8.278 +
   8.279 +(**Init, Acts, and AlowedActs  of SKIP **)
   8.280 +
   8.281 +lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state"
   8.282 +by (simp add: SKIP_def)
   8.283 +
   8.284 +lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)"
   8.285 +by (force simp add: SKIP_def)
   8.286 +
   8.287 +lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}"
   8.288 +by (force simp add: SKIP_def)
   8.289 +
   8.290 +lemma Init_SKIP [simp]: "Init(SKIP) = state"
   8.291 +by (force simp add: SKIP_def)
   8.292 +
   8.293 +lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}"
   8.294 +by (force simp add: SKIP_def)
   8.295 +
   8.296 +lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)"
   8.297 +by (force simp add: SKIP_def)
   8.298 +
   8.299 +(** Equality of UNITY programs **)
   8.300 +
   8.301 +lemma raw_surjective_mk_program:
   8.302 +     "F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"
   8.303 +apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def
   8.304 +            RawAllowedActs_def, blast+)
   8.305 +done
   8.306 +
   8.307 +lemma surjective_mk_program [simp]:
   8.308 +  "mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"
   8.309 +by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def)
   8.310 +
   8.311 +lemma program_equalityI:                             
   8.312 +    "[|Init(F) = Init(G); Acts(F) = Acts(G);
   8.313 +       AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G"
   8.314 +apply (subgoal_tac "programify(F) = programify(G)") 
   8.315 +apply simp 
   8.316 +apply (simp only: surjective_mk_program [symmetric]) 
   8.317 +done
   8.318 +
   8.319 +lemma program_equalityE:                             
   8.320 + "[|F = G;
   8.321 +    [|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]
   8.322 +    ==> P |] 
   8.323 +  ==> P"
   8.324 +by force
   8.325 +
   8.326 +
   8.327 +lemma program_equality_iff:
   8.328 +    "[| F \<in> program; G \<in> program |] ==>(F=G)  <->
   8.329 +     (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"
   8.330 +by (blast intro: program_equalityI program_equalityE)
   8.331 +
   8.332 +subsection{*These rules allow "lazy" definition expansion*}
   8.333 +
   8.334 +lemma def_prg_Init:
   8.335 +     "F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state"
   8.336 +by auto
   8.337 +
   8.338 +lemma def_prg_Acts:
   8.339 +     "F == mk_program (init,acts,allowed)
   8.340 +      ==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))"
   8.341 +by auto
   8.342 +
   8.343 +lemma def_prg_AllowedActs:
   8.344 +     "F == mk_program (init,acts,allowed)
   8.345 +      ==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
   8.346 +by auto
   8.347 +
   8.348 +lemma def_prg_simps:
   8.349 +    "[| F == mk_program (init,acts,allowed) |]
   8.350 +     ==> Init(F) = init \<inter> state & 
   8.351 +         Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) &
   8.352 +         AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))"
   8.353 +by auto
   8.354 +
   8.355 +
   8.356 +(*An action is expanded only if a pair of states is being tested against it*)
   8.357 +lemma def_act_simp:
   8.358 +     "[| act == {<s,s'> \<in> A*B. P(s, s')} |]
   8.359 +      ==> (<s,s'> \<in> act) <-> (<s,s'> \<in> A*B & P(s, s'))"
   8.360 +by auto
   8.361 +
   8.362 +(*A set is expanded only if an element is being tested against it*)
   8.363 +lemma def_set_simp: "A == B ==> (x \<in> A) <-> (x \<in> B)"
   8.364 +by auto
   8.365 +
   8.366 +
   8.367 +subsection{*The Constrains Operator*}
   8.368 +
   8.369 +lemma constrains_type: "A co B \<subseteq> program"
   8.370 +by (force simp add: constrains_def)
   8.371 +
   8.372 +lemma constrainsI:
   8.373 +    "[|(!!act s s'. [| act: Acts(F);  <s,s'> \<in> act; s \<in> A|] ==> s' \<in> A');
   8.374 +        F \<in> program; st_set(A) |]  ==> F \<in> A co A'"
   8.375 +by (force simp add: constrains_def)
   8.376 +
   8.377 +lemma constrainsD:
   8.378 +   "F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B"
   8.379 +by (force simp add: constrains_def)
   8.380 +
   8.381 +lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)"
   8.382 +by (force simp add: constrains_def)
   8.383 +
   8.384 +lemma constrains_empty [iff]: "F \<in> 0 co B <-> F \<in> program"
   8.385 +by (force simp add: constrains_def st_set_def)
   8.386 +
   8.387 +lemma constrains_empty2 [iff]: "(F \<in> A co 0) <-> (A=0 & F \<in> program)"
   8.388 +by (force simp add: constrains_def st_set_def)
   8.389 +
   8.390 +lemma constrains_state [iff]: "(F \<in> state co B) <-> (state\<subseteq>B & F \<in> program)"
   8.391 +apply (cut_tac F = F in Acts_type)
   8.392 +apply (force simp add: constrains_def st_set_def)
   8.393 +done
   8.394 +
   8.395 +lemma constrains_state2 [iff]: "F \<in> A co state <-> (F \<in> program & st_set(A))"
   8.396 +apply (cut_tac F = F in Acts_type)
   8.397 +apply (force simp add: constrains_def st_set_def)
   8.398 +done
   8.399 +
   8.400 +(*monotonic in 2nd argument*)
   8.401 +lemma constrains_weaken_R:
   8.402 +    "[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'"
   8.403 +apply (unfold constrains_def, blast)
   8.404 +done
   8.405 +
   8.406 +(*anti-monotonic in 1st argument*)
   8.407 +lemma constrains_weaken_L:
   8.408 +    "[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'"
   8.409 +apply (unfold constrains_def st_set_def, blast)
   8.410 +done
   8.411 +
   8.412 +lemma constrains_weaken:
   8.413 +   "[| F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' |] ==> F \<in> B co B'"
   8.414 +apply (drule constrains_weaken_R)
   8.415 +apply (drule_tac [2] constrains_weaken_L, blast+)
   8.416 +done
   8.417 +
   8.418 +
   8.419 +subsection{*Constrains and Union*}
   8.420 +
   8.421 +lemma constrains_Un:
   8.422 +    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A Un B) co (A' Un B')"
   8.423 +by (auto simp add: constrains_def st_set_def, force)
   8.424 +
   8.425 +lemma constrains_UN:
   8.426 +     "[|!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program |]
   8.427 +      ==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))"
   8.428 +by (force simp add: constrains_def st_set_def) 
   8.429 +
   8.430 +lemma constrains_Un_distrib:
   8.431 +     "(A Un B) co C = (A co C) \<inter> (B co C)"
   8.432 +by (force simp add: constrains_def st_set_def)
   8.433 +
   8.434 +lemma constrains_UN_distrib:
   8.435 +   "i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)"
   8.436 +by (force simp add: constrains_def st_set_def)
   8.437 +
   8.438 +
   8.439 +subsection{*Constrains and Intersection*}
   8.440 +
   8.441 +lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
   8.442 +by (force simp add: constrains_def st_set_def)
   8.443 +
   8.444 +lemma constrains_INT_distrib:
   8.445 +     "x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))"
   8.446 +by (force simp add: constrains_def st_set_def)
   8.447 +
   8.448 +lemma constrains_Int:
   8.449 +    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
   8.450 +by (force simp add: constrains_def st_set_def)
   8.451 +
   8.452 +lemma constrains_INT [rule_format]:
   8.453 +     "[| \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program|]
   8.454 +      ==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))"
   8.455 +apply (case_tac "I=0")
   8.456 + apply (simp add: Inter_def)
   8.457 +apply (erule not_emptyE)
   8.458 +apply (auto simp add: constrains_def st_set_def, blast) 
   8.459 +apply (drule bspec, assumption, force) 
   8.460 +done
   8.461 +
   8.462 +(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *)
   8.463 +lemma constrains_All:
   8.464 +"[| \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program |]==>
   8.465 +    F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}"
   8.466 +by (unfold constrains_def, blast)
   8.467 +
   8.468 +lemma constrains_imp_subset:
   8.469 +  "[| F \<in> A co A' |] ==> A \<subseteq> A'"
   8.470 +by (unfold constrains_def st_set_def, force)
   8.471 +
   8.472 +(*The reasoning is by subsets since "co" refers to single actions
   8.473 +  only.  So this rule isn't that useful.*)
   8.474 +
   8.475 +lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
   8.476 +by (unfold constrains_def st_set_def, auto, blast)
   8.477 +
   8.478 +lemma constrains_cancel:
   8.479 +"[| F \<in> A co (A' Un B); F \<in> B co B' |] ==> F \<in> A co (A' Un B')"
   8.480 +apply (drule_tac A = B in constrains_imp_subset)
   8.481 +apply (blast intro: constrains_weaken_R)
   8.482 +done
   8.483 +
   8.484 +
   8.485 +subsection{*The Unless Operator*}
   8.486 +
   8.487 +lemma unless_type: "A unless B \<subseteq> program"
   8.488 +by (force simp add: unless_def constrains_def) 
   8.489 +
   8.490 +lemma unlessI: "[| F \<in> (A-B) co (A Un B) |] ==> F \<in> A unless B"
   8.491 +apply (unfold unless_def)
   8.492 +apply (blast dest: constrainsD2)
   8.493 +done
   8.494 +
   8.495 +lemma unlessD: "F :A unless B ==> F \<in> (A-B) co (A Un B)"
   8.496 +by (unfold unless_def, auto)
   8.497 +
   8.498 +
   8.499 +subsection{*The Operator @{term initially}*}
   8.500 +
   8.501 +lemma initially_type: "initially(A) \<subseteq> program"
   8.502 +by (unfold initially_def, blast)
   8.503 +
   8.504 +lemma initiallyI: "[| F \<in> program; Init(F)\<subseteq>A |] ==> F \<in> initially(A)"
   8.505 +by (unfold initially_def, blast)
   8.506 +
   8.507 +lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A"
   8.508 +by (unfold initially_def, blast)
   8.509 +
   8.510 +
   8.511 +subsection{*The Operator @{term stable}*}
   8.512 +
   8.513 +lemma stable_type: "stable(A)\<subseteq>program"
   8.514 +by (unfold stable_def constrains_def, blast)
   8.515 +
   8.516 +lemma stableI: "F \<in> A co A ==> F \<in> stable(A)"
   8.517 +by (unfold stable_def, assumption)
   8.518 +
   8.519 +lemma stableD: "F \<in> stable(A) ==> F \<in> A co A"
   8.520 +by (unfold stable_def, assumption)
   8.521 +
   8.522 +lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)"
   8.523 +by (unfold stable_def constrains_def, auto)
   8.524 +
   8.525 +lemma stable_state [simp]: "stable(state) = program"
   8.526 +by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD])
   8.527 +
   8.528 +
   8.529 +lemma stable_unless: "stable(A)= A unless 0"
   8.530 +by (auto simp add: unless_def stable_def)
   8.531 +
   8.532 +
   8.533 +subsection{*Union and Intersection with @{term stable}*}
   8.534 +
   8.535 +lemma stable_Un:
   8.536 +    "[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable(A Un A')"
   8.537 +apply (unfold stable_def)
   8.538 +apply (blast intro: constrains_Un)
   8.539 +done
   8.540 +
   8.541 +lemma stable_UN:
   8.542 +     "[|!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program |] 
   8.543 +      ==> F \<in> stable (\<Union>i \<in> I. A(i))"
   8.544 +apply (unfold stable_def)
   8.545 +apply (blast intro: constrains_UN)
   8.546 +done
   8.547 +
   8.548 +lemma stable_Int:
   8.549 +    "[| F \<in> stable(A);  F \<in> stable(A') |] ==> F \<in> stable (A \<inter> A')"
   8.550 +apply (unfold stable_def)
   8.551 +apply (blast intro: constrains_Int)
   8.552 +done
   8.553 +
   8.554 +lemma stable_INT:
   8.555 +     "[| !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program |]
   8.556 +      ==> F \<in> stable (\<Inter>i \<in> I. A(i))"
   8.557 +apply (unfold stable_def)
   8.558 +apply (blast intro: constrains_INT)
   8.559 +done
   8.560 +
   8.561 +lemma stable_All:
   8.562 +    "[|\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program|]
   8.563 +     ==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})"
   8.564 +apply (unfold stable_def)
   8.565 +apply (rule constrains_All, auto)
   8.566 +done
   8.567 +
   8.568 +lemma stable_constrains_Un:
   8.569 +     "[| F \<in> stable(C); F \<in> A co (C Un A') |] ==> F \<in> (C Un A) co (C Un A')"
   8.570 +apply (unfold stable_def constrains_def st_set_def, auto)
   8.571 +apply (blast dest!: bspec)
   8.572 +done
   8.573 +
   8.574 +lemma stable_constrains_Int:
   8.575 +     "[| F \<in> stable(C); F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
   8.576 +by (unfold stable_def constrains_def st_set_def, blast)
   8.577 +
   8.578 +(* [| F \<in> stable(C); F  \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *)
   8.579 +lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
   8.580 +
   8.581 +subsection{*The Operator @{term invariant}*}
   8.582 +
   8.583 +lemma invariant_type: "invariant(A) \<subseteq> program"
   8.584 +apply (unfold invariant_def)
   8.585 +apply (blast dest: stable_type [THEN subsetD])
   8.586 +done
   8.587 +
   8.588 +lemma invariantI: "[| Init(F)\<subseteq>A;  F \<in> stable(A) |] ==> F \<in> invariant(A)"
   8.589 +apply (unfold invariant_def initially_def)
   8.590 +apply (frule stable_type [THEN subsetD], auto)
   8.591 +done
   8.592 +
   8.593 +lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)"
   8.594 +by (unfold invariant_def initially_def, auto)
   8.595 +
   8.596 +lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)"
   8.597 +apply (unfold invariant_def)
   8.598 +apply (blast dest: stableD2)
   8.599 +done
   8.600 +
   8.601 +text{*Could also say
   8.602 +      @{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}*}
   8.603 +lemma invariant_Int:
   8.604 +  "[| F \<in> invariant(A);  F \<in> invariant(B) |] ==> F \<in> invariant(A \<inter> B)"
   8.605 +apply (unfold invariant_def initially_def)
   8.606 +apply (simp add: stable_Int, blast)
   8.607 +done
   8.608 +
   8.609 +
   8.610 +subsection{*The Elimination Theorem*}
   8.611 +
   8.612 +(** The "free" m has become universally quantified!
   8.613 + Should the premise be !!m instead of \<forall>m ? Would make it harder
   8.614 + to use in forward proof. **)
   8.615 +
   8.616 +(* The general case easier to prove that le special case! *)
   8.617 +lemma "elimination":
   8.618 +    "[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program  |]
   8.619 +     ==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
   8.620 +by (auto simp add: constrains_def st_set_def, blast)
   8.621 +
   8.622 +(* As above, but for the special case of A=state *)
   8.623 +lemma elimination2:
   8.624 +     "[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program  |]
   8.625 +     ==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))"
   8.626 +by (rule UNITY.elimination, auto)
   8.627 +
   8.628 +subsection{*The Operator @{term strongest_rhs}*}
   8.629 +
   8.630 +lemma constrains_strongest_rhs:
   8.631 +    "[| F \<in> program; st_set(A) |] ==> F \<in> A co (strongest_rhs(F,A))"
   8.632 +by (auto simp add: constrains_def strongest_rhs_def st_set_def
   8.633 +              dest: Acts_type [THEN subsetD])
   8.634 +
   8.635 +lemma strongest_rhs_is_strongest:
   8.636 +     "[| F \<in> A co B; st_set(B) |] ==> strongest_rhs(F,A) \<subseteq> B"
   8.637 +by (auto simp add: constrains_def strongest_rhs_def st_set_def)
   8.638 +
   8.639 +ML
   8.640 +{*
   8.641 +val constrains_def = thm "constrains_def";
   8.642 +val stable_def = thm "stable_def";
   8.643 +val invariant_def = thm "invariant_def";
   8.644 +val unless_def = thm "unless_def";
   8.645 +val initially_def = thm "initially_def";
   8.646 +val SKIP_def = thm "SKIP_def";
   8.647 +val Allowed_def = thm "Allowed_def";
   8.648 +val programify_def = thm "programify_def";
   8.649 +val metacomp_def = thm "metacomp_def";
   8.650 +
   8.651 +val id_in_Acts = thm "id_in_Acts";
   8.652 +val id_in_RawAllowedActs = thm "id_in_RawAllowedActs";
   8.653 +val id_in_AllowedActs = thm "id_in_AllowedActs";
   8.654 +val cons_id_Acts = thm "cons_id_Acts";
   8.655 +val cons_id_AllowedActs = thm "cons_id_AllowedActs";
   8.656 +val Init_type = thm "Init_type";
   8.657 +val st_set_Init = thm "st_set_Init";
   8.658 +val Acts_type = thm "Acts_type";
   8.659 +val AllowedActs_type = thm "AllowedActs_type";
   8.660 +val ActsD = thm "ActsD";
   8.661 +val AllowedActsD = thm "AllowedActsD";
   8.662 +val mk_program_in_program = thm "mk_program_in_program";
   8.663 +val Init_eq = thm "Init_eq";
   8.664 +val Acts_eq = thm "Acts_eq";
   8.665 +val AllowedActs_eq = thm "AllowedActs_eq";
   8.666 +val Init_SKIP = thm "Init_SKIP";
   8.667 +val Acts_SKIP = thm "Acts_SKIP";
   8.668 +val AllowedActs_SKIP = thm "AllowedActs_SKIP";
   8.669 +val raw_surjective_mk_program = thm "raw_surjective_mk_program";
   8.670 +val surjective_mk_program = thm "surjective_mk_program";
   8.671 +val program_equalityI = thm "program_equalityI";
   8.672 +val program_equalityE = thm "program_equalityE";
   8.673 +val program_equality_iff = thm "program_equality_iff";
   8.674 +val def_prg_Init = thm "def_prg_Init";
   8.675 +val def_prg_Acts = thm "def_prg_Acts";
   8.676 +val def_prg_AllowedActs = thm "def_prg_AllowedActs";
   8.677 +val def_prg_simps = thm "def_prg_simps";
   8.678 +val def_act_simp = thm "def_act_simp";
   8.679 +val def_set_simp = thm "def_set_simp";
   8.680 +val constrains_type = thm "constrains_type";
   8.681 +val constrainsI = thm "constrainsI";
   8.682 +val constrainsD = thm "constrainsD";
   8.683 +val constrainsD2 = thm "constrainsD2";
   8.684 +val constrains_empty = thm "constrains_empty";
   8.685 +val constrains_empty2 = thm "constrains_empty2";
   8.686 +val constrains_state = thm "constrains_state";
   8.687 +val constrains_state2 = thm "constrains_state2";
   8.688 +val constrains_weaken_R = thm "constrains_weaken_R";
   8.689 +val constrains_weaken_L = thm "constrains_weaken_L";
   8.690 +val constrains_weaken = thm "constrains_weaken";
   8.691 +val constrains_Un = thm "constrains_Un";
   8.692 +val constrains_UN = thm "constrains_UN";
   8.693 +val constrains_Un_distrib = thm "constrains_Un_distrib";
   8.694 +val constrains_UN_distrib = thm "constrains_UN_distrib";
   8.695 +val constrains_Int_distrib = thm "constrains_Int_distrib";
   8.696 +val constrains_INT_distrib = thm "constrains_INT_distrib";
   8.697 +val constrains_Int = thm "constrains_Int";
   8.698 +val constrains_INT = thm "constrains_INT";
   8.699 +val constrains_All = thm "constrains_All";
   8.700 +val constrains_imp_subset = thm "constrains_imp_subset";
   8.701 +val constrains_trans = thm "constrains_trans";
   8.702 +val constrains_cancel = thm "constrains_cancel";
   8.703 +val unless_type = thm "unless_type";
   8.704 +val unlessI = thm "unlessI";
   8.705 +val unlessD = thm "unlessD";
   8.706 +val initially_type = thm "initially_type";
   8.707 +val initiallyI = thm "initiallyI";
   8.708 +val initiallyD = thm "initiallyD";
   8.709 +val stable_type = thm "stable_type";
   8.710 +val stableI = thm "stableI";
   8.711 +val stableD = thm "stableD";
   8.712 +val stableD2 = thm "stableD2";
   8.713 +val stable_state = thm "stable_state";
   8.714 +val stable_unless = thm "stable_unless";
   8.715 +val stable_Un = thm "stable_Un";
   8.716 +val stable_UN = thm "stable_UN";
   8.717 +val stable_Int = thm "stable_Int";
   8.718 +val stable_INT = thm "stable_INT";
   8.719 +val stable_All = thm "stable_All";
   8.720 +val stable_constrains_Un = thm "stable_constrains_Un";
   8.721 +val stable_constrains_Int = thm "stable_constrains_Int";
   8.722 +val invariant_type = thm "invariant_type";
   8.723 +val invariantI = thm "invariantI";
   8.724 +val invariantD = thm "invariantD";
   8.725 +val invariantD2 = thm "invariantD2";
   8.726 +val invariant_Int = thm "invariant_Int";
   8.727 +val elimination = thm "elimination";
   8.728 +val elimination2 = thm "elimination2";
   8.729 +val constrains_strongest_rhs = thm "constrains_strongest_rhs";
   8.730 +val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest";
   8.731 +
   8.732 +fun simp_of_act def = def RS def_act_simp;
   8.733 +fun simp_of_set def = def RS def_set_simp;
   8.734 +*}
   8.735 +
   8.736  end
   8.737 -
     9.1 --- a/src/ZF/UNITY/Union.ML	Fri Jun 27 13:15:40 2003 +0200
     9.2 +++ b/src/ZF/UNITY/Union.ML	Fri Jun 27 18:40:25 2003 +0200
     9.3 @@ -168,7 +168,9 @@
     9.4  
     9.5  Goal "Init(JN i:I. F(i)) = (if I=0 then state else (INT i:I. Init(F(i))))";
     9.6  by (simp_tac (simpset() addsimps [JOIN_def]) 1);
     9.7 -by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [INT_Int_distrib]));
     9.8 +by (auto_tac (claset() addSEs [not_emptyE],
     9.9 +               simpset() addsimps INT_extend_simps
    9.10 +                         delsimps INT_simps));
    9.11  qed "Init_JN";
    9.12  
    9.13  Goalw [JOIN_def]
    9.14 @@ -496,11 +498,10 @@
    9.15  qed "ok_Join_commute_I";
    9.16  
    9.17  Goal "F ok JOIN(I,G) <-> (ALL i:I. F ok G(i))";
    9.18 -by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
    9.19 -by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
    9.20 +by (force_tac (claset() addDs [Acts_type RS subsetD] addSEs [not_emptyE],
    9.21 +               simpset() addsimps [ok_def]) 1);
    9.22  qed "ok_JN_iff1";
    9.23  
    9.24 -
    9.25  Goal "JOIN(I,G) ok F   <->  (ALL i:I. G(i) ok F)";
    9.26  by (auto_tac (claset() addSEs [not_emptyE], simpset() addsimps [ok_def]));
    9.27  by (blast_tac (claset() addDs [Acts_type RS subsetD]) 1);
    9.28 @@ -531,11 +532,11 @@
    9.29  Goal "i:I ==> \
    9.30  \  Allowed(JOIN(I,F)) = (INT i:I. Allowed(programify(F(i))))";
    9.31  by (auto_tac (claset(), simpset() addsimps [Allowed_def]));
    9.32 +by (Blast_tac 1); 
    9.33  qed "Allowed_JN";
    9.34  Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
    9.35  
    9.36 -Goal 
    9.37 -"F ok G <-> (programify(F):Allowed(programify(G)) & \
    9.38 +Goal "F ok G <-> (programify(F):Allowed(programify(G)) & \
    9.39  \  programify(G):Allowed(programify(F)))";
    9.40  by (asm_simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
    9.41  qed "ok_iff_Allowed";
    10.1 --- a/src/ZF/UNITY/WFair.thy	Fri Jun 27 13:15:40 2003 +0200
    10.2 +++ b/src/ZF/UNITY/WFair.thy	Fri Jun 27 18:40:25 2003 +0200
    10.3 @@ -37,7 +37,7 @@
    10.4  	      <Union(S),B>:leads(D, F)"
    10.5  
    10.6    monos        Pow_mono
    10.7 -  type_intrs  "[Union_PowI, UnionI, PowI]"
    10.8 +  type_intrs  "[Union_Pow_iff RS iffD2, UnionI, PowI]"
    10.9   
   10.10  constdefs
   10.11  
    11.1 --- a/src/ZF/equalities.thy	Fri Jun 27 13:15:40 2003 +0200
    11.2 +++ b/src/ZF/equalities.thy	Fri Jun 27 18:40:25 2003 +0200
    11.3 @@ -922,6 +922,9 @@
    11.4  lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
    11.5  by blast
    11.6  
    11.7 +lemma Union_Pow_iff: "Union(A) \<in> Pow(B) <-> A \<in> Pow(Pow(B))"
    11.8 +by blast
    11.9 +
   11.10  lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
   11.11  by blast
   11.12  
   11.13 @@ -1231,6 +1234,7 @@
   11.14  val UN_Pow_subset = thm "UN_Pow_subset";
   11.15  val subset_Pow_Union = thm "subset_Pow_Union";
   11.16  val Union_Pow_eq = thm "Union_Pow_eq";
   11.17 +val Union_Pow_iff = thm "Union_Pow_iff";
   11.18  val Pow_Int_eq = thm "Pow_Int_eq";
   11.19  val Pow_INT_eq = thm "Pow_INT_eq";
   11.20  val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";