969

1 
(* Title: HOL/ex/mt.ML


2 
ID: $Id$


3 
Author: Jacob Frost, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Based upon the article


7 
Robin Milner and Mads Tofte,


8 
Coinduction in Relational Semantics,


9 
Theoretical Computer Science 87 (1991), pages 209220.


10 


11 
Written up as


12 
Jacob Frost, A Case Study of Coinduction in Isabelle/HOL


13 
Report 308, Computer Lab, University of Cambridge (1993).


14 
*)


15 


16 
open MT;


17 


18 
val prems = goal MT.thy "~a:{b} ==> ~a=b";


19 
by (cut_facts_tac prems 1);


20 
by (rtac notI 1);


21 
by (dtac notE 1);


22 
by (hyp_subst_tac 1);


23 
by (rtac singletonI 1);


24 
by (assume_tac 1);


25 
qed "notsingletonI";


26 


27 
val prems = goalw MT.thy [Un_def]


28 
"[ c : A Un B; c : A & ~c : B ==> P; c : B ==> P ] ==> P";


29 
by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1;


30 
by (cut_facts_tac [excluded_middle] 1);be disjE 1;


31 
by (resolve_tac prems 1);br conjI 1;ba 1;ba 1;


32 
by (eresolve_tac prems 1);


33 
by (eresolve_tac prems 1);


34 
qed "UnSE";


35 


36 
(* ############################################################ *)


37 
(* Inference systems *)


38 
(* ############################################################ *)


39 


40 
val infsys_mono_tac =


41 
(rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN


42 
(rtac CollectI 1) THEN (dtac CollectD 1) THEN


43 
REPEAT


44 
( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN


45 
(REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)


46 
);


47 


48 
val prems = goal MT.thy "P a b ==> P (fst <a,b>) (snd <a,b>)";


49 
by (rtac (fst_conv RS ssubst) 1);


50 
by (rtac (snd_conv RS ssubst) 1);


51 
by (resolve_tac prems 1);


52 
qed "infsys_p1";


53 


54 
val prems = goal MT.thy "P (fst <a,b>) (snd <a,b>) ==> P a b";


55 
by (cut_facts_tac prems 1);


56 
by (dtac (fst_conv RS subst) 1);


57 
by (dtac (snd_conv RS subst) 1);


58 
by (assume_tac 1);


59 
qed "infsys_p2";


60 


61 
val prems = goal MT.thy


62 
"P a b c ==> P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>)";


63 
by (rtac (fst_conv RS ssubst) 1);


64 
by (rtac (fst_conv RS ssubst) 1);


65 
by (rtac (snd_conv RS ssubst) 1);


66 
by (rtac (snd_conv RS ssubst) 1);


67 
by (resolve_tac prems 1);


68 
qed "infsys_pp1";


69 


70 
val prems = goal MT.thy


71 
"P (fst(fst <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,c>) ==> P a b c";


72 
by (cut_facts_tac prems 1);


73 
by (dtac (fst_conv RS subst) 1);


74 
by (dtac (fst_conv RS subst) 1);


75 
by (dtac (snd_conv RS subst) 1);


76 
by (dtac (snd_conv RS subst) 1);


77 
by (assume_tac 1);


78 
qed "infsys_pp2";


79 


80 
(* ############################################################ *)


81 
(* Fixpoints *)


82 
(* ############################################################ *)


83 


84 
(* Least fixpoints *)


85 


86 
val prems = goal MT.thy "[ mono(f); x:f(lfp(f)) ] ==> x:lfp(f)";


87 
by (rtac subsetD 1);


88 
by (rtac lfp_lemma2 1);


89 
by (resolve_tac prems 1);brs prems 1;


90 
qed "lfp_intro2";


91 


92 
val prems = goal MT.thy


93 
" [ x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) ] ==> \


94 
\ P(x)";


95 
by (cut_facts_tac prems 1);


96 
by (resolve_tac prems 1);br subsetD 1;


97 
by (rtac lfp_lemma3 1);ba 1;ba 1;


98 
qed "lfp_elim2";


99 


100 
val prems = goal MT.thy


101 
" [ x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) ] ==> \


102 
\ P(x)";


103 
by (cut_facts_tac prems 1);


104 
by (etac induct 1);ba 1;


105 
by (eresolve_tac prems 1);


106 
qed "lfp_ind2";


107 


108 
(* Greatest fixpoints *)


109 


110 
(* Note : "[ x:S; S <= f(S Un gfp(f)); mono(f) ] ==> x:gfp(f)" *)


111 


112 
val [cih,monoh] = goal MT.thy "[ x:f({x} Un gfp(f)); mono(f) ] ==> x:gfp(f)";


113 
by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);


114 
by (rtac (monoh RS monoD) 1);


115 
by (rtac (UnE RS subsetI) 1);ba 1;


116 
by (fast_tac (set_cs addSIs [cih]) 1);


117 
by (rtac (monoh RS monoD RS subsetD) 1);


118 
by (rtac Un_upper2 1);


119 
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);


120 
qed "gfp_coind2";


121 


122 
val [gfph,monoh,caseh] = goal MT.thy


123 
"[ x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) ] ==> P(x)";


124 
by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1;


125 
qed "gfp_elim2";


126 


127 
(* ############################################################ *)


128 
(* Expressions *)


129 
(* ############################################################ *)


130 


131 
val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];


132 


133 
val e_disjs =


134 
[ e_disj_const_var,


135 
e_disj_const_fn,


136 
e_disj_const_fix,


137 
e_disj_const_app,


138 
e_disj_var_fn,


139 
e_disj_var_fix,


140 
e_disj_var_app,


141 
e_disj_fn_fix,


142 
e_disj_fn_app,


143 
e_disj_fix_app


144 
];


145 


146 
val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);


147 
val e_disj_se = (e_disj_si RL [notE]);


148 


149 
fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;


150 


151 
(* ############################################################ *)


152 
(* Values *)


153 
(* ############################################################ *)


154 


155 
val v_disjs = [v_disj_const_clos];


156 
val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);


157 
val v_disj_se = (v_disj_si RL [notE]);


158 


159 
val v_injs = [v_const_inj, v_clos_inj];


160 


161 
fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;


162 


163 
(* ############################################################ *)


164 
(* Evaluations *)


165 
(* ############################################################ *)


166 


167 
(* Monotonicity of eval_fun *)


168 


169 
goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";


170 
by infsys_mono_tac;


171 
qed "eval_fun_mono";


172 


173 
(* Introduction rules *)


174 


175 
goalw MT.thy [eval_def, eval_rel_def] "ve  e_const(c) > v_const(c)";


176 
by (rtac lfp_intro2 1);


177 
by (rtac eval_fun_mono 1);


178 
by (rewtac eval_fun_def);


179 
by (rtac CollectI 1);br disjI1 1;


180 
by (fast_tac HOL_cs 1);


181 
qed "eval_const";


182 


183 
val prems = goalw MT.thy [eval_def, eval_rel_def]


184 
"ev:ve_dom(ve) ==> ve  e_var(ev) > ve_app ve ev";


185 
by (cut_facts_tac prems 1);


186 
by (rtac lfp_intro2 1);


187 
by (rtac eval_fun_mono 1);


188 
by (rewtac eval_fun_def);


189 
by (rtac CollectI 1);br disjI2 1;br disjI1 1;


190 
by (fast_tac HOL_cs 1);


191 
qed "eval_var";


192 


193 
val prems = goalw MT.thy [eval_def, eval_rel_def]


194 
"ve  fn ev => e > v_clos(<ev,e,ve>)";


195 
by (cut_facts_tac prems 1);


196 
by (rtac lfp_intro2 1);


197 
by (rtac eval_fun_mono 1);


198 
by (rewtac eval_fun_def);


199 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;


200 
by (fast_tac HOL_cs 1);


201 
qed "eval_fn";


202 


203 
val prems = goalw MT.thy [eval_def, eval_rel_def]


204 
" cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \


205 
\ ve  fix ev2(ev1) = e > v_clos(cl)";


206 
by (cut_facts_tac prems 1);


207 
by (rtac lfp_intro2 1);


208 
by (rtac eval_fun_mono 1);


209 
by (rewtac eval_fun_def);


210 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;


211 
by (fast_tac HOL_cs 1);


212 
qed "eval_fix";


213 


214 
val prems = goalw MT.thy [eval_def, eval_rel_def]


215 
" [ ve  e1 > v_const(c1); ve  e2 > v_const(c2) ] ==> \


216 
\ ve  e1 @ e2 > v_const(c_app c1 c2)";


217 
by (cut_facts_tac prems 1);


218 
by (rtac lfp_intro2 1);


219 
by (rtac eval_fun_mono 1);


220 
by (rewtac eval_fun_def);


221 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;


222 
by (fast_tac HOL_cs 1);


223 
qed "eval_app1";


224 


225 
val prems = goalw MT.thy [eval_def, eval_rel_def]


226 
" [ ve  e1 > v_clos(<xm,em,vem>); \


227 
\ ve  e2 > v2; \


228 
\ vem + {xm > v2}  em > v \


229 
\ ] ==> \


230 
\ ve  e1 @ e2 > v";


231 
by (cut_facts_tac prems 1);


232 
by (rtac lfp_intro2 1);


233 
by (rtac eval_fun_mono 1);


234 
by (rewtac eval_fun_def);


235 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;


236 
by (fast_tac HOL_cs 1);


237 
qed "eval_app2";


238 


239 
(* Strong elimination, induction on evaluations *)


240 


241 
val prems = goalw MT.thy [eval_def, eval_rel_def]


242 
" [ ve  e > v; \


243 
\ !!ve c. P(<<ve,e_const(c)>,v_const(c)>); \


244 
\ !!ev ve. ev:ve_dom(ve) ==> P(<<ve,e_var(ev)>,ve_app ve ev>); \


245 
\ !!ev ve e. P(<<ve,fn ev => e>,v_clos(<ev,e,ve>)>); \


246 
\ !!ev1 ev2 ve cl e. \


247 
\ cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \


248 
\ P(<<ve,fix ev2(ev1) = e>,v_clos(cl)>); \


249 
\ !!ve c1 c2 e1 e2. \


250 
\ [ P(<<ve,e1>,v_const(c1)>); P(<<ve,e2>,v_const(c2)>) ] ==> \


251 
\ P(<<ve,e1 @ e2>,v_const(c_app c1 c2)>); \


252 
\ !!ve vem xm e1 e2 em v v2. \


253 
\ [ P(<<ve,e1>,v_clos(<xm,em,vem>)>); \


254 
\ P(<<ve,e2>,v2>); \


255 
\ P(<<vem + {xm > v2},em>,v>) \


256 
\ ] ==> \


257 
\ P(<<ve,e1 @ e2>,v>) \


258 
\ ] ==> \


259 
\ P(<<ve,e>,v>)";


260 
by (resolve_tac (prems RL [lfp_ind2]) 1);


261 
by (rtac eval_fun_mono 1);


262 
by (rewtac eval_fun_def);


263 
by (dtac CollectD 1);


264 
by (safe_tac HOL_cs);


265 
by (ALLGOALS (resolve_tac prems));


266 
by (ALLGOALS (fast_tac set_cs));


267 
qed "eval_ind0";


268 


269 
val prems = goal MT.thy


270 
" [ ve  e > v; \


271 
\ !!ve c. P ve (e_const c) (v_const c); \


272 
\ !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \


273 
\ !!ev ve e. P ve (fn ev => e) (v_clos <ev,e,ve>); \


274 
\ !!ev1 ev2 ve cl e. \


275 
\ cl = < ev1, e, ve + {ev2 > v_clos(cl)} > ==> \


276 
\ P ve (fix ev2(ev1) = e) (v_clos cl); \


277 
\ !!ve c1 c2 e1 e2. \


278 
\ [ P ve e1 (v_const c1); P ve e2 (v_const c2) ] ==> \


279 
\ P ve (e1 @ e2) (v_const(c_app c1 c2)); \


280 
\ !!ve vem evm e1 e2 em v v2. \


281 
\ [ P ve e1 (v_clos <evm,em,vem>); \


282 
\ P ve e2 v2; \


283 
\ P (vem + {evm > v2}) em v \


284 
\ ] ==> P ve (e1 @ e2) v \


285 
\ ] ==> P ve e v";


286 
by (res_inst_tac [("P","P")] infsys_pp2 1);


287 
by (rtac eval_ind0 1);


288 
by (ALLGOALS (rtac infsys_pp1));


289 
by (ALLGOALS (resolve_tac prems));


290 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));


291 
qed "eval_ind";


292 


293 
(* ############################################################ *)


294 
(* Elaborations *)


295 
(* ############################################################ *)


296 


297 
goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";


298 
by infsys_mono_tac;


299 
qed "elab_fun_mono";


300 


301 
(* Introduction rules *)


302 


303 
val prems = goalw MT.thy [elab_def, elab_rel_def]


304 
"c isof ty ==> te  e_const(c) ===> ty";


305 
by (cut_facts_tac prems 1);


306 
by (rtac lfp_intro2 1);


307 
by (rtac elab_fun_mono 1);


308 
by (rewtac elab_fun_def);


309 
by (rtac CollectI 1);br disjI1 1;


310 
by (fast_tac HOL_cs 1);


311 
qed "elab_const";


312 


313 
val prems = goalw MT.thy [elab_def, elab_rel_def]


314 
"x:te_dom(te) ==> te  e_var(x) ===> te_app te x";


315 
by (cut_facts_tac prems 1);


316 
by (rtac lfp_intro2 1);


317 
by (rtac elab_fun_mono 1);


318 
by (rewtac elab_fun_def);


319 
by (rtac CollectI 1);br disjI2 1;br disjI1 1;


320 
by (fast_tac HOL_cs 1);


321 
qed "elab_var";


322 


323 
val prems = goalw MT.thy [elab_def, elab_rel_def]


324 
"te + {x => ty1}  e ===> ty2 ==> te  fn x => e ===> ty1>ty2";


325 
by (cut_facts_tac prems 1);


326 
by (rtac lfp_intro2 1);


327 
by (rtac elab_fun_mono 1);


328 
by (rewtac elab_fun_def);


329 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1;


330 
by (fast_tac HOL_cs 1);


331 
qed "elab_fn";


332 


333 
val prems = goalw MT.thy [elab_def, elab_rel_def]


334 
" te + {f => ty1>ty2} + {x => ty1}  e ===> ty2 ==> \


335 
\ te  fix f(x) = e ===> ty1>ty2";


336 
by (cut_facts_tac prems 1);


337 
by (rtac lfp_intro2 1);


338 
by (rtac elab_fun_mono 1);


339 
by (rewtac elab_fun_def);


340 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1;


341 
by (fast_tac HOL_cs 1);


342 
qed "elab_fix";


343 


344 
val prems = goalw MT.thy [elab_def, elab_rel_def]


345 
" [ te  e1 ===> ty1>ty2; te  e2 ===> ty1 ] ==> \


346 
\ te  e1 @ e2 ===> ty2";


347 
by (cut_facts_tac prems 1);


348 
by (rtac lfp_intro2 1);


349 
by (rtac elab_fun_mono 1);


350 
by (rewtac elab_fun_def);


351 
by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;


352 
by (fast_tac HOL_cs 1);


353 
qed "elab_app";


354 


355 
(* Strong elimination, induction on elaborations *)


356 


357 
val prems = goalw MT.thy [elab_def, elab_rel_def]


358 
" [ te  e ===> t; \


359 
\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \


360 
\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \


361 
\ !!te x e t1 t2. \


362 
\ [ te + {x => t1}  e ===> t2; P(<<te + {x => t1},e>,t2>) ] ==> \


363 
\ P(<<te,fn x => e>,t1>t2>); \


364 
\ !!te f x e t1 t2. \


365 
\ [ te + {f => t1>t2} + {x => t1}  e ===> t2; \


366 
\ P(<<te + {f => t1>t2} + {x => t1},e>,t2>) \


367 
\ ] ==> \


368 
\ P(<<te,fix f(x) = e>,t1>t2>); \


369 
\ !!te e1 e2 t1 t2. \


370 
\ [ te  e1 ===> t1>t2; P(<<te,e1>,t1>t2>); \


371 
\ te  e2 ===> t1; P(<<te,e2>,t1>) \


372 
\ ] ==> \


373 
\ P(<<te,e1 @ e2>,t2>) \


374 
\ ] ==> \


375 
\ P(<<te,e>,t>)";


376 
by (resolve_tac (prems RL [lfp_ind2]) 1);


377 
by (rtac elab_fun_mono 1);


378 
by (rewtac elab_fun_def);


379 
by (dtac CollectD 1);


380 
by (safe_tac HOL_cs);


381 
by (ALLGOALS (resolve_tac prems));


382 
by (ALLGOALS (fast_tac set_cs));


383 
qed "elab_ind0";


384 


385 
val prems = goal MT.thy


386 
" [ te  e ===> t; \


387 
\ !!te c t. c isof t ==> P te (e_const c) t; \


388 
\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \


389 
\ !!te x e t1 t2. \


390 
\ [ te + {x => t1}  e ===> t2; P (te + {x => t1}) e t2 ] ==> \


391 
\ P te (fn x => e) (t1>t2); \


392 
\ !!te f x e t1 t2. \


393 
\ [ te + {f => t1>t2} + {x => t1}  e ===> t2; \


394 
\ P (te + {f => t1>t2} + {x => t1}) e t2 \


395 
\ ] ==> \


396 
\ P te (fix f(x) = e) (t1>t2); \


397 
\ !!te e1 e2 t1 t2. \


398 
\ [ te  e1 ===> t1>t2; P te e1 (t1>t2); \


399 
\ te  e2 ===> t1; P te e2 t1 \


400 
\ ] ==> \


401 
\ P te (e1 @ e2) t2 \


402 
\ ] ==> \


403 
\ P te e t";


404 
by (res_inst_tac [("P","P")] infsys_pp2 1);


405 
by (rtac elab_ind0 1);


406 
by (ALLGOALS (rtac infsys_pp1));


407 
by (ALLGOALS (resolve_tac prems));


408 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));


409 
qed "elab_ind";


410 


411 
(* Weak elimination, case analysis on elaborations *)


412 


413 
val prems = goalw MT.thy [elab_def, elab_rel_def]


414 
" [ te  e ===> t; \


415 
\ !!te c t. c isof t ==> P(<<te,e_const(c)>,t>); \


416 
\ !!te x. x:te_dom(te) ==> P(<<te,e_var(x)>,te_app te x>); \


417 
\ !!te x e t1 t2. \


418 
\ te + {x => t1}  e ===> t2 ==> P(<<te,fn x => e>,t1>t2>); \


419 
\ !!te f x e t1 t2. \


420 
\ te + {f => t1>t2} + {x => t1}  e ===> t2 ==> \


421 
\ P(<<te,fix f(x) = e>,t1>t2>); \


422 
\ !!te e1 e2 t1 t2. \


423 
\ [ te  e1 ===> t1>t2; te  e2 ===> t1 ] ==> \


424 
\ P(<<te,e1 @ e2>,t2>) \


425 
\ ] ==> \


426 
\ P(<<te,e>,t>)";


427 
by (resolve_tac (prems RL [lfp_elim2]) 1);


428 
by (rtac elab_fun_mono 1);


429 
by (rewtac elab_fun_def);


430 
by (dtac CollectD 1);


431 
by (safe_tac HOL_cs);


432 
by (ALLGOALS (resolve_tac prems));


433 
by (ALLGOALS (fast_tac set_cs));


434 
qed "elab_elim0";


435 


436 
val prems = goal MT.thy


437 
" [ te  e ===> t; \


438 
\ !!te c t. c isof t ==> P te (e_const c) t; \


439 
\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \


440 
\ !!te x e t1 t2. \


441 
\ te + {x => t1}  e ===> t2 ==> P te (fn x => e) (t1>t2); \


442 
\ !!te f x e t1 t2. \


443 
\ te + {f => t1>t2} + {x => t1}  e ===> t2 ==> \


444 
\ P te (fix f(x) = e) (t1>t2); \


445 
\ !!te e1 e2 t1 t2. \


446 
\ [ te  e1 ===> t1>t2; te  e2 ===> t1 ] ==> \


447 
\ P te (e1 @ e2) t2 \


448 
\ ] ==> \


449 
\ P te e t";


450 
by (res_inst_tac [("P","P")] infsys_pp2 1);


451 
by (rtac elab_elim0 1);


452 
by (ALLGOALS (rtac infsys_pp1));


453 
by (ALLGOALS (resolve_tac prems));


454 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));


455 
qed "elab_elim";


456 


457 
(* Elimination rules for each expression *)


458 


459 
fun elab_e_elim_tac p =


460 
( (rtac elab_elim 1) THEN


461 
(resolve_tac p 1) THEN


462 
(REPEAT (fast_tac (e_ext_cs HOL_cs) 1))


463 
);


464 


465 
val prems = goal MT.thy "te  e ===> t ==> (e = e_const(c) > c isof t)";


466 
by (elab_e_elim_tac prems);


467 
qed "elab_const_elim_lem";


468 


469 
val prems = goal MT.thy "te  e_const(c) ===> t ==> c isof t";


470 
by (cut_facts_tac prems 1);


471 
by (dtac elab_const_elim_lem 1);


472 
by (fast_tac prop_cs 1);


473 
qed "elab_const_elim";


474 


475 
val prems = goal MT.thy


476 
"te  e ===> t ==> (e = e_var(x) > t=te_app te x & x:te_dom(te))";


477 
by (elab_e_elim_tac prems);


478 
qed "elab_var_elim_lem";


479 


480 
val prems = goal MT.thy


481 
"te  e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";


482 
by (cut_facts_tac prems 1);


483 
by (dtac elab_var_elim_lem 1);


484 
by (fast_tac prop_cs 1);


485 
qed "elab_var_elim";


486 


487 
val prems = goal MT.thy


488 
" te  e ===> t ==> \


489 
\ ( e = fn x1 => e1 > \


490 
\ (? t1 t2.t=t_fun t1 t2 & te + {x1 => t1}  e1 ===> t2) \


491 
\ )";


492 
by (elab_e_elim_tac prems);


493 
qed "elab_fn_elim_lem";


494 


495 
val prems = goal MT.thy


496 
" te  fn x1 => e1 ===> t ==> \


497 
\ (? t1 t2. t=t1>t2 & te + {x1 => t1}  e1 ===> t2)";


498 
by (cut_facts_tac prems 1);


499 
by (dtac elab_fn_elim_lem 1);


500 
by (fast_tac prop_cs 1);


501 
qed "elab_fn_elim";


502 


503 
val prems = goal MT.thy


504 
" te  e ===> t ==> \


505 
\ (e = fix f(x) = e1 > \


506 
\ (? t1 t2. t=t1>t2 & te + {f => t1>t2} + {x => t1}  e1 ===> t2))";


507 
by (elab_e_elim_tac prems);


508 
qed "elab_fix_elim_lem";


509 


510 
val prems = goal MT.thy


511 
" te  fix ev1(ev2) = e1 ===> t ==> \


512 
\ (? t1 t2. t=t1>t2 & te + {ev1 => t1>t2} + {ev2 => t1}  e1 ===> t2)";


513 
by (cut_facts_tac prems 1);


514 
by (dtac elab_fix_elim_lem 1);


515 
by (fast_tac prop_cs 1);


516 
qed "elab_fix_elim";


517 


518 
val prems = goal MT.thy


519 
" te  e ===> t2 ==> \


520 
\ (e = e1 @ e2 > (? t1 . te  e1 ===> t1>t2 & te  e2 ===> t1))";


521 
by (elab_e_elim_tac prems);


522 
qed "elab_app_elim_lem";


523 


524 
val prems = goal MT.thy


525 
"te  e1 @ e2 ===> t2 ==> (? t1 . te  e1 ===> t1>t2 & te  e2 ===> t1)";


526 
by (cut_facts_tac prems 1);


527 
by (dtac elab_app_elim_lem 1);


528 
by (fast_tac prop_cs 1);


529 
qed "elab_app_elim";


530 


531 
(* ############################################################ *)


532 
(* The extended correspondence relation *)


533 
(* ############################################################ *)


534 


535 
(* Monotonicity of hasty_fun *)


536 


537 
goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";


538 
by infsys_mono_tac;


539 
bind_thm("mono_hasty_fun", result());


540 


541 
(*


542 
Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it


543 
enjoys two strong indtroduction (coinduction) rules and an elimination rule.


544 
*)


545 


546 
(* First strong indtroduction (coinduction) rule for hasty_rel *)


547 


548 
val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> <v_const(c),t> : hasty_rel";


549 
by (cut_facts_tac prems 1);


550 
by (rtac gfp_coind2 1);


551 
by (rewtac MT.hasty_fun_def);


552 
by (rtac CollectI 1);br disjI1 1;


553 
by (fast_tac HOL_cs 1);


554 
by (rtac mono_hasty_fun 1);


555 
qed "hasty_rel_const_coind";


556 


557 
(* Second strong introduction (coinduction) rule for hasty_rel *)


558 


559 
val prems = goalw MT.thy [hasty_rel_def]


560 
" [ te  fn ev => e ===> t; \


561 
\ ve_dom(ve) = te_dom(te); \


562 
\ ! ev1. \


563 
\ ev1:ve_dom(ve) > \


564 
\ <ve_app ve ev1,te_app te ev1> : {<v_clos(<ev,e,ve>),t>} Un hasty_rel \


565 
\ ] ==> \


566 
\ <v_clos(<ev,e,ve>),t> : hasty_rel";


567 
by (cut_facts_tac prems 1);


568 
by (rtac gfp_coind2 1);


569 
by (rewtac hasty_fun_def);


570 
by (rtac CollectI 1);br disjI2 1;


571 
by (fast_tac HOL_cs 1);


572 
by (rtac mono_hasty_fun 1);


573 
qed "hasty_rel_clos_coind";


574 


575 
(* Elimination rule for hasty_rel *)


576 


577 
val prems = goalw MT.thy [hasty_rel_def]


578 
" [ !! c t.c isof t ==> P(<v_const(c),t>); \


579 
\ !! te ev e t ve. \


580 
\ [ te  fn ev => e ===> t; \


581 
\ ve_dom(ve) = te_dom(te); \


582 
\ !ev1.ev1:ve_dom(ve) > <ve_app ve ev1,te_app te ev1> : hasty_rel \


583 
\ ] ==> P(<v_clos(<ev,e,ve>),t>); \


584 
\ <v,t> : hasty_rel \


585 
\ ] ==> P(<v,t>)";


586 
by (cut_facts_tac prems 1);


587 
by (etac gfp_elim2 1);


588 
by (rtac mono_hasty_fun 1);


589 
by (rewtac hasty_fun_def);


590 
by (dtac CollectD 1);


591 
by (fold_goals_tac [hasty_fun_def]);


592 
by (safe_tac HOL_cs);


593 
by (ALLGOALS (resolve_tac prems));


594 
by (ALLGOALS (fast_tac set_cs));


595 
qed "hasty_rel_elim0";


596 


597 
val prems = goal MT.thy


598 
" [ <v,t> : hasty_rel; \


599 
\ !! c t.c isof t ==> P (v_const c) t; \


600 
\ !! te ev e t ve. \


601 
\ [ te  fn ev => e ===> t; \


602 
\ ve_dom(ve) = te_dom(te); \


603 
\ !ev1.ev1:ve_dom(ve) > <ve_app ve ev1,te_app te ev1> : hasty_rel \


604 
\ ] ==> P (v_clos <ev,e,ve>) t \


605 
\ ] ==> P v t";


606 
by (res_inst_tac [("P","P")] infsys_p2 1);


607 
by (rtac hasty_rel_elim0 1);


608 
by (ALLGOALS (rtac infsys_p1));


609 
by (ALLGOALS (resolve_tac prems));


610 
by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));


611 
qed "hasty_rel_elim";


612 


613 
(* Introduction rules for hasty *)


614 


615 
val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";


616 
by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);


617 
qed "hasty_const";


618 


619 
val prems = goalw MT.thy [hasty_def,hasty_env_def]


620 
"te  fn ev => e ===> t & ve hastyenv te ==> v_clos(<ev,e,ve>) hasty t";


621 
by (cut_facts_tac prems 1);


622 
by (rtac hasty_rel_clos_coind 1);


623 
by (ALLGOALS (fast_tac set_cs));


624 
qed "hasty_clos";


625 


626 
(* Elimination on constants for hasty *)


627 


628 
val prems = goalw MT.thy [hasty_def]


629 
"v hasty t ==> (!c.(v = v_const(c) > c isof t))";


630 
by (cut_facts_tac prems 1);


631 
by (rtac hasty_rel_elim 1);


632 
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));


633 
qed "hasty_elim_const_lem";


634 


635 
val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";


636 
by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);


637 
by (fast_tac HOL_cs 1);


638 
qed "hasty_elim_const";


639 


640 
(* Elimination on closures for hasty *)


641 


642 
val prems = goalw MT.thy [hasty_env_def,hasty_def]


643 
" v hasty t ==> \


644 
\ ! x e ve. \


645 
\ v=v_clos(<x,e,ve>) > (? te.te  fn x => e ===> t & ve hastyenv te)";


646 
by (cut_facts_tac prems 1);


647 
by (rtac hasty_rel_elim 1);


648 
by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));


649 
qed "hasty_elim_clos_lem";


650 


651 
val prems = goal MT.thy


652 
"v_clos(<ev,e,ve>) hasty t ==> ? te.te  fn ev => e ===> t & ve hastyenv te ";


653 
by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);


654 
by (fast_tac HOL_cs 1);


655 
qed "hasty_elim_clos";


656 


657 
(* ############################################################ *)


658 
(* The pointwise extension of hasty to environments *)


659 
(* ############################################################ *)


660 


661 
val prems = goal MT.thy


662 
"[ ve hastyenv te; v hasty t ] ==> \


663 
\ ve + {ev > v} hastyenv te + {ev => t}";


664 
by (cut_facts_tac prems 1);


665 
by (SELECT_GOAL (rewtac hasty_env_def) 1);


666 
by (safe_tac HOL_cs);


667 
by (rtac (ve_dom_owr RS ssubst) 1);


668 
by (rtac (te_dom_owr RS ssubst) 1);


669 
by (etac subst 1);br refl 1;


670 


671 
by (dtac (ve_dom_owr RS subst) 1);back();back();back();


672 
by (etac UnSE 1);be conjE 1;


673 
by (dtac notsingletonI 1);bd not_sym 1;


674 
by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;


675 
by (rtac (te_app_owr2 RS ssubst) 1);ba 1;


676 
by (fast_tac HOL_cs 1);


677 
by (dtac singletonD 1);by (hyp_subst_tac 1);


678 


679 
by (rtac (ve_app_owr1 RS ssubst) 1);


680 
by (rtac (te_app_owr1 RS ssubst) 1);


681 
by (assume_tac 1);


682 
qed "hasty_env1";


683 


684 
(* ############################################################ *)


685 
(* The Consistency theorem *)


686 
(* ############################################################ *)


687 


688 
val prems = goal MT.thy


689 
"[ ve hastyenv te ; te  e_const(c) ===> t ] ==> v_const(c) hasty t";


690 
by (cut_facts_tac prems 1);


691 
by (dtac elab_const_elim 1);


692 
by (etac hasty_const 1);


693 
qed "consistency_const";


694 


695 
val prems = goalw MT.thy [hasty_env_def]


696 
" [ ev : ve_dom(ve); ve hastyenv te ; te  e_var(ev) ===> t ] ==> \


697 
\ ve_app ve ev hasty t";


698 
by (cut_facts_tac prems 1);


699 
by (dtac elab_var_elim 1);


700 
by (fast_tac HOL_cs 1);


701 
qed "consistency_var";


702 


703 
val prems = goal MT.thy


704 
" [ ve hastyenv te ; te  fn ev => e ===> t ] ==> \


705 
\ v_clos(< ev, e, ve >) hasty t";


706 
by (cut_facts_tac prems 1);


707 
by (rtac hasty_clos 1);


708 
by (fast_tac prop_cs 1);


709 
qed "consistency_fn";


710 


711 
val prems = goalw MT.thy [hasty_env_def,hasty_def]


712 
" [ cl = < ev1, e, ve + { ev2 > v_clos(cl) } >; \


713 
\ ve hastyenv te ; \


714 
\ te  fix ev2 ev1 = e ===> t \


715 
\ ] ==> \


716 
\ v_clos(cl) hasty t";


717 
by (cut_facts_tac prems 1);


718 
by (dtac elab_fix_elim 1);


719 
by (safe_tac HOL_cs);


720 
by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN


721 
(rtac hasty_rel_clos_coind 1));


722 
by (etac elab_fn 1);


723 


724 
by (rtac (ve_dom_owr RS ssubst) 1);


725 
by (rtac (te_dom_owr RS ssubst) 1);


726 
by ((etac subst 1) THEN (rtac refl 1));


727 


728 
by (rtac (ve_dom_owr RS ssubst) 1);


729 
by (safe_tac HOL_cs);


730 
by (dtac (Un_commute RS subst) 1);


731 
by (etac UnSE 1);


732 


733 
by (safe_tac HOL_cs);


734 
by (dtac notsingletonI 1);bd not_sym 1;


735 
by (rtac (ve_app_owr2 RS ssubst) 1);ba 1;


736 
by (rtac (te_app_owr2 RS ssubst) 1);ba 1;


737 
by (fast_tac set_cs 1);


738 


739 
by (etac singletonE 1);


740 
by (hyp_subst_tac 1);


741 
by (rtac (ve_app_owr1 RS ssubst) 1);


742 
by (rtac (te_app_owr1 RS ssubst) 1);


743 
by (etac subst 1);


744 
by (fast_tac set_cs 1);


745 
qed "consistency_fix";


746 


747 
val prems = goal MT.thy


748 
" [ ! t te. ve hastyenv te > te  e1 ===> t > v_const(c1) hasty t; \


749 
\ ! t te. ve hastyenv te > te  e2 ===> t > v_const(c2) hasty t; \


750 
\ ve hastyenv te ; te  e1 @ e2 ===> t \


751 
\ ] ==> \


752 
\ v_const(c_app c1 c2) hasty t";


753 
by (cut_facts_tac prems 1);


754 
by (dtac elab_app_elim 1);


755 
by (safe_tac HOL_cs);


756 
by (rtac hasty_const 1);


757 
by (rtac isof_app 1);


758 
by (rtac hasty_elim_const 1);


759 
by (fast_tac HOL_cs 1);


760 
by (rtac hasty_elim_const 1);


761 
by (fast_tac HOL_cs 1);


762 
qed "consistency_app1";


763 


764 
val prems = goal MT.thy


765 
" [ ! t te. \


766 
\ ve hastyenv te > \


767 
\ te  e1 ===> t > v_clos(<evm, em, vem>) hasty t; \


768 
\ ! t te. ve hastyenv te > te  e2 ===> t > v2 hasty t; \


769 
\ ! t te. \


770 
\ vem + { evm > v2 } hastyenv te > te  em ===> t > v hasty t; \


771 
\ ve hastyenv te ; \


772 
\ te  e1 @ e2 ===> t \


773 
\ ] ==> \


774 
\ v hasty t";


775 
by (cut_facts_tac prems 1);


776 
by (dtac elab_app_elim 1);


777 
by (safe_tac HOL_cs);


778 
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;


779 
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1;


780 
by (dtac hasty_elim_clos 1);


781 
by (safe_tac HOL_cs);


782 
by (dtac elab_fn_elim 1);


783 
by (safe_tac HOL_cs);


784 
by (dtac t_fun_inj 1);


785 
by (safe_tac prop_cs);


786 
by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));


787 
qed "consistency_app2";


788 


789 
val prems = goal MT.thy


790 
"ve  e > v ==> (! t te. ve hastyenv te > te  e ===> t > v hasty t)";


791 


792 
(* Proof by induction on the structure of evaluations *)


793 


794 
by (resolve_tac (prems RL [eval_ind]) 1);


795 
by (safe_tac HOL_cs);


796 


797 
by (rtac consistency_const 1);ba 1;ba 1;


798 
by (rtac consistency_var 1);ba 1;ba 1;ba 1;


799 
by (rtac consistency_fn 1);ba 1;ba 1;


800 
by (rtac consistency_fix 1);ba 1;ba 1;ba 1;


801 
by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1;


802 
by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1;


803 
qed "consistency";


804 


805 
(* ############################################################ *)


806 
(* The Basic Consistency theorem *)


807 
(* ############################################################ *)


808 


809 
val prems = goalw MT.thy [isof_env_def,hasty_env_def]


810 
"ve isofenv te ==> ve hastyenv te";


811 
by (cut_facts_tac prems 1);


812 
by (safe_tac HOL_cs);


813 
by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1;


814 
by (dtac hasty_const 1);


815 
by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1));


816 
qed "basic_consistency_lem";


817 


818 
val prems = goal MT.thy


819 
"[ ve isofenv te; ve  e > v_const(c); te  e ===> t ] ==> c isof t";


820 
by (cut_facts_tac prems 1);


821 
by (rtac hasty_elim_const 1);


822 
by (dtac consistency 1);


823 
by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);


824 
qed "basic_consistency";


825 


826 
