Theory TypedSigma

(*  Title:      Sigma/Typed_Sigma.thy
    Author:     Florian Kammuller and Henry Sudhof, 2006
*)

section ‹First Order Types for Sigma terms›

theory TypedSigma imports "../preliminary/Environments" Sigma begin

subsubsection ‹Types and typing rules›
text‹The inductive definition of the typing relation.›

definition
  return :: "(type × type) ⇒ type" where
  "return a = fst a"

definition
  param :: "(type × type) ⇒ type" where
  "param a = snd a"

primrec
  do :: "type ⇒ (Label set)"  
where
 "do (Object l) = (dom l)"

primrec
  type_get :: "type ⇒ Label ⇒ (type × type) option "  ("_^_" 1000)
where
 "(Object l)^n = (l n)"

  (* we need to restrict objects to ok environments, 
     as the empty object does not yield ok env otherwise *)
inductive 
  typing :: "(type environment) ⇒ sterm ⇒ type ⇒ bool"    
  ("_ ⊢ _ : _" [80, 0, 80] 230)
where 
  T_Var[intro!]:
    "⟦ ok env; x ∈ env_dom env; (the (env!x)) = T ⟧ 
    ⟹ env ⊢ (Fvar x) : T"
| T_Obj[intro!]:
    "⟦ ok env; dom b = do A;  finite F; 
       ∀l∈do A. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
        ⟶ env⦇s:A⦈⦇p:param(the (A^l))⦈ 
            ⊢ (the (b l)⇗[Fvar s,Fvar p]⇖) : return(the (A^l)) ⟧ 
    ⟹ env ⊢ (Obj b A) : A"
| T_Upd[intro!]:  
    "⟦ finite F; 
       ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
        ⟶  env⦇s:A⦈⦇p:param(the (A^l))⦈
             ⊢ (n⇗[Fvar s,Fvar p]⇖) : return(the (A^l));
    env ⊢ a : A; l ∈ do A ⟧ ⟹ env ⊢ Upd a l n : A"
| T_Call[intro!]: 
    "⟦ env ⊢ a : A; env ⊢ b : param(the (A^l)); l ∈ do A ⟧ 
    ⟹ env ⊢ (Call a l b) : return(the (A^l))"

inductive_cases typing_elims [elim!]:
  "e ⊢ Obj b T : T"
  "e ⊢ Fvar x : T"
  "e ⊢ Call a l b : T"
  "e ⊢ Upd a l n : T"

subsubsection ‹Basic lemmas›
text‹Basic treats of the type system.›
lemma not_bvar: "e ⊢ t : T ⟹ ∀i. t ≠ Bvar i"
  by (erule typing.cases, simp_all)

lemma typing_regular': "e ⊢ t : T ⟹ ok e" 
  by (induct rule:typing.induct, auto)

lemma typing_regular'': "e ⊢ t : T ⟹ lc t" 
  by (induct rule:typing.induct, auto)

theorem typing_regular: "e ⊢ t : T ⟹ ok e ∧ lc t" 
  by (simp add: typing_regular' typing_regular'')

lemma obj_inv: "e ⊢ Obj f U : A ⟹ A = U"
  by (erule typing.cases, auto)

lemma obj_inv_elim: 
  "e ⊢ Obj f U : U 
  ⟹ (dom f = do U) 
    ∧ (∃F. finite F ∧ (∀l∈do U. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
        ⟶ e⦇s:U⦈⦇p:param(the U^l)⦈
            ⊢ (the (f l)⇗[Fvar s,Fvar p]⇖) : return(the (U^l))))"
  by (erule typing.cases, simp_all, blast)

lemma typing_induct[consumes 1, case_names Fvar Call Upd Obj Bnd]:
  fixes 
  env :: "type environment" and t :: sterm and T :: type and 
  P1 :: "type environment ⇒ sterm ⇒ type ⇒ bool" and
  P2 :: "type environment ⇒ sterm ⇒ type ⇒ Label ⇒ bool"
  assumes
  "env ⊢ t : T" and
  "⋀env T x. ⟦ ok env; x ∈ env_dom env; the env!x = T ⟧
  ⟹ P1 env (Fvar x) T" and
  "⋀env T t l p. ⟦ env ⊢ t : T; P1 env t T; env ⊢ p : param (the(T^l));
                    P1 env p (param (the(T^l))); l ∈ do T ⟧
  ⟹ P1 env (Call t l p) (return (the(T^l)))" and
  "⋀env T t l u. ⟦ env ⊢ t : T; P1 env t T; l ∈ do T; P2 env u T l ⟧
  ⟹ P1 env (Upd t l u) T" and
  "⋀env T f. ⟦ ok env; dom f = do T; ∀l∈dom f. P2 env (the(f l)) T l ⟧
  ⟹ P1 env (Obj f T) T" and
  "⋀env T l t L. ⟦ ok env; finite L; 
                  ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                   ⟶ env⦇s:T⦈⦇p:param (the(T^l))⦈ 
                       ⊢ (t⇗[Fvar s, Fvar p]⇖) : return (the(T^l))
                      ∧ P1 (env⦇s:T⦈⦇p:param (the(T^l))⦈) (t⇗[Fvar s, Fvar p]⇖) 
                           (return (the(T^l))) ⟧
  ⟹ P2 env t T l"
  shows
  "P1 env t T"
  using assms by (induct rule: typing.induct, auto simp: typing_regular')

(* TODO: delete after refactoring of disjunct_env *)
lemma ball_Tltsp:
  fixes 
  P1 :: "type ⇒ Label ⇒ sterm ⇒ string ⇒ string ⇒ bool" and 
  P2 :: "type ⇒ Label ⇒ sterm ⇒ string ⇒ string ⇒ bool"
  assumes 
  "⋀l t t'. ⟦ ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p ⟶ P1 T l t s p ⟧ 
  ⟹ ∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p ⟶ P2 T l t s p" and
  "∀l∈do T. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p ⟶ P1 T l (the(f l)) s p"
  shows "∀l∈do T. ∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p ⟶ P2 T l (the(f l)) s p"
proof
  fix l assume "l ∈ do T"
  with assms(2) 
  have "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p ⟶ P1 T l (the(f l)) s p"
    by simp
  with assms(1) 
  show "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p ⟶ P2 T l (the(f l)) s p"
    by simp
qed

(* TODO: delete after refactoring of subject_reduction *)
lemma ball_ex_finite:
  fixes 
  S :: "'a set" and F :: "'b set" and x :: 'a and 
  P :: "'a ⇒ 'b ⇒ 'b ⇒ bool"
  assumes 
  "finite S" and "finite F" and
  "∀x∈S. (∃F'. finite F'
              ∧ (∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
                  ⟶ P x s p))"
  shows 
  "∃F'. finite F'
      ∧ (∀x∈S. ∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
                 ⟶ P x s p)"
proof -
  from assms show ?thesis 
  proof (induct S)
    case empty thus ?case by force
  next
    case (insert x S)
    from insert(5)
    have 
      "∀y∈S. (∃F'. finite F' 
                  ∧ (∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
                      ⟶ P y s p))"
      by simp
    from insert(3)[OF ‹finite F› this]
    obtain F1 where 
      "finite F1" and
      pred_S: "∀y∈S. ∀s p. s ∉ F1 ∪ F ∧ p ∉ F1 ∪ F ∧ s ≠ p
                       ⟶ P y s p"
      by auto
    from insert(5)
    obtain F2 where 
      "finite F2" and
      "∀s p. s ∉ F2 ∪ F ∧ p ∉ F2 ∪ F ∧ s ≠ p ⟶ P x s p"
      by auto
    with pred_S have 
      "∀y∈insert x S. ∀s p. s ∉ F1 ∪ F2 ∪ F ∧ p ∉ F1 ∪ F2 ∪ F ∧ s ≠ p
                        ⟶ P y s p"
      by auto
    moreover
    from ‹finite F1› ‹finite F2› have "finite (F1 ∪ F2)" by simp
    ultimately
    show ?case by blast
  qed
qed

(* TODO: delete after refactoring of type_renaming' *)
lemma bnd_renaming_lem:
  assumes 
  "s ∉ FV t'" and "p ∉ FV t'" and "x ∉ FV t'" and "y ∉ FV t'" and
  "x ∉ env_dom env'" and "y ∉ env_dom env'" and "s ≠ p" and "x ≠ y" and
  "t = {Suc n → [Fvar s, Fvar p]} t'" and "env = env'⦇s:A⦈⦇p:B⦈" and
  pred_bnd:
  "∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa 
    ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ ⊢ (t⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
        ∧ (∀env'' t'' s' p' x' y' A' B' n'. 
            s' ∉ FV t'' ⟶ p' ∉ FV t'' ⟶ x' ∉ FV t'' ⟶ y' ∉ FV t'' ⟶ 
            x' ∉ env_dom env'' ⟶ y' ∉ env_dom env'' ⟶ x' ≠ y' ⟶ s' ≠ p' 
            ⟶ (t⇗[Fvar sa,Fvar pa]⇖) = {n' → [Fvar s',Fvar p']} t'' 
            ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env''⦇s':A'⦈⦇p':B'⦈ 
            ⟶ env''⦇x':A'⦈⦇y':B'⦈ 
                ⊢ {n' → [Fvar x',Fvar y']} t'' : return(the(T^l)))" and
  "FV t' ⊆ F'"
  shows
  "∀sa pa. sa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env' 
         ∧ pa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env' 
         ∧ sa ≠ pa
    ⟶ env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
        ⊢ ({Suc n → [Fvar x, Fvar y]} t'⇗[Fvar sa,Fvar pa]⇖) : return (the(T^l))"
proof (intro strip, elim conjE)
  fix sa pa 
  assume 
    nin_sa: "sa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'" and
    nin_pa: "pa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'" and "sa ≠ pa"
  hence "sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa" by auto
  moreover
  {
    fix a assume "a ∉ FV t'" and "a ∈ {s,p,x,y}"
    with 
      ‹FV t' ⊆ F'› nin_sa nin_pa ‹sa ≠ pa› 
      sopen_FV[of 0 "Fvar sa" "Fvar pa" t']
    have "a ∉ FV (t'⇗[Fvar sa,Fvar pa]⇖)" by (auto simp: openz_def)
  } note 
      this[OF ‹s ∉ FV t'›] this[OF ‹p ∉ FV t'›] 
      this[OF ‹x ∉ FV t'›] this[OF ‹y ∉ FV t'›]
  moreover
  from 
    not_in_env_bigger_2[OF ‹x ∉ env_dom env'›] 
    not_in_env_bigger_2[OF ‹y ∉ env_dom env'›]
    nin_sa nin_pa
  have 
    "x ∉ env_dom (env'⦇sa:T⦈⦇pa:param(the(T^l))⦈) 
    ∧ y ∉ env_dom (env'⦇sa:T⦈⦇pa:param(the(T^l))⦈)" by auto
  moreover
  from ‹t = {Suc n → [Fvar s, Fvar p]} t'› sopen_commute[OF Suc_not_Zero] 
  have "(t⇗[Fvar sa,Fvar pa]⇖) = {Suc n → [Fvar s,Fvar p]} (t'⇗[Fvar sa,Fvar pa]⇖)"
    by (auto simp: openz_def)
  moreover
  from 
    subst_add[of s sa env' A T] subst_add[of sa p "env'⦇s:A⦈" T B] 
    subst_add[of s pa "env'⦇sa:T⦈" A "param(the(T^l))"]
    subst_add[of p pa "env'⦇sa:T⦈⦇s:A⦈" B "param(the(T^l))"]
    ‹env = env'⦇s:A⦈⦇p:B⦈› nin_sa nin_pa
  have "env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env'⦇sa:T⦈⦇pa:param(the(T^l))⦈⦇s:A⦈⦇p:B⦈"
    by auto
  ultimately
  have 
    "env'⦇sa:T⦈⦇pa:param(the T^l)⦈⦇x:A⦈⦇y:B⦈
     ⊢ {Suc n → [Fvar x, Fvar y]} (t'⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
    using ‹s ≠ p› ‹x ≠ y› pred_bnd by auto
  moreover
  from 
    subst_add[of y sa "env'⦇x:A⦈" B T] subst_add[of x sa env' A T] 
    subst_add[of y pa "env'⦇sa:T⦈⦇x:A⦈" B "param(the(T^l))"]
    subst_add[of x pa "env'⦇sa:T⦈" A "param(the(T^l))"] 
    nin_sa nin_pa
  have 
    "env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
     = env'⦇sa:T⦈⦇pa:param(the(T^l))⦈⦇x:A⦈⦇y:B⦈"
    by auto
  ultimately 
  show 
    "env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
     ⊢ ({Suc n → [Fvar x, Fvar y]} t'⇗[Fvar sa,Fvar pa]⇖) : return (the(T^l))"
    using sopen_commute[OF not_sym[OF Suc_not_Zero]]
    by (simp add: openz_def)
qed

(* TODO: refactor to work with typing_induct *)
lemma type_renaming'[rule_format]:
  "e ⊢ t : C ⟹
  (⋀env t' s p x y A B n. ⟦ s ∉ FV t'; p ∉ FV t'; x ∉ FV t'; y ∉ FV t'; 
                             x ∉ env_dom env; y ∉ env_dom env; s ≠ p;  x ≠ y;
                             t = {n → [Fvar s,Fvar p]} t'; e = env⦇s:A⦈⦇p:B⦈ ⟧
    ⟹ env⦇x:A⦈⦇y:B⦈ ⊢ {n → [Fvar x,Fvar y]} t' : C)"
proof (induct set:typing)
  case (T_Call env t1 T t2 l env' t' s p x y A B n)
  with sopen_eq_Call[OF sym[OF ‹Call t1 l t2 = {n → [Fvar s,Fvar p]} t'›]]
  show ?case by auto
next
  case (T_Var env a T env' t' s p x y A B n)
  from ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ok_add_2[of env' s A p B] 
  have "ok env'" by simp
  from 
    ok_add_ok[OF ok_add_ok[OF this ‹x ∉ env_dom env'›]
                 not_in_env_bigger[OF ‹y ∉ env_dom env'› not_sym[OF ‹x ≠ y›]]]
  have ok: "ok (env'⦇x:A⦈⦇y:B⦈)" by assumption

  from sopen_eq_Fvar[OF sym[OF ‹Fvar a = {n → [Fvar s,Fvar p]} t'›]] 
  show ?case
  proof (elim disjE conjE)
    assume "t' = Fvar a" with T_Var(4-7)
    obtain "a ≠ s" and "a ≠ p" and "a ≠ x" and "a ≠ y" by auto
    note in_env_smaller2[OF _ this(1-2)]
    from ‹a ∈ env_dom env› ‹env = env'⦇s:A⦈⦇p:B⦈› this[of env' A B]
    have "a ∈ env_dom env'" by simp
    from env_bigger2[OF ‹x ∉ env_dom env'› ‹y ∉ env_dom env'› this ‹x ≠ y›]
    have inenv: "a ∈ env_dom (env'⦇x:A⦈⦇y:B⦈)" by assumption
    note get_env_bigger2[OF _ ‹a ≠ s› ‹a ≠ p›]
    from 
      this[of env' A B] ‹a ∈ env_dom env› ‹the env!a = T› 
      ‹env = env'⦇s:A⦈⦇p:B⦈› get_env_bigger2[OF inenv ‹a ≠ x› ‹a ≠ y›] 
    have "the (env'⦇x:A⦈⦇y:B⦈!a) = T" by simp
    from typing.T_Var[OF ok inenv this] ‹t' = Fvar a› show ?case by simp
  next
    assume "a = s" and "t' = Bvar (Self n)"
    from 
      this(1) ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ‹the env!a = T› 
      add_get2_1[of env' s A p B]
    have "T = A" by simp
    moreover
    from ‹t' = Bvar (Self n)› have "{n → [Fvar x,Fvar y]} t' = Fvar x" by simp
    ultimately
    show ?case using in_add_2[OF ok] typing.T_Var[OF ok _ add_get2_1[OF ok]]
      by simp
  next
    note subst = subst_add[OF ‹x ≠ y›] 
    from subst[of env' A B] ok have ok': "ok (env'⦇y:B⦈⦇x:A⦈)" by simp
    assume "a = p" and "t' = Bvar (Param n)"
    from 
      this(1) ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ‹the env!a = T›
      add_get2_2[of env' s A p B]
    have "T = B" by simp
    moreover
    from ‹t' = Bvar (Param n)› have "{n → [Fvar x,Fvar y]} t' = Fvar y" by simp
    ultimately
    show ?case 
      using 
        subst[of env' A B] in_add_2[OF ok'] 
        typing.T_Var[OF ok' _ add_get2_1[OF ok']]
      by simp
  qed
next
  case (T_Upd F env T l t2 t1 env' t' s p x y A B n)
  from sopen_eq_Upd[OF sym[OF ‹Upd t1 l t2 = {n → [Fvar s,Fvar p]} t'›]]
  obtain t1' t2' where 
    t1: "t1 = {n → [Fvar s,Fvar p]} t1'" and
    t2: "t2 = {Suc n → [Fvar s,Fvar p]} t2'" and
    t': "t' = Upd t1' l t2'" 
    by auto
  { fix a assume "a ∉ FV t'" with t' have "a ∉ FV t1'" by simp } 
  note 
    t1' = T_Upd(4)[OF this[OF ‹s ∉ FV t'›] this[OF ‹p ∉ FV t'›] 
                      this[OF ‹x ∉ FV t'›] this[OF ‹y ∉ FV t'›] 
                      ‹x ∉ env_dom env'› ‹y ∉ env_dom env'›
                      ‹s ≠ p› ‹x ≠ y› t1 ‹env = env'⦇s:A⦈⦇p:B⦈›]
  from ok_finite[of env'] ok_add_2[OF typing_regular'[OF this]]
  have findom: "finite (env_dom env')" by simp

  { fix a assume "a ∉ FV t'" with t' have "a ∉ FV t2'" by simp }
  note 
    bnd_renaming_lem[OF this[OF ‹s ∉ FV t'›] this[OF ‹p ∉ FV t'›] 
                        this[OF ‹x ∉ FV t'›] this[OF ‹y ∉ FV t'›] 
                        ‹x ∉ env_dom env'› ‹y ∉ env_dom env'›
                        ‹s ≠ p› ‹x ≠ y› t2 ‹env = env'⦇s:A⦈⦇p:B⦈›]
  from this[of F T l "FV t2'"] T_Upd(2)
  have 
    "∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV t2' ∪ env_dom env' 
           ∧ pa ∉ F ∪ {s, p, x, y} ∪ FV t2' ∪ env_dom env' 
           ∧ sa ≠ pa 
      ⟶ env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
          ⊢ ({Suc n → [Fvar x,Fvar y]} t2'⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
    by simp
  from 
    typing.T_Upd[OF _ this t1' ‹l ∈ do T›]
    ‹finite F› findom t' 
  show ?case by simp
next
  case (T_Obj env f T F env' t' s p x y A B n)
  from ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ok_add_2[of env' s A p B] 
  have "ok env'" by simp
  from 
    ok_add_ok[OF ok_add_ok[OF this ‹x ∉ env_dom env'›]
                 not_in_env_bigger[OF ‹y ∉ env_dom env'› not_sym[OF ‹x ≠ y›]]]
  have ok: "ok (env'⦇x:A⦈⦇y:B⦈)" by assumption
  from sopen_eq_Obj[OF sym[OF ‹Obj f T = {n → [Fvar s,Fvar p]} t'›]] 
  obtain f' where 
    obj: "{n → [Fvar s,Fvar p]} Obj f' T = Obj f T" and
    t': "t' = Obj f' T" by auto
  from 
    this(1) ‹dom f = do T›
    sym[OF dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']]
    dom_sopenoption_lem[of "Suc n" "Fvar x" "Fvar y" f']
  have dom: "dom (λl. sopen_option (Suc n) (Fvar x) (Fvar y) (f' l)) = do T" 
    by simp
    
  from 
    ‹finite F› finite_FV[of "Obj f' T"] 
    ok_finite[of env'] ok_add_2[OF ok]
  have finF: "finite (F ∪ {s,p,x,y} ∪  FV (Obj f' T) ∪ env_dom env')"
    by simp

  have 
    "∀l∈do T. ∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env' 
                     ∧ pa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env' 
                     ∧ sa ≠ pa 
      ⟶ env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
          ⊢ (the(sopen_option (Suc n) (Fvar x) (Fvar y) (f' l))⇗[Fvar sa,Fvar pa]⇖) : 
          return(the(T^l))"
  proof 
    fix l assume "l ∈ do T" with T_Obj(4)
    have cof: 
      "∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
        ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈
            ⊢ (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
          ∧ (∀env'' t'' s' p' x' y' A' B' n'.
               s' ∉ FV t'' ⟶ p' ∉ FV t'' ⟶ x' ∉ FV t'' ⟶ y' ∉ FV t'' 
               ⟶ x' ∉ env_dom env'' ⟶ y' ∉ env_dom env'' ⟶ x' ≠ y' 
               ⟶ s' ≠ p' 
               ⟶ (the(f l)⇗[Fvar sa,Fvar pa]⇖) = {n' → [Fvar s',Fvar p']} t'' 
               ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env''⦇s':A'⦈⦇p':B'⦈ 
               ⟶ env''⦇x':A'⦈⦇y':B'⦈
                   ⊢ {n' → [Fvar x',Fvar y']} t'' : return(the(T^l)))"
      by simp
    from 
      ‹l ∈ do T› ‹dom f = do T› ‹Obj f T = {n → [Fvar s,Fvar p]} t'› obj t'
      dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']
    have indomf': "l ∈ dom f'" by auto
    hence 
      opened: "the (sopen_option (Suc n) (Fvar x) (Fvar y) (f' l)) 
               = {Suc n → [Fvar x,Fvar y]} the(f' l)" 
      by force
    from indomf' have FVsubset: "FV (the(f' l)) ⊆ FV (Obj f' T)" by force
    with 
      ‹s ∉ FV t'› ‹p ∉ FV t'› ‹x ∉ FV t'› ‹y ∉ FV t'› obj t'
      indomf' FV_option_lem[of f']
    obtain 
      "s ∉ FV (the(f' l))" and "p ∉ FV (the(f' l))" and
      "x ∉ FV (the(f' l))" and "y ∉ FV (the(f' l))" and
      "the(f l) = {Suc n → [Fvar s,Fvar p]} the(f' l)" by auto
    from 
      bnd_renaming_lem[OF this(1-4) ‹x ∉ env_dom env'› ‹y ∉ env_dom env'›
                          ‹s ≠ p› ‹x ≠ y› this(5) ‹env = env'⦇s:A⦈⦇p:B⦈› 
                          cof FVsubset]
    show 
      "∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env' 
             ∧ pa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env' 
             ∧ sa ≠ pa 
        ⟶ env'⦇x:A⦈⦇y:B⦈⦇sa:T⦈⦇pa:param(the(T^l))⦈
            ⊢ (the(sopen_option (Suc n) (Fvar x) (Fvar y) (f' l))⇗[Fvar sa,Fvar pa]⇖) : 
              return(the(T^l))"
      by (subst opened, assumption)
  qed
  from typing.T_Obj[OF ok dom finF this] t' show ?case by simp
qed

lemma type_renaming: 
  "⟦ e⦇s:A⦈⦇p:B⦈ ⊢ {n → [Fvar s,Fvar p]} t : T; 
     s ∉ FV t; p ∉ FV t; x ∉ FV t; y ∉ FV t; 
     x ∉ env_dom e; y ∉ env_dom e; x ≠ y; s ≠ p⟧ 
  ⟹ e⦇x:A⦈⦇y:B⦈ ⊢ {n → [Fvar x,Fvar y]} t : T"
  by (auto simp: type_renaming')
(* too weak, as we need specific s,p *)

lemma obj_inv_elim': 
  assumes 
  "e ⊢ Obj f U : U" and 
  nin_s: "s ∉ FV (Obj f U) ∪ env_dom e" and
  nin_p: "p ∉ FV (Obj f U) ∪ env_dom e" and "s ≠ p"
  shows 
  "(dom f = do U) ∧ (∀l∈do U. e⦇s:U⦈⦇p:param(the(U^l))⦈
                               ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(U^l)))"
  using assms
proof (cases rule: typing.cases)
  case (T_Obj F)
(*  from `e = env` `Obj f U = Obj f' T` `dom f' = do T`
  have "dom f = do U" by simp*)
  thus ?thesis 
  proof (simp, intro strip)
    fix l assume "l ∈ do U"
    from ‹finite F› finite_FV[of "Obj f U"] have "finite (F ∪ FV (Obj f U) ∪ {s,p})"
      by simp
    from exFresh_s_p_cof[OF this]
    obtain sa pa where 
      "sa ≠ pa" and
      nin_sa: "sa ∉ F ∪ FV (Obj f U)" and
      nin_pa: "pa ∉ F ∪ FV (Obj f U)" by auto
    with ‹l ∈ do U› T_Obj(4)
    have 
      "e⦇sa:U⦈⦇pa:param(the(U^l))⦈ 
       ⊢ (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(U^l))"
      by simp
    moreover
    from ‹l ∈ do U› ‹dom f = do U›  
    have "l ∈ dom f" by simp
    with nin_s nin_p nin_sa nin_pa FV_option_lem[of f]
    have 
      "sa ∉ FV (the(f l)) ∧ pa ∉ FV (the(f l)) 
       ∧ s ∉ FV (the(f l)) ∧ p ∉ FV (the(f l))
       ∧ s ∉ env_dom e ∧ p ∉ env_dom e" by auto
    ultimately
    show 
      "e⦇s:U⦈⦇p:param(the(U^l))⦈ 
       ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(U^l))"
      using type_renaming[OF _ _ _ _ _ _ _ ‹s ≠ p› ‹sa ≠ pa›]
      by (simp add: openz_def)
  qed
qed

lemma dom_lem: "e ⊢ Obj f (Object fun) : Object fun ⟹ dom f = dom fun"
  by (erule typing.cases, auto)

lemma abs_typeE: 
  assumes "e ⊢ Call (Obj f U) l b : T"
  shows 
  "(∃F. finite F 
      ∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
          ⟶ e⦇s:U⦈⦇p: param(the(U^l))⦈ ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : T) ⟹ P) 
  ⟹ P"
  using assms
proof (cases rule: typing.cases)
  case (T_Call A (*env t1 t2=b*))
  assume 
    cof: "∃F. finite F 
            ∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
                ⟶ e⦇s:U⦈⦇p: param(the(U^l))⦈ ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : T) 
          ⟹ P"
  from 
    ‹T = return(the(A^l))›
    ‹e ⊢ Obj f U : A› ‹l ∈ do A› obj_inv[of e f U A]
  obtain "e ⊢ (Obj f U) : U" and "T = return(the(U^l))" and "l ∈ do U" 
    by simp
  from obj_inv_elim[OF this(1)] this(2-3) cof show ?thesis by blast
qed

subsubsection ‹Substitution preserves Well-Typedness›
lemma bigger_env_lemma[rule_format]: 
  assumes "e ⊢ t : T"
  shows "∀x X. x ∉ env_dom e ⟶ e⦇x:X⦈ ⊢ t: T"
proof -
  define pred_cof
    where "pred_cof L env t T l ⟷
      (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
        ⟶ env⦇s:T⦈⦇p:param (the(T^l))⦈ ⊢ (t⇗[Fvar s,Fvar p]⇖) : return (the(T^l)))"
    for L env t T l
  from assms show ?thesis
  proof (induct
      taking: "λenv t T l. ∀x X. x ∉ env_dom env 
                            ⟶ (∃L. finite L ∧ pred_cof L (env⦇x:X⦈) t T l)"
      rule: typing_induct)
    case Call thus ?case by auto
  next
    case (Fvar env Ta xa) thus ?case
    proof (intro strip)
      fix x X assume "x ∉ env_dom env"
      from 
        get_env_smaller[OF ‹xa ∈ env_dom env› this]
        T_Var[OF ok_add_ok[OF ‹ok env› this]
        env_bigger[OF this ‹xa ∈ env_dom env›]]
        ‹the env!xa = Ta›
      show "env⦇x:X⦈ ⊢ Fvar xa : Ta" by simp
    qed
  next
    case (Obj env Ta f) note pred_o = this(3)
    define pred_cof'
      where "pred_cof' x X b l ⟷ (∃L. finite L ∧ pred_cof L (env⦇x:X⦈) (the b) Ta l)" for x X b l
    from pred_o
    have pred: "∀x X. x ∉ env_dom env ⟶ (∀l∈dom f. pred_cof' x X (f l) l)"
      by (intro fmap_ball_all2'[of f "λx X. x ∉ env_dom env" pred_cof'],
        unfold pred_cof_def pred_cof'_def, simp)
    show ?case
    proof (intro strip)
      fix x X 
      define pred_bnd
        where "pred_bnd s p b l ⟷
          env⦇x:X⦈⦇s:Ta⦈⦇p:param (the(Ta^l))⦈ ⊢ (the b⇗[Fvar s,Fvar p]⇖) : return (the(Ta^l))"
        for s p b l
      assume "x ∉ env_dom env"
      with pred fmap_ex_cof[of f pred_bnd] ‹dom f = do Ta›
      obtain L where
        "finite L" and "∀l∈do Ta. pred_cof L (env⦇x:X⦈) (the(f l)) Ta l"
        unfolding pred_bnd_def pred_cof_def pred_cof'_def
        by auto
      from 
        T_Obj[OF ok_add_ok[OF ‹ok env› ‹x ∉ env_dom env›] 
                 ‹dom f = do Ta› this(1)]
        this(2)
      show "env⦇x:X⦈ ⊢ Obj f Ta : Ta"
        unfolding pred_cof_def
        by simp
    qed
  next
    case (Upd env Ta t l u) 
    note pred_t = this(2) and pred_u = this(4)
    show ?case
    proof (intro strip)
      fix x X assume "x ∉ env_dom env" 
      with pred_u obtain L where
        "finite L" and "pred_cof L (env⦇x:X⦈) u Ta l" by auto
      with ‹l ∈ do Ta› ‹x ∉ env_dom env› pred_t
      show "env⦇x:X⦈ ⊢ Upd t l u : Ta" 
        unfolding pred_cof_def
        by auto
    qed
  next
    case (Bnd env Ta l t L) note pred = this(3)
    show ?case
    proof (intro strip)
      fix x X assume "x ∉ env_dom env"
      thus "∃L. finite L ∧ pred_cof L (env⦇x:X⦈) t Ta l"
      proof (rule_tac x = "L ∪ {x}" in exI, simp add: ‹finite L›, 
          unfold pred_cof_def, auto)
        fix s p
        assume 
          "s ∉ L" and "p ∉ L" and "s ≠ p" and
          "s ≠ x" and "p ≠ x"
        note 
          subst_add[OF not_sym[OF ‹s ≠ x›]]
          subst_add[OF not_sym[OF ‹p ≠ x›]]
        from 
          this(1)[of env X Ta] this(2)[of "env⦇s:Ta⦈" X "param (the(Ta^l))"]
          pred ‹s ∉ L› ‹p ∉ L› ‹s ≠ p›
          not_in_env_bigger_2[OF ‹x ∉ env_dom env› 
                                 not_sym[OF ‹s ≠ x›] not_sym[OF ‹p ≠ x›]]
        show 
          "env⦇x:X⦈⦇s:Ta⦈⦇p:param (the(Ta^l))⦈ 
          ⊢ (t⇗[Fvar s,Fvar p]⇖) : return (the(Ta^l))"
          by auto
      qed
    qed
  qed
qed

lemma bnd_disj_env_lem: 
  assumes 
  "ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2" and
  "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
    ⟶ e1⦇s:T⦈⦇p:param(the(T^l))⦈
        ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l)) 
        ∧ (env_dom (e1⦇s:T⦈⦇p:param(the(T^l))⦈) ∩ env_dom e2 = {} 
    ⟶ ok e2 
    ⟶ e1⦇s:T⦈⦇p:param(the(T^l))⦈+e2 
        ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))"
  shows 
  "∀s p. s ∉ F ∪ env_dom (e1+e2) ∧ p ∉ F ∪ env_dom (e1+e2) ∧ s ≠ p
    ⟶ (e1+e2)⦇s:T⦈⦇p:param(the(T^l))⦈ ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
proof (intro strip, elim conjE)
  fix s p assume 
    nin_s: "s ∉ F ∪ env_dom (e1+e2)" and
    nin_p: "p ∉ F ∪ env_dom (e1+e2)" and "s ≠ p"
  from 
    this(1-2) env_add_dom_2[OF assms(1) _ _ this(3)]
    assms(2) env_app_dom[OF assms(1-3)]
  have "env_dom (e1⦇s:T⦈⦇p:param(the(T^l))⦈) ∩ env_dom e2 = {}" by simp
  with 
    env_app_add2[OF assms(1-3) _ _ _ _ ‹s ≠ p›]
    env_app_dom[OF assms(1-3)] ‹ok e2› assms(4) nin_s nin_p ‹s ≠ p›
  show "(e1+e2)⦇s:T⦈⦇p:param(the(T^l))⦈ ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
    by auto
qed

(* TODO: refactor to work with typing_induct *)
lemma disjunct_env: 
  assumes "e ⊢ t : A" 
  shows "(env_dom e ∩ env_dom e' = {} ⟹ ok e' ⟹ e + e' ⊢ t : A)"
  using assms
proof (induct rule: typing.induct)
  case T_Call thus ?case by auto
next
  case (T_Var env x T)
  from 
    env_app_dom[OF ‹ok env› ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›]
    ‹x ∈ env_dom env›
  have indom: "x ∈ env_dom (env+e')" by simp
  from 
    ‹ok env› ‹x ∈ env_dom env› ‹the env!x = T› ‹env_dom env ∩ env_dom e' = {}›
    ‹ok e'› 
  have "the (env+e')!x = T" by simp
  from 
    typing.T_Var[OF env_app_ok[OF ‹ok env› ‹env_dom env ∩ env_dom e' = {}› 
                                  ‹ok e'›] 
                    indom this] 
  show ?case by assumption
next
  case (T_Upd F env T l t2 t1)
  from 
    typing.T_Upd[OF _ bnd_disj_env_lem[OF typing_regular'[OF ‹env ⊢ t1 : T›] 
                                          ‹env_dom env ∩ env_dom e' = {}› ‹ok e'› 
                                          T_Upd(2)] 
                    T_Upd(4)[OF ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›] 
                    ‹l ∈ do T›]
    ‹finite F› ok_finite[OF env_app_ok[OF typing_regular'[OF ‹env ⊢ t1 : T›] 
                                          ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›]]
  show ?case by simp
next
  case (T_Obj env f T F)
  from 
    ok_finite[OF env_app_ok[OF ‹ok env› ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›]]
    ‹finite F› 
  have finF: "finite (F ∪ env_dom (env+e'))" by simp
  note 
    ball_Tltsp[of F
    "λT l t s p. env⦇s:T⦈⦇p:param(the(T^l))⦈ ⊢ (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l))
               ∧ (env_dom (env⦇s:T⦈⦇p:param(the(T^l))⦈) ∩ env_dom e' = {} 
                  ⟶ ok e' 
                  ⟶ env⦇s:T⦈⦇p:param(the(T^l))⦈+e' 
                      ⊢ (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))"
    T "F ∪ env_dom (env+e')"
    "λT l t s p. (env+e')⦇s:T⦈⦇p:param(the(T^l))⦈ 
                 ⊢ (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"]
  from 
    this[OF _ T_Obj(4)] 
    bnd_disj_env_lem[OF ‹ok env› ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›] 
    typing.T_Obj[OF env_app_ok[OF ‹ok env› 
                    ‹env_dom env ∩ env_dom e' = {}› ‹ok e'›] 
                    ‹dom f = do T› finF]
  show ?case by simp
qed

text ‹Typed in the Empty Environment implies typed in any Environment›
lemma empty_env: 
  assumes "(Env Map.empty) ⊢ t : A" and "ok env"
  shows "env ⊢ t : A"
proof -
  from ‹ok env› have "env = (Env Map.empty)+env" by (cases env, auto)
  with disjunct_env[OF assms(1) _ assms(2)] show ?thesis by simp
qed

lemma bnd_open_lem:
  assumes
  pred_bnd:
  "∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa 
    ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ 
        ⊢ (t⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l)) 
     ∧ (∀env'' t'' s' p' x' y' A' B' n'. s' ∉ FV t'' ∪ FV x' ∪ FV y' 
         ⟶ p' ∉ FV t'' ∪ FV x' ∪ FV y' ⟶ s' ≠ p' 
         ⟶ env'' ⊢ x' : A' ⟶ env'' ⊢ y' : B' 
         ⟶ (t⇗[Fvar sa,Fvar pa]⇖) = {n' → [Fvar s',Fvar p']} t'' 
         ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env''⦇s':A'⦈⦇p':B'⦈ 
         ⟶ env'' ⊢ {n' → [x',y']} t'' : return(the(T^l)))" and
  "ok env" and "env = env'⦇s:A⦈⦇p:B⦈" and 
  "s ∉ FV t'' ∪ FV x ∪ FV y" and "p ∉ FV t'' ∪ FV x ∪ FV y" and "s ≠ p" and 
  "env' ⊢ x : A" and "env' ⊢ y : B" and 
  "t = {Suc n → [Fvar s,Fvar p]} t'" and "FV t' ⊆ FV t''"
  shows 
  "∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env' 
         ∧ pa ∉ F ∪ {s,p} ∪ env_dom env' ∧ sa ≠ pa
    ⟶ env'⦇sa:T⦈⦇pa:param(the(T^l))⦈
        ⊢ ({Suc n → [x,y]} t'⇗[Fvar sa, Fvar pa]⇖) : return(the(T^l))"
proof (intro strip, elim conjE)
  fix sa pa assume 
    nin_sa: "sa ∉ F ∪ {s,p} ∪ env_dom env'" and 
    nin_pa: "pa ∉ F ∪ {s,p} ∪ env_dom env'" and "sa ≠ pa"
  hence "sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa" by auto
  moreover
  {
    fix a assume "a ∉ FV t'' ∪ FV x ∪ FV y" and "a ∈ {s,p}"
    with 
      ‹FV t' ⊆ FV t''› nin_sa nin_pa ‹sa ≠ pa› 
      sopen_FV[of 0 "Fvar sa" "Fvar pa" t']
    have "a ∉ FV (t'⇗[Fvar sa,Fvar pa]⇖) ∪ FV x ∪ FV y" by (auto simp: openz_def)
  } note 
      this[OF ‹s ∉ FV t'' ∪ FV x ∪ FV y›] 
      this[OF ‹p ∉ FV t'' ∪ FV x ∪ FV y›]
  moreover
  {
    from ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ok_add_2[of env' s A p B]
    have "ok env'" by simp
    from nin_sa nin_pa ‹sa ≠ pa› env_add_dom[OF this] 
    obtain "sa ∉ env_dom env'" and "pa ∉ env_dom (env'⦇sa:T⦈)" by auto
    note 
      bigger_env_lemma[OF bigger_env_lemma[OF ‹env' ⊢ x : A› this(1)] this(2)]
      bigger_env_lemma[OF bigger_env_lemma[OF ‹env' ⊢ y : B› this(1)] this(2)]
  }note 
      this(1)[of "param(the(T^l))"] 
      this(2)[of "param(the(T^l))"]
  moreover
  from ‹t = {Suc n → [Fvar s,Fvar p]} t'› sopen_commute[of 0 "Suc n" sa pa s p t']
  have "(t⇗[Fvar sa,Fvar pa]⇖) = {Suc n → [Fvar s,Fvar p]} (t'⇗[Fvar sa,Fvar pa]⇖)"
    by (simp add: openz_def)
  moreover
  from 
    subst_add[of p sa "env'⦇s:A⦈" B T] subst_add[of s sa env' A T]
    subst_add[of p pa "env'⦇sa:T⦈⦇s:A⦈" B "param(the(T^l))"] 
    subst_add[of s pa "env'⦇sa:T⦈" A "param(the(T^l))"]
    ‹env = env'⦇s:A⦈⦇p:B⦈› nin_sa nin_pa
  have "env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env'⦇sa:T⦈⦇pa:param(the(T^l))⦈⦇s:A⦈⦇p:B⦈"
    by auto
  ultimately
  show 
    "env'⦇sa:T⦈⦇pa:param(the(T^l))⦈
     ⊢ ({Suc n → [x,y]} t'⇗[Fvar sa, Fvar pa]⇖) : return(the(T^l))"
    using 
      pred_bnd ‹s ≠ p›
      sopen_commute_gen[OF lc_Fvar[of sa] lc_Fvar[of pa] 
                           typing_regular''[OF ‹env' ⊢ x : A›] 
                           typing_regular''[OF ‹env' ⊢ y : B›]
                           not_sym[OF Suc_not_Zero]]
    by (auto simp: openz_def)
qed

(* A variation of the Type Renaming lemma above. This is stronger and could be extended to show type renaming, using that a term typed in one environment is typed in any bigger environment *)
(* TODO: refactor to work with typing_induct *)
lemma open_lemma':
  shows 
  "e ⊢ t : C 
  ⟹ (⋀env t' s p x y A B n. s ∉ FV t' ∪ FV x ∪ FV y 
         ⟹ p ∉ FV t' ∪ FV x ∪ FV y ⟹ s ≠ p
         ⟹ env ⊢ x : A ⟹ env ⊢ y : B 
         ⟹ t = {n → [Fvar s,Fvar p]} t'
         ⟹ e = env⦇s:A⦈⦇p:B⦈
         ⟹ env ⊢ {n → [x,y]} t' : C)"
proof (induct set:typing)
  case (T_Var env x T env' t' s p y z A B n)
  from sopen_eq_Fvar[OF sym[OF ‹Fvar x = {n → [Fvar s,Fvar p]} t'›]] 
  show ?case
  proof (elim disjE conjE)
    assume "t' = Fvar x" 
    with ‹s ∉ FV t' ∪ FV y ∪ FV z› ‹p ∉ FV t' ∪ FV y ∪ FV z› 
    obtain "x ≠ s" and "x ≠ p" by auto
    from ‹x ∈ env_dom env› ‹env = env'⦇s:A⦈⦇p:B⦈› in_env_smaller2[OF _ this]
    have indom: "x ∈ env_dom env'" by simp
    from 
      ‹ok env› ‹the env!x = T› ‹env = env'⦇s:A⦈⦇p:B⦈›
      ok_add_2[of env' s A p B] get_env_smaller2[OF this _ _ ‹s ≠ p›]
    have "the env'!x = T" by simp
    from 
      ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› ‹t' = Fvar x›
      ok_add_2[of env' s A p B] typing.T_Var[OF _ indom this]
    show ?case by simp
  next
    assume "x = s"
    with 
      ‹ok env› ‹the env!x = T› ‹env = env'⦇s:A⦈⦇p:B⦈› 
      add_get2_1[of env' s A p B] 
    have "T = A" by simp
    moreover assume "t' = Bvar (Self n)"
    ultimately show ?thesis using ‹env' ⊢ y : A› by simp
  next
    assume "x = p" 
    with 
      ‹ok env› ‹the env!x = T› ‹env = env'⦇s:A⦈⦇p:B⦈› 
      add_get2_2[of env' s A p B] have "T = B" by simp
    moreover assume "t' = Bvar (Param n)"
    ultimately show ?thesis using ‹env' ⊢ z : B› by simp
  qed
next
  case (T_Upd F env T l t2 t1 env' t' s p x y A B n)
  from sopen_eq_Upd[OF sym[OF ‹Upd t1 l t2 = {n → [Fvar s,Fvar p]} t'›]]
  obtain t1' t2' where 
    t1': "t1 = {n → [Fvar s,Fvar p]} t1'" and
    t2': "t2 = {Suc n → [Fvar s,Fvar p]} t2'" and
    t': "t' = Upd t1' l t2'" by auto
  hence "FV t2' ⊆ FV t'" by auto
  from 
    ‹s ∉ FV t' ∪ FV x ∪ FV y› ‹p ∉ FV t' ∪ FV x ∪ FV y›
    t' ‹finite F› ok_finite[OF typing_regular'[OF ‹env' ⊢ x : A›]]
    typing.T_Upd[OF _ bnd_open_lem[OF T_Upd(2) 
                    typing_regular'[OF ‹env ⊢ t1 : T›] 
                    ‹env = env'⦇s:A⦈⦇p:B⦈› 
                    ‹s ∉ FV t' ∪ FV x ∪ FV y› 
                    ‹p ∉ FV t' ∪ FV x ∪ FV y› ‹s ≠ p›
                    ‹env' ⊢ x : A› ‹env' ⊢ y : B› t2' this]
    T_Upd(4)[OF _ _ ‹s ≠ p› ‹env' ⊢ x : A› ‹env' ⊢ y : B› 
                t1' ‹env = env'⦇s:A⦈⦇p:B⦈›] ‹l ∈ do T›]
  show ?case by simp
next
  case (T_Obj env f T F env' t' s p x y A B n)
  from sopen_eq_Obj[OF sym[OF ‹Obj f T = {n → [Fvar s,Fvar p]} t'›]]
  obtain f' where 
    obj: "Obj f T = {n → [Fvar s,Fvar p]} Obj f' T" and 
    t': "t' = Obj f' T" by auto
  from 
    sym[OF this(1)] ‹dom f = do T›
    sym[OF dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']]
    dom_sopenoption_lem[of "Suc n" x y f']
  have dom: "dom (λl. sopen_option (Suc n) x y (f' l)) = do T" by simp

  from ‹finite F› ok_finite[OF typing_regular'[OF ‹env' ⊢ x : A›]] 
  have finF: "finite (F ∪ {s,p} ∪ env_dom env')"
    by simp

  have
    "∀l∈do T. ∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env' 
                     ∧ pa ∉ F ∪ {s,p} ∪ env_dom env' 
                     ∧ sa ≠ pa 
      ⟶ env'⦇sa:T⦈⦇pa:param(the(T^l))⦈
          ⊢ (the(sopen_option (Suc n) x y (f' l))⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
  proof 
    fix l assume "l ∈ do T" with T_Obj(4)
    have 
      cof: 
      "∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
        ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ 
            ⊢ (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
          ∧ (∀env'' t'' s' p' x' y' A' B' n'.
               s' ∉ FV t'' ∪ FV x' ∪ FV y' ⟶ p' ∉ FV t'' ∪ FV x' ∪ FV y' 
               ⟶ s' ≠ p' ⟶ env'' ⊢ x' : A' ⟶ env'' ⊢ y' : B'
               ⟶ (the(f l)⇗[Fvar sa,Fvar pa]⇖) = {n' → [Fvar s',Fvar p']} t''
               ⟶ env⦇sa:T⦈⦇pa:param(the(T^l))⦈ = env''⦇s':A'⦈⦇p':B'⦈ 
               ⟶ env'' ⊢ {n' → [x',y']} t'' : return(the(T^l)))"
      by simp
    from 
      ‹l ∈ do T› ‹dom f = do T› ‹Obj f T = {n → [Fvar s,Fvar p]} t'› obj t'
      dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']
    have indomf': "l ∈ dom f'" by auto
    with obj sopen_option_lem[of f' "Suc n" "Fvar s" "Fvar p"] FV_option_lem[of f'] t'
    obtain 
      "the(f l) = {Suc n → [Fvar s,Fvar p]} the(f' l)" and
      "FV (the(f' l)) ⊆ FV t'" by auto
    from 
      bnd_open_lem[OF cof ‹ok env› ‹env = env'⦇s:A⦈⦇p:B⦈› 
                      ‹s ∉ FV t' ∪ FV x ∪ FV y› ‹p ∉ FV t' ∪ FV x ∪ FV y›
                      ‹s ≠ p› ‹env' ⊢ x : A› ‹env' ⊢ y : B› this]
      indomf' sopen_option_lem[of f' "Suc n" x y] T_Obj(4)
    show 
      "∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env' 
             ∧ pa ∉ F ∪ {s,p} ∪ env_dom env' ∧ sa ≠ pa 
        ⟶ env'⦇sa:T⦈⦇pa:param(the(T^l))⦈
            ⊢ (the(sopen_option (Suc n) x y (f' l))⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
      by simp
  qed
  from typing.T_Obj[OF typing_regular'[OF ‹env' ⊢ x : A›] dom finF this] t' 
  show ?case by simp
next
  case (T_Call env t1 T t2 l env' t' s p x y A B n)
  from sopen_eq_Call[OF sym[OF ‹Call t1 l t2 = {n → [Fvar s,Fvar p]} t'›]]
  obtain t1' t2' where 
    t1: "t1 = {n → [Fvar s,Fvar p]} t1'" and
    t2: "t2 = {n → [Fvar s,Fvar p]} t2'" and
    t': "t' = Call t1' l t2'" by auto
  { fix a assume "a ∉ FV t' ∪ FV x ∪ FV y" 
    with t' have "a ∉ FV t1' ∪ FV x ∪ FV y" by simp
  }note 
      t1' = T_Call(2)[OF this[OF ‹s ∉ FV t' ∪ FV x ∪ FV y›]
                        this[OF ‹p ∉ FV t' ∪ FV x ∪ FV y›]
                        ‹s ≠ p› ‹env' ⊢ x : A› ‹env' ⊢ y : B›
                        t1 ‹env = env'⦇s:A⦈⦇p:B⦈›]
  { fix a assume "a ∉ FV t' ∪ FV x ∪ FV y" 
    with t' have "a ∉ FV t2' ∪ FV x ∪ FV y" by simp
  }
  from 
    typing.T_Call[OF t1' T_Call(4)[OF this[OF ‹s ∉ FV t' ∪ FV x ∪ FV y›]
                                     this[OF ‹p ∉ FV t' ∪ FV x ∪ FV y›]
                                     ‹s ≠ p› ‹env' ⊢ x : A› ‹env' ⊢ y : B›
                                     t2 ‹env = env'⦇s:A⦈⦇p:B⦈›] 
                     ‹l ∈ do T›]
    t'
  show ?case by simp
qed

lemma open_lemma: 
  "⟦ env⦇s:A⦈⦇p:B⦈ ⊢ {n → [Fvar s,Fvar p]} t : T; 
     s ∉ FV t ∪ FV x ∪ FV y;  p ∉ FV t ∪ FV x ∪ FV y; s ≠ p; 
     env ⊢ x : A; env ⊢ y : B ⟧ 
  ⟹ env ⊢ {n → [x,y]} t : T"  
  by (simp add: open_lemma')

subsubsection ‹Subject reduction›
lemma type_dom[simp]: "env ⊢ (Obj a A) : A ⟹ dom a = do A" 
  by (erule typing.cases, auto)

lemma select_preserve_type[simp]:
  assumes 
  "env ⊢ Obj f (Object t) : Object t" and "s ∉ FV a" and "p ∉ FV a" and
  "env⦇s:(Object t)⦈⦇p:param(the(t l2))⦈ ⊢ (a⇗[Fvar s,Fvar p]⇖) : return(the(t l2))" and
  "l1 ∈ dom t" and "l2 ∈ dom t"
  shows 
  "∃F. finite F 
     ∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
         ⟶ env⦇s:(Object t)⦈⦇p:param(the(t l1))⦈
             ⊢ (the((f(l2 ↦ a)) l1)⇗[Fvar s,Fvar p]⇖) : return(the(t l1)))"
proof -
  from ok_finite[OF typing_regular'[OF ‹env ⊢ Obj f (Object t) : Object t›]]
  have finF: "finite ({s,p} ∪ env_dom env)" by simp

  { 
    note 
      ok_env = typing_regular'[OF ‹env ⊢ Obj f (Object t) : Object t›] and
      ok_env_sp = typing_regular'[OF assms(4)]
    fix sa pa assume 
      nin_sa: "sa ∉ {s,p} ∪ env_dom env" and
      nin_pa: "pa ∉ {s,p} ∪ env_dom env" and "sa ≠ pa"
    from this(1) ok_add_2[OF ok_env_sp] env_add_dom_2[OF ok_env]
    have "sa ∉ env_dom (env⦇s:Object t⦈⦇p:param(the(t l2))⦈)" by simp
    from 
      nin_sa bigger_env_lemma[OF assms(4) this]
      subst_add[of sa p "env⦇s:Object t⦈" "Object t" "param(the(t l2))"]
      subst_add[of sa s env "Object t" "Object t"]
    have 
      aT_sa: "env⦇sa:Object t⦈⦇s:Object t⦈⦇p:param(the(t l2))⦈
              ⊢ (a⇗[Fvar s,Fvar p]⇖) : return(the(t l2))" by simp
    from 
      ‹sa ≠ pa› nin_sa nin_pa env_add_dom[OF ok_env] 
      ok_add_2[OF ok_env_sp]
    obtain 
      "s ∉ env_dom (env⦇sa:Object t⦈)" and
      "p ∉ env_dom (env⦇sa:Object t⦈)" and "s ≠ p" and 
      "sa ∉ env_dom env" and "pa ∉ env_dom (env⦇sa:Object t⦈)" 
      by auto
    with env_add_dom_2[OF ok_add_ok[OF ok_env this(4)] this(1-3)] nin_pa
    have "pa ∉ env_dom (env⦇sa:Object t⦈⦇s:Object t⦈⦇p:param(the(t l2))⦈)"
      by simp
    from 
      nin_pa bigger_env_lemma[OF aT_sa this]
      subst_add[of pa p "env⦇sa:Object t⦈⦇s:Object t⦈" 
                   "param(the(t l2))" "param(the(t l2))"]
      subst_add[of pa s "env⦇sa:Object t⦈" "param(the(t l2))" "Object t"]
    have 
      aT_sapa: 
      "env⦇sa:Object t⦈⦇pa:param(the(t l2))⦈⦇s:Object t⦈⦇p:param(the(t l2))⦈
      ⊢ {0 → [Fvar s, Fvar p]} a : return(the(t l2))" by (simp add: openz_def)
    from nin_sa nin_pa ‹s ∉ FV a› ‹p ∉ FV a› ok_add_2[OF ok_env_sp] 
    obtain 
      ninFV_s: "s ∉ FV a ∪ FV (Fvar sa) ∪ FV (Fvar pa)" and
      ninFV_p: "p ∉ FV a ∪ FV (Fvar sa) ∪ FV (Fvar pa)" and "s ≠ p"
      by auto
    from ok_add_2[OF typing_regular'[OF aT_sapa]]
    have ok_env_sapa: "ok (env⦇sa:Object t⦈⦇pa:param(the(t l2))⦈)"
      by simp
    with ok_add_reverse[OF this]
    have ok_env_pasa: "ok (env⦇pa:param(the(t l2))⦈⦇sa:Object t⦈)"
      by simp

    from 
      open_lemma[OF aT_sapa ninFV_s ninFV_p ‹s ≠ p› _
                    T_Var[OF ok_env_sapa in_add[OF ok_env_sapa] 
                             add_get2_2[OF ok_env_sapa]]]
      T_Var[OF ok_env_pasa in_add[OF ok_env_pasa] add_get2_2[OF ok_env_pasa]]
      ok_add_reverse[OF ok_env_sapa]
    have 
      "env⦇sa:(Object t)⦈⦇pa:param(the(t l2))⦈ 
       ⊢ (a⇗[Fvar sa,Fvar pa]⇖) : return(the(t l2))"
      by (simp add: openz_def)
  }note alem = this

(* case split *)
  show ?thesis
  proof (cases "l1 = l2")
    case True with assms obj_inv_elim'[OF assms(1)] show ?thesis
      by (simp (no_asm_simp), rule_tac x = "{s,p} ∪ env_dom env" in exI,
          auto simp: finF alem)
  next
    case False
    from obj_inv_elim[OF ‹env ⊢ Obj f (Object t) : Object t›]
    obtain F where 
      "finite F" and
      "∀l∈dom t. 
        ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
         ⟶ env⦇s:Object t⦈⦇p:param(the(Object t^l))⦈
             ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(Object t^l))"
      by auto
    from this(2) ‹l1 ∈ dom t›
    have 
      "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
        ⟶ env⦇s:Object t⦈⦇p:param(the(Object t^l1))⦈
            ⊢ (the(f l1)⇗[Fvar s,Fvar p]⇖) : return(the(Object t^l1))"
      by auto
    thus ?thesis using ‹finite F› ‹l1 ≠ l2› by (simp,blast)
  qed
qed

text ‹Main Lemma›
(* TODO: refactor to work with typing_induct *)
lemma subject_reduction: "e ⊢ t : T ⟹ (⋀t'. t →⇩β t' ⟹ e ⊢ t' : T)"
proof (induct set: typing)
  case (T_Var env x T t') 
  from Fvar_beta[OF ‹Fvar x →⇩β t'›] show ?case by simp 
next
  case (T_Upd F env T l t2 t1 t')
  from Upd_beta[OF ‹Upd t1 l t2 →⇩β t'›] show ?case
  proof (elim disjE exE conjE)
    fix t1' assume "t1 →⇩β t1'" and "t' = Upd t1' l t2"
    from 
      this(2) T_Upd(2) 
      typing.T_Upd[OF ‹finite F› _ T_Upd(4)[OF this(1)] ‹l ∈ do T›]
    show ?case by simp
  next
    fix t2' F' 
    assume 
      "finite F'" and
      pred_F': "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p 
                 ⟶ (∃t''. t2⇗[Fvar s,Fvar p]⇖ →⇩β t'' ∧ t2' = σ[s,p] t'')"  and
      t': "t' = Upd t1 l t2'"
    have 
      "∀s p. s ∉ F ∪ F' ∧ p ∉ F ∪ F' ∧ s ≠ p
        ⟶ env⦇s:T⦈⦇p:param(the(T^l))⦈ ⊢ (t2'⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
    proof (intro strip, elim conjE)
      fix s p assume 
        nin_s: "s ∉ F ∪ F'" and
        nin_p: "p ∉ F ∪ F'" and "s ≠ p"
      with pred_F' obtain t'' where "t2⇗[Fvar s,Fvar p]⇖ →⇩β t''" and "t2' = σ[s,p] t''"
        by auto
      with beta_lc[OF this(1)] sopen_sclose_eq_t[of t'' 0 s p]
      have "t2⇗[Fvar s,Fvar p]⇖ →⇩β (t2'⇗[Fvar s,Fvar p]⇖)" 
        by (simp add: openz_def closez_def)
      with nin_s nin_p ‹s ≠ p› T_Upd(2) 
      show "env⦇s:T⦈⦇p:param(the(T^l))⦈ ⊢ (t2'⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
        by auto
    qed
    from t' ‹finite F› ‹finite F'› typing.T_Upd[OF _ this ‹env ⊢ t1 : T› ‹l ∈ do T›]
    show ?case by simp
  next
    fix f U assume 
      "l ∈ dom f" and "Obj f U = t1" and 
      t': "t' = Obj (f(l ↦ t2)) U"
    from this(1-2) ‹env ⊢ t1 : T› obj_inv[of env f U T]
    obtain t where 
      objT: "env ⊢ Obj f (Object t) : (Object t)" and 
      "Object t = T" and "T = U" 
      by (cases T, auto)
    from obj_inv_elim[OF objT] ‹Object t = T› ‹l ∈ dom f› 
    have domf': "dom (f(l ↦ t2)) = do T" by auto
    have 
      exF: "∀l'∈do T. 
             (∃F'. finite F' 
                 ∧ (∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p 
                     ⟶ env⦇s:T⦈⦇p:param(the(T^l'))⦈
                         ⊢ (the ((f(l ↦ t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))))"
    proof
      fix l' assume "l' ∈ do T"
      with dom_lem[OF objT] ‹l ∈ dom f› ‹Object t = T›
      obtain ll': "l' ∈ dom t" and "l ∈ dom t" by auto

      from ‹finite F› have "finite (F ∪ FV t2)" by simp
      from exFresh_s_p_cof[OF this]
      obtain s p where 
        nin_s: "s ∉ F ∪ FV t2" and 
        nin_p: "p ∉ F ∪ FV t2" and "s ≠ p"
        by auto
      with T_Upd(2) ‹Object t = T› 
      have 
        "env⦇s:Object t⦈⦇p:param(the(t l))⦈ 
         ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(t l))"
        by auto
      from 
        select_preserve_type[OF objT _ _ this ll'] sym[OF ‹Object t = T›]
        nin_s nin_p ‹l ∈ dom t›
      obtain F' where 
        "finite F'" and
        "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p
          ⟶ env⦇s:T⦈⦇p:param(the(T^l'))⦈
              ⊢ (the ((f(l ↦ t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
        by auto
      thus 
        "∃F'. finite F' 
            ∧ (∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p
                ⟶ env⦇s:T⦈⦇p:param(the(T^l'))⦈
                    ⊢ (the ((f(l ↦ t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l')))"
        by blast
    qed
    { fix Ta from finite_dom_fmap have "finite (do Ta)" by (cases Ta, auto) }
    note fin_doT = this ball_ex_finite[of "do T" "F ∪ FV t2"]
    from this(2)[OF this(1)[of T] _ exF] ‹finite F›
    obtain F' where 
      "finite F'" and
      "∀l'∈do T. ∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p
                   ⟶ env⦇s:T⦈⦇p:param(the(T^l'))⦈
                       ⊢ (the ((f(l ↦ t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
      by auto
    moreover
    from ‹finite F'› ‹finite F› have "finite (F' ∪ (F ∪ FV t2))" by simp
    note typing.T_Obj[OF typing_regular'[OF ‹env ⊢ t1 : T›] domf' this]
    ultimately show ?case using t' ‹T = U› by auto
  qed
next
  case (T_Obj env f T F t')
  from Obj_beta[OF ‹Obj f T →⇩β t'›] show ?case
  proof (elim exE conjE)
    fix l f' a a' F' assume 
      "dom f = dom f'" and "f = f'(l ↦ a)" and "l ∈ dom f'" and
      t': "t' = Obj (f'(l ↦ a')) T" and "finite F'" and
      red_sp: "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p 
                ⟶ (∃t''. a⇗[Fvar s, Fvar p]⇖ →⇩β t'' ∧ a' = σ[s,p] t'')"
    from this(2) ‹dom f = do T› have domf': "dom (f'(l ↦ a')) = do T" by auto
    have 
      exF: "∀l'∈do T. ∀s p. s ∉ F ∪ F' ∧ p ∉ F ∪ F' ∧ s ≠ p 
             ⟶ env⦇s:T⦈⦇p:param(the(T^l'))⦈
                 ⊢ (the ((f'(l ↦ a')) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
    proof (intro strip, elim conjE)
      fix l' s p assume 
        "l' ∈ do T" and 
        nin_s: "s ∉ F ∪ F'" and
        nin_p: "p ∉ F ∪ F'" and "s ≠ p"
      with red_sp obtain t'' where "a⇗[Fvar s,Fvar p]⇖ →⇩β t''" and "a' = σ[s,p] t''" 
        by auto
      with 
        beta_lc[OF this(1)] sopen_sclose_eq_t[of t'' 0 s p] 
        ‹f = f'(l ↦ a)›
      have "the (f l)⇗[Fvar s,Fvar p]⇖ →⇩β (the((f'(l ↦ a')) l)⇗[Fvar s,Fvar p]⇖)" 
        by (simp add: openz_def closez_def)
      with T_Obj(4) nin_s nin_p ‹s ≠ p› ‹l' ∈ do T› ‹f = f'(l ↦ a)›
      show 
        "env⦇s:T⦈⦇p:param(the(T^l'))⦈
         ⊢ (the((f'(l ↦ a')) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
        by auto
    qed
    from typing.T_Obj[OF ‹ok env› domf' _ this] ‹finite F› ‹finite F'› t'
    show ?case by (simp (no_asm_simp))
  qed
next
  case (T_Call env t1 T t2 l t')
  from Call_beta[OF ‹Call t1 l t2 →⇩β t'›] show ?case
  proof (elim disjE conjE exE)
    fix t1' assume "t1 →⇩β t1'" and "t' = Call t1' l t2"
    from 
      typing.T_Call[OF T_Call(2)[OF this(1)] 
                       ‹env ⊢ t2 : param(the(T^l))› ‹l ∈ do T›]
      this(2)
    show ?case by simp
  next
    fix t2' assume "t2 →⇩β t2'" and "t' = Call t1 l t2'"
    from 
      typing.T_Call[OF ‹env ⊢ t1 : T› T_Call(4)[OF this(1)] ‹l ∈ do T›]
      this(2) 
    show ?case by simp
  next
    fix f U assume "Obj f U = t1" and "l ∈ dom f" and t': "t' = (the(f l)⇗[Obj f U,t2]⇖)"
    from 
      typing.T_Call[OF ‹env ⊢ t1 : T› ‹env ⊢ t2 : param(the(T^l))› ‹l ∈ do T›]
      sym[OF this(1)] ‹env ⊢ t1 : T› ‹env ⊢ t2 : param(the(T^l))› 
      obj_inv[of env f U T]
    obtain 
      objT: "env ⊢ (Obj f T) : T" and "T = U" and
      callT: "env ⊢ Call (Obj f T) l t2 : return(the(T^l))" 
      by auto
    have 
      "(∃F. finite F 
          ∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p 
              ⟶ env⦇s:T⦈⦇p:param(the(T^l))⦈ 
                  ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))
      ⟹ env ⊢ (the (f l)⇗[Obj f T,t2]⇖) : return (the(T^l)))"
    proof (elim exE conjE)
      fix F 
      assume 
        "finite F" and
        pred_F:
        "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
          ⟶ env⦇s:T⦈⦇p:param(the(T^l))⦈ 
              ⊢ (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
      from this(1) finite_FV[of "Obj f T"]
      have "finite (F ∪ FV (Obj f T) ∪ FV t2)" by simp
      from exFresh_s_p_cof[OF this]
      obtain s p where 
        nin_s: "s ∉ F ∪ FV (Obj f T) ∪ FV t2" and
        nin_p: "p ∉ F ∪ FV (Obj f T) ∪ FV t2" and "s ≠ p" 
        by auto
      with pred_F
      have 
        type_opened: "env⦇s:T⦈⦇p:param(the(T^l))⦈
                      ⊢ {0 → [Fvar s,Fvar p]} the(f l) : return(the(T^l))"
        by (auto simp: openz_def)
      from nin_s nin_p FV_option_lem[of f] objT ‹l ∈ do T›
      obtain 
        "s ∉ FV (the(f l)) ∪ FV (Obj f T) ∪ FV t2" and
        "p ∉ FV (the(f l)) ∪ FV (Obj f T) ∪ FV t2" by auto
      from 
        open_lemma[OF type_opened this ‹s ≠ p› 
        objT ‹env ⊢ t2 : param(the(T^l))›]
      show ?thesis by (simp add: openz_def)
    qed
    with abs_typeE[OF callT] t' ‹T = U› show ?case by auto
  qed
qed

theorem subject_reduction': "t →⇩β⇧* t' ⟹ e ⊢ t : T ⟹ e ⊢ t' : T"
  by (induct set: rtranclp) (iprover intro: subject_reduction)+

lemma type_members_equal: 
  fixes A :: type and B :: type
  assumes "do A = do B" and "∀i. (A^i) = (B^i)"
  shows "A = B"
proof (cases A)
  case (Object ta) thus ?thesis
  proof (cases B)
    case (Object tb)
    from ‹∀i. (A^i) = (B^i)› ‹A = Object ta› ‹B = Object tb› 
    have "⋀i. ta i = tb i" by auto
    with ‹A = Object ta› ‹B = Object tb› show ?thesis by (simp add: ext)
  qed
qed

lemma not_var: "Env Map.empty ⊢ a : A ⟹ ∀x. a ≠ Fvar x"
  by (rule allI, case_tac x, auto)

lemma Call_label_range: "(Env Map.empty) ⊢ Call (Obj c T) l b : A ⟹ l ∈ dom c"
  by (erule typing_elims, erule typing.cases, simp_all)

lemma  Call_subterm_type: "Env Map.empty ⊢ Call t l b: T 
  ⟹ (∃T'. Env Map.empty ⊢ t : T') ∧  (∃T'. Env Map.empty ⊢ b : T')"
  by (erule typing.cases) auto

lemma Upd_label_range: "Env Map.empty ⊢ Upd (Obj c T) l x : A ⟹ l ∈ dom c"
  by (erule typing_elims, erule typing.cases, simp_all)

lemma Upd_subterm_type: 
  "Env Map.empty ⊢ Upd t l x : T ⟹ ∃T'. Env Map.empty ⊢ t : T'" 
  by (erule typing.cases) auto

lemma no_var: "∃T. Env Map.empty ⊢ Fvar x : T ⟹ False"
  by (case_tac x, auto)

lemma no_bvar: "e ⊢ Bvar x : T ⟹ False" 
  by (erule typing.cases, auto)

subsubsection‹Unique Type›
theorem type_unique[rule_format]: 
  assumes "env ⊢ a: T"
  shows "∀T'. env ⊢ a: T' ⟶ T = T'"
  using assms
proof (induct rule: typing.induct)
  case T_Var thus ?case by (auto simp: add_get_eq)
next
  case T_Obj show ?case by (auto simp: sym[OF obj_inv])
next
  case T_Call from this(2) show ?case by auto
next 
  case T_Upd from this(4) show ?case by auto
qed

subsubsection‹Progress›
text ‹Final Type Soundness Lemma›
theorem progress: 
  assumes "Env Map.empty ⊢ t : A" and "¬(∃c A. t = Obj c A)"
  shows "∃b. t →⇩β b"
proof -
  fix f
  have 
    "(∀A. Env Map.empty ⊢ t : A ⟶ ¬(∃c T. t = Obj c T) ⟶ (∃b. t →⇩β b))
    &(∀A. Env Map.empty ⊢ Obj f A : A ⟶ ¬(∃c T. Obj f A = Obj c T) 
       ⟶ (∃b. Obj f A →⇩β b))"
  proof (induct rule: sterm_induct)
    case (Bvar b) with no_bvar[of "Env Map.empty" b] show ?case 
      by auto (* contradiction *)
  next
    case (Fvar x) with Fvar_beta[of x] show ?case
      by auto (* contradiction *)
  next
    case Obj show ?case by auto (* contradiction *)
  next
    case empty thus ?case by auto (* contradiction *)
  next
    case insert show ?case by auto (* contradiction *)
  next
    case (Call t1 l t2) show ?case
    proof (clarify)
      fix T assume 
        "Env Map.empty ⊢ t1 : T" and "Env Map.empty ⊢ t2 : param(the(T^l))" and "l ∈ do T"
      note lc = typing_regular''[OF this(1)] typing_regular''[OF this(2)]
      from 
        ‹Env Map.empty ⊢ t1 : T› 
        ‹∀A. Env Map.empty ⊢ t1 : A ⟶ ¬ (∃c T. t1 = Obj c T) ⟶ (∃b. t1 →⇩β b)›
      have "(∃c B. t1 = Obj c B) ∨ (∃b. t1 →⇩β b)" by auto
      thus "∃b. Call t1 l t2 →⇩β b"
      proof (elim disjE exE)
        fix c B assume "t1 = Obj c B" 
        with 
          ‹Env Map.empty ⊢ t1 : T› obj_inv[of "Env Map.empty" c B T] 
          ‹l ∈ do T› obj_inv_elim[of "Env Map.empty" c B]
        have "l ∈ dom c" by auto
        with ‹t1 = Obj c B› lc beta.beta[of l c B t2]
        show ?thesis by auto
      next
        fix b assume "t1 →⇩β b"
        from beta.beta_CallL[OF this lc(2)] show ?thesis by auto
      qed
    qed
  next
    case (Upd t1 l t2) show ?case
    proof (clarify)
      fix T F
      assume 
        "finite F" and
        "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
          ⟶ Env Map.empty⦇s:T⦈⦇p:param(the(T^l))⦈ 
              ⊢ (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))" and
        "Env Map.empty ⊢ t1 : T" and
        "l ∈ do T"
      from typing_regular''[OF T_Upd[OF this]] lc_upd[of t1 l t2]
      obtain "lc t1" and "body t2" by auto
      from 
        ‹Env Map.empty ⊢ t1 : T› 
        ‹∀A. Env Map.empty ⊢ t1 : A ⟶ ¬ (∃c T. t1 = Obj c T) ⟶ (∃b. t1 →⇩β b)›
      have "(∃c B. t1 = Obj c B) ∨ (∃b. t1 →⇩β b)" by auto
      thus "∃b. Upd t1 l t2 →⇩β b"
      proof (elim disjE exE)
        fix c B assume "t1 = Obj c B" 
        with 
          ‹Env Map.empty ⊢ t1 : T› obj_inv[of "Env Map.empty" c B T] 
          ‹l ∈ do T› obj_inv_elim[of "Env Map.empty" c B]
        have "l ∈ dom c" by auto
        with ‹t1 = Obj c B› ‹lc t1› ‹body t2› beta.beta_Upd[of l c B t2]
        show ?thesis by auto
      next
        fix b assume "t1 →⇩β b"
        from beta.beta_UpdL[OF this ‹body t2›] show ?thesis by auto
      qed
    qed
  qed
  with assms show ?thesis by auto
qed

end