(* 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 $$:= τ₁) ⊨ e, eP, eV : τ₂ ]
    ==> Γ ⊨ Lam x e, Lam x eP, Lam x eV : Fun τ₁ τ₂" |
  a_App: "[ Γ ⊨ e₁, eP₁, eV₁ : Fun τ₁ τ₂; Γ ⊨ e₂, eP₂, eV₂ : τ₁ ]
    ==> Γ ⊨ App e₁ e₂, App eP₁ eP₂, App eV₁ eV₂ : τ₂" |
  a_Let: "[ atom x ♯ (Γ, e₁, eP₁, eV₁); Γ ⊨ e₁, eP₁, eV₁ : τ₁; Γ(x $$:= τ₁) ⊨ e₂, eP₂, eV₂ : τ₂ ]
    ==> Γ ⊨ Let e₁ x e₂, Let eP₁ x eP₂, Let eV₁ x eV₂ : τ₂" |
  a_Rec: "[ atom x ♯ Γ; atom y ♯ (Γ,x); Γ(x $$:= Fun τ₁ τ₂) ⊨ Lam y e, Lam y eP, Lam y eV : Fun τ₁ τ₂ ]
    ==> Γ ⊨ Rec x (Lam y e), Rec x (Lam y eP), Rec x (Lam y eV) : Fun τ₁ τ₂" |
  a_Inj1: "[ Γ ⊨ e, eP, eV : τ₁ ]
    ==> Γ ⊨ Inj1 e, Inj1 eP, Inj1 eV : Sum τ₁ τ₂" |
  a_Inj2: "[ Γ ⊨ e, eP, eV : τ₂ ]
    ==> Γ ⊨ Inj2 e, Inj2 eP, Inj2 eV : Sum τ₁ τ₂" |
  a_Case: "[ Γ ⊨ e, eP, eV : Sum τ₁ τ₂; Γ ⊨ e₁, eP₁, eV₁ : Fun τ₁ τ; Γ ⊨ e₂, eP₂, eV₂ : Fun τ₂ τ ]
    ==> Γ ⊨ Case e e₁ e₂, Case eP eP₁ eP₂, Case eV eV₁ eV₂ : τ" |
  a_Pair: "[ Γ ⊨ e₁, eP₁, eV₁ : τ₁; Γ ⊨ e₂, eP₂, eV₂ : τ₂ ]
    ==> Γ ⊨ Pair e₁ e₂, Pair eP₁ eP₂, Pair eV₁ eV₂ : Prod τ₁ τ₂" |
  a_Prj1: "[ Γ ⊨ e, eP, eV : Prod τ₁ τ₂ ]
    ==> Γ ⊨ Prj1 e, Prj1 eP, Prj1 eV : τ₁" |
  a_Prj2: "[ Γ ⊨ e, eP, eV : Prod τ₁ τ₂ ]
    ==> Γ ⊨ Prj2 e, Prj2 eP, Prj2 eV : τ₂" |
  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 τ₁ τ₂)"
  and     "atom x ♯ Γ"
  obtains eP' eV' where "eP = Lam x eP'" "eV = Lam x eV'" "Γ(x $$:= τ₁) ⊨ e', eP', eV' : τ₂"
  using assms
proof (atomize_elim, nominal_induct Γ "Lam x e'" eP eV "Fun τ₁ τ₂" avoiding: x e' τ₁ τ₂ rule: agree.strong_induct)
  case (a_Lam x Γ τ₁ e eP eV τ₂ 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 $$:= τ₁) ⊨ e', (x ↔ y) ∙ eP, (x ↔ y) ∙ eV : τ₂"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x ↔ y)", of "Γ(x $$:= τ₁)"])
  qed
qed

lemma a_Lam_inv_P[elim]:
  assumes "{$$} ⊨ v, (Lam x vP'), vV : (Fun τ₁ τ₂)"
  obtains v' vV' where "v = Lam x v'" "vV = Lam x vV'" "{$$}(x $$:= τ₁) ⊨ v', vP', vV' : τ₂"
  using assms
proof (atomize_elim, nominal_induct "{$$}::tyenv" v "Lam x vP'" vV "Fun τ₁ τ₂" 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 $$:= τ₁) ⊨ (x' ↔ x) ∙ e, vP', (x' ↔ x) ∙ eV : τ₂"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x' ↔ x)", of "{$$}(x' $$:= τ₁)"])
  qed
qed

lemma a_Lam_inv_V[elim]:
  assumes "{$$} ⊨ v, vP, (Lam x vV') : (Fun τ₁ τ₂)"
  obtains v' vP' where "v = Lam x v'" "vP = Lam x vP'" "{$$}(x $$:= τ₁) ⊨ v', vP', vV' : τ₂"
  using assms
proof (atomize_elim, nominal_induct "{$$}::tyenv" v vP "Lam x vV'" "Fun τ₁ τ₂" 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 $$:= τ₁) ⊨ (x' ↔ x) ∙ e, (x' ↔ x) ∙ eP, vV' : τ₂"
      by (auto simp: perm_supp_eq Abs1_eq_iff(3)
        dest!: agree.eqvt[where p = "(x' ↔ x)", of "{$$}(x' $$:= τ₁)"])
  qed
qed

lemma a_Rec_inv_I[elim]:
  assumes "Γ ⊨ Rec x e, eP, eV : Fun τ₁ τ₂"
  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 τ₁ τ₂) ⊨ Lam y e', Lam y eP', Lam y eV' : Fun τ₁ τ₂"
  using assms
proof (atomize_elim, nominal_induct Γ "Rec x e" eP eV "Fun τ₁ τ₂" 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 τ₁ τ₂) ⊨
        Lam y ((z ↔ y) ∙ ee), Lam y ((x' ↔ x) ∙ eP), Lam y ((x' ↔ x) ∙ eV) : Fun τ₁ τ₂"
        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 τ₁ τ₂"
  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 τ₁ τ₂) ⊨ Lam y e', Lam y eP', Lam y eV' : Fun τ₁ τ₂"
  using assms
proof (atomize_elim,nominal_induct Γ e "Rec x eP" eV "Fun τ₁ τ₂" 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 τ₁ τ₂) ⊨
        Lam y ((x ↔ x') ∙ e), Lam y ((x ↔ x') ∙ eP), Lam y ((x ↔ x') ∙ eV) : Fun τ₁ τ₂"
        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 τ₁ τ₂"
    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 τ₁ τ₂) ⊨ Lam y e', Lam y eP', Lam y eV' : Fun τ₁ τ₂"
  using assms
proof (atomize_elim, nominal_induct Γ e eP "Rec x eV" "Fun τ₁ τ₂" 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 τ₁ τ₂) ⊨
        Lam y ((x ↔ x') ∙ e), Lam y ((x ↔ x') ∙ eP), Lam y ((x ↔ x') ∙ eV) : Fun τ₁ τ₂"
        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 τ₁ τ₂"
inductive_cases a_Inj1_inv_P[elim]: "Γ ⊨ e, Inj1 eP, eV : Sum τ₁ τ₂"
inductive_cases a_Inj1_inv_V[elim]: "Γ ⊨ e, eP, Inj1 eV : Sum τ₁ τ₂"

inductive_cases a_Inj2_inv_I[elim]: "Γ ⊨ Inj2 e, eP, eV : Sum τ₁ τ₂"
inductive_cases a_Inj2_inv_P[elim]: "Γ ⊨ e, Inj2 eP, eV : Sum τ₁ τ₂"
inductive_cases a_Inj2_inv_V[elim]: "Γ ⊨ e, eP, Inj2 eV : Sum τ₁ τ₂"

inductive_cases a_Pair_inv_I[elim]: "Γ ⊨ Pair e₁ e₂, eP, eV : Prod τ₁ τ₂"
inductive_cases a_Pair_inv_P[elim]: "Γ ⊨ e, Pair eP₁ eP₂, eV : Prod τ₁ τ₂"

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 τ₁ τ₂"
inductive_cases a_Prod_inv[elim]: "Γ ⊨ e, eP, eV : Prod τ₁ τ₂"
inductive_cases a_Fun_inv[elim]: "Γ ⊨ e, eP, eV : Fun τ₁ τ₂"

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 Γ τ₁ e eP eV τ₂)
  then show ?case
    by (force simp add: fresh_at_base fresh_fmap_update fmupd_reorder_neq)
next
  case (a_App v₁ v₂ vP₁ vP₂ vV₁ vV₂ Γ τ₁ τ₂)
  then show ?case
    using term.fresh(9) by blast
next
  case (a_Let x Γ e₁ eP₁ eV₁ τ₁ 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_Let(10) agree.a_Let[of x])
next
  case (a_Rec x Γ z τ₁ τ₂ 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₁ v₂ vP vP₁ vP₂ vV vV₁ vV₂ Γ τ₁ τ₂ τ)
  then show ?case
    by (fastforce simp: fresh_at_base)
next
  case (a_Prj1 v vP vV Γ τ₁ τ₂)
  then show ?case
    by (fastforce simp: fresh_at_base)
next
  case (a_Prj2 v vP vV Γ τ₁ τ₂)
  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
(*>*)