Theory Results

(* 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⇩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]])
  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⇩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

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 Γ τ⇩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"
    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 τ⇩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(8,11-) have "fmdrop_fset A Γ ⊢ psubst_term e⇩1 vs, psubst_term e⇩1 vPs, psubst_term e⇩1 vVs : τ⇩1"
    by simp
  moreover from j_Let(4,5,11-) have "fmdrop_fset A Γ(x $$:= τ⇩1) ⊢ psubst_term e⇩2 vs, psubst_term e⇩2 vPs, psubst_term e⇩2 vVs : τ⇩2"
    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 τ⇩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"
    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 τ⇩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 Γ

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 τ⇩1 e eP eV τ⇩2)
  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⇩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
    using agree_empty_fresh by (auto simp: fmupd_reorder_neq intro!: agree.a_Let[where x=y])
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
    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⇩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

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⇩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(2) obtain eP⇩1' eV⇩1' π where *: "{$$} ⊢ e⇩1', eP⇩1', eV⇩1' : Fun τ⇩1 τ⇩2"
      "∀π⇩P. ≪π⇩P, eP⇩1≫ P→ ≪π⇩P @ π, eP⇩1'≫" "∀π'. ≪π @ π', eV⇩1≫ V→ ≪π', eV⇩1'≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * App1 a_App(1,3,5-)
      show "{$$} ⊢ e', App eP⇩1' eP⇩2, App eV⇩1' eV⇩2 : τ⇩2"
        "∀π⇩P. ≪π⇩P, App eP⇩1 eP⇩2≫ P→ ≪π⇩P @ π, App eP⇩1' eP⇩2≫"
        "∀π'. ≪π @ π', App eV⇩1 eV⇩2≫ V→ ≪π', App eV⇩1' eV⇩2≫"
        by auto
    qed
  next
    case (App2 e⇩2')
    with a_App(4) obtain eP⇩2' eV⇩2' π where *: "{$$} ⊢ e⇩2', eP⇩2', eV⇩2' : τ⇩1"
      "∀π⇩P. ≪π⇩P, eP⇩2≫ P→ ≪π⇩P @ π, eP⇩2'≫" "∀π'. ≪π @ π', eV⇩2≫ V→ ≪π', eV⇩2'≫"
      by blast
    show ?thesis
    proof (intro exI conjI)
      from * App2 a_App(1,3,5-)
      show "{$$} ⊢ e', App eP⇩1 eP⇩2', App eV⇩1 eV⇩2' : τ⇩2"
        "∀π⇩P. ≪π⇩P, App eP⇩1 eP⇩2≫ P→ ≪π⇩P @ π, App eP⇩1 eP⇩2'≫"
        "∀π'. ≪π @ π', App eV⇩1 eV⇩2≫ V→ ≪π', App eV⇩1 eV⇩2'≫"
        by auto
    qed
  next
    case (AppLam x e)
    from a_App(1)[unfolded ‹e⇩1 = 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⇩2 / x], eV[eV⇩2 / x] : τ⇩2"
          by (auto intro: lemma4)
        from Lam a_App(3,5) AppLam show "∀π⇩P. ≪π⇩P, App eP⇩1 eP⇩2≫ P→ ≪π⇩P @ [], eP[eP⇩2 / x]≫"
          by (intro allI iffD1[OF smallstepP_ps_prepend[where π = "[]", simplified]])
            (auto simp: fresh_Pair intro!: s_AppLam[where v=eP⇩2])
        from Lam a_App(3,5) AppLam show "∀π'. ≪[] @ π', App eV⇩1 eV⇩2≫ V→ ≪π', eV[eV⇩2 / x]≫"
          by (intro allI iffD1[OF smallstepV_ps_append[where π' = "[]", simplified]])
            (auto simp: fresh_Pair intro!: s_AppLam[where v=eV⇩2])
      qed
    qed simp
  next
    case (AppRec x e)
    from a_App(1)[unfolded ‹e⇩1 = 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⇩2"
          let ?eV = "App (Lam y eV''[Rec x (Lam y eV'') / x]) eV⇩2"
          from a_App(3) AppRec have [simp]: "value eP⇩2" "atom x ♯ eP⇩2" "value eV⇩2" "atom x ♯ eV⇩2"
            by (auto simp: fresh_Pair)
          from Lam a_App(3,5-) AppRec Rec show "{$$} ⊢ e', ?eP, ?eV : τ⇩2"
            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⇩1 eP⇩2≫ P→ ≪π⇩P @ [], ?eP≫"
            unfolding term.eq_iff Abs1_eq(3)
            using s_AppRec[where v=eP⇩2 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⇩1 eV⇩2≫ V→ ≪π', ?eV≫"
            unfolding term.eq_iff Abs1_eq(3)
            using s_AppRec[where v=eV⇩2 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⇩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
    show ?thesis
    proof (intro conjI exI[of _ "[]"] exI)
      from a_Let(6,8) Let1 show "{$$} ⊢ e', eP⇩2[eP⇩1 / x], eV⇩2[eV⇩1 / x] : τ⇩2"
        by (auto intro: lemma4)
      from a_Let(4,6) Let1 show "∀π⇩P. ≪π⇩P, Let eP⇩1 x eP⇩2≫ P→ ≪π⇩P @ [], eP⇩2[eP⇩1 / x]≫"
        by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Let2) auto
      from a_Let(5,6) Let1 show "∀π'. ≪[] @ π', Let eV⇩1 x eV⇩2≫ V→ ≪π', eV⇩2[eV⇩1 / x]≫"
        by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]] s_Let2) auto
    qed
  next
    case (Let2 e⇩1')
    moreover
    from Let2 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 dest: spec[of _ "[]"])
    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
    moreover from a_Let(4,5) ih(1) spec[OF ih(2), of "[]", simplified]
    have "≪π', Let eP⇩1 x eP⇩2≫ P→ ≪π' @ π, Let eP⇩1' x eP⇩2≫" 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⇩1 x eV⇩2≫ V→ ≪π', Let eV⇩1' x eV⇩2≫" 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 τ⇩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(2)[of e''] obtain eP'' eV'' π where ih: "{$$} ⊢ e'', eP'', eV'' : Syntax.Sum τ⇩1 τ⇩2"
      "∀π⇩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⇩1 eP⇩2, Case eV'' eV⇩1 eV⇩2 : τ"
        by auto
      from a_Case(5) spec[OF ih(2), of "[]", simplified]
      show "∀π⇩P. ≪π⇩P, Case eP eP⇩1 eP⇩2≫ P→ ≪π⇩P @ π, Case eP'' eP⇩1 eP⇩2≫"
        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⇩1 eV⇩2≫ V→ ≪π', Case eV'' eV⇩1 eV⇩2≫"
        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⇩1 vP, App eV⇩1 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⇩2 vP, App eV⇩2 vV : τ"
          by auto
      qed auto
    qed
  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
      by (blast dest!: a_Prj1(2))
  next
    case (PrjPair1 v⇩2)
    from a_Prj1(1)[unfolded ‹e = Syntax.Pair e' v⇩2›] show ?thesis
    proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
      case (Pair eP⇩1 eV⇩1 eP⇩2 eV⇩2)
      with PrjPair1 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        show "{$$} ⊢ e', eP⇩1, eV⇩1 : τ⇩1"
          by (rule Pair)
      qed auto
    qed
  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
      by (blast dest!: a_Prj2(2))
  next
    case (PrjPair2 v⇩1)
    from a_Prj2(1)[unfolded ‹e = Syntax.Pair v⇩1 e'›] show ?thesis
    proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
      case (Pair eP⇩1 eV⇩1 eP⇩2 eV⇩2)
      with PrjPair2 show ?thesis
      proof (intro conjI exI[of _ "[]"] exI)
        show "{$$} ⊢ e', eP⇩2, eV⇩2 : τ⇩2"
          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⇩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
      by (blast dest!: a_Pair(2))
  next
    case (Pair2 e⇩2')
    with a_Pair(1,3) show ?thesis
      by (blast dest!: a_Pair(4))
  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
      by (blast dest!: a_Inj1(2))
  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
      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⇩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
      by (blast dest!: a_App(2))
  next
    case (App2 e⇩2')
    with a_App(1,3) show ?thesis
      by (blast dest!: a_App(4))
  next
    case (AppLam x eV'')
    from a_App(1)[unfolded ‹eV⇩1 = 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⇩2 / x], eP''[eP⇩2 / x], eV' : τ⇩2"
          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⇩1 = 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⇩2"
        let ?eP = "App (Lam y eP'''[Rec x (Lam y eP''') / x]) eP⇩2"
        from Rec a_App(3) AppRec show "{$$} ⊢ ?e, ?eP, eV' : τ⇩2"
          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⇩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
    proof (intro conjI exI[of _ "[]"] exI disjI1)
      from Let1 a_Let(5,6,8,10) show "{$$} ⊢ e⇩2[e⇩1 / x], eP⇩2[eP⇩1 / x], eV' : τ⇩2"
        by (auto intro: lemma4)
    qed (auto 0 3 intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
  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
    proof (intro conjI exI[of _ "π"] exI)
      from ‹atom x ♯ π› Let2 a_Let(1-8,10,12-) fresh ih
      show "{$$} ⊢ Let e⇩1' x e⇩2, Let eP⇩1' x eP⇩2, eV' : τ⇩2 ∧ π⇩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 τ⇩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'')
    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⇩1 e⇩2≫ I→ ≪[], Case e'' e⇩1 e⇩2≫"
          "∀π⇩P. ≪π⇩P, Case eP eP⇩1 eP⇩2≫ P→ ≪π⇩P @ [s], Case eP'' eP⇩1 eP⇩2≫"
          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⇩1 v', App eP⇩1 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⇩2 v', App eP⇩2 vP', eV' : τ"
          by auto
      qed auto
    qed
  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
      by (blast dest!: a_Prj1(2))
  next
    case (PrjPair1 v⇩2)
    with a_Prj1(1) show ?thesis
    proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
      case (Pair e⇩1 eP⇩1 eV⇩1 e⇩2 eP⇩2 eV⇩2)
      with PrjPair1 a_Prj1(1) show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from Pair PrjPair1 a_Prj1(1) show "{$$} ⊢ e⇩1, eP⇩1, eV' : τ⇩1"
          by auto
      qed auto
    qed simp_all
  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
      by (blast dest!: a_Prj2(2))
  next
    case (PrjPair2 v⇩2)
    with a_Prj2(1) show ?thesis
    proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
      case (Pair e⇩1 eP⇩1 eV⇩1 e⇩2 eP⇩2 eV⇩2)
      with PrjPair2 a_Prj2(1) show ?thesis
      proof (intro conjI exI[of _ "[]"] exI disjI1)
        from Pair PrjPair2 a_Prj2(1) show "{$$} ⊢ e⇩2, eP⇩2, eV' : τ⇩2"
          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⇩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)+

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⇩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 : τ"
    by (atomize_elim, intro s_Tr(2)) auto
  moreover obtain eP⇩3 eV⇩3 π' where agree: "{$$} ⊢ e⇩3, eP⇩3, eV⇩3 : τ"
    and "≪π⇩P, eP⇩2≫ P→ ≪π⇩P @ π', eP⇩3≫" "≪π' @ π'', eV⇩2≫ V→ ≪π'', eV⇩3≫"
  for π⇩P π'' using lemma5[OF ih(3) s_Tr(3)[unfolded ‹π⇩2 = []›], of thesis] by blast
  ultimately have "≪[], eP≫ P→i + 1 ≪π @ π', eP⇩3≫" "≪π @ π', eV≫ V→i + 1 ≪[], eV⇩3≫"
    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 π⇩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'"
    by blast
  then show ?case
  proof (elim disjE conjE, goal_cases ok collision)
    case ok
    obtain e⇩3 eP⇩3 π' where
      "≪[], e⇩2≫ I→ ≪[], e⇩3≫" "≪π⇩P, eP⇩2≫ P→ ≪π⇩P @ π', eP⇩3≫"
      "{$$} ⊢ e⇩3, eP⇩3, eV⇩3 : τ ∧ π⇩2 = π' @ π⇩3 ∨
      (∃s s'. closed s ∧ closed s' ∧ π' = [s] ∧ π⇩2 = [s'] @ π⇩3 ∧ 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⇩3≫"
          by (elim smallsteps.s_Tr) auto
        from ok collision show "π⇩1 = π @ [s'] @ [] @ π⇩3"
          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 π⇩0''
      assume *: "π⇩2 = π⇩0'' @ π⇩3"
      from collision * show "π⇩1 = π⇩0 @ [s'] @ (π⇩0' @ π⇩0'') @ π⇩3"
        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⇩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)
    from a_App(1)[unfolded ‹eP⇩1 = 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⇩1 = 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⇩2"
        let ?eV = "App (Lam y (eV''[Rec x (Lam y eV'') / x])) eV⇩2"
        from a_App(3) Rec AppRec show "{$$} ⊢ ?e, eP', ?eV : τ⇩2"
          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⇩1 e⇩2≫ I→ ≪[], ?e≫"
          by (auto intro!: s_AppRec[where v=e⇩2]
            simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
        from a_App(3) Rec AppRec show "≪π, App eV⇩1 eV⇩2≫ V→ ≪[], ?eV≫"
          by (auto intro!: s_AppRec[where v=eV⇩2]
            simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
      qed
    qed simp
  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
      by (intro exI[where P = "λx. ∃y. (Q x y)" for Q, OF exI, of _ "e⇩2[e⇩1 / x]" "eV⇩2[eV⇩1 / x]"])
        (auto intro!: lemma4)
  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
      by (intro exI[where P = "λx. ∃y. (Q x y)" for Q, OF exI, of _ "Let e⇩1' x e⇩2" "Let eV⇩1' x eV⇩2"])
       (fastforce simp: fresh_Pair del: agree.a_Let intro!: agree.a_Let)
  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
      by (auto 0 4 simp: lemma2_1 intro: exI[of _ "Hash (hash ⦇eP⦈)"] exI[of _ e])
  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
      by (force intro: a_AuthT_value_inv[OF a_Unauth(1)] simp: fresh_shallow)
  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(2,1)
proof (atomize_elim, 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 ps: "π⇩2 = π⇩1 @ π'" "π = π' @ π''"
    by (force elim: smallstepP_generates_proofstream 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 π'])
  moreover
  obtain e⇩3 eV⇩3 where agree: "{$$} ⊢ e⇩3, eP⇩3, eV⇩3 : τ" and
    "≪[], e⇩2≫ I→ ≪[], e⇩3≫" "≪π'', eV⇩2≫ V→ ≪[], eV⇩3≫"
    by (rule remark1_single[OF ih(1) iffD2[OF smallstepP_ps_prepend s_Tr(3)[unfolded ps]]]) blast
  ultimately have "≪[], e≫ I→i + 1 ≪[], e⇩3≫" "≪π, eV≫ V→i + 1 ≪[], eV⇩3≫"
    by (auto simp: smallstepsV_ps_append[of _ _ _ "[]", simplified, symmetric] ps
       intro!: smallsteps.s_Tr[where m=V and π⇩1="π' @ π''" and π⇩2=π''])
  with agree show ?case
    by blast
qed

(*<*)
end
(*>*)