SSL Results.thy

(* Author: Matthias Brun,   ETH Zürich, 2019 *)
(* Author: Dmitriy Traytel, ETH Zürich, 2019 *)

section ‹Formalization of Miller et al.'s~cite‹"adsg"› Main Results›

(*<*)
theory Results
  imports Agreement
begin
(*>*)

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

subsection ‹Lemma 2.1›

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

subsection ‹Counterexample to Lemma 2.2›

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₁ e₁' e₂)
  from s_App1(3) value_no_step[OF s_App1(1)] show ?case
    by (auto dest!: s_App1(2))
next
  case (s_App2 v₁ e₂ e₂')
  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]])
  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
      apply (auto simp: fresh_Pair AppRec(1))
      apply (rule box_equals[OF _ subst_term_perm[symmetric, of z] subst_term_perm[symmetric, of z]])
      using AppRec(1) apply auto
      done
  qed (auto dest: value_no_step)
next
  case (s_Let1 x e₁ e₁' e₂)
  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₁ e₂)
  from s_Case(2,3) value_no_step[OF s_Case(1)] show ?case
    by auto
next
  case (s_Pair1 e₁ e₁' e₂)
  from s_Pair1(2,3) value_no_step[OF s_Pair1(1)] show ?case
    by auto
next
  case (s_Pair2 v₁ e₂ e₂')
  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₁ i π₂ e₂ e₃)
  from s_Tr(4) show ?case
  proof (cases rule: smallsteps.cases)
    case _: (s_Tr i π₄ e₄)
    with s_Tr(1,3) s_Tr(2)[of e₄] show ?thesis
      using smallstepsI_ps_emptyD(2)[of e₁ i π₄ e₄] smallstepI_ps_eq[of π₂ e₂ "[]" e₃]
      by (auto intro!: smallstep_ideal_deterministic elim!: smallstepI_ps_emptyD)
  qed simp
qed auto

subsection ‹Lemma 2.3›

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
    by (induct Γ) (auto simp: judge_weak_weakening_2 fmmap_fmupd judge_weak_fresh_env_fresh_term fresh_tyenv_None)
qed (simp_all add: fresh_fmmap_erase_fresh fmmap_fmupd judge_weak_fresh_env_fresh_term)

subsection ‹Lemma 2.4›

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

subsection ‹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
      by (auto simp add: a_Var dest!: fmdomI split: option.splits)
  qed
next
  case (j_Lam x Γ τ₁ e τ₂)
  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 $$:= τ₁) ⊨ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : τ₂"
    by (intro j_Lam(7)[of A vs vPs vVs]) (auto simp: fresh_tyenv_None)
  with j_Lam(1-5) show ?case
    by (auto simp: fresh_fmdrop_fset)
next
  case (j_App Γ e τ₁ τ₂ e')
  then have "fmdrop_fset A Γ ⊨ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Fun τ₁ τ₂"
    and "fmdrop_fset A Γ ⊨ psubst_term e' vs, psubst_term e' vPs, psubst_term e' vVs : τ₁"
    by simp_all
  then show ?case
    by auto
next
  case (j_Let x Γ e₁ τ₁ e₂ τ₂)
  from j_Let(4) have [simp]: "A |-| {|x|} = A"
    by (simp add: fresh_fset_fminus)
  from j_Let(8,11-) have "fmdrop_fset A Γ ⊨ psubst_term e₁ vs, psubst_term e₁ vPs, psubst_term e₁ vVs : τ₁"
    by simp
  moreover from j_Let(4,5,11-) have "fmdrop_fset A Γ(x $$:= τ₁) ⊨ psubst_term e₂ vs, psubst_term e₂ vPs, psubst_term e₂ vVs : τ₂"
    by (intro j_Let(10)) (auto simp: fresh_tyenv_None)
  ultimately show ?case using j_Let(1-6)
    by (auto simp: fresh_fmdrop_fset fresh_Pair fresh_psubst)
next
  case (j_Rec x Γ y τ₁ τ₂ 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 τ₁ τ₂) ⊨ psubst_term (Lam y e') vs, psubst_term (Lam y e') vPs, psubst_term (Lam y e') vVs : Fun τ₁ τ₂"
    by (intro j_Rec(13)) (auto simp: fresh_tyenv_None)
  with j_Rec(1-11) show ?case
    by (auto simp: fresh_fmdrop_fset)
next
  case (j_Case Γ e τ₁ τ₂ e₁ τ e₂)
  then have "fmdrop_fset A Γ ⊨ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Sum τ₁ τ₂"
    and "fmdrop_fset A Γ ⊨ psubst_term e₁ vs, psubst_term e₁ vPs, psubst_term e₁ vVs : Fun τ₁ τ"
    and "fmdrop_fset A Γ ⊨ psubst_term e₂ vs, psubst_term e₂ vPs, psubst_term e₂ vVs : Fun τ₂ τ"
    by simp_all
  then show ?case
    by auto
next
  case (j_Prj1 Γ e τ₁ τ₂)
  then have "fmdrop_fset A Γ ⊨ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod τ₁ τ₂"
    by simp
  then show ?case
    by auto
next
  case (j_Prj2 Γ e τ₁ τ₂)
  then have "fmdrop_fset A Γ ⊨ psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod τ₁ τ₂"
    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 Γ

subsection ‹Lemma 4›

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
  proof (induct Γ)
    case fmempty
    then show ?case by (metis agree.a_Var fmupd_lookup option.sel subst_term.simps(2))
  next
    case (fmupd x y Γ)
    then show ?case
      using agree_weakening_2 fresh_tyenv_None by auto
  qed
next
  case (a_Lam y τ₁ e eP eV τ₂)
  from a_Lam(1,2,5,6,7-) show ?case
    using agree_empty_fresh by (auto simp: fmupd_reorder_neq)
next
  case (a_App v₁ v₂ v₁P v₂P v₁V v₂V τ₁ τ₂)
  from a_App(5-) show ?case
    by (auto intro: a_App(2,4))
next
  case (a_Let y e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  then show ?case
    using agree_empty_fresh by (auto simp: fmupd_reorder_neq intro!: agree.a_Let[where x=y])
next
  case (a_Rec y z τ₁ τ₂ 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
    using a_Rec(9)[OF fmupd_reorder_neq]
    by (auto simp: fmupd_reorder_neq intro!: agree.a_Rec[where x=y])
next
  case (a_Case v v₁ v₂ vP v₁P v₂P vV v₁V v₂V τ₁ τ₂ τ)
  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

subsection ‹Lemma 5: Single-Step 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' ≫"
proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV τ avoiding: e' rule: agree.strong_induct)
  case (a_App e₁ eP₁ eV₁ τ₁ τ₂ e₂ eP₂ eV₂)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 e₁')
    with a_App(2) obtain eP₁' eV₁' π where *: "{$$} ⊨ e₁', eP₁', eV₁' : Fun τ₁ τ₂"
      "∀π_P. ≪π_P, eP₁≫ P→ ≪π_P @ π, eP₁'≫" "∀π'. ≪π @ π', eV₁≫ V→ ≪π', eV₁'≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * App1 a_App(1,3,5-)
      show "{$$} ⊨ e', App eP₁' eP₂, App eV₁' eV₂ : τ₂"
        "∀π_P. ≪π_P, App eP₁ eP₂≫ P→ ≪π_P @ π, App eP₁' eP₂≫"
        "∀π'. ≪π @ π', App eV₁ eV₂≫ V→ ≪π', App eV₁' eV₂≫"
        by auto
    qed
  next
    case (App2 e₂')
    with a_App(4) obtain eP₂' eV₂' π where *: "{$$} ⊨ e₂', eP₂', eV₂' : τ₁"
      "∀π_P. ≪π_P, eP₂≫ P→ ≪π_P @ π, eP₂'≫" "∀π'. ≪π @ π', eV₂≫ V→ ≪π', eV₂'≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * App2 a_App(1,3,5-)
      show "{$$} ⊨ e', App eP₁ eP₂', App eV₁ eV₂' : τ₂"
        "∀π_P. ≪π_P, App eP₁ eP₂≫ P→ ≪π_P @ π, App eP₁ eP₂'≫"
        "∀π'. ≪π @ π', App eV₁ eV₂≫ V→ ≪π', App eV₁ eV₂'≫"
        by auto
    qed
  next
    case (AppLam x e)
    from a_App(1)[unfolded ‹e₁ = Lam x e›] show ?thesis
    proof (cases rule: a_Lam_inv_I[case_names _ Lam])
      case (Lam eP eV)
      show ?thesis
      proof (intro exI conjI)
        from Lam a_App(3,5) AppLam show "{$$} ⊨ e', eP[eP₂ / x], eV[eV₂ / x] : τ₂"
          by (auto intro: lemma4)
        from Lam a_App(3,5) AppLam show "∀π_P. ≪π_P, App eP₁ eP₂≫ P→ ≪π_P @ [], eP[eP₂ / x]≫"
          by (intro allI iffD1[OF smallstepP_ps_prepend[where π = "[]", simplified]])
            (auto simp: fresh_Pair intro!: s_AppLam[where v=eP₂])
        from Lam a_App(3,5) AppLam show "∀π'. ≪[] @ π', App eV₁ eV₂≫ V→ ≪π', eV[eV₂ / x]≫"
          by (intro allI iffD1[OF smallstepV_ps_append[where π' = "[]", simplified]])
            (auto simp: fresh_Pair intro!: s_AppLam[where v=eV₂])
      qed
    qed simp
  next
    case (AppRec x e)
    from a_App(1)[unfolded ‹e₁ = Rec x e›] show ?thesis
    proof (cases rule: a_Rec_inv_I[consumes 1, case_names _ Rec])
      case (Rec y e'' eP' eV')
      from Rec(5,4) show ?thesis
      proof (cases rule: a_Lam_inv_I[consumes 1, case_names _ Lam])
        case (Lam eP'' eV'')
        show ?thesis
        proof (intro conjI exI[of _ "[]"] exI)
          let ?eP = "App (Lam y eP''[Rec x (Lam y eP'') / x]) eP₂"
          let ?eV = "App (Lam y eV''[Rec x (Lam y eV'') / x]) eV₂"
          from a_App(3) AppRec have [simp]: "value eP₂" "atom x ♯ eP₂" "value eV₂" "atom x ♯ eV₂"
            by (auto simp: fresh_Pair)
          from Lam a_App(3,5-) AppRec Rec show "{$$} ⊨ e', ?eP, ?eV : τ₂"
            unfolding term.eq_iff Abs1_eq(3)
            by (auto simp: fmupd_reorder_neq
              intro!: agree.a_App[where Γ="{$$}"] a_Lam[where x=y] lemma4)
          from Lam a_App(3,5-) AppRec Rec show "∀π_P. ≪π_P, App eP₁ eP₂≫ P→ ≪π_P @ [], ?eP≫"
            unfolding term.eq_iff Abs1_eq(3)
            using s_AppRec[where v=eP₂ and x=x and π="[]" and e="Lam y eP''" and uv=P]
            by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]])
              (auto simp: fresh_Pair simp del: s_AppRec)
          from Lam a_App(3,5-) AppRec Rec show "∀π'. ≪[] @ π', App eV₁ eV₂≫ V→ ≪π', ?eV≫"
            unfolding term.eq_iff Abs1_eq(3)
            using s_AppRec[where v=eV₂ and x=x and π="[]" and e="Lam y eV''" and uv=V]
            by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]])
              (auto simp: fresh_Pair simp del: s_AppRec)
        qed
      qed (simp add: fresh_fmap_update)
    qed simp
  qed
next
  case (a_Let x e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  then have "atom x ♯ (e₁, [])" by auto
  with a_Let(10) show ?case
  proof (cases rule: s_Let_inv)
    case Let1
    show ?thesis
    proof (intro conjI exI[of _ "[]"] exI)
      from a_Let(6,8) Let1 show "{$$} ⊨ e', eP₂[eP₁ / x], eV₂[eV₁ / x] : τ₂"
        by (auto intro: lemma4)
      from a_Let(4,6) Let1 show "∀π_P. ≪π_P, Let eP₁ x eP₂≫ P→ ≪π_P @ [], eP₂[eP₁ / x]≫"
        by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Let2) auto
      from a_Let(5,6) Let1 show "∀π'. ≪[] @ π', Let eV₁ x eV₂≫ V→ ≪π', eV₂[eV₁ / x]≫"
        by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]] s_Let2) auto
    qed
  next
    case (Let2 e₁')
    moreover
    from Let2 a_Let(7) obtain eP₁' eV₁' π
      where ih: "{$$} ⊨ e₁', eP₁', eV₁' : τ₁"
        "∀π_P. ≪π_P, eP₁≫ P→ ≪π_P @ π, eP₁'≫"
        "∀π'. ≪π @ π', eV₁≫ V→ ≪π', eV₁'≫"
      by (blast dest: spec[of _ "[]"])
    then have [simp]: "atom x ♯ ({$$}, e₁', eP₁', eV₁')"
      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₁' x e₂, Let eP₁' x eP₂, Let eV₁' x eV₂ : τ₂"
      by auto
    moreover from a_Let(4,5) ih(1) spec[OF ih(2), of "[]", simplified]
    have "≪π', Let eP₁ x eP₂≫ P→ ≪π' @ π, Let eP₁' x eP₂≫" for π'
      by (intro iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Let1) (auto simp: fresh_Pair)
    moreover from a_Let(4,5) ih(1) spec[OF ih(3), of "[]", simplified]
    have "≪π @ π', Let eV₁ x eV₂≫ V→ ≪π', Let eV₁' x eV₂≫" for π'
      by (intro iffD1[OF smallstepV_ps_append[of π _ "[]", simplified]] s_Let1) (auto simp: fresh_Pair)
    ultimately show ?thesis
      by blast
  qed
next
  case (a_Case e eP eV τ₁ τ₂ e₁ eP₁ eV₁ τ e₂ eP₂ eV₂)
  from a_Case(7) show ?case
  proof (cases rule: s_Case_inv)
    case (Case e'')
    with a_Case(2)[of e''] obtain eP'' eV'' π where ih: "{$$} ⊨ e'', eP'', eV'' : Syntax.Sum τ₁ τ₂"
      "∀π_P. ≪π_P, eP≫ P→ ≪π_P @ π, eP''≫" "∀π'. ≪π @ π', eV≫ V→ ≪π', eV''≫"
      by blast
    show ?thesis
    proof (intro conjI exI[of _ π] exI)
      from ih(1) a_Case(3,5) Case show "{$$} ⊨ e', Case eP'' eP₁ eP₂, Case eV'' eV₁ eV₂ : τ"
        by auto
      from a_Case(5) spec[OF ih(2), of "[]", simplified]
      show "∀π_P. ≪π_P, Case eP eP₁ eP₂≫ P→ ≪π_P @ π, Case eP'' eP₁ eP₂≫"
        by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Case) auto
      from a_Case(5) spec[OF ih(3), of "[]", simplified]
      show "∀π'. ≪π @ π', Case eV eV₁ eV₂≫ V→ ≪π', Case eV'' eV₁ eV₂≫"
        by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]] s_Case) auto
    qed
  next
    case (Inj1 v)
    from a_Case(1)[unfolded ‹e = Inj1 v›] show ?thesis
    proof (cases rule: a_Inj1_inv_I[consumes 1, case_names Case])
      case (Case vP vV)
      with a_Case(3,5) Inj1 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        from Case a_Case(3,5) Inj1 show "{$$} ⊨ e', App eP₁ vP, App eV₁ vV : τ"
          by auto
      qed auto
    qed
  next
    case (Inj2 v)
    from a_Case(1)[unfolded ‹e = Inj2 v›] show ?thesis
    proof (cases rule: a_Inj2_inv_I[consumes 1, case_names Case])
      case (Case vP vV)
      with a_Case(3,5) Inj2 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        from Case a_Case(3,5) Inj2 show "{$$} ⊨ e', App eP₂ vP, App eV₂ vV : τ"
          by auto
      qed auto
    qed
  qed
next
  case (a_Prj1 e eP eV τ₁ τ₂)
  from a_Prj1(3) show ?case
  proof (cases rule: s_Prj1_inv)
    case (Prj1 e'')
    then show ?thesis
      by (blast dest!: a_Prj1(2))
  next
    case (PrjPair1 v₂)
    from a_Prj1(1)[unfolded ‹e = Syntax.Pair e' v₂›] show ?thesis
    proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
      case (Pair eP₁ eV₁ eP₂ eV₂)
      with PrjPair1 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        show "{$$} ⊨ e', eP₁, eV₁ : τ₁"
          by (rule Pair)
      qed auto
    qed
  qed
next
  case (a_Prj2 e eP eV τ₁ τ₂)
  from a_Prj2(3) show ?case
  proof (cases rule: s_Prj2_inv)
    case (Prj2 e'')
    then show ?thesis
      by (blast dest!: a_Prj2(2))
  next
    case (PrjPair2 v₁)
    from a_Prj2(1)[unfolded ‹e = Syntax.Pair v₁ e'›] show ?thesis
    proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
      case (Pair eP₁ eV₁ eP₂ eV₂)
      with PrjPair2 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        show "{$$} ⊨ e', eP₂, eV₂ : τ₂"
          by (rule Pair)
      qed auto
    qed
  qed
next
  case (a_Roll α e eP eV τ)
  from a_Roll(5) show ?case
  proof (cases rule: s_Roll_inv)
    case (Roll e'')
    with a_Roll(4) obtain eP'' eV'' π where *: "{$$} ⊨ e'', eP'', eV'' : subst_type τ (Mu α τ) α"
      "∀π_P. ≪π_P, eP≫ P→ ≪π_P @ π, eP''≫" "∀π'. ≪π @ π', eV≫ V→ ≪π', eV''≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * Roll
      show "{$$} ⊨ e', Roll eP'', Roll eV'' : Mu α τ"
        "∀π_P. ≪π_P, Roll eP≫ P→ ≪π_P @ π, Roll eP''≫"
        "∀π'. ≪π @ π', Roll eV≫ V→ ≪π', Roll eV''≫"
        by auto
    qed
  qed
next
  case (a_Unroll α e eP eV τ)
  from a_Unroll(5) show ?case
  proof (cases rule: s_Unroll_inv)
    case (Unroll e'')
    with a_Unroll(4) obtain eP'' eV'' π where *: "{$$} ⊨ e'', eP'', eV'' : Mu α τ"
      "∀π_P. ≪π_P, eP≫ P→ ≪π_P @ π, eP''≫" "∀π'. ≪π @ π', eV≫ V→ ≪π', eV''≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * Unroll
      show "{$$} ⊨ e', Unroll eP'', Unroll eV'' : subst_type τ (Mu α τ) α"
        "∀π_P. ≪π_P, Unroll eP≫ P→ ≪π_P @ π, Unroll eP''≫"
        "∀π'. ≪π @ π', Unroll eV≫ V→ ≪π', Unroll eV''≫"
        by auto
    qed
  next
    case UnrollRoll
    with a_Unroll(3)[unfolded ‹e = Roll e'›] show ?thesis
    proof (cases rule: a_Roll_inv_I[case_names Roll])
      case (Roll eP' eV')
      with UnrollRoll show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        show "{$$} ⊨ e', eP', eV' : subst_type τ (Mu α τ) α" by fact
      qed auto
    qed
  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
      by (blast dest!: a_Auth(2))
  next
    case AuthI
    with a_Auth(1) have "value eP" "value eV" by auto
    with a_Auth(1) AuthI(2) show ?thesis
    proof (intro conjI exI[of _ "[]"] exI)
      from a_Auth(1) AuthI(2) ‹value eP›
      show "{$$} ⊨ e', Hashed (hash (eP)) eP, Hash (hash (eP)) : AuthT τ"
        by (auto dest: lemma2_1 simp: fresh_shallow)
    qed (auto dest: lemma2_1 simp: fresh_shallow)
  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
      by (blast dest!: a_Unauth(2))
  next
    case UnauthI
    with a_Unauth(1) have "value eP" "value eV" by auto
    from a_Unauth(1) show ?thesis
    proof (cases rule: a_AuthT_value_inv[case_names _ _ _ Unauth])
      case (Unauth vP')
      show ?thesis
      proof (intro conjI exI[of _ "[(vP')]"] exI)
        from Unauth(1,2) UnauthI(2) a_Unauth(1)
        show "{$$} ⊨ e', vP', (vP') : τ"
          by (auto simp: fresh_shallow)
        then have "closed vP'"
          by auto
        with Unauth(1,2) a_Unauth(1) show
          "∀π_P. ≪π_P, Unauth eP≫ P→ ≪π_P @ [(vP')], vP'≫"
          "∀π'. ≪[(vP')] @ π', Unauth eV≫ V→ ≪π', (vP')≫"
          by (auto simp: fresh_shallow)
      qed
    qed (auto simp: ‹value e› ‹value eP› ‹value eV›)
  qed
next
  case (a_Pair e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 e₁')
    with a_Pair(1,3) show ?thesis
      by (blast dest!: a_Pair(2))
  next
    case (Pair2 e₂')
    with a_Pair(1,3) show ?thesis
      by (blast dest!: a_Pair(4))
  qed
next
  case (a_Inj1 e eP eV τ₁ τ₂)
  from a_Inj1(3) show ?case
  proof (cases rule: s_Inj1_inv)
    case (Inj1 e')
    with a_Inj1(1) show ?thesis
      by (blast dest!: a_Inj1(2))
  qed
next
  case (a_Inj2 e eP eV τ₂ τ₁)
  from a_Inj2(3) show ?case
  proof (cases rule: s_Inj2_inv)
    case (Inj2 e'')
    with a_Inj2(1) show ?thesis
      by (blast dest!: a_Inj2(2))
  qed
qed (simp, meson value.intros value_no_step)+

subsection ‹Lemma 6: Single-Step Security›

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')"
proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV τ avoiding: π_A π' eV' rule: agree.strong_induct)
  case (a_App e₁ eP₁ eV₁ τ₁ τ₂ e₂ eP₂ eV₂)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 eV₁')
    with a_App(1,3) show ?thesis
      by (blast dest!: a_App(2))
  next
    case (App2 e₂')
    with a_App(1,3) show ?thesis
      by (blast dest!: a_App(4))
  next
    case (AppLam x eV'')
    from a_App(1)[unfolded ‹eV₁ = Lam x eV''›] show ?thesis
    proof (cases rule: a_Lam_inv_V[case_names Lam])
      case (Lam e'' eP'')
      with a_App(3) AppLam show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from Lam a_App(3) AppLam show "{$$} ⊨ e''[e₂ / x], eP''[eP₂ / x], eV' : τ₂"
          by (auto intro: lemma4)
      qed (auto 0 3 simp: fresh_Pair intro!: s_AppLam[where π="[]"]
          intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
    qed
  next
    case (AppRec x eV'')
    from a_App(1)[unfolded ‹eV₁ = Rec x eV''›] show ?thesis
    proof (cases rule: a_Rec_inv_V[case_names _ Rec])
      case (Rec y e'''  eP''' eV''')
      with a_App(1,3) AppRec show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        let ?e = "App (Lam y e'''[Rec x (Lam y e''') / x]) e₂"
        let ?eP = "App (Lam y eP'''[Rec x (Lam y eP''') / x]) eP₂"
        from Rec a_App(3) AppRec show "{$$} ⊨ ?e, ?eP, eV' : τ₂"
          by (auto simp del: subst_term.simps(3) intro!: agree.a_App[where Γ="{$$}"] lemma4)
      qed (auto 0 3 simp del: subst_term.simps(3) simp: fresh_Pair intro!: s_AppRec[where π="[]"]
          intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
    qed simp
  qed
next
  case (a_Let x e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  then have "atom x ♯ (eV₁, π_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
    proof (intro conjI exI[of _ "[]"] exI disjI1)
      from Let1 a_Let(5,6,8,10) show "{$$} ⊨ e₂[e₁ / x], eP₂[eP₁ / x], eV' : τ₂"
        by (auto intro: lemma4)
    qed (auto 0 3 intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
  next
    case (Let2 eV₁')
    with a_Let(9)[of π_A π' eV₁'] obtain e₁' π eP₁' s s' where
      ih: "≪[], e₁≫ I→ ≪[], e₁'≫" "∀π_P. ≪π_P, eP₁≫ P→ ≪π_P @ π, eP₁'≫"
        "{$$} ⊨ e₁', eP₁', eV₁' : τ₁ ∧ π_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₁'" "atom x ♯ eP₁'"
      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
    proof (intro conjI exI[of _ "π"] exI)
      from ‹atom x ♯ π› Let2 a_Let(1-8,10,12-) fresh ih
      show "{$$} ⊨ Let e₁' x e₂, Let eP₁' x eP₂, eV' : τ₂ ∧ π_A = π @ π' ∨
        (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
        by auto
    qed (auto dest: spec[of _ "[]"] intro!: iffD1[OF smallstepP_ps_prepend, of "[]", simplified])
  qed
next
  case (a_Case e eP eV τ₁ τ₂ e₁ eP₁ eV₁ τ e₂ eP₂ eV₂)
  from a_Case(7) show ?case
  proof (cases rule: s_Case_inv)
    case (Case eV'')
    from a_Case(2)[OF Case(2)] show ?thesis
    proof (elim exE disjE conjE, goal_cases ok collision)
      case (ok e'' π eP'')
      with Case a_Case(3,5) show ?case by blast
    next
      case (collision e'' π eP'' s s')
      with Case a_Case(3,5) show ?case
      proof (intro exI[of _ "[s]"] exI conjI disjI2)
        from Case a_Case(3,5) collision show "≪[], Case e e₁ e₂≫ I→ ≪[], Case e'' e₁ e₂≫"
          "∀π_P. ≪π_P, Case eP eP₁ eP₂≫ P→ ≪π_P @ [s], Case eP'' eP₁ eP₂≫"
          by auto
        from collision show "closed s" "closed s'" "s ≠ s'" "hash s = hash s'" by auto
      qed simp
    qed
  next
    case (Inj1 vV)
    from a_Case(1)[unfolded ‹eV = Inj1 vV›] show ?thesis
    proof (cases rule: a_Inj1_inv_V[consumes 1, case_names Inj])
      case (Inj v' vP')
      with Inj1 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from a_Case(3) Inj Inj1 show "{$$} ⊨ App e₁ v', App eP₁ vP', eV' : τ"
          by auto
      qed auto
    qed
  next
    case (Inj2 vV)
    from a_Case(1)[unfolded ‹eV = Inj2 vV›] show ?thesis
    proof (cases rule: a_Inj2_inv_V[consumes 1, case_names Inj])
      case (Inj v' vP')
      with Inj2 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from a_Case(5) Inj Inj2 show "{$$} ⊨ App e₂ v', App eP₂ vP', eV' : τ"
          by auto
      qed auto
    qed
  qed
next
  case (a_Prj1 e eP eV τ₁ τ₂)
  from a_Prj1(3) show ?case
  proof (cases rule: s_Prj1_inv)
    case (Prj1 eV'')
    then show ?thesis
      by (blast dest!: a_Prj1(2))
  next
    case (PrjPair1 v₂)
    with a_Prj1(1) show ?thesis
    proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
      case (Pair e₁ eP₁ eV₁ e₂ eP₂ eV₂)
      with PrjPair1 a_Prj1(1) show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from Pair PrjPair1 a_Prj1(1) show "{$$} ⊨ e₁, eP₁, eV' : τ₁"
          by auto
      qed auto
    qed simp_all
  qed
next
  case (a_Prj2 e eP eV τ₁ τ₂)
  from a_Prj2(3) show ?case
  proof (cases rule: s_Prj2_inv)
    case (Prj2 eV'')
    then show ?thesis
      by (blast dest!: a_Prj2(2))
  next
    case (PrjPair2 v₂)
    with a_Prj2(1) show ?thesis
    proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
      case (Pair e₁ eP₁ eV₁ e₂ eP₂ eV₂)
      with PrjPair2 a_Prj2(1) show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from Pair PrjPair2 a_Prj2(1) show "{$$} ⊨ e₂, eP₂, eV' : τ₂"
          by auto
      qed auto
    qed simp_all
  qed
next
  case (a_Roll α e eP eV τ)
  from a_Roll(7) show ?case
  proof (cases rule: s_Roll_inv)
    case (Roll eV'')
    from a_Roll(6)[OF Roll(2)] obtain e'' π eP'' where ih:
      "≪[], e≫ I→ ≪[], e''≫" "∀π_P. ≪π_P, eP≫ P→ ≪π_P @ π, eP''≫"
      "{$$} ⊨ e'', eP'', eV'' : subst_type τ (Mu α τ) α ∧ π_A = π @ π' ∨
      (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
      by blast
    with Roll show ?thesis
    proof (intro exI[of _ "π"] exI conjI)
      from ih Roll show "{$$} ⊨ Roll e'', Roll eP'', eV' : Mu α τ ∧ π_A = π @ π' ∨
        (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
        by auto
    qed auto
  qed
next
  case (a_Unroll α e eP eV τ)
  from a_Unroll(7) show ?case
  proof (cases rule: s_Unroll_inv)
    case (Unroll eV'')
    from a_Unroll(6)[OF Unroll(2)] obtain e'' π eP'' where ih:
      "≪[], e≫ I→ ≪[], e''≫" "∀π_P. ≪π_P, eP≫ P→ ≪π_P @ π, eP''≫"
      "{$$} ⊨ e'', eP'', eV'' : Mu α τ ∧ π_A = π @ π' ∨
      (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
      by blast
    with Unroll show ?thesis
    proof (intro exI[of _ "π"] exI conjI)
      from ih Unroll show "{$$} ⊨ Unroll e'', Unroll eP'', eV' : subst_type τ (Mu α τ) α ∧ π_A = π @ π' ∨
        (∃s s'. closed s ∧ closed s' ∧ π = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
        by auto
    qed auto
  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'')
    from a_Auth(2)[OF Auth(2)] show ?thesis
    proof (elim exE disjE conjE, goal_cases ok collision)
      case (ok e'' π eP'')
      with Auth show ?case
      proof (intro conjI exI[of _ "π"] exI disjI1)
        from ok Auth show "{$$} ⊨ Auth e'', Auth eP'', eV' : AuthT τ"
          by auto
      qed auto
    next
      case (collision e'' π eP'' s s')
      then show ?case by blast
    qed
  next
    case AuthV
    with a_Auth(1) show ?thesis
    proof (intro exI[of _ "[]"] exI conjI disjI1)
      from a_Auth(1) AuthV show "{$$} ⊨ e, Hashed (hash (eP)) eP, eV' : AuthT τ"
        by (auto dest: lemma2_1)
    qed (auto simp: fresh_shallow)
  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
      by (blast dest!: a_Unauth(2))
  next
    case UnauthV
    from a_Unauth(1)[unfolded ‹eV = Hash (hash eV')›] UnauthV a_Unauth(1) show ?thesis
    proof (cases rule: a_AuthT_value_inv[consumes 1, case_names _ _ _ Hashed])
      case (Hashed vP')
      with UnauthV a_Unauth(1) show ?thesis
      proof (intro exI[of _ "[(vP')]"] exI conjI)
        from Hashed UnauthV a_Unauth(1) show "{$$} ⊨ e, vP', eV' : τ ∧ π_A = [(vP')] @ π' ∨
          (∃s s'. closed s ∧ closed s' ∧ [(vP')] = [s] ∧ π_A = [s'] @ π' ∧ s ≠ s' ∧ hash s = hash s')"
          by (fastforce elim: a_HashI_inv[where Γ="{$$}"])
      qed auto
    qed auto
  qed
next
  case (a_Pair e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 eV₁')
    with a_Pair(3) show ?thesis
      using a_Pair(2)[of π_A π' eV₁'] by blast
  next
    case (Pair2 eV₂')
    with a_Pair(1) show ?thesis
      using a_Pair(4)[of π_A π' eV₂'] by blast
  qed
next
  case (a_Inj1 e eP eV τ₁ τ₂)
  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 τ₂ τ₁)
  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)+

subsection ‹Theorem 1: Correctness›

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(2,1)
proof (atomize_elim, induct "[]::proofstream" e I i "[]::proofstream" e' rule: smallsteps.induct)
  case (s_Id e)
  then show ?case by auto
next
  case (s_Tr e₁ i π₂ e₂ e₃)
  then have "π₂ = []" by (auto dest: smallstepI_ps_eq)
  with s_Tr obtain eP₂ π eV₂ where ih:
    "≪[], eP≫ P→i ≪π, eP₂≫" "≪π, eV≫ V→i ≪[], eV₂≫" "{$$} ⊨ e₂, eP₂, eV₂ : τ"
    by (atomize_elim, intro s_Tr(2)) auto
  moreover obtain eP₃ eV₃ π' where agree: "{$$} ⊨ e₃, eP₃, eV₃ : τ"
    and "≪π_P, eP₂≫ P→ ≪π_P @ π', eP₃≫" "≪π' @ π'', eV₂≫ V→ ≪π'', eV₃≫"
  for π_P π'' using lemma5[OF ih(3) s_Tr(3)[unfolded ‹π₂ = []›], of thesis] by blast
  ultimately have "≪[], eP≫ P→i + 1 ≪π @ π', eP₃≫" "≪π @ π', eV≫ V→i + 1 ≪[], eV₃≫"
    by (auto simp: smallstepsV_ps_append[of _ _ _ "[]", simplified, symmetric]
       intro!: smallsteps.s_Tr[of "π @ π'"])
  with agree show ?case by blast
qed

subsection ‹Counterexamples to Theorem 1: Security›

text ‹Counterexample using administrative normal form.›

lemma security_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]
  have prover: "≪ [], t ≫ P→i ≪ [Inj1 Unit, Unit], Inj1 Unit ≫" ― ‹prover execution›
    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
  have verifier1: "≪ [Inj1 Unit, Unit], t ≫ V→i ≪ [], Inj1 Unit ≫" ― ‹verifier execution›
    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
  have verifier2: "≪ [Inj2 Unit, Unit], t ≫ V→i ≪ [], Inj2 Unit ≫" ― ‹verifier execution with proofstream containing collision›
    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

text ‹Alternative, shorter counterexample not in administrative normal form.›

lemma security_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]
  have prover: "≪ [], t ≫ P→i ≪ [Inj1 Unit, Unit], Inj1 Unit ≫" ― ‹prover execution›
    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
  have verifier1: "≪ [Inj1 Unit, Unit], t ≫ V→i ≪ [], Inj1 Unit ≫" ― ‹verifier execution›
    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
  have verifier2: "≪ [Inj2 Unit, Unit], t ≫ V→i ≪ [], Inj2 Unit ≫" ― ‹verifier execution with proofstream containing collision›
    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

subsection ‹Corrected Theorem 1: Security›

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 π₀ π₀' s s'. j ≤ i ∧ ≪ [], eP ≫ P→j ≪ π₀ @ [s], eP' ≫ ∧ π_A = π₀ @ [s'] @ π₀' @ π' ∧ 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 π₁ eV₁ i π₂ eV₂ π₃ eV₃)
  then obtain e₂ π eP₂ j π₀ π₀' s s'
    where "≪[], e≫ I→i ≪[], e₂≫ ∧ ≪[], eP≫ P→i ≪π, eP₂≫ ∧ π₁ = π @ π₂ ∧ {$$} ⊨ e₂, eP₂, eV₂ : τ ∨
            j ≤ i ∧ ≪[], eP≫ P→j ≪π₀ @ [s], eP₂≫ ∧ closed s ∧ closed s' ∧ π₁ = π₀ @ [s'] @ π₀' @ π₂ ∧ s ≠ s' ∧ hash s = hash s'"
    by blast
  then show ?case
  proof (elim disjE conjE, goal_cases ok collision)
    case ok
    obtain e₃ eP₃ π' where
      "≪[], e₂≫ I→ ≪[], e₃≫" "≪π_P, eP₂≫ P→ ≪π_P @ π', eP₃≫"
      "{$$} ⊨ e₃, eP₃, eV₃ : τ ∧ π₂ = π' @ π₃ ∨
      (∃s s'. closed s ∧ closed s' ∧ π' = [s] ∧ π₂ = [s'] @ π₃ ∧ s ≠ s' ∧ hash s = hash s')"
    for π_P using lemma6[OF ok(4) s_Tr(3), of thesis] by blast
    then show ?case
    proof (elim disjE conjE exE, goal_cases ok2 collision)
      case ok2
      with s_Tr(1,3-) ok show ?case
        by auto
    next
      case (collision s s')
      then show ?case
      proof (intro disjI2 exI conjI)
        from ok collision show "≪[], eP≫ P→i + 1 ≪π @ [s], eP₃≫"
          by (elim smallsteps.s_Tr) auto
        from ok collision show "π₁ = π @ [s'] @ [] @ π₃"
          by simp
      qed simp_all
    qed
  next
    case collision
    from s_Tr(3) collision show ?case
    proof (elim smallstepV_consumes_proofstream, intro disjI2 exI conjI)
      fix π₀''
      assume *: "π₂ = π₀'' @ π₃"
      from collision * show "π₁ = π₀ @ [s'] @ (π₀' @ π₀'') @ π₃"
        by simp
    qed simp_all
  qed
qed

subsection ‹Remark 1›

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' ≫"
proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV τ avoiding: πP π eP' rule: agree.strong_induct)
  case (a_App e₁ eP₁ eV₁ τ₁ τ₂ e₂ eP₂ eV₂)
  from a_App(5) show ?case
  proof (cases rule: s_App_inv)
    case (App1 eP₁')
    with a_App(2,3) show ?thesis by blast
  next
    case (App2 eP₂')
    with a_App(1,4) show ?thesis by blast
  next
    case (AppLam x eP)
    from a_App(1)[unfolded ‹eP₁ = Lam x eP›] show ?thesis
    proof (cases rule: a_Lam_inv_P[case_names Lam])
      case (Lam v' vV')
      with a_App(3) AppLam show ?thesis
        by (auto 0 4 simp: fresh_Pair del: s_AppLam intro!: s_AppLam lemma4)
    qed
  next
    case (AppRec x e)
    from a_App(1)[unfolded ‹eP₁ = Rec x e›] show ?thesis
    proof (cases rule: a_Rec_inv_P[case_names _ Rec])
      case (Rec y e'' eP'' eV'')
      show ?thesis
      proof (intro exI conjI)
        let ?e = "App (Lam y (e''[Rec x (Lam y e'') / x])) e₂"
        let ?eV = "App (Lam y (eV''[Rec x (Lam y eV'') / x])) eV₂"
        from a_App(3) Rec AppRec show "{$$} ⊨ ?e, eP', ?eV : τ₂"
          by (auto intro!: agree.a_App[where Γ="{$$}"] lemma4
            simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric])
        from a_App(3) Rec AppRec show "≪[], App e₁ e₂≫ I→ ≪[], ?e≫"
          by (auto intro!: s_AppRec[where v=e₂]
            simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
        from a_App(3) Rec AppRec show "≪π, App eV₁ eV₂≫ V→ ≪[], ?eV≫"
          by (auto intro!: s_AppRec[where v=eV₂]
            simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
      qed
    qed simp
  qed
next
  case (a_Let x e₁ eP₁ eV₁ τ₁ e₂ eP₂ eV₂ τ₂)
  then have "atom x ♯ (eP₁, πP)" by auto
  with a_Let(12) show ?case
  proof (cases rule: s_Let_inv)
    case Let1
    with a_Let show ?thesis
      by (intro exI[where P = "λx. ∃y. (Q x y)" for Q, OF exI, of _ "e₂[e₁ / x]" "eV₂[eV₁ / x]"])
        (auto intro!: lemma4)
  next
    case (Let2 eP₁')
    with a_Let(9) obtain e₁' eV₁'
      where ih: "{$$} ⊨ e₁', eP₁', eV₁' : τ₁" "≪[], e₁≫ I→ ≪[], e₁'≫" "≪π, eV₁≫ V→ ≪[], eV₁'≫"
      by blast
    from a_Let Let2 have "¬ value e₁" "¬ value eP₁" "¬ value eV₁" by auto
    with Let2 a_Let(2,5,7,10) ih show ?thesis
      by (intro exI[where P = "\<lambda>x. \<exists>y. (Q x y)" for Q, OF exI, of _ "Let e\<^sub>1' x e\<^sub>2" "Let eV\<^sub>1' x eV\<^sub>2"])
       (fastforce simp: fresh_Pair del: agree.a_Let intro!: agree.a_Let)
  qed
next
  case (a_Case e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>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 \<tau>\<^sub>1 \<tau>\<^sub>2 \<pi>P \<pi> 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\<^sub>2)
    with a_Prj1(1) show ?thesis by fastforce
  qed
next
  case (a_Prj2 v vP vV \<tau>\<^sub>1 \<tau>\<^sub>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\<^sub>2)
    with a_Prj2(1) show ?thesis by fastforce
  qed
next
  case (a_Roll \<alpha> e eP eV \<tau>)
  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 \<alpha> e eP eV \<tau>)
  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 \<tau>)
  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 \<pi>P \<pi> eP''])
  next
    case AuthP
    with a_Auth(1) show ?thesis
      by (auto 0 4 simp: lemma2_1 intro: exI[of _ "Hash (hash \<lparr>eP\<rparr>)"] exI[of _ e])
  qed
next
  case (a_Unauth e eP eV \<tau>)
  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
      by (force intro: a_AuthT_value_inv[OF a_Unauth(1)] simp: fresh_shallow)
  qed
next
  case (a_Inj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>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 \<tau>\<^sub>2 \<tau>\<^sub>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\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
  from a_Pair(5) show ?case
  proof (cases rule: s_Pair_inv)
    case (Pair1 eP\<^sub>1')
    with a_Pair(1,2,3) show ?thesis by blast
  next
    case (Pair2 eP\<^sub>2')
    with a_Pair(1,3,4) show ?thesis by blast
  qed
qed (auto dest: value_no_step)

lemma remark1:
  assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
  and     "\<lless> \<pi>\<^sub>P, eP \<ggreater> P\<rightarrow>i \<lless> \<pi>\<^sub>P @ \<pi>, eP' \<ggreater>"
  obtains e' eV'
  where "{$$} \<turnstile> e', eP', eV' : \<tau>" "\<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater>" "\<lless> \<pi>, eV \<ggreater> V\<rightarrow>i \<lless> [], eV' \<ggreater>"
  using assms(2,1)
proof (atomize_elim, nominal_induct \<pi>\<^sub>P eP P i "\<pi>\<^sub>P @ \<pi>" eP' arbitrary: \<pi> rule: smallsteps.strong_induct)
  case (s_Id e \<pi>P)
  then show ?case
    using s_Id_inv by blast
next
  case (s_Tr \<pi>\<^sub>1 eP\<^sub>1 i \<pi>\<^sub>2 eP\<^sub>2 eP\<^sub>3)
  from s_Tr obtain \<pi>' \<pi>'' where ps: "\<pi>\<^sub>2 = \<pi>\<^sub>1 @ \<pi>'" "\<pi> = \<pi>' @ \<pi>''"
    by (force elim: smallstepP_generates_proofstream smallstepsP_generates_proofstream)
  with s_Tr obtain e\<^sub>2 eV\<^sub>2 where ih: "{$$} \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>"
    "\<lless>[], e\<ggreater> I\<rightarrow>i \<lless>[], e\<^sub>2\<ggreater>" "\<lless>\<pi>', eV\<ggreater> V\<rightarrow>i \<lless>[], eV\<^sub>2\<ggreater>"
    by atomize_elim (auto elim: s_Tr(2)[of \<pi>'])
  moreover
  obtain e\<^sub>3 eV\<^sub>3 where agree: "{$$} \<turnstile> e\<^sub>3, eP\<^sub>3, eV\<^sub>3 : \<tau>" and
    "\<lless>[], e\<^sub>2\<ggreater> I\<rightarrow> \<lless>[], e\<^sub>3\<ggreater>" "\<lless>\<pi>'', eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>[], eV\<^sub>3\<ggreater>"
    by (rule remark1_single[OF ih(1) iffD2[OF smallstepP_ps_prepend s_Tr(3)[unfolded ps]]]) blast
  ultimately have "\<lless>[], e\<ggreater> I\<rightarrow>i + 1 \<lless>[], e\<^sub>3\<ggreater>" "\<lless>\<pi>, eV\<ggreater> V\<rightarrow>i + 1 \<lless>[], eV\<^sub>3\<ggreater>"
    by (auto simp: smallstepsV_ps_append[of _ _ _ "[]", simplified, symmetric] ps
       intro!: smallsteps.s_Tr[where m=V and \<pi>\<^sub>1="\<pi>' @ \<pi>''" and \<pi>\<^sub>2=\<pi>''])
  with agree show ?case
    by blast
qed

(*<*)
end
(*>*)