src/HOL/ex/MT.ML
author clasohm
Tue Jan 30 15:24:36 1996 +0100 (1996-01-30)
changeset 1465 5d7a7e439cec
parent 1266 3ae9fe3c0f68
child 1584 3d59c407bd36
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      HOL/ex/MT.ML
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Based upon the article
     7     Robin Milner and Mads Tofte,
     8     Co-induction in Relational Semantics,
     9     Theoretical Computer Science 87 (1991), pages 209-220.
    10 
    11 Written up as
    12     Jacob Frost, A Case Study of Co-induction in Isabelle/HOL
    13     Report 308, Computer Lab, University of Cambridge (1993).
    14 
    15 NEEDS TO USE INDUCTIVE DEFS PACKAGE
    16 *)
    17 
    18 open MT;
    19 
    20 val prems = goal MT.thy "~a:{b} ==> ~a=b";
    21 by (cut_facts_tac prems 1);
    22 by (rtac notI 1);
    23 by (dtac notE 1);
    24 by (hyp_subst_tac 1);
    25 by (rtac singletonI 1);
    26 by (assume_tac 1);
    27 qed "notsingletonI";
    28 
    29 (* ############################################################ *)
    30 (* Inference systems                                            *)
    31 (* ############################################################ *)
    32 
    33 val infsys_mono_tac =
    34   (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
    35   (rtac CollectI 1) THEN (dtac CollectD 1) THEN
    36   REPEAT 
    37     ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
    38       (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
    39     );
    40 
    41 val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
    42 by (simp_tac (!simpset addsimps prems) 1);
    43 qed "infsys_p1";
    44 
    45 val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
    46 by (Asm_full_simp_tac 1);
    47 qed "infsys_p2";
    48 
    49 val prems = goal MT.thy 
    50  "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    51 by (Asm_full_simp_tac 1);
    52 qed "infsys_pp1";
    53 
    54 val prems = goal MT.thy 
    55  "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    56 by (Asm_full_simp_tac 1);
    57 qed "infsys_pp2";
    58 
    59 (* ############################################################ *)
    60 (* Fixpoints                                                    *)
    61 (* ############################################################ *)
    62 
    63 (* Least fixpoints *)
    64 
    65 val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
    66 by (rtac subsetD 1);
    67 by (rtac lfp_lemma2 1);
    68 by (resolve_tac prems 1);
    69 by (resolve_tac prems 1);
    70 qed "lfp_intro2";
    71 
    72 val prems = goal MT.thy
    73   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
    74 \   P(x)";
    75 by (cut_facts_tac prems 1);
    76 by (resolve_tac prems 1);
    77 by (rtac subsetD 1);
    78 by (rtac lfp_lemma3 1);
    79 by (assume_tac 1);
    80 by (assume_tac 1);
    81 qed "lfp_elim2";
    82 
    83 val prems = goal MT.thy
    84   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
    85 \   P(x)";
    86 by (cut_facts_tac prems 1);
    87 by (etac induct 1);
    88 by (assume_tac 1);
    89 by (eresolve_tac prems 1);
    90 qed "lfp_ind2";
    91 
    92 (* Greatest fixpoints *)
    93 
    94 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
    95 
    96 val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
    97 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
    98 by (rtac (monoh RS monoD) 1);
    99 by (rtac (UnE RS subsetI) 1);
   100 by (assume_tac 1);
   101 by (fast_tac (set_cs addSIs [cih]) 1);
   102 by (rtac (monoh RS monoD RS subsetD) 1);
   103 by (rtac Un_upper2 1);
   104 by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
   105 qed "gfp_coind2";
   106 
   107 val [gfph,monoh,caseh] = goal MT.thy 
   108   "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
   109 by (rtac caseh 1);
   110 by (rtac subsetD 1);
   111 by (rtac gfp_lemma2 1);
   112 by (rtac monoh 1);
   113 by (rtac gfph 1);
   114 qed "gfp_elim2";
   115 
   116 (* ############################################################ *)
   117 (* Expressions                                                  *)
   118 (* ############################################################ *)
   119 
   120 val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
   121 
   122 val e_disjs = 
   123   [ e_disj_const_var, 
   124     e_disj_const_fn, 
   125     e_disj_const_fix, 
   126     e_disj_const_app,
   127     e_disj_var_fn, 
   128     e_disj_var_fix, 
   129     e_disj_var_app, 
   130     e_disj_fn_fix, 
   131     e_disj_fn_app, 
   132     e_disj_fix_app
   133   ];
   134 
   135 val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
   136 val e_disj_se = (e_disj_si RL [notE]);
   137 
   138 fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
   139 
   140 (* ############################################################ *)
   141 (* Values                                                      *)
   142 (* ############################################################ *)
   143 
   144 val v_disjs = [v_disj_const_clos];
   145 val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
   146 val v_disj_se = (v_disj_si RL [notE]);
   147 
   148 val v_injs = [v_const_inj, v_clos_inj];
   149 
   150 fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
   151 
   152 (* ############################################################ *)
   153 (* Evaluations                                                  *)
   154 (* ############################################################ *)
   155 
   156 (* Monotonicity of eval_fun *)
   157 
   158 goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)";
   159 by infsys_mono_tac;
   160 qed "eval_fun_mono";
   161 
   162 (* Introduction rules *)
   163 
   164 goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
   165 by (rtac lfp_intro2 1);
   166 by (rtac eval_fun_mono 1);
   167 by (rewtac eval_fun_def);
   168 by (fast_tac set_cs 1);
   169 qed "eval_const";
   170 
   171 val prems = goalw MT.thy [eval_def, eval_rel_def] 
   172   "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
   173 by (cut_facts_tac prems 1);
   174 by (rtac lfp_intro2 1);
   175 by (rtac eval_fun_mono 1);
   176 by (rewtac eval_fun_def);
   177 by (fast_tac set_cs 1);
   178 qed "eval_var2";
   179 
   180 val prems = goalw MT.thy [eval_def, eval_rel_def] 
   181   "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
   182 by (cut_facts_tac prems 1);
   183 by (rtac lfp_intro2 1);
   184 by (rtac eval_fun_mono 1);
   185 by (rewtac eval_fun_def);
   186 by (fast_tac set_cs 1);
   187 qed "eval_fn";
   188 
   189 val prems = goalw MT.thy [eval_def, eval_rel_def] 
   190   " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   191 \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
   192 by (cut_facts_tac prems 1);
   193 by (rtac lfp_intro2 1);
   194 by (rtac eval_fun_mono 1);
   195 by (rewtac eval_fun_def);
   196 by (fast_tac set_cs 1);
   197 qed "eval_fix";
   198 
   199 val prems = goalw MT.thy [eval_def, eval_rel_def]
   200   " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
   201 \   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
   202 by (cut_facts_tac prems 1);
   203 by (rtac lfp_intro2 1);
   204 by (rtac eval_fun_mono 1);
   205 by (rewtac eval_fun_def);
   206 by (fast_tac set_cs 1);
   207 qed "eval_app1";
   208 
   209 val prems = goalw MT.thy [eval_def, eval_rel_def] 
   210   " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
   211 \       ve |- e2 ---> v2; \
   212 \       vem + {xm |-> v2} |- em ---> v \
   213 \   |] ==> \
   214 \   ve |- e1 @ e2 ---> v";
   215 by (cut_facts_tac prems 1);
   216 by (rtac lfp_intro2 1);
   217 by (rtac eval_fun_mono 1);
   218 by (rewtac eval_fun_def);
   219 by (fast_tac (set_cs addSIs [disjI2]) 1);
   220 qed "eval_app2";
   221 
   222 (* Strong elimination, induction on evaluations *)
   223 
   224 val prems = goalw MT.thy [eval_def, eval_rel_def]
   225   " [| ve |- e ---> v; \
   226 \      !!ve c. P(((ve,e_const(c)),v_const(c))); \
   227 \      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
   228 \      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
   229 \      !!ev1 ev2 ve cl e. \
   230 \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   231 \        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
   232 \      !!ve c1 c2 e1 e2. \
   233 \        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
   234 \        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
   235 \      !!ve vem xm e1 e2 em v v2. \
   236 \        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
   237 \            P(((ve,e2),v2)); \
   238 \            P(((vem + {xm |-> v2},em),v)) \
   239 \        |] ==> \
   240 \        P(((ve,e1 @ e2),v)) \
   241 \   |] ==> \
   242 \   P(((ve,e),v))";
   243 by (resolve_tac (prems RL [lfp_ind2]) 1);
   244 by (rtac eval_fun_mono 1);
   245 by (rewtac eval_fun_def);
   246 by (dtac CollectD 1);
   247 by (safe_tac HOL_cs);
   248 by (ALLGOALS (resolve_tac prems));
   249 by (ALLGOALS (fast_tac set_cs));
   250 qed "eval_ind0";
   251 
   252 val prems = goal MT.thy 
   253   " [| ve |- e ---> v; \
   254 \      !!ve c. P ve (e_const c) (v_const c); \
   255 \      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
   256 \      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
   257 \      !!ev1 ev2 ve cl e. \
   258 \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   259 \        P ve (fix ev2(ev1) = e) (v_clos cl); \
   260 \      !!ve c1 c2 e1 e2. \
   261 \        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
   262 \        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
   263 \      !!ve vem evm e1 e2 em v v2. \
   264 \        [|  P ve e1 (v_clos <|evm,em,vem|>); \
   265 \            P ve e2 v2; \
   266 \            P (vem + {evm |-> v2}) em v \
   267 \        |] ==> P ve (e1 @ e2) v \
   268 \   |] ==> P ve e v";
   269 by (res_inst_tac [("P","P")] infsys_pp2 1);
   270 by (rtac eval_ind0 1);
   271 by (ALLGOALS (rtac infsys_pp1));
   272 by (ALLGOALS (resolve_tac prems));
   273 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   274 qed "eval_ind";
   275 
   276 (* ############################################################ *)
   277 (* Elaborations                                                 *)
   278 (* ############################################################ *)
   279 
   280 goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)";
   281 by infsys_mono_tac;
   282 qed "elab_fun_mono";
   283 
   284 (* Introduction rules *)
   285 
   286 val prems = goalw MT.thy [elab_def, elab_rel_def] 
   287   "c isof ty ==> te |- e_const(c) ===> ty";
   288 by (cut_facts_tac prems 1);
   289 by (rtac lfp_intro2 1);
   290 by (rtac elab_fun_mono 1);
   291 by (rewtac elab_fun_def);
   292 by (fast_tac set_cs 1);
   293 qed "elab_const";
   294 
   295 val prems = goalw MT.thy [elab_def, elab_rel_def] 
   296   "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   297 by (cut_facts_tac prems 1);
   298 by (rtac lfp_intro2 1);
   299 by (rtac elab_fun_mono 1);
   300 by (rewtac elab_fun_def);
   301 by (fast_tac set_cs 1);
   302 qed "elab_var";
   303 
   304 val prems = goalw MT.thy [elab_def, elab_rel_def] 
   305   "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   306 by (cut_facts_tac prems 1);
   307 by (rtac lfp_intro2 1);
   308 by (rtac elab_fun_mono 1);
   309 by (rewtac elab_fun_def);
   310 by (fast_tac set_cs 1);
   311 qed "elab_fn";
   312 
   313 val prems = goalw MT.thy [elab_def, elab_rel_def]
   314   " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   315 \   te |- fix f(x) = e ===> ty1->ty2";
   316 by (cut_facts_tac prems 1);
   317 by (rtac lfp_intro2 1);
   318 by (rtac elab_fun_mono 1);
   319 by (rewtac elab_fun_def);
   320 by (fast_tac set_cs 1);
   321 qed "elab_fix";
   322 
   323 val prems = goalw MT.thy [elab_def, elab_rel_def] 
   324   " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   325 \   te |- e1 @ e2 ===> ty2";
   326 by (cut_facts_tac prems 1);
   327 by (rtac lfp_intro2 1);
   328 by (rtac elab_fun_mono 1);
   329 by (rewtac elab_fun_def);
   330 by (fast_tac (set_cs addSIs [disjI2]) 1);
   331 qed "elab_app";
   332 
   333 (* Strong elimination, induction on elaborations *)
   334 
   335 val prems = goalw MT.thy [elab_def, elab_rel_def]
   336   " [| te |- e ===> t; \
   337 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   338 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   339 \      !!te x e t1 t2. \
   340 \        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
   341 \        P(((te,fn x => e),t1->t2)); \
   342 \      !!te f x e t1 t2. \
   343 \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
   344 \           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
   345 \        |] ==> \
   346 \        P(((te,fix f(x) = e),t1->t2)); \
   347 \      !!te e1 e2 t1 t2. \
   348 \        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
   349 \           te |- e2 ===> t1; P(((te,e2),t1)) \
   350 \        |] ==> \
   351 \        P(((te,e1 @ e2),t2)) \
   352 \   |] ==> \
   353 \   P(((te,e),t))";
   354 by (resolve_tac (prems RL [lfp_ind2]) 1);
   355 by (rtac elab_fun_mono 1);
   356 by (rewtac elab_fun_def);
   357 by (dtac CollectD 1);
   358 by (safe_tac HOL_cs);
   359 by (ALLGOALS (resolve_tac prems));
   360 by (ALLGOALS (fast_tac set_cs));
   361 qed "elab_ind0";
   362 
   363 val prems = goal MT.thy
   364   " [| te |- e ===> t; \
   365 \       !!te c t. c isof t ==> P te (e_const c) t; \
   366 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
   367 \      !!te x e t1 t2. \
   368 \        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
   369 \        P te (fn x => e) (t1->t2); \
   370 \      !!te f x e t1 t2. \
   371 \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
   372 \           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
   373 \        |] ==> \
   374 \        P te (fix f(x) = e) (t1->t2); \
   375 \      !!te e1 e2 t1 t2. \
   376 \        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
   377 \           te |- e2 ===> t1; P te e2 t1 \
   378 \        |] ==> \
   379 \        P te (e1 @ e2) t2 \ 
   380 \   |] ==> \
   381 \   P te e t";
   382 by (res_inst_tac [("P","P")] infsys_pp2 1);
   383 by (rtac elab_ind0 1);
   384 by (ALLGOALS (rtac infsys_pp1));
   385 by (ALLGOALS (resolve_tac prems));
   386 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   387 qed "elab_ind";
   388 
   389 (* Weak elimination, case analysis on elaborations *)
   390 
   391 val prems = goalw MT.thy [elab_def, elab_rel_def]
   392   " [| te |- e ===> t; \
   393 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   394 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   395 \      !!te x e t1 t2. \
   396 \        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
   397 \      !!te f x e t1 t2. \
   398 \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
   399 \        P(((te,fix f(x) = e),t1->t2)); \
   400 \      !!te e1 e2 t1 t2. \
   401 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
   402 \        P(((te,e1 @ e2),t2)) \
   403 \   |] ==> \
   404 \   P(((te,e),t))";
   405 by (resolve_tac (prems RL [lfp_elim2]) 1);
   406 by (rtac elab_fun_mono 1);
   407 by (rewtac elab_fun_def);
   408 by (dtac CollectD 1);
   409 by (safe_tac HOL_cs);
   410 by (ALLGOALS (resolve_tac prems));
   411 by (ALLGOALS (fast_tac set_cs));
   412 qed "elab_elim0";
   413 
   414 val prems = goal MT.thy
   415   " [| te |- e ===> t; \
   416 \       !!te c t. c isof t ==> P te (e_const c) t; \
   417 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
   418 \      !!te x e t1 t2. \
   419 \        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
   420 \      !!te f x e t1 t2. \
   421 \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
   422 \        P te (fix f(x) = e) (t1->t2); \
   423 \      !!te e1 e2 t1 t2. \
   424 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
   425 \        P te (e1 @ e2) t2 \ 
   426 \   |] ==> \
   427 \   P te e t";
   428 by (res_inst_tac [("P","P")] infsys_pp2 1);
   429 by (rtac elab_elim0 1);
   430 by (ALLGOALS (rtac infsys_pp1));
   431 by (ALLGOALS (resolve_tac prems));
   432 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   433 qed "elab_elim";
   434 
   435 (* Elimination rules for each expression *)
   436 
   437 fun elab_e_elim_tac p = 
   438   ( (rtac elab_elim 1) THEN 
   439     (resolve_tac p 1) THEN 
   440     (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
   441   );
   442 
   443 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
   444 by (elab_e_elim_tac prems);
   445 qed "elab_const_elim_lem";
   446 
   447 val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
   448 by (cut_facts_tac prems 1);
   449 by (dtac elab_const_elim_lem 1);
   450 by (fast_tac prop_cs 1);
   451 qed "elab_const_elim";
   452 
   453 val prems = goal MT.thy 
   454   "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
   455 by (elab_e_elim_tac prems);
   456 qed "elab_var_elim_lem";
   457 
   458 val prems = goal MT.thy 
   459   "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   460 by (cut_facts_tac prems 1);
   461 by (dtac elab_var_elim_lem 1);
   462 by (fast_tac prop_cs 1);
   463 qed "elab_var_elim";
   464 
   465 val prems = goal MT.thy 
   466   " te |- e ===> t ==> \
   467 \   ( e = fn x1 => e1 --> \
   468 \     (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
   469 \   )";
   470 by (elab_e_elim_tac prems);
   471 qed "elab_fn_elim_lem";
   472 
   473 val prems = goal MT.thy 
   474   " te |- fn x1 => e1 ===> t ==> \
   475 \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   476 by (cut_facts_tac prems 1);
   477 by (dtac elab_fn_elim_lem 1);
   478 by (fast_tac prop_cs 1);
   479 qed "elab_fn_elim";
   480 
   481 val prems = goal MT.thy 
   482   " te |- e ===> t ==> \
   483 \   (e = fix f(x) = e1 --> \
   484 \   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
   485 by (elab_e_elim_tac prems);
   486 qed "elab_fix_elim_lem";
   487 
   488 val prems = goal MT.thy 
   489   " te |- fix ev1(ev2) = e1 ===> t ==> \
   490 \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   491 by (cut_facts_tac prems 1);
   492 by (dtac elab_fix_elim_lem 1);
   493 by (fast_tac prop_cs 1);
   494 qed "elab_fix_elim";
   495 
   496 val prems = goal MT.thy 
   497   " te |- e ===> t2 ==> \
   498 \   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
   499 by (elab_e_elim_tac prems);
   500 qed "elab_app_elim_lem";
   501 
   502 val prems = goal MT.thy
   503  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
   504 by (cut_facts_tac prems 1);
   505 by (dtac elab_app_elim_lem 1);
   506 by (fast_tac prop_cs 1);
   507 qed "elab_app_elim";
   508 
   509 (* ############################################################ *)
   510 (* The extended correspondence relation                       *)
   511 (* ############################################################ *)
   512 
   513 (* Monotonicity of hasty_fun *)
   514 
   515 goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)";
   516 by infsys_mono_tac;
   517 bind_thm("mono_hasty_fun",  result());
   518 
   519 (* 
   520   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it 
   521   enjoys two strong indtroduction (co-induction) rules and an elimination rule.
   522 *)
   523 
   524 (* First strong indtroduction (co-induction) rule for hasty_rel *)
   525 
   526 val prems =
   527   goalw MT.thy [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
   528 by (cut_facts_tac prems 1);
   529 by (rtac gfp_coind2 1);
   530 by (rewtac MT.hasty_fun_def);
   531 by (rtac CollectI 1);
   532 by (rtac disjI1 1);
   533 by (fast_tac HOL_cs 1);
   534 by (rtac mono_hasty_fun 1);
   535 qed "hasty_rel_const_coind";
   536 
   537 (* Second strong introduction (co-induction) rule for hasty_rel *)
   538 
   539 val prems = goalw MT.thy [hasty_rel_def]
   540   " [|  te |- fn ev => e ===> t; \
   541 \       ve_dom(ve) = te_dom(te); \
   542 \       ! ev1. \
   543 \         ev1:ve_dom(ve) --> \
   544 \         (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
   545 \   |] ==> \
   546 \   (v_clos(<|ev,e,ve|>),t) : hasty_rel";
   547 by (cut_facts_tac prems 1);
   548 by (rtac gfp_coind2 1);
   549 by (rewtac hasty_fun_def);
   550 by (rtac CollectI 1);
   551 by (rtac disjI2 1);
   552 by (fast_tac HOL_cs 1);
   553 by (rtac mono_hasty_fun 1);
   554 qed "hasty_rel_clos_coind";
   555 
   556 (* Elimination rule for hasty_rel *)
   557 
   558 val prems = goalw MT.thy [hasty_rel_def]
   559   " [| !! c t.c isof t ==> P((v_const(c),t)); \
   560 \      !! te ev e t ve. \
   561 \        [| te |- fn ev => e ===> t; \
   562 \           ve_dom(ve) = te_dom(te); \
   563 \           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
   564 \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
   565 \      (v,t) : hasty_rel \
   566 \   |] ==> P((v,t))";
   567 by (cut_facts_tac prems 1);
   568 by (etac gfp_elim2 1);
   569 by (rtac mono_hasty_fun 1);
   570 by (rewtac hasty_fun_def);
   571 by (dtac CollectD 1);
   572 by (fold_goals_tac [hasty_fun_def]);
   573 by (safe_tac HOL_cs);
   574 by (ALLGOALS (resolve_tac prems));
   575 by (ALLGOALS (fast_tac set_cs));
   576 qed "hasty_rel_elim0";
   577 
   578 val prems = goal MT.thy 
   579   " [| (v,t) : hasty_rel; \
   580 \      !! c t.c isof t ==> P (v_const c) t; \
   581 \      !! te ev e t ve. \
   582 \        [| te |- fn ev => e ===> t; \
   583 \           ve_dom(ve) = te_dom(te); \
   584 \           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
   585 \        |] ==> P (v_clos <|ev,e,ve|>) t \
   586 \   |] ==> P v t";
   587 by (res_inst_tac [("P","P")] infsys_p2 1);
   588 by (rtac hasty_rel_elim0 1);
   589 by (ALLGOALS (rtac infsys_p1));
   590 by (ALLGOALS (resolve_tac prems));
   591 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1)));
   592 qed "hasty_rel_elim";
   593 
   594 (* Introduction rules for hasty *)
   595 
   596 val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t";
   597 by (resolve_tac (prems RL [hasty_rel_const_coind]) 1);
   598 qed "hasty_const";
   599 
   600 val prems = goalw MT.thy [hasty_def,hasty_env_def] 
   601   "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
   602 by (cut_facts_tac prems 1);
   603 by (rtac hasty_rel_clos_coind 1);
   604 by (ALLGOALS (fast_tac set_cs));
   605 qed "hasty_clos";
   606 
   607 (* Elimination on constants for hasty *)
   608 
   609 val prems = goalw MT.thy [hasty_def] 
   610   "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
   611 by (cut_facts_tac prems 1);
   612 by (rtac hasty_rel_elim 1);
   613 by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
   614 qed "hasty_elim_const_lem";
   615 
   616 val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
   617 by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
   618 by (fast_tac HOL_cs 1);
   619 qed "hasty_elim_const";
   620 
   621 (* Elimination on closures for hasty *)
   622 
   623 val prems = goalw MT.thy [hasty_env_def,hasty_def] 
   624   " v hasty t ==> \
   625 \   ! x e ve. \
   626 \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
   627 by (cut_facts_tac prems 1);
   628 by (rtac hasty_rel_elim 1);
   629 by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
   630 qed "hasty_elim_clos_lem";
   631 
   632 val prems = goal MT.thy 
   633   "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
   634   \t & ve hastyenv te ";
   635 by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
   636 by (fast_tac HOL_cs 1);
   637 qed "hasty_elim_clos";
   638 
   639 (* ############################################################ *)
   640 (* The pointwise extension of hasty to environments             *)
   641 (* ############################################################ *)
   642 
   643 goal MT.thy
   644   "!!ve. [| ve hastyenv te; v hasty t |] ==> \
   645 \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   646 by (rewtac hasty_env_def);
   647 by (asm_full_simp_tac (!simpset delsimps mem_simps
   648                                 addsimps [ve_dom_owr, te_dom_owr]) 1);
   649 by (safe_tac HOL_cs);
   650 by (excluded_middle_tac "ev=x" 1);
   651 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   652 by (fast_tac set_cs 1);
   653 by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
   654 qed "hasty_env1";
   655 
   656 (* ############################################################ *)
   657 (* The Consistency theorem                                      *)
   658 (* ############################################################ *)
   659 
   660 val prems = goal MT.thy 
   661   "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   662 by (cut_facts_tac prems 1);
   663 by (dtac elab_const_elim 1);
   664 by (etac hasty_const 1);
   665 qed "consistency_const";
   666 
   667 val prems = goalw MT.thy [hasty_env_def]
   668   " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   669 \   ve_app ve ev hasty t";
   670 by (cut_facts_tac prems 1);
   671 by (dtac elab_var_elim 1);
   672 by (fast_tac HOL_cs 1);
   673 qed "consistency_var";
   674 
   675 val prems = goal MT.thy
   676   " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   677 \   v_clos(<| ev, e, ve |>) hasty t";
   678 by (cut_facts_tac prems 1);
   679 by (rtac hasty_clos 1);
   680 by (fast_tac prop_cs 1);
   681 qed "consistency_fn";
   682 
   683 val prems = goalw MT.thy [hasty_env_def,hasty_def]
   684   " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   685 \      ve hastyenv te ; \
   686 \      te |- fix ev2  ev1  = e ===> t \
   687 \   |] ==> \
   688 \   v_clos(cl) hasty t";
   689 by (cut_facts_tac prems 1);
   690 by (dtac elab_fix_elim 1);
   691 by (safe_tac HOL_cs);
   692 (*Do a single unfolding of cl*)
   693 by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
   694 by (rtac hasty_rel_clos_coind 1);
   695 by (etac elab_fn 1);
   696 by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
   697 
   698 by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
   699 by (safe_tac HOL_cs);
   700 by (excluded_middle_tac "ev2=ev1a" 1);
   701 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
   702 by (fast_tac set_cs 1);
   703 
   704 by (asm_simp_tac (!simpset delsimps mem_simps
   705                            addsimps [ve_app_owr1, te_app_owr1]) 1);
   706 by (hyp_subst_tac 1);
   707 by (etac subst 1);
   708 by (fast_tac set_cs 1);
   709 qed "consistency_fix";
   710 
   711 val prems = goal MT.thy 
   712   " [| ! t te. ve hastyenv te  --> te |- e1 ===> t --> v_const(c1) hasty t; \
   713 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
   714 \      ve hastyenv te ; te |- e1 @ e2 ===> t \
   715 \   |] ==> \
   716 \   v_const(c_app c1 c2) hasty t";
   717 by (cut_facts_tac prems 1);
   718 by (dtac elab_app_elim 1);
   719 by (safe_tac HOL_cs);
   720 by (rtac hasty_const 1);
   721 by (rtac isof_app 1);
   722 by (rtac hasty_elim_const 1);
   723 by (fast_tac HOL_cs 1);
   724 by (rtac hasty_elim_const 1);
   725 by (fast_tac HOL_cs 1);
   726 qed "consistency_app1";
   727 
   728 val prems = goal MT.thy 
   729   " [| ! t te. \
   730 \        ve hastyenv te  --> \
   731 \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
   732 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
   733 \      ! t te. \
   734 \        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
   735 \      ve hastyenv te ; \
   736 \      te |- e1 @ e2 ===> t \
   737 \   |] ==> \
   738 \   v hasty t";
   739 by (cut_facts_tac prems 1);
   740 by (dtac elab_app_elim 1);
   741 by (safe_tac HOL_cs);
   742 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   743 by (assume_tac 1);
   744 by (etac impE 1);
   745 by (assume_tac 1);
   746 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   747 by (assume_tac 1);
   748 by (etac impE 1);
   749 by (assume_tac 1);
   750 by (dtac hasty_elim_clos 1);
   751 by (safe_tac HOL_cs);
   752 by (dtac elab_fn_elim 1);
   753 by (safe_tac HOL_cs);
   754 by (dtac t_fun_inj 1);
   755 by (safe_tac prop_cs);
   756 by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
   757 qed "consistency_app2";
   758 
   759 val [major] = goal MT.thy 
   760   "ve |- e ---> v ==> \
   761 \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   762 
   763 (* Proof by induction on the structure of evaluations *)
   764 
   765 by (rtac (major RS eval_ind) 1);
   766 by (safe_tac HOL_cs);
   767 by (DEPTH_SOLVE 
   768     (ares_tac [consistency_const, consistency_var, consistency_fn,
   769                consistency_fix, consistency_app1, consistency_app2] 1));
   770 qed "consistency";
   771 
   772 (* ############################################################ *)
   773 (* The Basic Consistency theorem                                *)
   774 (* ############################################################ *)
   775 
   776 val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   777   "ve isofenv te ==> ve hastyenv te";
   778 by (cut_facts_tac prems 1);
   779 by (safe_tac HOL_cs);
   780 by (etac allE 1);
   781 by (etac impE 1);
   782 by (assume_tac 1);
   783 by (etac exE 1);
   784 by (etac conjE 1);
   785 by (dtac hasty_const 1);
   786 by (Asm_simp_tac 1);
   787 qed "basic_consistency_lem";
   788 
   789 val prems = goal MT.thy
   790   "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
   791 by (cut_facts_tac prems 1);
   792 by (rtac hasty_elim_const 1);
   793 by (dtac consistency 1);
   794 by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
   795 qed "basic_consistency";