Theory Agreement

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

section ‹Agreement Relation›

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

inductive agree :: "tyenv ⇒ term ⇒ term ⇒ term ⇒ ty ⇒ bool" (‹_ ⊢ _, _, _ : _› [150,0,0,0,150] 149) where
  a_Unit: "Γ ⊢ Unit, Unit, Unit : One" |
  a_Var: "Γ $$ x = Some τ
    ⟹ Γ ⊢ Var x, Var x, Var x : τ" |
  a_Lam: "⟦ atom x ♯ Γ; Γ(x $$:= τ⇩1) ⊢ e, eP, eV : τ⇩2 ⟧
    ⟹ Γ ⊢ Lam x e, Lam x eP, Lam x eV : Fun τ⇩1 τ⇩2" |
  a_App: "⟦ Γ ⊢ e⇩1, eP⇩1, eV⇩1 : Fun τ⇩1 τ⇩2; Γ ⊢ e⇩2, eP⇩2, eV⇩2 : τ⇩1 ⟧
    ⟹ Γ ⊢ App e⇩1 e⇩2, App eP⇩1 eP⇩2, App eV⇩1 eV⇩2 : τ⇩2" |
  a_Let: "⟦ atom x ♯ (Γ, e⇩1, eP⇩1, eV⇩1); Γ ⊢ e⇩1, eP⇩1, eV⇩1 : τ⇩1; Γ(x $$:= τ⇩1) ⊢ e⇩2, eP⇩2, eV⇩2 : τ⇩2 ⟧
    ⟹ Γ ⊢ Let e⇩1 x e⇩2, Let eP⇩1 x eP⇩2, Let eV⇩1 x eV⇩2 : τ⇩2" |
  a_Rec: "⟦ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ Lam y e, Lam y eP, Lam y eV : Fun τ⇩1 τ⇩2 ⟧
    ⟹ Γ ⊢ Rec x (Lam y e), Rec x (Lam y eP), Rec x (Lam y eV) : Fun τ⇩1 τ⇩2" |
  a_Inj1: "⟦ Γ ⊢ e, eP, eV : τ⇩1 ⟧
    ⟹ Γ ⊢ Inj1 e, Inj1 eP, Inj1 eV : Sum τ⇩1 τ⇩2" |
  a_Inj2: "⟦ Γ ⊢ e, eP, eV : τ⇩2 ⟧
    ⟹ Γ ⊢ Inj2 e, Inj2 eP, Inj2 eV : Sum τ⇩1 τ⇩2" |
  a_Case: "⟦ Γ ⊢ e, eP, eV : Sum τ⇩1 τ⇩2; Γ ⊢ e⇩1, eP⇩1, eV⇩1 : Fun τ⇩1 τ; Γ ⊢ e⇩2, eP⇩2, eV⇩2 : Fun τ⇩2 τ ⟧
    ⟹ Γ ⊢ Case e e⇩1 e⇩2, Case eP eP⇩1 eP⇩2, Case eV eV⇩1 eV⇩2 : τ" |
  a_Pair: "⟦ Γ ⊢ e⇩1, eP⇩1, eV⇩1 : τ⇩1; Γ ⊢ e⇩2, eP⇩2, eV⇩2 : τ⇩2 ⟧
    ⟹ Γ ⊢ Pair e⇩1 e⇩2, Pair eP⇩1 eP⇩2, Pair eV⇩1 eV⇩2 : Prod τ⇩1 τ⇩2" |
  a_Prj1: "⟦ Γ ⊢ e, eP, eV : Prod τ⇩1 τ⇩2 ⟧
    ⟹ Γ ⊢ Prj1 e, Prj1 eP, Prj1 eV : τ⇩1" |
  a_Prj2: "⟦ Γ ⊢ e, eP, eV : Prod τ⇩1 τ⇩2 ⟧
    ⟹ Γ ⊢ Prj2 e, Prj2 eP, Prj2 eV : τ⇩2" |
  a_Roll: "⟦ atom α ♯ Γ; Γ ⊢ e, eP, eV : subst_type τ (Mu α τ) α ⟧
    ⟹ Γ ⊢ Roll e, Roll eP, Roll eV : Mu α τ" |
  a_Unroll: "⟦ atom α ♯ Γ; Γ ⊢ e, eP, eV : Mu α τ ⟧
    ⟹ Γ ⊢ Unroll e, Unroll eP, Unroll eV : subst_type τ (Mu α τ) α" |
  a_Auth: "⟦ Γ ⊢ e, eP, eV : τ ⟧
    ⟹ Γ ⊢ Auth e, Auth eP, Auth eV : AuthT τ" |
  a_Unauth: "⟦ Γ ⊢ e, eP, eV : AuthT τ ⟧
    ⟹ Γ ⊢ Unauth e, Unauth eP, Unauth eV : τ" |
  a_HashI: "⟦ {$$} ⊢ v, vP, ⦇vP⦈ : τ; hash ⦇vP⦈ = h; value v; value vP ⟧
    ⟹ Γ ⊢ v, Hashed h vP, Hash h : AuthT τ"

declare agree.intros[intro]

equivariance agree
nominal_inductive agree
  avoids a_Lam: x
       | a_Rec: x and y
       | a_Let: x
       | a_Roll: α
       | a_Unroll: α
  by (auto simp: fresh_Pair fresh_subst_type)

lemma Abs_lst_eq_3tuple:
  fixes x x' :: var
  fixes e eP eV e' eP' eV' :: "term"
  assumes "[[atom x]]lst. e = [[atom x']]lst. e'"
  and     "[[atom x]]lst. eP = [[atom x']]lst. eP'"
  and     "[[atom x]]lst. eV = [[atom x']]lst. eV'"
  shows   "[[atom x]]lst. (e, eP, eV) = [[atom x']]lst. (e', eP', eV')"
  using assms by (simp add: fresh_Pair)

lemma agree_fresh_env_fresh_term:
  fixes a :: var
  assumes "Γ ⊢ e, eP, eV : τ" "atom a ♯ Γ"
  shows   "atom a ♯ (e, eP, eV)"
  using assms proof (nominal_induct Γ e eP eV τ avoiding: a rule: agree.strong_induct)
  case (a_Var Γ x τ)
  then show ?case
    by (cases "a = x") (auto simp: fresh_tyenv_None)
qed (simp_all add: fresh_Cons fresh_fmap_update fresh_Pair)

lemma agree_empty_fresh[dest]:
  fixes a :: var
  assumes "{$$} ⊢ e, eP, eV : τ"
  shows   "{atom a} ♯* {e, eP, eV}"
  using assms by (auto simp: fresh_Pair dest: agree_fresh_env_fresh_term)

text ‹Inversion rules for agreement.›

declare [[simproc del: alpha_lst]]

lemma a_Lam_inv_I[elim]:
  assumes "Γ ⊢ (Lam x e'), eP, eV : (Fun τ⇩1 τ⇩2)"
  and     "atom x ♯ Γ"
  obtains eP' eV' where "eP = Lam x eP'" "eV = Lam x eV'" "Γ(x $$:= τ⇩1) ⊢ e', eP', eV' : τ⇩2"
  using assms
proof (atomize_elim, nominal_induct Γ "Lam x e'" eP eV "Fun τ⇩1 τ⇩2" avoiding: x e' τ⇩1 τ⇩2 rule: agree.strong_induct)
  case (a_Lam x Γ τ⇩1 e eP eV τ⇩2 y e')
  show ?case
  proof (intro exI conjI)
    from a_Lam show "Lam x eP = Lam y ((x ↔ y) ∙ eP)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam show "Lam x eV = Lam y ((x ↔ y) ∙ eV)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam(1-6,8,10) show "Γ(y $$:= τ⇩1) ⊢ e', (x ↔ y) ∙ eP, (x ↔ y) ∙ eV : τ⇩2"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x ↔ y)", of "Γ(x $$:= τ⇩1)"])
  qed
qed

lemma a_Lam_inv_P[elim]:
  assumes "{$$} ⊢ v, (Lam x vP'), vV : (Fun τ⇩1 τ⇩2)"
  obtains v' vV' where "v = Lam x v'" "vV = Lam x vV'" "{$$}(x $$:= τ⇩1) ⊢ v', vP', vV' : τ⇩2"
  using assms
proof (atomize_elim, nominal_induct "{$$}::tyenv" v "Lam x vP'" vV "Fun τ⇩1 τ⇩2" avoiding: x vP' rule: agree.strong_induct)
  case (a_Lam x' e eP eV)
  show ?case
  proof (intro exI conjI)
    from a_Lam show "Lam x' e = Lam x ((x' ↔ x) ∙ e)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam show "Lam x' eV = Lam x ((x' ↔ x) ∙ eV)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam(1-4,6) show "{$$}(x $$:= τ⇩1) ⊢ (x' ↔ x) ∙ e, vP', (x' ↔ x) ∙ eV : τ⇩2"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x' ↔ x)", of "{$$}(x' $$:= τ⇩1)"])
  qed
qed

lemma a_Lam_inv_V[elim]:
  assumes "{$$} ⊢ v, vP, (Lam x vV') : (Fun τ⇩1 τ⇩2)"
  obtains v' vP' where "v = Lam x v'" "vP = Lam x vP'" "{$$}(x $$:= τ⇩1) ⊢ v', vP', vV' : τ⇩2"
  using assms
proof (atomize_elim, nominal_induct "{$$}::tyenv" v vP "Lam x vV'" "Fun τ⇩1 τ⇩2" avoiding: x vV' rule: agree.strong_induct)
  case (a_Lam x' e eP eV)
  show ?case
  proof (intro exI conjI)
    from a_Lam show "Lam x' e = Lam x ((x' ↔ x) ∙ e)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam show "Lam x' eP = Lam x ((x' ↔ x) ∙ eP)"
      by (auto intro!: Abs_lst_eq_flipI  dest!: agree_fresh_env_fresh_term
        simp: fresh_fmap_update fresh_Pair)
    from a_Lam(1-4,6) show "{$$}(x $$:= τ⇩1) ⊢ (x' ↔ x) ∙ e, (x' ↔ x) ∙ eP, vV' : τ⇩2"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x' ↔ x)", of "{$$}(x' $$:= τ⇩1)"])
  qed
qed

lemma a_Rec_inv_I[elim]:
  assumes "Γ ⊢ Rec x e, eP, eV : Fun τ⇩1 τ⇩2"
  and     "atom x ♯ Γ"
  obtains y e' eP' eV'
  where "e = Lam y e'" "eP = Rec x (Lam y eP')" "eV = Rec x (Lam y eV')" "atom y ♯ (Γ,x)"
        "Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ Lam y e', Lam y eP', Lam y eV' : Fun τ⇩1 τ⇩2"
  using assms
proof (atomize_elim, nominal_induct Γ "Rec x e" eP eV "Fun τ⇩1 τ⇩2" avoiding: x e rule: agree.strong_induct)
  case (a_Rec x' Γ y e' eP eV)
  then show ?case
  proof (nominal_induct e avoiding: x x' y rule: term.strong_induct)
    case Unit
    from Unit(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Var x)
    from Var(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Lam z ee)
    show ?case
    proof (intro conjI exI)
      from Lam(1-3,5-13,15) show "Lam z ee = Lam y ((z ↔ y) ∙ ee)"
        by (auto intro: Abs_lst_eq_flipI simp: fresh_fmap_update fresh_Pair)
      from Lam(1-3,5-13,15) show "Rec x' (Lam y eP) = Rec x (Lam y ((x' ↔ x) ∙ eP))"
        using Abs_lst_eq_flipI[of x "Lam y eP" x']
        by (elim agree_fresh_env_fresh_term[where a = x, elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(1-3,5-13,15) show "Rec x' (Lam y eV) = Rec x (Lam y ((x' ↔ x) ∙ eV))"
        using Abs_lst_eq_flipI[of x "Lam y eV" x']
        by (elim agree_fresh_env_fresh_term[where a = x, elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(7,10) show "atom y ♯ (Γ, x)"
        by simp
      from Lam(1-3,5-11,13) have "(x' ↔ x) ∙ e' = (z ↔ y) ∙ ee"
        by (simp add: Abs1_eq_iff flip_commute swap_permute_swap fresh_perm fresh_at_base)
      with Lam(1-2,7,9,11-12,15) show "Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢
        Lam y ((z ↔ y) ∙ ee), Lam y ((x' ↔ x) ∙ eP), Lam y ((x' ↔ x) ∙ eV) : Fun τ⇩1 τ⇩2"
        by (elim agree.eqvt[of _ "Lam y e'" _ _ _ "(x' ↔ x)", elim_format]) (simp add:  perm_supp_eq)
    qed
  next
    case (Rec x1 x2a)
    from Rec(13) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj1 x)
    from Inj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj2 x)
    from Inj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Pair x1 x2a)
    from Pair(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Roll x)
    from Roll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Let x1 x2a x3)
    from Let(14) show ?case by (simp add: Abs1_eq_iff)
  next
    case (App x1 x2a)
    from App(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Case x1 x2a x3)
    from Case(12) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj1 x)
    from Prj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj2 x)
    from Prj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unroll x)
    from Unroll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Auth x)
    from Auth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unauth x)
    from Unauth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hash x)
    from Hash(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hashed x1 x2a)
    from Hashed(10) show ?case by (simp add: Abs1_eq_iff)
  qed
qed

lemma a_Rec_inv_P[elim]:
  assumes "Γ ⊢ e, Rec x eP, eV : Fun τ⇩1 τ⇩2"
  and     "atom x ♯ Γ"
  obtains y e' eP' eV'
  where "e = Rec x (Lam y e')" "eP = Lam y eP'" "eV = Rec x (Lam y eV')" "atom y ♯ (Γ,x)"
        "Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ Lam y e', Lam y eP', Lam y eV' : Fun τ⇩1 τ⇩2"
  using assms
proof (atomize_elim,nominal_induct Γ e "Rec x eP" eV "Fun τ⇩1 τ⇩2" avoiding: x eP rule: agree.strong_induct)
  case (a_Rec x Γ y e eP eV x' eP')
  then show ?case
  proof (nominal_induct eP' avoiding: x' x y rule: term.strong_induct)
    case Unit
    from Unit(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Var x)
    from Var(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Lam ya eP')
    show ?case
    proof (intro conjI exI)
      from Lam(1-3,5-13,15) show "Rec x (Lam y e) = Rec x' (Lam y ((x ↔ x') ∙ e))"
        using Abs_lst_eq_flipI[of x' "Lam y e" x]
        by (elim agree_fresh_env_fresh_term[where a = x', elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(1-3,5-13,15) show "Lam ya eP' = Lam y ((x ↔ x') ∙ eP)"
        unfolding trans[OF eq_sym_conv Abs1_eq_iff(3)]
        by (simp add: flip_commute fresh_at_base)
      from Lam(1-3,5-13,15) show "Rec x (Lam y eV) = Rec x' (Lam y ((x ↔ x') ∙ eV))"
        using Abs_lst_eq_flipI[of x' "Lam y eV" x]
        by (elim agree_fresh_env_fresh_term[where a = x', elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(7,10) show "atom y ♯ (Γ, x')"
        by simp
      with Lam(1-2,7,9,11-12,15) show "Γ(x' $$:= Fun τ⇩1 τ⇩2) ⊢
        Lam y ((x ↔ x') ∙ e), Lam y ((x ↔ x') ∙ eP), Lam y ((x ↔ x') ∙ eV) : Fun τ⇩1 τ⇩2"
        by (elim agree.eqvt[of _ "Lam y _" _ _ _ "(x' ↔ x)", elim_format])
          (simp add:  perm_supp_eq flip_commute)
    qed
  next
    case (Rec x1 x2a)
    from Rec(13) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj1 x)
    from Inj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj2 x)
    from Inj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Pair x1 x2a)
    from Pair(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Roll x)
    from Roll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Let x1 x2a x3)
    from Let(14) show ?case by (simp add: Abs1_eq_iff)
  next
    case (App x1 x2a)
    from App(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Case x1 x2a x3)
    from Case(12) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj1 x)
    from Prj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj2 x)
    from Prj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unroll x)
    from Unroll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Auth x)
    from Auth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unauth x)
    from Unauth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hash x)
    from Hash(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hashed x1 x2a)
    from Hashed(10) show ?case by (simp add: Abs1_eq_iff)
  qed
qed

lemma a_Rec_inv_V[elim]:
  assumes "Γ ⊢ e, eP, Rec x eV : Fun τ⇩1 τ⇩2"
    and     "atom x ♯ Γ"
  obtains y e' eP' eV'
  where "e = Rec x (Lam y e')" "eP = Rec x (Lam y eP')" "eV = Lam y eV'" "atom y ♯ (Γ,x)"
    "Γ(x $$:= Fun τ⇩1 τ⇩2) ⊢ Lam y e', Lam y eP', Lam y eV' : Fun τ⇩1 τ⇩2"
  using assms
proof (atomize_elim, nominal_induct Γ e eP "Rec x eV" "Fun τ⇩1 τ⇩2" avoiding: x eV rule: agree.strong_induct)
  case (a_Rec x Γ y e eP eV x' eV')
  then show ?case
  proof (nominal_induct eV' avoiding: x' x y rule: term.strong_induct)
    case Unit
    from Unit(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Var x)
    from Var(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Lam ya eV')
    show ?case
    proof (intro conjI exI)
      from Lam(1-3,5-13,15) show "Rec x (Lam y e) = Rec x' (Lam y ((x ↔ x') ∙ e))"
        using Abs_lst_eq_flipI[of x' "Lam y e" x]
        by (elim agree_fresh_env_fresh_term[where a = x', elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(1-3,5-13,15) show "Lam ya eV' = Lam y ((x ↔ x') ∙ eV)"
        unfolding trans[OF eq_sym_conv Abs1_eq_iff(3)]
        by (simp add: flip_commute fresh_at_base)
      from Lam(1-3,5-13,15) show "Rec x (Lam y eP) = Rec x' (Lam y ((x ↔ x') ∙ eP))"
        using Abs_lst_eq_flipI[of x' "Lam y eP" x]
        by (elim agree_fresh_env_fresh_term[where a = x', elim_format])
          (simp_all add: fresh_fmap_update fresh_Pair)
      from Lam(7,10) show "atom y ♯ (Γ, x')"
        by simp
      with Lam(1-2,7,9,11-12,15) show "Γ(x' $$:= Fun τ⇩1 τ⇩2) ⊢
        Lam y ((x ↔ x') ∙ e), Lam y ((x ↔ x') ∙ eP), Lam y ((x ↔ x') ∙ eV) : Fun τ⇩1 τ⇩2"
        by (elim agree.eqvt[of _ "Lam y _" _ _ _ "(x' ↔ x)", elim_format])
          (simp add:  perm_supp_eq flip_commute)
    qed
  next
    case (Rec x1 x2a)
    from Rec(13) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj1 x)
    from Inj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Inj2 x)
    from Inj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Pair x1 x2a)
    from Pair(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Roll x)
    from Roll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Let x1 x2a x3)
    from Let(14) show ?case by (simp add: Abs1_eq_iff)
  next
    case (App x1 x2a)
    from App(11) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Case x1 x2a x3)
    from Case(12) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj1 x)
    from Prj1(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Prj2 x)
    from Prj2(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unroll x)
    from Unroll(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Auth x)
    from Auth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Unauth x)
    from Unauth(10) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hash x)
    from Hash(9) show ?case by (simp add: Abs1_eq_iff)
  next
    case (Hashed x1 x2a)
    from Hashed(10) show ?case by (simp add: Abs1_eq_iff)
  qed
qed

inductive_cases a_Inj1_inv_I[elim]: "Γ ⊢ Inj1 e, eP, eV : Sum τ⇩1 τ⇩2"
inductive_cases a_Inj1_inv_P[elim]: "Γ ⊢ e, Inj1 eP, eV : Sum τ⇩1 τ⇩2"
inductive_cases a_Inj1_inv_V[elim]: "Γ ⊢ e, eP, Inj1 eV : Sum τ⇩1 τ⇩2"

inductive_cases a_Inj2_inv_I[elim]: "Γ ⊢ Inj2 e, eP, eV : Sum τ⇩1 τ⇩2"
inductive_cases a_Inj2_inv_P[elim]: "Γ ⊢ e, Inj2 eP, eV : Sum τ⇩1 τ⇩2"
inductive_cases a_Inj2_inv_V[elim]: "Γ ⊢ e, eP, Inj2 eV : Sum τ⇩1 τ⇩2"

inductive_cases a_Pair_inv_I[elim]: "Γ ⊢ Pair e⇩1 e⇩2, eP, eV : Prod τ⇩1 τ⇩2"
inductive_cases a_Pair_inv_P[elim]: "Γ ⊢ e, Pair eP⇩1 eP⇩2, eV : Prod τ⇩1 τ⇩2"

lemma a_Roll_inv_I[elim]:
  assumes "Γ ⊢ Roll e', eP, eV : Mu α τ"
  obtains eP' eV'
  where "eP = Roll eP'" "eV = Roll eV'" "Γ ⊢ e', eP', eV' : subst_type τ (Mu α τ) α"
  using assms
  by (nominal_induct Γ "Roll e'" eP eV "Mu α τ" avoiding: α τ rule: agree.strong_induct)
     (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)

lemma a_Roll_inv_P[elim]:
  assumes "Γ ⊢ e, Roll eP', eV : Mu α τ"
  obtains e' eV'
  where "e = Roll e'" "eV = Roll eV'" "Γ ⊢ e', eP', eV' : subst_type τ (Mu α τ) α"
  using assms
  by (nominal_induct Γ e "Roll eP'" eV "Mu α τ" avoiding: α τ rule: agree.strong_induct)
     (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)

lemma a_Roll_inv_V[elim]:
  assumes "Γ ⊢ e, eP, Roll eV' : Mu α τ"
  obtains e' eP'
  where "e = Roll e'" "eP = Roll eP'" "Γ ⊢ e', eP', eV' : subst_type τ (Mu α τ) α"
  using assms
  by (nominal_induct Γ e eP "Roll eV'" "Mu α τ" avoiding: α τ rule: agree.strong_induct)
     (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)

inductive_cases a_HashI_inv[elim]: "Γ ⊢ v, Hashed (hash ⦇vP⦈) vP, Hash (hash ⦇vP⦈) : AuthT τ"

text ‹Inversion on types for agreement.›

lemma a_AuthT_value_inv:
  assumes "{$$} ⊢ v, vP, vV : AuthT τ"
  and     "value v" "value vP" "value vV"
  obtains vP' where "vP = Hashed (hash ⦇vP'⦈) vP'" "vV = Hash (hash ⦇vP'⦈)" "value vP'"
  using assms by (atomize_elim, induct "{$$}::tyenv" v vP vV "AuthT τ" rule: agree.induct) simp_all

inductive_cases a_Mu_inv[elim]: "Γ ⊢ e, eP, eV : Mu α τ"
inductive_cases a_Sum_inv[elim]: "Γ ⊢ e, eP, eV : Sum τ⇩1 τ⇩2"
inductive_cases a_Prod_inv[elim]: "Γ ⊢ e, eP, eV : Prod τ⇩1 τ⇩2"
inductive_cases a_Fun_inv[elim]: "Γ ⊢ e, eP, eV : Fun τ⇩1 τ⇩2"

declare [[simproc add: alpha_lst]]

lemma agree_weakening_1:
  assumes "Γ ⊢ e, eP, eV : τ" "atom y ♯ e" "atom y ♯ eP" "atom y ♯ eV"
  shows   "Γ(y $$:= τ') ⊢ e, eP, eV : τ"
using assms proof (nominal_induct Γ e eP eV τ avoiding: y τ' rule: agree.strong_induct)
  case (a_Lam x Γ τ⇩1 e eP eV τ⇩2)
  then show ?case
    by (force simp add: fresh_at_base fresh_fmap_update fmupd_reorder_neq)
next
  case (a_App v⇩1 v⇩2 vP⇩1 vP⇩2 vV⇩1 vV⇩2 Γ τ⇩1 τ⇩2)
  then show ?case
    using term.fresh(9) by blast
next
  case (a_Let x Γ e⇩1 eP⇩1 eV⇩1 τ⇩1 e⇩2 eP⇩2 eV⇩2 τ⇩2)
  then show ?case
    by (auto simp add: fresh_at_base fresh_Pair fresh_fmap_update fmupd_reorder_neq[of x y]
      intro!: a_Let(10) agree.a_Let[of x])
next
  case (a_Rec x Γ z τ⇩1 τ⇩2 e eP eV)
  then show ?case
    by (auto simp add: fresh_at_base fresh_Pair fresh_fmap_update fmupd_reorder_neq[of x y]
      intro!: a_Rec(9) agree.a_Rec[of x])
next
  case (a_Case v v⇩1 v⇩2 vP vP⇩1 vP⇩2 vV vV⇩1 vV⇩2 Γ τ⇩1 τ⇩2 τ)
  then show ?case
    by (fastforce simp: fresh_at_base)
next
  case (a_Prj1 v vP vV Γ τ⇩1 τ⇩2)
  then show ?case
    by (fastforce simp: fresh_at_base)
next
  case (a_Prj2 v vP vV Γ τ⇩1 τ⇩2)
  then show ?case
    by (fastforce simp: fresh_at_base)
qed (auto simp: fresh_fmap_update)

lemma agree_weakening_2:
  assumes "Γ ⊢ e, eP, eV : τ" "atom y ♯ Γ"
  shows   "Γ(y $$:= τ') ⊢ e, eP, eV : τ"
proof -
  from assms have "{atom y} ♯* {e, eP, eV}" by (auto simp: fresh_Pair dest: agree_fresh_env_fresh_term)
  with assms show "Γ(y $$:= τ') ⊢ e, eP, eV : τ" by (simp add: agree_weakening_1)
qed

lemma agree_weakening_env:
  assumes "{$$} ⊢ e, eP, eV : τ"
  shows   "Γ ⊢ e, eP, eV : τ"
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 agree_weakening_2)
qed

(*<*)
end
(*>*)