Theory Agreement

theory Agreement
  imports Lambda_Auth
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)

(* Inversion rules for agreement *)

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)

(* Inversion rules *)

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 xa e')
  then show ?case
    apply -
    apply (rule exI)
    apply (rule exI)
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (auto simp: fresh_fmap_update fresh_Pair dest!: agree_fresh_env_fresh_term) []
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (auto simp: fresh_fmap_update fresh_Pair dest!: agree_fresh_env_fresh_term) []
    apply (rule iffD1[OF Abs_lst1_fcb2'[where f = "λx (e,eP,eV) (τ⇩1,Γ,τ⇩2). (Γ(x $$:= τ⇩1) ⊢ e, eP, eV : τ⇩2)"
            and x = "(e,eP,eV)" and y = "(e',(x ↔ xa) ∙ eP,(x ↔ xa) ∙ eV)"
            and c = "(τ⇩1,Γ,τ⇩2)", unfolded prod.case], rotated -1], assumption)
        apply (erule Abs_lst_eq_3tuple)
         apply (auto simp: fresh_fmap_update fresh_Pair dest!: agree_fresh_env_fresh_term intro: Abs_lst_eq_flipI) [4]
    subgoal for p by (drule agree.eqvt[where p = p], auto simp: perm_supp_eq)
    apply (auto simp: perm_supp_eq flip_eqvt permute_eqvt[where q = "(x ↔ y)" for x y])
    done
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 apply atomize_elim
proof (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)
  then show ?case
    apply -
    apply (rule exI[of ])
    apply (rule exI[of _])
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (drule agree_fresh_env_fresh_term[where a = x])
      apply (simp add: fresh_fmap_update)
     apply (simp add: fresh_Pair)
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (drule agree_fresh_env_fresh_term[where a = x])
      apply (simp add: fresh_fmap_update)
     apply (simp add: fresh_Pair)
    apply (drule agree.eqvt[where p = "(x' ↔ x)"])
    apply (auto simp: Abs1_eq_iff perm_supp_eq)
    done
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 apply atomize_elim
proof (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)
  then show ?case
    apply -
    apply (rule exI[of ])
    apply (rule exI[of _])
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (drule agree_fresh_env_fresh_term[where a = x])
      apply (simp add: fresh_fmap_update)
     apply (simp add: fresh_Pair)
    apply (rule conjI)
     apply simp
     apply (rule Abs_lst_eq_flipI)
     apply (drule agree_fresh_env_fresh_term[where a = x])
      apply (simp add: fresh_fmap_update)
     apply (simp add: fresh_Pair)
    apply (drule agree.eqvt[where p = "(x' ↔ x)"])
    apply (auto simp: Abs1_eq_iff perm_supp_eq)
    done
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 apply atomize_elim
proof (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 ya ea)
  from this(1-3,5-) show ?case
    apply -
    apply (rule exI[of _ y])
    apply (rule exI[of _ "(ya ↔ y) ∙ ea"])
    apply (rule exI[of _ "(x' ↔ x) ∙ eP"])
    apply (rule exI[of _ "(x' ↔ x) ∙ eV"])
    apply (rule conjI, simp)
     apply (rule Abs_lst_eq_flipI)
     apply (meson fresh_at_base(2))
    apply (rule conjI, simp)
    apply (subst (2) fresh_at_base_permI[of y "(x' ↔ x)", symmetric])
    apply (simp add: fresh_perm)
     apply (subst term.perm_simps(3)[symmetric])
     apply (rule Abs_lst_eq_flipI)
      apply (drule agree_fresh_env_fresh_term[where a = x])
       apply (simp add: fresh_fmap_update)
      apply (simp add: fresh_Pair)
    apply (rule conjI, simp)
     apply (subst (2) fresh_at_base_permI[of y "(x' ↔ x)", symmetric])
    apply (simp add: fresh_perm)
     apply (subst term.perm_simps(3)[symmetric])
     apply (rule Abs_lst_eq_flipI)
      apply (drule agree_fresh_env_fresh_term[where a = x])
       apply (simp add: fresh_fmap_update)
      apply (simp add: fresh_Pair)
    apply (rule conjI, simp)
    apply (drule agree.eqvt[of "Γ(x' $$:= Fun τ⇩1 τ⇩2)" "Lam y e'" "Lam y eP" "Lam y eV" "Fun τ⇩1 τ⇩2" "(x' ↔ x)"])
    apply (simp add: Abs1_eq_iff perm_supp_eq)
    apply (subst (asm) permute_eqvt)
    apply (simp add: )
    apply (metis Lam.hyps(3) Lam.prems(1) fresh_at_base(2) permute_flip_cancel permute_flip_cancel2)
    done
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 apply atomize_elim
proof (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')
    from this(1-3,5-) show ?case
      apply -
      apply (rule exI[of _ y])
      apply (rule exI[of _ "(x ↔ x') ∙ e"])
      apply (rule exI[of _ "(x ↔ x') ∙ eP"])
      apply (rule exI[of _ "(x ↔ x') ∙ eV"])
      apply (rule conjI, simp)
       apply (subst (2) fresh_at_base_permI[of y "(x ↔ x')", symmetric])
        apply (simp add: fresh_perm)
       apply (subst term.perm_simps(3)[symmetric])
       apply (subst Abs_lst_eq_flipI[of x' "Lam y e" x])
        apply (drule agree_fresh_env_fresh_term[where a = x'])
         apply (simp add: fresh_fmap_update)
        apply (simp add: fresh_Pair)
       apply simp
      apply (rule conjI)
       apply (subst fresh_at_base_permI[of y "(x ↔ x')", symmetric])
        apply (simp add: fresh_perm)
       apply (subst term.perm_simps(3)[symmetric])
       apply (metis Abs1_eq_iff(3) flip_commute fresh_at_base(2))
      apply (rule conjI, simp)
       apply (subst (2) fresh_at_base_permI[of y "(x ↔ x')", symmetric])
        apply (simp add: fresh_perm)
       apply (subst term.perm_simps(3)[symmetric])
       apply (rule Abs_lst_eq_flipI)
       apply (drule agree_fresh_env_fresh_term[where a = x'])
        apply (simp add: fresh_fmap_update)
       apply (simp add: fresh_Pair)
      apply (rule conjI)
       apply simp
      apply (subst fresh_at_base_permI[of y "(x ↔ x')", symmetric])
      apply (simp add: fresh_perm)
      apply (subst term.perm_simps(3)[symmetric])
      apply (drule agree.eqvt[of "Γ(x $$:= Fun τ⇩1 τ⇩2)" "Lam y e" "Lam y eP" "Lam y eV" "Fun τ⇩1 τ⇩2" "(x ↔ x')"])
      apply (simp add: Abs1_eq_iff perm_supp_eq)
      done
  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 apply atomize_elim
proof (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')
  from this(1-3,5-) show ?case
    apply -
    apply (rule exI[of _ y])
    apply (rule exI[of _ "(x ↔ x') ∙ e"])
    apply (rule exI[of _ "(x ↔ x') ∙ eP"])
    apply (rule exI[of _ "(x ↔ x') ∙ eV"])
    apply (rule conjI, simp)
     apply (subst (2) fresh_at_base_permI[of y "(x ↔ x')", symmetric])
    apply (simp add: fresh_perm)
     apply (subst term.perm_simps(3)[symmetric])
     apply (subst Abs_lst_eq_flipI[of x' "Lam y e" x])
      apply (drule agree_fresh_env_fresh_term[where a = x'])
       apply (simp add: fresh_fmap_update)
      apply (simp add: fresh_Pair)
    apply simp
    apply (rule conjI, simp)
     apply (subst (2) fresh_at_base_permI[of y "(x ↔ x')", symmetric])
    apply (simp add: fresh_perm)
     apply (subst term.perm_simps(3)[symmetric])
     apply (rule Abs_lst_eq_flipI)
      apply (drule agree_fresh_env_fresh_term[where a = x'])
       apply (simp add: fresh_fmap_update)
      apply (simp add: fresh_Pair)
    apply (rule conjI)
     apply (subst fresh_at_base_permI[of y "(x ↔ x')", symmetric])
    apply (simp add: fresh_perm)
     apply (subst term.perm_simps(3)[symmetric])
     apply (metis Abs1_eq_iff(3) flip_commute fresh_at_base(2))
    apply (rule conjI, simp)
    apply (drule agree.eqvt[of "Γ(x $$:= Fun τ⇩1 τ⇩2)" "Lam y e" "Lam y eP" "Lam y eV" "Fun τ⇩1 τ⇩2" "(x ↔ x')"])
    apply (simp add: Abs1_eq_iff perm_supp_eq)
    done
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 apply atomize_elim
  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 apply atomize_elim
  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 apply atomize_elim
  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 τ"

(* Inversion on type *)

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
    apply (simp add: fresh_at_base)
    by (metis a_Lam.hyps(1) agree.a_Lam fmap_reorder_neq_updates fresh_fmap_update no_vars_in_ty)
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
    apply (simp add: fresh_at_base)
    apply (rule agree.a_Let)
      apply (simp add: fresh_Pair fresh_fmap_update)
     apply auto []
    apply (subst fmap_reorder_neq_updates)
     apply simp
    apply (rule a_Let(10))
      apply (simp_all add: fresh_fmap_update)
    done
next
  case (a_Rec x Γ z τ⇩1 τ⇩2 e eP eV)
  then show ?case
    apply (simp add: fresh_at_base)
    apply (rule agree.a_Rec)
      apply (simp add: fresh_fmap_update)
     apply (simp add: fresh_Pair fresh_fmap_update)
    apply (subst fmap_reorder_neq_updates)
     apply simp
    apply (rule a_Rec(9))
      apply (simp_all add: fresh_fmap_update)
    done
next
  case (a_Case v v⇩1 v⇩2 vP vP⇩1 vP⇩2 vV vV⇩1 vV⇩2 Γ τ⇩1 τ⇩2 τ)
  then show ?case
    apply (simp add: fresh_at_base)
    apply (rule agree.a_Case)
    by auto
next
  case (a_Prj1 v vP vV Γ τ⇩1 τ⇩2)
  then show ?case
    apply (simp add: fresh_at_base)
    apply (rule agree.a_Prj1)
    by auto
next
  case (a_Prj2 v vP vV Γ τ⇩1 τ⇩2)
  then show ?case
    apply (simp add: fresh_at_base)
    apply (rule agree.a_Prj2)
    by auto
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