Theory Lemmas

theory Lemmas
  imports Agreement
begin

lemma judge_imp_agree:
  assumes "Γ ⊢ e : τ"
  shows   "Γ ⊢ e, e, e : τ"
  using assms by (induct Γ e τ) (auto simp: fresh_Pair)

lemma lemma2_1:
  assumes "Γ ⊢ e, eP, eV : τ"
  shows   "⦇eP⦈ = eV"
  using assms by (induct Γ e eP eV τ) (simp_all add: Abs1_eq)

(* Lemma 2.2 doesn't hold *)
lemma lemma2_2_false:
  fixes x :: var
  assumes "⋀Γ e eP eV τ eP' eV'. ⟦ Γ ⊢ e, eP, eV : τ; Γ ⊢ e, eP', eV' : τ ⟧ ⟹ eP = eP' ∧ eV = eV'"
  shows False
proof -
  have a1: "{$$} ⊢ Prj1 (Pair Unit Unit), Prj1 (Pair Unit Unit), Prj1 (Pair Unit Unit) : One"
    by fastforce
  also have a2: "{$$} ⊢ Prj1 (Pair Unit Unit), Prj1 (Pair Unit (Hashed (hash Unit) Unit)), Prj1 (Pair Unit (Hash (hash Unit))) : One"
    by fastforce
  from a1 a2 have "Prj1 (Pair Unit Unit) = Prj1 (Pair Unit (Hash (hash Unit)))"
    by (auto dest: assms)
  then show False
    by simp
qed

lemma smallstep_ideal_deterministic: 
  "≪[], t≫ I→ ≪[], u≫ ⟹ ≪[], t≫ I→ ≪[], u'≫ ⟹ u = u'"
proof (nominal_induct "[]::proofstream" t I "[]::proofstream" u avoiding: u' rule: smallstep.strong_induct)
  case (s_App1 e⇩1 e⇩1' e⇩2)
  from s_App1(3) value_no_step[OF s_App1(1)] show ?case
    by (auto dest!: s_App1(2))
next
  case (s_App2 v⇩1 e⇩2 e⇩2')
  from s_App2(4) value_no_step[OF s_App2(2)] value_no_step[OF _ s_App2(1)] show ?case
    by (force dest!: s_App2(3))
next
  case (s_AppLam v x e)
  from  s_AppLam(5,1,3) value_no_step[OF _ s_AppLam(2)] show ?case
  proof (cases rule: s_App_inv)
    case (AppLam y e')
    obtain z :: var where "atom z ♯ (x, e, y, e')"
      by (metis obtain_fresh)
    with AppLam s_AppLam(1,3) show ?thesis
      by (auto simp: fresh_Pair intro: box_equals[OF _ subst_term_perm[symmetric, of z] subst_term_perm[symmetric, of z]])
    thm box_equals[OF _ subst_term_perm[symmetric] subst_term_perm[symmetric]]
  qed (auto dest: value_no_step)
next
  case (s_AppRec v x e)
  from s_AppRec(5,1,3) value_no_step[OF _ s_AppRec(2)] show ?case
  proof (cases rule: s_App_inv)
    case (AppRec y e')
    obtain z :: var where "atom z ♯ (x, e, y, e')"
      by (metis obtain_fresh)
    with AppRec(1-4) AppRec(5)[simplified] s_AppRec(1,3) show ?thesis
      by (auto simp: fresh_Pair AppRec(5)
          intro: box_equals[OF _ subst_term_perm[symmetric, of z] subst_term_perm[symmetric, of z]])
  qed (auto dest: value_no_step)
next
  case (s_Let1 x e⇩1 e⇩1' e⇩2)
  from s_Let1(1,2,3,8) value_no_step[OF s_Let1(6)] show ?case
    by (auto dest: s_Let1(7))
next
  case (s_Let2 v x e)
  from s_Let2(1,3,5) value_no_step[OF _ s_Let2(2)] show ?case
    by force
next
  case (s_Inj1 e e')
  from s_Inj1(2,3) show ?case
    by auto
next
  case (s_Inj2 e e')
  from s_Inj2(2,3) show ?case
    by auto
next
  case (s_Case e e' e⇩1 e⇩2)
  from s_Case(2,3) value_no_step[OF s_Case(1)] show ?case
    by auto
next
  case (s_Pair1 e⇩1 e⇩1' e⇩2)
  from s_Pair1(2,3) value_no_step[OF s_Pair1(1)] show ?case
    by auto
next
  case (s_Pair2 v⇩1 e⇩2 e⇩2')
  from s_Pair2(3,4) value_no_step[OF _ s_Pair2(1)] value_no_step[OF s_Pair2(2)] show ?case
    by force
next
  case (s_Prj1 e e')
  from s_Prj1(2,3) value_no_step[OF s_Prj1(1)] show ?case
    by auto
next
  case (s_Prj2 e e')
  from s_Prj2(2,3) value_no_step[OF s_Prj2(1)] show ?case
    by auto
next
  case (s_Unroll e e')
  from s_Unroll(2,3) value_no_step[OF s_Unroll(1)] show ?case
    by auto
next
  case (s_Roll e e')
  from s_Roll(2,3) show ?case
    by auto
next
  case (s_Auth e e')
  from s_Auth(2,3) value_no_step[OF s_Auth(1)] show ?case
    by auto
next
  case (s_Unauth e e')
  from s_Unauth(2,3) value_no_step[OF s_Unauth(1)] show ?case
    by auto
qed (auto 0 3 dest: value_no_step)

lemma smallsteps_ideal_deterministic: 
  "≪[], t≫ I→i ≪[], u≫ ⟹ ≪[], t≫ I→i ≪[], u'≫ ⟹ u = u'"
proof (induct "[]::proofstream" t I i "[]::proofstream" u arbitrary: u' rule: smallsteps.induct)
  case (s_Tr e⇩1 i π⇩2 e⇩2 e⇩3)
  from s_Tr(4) show ?case
  proof (cases rule: smallsteps.cases)
    case _: (s_Tr i π⇩4 e⇩4)
    with s_Tr(1,3) s_Tr(2)[of e⇩4] show ?thesis
      using smallstepsI_ps_emptyD(2)[of e⇩1 i π⇩4 e⇩4] smallstepI_ps_eq[of π⇩2 e⇩2 "[]" e⇩3]
      by (auto intro!: smallstep_ideal_deterministic elim!: smallstepI_ps_emptyD)
  qed simp
qed auto

(* Counterexample for lemma 6 as stated in the paper, using administrative normal form *)
lemma lemma6_false:
  assumes agree: "⋀e eP eV τ πA i π' eV'. ⟦ {$$} ⊢ e, eP, eV : τ; ≪ πA, eV ≫ V→i ≪ π', eV' ≫ ⟧ ⟹
      ∃e' eP' π j π0 s s'. (≪ [], e ≫ I→i ≪ [], e' ≫ ∧ ≪ [], eP ≫ P→i ≪ π, eP' ≫ ∧ (πA = π @ π') ∧ {$$} ⊢ e', eP', eV' : τ) ∨
       (j ≤ i ∧ ≪ [], eP ≫ P→j ≪ π0 @ [s], eP' ≫ ∧ (πA = π0 @ [s'] @ π') ∧ s ≠ s' ∧ hash s = hash s')"
  and     collision: "hash (Inj1 Unit) = hash (Inj2 Unit)"
  and     no_collision_with_Unit: "⋀t. hash Unit = hash t ⟹ t = Unit"
  shows   False
proof -
  define i where "i = Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))"
  obtain x y z :: var where fresh: "atom y ♯ x" "atom z ♯ (x, y)"
    by (metis obtain_fresh)
  define t where "t = Let (Let (Auth (Inj1 Unit)) y (Unauth (Var y))) x (Let (Let (Auth Unit) z (Unauth (Var z))) y (Var x))"
  note fresh_Cons[simp]
    (* prover execution *)
  have prover: "≪ [], t ≫ P→i ≪ [Inj1 Unit, Unit], Inj1 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
           apply (rule s_Let1[rotated])
            apply (rule s_Let1[rotated])
             apply (rule s_AuthP[rotated])
              apply simp
             apply simp
            apply simp
           apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_Let2)
            apply simp
           apply simp
          apply simp
         apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthP)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let1[rotated])
         apply (rule s_AuthP[rotated])
          apply simp
         apply simp
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
     apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthP)
      apply simp
     apply simp
    apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
      (* verifier execution *)
  have verifier1: "≪ [Inj1 Unit, Unit], t ≫ V→i ≪ [], Inj1 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
           apply (rule s_Let1[rotated])
            apply (rule s_Let1[rotated])
             apply (rule s_AuthV[rotated])
              apply simp
             apply simp
            apply simp
           apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_Let2)
            apply simp
           apply simp
          apply simp
         apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthV)
           apply simp
          apply simp
         apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let1[rotated])
         apply (rule s_AuthV[rotated])
          apply simp
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
     apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthV)
       apply simp
      apply simp
     apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
      (* verifier execution with proofstream containing collision *)
  have verifier2: "≪ [Inj2 Unit, Unit], t ≫ V→i ≪ [], Inj2 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
           apply (rule s_Let1[rotated])
            apply (rule s_Let1[rotated])
             apply (rule s_AuthV[rotated])
              apply simp
             apply simp
            apply simp
           apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_Let2)
            apply simp
           apply simp
          apply simp
         apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthV)
           apply simp
          apply (simp add: collision)
         apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let1[rotated])
         apply (rule s_AuthV[rotated])
          apply simp
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
     apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthV)
       apply simp
      apply simp
     apply simp
    apply (rule s_Let2[of Unit y _ "Inj2 Unit", simplified])
    apply simp
    done
  have judge: "{$$} ⊢ t : Sum One One"
    unfolding t_def using fresh
    by (force simp: fresh_Pair fresh_fmap_update)
  have ideal_deterministic: "e = Inj1 Unit" if "≪[], t≫ I→i ≪[], e≫" for e
    apply (rule smallsteps_ideal_deterministic[OF that])
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
           apply (rule s_Let1[rotated])
            apply (rule s_Let1[rotated])
             apply (rule s_AuthI[rotated])
             apply simp
            apply simp
           apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_Let2)
            apply simp
           apply simp
          apply simp
         apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthI)
          apply simp
         apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let1[rotated])
         apply (rule s_AuthI[rotated])
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
     apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthI)
      apply simp
     apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
  from agree[OF judge_imp_agree[OF judge] verifier2] collision prover verifier1  show "False"
  proof safe
    fix e' eP'
    assume agree: "{$$} ⊢ e', eP', Inj2 Unit : Sum One One"
    assume assm: "≪[], t≫ I→i ≪[], e'≫"
    then have "e' = Inj1 Unit"
      by (simp add: ideal_deterministic)
    with agree show False
      by auto
  qed (auto dest!: no_collision_with_Unit[OF sym])
qed

(* Alternative, shorter counterexample for lemma 6 as stated in the paper *)
lemma lemma6_false_alt:
  assumes agree: "⋀e eP eV τ πA i π' eV'. ⟦ {$$} ⊢ e, eP, eV : τ; ≪ πA, eV ≫ V→i ≪ π', eV' ≫ ⟧ ⟹
      ∃e' eP' π j π0 s s'. (≪ [], e ≫ I→i ≪ [], e' ≫ ∧ ≪ [], eP ≫ P→i ≪ π, eP' ≫ ∧ (πA = π @ π') ∧ {$$} ⊢ e', eP', eV' : τ) ∨
       (j ≤ i ∧ ≪ [], eP ≫ P→j ≪ π0 @ [s], eP' ≫ ∧ (πA = π0 @ [s'] @ π') ∧ s ≠ s' ∧ hash s = hash s')"
  and     collision: "hash (Inj1 Unit) = hash (Inj2 Unit)"
  and     no_collision_with_Unit: "⋀t. hash Unit = hash t ⟹ t = Unit"
  shows   False
proof -
  define i where "i = Suc (Suc (Suc (Suc (Suc (Suc 0)))))"
  obtain x y z :: var where fresh: "atom y ♯ x" "atom z ♯ (x, y)"
    by (metis obtain_fresh)
  define t where "t = Let (Unauth (Auth (Inj1 Unit))) x (Let (Unauth (Auth Unit)) y (Var x))"
  note fresh_Cons[simp]
    (* prover execution *)
  have prover: "≪ [], t ≫ P→i ≪ [Inj1 Unit, Unit], Inj1 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
         apply (rule s_Let1[rotated])
          apply (rule s_Unauth)
          apply (rule s_AuthP[rotated])
           apply simp
          apply simp
         apply simp
        apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_UnauthP)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Unauth)
       apply (rule s_AuthP[rotated])
        apply simp
       apply simp
      apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthP)
      apply simp
     apply simp
    apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
      (* verifier execution *)
  have verifier1: "≪ [Inj1 Unit, Unit], t ≫ V→i ≪ [], Inj1 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
         apply (rule s_Let1[rotated])
          apply (rule s_Unauth)
          apply (rule s_AuthV[rotated])
           apply simp
          apply simp
         apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_UnauthV)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Unauth)
       apply (rule s_AuthV[rotated])
        apply simp
       apply simp
      apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthV)
      apply simp
     apply simp
    apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
      (* verifier execution with proofstream containing collision *)
  have verifier2: "≪ [Inj2 Unit, Unit], t ≫ V→i ≪ [], Inj2 Unit ≫"
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
         apply (rule s_Let1[rotated])
          apply (rule s_Unauth)
          apply (rule s_AuthV[rotated])
           apply simp
          apply simp
         apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_UnauthV)
          apply simp
         apply (simp add: collision)
        apply simp
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Unauth)
       apply (rule s_AuthV[rotated])
        apply simp
       apply simp
      apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthV)
      apply simp
     apply simp
    apply simp
    apply (rule s_Let2[of Unit y _ "Inj2 Unit", simplified])
    apply simp
    done
  have judge: "{$$} ⊢ t : Sum One One"
    unfolding t_def using fresh
    by (force simp: fresh_Pair fresh_fmap_update)
  have ideal_deterministic: "e = Inj1 Unit" if "≪[], t≫ I→i ≪[], e≫" for e
    apply (rule smallsteps_ideal_deterministic[OF that])
    unfolding i_def t_def Suc_eq_plus1 using fresh
    apply -
    apply (rule smallsteps.intros)+
         apply (rule s_Let1[rotated])
          apply (rule s_Unauth)
          apply (rule s_AuthI[rotated])
          apply simp
         apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_UnauthI)
         apply simp
        apply simp
       apply (rule s_Let2)
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_Unauth)
       apply (rule s_AuthI[rotated])
       apply simp
      apply simp
     apply (rule s_Let1[rotated])
      apply (rule s_UnauthI)
      apply simp
     apply simp
    apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
    apply simp
    done
  from agree[OF judge_imp_agree[OF judge] verifier2] collision prover verifier1  show "False"
  proof safe
    fix e' eP'
    assume agree: "{$$} ⊢ e', eP', Inj2 Unit : Sum One One"
    assume assm: "≪[], t≫ I→i ≪[], e'≫"
    then have "e' = Inj1 Unit"
      by (simp add: ideal_deterministic)
    with agree show False
      by auto
  qed (auto dest!: no_collision_with_Unit[OF sym])
qed

lemma lemma2_3:
  assumes "Γ ⊢ e, eP, eV : τ"
  shows   "erase_env Γ ⊢⇩W e : erase τ"
  using assms unfolding erase_env_def proof (nominal_induct Γ e eP eV τ rule: agree.strong_induct)
  case (a_HashI v vP τ h Γ)
  then show ?case
    apply (induct Γ)
     apply (auto simp: judge_weak_weakening_2 fmmap_fmupd judge_weak_fresh_env_fresh_term fresh_tyenv_None)
    done
qed (simp_all add: fresh_fmmap_erase_fresh fmmap_fmupd judge_weak_fresh_env_fresh_term)

lemma lemma2_4[dest]:
  assumes "Γ ⊢ e, eP, eV : τ"
  shows   "value e ∧ value eP ∧ value eV ∨ ¬ value e ∧ ¬ value eP ∧ ¬ value eV"
  using assms by (nominal_induct Γ e eP eV τ rule: agree.strong_induct) auto

lemma lemma4:
  assumes "Γ(x $$:= τ') ⊢ e, eP, eV : τ"
  and     "{$$} ⊢ v, vP, vV : τ'"
  and     "value v" "value vP" "value vV"
  shows   "Γ ⊢ e[v / x], eP[vP / x], eV[vV / x] : τ"
  using assms proof (nominal_induct "Γ(x $$:= τ')" e eP eV τ avoiding: x Γ rule: agree.strong_induct)
  case a_Unit
  then show ?case by auto
next
  case (a_Var y τ)
  then show ?case
    apply (induct Γ)
     apply (metis agree.a_Var fmupd_lookup option.sel subst_term.simps(2))
    using agree_weakening_2 fresh_tyenv_None by auto
next
  case (a_Lam y τ⇩1 e eP eV τ⇩2)
  from a_Lam(1,2,5,6,7-) show ?case
    using agree_empty_fresh by (auto simp: fmap_reorder_neq_updates)
next
  case (a_App v⇩1 v⇩2 v⇩1P v⇩2P v⇩1V v⇩2V τ⇩1 τ⇩2)
  from a_App(5-) show ?case
    by (auto intro: a_App(2,4))
next
  case (a_Let y e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  then show ?case
    apply (subst (1 2 3) subst_term.simps(9))
    using agree_empty_fresh apply (simp_all add: fmap_reorder_neq_updates) [3]
    apply (rule agree.a_Let)
    using agree_empty_fresh apply (auto simp: fmap_reorder_neq_updates)
    done
next
  case (a_Rec y z τ⇩1 τ⇩2 e eP eV)
  from a_Rec(10) have "∀a::var. atom a ♯ v" "∀a::var. atom a ♯ vP" "∀a::var. atom a ♯ vV"
    by auto
  with a_Rec(1-8,10-) show ?case
    apply simp
    apply (rule agree.a_Rec)
    apply (simp_all del: subst_term.simps(3) add: subst_term.simps(3)[symmetric] fresh_at_base)
    apply (rule a_Rec(9))
    apply (simp_all add: fmap_reorder_neq_updates)+
    done
next
  case (a_Case v v⇩1 v⇩2 vP v⇩1P v⇩2P vV v⇩1V v⇩2V τ⇩1 τ⇩2 τ)
  from a_Case(7-) show ?case
    by (auto intro: a_Case(2,4,6))
next
  case (a_HashI v vP τ h)
  then have "atom x ♯ v" "atom x ♯ vP" by auto
  with a_HashI show ?case by auto
qed auto

(* Lemma 3 *)
lemma lemma3_general:
  fixes Γ :: tyenv and vs vPs vVs :: tenv
  assumes "Γ ⊢ e : τ" "A |⊆| fmdom Γ"
  and     "fmdom vs = A" "fmdom vPs = A" "fmdom vVs = A"
  and     "∀x. x |∈| A ⟶ (∃τ' v vP h.
    Γ $$ x = Some (AuthT τ') ∧
    vs $$ x = Some v ∧
   vPs $$ x = Some (Hashed h vP) ∧
   vVs $$ x = Some (Hash h) ∧
   {$$} ⊢ v, Hashed h vP, Hash h : (AuthT τ'))"
  shows  "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : τ"
  using assms proof (nominal_induct Γ e τ avoiding: vs vPs vVs A rule: judge.strong_induct)
  case (j_Unit Γ)
  then show ?case
    by auto
next
  case (j_Var Γ x τ)
  with j_Var show ?case
  proof (cases "x |∈| A")
    case True
    with j_Var show ?thesis
      by (fastforce dest!: spec[of _ x] intro: agree_weakening_env)
  next
    case False
    with j_Var show ?thesis
      apply (simp split: option.splits)
      apply safe
             apply (simp add: a_Var)
            apply (metis fmdomI)+
      done
  qed
next
  case (j_Lam x Γ τ⇩1 e τ⇩2)
  from j_Lam(4) have [simp]: "A |-| {|x|} = A"
    by (simp add: fresh_fset_fminus)
  from j_Lam(5,8-) have "fmdrop_fset A Γ(x $$:= τ⇩1) ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : τ⇩2"
    apply -
    apply (rule j_Lam(7)[of A vs vPs vVs])
        apply (auto simp: fresh_tyenv_None)
    done
  with j_Lam(1-5) show ?case
    by (auto simp: fresh_fmdrop_fset)
next
  case (j_App Γ e τ⇩1 τ⇩2 e')
  then have "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Fun τ⇩1 τ⇩2"
    and "fmdrop_fset A Γ ⊢ psubst_term e' vs, psubst_term e' vPs, psubst_term e' vVs : τ⇩1"
    by simp_all
  then show ?case
    by auto
next
  case (j_Let x Γ e⇩1 τ⇩1 e⇩2 τ⇩2)
  from j_Let(4) have [simp]: "A |-| {|x|} = A"
    by (simp add: fresh_fset_fminus)
  from j_Let(4,5,8,11-) have "fmdrop_fset A Γ ⊢ psubst_term e⇩1 vs, psubst_term e⇩1 vPs, psubst_term e⇩1 vVs : τ⇩1"
    and "fmdrop_fset A Γ(x $$:= τ⇩1) ⊢ psubst_term e⇩2 vs, psubst_term e⇩2 vPs, psubst_term e⇩2 vVs : τ⇩2"
    apply -
    apply simp
    apply (rule j_Let(10))
    apply (auto simp: fresh_tyenv_None)
    done
  with j_Let(1-6) show ?case
    by (auto simp: fresh_fmdrop_fset fresh_Pair fresh_psubst)
next
  case (j_Rec x Γ y τ⇩1 τ⇩2 e')
  from j_Rec(4) have [simp]: "A |-| {|x|} = A"
    by (simp add: fresh_fset_fminus)
  from j_Rec(9,14-) have "fmdrop_fset A Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ psubst_term (Lam y e') vs, psubst_term (Lam y e') vPs, psubst_term (Lam y e') vVs : Fun τ⇩1 τ⇩2"
    apply -
    apply (rule j_Rec(13))
    apply (auto simp: fresh_tyenv_None)
    done
  with j_Rec(1-11) show ?case
    by (auto simp: fresh_fmdrop_fset)
next
  case (j_Case Γ e τ⇩1 τ⇩2 e⇩1 τ e⇩2)
  then have "fmdrop_fset A Γ ⊢ psubst_term e  vs, psubst_term e  vPs, psubst_term e  vVs : Sum τ⇩1 τ⇩2"
    and "fmdrop_fset A Γ ⊢ psubst_term e⇩1 vs, psubst_term e⇩1 vPs, psubst_term e⇩1 vVs : Fun τ⇩1 τ"
    and "fmdrop_fset A Γ ⊢ psubst_term e⇩2 vs, psubst_term e⇩2 vPs, psubst_term e⇩2 vVs : Fun τ⇩2 τ"
    by simp_all
  then show ?case
    by auto
next
  case (j_Prj1 Γ e τ⇩1 τ⇩2)
  then have "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod τ⇩1 τ⇩2"
    by simp
  then show ?case
    by auto
next
  case (j_Prj2 Γ e τ⇩1 τ⇩2)
  then have "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod τ⇩1 τ⇩2"
    by simp
  then show ?case
    by auto
next
  case (j_Roll α Γ e τ)
  then have "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : subst_type τ (Mu α τ) α"
    by simp
  with j_Roll(4,5) show ?case
    by (auto simp: fresh_fmdrop_fset)
next
  case (j_Unroll α Γ e τ)
  then have "fmdrop_fset A Γ ⊢ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Mu α τ"
    by simp
  with j_Unroll(4,5) show ?case
    by (auto simp: fresh_fmdrop_fset)
qed auto

lemmas lemma3 = lemma3_general[where A = "fmdom Γ" and Γ = Γ, simplified] for Γ
thm lemma3[no_vars]

(* Correctness *)
lemma lemma5:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ [], e ≫ I→ ≪ [], e' ≫"
  obtains eP' eV' π
  where   "{$$} ⊢ e', eP', eV' : τ" "∀π⇩P. ≪ π⇩P, eP ≫ P→ ≪ π⇩P @ π, eP' ≫" "∀π'. ≪ π @ π', eV ≫ V→ ≪ π', eV' ≫"
  using [[simproc del: alpha_lst]] assms apply atomize_elim
proof (nominal_induct "{$$}::tyenv" e eP eV τ avoiding: e' rule: agree.strong_induct)
  case (a_App e⇩1 eP⇩1 eV⇩1 τ⇩1 τ⇩2 e⇩2 eP⇩2 eV⇩2)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 e⇩1')
    with a_App(1,3,5-) show ?thesis
      apply -
      apply (drule a_App(2))
      apply safe
      subgoal for eP⇩1' eV⇩1' π''
        apply (rule exI[of _ "App eP⇩1' eP⇩2"])
        apply (rule exI[of _ "App eV⇩1' eV⇩2"])
        apply (rule exI[of _ π''])
        apply (rule conjI)
        apply auto []
        apply (rule conjI)
        apply (rule allI)
        subgoal for πP
          apply (subst append_Nil2[symmetric])
          apply (rule iffD1[OF smallstepP_ps_prepend])
          apply (rule s_App1)
          apply (auto simp: iffD2[OF smallstepP_ps_prepend])
          done
        apply (rule allI)
        apply (rule iffD1[OF smallstepV_ps_append[where π' = "[]", simplified]])
        apply (rule s_App1)
        apply (auto simp: iffD2[OF smallstepV_ps_append])
        done
      done
  next
    case (App2 e⇩2')
    with a_App(1,3,5-) show ?thesis
      apply -
      apply (drule a_App(4))
      apply safe
      subgoal for eP⇩2' eV⇩2' π
        apply (rule exI[of _ "App eP⇩1 eP⇩2'"])
        apply (rule exI[of _ "App eV⇩1 eV⇩2'"])
        apply (rule exI[of _ π])
        apply (rule conjI)
        apply auto []
        apply (rule conjI)
        apply (rule allI)
        apply (rule iffD1[OF smallstepP_ps_prepend[where π = "[]", simplified]])
        apply (rule s_App2)
        apply (drule lemma2_4)
        apply simp
        apply (auto simp: iffD2[OF smallstepP_ps_prepend]) []
        apply (rule allI)
        apply (rule iffD1[OF smallstepV_ps_append[where π' = "[]", simplified]])
        apply (rule s_App2)
        apply (auto simp: iffD2[OF smallstepV_ps_append])
        done
      done
  next
    case (AppLam x e)
    with a_App(1,3,5-) show ?thesis
      apply simp
      apply (erule a_Lam_inv_I)
      apply simp
      subgoal for eP eV
        apply (rule exI[of _ "eP[eP⇩2 / x]"])
        apply (rule exI[of _ "eV[eV⇩2 / x]"])
        apply (rule conjI)
        apply (rule lemma4)
        apply auto [5]
        apply (rule exI[of _ "[]"])
        apply (rule conjI)
        apply (rule allI)
        subgoal for πP
          apply (rule iffD1[OF smallstepP_ps_prepend[where π = "[]", simplified]])
          apply simp
          apply (rule s_AppLam)
          apply (auto simp: fresh_Pair)
          done
        apply simp
        apply (rule allI)
        apply (rule iffD1[OF smallstepV_ps_append[of "[]" _ "[]" , simplified]])
        apply (rule s_AppLam)
        apply (auto simp: fresh_Pair)
        done
      done
  next
    case (AppRec x e)
    with a_App(1,3,5-) show ?thesis
      apply -
      apply (rule a_Rec_inv_I)
      apply simp
      apply simp
      apply (rule a_Lam_inv_I)
      apply simp
      apply (simp add: fresh_fmap_update)
      subgoal for y e'' eP' eV' eP'' eV''
        apply (rule exI[of _ "App (Lam y eP''[Rec x (Lam y eP'') / x]) eP⇩2"])
        apply (rule exI[of _ "App (Lam y eV''[Rec x (Lam y eV'') / x]) eV⇩2"])
        apply (rule exI[of _ "[]"])
        apply (rule conjI)
        apply simp
        apply (rule agree.a_App)
        apply (rule a_Lam)
        apply simp
        apply (rule lemma4)
        apply (auto simp: fmap_reorder_neq_updates) [6]
        apply (rule conjI)
        apply (rule allI)
        apply simp
        apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
        apply (subst subst_term.simps(3)[symmetric])
        apply simp
        apply (rule s_AppRec)
        apply (auto simp: fresh_Pair) [2]
        apply (rule allI)
        apply simp
        apply (rule iffD1[OF smallstepV_ps_append[of "[]" _ "[]", simplified]])
        apply (subst subst_term.simps(3)[symmetric])
        apply simp
        apply (rule s_AppRec)
        apply (auto simp: fresh_Pair)
        done
      done
  qed
next
  case (a_Let x e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  then have "atom x ♯ (e⇩1, [])" by auto
  with a_Let(10) show ?case
  proof (cases rule: s_Let_inv)
    case Let1
    with a_Let show ?thesis
      apply -
      apply (rule exI[of _ "eP⇩2[eP⇩1 / x]"])
      apply (rule exI[of _ "eV⇩2[eV⇩1 / x]"])
      apply (rule exI[of _ "[]"])
      apply (rule conjI)
      apply simp
      apply (erule lemma4)
      apply simp
      apply (drule lemma2_4, simp)
      apply (drule lemma2_4, simp)
      apply (drule lemma2_4, simp)
      apply (rule conjI)
      apply simp
      apply (rule allI)
      apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
      apply (rule s_Let2)
      apply auto [2]
      apply simp
      apply (rule allI)
      apply (rule iffD1[OF smallstepV_ps_append[of "[]" _ "[]", simplified]])
      apply (rule s_Let2)
      apply auto
      done
  next
    case (Let2 e⇩1')
    with a_Let(7) obtain eP⇩1' eV⇩1' π
      where ih: "{$$} ⊢ e⇩1', eP⇩1', eV⇩1' : τ⇩1"
        "∀π⇩P. ≪π⇩P, eP⇩1≫ P→ ≪π⇩P @ π, eP⇩1'≫"
        "∀π'. ≪π @ π', eV⇩1≫ V→ ≪π', eV⇩1'≫"
      by blast
    then have [simp]: "atom x ♯ ({$$}, e⇩1', eP⇩1', eV⇩1')"
      using agree_empty_fresh by auto
    from ih a_Let(4) have [simp]: "atom x ♯ π"
      using fresh_Nil fresh_append fresh_ps_smallstep_P by blast
    from a_Let ih have agree: "{$$} ⊢ Let e⇩1' x e⇩2, Let eP⇩1' x eP⇩2, Let eV⇩1' x eV⇩2 : τ⇩2"
      by auto
    from a_Let(4,5) ih have "≪[], Let eP⇩1 x eP⇩2≫ P→ ≪π, Let eP⇩1' x eP⇩2≫"
      "≪π, Let eV⇩1 x eV⇩2≫ V→ ≪[], Let eV⇩1' x eV⇩2≫"
       apply -
       apply (rule s_Let1)
        apply (auto simp: fresh_Pair) []
      using smallstepP_ps_prepend apply fastforce []
      apply (rule s_Let1)
       apply (auto simp: fresh_Pair) []
      using smallstepV_ps_append apply fastforce+
      done
    with a_Let(4,6) Let2 agree show ?thesis
      apply -
      apply (rule s_Let_inv')
        apply simp
      apply auto []
      apply (erule disjE)
      apply blast
      subgoal for eP⇩1''
        apply -
        apply (rule exI[of _ "Let eP⇩1' x eP⇩2"])
        apply (rule exI[of _ "Let eV⇩1' x eV⇩2"])
        apply (rule exI[of _ π])
        apply (subst iffD1[OF smallstepP_ps_prepend[of "[]" _ π, simplified]])
        apply simp
        apply (subst iffD1[OF smallstepV_ps_append[of π _ "[]", simplified]])
        apply auto
        done
      done
  qed
next
  case (a_Case e eP eV τ⇩1 τ⇩2 e⇩1 eP⇩1 eV⇩1 τ e⇩2 eP⇩2 eV⇩2)
  from a_Case(7) show ?case
  proof (cases rule: s_Case_inv)
    case (Case e'')
    with a_Case(3,5) show ?thesis
      apply -
      apply (drule a_Case(2)[of e''])
      apply safe
      subgoal for eP'' eV'' π
        apply (rule exI[of _ "Case eP'' eP⇩1 eP⇩2"])
        apply (rule exI[of _ "Case eV'' eV⇩1 eV⇩2"])
        apply (rule exI[of _ π])
        apply (rule conjI)
        apply (rule agree.a_Case)
        apply simp
        apply simp
        apply simp
        apply (rule conjI)
        apply (rule allI)
        apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ π, simplified]])
        apply (rule s_Case)
        using iffD2[OF smallstepP_ps_prepend] apply auto []
        apply (rule allI)
        apply (rule iffD1[OF smallstepV_ps_append[of π _ "[]", simplified]])
        apply (rule s_Case)
        using iffD2[OF smallstepV_ps_append] apply auto
        done
      done
  next
    case (Inj1 v)
    with a_Case(1,3,5) show ?thesis
      apply -
      apply (rule a_Inj1_inv_I)
      apply simp
      subgoal for vP vV
        apply (rule exI[of _ "App eP⇩1 vP"])
        apply (rule exI[of _ "App eV⇩1 vV"])
        apply (rule exI[of _ "[]"])
        apply auto
        done
      done
  next
    case (Inj2 v)
    with a_Case(1,3,5) show ?thesis
      apply -
      apply (rule a_Inj2_inv_I)
      apply simp
      subgoal for vP vV
        apply (rule exI[of _ "App eP⇩2 vP"])
        apply (rule exI[of _ "App eV⇩2 vV"])
        apply (rule exI[of _ "[]"])
        apply auto
        done
      done
  qed
next
  case (a_Prj1 e eP eV τ⇩1 τ⇩2)
  from a_Prj1(3) show ?case
  proof (cases rule: s_Prj1_inv)
    case (Prj1 e'')
    then show ?thesis
      apply -
      by (drule a_Prj1(2), blast+)
  next
    case (PrjPair1 v⇩2)
    with a_Prj1(1) show ?thesis
      apply -
      apply (rule a_Pair_inv_I)
      apply simp
      subgoal for eP⇩1 eV⇩1 eP⇩2 eV⇩2
        apply (rule exI[of _ eP⇩1])
        apply (rule exI[of _ eV⇩1])
        apply (rule exI[of _ "[]"])
        apply auto
        done
      done
  qed
next
  case (a_Prj2 e eP eV τ⇩1 τ⇩2)
  from a_Prj2(3) show ?case
  proof (cases rule: s_Prj2_inv)
    case (Prj2 e'')
    then show ?thesis
      apply -
      by (drule a_Prj2(2), blast+)
  next
    case (PrjPair2 v⇩1)
    with a_Prj2(1) show ?thesis
      apply -
      apply (rule a_Pair_inv_I)
      apply simp
      subgoal for eP⇩1 eV⇩1 eP⇩2 eV⇩2
        apply (rule exI[of _ eP⇩2])
        apply (rule exI[of _ eV⇩2])
        apply (rule exI[of _ "[]"])
        apply auto
        done
      done
  qed
next
  case (a_Roll α e eP eV τ)
  from a_Roll(5) show ?case
  proof (cases rule: s_Roll_inv)
    case (Roll e'')
    then show ?thesis
      apply -
      apply (drule a_Roll(4))
      apply safe
      subgoal for eP'' eV'' π
        apply (rule exI[of _ "Roll eP''"])
        apply (rule exI[of _ "Roll eV''"])
        apply (rule exI[of _ π])
        apply auto
        done
      done
  qed
next
  case (a_Unroll α e eP eV τ)
  from a_Unroll(5) show ?case
  proof (cases rule: s_Unroll_inv)
    case (Unroll e'')
    then show ?thesis
      apply -
      apply (drule a_Unroll(4))
      apply safe
      subgoal for eP'' eV'' π
        apply (rule exI[of _ "Unroll eP''"])
        apply (rule exI[of _ "Unroll eV''"])
        apply (rule exI[of _ π])
        apply auto
        done
      done
  next
    case UnrollRoll
    with a_Unroll(3) show ?thesis
      apply -
      apply (rule a_Roll_inv_I)
      apply simp
      subgoal for eP' eV'
        apply (rule exI[of _ eP'])
        apply (rule exI[of _ eV'])
        apply (rule exI[of _ "[]"])
        apply auto
        done
      done
  qed
next
  case (a_Auth e eP eV τ)
  from a_Auth(1) have [simp]: "atom x ♯ eP" for x :: var
    using agree_empty_fresh by simp
  from a_Auth(3) show ?case
  proof (cases rule: s_AuthI_inv)
    case (Auth e'')
    then show ?thesis
      apply -
      by (drule a_Auth(2), blast+)
  next
    case AuthI
    with a_Auth(1) have "value eP" "value eV" by auto
    with a_Auth(1) AuthI(2) show ?thesis
      apply -
      apply (rule exI[of _ "Hashed (hash ⦇eP⦈) eP"])
      apply (rule exI[of _ "Hash (hash ⦇eP⦈)"])
      apply (rule exI[of _ "[]"])
      apply (auto dest: lemma2_1 simp: fresh_shallow)
      done
  qed
next
  case (a_Unauth e eP eV τ)
  from a_Unauth(1) have eP_closed: "closed eP"
    using agree_empty_fresh by simp
  from a_Unauth(3) show ?case
  proof (cases rule: s_UnauthI_inv)
    case (Unauth e')
    then show ?thesis
      apply -
      by (drule a_Unauth(2), blast+)
  next
    case UnauthI
    with a_Unauth eP_closed show ?thesis
      apply -
      apply (rule a_AuthT_value_inv)
      apply simp
      apply auto [3]
      subgoal for vP'
        apply (rule exI[of _ vP'])
        apply (rule exI[of _ "⦇vP'⦈"])
        apply (rule exI[of _ "[⦇vP'⦈]"])
        apply (auto simp: fresh_shallow)
        done
      done
  qed
next
  case (a_Pair e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 e⇩1')
    with a_Pair(1,3) show ?thesis
      apply -
      by (drule a_Pair(2), blast+)
  next
    case (Pair2 e⇩2')
    with a_Pair(1,3) show ?thesis
      apply -
      by (drule a_Pair(4), blast+)
  qed
next
  case (a_Inj1 e eP eV τ⇩1 τ⇩2)
  from a_Inj1(3) show ?case
  proof (cases rule: s_Inj1_inv)
    case (Inj1 e')
    with a_Inj1(1) show ?thesis
      apply -
      by (drule a_Inj1(2), blast+)
  qed
next
  case (a_Inj2 e eP eV τ⇩2 τ⇩1)
  from a_Inj2(3) show ?case
  proof (cases rule: s_Inj2_inv)
    case (Inj2 e'')
    with a_Inj2(1) show ?thesis
      apply -
      by (drule a_Inj2(2), blast+)
  qed
qed (simp, meson value.intros value_no_step)+

lemma lemma6:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ π⇩A, eV ≫ V→ ≪ π', eV' ≫"
  obtains e' eP' π
  where "≪ [], e ≫ I→ ≪ [], e' ≫" "∀π⇩P. ≪ π⇩P, eP ≫ P→ ≪ π⇩P @ π, eP' ≫"
  and   "{$$} ⊢ e', eP', eV' : τ ∧ π⇩A = π @ π' ∨
         (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π⇩A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
  using assms [[simproc del: alpha_lst]] apply atomize_elim
proof (nominal_induct "{$$}::tyenv" e eP eV τ avoiding: π⇩A π' eV' rule: agree.strong_induct)
  case (a_App e⇩1 eP⇩1 eV⇩1 τ⇩1 τ⇩2 e⇩2 eP⇩2 eV⇩2)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 eV⇩1')
    with a_App(1,3) show ?thesis
      apply -
      apply (drule a_App(2))
      apply blast+
      done
  next
    case (App2 e⇩2')
    with a_App(1,3) show ?thesis
      apply -
      apply (drule a_App(4))
      apply blast+
      done
  next
    case (AppLam x eV'')
    with a_App(1,3) show ?thesis
      apply -
      apply (rule a_Lam_inv_V)
      apply simp
      subgoal for e'' eP''
        apply (rule exI[of _ "e''[e⇩2 / x]"])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ "eP''[eP⇩2 / x]"])
        apply (rule conjI)
        apply simp
        apply (rule s_AppLam)
        apply (auto simp: fresh_Pair) [2]
        apply (rule conjI)
        apply (rule allI)
        apply simp
        apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
        apply (rule s_AppLam)
        apply (auto simp: fresh_Pair) [2]
        apply safe
        apply (rule lemma4)
        apply auto
        done
      done
  next
    case (AppRec x eV'')
    with a_App(1,3) show ?thesis
      apply -
      apply (rule a_Rec_inv_V)
      apply simp
      apply simp
      subgoal for y e'''  eP''' eV'''
        apply (rule exI[of _ "App (Lam y e'''[Rec x (Lam y e''') / x]) e⇩2"])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ "App (Lam y eP'''[Rec x (Lam y eP''') / x]) eP⇩2"])
        apply (rule conjI)
        apply (simp del: subst_term.simps)
        apply (rule s_AppRec)
        apply (auto simp: fresh_Pair) [2]
        apply (rule conjI)
        apply (rule allI)
        apply (simp del: subst_term.simps)
        apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
        apply (simp del: subst_term.simps)
        apply (rule s_AppRec)
        apply (auto simp: fresh_Pair) [2]
        apply safe
        apply (rule agree.a_App)
        apply (rule lemma4)
        apply auto
        done
      done
  qed
next
  case (a_Let x e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  then have "atom x ♯ (eV⇩1, π⇩A)" by auto
  with a_Let(12) show ?case
  proof (cases rule: s_Let_inv)
    case Let1
    with a_Let(5,6,8,10) show ?thesis
      apply -
      apply (rule exI[of _ "e⇩2[e⇩1 / x]"])
      apply (rule exI[of _ "[]"])
      apply (rule exI[of _ "eP⇩2[eP⇩1 / x]"])
      apply (rule conjI)
       apply (drule lemma2_4)
       apply simp
      apply (rule conjI)
       apply (rule allI)
       apply simp
       apply (rule iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
       apply (auto intro: lemma4)
      done
  next
    case (Let2 eV⇩1')
    with a_Let(9)[of π⇩A π' eV⇩1'] obtain e⇩1' π eP⇩1' s s' where
      ih: "≪[], e⇩1≫ I→ ≪[], e⇩1'≫ ∧ (∀π⇩P. ≪π⇩P, eP⇩1≫ P→ ≪π⇩P @ π, eP⇩1'≫)
           ∧ ({$$} ⊢ e⇩1', eP⇩1', eV⇩1' : τ⇩1 ∧ π⇩A = π @ π'
             ∨ closed s ∧ closed s' ∧ π = [s] ∧ π⇩A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
      by blast
    with a_Let(5,6) have fresh: "atom x ♯ e⇩1'" "atom x ♯ eP⇩1'"
      using fresh_smallstep_I fresh_smallstep_P by blast+
    from ih a_Let(2,6) have "atom x ♯ π"
      using fresh_append fresh_ps_smallstep_P by blast
    with Let2 a_Let(1-8,10,12-) fresh ih show ?thesis
      apply -
      apply (rule exI[of _ "Let e⇩1' x e⇩2"])
      apply (rule exI[of _ π])
      apply (rule exI[of _ "Let eP⇩1' x eP⇩2"])
      apply (rule conjI)
       apply rule
        apply (simp add: fresh_Pair)
       apply simp
      apply (rule conjI)
       apply (rule allI)
      subgoal for πP
        apply (rule iffD1[OF smallstepP_ps_prepend, of "[]", simplified])
        using smallstepP_ps_prepend apply (fastforce del: s_Let1 intro!: s_Let1)
        done
      apply auto
      done
  qed
next
  case (a_Case e eP eV τ⇩1 τ⇩2 e⇩1 eP⇩1 eV⇩1 τ e⇩2 eP⇩2 eV⇩2)
  from a_Case(7) show ?case
  proof (cases rule: s_Case_inv)
    case (Case eV'')
    with a_Case(3,5) show ?thesis
      apply -
      apply (drule a_Case(2)[of π⇩A π' eV''])
      apply safe
      subgoal by blast
      subgoal for e'' π eP'' s s'
        apply (rule exI[of _ "Case e'' e⇩1 e⇩2"])
        apply (rule exI[of _ "[s]"])
        apply (rule exI[of _ "Case eP'' eP⇩1 eP⇩2"])
        apply auto
        done
      done
  next
    case (Inj1 vV)
    with a_Case(1,3,5) show ?thesis
      apply -
      apply (rule a_Inj1_inv_V)
      apply simp
      subgoal for v' vP'
        apply (rule exI[of _ "App e⇩1 v'"])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ "App eP⇩1 vP'"])
        apply auto
        done
      done
  next
    case (Inj2 vV)
    with a_Case(1,3,5) show ?thesis
      apply -
      apply (rule a_Inj2_inv_V)
      apply simp
      subgoal for v' vP'
        apply (rule exI[of _ "App e⇩2 v'"])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ "App eP⇩2 vP'"])
        apply auto
        done
      done
  qed
next
  case (a_Prj1 e eP eV τ⇩1 τ⇩2)
  from a_Prj1(3) show ?case
  proof (cases rule: s_Prj1_inv)
    case (Prj1 eV'')
    then show ?thesis
      apply -
      apply (drule a_Prj1(2))
      apply blast+
      done
  next
    case (PrjPair1 v⇩2)
    with a_Prj1(1) show ?thesis
      apply -
      apply (erule a_Prod_inv)
      prefer 5
      subgoal for e⇩1 eP⇩1 eV⇩1 e⇩2 eP⇩2 eV⇩2
        apply (rule exI[of _ e⇩1])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ eP⇩1])
        apply auto
        done
      apply auto
      done
  qed
next
  case (a_Prj2 e eP eV τ⇩1 τ⇩2)
  from a_Prj2(3) show ?case
  proof (cases rule: s_Prj2_inv)
    case (Prj2 eV'')
    then show ?thesis
      apply -
      apply (drule a_Prj2(2))
      apply blast+
      done
  next
    case (PrjPair2 v⇩2)
    with a_Prj2(1) show ?thesis
      apply -
      apply (erule a_Prod_inv)
      prefer 5
      subgoal for e⇩1 eP⇩1 eV⇩1 e⇩2 eP⇩2 eV⇩2
        apply (rule exI[of _ e⇩2])
        apply (rule exI[of _ "[]"])
        apply (rule exI[of _ eP⇩2])
        apply auto
        done
      apply auto
      done
  qed
next
  case (a_Roll α e eP eV τ)
  from a_Roll(7) show ?case
  proof (cases rule: s_Roll_inv)
    case (Roll eV'')
    then show ?thesis
      apply -
      apply (drule a_Roll(6)[of π⇩A π' eV''])
      apply safe
      subgoal for e'' π eP''
        apply (rule exI[of _ "Roll e''"])
        apply (rule exI[of _ π])
        apply (rule exI[of _ "Roll eP''"])
        apply auto
        done
      apply blast
      done
  qed
next
  case (a_Unroll α e eP eV τ)
  from a_Unroll(7) show ?case
  proof (cases rule: s_Unroll_inv)
    case (Unroll eV'')
    then show ?thesis
      apply -
      apply (drule a_Unroll(6)[of π⇩A π' eV''])
      apply safe
      subgoal for e'' π eP''
        apply (rule exI[of _ "Unroll e''"])
        apply (rule exI[of _ π])
        apply (rule exI[of _ "Unroll eP''"])
        apply auto
        done
      apply blast
      done
  next
    case UnrollRoll
    with a_Unroll(5) show ?thesis
      by fastforce
  qed
next
  case (a_Auth e eP eV τ)
  from a_Auth(1) have [simp]: "atom x ♯ eP" for x :: var
    using agree_empty_fresh by simp
  from a_Auth(3) show ?case
  proof (cases rule: s_AuthV_inv)
    case (Auth eV'')
    then show ?thesis
      apply -
      apply (drule a_Auth(2)[of π⇩A π' eV''])
      apply safe
      subgoal for e'' π eP''
        apply (rule exI[of _ "Auth e''"])
        apply (rule exI[of _ π])
        apply (rule exI[of _ "Auth eP''"])
        apply auto
        done
      apply blast
      done
  next
    case AuthV
    with a_Auth(1) have "value eP" by auto
    with a_Auth(1) AuthV show ?thesis
      apply -
      apply (rule exI[of _ e])
      apply (rule exI[of _ "[]"])
      apply (rule exI[of _ "Hashed (hash ⦇eP⦈) eP"])
      apply simp
      apply (auto dest: lemma2_1 simp: fresh_shallow)
      done
  qed
next
  case (a_Unauth e eP eV τ)
  from a_Unauth(3) show ?case
  proof (cases rule: s_UnauthV_inv)
    case (Unauth e')
    then show ?thesis
      apply -
      by (drule a_Unauth(2), blast+)
  next
    case UnauthV
    with a_Unauth(1) show ?thesis
      apply -
      apply (rule a_AuthT_value_inv)
      apply simp
      apply auto [3]
      subgoal for vP'
        apply (rule exI[of _ e])
        apply (rule exI[of _ "[⦇vP'⦈]"])
        apply (rule exI[of _ vP'])
        apply (rule conjI)
        apply (rule s_UnauthI)
        apply auto []
        apply (rule conjI)
        apply simp
        apply simp
        apply (erule a_HashI_inv)
        apply auto
        done
      done
  qed
next
  case (a_Pair e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 eV⇩1')
    with a_Pair(3) show ?thesis
      using a_Pair(2)[of π⇩A π' eV⇩1'] by blast
  next
    case (Pair2 eV⇩2')
    with a_Pair(1) show ?thesis
      using a_Pair(4)[of π⇩A π' eV⇩2'] by blast
  qed
next
  case (a_Inj1 e eP eV τ⇩1 τ⇩2)
  from a_Inj1(3) show ?case
  proof (cases rule: s_Inj1_inv)
    case (Inj1 eV'')
    then show ?thesis
      using a_Inj1(2)[of π⇩A π' eV''] by blast
  qed
next
  case (a_Inj2 e eP eV τ⇩2 τ⇩1)
  from a_Inj2(3) show ?case
  proof (cases rule: s_Inj2_inv)
    case (Inj2 eV'')
    with a_Inj2(1) show ?thesis
      using a_Inj2(2)[of π⇩A π' eV''] by blast
  qed
qed (simp, meson value.intros value_no_step)+

lemma theorem1_correctness:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ [], e ≫ I→i ≪ [], e' ≫"
  obtains eP' eV' π
  where "≪ [], eP ≫ P→i ≪ π, eP' ≫"
    "≪ π, eV ≫ V→i ≪ [], eV' ≫"
    "{$$} ⊢ e', eP', eV' : τ"
  using assms apply (atomize_elim, rotate_tac)
proof (induct "[]::proofstream" e I i "[]::proofstream" e' rule: smallsteps.induct)
  case (s_Id e)
  then show ?case by auto
next
  case (s_Tr e⇩1 i π⇩2 e⇩2 e⇩3)
  then have "π⇩2 = []" by (auto dest: smallstepI_ps_eq)
  with s_Tr obtain eP⇩2 π eV⇩2 where ih: "≪[], eP≫ P→i ≪π, eP⇩2≫ ∧ ≪π, eV≫ V→i ≪[], eV⇩2≫ ∧ {$$} ⊢ e⇩2, eP⇩2, eV⇩2 : τ"
    apply atomize_elim
    apply (rule s_Tr(2))
    apply auto
    done
  from ‹π⇩2 = []› ih s_Tr(1,3-) show ?case
    apply -
    apply (rule lemma5[of e⇩2 eP⇩2 eV⇩2 τ e⇩3])
    apply simp
    apply simp
    subgoal for eP⇩3 eV⇩3 π'
      apply (rule exI[of _ "π @ π'"])
      apply (rule exI[of _ eP⇩3])
      apply (rule exI[of _ eV⇩3])
      apply (rule conjI) (* Prover step *)
      apply (rule smallsteps.s_Tr[of "[]" eP P i π eP⇩2 "π @ π'" eP⇩3])
      apply simp
      apply simp
      apply (rule conjI) (* Verifier step *)
      apply (rule smallsteps.s_Tr[of "π @ π'" eV V i π' eV⇩2 "[]" eV⇩3])
      apply (rule iffD1[OF smallstepsV_ps_append[of π eV i "[]" eV⇩2 π', simplified]])
      using iffD2[OF smallstepV_ps_append] by auto
    done
qed

lemma theorem1_security:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ π⇩A, eV ≫ V→i ≪ π', eV' ≫"
shows "(∃e' eP' π. ≪ [], e ≫ I→i ≪ [], e' ≫ ∧ ≪ [], eP ≫ P→i ≪ π, eP' ≫ ∧ π⇩A = π @ π' ∧ {$$} ⊢ e', eP', eV' : τ) ∨
       (∃eP' j π⇩0 π⇩0' s s'. j ≤ i ∧ ≪ [], eP ≫ P→j ≪ π⇩0 @ [s], eP' ≫ ∧ π⇩A = π⇩0 @ [s'] @ π⇩0' @ π' ∧ s ≠ s' ∧ hash s = hash s' ∧ closed s ∧ closed s')"
using assms(2,1) proof (induct π⇩A eV V i π' eV' rule: smallsteps.induct)
  case (s_Id π e)
  then show ?case by blast
next
  case (s_Tr π⇩1 eV⇩1 i π⇩2 eV⇩2 π⇩3 eV⇩3)
  then obtain e⇩2 π eP⇩2 j π⇩0 π⇩0' s s'
    where "≪[], e≫ I→i ≪[], e⇩2≫ ∧ ≪[], eP≫ P→i ≪π, eP⇩2≫ ∧ π⇩1 = π @ π⇩2 ∧ {$$} ⊢ e⇩2, eP⇩2, eV⇩2 : τ ∨
            j ≤ i ∧ ≪[], eP≫ P→j ≪π⇩0 @ [s], eP⇩2≫ ∧ closed s ∧ closed s' ∧ π⇩1 = π⇩0 @ [s'] @ π⇩0' @ π⇩2 ∧ s ≠ s' ∧ hash s = hash s'"
    apply atomize_elim
    apply (drule s_Tr(2))
    apply (auto 8 0)
    done
  with s_Tr(1,3-) show ?case
    apply -
    apply (erule disjE; (erule conjE)+)
    subgoal (* case 1 *)
      apply (rule lemma6[of e⇩2 eP⇩2 eV⇩2 τ π⇩2 π⇩3 eV⇩3])
      apply simp
      apply simp
      subgoal for e⇩3 eP⇩3 π'
        apply (erule disjE)
        apply (erule conjE)+ (* case 1.1 *)
        apply (rule disjI1)
        apply (rule exI[of _ e⇩3])
        apply (rule exI[of _ eP⇩3])
        apply (rule exI)+
        apply (rule conjI, simp)
        apply (rule conjI)
        apply (rule smallsteps.s_Tr[of "[]" eP P i π eP⇩2 "π @ π'" eP⇩3])
        apply simp
        apply (rule iffD1[OF smallstepP_ps_prepend[of "[]", simplified]])
        using iffD2[OF smallstepP_ps_prepend] apply auto []
         apply simp
        apply (erule exE conjE)+
          (* case 1.2 *)
        subgoal for s s'
          apply (rule disjI2)
          apply (rule exI[of _ eP⇩3])
          apply (rule exI[of _ "i+1"])
          apply (rule exI[of _ π])
          apply (rule exI[of _ "[]"])
          apply (rule exI[of _ s])
          apply (rule exI[of _ s'])
          apply (rule conjI)
          apply simp
          apply (rule conjI)
          apply (rule smallsteps.s_Tr[of _ _ _ _ π eP⇩2])
          apply simp
          apply (rule iffD1[OF smallstepP_ps_prepend[of "[]", simplified]])
          using iffD2[OF smallstepP_ps_prepend] apply auto []
          apply simp
          done
        done
      done
        (* case 2 *)
    apply (erule smallstepV_consumes_proofstream)
    subgoal for π⇩0''
      apply (rule disjI2)
      apply (rule exI[of _ eP⇩2])
      apply (rule exI[of _ j])
      apply (rule exI[of _ π⇩0])
      apply (rule exI[of _ "π⇩0' @ π⇩0''"])
      apply (rule exI[of _ s])
      apply (rule exI[of _ s'])
      apply auto
      done
    done
qed

lemma remark1_single:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ πP, eP ≫ P→ ≪ πP @ π, eP' ≫"
  obtains e' eV' where "{$$} ⊢ e', eP', eV' : τ ∧ ≪ [], e ≫ I→ ≪ [], e' ≫ ∧ ≪ π, eV ≫ V→ ≪ [], eV' ≫"
  using assms [[simproc del: alpha_lst]] apply atomize_elim
proof (nominal_induct "{$$}::tyenv" e eP eV τ avoiding: πP π eP' rule: agree.strong_induct)
  case (a_App e⇩1 eP⇩1 eV⇩1 τ⇩1 τ⇩2 e⇩2 eP⇩2 eV⇩2)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 eP⇩1')
    with a_App(2,3) show ?thesis by blast
  next
    case (App2 eP⇩2')
    with a_App(1,4) show ?thesis by blast
  next
    case (AppLam x eP)
    with a_App(1,3) show ?thesis
      apply -
      apply (rule a_Lam_inv_P)
      apply simp
      subgoal for v' vV'
        apply simp
        apply (rule exI[of _ "v'[e⇩2 / x]"])
        apply (rule exI[of _ "vV'[eV⇩2 / x]"])
        apply (auto simp: fresh_Pair del: s_AppLam intro!: s_AppLam lemma4)
        done
      done
  next
    case (AppRec x e)
    with a_App(1,3) show ?thesis
      apply -
      apply (rule a_Rec_inv_P)
      apply simp
      apply simp
      subgoal for y e'' eP'' eV''
        apply simp
        apply (rule exI[of _ "App (Lam y (e''[Rec x (Lam y e'') / x])) e⇩2"])
        apply (rule exI[of _ "App (Lam y (eV''[Rec x (Lam y eV'') / x])) eV⇩2"])
        apply (rule conjI)
        apply (rule agree.a_App)
        apply (subst (1 2 3) subst_term.simps(3)[symmetric])
        apply simp
        apply simp
        apply simp
        apply (rule lemma4)
        apply auto [6]
        apply (rule conjI)
        apply (subst subst_term.simps(3)[symmetric])
        apply simp
        apply (rule s_AppRec)
        apply (auto simp add: fresh_Pair) [2]
        apply (subst subst_term.simps(3)[symmetric])
        apply simp
        apply (rule s_AppRec)
        apply (auto simp add: fresh_Pair) [2]
        done
      done
  qed
next
  case (a_Let x e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  then have "atom x ♯ (eP⇩1, πP)" by auto
  with a_Let(12) show ?case
  proof (cases rule: s_Let_inv)
    case Let1
    with a_Let show ?thesis
      apply -
      apply (rule exI[of _ "e⇩2[e⇩1 / x]"])
      apply (rule exI[of _ "eV⇩2[eV⇩1 / x]"])
      apply (auto intro!: lemma4)
      done
  next
    case (Let2 eP⇩1')
    with a_Let(9) obtain e⇩1' eV⇩1'
      where ih: "{$$} ⊢ e⇩1', eP⇩1', eV⇩1' : τ⇩1" "≪[], e⇩1≫ I→ ≪[], e⇩1'≫" "≪π, eV⇩1≫ V→ ≪[], eV⇩1'≫"
      by blast
    from a_Let Let2 have "¬ value e⇩1" "¬ value eP⇩1" "¬ value eV⇩1" by auto
    with Let2 a_Let(2,5,7,10) ih show ?thesis
      apply -
      apply (rule exI[of _ "Let e⇩1' x e⇩2"])
      apply (rule exI[of _ "Let eV⇩1' x eV⇩2"])
      apply (fastforce simp: fresh_Pair del: agree.a_Let intro!: agree.a_Let)
      done
  qed
next
  case (a_Case e eP eV τ⇩1 τ⇩2 e⇩1 eP⇩1 eV⇩1 τ e⇩2 eP⇩2 eV⇩2)
  from a_Case(7) show ?case
  proof (cases rule: s_Case_inv)
    case (Case eP'')
    with a_Case(2,3,5) show ?thesis by blast
  next
    case (Inj1 v)
    with a_Case(1,3,5) show ?thesis by blast
  next
    case (Inj2 v)
    with a_Case(1,3,5) show ?thesis by blast
  qed
next
  case (a_Prj1 e eP eV τ⇩1 τ⇩2 πP π eP')
  from a_Prj1(3) show ?case
  proof (cases rule: s_Prj1_inv)
    case (Prj1 eP'')
    with a_Prj1(2) show ?thesis by blast
  next
    case (PrjPair1 v⇩2)
    with a_Prj1(1) show ?thesis by fastforce
  qed
next
  case (a_Prj2 v vP vV τ⇩1 τ⇩2)
  from a_Prj2(3) show ?case
  proof (cases rule: s_Prj2_inv)
    case (Prj2 eP'')
    with a_Prj2(2) show ?thesis by blast
  next
    case (PrjPair2 v⇩2)
    with a_Prj2(1) show ?thesis by fastforce
  qed
next
  case (a_Roll α e eP eV τ)
  from a_Roll(7) show ?case
  proof (cases rule: s_Roll_inv)
    case (Roll eP'')
    with a_Roll(4,5,6) show ?thesis by blast
  qed
next
  case (a_Unroll α e eP eV τ)
  from a_Unroll(7) show ?case
  proof (cases rule: s_Unroll_inv)
    case (Unroll eP'')
    with a_Unroll(5,6) show ?thesis by fastforce
  next
    case UnrollRoll
    with a_Unroll(5) show ?thesis by blast
  qed
next
  case (a_Auth e eP eV τ)
  from a_Auth(3) show ?case
  proof (cases rule: s_AuthP_inv)
    case (Auth eP'')
    with a_Auth(3) show ?thesis
      by (auto dest!: a_Auth(2)[of πP π eP''])
  next
    case AuthP
    with a_Auth(1) show ?thesis
      apply -
      apply (rule exI[of _ e])
      apply (rule exI[of _ "Hash (hash ⦇eP⦈)"])
      apply (auto simp: lemma2_1)
      done
  qed
next
  case (a_Unauth e eP eV τ)
  from a_Unauth(1) have eP_closed: "closed eP"
    using agree_empty_fresh by simp
  from a_Unauth(3) show ?case
  proof (cases rule: s_UnauthP_inv)
    case (Unauth e')
    with a_Unauth(2) show ?thesis
      by blast
  next
    case (UnauthP h)
    with a_Unauth(1,3) eP_closed show ?thesis
      apply -
      apply (rule a_AuthT_value_inv)
      apply simp
      apply (auto 0 4 simp: fresh_shallow)
      done
  qed
next
  case (a_Inj1 e eP eV τ⇩1 τ⇩2)
  from a_Inj1(3) show ?case
  proof (cases rule: s_Inj1_inv)
    case (Inj1 eP'')
    with a_Inj1(1,2) show ?thesis by blast
  qed
next
  case (a_Inj2 e eP eV τ⇩2 τ⇩1)
  from a_Inj2(3) show ?case
  proof (cases rule: s_Inj2_inv)
    case (Inj2 eP'')
    with a_Inj2(1,2) show ?thesis by blast
  qed
next
  case (a_Pair e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 eP⇩1')
    with a_Pair(1,2,3) show ?thesis by blast
  next
    case (Pair2 eP⇩2')
    with a_Pair(1,3,4) show ?thesis by blast
  qed
qed (auto dest: value_no_step)

lemma remark1:
  assumes "{$$} ⊢ e, eP, eV : τ"
  and     "≪ π⇩P, eP ≫ P→i ≪ π⇩P @ π, eP' ≫"
  obtains e' eV'
  where "{$$} ⊢ e', eP', eV' : τ" "≪ [], e ≫ I→i ≪ [], e' ≫" "≪ π, eV ≫ V→i ≪ [], eV' ≫"
  using assms apply (atomize_elim, rotate_tac)
proof (nominal_induct π⇩P eP P i "π⇩P @ π" eP' arbitrary: π rule: smallsteps.strong_induct)
  case (s_Id e πP)
  then show ?case
    using s_Id_inv by blast
next
  case (s_Tr π⇩1 eP⇩1 i π⇩2 eP⇩2 eP⇩3)
  from s_Tr obtain π' where "π⇩2 = π⇩1 @ π'"
    by (auto elim: smallstepsP_generates_proofstream)
  with s_Tr obtain e⇩2 eV⇩2 where ih: "{$$} ⊢ e⇩2, eP⇩2, eV⇩2 : τ"
    "≪[], e≫ I→i ≪[], e⇩2≫" "≪π', eV≫ V→i ≪[], eV⇩2≫"
    by atomize_elim (auto elim: s_Tr(2)[of π'])
  with ‹π⇩2 = π⇩1 @ π'› s_Tr(1,3-) show ?case
    apply simp
    apply (drule iffD2[OF smallstepP_ps_prepend])
    apply (erule smallstepP_generates_proofstream)
    subgoal for π''
      apply simp
      apply (erule remark1_single[of e⇩2 eP⇩2 eV⇩2 τ π' π'' eP⇩3])
      using s_Tr(3) apply simp
      apply (drule iffD2[OF smallstepP_ps_prepend])
      apply simp
      by (metis ih(2) ih(3) self_append_conv2 smallsteps.s_Tr iffD1[OF smallstepsV_ps_append])
    done
qed

end