src/HOL/ex/MT.ML
author paulson
Wed Jul 15 14:19:02 1998 +0200 (1998-07-15)
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5227 e5a6ace920a0
permissions -rw-r--r--
More tidying and removal of "\!\!... from 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 Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
    31 by (Asm_full_simp_tac 1);
    32 qed "infsys_p2";
    33 
    34 Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
    35 by (Asm_full_simp_tac 1);
    36 qed "infsys_pp1";
    37 
    38 Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
    39 by (Asm_full_simp_tac 1);
    40 qed "infsys_pp2";
    41 
    42 (* ############################################################ *)
    43 (* Fixpoints                                                    *)
    44 (* ############################################################ *)
    45 
    46 (* Least fixpoints *)
    47 
    48 val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)";
    49 by (rtac subsetD 1);
    50 by (rtac lfp_lemma2 1);
    51 by (resolve_tac prems 1);
    52 by (resolve_tac prems 1);
    53 qed "lfp_intro2";
    54 
    55 val prems = goal MT.thy
    56   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \
    57 \   P(x)";
    58 by (cut_facts_tac prems 1);
    59 by (resolve_tac prems 1);
    60 by (rtac subsetD 1);
    61 by (rtac lfp_lemma3 1);
    62 by (assume_tac 1);
    63 by (assume_tac 1);
    64 qed "lfp_elim2";
    65 
    66 val prems = goal MT.thy
    67   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
    68 \   P(x)";
    69 by (cut_facts_tac prems 1);
    70 by (etac induct 1);
    71 by (assume_tac 1);
    72 by (eresolve_tac prems 1);
    73 qed "lfp_ind2";
    74 
    75 (* Greatest fixpoints *)
    76 
    77 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
    78 
    79 val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)";
    80 by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1);
    81 by (rtac (monoh RS monoD) 1);
    82 by (rtac (UnE RS subsetI) 1);
    83 by (assume_tac 1);
    84 by (blast_tac (claset() addSIs [cih]) 1);
    85 by (rtac (monoh RS monoD RS subsetD) 1);
    86 by (rtac Un_upper2 1);
    87 by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
    88 qed "gfp_coind2";
    89 
    90 val [gfph,monoh,caseh] = goal MT.thy 
    91   "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)";
    92 by (rtac caseh 1);
    93 by (rtac subsetD 1);
    94 by (rtac gfp_lemma2 1);
    95 by (rtac monoh 1);
    96 by (rtac gfph 1);
    97 qed "gfp_elim2";
    98 
    99 (* ############################################################ *)
   100 (* Expressions                                                  *)
   101 (* ############################################################ *)
   102 
   103 val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj];
   104 
   105 val e_disjs = 
   106   [ e_disj_const_var, 
   107     e_disj_const_fn, 
   108     e_disj_const_fix, 
   109     e_disj_const_app,
   110     e_disj_var_fn, 
   111     e_disj_var_fix, 
   112     e_disj_var_app, 
   113     e_disj_fn_fix, 
   114     e_disj_fn_app, 
   115     e_disj_fix_app
   116   ];
   117 
   118 val e_disj_si = e_disjs @ (e_disjs RL [not_sym]);
   119 val e_disj_se = (e_disj_si RL [notE]);
   120 
   121 fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs;
   122 
   123 (* ############################################################ *)
   124 (* Values                                                      *)
   125 (* ############################################################ *)
   126 
   127 val v_disjs = [v_disj_const_clos];
   128 val v_disj_si = v_disjs @ (v_disjs RL [not_sym]);
   129 val v_disj_se = (v_disj_si RL [notE]);
   130 
   131 val v_injs = [v_const_inj, v_clos_inj];
   132 
   133 fun v_ext_cs cs  = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs;
   134 
   135 (* ############################################################ *)
   136 (* Evaluations                                                  *)
   137 (* ############################################################ *)
   138 
   139 (* Monotonicity of eval_fun *)
   140 
   141 Goalw [mono_def, eval_fun_def] "mono(eval_fun)";
   142 by infsys_mono_tac;
   143 qed "eval_fun_mono";
   144 
   145 (* Introduction rules *)
   146 
   147 Goalw [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)";
   148 by (rtac lfp_intro2 1);
   149 by (rtac eval_fun_mono 1);
   150 by (rewtac eval_fun_def);
   151 	(*Naughty!  But the quantifiers are nested VERY deeply...*)
   152 by (blast_tac (claset() addSIs [exI]) 1);
   153 qed "eval_const";
   154 
   155 Goalw [eval_def, eval_rel_def] 
   156   "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
   157 by (rtac lfp_intro2 1);
   158 by (rtac eval_fun_mono 1);
   159 by (rewtac eval_fun_def);
   160 by (blast_tac (claset() addSIs [exI]) 1);
   161 qed "eval_var2";
   162 
   163 Goalw [eval_def, eval_rel_def] 
   164   "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
   165 by (rtac lfp_intro2 1);
   166 by (rtac eval_fun_mono 1);
   167 by (rewtac eval_fun_def);
   168 by (blast_tac (claset() addSIs [exI]) 1);
   169 qed "eval_fn";
   170 
   171 Goalw [eval_def, eval_rel_def] 
   172   " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   173 \   ve |- fix ev2(ev1) = e ---> v_clos(cl)";
   174 by (rtac lfp_intro2 1);
   175 by (rtac eval_fun_mono 1);
   176 by (rewtac eval_fun_def);
   177 by (blast_tac (claset() addSIs [exI]) 1);
   178 qed "eval_fix";
   179 
   180 Goalw [eval_def, eval_rel_def]
   181   " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
   182 \   ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
   183 by (rtac lfp_intro2 1);
   184 by (rtac eval_fun_mono 1);
   185 by (rewtac eval_fun_def);
   186 by (blast_tac (claset() addSIs [exI]) 1);
   187 qed "eval_app1";
   188 
   189 Goalw [eval_def, eval_rel_def] 
   190   " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>); \
   191 \       ve |- e2 ---> v2; \
   192 \       vem + {xm |-> v2} |- em ---> v \
   193 \   |] ==> \
   194 \   ve |- e1 @ e2 ---> v";
   195 by (rtac lfp_intro2 1);
   196 by (rtac eval_fun_mono 1);
   197 by (rewtac eval_fun_def);
   198 by (blast_tac (claset() addSIs [disjI2]) 1);
   199 qed "eval_app2";
   200 
   201 (* Strong elimination, induction on evaluations *)
   202 
   203 val prems = goalw MT.thy [eval_def, eval_rel_def]
   204   " [| ve |- e ---> v; \
   205 \      !!ve c. P(((ve,e_const(c)),v_const(c))); \
   206 \      !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev)); \
   207 \      !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>))); \
   208 \      !!ev1 ev2 ve cl e. \
   209 \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   210 \        P(((ve,fix ev2(ev1) = e),v_clos(cl))); \
   211 \      !!ve c1 c2 e1 e2. \
   212 \        [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==> \
   213 \        P(((ve,e1 @ e2),v_const(c_app c1 c2))); \
   214 \      !!ve vem xm e1 e2 em v v2. \
   215 \        [|  P(((ve,e1),v_clos(<|xm,em,vem|>))); \
   216 \            P(((ve,e2),v2)); \
   217 \            P(((vem + {xm |-> v2},em),v)) \
   218 \        |] ==> \
   219 \        P(((ve,e1 @ e2),v)) \
   220 \   |] ==> \
   221 \   P(((ve,e),v))";
   222 by (resolve_tac (prems RL [lfp_ind2]) 1);
   223 by (rtac eval_fun_mono 1);
   224 by (rewtac eval_fun_def);
   225 by (dtac CollectD 1);
   226 by Safe_tac;
   227 by (ALLGOALS (resolve_tac prems));
   228 by (ALLGOALS (Blast_tac));
   229 qed "eval_ind0";
   230 
   231 val prems = goal MT.thy 
   232   " [| ve |- e ---> v; \
   233 \      !!ve c. P ve (e_const c) (v_const c); \
   234 \      !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \
   235 \      !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \
   236 \      !!ev1 ev2 ve cl e. \
   237 \        cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
   238 \        P ve (fix ev2(ev1) = e) (v_clos cl); \
   239 \      !!ve c1 c2 e1 e2. \
   240 \        [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \
   241 \        P ve (e1 @ e2) (v_const(c_app c1 c2)); \
   242 \      !!ve vem evm e1 e2 em v v2. \
   243 \        [|  P ve e1 (v_clos <|evm,em,vem|>); \
   244 \            P ve e2 v2; \
   245 \            P (vem + {evm |-> v2}) em v \
   246 \        |] ==> P ve (e1 @ e2) v \
   247 \   |] ==> P ve e v";
   248 by (res_inst_tac [("P","P")] infsys_pp2 1);
   249 by (rtac eval_ind0 1);
   250 by (ALLGOALS (rtac infsys_pp1));
   251 by (ALLGOALS (resolve_tac prems));
   252 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   253 qed "eval_ind";
   254 
   255 (* ############################################################ *)
   256 (* Elaborations                                                 *)
   257 (* ############################################################ *)
   258 
   259 Goalw [mono_def, elab_fun_def] "mono(elab_fun)";
   260 by infsys_mono_tac;
   261 qed "elab_fun_mono";
   262 
   263 (* Introduction rules *)
   264 
   265 Goalw [elab_def, elab_rel_def] 
   266   "c isof ty ==> te |- e_const(c) ===> ty";
   267 by (rtac lfp_intro2 1);
   268 by (rtac elab_fun_mono 1);
   269 by (rewtac elab_fun_def);
   270 by (blast_tac (claset() addSIs [exI]) 1);
   271 qed "elab_const";
   272 
   273 Goalw [elab_def, elab_rel_def] 
   274   "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
   275 by (rtac lfp_intro2 1);
   276 by (rtac elab_fun_mono 1);
   277 by (rewtac elab_fun_def);
   278 by (blast_tac (claset() addSIs [exI]) 1);
   279 qed "elab_var";
   280 
   281 Goalw [elab_def, elab_rel_def] 
   282   "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
   283 by (rtac lfp_intro2 1);
   284 by (rtac elab_fun_mono 1);
   285 by (rewtac elab_fun_def);
   286 by (blast_tac (claset() addSIs [exI]) 1);
   287 qed "elab_fn";
   288 
   289 Goalw [elab_def, elab_rel_def]
   290   "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
   291 \        te |- fix f(x) = e ===> ty1->ty2";
   292 by (rtac lfp_intro2 1);
   293 by (rtac elab_fun_mono 1);
   294 by (rewtac elab_fun_def);
   295 by (blast_tac (claset() addSIs [exI]) 1);
   296 qed "elab_fix";
   297 
   298 Goalw [elab_def, elab_rel_def] 
   299   "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
   300 \        te |- e1 @ e2 ===> ty2";
   301 by (rtac lfp_intro2 1);
   302 by (rtac elab_fun_mono 1);
   303 by (rewtac elab_fun_def);
   304 by (blast_tac (claset() addSIs [disjI2]) 1);
   305 qed "elab_app";
   306 
   307 (* Strong elimination, induction on elaborations *)
   308 
   309 val prems = goalw MT.thy [elab_def, elab_rel_def]
   310   " [| te |- e ===> t; \
   311 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   312 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   313 \      !!te x e t1 t2. \
   314 \        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==> \
   315 \        P(((te,fn x => e),t1->t2)); \
   316 \      !!te f x e t1 t2. \
   317 \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
   318 \           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2)) \
   319 \        |] ==> \
   320 \        P(((te,fix f(x) = e),t1->t2)); \
   321 \      !!te e1 e2 t1 t2. \
   322 \        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2)); \
   323 \           te |- e2 ===> t1; P(((te,e2),t1)) \
   324 \        |] ==> \
   325 \        P(((te,e1 @ e2),t2)) \
   326 \   |] ==> \
   327 \   P(((te,e),t))";
   328 by (resolve_tac (prems RL [lfp_ind2]) 1);
   329 by (rtac elab_fun_mono 1);
   330 by (rewtac elab_fun_def);
   331 by (dtac CollectD 1);
   332 by Safe_tac;
   333 by (ALLGOALS (resolve_tac prems));
   334 by (ALLGOALS (Blast_tac));
   335 qed "elab_ind0";
   336 
   337 val prems = goal MT.thy
   338   " [| te |- e ===> t; \
   339 \       !!te c t. c isof t ==> P te (e_const c) t; \
   340 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
   341 \      !!te x e t1 t2. \
   342 \        [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \
   343 \        P te (fn x => e) (t1->t2); \
   344 \      !!te f x e t1 t2. \
   345 \        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \
   346 \           P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \
   347 \        |] ==> \
   348 \        P te (fix f(x) = e) (t1->t2); \
   349 \      !!te e1 e2 t1 t2. \
   350 \        [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \
   351 \           te |- e2 ===> t1; P te e2 t1 \
   352 \        |] ==> \
   353 \        P te (e1 @ e2) t2 \ 
   354 \   |] ==> \
   355 \   P te e t";
   356 by (res_inst_tac [("P","P")] infsys_pp2 1);
   357 by (rtac elab_ind0 1);
   358 by (ALLGOALS (rtac infsys_pp1));
   359 by (ALLGOALS (resolve_tac prems));
   360 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   361 qed "elab_ind";
   362 
   363 (* Weak elimination, case analysis on elaborations *)
   364 
   365 val prems = goalw MT.thy [elab_def, elab_rel_def]
   366   " [| te |- e ===> t; \
   367 \      !!te c t. c isof t ==> P(((te,e_const(c)),t)); \
   368 \      !!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x)); \
   369 \      !!te x e t1 t2. \
   370 \        te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2)); \
   371 \      !!te f x e t1 t2. \
   372 \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
   373 \        P(((te,fix f(x) = e),t1->t2)); \
   374 \      !!te e1 e2 t1 t2. \
   375 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
   376 \        P(((te,e1 @ e2),t2)) \
   377 \   |] ==> \
   378 \   P(((te,e),t))";
   379 by (resolve_tac (prems RL [lfp_elim2]) 1);
   380 by (rtac elab_fun_mono 1);
   381 by (rewtac elab_fun_def);
   382 by (dtac CollectD 1);
   383 by Safe_tac;
   384 by (ALLGOALS (resolve_tac prems));
   385 by (ALLGOALS (Blast_tac));
   386 qed "elab_elim0";
   387 
   388 val prems = goal MT.thy
   389   " [| te |- e ===> t; \
   390 \       !!te c t. c isof t ==> P te (e_const c) t; \
   391 \      !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \
   392 \      !!te x e t1 t2. \
   393 \        te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \
   394 \      !!te f x e t1 t2. \
   395 \        te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \
   396 \        P te (fix f(x) = e) (t1->t2); \
   397 \      !!te e1 e2 t1 t2. \
   398 \        [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \
   399 \        P te (e1 @ e2) t2 \ 
   400 \   |] ==> \
   401 \   P te e t";
   402 by (res_inst_tac [("P","P")] infsys_pp2 1);
   403 by (rtac elab_elim0 1);
   404 by (ALLGOALS (rtac infsys_pp1));
   405 by (ALLGOALS (resolve_tac prems));
   406 by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1)));
   407 qed "elab_elim";
   408 
   409 (* Elimination rules for each expression *)
   410 
   411 fun elab_e_elim_tac p = 
   412   ( (rtac elab_elim 1) THEN 
   413     (resolve_tac p 1) THEN 
   414     (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
   415   );
   416 
   417 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
   418 by (elab_e_elim_tac prems);
   419 qed "elab_const_elim_lem";
   420 
   421 Goal "te |- e_const(c) ===> t ==> c isof t";
   422 by (dtac elab_const_elim_lem 1);
   423 by (Blast_tac 1);
   424 qed "elab_const_elim";
   425 
   426 val prems = goal MT.thy 
   427   "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))";
   428 by (elab_e_elim_tac prems);
   429 qed "elab_var_elim_lem";
   430 
   431 Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
   432 by (dtac elab_var_elim_lem 1);
   433 by (Blast_tac 1);
   434 qed "elab_var_elim";
   435 
   436 val prems = goal MT.thy 
   437   " te |- e ===> t ==> \
   438 \   ( e = fn x1 => e1 --> \
   439 \     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
   440 \   )";
   441 by (elab_e_elim_tac prems);
   442 qed "elab_fn_elim_lem";
   443 
   444 Goal 
   445   " te |- fn x1 => e1 ===> t ==> \
   446 \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
   447 by (dtac elab_fn_elim_lem 1);
   448 by (Blast_tac 1);
   449 qed "elab_fn_elim";
   450 
   451 val prems = goal MT.thy 
   452   " te |- e ===> t ==> \
   453 \   (e = fix f(x) = e1 --> \
   454 \   (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; 
   455 by (elab_e_elim_tac prems);
   456 qed "elab_fix_elim_lem";
   457 
   458 Goal 
   459   " te |- fix ev1(ev2) = e1 ===> t ==> \
   460 \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
   461 by (dtac elab_fix_elim_lem 1);
   462 by (Blast_tac 1);
   463 qed "elab_fix_elim";
   464 
   465 val prems = goal MT.thy 
   466   " te |- e ===> t2 ==> \
   467 \   (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; 
   468 by (elab_e_elim_tac prems);
   469 qed "elab_app_elim_lem";
   470 
   471 Goal
   472  "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,MT.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 MT.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 MT.thy [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 MT.thy 
   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 
   595   "v_clos(<|ev,e,ve|>) hasty t ==>  \
   596 \       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
   597 by (dtac hasty_elim_clos_lem 1);
   598 by (Blast_tac 1);
   599 qed "hasty_elim_clos";
   600 
   601 (* ############################################################ *)
   602 (* The pointwise extension of hasty to environments             *)
   603 (* ############################################################ *)
   604 
   605 Goal
   606   "[| ve hastyenv te; v hasty t |] ==> \
   607 \        ve + {ev |-> v} hastyenv te + {ev |=> t}";
   608 by (rewtac hasty_env_def);
   609 by (asm_full_simp_tac (simpset() delsimps mem_simps
   610                                 addsimps [ve_dom_owr, te_dom_owr]) 1);
   611 by (safe_tac HOL_cs);
   612 by (excluded_middle_tac "ev=x" 1);
   613 by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
   614 by (Blast_tac 1);
   615 by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
   616 qed "hasty_env1";
   617 
   618 (* ############################################################ *)
   619 (* The Consistency theorem                                      *)
   620 (* ############################################################ *)
   621 
   622 Goal 
   623   "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
   624 by (dtac elab_const_elim 1);
   625 by (etac hasty_const 1);
   626 qed "consistency_const";
   627 
   628 Goalw [hasty_env_def]
   629   "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
   630 \       ve_app ve ev hasty t";
   631 by (dtac elab_var_elim 1);
   632 by (Blast_tac 1);
   633 qed "consistency_var";
   634 
   635 Goal
   636   "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
   637 \       v_clos(<| ev, e, ve |>) hasty t";
   638 by (rtac hasty_clos 1);
   639 by (Blast_tac 1);
   640 qed "consistency_fn";
   641 
   642 Goalw [hasty_env_def,hasty_def]
   643   "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
   644 \      ve hastyenv te ; \
   645 \      te |- fix ev2  ev1  = e ===> t \
   646 \   |] ==> \
   647 \   v_clos(cl) hasty t";
   648 by (dtac elab_fix_elim 1);
   649 by (safe_tac HOL_cs);
   650 (*Do a single unfolding of cl*)
   651 by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
   652 by (rtac hasty_rel_clos_coind 1);
   653 by (etac elab_fn 1);
   654 by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
   655 
   656 by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1);
   657 by (safe_tac HOL_cs);
   658 by (excluded_middle_tac "ev2=ev1a" 1);
   659 by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
   660 by (Blast_tac 1);
   661 
   662 by (asm_simp_tac (simpset() delsimps mem_simps
   663                            addsimps [ve_app_owr1, te_app_owr1]) 1);
   664 by (hyp_subst_tac 1);
   665 by (etac subst 1);
   666 by (Blast_tac 1);
   667 qed "consistency_fix";
   668 
   669 Goal 
   670   "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
   671 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t; \
   672 \      ve hastyenv te ; te |- e1 @ e2 ===> t \
   673 \   |] ==> \
   674 \   v_const(c_app c1 c2) hasty t";
   675 by (dtac elab_app_elim 1);
   676 by Safe_tac;
   677 by (rtac hasty_const 1);
   678 by (rtac isof_app 1);
   679 by (rtac hasty_elim_const 1);
   680 by (Blast_tac 1);
   681 by (rtac hasty_elim_const 1);
   682 by (Blast_tac 1);
   683 qed "consistency_app1";
   684 
   685 Goal 
   686   "[| ! t te. \
   687 \        ve hastyenv te  --> \
   688 \        te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
   689 \      ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t; \
   690 \      ! t te. \
   691 \        vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t; \
   692 \      ve hastyenv te ; \
   693 \      te |- e1 @ e2 ===> t \
   694 \   |] ==> \
   695 \   v hasty t";
   696 by (dtac elab_app_elim 1);
   697 by Safe_tac;
   698 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   699 by (assume_tac 1);
   700 by (etac impE 1);
   701 by (assume_tac 1);
   702 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   703 by (assume_tac 1);
   704 by (etac impE 1);
   705 by (assume_tac 1);
   706 by (dtac hasty_elim_clos 1);
   707 by Safe_tac;
   708 by (dtac elab_fn_elim 1);
   709 by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
   710 qed "consistency_app2";
   711 
   712 Goal
   713   "ve |- e ---> v ==> \
   714 \  (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
   715 
   716 (* Proof by induction on the structure of evaluations *)
   717 
   718 by (etac eval_ind 1);
   719 by Safe_tac;
   720 by (DEPTH_SOLVE 
   721     (ares_tac [consistency_const, consistency_var, consistency_fn,
   722                consistency_fix, consistency_app1, consistency_app2] 1));
   723 qed "consistency";
   724 
   725 (* ############################################################ *)
   726 (* The Basic Consistency theorem                                *)
   727 (* ############################################################ *)
   728 
   729 Goalw [isof_env_def,hasty_env_def] 
   730   "ve isofenv te ==> ve hastyenv te";
   731 by Safe_tac;
   732 by (etac allE 1);
   733 by (etac impE 1);
   734 by (assume_tac 1);
   735 by (etac exE 1);
   736 by (etac conjE 1);
   737 by (dtac hasty_const 1);
   738 by (Asm_simp_tac 1);
   739 qed "basic_consistency_lem";
   740 
   741 Goal
   742   "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
   743 by (rtac hasty_elim_const 1);
   744 by (dtac consistency 1);
   745 by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
   746 qed "basic_consistency";
   747 
   748 writeln"Reached end of file.";