# Theory MT

Up to index of Isabelle/HOL/ex

theory MT
imports Main
uses [MT.ML]
begin

    (*  Title:      HOL/ex/mt.thy
        ID:         $Id: MT.thy,v 1.11 2005/09/06 17:10:43 wenzelm Exp $
        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).
    *)

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

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem infsys_p1:

      P a b ==> P (fst (a, b)) (snd (a, b))

theorem infsys_p2:

      P (fst (a, b)) (snd (a, b)) ==> P a b

theorem infsys_pp1:

      P a b c ==> P (fst (fst ((a, b), c))) (snd (fst ((a, b), c))) (snd ((a, b), c))

theorem infsys_pp2:

      P (fst (fst ((a, b), c))) (snd (fst ((a, b), c))) (snd ((a, b), c)) ==> P a b c

theorem lfp_intro2:

      [| mono f; x ∈ f (lfp f) |] ==> x ∈ lfp f

theorem lfp_elim2:

      [| x ∈ lfp f; mono f; !!y. y ∈ f (lfp f) ==> P y |] ==> P x

theorem lfp_ind2:

      [| x ∈ lfp f; mono f; !!y. y ∈ f (lfp f ∩ {x. P x}) ==> P y |] ==> P x

theorem gfp_coind2:

      [| x ∈ f ({x} ∪ gfp f); mono f |] ==> x ∈ gfp f

theorem gfp_elim2:

      [| x ∈ gfp f; mono f; !!y. y ∈ f (gfp f) ==> P y |] ==> P x

theorem eval_fun_mono:

      mono eval_fun

theorem eval_const:

      ve |- e_const c ---> v_const c

theorem eval_var2:

      ev ∈ ve_dom ve ==> ve |- e_var ev ---> ve_app ve ev

theorem eval_fn:

      ve |- fn ev => e ---> v_clos <| ev , e , ve |>

theorem eval_fix:

      cl = <| ev1.0 , e , ve + { ev2.0 |-> v_clos cl } |>
      ==> ve |- fix ev2.0  ev1.0  = e ---> v_clos cl

theorem eval_app1:

      [| ve |- e1.0 ---> v_const c1.0; ve |- e2.0 ---> v_const c2.0 |]
      ==> ve |- e1.0 @@ e2.0 ---> v_const (c_app c1.0 c2.0)

theorem eval_app2:

      [| ve |- e1.0 ---> v_clos <| xm , em , vem |>; ve |- e2.0 ---> v2.0;
         vem + { xm |-> v2.0 } |- em ---> v |]
      ==> ve |- e1.0 @@ e2.0 ---> v

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

theorem 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

theorem elab_fun_mono:

      mono elab_fun

theorem elab_const:

      c isof ty ==> te |- e_const c ===> ty

theorem elab_var:

      x ∈ te_dom te ==> te |- e_var x ===> te_app te x

theorem elab_fn:

      te + { x |=> ty1.0 } |- e ===> ty2.0 ==> te |- fn x => e ===> ty1.0 -> ty2.0

theorem elab_fix:

      te + { f |=> ty1.0 -> ty2.0 } + { x |=> ty1.0 } |- e ===> ty2.0
      ==> te |- fix f  x  = e ===> ty1.0 -> ty2.0

theorem elab_app:

      [| te |- e1.0 ===> ty1.0 -> ty2.0; te |- e2.0 ===> ty1.0 |]
      ==> te |- e1.0 @@ e2.0 ===> ty2.0

theorem elab_ind0:

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

theorem 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

theorem elab_elim0:

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

theorem 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

theorem elab_const_elim_lem:

      te |- e ===> t ==> e = e_const c --> c isof t

theorem elab_const_elim:

      te |- e_const c ===> t ==> c isof t

theorem elab_var_elim_lem:

      te |- e ===> t ==> e = e_var x --> t = te_app te x ∧ x ∈ te_dom te

theorem elab_var_elim:

      te |- e_var ev ===> t ==> t = te_app te ev ∧ ev ∈ te_dom te

theorem elab_fn_elim_lem:

      te |- e ===> t
      ==> e = fn x1.0 => e1.0 -->
          (∃t1 t2. t = t1 -> t2 ∧ te + { x1.0 |=> t1 } |- e1.0 ===> t2)

theorem elab_fn_elim:

      te |- fn x1.0 => e1.0 ===> t
      ==> ∃t1 t2. t = t1 -> t2 ∧ te + { x1.0 |=> t1 } |- e1.0 ===> t2

theorem elab_fix_elim_lem:

      te |- e ===> t
      ==> e = fix f  x  = e1.0 -->
          (∃t1 t2.
              t = t1 -> t2 ∧ te + { f |=> t1 -> t2 } + { x |=> t1 } |- e1.0 ===> t2)

theorem elab_fix_elim:

      te |- fix ev1.0  ev2.0  = e1.0 ===> t
      ==> ∃t1 t2.
             t = t1 -> t2 ∧
             te + { ev1.0 |=> t1 -> t2 } + { ev2.0 |=> t1 } |- e1.0 ===> t2

theorem elab_app_elim_lem:

      te |- e ===> t2.0
      ==> e = e1.0 @@ e2.0 --> (∃t1. te |- e1.0 ===> t1 -> t2.0 ∧ te |- e2.0 ===> t1)

theorem elab_app_elim:

      te |- e1.0 @@ e2.0 ===> t2.0
      ==> ∃t1. te |- e1.0 ===> t1 -> t2.0 ∧ te |- e2.0 ===> t1

theorem mono_hasty_fun:

      mono hasty_fun

theorem hasty_rel_const_coind:

      c isof t ==> (v_const c, t) ∈ hasty_rel

theorem 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)} ∪ hasty_rel |]
      ==> (v_clos <| ev , e , ve |>, t) ∈ hasty_rel

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

theorem 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

theorem hasty_const:

      c isof t ==> v_const c hasty t

theorem hasty_clos:

      te |- fn ev => e ===> t ∧ ve hastyenv te  ==> v_clos <| ev , e , ve |> hasty t

theorem hasty_elim_const_lem:

      v hasty t ==> ∀c. v = v_const c --> c isof t

theorem hasty_elim_const:

      v_const c hasty t ==> c isof t

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

theorem hasty_elim_clos:

      v_clos <| ev , e , ve |> hasty t
      ==> ∃te. te |- fn ev => e ===> t ∧ ve hastyenv te

theorem hasty_env1:

      [| ve hastyenv te ; v hasty t |]
      ==> ve + { ev |-> v } hastyenv te + { ev |=> t }

theorem consistency_const:

      [| ve hastyenv te ; te |- e_const c ===> t |] ==> v_const c hasty t

theorem consistency_var:

      [| ev ∈ ve_dom ve; ve hastyenv te ; te |- e_var ev ===> t |]
      ==> ve_app ve ev hasty t

theorem consistency_fn:

      [| ve hastyenv te ; te |- fn ev => e ===> t |]
      ==> v_clos <| ev , e , ve |> hasty t

theorem consistency_fix:

      [| cl = <| ev1.0 , e , ve + { ev2.0 |-> v_clos cl } |>; ve hastyenv te ;
         te |- fix ev2.0  ev1.0  = e ===> t |]
      ==> v_clos cl hasty t

theorem consistency_app1:

      [| ∀t te. ve hastyenv te  --> te |- e1.0 ===> t --> v_const c1.0 hasty t;
         ∀t te. ve hastyenv te  --> te |- e2.0 ===> t --> v_const c2.0 hasty t;
         ve hastyenv te ; te |- e1.0 @@ e2.0 ===> t |]
      ==> v_const (c_app c1.0 c2.0) hasty t

theorem consistency_app2:

      [| ∀t te. ve hastyenv te  -->
                te |- e1.0 ===> t --> v_clos <| evm , em , vem |> hasty t;
         ∀t te. ve hastyenv te  --> te |- e2.0 ===> t --> v2.0 hasty t;
         ∀t te. vem + { evm |-> v2.0 } hastyenv te  --> te |- em ===> t --> v hasty t;
         ve hastyenv te ; te |- e1.0 @@ e2.0 ===> t |]
      ==> v hasty t

theorem consistency:

      ve |- e ---> v ==> ∀t te. ve hastyenv te  --> te |- e ===> t --> v hasty t

theorem basic_consistency_lem:

      ve isofenv te ==> ve hastyenv te

theorem basic_consistency:

      [| ve isofenv te; ve |- e ---> v_const c; te |- e ===> t |] ==> c isof t