src/HOL/ex/MT.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61343 5b5656a63bd6
permissions -rw-r--r--
eliminated old defs;
     1 (*  Title:      HOL/ex/MT.thy
     2     Author:     Jacob Frost, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Based upon the article
     6     Robin Milner and Mads Tofte,
     7     Co-induction in Relational Semantics,
     8     Theoretical Computer Science 87 (1991), pages 209-220.
     9 
    10 Written up as
    11     Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
    12     Report 308, Computer Lab, University of Cambridge (1993).
    13 *)
    14 
    15 section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close>
    16 
    17 theory MT
    18 imports Main
    19 begin
    20 
    21 typedecl Const
    22 
    23 typedecl ExVar
    24 typedecl Ex
    25 
    26 typedecl TyConst
    27 typedecl Ty
    28 
    29 typedecl Clos
    30 typedecl Val
    31 
    32 typedecl ValEnv
    33 typedecl TyEnv
    34 
    35 consts
    36   c_app :: "[Const, Const] => Const"
    37 
    38   e_const :: "Const => Ex"
    39   e_var :: "ExVar => Ex"
    40   e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
    41   e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
    42   e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000)
    43   e_const_fst :: "Ex => Const"
    44 
    45   t_const :: "TyConst => Ty"
    46   t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
    47 
    48   v_const :: "Const => Val"
    49   v_clos :: "Clos => Val"
    50 
    51   ve_emp :: ValEnv
    52   ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
    53   ve_dom :: "ValEnv => ExVar set"
    54   ve_app :: "[ValEnv, ExVar] => Val"
    55 
    56   clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
    57 
    58   te_emp :: TyEnv
    59   te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
    60   te_app :: "[TyEnv, ExVar] => Ty"
    61   te_dom :: "TyEnv => ExVar set"
    62 
    63   isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
    64 
    65 (*
    66   Expression constructors must be injective, distinct and it must be possible
    67   to do induction over expressions.
    68 *)
    69 
    70 (* All the constructors are injective *)
    71 axiomatization where
    72   e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2" and
    73   e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" and
    74   e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" and
    75   e_fix_inj:
    76     " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
    77      ev11 = ev21 & ev12 = ev22 & e1 = e2" and
    78   e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
    79 
    80 (* All constructors are distinct *)
    81 
    82 axiomatization where
    83   e_disj_const_var: "~e_const(c) = e_var(ev)" and
    84   e_disj_const_fn: "~e_const(c) = fn ev => e" and
    85   e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e" and
    86   e_disj_const_app: "~e_const(c) = e1 @@ e2" and
    87   e_disj_var_fn: "~e_var(ev1) = fn ev2 => e" and
    88   e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e" and
    89   e_disj_var_app: "~e_var(ev) = e1 @@ e2" and
    90   e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2" and
    91   e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22" and
    92   e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
    93 
    94 (* Strong elimination, induction on expressions  *)
    95 
    96 axiomatization where
    97   e_ind:
    98     " [|  !!ev. P(e_var(ev));
    99          !!c. P(e_const(c));
   100          !!ev e. P(e) ==> P(fn ev => e);
   101          !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
   102          !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2)
   103      |] ==>
   104    P(e)
   105    "
   106 
   107 (* Types - same scheme as for expressions *)
   108 
   109 (* All constructors are injective *)
   110 
   111 axiomatization where
   112   t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2" and
   113   t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
   114 
   115 (* All constructors are distinct, not needed so far ... *)
   116 
   117 (* Strong elimination, induction on types *)
   118 
   119 axiomatization where
   120  t_ind:
   121     "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
   122     ==> P(t)"
   123 
   124 
   125 (* Values - same scheme again *)
   126 
   127 (* All constructors are injective *)
   128 
   129 axiomatization where
   130   v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2" and
   131   v_clos_inj:
   132     " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
   133      ev1 = ev2 & e1 = e2 & ve1 = ve2"
   134 
   135 (* All constructors are distinct *)
   136 
   137 axiomatization where
   138   v_disj_const_clos: "~v_const(c) = v_clos(cl)"
   139 
   140 (* No induction on values: they are a codatatype! ... *)
   141 
   142 
   143 (*
   144   Value environments bind variables to values. Only the following trivial
   145   properties are needed.
   146 *)
   147 
   148 axiomatization where
   149   ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" and
   150 
   151   ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v" and
   152   ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
   153 
   154 
   155 (* Type Environments bind variables to types. The following trivial
   156 properties are needed.  *)
   157 
   158 axiomatization where
   159   te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" and
   160 
   161   te_app_owr1: "te_app (te + {ev |=> t}) ev=t" and
   162   te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
   163 
   164 
   165 (* The dynamic semantics is defined inductively by a set of inference
   166 rules.  These inference rules allows one to draw conclusions of the form ve
   167 |- e ---> v, read the expression e evaluates to the value v in the value
   168 environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
   169 as the least fixpoint of the functor eval_fun below.  From this definition
   170 introduction rules and a strong elimination (induction) rule can be
   171 derived.
   172 *)
   173 
   174 definition eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
   175   where "eval_fun(s) ==
   176      { pp.
   177        (? ve c. pp=((ve,e_const(c)),v_const(c))) |
   178        (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
   179        (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
   180        ( ? ve e x f cl.
   181            pp=((ve,fix f(x) = e),v_clos(cl)) &
   182            cl=<|x, e, ve+{f |-> v_clos(cl)} |>
   183        ) |
   184        ( ? ve e1 e2 c1 c2.
   185            pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) &
   186            ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
   187        ) |
   188        ( ? ve vem e1 e2 em xm v v2.
   189            pp=((ve,e1 @@ e2),v) &
   190            ((ve,e1),v_clos(<|xm,em,vem|>)):s &
   191            ((ve,e2),v2):s &
   192            ((vem+{xm |-> v2},em),v):s
   193        )
   194      }"
   195 
   196 definition eval_rel :: "((ValEnv * Ex) * Val) set"
   197   where "eval_rel == lfp(eval_fun)"
   198 
   199 definition eval :: "[ValEnv, Ex, Val] => bool"  ("_ |- _ ---> _" [36,0,36] 50)
   200   where "ve |- e ---> v == ((ve,e),v) \<in> eval_rel"
   201 
   202 (* The static semantics is defined in the same way as the dynamic
   203 semantics.  The relation te |- e ===> t express the expression e has the
   204 type t in the type environment te.
   205 *)
   206 
   207 definition elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
   208   where "elab_fun(s) ==
   209     { pp.
   210       (? te c t. pp=((te,e_const(c)),t) & c isof t) |
   211       (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
   212       (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
   213       (? te f x e t1 t2.
   214          pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
   215       ) |
   216       (? te e1 e2 t1 t2.
   217          pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
   218       )
   219     }"
   220 
   221 definition elab_rel :: "((TyEnv * Ex) * Ty) set"
   222   where "elab_rel == lfp(elab_fun)"
   223 
   224 definition elab :: "[TyEnv, Ex, Ty] => bool"  ("_ |- _ ===> _" [36,0,36] 50)
   225   where "te |- e ===> t == ((te,e),t):elab_rel"
   226 
   227 
   228 (* The original correspondence relation *)
   229 
   230 definition isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
   231   where "ve isofenv te ==
   232     ve_dom(ve) = te_dom(te) &
   233      (! x.
   234          x:ve_dom(ve) -->
   235          (? c. ve_app ve x = v_const(c) & c isof te_app te x))"
   236 
   237 axiomatization where
   238   isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
   239 
   240 
   241 (* The extented correspondence relation *)
   242 
   243 definition hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
   244   where "hasty_fun(r) ==
   245     { p.
   246        ( ? c t. p = (v_const(c),t) & c isof t) |
   247        ( ? ev e ve t te.
   248            p = (v_clos(<|ev,e,ve|>),t) &
   249            te |- fn ev => e ===> t &
   250            ve_dom(ve) = te_dom(te) &
   251            (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
   252        )
   253     }"
   254 
   255 definition hasty_rel :: "(Val * Ty) set"
   256   where "hasty_rel == gfp(hasty_fun)"
   257 
   258 definition hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
   259   where "v hasty t == (v,t) : hasty_rel"
   260 
   261 definition hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
   262   where "ve hastyenv te ==
   263     ve_dom(ve) = te_dom(te) &
   264       (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
   265 
   266 
   267 (* ############################################################ *)
   268 (* Inference systems                                            *)
   269 (* ############################################################ *)
   270 
   271 ML \<open>
   272 fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
   273 \<close>
   274 
   275 lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
   276   by simp
   277 
   278 lemma infsys_p2: "P (fst (a,b)) (snd (a,b)) ==> P a b"
   279   by simp
   280 
   281 lemma infsys_pp1: "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"
   282   by simp
   283 
   284 lemma infsys_pp2: "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"
   285   by simp
   286 
   287 
   288 (* ############################################################ *)
   289 (* Fixpoints                                                    *)
   290 (* ############################################################ *)
   291 
   292 (* Least fixpoints *)
   293 
   294 lemma lfp_intro2: "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"
   295 apply (rule subsetD)
   296 apply (rule lfp_lemma2)
   297 apply assumption+
   298 done
   299 
   300 lemma lfp_elim2:
   301   assumes lfp: "x:lfp(f)"
   302     and mono: "mono(f)"
   303     and r: "!!y. y:f(lfp(f)) ==> P(y)"
   304   shows "P(x)"
   305 apply (rule r)
   306 apply (rule subsetD)
   307 apply (rule lfp_lemma3)
   308 apply (rule mono)
   309 apply (rule lfp)
   310 done
   311 
   312 lemma lfp_ind2:
   313   assumes lfp: "x:lfp(f)"
   314     and mono: "mono(f)"
   315     and r: "!!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y)"
   316   shows "P(x)"
   317 apply (rule lfp_induct_set [OF lfp mono])
   318 apply (erule r)
   319 done
   320 
   321 (* Greatest fixpoints *)
   322 
   323 (* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
   324 
   325 lemma gfp_coind2:
   326   assumes cih: "x:f({x} Un gfp(f))"
   327     and monoh: "mono(f)"
   328   shows "x:gfp(f)"
   329 apply (rule cih [THEN [2] gfp_upperbound [THEN subsetD]])
   330 apply (rule monoh [THEN monoD])
   331 apply (rule UnE [THEN subsetI])
   332 apply assumption
   333 apply (blast intro!: cih)
   334 apply (rule monoh [THEN monoD [THEN subsetD]])
   335 apply (rule Un_upper2)
   336 apply (erule monoh [THEN gfp_lemma2, THEN subsetD])
   337 done
   338 
   339 lemma gfp_elim2:
   340   assumes gfph: "x:gfp(f)"
   341     and monoh: "mono(f)"
   342     and caseh: "!!y. y:f(gfp(f)) ==> P(y)"
   343   shows "P(x)"
   344 apply (rule caseh)
   345 apply (rule subsetD)
   346 apply (rule gfp_lemma2)
   347 apply (rule monoh)
   348 apply (rule gfph)
   349 done
   350 
   351 (* ############################################################ *)
   352 (* Expressions                                                  *)
   353 (* ############################################################ *)
   354 
   355 lemmas e_injs = e_const_inj e_var_inj e_fn_inj e_fix_inj e_app_inj
   356 
   357 lemmas e_disjs =
   358   e_disj_const_var
   359   e_disj_const_fn
   360   e_disj_const_fix
   361   e_disj_const_app
   362   e_disj_var_fn
   363   e_disj_var_fix
   364   e_disj_var_app
   365   e_disj_fn_fix
   366   e_disj_fn_app
   367   e_disj_fix_app
   368 
   369 lemmas e_disj_si = e_disjs  e_disjs [symmetric]
   370 
   371 lemmas e_disj_se = e_disj_si [THEN notE]
   372 
   373 (* ############################################################ *)
   374 (* Values                                                      *)
   375 (* ############################################################ *)
   376 
   377 lemmas v_disjs = v_disj_const_clos
   378 lemmas v_disj_si = v_disjs  v_disjs [symmetric]
   379 lemmas v_disj_se = v_disj_si [THEN notE]
   380 
   381 lemmas v_injs = v_const_inj v_clos_inj
   382 
   383 (* ############################################################ *)
   384 (* Evaluations                                                  *)
   385 (* ############################################################ *)
   386 
   387 (* Monotonicity of eval_fun *)
   388 
   389 lemma eval_fun_mono: "mono(eval_fun)"
   390 unfolding mono_def eval_fun_def
   391 apply (tactic "infsys_mono_tac @{context}")
   392 done
   393 
   394 (* Introduction rules *)
   395 
   396 lemma eval_const: "ve |- e_const(c) ---> v_const(c)"
   397 unfolding eval_def eval_rel_def
   398 apply (rule lfp_intro2)
   399 apply (rule eval_fun_mono)
   400 apply (unfold eval_fun_def)
   401         (*Naughty!  But the quantifiers are nested VERY deeply...*)
   402 apply (blast intro!: exI)
   403 done
   404 
   405 lemma eval_var2:
   406   "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev"
   407 apply (unfold eval_def eval_rel_def)
   408 apply (rule lfp_intro2)
   409 apply (rule eval_fun_mono)
   410 apply (unfold eval_fun_def)
   411 apply (blast intro!: exI)
   412 done
   413 
   414 lemma eval_fn:
   415   "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"
   416 apply (unfold eval_def eval_rel_def)
   417 apply (rule lfp_intro2)
   418 apply (rule eval_fun_mono)
   419 apply (unfold eval_fun_def)
   420 apply (blast intro!: exI)
   421 done
   422 
   423 lemma eval_fix:
   424   " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
   425     ve |- fix ev2(ev1) = e ---> v_clos(cl)"
   426 apply (unfold eval_def eval_rel_def)
   427 apply (rule lfp_intro2)
   428 apply (rule eval_fun_mono)
   429 apply (unfold eval_fun_def)
   430 apply (blast intro!: exI)
   431 done
   432 
   433 lemma eval_app1:
   434   " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==>
   435     ve |- e1 @@ e2 ---> v_const(c_app c1 c2)"
   436 apply (unfold eval_def eval_rel_def)
   437 apply (rule lfp_intro2)
   438 apply (rule eval_fun_mono)
   439 apply (unfold eval_fun_def)
   440 apply (blast intro!: exI)
   441 done
   442 
   443 lemma eval_app2:
   444   " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>);
   445         ve |- e2 ---> v2;
   446         vem + {xm |-> v2} |- em ---> v
   447     |] ==>
   448     ve |- e1 @@ e2 ---> v"
   449 apply (unfold eval_def eval_rel_def)
   450 apply (rule lfp_intro2)
   451 apply (rule eval_fun_mono)
   452 apply (unfold eval_fun_def)
   453 apply (blast intro!: disjI2)
   454 done
   455 
   456 (* Strong elimination, induction on evaluations *)
   457 
   458 lemma eval_ind0:
   459   " [| ve |- e ---> v;
   460        !!ve c. P(((ve,e_const(c)),v_const(c)));
   461        !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev));
   462        !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>)));
   463        !!ev1 ev2 ve cl e.
   464          cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
   465          P(((ve,fix ev2(ev1) = e),v_clos(cl)));
   466        !!ve c1 c2 e1 e2.
   467          [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==>
   468          P(((ve,e1 @@ e2),v_const(c_app c1 c2)));
   469        !!ve vem xm e1 e2 em v v2.
   470          [|  P(((ve,e1),v_clos(<|xm,em,vem|>)));
   471              P(((ve,e2),v2));
   472              P(((vem + {xm |-> v2},em),v))
   473          |] ==>
   474          P(((ve,e1 @@ e2),v))
   475     |] ==>
   476     P(((ve,e),v))"
   477 unfolding eval_def eval_rel_def
   478 apply (erule lfp_ind2)
   479 apply (rule eval_fun_mono)
   480 apply (unfold eval_fun_def)
   481 apply (drule CollectD)
   482 apply safe
   483 apply auto
   484 done
   485 
   486 lemma eval_ind:
   487   " [| ve |- e ---> v;
   488        !!ve c. P ve (e_const c) (v_const c);
   489        !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev);
   490        !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>);
   491        !!ev1 ev2 ve cl e.
   492          cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
   493          P ve (fix ev2(ev1) = e) (v_clos cl);
   494        !!ve c1 c2 e1 e2.
   495          [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==>
   496          P ve (e1 @@ e2) (v_const(c_app c1 c2));
   497        !!ve vem evm e1 e2 em v v2.
   498          [|  P ve e1 (v_clos <|evm,em,vem|>);
   499              P ve e2 v2;
   500              P (vem + {evm |-> v2}) em v
   501          |] ==> P ve (e1 @@ e2) v
   502     |] ==> P ve e v"
   503 apply (rule_tac P = "P" in infsys_pp2)
   504 apply (rule eval_ind0)
   505 apply (rule infsys_pp1)
   506 apply auto
   507 done
   508 
   509 (* ############################################################ *)
   510 (* Elaborations                                                 *)
   511 (* ############################################################ *)
   512 
   513 lemma elab_fun_mono: "mono(elab_fun)"
   514 unfolding mono_def elab_fun_def
   515 apply (tactic "infsys_mono_tac @{context}")
   516 done
   517 
   518 (* Introduction rules *)
   519 
   520 lemma elab_const:
   521   "c isof ty ==> te |- e_const(c) ===> ty"
   522 apply (unfold elab_def elab_rel_def)
   523 apply (rule lfp_intro2)
   524 apply (rule elab_fun_mono)
   525 apply (unfold elab_fun_def)
   526 apply (blast intro!: exI)
   527 done
   528 
   529 lemma elab_var:
   530   "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x"
   531 apply (unfold elab_def elab_rel_def)
   532 apply (rule lfp_intro2)
   533 apply (rule elab_fun_mono)
   534 apply (unfold elab_fun_def)
   535 apply (blast intro!: exI)
   536 done
   537 
   538 lemma elab_fn:
   539   "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"
   540 apply (unfold elab_def elab_rel_def)
   541 apply (rule lfp_intro2)
   542 apply (rule elab_fun_mono)
   543 apply (unfold elab_fun_def)
   544 apply (blast intro!: exI)
   545 done
   546 
   547 lemma elab_fix:
   548   "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==>
   549          te |- fix f(x) = e ===> ty1->ty2"
   550 apply (unfold elab_def elab_rel_def)
   551 apply (rule lfp_intro2)
   552 apply (rule elab_fun_mono)
   553 apply (unfold elab_fun_def)
   554 apply (blast intro!: exI)
   555 done
   556 
   557 lemma elab_app:
   558   "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==>
   559          te |- e1 @@ e2 ===> ty2"
   560 apply (unfold elab_def elab_rel_def)
   561 apply (rule lfp_intro2)
   562 apply (rule elab_fun_mono)
   563 apply (unfold elab_fun_def)
   564 apply (blast intro!: disjI2)
   565 done
   566 
   567 (* Strong elimination, induction on elaborations *)
   568 
   569 lemma elab_ind0:
   570   assumes 1: "te |- e ===> t"
   571     and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
   572     and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
   573     and 4: "!!te x e t1 t2.
   574        [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==>
   575        P(((te,fn x => e),t1->t2))"
   576     and 5: "!!te f x e t1 t2.
   577        [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
   578           P(((te + {f |=> t1->t2} + {x |=> t1},e),t2))
   579        |] ==>
   580        P(((te,fix f(x) = e),t1->t2))"
   581     and 6: "!!te e1 e2 t1 t2.
   582        [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2));
   583           te |- e2 ===> t1; P(((te,e2),t1))
   584        |] ==>
   585        P(((te,e1 @@ e2),t2))"
   586   shows "P(((te,e),t))"
   587 apply (rule lfp_ind2 [OF 1 [unfolded elab_def elab_rel_def]])
   588 apply (rule elab_fun_mono)
   589 apply (unfold elab_fun_def)
   590 apply (drule CollectD)
   591 apply safe
   592 apply (erule 2)
   593 apply (erule 3)
   594 apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
   595 apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
   596 apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
   597 done
   598 
   599 lemma elab_ind:
   600   " [| te |- e ===> t;
   601         !!te c t. c isof t ==> P te (e_const c) t;
   602        !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
   603        !!te x e t1 t2.
   604          [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==>
   605          P te (fn x => e) (t1->t2);
   606        !!te f x e t1 t2.
   607          [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
   608             P (te + {f |=> t1->t2} + {x |=> t1}) e t2
   609          |] ==>
   610          P te (fix f(x) = e) (t1->t2);
   611        !!te e1 e2 t1 t2.
   612          [| te |- e1 ===> t1->t2; P te e1 (t1->t2);
   613             te |- e2 ===> t1; P te e2 t1
   614          |] ==>
   615          P te (e1 @@ e2) t2
   616     |] ==>
   617     P te e t"
   618 apply (rule_tac P = "P" in infsys_pp2)
   619 apply (erule elab_ind0)
   620 apply (rule_tac [!] infsys_pp1)
   621 apply auto
   622 done
   623 
   624 (* Weak elimination, case analysis on elaborations *)
   625 
   626 lemma elab_elim0:
   627   assumes 1: "te |- e ===> t"
   628     and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
   629     and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
   630     and 4: "!!te x e t1 t2.
   631          te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2))"
   632     and 5: "!!te f x e t1 t2.
   633          te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
   634          P(((te,fix f(x) = e),t1->t2))"
   635     and 6: "!!te e1 e2 t1 t2.
   636          [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
   637          P(((te,e1 @@ e2),t2))"
   638   shows "P(((te,e),t))"
   639 apply (rule lfp_elim2 [OF 1 [unfolded elab_def elab_rel_def]])
   640 apply (rule elab_fun_mono)
   641 apply (unfold elab_fun_def)
   642 apply (drule CollectD)
   643 apply safe
   644 apply (erule 2)
   645 apply (erule 3)
   646 apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
   647 apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
   648 apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
   649 done
   650 
   651 lemma elab_elim:
   652   " [| te |- e ===> t;
   653         !!te c t. c isof t ==> P te (e_const c) t;
   654        !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
   655        !!te x e t1 t2.
   656          te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2);
   657        !!te f x e t1 t2.
   658          te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
   659          P te (fix f(x) = e) (t1->t2);
   660        !!te e1 e2 t1 t2.
   661          [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
   662          P te (e1 @@ e2) t2
   663     |] ==>
   664     P te e t"
   665 apply (rule_tac P = "P" in infsys_pp2)
   666 apply (rule elab_elim0)
   667 apply auto
   668 done
   669 
   670 (* Elimination rules for each expression *)
   671 
   672 lemma elab_const_elim_lem:
   673     "te |- e ===> t ==> (e = e_const(c) --> c isof t)"
   674 apply (erule elab_elim)
   675 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
   676 done
   677 
   678 lemma elab_const_elim: "te |- e_const(c) ===> t ==> c isof t"
   679 apply (drule elab_const_elim_lem)
   680 apply blast
   681 done
   682 
   683 lemma elab_var_elim_lem:
   684   "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))"
   685 apply (erule elab_elim)
   686 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
   687 done
   688 
   689 lemma elab_var_elim: "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"
   690 apply (drule elab_var_elim_lem)
   691 apply blast
   692 done
   693 
   694 lemma elab_fn_elim_lem:
   695   " te |- e ===> t ==>
   696     ( e = fn x1 => e1 -->
   697       (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2)
   698     )"
   699 apply (erule elab_elim)
   700 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
   701 done
   702 
   703 lemma elab_fn_elim: " te |- fn x1 => e1 ===> t ==>
   704     (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"
   705 apply (drule elab_fn_elim_lem)
   706 apply blast
   707 done
   708 
   709 lemma elab_fix_elim_lem:
   710   " te |- e ===> t ==>
   711     (e = fix f(x) = e1 -->
   712     (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"
   713 apply (erule elab_elim)
   714 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
   715 done
   716 
   717 lemma elab_fix_elim: " te |- fix ev1(ev2) = e1 ===> t ==>
   718     (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"
   719 apply (drule elab_fix_elim_lem)
   720 apply blast
   721 done
   722 
   723 lemma elab_app_elim_lem:
   724   " te |- e ===> t2 ==>
   725     (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"
   726 apply (erule elab_elim)
   727 apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
   728 done
   729 
   730 lemma elab_app_elim: "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"
   731 apply (drule elab_app_elim_lem)
   732 apply blast
   733 done
   734 
   735 (* ############################################################ *)
   736 (* The extended correspondence relation                       *)
   737 (* ############################################################ *)
   738 
   739 (* Monotonicity of hasty_fun *)
   740 
   741 lemma mono_hasty_fun: "mono(hasty_fun)"
   742 unfolding mono_def hasty_fun_def
   743 apply (tactic "infsys_mono_tac @{context}")
   744 apply blast
   745 done
   746 
   747 (*
   748   Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
   749   enjoys two strong indtroduction (co-induction) rules and an elimination rule.
   750 *)
   751 
   752 (* First strong indtroduction (co-induction) rule for hasty_rel *)
   753 
   754 lemma hasty_rel_const_coind: "c isof t ==> (v_const(c),t) : hasty_rel"
   755 apply (unfold hasty_rel_def)
   756 apply (rule gfp_coind2)
   757 apply (unfold hasty_fun_def)
   758 apply (rule CollectI)
   759 apply (rule disjI1)
   760 apply blast
   761 apply (rule mono_hasty_fun)
   762 done
   763 
   764 (* Second strong introduction (co-induction) rule for hasty_rel *)
   765 
   766 lemma hasty_rel_clos_coind:
   767   " [|  te |- fn ev => e ===> t;
   768         ve_dom(ve) = te_dom(te);
   769         ! ev1.
   770           ev1:ve_dom(ve) -->
   771           (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel
   772     |] ==>
   773     (v_clos(<|ev,e,ve|>),t) : hasty_rel"
   774 apply (unfold hasty_rel_def)
   775 apply (rule gfp_coind2)
   776 apply (unfold hasty_fun_def)
   777 apply (rule CollectI)
   778 apply (rule disjI2)
   779 apply blast
   780 apply (rule mono_hasty_fun)
   781 done
   782 
   783 (* Elimination rule for hasty_rel *)
   784 
   785 lemma hasty_rel_elim0:
   786   " [| !! c t. c isof t ==> P((v_const(c),t));
   787        !! te ev e t ve.
   788          [| te |- fn ev => e ===> t;
   789             ve_dom(ve) = te_dom(te);
   790             !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
   791          |] ==> P((v_clos(<|ev,e,ve|>),t));
   792        (v,t) : hasty_rel
   793     |] ==> P(v,t)"
   794 unfolding hasty_rel_def
   795 apply (erule gfp_elim2)
   796 apply (rule mono_hasty_fun)
   797 apply (unfold hasty_fun_def)
   798 apply (drule CollectD)
   799 apply (fold hasty_fun_def)
   800 apply auto
   801 done
   802 
   803 lemma hasty_rel_elim:
   804   " [| (v,t) : hasty_rel;
   805        !! c t. c isof t ==> P (v_const c) t;
   806        !! te ev e t ve.
   807          [| te |- fn ev => e ===> t;
   808             ve_dom(ve) = te_dom(te);
   809             !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
   810          |] ==> P (v_clos <|ev,e,ve|>) t
   811     |] ==> P v t"
   812 apply (rule_tac P = "P" in infsys_p2)
   813 apply (rule hasty_rel_elim0)
   814 apply auto
   815 done
   816 
   817 (* Introduction rules for hasty *)
   818 
   819 lemma hasty_const: "c isof t ==> v_const(c) hasty t"
   820 apply (unfold hasty_def)
   821 apply (erule hasty_rel_const_coind)
   822 done
   823 
   824 lemma hasty_clos:
   825  "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"
   826 apply (unfold hasty_def hasty_env_def)
   827 apply (rule hasty_rel_clos_coind)
   828 apply (blast del: equalityI)+
   829 done
   830 
   831 (* Elimination on constants for hasty *)
   832 
   833 lemma hasty_elim_const_lem:
   834   "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"
   835 apply (unfold hasty_def)
   836 apply (rule hasty_rel_elim)
   837 apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
   838 done
   839 
   840 lemma hasty_elim_const: "v_const(c) hasty t ==> c isof t"
   841 apply (drule hasty_elim_const_lem)
   842 apply blast
   843 done
   844 
   845 (* Elimination on closures for hasty *)
   846 
   847 lemma hasty_elim_clos_lem:
   848   " v hasty t ==>
   849     ! x e ve.
   850       v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)"
   851 apply (unfold hasty_env_def hasty_def)
   852 apply (rule hasty_rel_elim)
   853 apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
   854 done
   855 
   856 lemma hasty_elim_clos: "v_clos(<|ev,e,ve|>) hasty t ==>
   857         ? te. te |- fn ev => e ===> t & ve hastyenv te "
   858 apply (drule hasty_elim_clos_lem)
   859 apply blast
   860 done
   861 
   862 (* ############################################################ *)
   863 (* The pointwise extension of hasty to environments             *)
   864 (* ############################################################ *)
   865 
   866 lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==>
   867          ve + {ev |-> v} hastyenv te + {ev |=> t}"
   868 apply (unfold hasty_env_def)
   869 apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
   870 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
   871 apply (case_tac "ev=x")
   872 apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
   873 apply (simp add: ve_app_owr2 te_app_owr2)
   874 done
   875 
   876 (* ############################################################ *)
   877 (* The Consistency theorem                                      *)
   878 (* ############################################################ *)
   879 
   880 lemma consistency_const: "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"
   881 apply (drule elab_const_elim)
   882 apply (erule hasty_const)
   883 done
   884 
   885 lemma consistency_var:
   886   "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==>
   887         ve_app ve ev hasty t"
   888 apply (unfold hasty_env_def)
   889 apply (drule elab_var_elim)
   890 apply blast
   891 done
   892 
   893 lemma consistency_fn: "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==>
   894         v_clos(<| ev, e, ve |>) hasty t"
   895 apply (rule hasty_clos)
   896 apply blast
   897 done
   898 
   899 lemma consistency_fix:
   900   "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>;
   901        ve hastyenv te ;
   902        te |- fix ev2  ev1  = e ===> t
   903     |] ==>
   904     v_clos(cl) hasty t"
   905 apply (unfold hasty_env_def hasty_def)
   906 apply (drule elab_fix_elim)
   907 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
   908 (*Do a single unfolding of cl*)
   909 apply (frule ssubst) prefer 2 apply assumption
   910 apply (rule hasty_rel_clos_coind)
   911 apply (erule elab_fn)
   912 apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
   913 
   914 apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
   915 apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
   916 apply (case_tac "ev2=ev1a")
   917 apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
   918 apply blast
   919 apply (simp add: ve_app_owr2 te_app_owr2)
   920 done
   921 
   922 lemma consistency_app1: "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;
   923        ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t;
   924        ve hastyenv te ; te |- e1 @@ e2 ===> t
   925     |] ==>
   926     v_const(c_app c1 c2) hasty t"
   927 apply (drule elab_app_elim)
   928 apply safe
   929 apply (rule hasty_const)
   930 apply (rule isof_app)
   931 apply (rule hasty_elim_const)
   932 apply blast
   933 apply (rule hasty_elim_const)
   934 apply blast
   935 done
   936 
   937 lemma consistency_app2: "[| ! t te.
   938          ve hastyenv te  -->
   939          te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t;
   940        ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t;
   941        ! t te.
   942          vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t;
   943        ve hastyenv te ;
   944        te |- e1 @@ e2 ===> t
   945     |] ==>
   946     v hasty t"
   947 apply (drule elab_app_elim)
   948 apply safe
   949 apply (erule allE, erule allE, erule impE)
   950 apply assumption
   951 apply (erule impE)
   952 apply assumption
   953 apply (erule allE, erule allE, erule impE)
   954 apply assumption
   955 apply (erule impE)
   956 apply assumption
   957 apply (drule hasty_elim_clos)
   958 apply safe
   959 apply (drule elab_fn_elim)
   960 apply (blast intro: hasty_env1 dest!: t_fun_inj)
   961 done
   962 
   963 lemma consistency: "ve |- e ---> v ==>
   964    (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"
   965 
   966 (* Proof by induction on the structure of evaluations *)
   967 
   968 apply (erule eval_ind)
   969 apply safe
   970 apply (blast intro: consistency_const consistency_var consistency_fn consistency_fix consistency_app1 consistency_app2)+
   971 done
   972 
   973 (* ############################################################ *)
   974 (* The Basic Consistency theorem                                *)
   975 (* ############################################################ *)
   976 
   977 lemma basic_consistency_lem:
   978   "ve isofenv te ==> ve hastyenv te"
   979 apply (unfold isof_env_def hasty_env_def)
   980 apply safe
   981 apply (erule allE)
   982 apply (erule impE)
   983 apply assumption
   984 apply (erule exE)
   985 apply (erule conjE)
   986 apply (drule hasty_const)
   987 apply (simp (no_asm_simp))
   988 done
   989 
   990 lemma basic_consistency:
   991   "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"
   992 apply (rule hasty_elim_const)
   993 apply (drule consistency)
   994 apply (blast intro!: basic_consistency_lem)
   995 done
   996 
   997 end