# HG changeset patch
# User traytel
# Date 1452587288 -3600
# Node ID c92d82c3f41bf7c632cdff32b9f427445ddda6b1
# Parent  fcf3bb1b54e1cbccc8583f181fa0377f72588117
removed outdated example

diff -r fcf3bb1b54e1 -r c92d82c3f41b src/HOL/Datatype_Examples/Milner_Tofte.thy
--- a/src/HOL/Datatype_Examples/Milner_Tofte.thy	Tue Jan 12 11:03:40 2016 +1100
+++ b/src/HOL/Datatype_Examples/Milner_Tofte.thy	Tue Jan 12 09:28:08 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Dmitriy Traytel, ETH Zürich
     Copyright   2015
 
-Modernized version of HOL/ex/MT.thy by Jacob Frost
+Modernized version of an old development by Jacob Frost
 
 Based upon the article
     Robin Milner and Mads Tofte,
diff -r fcf3bb1b54e1 -r c92d82c3f41b src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jan 12 11:03:40 2016 +1100
+++ b/src/HOL/ROOT	Tue Jan 12 09:28:08 2016 +0100
@@ -574,7 +574,6 @@
     MergeSort
     Lagrange
     Groebner_Examples
-    MT
     Unification
     Primrec
     Tarski
diff -r fcf3bb1b54e1 -r c92d82c3f41b src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Tue Jan 12 11:03:40 2016 +1100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1004 +0,0 @@
-(*  Title:      HOL/ex/MT.thy
-    Author:     Jacob Frost, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Based upon the article
-    Robin Milner and Mads Tofte,
-    Co-induction in Relational Semantics,
-    Theoretical Computer Science 87 (1991), pages 209-220.
-
-Written up as
-    Jacob Frost, A Case Study of Co_induction in Isabelle/HOL
-    Report 308, Computer Lab, University of Cambridge (1993).
-*)
-
-section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close>
-
-theory MT
-imports Main
-begin
-
-typedecl Const
-
-typedecl ExVar
-typedecl Ex
-
-typedecl TyConst
-typedecl Ty
-
-typedecl Clos
-typedecl Val
-
-typedecl ValEnv
-typedecl TyEnv
-
-consts
-  c_app :: "[Const, Const] => Const"
-
-  e_const :: "Const => Ex"
-  e_var :: "ExVar => Ex"
-  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
-  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
-  e_app :: "[Ex, Ex] => Ex" ("_ @@ _" [51,51] 1000)
-  e_const_fst :: "Ex => Const"
-
-  t_const :: "TyConst => Ty"
-  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
-
-  v_const :: "Const => Val"
-  v_clos :: "Clos => Val"
-
-  ve_emp :: ValEnv
-  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
-  ve_dom :: "ValEnv => ExVar set"
-  ve_app :: "[ValEnv, ExVar] => Val"
-
-  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
-
-  te_emp :: TyEnv
-  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
-  te_app :: "[TyEnv, ExVar] => Ty"
-  te_dom :: "TyEnv => ExVar set"
-
-  eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
-  eval_rel :: "((ValEnv * Ex) * Val) set"
-  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
-
-  elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
-  elab_rel :: "((TyEnv * Ex) * Ty) set"
-  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
-
-  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
-  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
-
-  hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
-  hasty_rel :: "(Val * Ty) set"
-  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
-  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
-
-(*
-  Expression constructors must be injective, distinct and it must be possible
-  to do induction over expressions.
-*)
-
-(* All the constructors are injective *)
-axiomatization where
-  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2" and
-  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" and
-  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" and
-  e_fix_inj:
-    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
-     ev11 = ev21 & ev12 = ev22 & e1 = e2" and
-  e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"
-
-(* All constructors are distinct *)
-
-axiomatization where
-  e_disj_const_var: "~e_const(c) = e_var(ev)" and
-  e_disj_const_fn: "~e_const(c) = fn ev => e" and
-  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e" and
-  e_disj_const_app: "~e_const(c) = e1 @@ e2" and
-  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e" and
-  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e" and
-  e_disj_var_app: "~e_var(ev) = e1 @@ e2" and
-  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2" and
-  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22" and
-  e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"
-
-(* Strong elimination, induction on expressions  *)
-
-axiomatization where
-  e_ind:
-    " [|  !!ev. P(e_var(ev));
-         !!c. P(e_const(c));
-         !!ev e. P(e) ==> P(fn ev => e);
-         !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
-         !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @@ e2)
-     |] ==>
-   P(e)
-   "
-
-(* Types - same scheme as for expressions *)
-
-(* All constructors are injective *)
-
-axiomatization where
-  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2" and
-  t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"
-
-(* All constructors are distinct, not needed so far ... *)
-
-(* Strong elimination, induction on types *)
-
-axiomatization where
- t_ind:
-    "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
-    ==> P(t)"
-
-
-(* Values - same scheme again *)
-
-(* All constructors are injective *)
-
-axiomatization where
-  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2" and
-  v_clos_inj:
-    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
-     ev1 = ev2 & e1 = e2 & ve1 = ve2"
-
-(* All constructors are distinct *)
-
-axiomatization where
-  v_disj_const_clos: "~v_const(c) = v_clos(cl)"
-
-(* No induction on values: they are a codatatype! ... *)
-
-
-(*
-  Value environments bind variables to values. Only the following trivial
-  properties are needed.
-*)
-
-axiomatization where
-  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" and
-
-  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v" and
-  ve_app_owr2: "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2"
-
-
-(* Type Environments bind variables to types. The following trivial
-properties are needed.  *)
-
-axiomatization where
-  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" and
-
-  te_app_owr1: "te_app (te + {ev |=> t}) ev=t" and
-  te_app_owr2: "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2"
-
-
-(* The dynamic semantics is defined inductively by a set of inference
-rules.  These inference rules allows one to draw conclusions of the form ve
-|- e ---> v, read the expression e evaluates to the value v in the value
-environment ve.  Therefore the relation _ |- _ ---> _ is defined in Isabelle
-as the least fixpoint of the functor eval_fun below.  From this definition
-introduction rules and a strong elimination (induction) rule can be
-derived.
-*)
-
-defs
-  eval_fun_def:
-    " eval_fun(s) ==
-     { pp.
-       (? ve c. pp=((ve,e_const(c)),v_const(c))) |
-       (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
-       (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
-       ( ? ve e x f cl.
-           pp=((ve,fix f(x) = e),v_clos(cl)) &
-           cl=<|x, e, ve+{f |-> v_clos(cl)} |>
-       ) |
-       ( ? ve e1 e2 c1 c2.
-           pp=((ve,e1 @@ e2),v_const(c_app c1 c2)) &
-           ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
-       ) |
-       ( ? ve vem e1 e2 em xm v v2.
-           pp=((ve,e1 @@ e2),v) &
-           ((ve,e1),v_clos(<|xm,em,vem|>)):s &
-           ((ve,e2),v2):s &
-           ((vem+{xm |-> v2},em),v):s
-       )
-     }"
-
-  eval_rel_def: "eval_rel == lfp(eval_fun)"
-  eval_def: "ve |- e ---> v == ((ve,e),v):eval_rel"
-
-(* The static semantics is defined in the same way as the dynamic
-semantics.  The relation te |- e ===> t express the expression e has the
-type t in the type environment te.
-*)
-
-  elab_fun_def:
-  "elab_fun(s) ==
-  { pp.
-    (? te c t. pp=((te,e_const(c)),t) & c isof t) |
-    (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
-    (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
-    (? te f x e t1 t2.
-       pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
-    ) |
-    (? te e1 e2 t1 t2.
-       pp=((te,e1 @@ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
-    )
-  }"
-
-  elab_rel_def: "elab_rel == lfp(elab_fun)"
-  elab_def: "te |- e ===> t == ((te,e),t):elab_rel"
-
-(* The original correspondence relation *)
-
-  isof_env_def:
-    " ve isofenv te ==
-     ve_dom(ve) = te_dom(te) &
-     ( ! x.
-         x:ve_dom(ve) -->
-         (? c. ve_app ve x = v_const(c) & c isof te_app te x)
-     )
-   "
-
-axiomatization where
-  isof_app: "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
-
-defs
-(* The extented correspondence relation *)
-
-  hasty_fun_def:
-    " hasty_fun(r) ==
-     { p.
-       ( ? c t. p = (v_const(c),t) & c isof t) |
-       ( ? ev e ve t te.
-           p = (v_clos(<|ev,e,ve|>),t) &
-           te |- fn ev => e ===> t &
-           ve_dom(ve) = te_dom(te) &
-           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
-       )
-     }
-   "
-
-  hasty_rel_def: "hasty_rel == gfp(hasty_fun)"
-  hasty_def: "v hasty t == (v,t) : hasty_rel"
-  hasty_env_def:
-    " ve hastyenv te ==
-     ve_dom(ve) = te_dom(te) &
-     (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
-
-
-(* ############################################################ *)
-(* Inference systems                                            *)
-(* ############################################################ *)
-
-ML \<open>
-fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
-\<close>
-
-lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
-  by simp
-
-lemma infsys_p2: "P (fst (a,b)) (snd (a,b)) ==> P a b"
-  by simp
-
-lemma infsys_pp1: "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))"
-  by simp
-
-lemma infsys_pp2: "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c"
-  by simp
-
-
-(* ############################################################ *)
-(* Fixpoints                                                    *)
-(* ############################################################ *)
-
-(* Least fixpoints *)
-
-lemma lfp_intro2: "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"
-apply (rule subsetD)
-apply (rule lfp_lemma2)
-apply assumption+
-done
-
-lemma lfp_elim2:
-  assumes lfp: "x:lfp(f)"
-    and mono: "mono(f)"
-    and r: "!!y. y:f(lfp(f)) ==> P(y)"
-  shows "P(x)"
-apply (rule r)
-apply (rule subsetD)
-apply (rule lfp_lemma3)
-apply (rule mono)
-apply (rule lfp)
-done
-
-lemma lfp_ind2:
-  assumes lfp: "x:lfp(f)"
-    and mono: "mono(f)"
-    and r: "!!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y)"
-  shows "P(x)"
-apply (rule lfp_induct_set [OF lfp mono])
-apply (erule r)
-done
-
-(* Greatest fixpoints *)
-
-(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *)
-
-lemma gfp_coind2:
-  assumes cih: "x:f({x} Un gfp(f))"
-    and monoh: "mono(f)"
-  shows "x:gfp(f)"
-apply (rule cih [THEN [2] gfp_upperbound [THEN subsetD]])
-apply (rule monoh [THEN monoD])
-apply (rule UnE [THEN subsetI])
-apply assumption
-apply (blast intro!: cih)
-apply (rule monoh [THEN monoD [THEN subsetD]])
-apply (rule Un_upper2)
-apply (erule monoh [THEN gfp_lemma2, THEN subsetD])
-done
-
-lemma gfp_elim2:
-  assumes gfph: "x:gfp(f)"
-    and monoh: "mono(f)"
-    and caseh: "!!y. y:f(gfp(f)) ==> P(y)"
-  shows "P(x)"
-apply (rule caseh)
-apply (rule subsetD)
-apply (rule gfp_lemma2)
-apply (rule monoh)
-apply (rule gfph)
-done
-
-(* ############################################################ *)
-(* Expressions                                                  *)
-(* ############################################################ *)
-
-lemmas e_injs = e_const_inj e_var_inj e_fn_inj e_fix_inj e_app_inj
-
-lemmas e_disjs =
-  e_disj_const_var
-  e_disj_const_fn
-  e_disj_const_fix
-  e_disj_const_app
-  e_disj_var_fn
-  e_disj_var_fix
-  e_disj_var_app
-  e_disj_fn_fix
-  e_disj_fn_app
-  e_disj_fix_app
-
-lemmas e_disj_si = e_disjs  e_disjs [symmetric]
-
-lemmas e_disj_se = e_disj_si [THEN notE]
-
-(* ############################################################ *)
-(* Values                                                      *)
-(* ############################################################ *)
-
-lemmas v_disjs = v_disj_const_clos
-lemmas v_disj_si = v_disjs  v_disjs [symmetric]
-lemmas v_disj_se = v_disj_si [THEN notE]
-
-lemmas v_injs = v_const_inj v_clos_inj
-
-(* ############################################################ *)
-(* Evaluations                                                  *)
-(* ############################################################ *)
-
-(* Monotonicity of eval_fun *)
-
-lemma eval_fun_mono: "mono(eval_fun)"
-unfolding mono_def eval_fun_def
-apply (tactic "infsys_mono_tac @{context}")
-done
-
-(* Introduction rules *)
-
-lemma eval_const: "ve |- e_const(c) ---> v_const(c)"
-unfolding eval_def eval_rel_def
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-        (*Naughty!  But the quantifiers are nested VERY deeply...*)
-apply (blast intro!: exI)
-done
-
-lemma eval_var2:
-  "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev"
-apply (unfold eval_def eval_rel_def)
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma eval_fn:
-  "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"
-apply (unfold eval_def eval_rel_def)
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma eval_fix:
-  " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
-    ve |- fix ev2(ev1) = e ---> v_clos(cl)"
-apply (unfold eval_def eval_rel_def)
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma eval_app1:
-  " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==>
-    ve |- e1 @@ e2 ---> v_const(c_app c1 c2)"
-apply (unfold eval_def eval_rel_def)
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma eval_app2:
-  " [|  ve |- e1 ---> v_clos(<|xm,em,vem|>);
-        ve |- e2 ---> v2;
-        vem + {xm |-> v2} |- em ---> v
-    |] ==>
-    ve |- e1 @@ e2 ---> v"
-apply (unfold eval_def eval_rel_def)
-apply (rule lfp_intro2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (blast intro!: disjI2)
-done
-
-(* Strong elimination, induction on evaluations *)
-
-lemma eval_ind0:
-  " [| ve |- e ---> v;
-       !!ve c. P(((ve,e_const(c)),v_const(c)));
-       !!ev ve. ev:ve_dom(ve) ==> P(((ve,e_var(ev)),ve_app ve ev));
-       !!ev ve e. P(((ve,fn ev => e),v_clos(<|ev,e,ve|>)));
-       !!ev1 ev2 ve cl e.
-         cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
-         P(((ve,fix ev2(ev1) = e),v_clos(cl)));
-       !!ve c1 c2 e1 e2.
-         [| P(((ve,e1),v_const(c1))); P(((ve,e2),v_const(c2))) |] ==>
-         P(((ve,e1 @@ e2),v_const(c_app c1 c2)));
-       !!ve vem xm e1 e2 em v v2.
-         [|  P(((ve,e1),v_clos(<|xm,em,vem|>)));
-             P(((ve,e2),v2));
-             P(((vem + {xm |-> v2},em),v))
-         |] ==>
-         P(((ve,e1 @@ e2),v))
-    |] ==>
-    P(((ve,e),v))"
-unfolding eval_def eval_rel_def
-apply (erule lfp_ind2)
-apply (rule eval_fun_mono)
-apply (unfold eval_fun_def)
-apply (drule CollectD)
-apply safe
-apply auto
-done
-
-lemma eval_ind:
-  " [| ve |- e ---> v;
-       !!ve c. P ve (e_const c) (v_const c);
-       !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev);
-       !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>);
-       !!ev1 ev2 ve cl e.
-         cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==>
-         P ve (fix ev2(ev1) = e) (v_clos cl);
-       !!ve c1 c2 e1 e2.
-         [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==>
-         P ve (e1 @@ e2) (v_const(c_app c1 c2));
-       !!ve vem evm e1 e2 em v v2.
-         [|  P ve e1 (v_clos <|evm,em,vem|>);
-             P ve e2 v2;
-             P (vem + {evm |-> v2}) em v
-         |] ==> P ve (e1 @@ e2) v
-    |] ==> P ve e v"
-apply (rule_tac P = "P" in infsys_pp2)
-apply (rule eval_ind0)
-apply (rule infsys_pp1)
-apply auto
-done
-
-(* ############################################################ *)
-(* Elaborations                                                 *)
-(* ############################################################ *)
-
-lemma elab_fun_mono: "mono(elab_fun)"
-unfolding mono_def elab_fun_def
-apply (tactic "infsys_mono_tac @{context}")
-done
-
-(* Introduction rules *)
-
-lemma elab_const:
-  "c isof ty ==> te |- e_const(c) ===> ty"
-apply (unfold elab_def elab_rel_def)
-apply (rule lfp_intro2)
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma elab_var:
-  "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x"
-apply (unfold elab_def elab_rel_def)
-apply (rule lfp_intro2)
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma elab_fn:
-  "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"
-apply (unfold elab_def elab_rel_def)
-apply (rule lfp_intro2)
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma elab_fix:
-  "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==>
-         te |- fix f(x) = e ===> ty1->ty2"
-apply (unfold elab_def elab_rel_def)
-apply (rule lfp_intro2)
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (blast intro!: exI)
-done
-
-lemma elab_app:
-  "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==>
-         te |- e1 @@ e2 ===> ty2"
-apply (unfold elab_def elab_rel_def)
-apply (rule lfp_intro2)
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (blast intro!: disjI2)
-done
-
-(* Strong elimination, induction on elaborations *)
-
-lemma elab_ind0:
-  assumes 1: "te |- e ===> t"
-    and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
-    and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
-    and 4: "!!te x e t1 t2.
-       [| te + {x |=> t1} |- e ===> t2; P(((te + {x |=> t1},e),t2)) |] ==>
-       P(((te,fn x => e),t1->t2))"
-    and 5: "!!te f x e t1 t2.
-       [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
-          P(((te + {f |=> t1->t2} + {x |=> t1},e),t2))
-       |] ==>
-       P(((te,fix f(x) = e),t1->t2))"
-    and 6: "!!te e1 e2 t1 t2.
-       [| te |- e1 ===> t1->t2; P(((te,e1),t1->t2));
-          te |- e2 ===> t1; P(((te,e2),t1))
-       |] ==>
-       P(((te,e1 @@ e2),t2))"
-  shows "P(((te,e),t))"
-apply (rule lfp_ind2 [OF 1 [unfolded elab_def elab_rel_def]])
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (drule CollectD)
-apply safe
-apply (erule 2)
-apply (erule 3)
-apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
-apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
-apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
-done
-
-lemma elab_ind:
-  " [| te |- e ===> t;
-        !!te c t. c isof t ==> P te (e_const c) t;
-       !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
-       !!te x e t1 t2.
-         [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==>
-         P te (fn x => e) (t1->t2);
-       !!te f x e t1 t2.
-         [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2;
-            P (te + {f |=> t1->t2} + {x |=> t1}) e t2
-         |] ==>
-         P te (fix f(x) = e) (t1->t2);
-       !!te e1 e2 t1 t2.
-         [| te |- e1 ===> t1->t2; P te e1 (t1->t2);
-            te |- e2 ===> t1; P te e2 t1
-         |] ==>
-         P te (e1 @@ e2) t2
-    |] ==>
-    P te e t"
-apply (rule_tac P = "P" in infsys_pp2)
-apply (erule elab_ind0)
-apply (rule_tac [!] infsys_pp1)
-apply auto
-done
-
-(* Weak elimination, case analysis on elaborations *)
-
-lemma elab_elim0:
-  assumes 1: "te |- e ===> t"
-    and 2: "!!te c t. c isof t ==> P(((te,e_const(c)),t))"
-    and 3: "!!te x. x:te_dom(te) ==> P(((te,e_var(x)),te_app te x))"
-    and 4: "!!te x e t1 t2.
-         te + {x |=> t1} |- e ===> t2 ==> P(((te,fn x => e),t1->t2))"
-    and 5: "!!te f x e t1 t2.
-         te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
-         P(((te,fix f(x) = e),t1->t2))"
-    and 6: "!!te e1 e2 t1 t2.
-         [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
-         P(((te,e1 @@ e2),t2))"
-  shows "P(((te,e),t))"
-apply (rule lfp_elim2 [OF 1 [unfolded elab_def elab_rel_def]])
-apply (rule elab_fun_mono)
-apply (unfold elab_fun_def)
-apply (drule CollectD)
-apply safe
-apply (erule 2)
-apply (erule 3)
-apply (rule 4 [unfolded elab_def elab_rel_def]) apply blast+
-apply (rule 5 [unfolded elab_def elab_rel_def]) apply blast+
-apply (rule 6 [unfolded elab_def elab_rel_def]) apply blast+
-done
-
-lemma elab_elim:
-  " [| te |- e ===> t;
-        !!te c t. c isof t ==> P te (e_const c) t;
-       !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x);
-       !!te x e t1 t2.
-         te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2);
-       !!te f x e t1 t2.
-         te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==>
-         P te (fix f(x) = e) (t1->t2);
-       !!te e1 e2 t1 t2.
-         [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==>
-         P te (e1 @@ e2) t2
-    |] ==>
-    P te e t"
-apply (rule_tac P = "P" in infsys_pp2)
-apply (rule elab_elim0)
-apply auto
-done
-
-(* Elimination rules for each expression *)
-
-lemma elab_const_elim_lem:
-    "te |- e ===> t ==> (e = e_const(c) --> c isof t)"
-apply (erule elab_elim)
-apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
-done
-
-lemma elab_const_elim: "te |- e_const(c) ===> t ==> c isof t"
-apply (drule elab_const_elim_lem)
-apply blast
-done
-
-lemma elab_var_elim_lem:
-  "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))"
-apply (erule elab_elim)
-apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
-done
-
-lemma elab_var_elim: "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"
-apply (drule elab_var_elim_lem)
-apply blast
-done
-
-lemma elab_fn_elim_lem:
-  " te |- e ===> t ==>
-    ( e = fn x1 => e1 -->
-      (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2)
-    )"
-apply (erule elab_elim)
-apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
-done
-
-lemma elab_fn_elim: " te |- fn x1 => e1 ===> t ==>
-    (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"
-apply (drule elab_fn_elim_lem)
-apply blast
-done
-
-lemma elab_fix_elim_lem:
-  " te |- e ===> t ==>
-    (e = fix f(x) = e1 -->
-    (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"
-apply (erule elab_elim)
-apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
-done
-
-lemma elab_fix_elim: " te |- fix ev1(ev2) = e1 ===> t ==>
-    (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"
-apply (drule elab_fix_elim_lem)
-apply blast
-done
-
-lemma elab_app_elim_lem:
-  " te |- e ===> t2 ==>
-    (e = e1 @@ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"
-apply (erule elab_elim)
-apply (fast intro!: e_disj_si elim!: e_disj_se dest!: e_injs)+
-done
-
-lemma elab_app_elim: "te |- e1 @@ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"
-apply (drule elab_app_elim_lem)
-apply blast
-done
-
-(* ############################################################ *)
-(* The extended correspondence relation                       *)
-(* ############################################################ *)
-
-(* Monotonicity of hasty_fun *)
-
-lemma mono_hasty_fun: "mono(hasty_fun)"
-unfolding mono_def hasty_fun_def
-apply (tactic "infsys_mono_tac @{context}")
-apply blast
-done
-
-(*
-  Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it
-  enjoys two strong indtroduction (co-induction) rules and an elimination rule.
-*)
-
-(* First strong indtroduction (co-induction) rule for hasty_rel *)
-
-lemma hasty_rel_const_coind: "c isof t ==> (v_const(c),t) : hasty_rel"
-apply (unfold hasty_rel_def)
-apply (rule gfp_coind2)
-apply (unfold hasty_fun_def)
-apply (rule CollectI)
-apply (rule disjI1)
-apply blast
-apply (rule mono_hasty_fun)
-done
-
-(* Second strong introduction (co-induction) rule for hasty_rel *)
-
-lemma hasty_rel_clos_coind:
-  " [|  te |- fn ev => e ===> t;
-        ve_dom(ve) = te_dom(te);
-        ! ev1.
-          ev1:ve_dom(ve) -->
-          (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel
-    |] ==>
-    (v_clos(<|ev,e,ve|>),t) : hasty_rel"
-apply (unfold hasty_rel_def)
-apply (rule gfp_coind2)
-apply (unfold hasty_fun_def)
-apply (rule CollectI)
-apply (rule disjI2)
-apply blast
-apply (rule mono_hasty_fun)
-done
-
-(* Elimination rule for hasty_rel *)
-
-lemma hasty_rel_elim0:
-  " [| !! c t. c isof t ==> P((v_const(c),t));
-       !! te ev e t ve.
-         [| te |- fn ev => e ===> t;
-            ve_dom(ve) = te_dom(te);
-            !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
-         |] ==> P((v_clos(<|ev,e,ve|>),t));
-       (v,t) : hasty_rel
-    |] ==> P(v,t)"
-unfolding hasty_rel_def
-apply (erule gfp_elim2)
-apply (rule mono_hasty_fun)
-apply (unfold hasty_fun_def)
-apply (drule CollectD)
-apply (fold hasty_fun_def)
-apply auto
-done
-
-lemma hasty_rel_elim:
-  " [| (v,t) : hasty_rel;
-       !! c t. c isof t ==> P (v_const c) t;
-       !! te ev e t ve.
-         [| te |- fn ev => e ===> t;
-            ve_dom(ve) = te_dom(te);
-            !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel
-         |] ==> P (v_clos <|ev,e,ve|>) t
-    |] ==> P v t"
-apply (rule_tac P = "P" in infsys_p2)
-apply (rule hasty_rel_elim0)
-apply auto
-done
-
-(* Introduction rules for hasty *)
-
-lemma hasty_const: "c isof t ==> v_const(c) hasty t"
-apply (unfold hasty_def)
-apply (erule hasty_rel_const_coind)
-done
-
-lemma hasty_clos:
- "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"
-apply (unfold hasty_def hasty_env_def)
-apply (rule hasty_rel_clos_coind)
-apply (blast del: equalityI)+
-done
-
-(* Elimination on constants for hasty *)
-
-lemma hasty_elim_const_lem:
-  "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"
-apply (unfold hasty_def)
-apply (rule hasty_rel_elim)
-apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
-done
-
-lemma hasty_elim_const: "v_const(c) hasty t ==> c isof t"
-apply (drule hasty_elim_const_lem)
-apply blast
-done
-
-(* Elimination on closures for hasty *)
-
-lemma hasty_elim_clos_lem:
-  " v hasty t ==>
-    ! x e ve.
-      v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)"
-apply (unfold hasty_env_def hasty_def)
-apply (rule hasty_rel_elim)
-apply (blast intro!: v_disj_si elim!: v_disj_se dest!: v_injs)+
-done
-
-lemma hasty_elim_clos: "v_clos(<|ev,e,ve|>) hasty t ==>
-        ? te. te |- fn ev => e ===> t & ve hastyenv te "
-apply (drule hasty_elim_clos_lem)
-apply blast
-done
-
-(* ############################################################ *)
-(* The pointwise extension of hasty to environments             *)
-(* ############################################################ *)
-
-lemma hasty_env1: "[| ve hastyenv te; v hasty t |] ==>
-         ve + {ev |-> v} hastyenv te + {ev |=> t}"
-apply (unfold hasty_env_def)
-apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
-apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
-apply (case_tac "ev=x")
-apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
-apply (simp add: ve_app_owr2 te_app_owr2)
-done
-
-(* ############################################################ *)
-(* The Consistency theorem                                      *)
-(* ############################################################ *)
-
-lemma consistency_const: "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"
-apply (drule elab_const_elim)
-apply (erule hasty_const)
-done
-
-lemma consistency_var:
-  "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==>
-        ve_app ve ev hasty t"
-apply (unfold hasty_env_def)
-apply (drule elab_var_elim)
-apply blast
-done
-
-lemma consistency_fn: "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==>
-        v_clos(<| ev, e, ve |>) hasty t"
-apply (rule hasty_clos)
-apply blast
-done
-
-lemma consistency_fix:
-  "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>;
-       ve hastyenv te ;
-       te |- fix ev2  ev1  = e ===> t
-    |] ==>
-    v_clos(cl) hasty t"
-apply (unfold hasty_env_def hasty_def)
-apply (drule elab_fix_elim)
-apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
-(*Do a single unfolding of cl*)
-apply (frule ssubst) prefer 2 apply assumption
-apply (rule hasty_rel_clos_coind)
-apply (erule elab_fn)
-apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
-
-apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
-apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
-apply (case_tac "ev2=ev1a")
-apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
-apply blast
-apply (simp add: ve_app_owr2 te_app_owr2)
-done
-
-lemma consistency_app1: "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;
-       ! t te. ve hastyenv te  --> te |- e2 ===> t --> v_const(c2) hasty t;
-       ve hastyenv te ; te |- e1 @@ e2 ===> t
-    |] ==>
-    v_const(c_app c1 c2) hasty t"
-apply (drule elab_app_elim)
-apply safe
-apply (rule hasty_const)
-apply (rule isof_app)
-apply (rule hasty_elim_const)
-apply blast
-apply (rule hasty_elim_const)
-apply blast
-done
-
-lemma consistency_app2: "[| ! t te.
-         ve hastyenv te  -->
-         te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t;
-       ! t te. ve hastyenv te  --> te |- e2 ===> t --> v2 hasty t;
-       ! t te.
-         vem + { evm |-> v2 } hastyenv te  --> te |- em ===> t --> v hasty t;
-       ve hastyenv te ;
-       te |- e1 @@ e2 ===> t
-    |] ==>
-    v hasty t"
-apply (drule elab_app_elim)
-apply safe
-apply (erule allE, erule allE, erule impE)
-apply assumption
-apply (erule impE)
-apply assumption
-apply (erule allE, erule allE, erule impE)
-apply assumption
-apply (erule impE)
-apply assumption
-apply (drule hasty_elim_clos)
-apply safe
-apply (drule elab_fn_elim)
-apply (blast intro: hasty_env1 dest!: t_fun_inj)
-done
-
-lemma consistency: "ve |- e ---> v ==>
-   (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"
-
-(* Proof by induction on the structure of evaluations *)
-
-apply (erule eval_ind)
-apply safe
-apply (blast intro: consistency_const consistency_var consistency_fn consistency_fix consistency_app1 consistency_app2)+
-done
-
-(* ############################################################ *)
-(* The Basic Consistency theorem                                *)
-(* ############################################################ *)
-
-lemma basic_consistency_lem:
-  "ve isofenv te ==> ve hastyenv te"
-apply (unfold isof_env_def hasty_env_def)
-apply safe
-apply (erule allE)
-apply (erule impE)
-apply assumption
-apply (erule exE)
-apply (erule conjE)
-apply (drule hasty_const)
-apply (simp (no_asm_simp))
-done
-
-lemma basic_consistency:
-  "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"
-apply (rule hasty_elim_const)
-apply (drule consistency)
-apply (blast intro!: basic_consistency_lem)
-done
-
-end