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