converted ex/MT.ML;
authorwenzelm
Sat Aug 18 17:42:38 2007 +0200 (2007-08-18)
changeset 243263e9d3ba894b8
parent 24325 5c29e8822f50
child 24327 a207114007c6
converted ex/MT.ML;
src/HOL/IsaMakefile
src/HOL/ex/MT.ML
src/HOL/ex/MT.thy
     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