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