src/HOL/ex/MT.thy

improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging

(*  Title:      HOL/ex/MT.thy
    ID:         $Id$
    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).
*)

header {* Milner-Tofte: Co-induction in Relational Semantics *}

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)

axioms

(*
  Expression constructors must be injective, distinct and it must be possible
  to do induction over expressions.
*)

(* All the constructors are injective *)

  e_const_inj: "e_const(c1) = e_const(c2) ==> c1 = c2"
  e_var_inj: "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
  e_fn_inj: "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
  e_fix_inj:
    " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
     ev11 = ev21 & ev12 = ev22 & e1 = e2
   "
  e_app_inj: "e11 @@ e12 = e21 @@ e22 ==> e11 = e21 & e12 = e22"

(* All constructors are distinct *)

  e_disj_const_var: "~e_const(c) = e_var(ev)"
  e_disj_const_fn: "~e_const(c) = fn ev => e"
  e_disj_const_fix: "~e_const(c) = fix ev1(ev2) = e"
  e_disj_const_app: "~e_const(c) = e1 @@ e2"
  e_disj_var_fn: "~e_var(ev1) = fn ev2 => e"
  e_disj_var_fix: "~e_var(ev) = fix ev1(ev2) = e"
  e_disj_var_app: "~e_var(ev) = e1 @@ e2"
  e_disj_fn_fix: "~fn ev1 => e1 = fix ev21(ev22) = e2"
  e_disj_fn_app: "~fn ev1 => e1 = e21 @@ e22"
  e_disj_fix_app: "~fix ev11(ev12) = e1 = e21 @@ e22"

(* Strong elimination, induction on expressions  *)

  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 *)

  t_const_inj: "t_const(c1) = t_const(c2) ==> c1 = c2"
  t_fun_inj: "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22"

(* All constructors are distinct, not needed so far ... *)

(* Strong elimination, induction on types *)

 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 *)

  v_const_inj: "v_const(c1) = v_const(c2) ==> c1 = c2"
  v_clos_inj:
    " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
     ev1 = ev2 & e1 = e2 & ve1 = ve2"

(* All constructors are distinct *)

  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.
*)

  ve_dom_owr: "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}"

  ve_app_owr1: "ve_app (ve + {ev |-> v}) ev=v"
  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.  *)

  te_dom_owr: "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}"

  te_app_owr1: "te_app (te + {ev |=> t}) ev=t"
  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)
     )
   "

axioms
  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 {*
val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
*}

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)
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)
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)
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 {* safe_tac HOL_cs *})
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 {* safe_tac HOL_cs *})
(*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 {* safe_tac HOL_cs *})
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