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