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