Theory Lambda_Auth

theory Lambda_Auth
  imports FMap_Lemmas De_Bruijn
begin

(* Avoids clash with substitution notation *)
no_notation inverse_divide (infixl "'/" 70)
(* Helps automated provers with smallsteps *)
declare One_nat_def[simp del]

nominal_function subst_term :: "term ⇒ term ⇒ var ⇒ term" ("_[_ '/ _]" [250, 200, 200] 250) where
"Unit[t' / x] = Unit" |
"(Var y)[t' / x] = (if x = y then t' else Var y)" |
"atom y ♯ (x, t') ⟹ (Lam y t)[t' / x] = Lam y (t[t' / x])" |
"atom y ♯ (x, t') ⟹ (Rec y t)[t' / x] = Rec y (t[t' / x])" |
"(Inj1 t)[t' / x] = Inj1 (t[t' / x])" |
"(Inj2 t)[t' / x] = Inj2 (t[t' / x])" |
"(Pair t1 t2)[t' / x] = Pair (t1[t' / x]) (t2[t' / x]) " |
"(Roll t)[t' / x] = Roll (t[t' / x])" |
"atom y ♯ (x, t') ⟹ (Let t1 y t2)[t' / x] = Let (t1[t' / x]) y (t2[t' / x])" |
"(App t1 t2)[t' / x] = App (t1[t' / x]) (t2[t' / x])" |
"(Case t1 t2 t3)[t' / x] = Case (t1[t' / x]) (t2[t' / x]) (t3[t' / x])" |
"(Prj1 t)[t' / x] = Prj1 (t[t' / x])" |
"(Prj2 t)[t' / x] = Prj2 (t[t' / x])" |
"(Unroll t)[t' / x] = Unroll (t[t' / x])" |
"(Auth t)[t' / x] = Auth (t[t' / x])" |
"(Unauth t)[t' / x] = Unauth (t[t' / x])" |
"(Hash h)[t' / x] = Hash h" |
"(Hashed h t)[t' / x] = Hashed h (t[t' / x])"
  using [[simproc del: alpha_lst]]
  subgoal by (simp add: eqvt_def subst_term_graph_aux_def)
  subgoal by (erule subst_term_graph.induct) (auto simp: fresh_star_def fresh_at_base)
                      apply clarify
  subgoal for P a b t
    by (rule term.strong_exhaust[of a P "(b, t)"]) (auto simp: fresh_star_def fresh_Pair)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
       apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
       apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
       apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  done
nominal_termination (eqvt)
  by lexicographic_order

type_synonym tenv = "(var, term) fmap"

nominal_function psubst_term :: "term ⇒ tenv ⇒ term" where
"psubst_term Unit f = Unit" |
"psubst_term (Var y) f = (case f $$ y of Some t ⇒ t | None ⇒ Var y)" |
"atom y ♯ f ⟹ psubst_term (Lam y t) f = Lam y (psubst_term t f)" |
"atom y ♯ f ⟹ psubst_term (Rec y t) f = Rec y (psubst_term t f)" |
"psubst_term (Inj1 t) f = Inj1 (psubst_term t f)" |
"psubst_term (Inj2 t) f = Inj2 (psubst_term t f)" |
"psubst_term (Pair t1 t2) f = Pair (psubst_term t1 f) (psubst_term t2 f) " |
"psubst_term (Roll t) f = Roll (psubst_term t f)" |
"atom y ♯ f ⟹ psubst_term (Let t1 y t2) f = Let (psubst_term t1 f) y (psubst_term t2 f)" |
"psubst_term (App t1 t2) f = App (psubst_term t1 f) (psubst_term t2 f)" |
"psubst_term (Case t1 t2 t3) f = Case (psubst_term t1 f) (psubst_term t2 f) (psubst_term t3 f)" |
"psubst_term (Prj1 t) f = Prj1 (psubst_term t f)" |
"psubst_term (Prj2 t) f = Prj2 (psubst_term t f)" |
"psubst_term (Unroll t) f = Unroll (psubst_term t f)" |
"psubst_term (Auth t) f = Auth (psubst_term t f)" |
"psubst_term (Unauth t) f = Unauth (psubst_term t f)" |
"psubst_term (Hash h) f = Hash h" |
"psubst_term (Hashed h t) f = Hashed h (psubst_term t f)"
  using [[simproc del: alpha_lst]]
  subgoal by (simp add: eqvt_def psubst_term_graph_aux_def)
  subgoal by (erule psubst_term_graph.induct) (auto simp: fresh_star_def fresh_at_base)
  apply clarify
  subgoal for P a b
    by (rule term.strong_exhaust[of a P b]) (auto simp: fresh_star_def fresh_Pair)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal by clarify
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  done
nominal_termination (eqvt)
  by lexicographic_order

(* subst_type t t' x --> In t substitute x's by t' *)
nominal_function subst_type :: "ty ⇒ ty ⇒ tvar ⇒ ty" where
"subst_type One t' x = One" |
"subst_type (Fun t1 t2) t' x = Fun (subst_type t1 t' x) (subst_type t2 t' x)" |
"subst_type (Sum t1 t2) t' x = Sum (subst_type t1 t' x) (subst_type t2 t' x)" |
"subst_type (Prod t1 t2) t' x = Prod (subst_type t1 t' x) (subst_type t2 t' x)" |
"atom y ♯ (t', x) ⟹ subst_type (Mu y t) t' x = Mu y (subst_type t t' x)" |
"subst_type (Alpha y) t' x = (if y = x then t' else Alpha y)" |
"subst_type (AuthT t) t' x = AuthT (subst_type t t' x)"
  using [[simproc del: alpha_lst]]
  subgoal by (simp add: eqvt_def subst_type_graph_aux_def)
  subgoal by (erule subst_type_graph.induct) (auto simp: fresh_star_def fresh_at_base)
  apply clarify
  subgoal for P a
    by (rule ty.strong_exhaust[of a P]) (auto simp: fresh_star_def)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  done
nominal_termination (eqvt)
  by lexicographic_order

(* Substitution lemmas for terms and types *)

lemma fresh_subst_term: "atom x ♯ t[t' / x'] ⟷ (x = x' ∨ atom x ♯ t) ∧ (atom x' ♯ t ∨ atom x ♯ t')"
  by (nominal_induct t avoiding: t' x x' rule: term.strong_induct) (auto simp add: fresh_at_base)

lemma term_fresh_subst[simp]: "atom x ♯ t ⟹ atom x ♯ s ⟹ (atom (x::var)) ♯ t[s / y]"
  by (nominal_induct t avoiding: s y rule: term.strong_induct) (auto)

lemma term_subst_idle[simp]: "atom y ♯ t ⟹ t[s / y] = t"
  by (nominal_induct t avoiding: s y rule: term.strong_induct) (auto simp: fresh_Pair fresh_at_base)

lemma term_subst_subst: "atom y1 ≠ atom y2 ⟹ atom y1 ♯ s2 ⟹ t[s1 / y1][s2 / y2] = t[s2 / y2][s1[s2 / y2] / y1]"
  by (nominal_induct t avoiding: y1 y2 s1 s2 rule: term.strong_induct) auto

lemma fresh_psubst:
  fixes x :: var
  assumes "atom x ♯ e" "atom x ♯ vs"
  shows   "atom x ♯ psubst_term e vs"
  using assms
  by (induct e vs rule: psubst_term.induct)
    (auto simp: fresh_at_base elim: fresh_fmap_fresh_Some split: option.splits)

lemma fresh_subst_type:
  "atom α ♯ subst_type τ τ' α' ⟷ ((α = α' ∨ atom α ♯ τ) ∧ (atom α' ♯ τ ∨ atom α ♯ τ'))"
  by (nominal_induct τ avoiding: α α' τ' rule: ty.strong_induct) (auto simp add: fresh_at_base)

lemma type_fresh_subst[simp]: "atom x ♯ t ⟹ atom x ♯ s ⟹ (atom (x::tvar)) ♯ subst_type t s y"
  by (nominal_induct t avoiding: s y rule: ty.strong_induct) (auto)

lemma type_subst_idle[simp]: "atom y ♯ t ⟹ subst_type t s y = t"
  by (nominal_induct t avoiding: s y rule: ty.strong_induct) (auto simp: fresh_Pair fresh_at_base)

lemma type_subst_subst: "atom y1 ≠ atom y2 ⟹ atom y1 ♯ s2 ⟹ (subst_type (subst_type t s1 y1) s2 y2) = subst_type (subst_type t s2 y2) (subst_type s1 s2 y2) y1"
  by (nominal_induct t avoiding: y1 y2 s1 s2 rule: ty.strong_induct) auto

type_synonym tyenv = "(var, ty) fmap"

inductive judge_weak :: "tyenv ⇒ term ⇒ ty ⇒ bool" ("_ ⊢⇩W _ : _" [150,0,150] 149) where
jw_Unit:   "Γ ⊢⇩W Unit : One" |
jw_Var:    "⟦ Γ $$ x = Some τ ⟧
         ⟹ Γ ⊢⇩W Var x : τ" |
jw_Lam:    "⟦ atom x ♯ Γ; Γ(x $$:= τ⇩1) ⊢⇩W e : τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Lam x e : Fun τ⇩1 τ⇩2" |
jw_App:    "⟦ Γ ⊢⇩W e : Fun τ⇩1 τ⇩2; Γ ⊢⇩W e' : τ⇩1 ⟧
         ⟹ Γ ⊢⇩W App e e' : τ⇩2" |
jw_Let:    "⟦ atom x ♯ (Γ, e⇩1); Γ ⊢⇩W e⇩1 : τ⇩1; Γ(x $$:= τ⇩1) ⊢⇩W e⇩2 : τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Let e⇩1 x e⇩2 : τ⇩2" |
jw_Rec:    "⟦ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢⇩W Lam y e : Fun τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Rec x (Lam y e) : Fun τ⇩1 τ⇩2" |
jw_Inj1:   "⟦ Γ ⊢⇩W e : τ⇩1 ⟧
         ⟹ Γ ⊢⇩W Inj1 e : Sum τ⇩1 τ⇩2" |
jw_Inj2:   "⟦ Γ ⊢⇩W e : τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Inj2 e : Sum τ⇩1 τ⇩2" |
jw_Case:   "⟦ Γ ⊢⇩W e : Sum τ⇩1 τ⇩2; Γ ⊢⇩W e⇩1 : Fun τ⇩1 τ; Γ ⊢⇩W e⇩2 : Fun τ⇩2 τ ⟧
         ⟹ Γ ⊢⇩W Case e e⇩1 e⇩2 : τ" |
jw_Pair:   "⟦ Γ ⊢⇩W e⇩1 : τ⇩1; Γ ⊢⇩W e⇩2 : τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Pair e⇩1 e⇩2 : Prod τ⇩1 τ⇩2" |
jw_Prj1:   "⟦ Γ ⊢⇩W e : Prod τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Prj1 e : τ⇩1" |
jw_Prj2:   "⟦ Γ ⊢⇩W e : Prod τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢⇩W Prj2 e : τ⇩2" |
jw_Roll:   "⟦ atom α ♯ Γ; Γ ⊢⇩W e : subst_type τ (Mu α τ) α ⟧
         ⟹ Γ ⊢⇩W Roll e : Mu α τ" |
jw_Unroll: "⟦ atom α ♯ Γ; Γ ⊢⇩W e : Mu α τ ⟧
         ⟹ Γ ⊢⇩W Unroll e : subst_type τ (Mu α τ) α" |
jw_Auth:   "⟦ Γ ⊢⇩W e : τ ⟧
         ⟹ Γ ⊢⇩W Auth e : τ" |
jw_Unauth: "⟦ Γ ⊢⇩W e : τ ⟧
         ⟹ Γ ⊢⇩W Unauth e : τ"

declare judge_weak.intros[simp]
declare judge_weak.intros[intro]

equivariance judge_weak
nominal_inductive judge_weak
  avoids jw_Lam: x
       | jw_Rec: x and y
       | jw_Let: x
       | jw_Roll: α
       | jw_Unroll: α
  by (auto simp: fresh_subst_type fresh_Pair)

(* Inversion rules for typing judgment *)
inductive_cases jw_Unit_inv[elim]: "Γ ⊢⇩W Unit : τ"
inductive_cases jw_Var_inv[elim]: "Γ ⊢⇩W Var x : τ"

lemma jw_Lam_inv[elim]:
  assumes "Γ ⊢⇩W Lam x e : τ"
  and     "atom x ♯ Γ"
  obtains τ⇩1 τ⇩2 where "τ = Fun τ⇩1 τ⇩2" "(Γ(x $$:= τ⇩1)) ⊢⇩W e : τ⇩2"
  using assms proof (atomize_elim, nominal_induct Γ "Lam x e" τ avoiding: x e rule: judge_weak.strong_induct)
  case (jw_Lam x Γ τ⇩1 t τ⇩2 y u)
  then show ?case
    by (auto simp: perm_supp_eq elim!:
        iffD1[OF Abs_lst1_fcb2'[where f = "λx t (Γ, τ⇩1, τ⇩2). (Γ(x $$:= τ⇩1)) ⊢⇩W t : τ⇩2"
        and c = "(Γ, τ⇩1, τ⇩2)" and a = x and b = y and x = t and y = u, unfolded prod.case],
        rotated -1])
qed

lemma jw_Rec_inv[elim]:
  assumes "Γ ⊢⇩W Rec x t : τ"
  and     "atom x ♯ Γ"
  obtains y e τ⇩1 τ⇩2 where "atom y ♯ (Γ,x)" "t = Lam y e" "τ = Fun τ⇩1 τ⇩2" "Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢⇩W Lam y e : Fun τ⇩1 τ⇩2"
  using [[simproc del: alpha_lst]] assms
proof (atomize_elim, nominal_induct Γ "Rec x t" τ avoiding: x t rule: judge_weak.strong_induct)
  case (jw_Rec x Γ y τ⇩1 τ⇩2 e xa t)
  then show ?case
  proof (nominal_induct t avoiding: y x xa rule: term.strong_induct)
    case (Lam y' e')
    then show ?case
      apply -
      apply (rule exI[of _ y])
      apply (rule exI[of _ "(y' ↔ y) ∙ e'"])
      apply (rule exI[of _ τ⇩1])
      apply (rule exI[of _ τ⇩2])
      apply (rule conjI, simp)
      apply (rule conjI)
       apply (subst term.eq_iff(3))
       apply (rule Abs_lst_eq_flipI)
       apply (simp add: fresh_at_base)
      apply (simp add: fresh_at_base)
      apply (drule judge_weak.eqvt[of "Γ(x $$:= Fun τ⇩1 τ⇩2)" "Lam y e" "Fun τ⇩1 τ⇩2" "(x ↔ xa)"])
      apply (simp add: perm_supp_eq Abs1_eq_iff)
      apply (subst (asm) (3) permute_eqvt)
      apply (simp add: flip_commute)
      done
  qed (simp_all add: Abs1_eq_iff)
qed

inductive_cases jw_Inj1_inv[elim]: "Γ ⊢⇩W Inj1 e : τ"
inductive_cases jw_Inj2_inv[elim]: "Γ ⊢⇩W Inj2 e : τ"
inductive_cases jw_Pair_inv[elim]: "Γ ⊢⇩W Pair e⇩1 e⇩2 : τ"

lemma jw_Let_inv[elim]:
  assumes "Γ ⊢⇩W Let e⇩1 x e⇩2 : τ⇩2"
  and     "atom x ♯ (e⇩1, Γ)"
  obtains τ⇩1 where "Γ ⊢⇩W e⇩1 : τ⇩1" "Γ(x $$:= τ⇩1) ⊢⇩W e⇩2 : τ⇩2"
using assms proof (atomize_elim, nominal_induct Γ "Let e⇩1 x e⇩2" τ⇩2 avoiding: e⇩1 x e⇩2 rule: judge_weak.strong_induct)
  case (jw_Let x Γ e⇩1 τ⇩1 e⇩2 τ⇩2 x' e⇩2')
  then show ?case
    by (auto simp: fresh_Pair perm_supp_eq elim!:
        iffD1[OF Abs_lst1_fcb2'[where f = "λx t (Γ, τ⇩1, τ⇩2). Γ(x $$:= τ⇩1) ⊢⇩W t : τ⇩2"
        and c = "(Γ, τ⇩1, τ⇩2)" and a = x and b = x' and x = e⇩2 and y = e⇩2', unfolded prod.case],
        rotated -1])
qed

inductive_cases jw_Prj1_inv[elim]: "Γ ⊢⇩W Prj1 e : τ⇩1"
inductive_cases jw_Prj2_inv[elim]: "Γ ⊢⇩W Prj2 e : τ⇩2"
inductive_cases jw_App_inv[elim]: "Γ ⊢⇩W App e e' : τ⇩2"
inductive_cases jw_Case_inv[elim]: "Γ ⊢⇩W Case e e⇩1 e⇩2 : τ"
inductive_cases jw_Auth_inv[elim]: "Γ ⊢⇩W Auth e : τ"
inductive_cases jw_Unauth_inv[elim]: "Γ ⊢⇩W Unauth e : τ"

lemma subst_type_perm_eq:
  assumes "atom b ♯ t"
  shows   "subst_type t (Mu a t) a = subst_type ((a ↔ b) ∙ t) (Mu b ((a ↔ b) ∙ t)) b"
  using assms proof -
  have f: "atom a ♯ subst_type t (Mu a t) a" by (rule iffD2[OF fresh_subst_type]) simp
  have    "atom b ♯ subst_type t (Mu a t) a" by (auto simp: assms)
  with f have "subst_type t (Mu a t) a = (a ↔ b) ∙ subst_type t (Mu a t) a"
    by (simp add: flip_fresh_fresh)
  then show "subst_type t (Mu a t) a  = subst_type ((a ↔ b) ∙ t) (Mu b ((a ↔ b) ∙ t)) b"
    by simp
qed

lemma jw_Roll_inv[elim]:
  assumes "Γ ⊢⇩W Roll e : τ"
  and     "atom α ♯ (Γ, τ)"
  obtains τ' where "τ = Mu α τ'" "Γ ⊢⇩W e : subst_type τ' (Mu α τ') α"
  using assms [[simproc del: alpha_lst]]
  proof (atomize_elim, nominal_induct Γ "Roll e" τ avoiding: e α rule: judge_weak.strong_induct)
  case (jw_Roll α Γ e τ α')
  then show ?case
    by (auto simp: perm_supp_eq fresh_Pair fresh_at_base subst_type.eqvt
      intro!: exI[of _ "(α ↔ α') ∙ τ"] Abs_lst_eq_flipI dest: judge_weak.eqvt[of _ _ _ "(α ↔ α')"])
qed

lemma jw_Unroll_inv[elim]:
  assumes "Γ ⊢⇩W Unroll e : τ"
  and     "atom α ♯ (Γ, τ)"
  obtains τ' where "τ = subst_type τ' (Mu α τ') α" "Γ ⊢⇩W e : Mu α τ'"
  using assms proof (atomize_elim, nominal_induct Γ "Unroll e" τ avoiding: e α rule: judge_weak.strong_induct)
  case (jw_Unroll α Γ e τ α')
  then show ?case
    by (auto simp: perm_supp_eq fresh_Pair subst_type_perm_eq fresh_subst_type
           intro!: exI[of _ "(α ↔ α') ∙ τ"] dest: judge_weak.eqvt[of _ _ _ "(α ↔ α')"])
qed

(* Additional inversion rules based on type rather than term *)

inductive_cases jw_Prod_inv[elim]: "{$$} ⊢⇩W e : Prod τ⇩1 τ⇩2"
inductive_cases jw_Sum_inv[elim]: "{$$} ⊢⇩W e : Sum τ⇩1 τ⇩2"

lemma jw_Fun_inv[elim]:
  assumes "{$$} ⊢⇩W v : Fun τ⇩1 τ⇩2" "value v"
  obtains e x where "v = Lam x e ∨ v = Rec x e" "atom x ♯ (c::term)"
  using assms [[simproc del: alpha_lst]]
  apply (atomize_elim)
  apply (nominal_induct "{$$} :: tyenv" v "Fun τ⇩1 τ⇩2" avoiding: τ⇩1 τ⇩2 rule: judge_weak.strong_induct)
           apply simp_all
  subgoal for x τ⇩1 e τ⇩2
  proof -
    obtain x' where "atom (x'::var) ♯ (c, e)" apply atomize_elim using finite_supp obtain_fresh' by blast
    then have "[[atom x]]lst. e = [[atom x']]lst. (x ↔ x') ∙ e ∧ atom x' ♯ c"
      by (simp add: Abs_lst_eq_flipI fresh_Pair)
    then show ?thesis
      by blast
  qed
  subgoal for x y τ⇩1 τ⇩2 e'
  proof -
    obtain x' where "atom (x'::var) ♯ (c, Lam y e')" apply atomize_elim using finite_supp obtain_fresh' by blast
    then have "[[atom x]]lst. Lam y e' = [[atom x']]lst. (x ↔ x') ∙ (Lam y e') ∧ atom x' ♯ c"
      using Abs_lst_eq_flipI fresh_Pair by blast
    then show ?thesis
      by blast
  qed
  done

lemma jw_Mu_inv[elim]:
  assumes "{$$} ⊢⇩W v : Mu α τ" "value v"
  obtains v' where "v = Roll v'"
  using assms by (atomize_elim, nominal_induct "{$$} :: tyenv" v "Mu α τ" rule: judge_weak.strong_induct) simp_all

nominal_function erase :: "ty ⇒ ty" where
"erase One = One" |
"erase (Fun τ⇩1 τ⇩2) = Fun (erase τ⇩1) (erase τ⇩2)" |
"erase (Sum τ⇩1 τ⇩2) = Sum (erase τ⇩1) (erase τ⇩2)" |
"erase (Prod τ⇩1 τ⇩2) = Prod (erase τ⇩1) (erase τ⇩2)" |
"erase (Mu α τ) = Mu α (erase τ)" |
"erase (Alpha α) = Alpha α" |
"erase (AuthT τ) = erase τ"
  using [[simproc del: alpha_lst]]
  subgoal by (simp add: eqvt_def erase_graph_aux_def)
  subgoal by (erule erase_graph.induct) (auto simp: fresh_star_def fresh_at_base)
  subgoal for P x
    by (rule ty.strong_exhaust[of x P x]) (auto simp: fresh_star_def)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  done
nominal_termination (eqvt)
  by lexicographic_order

(* Erase lemmas *)
lemma fresh_erase_fresh:
  assumes "atom x ♯ τ"
  shows   "atom x ♯ erase τ"
  using assms by (induct τ rule: ty.induct) auto

lemma fresh_fmmap_erase_fresh:
  assumes "atom x ♯ Γ"
  shows   "atom x ♯ fmmap erase Γ"
  using assms by transfer simp

lemma erase_subst_type_shift[simp]:
  "erase (subst_type τ τ' α) = subst_type (erase τ) (erase τ') α"
  by (induct τ τ' α rule: subst_type.induct) (auto simp: fresh_Pair fresh_erase_fresh)

definition erase_env :: "tyenv ⇒ tyenv" where
  "erase_env = fmmap erase"

(* Strong type judgment *)
inductive judge :: "tyenv ⇒ term ⇒ ty ⇒ bool" ("_ ⊢ _ : _" [150,0,150] 149) where
j_Unit:   "Γ ⊢ Unit : One" |
j_Var:    "⟦ Γ $$ x = Some τ ⟧
         ⟹ Γ ⊢ Var x : τ" |
j_Lam:    "⟦ atom x ♯ Γ; Γ(x $$:= τ⇩1) ⊢ e : τ⇩2 ⟧
         ⟹ Γ ⊢ Lam x e : Fun τ⇩1 τ⇩2" |
j_App:    "⟦ Γ ⊢ e : Fun τ⇩1 τ⇩2; Γ ⊢ e' : τ⇩1 ⟧
         ⟹ Γ ⊢ App e e' : τ⇩2" |
j_Let:    "⟦ atom x ♯ (Γ, e⇩1); Γ ⊢ e⇩1 : τ⇩1; Γ(x $$:= τ⇩1) ⊢ e⇩2 : τ⇩2 ⟧
         ⟹ Γ ⊢ Let e⇩1 x e⇩2 : τ⇩2" |
j_Rec:    "⟦ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ Lam y e' : Fun τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢ Rec x (Lam y e') : Fun τ⇩1 τ⇩2" |
j_Inj1:   "⟦ Γ ⊢ e : τ⇩1 ⟧
         ⟹ Γ ⊢ Inj1 e : Sum τ⇩1 τ⇩2" |
j_Inj2:   "⟦ Γ ⊢ e : τ⇩2 ⟧
         ⟹ Γ ⊢ Inj2 e : Sum τ⇩1 τ⇩2" |
j_Case:   "⟦ Γ ⊢ e : Sum τ⇩1 τ⇩2; Γ ⊢ e⇩1 : Fun τ⇩1 τ; Γ ⊢ e⇩2 : Fun τ⇩2 τ ⟧
         ⟹ Γ ⊢ Case e e⇩1 e⇩2 : τ" |
j_Pair:   "⟦ Γ ⊢ e⇩1 : τ⇩1; Γ ⊢ e⇩2 : τ⇩2 ⟧
         ⟹ Γ ⊢ Pair e⇩1 e⇩2 : Prod τ⇩1 τ⇩2" |
j_Prj1:   "⟦ Γ ⊢ e : Prod τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢ Prj1 e : τ⇩1" |
j_Prj2:   "⟦ Γ ⊢ e : Prod τ⇩1 τ⇩2 ⟧
         ⟹ Γ ⊢ Prj2 e : τ⇩2" |
j_Roll:   "⟦ atom α ♯ Γ; Γ ⊢ e : subst_type τ (Mu α τ) α ⟧
         ⟹ Γ ⊢ Roll e : Mu α τ" |
j_Unroll: "⟦ atom α ♯ Γ; Γ ⊢ e : Mu α τ ⟧
         ⟹ Γ ⊢ Unroll e : subst_type τ (Mu α τ) α" |
j_Auth:   "⟦ Γ ⊢ e : τ ⟧
         ⟹ Γ ⊢ Auth e : AuthT τ" |
j_Unauth: "⟦ Γ ⊢ e : AuthT τ ⟧
         ⟹ Γ ⊢ Unauth e : τ"

declare judge.intros[intro]

equivariance judge
nominal_inductive judge
  avoids j_Lam: x
       | j_Rec: x and y
       | j_Let: x
       | j_Roll: α
       | j_Unroll: α
  by (auto simp: fresh_subst_type fresh_Pair)

lemma judge_imp_judge_weak:
  assumes "Γ ⊢ e : τ"
  shows   "erase_env Γ ⊢⇩W e : erase τ"
  using assms unfolding erase_env_def
  by (induct Γ e τ rule: judge.induct) (simp_all add: fresh_Pair fresh_fmmap_erase_fresh fmmap_fmupd)

nominal_function shallow :: "term ⇒ term" ("⦇_⦈") where
"⦇Unit⦈  = Unit" |
"⦇Var v⦈ = Var v" |
"⦇Lam x e⦈ = Lam x ⦇e⦈" |
"⦇Rec x e⦈ = Rec x ⦇e⦈" |
"⦇Inj1 e⦈ = Inj1 ⦇e⦈" |
"⦇Inj2 e⦈ = Inj2 ⦇e⦈" |
"⦇Pair e⇩1 e⇩2⦈ = Pair ⦇e⇩1⦈ ⦇e⇩2⦈" |
"⦇Roll e⦈ = Roll ⦇e⦈" |
"⦇Let e⇩1 x e⇩2⦈ = Let ⦇e⇩1⦈ x ⦇e⇩2⦈" |
"⦇App e⇩1 e⇩2⦈ = App ⦇e⇩1⦈ ⦇e⇩2⦈" |
"⦇Case e e⇩1 e⇩2⦈ = Case ⦇e⦈ ⦇e⇩1⦈ ⦇e⇩2⦈" |
"⦇Prj1 e⦈ = Prj1 ⦇e⦈" |
"⦇Prj2 e⦈ = Prj2 ⦇e⦈" |
"⦇Unroll e⦈ = Unroll ⦇e⦈" |
"⦇Auth e⦈ = Auth ⦇e⦈" |
"⦇Unauth e⦈ = Unauth ⦇e⦈" |
(* No rule is defined for Hash, but: "[..] preserving that structure in every case but that of <h, v> [..]" *)
"⦇Hash h⦈ = Hash h" |
"⦇Hashed h e⦈ = Hash h"
  using [[simproc del: alpha_lst]]
  subgoal by (simp add: eqvt_def shallow_graph_aux_def)
  subgoal by (erule shallow_graph.induct) (auto simp: fresh_star_def fresh_at_base)
  subgoal for P a
    by (rule term.strong_exhaust[of a P a]) (auto simp: fresh_star_def)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  subgoal
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  subgoal
    apply (erule conjE)
    apply (erule Abs_lst1_fcb2')
       apply (simp_all add: eqvt_at_def)
      apply (simp_all add: perm_supp_eq Abs_fresh_iff)
    done
  done
nominal_termination (eqvt)
  by lexicographic_order

lemma fresh_shallow: "atom x ♯ e ⟹ atom x ♯ ⦇e⦈"
  by (induct e rule: term.induct) auto

(* Ideal, Prover and Verifier modes *)
datatype mode = I | P | V

instantiation mode :: pure
begin
definition permute_mode :: "perm ⇒ mode ⇒ mode" where
  "permute_mode π h = h"
instance proof qed (auto simp: permute_mode_def)
end

type_synonym proofstream = "term list"

(* Single step predicate *)
inductive smallstep :: "proofstream ⇒ term ⇒ mode ⇒ proofstream ⇒ term ⇒ bool" ("≪_, _≫ _→ ≪_, _≫") where
s_App1:      "⟦ ≪ π, e⇩1 ≫  m→  ≪ π', e⇩1' ≫ ⟧
            ⟹ ≪ π, App e⇩1 e⇩2 ≫  m→  ≪ π', App e⇩1' e⇩2 ≫" |
s_App2:      "⟦ value v⇩1; ≪ π, e⇩2 ≫  m→  ≪ π', e⇩2' ≫ ⟧
            ⟹ ≪ π, App v⇩1 e⇩2 ≫  m→  ≪ π', App v⇩1 e⇩2' ≫" |
s_AppLam:    "⟦ value v; atom x ♯ (v,π) ⟧
            ⟹ ≪ π, App (Lam x e) v ≫  _→  ≪ π, e[v / x] ≫" |
s_AppRec:    "⟦ value v; atom x ♯ (v,π) ⟧
            ⟹ ≪ π, App (Rec x e) v ≫  _→  ≪ π, App (e[(Rec x e) / x]) v ≫" |
s_Let1:      "⟦ atom x ♯ (e⇩1,e⇩1',π,π'); ≪ π, e⇩1 ≫  m→  ≪ π', e⇩1' ≫ ⟧
            ⟹ ≪ π, Let e⇩1 x e⇩2 ≫  m→  ≪ π', Let e⇩1' x e⇩2 ≫" |
s_Let2:      "⟦ value v; atom x ♯ (v,π) ⟧
            ⟹ ≪ π, Let v x e ≫  _→  ≪ π, e[v / x] ≫" |
s_Inj1:      "⟦ ≪ π, e ≫  m→  ≪ π', e' ≫ ⟧
            ⟹ ≪ π, Inj1 e ≫  m→  ≪ π', Inj1 e' ≫" |
s_Inj2:      "⟦ ≪ π, e ≫  m→  ≪ π', e' ≫ ⟧
            ⟹ ≪ π, Inj2 e ≫  m→  ≪ π', Inj2 e' ≫" |
s_Case:      "⟦ ≪ π, e ≫  m→  ≪ π', e' ≫ ⟧
            ⟹ ≪ π, Case e e⇩1 e⇩2 ≫  m→  ≪ π', Case e' e⇩1 e⇩2 ≫" |
(* Case rules are different from paper to account for recursive functions. *)
s_CaseInj1:  "⟦ value v ⟧
            ⟹ ≪ π, Case (Inj1 v) e⇩1 e⇩2 ≫  _→  ≪ π, App e⇩1 v ≫" |
s_CaseInj2:  "⟦ value v ⟧
            ⟹ ≪ π, Case (Inj2 v) e⇩1 e⇩2 ≫  _→  ≪ π, App e⇩2 v ≫" |
s_Pair1:     "⟦ ≪ π, e⇩1 ≫  m→  ≪ π', e⇩1' ≫ ⟧
            ⟹ ≪ π, Pair e⇩1 e⇩2 ≫  m→  ≪ π', Pair e⇩1' e⇩2 ≫" |
s_Pair2:     "⟦ value v⇩1; ≪ π, e⇩2 ≫  m→  ≪ π', e⇩2' ≫ ⟧
            ⟹ ≪ π, Pair v⇩1 e⇩2 ≫  m→  ≪ π', Pair v⇩1 e⇩2' ≫" |
s_Prj1:      "⟦ ≪ π, e ≫ m→ ≪ π', e' ≫ ⟧
            ⟹ ≪ π, Prj1 e ≫  m→  ≪ π', Prj1 e' ≫" |
s_Prj2:      "⟦ ≪ π, e ≫ m→ ≪ π', e' ≫ ⟧
            ⟹ ≪ π, Prj2 e ≫  m→  ≪ π', Prj2 e' ≫" |
s_PrjPair1:  "⟦ value v⇩1; value v⇩2 ⟧
            ⟹ ≪ π, Prj1 (Pair v⇩1 v⇩2) ≫  _→  ≪ π, v⇩1 ≫" |
s_PrjPair2:  "⟦ value v⇩1; value v⇩2 ⟧
            ⟹ ≪ π, Prj2 (Pair v⇩1 v⇩2) ≫  _→  ≪ π, v⇩2 ≫" |
s_Unroll:    "≪ π, e ≫  m→  ≪ π', e' ≫
            ⟹ ≪ π, Unroll e ≫  m→  ≪ π', Unroll e' ≫" |
s_Roll:      "≪ π, e ≫  m→  ≪ π', e' ≫
            ⟹ ≪ π, Roll e ≫  m→  ≪ π', Roll e' ≫" |
s_UnrollRoll:"⟦ value v ⟧
            ⟹ ≪ π, Unroll (Roll v) ≫  _→  ≪ π, v ≫" |
(* Mode-specific rules *)
s_Auth:      "≪ π, e ≫ m→ ≪ π', e' ≫
            ⟹ ≪ π, Auth e ≫ m→ ≪ π', Auth e' ≫" |
s_Unauth:    "≪ π, e ≫ m→ ≪ π', e' ≫
            ⟹ ≪ π, Unauth e ≫ m→ ≪ π', Unauth e' ≫" |
s_AuthI:     "⟦ value v ⟧
            ⟹ ≪ π, Auth v ≫ I→ ≪ π, v ≫" |
s_UnauthI:   "⟦ value v ⟧
            ⟹ ≪ π, Unauth v ≫ I→ ≪ π, v ≫" |
s_AuthP:     "⟦ closed ⦇v⦈; value v ⟧
            ⟹ ≪ π, Auth v ≫ P→ ≪ π, Hashed (hash ⦇v⦈) v ≫" |
s_UnauthP:   "⟦ value v ⟧
            ⟹ ≪ π, Unauth (Hashed h v) ≫ P→ ≪ π @ [⦇v⦈], v ≫" |
s_AuthV:     "⟦ closed v; value v ⟧
            ⟹ ≪ π, Auth v ≫ V→ ≪ π, Hash (hash v) ≫" |
s_UnauthV:   "⟦ closed s⇩0; hash s⇩0 = h ⟧
            ⟹ ≪ s⇩0#π, Unauth (Hash h) ≫ V→ ≪ π, s⇩0 ≫"

declare smallstep.intros[simp]
declare smallstep.intros[intro]

equivariance smallstep
nominal_inductive smallstep
  avoids s_AppLam: x
       | s_AppRec: x
       | s_Let1:   x
       | s_Let2:   x
  by (auto simp add: fresh_Pair fresh_subst_term)

(* Transitive smallstep predicate *)
inductive smallsteps :: "proofstream ⇒ term ⇒ mode ⇒ nat ⇒ proofstream ⇒ term ⇒ bool" ("≪_, _≫ _→_ ≪_, _≫") where
s_Id: "≪ π, e ≫ _→0 ≪ π, e ≫" |
s_Tr: "⟦ ≪ π⇩1, e⇩1 ≫ m→i ≪ π⇩2, e⇩2 ≫; ≪ π⇩2, e⇩2 ≫ m→ ≪ π⇩3, e⇩3 ≫ ⟧
     ⟹ ≪ π⇩1, e⇩1 ≫ m→(i+1) ≪ π⇩3, e⇩3 ≫"

declare smallsteps.intros[simp]
declare smallsteps.intros[intro]

equivariance smallsteps
nominal_inductive smallsteps .

lemma steps_1_step[simp]: "≪ π, e ≫ m→1 ≪ π', e' ≫ = ≪ π, e ≫ m→ ≪ π', e' ≫"
  apply (rule iffI)
  subgoal proof (induct π e m "1::nat" π' e' rule: smallsteps.induct)
    case (s_Tr π⇩1 e⇩1 m i π⇩2 e⇩2 π⇩3 e⇩3)
    then show ?case
      apply simp
      apply (induct π⇩1 e⇩1 m "0::nat" π⇩2 e⇩2 rule: smallsteps.induct)
       apply auto
      done
  qed simp
  apply (subst One_nat_def)
  apply (subst Suc_eq_plus1)
  apply (rule s_Tr)
   apply auto
  done

(* Inversion rules for smallstep predicate *)

lemma value_no_step[intro]:
  assumes "≪ π⇩1, v ≫ m→ ≪ π⇩2, t ≫" "value v"
  shows   "False"
  using assms by (induct π⇩1 v m π⇩2 t rule: smallstep.induct) auto

lemma subst_term_perm:
  assumes "atom x' ♯ (x, e)"
  shows "e[v / x] = ((x ↔ x') ∙ e)[v / x']"
  using assms [[simproc del: alpha_lst]]
  by (nominal_induct e avoiding: x x' v rule: term.strong_induct)
     (auto simp: fresh_Pair fresh_at_base(2) permute_hash_def)

inductive_cases s_Unit_inv[elim]: "≪ π⇩1, Unit ≫  m→  ≪ π⇩2, v ≫"

inductive_cases s_App_inv[consumes 1, case_names App1 App2 AppLam AppRec, elim]: "≪ π, App v⇩1 v⇩2 ≫ m→ ≪ π', e ≫"

lemma s_Let_inv':
  assumes "≪ π, Let e⇩1 x e⇩2 ≫  m→  ≪ π', e' ≫"
  and     "atom x ♯ (e⇩1,π)"
  obtains e⇩1' where "(e' = e⇩2[e⇩1 / x] ∧ value e⇩1 ∧ π = π') ∨ (≪ π, e⇩1 ≫  m→  ≪ π', e⇩1' ≫ ∧ e' = Let e⇩1' x e⇩2 ∧ ¬ value e⇩1)"
  using assms [[simproc del: alpha_lst]] apply atomize_elim
  by (induct π "Let e⇩1 x e⇩2" m π' e' rule: smallstep.induct)
     (auto simp: fresh_Pair fresh_subst_term perm_supp_eq elim: Abs_lst1_fcb2')

lemma s_Let_inv[consumes 2, case_names Let1 Let2, elim]:
  assumes "≪ π, Let e⇩1 x e⇩2 ≫  m→  ≪ π', e' ≫"
  and     "atom x ♯ (e⇩1,π)"
  and     "e' = e⇩2[e⇩1 / x] ∧ value e⇩1 ∧ π = π' ⟹ Q"
  and     "⋀e⇩1'. ≪ π, e⇩1 ≫  m→  ≪ π', e⇩1' ≫ ∧ e' = Let e⇩1' x e⇩2 ∧ ¬ value e⇩1 ⟹ Q"
  shows   "Q"
  using assms by (auto elim: s_Let_inv')

inductive_cases s_Case_inv[consumes 1, case_names Case Inj1 Inj2, elim]:
  "≪ π, Case e e⇩1 e⇩2 ≫  m→  ≪ π', e' ≫"
inductive_cases s_Prj1_inv[consumes 1, case_names Prj1 PrjPair1, elim]:
  "≪ π, Prj1 e ≫  m→  ≪ π', v ≫"
inductive_cases s_Prj2_inv[consumes 1, case_names Prj2 PrjPair2, elim]:
  "≪ π, Prj2 e ≫  m→  ≪ π', v ≫"
inductive_cases s_Pair_inv[consumes 1, case_names Pair1 Pair2, elim]:
  "≪ π, Pair e⇩1 e⇩2 ≫ m→ ≪ π', e' ≫"
inductive_cases s_Inj1_inv[consumes 1, case_names Inj1, elim]:
  "≪ π, Inj1 e ≫ m→ ≪ π', e' ≫"
inductive_cases s_Inj2_inv[consumes 1, case_names Inj2, elim]:
  "≪ π, Inj2 e ≫ m→ ≪ π', e' ≫"
inductive_cases s_Roll_inv[consumes 1, case_names Roll, elim]:
  "≪ π, Roll e ≫ m→ ≪ π', e' ≫"
inductive_cases s_Unroll_inv[consumes 1, case_names Unroll UnrollRoll, elim]:
  "≪ π, Unroll e ≫  m→  ≪ π', e' ≫"
inductive_cases s_AuthI_inv[consumes 1, case_names Auth AuthI, elim]:
  "≪ π, Auth e ≫  I→  ≪ π', e' ≫"
inductive_cases s_UnauthI_inv[consumes 1, case_names Unauth UnauthI, elim]:
  "≪ π, Unauth e ≫  I→  ≪ π', e' ≫"
inductive_cases s_AuthP_inv[consumes 1, case_names Auth AuthP, elim]:
  "≪ π, Auth e ≫  P→  ≪ π', e' ≫"
inductive_cases s_UnauthP_inv[consumes 1, case_names Unauth UnauthP, elim]:
  "≪ π, Unauth e ≫  P→  ≪ π', e' ≫"
inductive_cases s_AuthV_inv[consumes 1, case_names Auth AuthV, elim]:
  "≪ π, Auth e ≫  V→  ≪ π', e' ≫"
inductive_cases s_UnauthV_inv[consumes 1, case_names Unauth UnauthV, elim]:
  "≪ π, Unauth e ≫  V→  ≪ π', e' ≫"

(* Inversion rules for smallsteps *)
inductive_cases s_Id_inv[elim]: "≪ π⇩1, e⇩1 ≫ m→0 ≪ π⇩2, e⇩2 ≫"
inductive_cases s_Tr_inv[elim]: "≪ π⇩1, e⇩1 ≫ m→i ≪ π⇩3, e⇩3 ≫"

(* Freshness with smallstep *)
lemma fresh_smallstep_I:
  fixes x :: var
  assumes "≪ π, e ≫ I→ ≪ π', e' ≫" "atom x ♯ e"
  shows   "atom x ♯ e'"
  using assms by (induct π e I π' e' rule: smallstep.induct) (auto simp: fresh_subst_term)

lemma fresh_smallstep_P:
  fixes x :: var
  assumes "≪ π, e ≫ P→ ≪ π', e' ≫" "atom x ♯ e"
  shows   "atom x ♯ e'"
  using assms by (induct π e P π' e' rule: smallstep.induct) (auto simp: fresh_subst_term)

lemma fresh_smallsteps_I:
  fixes x :: var
  assumes "≪ π, e ≫ I→i ≪ π', e' ≫" "atom x ♯ e"
  shows   "atom x ♯ e'"
  using assms by (induct π e I i π' e' rule: smallsteps.induct) (simp_all add: fresh_smallstep_I)

lemma fresh_ps_smallstep_P:
  fixes x :: var
  assumes "≪ π, e ≫ P→ ≪ π', e' ≫" "atom x ♯ e" "atom x ♯ π"
  shows   "atom x ♯ π'"
  using assms proof (induct π e P π' e' rule: smallstep.induct)
  case (s_UnauthP v π h)
  then show ?case
    by (simp add: fresh_Cons fresh_append fresh_shallow)
  qed auto

(* Proofstream lemmas *)
lemma smallstepI_ps_eq:
  assumes "≪ π, e ≫ I→ ≪ π', e' ≫"
  shows   "π = π'"
  using assms by (induct π e I π' e' rule: smallstep.induct) auto

lemma smallstepI_ps_emptyD:
  "≪π, e≫ I→ ≪[], e'≫ ⟹ ≪[], e≫ I→ ≪[], e'≫"
  "≪[], e≫ I→ ≪π, e'≫ ⟹ ≪[], e≫ I→ ≪[], e'≫"
  using smallstepI_ps_eq by force+

lemma smallstepsI_ps_eq:
  assumes "≪π, e≫ I→i ≪π', e'≫"
  shows   "π = π'"
  using assms by (induct π e I i π' e' rule: smallsteps.induct) (auto dest: smallstepI_ps_eq)

lemma smallstepsI_ps_emptyD:
  "≪π, e≫ I→i ≪[], e'≫ ⟹ ≪[], e≫ I→i ≪[], e'≫"
  "≪[], e≫ I→i ≪π, e'≫ ⟹ ≪[], e≫ I→i ≪[], e'≫"
  using smallstepsI_ps_eq by force+

lemma smallstepV_consumes_proofstream:
  assumes "≪ π⇩1, eV ≫ V→ ≪ π⇩2, eV' ≫"
  obtains π where "π⇩1 = π @ π⇩2"
  using assms by (induct π⇩1 eV V π⇩2 eV' rule: smallstep.induct) auto

lemma smallstepsV_consumes_proofstream:
  assumes "≪ π⇩1, eV ≫ V→i ≪ π⇩2, eV' ≫"
  obtains π where "π⇩1 = π @ π⇩2"
  using assms by (induct π⇩1 eV V i π⇩2 eV' rule: smallsteps.induct)
                 (auto elim: smallstepV_consumes_proofstream)

lemma smallstepP_generates_proofstream:
  assumes "≪ π⇩1, eP ≫ P→ ≪ π⇩2, eP' ≫"
  obtains π where "π⇩2 = π⇩1 @ π"
  using assms by (induct π⇩1 eP P π⇩2 eP' rule: smallstep.induct) auto

lemma smallstepsP_generates_proofstream:
  assumes "≪ π⇩1, eP ≫ P→i ≪ π⇩2, eP' ≫"
  obtains π where "π⇩2 = π⇩1 @ π"
  using assms by (induct π⇩1 eP P i π⇩2 eP' rule: smallsteps.induct)
                 (auto elim: smallstepP_generates_proofstream)

lemma smallstepV_ps_append:
  "≪ π, eV ≫ V→ ≪ π', eV' ≫ ⟷ ≪ π @ X, eV ≫ V→ ≪ π' @ X, eV' ≫"
  apply (rule iffI)
  subgoal
    by (nominal_induct π eV V π' eV' avoiding: X rule: smallstep.strong_induct)
       (auto simp: fresh_append fresh_Pair)
  subgoal
    by (nominal_induct "π @ X" eV V "π' @ X" eV' avoiding: X rule: smallstep.strong_induct)
       (auto simp: fresh_append fresh_Pair)
  done

lemma smallstepV_ps_to_suffix:
  assumes "≪π, e≫ V→ ≪π' @ X, e'≫"
  obtains π'' where "π = π'' @ X"
  using assms apply atomize_elim
  by (induct π e V "π' @ X" e' rule: smallstep.induct) auto

lemma smallstepsV_ps_append:
  "≪ π, eV ≫ V→i ≪ π', eV' ≫ ⟷ ≪ π @ X, eV ≫ V→i ≪ π' @ X, eV' ≫"
  apply (rule iffI)
  subgoal
  proof (induct π eV V i π' eV' rule: smallsteps.induct)
    case (s_Tr π⇩1 e⇩1 i π⇩2 e⇩2 π⇩3 e⇩3)
    then show ?case
      by (auto simp: iffD1[OF smallstepV_ps_append])
  qed simp
  subgoal
  proof (induct "π @ X" eV V i "π' @ X" eV' arbitrary: π' rule: smallsteps.induct)
    case (s_Tr e⇩1 i π⇩2 e⇩2 e⇩3)
    from s_Tr(3) obtain π''' where "π⇩2 = π''' @ X"
      by (auto elim: smallstepV_ps_to_suffix)
    with s_Tr show ?case
      by (auto dest: iffD2[OF smallstepV_ps_append])
  qed simp
  done

lemma smallstepP_ps_prepend:
  "≪ π, eP ≫ P→ ≪ π', eP' ≫ ⟷ ≪ X @ π, eP ≫ P→ ≪ X @ π', eP' ≫"
  apply (rule iffI)
  subgoal
  proof (nominal_induct π eP P π' eP' avoiding: X rule: smallstep.strong_induct)
    case (s_UnauthP v π h)
    then show ?case
      apply (subst append_assoc[symmetric, of X π "[⦇v⦈]"])
      apply (erule smallstep.s_UnauthP)
      done
  qed (auto simp: fresh_append fresh_Pair)
  subgoal
    by (nominal_induct "X @ π" eP P "X @ π'" eP' avoiding: X rule: smallstep.strong_induct)
       (auto simp: fresh_append fresh_Pair)
  done

lemma smallstepsP_ps_prepend:
  "≪ π, eP ≫ P→i ≪ π', eP' ≫ ⟷ ≪ X @ π, eP ≫ P→i ≪ X @ π', eP' ≫"
  apply (rule iffI)
  subgoal
  proof (induct π eP P i π' eP' rule: smallsteps.induct)
    case (s_Tr π⇩1 e⇩1 i π⇩2 e⇩2 π⇩3 e⇩3)
    then show ?case
      by (auto simp: iffD1[OF smallstepP_ps_prepend])
  qed simp
  subgoal
  proof (induct "X @ π" eP P i "X @ π'" eP' arbitrary: π' rule: smallsteps.induct)
    case (s_Tr e⇩1 i π⇩2 e⇩2 e⇩3)
    then obtain π'' where π'': "π⇩2 = X @ π @ π''"
      by (auto elim: smallstepsP_generates_proofstream)
    then have "≪π, e⇩1≫ P→i ≪π @ π'', e⇩2≫"
      by (auto dest: s_Tr(2))
    with π'' s_Tr(1,3) show ?case
      by (auto dest: iffD2[OF smallstepP_ps_prepend])
  qed simp
  done

lemma type_progress:
  assumes "{$$} ⊢⇩W e : τ"
  shows   "value e ∨ (∃e'. ≪ [], e ≫ I→ ≪ [], e' ≫)"
using assms proof (nominal_induct "{$$} :: tyenv" e τ rule: judge_weak.strong_induct)
  case (jw_Let x e⇩1 τ⇩1 e⇩2 τ⇩2)
  then show ?case
    apply simp
    apply (rule disjE[of "value e⇩1" "Ex(smallstep [] e⇩1 I [])" _])
      apply simp
     apply (rule exI)
    apply simp
     apply (rule s_Let2)
      apply clarsimp+
    apply (rule exI)
    apply (rule s_Let1)
     apply (auto simp: fresh_Pair fresh_smallstep_I)
    done
next
  case (jw_Prj1 v τ⇩1 τ⇩2)
  then show ?case
    apply simp
    apply (rule jw_Prod_inv[of v τ⇩1 τ⇩2])
             apply force+
    done
next
  case (jw_Prj2 v τ⇩1 τ⇩2)
  then show ?case
    apply simp
    apply (erule jw_Prod_inv)
            apply force+
    done
next
  case (jw_App e τ⇩1 τ⇩2 e')
  then show ?case
    apply -
    apply (rule disjI2)
    apply (erule disjE; erule disjE)
       apply (erule jw_Fun_inv[of _ _ _ e'])
        apply force+
    done
next
  case (jw_Case v v⇩1 v⇩2 τ⇩1 τ⇩2 τ)
  then show ?case
    apply simp
    apply (erule jw_Sum_inv)
             apply force+
    done
qed fast+

lemma fresh_tyenv_None:
  fixes Γ :: tyenv
  shows "atom x ♯ Γ ⟷ Γ $$ x = None"
  apply (rule iffI)
  subgoal
  proof (rule ccontr)
    assume assm: "atom x ♯ Γ"
    assume "Γ $$ x ≠ None"
    then obtain τ where "Γ $$ x = Some τ" by blast
    with assm have "∀a :: var. atom a ♯ Γ ⟶ Γ $$ a = Some τ"
      using fmap_freshness_lemma_unique[OF exI, of x Γ]
      by (simp add: fresh_Pair fresh_Some) metis
    then have "{a :: var. atom a ♯ Γ} ⊆ fmdom' Γ"
      by (auto simp: image_iff Ball_def fmlookup_dom'_iff)
    moreover
    { assume "infinite {a :: var. ¬ atom a ♯ Γ}"
      then have "infinite {a :: var. atom a ∈ supp Γ}"
        unfolding fresh_def by auto
      then have "infinite (supp Γ)"
        by (rule contrapos_nn)
          (auto simp: image_iff inv_f_f[of atom] inj_on_def
            elim!: finite_surj[of _ _ "inv atom"] bexI[rotated])
      then have False
        using finite_supp[of Γ] by blast
    }
    then have "infinite {a :: var. atom a ♯ Γ}"
      by auto
    ultimately show False
      using finite_subset[of "{a. atom a ♯ Γ}" "fmdom' Γ"] unfolding fmdom'_alt_def
      by auto
  qed
  subgoal
    apply (induct Γ arbitrary: x)
     apply simp
    subgoal for x y Γ xa
      apply (cases "x=xa")
       apply (rule fresh_fmap_update)
         apply auto [3]
      apply (rule fresh_fmap_update)
        apply auto
      done
    done
  done

lemma judge_weak_fresh_env_fresh_term[dest]:
  fixes a :: var
  assumes "Γ ⊢⇩W e : τ" "atom a ♯ Γ"
  shows   "atom a ♯ e"
  using assms proof (nominal_induct Γ e τ avoiding: a rule: judge_weak.strong_induct)
  case (jw_Var Γ x τ)
  then show ?case
    by (cases "a = x") (auto simp: fresh_tyenv_None)
qed (simp_all add: fresh_Cons fresh_fmap_update)

lemma judge_weak_weakening_1:
  assumes "Γ ⊢⇩W e : τ" "atom y ♯ e"
  shows   "Γ(y $$:= τ') ⊢⇩W e : τ"
  using assms proof (nominal_induct Γ e τ avoiding: y τ' rule: judge_weak.strong_induct)
  case (jw_Lam x Γ τ⇩1 e τ⇩2)
  then show ?case
    apply (simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
    by (metis fmap_reorder_neq_updates fresh_fmap_update jw_Lam.hyps(1) judge_weak.jw_Lam no_vars_in_ty)
next
  case (jw_App v v' Γ τ⇩1 τ⇩2)
  then show ?case
    apply (simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
    using jw_App(1) by blast
next
  case (jw_Let x Γ e⇩1 τ⇩1 e⇩2 τ⇩2)
  then show ?case
    apply (simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
    by (metis (full_types) fmap_reorder_neq_updates fresh_Pair fresh_fmap_update jw_Let.hyps(1) jw_Let.hyps(2) jw_Let.hyps(3) judge_weak.jw_Let)
next
  case (jw_Rec x Γ z τ⇩1 τ⇩2 e')
  then show ?case
    apply (simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update fresh_Pair)
    apply (rule judge_weak.jw_Rec)
    subgoal by (simp add: fresh_fmap_update)
    subgoal by (simp add: fresh_fmap_update)
    by (metis fmap_reorder_neq_updates)
next
  case (jw_Case v v⇩1 v⇩2 Γ τ⇩1 τ⇩2 τ)
  then show ?case
    apply (simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
    using jw_Case(1) by blast
next
case (jw_Roll α Γ v τ)
then show ?case
  by (simp add: fresh_fmap_update)
next
  case (jw_Unroll α Γ v τ)
  then show ?case
    by (simp add: fresh_fmap_update)
qed auto

lemma judge_weak_weakening_2:
  assumes "Γ ⊢⇩W e : τ" "atom y ♯ Γ"
  shows   "Γ(y $$:= τ') ⊢⇩W e : τ"
  proof -
    from assms have "atom y ♯ e"
      by (rule judge_weak_fresh_env_fresh_term)
    with assms show "Γ(y $$:= τ') ⊢⇩W e : τ" by (simp add: judge_weak_weakening_1)
  qed

lemma judge_weak_weakening_env:
  assumes "{$$} ⊢⇩W e : τ"
  shows   "Γ ⊢⇩W e : τ"
using assms proof (induct Γ)
  case fmempty
  then show ?case by assumption
next
  case (fmupd x y Γ)
  then show ?case
    by (simp add: fresh_tyenv_None judge_weak_weakening_2)
qed

lemma value_subst_value:
  assumes "value e" "value e'"
  shows   "value (e[e' / x])"
  using assms by (induct e  e'  x rule: subst_term.induct) auto

lemma judge_weak_subst[intro]:
  assumes "Γ(a $$:= τ') ⊢⇩W e : τ" "{$$} ⊢⇩W e' : τ'"
  shows   "Γ ⊢⇩W e[e' / a] : τ"
  using assms proof (nominal_induct "Γ(a $$:= τ')" e τ avoiding: a e' Γ rule: judge_weak.strong_induct)
  case (jw_Var x τ)
  then show ?case
    by (auto simp: judge_weak_weakening_env)
next
  case (jw_Lam x τ⇩1 e τ⇩2)
  then show ?case
    by (fastforce simp: fmap_reorder_neq_updates)
next
  case (jw_Rec x y τ⇩1 τ⇩2 e)
  then show ?case
    by (fastforce simp: fmap_reorder_neq_updates)
next
  case (jw_Let x e⇩1 τ⇩1 e⇩2 τ⇩2)
  then show ?case
    by (fastforce simp: fmap_reorder_neq_updates)
qed fastforce+

lemma type_preservation:
  assumes "≪ [], e ≫ I→ ≪ [], e' ≫" "{$$} ⊢⇩W e : τ"
  shows   "{$$} ⊢⇩W e' : τ"
  using assms [[simproc del: alpha_lst]]
proof (nominal_induct "[]::proofstream" e I "[]::proofstream" e' arbitrary: τ rule: smallstep.strong_induct)
case (s_AppLam v x e)
  then show ?case by force
next
  case (s_AppRec v x e)
  then show ?case
    apply -
    apply (erule jw_App_inv)
    apply (erule jw_Rec_inv)
      apply simp
    subgoal for τ⇩1 y ea τ⇩1a τ⇩2
    apply (rule jw_App[of _ _ τ⇩1])
        apply simp
       apply (subst subst_term.simps[symmetric])
      apply simp
       apply (rule judge_weak_subst)
         apply auto
      done
    done
next
  case (s_Let1 x e⇩1 e⇩1' e⇩2)
  from s_Let1(1,2,7) show ?case
    by (auto intro: s_Let1(6) del: jw_Let_inv elim!: jw_Let_inv)
next
  case (s_Unroll e e')
  then obtain α::tvar where "atom α ♯ τ"
    using obtain_fresh by blast
  with s_Unroll show ?case
    by (auto elim: jw_Unroll_inv[where α = α])
next
  case (s_Roll e e')
  then obtain α::tvar where "atom α ♯ τ"
    using obtain_fresh by blast
  with s_Roll show ?case
    by (auto elim: jw_Roll_inv[where α = α])
next
  case (s_UnrollRoll v)
  then obtain α::tvar where "atom α ♯ τ"
    using obtain_fresh by blast
  with s_UnrollRoll show ?case
    by (fastforce simp: Abs1_eq(3) elim: jw_Roll_inv[where α = α] jw_Unroll_inv[where α = α])
qed fastforce+

(* Lemma 1 *)
lemma type_soundness:
  assumes "{$$} ⊢⇩W e : τ"
  shows   "value e ∨ (∃e'. ≪ [], e ≫ I→ ≪ [], e' ≫ ∧ {$$} ⊢⇩W e' : τ)"
  proof (cases "value e")
    case True
    then show ?thesis by simp
  next
    case False
    with assms obtain e' where "≪[], e≫ I→ ≪[], e'≫" by (auto dest: type_progress)
    with assms show ?thesis
      by (auto simp: type_preservation)
  qed

end