1.1 --- a/src/HOL/IsaMakefile Sat Aug 18 13:32:28 2007 +0200
1.2 +++ b/src/HOL/IsaMakefile Sat Aug 18 17:42:38 2007 +0200
1.3 @@ -658,8 +658,7 @@
1.4 ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
1.5 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
1.6 ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
1.7 - ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy \
1.8 - ex/LocaleTest2.thy ex/MT.ML \
1.9 + ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
1.10 ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
1.11 ex/NatSum.thy ex/NBE.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
1.12 ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
2.1 --- a/src/HOL/ex/MT.ML Sat Aug 18 13:32:28 2007 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,737 +0,0 @@
2.4 -(* Title: HOL/ex/MT.ML
2.5 - ID: $Id$
2.6 - Author: Jacob Frost, Cambridge University Computer Laboratory
2.7 - Copyright 1993 University of Cambridge
2.8 -
2.9 -Based upon the article
2.10 - Robin Milner and Mads Tofte,
2.11 - Co-induction in Relational Semantics,
2.12 - Theoretical Computer Science 87 (1991), pages 209-220.
2.13 -
2.14 -Written up as
2.15 - Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
2.16 - Report 308, Computer Lab, University of Cambridge (1993).
2.17 -
2.18 -NEEDS TO USE INDUCTIVE DEFS PACKAGE
2.19 -*)
2.20 -
2.21 -(* ############################################################ *)
2.22 -(* Inference systems *)
2.23 -(* ############################################################ *)
2.24 -
2.25 -val lfp_lemma2 = thm "lfp_lemma2";
2.26 -val lfp_lemma3 = thm "lfp_lemma3";
2.27 -val gfp_lemma2 = thm "gfp_lemma2";
2.28 -val gfp_lemma3 = thm "gfp_lemma3";
2.29 -
2.30 -val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
2.31 -
2.32 -val prems = goal (the_context ()) "P a b ==> P (fst (a,b)) (snd (a,b))";
2.33 -by (simp_tac (simpset() addsimps prems) 1);
2.34 -qed "infsys_p1";
2.35 -
2.36 -Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
2.37 -by (Asm_full_simp_tac 1);
2.38 -qed "infsys_p2";
2.39 -
2.40 -Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
2.41 -by (Asm_full_simp_tac 1);
2.42 -qed "infsys_pp1";
2.43 -
2.44 -Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
2.45 -by (Asm_full_simp_tac 1);
2.46 -qed "infsys_pp2";
2.47 -
2.48 -(* ############################################################ *)
2.49 -(* Fixpoints *)
2.50 -(* ############################################################ *)
2.51 -
2.52 -(* Least fixpoints *)
2.53 -
2.54 -val prems = goal (the_context ()) "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
2.55 -by (rtac subsetD 1);
2.56 -by (rtac lfp_lemma2 1);
2.57 -by (resolve_tac prems 1);
2.58 -by (resolve_tac prems 1);
2.59 -qed "lfp_intro2";
2.60 -
2.61 -val prems = goal (the_context ())
2.62 - " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
2.63 -\ P(x)";
2.64 -by (cut_facts_tac prems 1);
2.65 -by (resolve_tac prems 1);
2.66 -by (rtac subsetD 1);
2.67 -by (rtac lfp_lemma3 1);
2.68 -by (assume_tac 1);
2.69 -by (assume_tac 1);
2.70 -qed "lfp_elim2";
2.71 -
2.72 -val prems = goal (the_context ())
2.73 - " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
2.74 -\ P(x)";
2.75 -by (cut_facts_tac prems 1);
2.76 -by (etac (thm "lfp_induct_set") 1);
2.77 -by (assume_tac 1);
2.78 -by (eresolve_tac prems 1);
2.79 -qed "lfp_ind2";
2.80 -
2.81 -(* Greatest fixpoints *)
2.82 -
2.83 -(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
2.84 -
2.85 -val [cih,monoh] = goal (the_context ()) "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
2.86 -by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
2.87 -by (rtac (monoh RS @{thm monoD}) 1);
2.88 -by (rtac (UnE RS subsetI) 1);
2.89 -by (assume_tac 1);
2.90 -by (blast_tac (claset() addSIs [cih]) 1);
2.91 -by (rtac (monoh RS @{thm monoD} RS subsetD) 1);
2.92 -by (rtac (thm "Un_upper2") 1);
2.93 -by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
2.94 -qed "gfp_coind2";
2.95 -
2.96 -val [gfph,monoh,caseh] = goal (the_context ())
2.97 - "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
2.98 -by (rtac caseh 1);
2.99 -by (rtac subsetD 1);
2.100 -by (rtac gfp_lemma2 1);
2.101 -by (rtac monoh 1);
2.102 -by (rtac gfph 1);
2.103 -qed "gfp_elim2";
2.104 -
2.105 -(* ############################################################ *)
2.106 -(* Expressions *)
2.107 -(* ############################################################ *)
2.108 -
2.109 -val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
2.110 -
2.111 -val e_disjs =
2.112 - [ e_disj_const_var,
2.113 - e_disj_const_fn,
2.114 - e_disj_const_fix,
2.115 - e_disj_const_app,
2.116 - e_disj_var_fn,
2.117 - e_disj_var_fix,
2.118 - e_disj_var_app,
2.119 - e_disj_fn_fix,
2.120 - e_disj_fn_app,
2.121 - e_disj_fix_app
2.122 - ];
2.123 -
2.124 -val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
2.125 -val e_disj_se = (e_disj_si RL [notE]);
2.126 -
2.127 -fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
2.128 -
2.129 -(* ############################################################ *)
2.130 -(* Values *)
2.131 -(* ############################################################ *)
2.132 -
2.133 -val v_disjs = [v_disj_const_clos];
2.134 -val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
2.135 -val v_disj_se = (v_disj_si RL [notE]);
2.136 -
2.137 -val v_injs = [v_const_inj, v_clos_inj];
2.138 -
2.139 -fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
2.140 -
2.141 -(* ############################################################ *)
2.142 -(* Evaluations *)
2.143 -(* ############################################################ *)
2.144 -
2.145 -(* Monotonicity of eval_fun *)
2.146 -
2.147 -Goalw [thm "mono_def", eval_fun_def] "mono(eval_fun)";
2.148 -by infsys_mono_tac;
2.149 -qed "eval_fun_mono";
2.150 -
2.151 -(* Introduction rules *)
2.152 -
2.153 -Goalw [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
2.154 -by (rtac lfp_intro2 1);
2.155 -by (rtac eval_fun_mono 1);
2.156 -by (rewtac eval_fun_def);
2.157 - (*Naughty! But the quantifiers are nested VERY deeply...*)
2.158 -by (blast_tac (claset() addSIs [exI]) 1);
2.159 -qed "eval_const";
2.160 -
2.161 -Goalw [eval_def, eval_rel_def]
2.162 - "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
2.163 -by (rtac lfp_intro2 1);
2.164 -by (rtac eval_fun_mono 1);
2.165 -by (rewtac eval_fun_def);
2.166 -by (blast_tac (claset() addSIs [exI]) 1);
2.167 -qed "eval_var2";
2.168 -
2.169 -Goalw [eval_def, eval_rel_def]
2.170 - "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
2.171 -by (rtac lfp_intro2 1);
2.172 -by (rtac eval_fun_mono 1);
2.173 -by (rewtac eval_fun_def);
2.174 -by (blast_tac (claset() addSIs [exI]) 1);
2.175 -qed "eval_fn";
2.176 -
2.177 -Goalw [eval_def, eval_rel_def]
2.178 - " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
2.179 -\ ve |- fix ev2(ev1) = e ---> v_clos(cl)";
2.180 -by (rtac lfp_intro2 1);
2.181 -by (rtac eval_fun_mono 1);
2.182 -by (rewtac eval_fun_def);
2.183 -by (blast_tac (claset() addSIs [exI]) 1);
2.184 -qed "eval_fix";
2.185 -
2.186 -Goalw [eval_def, eval_rel_def]
2.187 - " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
2.188 -\ ve |- e1 @@ e2 ---> v_const(c_app c1 c2)";
2.189 -by (rtac lfp_intro2 1);
2.190 -by (rtac eval_fun_mono 1);
2.191 -by (rewtac eval_fun_def);
2.192 -by (blast_tac (claset() addSIs [exI]) 1);
2.193 -qed "eval_app1";
2.194 -
2.195 -Goalw [eval_def, eval_rel_def]
2.196 - " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \
2.197 -\ ve |- e2 ---> v2; \
2.198 -\ vem + {xm |-> v2} |- em ---> v \
2.199 -\ |] ==> \
2.200 -\ ve |- e1 @@ e2 ---> v";
2.201 -by (rtac lfp_intro2 1);
2.202 -by (rtac eval_fun_mono 1);
2.203 -by (rewtac eval_fun_def);
2.204 -by (blast_tac (claset() addSIs [disjI2]) 1);
2.205 -qed "eval_app2";
2.206 -
2.207 -(* Strong elimination, induction on evaluations *)
2.208 -
2.209 -val prems = goalw (the_context ()) [eval_def, eval_rel_def]
2.210 - " [| ve |- e ---> v; \
2.211 -\ !!ve c. P(((ve,e_const(c)),v_const(c))); \
2.212 -\ !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
2.213 -\ !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
2.214 -\ !!ev1 ev2 ve cl e. \
2.215 -\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
2.216 -\ P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
2.217 -\ !!ve c1 c2 e1 e2. \
2.218 -\ [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
2.219 -\ P(((ve,e1 @@ e2),v_const(c_app c1 c2))); \
2.220 -\ !!ve vem xm e1 e2 em v v2. \
2.221 -\ [| P(((ve,e1),v_clos(<|xm,em,vem|>))); \
2.222 -\ P(((ve,e2),v2)); \
2.223 -\ P(((vem + {xm |-> v2},em),v)) \
2.224 -\ |] ==> \
2.225 -\ P(((ve,e1 @@ e2),v)) \
2.226 -\ |] ==> \
2.227 -\ P(((ve,e),v))";
2.228 -by (resolve_tac (prems RL [lfp_ind2]) 1);
2.229 -by (rtac eval_fun_mono 1);
2.230 -by (rewtac eval_fun_def);
2.231 -by (dtac CollectD 1);
2.232 -by Safe_tac;
2.233 -by (ALLGOALS (resolve_tac prems));
2.234 -by (ALLGOALS (Blast_tac));
2.235 -qed "eval_ind0";
2.236 -
2.237 -val prems = goal (the_context ())
2.238 - " [| ve |- e ---> v; \
2.239 -\ !!ve c. P ve (e_const c) (v_const c); \
2.240 -\ !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
2.241 -\ !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
2.242 -\ !!ev1 ev2 ve cl e. \
2.243 -\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
2.244 -\ P ve (fix ev2(ev1) = e) (v_clos cl); \
2.245 -\ !!ve c1 c2 e1 e2. \
2.246 -\ [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
2.247 -\ P ve (e1 @@ e2) (v_const(c_app c1 c2)); \
2.248 -\ !!ve vem evm e1 e2 em v v2. \
2.249 -\ [| P ve e1 (v_clos <|evm,em,vem|>); \
2.250 -\ P ve e2 v2; \
2.251 -\ P (vem + {evm |-> v2}) em v \
2.252 -\ |] ==> P ve (e1 @@ e2) v \
2.253 -\ |] ==> P ve e v";
2.254 -by (res_inst_tac [("P","P")] infsys_pp2 1);
2.255 -by (rtac eval_ind0 1);
2.256 -by (ALLGOALS (rtac infsys_pp1));
2.257 -by (ALLGOALS (resolve_tac prems));
2.258 -by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
2.259 -qed "eval_ind";
2.260 -
2.261 -(* ############################################################ *)
2.262 -(* Elaborations *)
2.263 -(* ############################################################ *)
2.264 -
2.265 -Goalw [thm "mono_def", elab_fun_def] "mono(elab_fun)";
2.266 -by infsys_mono_tac;
2.267 -qed "elab_fun_mono";
2.268 -
2.269 -(* Introduction rules *)
2.270 -
2.271 -Goalw [elab_def, elab_rel_def]
2.272 - "c isof ty ==> te |- e_const(c) ===> ty";
2.273 -by (rtac lfp_intro2 1);
2.274 -by (rtac elab_fun_mono 1);
2.275 -by (rewtac elab_fun_def);
2.276 -by (blast_tac (claset() addSIs [exI]) 1);
2.277 -qed "elab_const";
2.278 -
2.279 -Goalw [elab_def, elab_rel_def]
2.280 - "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
2.281 -by (rtac lfp_intro2 1);
2.282 -by (rtac elab_fun_mono 1);
2.283 -by (rewtac elab_fun_def);
2.284 -by (blast_tac (claset() addSIs [exI]) 1);
2.285 -qed "elab_var";
2.286 -
2.287 -Goalw [elab_def, elab_rel_def]
2.288 - "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
2.289 -by (rtac lfp_intro2 1);
2.290 -by (rtac elab_fun_mono 1);
2.291 -by (rewtac elab_fun_def);
2.292 -by (blast_tac (claset() addSIs [exI]) 1);
2.293 -qed "elab_fn";
2.294 -
2.295 -Goalw [elab_def, elab_rel_def]
2.296 - "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
2.297 -\ te |- fix f(x) = e ===> ty1->ty2";
2.298 -by (rtac lfp_intro2 1);
2.299 -by (rtac elab_fun_mono 1);
2.300 -by (rewtac elab_fun_def);
2.301 -by (blast_tac (claset() addSIs [exI]) 1);
2.302 -qed "elab_fix";
2.303 -
2.304 -Goalw [elab_def, elab_rel_def]
2.305 - "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
2.306 -\ te |- e1 @@ e2 ===> ty2";
2.307 -by (rtac lfp_intro2 1);
2.308 -by (rtac elab_fun_mono 1);
2.309 -by (rewtac elab_fun_def);
2.310 -by (blast_tac (claset() addSIs [disjI2]) 1);
2.311 -qed "elab_app";
2.312 -
2.313 -(* Strong elimination, induction on elaborations *)
2.314 -
2.315 -val prems = goalw (the_context ()) [elab_def, elab_rel_def]
2.316 - " [| te |- e ===> t; \
2.317 -\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
2.318 -\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
2.319 -\ !!te x e t1 t2. \
2.320 -\ [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
2.321 -\ P(((te,fn x => e),t1->t2)); \
2.322 -\ !!te f x e t1 t2. \
2.323 -\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
2.324 -\ P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
2.325 -\ |] ==> \
2.326 -\ P(((te,fix f(x) = e),t1->t2)); \
2.327 -\ !!te e1 e2 t1 t2. \
2.328 -\ [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
2.329 -\ te |- e2 ===> t1; P(((te,e2),t1)) \
2.330 -\ |] ==> \
2.331 -\ P(((te,e1 @@ e2),t2)) \
2.332 -\ |] ==> \
2.333 -\ P(((te,e),t))";
2.334 -by (resolve_tac (prems RL [lfp_ind2]) 1);
2.335 -by (rtac elab_fun_mono 1);
2.336 -by (rewtac elab_fun_def);
2.337 -by (dtac CollectD 1);
2.338 -by Safe_tac;
2.339 -by (ALLGOALS (resolve_tac prems));
2.340 -by (ALLGOALS (Blast_tac));
2.341 -qed "elab_ind0";
2.342 -
2.343 -val prems = goal (the_context ())
2.344 - " [| te |- e ===> t; \
2.345 -\ !!te c t. c isof t ==> P te (e_const c) t; \
2.346 -\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
2.347 -\ !!te x e t1 t2. \
2.348 -\ [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
2.349 -\ P te (fn x => e) (t1->t2); \
2.350 -\ !!te f x e t1 t2. \
2.351 -\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
2.352 -\ P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
2.353 -\ |] ==> \
2.354 -\ P te (fix f(x) = e) (t1->t2); \
2.355 -\ !!te e1 e2 t1 t2. \
2.356 -\ [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
2.357 -\ te |- e2 ===> t1; P te e2 t1 \
2.358 -\ |] ==> \
2.359 -\ P te (e1 @@ e2) t2 \
2.360 -\ |] ==> \
2.361 -\ P te e t";
2.362 -by (res_inst_tac [("P","P")] infsys_pp2 1);
2.363 -by (rtac elab_ind0 1);
2.364 -by (ALLGOALS (rtac infsys_pp1));
2.365 -by (ALLGOALS (resolve_tac prems));
2.366 -by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
2.367 -qed "elab_ind";
2.368 -
2.369 -(* Weak elimination, case analysis on elaborations *)
2.370 -
2.371 -val prems = goalw (the_context ()) [elab_def, elab_rel_def]
2.372 - " [| te |- e ===> t; \
2.373 -\ !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
2.374 -\ !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
2.375 -\ !!te x e t1 t2. \
2.376 -\ te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
2.377 -\ !!te f x e t1 t2. \
2.378 -\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
2.379 -\ P(((te,fix f(x) = e),t1->t2)); \
2.380 -\ !!te e1 e2 t1 t2. \
2.381 -\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
2.382 -\ P(((te,e1 @@ e2),t2)) \
2.383 -\ |] ==> \
2.384 -\ P(((te,e),t))";
2.385 -by (resolve_tac (prems RL [lfp_elim2]) 1);
2.386 -by (rtac elab_fun_mono 1);
2.387 -by (rewtac elab_fun_def);
2.388 -by (dtac CollectD 1);
2.389 -by Safe_tac;
2.390 -by (ALLGOALS (resolve_tac prems));
2.391 -by (ALLGOALS (Blast_tac));
2.392 -qed "elab_elim0";
2.393 -
2.394 -val prems = goal (the_context ())
2.395 - " [| te |- e ===> t; \
2.396 -\ !!te c t. c isof t ==> P te (e_const c) t; \
2.397 -\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
2.398 -\ !!te x e t1 t2. \
2.399 -\ te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
2.400 -\ !!te f x e t1 t2. \
2.401 -\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
2.402 -\ P te (fix f(x) = e) (t1->t2); \
2.403 -\ !!te e1 e2 t1 t2. \
2.404 -\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
2.405 -\ P te (e1 @@ e2) t2 \
2.406 -\ |] ==> \
2.407 -\ P te e t";
2.408 -by (res_inst_tac [("P","P")] infsys_pp2 1);
2.409 -by (rtac elab_elim0 1);
2.410 -by (ALLGOALS (rtac infsys_pp1));
2.411 -by (ALLGOALS (resolve_tac prems));
2.412 -by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
2.413 -qed "elab_elim";
2.414 -
2.415 -(* Elimination rules for each expression *)
2.416 -
2.417 -fun elab_e_elim_tac p =
2.418 - ( (rtac elab_elim 1) THEN
2.419 - (resolve_tac p 1) THEN
2.420 - (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
2.421 - );
2.422 -
2.423 -val prems = goal (the_context ()) "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
2.424 -by (elab_e_elim_tac prems);
2.425 -qed "elab_const_elim_lem";
2.426 -
2.427 -Goal "te |- e_const(c) ===> t ==> c isof t";
2.428 -by (dtac elab_const_elim_lem 1);
2.429 -by (Blast_tac 1);
2.430 -qed "elab_const_elim";
2.431 -
2.432 -val prems = goal (the_context ())
2.433 - "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
2.434 -by (elab_e_elim_tac prems);
2.435 -qed "elab_var_elim_lem";
2.436 -
2.437 -Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
2.438 -by (dtac elab_var_elim_lem 1);
2.439 -by (Blast_tac 1);
2.440 -qed "elab_var_elim";
2.441 -
2.442 -val prems = goal (the_context ())
2.443 - " te |- e ===> t ==> \
2.444 -\ ( e = fn x1 => e1 --> \
2.445 -\ (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
2.446 -\ )";
2.447 -by (elab_e_elim_tac prems);
2.448 -qed "elab_fn_elim_lem";
2.449 -
2.450 -Goal " te |- fn x1 => e1 ===> t ==> \
2.451 -\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
2.452 -by (dtac elab_fn_elim_lem 1);
2.453 -by (Blast_tac 1);
2.454 -qed "elab_fn_elim";
2.455 -
2.456 -val prems = goal (the_context ())
2.457 - " te |- e ===> t ==> \
2.458 -\ (e = fix f(x) = e1 --> \
2.459 -\ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))";
2.460 -by (elab_e_elim_tac prems);
2.461 -qed "elab_fix_elim_lem";
2.462 -
2.463 -Goal " te |- fix ev1(ev2) = e1 ===> t ==> \
2.464 -\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
2.465 -by (dtac elab_fix_elim_lem 1);
2.466 -by (Blast_tac 1);
2.467 -qed "elab_fix_elim";
2.468 -
2.469 -val prems = goal (the_context ())
2.470 - " te |- e ===> t2 ==> \
2.471 -\ (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))";
2.472 -by (elab_e_elim_tac prems);
2.473 -qed "elab_app_elim_lem";
2.474 -
2.475 -Goal "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
2.476 -by (dtac elab_app_elim_lem 1);
2.477 -by (Blast_tac 1);
2.478 -qed "elab_app_elim";
2.479 -
2.480 -(* ############################################################ *)
2.481 -(* The extended correspondence relation *)
2.482 -(* ############################################################ *)
2.483 -
2.484 -(* Monotonicity of hasty_fun *)
2.485 -
2.486 -Goalw [thm "mono_def", hasty_fun_def] "mono(hasty_fun)";
2.487 -by infsys_mono_tac;
2.488 -by (Blast_tac 1);
2.489 -qed "mono_hasty_fun";
2.490 -
2.491 -(*
2.492 - Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
2.493 - enjoys two strong indtroduction (co-induction) rules and an elimination rule.
2.494 -*)
2.495 -
2.496 -(* First strong indtroduction (co-induction) rule for hasty_rel *)
2.497 -
2.498 -Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
2.499 -by (rtac gfp_coind2 1);
2.500 -by (rewtac hasty_fun_def);
2.501 -by (rtac CollectI 1);
2.502 -by (rtac disjI1 1);
2.503 -by (Blast_tac 1);
2.504 -by (rtac mono_hasty_fun 1);
2.505 -qed "hasty_rel_const_coind";
2.506 -
2.507 -(* Second strong introduction (co-induction) rule for hasty_rel *)
2.508 -
2.509 -Goalw [hasty_rel_def]
2.510 - " [| te |- fn ev => e ===> t; \
2.511 -\ ve_dom(ve) = te_dom(te); \
2.512 -\ ! ev1. \
2.513 -\ ev1:ve_dom(ve) --> \
2.514 -\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
2.515 -\ |] ==> \
2.516 -\ (v_clos(<|ev,e,ve|>),t) : hasty_rel";
2.517 -by (rtac gfp_coind2 1);
2.518 -by (rewtac hasty_fun_def);
2.519 -by (rtac CollectI 1);
2.520 -by (rtac disjI2 1);
2.521 -by (blast_tac HOL_cs 1);
2.522 -by (rtac mono_hasty_fun 1);
2.523 -qed "hasty_rel_clos_coind";
2.524 -
2.525 -(* Elimination rule for hasty_rel *)
2.526 -
2.527 -val prems = goalw (the_context ()) [hasty_rel_def]
2.528 - " [| !! c t. c isof t ==> P((v_const(c),t)); \
2.529 -\ !! te ev e t ve. \
2.530 -\ [| te |- fn ev => e ===> t; \
2.531 -\ ve_dom(ve) = te_dom(te); \
2.532 -\ !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
2.533 -\ |] ==> P((v_clos(<|ev,e,ve|>),t)); \
2.534 -\ (v,t) : hasty_rel \
2.535 -\ |] ==> P(v,t)";
2.536 -by (cut_facts_tac prems 1);
2.537 -by (etac gfp_elim2 1);
2.538 -by (rtac mono_hasty_fun 1);
2.539 -by (rewtac hasty_fun_def);
2.540 -by (dtac CollectD 1);
2.541 -by (fold_goals_tac [hasty_fun_def]);
2.542 -by Safe_tac;
2.543 -by (REPEAT (ares_tac prems 1));
2.544 -qed "hasty_rel_elim0";
2.545 -
2.546 -val prems = goal (the_context ())
2.547 - " [| (v,t) : hasty_rel; \
2.548 -\ !! c t. c isof t ==> P (v_const c) t; \
2.549 -\ !! te ev e t ve. \
2.550 -\ [| te |- fn ev => e ===> t; \
2.551 -\ ve_dom(ve) = te_dom(te); \
2.552 -\ !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
2.553 -\ |] ==> P (v_clos <|ev,e,ve|>) t \
2.554 -\ |] ==> P v t";
2.555 -by (res_inst_tac [("P","P")] infsys_p2 1);
2.556 -by (rtac hasty_rel_elim0 1);
2.557 -by (ALLGOALS (rtac infsys_p1));
2.558 -by (ALLGOALS (resolve_tac prems));
2.559 -by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
2.560 -qed "hasty_rel_elim";
2.561 -
2.562 -(* Introduction rules for hasty *)
2.563 -
2.564 -Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
2.565 -by (etac hasty_rel_const_coind 1);
2.566 -qed "hasty_const";
2.567 -
2.568 -Goalw [hasty_def,hasty_env_def]
2.569 - "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
2.570 -by (rtac hasty_rel_clos_coind 1);
2.571 -by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
2.572 -qed "hasty_clos";
2.573 -
2.574 -(* Elimination on constants for hasty *)
2.575 -
2.576 -Goalw [hasty_def]
2.577 - "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
2.578 -by (rtac hasty_rel_elim 1);
2.579 -by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
2.580 -qed "hasty_elim_const_lem";
2.581 -
2.582 -Goal "v_const(c) hasty t ==> c isof t";
2.583 -by (dtac hasty_elim_const_lem 1);
2.584 -by (Blast_tac 1);
2.585 -qed "hasty_elim_const";
2.586 -
2.587 -(* Elimination on closures for hasty *)
2.588 -
2.589 -Goalw [hasty_env_def,hasty_def]
2.590 - " v hasty t ==> \
2.591 -\ ! x e ve. \
2.592 -\ v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
2.593 -by (rtac hasty_rel_elim 1);
2.594 -by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
2.595 -qed "hasty_elim_clos_lem";
2.596 -
2.597 -Goal "v_clos(<|ev,e,ve|>) hasty t ==> \
2.598 -\ ? te. te |- fn ev => e ===> t & ve hastyenv te ";
2.599 -by (dtac hasty_elim_clos_lem 1);
2.600 -by (Blast_tac 1);
2.601 -qed "hasty_elim_clos";
2.602 -
2.603 -(* ############################################################ *)
2.604 -(* The pointwise extension of hasty to environments *)
2.605 -(* ############################################################ *)
2.606 -
2.607 -fun excluded_middle_tac sP =
2.608 - res_inst_tac [("Q", sP)] (excluded_middle RS disjE);
2.609 -
2.610 -Goal "[| ve hastyenv te; v hasty t |] ==> \
2.611 -\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
2.612 -by (rewtac hasty_env_def);
2.613 -by (asm_full_simp_tac (simpset() delsimps thms "mem_simps"
2.614 - addsimps [ve_dom_owr, te_dom_owr]) 1);
2.615 -by (safe_tac HOL_cs);
2.616 -by (excluded_middle_tac "ev=x" 1);
2.617 -by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
2.618 -by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
2.619 -qed "hasty_env1";
2.620 -
2.621 -(* ############################################################ *)
2.622 -(* The Consistency theorem *)
2.623 -(* ############################################################ *)
2.624 -
2.625 -Goal "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
2.626 -by (dtac elab_const_elim 1);
2.627 -by (etac hasty_const 1);
2.628 -qed "consistency_const";
2.629 -
2.630 -Goalw [hasty_env_def]
2.631 - "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
2.632 -\ ve_app ve ev hasty t";
2.633 -by (dtac elab_var_elim 1);
2.634 -by (Blast_tac 1);
2.635 -qed "consistency_var";
2.636 -
2.637 -Goal "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
2.638 -\ v_clos(<| ev, e, ve |>) hasty t";
2.639 -by (rtac hasty_clos 1);
2.640 -by (Blast_tac 1);
2.641 -qed "consistency_fn";
2.642 -
2.643 -Goalw [hasty_env_def,hasty_def]
2.644 - "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
2.645 -\ ve hastyenv te ; \
2.646 -\ te |- fix ev2 ev1 = e ===> t \
2.647 -\ |] ==> \
2.648 -\ v_clos(cl) hasty t";
2.649 -by (dtac elab_fix_elim 1);
2.650 -by (safe_tac HOL_cs);
2.651 -(*Do a single unfolding of cl*)
2.652 -by ((ftac ssubst 1) THEN (assume_tac 2));
2.653 -by (rtac hasty_rel_clos_coind 1);
2.654 -by (etac elab_fn 1);
2.655 -by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
2.656 -
2.657 -by (asm_simp_tac (simpset() delsimps thms "mem_simps" addsimps [ve_dom_owr]) 1);
2.658 -by (safe_tac HOL_cs);
2.659 -by (excluded_middle_tac "ev2=ev1a" 1);
2.660 -by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
2.661 -
2.662 -by (asm_simp_tac (simpset() delsimps thms "mem_simps"
2.663 - addsimps [ve_app_owr1, te_app_owr1]) 1);
2.664 -by (Blast_tac 1);
2.665 -qed "consistency_fix";
2.666 -
2.667 -Goal "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
2.668 -\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
2.669 -\ ve hastyenv te ; te |- e1 @@ e2 ===> t \
2.670 -\ |] ==> \
2.671 -\ v_const(c_app c1 c2) hasty t";
2.672 -by (dtac elab_app_elim 1);
2.673 -by Safe_tac;
2.674 -by (rtac hasty_const 1);
2.675 -by (rtac isof_app 1);
2.676 -by (rtac hasty_elim_const 1);
2.677 -by (Blast_tac 1);
2.678 -by (rtac hasty_elim_const 1);
2.679 -by (Blast_tac 1);
2.680 -qed "consistency_app1";
2.681 -
2.682 -Goal "[| ! t te. \
2.683 -\ ve hastyenv te --> \
2.684 -\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
2.685 -\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
2.686 -\ ! t te. \
2.687 -\ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \
2.688 -\ ve hastyenv te ; \
2.689 -\ te |- e1 @@ e2 ===> t \
2.690 -\ |] ==> \
2.691 -\ v hasty t";
2.692 -by (dtac elab_app_elim 1);
2.693 -by Safe_tac;
2.694 -by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
2.695 -by (assume_tac 1);
2.696 -by (etac impE 1);
2.697 -by (assume_tac 1);
2.698 -by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
2.699 -by (assume_tac 1);
2.700 -by (etac impE 1);
2.701 -by (assume_tac 1);
2.702 -by (dtac hasty_elim_clos 1);
2.703 -by Safe_tac;
2.704 -by (dtac elab_fn_elim 1);
2.705 -by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
2.706 -qed "consistency_app2";
2.707 -
2.708 -Goal "ve |- e ---> v ==> \
2.709 -\ (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
2.710 -
2.711 -(* Proof by induction on the structure of evaluations *)
2.712 -
2.713 -by (etac eval_ind 1);
2.714 -by Safe_tac;
2.715 -by (DEPTH_SOLVE
2.716 - (ares_tac [consistency_const, consistency_var, consistency_fn,
2.717 - consistency_fix, consistency_app1, consistency_app2] 1));
2.718 -qed "consistency";
2.719 -
2.720 -(* ############################################################ *)
2.721 -(* The Basic Consistency theorem *)
2.722 -(* ############################################################ *)
2.723 -
2.724 -Goalw [isof_env_def,hasty_env_def]
2.725 - "ve isofenv te ==> ve hastyenv te";
2.726 -by Safe_tac;
2.727 -by (etac allE 1);
2.728 -by (etac impE 1);
2.729 -by (assume_tac 1);
2.730 -by (etac exE 1);
2.731 -by (etac conjE 1);
2.732 -by (dtac hasty_const 1);
2.733 -by (Asm_simp_tac 1);
2.734 -qed "basic_consistency_lem";
2.735 -
2.736 -Goal "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
2.737 -by (rtac hasty_elim_const 1);
2.738 -by (dtac consistency 1);
2.739 -by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
2.740 -qed "basic_consistency";
3.1 --- a/src/HOL/ex/MT.thy Sat Aug 18 13:32:28 2007 +0200
3.2 +++ b/src/HOL/ex/MT.thy Sat Aug 18 17:42:38 2007 +0200
3.3 @@ -1,4 +1,4 @@
3.4 -(* Title: HOL/ex/mt.thy
3.5 +(* Title: HOL/ex/MT.thy
3.6 ID: $Id$
3.7 Author: Jacob Frost, Cambridge University Computer Laboratory
3.8 Copyright 1993 University of Cambridge
3.9 @@ -13,6 +13,8 @@
3.10 Report 308, Computer Lab, University of Cambridge (1993).
3.11 *)
3.12
3.13 +header {* Milner-Tofte: Co-induction in Relational Semantics *}
3.14 +
3.15 theory MT
3.16 imports Main
3.17 begin
3.18 @@ -264,6 +266,735 @@
3.19 ve_dom(ve) = te_dom(te) &
3.20 (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
3.21
3.22 -ML {* use_legacy_bindings (the_context ()) *}
3.23 +
3.24 +(* ############################################################ *)
3.25 +(* Inference systems *)
3.26 +(* ############################################################ *)
3.27 +
3.28 +ML {*
3.29 +val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
3.30 +*}
3.31 +
3.32 +lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
3.33 + by simp
3.34 +
3.35 +lemma infsys_p2: "P (fst (a,b)) (snd (a,b)) ==> P a b"
3.36 + by simp
3.37 +
3.38 +lemma infsys_pp1: "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"
3.39 + by simp
3.40 +
3.41 +lemma infsys_pp2: "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"
3.42 + by simp
3.43 +
3.44 +
3.45 +(* ############################################################ *)
3.46 +(* Fixpoints *)
3.47 +(* ############################################################ *)
3.48 +
3.49 +(* Least fixpoints *)
3.50 +
3.51 +lemma lfp_intro2: "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"
3.52 +apply (rule subsetD)
3.53 +apply (rule lfp_lemma2)
3.54 +apply assumption+
3.55 +done
3.56 +
3.57 +lemma lfp_elim2:
3.58 + assumes lfp: "x:lfp(f)"
3.59 + and mono: "mono(f)"
3.60 + and r: "!!y. y:f(lfp(f)) ==> P(y)"
3.61 + shows "P(x)"
3.62 +apply (rule r)
3.63 +apply (rule subsetD)
3.64 +apply (rule lfp_lemma3)
3.65 +apply (rule mono)
3.66 +apply (rule lfp)
3.67 +done
3.68 +
3.69 +lemma lfp_ind2:
3.70 + assumes lfp: "x:lfp(f)"
3.71 + and mono: "mono(f)"
3.72 + and r: "!!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y)"
3.73 + shows "P(x)"
3.74 +apply (rule lfp_induct_set [OF lfp mono])
3.75 +apply (erule r)
3.76 +done
3.77 +
3.78 +(* Greatest fixpoints *)
3.79 +
3.80 +(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
3.81 +
3.82 +lemma gfp_coind2:
3.83 + assumes cih: "x:f({x} Un gfp(f))"
3.84 + and monoh: "mono(f)"
3.85 + shows "x:gfp(f)"
3.86 +apply (rule cih [THEN [2] gfp_upperbound [THEN subsetD]])
3.87 +apply (rule monoh [THEN monoD])
3.88 +apply (rule UnE [THEN subsetI])
3.89 +apply assumption
3.90 +apply (blast intro!: cih)
3.91 +apply (rule monoh [THEN monoD [THEN subsetD]])
3.92 +apply (rule Un_upper2)
3.93 +apply (erule monoh [THEN gfp_lemma2, THEN subsetD])
3.94 +done
3.95 +
3.96 +lemma gfp_elim2:
3.97 + assumes gfph: "x:gfp(f)"
3.98 + and monoh: "mono(f)"
3.99 + and caseh: "!!y. y:f(gfp(f)) ==> P(y)"
3.100 + shows "P(x)"
3.101 +apply (rule caseh)
3.102 +apply (rule subsetD)
3.103 +apply (rule gfp_lemma2)
3.104 +apply (rule monoh)
3.105 +apply (rule gfph)
3.106 +done
3.107 +
3.108 +(* ############################################################ *)
3.109 +(* Expressions *)
3.110 +(* ############################################################ *)
3.111 +
3.112 +lemmas e_injs = e_const_inj e_var_inj e_fn_inj e_fix_inj e_app_inj
3.113 +
3.114 +lemmas e_disjs =
3.115 + e_disj_const_var
3.116 + e_disj_const_fn
3.117 + e_disj_const_fix
3.118 + e_disj_const_app
3.119 + e_disj_var_fn
3.120 + e_disj_var_fix
3.121 + e_disj_var_app
3.122 + e_disj_fn_fix
3.123 + e_disj_fn_app
3.124 + e_disj_fix_app
3.125 +
3.126 +lemmas e_disj_si = e_disjs e_disjs [symmetric]
3.127 +
3.128 +lemmas e_disj_se = e_disj_si [THEN notE]
3.129 +
3.130 +(* ############################################################ *)
3.131 +(* Values *)
3.132 +(* ############################################################ *)
3.133 +
3.134 +lemmas v_disjs = v_disj_const_clos
3.135 +lemmas v_disj_si = v_disjs v_disjs [symmetric]
3.136 +lemmas v_disj_se = v_disj_si [THEN notE]
3.137 +
3.138 +lemmas v_injs = v_const_inj v_clos_inj
3.139 +
3.140 +(* ############################################################ *)
3.141 +(* Evaluations *)
3.142 +(* ############################################################ *)
3.143 +
3.144 +(* Monotonicity of eval_fun *)
3.145 +
3.146 +lemma eval_fun_mono: "mono(eval_fun)"
3.147 +unfolding mono_def eval_fun_def
3.148 +apply (tactic infsys_mono_tac)
3.149 +done
3.150 +
3.151 +(* Introduction rules *)
3.152 +
3.153 +lemma eval_const: "ve |- e_const(c) ---> v_const(c)"
3.154 +unfolding eval_def eval_rel_def
3.155 +apply (rule lfp_intro2)
3.156 +apply (rule eval_fun_mono)
3.157 +apply (unfold eval_fun_def)
3.158 + (*Naughty! But the quantifiers are nested VERY deeply...*)
3.159 +apply (blast intro!: exI)
3.160 +done
3.161 +
3.162 +lemma eval_var2:
3.163 + "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev"
3.164 +apply (unfold eval_def eval_rel_def)
3.165 +apply (rule lfp_intro2)
3.166 +apply (rule eval_fun_mono)
3.167 +apply (unfold eval_fun_def)
3.168 +apply (blast intro!: exI)
3.169 +done
3.170 +
3.171 +lemma eval_fn:
3.172 + "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"
3.173 +apply (unfold eval_def eval_rel_def)
3.174 +apply (rule lfp_intro2)
3.175 +apply (rule eval_fun_mono)
3.176 +apply (unfold eval_fun_def)
3.177 +apply (blast intro!: exI)
3.178 +done
3.179 +
3.180 +lemma eval_fix:
3.181 + " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
3.182 + ve |- fix ev2(ev1) = e ---> v_clos(cl)"
3.183 +apply (unfold eval_def eval_rel_def)
3.184 +apply (rule lfp_intro2)
3.185 +apply (rule eval_fun_mono)
3.186 +apply (unfold eval_fun_def)
3.187 +apply (blast intro!: exI)
3.188 +done
3.189 +
3.190 +lemma eval_app1:
3.191 + " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==>
3.192 + ve |- e1 @@ e2 ---> v_const(c_app c1 c2)"
3.193 +apply (unfold eval_def eval_rel_def)
3.194 +apply (rule lfp_intro2)
3.195 +apply (rule eval_fun_mono)
3.196 +apply (unfold eval_fun_def)
3.197 +apply (blast intro!: exI)
3.198 +done
3.199 +
3.200 +lemma eval_app2:
3.201 + " [| ve |- e1 ---> v_clos(<|xm,em,vem|>);
3.202 + ve |- e2 ---> v2;
3.203 + vem + {xm |-> v2} |- em ---> v
3.204 + |] ==>
3.205 + ve |- e1 @@ e2 ---> v"
3.206 +apply (unfold eval_def eval_rel_def)
3.207 +apply (rule lfp_intro2)
3.208 +apply (rule eval_fun_mono)
3.209 +apply (unfold eval_fun_def)
3.210 +apply (blast intro!: disjI2)
3.211 +done
3.212 +
3.213 +(* Strong elimination, induction on evaluations *)
3.214 +
3.215 +lemma eval_ind0:
3.216 + " [| ve |- e ---> v;
3.217 + !!ve c. P(((ve,e_const(c)),v_const(c)));
3.218 + !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev));
3.219 + !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>)));
3.220 + !!ev1 ev2 ve cl e.
3.221 + cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
3.222 + P(((ve,fix ev2(ev1) = e),v_clos(cl)));
3.223 + !!ve c1 c2 e1 e2.
3.224 + [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==>
3.225 + P(((ve,e1 @@ e2),v_const(c_app c1 c2)));
3.226 + !!ve vem xm e1 e2 em v v2.
3.227 + [| P(((ve,e1),v_clos(<|xm,em,vem|>)));
3.228 + P(((ve,e2),v2));
3.229 + P(((vem + {xm |-> v2},em),v))
3.230 + |] ==>
3.231 + P(((ve,e1 @@ e2),v))
3.232 + |] ==>
3.233 + P(((ve,e),v))"
3.234 +unfolding eval_def eval_rel_def
3.235 +apply (erule lfp_ind2)
3.236 +apply (rule eval_fun_mono)
3.237 +apply (unfold eval_fun_def)
3.238 +apply (drule CollectD)
3.239 +apply safe
3.240 +apply auto
3.241 +done
3.242 +
3.243 +lemma eval_ind:
3.244 + " [| ve |- e ---> v;
3.245 + !!ve c. P ve (e_const c) (v_const c);
3.246 + !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev);
3.247 + !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>);
3.248 + !!ev1 ev2 ve cl e.
3.249 + cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
3.250 + P ve (fix ev2(ev1) = e) (v_clos cl);
3.251 + !!ve c1 c2 e1 e2.
3.252 + [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==>
3.253 + P ve (e1 @@ e2) (v_const(c_app c1 c2));
3.254 + !!ve vem evm e1 e2 em v v2.
3.255 + [| P ve e1 (v_clos <|evm,em,vem|>);
3.256 + P ve e2 v2;
3.257 + P (vem + {evm |-> v2}) em v
3.258 + |] ==> P ve (e1 @@ e2) v
3.259 + |] ==> P ve e v"
3.260 +apply (rule_tac P = "P" in infsys_pp2)
3.261 +apply (rule eval_ind0)
3.262 +apply (rule infsys_pp1)
3.263 +apply auto
3.264 +done
3.265 +
3.266 +(* ############################################################ *)
3.267 +(* Elaborations *)
3.268 +(* ############################################################ *)
3.269 +
3.270 +lemma elab_fun_mono: "mono(elab_fun)"
3.271 +unfolding mono_def elab_fun_def
3.272 +apply (tactic infsys_mono_tac)
3.273 +done
3.274 +
3.275 +(* Introduction rules *)
3.276 +
3.277 +lemma elab_const:
3.278 + "c isof ty ==> te |- e_const(c) ===> ty"
3.279 +apply (unfold elab_def elab_rel_def)
3.280 +apply (rule lfp_intro2)
3.281 +apply (rule elab_fun_mono)
3.282 +apply (unfold elab_fun_def)
3.283 +apply (blast intro!: exI)
3.284 +done
3.285 +
3.286 +lemma elab_var:
3.287 + "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x"
3.288 +apply (unfold elab_def elab_rel_def)
3.289 +apply (rule lfp_intro2)
3.290 +apply (rule elab_fun_mono)
3.291 +apply (unfold elab_fun_def)
3.292 +apply (blast intro!: exI)
3.293 +done
3.294 +
3.295 +lemma elab_fn:
3.296 + "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"
3.297 +apply (unfold elab_def elab_rel_def)
3.298 +apply (rule lfp_intro2)
3.299 +apply (rule elab_fun_mono)
3.300 +apply (unfold elab_fun_def)
3.301 +apply (blast intro!: exI)
3.302 +done
3.303 +
3.304 +lemma elab_fix:
3.305 + "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==>
3.306 + te |- fix f(x) = e ===> ty1->ty2"
3.307 +apply (unfold elab_def elab_rel_def)
3.308 +apply (rule lfp_intro2)
3.309 +apply (rule elab_fun_mono)
3.310 +apply (unfold elab_fun_def)
3.311 +apply (blast intro!: exI)
3.312 +done
3.313 +
3.314 +lemma elab_app:
3.315 + "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==>
3.316 + te |- e1 @@ e2 ===> ty2"
3.317 +apply (unfold elab_def elab_rel_def)
3.318 +apply (rule lfp_intro2)
3.319 +apply (rule elab_fun_mono)
3.320 +apply (unfold elab_fun_def)
3.321 +apply (blast intro!: disjI2)
3.322 +done
3.323 +
3.324 +(* Strong elimination, induction on elaborations *)
3.325 +
3.326 +lemma elab_ind0:
3.327 + assumes 1: "te |- e ===> t"
3.328 + and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
3.329 + and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
3.330 + and 4: "!!te x e t1 t2.
3.331 + [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==>
3.332 + P(((te,fn x => e),t1->t2))"
3.333 + and 5: "!!te f x e t1 t2.
3.334 + [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
3.335 + P(((te + {f |=> t1->t2} + {x |=> t1},e),t2))
3.336 + |] ==>
3.337 + P(((te,fix f(x) = e),t1->t2))"
3.338 + and 6: "!!te e1 e2 t1 t2.
3.339 + [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2));
3.340 + te |- e2 ===> t1; P(((te,e2),t1))
3.341 + |] ==>
3.342 + P(((te,e1 @@ e2),t2))"
3.343 + shows "P(((te,e),t))"
3.344 +apply (rule lfp_ind2 [OF 1 [unfolded elab_def elab_rel_def]])
3.345 +apply (rule elab_fun_mono)
3.346 +apply (unfold elab_fun_def)
3.347 +apply (drule CollectD)
3.348 +apply safe
3.349 +apply (erule 2)
3.350 +apply (erule 3)
3.351 +apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
3.352 +apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
3.353 +apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
3.354 +done
3.355 +
3.356 +lemma elab_ind:
3.357 + " [| te |- e ===> t;
3.358 + !!te c t. c isof t ==> P te (e_const c) t;
3.359 + !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
3.360 + !!te x e t1 t2.
3.361 + [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==>
3.362 + P te (fn x => e) (t1->t2);
3.363 + !!te f x e t1 t2.
3.364 + [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
3.365 + P (te + {f |=> t1->t2} + {x |=> t1}) e t2
3.366 + |] ==>
3.367 + P te (fix f(x) = e) (t1->t2);
3.368 + !!te e1 e2 t1 t2.
3.369 + [| te |- e1 ===> t1->t2; P te e1 (t1->t2);
3.370 + te |- e2 ===> t1; P te e2 t1
3.371 + |] ==>
3.372 + P te (e1 @@ e2) t2
3.373 + |] ==>
3.374 + P te e t"
3.375 +apply (rule_tac P = "P" in infsys_pp2)
3.376 +apply (erule elab_ind0)
3.377 +apply (rule_tac [!] infsys_pp1)
3.378 +apply auto
3.379 +done
3.380 +
3.381 +(* Weak elimination, case analysis on elaborations *)
3.382 +
3.383 +lemma elab_elim0:
3.384 + assumes 1: "te |- e ===> t"
3.385 + and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
3.386 + and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
3.387 + and 4: "!!te x e t1 t2.
3.388 + te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2))"
3.389 + and 5: "!!te f x e t1 t2.
3.390 + te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
3.391 + P(((te,fix f(x) = e),t1->t2))"
3.392 + and 6: "!!te e1 e2 t1 t2.
3.393 + [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
3.394 + P(((te,e1 @@ e2),t2))"
3.395 + shows "P(((te,e),t))"
3.396 +apply (rule lfp_elim2 [OF 1 [unfolded elab_def elab_rel_def]])
3.397 +apply (rule elab_fun_mono)
3.398 +apply (unfold elab_fun_def)
3.399 +apply (drule CollectD)
3.400 +apply safe
3.401 +apply (erule 2)
3.402 +apply (erule 3)
3.403 +apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
3.404 +apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
3.405 +apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
3.406 +done
3.407 +
3.408 +lemma elab_elim:
3.409 + " [| te |- e ===> t;
3.410 + !!te c t. c isof t ==> P te (e_const c) t;
3.411 + !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
3.412 + !!te x e t1 t2.
3.413 + te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2);
3.414 + !!te f x e t1 t2.
3.415 + te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
3.416 + P te (fix f(x) = e) (t1->t2);
3.417 + !!te e1 e2 t1 t2.
3.418 + [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
3.419 + P te (e1 @@ e2) t2
3.420 + |] ==>
3.421 + P te e t"
3.422 +apply (rule_tac P = "P" in infsys_pp2)
3.423 +apply (rule elab_elim0)
3.424 +apply auto
3.425 +done
3.426 +
3.427 +(* Elimination rules for each expression *)
3.428 +
3.429 +lemma elab_const_elim_lem:
3.430 + "te |- e ===> t ==> (e = e_const(c) --> c isof t)"
3.431 +apply (erule elab_elim)
3.432 +apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
3.433 +done
3.434 +
3.435 +lemma elab_const_elim: "te |- e_const(c) ===> t ==> c isof t"
3.436 +apply (drule elab_const_elim_lem)
3.437 +apply blast
3.438 +done
3.439 +
3.440 +lemma elab_var_elim_lem:
3.441 + "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))"
3.442 +apply (erule elab_elim)
3.443 +apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
3.444 +done
3.445 +
3.446 +lemma elab_var_elim: "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"
3.447 +apply (drule elab_var_elim_lem)
3.448 +apply blast
3.449 +done
3.450 +
3.451 +lemma elab_fn_elim_lem:
3.452 + " te |- e ===> t ==>
3.453 + ( e = fn x1 => e1 -->
3.454 + (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2)
3.455 + )"
3.456 +apply (erule elab_elim)
3.457 +apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
3.458 +done
3.459 +
3.460 +lemma elab_fn_elim: " te |- fn x1 => e1 ===> t ==>
3.461 + (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"
3.462 +apply (drule elab_fn_elim_lem)
3.463 +apply blast
3.464 +done
3.465 +
3.466 +lemma elab_fix_elim_lem:
3.467 + " te |- e ===> t ==>
3.468 + (e = fix f(x) = e1 -->
3.469 + (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"
3.470 +apply (erule elab_elim)
3.471 +apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
3.472 +done
3.473 +
3.474 +lemma elab_fix_elim: " te |- fix ev1(ev2) = e1 ===> t ==>
3.475 + (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"
3.476 +apply (drule elab_fix_elim_lem)
3.477 +apply blast
3.478 +done
3.479 +
3.480 +lemma elab_app_elim_lem:
3.481 + " te |- e ===> t2 ==>
3.482 + (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"
3.483 +apply (erule elab_elim)
3.484 +apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
3.485 +done
3.486 +
3.487 +lemma elab_app_elim: "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"
3.488 +apply (drule elab_app_elim_lem)
3.489 +apply blast
3.490 +done
3.491 +
3.492 +(* ############################################################ *)
3.493 +(* The extended correspondence relation *)
3.494 +(* ############################################################ *)
3.495 +
3.496 +(* Monotonicity of hasty_fun *)
3.497 +
3.498 +lemma mono_hasty_fun: "mono(hasty_fun)"
3.499 +unfolding mono_def hasty_fun_def
3.500 +apply (tactic infsys_mono_tac)
3.501 +apply blast
3.502 +done
3.503 +
3.504 +(*
3.505 + Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
3.506 + enjoys two strong indtroduction (co-induction) rules and an elimination rule.
3.507 +*)
3.508 +
3.509 +(* First strong indtroduction (co-induction) rule for hasty_rel *)
3.510 +
3.511 +lemma hasty_rel_const_coind: "c isof t ==> (v_const(c),t) : hasty_rel"
3.512 +apply (unfold hasty_rel_def)
3.513 +apply (rule gfp_coind2)
3.514 +apply (unfold hasty_fun_def)
3.515 +apply (rule CollectI)
3.516 +apply (rule disjI1)
3.517 +apply blast
3.518 +apply (rule mono_hasty_fun)
3.519 +done
3.520 +
3.521 +(* Second strong introduction (co-induction) rule for hasty_rel *)
3.522 +
3.523 +lemma hasty_rel_clos_coind:
3.524 + " [| te |- fn ev => e ===> t;
3.525 + ve_dom(ve) = te_dom(te);
3.526 + ! ev1.
3.527 + ev1:ve_dom(ve) -->
3.528 + (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel
3.529 + |] ==>
3.530 + (v_clos(<|ev,e,ve|>),t) : hasty_rel"
3.531 +apply (unfold hasty_rel_def)
3.532 +apply (rule gfp_coind2)
3.533 +apply (unfold hasty_fun_def)
3.534 +apply (rule CollectI)
3.535 +apply (rule disjI2)
3.536 +apply blast
3.537 +apply (rule mono_hasty_fun)
3.538 +done
3.539 +
3.540 +(* Elimination rule for hasty_rel *)
3.541 +
3.542 +lemma hasty_rel_elim0:
3.543 + " [| !! c t. c isof t ==> P((v_const(c),t));
3.544 + !! te ev e t ve.
3.545 + [| te |- fn ev => e ===> t;
3.546 + ve_dom(ve) = te_dom(te);
3.547 + !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
3.548 + |] ==> P((v_clos(<|ev,e,ve|>),t));
3.549 + (v,t) : hasty_rel
3.550 + |] ==> P(v,t)"
3.551 +unfolding hasty_rel_def
3.552 +apply (erule gfp_elim2)
3.553 +apply (rule mono_hasty_fun)
3.554 +apply (unfold hasty_fun_def)
3.555 +apply (drule CollectD)
3.556 +apply (fold hasty_fun_def)
3.557 +apply auto
3.558 +done
3.559 +
3.560 +lemma hasty_rel_elim:
3.561 + " [| (v,t) : hasty_rel;
3.562 + !! c t. c isof t ==> P (v_const c) t;
3.563 + !! te ev e t ve.
3.564 + [| te |- fn ev => e ===> t;
3.565 + ve_dom(ve) = te_dom(te);
3.566 + !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
3.567 + |] ==> P (v_clos <|ev,e,ve|>) t
3.568 + |] ==> P v t"
3.569 +apply (rule_tac P = "P" in infsys_p2)
3.570 +apply (rule hasty_rel_elim0)
3.571 +apply auto
3.572 +done
3.573 +
3.574 +(* Introduction rules for hasty *)
3.575 +
3.576 +lemma hasty_const: "c isof t ==> v_const(c) hasty t"
3.577 +apply (unfold hasty_def)
3.578 +apply (erule hasty_rel_const_coind)
3.579 +done
3.580 +
3.581 +lemma hasty_clos:
3.582 + "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"
3.583 +apply (unfold hasty_def hasty_env_def)
3.584 +apply (rule hasty_rel_clos_coind)
3.585 +apply (blast del: equalityI)+
3.586 +done
3.587 +
3.588 +(* Elimination on constants for hasty *)
3.589 +
3.590 +lemma hasty_elim_const_lem:
3.591 + "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"
3.592 +apply (unfold hasty_def)
3.593 +apply (rule hasty_rel_elim)
3.594 +apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
3.595 +done
3.596 +
3.597 +lemma hasty_elim_const: "v_const(c) hasty t ==> c isof t"
3.598 +apply (drule hasty_elim_const_lem)
3.599 +apply blast
3.600 +done
3.601 +
3.602 +(* Elimination on closures for hasty *)
3.603 +
3.604 +lemma hasty_elim_clos_lem:
3.605 + " v hasty t ==>
3.606 + ! x e ve.
3.607 + v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)"
3.608 +apply (unfold hasty_env_def hasty_def)
3.609 +apply (rule hasty_rel_elim)
3.610 +apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
3.611 +done
3.612 +
3.613 +lemma hasty_elim_clos: "v_clos(<|ev,e,ve|>) hasty t ==>
3.614 + ? te. te |- fn ev => e ===> t & ve hastyenv te "
3.615 +apply (drule hasty_elim_clos_lem)
3.616 +apply blast
3.617 +done
3.618 +
3.619 +(* ############################################################ *)
3.620 +(* The pointwise extension of hasty to environments *)
3.621 +(* ############################################################ *)
3.622 +
3.623 +lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==>
3.624 + ve + {ev |-> v} hastyenv te + {ev |=> t}"
3.625 +apply (unfold hasty_env_def)
3.626 +apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
3.627 +apply (tactic {* safe_tac HOL_cs *})
3.628 +apply (case_tac "ev=x")
3.629 +apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
3.630 +apply (simp add: ve_app_owr2 te_app_owr2)
3.631 +done
3.632 +
3.633 +(* ############################################################ *)
3.634 +(* The Consistency theorem *)
3.635 +(* ############################################################ *)
3.636 +
3.637 +lemma consistency_const: "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"
3.638 +apply (drule elab_const_elim)
3.639 +apply (erule hasty_const)
3.640 +done
3.641 +
3.642 +lemma consistency_var:
3.643 + "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==>
3.644 + ve_app ve ev hasty t"
3.645 +apply (unfold hasty_env_def)
3.646 +apply (drule elab_var_elim)
3.647 +apply blast
3.648 +done
3.649 +
3.650 +lemma consistency_fn: "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==>
3.651 + v_clos(<| ev, e, ve |>) hasty t"
3.652 +apply (rule hasty_clos)
3.653 +apply blast
3.654 +done
3.655 +
3.656 +lemma consistency_fix:
3.657 + "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>;
3.658 + ve hastyenv te ;
3.659 + te |- fix ev2 ev1 = e ===> t
3.660 + |] ==>
3.661 + v_clos(cl) hasty t"
3.662 +apply (unfold hasty_env_def hasty_def)
3.663 +apply (drule elab_fix_elim)
3.664 +apply (tactic {* safe_tac HOL_cs *})
3.665 +(*Do a single unfolding of cl*)
3.666 +apply (frule ssubst) prefer 2 apply assumption
3.667 +apply (rule hasty_rel_clos_coind)
3.668 +apply (erule elab_fn)
3.669 +apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
3.670 +
3.671 +apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
3.672 +apply (tactic {* safe_tac HOL_cs *})
3.673 +apply (case_tac "ev2=ev1a")
3.674 +apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
3.675 +apply blast
3.676 +apply (simp add: ve_app_owr2 te_app_owr2)
3.677 +done
3.678 +
3.679 +lemma consistency_app1: "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;
3.680 + ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t;
3.681 + ve hastyenv te ; te |- e1 @@ e2 ===> t
3.682 + |] ==>
3.683 + v_const(c_app c1 c2) hasty t"
3.684 +apply (drule elab_app_elim)
3.685 +apply safe
3.686 +apply (rule hasty_const)
3.687 +apply (rule isof_app)
3.688 +apply (rule hasty_elim_const)
3.689 +apply blast
3.690 +apply (rule hasty_elim_const)
3.691 +apply blast
3.692 +done
3.693 +
3.694 +lemma consistency_app2: "[| ! t te.
3.695 + ve hastyenv te -->
3.696 + te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t;
3.697 + ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t;
3.698 + ! t te.
3.699 + vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t;
3.700 + ve hastyenv te ;
3.701 + te |- e1 @@ e2 ===> t
3.702 + |] ==>
3.703 + v hasty t"
3.704 +apply (drule elab_app_elim)
3.705 +apply safe
3.706 +apply (erule allE, erule allE, erule impE)
3.707 +apply assumption
3.708 +apply (erule impE)
3.709 +apply assumption
3.710 +apply (erule allE, erule allE, erule impE)
3.711 +apply assumption
3.712 +apply (erule impE)
3.713 +apply assumption
3.714 +apply (drule hasty_elim_clos)
3.715 +apply safe
3.716 +apply (drule elab_fn_elim)
3.717 +apply (blast intro: hasty_env1 dest!: t_fun_inj)
3.718 +done
3.719 +
3.720 +lemma consistency: "ve |- e ---> v ==>
3.721 + (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"
3.722 +
3.723 +(* Proof by induction on the structure of evaluations *)
3.724 +
3.725 +apply (erule eval_ind)
3.726 +apply safe
3.727 +apply (blast intro: consistency_const consistency_var consistency_fn consistency_fix consistency_app1 consistency_app2)+
3.728 +done
3.729 +
3.730 +(* ############################################################ *)
3.731 +(* The Basic Consistency theorem *)
3.732 +(* ############################################################ *)
3.733 +
3.734 +lemma basic_consistency_lem:
3.735 + "ve isofenv te ==> ve hastyenv te"
3.736 +apply (unfold isof_env_def hasty_env_def)
3.737 +apply safe
3.738 +apply (erule allE)
3.739 +apply (erule impE)
3.740 +apply assumption
3.741 +apply (erule exE)
3.742 +apply (erule conjE)
3.743 +apply (drule hasty_const)
3.744 +apply (simp (no_asm_simp))
3.745 +done
3.746 +
3.747 +lemma basic_consistency:
3.748 + "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"
3.749 +apply (rule hasty_elim_const)
3.750 +apply (drule consistency)
3.751 +apply (blast intro!: basic_consistency_lem)
3.752 +done
3.753
3.754 end