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