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