Theory Semantics

(* 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 $$:= τ⇩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)

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 τ⇩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 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 τ⇩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 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 τ⇩1 τ⇩2) ⊢⇩W Lam y ((y' ↔ y) ∙ e') : Fun τ⇩1 τ⇩2"
        by (elim judge_weak.eqvt[of "Γ(x $$:= Fun τ⇩1 τ⇩2)" "Lam y e" "Fun τ⇩1 τ⇩2" "(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⇩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

text ‹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]]
proof (atomize_elim, nominal_induct "{$$} :: tyenv" v "Fun τ⇩1 τ⇩2" avoiding: τ⇩1 τ⇩2 rule: judge_weak.strong_induct)
  case (jw_Lam x τ⇩1 e τ⇩2)
  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 τ⇩1 τ⇩2 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 τ⇩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

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 $$:= τ⇩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)

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⇩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 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⇩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)

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' ≫" (is "?L ⟷ ?R")
proof
  assume ?L
  then show ?R
  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
      by (induct π⇩1 e⇩1 m i π⇩2 e⇩2 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 "≪ π⇩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]]
  by (atomize_elim, 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' ≫"

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 ≫"

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 "≪ π⇩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' ≫" (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 π⇩1 e⇩1 i π⇩2 e⇩2 π⇩3 e⇩3)
    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⇩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
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 π⇩1 e⇩1 i π⇩2 e⇩2 π⇩3 e⇩3)
    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⇩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
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⇩1 τ⇩1 e⇩2 τ⇩2)
  then show ?case
    by (auto 0 3 simp: fresh_smallstep_I elim!: s_Let2[of e⇩2]
      intro: exI[where P="λe. ≪_, _≫ _→ ≪_, e≫", OF s_Let1, rotated])
next
  case (jw_Prj1 v τ⇩1 τ⇩2)
  then show ?case
    by (auto elim!: jw_Prod_inv[of v τ⇩1 τ⇩2])
next
  case (jw_Prj2 v τ⇩1 τ⇩2)
  then show ?case
    by (auto elim!: jw_Prod_inv[of v τ⇩1 τ⇩2])
next
  case (jw_App e τ⇩1 τ⇩2 e')
  then show ?case
    by (auto 0 4 elim: jw_Fun_inv[of _ _ _ e'])
next
  case (jw_Case v v⇩1 v⇩2 τ⇩1 τ⇩2 τ)
  then show ?case
    by (auto 0 4 elim: jw_Sum_inv[of _ v⇩1 v⇩2])
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 Γ τ⇩1 e τ⇩2)
  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' Γ τ⇩1 τ⇩2)
  then show ?case
    by (force simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
next
  case (jw_Let x Γ e⇩1 τ⇩1 e⇩2 τ⇩2)
  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 τ⇩1 τ⇩2 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⇩1 v⇩2 Γ τ⇩1 τ⇩2 τ)
  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 τ⇩1 e τ⇩2)
  then show ?case
    by (fastforce simp: fmupd_reorder_neq)
next
  case (jw_Rec x y τ⇩1 τ⇩2 e)
  then show ?case
    by (fastforce simp: fmupd_reorder_neq)
next
  case (jw_Let x e⇩1 τ⇩1 e⇩2 τ⇩2)
  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⇩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+

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