Theory Sigma

section ‹Locally Nameless representation of basic Sigma calculus enriched with formal parameter›

theory Sigma
imports "../preliminary/FMap"
begin

subsection ‹Infrastructure for the finite maps›

axiomatization max_label :: nat where
  LabelAvail: "max_label > 10"

definition "Label = {n :: nat. n ≤ max_label}"

typedef Label = Label
  unfolding Label_def by auto

lemmas finite_Label_set = Finite_Set.finite_Collect_le_nat[of max_label]

lemma Univ_abs_label: 
  "(UNIV :: (Label set)) = Abs_Label ` {n :: nat. n ≤ max_label}"
proof -
  have "∀x :: Label. x : Abs_Label ` {n :: nat. n ≤ max_label}"
  proof
    fix x :: Label
    have "Rep_Label x ∈ {n. n ≤ max_label}"
      by (fold Label_def, rule Rep_Label)
    hence "Abs_Label (Rep_Label x) ∈ Abs_Label ` {n. n ≤ max_label}"
      by (rule imageI)
    thus "x ∈ Abs_Label ` {n. n ≤ max_label}"
      by (simp add: Rep_Label_inverse)
  qed
  thus ?thesis by force
qed

lemma finite_Label: "finite (UNIV :: (Label set))"
  by (simp add: Univ_abs_label finite_Label_set)

instance Label :: finite
proof
  show "finite (UNIV :: (Label set))" by (rule finite_Label)
qed

consts
Lsuc :: "(Label set) ⇒ Label ⇒ Label"
Lmin :: "(Label set) ⇒ Label"
Lmax :: "(Label set) ⇒ Label"

definition Llt :: "[Label, Label] ⇒ bool" (infixl ‹<› 50) where
  "Llt a b == Rep_Label a < Rep_Label b"
definition Lle :: "[Label, Label] ⇒ bool" (infixl ‹≤› 50) where
  "Lle a b == Rep_Label a ≤ Rep_Label b"

definition Ltake_eq :: "[Label set, (Label ⇀ 'a),  (Label ⇀ 'a)] ⇒ bool"
where  "Ltake_eq L f g  == ∀l∈L. f l = g l"

lemma Ltake_eq_all:
  fixes f g
  assumes "dom f = dom g" and "Ltake_eq (dom f) f g"
  shows "f = g"
proof
  fix x from assms show "f x = g x" 
    unfolding Ltake_eq_def
    by (cases "x ∈ dom f", auto)
qed

lemma Ltake_eq_dom: 
  fixes L :: "Label set" and f :: "Label -~> 'a"
  assumes "L ⊆ dom f" and "card L = card (dom f)"
  shows "L = (dom f)"
proof (auto)
  fix x :: Label assume "x ∈ L"
  with in_mono[OF assms(1)] show "∃y. f x = Some y" by blast
next
  fix x y assume "f x = Some y"
  from card_seteq[OF finite_dom_fmap[of f] ‹L ⊆ dom f›] ‹card L = card (dom f)›
  have "L = dom f" by simp
  with ‹f x = Some y› show "x ∈ L" by force
qed

subsection ‹Object-terms in Locally Nameless representation notation, beta-reduction and substitution›

datatype type = Object "Label -~> (type × type)"

datatype bVariable = Self nat | Param nat
type_synonym fVariable = string
(* each binder introduces 2 variables: self and parameter *)
(* thus to each deBruijn index (nat) correspond 2 variables of the same depth *)

subsubsection ‹Enriched Sigma datatype of objects›
datatype sterm =
  Bvar bVariable             (* bound variable -- as deBruijn index *)
| Fvar fVariable             (* free variable *)
| Obj "Label -~> sterm" type (* An object maps labels to terms and has a type *)
| Call sterm Label sterm     (* Call a l b calls method l on object a with param b *)
| Upd sterm Label sterm      (* Upd a l b updates method l of object a with body b *)

datatype_compat sterm

primrec applyPropOnOption:: "(sterm ⇒ bool) ⇒ sterm option ⇒ bool" where
f1:  "applyPropOnOption P None  = True" |
f2:  "applyPropOnOption P (Some t) = P t"

lemma sterm_induct[case_names Bvar Fvar Obj Call Upd empty insert]:
  fixes 
  t :: sterm and P1 :: "sterm ⇒ bool" and 
  f :: "Label -~> sterm" and P3 :: "(Label -~> sterm) ⇒ bool"
  assumes 
  "⋀b. P1 (Bvar b)" and
  "⋀x. P1 (Fvar x)" and
   a_obj: "⋀f T. P3 f ⟹ P1 (Obj f T)" and
  "⋀t1 l t2. ⟦ P1 t1; P1 t2 ⟧ ⟹ P1 (Call t1 l t2)" and
  "⋀t1 l t2. ⟦ P1 t1; P1 t2 ⟧ ⟹ P1 (Upd t1 l t2)" and
  "P3 Map.empty" and
  a_f: "⋀t1 f l . ⟦ l ∉ dom f; P1 t1; P3 f ⟧ ⟹ (P3 (f(l ↦ t1)))"
  shows "P1 t ∧ P3 f"
proof -
  have "∀t (f::Label -~> sterm) l.  P1 t ∧ (applyPropOnOption P1) (f l)"
  proof (intro strip)
    fix t :: sterm and f' :: "Label -~> sterm" and l :: Label
    define foobar where "foobar = f' l" 
    from assms show "P1 t ∧ applyPropOnOption P1 foobar"
    proof (induct_tac t and foobar rule: compat_sterm.induct compat_sterm_option.induct, auto)
      fix f :: "Label -~> sterm" and T :: type
      assume "⋀x. applyPropOnOption P1 (f x)"
      with a_f ‹P3 Map.empty› have "P3 f"
      proof (induct f rule: fmap_induct, simp)
        case (insert F x z)
        note 
          P1F'   = ‹⋀xa. applyPropOnOption P1 ((F(x ↦ z)) xa)› and
          predP3 = ‹⟦ ⋀l f t1. ⟦l ∉ dom f; P1 t1; P3 f⟧ ⟹ P3 (f(l ↦ t1)); 
                      P3 Map.empty; ⋀x. applyPropOnOption P1 (F x)⟧
                    ⟹ P3 F› and
          P3F'   = ‹⋀l f t f. ⟦ l ∉ dom f; P1 t; P3 f ⟧ ⟹ P3 (f(l ↦ t))›
        have "⋀xa. applyPropOnOption P1 (F xa)"
        proof -
          fix xa :: Label show "applyPropOnOption P1 (F xa)"
          proof (cases "xa = x")
            case True with P1F' ‹x ∉ dom F› have "F xa = None" by force
            thus ?thesis by simp
          next
            case False hence eq: "F xa = (F(x ↦ z)) xa" by auto
            from P1F'[of xa] show "applyPropOnOption P1 (F xa)" 
              by (simp only: ssubst[OF eq])
          qed
        qed
        from a_f predP3[OF _ ‹P3 Map.empty› this] have P3F: "P3 F" by simp
        from P1F'[of x]
        have "applyPropOnOption P1 (Some z)" by auto
        hence "P1 z" by simp
        from a_f[OF ‹x ∉ dom F› this P3F] show ?case by assumption
      qed
      with a_obj show "P1 (Obj f T)" by simp
    qed
  qed
  with assms show ?thesis
  proof (auto)
    assume "⋀l f t1. ⟦l ∉ dom f; P3 f⟧ ⟹ P3 (f(l ↦ t1))"
    with ‹P3 Map.empty› show "P3 f" by (rule fmap_induct)
  qed
qed

lemma ball_tsp_P3:
  fixes 
  P1 :: "sterm ⇒ bool" and 
  P2 :: "sterm ⇒ fVariable ⇒ fVariable ⇒ bool" and 
  P3 :: "sterm ⇒ bool" and f :: "Label -~> sterm"
  assumes 
  "⋀t. ⟦ P1 t; ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 t s p ⟧ ⟹ P3 t" and
  "∀l∈dom f. P1 (the(f l))" and
  "∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 (the(f l)) s p"
  shows "∀l∈dom f. P3 (the(f l))"
proof (intro strip)
  fix l assume "l ∈ dom f" with assms(2) have "P1 (the(f l))" by blast
  moreover
  from assms(3) ‹l ∈ dom f› have "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 (the(f l)) s p"
    by blast
  ultimately
  show "P3 (the(f l))" using assms(1) by simp
qed

lemma ball_tt'sp_P3:
  fixes 
  P1 :: "sterm ⇒ sterm ⇒ bool" and 
  P2 :: "sterm ⇒ sterm ⇒ fVariable ⇒ fVariable ⇒ bool" and 
  P3 :: "sterm ⇒ sterm ⇒ bool" and 
  f :: "Label -~> sterm" and f' :: "Label -~> sterm"
  assumes 
  "⋀t t'. ⟦ P1 t t'; ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 t t' s p ⟧ ⟹ P3 t t'" and
  "dom f = dom f'" and
  "∀l∈dom f. P1 (the(f l)) (the(f' l))" and
  "∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 (the(f l)) (the(f' l)) s p"
  shows "∀l∈dom f'. P3 (the(f l)) (the(f' l))"
proof (intro strip)
  fix l assume "l ∈ dom f'" with assms(2-3) have "P1 (the(f l)) (the(f' l))" 
    by blast
  moreover 
  from assms(2,4) ‹l ∈ dom f'›
  have "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P2 (the (f l)) (the(f' l)) s p" by blast
  ultimately
  show "P3 (the(f l)) (the(f' l))" using assms(1)[of "the(f l)" "the(f' l)"] 
    by simp
qed

subsubsection ‹Free variables›
primrec
 FV       :: "sterm ⇒ fVariable set"
and
 FVoption :: "sterm option ⇒ fVariable set"
where
  FV_Bvar : "FV(Bvar b) = {}"
| FV_Fvar : "FV(Fvar x) = {x}"
| FV_Call : "FV(Call t l a) = FV t ∪ FV a"
| FV_Upd  : "FV(Upd t l s) = FV t ∪ FV s"
| FV_Obj  : "FV(Obj f T) = (⋃ l ∈ dom f. FVoption(f l))"
| FV_None : "FVoption None = {}"
| FV_Some : "FVoption (Some t) = FV t"

definition closed :: "sterm ⇒ bool" where
 "closed t ⟷ FV t = {}"

(* finiteness of FV *)
lemma finite_FV_FVoption: "finite (FV t) ∧ finite (FVoption s)"
by(induct _ t _ s rule: compat_sterm_sterm_option.induct, simp_all)

(* for infiniteness of string sets see
    List.infinite_UNIV_listI *)

(* NOTE: ex_new_if_finite, infinite_UNIV_listI and finite_FV offer an easy way to proof exists-fresh-statements *)
lemma finite_FV[simp]: "finite (FV t)"
  by (simp add: finite_FV_FVoption)

lemma FV_and_cofinite: "⟦ ∀x. x ∉ L ⟶ P x; finite L ⟧ 
  ⟹ ∃L'. (finite L' ∧ FV t ⊆ L' ∧ (∀ x. x ∉ L' ⟶ P x))"
  by (rule_tac x = "L ∪ FV t" in exI, auto)

lemma exFresh_s_p_cof: 
  fixes L :: "fVariable set"
  assumes "finite L"
  shows "∃s p. s ∉ L ∧ p ∉ L ∧ s ≠ p"
proof -
  from assms have "∃s. s ∉ L" by (simp only: ex_new_if_finite[OF infinite_UNIV_listI])
  then obtain s where "s ∉ L" ..
  moreover
  from ‹finite L› have "finite (L ∪ {s})" by simp
  hence "∃p. p ∉ L ∪ {s}" by (simp only: ex_new_if_finite[OF infinite_UNIV_listI])
  then obtain p where "p ∉ L ∪ {s}" ..
  ultimately show ?thesis by blast
qed

lemma FV_option_lem: "∀l∈dom f. FV (the(f l)) = FVoption (f l)"
  by auto

subsubsection ‹Term opening›
primrec
  sopen        :: "[nat, sterm, sterm, sterm] ⇒ sterm" 
  (‹{_ → [_,_]} _› [0, 0, 0, 300] 300)
and
  sopen_option :: "[nat, sterm, sterm, sterm option] ⇒ sterm option"
where
  sopen_Bvar: 
    "{k → [s,p]}(Bvar b) = (case b of (Self i) ⇒ (if (k = i) then s else (Bvar b)) 
                                    | (Param i) ⇒ (if (k = i) then p else (Bvar b)))"
| sopen_Fvar: "{k → [s,p]}(Fvar x) = Fvar x"
| sopen_Call: "{k → [s,p]}(Call t l a) = Call ({k → [s,p]}t) l ({k → [s,p]}a)"
| sopen_Upd : "{k → [s,p]}(Upd t l u) = Upd ({k → [s,p]}t) l ({(Suc k) → [s,p]}u)"
| sopen_Obj : "{k → [s,p]}(Obj f T) = Obj (λl. sopen_option (Suc k) s p (f l)) T"
| sopen_None: "sopen_option k s p None = None"
| sopen_Some: "sopen_option k s p (Some t) = Some ({k → [s,p]}t)"

definition openz :: "[sterm, sterm, sterm] ⇒ sterm" (‹(_)⇗[_,_]⇖› [50, 0, 0] 50) where
 "t⇗[s,p]⇖ = {0 → [s,p]}t"

lemma sopen_eq_Fvar:
  fixes n s p t x
  assumes "{n → [Fvar s,Fvar p]} t = Fvar x"
  shows 
  "(t = Fvar x) ∨ (x = s ∧ t = (Bvar (Self n))) 
  ∨ (x = p ∧ t = (Bvar (Param n)))"
proof (cases t)
  case Obj with assms show ?thesis by simp
next
  case Call with assms show ?thesis by simp
next
  case Upd with assms show ?thesis by simp
next
  case (Fvar y) with assms show ?thesis
    by (cases "y = x", simp_all)
next
  case (Bvar b) thus ?thesis
  proof (cases b)
    case (Self k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  next
    case (Param k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  qed
qed

lemma sopen_eq_Fvar': 
  assumes "{n → [Fvar s,Fvar p]} t = Fvar x" and "x ≠ s" and "x ≠ p"
  shows "t = Fvar x"
proof -
  from sopen_eq_Fvar[OF assms(1)] ‹x ≠ s› ‹x ≠ p› show ?thesis
    by auto
qed

lemma sopen_eq_Bvar: 
  fixes n s p t b
  assumes "{n → [Fvar s,Fvar p]} t = Bvar b"
  shows "t = Bvar b"
proof (cases t)
  case Fvar with assms show ?thesis by (simp add: openz_def)
next
  case Obj with assms show ?thesis by (simp add: openz_def)
next
  case Call with assms show ?thesis by (simp add: openz_def)
next
  case Upd with assms show ?thesis by (simp add: openz_def)
next
  case (Bvar b') show ?thesis
  proof (cases b')
    case (Self k) with assms Bvar show ?thesis
      by (cases "k = n") (simp_all add: openz_def)
  next
    case (Param k) with assms Bvar show ?thesis
      by (cases "k = n") (simp_all add: openz_def)
  qed
qed

lemma sopen_eq_Obj: 
  fixes n s p t f T
  assumes "{n → [Fvar s,Fvar p]} t = Obj f T"
  shows 
  "∃f'. {n → [Fvar s, Fvar p]} Obj f' T = Obj f T  
      ∧  t = Obj f' T"
proof (cases t)
  case Fvar with assms show ?thesis by simp
next
  case Obj with assms show ?thesis by simp
next
  case Call with assms show ?thesis by simp
next
  case Upd with assms show ?thesis by simp
next
  case (Bvar b) thus ?thesis
  proof (cases b)
    case (Self k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  next
    case (Param k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  qed
qed

lemma sopen_eq_Upd: 
  fixes n s p t t1 l t2
  assumes "{n → [Fvar s,Fvar p]} t = Upd t1 l t2"
  shows 
  "∃t1' t2'. {n → [Fvar s,Fvar p]} t1' = t1 
           ∧ {(Suc n) → [Fvar s,Fvar p]} t2' = t2 ∧ t = Upd t1' l t2'"
proof (cases t)
  case Fvar with assms show ?thesis by simp
next
  case Obj with assms show ?thesis by simp
next
  case Call with assms show ?thesis by simp
next
  case Upd with assms show ?thesis by simp
next
  case (Bvar b) thus ?thesis
  proof (cases b)
    case (Self k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  next
    case (Param k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  qed
qed

lemma sopen_eq_Call: 
  fixes n s p t t1 l t2
  assumes "{n → [Fvar s,Fvar p]} t = Call t1 l t2"
  shows 
  "∃t1' t2'. {n → [Fvar s,Fvar p]} t1' = t1 
           ∧ {n → [Fvar s,Fvar p]} t2' = t2 ∧ t = Call t1' l t2'"
proof (cases t)
  case Fvar with assms show ?thesis by simp
next
  case Obj with assms show ?thesis by simp
next
  case Call with assms show ?thesis by simp
next
  case Upd with assms show ?thesis by simp
next
  case (Bvar b) thus ?thesis
  proof (cases b)
    case (Self k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  next
    case (Param k) with assms Bvar show ?thesis 
      by (cases "k = n") simp_all
  qed
qed

lemma dom_sopenoption_lem[simp]: "dom (λl. sopen_option k s t (f l)) = dom f"
  by (auto, case_tac "x ∈ dom f", auto)

lemma sopen_option_lem: 
  "∀l∈dom f. {n → [s,p]} the(f l) = the (sopen_option n s p (f l))" 
  by auto

lemma pred_sopenoption_lem:
  "(∀l∈dom (λl. sopen_option n s p (f l)).
     (P::sterm ⇒ bool) (the (sopen_option n s p (f l)))) = 
   (∀l∈dom f. (P::sterm ⇒ bool) ({n → [s,p]} the (f l)))"
  by (simp, force)

lemma sopen_FV[rule_format]:
  "∀n s p. FV ({n → [s,p]} t) ⊆ FV t ∪ FV s ∪ FV p"
proof -
  fix u
  have
    "(∀n s p. FV ({n → [s,p]} t) ⊆ FV t ∪ FV s ∪ FV p)
    &(∀n s p. FVoption (sopen_option n s p u) ⊆ FVoption u ∪ FV s ∪ FV p)"
    apply (induct u rule: compat_sterm_sterm_option.induct)
    apply (auto split: bVariable.split)
    apply (metis (no_types, lifting) FV_Some UnE domI sopen_Some subsetCE)
    apply blast
    apply blast
    done
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sopen_commute[rule_format]:
  "∀n k s p s' p'. n ≠ k
     ⟶ {n → [Fvar s', Fvar p']} {k → [Fvar s, Fvar p]} t 
         = {k → [Fvar s, Fvar p]} {n → [Fvar s', Fvar p']} t"
proof -
  fix u
  have
    "(∀n k s p s' p'. n ≠ k
      ⟶ {n → [Fvar s', Fvar p']} {k → [Fvar s, Fvar p]} t 
          = {k → [Fvar s, Fvar p]} {n → [Fvar s', Fvar p']} t)
    &(∀n k s p s' p'. n ≠ k
      ⟶ sopen_option n (Fvar s') (Fvar p') (sopen_option k (Fvar s) (Fvar p) u) 
          = sopen_option k (Fvar s) (Fvar p)
             (sopen_option n (Fvar s') (Fvar p') u))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sopen_fresh_inj[rule_format]:
  "∀n s p t'. {n → [Fvar s, Fvar p]} t = {n → [Fvar s, Fvar p]} t'
     ⟶ s ∉ FV t ⟶ s ∉ FV t' ⟶ p ∉ FV t ⟶ p ∉ FV t' ⟶ s ≠ p
     ⟶ t = t'"
proof -
  {
    fix 
      b s p n t
    assume 
      "(case b of Self i ⇒ if n = i then Fvar s else Bvar b
               | Param i ⇒ if n = i then Fvar p else Bvar b) = t"
    hence "Fvar s = t ∨ Fvar p = t ∨ Bvar b = t"
      by (cases b, auto, (rename_tac nat, case_tac "n = nat", auto)+)
  }
  note cT = this

(* induction *)
  fix u
  have
    "(∀n s p t'. {n → [Fvar s, Fvar p]} t = {n → [Fvar s, Fvar p]} t'
      ⟶ s ∉ FV t ⟶ s ∉ FV t' ⟶ p ∉ FV t ⟶ p ∉ FV t' ⟶ s ≠ p
      ⟶ t = t')
    &(∀n s p u'. sopen_option n (Fvar s) (Fvar p) u 
                  = sopen_option n (Fvar s) (Fvar p) u'
      ⟶ s ∉ FVoption u ⟶ s ∉ FVoption u' 
      ⟶ p ∉ FVoption u ⟶ p ∉ FVoption u' ⟶ s ≠ p
      ⟶ u = u')"
  proof (induct _ t _ u rule: compat_sterm_sterm_option.induct)
    case (Bvar b) thus ?case
    proof (auto)
      fix s p n t
      assume 
        a: "(case b of Self i ⇒ if n = i then Fvar s else Bvar b
                 | Param i ⇒ if n = i then Fvar p else Bvar b) 
         = {n → [Fvar s,Fvar p]} t"
      note cT[OF this]
      moreover assume "s ∉ FV t" and "p ∉ FV t" and "s ≠ p"
      ultimately show "Bvar b = t"
      proof (auto)
        {
          fix b'
          assume 
            "(case b' of Self i ⇒ if n = i then Fvar s else Bvar b'
                      | Param i ⇒ if n = i then Fvar p else Bvar b') = Fvar s"
          with ‹s ≠ p› have "b' = Self n"
            by (cases b', auto, (rename_tac nat, case_tac "n = nat", auto)+)
        }note fvS = this
        assume eq_s: "Fvar s = {n → [Fvar s,Fvar p]} t"
        with sym[OF this] ‹s ∉ FV t› ‹s ≠ p› fvS
        have "t = Bvar (Self n)" by (cases t, auto)
        moreover
        from a sym[OF eq_s] ‹s ≠ p› fvS[of b]
        have "Self n = b" by simp
        ultimately show "Bvar b = t" by simp
      next
        {
          fix b'
          assume 
            "(case b' of Self i ⇒ if n = i then Fvar s else Bvar b'
                      | Param i ⇒ if n = i then Fvar p else Bvar b') = Fvar p"
          with ‹s ≠ p› have "b' = Param n"
            by (cases b', auto, (rename_tac nat, case_tac "n = nat", auto)+)
        }note fvP = this
        assume eq_p: "Fvar p = {n → [Fvar s,Fvar p]} t"
        with sym[OF this] ‹p ∉ FV t› ‹s ≠ p› fvP
        have "t = Bvar (Param n)" by (cases t, auto)
        moreover
        from a sym[OF eq_p] ‹s ≠ p› fvP[of b]
        have "Param n = b" by simp
        ultimately show "Bvar b = t" by simp
      next
        assume "Bvar b = {n → [Fvar s, Fvar p]} t"
        from sym[OF this] show "{n → [Fvar s,Fvar p]} t = t"
        proof (cases t, auto)
          fix b'
          assume 
            "(case b' of Self i ⇒ if n = i then Fvar s else Bvar b'
                      | Param i ⇒ if n = i then Fvar p else Bvar b') = Bvar b"
          from cT[OF this] have "Bvar b = Bvar b'" by simp
          thus "b = b'" by simp
        qed
      qed
    qed
  next
    case (Fvar x) thus ?case
    proof (auto)
      fix n s p t
      assume 
        a: "Fvar x = {n → [Fvar s,Fvar p]} t" and
        "s ∉ FV ({n → [Fvar s,Fvar p]} t)"
      hence "s ≠ x" by force
      moreover
      assume "p ∉ FV ({n → [Fvar s,Fvar p]} t)"
      with a have "p ≠ x" by force
      ultimately
      show "{n → [Fvar s,Fvar p]} t = t"
        using a
      proof (cases t, auto)
        fix b
        assume 
          "Fvar x = (case b of Self i ⇒ if n = i then Fvar s else Bvar b
                            | Param i ⇒ if n = i then Fvar p else Bvar b)"
        from cT[OF sym[OF this]] ‹s ≠ x› ‹p ≠ x›
        have False by simp
        then show 
          "(case b of Self i ⇒ if n = i then Fvar s else Bvar b
                   | Param i ⇒ if n = i then Fvar p else Bvar b) = Bvar b" ..
      qed
    qed
  next
    case (Obj f T) thus ?case
    proof (auto)
      fix n s p t
      assume 
        "Obj (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) T 
         = {n → [Fvar s,Fvar p]} t" and
        "∀l∈dom f. s ∉ FVoption (f l)" and 
        "∀l∈dom f. p ∉ FVoption (f l)" and
        "s ∉ FV t" and "p ∉ FV t" and "s ≠ p"
      thus "Obj f T = t" using Obj
      proof (cases t, auto)
          (* case Bvar *)
        fix b
        assume 
          "Obj (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) T 
           = (case b of Self i ⇒ if n = i then Fvar s else Bvar b
                     | Param i ⇒ if n = i then Fvar p else Bvar b)"
        from cT[OF sym[OF this]] show False by auto
      next
          (* case Obj *)
        fix f'
        assume 
          nin_s: "∀l∈dom f'. s ∉ FVoption (f' l)" and
          nin_p: "∀l∈dom f'. p ∉ FVoption (f' l)" and
          ff':   "(λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) 
                  = (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f' l))"
        have "⋀l. f l = f' l"
        proof -
          fix  l
          from ff'
          have 
            "sopen_option (Suc n) (Fvar s) (Fvar p) (f l) 
             = sopen_option (Suc n) (Fvar s) (Fvar p) (f' l)"
            by (rule cong, simp)
          moreover
          from 
            ‹∀l∈dom f. s ∉ FVoption (f l)›
            ‹∀l∈dom f. p ∉ FVoption (f l)› 
          have "s ∉ FVoption (f l)" and "p ∉ FVoption (f l)"
            by (case_tac "l ∈ dom f", auto)+
          moreover
          from nin_s nin_p have "s ∉ FVoption (f' l)" and "p ∉ FVoption (f' l)"
            by (case_tac "l ∈ dom f'", auto)+
          ultimately show "f l = f' l" using Obj[of l] ‹s ≠ p›
            by simp
        qed
        thus "f = f'" by (rule ext)
      qed
    qed
  next
    case (Call t1 l t2) thus ?case
    proof (auto)
      fix n s p t
      assume 
        "s ∉ FV t1" and "s ∉ FV t2" and "p ∉ FV t1" and "p ∉ FV t2" and
        "s ≠ p" and "s ∉ FV t" and "p ∉ FV t" and 
        "Call ({n → [Fvar s,Fvar p]} t1) l ({n → [Fvar s,Fvar p]} t2)
         = {n → [Fvar s,Fvar p]} t"
      thus "Call t1 l t2 = t" using Call
      proof (cases t, auto)
          (* case Bvar *)
        fix b
        assume 
          "Call ({n → [Fvar s,Fvar p]} t1) l ({n → [Fvar s,Fvar p]} t2) 
           = (case b of Self i ⇒ if n = i then Fvar s else Bvar b
                     | Param i ⇒ if n = i then Fvar p else Bvar b)"
        from cT[OF sym[OF this]] show False by auto
      qed
    qed
  next
    case (Upd t1 l t2) thus ?case
    proof (auto)
      fix n s p t
      assume 
        "s ∉ FV t1" and "s ∉ FV t2" and "p ∉ FV t1" and "p ∉ FV t2" and
        "s ≠ p" and "s ∉ FV t" and "p ∉ FV t" and
        "Upd ({n → [Fvar s,Fvar p]} t1) l ({Suc n → [Fvar s,Fvar p]} t2)
         = {n → [Fvar s,Fvar p]} t"
      thus "Upd t1 l t2 = t" using Upd
      proof (cases t, auto)
          (* case Bvar *)
        fix b
        assume 
          "Upd ({n → [Fvar s,Fvar p]} t1) l ({Suc n → [Fvar s,Fvar p]} t2) 
           = (case b of Self i ⇒ if n = i then Fvar s else Bvar b
                     | Param i ⇒ if n = i then Fvar p else Bvar b)"
        from cT[OF sym[OF this]] show False by auto
      qed
    qed
  next
    case None_sterm thus ?case
    proof (auto)
      fix u s p n
      assume "None = sopen_option n (Fvar s) (Fvar p) u"
      thus "None = u" by (cases u, auto)
    qed
  next
    case (Some_sterm t) thus ?case
    proof (auto)
      fix u s p n
      assume 
        "Some ({n → [Fvar s,Fvar p]} t) = sopen_option n (Fvar s) (Fvar p) u" and
        "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" and 
        "s ∉ FVoption u" and "p ∉ FVoption u"
      with Some_sterm show "Some t = u" by (cases u) auto
    qed
  qed
  from conjunct1[OF this] show ?thesis by assumption
qed

subsubsection ‹Variable closing›
primrec
 sclose        :: "[nat, fVariable, fVariable, sterm] ⇒ sterm" 
 (‹{_ ← [_,_]} _› [0, 0, 0, 300] 300)
and
 sclose_option :: "[nat, fVariable, fVariable, sterm option] ⇒ sterm option"
where
  sclose_Bvar: "{k ← [s,p]}(Bvar b) = Bvar b"
| sclose_Fvar: 
    "{k ← [s,p]}(Fvar x) = (if x = s then (Bvar (Self k)) 
                                      else (if x = p then (Bvar (Param k))
                                                     else (Fvar x)))"
| sclose_Call: "{k ← [s,p]}(Call t l a) = Call ({k ← [s,p]}t) l ({k ← [s,p]}a)"
| sclose_Upd : "{k ← [s,p]}(Upd t l u) = Upd ({k ← [s,p]}t) l ({(Suc k) ← [s,p]}u)"
| sclose_Obj : "{k ← [s,p]}(Obj f T) = Obj (λl. sclose_option (Suc k) s p (f l)) T"
| sclose_None: "sclose_option k s p None = None"
| sclose_Some: "sclose_option k s p (Some t) = Some ({k ← [s,p]}t)"

definition closez :: "[fVariable, fVariable, sterm] ⇒ sterm" (‹σ[_,_] _› [0, 0, 300]) where
 "σ[s,p] t = {0 ← [s,p]}t"

lemma dom_scloseoption_lem[simp]: "dom (λl. sclose_option k s t (f l)) = dom f"
  by (auto, case_tac "x ∈ dom f", auto)

lemma sclose_option_lem: 
  "∀l∈dom f. {n ← [s,p]} the(f l) = the (sclose_option n s p (f l))" 
  by auto

lemma pred_scloseoption_lem:
  "(∀l∈dom (λl. sclose_option n s p (f l)).
     (P::sterm ⇒ bool) (the (sclose_option n s p (f l)))) = 
   (∀l∈dom f. (P::sterm ⇒ bool) ({n ← [s,p]} the (f l)))"
  by (simp, force)

lemma sclose_fresh[simp, rule_format]:
  "∀n s p. s ∉ FV t ⟶ p ∉ FV t ⟶ {n ← [s,p]} t = t"
proof -
  have 
    "(∀n s p. s ∉ FV t ⟶ p ∉ FV t ⟶ {n ← [s,p]} t = t)
    &(∀n s p. s ∉ FVoption u ⟶ p ∉ FVoption u 
       ⟶ sclose_option n s p u = u)"
  proof (induct _ t _ u rule: compat_sterm_sterm_option.induct, auto simp: bVariable.split)
    (* Obj *)
    fix f n s p
    assume 
      nin_s: "∀l∈dom f. s ∉ FVoption (f l)" and 
      nin_p: "∀l∈dom f. p ∉ FVoption (f l)"
    {
      fix l from nin_s have "s ∉ FVoption (f l)"
        by (case_tac "l ∈ dom f", auto)
    }
    moreover
    {
      fix l from nin_p have "p ∉ FVoption (f l)"
        by (case_tac "l ∈ dom f", auto)
    }
    moreover 
    assume 
      "⋀x. ∀n s. s ∉ FVoption (f x) 
             ⟶ (∀p. p ∉ FVoption (f x) 
                   ⟶ sclose_option n s p (f x) = f x)"
    ultimately
    have "⋀l. sclose_option (Suc n) s p (f l) = f l" by auto
    with ext show "(λl. sclose_option (Suc n) s p (f l)) = f" by auto
  qed
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sclose_FV[rule_format]:
  "∀n s p. FV ({n ← [s,p]} t) = FV t - {s} - {p}"
proof -
  have
    "(∀n s p. FV ({n ← [s,p]} t) = FV t - {s} - {p})
    &(∀n s p. FVoption (sclose_option n s p u) = FVoption u - {s} - {p})"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split, blast+)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sclose_subset_FV[rule_format]:
  "FV ({n ← [s,p]} t) ⊆ FV t"
  by (simp add: sclose_FV, blast)

lemma Self_not_in_closed[simp]: "sa ∉ FV ({n ← [sa,pa]} t)"
  by (simp add: sclose_FV)

lemma Param_not_in_closed[simp]: "pa ∉ FV ({n ← [sa,pa]} t)"
  by (simp add: sclose_FV)

subsubsection ‹Substitution›
primrec
 ssubst        :: "[fVariable, sterm, sterm] ⇒ sterm" 
 (‹[_ → _] _› [0, 0, 300] 300)
and
 ssubst_option :: "[fVariable, sterm, sterm option] ⇒ sterm option"
where
  ssubst_Bvar: "[z → u](Bvar v) = Bvar v"
| ssubst_Fvar: "[z → u](Fvar x) = (if (z = x) then u else (Fvar x))"
| ssubst_Call: "[z → u](Call t l s) = Call ([z → u]t) l ([z → u]s)"
| ssubst_Upd : "[z → u](Upd t l s) = Upd ([z → u]t) l ([z → u]s)"
| ssubst_Obj : "[z → u](Obj f T) = Obj (λl. ssubst_option z u (f l)) T"
| ssubst_None: "ssubst_option z u None = None"
| ssubst_Some: "ssubst_option z u (Some t) = Some ([z → u]t)"

lemma dom_ssubstoption_lem[simp]: "dom (λl. ssubst_option z u (f l)) = dom f"
  by (auto, case_tac "x ∈ dom f", auto)

lemma ssubst_option_lem: 
  "∀l∈dom f. [z → u] the(f l) = the (ssubst_option z u (f l))" 
  by auto

lemma pred_ssubstoption_lem:
  "(∀l∈dom (λl. ssubst_option x t (f l)).
     (P::sterm ⇒ bool) (the (ssubst_option x t (f l)))) = 
   (∀l∈dom f. (P::sterm ⇒ bool) ([x → t] the (f l)))"
  by (simp, force)

lemma ssubst_fresh[simp, rule_format]:
  "∀s sa. sa ∉ FV t ⟶ [sa → s] t = t"
proof -
  have 
    "(∀s sa. sa ∉ FV t ⟶ [sa → s] t = t)
    &(∀s sa. sa ∉ FVoption u ⟶ ssubst_option sa s u = u)"
  proof (induct _ t _ u rule: compat_sterm_sterm_option.induct, auto)
    fix s sa f
    assume 
      sa:     "∀l∈dom f. sa ∉ FVoption (f l)" and
      ssubst: "⋀x. ∀s sa. sa ∉ FVoption (f x) ⟶ ssubst_option sa s (f x) = f x"
    {
      fix l from sa have "sa ∉ FVoption (f l)" 
        by (case_tac "l ∈ dom f", auto)
      with ssubst have "ssubst_option sa s (f l) = f l" by auto
    }
    with ext show "(λl. ssubst_option sa s (f l)) = f" by auto
  qed
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma ssubst_commute[rule_format]:
  "∀s p sa pa. s ≠ p ⟶ s ∉ FV pa ⟶ p ∉ FV sa 
     ⟶ [s → sa] [p → pa] t = [p → pa] [s → sa] t"
proof -
  have
    "(∀s p sa pa. s ≠ p ⟶ s ∉ FV pa ⟶ p ∉ FV sa 
       ⟶ [s → sa] [p → pa] t = [p → pa] [s → sa] t)
    &(∀s p sa pa. s ≠ p ⟶ s ∉ FV pa ⟶ p ∉ FV sa 
       ⟶ ssubst_option s sa (ssubst_option p pa u) 
           = ssubst_option p pa (ssubst_option s sa u))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma ssubst_FV[rule_format]:
  "∀x s. FV ([x → s] t) ⊆ FV s ∪ (FV t - {x})"
proof -
  have
    "(∀x s. FV ([x → s] t) ⊆ FV s ∪ (FV t - {x}))
    &(∀x s. FVoption (ssubst_option x s u) ⊆ FV s ∪ (FVoption u - {x}))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split, blast+)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma ssubstoption_insert: 
  "l ∈ dom f 
  ⟹ (λ(la::Label). ssubst_option x t' (if la = l then Some t else f la))
      = (λ(la::Label). ssubst_option x t' (f la))(l ↦ [x → t'] t)"
  by (rule Ltake_eq_all, force, simp add: Ltake_eq_def)

subsubsection ‹Local closure›
inductive lc :: "sterm ⇒ bool"
where
  lc_Fvar[simp, intro!]: "lc (Fvar x)"
| lc_Call[simp, intro!]: "⟦ lc t; lc a ⟧ ⟹ lc (Call t l a)"
| lc_Upd[simp, intro!] : 
  "⟦ lc t; finite L; 
     ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ lc (u⇗[Fvar s, Fvar p]⇖) ⟧
  ⟹ lc (Upd t l u)"
| lc_Obj[simp, intro!] : 
  "⟦ finite L; ∀l∈dom f. 
     ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ lc (the(f l)⇗[Fvar s, Fvar p]⇖) ⟧
  ⟹ lc (Obj f T)"

definition body :: "sterm ⇒ bool" where
 "body t ⟷ (∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ lc (t⇗[Fvar s, Fvar p]⇖)))"

lemma lc_bvar: "lc (Bvar b) = False" 
  by (rule iffI, erule lc.cases, simp_all)

lemma lc_obj:
  "lc (Obj f T) = (∀l∈dom f. body (the(f l)))"
proof
  fix f T assume "lc (Obj f T)"
  thus "∀l∈dom f. body (the(f l))"
    unfolding body_def
    by (rule lc.cases, auto)
next
  fix f :: "Label -~> sterm" and T :: type
  assume "∀l∈dom f. body (the (f l))"
  hence 
    "∃L. finite L ∧ (∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                                 ⟶ lc (the (f l)⇗[Fvar s, Fvar p]⇖))"
  proof (induct f rule: fmap_induct)
    case empty thus ?case by blast
  next
    case (insert F x y) thus ?case
    proof -
      assume "x ∉ dom F" hence "∀l∈dom F. the(F l) = the ((F(x ↦ y)) l)" 
        by auto
      with ‹∀l∈dom (F(x ↦ y)). body (the((F(x ↦ y)) l))›
      have "∀l∈dom F. body (the (F l))" by force
      from insert(2)[OF this]
      obtain L where 
        "finite L" and
        "∀l∈dom F. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
                     ⟶ lc (the (F l)⇗[Fvar s, Fvar p]⇖)" by auto
      moreover
      from ‹∀l∈dom (F(x ↦ y)). body (the((F(x ↦ y)) l))› have "body y" by force
      then obtain L' where 
        "finite L'" and
        "∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
          ⟶ lc (y⇗[Fvar s, Fvar p]⇖)" by (auto simp: body_def)

      ultimately
      show 
        "∃L. finite L ∧ (∀l∈dom (F(x ↦ y)). ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                                               ⟶ lc (the ((F(x ↦ y)) l)⇗[Fvar s,Fvar p]⇖))" 
        by (rule_tac x = "L ∪ L'" in exI, auto)
    qed
  qed
  thus "lc (Obj f T)" by auto
qed

lemma lc_upd: "lc (Upd t l s) = (lc t ∧ body s)" 
  by (unfold body_def, rule iffI, erule lc.cases, auto)

lemma lc_call: "lc (Call t l s) = (lc t ∧ lc s)" 
  by (rule iffI, erule lc.cases, simp_all)

lemma lc_induct[consumes 1, case_names Fvar Call Upd Obj Bnd]:
  fixes P1 :: "sterm ⇒ bool" and P2 :: "sterm ⇒ bool"
  assumes
  "lc t" and
  "⋀x. P1 (Fvar x)" and
  "⋀t l a. ⟦ lc t; P1 t; lc a; P1 a ⟧ ⟹ P1 (Call t l a)" and
  "⋀t l u. ⟦ lc t; P1 t; P2 u ⟧ ⟹ P1 (Upd t l u)" and
  "⋀f T. ∀l∈dom f. P2 (the(f l)) ⟹ P1 (Obj f T)" and
  "⋀L t. ⟦ finite L; 
            ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
             ⟶ lc (t⇗[Fvar s, Fvar p]⇖) ∧ P1 (t⇗[Fvar s, Fvar p]⇖) ⟧
  ⟹ P2 t"
  shows "P1 t"
  using assms by (induct rule: lc.induct, auto)
  

subsubsection ‹Connections between sopen, sclose, ssubst, lc and body and resulting properties›
lemma ssubst_intro[rule_format]:
  "∀n s p sa pa. sa ∉ FV t ⟶ pa ∉ FV t ⟶ sa ≠ pa
     ⟶ sa ∉ FV p
     ⟶ {n → [s,p]} t = [sa → s] [pa → p] {n → [Fvar sa, Fvar pa]} t"
proof -
  have 
    "(∀n s p sa pa. sa ∉ FV t ⟶ pa ∉ FV t ⟶ sa ≠ pa
       ⟶ sa ∉ FV p
       ⟶ {n → [s,p]} t = [sa → s] [pa → p] {n → [Fvar sa, Fvar pa]} t)
    &(∀n s p sa pa. sa ∉ FVoption u ⟶ pa ∉ FVoption u ⟶ sa ≠ pa
       ⟶ sa ∉ FV p
       ⟶ sopen_option n s p u 
           = ssubst_option sa s (ssubst_option pa p 
              (sopen_option n (Fvar sa) (Fvar pa) u)))"
  proof (induct _ t _ u rule: compat_sterm_sterm_option.induct)
    case Bvar thus ?case by (simp split: bVariable.split)
  next
    case Fvar thus ?case by simp
  next
    case Upd thus ?case by simp
  next
    case Call thus ?case by simp
  next
    case None_sterm thus ?case by simp
  next
    case (Obj f T) thus ?case
    proof (clarify)
      fix n s p sa pa
      assume "sa ∉ FV (Obj f T)" and "pa ∉ FV (Obj f T)"
      {
        fix l 
        from ‹sa ∉ FV (Obj f T)› have "sa ∉ FVoption (f l)"
          by (case_tac "l ∈ dom f", auto)
      }
      moreover
      {
        fix l
        from ‹pa ∉ FV (Obj f T)› have pa: "pa ∉ FVoption (f l)"
          by (case_tac "l ∈ dom f", auto)
      }
      moreover assume "sa ≠ pa" and "sa ∉ FV p"
      ultimately
      have 
        "⋀l. sopen_option (Suc n) s p (f l) 
              = ssubst_option sa s (ssubst_option pa p
                 (sopen_option (Suc n) (Fvar sa) (Fvar pa) (f l)))"
        using Obj by auto
      with ext 
      show 
        "{n → [s,p]} Obj f T 
         = [sa → s] [pa → p] {n → [Fvar sa,Fvar pa]} Obj f T"
        by auto
    qed
  next
    case (Some_sterm t) thus ?case
    proof (clarify)
      fix n s p sa pa
      assume "sa ∉ FVoption (Some t)"
      hence "sa ∉ FV t" by simp
      moreover assume "pa ∉ FVoption (Some t)"
      hence "pa ∉ FV t" by simp
      moreover assume "sa ≠ pa" and "sa ∉ FV p"
      ultimately
      have "{n → [s,p]} t = [sa → s] [pa → p] {n → [Fvar sa,Fvar pa]} t" 
        using Some_sterm by blast
      thus 
        "sopen_option n s p (Some t) 
         = ssubst_option sa s (ssubst_option pa p 
            (sopen_option n (Fvar sa) (Fvar pa) (Some t)))"
        by simp
    qed
  qed
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sopen_lc_FV[rule_format]:
  fixes t
  assumes "lc t"
  shows "∀n s p. {n → [Fvar s, Fvar p]} t = t"
  using assms
proof 
  (induct
    taking: "λt. ∀n s p. {Suc n → [Fvar s, Fvar p]} t = t"
    rule: lc_induct)
  case Fvar thus ?case by simp
next
  case Call thus ?case by simp
next
  case Upd thus ?case by simp
next
  case (Obj f T) note pred = this 
  show ?case
  proof (intro strip, simp)
    fix n s p
    {
      fix l
      have "sopen_option (Suc n) (Fvar s) (Fvar p) (f l) = f l"
      proof (cases "l ∈ dom f")
        case False hence "f l = None" by force
        thus ?thesis by force
      next
        case True with pred show ?thesis by force
      qed
    } with ext 
    show "(λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) = f"
      by auto
  qed
next
  case (Bnd L t) note cof = this(2)  
  show ?case
  proof (intro strip)
    fix n s p
    from ‹finite L› exFresh_s_p_cof[of "L ∪ FV t ∪ {s} ∪ {p}"]
    obtain sa pa where
      sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
      by auto
    with cof
    have "{Suc n → [Fvar s,Fvar p]} (t⇗[Fvar sa, Fvar pa]⇖) = (t⇗[Fvar sa, Fvar pa]⇖)"
      by auto
    with sopen_commute[OF Suc_not_Zero[of n]]
    have 
      eq: "{0 → [Fvar sa,Fvar pa]} {Suc n → [Fvar s,Fvar p]} t
           = {0 → [Fvar sa,Fvar pa]} t" 
      by (simp add: openz_def)
    from sapa contra_subsetD[OF sopen_FV[of _ "Fvar s" "Fvar p" t]]
    have 
      "sa ∉ FV ({Suc n → [Fvar s,Fvar p]} t)" and "sa ∉ FV t" and
      "pa ∉ FV ({Suc n → [Fvar s,Fvar p]} t)" and "pa ∉ FV t" and 
      "sa ≠ pa" 
      by auto
    from sopen_fresh_inj[OF eq this] 
    show "{Suc n → [Fvar s,Fvar p]} t = t" by assumption
  qed
qed    

lemma sopen_lc[simp]: 
  fixes t n s p
  assumes "lc t"
  shows "{n → [s,p]} t = t"
proof -
  from exFresh_s_p_cof[of "FV t ∪ FV p"] 
  obtain sa pa where 
    "sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and 
    "sa ∉ FV p" and "pa ∉ FV p" 
    by auto
  from ssubst_intro[OF this(1-4)] 
  have "{n → [s,p]} t = [sa → s] [pa → p] {n → [Fvar sa,Fvar pa]} t" 
    by simp
  with assms have "{n → [s,p]} t = [sa → s] [pa → p] t" 
    using sopen_lc_FV 
    by simp
  with ssubst_fresh[OF ‹pa ∉ FV t›] 
  have "{n → [s,p]} t = [sa → s] t" by simp
  with ssubst_fresh[OF ‹sa ∉ FV t›] 
  show "{n → [s,p]} t = t" by simp
qed

lemma sopen_twice[rule_format]:
  "∀s p s' p' n. lc s ⟶ lc p 
     ⟶ {n → [s',p']} {n → [s,p]} t = {n → [s,p]} t"
proof -
  have
    "(∀s p s' p' n. lc s ⟶ lc p 
      ⟶ {n → [s',p']} {n → [s,p]} t = {n → [s,p]} t)
    &(∀s p s' p' n. lc s ⟶ lc p 
      ⟶ sopen_option n s' p' (sopen_option n s p u) = sopen_option n s p u)"
    by (rule compat_sterm_sterm_option.induct, auto simp: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sopen_sclose_commute[rule_format]:
  "∀n k s p sa pa. n ≠ k ⟶ sa ∉ FV s ⟶ sa ∉ FV p 
     ⟶ pa ∉ FV s ⟶ pa ∉ FV p
     ⟶ {n → [s, p]} {k ← [sa,pa]} t = {k ← [sa,pa]} {n → [s, p]} t"
proof -
  have 
    "(∀n k s p sa pa. n ≠ k ⟶ sa ∉ FV s ⟶ sa ∉ FV p 
       ⟶ pa ∉ FV s ⟶ pa ∉ FV p
       ⟶ {n → [s, p]} {k ← [sa,pa]} t = {k ← [sa,pa]} {n → [s, p]} t)
    &(∀n k s p sa pa. n ≠ k ⟶ sa ∉ FV s ⟶ sa ∉ FV p 
       ⟶ pa ∉ FV s ⟶ pa ∉ FV p
       ⟶ sopen_option n s p (sclose_option k sa pa u) 
           = sclose_option k sa pa (sopen_option n s p u))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sclose_sopen_eq_t[rule_format]:
  "∀n s p. s ∉ FV t ⟶ p ∉ FV t ⟶ s ≠ p
     ⟶ {n ← [s,p]} {n → [Fvar s, Fvar p]} t = t"
proof -
  have 
    "(∀n s p. s ∉ FV t ⟶ p ∉ FV t ⟶ s ≠ p
       ⟶ {n ← [s,p]} {n → [Fvar s, Fvar p]} t = t)
    &(∀n s p. s ∉ FVoption u ⟶ p ∉ FVoption u ⟶ s ≠ p
       ⟶ sclose_option n s p (sopen_option n (Fvar s) (Fvar p) u) = u)"
  proof (induct _ t _ u rule: compat_sterm_sterm_option.induct, simp_all split: bVariable.split, auto)
    (* Obj *)
    fix f n s p
    assume 
      nin_s: "∀l∈dom f. s ∉ FVoption (f l)" and
      nin_p: "∀l∈dom f. p ∉ FVoption (f l)"
    {
      fix l from nin_s have "s ∉ FVoption (f l)"
        by (case_tac "l ∈ dom f", auto)
    }
    moreover
    {
      fix l from nin_p have "p ∉ FVoption (f l)"
        by (case_tac "l ∈ dom f", auto)
    }
    moreover 
    assume 
      "s ≠ p" and
      "⋀x. ∀n s. s ∉ FVoption (f x) 
             ⟶ (∀p. p ∉ FVoption (f x) ⟶ s ≠ p 
                   ⟶ sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f x)) 
                       = f x)"
    ultimately
    have "⋀l. sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f l)) = f l"
      by auto
    with ext 
    show "(λl. sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f l))) = f "
      by auto
  qed
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma sopen_sclose_eq_t[simp, rule_format]:
  fixes t
  assumes "lc t"
  shows "∀n s p. {n → [Fvar s, Fvar p]} {n ← [s,p]} t = t"
  using assms
proof 
  (induct
    taking: "λt. ∀n s p. {Suc n → [Fvar s, Fvar p]} {Suc n ← [s,p]} t = t"
    rule: lc_induct)
  case Fvar thus ?case by simp
next
  case Call thus ?case by simp
next
  case Upd thus ?case by simp
next
  case (Obj f T) note pred = this
  show ?case
  proof (intro strip, simp)
    fix n s p
    {
      fix l
      have 
        "sopen_option (Suc n) (Fvar s) (Fvar p) (sclose_option (Suc n) s p (f l)) 
         = f l"
      proof (cases "l ∈ dom f")
        case False hence "f l = None" by force
        thus ?thesis by simp
      next
        case True with pred
        show ?thesis by force
      qed
    }
    with ext 
    show "(λl. sopen_option (Suc n) (Fvar s) (Fvar p) 
                 (sclose_option (Suc n) s p (f l))) = f" 
      by simp
  qed
next
  case (Bnd L t) note cof = this(2)
  show ?case
  proof (intro strip)
    fix n s p
    from ‹finite L› exFresh_s_p_cof[of "L ∪ FV t ∪ {s} ∪ {p}"]
    obtain sa pa where
      sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} 
             ∧ sa ≠ pa"
      by auto
    with cof
    have 
      eq: "{Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} (t⇗[Fvar sa, Fvar pa]⇖) 
           = (t⇗[Fvar sa, Fvar pa]⇖)" by blast

    {
      fix x assume "x ∉ FV t"
      from contra_subsetD[OF sclose_subset_FV this]
      have "x ∉ FV ({Suc n ← [s,p]} t)" by simp
      moreover assume "x ≠ p" and "x ≠ s"
      ultimately
      have "x ∉ FV ({Suc n ← [s,p]} t) ∪ FV (Fvar s) ∪ FV (Fvar p)"
        by simp
      from contra_subsetD[OF sopen_FV this]
      have "x ∉ FV ({Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} t)"
        by simp
    } with sapa
    have 
      "s ∉ FV (Fvar sa)" and "s ∉ FV (Fvar pa)" and
      "p ∉ FV (Fvar sa)" and "p ∉ FV (Fvar pa)" and
      "sa ∉ FV ({Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} t)" and
      "sa ∉ FV t" and
      "pa ∉ FV ({Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} t)" and
      "pa ∉ FV t" and "sa ≠ pa"
      by auto
(* proof:

{Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} (t⇗[Fvar sa,Fvar pa]⇖) 
= {Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} {0 → [Fvar sa,Fvar pa]} t
= {Suc n → [Fvar s,Fvar p]} {0 → [Fvar sa,Fvar pa]} {Suc n ← [s,p]} t
= {0 → [Fvar sa,Fvar pa]} {Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} t
= {0 → [Fvar sa,Fvar pa]} t
= (t⇗[Fvar sa,Fvar pa]⇖)
*)
    from
      eq
      sym[OF sopen_sclose_commute[OF not_sym[OF Suc_not_Zero[of n]] 
                                                this(1-4)]]
      sopen_commute[OF Suc_not_Zero[of n]]
      sopen_fresh_inj[OF _ this(5-9)]
    show "{Suc n → [Fvar s,Fvar p]} {Suc n ← [s,p]} t = t"
      by (auto simp: openz_def)
  qed
qed

lemma ssubst_sopen_distrib[rule_format]:
  "∀n s p t'. lc t' ⟶ [x → t'] {n → [s,p]} t 
   = {n → [[x → t']s, [x → t']p]} [x → t'] t"
proof -
  have
    "(∀n s p t'. lc t' 
       ⟶ [x → t'] {n → [s,p]} t = {n → [[x → t']s, [x → t']p]} [x → t'] t)
    &(∀n s p t'. lc t' 
       ⟶ ssubst_option x t' (sopen_option n s p u) 
           = sopen_option n ([x → t']s) ([x → t']p) (ssubst_option x t' u))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma ssubst_openz_distrib:
  "lc t' ⟹ [x → t'] (t⇗[s,p]⇖) = (([x → t'] t)⇗[[x → t'] s, [x → t'] p]⇖)"
  by (simp add: openz_def ssubst_sopen_distrib)

lemma ssubst_sopen_commute: "⟦ lc t'; x ∉ FV s; x ∉ FV p ⟧ 
  ⟹ [x → t'] {n → [s,p]} t = {n → [s,p]} [x → t'] t"
  by (frule ssubst_sopen_distrib[of t' x n s p t], simp)

lemma sopen_commute_gen:
  fixes s p s' p' n k t
  assumes "lc s" and "lc p" and "lc s'" and "lc p'" and "n ≠ k"
  shows "{n → [s,p]} {k → [s',p']} t = {k → [s',p']} {n → [s,p]} t"
proof -
  have "finite (FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t)" by auto
  from exFresh_s_p_cof[OF this]
  obtain sa pa where 
    "sa ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t 
    ∧ pa ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∧ sa ≠ pa" by auto
  moreover 
  hence "finite (FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa})" by auto
  from exFresh_s_p_cof[OF this]
  obtain sb pb where 
    "sb ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa} 
    ∧ pb ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa} 
    ∧ sb ≠ pb" by auto
  ultimately
  have
    "sa ∉ FV t" and "pa ∉ FV t" and "sb ∉ FV t" and "pb ∉ FV t" and
    "sa ∉ FV ({n → [s,p]} t)" and "pa ∉ FV ({n → [s,p]} t)" and
    "sb ∉ FV ({k → [s',p']} t)" and "pb ∉ FV ({k → [s',p']} t)" and

    "sa ≠ pa" and "sb ≠ pb" and "sb ≠ sa" and "sb ≠ pa" and 
    "pb ≠ sa" and "pb ≠ pa" and

    "sa ∉ FV s" and "sa ∉ FV p" and "pa ∉ FV s" and "pa ∉ FV p" and
    "sb ∉ FV s'" and "sb ∉ FV p'" and "pb ∉ FV s'" and "pb ∉ FV p'" and
    "sa ∉ FV p'" and "sb ∉ FV p" and

    "sa ∉ FV (Fvar sb)" and "sa ∉ FV (Fvar pb)" and
    "pa ∉ FV (Fvar sb)" and "pa ∉ FV (Fvar pb)" and
    "pb ∉ FV (Fvar sa)" and "pb ∉ FV (Fvar pa)" and
    "sb ∉ FV (Fvar sa)" and "sb ∉ FV (Fvar pa)" and

    "lc s" and "lc p" and "lc s'" and "lc p'"

    using contra_subsetD[OF sopen_FV] assms(1-4)
    by auto

(* proof:

{n → [s,p]} {k → [s',p']} t 
= {n → [s,p]} [sa → s'] [pa → p'] {k → [Fvar sa,Fvar pa]} t
= [sa → s'] [pa → p'] [pa → p'] {k → [Fvar sa,Fvar pa]} t
= [sb → s] [pb → p] {n → [Fvar sb,Fvar pb]} [sa → s'] [pa → p'] {k → [Fvar sa,Fvar pa]} t
= [sb → s] [pb → p] [sa → s'] {n → [Fvar sb,Fvar pb]} [pa → p'] {k → [Fvar sa,Fvar pa]} t
= [sb → s] [pb → p] [sa → s'] [pa → p'] {n → [Fvar sb,Fvar pb]} {k → [Fvar sa,Fvar pa]} t
= [sb → s] [pb → p] [sa → s'] [pa → p'] {k → [Fvar sa,Fvar pa]} {n → [Fvar sb,Fvar pb]} t
= [sb → s] [sa → s'] [pb → p] [pa → p'] {k → [Fvar sa,Fvar pa]} {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [sb → s] [pb → p] [pa → p'] {k → [Fvar sa,Fvar pa]} {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [sb → s] [pa → p'] [pb → p] {k → [Fvar sa,Fvar pa]} {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [pa → p'] [sb → s] [pb → p] {k → [Fvar sa,Fvar pa]} {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [pa → p'] [sb → s] {k → [Fvar sa,Fvar pa]} [pb → p] {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [pa → p'] {k → [Fvar sa,Fvar pa]} [sb → s] [pb → p] {n → [Fvar sb,Fvar pb]} t
= [sa → s'] [pa → p'] {k → [Fvar sa,Fvar pa]} {n → [s,p]} t
= {k → [s',p']} {n → [s,p]} t 
*)
  from 
    ssubst_intro[OF ‹sa ∉ FV t› ‹pa ∉ FV t› ‹sa ≠ pa› ‹sa ∉ FV p'›] 
    ssubst_intro[OF ‹sb ∉ FV ({k → [s',p']} t)› ‹pb ∉ FV ({k → [s',p']} t)› 
                    ‹sb ≠ pb› ‹sb ∉ FV p›]
    sym[OF ssubst_sopen_commute[OF ‹lc s'› 
                                   ‹sa ∉ FV (Fvar sb)› ‹sa ∉ FV (Fvar pb)›]]
    sym[OF ssubst_sopen_commute[OF ‹lc p'› 
                                   ‹pa ∉ FV (Fvar sb)› ‹pa ∉ FV (Fvar pb)›]]
    sopen_commute[OF ‹n ≠ k›]
    ssubst_commute[OF ‹pb ≠ sa› ‹pb ∉ FV s'› ‹sa ∉ FV p›]
    ssubst_commute[OF ‹sb ≠ sa› ‹sb ∉ FV s'› ‹sa ∉ FV s›]
    ssubst_commute[OF ‹pb ≠ pa› ‹pb ∉ FV p'› ‹pa ∉ FV p›]
    ssubst_commute[OF ‹sb ≠ pa› ‹sb ∉ FV p'› ‹pa ∉ FV s›]
    ssubst_sopen_commute[OF ‹lc s› ‹sb ∉ FV (Fvar sa)› ‹sb ∉ FV (Fvar pa)›] 
    ssubst_sopen_commute[OF ‹lc p› ‹pb ∉ FV (Fvar sa)› ‹pb ∉ FV (Fvar pa)›] 
    sym[OF ssubst_intro[OF ‹sb ∉ FV t› ‹pb ∉ FV t› ‹sb ≠ pb› ‹sb ∉ FV p›]] 
    sym[OF ssubst_intro[OF ‹sa ∉ FV ({n → [s,p]} t)› ‹pa ∉ FV ({n → [s,p]} t)›
                           ‹sa ≠ pa› ‹sa ∉ FV p'›]]
  show "{n → [s,p]} {k → [s',p']} t = {k → [s',p']} {n → [s,p]} t"
    by force
qed

lemma ssubst_preserves_lc[simp, rule_format]:
  fixes t
  assumes "lc t"
  shows "∀x t'. lc t' ⟶ lc ([x → t'] t)"
proof -
  define pred_cof
    where "pred_cof L t ⟷ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ lc (t⇗[Fvar s, Fvar p]⇖))" for L t

  {
    fix x v t
    assume 
      "lc v" and
      "∀x v. lc v ⟶ (∃L. finite L ∧ pred_cof L ([x → v] t))"
    hence
      "∃L. finite L ∧ pred_cof L ([x → v] t)"
        by auto
  }note Lex = this

  from assms show ?thesis
  proof 
    (induct
      taking: "λt. ∀x t'. lc t' ⟶ (∃L. finite L ∧ pred_cof L ([x → t'] t))"
      rule: lc_induct)
    case Fvar thus ?case by simp
  next
    case Call thus ?case by simp
  next
    case (Upd t l u) note pred_t = this(2) and pred_bnd = this(3)
    show ?case
    proof (intro strip)
      fix x t' assume "lc t'"
      note Lex[OF this pred_bnd] 
      from this[of x] 
      obtain L where "finite L" and "pred_cof L ([x → t'] u)"
        by auto
      with ‹lc t'› pred_t show "lc ([x → t'] Upd t l u)" 
        unfolding pred_cof_def
        by simp
    qed
  next
    case (Obj f T) note pred = this
    show ?case
    proof (intro strip)
      fix x t' assume "lc t'"
      define pred_fl where "pred_fl s p b l = lc ([x → t'] the b⇗[Fvar s, Fvar p]⇖)"
        for s p b and l::Label

      from ‹lc t'› fmap_ball_all2[OF pred]
      have "∀l∈dom f. ∃L. finite L ∧ pred_cof L ([x → t'] the(f l))"
        unfolding pred_cof_def
        by simp
      with fmap_ex_cof[of f pred_fl]
      obtain L where 
        "finite L" and "∀l∈dom f. pred_cof L ([x → t'] the(f l))"
        unfolding pred_cof_def pred_fl_def
        by auto
      with pred_ssubstoption_lem[of x t' f "pred_cof L"]
      show "lc ([x → t'] Obj f T)"
        unfolding pred_cof_def
        by simp
    qed
  next
    case (Bnd L t) note pred = this(2)
    show ?case
    proof (intro strip)
      fix x t' assume "lc t'"
      with ‹finite L› show "∃L. finite L ∧ pred_cof L ([x → t'] t)"
        unfolding pred_cof_def
      proof (
          rule_tac x = "L ∪ {x}" in exI, 
          intro conjI, simp, intro strip)
        fix s p assume sp: "s ∉ L ∪ {x} ∧ p ∉ L ∪ {x} ∧ s ≠ p"
        hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)"
          by auto
        from sp pred ‹lc t'›
        have "lc ([x → t'] (t⇗[Fvar s,Fvar p]⇖))"
          by blast
        with ssubst_sopen_commute[OF ‹lc t'› ‹x ∉ FV (Fvar s)› 
                                     ‹x ∉ FV (Fvar p)›]
        show "lc ([x → t'] t⇗[Fvar s,Fvar p]⇖)"
          by (auto simp: openz_def)
      qed
    qed
  qed
qed

lemma sopen_sclose_eq_ssubst: "⟦ sa ≠ pa; sa ∉ FV p; lc t ⟧ 
  ⟹ {n → [s,p]} {n ← [sa,pa]} t = [sa → s] [pa → p] t"
  by (rule_tac sa1 = sa and pa1 = pa and t1 = "{n ← [sa,pa]} t" 
    in ssubst[OF ssubst_intro], simp+)

lemma ssubst_sclose_commute[rule_format]:
  "∀x n s p t'. s ∉ FV t' ⟶ p ∉ FV t' ⟶ x ≠ s ⟶ x ≠ p 
     ⟶ [x → t'] {n ← [s,p]} t = {n ← [s,p]} [x → t'] t"
proof -
  have
    "(∀x n s p t'. s ∉ FV t' ⟶ p ∉ FV t' ⟶ x ≠ s ⟶ x ≠ p 
       ⟶ [x → t'] {n ← [s,p]} t = {n ← [s,p]} [x → t'] t)
    &(∀x n s p t'. s ∉ FV t' ⟶ p ∉ FV t' ⟶ x ≠ s ⟶ x ≠ p 
       ⟶ ssubst_option x t' (sclose_option n s p u) 
           = sclose_option n s p (ssubst_option x t' u))"
    by (rule compat_sterm_sterm_option.induct, simp_all split: bVariable.split)
  from conjunct1[OF this] show ?thesis by assumption
qed

lemma body_lc_FV: 
  fixes t s p
  assumes "body t"
  shows "lc (t⇗[Fvar s, Fvar p]⇖)"
proof -
  from assms 
  obtain L where 
    "finite L" and pred_sp: "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ lc (t⇗[Fvar s,Fvar p]⇖)"
    unfolding body_def by auto

  hence "finite (L ∪ FV t ∪ {s} ∪ {p})" by simp
  from exFresh_s_p_cof[OF this] obtain sa pa where sapa: 
    "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
    by auto
  hence "sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and "sa ∉ FV (Fvar p)" by auto
  from pred_sp sapa have "lc (t⇗[Fvar sa,Fvar pa]⇖)" by blast

  with 
    ssubst_intro[OF ‹sa ∉ FV t› ‹pa ∉ FV t› ‹sa ≠ pa› ‹sa ∉ FV (Fvar p)›] 
    ssubst_preserves_lc
  show "lc (t⇗[Fvar s,Fvar p]⇖)" by (auto simp: openz_def)
qed

lemma body_lc: 
  fixes t s p
  assumes "body t" and "lc s" and "lc p"
  shows "lc (t⇗[s, p]⇖)"
proof -
  have "finite (FV t ∪ FV p)" by simp
  from exFresh_s_p_cof[OF this] obtain sa pa where
    "sa ∉ FV t ∪ FV p ∧ pa ∉ FV t ∪ FV p ∧ sa ≠ pa" by auto
  hence "sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and "sa ∉ FV p" 
    by auto

  from body_lc_FV[OF ‹body t›] have lc: "lc (t⇗[Fvar sa,Fvar pa]⇖)"
    by assumption

  from
    ssubst_intro[OF ‹sa ∉ FV t› ‹pa ∉ FV t› ‹sa ≠ pa› ‹sa ∉ FV p›] 
    ssubst_preserves_lc[OF lc] ‹lc s› ‹lc p›
  show "lc (t⇗[s,p]⇖)" by (auto simp: openz_def)
qed

lemma lc_body: 
  fixes t s p
  assumes "lc t" and "s ≠ p"
  shows "body (σ[s,p] t)"
  unfolding body_def
proof 
  have 
    "∀sa pa. sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
      ⟶ lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖)"
  proof (intro strip)
    fix sa :: fVariable and pa :: fVariable
    assume "sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
    hence "s ∉ FV (Fvar pa)" by auto
    from 
      sopen_sclose_eq_ssubst[OF ‹s ≠ p› this ‹lc t›] 
      ssubst_preserves_lc[OF ‹lc t›]
    show "lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖)" by (simp add: openz_def closez_def)
  qed
  thus 
    "finite (FV t ∪ {s} ∪ {p}) 
     ∧ (∀sa pa. sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
         ⟶ lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖))" by simp
qed

lemma ssubst_preserves_lcE_lem[rule_format]:
  fixes t
  assumes "lc t"
  shows "∀x u t'. t = [x → u] t' ⟶ lc u ⟶ lc t'"
  using assms
proof 
  (induct
    taking: 
    "λt. ∀x u t'. t = [x → u] t' ⟶ lc u ⟶ body t'" 
    rule: lc_induct)
  case Fvar thus ?case by (intro strip, case_tac t', simp_all)
next
  case Call thus ?case by (intro strip, case_tac t', simp_all)
next
  case (Upd t l u) note pred_t = this(2) and pred_u = this(3) 
  show ?case
  proof (intro strip)
    fix x v t'' assume "Upd t l u = [x → v] t''" and "lc v"
    from this(1) have t'': "(∃t' u'. t'' = Upd t' l u') ∨ (t'' = Fvar x)"
    proof (cases t'', auto)
      fix y
      assume "Upd t l u = (if x = y then v else Fvar y)"
      thus "y = x" by (case_tac "y = x", auto)
    qed
    show "lc t''"
    proof (cases "t'' = Fvar x")
      case True thus ?thesis by simp
    next
      case False with ‹Upd t l u = [x → v] t''› t'' 
      show ?thesis
      proof (clarify)
        fix t' u' assume "Upd t l u = [x → v] Upd t' l u'"
        hence "t = [x → v] t'" and "u = [x → v] u'" 
          by auto
        with ‹lc v› pred_t pred_u lc_upd[of t' l u']
        show "lc (Upd t' l u')" by auto
      qed
    qed
  qed
next
  case (Obj f T) note pred = this
  show ?case
  proof (intro strip)
    fix x v t' assume "Obj f T = [x → v] t'" and "lc v"
    from this(1) have t': "(∃f'. t' = Obj f' T) ∨ (t' = Fvar x)"
    proof (cases t', auto)
      fix y :: fVariable
      assume "Obj f T = (if x = y then v else Fvar y)"
      thus "y = x" by (case_tac "y = x", auto)
    qed
    show "lc t'"
    proof (cases "t' = Fvar x")
      case True thus ?thesis by simp
    next
      case False with ‹Obj f T = [x → v] t'› t'
      show ?thesis
      proof (clarify)
        fix f' assume "Obj f T = [x → v] Obj f' T"
        hence
          ssubst: "∀l∈dom f. the(f l) = [x → v] the(f' l)" and
          "dom f = dom f'"
          by auto
        with pred ‹lc v› lc_obj[of f' T]
        show "lc (Obj f' T)"
          by auto
      qed
    qed
  qed
next
  case (Bnd L t) note pred = this(2)
  show ?case
  proof (intro strip)
    fix x v t' assume "t = [x → v] t'" and "lc v"
    from ‹finite L› exFresh_s_p_cof[of "L ∪ {x} ∪ FV t'"]
    obtain s p where 
      "s ∉ L" and "p ∉ L" and "s ≠ p" and
      "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" and
      "s ∉ FV t'" and "p ∉ FV t'"
      by auto
    from 
      ‹t = [x → v] t'›
      ssubst_sopen_commute[OF ‹lc v› ‹x ∉ FV (Fvar s)› ‹x ∉ FV (Fvar p)›]
    have "(t⇗[Fvar s, Fvar p]⇖) = [x → v] (t'⇗[Fvar s, Fvar p]⇖)"
      by (auto simp: openz_def)
    with 
      ‹s ∉ L› ‹p ∉ L› ‹s ≠ p› ‹lc v› pred
    have "lc (t'⇗[Fvar s, Fvar p]⇖)" by blast
    from 
      lc_body[OF this ‹s ≠ p›]
      sclose_sopen_eq_t[OF ‹s ∉ FV t'› ‹p ∉ FV t'› ‹s ≠ p›]
    show "body t'" by (auto simp: openz_def closez_def)
  qed
qed

lemma ssubst_preserves_lcE: "⟦ lc ([x → t'] t); lc t' ⟧ ⟹ lc t"
  by (drule_tac t = "[x → t'] t" and x = x and u = t' and t' = t 
    in ssubst_preserves_lcE_lem, simp+)

lemma obj_openz_lc: "⟦ lc (Obj f T); lc p; l ∈ dom f ⟧ ⟹ lc (the(f l)⇗[Obj f T, p]⇖)"
  by (rule_tac s = "Obj f T" and p = p in body_lc, (simp add: lc_obj)+)

lemma obj_insert_lc: 
  fixes f T t l
  assumes "lc (Obj f T)" and "body t"
  shows "lc (Obj (f(l ↦ t)) T)"
proof (rule ssubst[OF lc_obj], rule ballI)
  fix l' :: Label assume "l' ∈ dom (f(l ↦ t))"
  with assms show "body (the ((f(l ↦ t)) l'))"
    by (cases "l' = l", (auto simp: lc_obj))
qed

lemma ssubst_preserves_body[simp]:
  fixes t t' x
  assumes "body t" and "lc t'"
  shows "body ([x → t'] t)"
  unfolding body_def
proof -
  have 
    "∀s p. s ∉ FV t' ∪ {x} ∧ p ∉ FV t' ∪ {x} ∧ s ≠ p
      ⟶ lc ([x → t'] t⇗[Fvar s,Fvar p]⇖)"
  proof (intro strip)
    fix s :: fVariable and p :: fVariable
    from body_lc_FV[OF ‹body t›]
    have "lc ({0 → [Fvar s,Fvar p]} t)" by (simp add: openz_def)
    from ssubst_preserves_lc[OF this ‹lc t'›] 
    have "lc ([x → t'] (t⇗[Fvar s,Fvar p]⇖))" by (simp add: openz_def)

    moreover assume "s ∉ FV t' ∪ {x} ∧ p ∉ FV t' ∪ {x} ∧ s ≠ p"
    hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" by auto
    note ssubst_sopen_commute[OF ‹lc t'› this]
    ultimately
    show "lc ([x → t'] t⇗[Fvar s,Fvar p]⇖)" by (simp add: openz_def)
  qed
  thus 
    "∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                      ⟶ lc ([x → t'] t⇗[Fvar s,Fvar p]⇖))"
    by (rule_tac x = "FV t' ∪ {x}" in exI, simp)
qed

lemma sopen_preserves_body[simp]:
  fixes t s p
  assumes "body t" and "lc s" and "lc p"
  shows "body ({n → [s,p]} t)"
  unfolding body_def
proof -
  have 
    "∀sa pa. sa ∉ FV t ∪ FV s ∧ pa ∉ FV p ∧ sa ≠ pa
      ⟶ lc ({n → [s,p]} t⇗[Fvar sa,Fvar pa]⇖)"
  proof (cases "n = 0")
    case True thus ?thesis
      using body_lc[OF ‹body t› ‹lc s› ‹lc p›] sopen_twice[OF ‹lc s› ‹lc p›] 
      by (simp add: openz_def)
  next
    case False thus ?thesis
    proof (intro strip)
      fix sa :: fVariable and pa :: fVariable
      from body_lc_FV[OF ‹body t›] have "lc (t⇗[Fvar sa,Fvar pa]⇖)" by assumption
      moreover
      from sopen_commute_gen[OF _ _ ‹lc s› ‹lc p› not_sym[OF ‹n ≠ 0›]]
      have "{n → [s,p]} t⇗[Fvar sa,Fvar pa]⇖ = {n → [s,p]} (t⇗[Fvar sa,Fvar pa]⇖)"
        by (simp add: openz_def)
      ultimately show "lc ({n → [s,p]} t⇗[Fvar sa,Fvar pa]⇖)" by simp
    qed
  qed
  thus "∃L. finite L 
          ∧ (∀sa pa. sa ∉ L ∧ pa ∉ L ∧ sa ≠ pa 
              ⟶ lc ({n → [s,p]} t⇗[Fvar sa,Fvar pa]⇖))"
    by (rule_tac x = "FV t ∪ FV s ∪ FV p" in exI, simp)
qed

subsection ‹Beta-reduction›
inductive beta :: "[sterm, sterm] ⇒ bool" (infixl ‹→⇩β› 50)
where
  beta[simp, intro!]      : 
  "⟦ l ∈ dom f; lc (Obj f T); lc a ⟧ ⟹ Call (Obj f T) l a →⇩β (the (f l)⇗[(Obj f T), a]⇖)"
| beta_Upd[simp, intro!]  : 
  "⟦ l ∈ dom f; lc (Obj f T); body t ⟧ ⟹ Upd (Obj f T) l t →⇩β Obj (f(l ↦ t)) T" 
| beta_CallL[simp, intro!]: "⟦ t →⇩β t'; lc u ⟧ ⟹ Call t l u →⇩β Call t' l u"
| beta_CallR[simp, intro!]: "⟦ t →⇩β t'; lc u ⟧ ⟹ Call u l t →⇩β Call u l t'"
| beta_UpdL[simp, intro!] : "⟦ t →⇩β t'; body u ⟧ ⟹ Upd t l u →⇩β Upd t' l u"
| beta_UpdR[simp, intro!] : 
  "⟦ finite L; 
     ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β t''∧ t'= σ[s,p]t'');
     lc u ⟧ ⟹ Upd u l t →⇩β Upd u l t'"
| beta_Obj[simp, intro!]  : 
  "⟦ l ∈ dom f; finite L; 
     ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β t'' ∧ t'= σ[s,p]t'');
     ∀l∈dom f. body (the (f l)) ⟧ 
  ⟹ Obj (f(l ↦ t)) T →⇩β Obj (f(l ↦ t')) T"

inductive_cases beta_cases [elim!]:
  "Call s l t →⇩β u"
  "Upd s l t →⇩β u"
  "Obj s T  →⇩β t"

abbreviation
  beta_reds :: "[sterm, sterm] => bool"  (infixl ‹->>› 50) where
  "s ->> t == beta^** s t"
abbreviation
  beta_ascii :: "[sterm, sterm] => bool"  (infixl ‹->› 50) where
  "s -> t == beta s t"

notation (latex)
  beta_reds (infixl ‹→⇩β⇧*› 50)

lemma beta_induct[consumes 1, 
  case_names CallL CallR UpdL UpdR Upd Obj beta Bnd]:
  fixes 
  t :: sterm and t' :: sterm and 
  P1 :: "sterm ⇒ sterm ⇒ bool" and P2 :: "sterm ⇒ sterm ⇒ bool"
  assumes
  "t →⇩β t'" and
  "⋀t t' u l. ⟦ t →⇩β t'; P1 t t'; lc u ⟧ ⟹ P1 (Call t l u) (Call t' l u)" and
  "⋀t t' u l. ⟦ t →⇩β t'; P1 t t'; lc u ⟧ ⟹ P1 (Call u l t) (Call u l t')" and
  "⋀t t' u l. ⟦ t →⇩β t'; P1 t t'; body u⟧ ⟹ P1 (Upd t l u) (Upd t' l u)" and
  "⋀t t' u l. ⟦ P2 t t'; lc u ⟧ ⟹ P1 (Upd u l t) (Upd u l t')" and
  "⋀l f T t. ⟦ l ∈ dom f; lc (Obj f T); body t ⟧ 
      ⟹ P1 (Upd (Obj f T) l t) (Obj (f(l ↦ t)) T)" and
  "⋀l f t t' T. ⟦ l ∈ dom f; P2 t t'; ∀l∈dom f. body (the (f l)) ⟧
      ⟹ P1 (Obj (f(l ↦ t)) T) (Obj (f(l ↦ t')) T)" and
  "⋀l f T a. ⟦ l ∈ dom f; lc (Obj f T); lc a ⟧ 
      ⟹ P1 (Call (Obj f T) l a) (the (f l)⇗[Obj f T,a]⇖)" and
  "⋀L t t'. 
      ⟦ finite L; 
        ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
        ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β t'' 
                 ∧ P1 (t⇗[Fvar s,Fvar p]⇖) t'' ∧ t' = σ[s,p] t'') ⟧
      ⟹ P2 t t'"
  shows "P1 t t'"
  using assms by (induct rule: beta.induct, auto)

lemma Fvar_beta: "Fvar x →⇩β t ⟹ False"
  by (erule beta.cases, auto)

lemma Obj_beta: 
  assumes "Obj f T →⇩β z"
  shows
  "∃l f' t t'. dom f = dom f' ∧ f = (f'(l ↦ t)) ∧ l ∈ dom f' 
             ∧ (∃L. finite L 
                  ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
                      ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β t'' ∧ t'= σ[s,p]t'')))
             ∧ z = Obj (f'(l ↦ t')) T"
proof (cases rule: beta_cases(3)[OF assms])
  case (1 l fa L t t') thus ?thesis
    by (rule_tac x = l in exI, 
        rule_tac x = fa in exI,
        rule_tac x = t in exI,
        rule_tac x = t' in exI, auto)
qed

lemma Upd_beta: "Upd t l u →⇩β z ⟹
  (∃t'. t →⇩β t' ∧ z = Upd t' l u) 
  ∨(∃u' L. finite L 
         ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
             ⟶ (∃t''. (u⇗[Fvar s, Fvar p]⇖) →⇩β t'' ∧ u' = σ[s,p]t'')) 
         ∧ z = Upd t l u')
  ∨(∃f T. l ∈ dom f ∧ Obj f T = t ∧ z = Obj (f(l ↦ u)) T)"
  by (erule beta_cases, auto)

lemma Call_beta: "Call t l u →⇩β z ⟹
  (∃t'. t →⇩β t' ∧ z = Call t' l u) ∨ (∃u'. u →⇩β u' ∧ z = Call t l u')
  ∨(∃f T. Obj f T = t ∧ l ∈ dom f ∧ z = (the (f l)⇗[Obj f T, u]⇖))"
  by (erule beta_cases, auto)

subsubsection ‹Properties›
lemma beta_lc[simp]:
  fixes t t'
  assumes "t →⇩β t'"
  shows "lc t ∧ lc t'"
using assms
proof 
  (induct
    taking: "λt t'. body t ∧ body t'"
    rule: beta_induct)
  case CallL thus ?case by simp
next
  case CallR thus ?case by simp
next
  case UpdR thus ?case by (simp add: lc_upd)
next
  case UpdL thus ?case by (simp add: lc_upd)
next
  case beta thus ?case by (simp add: obj_openz_lc)
next
  case Upd thus ?case by (simp add: lc_obj lc_upd)
next
  case Obj thus ?case by (simp add: lc_obj)
next
  case (Bnd L t t') note cof = this(2)
  from ‹finite L› exFresh_s_p_cof[of "L ∪ FV t"]
  obtain s p where 
    "s ∉ L" and "s ∉ FV t" and "p ∉ L" and "p ∉ FV t" and "s ≠ p" 
    by auto  
  with cof obtain t'' where
    "lc (t⇗[Fvar s, Fvar p]⇖)" and "lc t''" and
    "t' = σ[s,p] t''" by auto
  from 
    lc_body[OF this(1) ‹s ≠ p›] 
    sclose_sopen_eq_t[OF ‹s ∉ FV t› ‹p ∉ FV t› ‹s ≠ p›]
    this(3) lc_body[OF this(2) ‹s ≠ p›]
  show ?case by (simp add: openz_def closez_def)
qed

lemma beta_ssubst[rule_format]:
  fixes t t'
  assumes "t →⇩β t'"
  shows "∀x v. lc v ⟶ [x → v] t →⇩β [x → v] t'"
proof -
  define pred_cof
    where "pred_cof L t t' ⟷
      (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. t⇗[Fvar s, Fvar p]⇖ →⇩β t'' ∧ t' = σ[s,p] t''))"
    for L t t'
  {
    fix x v t t'
    assume 
      "lc v" and
      "∀x v. lc v ⟶ (∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v] t'))"
    hence
      "∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v] t')"
        by auto
  }note Lex = this

  {
    fix x v l and f :: "Label ⇒ sterm option"
    assume "l ∈ dom f" hence "l ∈ dom (λl. ssubst_option x v (f l))"
      by simp
  }note domssubst = this
  {
    fix x v l T and f :: "Label ⇒ sterm option"
    assume "lc (Obj f T)" and "lc v" from ssubst_preserves_lc[OF this] 
    have obj: "lc (Obj (λl. ssubst_option x v (f l)) T)" by simp
  }note lcobj = this

  from assms show ?thesis
  proof 
    (induct
      taking: "λt t'. ∀x v. lc v 
                       ⟶ (∃L. finite L 
                              ∧ pred_cof L ([x → v] t) ([x → v] t'))"
      rule: beta_induct)
    case CallL thus ?case by simp
  next
    case CallR thus ?case by simp
  next
    case UpdL thus ?case by simp
  next
    case (UpdR t t' u l) note pred = this(1)
    show ?case
    proof (intro strip)
      fix x v assume "lc v"
      from Lex[OF this pred]
      obtain L where
        "finite L" and "pred_cof L ([x → v] t) ([x → v] t')"
        by auto
      with ssubst_preserves_lc[OF ‹lc u› ‹lc v›] 
      show "[x → v] Upd u l t →⇩β [x → v] Upd u l t'"
        unfolding pred_cof_def
        by auto
    qed
  next
    case (beta l f T t) thus ?case
    proof (intro strip, simp)
      fix x v assume "lc v"
      from ssubst_preserves_lc[OF ‹lc t› this] have "lc ([x → v] t)" 
        by simp
      note lem =
        beta.beta[OF domssubst[OF ‹l ∈ dom f›] 
        lcobj[OF ‹lc (Obj f T)› ‹lc v›] this]

      from ‹l ∈ dom f› have "the (ssubst_option x v (f l)) = [x → v] the (f l)"
        by auto
      with lem[of x] ssubst_openz_distrib[OF ‹lc v›]
      show
        "Call (Obj (λl. ssubst_option x v (f l)) T) l ([x → v] t)
         →⇩β [x → v] (the (f l)⇗[Obj f T, t]⇖)"
        by simp
    qed
  next
    case (Upd l f T t) thus ?case
    proof (intro strip, simp)
      fix x v assume "lc v"
      from ssubst_preserves_body[OF ‹body t› ‹lc v›] have "body ([x → v] t)" 
        by simp
      from
        beta.beta_Upd[OF domssubst[OF ‹l ∈ dom f›] 
                         lcobj[OF ‹lc (Obj f T)› ‹lc v›] this]
        ssubstoption_insert[OF ‹l ∈ dom f›] 
      show
        "Upd (Obj (λl. ssubst_option x v (f l)) T) l ([x → v] t)
         →⇩β Obj (λla. ssubst_option x v (if la = l then Some t else f la)) T"
        by simp
    qed
  next
    case (Obj l f t t' T) note pred = this(2)
    show ?case
    proof (intro strip, simp)
      fix x v assume "lc v"
      note Lex[OF this pred]
      from this[of x] obtain L where
        "finite L" and "pred_cof L ([x → v] t) ([x → v] t')"
        by auto
      have "∀l∈dom (λl. ssubst_option x v (f l)). body (the (ssubst_option x v (f l)))"
      proof (intro strip, simp)
        fix l' :: Label assume "l' ∈ dom f"
        with ‹∀l∈dom f. body (the(f l))› have "body (the (f l'))" by blast
        note ssubst_preserves_body[OF this ‹lc v›]
        with ‹l' ∈ dom f› ssubst_option_lem
        show "body (the (ssubst_option x v (f l')))" by auto
      qed
      from
        beta.beta_Obj[OF domssubst[OF ‹l ∈ dom f›] ‹finite L› _ this] 
        ssubstoption_insert[OF ‹l ∈ dom f›] ‹pred_cof L ([x → v] t) ([x → v] t')›
      show 
        "Obj (λla. ssubst_option x v (if la = l then Some t else f la)) T
         →⇩β Obj (λla. ssubst_option x v (if la = l then Some t' else f la)) T"
        unfolding pred_cof_def
        by simp
    qed
  next
    case (Bnd L t t') note pred = this(2)
    show ?case
    proof (intro strip)
      fix x v assume "lc v"
      from ‹finite L›
      show "∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v] t')"
      proof (rule_tac x = "L ∪ {x} ∪ FV v" in exI, 
          unfold pred_cof_def, auto)
        fix s p assume "s ∉ L" and "p ∉ L" and "s ≠ p"
        with pred ‹lc v› obtain t'' where
          "t⇗[Fvar s,Fvar p]⇖ →⇩β t''" and
          ssubst_beta: "[x → v] (t⇗[Fvar s,Fvar p]⇖) →⇩β [x → v] t''" and
          "t' = σ[s,p] t''"
          by blast
        assume "s ≠ x" and "p ≠ x"
        hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" by auto
        from ssubst_sopen_commute[OF ‹lc v› this] ssubst_beta
        have "[x → v] t⇗[Fvar s,Fvar p]⇖ →⇩β [x → v] t''" 
          by (simp add: openz_def)
        moreover
        assume "s ∉ FV v" and "p ∉ FV v"
        from 
          ssubst_sclose_commute[OF this not_sym[OF ‹s ≠ x›] 
                                        not_sym[OF ‹p ≠ x›]] 
          ‹t' = σ[s,p] t''›
        have "[x → v] t' = σ[s,p] [x → v] t''" 
          by (simp add: closez_def)
        ultimately
        show "∃t''. [x → v] t⇗[Fvar s,Fvar p]⇖ →⇩β t'' ∧ [x → v] t' = σ[s,p] t''" 
          by (rule_tac x = "[x → v] t''" in exI, simp)
      qed
    qed
  qed
qed

declare if_not_P [simp] not_less_eq [simp]
  ― ‹don't add @{text "r_into_rtrancl[intro!]"}›

lemma beta_preserves_FV[simp, rule_format]:
  fixes t t' x
  assumes "t →⇩β t'"
  shows "x ∉ FV t ⟶ x ∉ FV t'"
using assms
proof 
  (induct
    taking: "λt t'. x ∉ FV t ⟶ x ∉ FV t'"
    rule: beta_induct)
  case CallL thus ?case by simp
next
  case CallR thus ?case by simp
next
  case UpdL thus ?case by simp
next
  case UpdR thus ?case by simp
next
  case Upd thus ?case by simp
next
  case Obj thus ?case by simp
next
  case (beta l f T t) thus ?case
  proof (intro strip)
    assume "x ∉ FV (Call (Obj f T) l t)"
    with ‹l ∈ dom f› have "x ∉ FV (the (f l)) ∪ FV (Obj f T) ∪ FV t"
    proof (auto)
      fix y :: sterm
      assume "x ∈ FV y" and "f l = Some y"
      hence "x ∈ FVoption (f l)"
        by auto
      moreover assume "∀l∈dom f. x ∉ FVoption (f l)"
      ultimately show False using ‹l ∈ dom f›
        by blast
    qed
    from contra_subsetD[OF sopen_FV this]
    show "x ∉ FV (the (f l)⇗[Obj f T,t]⇖)" by (simp add: openz_def)
  qed
next
  case (Bnd L t t') thus ?case
  proof (intro strip)
    assume "x ∉ FV t"
    from ‹finite L› exFresh_s_p_cof[of "L ∪ {x}"]
    obtain s p where sp: "s ∉ L ∪ {x} ∧ p ∉ L ∪ {x} ∧ s ≠ p" by auto
    with ‹x ∉ FV t› sopen_FV[of 0 "Fvar s" "Fvar p" t]
    have "x ∉ FV (t⇗[Fvar s, Fvar p]⇖)" by (auto simp: openz_def)
    with sp Bnd(2) obtain t'' where
      "x ∉ FV t''" and "t' = σ[s,p] t''" 
      by auto
    with sclose_subset_FV[of 0 s p t''] show "x ∉ FV t'" 
      by (auto simp: closez_def)
  qed
qed

lemma rtrancl_beta_lc[simp, rule_format]: "t →⇩β⇧* t' ⟹ t ≠ t' ⟶ lc t ∧ lc t'"
  by (erule rtranclp.induct, simp, 
      drule beta_lc, blast)

lemma rtrancl_beta_lc2[simp]: "⟦ t →⇩β⇧* t'; lc t ⟧ ⟹ lc t'"
  by (case_tac "t = t'", simp+)

lemma rtrancl_beta_body:
  fixes L t t'
  assumes 
  "finite L" and
  "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
    ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'' ∧ t' = σ[s,p] t'')" and
  "body t"
  shows "body t'"
proof (cases "t = t'")
  case True with assms(3) show ?thesis by simp
next
  from exFresh_s_p_cof[OF ‹finite L›] 
  obtain s p where sp: "s ∉ L ∧ p ∉ L ∧ s ≠ p" by auto
  hence "s ≠ p" by simp

  from assms(2) sp
  obtain t'' where "t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t''" and "t' = σ[s,p] t''" 
    by auto
  with ‹body t› have "lc t''"
  proof (cases "(t⇗[Fvar s,Fvar p]⇖) = t''")
    case True with body_lc[OF ‹body t›] show "lc t''" by auto
  next
    case False with rtrancl_beta_lc[OF ‹t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t''›] 
    show "lc t''" by auto
  qed
  from lc_body[OF this ‹s ≠ p›] ‹t' = σ[s,p] t''› show "body t'" by simp
qed

lemma rtrancl_beta_preserves_FV[simp, rule_format]: 
  "t →⇩β⇧* t' ⟹ x ∉ FV t ⟶ x ∉ FV t'"
proof (induct t t' rule: rtranclp.induct, simp)
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (clarify)
    assume "x ∉ FV b" and "x ∈ FV c"
    from beta_preserves_FV[OF ‹b →⇩β c› this(1)] this(2)
    show False by simp
  qed
qed

subsubsection ‹Congruence rules›
lemma rtrancl_beta_CallL [intro!, rule_format]:
  "⟦ t →⇩β⇧* t'; lc u ⟧ ⟹ Call t l u →⇩β⇧* Call t' l u"
proof (induct t t' rule: rtranclp.induct, simp)
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (auto)
    from ‹b →⇩β c› ‹lc u› have "Call b l u →⇩β Call c l u" by simp
    with rtrancl_into_rtrancl(2)[OF ‹lc u›]
    show "Call a l u →⇩β⇧* Call c l u" by auto
  qed
qed

lemma rtrancl_beta_CallR [intro!, rule_format]:
  "⟦ t →⇩β⇧* t'; lc u ⟧ ⟹ Call u l t →⇩β⇧* Call u l t'"
proof (induct t t' rule: rtranclp.induct, simp)
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (auto)
    from ‹b →⇩β c› ‹lc u› have "Call u l b →⇩β Call u l c" by simp
    with rtrancl_into_rtrancl(2)[OF ‹lc u›]
    show "Call u l a →⇩β⇧* Call u l c" by auto
  qed
qed

lemma rtrancl_beta_Call [intro!, rule_format]:
  "⟦ t →⇩β⇧* t'; lc t; u →⇩β⇧* u'; lc u ⟧ 
  ⟹ Call t l u →⇩β⇧* Call t' l u'"
proof (induct t t' rule: rtranclp.induct, blast)
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (auto)
    from ‹u →⇩β⇧* u'› ‹lc u› have "lc u'" by auto
    with ‹b →⇩β c› have "Call b l u' →⇩β Call c l u'" by simp
    with rtrancl_into_rtrancl(2)[OF ‹lc a› ‹u →⇩β⇧* u'› ‹lc u›]
    show "Call a l u →⇩β⇧* Call c l u'" by auto
  qed
qed

lemma rtrancl_beta_UpdL:
  "⟦ t →⇩β⇧* t'; body u ⟧ ⟹ Upd t l u →⇩β⇧* Upd t' l u"
proof (induct t t' rule: rtranclp.induct, simp)
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (auto)
    from ‹b →⇩β c› ‹body u› have "Upd b l u →⇩β Upd c l u" by simp
    with rtrancl_into_rtrancl(2)[OF ‹body u›]
    show "Upd a l u →⇩β⇧* Upd c l u" by auto
  qed
qed

lemma beta_binder[rule_format]:
  fixes t t'
  assumes "t →⇩β t'"
  shows 
  "∀L s p. finite L ⟶ s ∉ L ⟶ p ∉ L ⟶ s ≠ p 
    ⟶ (∃L'. finite L' ∧ (∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
                            ⟶ (∃t''. (σ[s,p] t)⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' 
                                     ∧ σ[s,p] t' = σ[sa,pa] t'')))"
proof (intro strip)
  fix L :: "fVariable set" and s :: fVariable and p :: fVariable
  assume "s ≠ p"
  have 
    "∀sa pa. sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
      ⟶ (∃t''. (σ[s,p] t)⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' ∧ σ[s,p] t' = σ[sa,pa] t'')"
  proof (intro strip)
    fix sa :: fVariable and pa :: fVariable
    from beta_ssubst[OF ‹t →⇩β t'›] 
    have "[p → Fvar pa] t →⇩β [p → Fvar pa] t'" by simp
    from beta_ssubst[OF this] 
    have 
      betasubst: "[s → Fvar sa] [p → Fvar pa] t →⇩β [s → Fvar sa] [p → Fvar pa] t'" 
      by simp

    from beta_lc[OF ‹t →⇩β t'›] have "lc t" and "lc t'" by auto

    assume 
      sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
    hence "s ∉ FV (Fvar pa)" by auto
    from 
      sopen_sclose_eq_ssubst[OF ‹s ≠ p› this ‹lc t›] 
      sopen_sclose_eq_ssubst[OF ‹s ≠ p› this ‹lc t'›]
      betasubst
    have "σ[s,p] t⇗[Fvar sa, Fvar pa]⇖ →⇩β (σ[s,p] t'⇗[Fvar sa, Fvar pa]⇖)"
      by (simp add: openz_def closez_def)

    moreover
    {
      from sapa have "sa ∉ FV t" by simp
      from 
        contra_subsetD[OF sclose_subset_FV 
                          beta_preserves_FV[OF ‹t →⇩β t'› this]] 
      have "sa ∉ FV (σ[s,p] t')" by (simp add: closez_def)
      moreover
      from sapa have "pa ∉ FV t" by simp
      from 
        contra_subsetD[OF sclose_subset_FV 
                          beta_preserves_FV[OF ‹t →⇩β t'› this]]
      have "pa ∉ FV (σ[s,p] t')" by (simp add: closez_def)
      ultimately
      have "sa ∉ FV (σ[s,p] t')" and "pa ∉ FV (σ[s,p] t')" and "sa ≠ pa" 
        using sapa
        by auto
      note sym[OF sclose_sopen_eq_t[OF this]]
    }
    ultimately
    show 
      "∃t''. σ[s,p] t⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' ∧ σ[s,p] t' = σ[sa,pa] t''" 
      by (auto simp: openz_def closez_def)
  qed
  moreover assume "finite L"
  ultimately
  show 
    "∃L'. finite L' ∧ (∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa 
                        ⟶ (∃t''. σ[s,p] t⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' 
                                 ∧ σ[s,p] t' = σ[sa,pa] t''))"
    by (rule_tac x = "L ∪ FV t ∪ {s} ∪ {p}" in exI, simp)
qed

lemma rtrancl_beta_UpdR:
  fixes L t t' u l
  assumes 
  "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
    ⟶ (∃t''. (t⇗[Fvar s, Fvar p]⇖) →⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
  "finite L" and "lc u"
  shows "Upd u l t →⇩β⇧* Upd u l t'"
proof -
  from ‹finite L› have "finite (L ∪ FV t)" by simp
  from exFresh_s_p_cof[OF this]
  obtain s p where sp: "s ∉ L ∪ FV t ∧ p ∉ L ∪ FV t ∧ s ≠ p" by auto
  with assms(1) obtain t'' where "t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t''" and t': "t' = σ[s,p] t''" 
    by auto
  with ‹lc u› have "Upd u l t →⇩β⇧* Upd u l σ[s,p] t''"
  proof (erule_tac rtranclp_induct)
    from sp have "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" by auto
    from sclose_sopen_eq_t[OF this] 
    show "Upd u l t →⇩β⇧* Upd u l (σ[s,p](t⇗[Fvar s,Fvar p]⇖))" 
      by (simp add: openz_def closez_def)
  next
    fix y :: sterm and z :: sterm
    assume "y →⇩β z"
    from sp have "s ∉ L" and "p ∉ L" and "s ≠ p" by auto
    from beta_binder[OF ‹y →⇩β z› ‹finite L› this]
    obtain L' where 
      "finite L'" and
      "∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
        ⟶ (∃t''. σ[s,p] y⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' ∧ σ[s,p] z = σ[sa,pa] t'')"
      by auto
    from beta.beta_UpdR[OF this ‹lc u›]
    have "Upd u l (σ[s,p] y) →⇩β Upd u l (σ[s,p] z)" by assumption
    moreover assume "Upd u l t →⇩β⇧* Upd u l (σ[s,p] y)"
    ultimately show "Upd u l t →⇩β⇧* Upd u l (σ[s,p] z)" by simp
  qed
  with t' show "Upd u l t →⇩β⇧* Upd u l t'" by simp
qed

lemma rtrancl_beta_Upd: 
  "⟦ u →⇩β⇧* u'; finite L; 
     ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
      ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'' ∧ t' = σ[s,p]t'');
     lc u; body t ⟧
  ⟹ Upd u l t →⇩β⇧* Upd u' l t'"
proof (induct u u' rule: rtranclp.induct)
  case rtrancl_refl thus ?case by (simp add: rtrancl_beta_UpdR)
next
  case (rtrancl_into_rtrancl a b c) thus ?case
  proof (auto)
    from rtrancl_beta_body[OF ‹finite L› rtrancl_into_rtrancl(5) ‹body t›] ‹b →⇩β c›
    have "Upd b l t' →⇩β Upd c l t'" by simp
    with rtrancl_into_rtrancl(2)[OF ‹finite L› rtrancl_into_rtrancl(5) ‹lc a› ‹body t›]
    show "Upd a l t →⇩β⇧* Upd c l t'" by simp
  qed
qed

lemma rtrancl_beta_obj: 
  fixes l f L T t t'
  assumes 
  "l ∈ dom f" and "finite L" and
  "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
    ⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
  "∀l∈dom f. body (the(f l))" and "body t"
  shows "Obj (f (l ↦ t)) T →⇩β⇧* Obj (f (l ↦ t')) T"
proof -
  from ‹finite L› have "finite (L ∪ FV t)" by simp
  from exFresh_s_p_cof[OF this]
  obtain s p where sp: "s ∉ L ∪ FV t ∧ p ∉ L ∪ FV t ∧ s ≠ p" by auto
  with assms(3) obtain t'' where "t⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t''" and "t' = σ[s,p] t''" 
    by auto
  with ‹l ∈ dom f› ‹∀l∈dom f. body (the(f l))› 
  have "Obj (f(l ↦ t)) T →⇩β⇧* Obj (f(l ↦ σ[s,p] t'')) T"
  proof (erule_tac rtranclp_induct)
    from sp have "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" by auto
    from sclose_sopen_eq_t[OF this] 
    show "Obj (f(l ↦ t)) T →⇩β⇧* Obj (f(l ↦ σ[s,p] (t⇗[Fvar s,Fvar p]⇖))) T" 
      by (simp add: openz_def closez_def)
  next
    fix y :: sterm and z :: sterm assume "y →⇩β z"
    from sp have "s ∉ L" and "p ∉ L" and "s ≠ p" by auto
    from beta_binder[OF ‹y →⇩β z› ‹finite L› this]
    obtain L' where 
      "finite L'" and
      "∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
        ⟶ (∃t''. σ[s,p] y⇗[Fvar sa,Fvar pa]⇖ →⇩β t'' ∧ σ[s,p] z = σ[sa,pa] t'')"
      by auto
    from beta.beta_Obj[OF ‹l ∈ dom f› this ‹∀l∈dom f. body (the(f l))›]
    have "Obj (f(l ↦ σ[s,p] y)) T →⇩β Obj (f(l ↦ σ[s,p] z)) T"
      by assumption
    moreover assume "Obj (f(l ↦ t)) T →⇩β⇧* Obj (f(l ↦ σ[s,p] y)) T"
    ultimately
    show "Obj (f(l ↦ t)) T →⇩β⇧* Obj (f(l ↦ σ[s,p] z)) T" by simp
  qed
  with ‹t' = σ[s,p] t''› show "Obj (f(l ↦ t)) T →⇩β⇧* Obj (f(l ↦ t')) T" 
    by simp
qed

lemma obj_lem: 
  fixes l f T L t'
  assumes 
  "l ∈ dom f" and "finite L" and
  "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
    ⟶ (∃t''. ((the(f l))⇗[Fvar s,Fvar p]⇖) →⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
  "∀l∈dom f. body (the(f l))"
  shows "Obj f T →⇩β⇧* Obj (f(l ↦ t')) T"
proof 
  (rule_tac P = "λy. Obj y T →⇩β⇧* Obj (f(l ↦ t')) T" and s = "(f(l ↦ the(f l)))" 
    in subst)
  from ‹l ∈ dom f› fun_upd_idem show "f(l ↦ the (f l)) = f" by force
next
  from ‹l ∈ dom f› ‹∀l∈dom f. body (the(f l))› have "body (the (f l))" 
    by blast
  with 
    rtrancl_beta_obj[OF ‹l ∈ dom f› ‹finite L› assms(3) ‹∀l∈dom f. body (the(f l))›]
  show "Obj (f(l ↦ the (f l))) T →⇩β⇧* Obj (f(l ↦ t')) T" by simp
qed

lemma rtrancl_beta_obj_lem00: 
  fixes L f g
  assumes 
  "finite L" and
  "∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
               ⟶ (∃t''. ((the(f l))⇗[Fvar s, Fvar p]⇖) →⇩β⇧* t'' 
                        ∧ the(g l) = σ[s,p]t'')" and
  "dom f = dom g" and "∀l∈dom f. body (the (f l))"
  shows 
  "∀k ≤ (card (dom f)). 
    (∃ob. length ob = (k + 1)
        ∧ (∀obi. obi ∈ set ob ⟶ dom (fst(obi)) = dom f ∧ ((snd obi) ⊆ dom f)) 
        ∧ (fst (ob!0) = f)
        ∧ (card (snd (ob!k)) = k)
        ∧ (∀i < k. snd (ob!i) ⊂ snd (ob!k))
        ∧ (Obj (fst (ob!0)) T →⇩β⇧* Obj (fst (ob!k)) T)
        ∧ (card (snd (ob!k)) = k 
           ⟶ (Ltake_eq (snd (ob!k)) (fst (ob!k)) g)
                ∧ (Ltake_eq ((dom f) - (snd (ob!k))) (fst (ob!k)) f)))"
proof
  fix k :: nat
  show 
    "k ≤ card (dom f) 
    ⟶ (∃ob. length ob = k + 1 
            ∧ (∀obi. obi ∈ set ob ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f) 
            ∧ fst (ob ! 0) = f 
            ∧ card (snd (ob ! k)) = k 
            ∧ (∀i<k. snd (ob ! i) ⊂ snd (ob ! k)) 
            ∧ Obj (fst (ob ! 0)) T →⇩β⇧* Obj (fst (ob ! k)) T 
            ∧ (card (snd (ob ! k)) = k 
               ⟶ Ltake_eq (snd (ob ! k)) (fst (ob ! k)) g 
                   ∧ Ltake_eq (dom f - snd (ob ! k)) (fst (ob ! k)) f))"
  proof (induct k)
    case 0 thus ?case
    by (simp, rule_tac x = "[(f,{})]" in exI, simp add: Ltake_eq_def)
  next
    case (Suc k) thus ?case
    proof (clarify)
      assume "Suc k ≤ card (dom f)" hence "k < card (dom f)" by arith
      with Suc.hyps
      obtain ob where 
        "length ob = k + 1" and
        mem_ob: "∀obi. obi ∈ set ob 
                  ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f" and
        "fst (ob ! 0) = f" and
        "card (snd (ob ! k)) = k" and
        "∀i<k. snd (ob ! i) ⊂ snd (ob ! k)" and
        "Obj (fst (ob ! 0)) T →⇩β⇧* Obj (fst (ob ! k)) T" and
        card_k: "card (snd (ob ! k)) = k 
                 ⟶ Ltake_eq (snd (ob ! k)) (fst (ob ! k)) g 
                     ∧ Ltake_eq (dom f - snd (ob ! k)) (fst (ob ! k)) f"
        by auto
      from ‹length ob = k + 1› have obkmem: "(ob!k) ∈ set ob" by auto

      with mem_ob have obksnd: "snd(ob!k) ⊆ dom f" by blast
      from 
        card_psubset[OF finite_dom_fmap this] ‹card (snd(ob!k)) = k› 
        ‹k < card (dom f)›
      have "snd (ob!k) ⊂ dom f" by simp
      then obtain l' where "l' ∈ dom f" and "l' ∉ snd (ob!k)" by auto

      from obkmem mem_ob have obkfst: "dom (fst(ob!k)) = dom f" by blast 

        (* get witness *)
      define ob' where "ob' = ob @ [((fst(ob!k))(l' ↦ the (g l')), insert l' (snd(ob!k)))]"

      from nth_fst[OF ‹length ob = k + 1›] have first: "ob'!0 = ob!0" 
        by (simp add: ob'_def)

      from ‹length ob = k + 1› nth_last[of ob "Suc k"]
      have last: "ob'!Suc k = ((fst(ob!k))(l' ↦ the (g l')), insert l' (snd(ob!k)))"
        by (simp add: ob'_def)

      from ‹length ob = k + 1› nth_append[of ob _ k] have kth: "ob'!k = ob!k"
        by (auto simp: ob'_def)

      from ‹card (snd(ob!k)) = k› card_k
      have ass:
        "∀l∈(snd(ob!k)). fst(ob!k) l = g l"
        "∀l∈(dom f - snd(ob!k)). fst(ob!k) l = f l"
        by (auto simp: Ltake_eq_def)


        (* prop#1 *)
      from ‹length ob = k + 1› have "length ob' = Suc k + 1" 
        by (auto simp: ob'_def)

        (* prop#2 *)
      moreover
      have "∀obi. obi ∈ set ob' ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
        unfolding ob'_def
      proof (intro strip)
        fix obi :: "(Label -~> sterm) × (Label set)"
        assume "obi ∈ set (ob @ [((fst(ob!k))(l' ↦ the (g l')), insert l' (snd (ob!k)))])"
        note mem_append_lem'[OF this]
        thus "dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
        proof (rule disjE, simp_all)
          assume "obi ∈ set ob" 
          with mem_ob show "dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
            by blast
        next
          from obkfst obksnd ‹l' ∈ dom f›
          show 
            "insert l' (dom (fst (ob!k))) = dom f 
             ∧ l' ∈ dom f ∧ snd(ob!k) ⊆ dom f" 
            by blast
        qed
      qed

        (* prop#3 *)
      moreover 
      from first ‹fst(ob!0) = f› have "fst(ob'!0) = f" by simp

        (* prop#4 *)
      moreover
      from obksnd finite_dom_fmap finite_subset 
      have "finite (snd (ob!k))" by auto
      from card.insert_remove[OF this]
      have "card (insert l' (snd (ob!k))) = Suc (card (snd(ob!k) - {l'}))" 
        by simp
      with ‹l' ∉ snd (ob!k)› ‹card (snd(ob!k)) = k› last
      have "card(snd(ob'!Suc k)) = Suc k" by auto

        (* prop#5 *)
      moreover
      have "∀i<Suc k. snd (ob'!i) ⊂ snd (ob'!Suc k)"
      proof (intro strip)
        fix i :: nat
        from last have "snd(ob'!Suc k) = insert l' (snd (ob!k))" by simp
        with ‹l' ∉ snd (ob!k)› have "snd(ob!k) ⊂ snd(ob'!Suc k)" by auto
        moreover
        assume "i < Suc k"
        with ‹length ob = k + 1› have "i < length ob" by simp
        with nth_append[of ob _ i] have "ob'!i = ob!i" by (simp add: ob'_def)
        ultimately show "snd(ob'!i) ⊂ snd(ob'!Suc k)"
        proof (cases "i < k")
          case True 
          with 
            ‹∀i<k. snd(ob!i) ⊂ snd(ob!k)› ‹ob'!i = ob!i› 
            ‹snd(ob!k) ⊂ snd(ob'!Suc k)›
          show "snd (ob'!i) ⊂ snd (ob'!Suc k)" by auto
        next
          case False with ‹i < Suc k› have "i = k" by arith
          with ‹ob'!i = ob!i› ‹snd(ob!k) ⊂ snd(ob'!Suc k)›
          show "snd (ob'!i) ⊂ snd (ob'!Suc k)" by auto
        qed
      qed

        (* prop#6 -- the main statement *)
      moreover
      {
        from ‹l' ∈ dom f› ‹l' ∉ snd(ob!k)› have "l' ∈ (dom f - snd(ob!k))" 
          by auto
        with ass have "the(fst(ob!k) l') = the(f l')" by auto 
        with ‹l' ∈ dom f› assms(2)
        have 
          sp: "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p 
                ⟶ (∃t''. the(fst(ob!k) l')⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'' 
                         ∧ the (g l') = σ[s,p] t'')"
          by simp

        moreover
        have "∀l∈dom (fst(ob!k)). body (the(fst(ob!k) l))"
        proof (intro strip)
          fix la :: Label
          assume "la ∈ dom (fst(ob!k))"
          with obkfst have inf: "la ∈ dom f" by auto
          with assms(4) have bodyf: "body (the(f la))" by auto
          show "body (the(fst(ob!k) la))"
          proof (cases "la ∈ snd(ob!k)")
            case False with inf have "la ∈ (dom f - snd(ob!k))" by auto
            with ass have "fst(ob!k) la = f la" by blast
            with bodyf show "body (the (fst(ob!k) la))" by auto
          next
            from exFresh_s_p_cof[OF ‹finite L›]
            obtain s p where "s ∉ L ∧ p ∉ L ∧ s ≠ p" by auto
            with assms(2) inf
            obtain t' where 
              "the (f la)⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'" and
              "the (g la) = σ[s,p] t'" by blast
            from body_lc[OF bodyf] have lcf: "lc (the (f la)⇗[Fvar s,Fvar p]⇖)" by auto
            hence bodyg: "body (the(g la))"
            proof (cases "(the (f la)⇗[Fvar s,Fvar p]⇖) = t'")
              case True 
              with 
                lcf lc_body ‹s ∉ L ∧ p ∉ L ∧ s ≠ p› 
                ‹the(g la) = σ[s,p] t'›
              show "body (the(g la))" by auto
            next
              case False 
              with 
                rtrancl_beta_lc[OF ‹the (f la)⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'›] 
                lc_body ‹s ∉ L ∧ p ∉ L ∧ s ≠ p› ‹the(g la) = σ[s,p] t'›
              show "body (the(g la))" by auto
            qed
            case True with ass bodyg show "body (the(fst(ob!k) la))" by simp
          qed
        qed

        moreover
        from ‹l' ∈ dom f› obkfst have "l' ∈ dom(fst(ob!k))" by auto
        note obj_lem[OF this ‹finite L›]

        ultimately
        have "Obj (fst(ob!k)) T →⇩β⇧* Obj ((fst(ob!k))(l' ↦ the (g l'))) T"
          by blast

        moreover
        from last have "fst(ob'!Suc k) = (fst(ob!k))(l' ↦ the (g l'))"
          by auto

        ultimately
        have "Obj (fst(ob'!0)) T →⇩β⇧* Obj (fst(ob'!Suc k)) T"
          using 
            rtranclp_trans[OF ‹Obj (fst (ob!0)) T →⇩β⇧* Obj (fst (ob!k)) T›] first kth
          by auto
      }

        (* prop#7 *)
      moreover
      from ‹l' ∈ dom f› ‹dom f = dom g›
      have 
        "card (snd(ob'!Suc k)) = Suc k 
         ⟶ Ltake_eq (snd (ob'!Suc k)) (fst (ob'!Suc k)) g 
             ∧ Ltake_eq (dom f - snd(ob'!Suc k)) (fst(ob'!Suc k)) f"
        by (auto simp: Ltake_eq_def last ass)
      
      ultimately
      show 
        "∃ob. length ob = Suc k + 1 
            ∧ (∀obi. obi ∈ set ob ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f) 
            ∧ fst (ob ! 0) = f 
            ∧ card (snd (ob ! Suc k)) = Suc k 
            ∧ (∀i<Suc k. snd (ob ! i) ⊂ snd (ob ! Suc k)) 
            ∧ Obj (fst (ob ! 0)) T →⇩β⇧* Obj (fst (ob ! Suc k)) T 
            ∧ (card (snd (ob ! Suc k)) = Suc k 
               ⟶ Ltake_eq (snd (ob ! Suc k)) (fst (ob ! Suc k)) g 
                   ∧ Ltake_eq (dom f - snd (ob ! Suc k)) (fst (ob ! Suc k)) f)"
        by (rule_tac x = ob' in exI, simp)
    qed
  qed
qed

lemma rtrancl_beta_obj_n: 
  fixes f g L T
  assumes 
  "finite L" and
  "∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
               ⟶ (∃t''. ((the(f l))⇗[Fvar s, Fvar p]⇖) →⇩β⇧* t'' 
                        ∧ the(g l) = σ[s,p]t'')" and
  "dom f = dom g" and "∀l∈dom f. body (the(f l))"
  shows "Obj f T →⇩β⇧* Obj g T"
proof (cases "f = Map.empty")
  case True with ‹dom f = dom g› have "{} = dom g" by simp
  from ‹f = Map.empty› empty_dom[OF this] show ?thesis by simp
next
  from rtrancl_beta_obj_lem00[OF assms]
  obtain ob :: "((Label -~> sterm) × (Label set)) list" 
    where 
    "length ob = card(dom f) + 1" and
    "∀obi. obi ∈ set ob ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f" and
    "fst(ob!0) = f" and
    "card (snd(ob!card(dom f))) = card(dom f)" and
    "Obj (fst(ob!0)) T →⇩β⇧* Obj (fst(ob!card(dom f))) T" and
    "Ltake_eq (snd(ob!card(dom f))) (fst(ob!card(dom f))) g"
    by blast
  from ‹length ob = card (dom f) + 1› have "(ob!card(dom f)) ∈ set ob" by auto
  with ‹∀obi. obi ∈ set ob ⟶ dom (fst obi) = dom f ∧ snd obi ⊆ dom f›
  have "dom (fst(ob!card(dom f))) = dom f" and "snd(ob!card(dom f)) ⊆ dom f"
    by blast+

  {
    fix l :: Label
    from 
      ‹snd(ob!card(dom f)) ⊆ dom f› ‹card (snd(ob!card(dom f))) = card(dom f)›
      Ltake_eq_dom
    have "snd(ob!card(dom f)) = dom f" by blast
    with ‹Ltake_eq (snd(ob!card (dom f))) (fst(ob!card (dom f))) g› 
    have "fst(ob!card(dom f)) l = g l"
    proof (cases "l ∈ dom f", simp_all add: Ltake_eq_def)
      assume "l ∉ dom f" 
      with ‹dom f = dom g› ‹dom (fst(ob!card(dom f))) = dom f› 
      show "fst(ob!card(dom f)) l = g l" by auto
    qed
  }
  with ext have "fst(ob!card(dom f)) = g" by auto
  with ‹fst(ob!0) = f› ‹Obj (fst(ob!0)) T →⇩β⇧* Obj (fst(ob!card (dom f))) T› 
  show "Obj f T →⇩β⇧* Obj g T" by simp
qed

subsection ‹Size of sterms›

(* this section defines the size of sterms 
compared to size, the size of an object is the sum of the size of its fields +1 *)

definition fsize0 :: "(Label -~> sterm) ⇒ (sterm ⇒ nat) ⇒ nat" where
  "fsize0 f sts =
    foldl (+) 0 (map sts (Finite_Set.fold (λx z. z@[THE y. Some y = f x]) [] (dom f)))"

primrec
 ssize        :: "sterm ⇒ nat" 
and
 ssize_option :: "sterm option ⇒ nat"
where
  ssize_Bvar : "ssize (Bvar b) = 0"
| ssize_Fvar : "ssize (Fvar x) = 0"
| ssize_Call : "ssize (Call a l b) = (ssize a) + (ssize b) + Suc 0"
| ssize_Upd  : "ssize (Upd a l b) = (ssize a) + (ssize b) + Suc 0" 
| ssize_Obj  : "ssize (Obj f T) = Finite_Set.fold (λx y. y + ssize_option (f x)) (Suc 0) (dom f)"
| ssize_None : "ssize_option (None) = 0"
| ssize_Some : "ssize_option (Some y) = ssize y + Suc 0"

(* We need this locale, as all the handy functions are there now *)
interpretation comp_fun_commute "(λx y::nat. y + (f x))"
  by (unfold comp_fun_commute_def, force)

lemma SizeOfObjectPos: "ssize (Obj (f::Label -~> sterm) T) > 0"
proof (simp)
  from finite_dom_fmap have "finite (dom f)" by auto
  thus "0 < Finite_Set.fold (λx y. y + ssize_option (f x)) (Suc 0) (dom f)"
  proof (induct)
    case empty thus ?case by simp
  next
    case (insert A a) thus ?case by auto
  qed
qed

end