6297

1 
(* Title: HOL/UNITY/Extend.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1999 University of Cambridge


5 


6 
Extending of state sets


7 
function f (forget) maps the extended state to the original state


8 
function g (forgotten) maps the extended state to the "extending part"


9 
*)


10 


11 
Open_locale "Extend";


12 


13 
val slice_def = thm "slice_def";


14 
val f_act_def = thm "f_act_def";


15 


16 
(*** Trivial properties of f, g, h ***)


17 


18 
val inj_h = thm "inj_h";


19 
val surj_h = thm "surj_h";


20 
Addsimps [inj_h, inj_h RS inj_eq, surj_h];


21 


22 
val f_def = thm "f_def";


23 
val g_def = thm "g_def";


24 


25 
Goal "f(h(x,y)) = x";


26 
by (simp_tac (simpset() addsimps [f_def]) 1);


27 
qed "f_h_eq";


28 
Addsimps [f_h_eq];


29 


30 
Goal "g(h(x,y)) = y";


31 
by (simp_tac (simpset() addsimps [g_def]) 1);


32 
qed "g_h_eq";


33 
Addsimps [g_h_eq];


34 


35 
Goal "h(f z, g z) = z";


36 
by (cut_inst_tac [("y", "z")] (surj_h RS surjD) 1);


37 
by Auto_tac;


38 
qed "h_f_g_eq";


39 


40 


41 
(*** extend_set: basic properties ***)


42 


43 
Goalw [extend_set_def]


44 
"(h(x,y)) : extend_set h A = (x : A)";


45 
by Auto_tac;


46 
qed "mem_extend_set_iff";


47 
AddIffs [mem_extend_set_iff];


48 


49 
Goal "inj (extend_set h)";


50 
by (rtac injI 1);


51 
by (rewtac extend_set_def);


52 
by (etac equalityE 1);


53 
by (blast_tac (claset() addSDs [inj_h RS inj_image_mem_iff RS iffD1]) 1);


54 
qed "inj_extend_set";


55 


56 
Goalw [extend_set_def]


57 
"extend_set h (A Un B) = extend_set h A Un extend_set h B";


58 
by Auto_tac;


59 
qed "extend_set_Un_distrib";


60 


61 
Goalw [extend_set_def]


62 
"extend_set h (A Int B) = extend_set h A Int extend_set h B";


63 
by Auto_tac;


64 
qed "extend_set_Int_distrib";


65 


66 
Goalw [extend_set_def]

6647

67 
"extend_set h (INTER A B) = (INT x:A. extend_set h (B x))";


68 
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);


69 
qed "extend_set_INTER_distrib";


70 


71 
Goalw [extend_set_def]

6297

72 
"extend_set h (A  B) = extend_set h A  extend_set h B";


73 
by Auto_tac;


74 
qed "extend_set_Diff_distrib";


75 


76 
Goalw [extend_set_def] "extend_set h (Union A) = (UN X:A. extend_set h X)";


77 
by (Blast_tac 1);


78 
qed "extend_set_Union";


79 


80 
Goalw [extend_set_def]


81 
"(extend_set h A <=  extend_set h B) = (A <=  B)";


82 
by Auto_tac;


83 
qed "extend_set_subset_Compl_eq";


84 


85 


86 
Goalw [extend_set_def] "f `` extend_set h A = A";


87 
by Auto_tac;


88 
by (blast_tac (claset() addIs [f_h_eq RS sym]) 1);


89 
qed "f_image_extend_set";


90 
Addsimps [f_image_extend_set];


91 


92 


93 
(*** extend_act ***)


94 


95 
Goalw [extend_act_def]


96 
"((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";


97 
by Auto_tac;


98 
qed "mem_extend_act_iff";


99 
AddIffs [mem_extend_act_iff];


100 


101 
Goal "inj (extend_act h)";


102 
by (rtac injI 1);


103 
by (rewtac extend_act_def);


104 
by (force_tac (claset() addSEs [equalityE]


105 
addIs [h_f_g_eq RS sym],


106 
simpset()) 1);


107 
qed "inj_extend_act";


108 


109 
Goalw [extend_set_def, extend_act_def]


110 
"extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)";


111 
by (Force_tac 1);


112 
qed "extend_act_Image";


113 
Addsimps [extend_act_Image];


114 


115 
Goalw [extend_set_def, extend_act_def]


116 
"(extend_set h A <= extend_set h B) = (A <= B)";


117 
by (Force_tac 1);


118 
qed "extend_set_strict_mono";


119 
Addsimps [extend_set_strict_mono];


120 


121 
Goalw [extend_set_def, extend_act_def]


122 
"Domain (extend_act h act) = extend_set h (Domain act)";


123 
by (Force_tac 1);


124 
qed "Domain_extend_act";


125 


126 
Goalw [extend_set_def, extend_act_def]


127 
"extend_act h Id = Id";


128 
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);


129 
qed "extend_act_Id";


130 
Addsimps [extend_act_Id];


131 


132 
Goal "Id : extend_act h `` Acts F";


133 
by (auto_tac (claset() addSIs [extend_act_Id RS sym],


134 
simpset() addsimps [image_iff]));


135 
qed "Id_mem_extend_act";


136 


137 


138 
(**** extend ****)


139 


140 
(*** Basic properties ***)


141 


142 
Goalw [extend_set_def, extend_def]


143 
"Init (extend h F) = extend_set h (Init F)";


144 
by Auto_tac;


145 
qed "Init_extend";


146 


147 
Goal "Acts (extend h F) = (extend_act h `` Acts F)";


148 
by (auto_tac (claset() addSIs [extend_act_Id RS sym],


149 
simpset() addsimps [extend_def, image_iff]));


150 
qed "Acts_extend";


151 


152 
Addsimps [Init_extend, Acts_extend];


153 


154 
Goalw [SKIP_def] "extend h SKIP = SKIP";


155 
by (rtac program_equalityI 1);


156 
by (auto_tac (claset() addIs [h_f_g_eq RS sym],


157 
simpset() addsimps [extend_set_def]));


158 
qed "extend_SKIP";


159 
Addsimps [extend_SKIP];


160 


161 
Goal "inj (extend h)";


162 
by (rtac injI 1);


163 
by (rewtac extend_def);


164 
by (etac program_equalityE 1);


165 
by (full_simp_tac


166 
(simpset() addsimps [inj_extend_set RS inj_eq,


167 
inj_extend_act RS inj_image_eq_iff,


168 
Id_mem_extend_act RS insert_absorb]) 1);


169 
by (blast_tac (claset() addIs [program_equalityI]) 1);


170 
qed "inj_extend";


171 


172 
Goal "extend h (F Join G) = extend h F Join extend h G";


173 
by (rtac program_equalityI 1);


174 
by (simp_tac (simpset() addsimps [image_Un, Acts_Join]) 2);


175 
by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);


176 
qed "extend_Join";


177 
Addsimps [extend_Join];


178 

6647

179 
Goal "extend h (JOIN I F) = (JN i:I. extend h (F i))";


180 
by (rtac program_equalityI 1);


181 
by (simp_tac (simpset() addsimps [image_UNION, Acts_JN]) 2);


182 
by (simp_tac (simpset() addsimps [extend_set_INTER_distrib]) 1);


183 
qed "extend_JN";


184 
Addsimps [extend_JN];


185 

6297

186 

6536

187 
(*** Safety: co, stable ***)

6297

188 

6536

189 
Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \


190 
\ (F : A co B)";

6297

191 
by (simp_tac (simpset() addsimps [constrains_def]) 1);


192 
qed "extend_constrains";


193 


194 
Goal "(extend h F : stable (extend_set h A)) = (F : stable A)";


195 
by (asm_simp_tac (simpset() addsimps [stable_def, extend_constrains]) 1);


196 
qed "extend_stable";


197 


198 
Goal "(extend h F : invariant (extend_set h A)) = (F : invariant A)";


199 
by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);


200 
qed "extend_invariant";


201 

6536

202 
(** Substitution Axiom versions: Co, Stable **)

6297

203 


204 
Goal "p : reachable (extend h F) ==> f p : reachable F";


205 
by (etac reachable.induct 1);


206 
by (auto_tac


207 
(claset() addIs reachable.intrs,


208 
simpset() addsimps [extend_set_def, extend_act_def, image_iff]));


209 
qed "reachable_extend_f";


210 


211 
Goal "h(s,y) : reachable (extend h F) ==> s : reachable F";


212 
by (force_tac (claset() addSDs [reachable_extend_f], simpset()) 1);


213 
qed "h_reachable_extend";


214 


215 
Goalw [extend_set_def]


216 
"reachable (extend h F) = extend_set h (reachable F)";


217 
by (rtac equalityI 1);


218 
by (force_tac (claset() addIs [h_f_g_eq RS sym]


219 
addSDs [reachable_extend_f],


220 
simpset()) 1);


221 
by (Clarify_tac 1);


222 
by (etac reachable.induct 1);


223 
by (ALLGOALS (force_tac (claset() addIs reachable.intrs,


224 
simpset())));


225 
qed "reachable_extend_eq";


226 

6536

227 
Goal "(extend h F : (extend_set h A) Co (extend_set h B)) = \


228 
\ (F : A Co B)";

6297

229 
by (simp_tac


230 
(simpset() addsimps [Constrains_def, reachable_extend_eq,


231 
extend_constrains, extend_set_Int_distrib RS sym]) 1);


232 
qed "extend_Constrains";


233 


234 
Goal "(extend h F : Stable (extend_set h A)) = (F : Stable A)";


235 
by (simp_tac (simpset() addsimps [Stable_def, extend_Constrains]) 1);


236 
qed "extend_Stable";


237 

6647

238 
Goal "(extend h F : Always (extend_set h A)) = (F : Always A)";


239 
by (asm_simp_tac (simpset() addsimps [Always_def, extend_Stable]) 1);


240 
qed "extend_Always";


241 

6297

242 


243 
(*** Progress: transient, ensures ***)


244 


245 
Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";


246 
by (auto_tac (claset(),


247 
simpset() addsimps [transient_def, extend_set_subset_Compl_eq,


248 
Domain_extend_act]));


249 
qed "extend_transient";


250 

6536

251 
Goal "(extend h F : (extend_set h A) ensures (extend_set h B)) = \


252 
\ (F : A ensures B)";

6297

253 
by (simp_tac


254 
(simpset() addsimps [ensures_def, extend_constrains, extend_transient,


255 
extend_set_Un_distrib RS sym,


256 
extend_set_Diff_distrib RS sym]) 1);


257 
qed "extend_ensures";


258 

6536

259 
Goal "F : A leadsTo B \


260 
\ ==> extend h F : (extend_set h A) leadsTo (extend_set h B)";

6297

261 
by (etac leadsTo_induct 1);


262 
by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);


263 
by (blast_tac (claset() addIs [leadsTo_Trans]) 2);


264 
by (asm_simp_tac (simpset() addsimps [leadsTo_Basis, extend_ensures]) 1);


265 
qed "leadsTo_imp_extend_leadsTo";


266 


267 
(*** Proving the converse takes some doing! ***)


268 


269 
Goalw [slice_def] "slice (Union S) y = (UN x:S. slice x y)";


270 
by Auto_tac;


271 
qed "slice_Union";


272 


273 
Goalw [slice_def] "slice (extend_set h A) y = A";


274 
by Auto_tac;


275 
qed "slice_extend_set";


276 


277 
Goalw [slice_def] "f``A = (UN y. slice A y)";


278 
by Auto_tac;


279 
by (blast_tac (claset() addIs [f_h_eq RS sym]) 2);


280 
by (best_tac (claset() addIs [h_f_g_eq RS ssubst]) 1);


281 
qed "image_is_UN_slice";


282 


283 
Goalw [slice_def, transient_def]


284 
"extend h F : transient A ==> F : transient (slice A y)";


285 
by Auto_tac;


286 
by (rtac bexI 1);


287 
by Auto_tac;


288 
by (force_tac (claset(), simpset() addsimps [extend_act_def]) 1);


289 
qed "extend_transient_slice";


290 

6536

291 
Goal "extend h F : A ensures B ==> F : (slice A y) ensures (f `` B)";

6297

292 
by (full_simp_tac


293 
(simpset() addsimps [ensures_def, extend_constrains, extend_transient,


294 
image_Un RS sym,


295 
extend_set_Un_distrib RS sym,


296 
extend_set_Diff_distrib RS sym]) 1);


297 
by Safe_tac;


298 
by (full_simp_tac (simpset() addsimps [constrains_def, extend_act_def,


299 
extend_set_def]) 1);


300 
by (Clarify_tac 1);


301 
by (ball_tac 1);


302 
by (full_simp_tac (simpset() addsimps [slice_def, image_iff, Image_iff]) 1);


303 
by (force_tac (claset() addSIs [h_f_g_eq RS sym], simpset()) 1);


304 
(*transient*)


305 
by (dtac extend_transient_slice 1);


306 
by (etac transient_strengthen 1);


307 
by (force_tac (claset() addIs [f_h_eq RS sym],


308 
simpset() addsimps [slice_def]) 1);


309 
qed "extend_ensures_slice";


310 

6536

311 
Goal "ALL y. F : (slice B y) leadsTo CU ==> F : (f `` B) leadsTo CU";

6297

312 
by (simp_tac (simpset() addsimps [image_is_UN_slice]) 1);


313 
by (blast_tac (claset() addIs [leadsTo_UN]) 1);


314 
qed "leadsTo_slice_image";


315 


316 

6536

317 
Goal "extend h F : AU leadsTo BU \


318 
\ ==> ALL y. F : (slice AU y) leadsTo (f `` BU)";

6297

319 
by (etac leadsTo_induct 1);


320 
by (full_simp_tac (simpset() addsimps [slice_Union]) 3);


321 
by (blast_tac (claset() addIs [leadsTo_UN]) 3);


322 
by (blast_tac (claset() addIs [leadsTo_slice_image, leadsTo_Trans]) 2);


323 
by (blast_tac (claset() addIs [extend_ensures_slice, leadsTo_Basis]) 1);


324 
qed_spec_mp "extend_leadsTo_slice";


325 

6536

326 
Goal "(extend h F : (extend_set h A) leadsTo (extend_set h B)) = \


327 
\ (F : A leadsTo B)";

6297

328 
by Safe_tac;


329 
by (etac leadsTo_imp_extend_leadsTo 2);


330 
by (dtac extend_leadsTo_slice 1);


331 
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);

6647

332 
qed "extend_leadsto";

6297

333 

6536

334 
Goal "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) = \


335 
\ (F : A LeadsTo B)";

6454

336 
by (simp_tac


337 
(simpset() addsimps [LeadsTo_def, reachable_extend_eq,

6647

338 
extend_leadsto, extend_set_Int_distrib RS sym]) 1);

6454

339 
qed "extend_LeadsTo";


340 

6297

341 


342 
(*** guarantees properties ***)


343 


344 
Goalw [f_act_def, extend_act_def] "f_act (extend_act h act1) = act1";


345 
by (force_tac


346 
(claset() addSIs [rev_bexI],


347 
simpset() addsimps [image_iff]) 1);


348 
qed "f_act_extend_act";


349 
Addsimps [f_act_extend_act];


350 


351 
Goalw [extend_set_def]


352 
"f `` (extend_set h A Int B) = (f `` extend_set h A) Int (f``B)";


353 
by (force_tac (claset() addIs [h_f_g_eq RS sym], simpset()) 1);


354 
qed "image_extend_set_Int_eq";


355 


356 
Goal "(extend h F) Join G = extend h H ==> EX J. H = F Join J";


357 
by (etac program_equalityE 1);


358 
by (auto_tac (claset(), simpset() addsimps [Acts_Join]));


359 
by (res_inst_tac [("x", "mk_program(f``(Init G), f_act``Acts G)")] exI 1);


360 
by (rtac program_equalityI 1);


361 
(*Init*)


362 
by (REPEAT (dres_inst_tac [("f", "op `` f")] arg_cong 1));


363 
by (asm_full_simp_tac (simpset() addsimps [image_extend_set_Int_eq]) 1);


364 
(*Now for the Actions*)


365 
by (dres_inst_tac [("f", "op `` f_act")] arg_cong 1);


366 
by (asm_full_simp_tac


367 
(simpset() addsimps [Acts_Join, image_Un, image_compose RS sym, o_def]) 1);


368 
qed "extend_Join_eq_extend_D";


369 


370 
Goal "F : X guarantees Y \


371 
\ ==> extend h F : (extend h `` X) guarantees (extend h `` Y)";


372 
by (rtac guaranteesI 1);


373 
by Auto_tac;


374 
by (blast_tac (claset() addDs [extend_Join_eq_extend_D, guaranteesD]) 1);


375 
qed "guarantees_imp_extend_guarantees";


376 


377 
Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \


378 
\ ==> F : X guarantees Y";


379 
by (rtac guaranteesI 1);


380 
by (rewrite_goals_tac [guarantees_def, component_def]);


381 
by Auto_tac;


382 
by (dtac spec 1);


383 
by (dtac (mp RS mp) 1);


384 
by (Blast_tac 2);


385 
by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);


386 
by Auto_tac;


387 
qed "extend_guarantees_imp_guarantees";


388 


389 
Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) \


390 
\ = (F : X guarantees Y)";


391 
by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,


392 
extend_guarantees_imp_guarantees]) 1);


393 
qed "extend_guarantees_eq";


394 


395 


396 
Close_locale "Extend";
