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

section ‹Semantics of $\lambda\bullet$›

(*<*)
theory Semantics
  imports FMap_Lemmas Syntax
begin
(*>*)

text ‹Avoid clash with substitution notation.›
no_notation inverse_divide (infixl ‹'/› 70)

text ‹Help automated provers with smallsteps.›
declare One_nat_def[simp del]

subsection ‹Equivariant Hash Function›

consts hash_real :: "term → hash"

nominal_function map_fixed :: "var → var list → term → term" where
  "map_fixed fp l Unit = Unit" |
  "map_fixed fp l (Var y) = (if y ∈ set l then (Var y) else (Var fp))" |
  "atom y ♯ (fp, l) ==> map_fixed fp l (Lam y t) = (Lam y ((map_fixed fp (y # l) t)))" |
  "atom y ♯ (fp, l) ==> map_fixed fp l (Rec y t) = (Rec y ((map_fixed fp (y # l) t)))" |
  "map_fixed fp l (Inj1 t) = (Inj1 ((map_fixed fp l t)))" |
  "map_fixed fp l (Inj2 t) = (Inj2 ((map_fixed fp l t)))" |
  "map_fixed fp l (Pair t1 t2) = (Pair ((map_fixed fp l t1)) ((map_fixed fp l t2)))" |
  "map_fixed fp l (Roll t) = (Roll ((map_fixed fp l t)))" |
  "atom y ♯ (fp, l) ==> map_fixed fp l (Let t1 y t2) = (Let ((map_fixed fp l t1)) y ((map_fixed fp (y # l) t2)))" |
  "map_fixed fp l (App t1 t2) = (App ((map_fixed fp l t1)) ((map_fixed fp l t2)))" |
  "map_fixed fp l (Case t1 t2 t3) = (Case ((map_fixed fp l t1)) ((map_fixed fp l t2)) ((map_fixed fp l t3)))" |
  "map_fixed fp l (Prj1 t) = (Prj1 ((map_fixed fp l t)))" |
  "map_fixed fp l (Prj2 t) = (Prj2 ((map_fixed fp l t)))" |
  "map_fixed fp l (Unroll t) = (Unroll ((map_fixed fp l t)))" |
  "map_fixed fp l (Auth t) = (Auth ((map_fixed fp l t)))" |
  "map_fixed fp l (Unauth t) = (Unauth ((map_fixed fp l t)))" |
  "map_fixed fp l (Hash h) = (Hash h)" |
  "map_fixed fp l (Hashed h t) = (Hashed h ((map_fixed fp l t)))"
  using [[simproc del: alpha_lst defined_all]]
  subgoal by (simp add: eqvt_def map_fixed_graph_aux_def)
  subgoal by (erule map_fixed_graph.induct) (auto simp: fresh_star_def fresh_at_base)
                      apply clarify
  subgoal for P fp l t
    by (rule term.strong_exhaust[of t P "(fp, l)"]) (auto simp: fresh_star_def fresh_Pair)
                      apply (simp_all add: fresh_star_def fresh_at_base)
  subgoal for y fp l t ya fpa la ta
    apply (erule conjE)+
    apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"])
       apply (simp_all add: eqvt_at_def)
       apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  subgoal for y fp l t ya fpa la ta
    apply (erule conjE)+
    apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"])
       apply (simp_all add: eqvt_at_def)
       apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair)
    done
  subgoal for y fp l t ya fpa la ta
    apply (erule conjE)+
    apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"])
       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

definition hash where
  "hash t = hash_real (map_fixed undefined [] t)"

lemma permute_map_list: "p ∙ l = map (λx. p ∙ x) l"
  by (induct l) auto

lemma map_fixed_eqvt: "p ∙ l = l ==> map_fixed v l (p ∙ t) = map_fixed v l t"
proof (nominal_induct t avoiding: v l p rule: term.strong_induct)
  case (Var x)
  then show ?case
    by (auto simp: term.supp supp_at_base permute_map_list list_eq_iff_nth_eq in_set_conv_nth)
next
  case (Lam y e)
  from Lam(1,2,3,5) Lam(4)[of p "y # l" v] show ?case
    by (auto simp: fresh_perm)
next
  case (Rec y e)
  from Rec(1,2,3,5) Rec(4)[of p "y # l" v] show ?case
    by (auto simp: fresh_perm)
next
  case (Let e' y e)
  from Let(1,2,3,6) Let(4)[of p l v] Let(5)[of p "y # l" v] show ?case
    by (auto simp: fresh_perm)
qed (auto simp: permute_pure)

lemma hash_eqvt[eqvt]: "p ∙ hash t = hash (p ∙ t)"
  unfolding permute_pure hash_def by (auto simp: map_fixed_eqvt)

lemma map_fixed_idle: "{x. ¬ atom x ♯ t} ⊆ set l ==> map_fixed v l t = t"
proof (nominal_induct t avoiding: v l rule: term.strong_induct)
  case (Var x)
  then show ?case
    by (auto simp: subset_iff fresh_at_base)
next
  case (Lam y e)
  from Lam(1,2,4) Lam(3)[of "y # l" v] show ?case
    by (auto simp: fresh_Pair Abs1_eq)
next
  case (Rec y e)
  from Rec(1,2,4) Rec(3)[of "y # l" v] show ?case
    by (auto simp: fresh_Pair Abs1_eq)
next
  case (Let e' y e)
  from Let(1,2,5) Let(3)[of l v] Let(4)[of "y # l" v] show ?case
    by (auto simp: fresh_Pair Abs1_eq)
qed (auto simp: subset_iff)

lemma map_fixed_idle_closed:
  "closed t ==> map_fixed undefined [] t = t"
  by (rule map_fixed_idle) auto

lemma map_fixed_inj_closed:
  "closed t ==> closed u ==> map_fixed undefined [] t = map_fixed undefined [] u ==> t = u"
  by (rule box_equals[OF _ map_fixed_idle_closed map_fixed_idle_closed])

lemma hash_eq_hash_real_closed:
  assumes "closed t"
  shows "hash t = hash_real t"
  unfolding hash_def map_fixed_idle_closed[OF assms] ..

subsection ‹Substitution›

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 defined_all]]
  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 defined_all]]
  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

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 defined_all]]
  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

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

subsection ‹Weak Typing Judgement›

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 $$:= τ₁) ⊨_W e : τ₂ ]
           ==> Γ ⊨_W Lam x e : Fun τ₁ τ₂" |
  jw_App:    "[ Γ ⊨_W e : Fun τ₁ τ₂; Γ ⊨_W e' : τ₁ ]
           ==> Γ ⊨_W App e e' : τ₂" |
  jw_Let:    "[ atom x ♯ (Γ, e₁); Γ ⊨_W e₁ : τ₁; Γ(x $$:= τ₁) ⊨_W e₂ : τ₂ ]
           ==> Γ ⊨_W Let e₁ x e₂ : τ₂" |
  jw_Rec:    "[ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ₁ τ₂) ⊨_W Lam y e : Fun τ₁ τ₂ ]
           ==> Γ ⊨_W Rec x (Lam y e) : Fun τ₁ τ₂" |
  jw_Inj1:   "[ Γ ⊨_W e : τ₁ ]
           ==> Γ ⊨_W Inj1 e : Sum τ₁ τ₂" |
  jw_Inj2:   "[ Γ ⊨_W e : τ₂ ]
           ==> Γ ⊨_W Inj2 e : Sum τ₁ τ₂" |
  jw_Case:   "[ Γ ⊨_W e : Sum τ₁ τ₂; Γ ⊨_W e₁ : Fun τ₁ τ; Γ ⊨_W e₂ : Fun τ₂ τ ]
           ==> Γ ⊨_W Case e e₁ e₂ : τ" |
  jw_Pair:   "[ Γ ⊨_W e₁ : τ₁; Γ ⊨_W e₂ : τ₂ ]
           ==> Γ ⊨_W Pair e₁ e₂ : Prod τ₁ τ₂" |
  jw_Prj1:   "[ Γ ⊨_W e : Prod τ₁ τ₂ ]
           ==> Γ ⊨_W Prj1 e : τ₁" |
  jw_Prj2:   "[ Γ ⊨_W e : Prod τ₁ τ₂ ]
           ==> Γ ⊨_W Prj2 e : τ₂" |
  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)

text ‹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 τ₁ τ₂ where "τ = Fun τ₁ τ₂" "(Γ(x $$:= τ₁)) ⊨_W e : τ₂"
  using assms proof (atomize_elim, nominal_induct Γ "Lam x e" τ avoiding: x e rule: judge_weak.strong_induct)
  case (jw_Lam x Γ τ₁ t τ₂ y u)
  then show ?case
    by (auto simp: perm_supp_eq elim!:
        iffD1[OF Abs_lst1_fcb2'[where f = "λx t (Γ, τ₁, τ₂). (Γ(x $$:= τ₁)) ⊨_W t : τ₂"
        and c = "(Γ, τ₁, τ₂)" and a = x and b = y and x = t and y = u, unfolded prod.case],
        rotated -1])
qed

lemma swap_permute_swap: "atom x ♯ π ==> atom y ♯ π ==> (x ↔ y) ∙ π ∙ (x ↔ y) ∙ t = π ∙ t"
  by (subst permute_eqvt) (auto simp: flip_fresh_fresh)

lemma jw_Rec_inv[elim]:
  assumes "Γ ⊨_W Rec x t : τ"
  and     "atom x ♯ Γ"
  obtains y e τ₁ τ₂ where "atom y ♯ (Γ,x)" "t = Lam y e" "τ = Fun τ₁ τ₂" "Γ(x $$:= Fun τ₁ τ₂) ⊨_W Lam y e : Fun τ₁ τ₂"
  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 τ₁ τ₂ e z t)
  then show ?case
  proof (nominal_induct t avoiding: y x z rule: term.strong_induct)
    case (Lam y' e')
    show ?case
    proof (intro exI conjI)
      from Lam.prems show "atom y ♯ (Γ, z)" by simp
      from Lam.hyps(1-3) Lam.prems show "Lam y' e' = Lam y ((y' ↔ y) ∙ e')"
        by (subst term.eq_iff(3), intro Abs_lst_eq_flipI) (simp add: fresh_at_base)
      from Lam.hyps(1-3) Lam.prems show "Γ(z $$:= Fun τ₁ τ₂) ⊨_W Lam y ((y' ↔ y) ∙ e') : Fun τ₁ τ₂"
        by (elim judge_weak.eqvt[of "Γ(x $$:= Fun τ₁ τ₂)" "Lam y e" "Fun τ₁ τ₂" "(x ↔ z)", elim_format])
          (simp add: perm_supp_eq Abs1_eq_iff fresh_at_base swap_permute_swap fresh_perm flip_commute)
    qed simp
  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₁ e₂ : τ"

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

inductive_cases jw_Prj1_inv[elim]: "Γ ⊨_W Prj1 e : τ₁"
inductive_cases jw_Prj2_inv[elim]: "Γ ⊨_W Prj2 e : τ₂"
inductive_cases jw_App_inv[elim]: "Γ ⊨_W App e e' : τ₂"
inductive_cases jw_Case_inv[elim]: "Γ ⊨_W Case e e₁ e₂ : τ"
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

text ‹Additional inversion rules based on type rather than term.›

inductive_cases jw_Prod_inv[elim]: "{$$} ⊨_W e : Prod τ₁ τ₂"
inductive_cases jw_Sum_inv[elim]: "{$$} ⊨_W e : Sum τ₁ τ₂"

lemma jw_Fun_inv[elim]:
  assumes "{$$} ⊨_W v : Fun τ₁ τ₂" "value v"
  obtains e x where "v = Lam x e ∨ v = Rec x e" "atom x ♯ (c::term)"
  using assms [[simproc del: alpha_lst]]
proof (atomize_elim, nominal_induct "{$$} :: tyenv" v "Fun τ₁ τ₂" avoiding: τ₁ τ₂ rule: judge_weak.strong_induct)
  case (jw_Lam x τ₁ e τ₂)
  then obtain x' where "atom (x'::var) ♯ (c, e)" 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 ?case
    by auto
next
  case (jw_Rec x y τ₁ τ₂ e')
  obtain x' where "atom (x'::var) ♯ (c, Lam y e')" 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 ?case
    by auto
qed simp_all

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


subsection ‹Erasure of Authenticated Types›

nominal_function erase :: "ty → ty" where
  "erase One = One" |
  "erase (Fun τ₁ τ₂) = Fun (erase τ₁) (erase τ₂)" |
  "erase (Sum τ₁ τ₂) = Sum (erase τ₁) (erase τ₂)" |
  "erase (Prod τ₁ τ₂) = Prod (erase τ₁) (erase τ₂)" |
  "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

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"

subsection ‹Strong Typing Judgement›

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 $$:= τ₁) ⊨ e : τ₂ ]
           ==> Γ ⊨ Lam x e : Fun τ₁ τ₂" |
  j_App:    "[ Γ ⊨ e : Fun τ₁ τ₂; Γ ⊨ e' : τ₁ ]
           ==> Γ ⊨ App e e' : τ₂" |
  j_Let:    "[ atom x ♯ (Γ, e₁); Γ ⊨ e₁ : τ₁; Γ(x $$:= τ₁) ⊨ e₂ : τ₂ ]
           ==> Γ ⊨ Let e₁ x e₂ : τ₂" |
  j_Rec:    "[ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ₁ τ₂) ⊨ Lam y e' : Fun τ₁ τ₂ ]
           ==> Γ ⊨ Rec x (Lam y e') : Fun τ₁ τ₂" |
  j_Inj1:   "[ Γ ⊨ e : τ₁ ]
           ==> Γ ⊨ Inj1 e : Sum τ₁ τ₂" |
  j_Inj2:   "[ Γ ⊨ e : τ₂ ]
           ==> Γ ⊨ Inj2 e : Sum τ₁ τ₂" |
  j_Case:   "[ Γ ⊨ e : Sum τ₁ τ₂; Γ ⊨ e₁ : Fun τ₁ τ; Γ ⊨ e₂ : Fun τ₂ τ ]
           ==> Γ ⊨ Case e e₁ e₂ : τ" |
  j_Pair:   "[ Γ ⊨ e₁ : τ₁; Γ ⊨ e₂ : τ₂ ]
           ==> Γ ⊨ Pair e₁ e₂ : Prod τ₁ τ₂" |
  j_Prj1:   "[ Γ ⊨ e : Prod τ₁ τ₂ ]
           ==> Γ ⊨ Prj1 e : τ₁" |
  j_Prj2:   "[ Γ ⊨ e : Prod τ₁ τ₂ ]
           ==> Γ ⊨ Prj2 e : τ₂" |
  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)

subsection ‹Shallow Projection›

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₁ e₂) = Pair (e₁) (e₂)" |
  "(Roll e) = Roll (e)" |
  "(Let e₁ x e₂) = Let (e₁) x (e₂)" |
  "(App e₁ e₂) = App (e₁) (e₂)" |
  "(Case e e₁ e₂) = Case (e) (e₁) (e₂)" |
  "(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 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

subsection ‹Small-step Semantics›

datatype mode = I | P | V ― ‹Ideal, Prover and Verifier modes›

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"

inductive smallstep :: "proofstream → term → mode → proofstream → term → bool" (‹≪_, _≫ _→ ≪_, _≫›) where
  s_App1:      "[ ≪ π, e₁ ≫ m→ ≪ π', e₁' ≫ ]
              ==> ≪ π, App e₁ e₂ ≫ m→ ≪ π', App e₁' e₂ ≫" |
  s_App2:      "[ value v₁; ≪ π, e₂ ≫ m→ ≪ π', e₂' ≫ ]
              ==> ≪ π, App v₁ e₂ ≫ m→ ≪ π', App v₁ e₂' ≫" |
  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₁,e₁',π,π'); ≪ π, e₁ ≫ m→ ≪ π', e₁' ≫ ]
              ==> ≪ π, Let e₁ x e₂ ≫ m→ ≪ π', Let e₁' x e₂ ≫" |
  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₁ e₂ ≫ m→ ≪ π', Case e' e₁ e₂ ≫" |
  ― ‹Case rules are different from paper to account for recursive functions.›
  s_CaseInj1:  "[ value v ]
              ==> ≪ π, Case (Inj1 v) e₁ e₂ ≫ _→ ≪ π, App e₁ v ≫" |
  s_CaseInj2:  "[ value v ]
              ==> ≪ π, Case (Inj2 v) e₁ e₂ ≫ _→ ≪ π, App e₂ v ≫" |
  s_Pair1:     "[ ≪ π, e₁ ≫ m→ ≪ π', e₁' ≫ ]
              ==> ≪ π, Pair e₁ e₂ ≫ m→ ≪ π', Pair e₁' e₂ ≫" |
  s_Pair2:     "[ value v₁; ≪ π, e₂ ≫ m→ ≪ π', e₂' ≫ ]
              ==> ≪ π, Pair v₁ e₂ ≫ m→ ≪ π', Pair v₁ e₂' ≫" |
  s_Prj1:      "[ ≪ π, e ≫ m→ ≪ π', e' ≫ ]
              ==> ≪ π, Prj1 e ≫ m→ ≪ π', Prj1 e' ≫" |
  s_Prj2:      "[ ≪ π, e ≫ m→ ≪ π', e' ≫ ]
              ==> ≪ π, Prj2 e ≫ m→ ≪ π', Prj2 e' ≫" |
  s_PrjPair1:  "[ value v₁; value v₂ ]
              ==> ≪ π, Prj1 (Pair v₁ v₂) ≫ _→ ≪ π, v₁ ≫" |
  s_PrjPair2:  "[ value v₁; value v₂ ]
              ==> ≪ π, Prj2 (Pair v₁ v₂) ≫ _→ ≪ π, v₂ ≫" |
  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₀; hash s₀ = h ]
              ==> ≪ s₀#π, Unauth (Hash h) ≫ V→ ≪ π, s₀ ≫"

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)

inductive smallsteps :: "proofstream → term → mode → nat → proofstream → term → bool" (‹≪_, _≫ _→_ ≪_, _≫›) where
  s_Id: "≪ π, e ≫ _→0 ≪ π, e ≫" |
  s_Tr: "[ ≪ π₁, e₁ ≫ m→i ≪ π₂, e₂ ≫; ≪ π₂, e₂ ≫ m→ ≪ π₃, e₃ ≫ ]
       ==> ≪ π₁, e₁ ≫ m→(i+1) ≪ π₃, e₃ ≫"

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' ≫" (is "?L ⟷ ?R")
proof
  assume ?L
  then show ?R
  proof (induct π e m "1::nat" π' e' rule: smallsteps.induct)
    case (s_Tr π₁ e₁ m i π₂ e₂ π₃ e₃)
    then show ?case
      by (induct π₁ e₁ m i π₂ e₂ rule: smallsteps.induct) auto
  qed simp
qed (auto intro: s_Tr[where i=0, simplified])

text ‹Inversion rules for smallstep(s) predicates.›

lemma value_no_step[intro]:
  assumes "≪ π₁, v ≫ m→ ≪ π₂, t ≫" "value v"
  shows   "False"
  using assms by (induct π₁ v m π₂ 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]: "≪ π₁, Unit ≫ m→ ≪ π₂, v ≫"

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

lemma s_Let_inv':
  assumes "≪ π, Let e₁ x e₂ ≫ m→ ≪ π', e' ≫"
  and     "atom x ♯ (e₁,π)"
  obtains e₁' where "(e' = e₂[e₁ / x] ∧ value e₁ ∧ π = π') ∨ (≪ π, e₁ ≫ m→ ≪ π', e₁' ≫ ∧ e' = Let e₁' x e₂ ∧ ¬ value e₁)"
  using assms [[simproc del: alpha_lst]]
  by (atomize_elim, induct π "Let e₁ x e₂" 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₁ x e₂ ≫ m→ ≪ π', e' ≫"
  and     "atom x ♯ (e₁,π)"
  and     "e' = e₂[e₁ / x] ∧ value e₁ ∧ π = π' ==> Q"
  and     "∧e₁'. ≪ π, e₁ ≫ m→ ≪ π', e₁' ≫ ∧ e' = Let e₁' x e₂ ∧ ¬ value e₁ ==> 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₁ e₂ ≫ 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₁ e₂ ≫ 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' ≫"

inductive_cases s_Id_inv[elim]: "≪ π₁, e₁ ≫ m→0 ≪ π₂, e₂ ≫"
inductive_cases s_Tr_inv[elim]: "≪ π₁, e₁ ≫ m→i ≪ π₃, e₃ ≫"

text ‹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

text ‹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 "≪ π₁, eV ≫ V→ ≪ π₂, eV' ≫"
  obtains π where "π₁ = π @ π₂"
  using assms by (induct π₁ eV V π₂ eV' rule: smallstep.induct) auto

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

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

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

lemma smallstepV_ps_append:
  "≪ π, eV ≫ V→ ≪ π', eV' ≫ ⟷ ≪ π @ X, eV ≫ V→ ≪ π' @ X, eV' ≫" (is "?L ⟷ ?R")
proof (rule iffI)
  assume ?L then show ?R
    by (nominal_induct π eV V π' eV' avoiding: X rule: smallstep.strong_induct)
       (auto simp: fresh_append fresh_Pair)
next
  assume ?R then show ?L
    by (nominal_induct "π @ X" eV V "π' @ X" eV' avoiding: X rule: smallstep.strong_induct)
       (auto simp: fresh_append fresh_Pair)
qed

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

lemma smallstepsV_ps_append:
  "≪ π, eV ≫ V→i ≪ π', eV' ≫ ⟷ ≪ π @ X, eV ≫ V→i ≪ π' @ X, eV' ≫" (is "?L ⟷ ?R")
proof (rule iffI)
  assume ?L then show ?R
  proof (induct π eV V i π' eV' rule: smallsteps.induct)
    case (s_Tr π₁ e₁ i π₂ e₂ π₃ e₃)
    then show ?case
      by (auto simp: iffD1[OF smallstepV_ps_append])
  qed simp
next
  assume ?R then show ?L
  proof (induct "π @ X" eV V i "π' @ X" eV' arbitrary: π' rule: smallsteps.induct)
    case (s_Tr e₁ i π₂ e₂ e₃)
    from s_Tr(3) obtain π''' where "π₂ = π''' @ X"
      by (auto elim: smallstepV_ps_to_suffix)
    with s_Tr show ?case
      by (auto dest: iffD2[OF smallstepV_ps_append])
  qed simp
qed

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

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

subsection ‹Type Progress›

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₁ τ₁ e₂ τ₂)
  then show ?case
    by (auto 0 3 simp: fresh_smallstep_I elim!: s_Let2[of e₂]
      intro: exI[where P="λe. ≪_, _≫ _→ ≪_, e≫", OF s_Let1, rotated])
next
  case (jw_Prj1 v τ₁ τ₂)
  then show ?case
    by (auto elim!: jw_Prod_inv[of v τ₁ τ₂])
next
  case (jw_Prj2 v τ₁ τ₂)
  then show ?case
    by (auto elim!: jw_Prod_inv[of v τ₁ τ₂])
next
  case (jw_App e τ₁ τ₂ e')
  then show ?case
    by (auto 0 4 elim: jw_Fun_inv[of _ _ _ e'])
next
  case (jw_Case v v₁ v₂ τ₁ τ₂ τ)
  then show ?case
    by (auto 0 4 elim: jw_Sum_inv[of _ v₁ v₂])
qed fast+

subsection ‹Weak Type Preservation›

lemma fresh_tyenv_None:
  fixes Γ :: tyenv
  shows "atom x ♯ Γ ⟷ Γ $$ x = None" (is "?L ⟷ ?R")
proof
  assume assm: ?L show ?R
  proof (rule ccontr)
    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
next
  assume ?R then show ?L
  proof (induct Γ arbitrary: x)
    case (fmupd y z Γ)
    then show ?case
      by (cases "y = x") (auto intro: fresh_fmap_update)
  qed simp
qed

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 Γ τ₁ e τ₂)
  from jw_Lam(5)[of y τ'] jw_Lam(1-4,6) show ?case
    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
next
  case (jw_App v v' Γ τ₁ τ₂)
  then show ?case
    by (force simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
next
  case (jw_Let x Γ e₁ τ₁ e₂ τ₂)
  from jw_Let(6)[of y τ'] jw_Let(8)[of y τ'] jw_Let(1-5,7,9) show ?case
    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
next
  case (jw_Rec x Γ z τ₁ τ₂ e')
  from jw_Rec(9)[of y τ'] jw_Rec(1-8,10) show ?case
    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update fresh_Pair)
next
  case (jw_Case v v₁ v₂ Γ τ₁ τ₂ τ)
  then show ?case
    by (fastforce simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
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 τ₁ e τ₂)
  then show ?case
    by (fastforce simp: fmupd_reorder_neq)
next
  case (jw_Rec x y τ₁ τ₂ e)
  then show ?case
    by (fastforce simp: fmupd_reorder_neq)
next
  case (jw_Let x e₁ τ₁ e₂ τ₂)
  then show ?case
    by (fastforce simp: fmupd_reorder_neq)
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
    by (elim jw_App_inv jw_Rec_inv) (auto 0 3 simp del: subst_term.simps)
next
  case (s_Let1 x e₁ e₁' e₂)
  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+

subsection ‹Corrected Lemma 1 from Miller et al.~cite‹"adsg"›: Weak Type Soundness›

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