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