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