diff --git a/thys/LambdaAuth/Agreement.thy b/thys/LambdaAuth/Agreement.thy
--- a/thys/LambdaAuth/Agreement.thy
+++ b/thys/LambdaAuth/Agreement.thy
@@ -1,515 +1,515 @@
 (* Author: Matthias Brun,   ETH Zürich, 2019 *)
 (* Author: Dmitriy Traytel, ETH Zürich, 2019 *)
 
 section \<open>Agreement Relation\<close>
 
 (*<*)
 theory Agreement
   imports Semantics
 begin
 (*>*)
 
 inductive agree :: "tyenv \<Rightarrow> term \<Rightarrow> term \<Rightarrow> term \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _, _, _ : _" [150,0,0,0,150] 149) where
   a_Unit: "\<Gamma> \<turnstile> Unit, Unit, Unit : One" |
   a_Var: "\<Gamma> $$ x = Some \<tau>
     \<Longrightarrow> \<Gamma> \<turnstile> Var x, Var x, Var x : \<tau>" |
   a_Lam: "\<lbrakk> atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e, eP, eV : \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Lam x e, Lam x eP, Lam x eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   a_App: "\<lbrakk> \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>1 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2, App eP\<^sub>1 eP\<^sub>2, App eV\<^sub>1 eV\<^sub>2 : \<tau>\<^sub>2" |
   a_Let: "\<lbrakk> atom x \<sharp> (\<Gamma>, e\<^sub>1, eP\<^sub>1, eV\<^sub>1); \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Let e\<^sub>1 x e\<^sub>2, Let eP\<^sub>1 x eP\<^sub>2, Let eV\<^sub>1 x eV\<^sub>2 : \<tau>\<^sub>2" |
   a_Rec: "\<lbrakk> atom x \<sharp> \<Gamma>; atom y \<sharp> (\<Gamma>,x); \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e, Lam y eP, Lam y eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Rec x (Lam y e), Rec x (Lam y eP), Rec x (Lam y eV) : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   a_Inj1: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>1 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Inj1 e, Inj1 eP, Inj1 eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   a_Inj2: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Inj2 e, Inj2 eP, Inj2 eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   a_Case: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : Fun \<tau>\<^sub>2 \<tau> \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Case e e\<^sub>1 e\<^sub>2, Case eP eP\<^sub>1 eP\<^sub>2, Case eV eV\<^sub>1 eV\<^sub>2 : \<tau>" |
   a_Pair: "\<lbrakk> \<Gamma> \<turnstile> e\<^sub>1, eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1; \<Gamma> \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Pair e\<^sub>1 e\<^sub>2, Pair eP\<^sub>1 eP\<^sub>2, Pair eV\<^sub>1 eV\<^sub>2 : Prod \<tau>\<^sub>1 \<tau>\<^sub>2" |
   a_Prj1: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Prj1 e, Prj1 eP, Prj1 eV : \<tau>\<^sub>1" |
   a_Prj2: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Prj2 e, Prj2 eP, Prj2 eV : \<tau>\<^sub>2" |
   a_Roll: "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile> e, eP, eV : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha> \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Roll e, Roll eP, Roll eV : Mu \<alpha> \<tau>" |
   a_Unroll: "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile> e, eP, eV : Mu \<alpha> \<tau> \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Unroll e, Unroll eP, Unroll eV : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>" |
   a_Auth: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : \<tau> \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Auth e, Auth eP, Auth eV : AuthT \<tau>" |
   a_Unauth: "\<lbrakk> \<Gamma> \<turnstile> e, eP, eV : AuthT \<tau> \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> Unauth e, Unauth eP, Unauth eV : \<tau>" |
   a_HashI: "\<lbrakk> {$$} \<turnstile> v, vP, \<lparr>vP\<rparr> : \<tau>; hash \<lparr>vP\<rparr> = h; value v; value vP \<rbrakk>
     \<Longrightarrow> \<Gamma> \<turnstile> v, Hashed h vP, Hash h : AuthT \<tau>"
 
 declare agree.intros[intro]
 
 equivariance agree
 nominal_inductive agree
   avoids a_Lam: x
        | a_Rec: x and y
        | a_Let: x
        | a_Roll: \<alpha>
        | a_Unroll: \<alpha>
   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 "\<Gamma> \<turnstile> e, eP, eV : \<tau>" "atom a \<sharp> \<Gamma>"
   shows   "atom a \<sharp> (e, eP, eV)"
   using assms proof (nominal_induct \<Gamma> e eP eV \<tau> avoiding: a rule: agree.strong_induct)
   case (a_Var \<Gamma> x \<tau>)
   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 "{$$} \<turnstile> e, eP, eV : \<tau>"
   shows   "{atom a} \<sharp>* {e, eP, eV}"
   using assms by (auto simp: fresh_Pair dest: agree_fresh_env_fresh_term)
 
 text \<open>Inversion rules for agreement.\<close>
 
 declare [[simproc del: alpha_lst]]
 
 lemma a_Lam_inv_I[elim]:
   assumes "\<Gamma> \<turnstile> (Lam x e'), eP, eV : (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)"
   and     "atom x \<sharp> \<Gamma>"
   obtains eP' eV' where "eP = Lam x eP'" "eV = Lam x eV'" "\<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e', eP', eV' : \<tau>\<^sub>2"
   using assms
 proof (atomize_elim, nominal_induct \<Gamma> "Lam x e'" eP eV "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" avoiding: x e' \<tau>\<^sub>1 \<tau>\<^sub>2 rule: agree.strong_induct)
   case (a_Lam x \<Gamma> \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2 y e')
   show ?case
   proof (intro exI conjI)
     from a_Lam show "Lam x eP = Lam y ((x \<leftrightarrow> y) \<bullet> 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 \<leftrightarrow> y) \<bullet> 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 "\<Gamma>(y $$:= \<tau>\<^sub>1) \<turnstile> e', (x \<leftrightarrow> y) \<bullet> eP, (x \<leftrightarrow> y) \<bullet> eV : \<tau>\<^sub>2"
       by (auto simp: perm_supp_eq Abs1_eq_iff(3)
         dest!: agree.eqvt[where p = "(x \<leftrightarrow> y)", of "\<Gamma>(x $$:= \<tau>\<^sub>1)"])
   qed
 qed
 
 lemma a_Lam_inv_P[elim]:
   assumes "{$$} \<turnstile> v, (Lam x vP'), vV : (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)"
   obtains v' vV' where "v = Lam x v'" "vV = Lam x vV'" "{$$}(x $$:= \<tau>\<^sub>1) \<turnstile> v', vP', vV' : \<tau>\<^sub>2"
-  using assms 
+  using assms
 proof (atomize_elim, nominal_induct "{$$}::tyenv" v "Lam x vP'" vV "Fun \<tau>\<^sub>1 \<tau>\<^sub>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' \<leftrightarrow> x) \<bullet> 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' \<leftrightarrow> x) \<bullet> 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 $$:= \<tau>\<^sub>1) \<turnstile> (x' \<leftrightarrow> x) \<bullet> e, vP', (x' \<leftrightarrow> x) \<bullet> eV : \<tau>\<^sub>2"
       by (auto simp: perm_supp_eq Abs1_eq_iff(3)
         dest!: agree.eqvt[where p = "(x' \<leftrightarrow> x)", of "{$$}(x' $$:= \<tau>\<^sub>1)"])
   qed
 qed
 
 lemma a_Lam_inv_V[elim]:
   assumes "{$$} \<turnstile> v, vP, (Lam x vV') : (Fun \<tau>\<^sub>1 \<tau>\<^sub>2)"
   obtains v' vP' where "v = Lam x v'" "vP = Lam x vP'" "{$$}(x $$:= \<tau>\<^sub>1) \<turnstile> v', vP', vV' : \<tau>\<^sub>2"
   using assms
 proof (atomize_elim, nominal_induct "{$$}::tyenv" v vP "Lam x vV'" "Fun \<tau>\<^sub>1 \<tau>\<^sub>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' \<leftrightarrow> x) \<bullet> 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' \<leftrightarrow> x) \<bullet> 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 $$:= \<tau>\<^sub>1) \<turnstile> (x' \<leftrightarrow> x) \<bullet> e, (x' \<leftrightarrow> x) \<bullet> eP, vV' : \<tau>\<^sub>2"
       by (auto simp: perm_supp_eq Abs1_eq_iff(3)
         dest!: agree.eqvt[where p = "(x' \<leftrightarrow> x)", of "{$$}(x' $$:= \<tau>\<^sub>1)"])
   qed
 qed
 
 lemma a_Rec_inv_I[elim]:
   assumes "\<Gamma> \<turnstile> Rec x e, eP, eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   and     "atom x \<sharp> \<Gamma>"
   obtains y e' eP' eV'
   where "e = Lam y e'" "eP = Rec x (Lam y eP')" "eV = Rec x (Lam y eV')" "atom y \<sharp> (\<Gamma>,x)"
         "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e', Lam y eP', Lam y eV' : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   using assms
 proof (atomize_elim, nominal_induct \<Gamma> "Rec x e" eP eV "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" avoiding: x e rule: agree.strong_induct)
   case (a_Rec x' \<Gamma> 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 \<leftrightarrow> y) \<bullet> 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' \<leftrightarrow> x) \<bullet> 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' \<leftrightarrow> x) \<bullet> 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 \<sharp> (\<Gamma>, x)"
         by simp
       from Lam(1-3,5-11,13) have "(x' \<leftrightarrow> x) \<bullet> e' = (z \<leftrightarrow> y) \<bullet> 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 "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>
         Lam y ((z \<leftrightarrow> y) \<bullet> ee), Lam y ((x' \<leftrightarrow> x) \<bullet> eP), Lam y ((x' \<leftrightarrow> x) \<bullet> eV) : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
         by (elim agree.eqvt[of _ "Lam y e'" _ _ _ "(x' \<leftrightarrow> 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 "\<Gamma> \<turnstile> e, Rec x eP, eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   and     "atom x \<sharp> \<Gamma>"
   obtains y e' eP' eV'
   where "e = Rec x (Lam y e')" "eP = Lam y eP'" "eV = Rec x (Lam y eV')" "atom y \<sharp> (\<Gamma>,x)"
         "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e', Lam y eP', Lam y eV' : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   using assms
 proof (atomize_elim,nominal_induct \<Gamma> e "Rec x eP" eV "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" avoiding: x eP rule: agree.strong_induct)
   case (a_Rec x \<Gamma> 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 \<leftrightarrow> x') \<bullet> 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 \<leftrightarrow> x') \<bullet> 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 \<leftrightarrow> x') \<bullet> 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 \<sharp> (\<Gamma>, x')"
         by simp
       with Lam(1-2,7,9,11-12,15) show "\<Gamma>(x' $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>
         Lam y ((x \<leftrightarrow> x') \<bullet> e), Lam y ((x \<leftrightarrow> x') \<bullet> eP), Lam y ((x \<leftrightarrow> x') \<bullet> eV) : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
         by (elim agree.eqvt[of _ "Lam y _" _ _ _ "(x' \<leftrightarrow> 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 "\<Gamma> \<turnstile> e, eP, Rec x eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
     and     "atom x \<sharp> \<Gamma>"
   obtains y e' eP' eV'
   where "e = Rec x (Lam y e')" "eP = Rec x (Lam y eP')" "eV = Lam y eV'" "atom y \<sharp> (\<Gamma>,x)"
     "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e', Lam y eP', Lam y eV' : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   using assms
 proof (atomize_elim, nominal_induct \<Gamma> e eP "Rec x eV" "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" avoiding: x eV rule: agree.strong_induct)
   case (a_Rec x \<Gamma> 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 \<leftrightarrow> x') \<bullet> 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 \<leftrightarrow> x') \<bullet> 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 \<leftrightarrow> x') \<bullet> 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 \<sharp> (\<Gamma>, x')"
         by simp
       with Lam(1-2,7,9,11-12,15) show "\<Gamma>(x' $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>
         Lam y ((x \<leftrightarrow> x') \<bullet> e), Lam y ((x \<leftrightarrow> x') \<bullet> eP), Lam y ((x \<leftrightarrow> x') \<bullet> eV) : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
         by (elim agree.eqvt[of _ "Lam y _" _ _ _ "(x' \<leftrightarrow> 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]: "\<Gamma> \<turnstile> Inj1 e, eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Inj1_inv_P[elim]: "\<Gamma> \<turnstile> e, Inj1 eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Inj1_inv_V[elim]: "\<Gamma> \<turnstile> e, eP, Inj1 eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 
 inductive_cases a_Inj2_inv_I[elim]: "\<Gamma> \<turnstile> Inj2 e, eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Inj2_inv_P[elim]: "\<Gamma> \<turnstile> e, Inj2 eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Inj2_inv_V[elim]: "\<Gamma> \<turnstile> e, eP, Inj2 eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 
 inductive_cases a_Pair_inv_I[elim]: "\<Gamma> \<turnstile> Pair e\<^sub>1 e\<^sub>2, eP, eV : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Pair_inv_P[elim]: "\<Gamma> \<turnstile> e, Pair eP\<^sub>1 eP\<^sub>2, eV : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
 
 lemma a_Roll_inv_I[elim]:
   assumes "\<Gamma> \<turnstile> Roll e', eP, eV : Mu \<alpha> \<tau>"
   obtains eP' eV'
   where "eP = Roll eP'" "eV = Roll eV'" "\<Gamma> \<turnstile> e', eP', eV' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
   using assms
   by (nominal_induct \<Gamma> "Roll e'" eP eV "Mu \<alpha> \<tau>" avoiding: \<alpha> \<tau> rule: agree.strong_induct)
      (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)
 
 lemma a_Roll_inv_P[elim]:
   assumes "\<Gamma> \<turnstile> e, Roll eP', eV : Mu \<alpha> \<tau>"
   obtains e' eV'
   where "e = Roll e'" "eV = Roll eV'" "\<Gamma> \<turnstile> e', eP', eV' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
   using assms
   by (nominal_induct \<Gamma> e "Roll eP'" eV "Mu \<alpha> \<tau>" avoiding: \<alpha> \<tau> rule: agree.strong_induct)
      (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)
 
 lemma a_Roll_inv_V[elim]:
   assumes "\<Gamma> \<turnstile> e, eP, Roll eV' : Mu \<alpha> \<tau>"
   obtains e' eP'
   where "e = Roll e'" "eP = Roll eP'" "\<Gamma> \<turnstile> e', eP', eV' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
   using assms
   by (nominal_induct \<Gamma> e eP "Roll eV'" "Mu \<alpha> \<tau>" avoiding: \<alpha> \<tau> rule: agree.strong_induct)
      (simp add: Abs1_eq(3) Abs_lst_eq_flipI subst_type_perm_eq)
 
 inductive_cases a_HashI_inv[elim]: "\<Gamma> \<turnstile> v, Hashed (hash \<lparr>vP\<rparr>) vP, Hash (hash \<lparr>vP\<rparr>) : AuthT \<tau>"
 
 text \<open>Inversion on types for agreement.\<close>
 
 lemma a_AuthT_value_inv:
   assumes "{$$} \<turnstile> v, vP, vV : AuthT \<tau>"
   and     "value v" "value vP" "value vV"
   obtains vP' where "vP = Hashed (hash \<lparr>vP'\<rparr>) vP'" "vV = Hash (hash \<lparr>vP'\<rparr>)" "value vP'"
   using assms by (atomize_elim, induct "{$$}::tyenv" v vP vV "AuthT \<tau>" rule: agree.induct) simp_all
 
 inductive_cases a_Mu_inv[elim]: "\<Gamma> \<turnstile> e, eP, eV : Mu \<alpha> \<tau>"
 inductive_cases a_Sum_inv[elim]: "\<Gamma> \<turnstile> e, eP, eV : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Prod_inv[elim]: "\<Gamma> \<turnstile> e, eP, eV : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases a_Fun_inv[elim]: "\<Gamma> \<turnstile> e, eP, eV : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
 
 declare [[simproc add: alpha_lst]]
 
 lemma agree_weakening_1:
   assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>" "atom y \<sharp> e" "atom y \<sharp> eP" "atom y \<sharp> eV"
   shows   "\<Gamma>(y $$:= \<tau>') \<turnstile> e, eP, eV : \<tau>"
 using assms proof (nominal_induct \<Gamma> e eP eV \<tau> avoiding: y \<tau>' rule: agree.strong_induct)
   case (a_Lam x \<Gamma> \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2)
   then show ?case
-    by (force simp add: fresh_at_base fresh_fmap_update fmap_reorder_neq_updates)
+    by (force simp add: fresh_at_base fresh_fmap_update fmupd_reorder_neq)
 next
   case (a_App v\<^sub>1 v\<^sub>2 vP\<^sub>1 vP\<^sub>2 vV\<^sub>1 vV\<^sub>2 \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
     using term.fresh(9) by blast
 next
   case (a_Let x \<Gamma> e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   then show ?case
-    by (auto simp add: fresh_at_base fresh_Pair fresh_fmap_update fmap_reorder_neq_updates[of y x]
+    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 \<Gamma> z \<tau>\<^sub>1 \<tau>\<^sub>2 e eP eV)
   then show ?case
-    by (auto simp add: fresh_at_base fresh_Pair fresh_fmap_update fmap_reorder_neq_updates[of y x]
+    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\<^sub>1 v\<^sub>2 vP vP\<^sub>1 vP\<^sub>2 vV vV\<^sub>1 vV\<^sub>2 \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2 \<tau>)
   then show ?case
     by (fastforce simp: fresh_at_base)
 next
   case (a_Prj1 v vP vV \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
     by (fastforce simp: fresh_at_base)
 next
   case (a_Prj2 v vP vV \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
     by (fastforce simp: fresh_at_base)
 qed (auto simp: fresh_fmap_update)
 
 lemma agree_weakening_2:
   assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>" "atom y \<sharp> \<Gamma>"
   shows   "\<Gamma>(y $$:= \<tau>') \<turnstile> e, eP, eV : \<tau>"
 proof -
   from assms have "{atom y} \<sharp>* {e, eP, eV}" by (auto simp: fresh_Pair dest: agree_fresh_env_fresh_term)
   with assms show "\<Gamma>(y $$:= \<tau>') \<turnstile> e, eP, eV : \<tau>" by (simp add: agree_weakening_1)
 qed
 
 lemma agree_weakening_env:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   shows   "\<Gamma> \<turnstile> e, eP, eV : \<tau>"
 using assms proof (induct \<Gamma>)
   case fmempty
   then show ?case by assumption
 next
   case (fmupd x y \<Gamma>)
   then show ?case
     by (simp add: fresh_tyenv_None agree_weakening_2)
 qed
 
 (*<*)
 end
 (*>*)
\ No newline at end of file
diff --git a/thys/LambdaAuth/FMap_Lemmas.thy b/thys/LambdaAuth/FMap_Lemmas.thy
--- a/thys/LambdaAuth/FMap_Lemmas.thy
+++ b/thys/LambdaAuth/FMap_Lemmas.thy
@@ -1,197 +1,174 @@
 (* Author: Matthias Brun,   ETH Zürich, 2019 *)
 (* Author: Dmitriy Traytel, ETH Zürich, 2019 *)
 
 (*<*)
 theory FMap_Lemmas
   imports "HOL-Library.Finite_Map"
           Nominal2_Lemmas
 begin
 (*>*)
 
 text \<open>Nominal setup for finite maps.\<close>
 
 abbreviation fmap_update ("_'(_ $$:= _')" [1000,0,0] 1000)  where "fmap_update \<Gamma> x \<tau> \<equiv> fmupd x \<tau> \<Gamma>"
 notation fmlookup (infixl "$$" 999)
 notation fmempty ("{$$}")
 
 instantiation fmap :: (pt, pt) pt
 begin
 
 unbundle fmap.lifting
 
 lift_definition
   permute_fmap :: "perm \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
   is
   "permute :: perm \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"
 proof -
   fix p and f :: "'a \<rightharpoonup> 'b"
   assume "finite (dom f)"
   then show "finite (dom (p \<bullet> f))"
   proof (rule finite_surj[of _ _ "permute p"]; unfold dom_def, safe)
     fix x y
     assume some: "(p \<bullet> f) x = Some y"
     show "x \<in> permute p ` {a. f a \<noteq> None}"
     proof (rule image_eqI[of _ _ "- p \<bullet> x"])
       from some show "- p \<bullet> x \<in> {a. f a \<noteq> None}"
         by (auto simp: permute_self pemute_minus_self
           dest: arg_cong[of _ _ "permute (- p)"] intro!: exI[of _ "- p \<bullet> y"])
     qed (simp only: permute_minus_cancel)
   qed
 qed
 
 instance
 proof
   fix x :: "('a, 'b) fmap"
   show "0 \<bullet> x = x"
     by transfer simp
 next
   fix p q and x :: "('a, 'b) fmap"
   show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"
     by transfer simp
 qed
 
 end
 
 lemma fmempty_eqvt[eqvt]:
   shows "(p \<bullet> {$$}) = {$$}"
   by transfer simp
 
 lemma fmap_update_eqvt[eqvt]:
   shows "(p \<bullet> f(a $$:= b)) = (p \<bullet> f)((p \<bullet> a) $$:= (p \<bullet> b))"
   by transfer (simp add: map_upd_def)
 
 lemma fmap_apply_eqvt[eqvt]:
   shows "(p \<bullet> (f $$ b)) = (p \<bullet> f) $$ (p \<bullet> b)"
   by transfer simp
 
 lemma fresh_fmempty[simp]:
   shows "a \<sharp> {$$}"
   unfolding fresh_def supp_def
   by transfer simp
 
 lemma fresh_fmap_update:
   shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> f(x $$:= y)"
   unfolding fresh_conv_MOST
   by (elim MOST_rev_mp) simp
 
 lemma supp_fmempty[simp]:
   shows "supp {$$} = {}"
   by (simp add: supp_def)
 
 lemma supp_fmap_update:
   shows "supp (f(x $$:= y)) \<subseteq> supp(f, x, y)"
   using fresh_fmap_update
   by (auto simp: fresh_def supp_Pair)
 
 instance fmap :: (fs, fs) fs
 proof
   fix x :: "('a, 'b) fmap"
   show "finite (supp x)"
     by (induct x rule: fmap_induct)
       (simp_all add: supp_Pair finite_supp finite_subset[OF supp_fmap_update])
 qed
 
-lemma fmap_reorder_neq_updates:
-  assumes "a \<noteq> b"
-  shows   "\<Gamma>(a $$:= x)(b $$:= y) = \<Gamma>(b $$:= y)(a $$:= x)"
-  using assms by transfer (auto simp: map_upd_def)
-
-lemma fmap_upd_upd[simp]: "\<Gamma>(x $$:= y)(x $$:= z) = \<Gamma>(x $$:= z)"
-  by transfer (simp add: map_upd_def)
-
 lemma fresh_transfer[transfer_rule]:
   "((=) ===> pcr_fmap (=) (=) ===> (=)) fresh fresh"
   unfolding fresh_def supp_def rel_fun_def pcr_fmap_def cr_fmap_def simp_thms
     option.rel_eq fun_eq_iff[symmetric]
   by (auto elim!: finite_subset[rotated] simp: fmap_ext)
 
-lemma fmmap_fmupd: "fmmap f F(x $$:= y) = (fmmap f F)(x $$:= f y)"
-  by transfer (auto simp: fun_eq_iff map_upd_def)
-
 lemma fmmap_eqvt[eqvt]: "p \<bullet> (fmmap f F) = fmmap (p \<bullet> f) (p \<bullet> F)"
   by (induct F arbitrary: f rule: fmap_induct) (auto simp add: fmap_update_eqvt fmmap_fmupd)
 
 lemma fmap_freshness_lemma:
   fixes h :: "('a::at,'b::pt) fmap"
   assumes a: "\<exists>a. atom a \<sharp> (h, h $$ a)"
   shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h $$ a = x"
   using assms unfolding fresh_Pair
   by transfer (simp add: fresh_Pair freshness_lemma)
 
 lemma fmap_freshness_lemma_unique:
   fixes h :: "('a::at,'b::pt) fmap"
   assumes "\<exists>a. atom a \<sharp> (h, h $$ a)"
   shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h $$ a = x"
   using assms unfolding fresh_Pair
   by transfer (rule freshness_lemma_unique, auto simp: fresh_Pair)
 
 lemma fmdrop_fset_fmupd[simp]:
   "(fmdrop_fset A f)(x $$:= y) = fmdrop_fset (A |-| {|x|}) f(x $$:= y)"
   including fmap.lifting fset.lifting
   by transfer (auto simp: map_drop_set_def map_upd_def map_filter_def)
 
 lemma fresh_fset_fminus:
   assumes "atom x \<sharp> A"
   shows   "A |-| {|x|} = A"
   using assms by (induct A) (simp_all add: finsert_fminus_if fresh_finsert)
 
 lemma fresh_fun_app:
   shows "atom x \<sharp> F \<Longrightarrow> x \<noteq> y \<Longrightarrow> F y = Some a \<Longrightarrow> atom x \<sharp> a"
   using supp_fun_app[of F y]
   by (auto simp: fresh_def supp_Some atom_not_fresh_eq)
 
 lemma fresh_fmap_fresh_Some:
   "atom x \<sharp> F \<Longrightarrow> x \<noteq> y \<Longrightarrow> F $$ y = Some a \<Longrightarrow> atom x \<sharp> a"
   including fmap.lifting
   by (transfer) (auto elim: fresh_fun_app)
 
 lemma fmdrop_eqvt: "p \<bullet> fmdrop x F = fmdrop (p \<bullet> x) (p \<bullet> F)"
   by transfer (auto simp: map_drop_def map_filter_def)
 
 lemma fmfilter_eqvt: "p \<bullet> fmfilter Q F = fmfilter (p \<bullet> Q) (p \<bullet> F)"
   by transfer (auto simp: map_filter_def)
 
-lemma fmdrop_fmupd: "fmdrop x F(y $$:= z) = (if x = y then fmdrop x F else (fmdrop x F)(y $$:= z))"
-  by transfer (auto simp: map_drop_def map_filter_def map_upd_def)
-
 lemma fmdrop_eq_iff:
   "fmdrop x B = fmdrop y B \<longleftrightarrow> x = y \<or> (x \<notin> fmdom' B \<and> y \<notin> fmdom' B)"
   by transfer (auto simp: map_drop_def map_filter_def fun_eq_iff, metis)
 
-lemma fmdrop_idle: "x \<notin> fmdom' B \<Longrightarrow> fmdrop x B = B"
-  by transfer (auto simp: map_drop_def map_filter_def)
-
-lemma fmdrop_fmupd_same: "fmdrop x B(x $$:= y) = fmdrop x B"
-  by transfer (auto simp: map_drop_def map_filter_def map_upd_def)
-
 lemma fresh_fun_upd:
   shows "\<lbrakk>a \<sharp> f; a \<sharp> x; a \<sharp> y\<rbrakk> \<Longrightarrow> a \<sharp> f(x := y)"
   unfolding fresh_conv_MOST by (elim MOST_rev_mp) simp
 
 lemma supp_fun_upd:
   shows "supp (f(x := y)) \<subseteq> supp(f, x, y)"
   using fresh_fun_upd by (auto simp: fresh_def supp_Pair)
 
 lemma map_drop_fun_upd: "map_drop x F = F(x := None)"
   unfolding map_drop_def map_filter_def by auto
 
 lemma fresh_fmdrop_in_fmdom: "\<lbrakk> x \<in> fmdom' B; y \<sharp> B; y \<sharp> x \<rbrakk> \<Longrightarrow> y \<sharp> fmdrop x B"
   by transfer (auto simp: map_drop_fun_upd fresh_None intro!: fresh_fun_upd)
 
 lemma fresh_fmdrop:
   assumes "x \<sharp> B" "x \<sharp> y"
   shows   "x \<sharp> fmdrop y B"
-  using assms by (cases "y \<in> fmdom' B") (auto dest!: fresh_fmdrop_in_fmdom simp: fmdrop_idle)
+  using assms by (cases "y \<in> fmdom' B") (auto dest!: fresh_fmdrop_in_fmdom simp: fmdrop_idle')
 
 lemma fresh_fmdrop_fset:
   fixes x :: atom and A :: "(_ :: at_base) fset"
   assumes "x \<sharp> A" "x \<sharp> B"
   shows   "x \<sharp> fmdrop_fset A B"
   using assms(1) by (induct A) (auto simp: fresh_fmdrop assms(2) fresh_finsert)
 
-lemma fmdrop_fset_fmdom[simp]: "fmdrop_fset (fmdom A) A = {$$}"
-  by (induct A) (simp_all add: fmap_ext fmdom_notD)
-
 (*<*)
 end
 (*>*)
\ No newline at end of file
diff --git a/thys/LambdaAuth/Results.thy b/thys/LambdaAuth/Results.thy
--- a/thys/LambdaAuth/Results.thy
+++ b/thys/LambdaAuth/Results.thy
@@ -1,1557 +1,1557 @@
 (* Author: Matthias Brun,   ETH Zürich, 2019 *)
 (* Author: Dmitriy Traytel, ETH Zürich, 2019 *)
 
 section \<open>Formalization of Miller et al.'s~\cite{adsg} Main Results\<close>
 
 (*<*)
 theory Results
   imports Agreement
 begin
 (*>*)
 
 lemma judge_imp_agree:
   assumes "\<Gamma> \<turnstile> e : \<tau>"
   shows   "\<Gamma> \<turnstile> e, e, e : \<tau>"
   using assms by (induct \<Gamma> e \<tau>) (auto simp: fresh_Pair)
 
 subsection \<open>Lemma 2.1\<close>
 
 lemma lemma2_1:
   assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>"
   shows   "\<lparr>eP\<rparr> = eV"
   using assms by (induct \<Gamma> e eP eV \<tau>) (simp_all add: Abs1_eq)
 
 subsection \<open>Counterexample to Lemma 2.2\<close>
 
 lemma lemma2_2_false:
   fixes x :: var
   assumes "\<And>\<Gamma> e eP eV \<tau> eP' eV'. \<lbrakk> \<Gamma> \<turnstile> e, eP, eV : \<tau>; \<Gamma> \<turnstile> e, eP', eV' : \<tau> \<rbrakk> \<Longrightarrow> eP = eP' \<and> eV = eV'"
   shows False
 proof -
   have a1: "{$$} \<turnstile> Prj1 (Pair Unit Unit), Prj1 (Pair Unit Unit), Prj1 (Pair Unit Unit) : One"
     by fastforce
   also have a2: "{$$} \<turnstile> Prj1 (Pair Unit Unit), Prj1 (Pair Unit (Hashed (hash Unit) Unit)), Prj1 (Pair Unit (Hash (hash Unit))) : One"
     by fastforce
   from a1 a2 have "Prj1 (Pair Unit Unit) = Prj1 (Pair Unit (Hash (hash Unit)))"
     by (auto dest: assms)
   then show False
     by simp
 qed
 
 lemma smallstep_ideal_deterministic:
   "\<lless>[], t\<ggreater> I\<rightarrow> \<lless>[], u\<ggreater> \<Longrightarrow> \<lless>[], t\<ggreater> I\<rightarrow> \<lless>[], u'\<ggreater> \<Longrightarrow> u = u'"
 proof (nominal_induct "[]::proofstream" t I "[]::proofstream" u avoiding: u' rule: smallstep.strong_induct)
   case (s_App1 e\<^sub>1 e\<^sub>1' e\<^sub>2)
   from s_App1(3) value_no_step[OF s_App1(1)] show ?case
     by (auto dest!: s_App1(2))
 next
   case (s_App2 v\<^sub>1 e\<^sub>2 e\<^sub>2')
   from s_App2(4) value_no_step[OF s_App2(2)] value_no_step[OF _ s_App2(1)] show ?case
     by (force dest!: s_App2(3))
 next
   case (s_AppLam v x e)
   from  s_AppLam(5,1,3) value_no_step[OF _ s_AppLam(2)] show ?case
   proof (cases rule: s_App_inv)
     case (AppLam y e')
     obtain z :: var where "atom z \<sharp> (x, e, y, e')"
       by (metis obtain_fresh)
     with AppLam s_AppLam(1,3) show ?thesis
       by (auto simp: fresh_Pair intro: box_equals[OF _ subst_term_perm[symmetric, of z] subst_term_perm[symmetric, of z]])
   qed (auto dest: value_no_step)
 next
   case (s_AppRec v x e)
   from s_AppRec(5,1,3) value_no_step[OF _ s_AppRec(2)] show ?case
   proof (cases rule: s_App_inv)
     case (AppRec y e')
     obtain z :: var where "atom z \<sharp> (x, e, y, e')"
       by (metis obtain_fresh)
     with AppRec(1-4) AppRec(5)[simplified] s_AppRec(1,3) show ?thesis
       by (auto simp: fresh_Pair AppRec(5)
           intro: box_equals[OF _ subst_term_perm[symmetric, of z] subst_term_perm[symmetric, of z]])
   qed (auto dest: value_no_step)
 next
   case (s_Let1 x e\<^sub>1 e\<^sub>1' e\<^sub>2)
   from s_Let1(1,2,3,8) value_no_step[OF s_Let1(6)] show ?case
     by (auto dest: s_Let1(7))
 next
   case (s_Let2 v x e)
   from s_Let2(1,3,5) value_no_step[OF _ s_Let2(2)] show ?case
     by force
 next
   case (s_Inj1 e e')
   from s_Inj1(2,3) show ?case
     by auto
 next
   case (s_Inj2 e e')
   from s_Inj2(2,3) show ?case
     by auto
 next
   case (s_Case e e' e\<^sub>1 e\<^sub>2)
   from s_Case(2,3) value_no_step[OF s_Case(1)] show ?case
     by auto
 next
   case (s_Pair1 e\<^sub>1 e\<^sub>1' e\<^sub>2)
   from s_Pair1(2,3) value_no_step[OF s_Pair1(1)] show ?case
     by auto
 next
   case (s_Pair2 v\<^sub>1 e\<^sub>2 e\<^sub>2')
   from s_Pair2(3,4) value_no_step[OF _ s_Pair2(1)] value_no_step[OF s_Pair2(2)] show ?case
     by force
 next
   case (s_Prj1 e e')
   from s_Prj1(2,3) value_no_step[OF s_Prj1(1)] show ?case
     by auto
 next
   case (s_Prj2 e e')
   from s_Prj2(2,3) value_no_step[OF s_Prj2(1)] show ?case
     by auto
 next
   case (s_Unroll e e')
   from s_Unroll(2,3) value_no_step[OF s_Unroll(1)] show ?case
     by auto
 next
   case (s_Roll e e')
   from s_Roll(2,3) show ?case
     by auto
 next
   case (s_Auth e e')
   from s_Auth(2,3) value_no_step[OF s_Auth(1)] show ?case
     by auto
 next
   case (s_Unauth e e')
   from s_Unauth(2,3) value_no_step[OF s_Unauth(1)] show ?case
     by auto
 qed (auto 0 3 dest: value_no_step)
 
 lemma smallsteps_ideal_deterministic:
   "\<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], u\<ggreater> \<Longrightarrow> \<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], u'\<ggreater> \<Longrightarrow> u = u'"
 proof (induct "[]::proofstream" t I i "[]::proofstream" u arbitrary: u' rule: smallsteps.induct)
   case (s_Tr e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 e\<^sub>3)
   from s_Tr(4) show ?case
   proof (cases rule: smallsteps.cases)
     case _: (s_Tr i \<pi>\<^sub>4 e\<^sub>4)
     with s_Tr(1,3) s_Tr(2)[of e\<^sub>4] show ?thesis
       using smallstepsI_ps_emptyD(2)[of e\<^sub>1 i \<pi>\<^sub>4 e\<^sub>4] smallstepI_ps_eq[of \<pi>\<^sub>2 e\<^sub>2 "[]" e\<^sub>3]
       by (auto intro!: smallstep_ideal_deterministic elim!: smallstepI_ps_emptyD)
   qed simp
 qed auto
 
 subsection \<open>Lemma 2.3\<close>
 
 lemma lemma2_3:
   assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>"
   shows   "erase_env \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>"
   using assms unfolding erase_env_def
 proof (nominal_induct \<Gamma> e eP eV \<tau> rule: agree.strong_induct)
   case (a_HashI v vP \<tau> h \<Gamma>)
   then show ?case
     by (induct \<Gamma>) (auto simp: judge_weak_weakening_2 fmmap_fmupd judge_weak_fresh_env_fresh_term fresh_tyenv_None)
 qed (simp_all add: fresh_fmmap_erase_fresh fmmap_fmupd judge_weak_fresh_env_fresh_term)
 
 subsection \<open>Lemma 2.4\<close>
 
 lemma lemma2_4[dest]:
   assumes "\<Gamma> \<turnstile> e, eP, eV : \<tau>"
   shows   "value e \<and> value eP \<and> value eV \<or> \<not> value e \<and> \<not> value eP \<and> \<not> value eV"
   using assms by (nominal_induct \<Gamma> e eP eV \<tau> rule: agree.strong_induct) auto
 
 subsection \<open>Lemma 3\<close>
 
 lemma lemma3_general:
   fixes \<Gamma> :: tyenv and vs vPs vVs :: tenv
   assumes "\<Gamma> \<turnstile> e : \<tau>" "A |\<subseteq>| fmdom \<Gamma>"
   and     "fmdom vs = A" "fmdom vPs = A" "fmdom vVs = A"
   and     "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>\<tau>' v vP h.
     \<Gamma> $$ x = Some (AuthT \<tau>') \<and>
     vs $$ x = Some v \<and>
    vPs $$ x = Some (Hashed h vP) \<and>
    vVs $$ x = Some (Hash h) \<and>
    {$$} \<turnstile> v, Hashed h vP, Hash h : (AuthT \<tau>'))"
   shows  "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : \<tau>"
   using assms
 proof (nominal_induct \<Gamma> e \<tau> avoiding: vs vPs vVs A rule: judge.strong_induct)
   case (j_Unit \<Gamma>)
   then show ?case
     by auto
 next
   case (j_Var \<Gamma> x \<tau>)
   with j_Var show ?case
   proof (cases "x |\<in>| A")
     case True
     with j_Var show ?thesis
       by (fastforce dest!: spec[of _ x] intro: agree_weakening_env)
   next
     case False
     with j_Var show ?thesis
       by (auto simp add: a_Var dest!: fmdomI split: option.splits)
   qed
 next
   case (j_Lam x \<Gamma> \<tau>\<^sub>1 e \<tau>\<^sub>2)
   from j_Lam(4) have [simp]: "A |-| {|x|} = A"
     by (simp add: fresh_fset_fminus)
   from j_Lam(5,8-) have "fmdrop_fset A \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : \<tau>\<^sub>2"
     by (intro j_Lam(7)[of A vs vPs vVs]) (auto simp: fresh_tyenv_None)
   with j_Lam(1-5) show ?case
     by (auto simp: fresh_fmdrop_fset)
 next
   case (j_App \<Gamma> e \<tau>\<^sub>1 \<tau>\<^sub>2 e')
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
     and "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e' vs, psubst_term e' vPs, psubst_term e' vVs : \<tau>\<^sub>1"
     by simp_all
   then show ?case
     by auto
 next
   case (j_Let x \<Gamma> e\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 \<tau>\<^sub>2)
   from j_Let(4) have [simp]: "A |-| {|x|} = A"
     by (simp add: fresh_fset_fminus)
   from j_Let(8,11-) have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e\<^sub>1 vs, psubst_term e\<^sub>1 vPs, psubst_term e\<^sub>1 vVs : \<tau>\<^sub>1"
     by simp
   moreover from j_Let(4,5,11-) have "fmdrop_fset A \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> psubst_term e\<^sub>2 vs, psubst_term e\<^sub>2 vPs, psubst_term e\<^sub>2 vVs : \<tau>\<^sub>2"
     by (intro j_Let(10)) (auto simp: fresh_tyenv_None)
   ultimately show ?case using j_Let(1-6)
     by (auto simp: fresh_fmdrop_fset fresh_Pair fresh_psubst)
 next
   case (j_Rec x \<Gamma> y \<tau>\<^sub>1 \<tau>\<^sub>2 e')
   from j_Rec(4) have [simp]: "A |-| {|x|} = A"
     by (simp add: fresh_fset_fminus)
   from j_Rec(9,14-) have "fmdrop_fset A \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> psubst_term (Lam y e') vs, psubst_term (Lam y e') vPs, psubst_term (Lam y e') vVs : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
     by (intro j_Rec(13)) (auto simp: fresh_tyenv_None)
   with j_Rec(1-11) show ?case
     by (auto simp: fresh_fmdrop_fset)
 next
   case (j_Case \<Gamma> e \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 \<tau> e\<^sub>2)
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e  vs, psubst_term e  vPs, psubst_term e  vVs : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
     and "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e\<^sub>1 vs, psubst_term e\<^sub>1 vPs, psubst_term e\<^sub>1 vVs : Fun \<tau>\<^sub>1 \<tau>"
     and "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e\<^sub>2 vs, psubst_term e\<^sub>2 vPs, psubst_term e\<^sub>2 vVs : Fun \<tau>\<^sub>2 \<tau>"
     by simp_all
   then show ?case
     by auto
 next
   case (j_Prj1 \<Gamma> e \<tau>\<^sub>1 \<tau>\<^sub>2)
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
     by simp
   then show ?case
     by auto
 next
   case (j_Prj2 \<Gamma> e \<tau>\<^sub>1 \<tau>\<^sub>2)
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
     by simp
   then show ?case
     by auto
 next
   case (j_Roll \<alpha> \<Gamma> e \<tau>)
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
     by simp
   with j_Roll(4,5) show ?case
     by (auto simp: fresh_fmdrop_fset)
 next
   case (j_Unroll \<alpha> \<Gamma> e \<tau>)
   then have "fmdrop_fset A \<Gamma> \<turnstile> psubst_term e vs, psubst_term e vPs, psubst_term e vVs : Mu \<alpha> \<tau>"
     by simp
   with j_Unroll(4,5) show ?case
     by (auto simp: fresh_fmdrop_fset)
 qed auto
 
 lemmas lemma3 = lemma3_general[where A = "fmdom \<Gamma>" and \<Gamma> = \<Gamma>, simplified] for \<Gamma>
 
 subsection \<open>Lemma 4\<close>
 
 lemma lemma4:
   assumes "\<Gamma>(x $$:= \<tau>') \<turnstile> e, eP, eV : \<tau>"
   and     "{$$} \<turnstile> v, vP, vV : \<tau>'"
   and     "value v" "value vP" "value vV"
   shows   "\<Gamma> \<turnstile> e[v / x], eP[vP / x], eV[vV / x] : \<tau>"
   using assms
 proof (nominal_induct "\<Gamma>(x $$:= \<tau>')" e eP eV \<tau> avoiding: x \<Gamma> rule: agree.strong_induct)
   case a_Unit
   then show ?case by auto
 next
   case (a_Var y \<tau>)
   then show ?case
   proof (induct \<Gamma>)
     case fmempty
     then show ?case by (metis agree.a_Var fmupd_lookup option.sel subst_term.simps(2))
   next
     case (fmupd x y \<Gamma>)
     then show ?case
       using agree_weakening_2 fresh_tyenv_None by auto
   qed
 next
   case (a_Lam y \<tau>\<^sub>1 e eP eV \<tau>\<^sub>2)
   from a_Lam(1,2,5,6,7-) show ?case
-    using agree_empty_fresh by (auto simp: fmap_reorder_neq_updates)
+    using agree_empty_fresh by (auto simp: fmupd_reorder_neq)
 next
   case (a_App v\<^sub>1 v\<^sub>2 v\<^sub>1P v\<^sub>2P v\<^sub>1V v\<^sub>2V \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_App(5-) show ?case
     by (auto intro: a_App(2,4))
 next
   case (a_Let y e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   then show ?case
-    using agree_empty_fresh by (auto simp: fmap_reorder_neq_updates intro!: agree.a_Let[where x=y])
+    using agree_empty_fresh by (auto simp: fmupd_reorder_neq intro!: agree.a_Let[where x=y])
 next
   case (a_Rec y z \<tau>\<^sub>1 \<tau>\<^sub>2 e eP eV)
   from a_Rec(10) have "\<forall>a::var. atom a \<sharp> v" "\<forall>a::var. atom a \<sharp> vP" "\<forall>a::var. atom a \<sharp> vV"
     by auto
   with a_Rec(1-8,10-) show ?case
-    using a_Rec(9)[OF fmap_reorder_neq_updates]
-    by (auto simp: fmap_reorder_neq_updates intro!: agree.a_Rec[where x=y])
+    using a_Rec(9)[OF fmupd_reorder_neq]
+    by (auto simp: fmupd_reorder_neq intro!: agree.a_Rec[where x=y])
 next
   case (a_Case v v\<^sub>1 v\<^sub>2 vP v\<^sub>1P v\<^sub>2P vV v\<^sub>1V v\<^sub>2V \<tau>\<^sub>1 \<tau>\<^sub>2 \<tau>)
   from a_Case(7-) show ?case
     by (auto intro: a_Case(2,4,6))
 next
   case (a_HashI v vP \<tau> h)
   then have "atom x \<sharp> v" "atom x \<sharp> vP" by auto
   with a_HashI show ?case by auto
 qed auto
 
 subsection \<open>Lemma 5:  Single-Step Correctness\<close>
 
 lemma lemma5:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater>"
   obtains eP' eV' \<pi>
   where   "{$$} \<turnstile> e', eP', eV' : \<tau>" "\<forall>\<pi>\<^sub>P. \<lless> \<pi>\<^sub>P, eP \<ggreater> P\<rightarrow> \<lless> \<pi>\<^sub>P @ \<pi>, eP' \<ggreater>" "\<forall>\<pi>'. \<lless> \<pi> @ \<pi>', eV \<ggreater> V\<rightarrow> \<lless> \<pi>', eV' \<ggreater>"
 proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV \<tau> avoiding: e' rule: agree.strong_induct)
   case (a_App e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_App(5) show ?case
   proof (cases rule: s_App_inv)
     case (App1 e\<^sub>1')
     with a_App(2) obtain eP\<^sub>1' eV\<^sub>1' \<pi> where *: "{$$} \<turnstile> e\<^sub>1', eP\<^sub>1', eV\<^sub>1' : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
       "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<^sub>1\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP\<^sub>1'\<ggreater>" "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<^sub>1\<ggreater> V\<rightarrow> \<lless>\<pi>', eV\<^sub>1'\<ggreater>"
       by blast
     show ?thesis
     proof (intro exI conjI)
       from * App1 a_App(1,3,5-)
       show "{$$} \<turnstile> e', App eP\<^sub>1' eP\<^sub>2, App eV\<^sub>1' eV\<^sub>2 : \<tau>\<^sub>2"
         "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, App eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, App eP\<^sub>1' eP\<^sub>2\<ggreater>"
         "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', App eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', App eV\<^sub>1' eV\<^sub>2\<ggreater>"
         by auto
     qed
   next
     case (App2 e\<^sub>2')
     with a_App(4) obtain eP\<^sub>2' eV\<^sub>2' \<pi> where *: "{$$} \<turnstile> e\<^sub>2', eP\<^sub>2', eV\<^sub>2' : \<tau>\<^sub>1"
       "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP\<^sub>2'\<ggreater>" "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', eV\<^sub>2'\<ggreater>"
       by blast
     show ?thesis
     proof (intro exI conjI)
       from * App2 a_App(1,3,5-)
       show "{$$} \<turnstile> e', App eP\<^sub>1 eP\<^sub>2', App eV\<^sub>1 eV\<^sub>2' : \<tau>\<^sub>2"
         "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, App eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, App eP\<^sub>1 eP\<^sub>2'\<ggreater>"
         "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', App eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', App eV\<^sub>1 eV\<^sub>2'\<ggreater>"
         by auto
     qed
   next
     case (AppLam x e)
     from a_App(1)[unfolded \<open>e\<^sub>1 = Lam x e\<close>] show ?thesis
     proof (cases rule: a_Lam_inv_I[case_names _ Lam])
       case (Lam eP eV)
       show ?thesis
       proof (intro exI conjI)
         from Lam a_App(3,5) AppLam show "{$$} \<turnstile> e', eP[eP\<^sub>2 / x], eV[eV\<^sub>2 / x] : \<tau>\<^sub>2"
           by (auto intro: lemma4)
         from Lam a_App(3,5) AppLam show "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, App eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ [], eP[eP\<^sub>2 / x]\<ggreater>"
           by (intro allI iffD1[OF smallstepP_ps_prepend[where \<pi> = "[]", simplified]])
             (auto simp: fresh_Pair intro!: s_AppLam[where v=eP\<^sub>2])
         from Lam a_App(3,5) AppLam show "\<forall>\<pi>'. \<lless>[] @ \<pi>', App eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', eV[eV\<^sub>2 / x]\<ggreater>"
           by (intro allI iffD1[OF smallstepV_ps_append[where \<pi>' = "[]", simplified]])
             (auto simp: fresh_Pair intro!: s_AppLam[where v=eV\<^sub>2])
       qed
     qed simp
   next
     case (AppRec x e)
     from a_App(1)[unfolded \<open>e\<^sub>1 = Rec x e\<close>] show ?thesis
     proof (cases rule: a_Rec_inv_I[consumes 1, case_names _ Rec])
       case (Rec y e'' eP' eV')
       from Rec(5,4) show ?thesis
       proof (cases rule: a_Lam_inv_I[consumes 1, case_names _ Lam])
         case (Lam eP'' eV'')
         show ?thesis
         proof (intro conjI exI[of _ "[]"] exI)
           let ?eP = "App (Lam y eP''[Rec x (Lam y eP'') / x]) eP\<^sub>2"
           let ?eV = "App (Lam y eV''[Rec x (Lam y eV'') / x]) eV\<^sub>2"
           from a_App(3) AppRec have [simp]: "value eP\<^sub>2" "atom x \<sharp> eP\<^sub>2" "value eV\<^sub>2" "atom x \<sharp> eV\<^sub>2"
             by (auto simp: fresh_Pair)
           from Lam a_App(3,5-) AppRec Rec show "{$$} \<turnstile> e', ?eP, ?eV : \<tau>\<^sub>2"
             unfolding term.eq_iff Abs1_eq(3)
-            by (auto simp: fmap_reorder_neq_updates
+            by (auto simp: fmupd_reorder_neq
               intro!: agree.a_App[where \<Gamma>="{$$}"] a_Lam[where x=y] lemma4)
           from Lam a_App(3,5-) AppRec Rec show "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, App eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ [], ?eP\<ggreater>"
             unfolding term.eq_iff Abs1_eq(3)
             using s_AppRec[where v=eP\<^sub>2 and x=x and \<pi>="[]" and e="Lam y eP''" and uv=P]
             by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]])
               (auto simp: fresh_Pair simp del: s_AppRec)
           from Lam a_App(3,5-) AppRec Rec show "\<forall>\<pi>'. \<lless>[] @ \<pi>', App eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', ?eV\<ggreater>"
             unfolding term.eq_iff Abs1_eq(3)
             using s_AppRec[where v=eV\<^sub>2 and x=x and \<pi>="[]" and e="Lam y eV''" and uv=V]
             by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]])
               (auto simp: fresh_Pair simp del: s_AppRec)
         qed
       qed (simp add: fresh_fmap_update)
     qed simp
   qed
 next
   case (a_Let x e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   then have "atom x \<sharp> (e\<^sub>1, [])" by auto
   with a_Let(10) show ?case
   proof (cases rule: s_Let_inv)
     case Let1
     show ?thesis
     proof (intro conjI exI[of _ "[]"] exI)
       from a_Let(6,8) Let1 show "{$$} \<turnstile> e', eP\<^sub>2[eP\<^sub>1 / x], eV\<^sub>2[eV\<^sub>1 / x] : \<tau>\<^sub>2"
         by (auto intro: lemma4)
       from a_Let(4,6) Let1 show "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Let eP\<^sub>1 x eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ [], eP\<^sub>2[eP\<^sub>1 / x]\<ggreater>"
         by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Let2) auto
       from a_Let(5,6) Let1 show "\<forall>\<pi>'. \<lless>[] @ \<pi>', Let eV\<^sub>1 x eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', eV\<^sub>2[eV\<^sub>1 / x]\<ggreater>"
         by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]] s_Let2) auto
     qed
   next
     case (Let2 e\<^sub>1')
     moreover
     from Let2 a_Let(7) obtain eP\<^sub>1' eV\<^sub>1' \<pi>
       where ih: "{$$} \<turnstile> e\<^sub>1', eP\<^sub>1', eV\<^sub>1' : \<tau>\<^sub>1"
         "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<^sub>1\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP\<^sub>1'\<ggreater>"
         "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<^sub>1\<ggreater> V\<rightarrow> \<lless>\<pi>', eV\<^sub>1'\<ggreater>"
       by (blast dest: spec[of _ "[]"])
     then have [simp]: "atom x \<sharp> ({$$}, e\<^sub>1', eP\<^sub>1', eV\<^sub>1')"
       using agree_empty_fresh by auto
     from ih a_Let(4) have [simp]: "atom x \<sharp> \<pi>"
       using fresh_Nil fresh_append fresh_ps_smallstep_P by blast
     from a_Let ih have agree: "{$$} \<turnstile> Let e\<^sub>1' x e\<^sub>2, Let eP\<^sub>1' x eP\<^sub>2, Let eV\<^sub>1' x eV\<^sub>2 : \<tau>\<^sub>2"
       by auto
     moreover from a_Let(4,5) ih(1) spec[OF ih(2), of "[]", simplified]
     have "\<lless>\<pi>', Let eP\<^sub>1 x eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>' @ \<pi>, Let eP\<^sub>1' x eP\<^sub>2\<ggreater>" for \<pi>'
       by (intro iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Let1) (auto simp: fresh_Pair)
     moreover from a_Let(4,5) ih(1) spec[OF ih(3), of "[]", simplified]
     have "\<lless>\<pi> @ \<pi>', Let eV\<^sub>1 x eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', Let eV\<^sub>1' x eV\<^sub>2\<ggreater>" for \<pi>'
       by (intro iffD1[OF smallstepV_ps_append[of \<pi> _ "[]", simplified]] s_Let1) (auto simp: fresh_Pair)
     ultimately show ?thesis
       by blast
   qed
 next
   case (a_Case e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_Case(7) show ?case
   proof (cases rule: s_Case_inv)
     case (Case e'')
     with a_Case(2)[of e''] obtain eP'' eV'' \<pi> where ih: "{$$} \<turnstile> e'', eP'', eV'' : Syntax.Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
       "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP''\<ggreater>" "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<ggreater> V\<rightarrow> \<lless>\<pi>', eV''\<ggreater>"
       by blast
     show ?thesis
     proof (intro conjI exI[of _ \<pi>] exI)
       from ih(1) a_Case(3,5) Case show "{$$} \<turnstile> e', Case eP'' eP\<^sub>1 eP\<^sub>2, Case eV'' eV\<^sub>1 eV\<^sub>2 : \<tau>"
         by auto
       from a_Case(5) spec[OF ih(2), of "[]", simplified]
       show "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Case eP eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, Case eP'' eP\<^sub>1 eP\<^sub>2\<ggreater>"
         by (intro allI iffD1[OF smallstepP_ps_prepend[of "[]", simplified]] s_Case) auto
       from a_Case(5) spec[OF ih(3), of "[]", simplified]
       show "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', Case eV eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>', Case eV'' eV\<^sub>1 eV\<^sub>2\<ggreater>"
         by (intro allI iffD1[OF smallstepV_ps_append[of _ _ "[]", simplified]] s_Case) auto
     qed
   next
     case (Inj1 v)
     from a_Case(1)[unfolded \<open>e = Inj1 v\<close>] show ?thesis
     proof (cases rule: a_Inj1_inv_I[consumes 1, case_names Case])
       case (Case vP vV)
       with a_Case(3,5) Inj1 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI)
         from Case a_Case(3,5) Inj1 show "{$$} \<turnstile> e', App eP\<^sub>1 vP, App eV\<^sub>1 vV : \<tau>"
           by auto
       qed auto
     qed
   next
     case (Inj2 v)
     from a_Case(1)[unfolded \<open>e = Inj2 v\<close>] show ?thesis
     proof (cases rule: a_Inj2_inv_I[consumes 1, case_names Case])
       case (Case vP vV)
       with a_Case(3,5) Inj2 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI)
         from Case a_Case(3,5) Inj2 show "{$$} \<turnstile> e', App eP\<^sub>2 vP, App eV\<^sub>2 vV : \<tau>"
           by auto
       qed auto
     qed
   qed
 next
   case (a_Prj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Prj1(3) show ?case
   proof (cases rule: s_Prj1_inv)
     case (Prj1 e'')
     then show ?thesis
       by (blast dest!: a_Prj1(2))
   next
     case (PrjPair1 v\<^sub>2)
     from a_Prj1(1)[unfolded \<open>e = Syntax.Pair e' v\<^sub>2\<close>] show ?thesis
     proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
       case (Pair eP\<^sub>1 eV\<^sub>1 eP\<^sub>2 eV\<^sub>2)
       with PrjPair1 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI)
         show "{$$} \<turnstile> e', eP\<^sub>1, eV\<^sub>1 : \<tau>\<^sub>1"
           by (rule Pair)
       qed auto
     qed
   qed
 next
   case (a_Prj2 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Prj2(3) show ?case
   proof (cases rule: s_Prj2_inv)
     case (Prj2 e'')
     then show ?thesis
       by (blast dest!: a_Prj2(2))
   next
     case (PrjPair2 v\<^sub>1)
     from a_Prj2(1)[unfolded \<open>e = Syntax.Pair v\<^sub>1 e'\<close>] show ?thesis
     proof (cases rule: a_Pair_inv_I[consumes 1, case_names Pair])
       case (Pair eP\<^sub>1 eV\<^sub>1 eP\<^sub>2 eV\<^sub>2)
       with PrjPair2 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI)
         show "{$$} \<turnstile> e', eP\<^sub>2, eV\<^sub>2 : \<tau>\<^sub>2"
           by (rule Pair)
       qed auto
     qed
   qed
 next
   case (a_Roll \<alpha> e eP eV \<tau>)
   from a_Roll(5) show ?case
   proof (cases rule: s_Roll_inv)
     case (Roll e'')
     with a_Roll(4) obtain eP'' eV'' \<pi> where *: "{$$} \<turnstile> e'', eP'', eV'' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
       "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP''\<ggreater>" "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<ggreater> V\<rightarrow> \<lless>\<pi>', eV''\<ggreater>"
       by blast
     show ?thesis
     proof (intro exI conjI)
       from * Roll
       show "{$$} \<turnstile> e', Roll eP'', Roll eV'' : Mu \<alpha> \<tau>"
         "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Roll eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, Roll eP''\<ggreater>"
         "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', Roll eV\<ggreater> V\<rightarrow> \<lless>\<pi>', Roll eV''\<ggreater>"
         by auto
     qed
   qed
 next
   case (a_Unroll \<alpha> e eP eV \<tau>)
   from a_Unroll(5) show ?case
   proof (cases rule: s_Unroll_inv)
     case (Unroll e'')
     with a_Unroll(4) obtain eP'' eV'' \<pi> where *: "{$$} \<turnstile> e'', eP'', eV'' : Mu \<alpha> \<tau>"
       "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP''\<ggreater>" "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', eV\<ggreater> V\<rightarrow> \<lless>\<pi>', eV''\<ggreater>"
       by blast
     show ?thesis
     proof (intro exI conjI)
       from * Unroll
       show "{$$} \<turnstile> e', Unroll eP'', Unroll eV'' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>"
         "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Unroll eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, Unroll eP''\<ggreater>"
         "\<forall>\<pi>'. \<lless>\<pi> @ \<pi>', Unroll eV\<ggreater> V\<rightarrow> \<lless>\<pi>', Unroll eV''\<ggreater>"
         by auto
     qed
   next
     case UnrollRoll
     with a_Unroll(3)[unfolded \<open>e = Roll e'\<close>] show ?thesis
     proof (cases rule: a_Roll_inv_I[case_names Roll])
       case (Roll eP' eV')
       with UnrollRoll show ?thesis
       proof (intro conjI exI[of _ "[]"] exI)
         show "{$$} \<turnstile> e', eP', eV' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>" by fact
       qed auto
     qed
   qed
 next
   case (a_Auth e eP eV \<tau>)
   from a_Auth(1) have [simp]: "atom x \<sharp> eP" for x :: var
     using agree_empty_fresh by simp
   from a_Auth(3) show ?case
   proof (cases rule: s_AuthI_inv)
     case (Auth e'')
     then show ?thesis
       by (blast dest!: a_Auth(2))
   next
     case AuthI
     with a_Auth(1) have "value eP" "value eV" by auto
     with a_Auth(1) AuthI(2) show ?thesis
     proof (intro conjI exI[of _ "[]"] exI)
       from a_Auth(1) AuthI(2) \<open>value eP\<close>
       show "{$$} \<turnstile> e', Hashed (hash \<lparr>eP\<rparr>) eP, Hash (hash \<lparr>eP\<rparr>) : AuthT \<tau>"
         by (auto dest: lemma2_1 simp: fresh_shallow)
     qed (auto dest: lemma2_1 simp: fresh_shallow)
   qed
 next
   case (a_Unauth e eP eV \<tau>)
   from a_Unauth(1) have eP_closed: "closed eP"
     using agree_empty_fresh by simp
   from a_Unauth(3) show ?case
   proof (cases rule: s_UnauthI_inv)
     case (Unauth e')
     then show ?thesis
       by (blast dest!: a_Unauth(2))
   next
     case UnauthI
     with a_Unauth(1) have "value eP" "value eV" by auto
     from a_Unauth(1) show ?thesis
     proof (cases rule: a_AuthT_value_inv[case_names _ _ _ Unauth])
       case (Unauth vP')
       show ?thesis
       proof (intro conjI exI[of _ "[\<lparr>vP'\<rparr>]"] exI)
         from Unauth(1,2) UnauthI(2) a_Unauth(1)
         show "{$$} \<turnstile> e', vP', \<lparr>vP'\<rparr> : \<tau>"
           by (auto simp: fresh_shallow)
         then have "closed vP'"
           by auto
         with Unauth(1,2) a_Unauth(1) show
           "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Unauth eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ [\<lparr>vP'\<rparr>], vP'\<ggreater>"
           "\<forall>\<pi>'. \<lless>[\<lparr>vP'\<rparr>] @ \<pi>', Unauth eV\<ggreater> V\<rightarrow> \<lless>\<pi>', \<lparr>vP'\<rparr>\<ggreater>"
           by (auto simp: fresh_shallow)
       qed
     qed (auto simp: \<open>value e\<close> \<open>value eP\<close> \<open>value eV\<close>)
   qed
 next
   case (a_Pair e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   from a_Pair(5) show ?case
   proof (cases rule: s_Pair_inv)
     case (Pair1 e\<^sub>1')
     with a_Pair(1,3) show ?thesis
       by (blast dest!: a_Pair(2))
   next
     case (Pair2 e\<^sub>2')
     with a_Pair(1,3) show ?thesis
       by (blast dest!: a_Pair(4))
   qed
 next
   case (a_Inj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Inj1(3) show ?case
   proof (cases rule: s_Inj1_inv)
     case (Inj1 e')
     with a_Inj1(1) show ?thesis
       by (blast dest!: a_Inj1(2))
   qed
 next
   case (a_Inj2 e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1)
   from a_Inj2(3) show ?case
   proof (cases rule: s_Inj2_inv)
     case (Inj2 e'')
     with a_Inj2(1) show ?thesis
       by (blast dest!: a_Inj2(2))
   qed
 qed (simp, meson value.intros value_no_step)+
 
 subsection \<open>Lemma 6: Single-Step Security\<close>
 
 lemma lemma6:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> \<pi>\<^sub>A, eV \<ggreater> V\<rightarrow> \<lless> \<pi>', eV' \<ggreater>"
   obtains e' eP' \<pi>
   where "\<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater>" "\<forall>\<pi>\<^sub>P. \<lless> \<pi>\<^sub>P, eP \<ggreater> P\<rightarrow> \<lless> \<pi>\<^sub>P @ \<pi>, eP' \<ggreater>"
   and   "{$$} \<turnstile> e', eP', eV' : \<tau> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
          (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
 proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV \<tau> avoiding: \<pi>\<^sub>A \<pi>' eV' rule: agree.strong_induct)
   case (a_App e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_App(5) show ?case
   proof (cases rule: s_App_inv)
     case (App1 eV\<^sub>1')
     with a_App(1,3) show ?thesis
       by (blast dest!: a_App(2))
   next
     case (App2 e\<^sub>2')
     with a_App(1,3) show ?thesis
       by (blast dest!: a_App(4))
   next
     case (AppLam x eV'')
     from a_App(1)[unfolded \<open>eV\<^sub>1 = Lam x eV''\<close>] show ?thesis
     proof (cases rule: a_Lam_inv_V[case_names Lam])
       case (Lam e'' eP'')
       with a_App(3) AppLam show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         from Lam a_App(3) AppLam show "{$$} \<turnstile> e''[e\<^sub>2 / x], eP''[eP\<^sub>2 / x], eV' : \<tau>\<^sub>2"
           by (auto intro: lemma4)
       qed (auto 0 3 simp: fresh_Pair intro!: s_AppLam[where \<pi>="[]"]
           intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
     qed
   next
     case (AppRec x eV'')
     from a_App(1)[unfolded \<open>eV\<^sub>1 = Rec x eV''\<close>] show ?thesis
     proof (cases rule: a_Rec_inv_V[case_names _ Rec])
       case (Rec y e'''  eP''' eV''')
       with a_App(1,3) AppRec show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         let ?e = "App (Lam y e'''[Rec x (Lam y e''') / x]) e\<^sub>2"
         let ?eP = "App (Lam y eP'''[Rec x (Lam y eP''') / x]) eP\<^sub>2"
         from Rec a_App(3) AppRec show "{$$} \<turnstile> ?e, ?eP, eV' : \<tau>\<^sub>2"
           by (auto simp del: subst_term.simps(3) intro!: agree.a_App[where \<Gamma>="{$$}"] lemma4)
       qed (auto 0 3 simp del: subst_term.simps(3) simp: fresh_Pair intro!: s_AppRec[where \<pi>="[]"]
           intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
     qed simp
   qed
 next
   case (a_Let x e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   then have "atom x \<sharp> (eV\<^sub>1, \<pi>\<^sub>A)" by auto
   with a_Let(12) show ?case
   proof (cases rule: s_Let_inv)
     case Let1
     with a_Let(5,6,8,10) show ?thesis
     proof (intro conjI exI[of _ "[]"] exI disjI1)
       from Let1 a_Let(5,6,8,10) show "{$$} \<turnstile> e\<^sub>2[e\<^sub>1 / x], eP\<^sub>2[eP\<^sub>1 / x], eV' : \<tau>\<^sub>2"
         by (auto intro: lemma4)
     qed (auto 0 3 intro: iffD1[OF smallstepP_ps_prepend[of "[]" _ "[]", simplified]])
   next
     case (Let2 eV\<^sub>1')
     with a_Let(9)[of \<pi>\<^sub>A \<pi>' eV\<^sub>1'] obtain e\<^sub>1' \<pi> eP\<^sub>1' s s' where
       ih: "\<lless>[], e\<^sub>1\<ggreater> I\<rightarrow> \<lless>[], e\<^sub>1'\<ggreater>" "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<^sub>1\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP\<^sub>1'\<ggreater>"
         "{$$} \<turnstile> e\<^sub>1', eP\<^sub>1', eV\<^sub>1' : \<tau>\<^sub>1 \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
          closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s'"
       by blast
     with a_Let(5,6) have fresh: "atom x \<sharp> e\<^sub>1'" "atom x \<sharp> eP\<^sub>1'"
       using fresh_smallstep_I fresh_smallstep_P by blast+
     from ih a_Let(2,6) have "atom x \<sharp> \<pi>"
       using fresh_append fresh_ps_smallstep_P by blast
     with Let2 a_Let(1-8,10,12-) fresh ih show ?thesis
     proof (intro conjI exI[of _ "\<pi>"] exI)
       from \<open>atom x \<sharp> \<pi>\<close> Let2 a_Let(1-8,10,12-) fresh ih
       show "{$$} \<turnstile> Let e\<^sub>1' x e\<^sub>2, Let eP\<^sub>1' x eP\<^sub>2, eV' : \<tau>\<^sub>2 \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
         (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
         by auto
     qed (auto dest: spec[of _ "[]"] intro!: iffD1[OF smallstepP_ps_prepend, of "[]", simplified])
   qed
 next
   case (a_Case e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_Case(7) show ?case
   proof (cases rule: s_Case_inv)
     case (Case eV'')
     from a_Case(2)[OF Case(2)] show ?thesis
     proof (elim exE disjE conjE, goal_cases ok collision)
       case (ok e'' \<pi> eP'')
       with Case a_Case(3,5) show ?case by blast
     next
       case (collision e'' \<pi> eP'' s s')
       with Case a_Case(3,5) show ?case
       proof (intro exI[of _ "[s]"] exI conjI disjI2)
         from Case a_Case(3,5) collision show "\<lless>[], Case e e\<^sub>1 e\<^sub>2\<ggreater> I\<rightarrow> \<lless>[], Case e'' e\<^sub>1 e\<^sub>2\<ggreater>"
           "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, Case eP eP\<^sub>1 eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ [s], Case eP'' eP\<^sub>1 eP\<^sub>2\<ggreater>"
           by auto
         from collision show "closed s" "closed s'" "s \<noteq> s'" "hash s = hash s'" by auto
       qed simp
     qed
   next
     case (Inj1 vV)
     from a_Case(1)[unfolded \<open>eV = Inj1 vV\<close>] show ?thesis
     proof (cases rule: a_Inj1_inv_V[consumes 1, case_names Inj])
       case (Inj v' vP')
       with Inj1 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         from a_Case(3) Inj Inj1 show "{$$} \<turnstile> App e\<^sub>1 v', App eP\<^sub>1 vP', eV' : \<tau>"
           by auto
       qed auto
     qed
   next
     case (Inj2 vV)
     from a_Case(1)[unfolded \<open>eV = Inj2 vV\<close>] show ?thesis
     proof (cases rule: a_Inj2_inv_V[consumes 1, case_names Inj])
       case (Inj v' vP')
       with Inj2 show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         from a_Case(5) Inj Inj2 show "{$$} \<turnstile> App e\<^sub>2 v', App eP\<^sub>2 vP', eV' : \<tau>"
           by auto
       qed auto
     qed
   qed
 next
   case (a_Prj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Prj1(3) show ?case
   proof (cases rule: s_Prj1_inv)
     case (Prj1 eV'')
     then show ?thesis
       by (blast dest!: a_Prj1(2))
   next
     case (PrjPair1 v\<^sub>2)
     with a_Prj1(1) show ?thesis
     proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
       case (Pair e\<^sub>1 eP\<^sub>1 eV\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
       with PrjPair1 a_Prj1(1) show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         from Pair PrjPair1 a_Prj1(1) show "{$$} \<turnstile> e\<^sub>1, eP\<^sub>1, eV' : \<tau>\<^sub>1"
           by auto
       qed auto
     qed simp_all
   qed
 next
   case (a_Prj2 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Prj2(3) show ?case
   proof (cases rule: s_Prj2_inv)
     case (Prj2 eV'')
     then show ?thesis
       by (blast dest!: a_Prj2(2))
   next
     case (PrjPair2 v\<^sub>2)
     with a_Prj2(1) show ?thesis
     proof (cases rule: a_Prod_inv[consumes 1, case_names _ _ _ _ Pair])
       case (Pair e\<^sub>1 eP\<^sub>1 eV\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
       with PrjPair2 a_Prj2(1) show ?thesis
       proof (intro conjI exI[of _ "[]"] exI disjI1)
         from Pair PrjPair2 a_Prj2(1) show "{$$} \<turnstile> e\<^sub>2, eP\<^sub>2, eV' : \<tau>\<^sub>2"
           by auto
       qed auto
     qed simp_all
   qed
 next
   case (a_Roll \<alpha> e eP eV \<tau>)
   from a_Roll(7) show ?case
   proof (cases rule: s_Roll_inv)
     case (Roll eV'')
     from a_Roll(6)[OF Roll(2)] obtain e'' \<pi> eP'' where ih:
       "\<lless>[], e\<ggreater> I\<rightarrow> \<lless>[], e''\<ggreater>" "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP''\<ggreater>"
       "{$$} \<turnstile> e'', eP'', eV'' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
       (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
       by blast
     with Roll show ?thesis
     proof (intro exI[of _ "\<pi>"] exI conjI)
       from ih Roll show "{$$} \<turnstile> Roll e'', Roll eP'', eV' : Mu \<alpha> \<tau> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
         (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
         by auto
     qed auto
   qed
 next
   case (a_Unroll \<alpha> e eP eV \<tau>)
   from a_Unroll(7) show ?case
   proof (cases rule: s_Unroll_inv)
     case (Unroll eV'')
     from a_Unroll(6)[OF Unroll(2)] obtain e'' \<pi> eP'' where ih:
       "\<lless>[], e\<ggreater> I\<rightarrow> \<lless>[], e''\<ggreater>" "\<forall>\<pi>\<^sub>P. \<lless>\<pi>\<^sub>P, eP\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>, eP''\<ggreater>"
       "{$$} \<turnstile> e'', eP'', eV'' : Mu \<alpha> \<tau> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
       (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
       by blast
     with Unroll show ?thesis
     proof (intro exI[of _ "\<pi>"] exI conjI)
       from ih Unroll show "{$$} \<turnstile> Unroll e'', Unroll eP'', eV' : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<or>
         (\<exists>s s'. closed s \<and> closed s' \<and> \<pi> = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
         by auto
     qed auto
   next
     case UnrollRoll
     with a_Unroll(5) show ?thesis
       by fastforce
   qed
 next
   case (a_Auth e eP eV \<tau>)
   from a_Auth(1) have [simp]: "atom x \<sharp> eP" for x :: var
     using agree_empty_fresh by simp
   from a_Auth(3) show ?case
   proof (cases rule: s_AuthV_inv)
     case (Auth eV'')
     from a_Auth(2)[OF Auth(2)] show ?thesis
     proof (elim exE disjE conjE, goal_cases ok collision)
       case (ok e'' \<pi> eP'')
       with Auth show ?case
       proof (intro conjI exI[of _ "\<pi>"] exI disjI1)
         from ok Auth show "{$$} \<turnstile> Auth e'', Auth eP'', eV' : AuthT \<tau>"
           by auto
       qed auto
     next
       case (collision e'' \<pi> eP'' s s')
       then show ?case by blast
     qed
   next
     case AuthV
     with a_Auth(1) show ?thesis
     proof (intro exI[of _ "[]"] exI conjI disjI1)
       from a_Auth(1) AuthV show "{$$} \<turnstile> e, Hashed (hash \<lparr>eP\<rparr>) eP, eV' : AuthT \<tau>"
         by (auto dest: lemma2_1)
     qed (auto simp: fresh_shallow)
   qed
 next
   case (a_Unauth e eP eV \<tau>)
   from a_Unauth(3) show ?case
   proof (cases rule: s_UnauthV_inv)
     case (Unauth e')
     then show ?thesis
       by (blast dest!: a_Unauth(2))
   next
     case UnauthV
     from a_Unauth(1)[unfolded \<open>eV = Hash (hash eV')\<close>] UnauthV a_Unauth(1) show ?thesis
     proof (cases rule: a_AuthT_value_inv[consumes 1, case_names _ _ _ Hashed])
       case (Hashed vP')
       with UnauthV a_Unauth(1) show ?thesis
       proof (intro exI[of _ "[\<lparr>vP'\<rparr>]"] exI conjI)
         from Hashed UnauthV a_Unauth(1) show "{$$} \<turnstile> e, vP', eV' : \<tau> \<and> \<pi>\<^sub>A = [\<lparr>vP'\<rparr>] @ \<pi>' \<or>
           (\<exists>s s'. closed s \<and> closed s' \<and> [\<lparr>vP'\<rparr>] = [s] \<and> \<pi>\<^sub>A = [s'] @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s')"
           by (fastforce elim: a_HashI_inv[where \<Gamma>="{$$}"])
       qed auto
     qed auto
   qed
 next
   case (a_Pair e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   from a_Pair(5) show ?case
   proof (cases rule: s_Pair_inv)
     case (Pair1 eV\<^sub>1')
     with a_Pair(3) show ?thesis
       using a_Pair(2)[of \<pi>\<^sub>A \<pi>' eV\<^sub>1'] by blast
   next
     case (Pair2 eV\<^sub>2')
     with a_Pair(1) show ?thesis
       using a_Pair(4)[of \<pi>\<^sub>A \<pi>' eV\<^sub>2'] by blast
   qed
 next
   case (a_Inj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Inj1(3) show ?case
   proof (cases rule: s_Inj1_inv)
     case (Inj1 eV'')
     then show ?thesis
       using a_Inj1(2)[of \<pi>\<^sub>A \<pi>' eV''] by blast
   qed
 next
   case (a_Inj2 e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1)
   from a_Inj2(3) show ?case
   proof (cases rule: s_Inj2_inv)
     case (Inj2 eV'')
     with a_Inj2(1) show ?thesis
       using a_Inj2(2)[of \<pi>\<^sub>A \<pi>' eV''] by blast
   qed
 qed (simp, meson value.intros value_no_step)+
 
 subsection \<open>Theorem 1: Correctness\<close>
 
 lemma theorem1_correctness:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater>"
   obtains eP' eV' \<pi>
   where "\<lless> [], eP \<ggreater> P\<rightarrow>i \<lless> \<pi>, eP' \<ggreater>"
     "\<lless> \<pi>, eV \<ggreater> V\<rightarrow>i \<lless> [], eV' \<ggreater>"
     "{$$} \<turnstile> e', eP', eV' : \<tau>"
   using assms(2,1)
 proof (atomize_elim, induct "[]::proofstream" e I i "[]::proofstream" e' rule: smallsteps.induct)
   case (s_Id e)
   then show ?case by auto
 next
   case (s_Tr e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 e\<^sub>3)
   then have "\<pi>\<^sub>2 = []" by (auto dest: smallstepI_ps_eq)
   with s_Tr obtain eP\<^sub>2 \<pi> eV\<^sub>2 where ih:
     "\<lless>[], eP\<ggreater> P\<rightarrow>i \<lless>\<pi>, eP\<^sub>2\<ggreater>" "\<lless>\<pi>, eV\<ggreater> V\<rightarrow>i \<lless>[], eV\<^sub>2\<ggreater>" "{$$} \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>"
     by (atomize_elim, intro s_Tr(2)) auto
   moreover obtain eP\<^sub>3 eV\<^sub>3 \<pi>' where agree: "{$$} \<turnstile> e\<^sub>3, eP\<^sub>3, eV\<^sub>3 : \<tau>"
     and "\<lless>\<pi>\<^sub>P, eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>', eP\<^sub>3\<ggreater>" "\<lless>\<pi>' @ \<pi>'', eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>\<pi>'', eV\<^sub>3\<ggreater>"
   for \<pi>\<^sub>P \<pi>'' using lemma5[OF ih(3) s_Tr(3)[unfolded \<open>\<pi>\<^sub>2 = []\<close>], of thesis] by blast
   ultimately have "\<lless>[], eP\<ggreater> P\<rightarrow>i + 1 \<lless>\<pi> @ \<pi>', eP\<^sub>3\<ggreater>" "\<lless>\<pi> @ \<pi>', eV\<ggreater> V\<rightarrow>i + 1 \<lless>[], eV\<^sub>3\<ggreater>"
     by (auto simp: smallstepsV_ps_append[of _ _ _ "[]", simplified, symmetric]
        intro!: smallsteps.s_Tr[of "\<pi> @ \<pi>'"])
   with agree show ?case by blast
 qed
 
 subsection \<open>Counterexamples to Theorem 1: Security\<close>
 
 text \<open>Counterexample using administrative normal form.\<close>
 
 lemma security_false:
   assumes agree: "\<And>e eP eV \<tau> \<pi>A i \<pi>' eV'. \<lbrakk> {$$} \<turnstile> e, eP, eV : \<tau>; \<lless> \<pi>A, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>', eV' \<ggreater> \<rbrakk> \<Longrightarrow>
       \<exists>e' eP' \<pi> j \<pi>0 s s'. (\<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater> \<and> \<lless> [], eP \<ggreater> P\<rightarrow>i \<lless> \<pi>, eP' \<ggreater> \<and> (\<pi>A = \<pi> @ \<pi>') \<and> {$$} \<turnstile> e', eP', eV' : \<tau>) \<or>
        (j \<le> i \<and> \<lless> [], eP \<ggreater> P\<rightarrow>j \<lless> \<pi>0 @ [s], eP' \<ggreater> \<and> (\<pi>A = \<pi>0 @ [s'] @ \<pi>') \<and> s \<noteq> s' \<and> hash s = hash s')"
   and     collision: "hash (Inj1 Unit) = hash (Inj2 Unit)"
   and     no_collision_with_Unit: "\<And>t. hash Unit = hash t \<Longrightarrow> t = Unit"
   shows   False
 proof -
   define i where "i = Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))"
   obtain x y z :: var where fresh: "atom y \<sharp> x" "atom z \<sharp> (x, y)"
     by (metis obtain_fresh)
   define t where "t = Let (Let (Auth (Inj1 Unit)) y (Unauth (Var y))) x (Let (Let (Auth Unit) z (Unauth (Var z))) y (Var x))"
   note fresh_Cons[simp]
   have prover: "\<lless> [], t \<ggreater> P\<rightarrow>i \<lless> [Inj1 Unit, Unit], Inj1 Unit \<ggreater>" \<comment> \<open>prover execution\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
            apply (rule s_Let1[rotated])
             apply (rule s_Let1[rotated])
              apply (rule s_AuthP[rotated])
               apply simp
              apply simp
             apply simp
            apply simp
           apply (rule s_Let1[rotated])
            apply (rule s_Let2)
             apply simp
            apply simp
           apply simp
          apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_UnauthP)
           apply simp
          apply simp
         apply simp
         apply (rule s_Let2)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_Let1[rotated])
          apply (rule s_AuthP[rotated])
           apply simp
          apply simp
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthP)
       apply simp
      apply simp
     apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   have verifier1: "\<lless> [Inj1 Unit, Unit], t \<ggreater> V\<rightarrow>i \<lless> [], Inj1 Unit \<ggreater>" \<comment> \<open>verifier execution\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
            apply (rule s_Let1[rotated])
             apply (rule s_Let1[rotated])
              apply (rule s_AuthV[rotated])
               apply simp
              apply simp
             apply simp
            apply simp
           apply (rule s_Let1[rotated])
            apply (rule s_Let2)
             apply simp
            apply simp
           apply simp
          apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_UnauthV)
            apply simp
           apply simp
          apply simp
         apply (rule s_Let2)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_Let1[rotated])
          apply (rule s_AuthV[rotated])
           apply simp
          apply simp
         apply simp
        apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthV)
        apply simp
       apply simp
      apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   have verifier2: "\<lless> [Inj2 Unit, Unit], t \<ggreater> V\<rightarrow>i \<lless> [], Inj2 Unit \<ggreater>" \<comment> \<open>verifier execution with proofstream containing collision\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
            apply (rule s_Let1[rotated])
             apply (rule s_Let1[rotated])
              apply (rule s_AuthV[rotated])
               apply simp
              apply simp
             apply simp
            apply simp
           apply (rule s_Let1[rotated])
            apply (rule s_Let2)
             apply simp
            apply simp
           apply simp
          apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_UnauthV)
            apply simp
           apply (simp add: collision)
          apply simp
         apply (rule s_Let2)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_Let1[rotated])
          apply (rule s_AuthV[rotated])
           apply simp
          apply simp
         apply simp
        apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthV)
        apply simp
       apply simp
      apply simp
     apply (rule s_Let2[of Unit y _ "Inj2 Unit", simplified])
     apply simp
     done
   have judge: "{$$} \<turnstile> t : Sum One One"
     unfolding t_def using fresh
     by (force simp: fresh_Pair fresh_fmap_update)
   have ideal_deterministic: "e = Inj1 Unit" if "\<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], e\<ggreater>" for e
     apply (rule smallsteps_ideal_deterministic[OF that])
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
            apply (rule s_Let1[rotated])
             apply (rule s_Let1[rotated])
              apply (rule s_AuthI[rotated])
              apply simp
             apply simp
            apply simp
           apply (rule s_Let1[rotated])
            apply (rule s_Let2)
             apply simp
            apply simp
           apply simp
          apply simp
          apply (rule s_Let1[rotated])
           apply (rule s_UnauthI)
           apply simp
          apply simp
         apply (rule s_Let2)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let1[rotated])
         apply (rule s_Let1[rotated])
          apply (rule s_AuthI[rotated])
          apply simp
         apply simp
        apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
      apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthI)
       apply simp
      apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   from agree[OF judge_imp_agree[OF judge] verifier2] collision prover verifier1 show False
   proof safe
     fix e' eP'
     assume agree: "{$$} \<turnstile> e', eP', Inj2 Unit : Sum One One"
     assume assm: "\<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], e'\<ggreater>"
     then have "e' = Inj1 Unit"
       by (simp add: ideal_deterministic)
     with agree show False
       by auto
   qed (auto dest!: no_collision_with_Unit[OF sym])
 qed
 
 text \<open>Alternative, shorter counterexample not in administrative normal form.\<close>
 
 lemma security_false_alt:
   assumes agree: "\<And>e eP eV \<tau> \<pi>A i \<pi>' eV'. \<lbrakk> {$$} \<turnstile> e, eP, eV : \<tau>; \<lless> \<pi>A, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>', eV' \<ggreater> \<rbrakk> \<Longrightarrow>
       \<exists>e' eP' \<pi> j \<pi>0 s s'. (\<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater> \<and> \<lless> [], eP \<ggreater> P\<rightarrow>i \<lless> \<pi>, eP' \<ggreater> \<and> (\<pi>A = \<pi> @ \<pi>') \<and> {$$} \<turnstile> e', eP', eV' : \<tau>) \<or>
        (j \<le> i \<and> \<lless> [], eP \<ggreater> P\<rightarrow>j \<lless> \<pi>0 @ [s], eP' \<ggreater> \<and> (\<pi>A = \<pi>0 @ [s'] @ \<pi>') \<and> s \<noteq> s' \<and> hash s = hash s')"
   and     collision: "hash (Inj1 Unit) = hash (Inj2 Unit)"
   and     no_collision_with_Unit: "\<And>t. hash Unit = hash t \<Longrightarrow> t = Unit"
   shows   False
 proof -
   define i where "i = Suc (Suc (Suc (Suc (Suc (Suc 0)))))"
   obtain x y z :: var where fresh: "atom y \<sharp> x" "atom z \<sharp> (x, y)"
     by (metis obtain_fresh)
   define t where "t = Let (Unauth (Auth (Inj1 Unit))) x (Let (Unauth (Auth Unit)) y (Var x))"
   note fresh_Cons[simp]
   have prover: "\<lless> [], t \<ggreater> P\<rightarrow>i \<lless> [Inj1 Unit, Unit], Inj1 Unit \<ggreater>" \<comment> \<open>prover execution\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
          apply (rule s_Let1[rotated])
           apply (rule s_Unauth)
           apply (rule s_AuthP[rotated])
            apply simp
           apply simp
          apply simp
         apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthP)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Unauth)
        apply (rule s_AuthP[rotated])
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthP)
       apply simp
      apply simp
     apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   have verifier1: "\<lless> [Inj1 Unit, Unit], t \<ggreater> V\<rightarrow>i \<lless> [], Inj1 Unit \<ggreater>" \<comment> \<open>verifier execution\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
          apply (rule s_Let1[rotated])
           apply (rule s_Unauth)
           apply (rule s_AuthV[rotated])
            apply simp
           apply simp
          apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthV)
          apply simp
         apply simp
        apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Unauth)
        apply (rule s_AuthV[rotated])
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthV)
       apply simp
      apply simp
     apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   have verifier2: "\<lless> [Inj2 Unit, Unit], t \<ggreater> V\<rightarrow>i \<lless> [], Inj2 Unit \<ggreater>" \<comment> \<open>verifier execution with proofstream containing collision\<close>
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
          apply (rule s_Let1[rotated])
           apply (rule s_Unauth)
           apply (rule s_AuthV[rotated])
            apply simp
           apply simp
          apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthV)
           apply simp
          apply (simp add: collision)
         apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Unauth)
        apply (rule s_AuthV[rotated])
         apply simp
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthV)
       apply simp
      apply simp
     apply simp
     apply (rule s_Let2[of Unit y _ "Inj2 Unit", simplified])
     apply simp
     done
   have judge: "{$$} \<turnstile> t : Sum One One"
     unfolding t_def using fresh
     by (force simp: fresh_Pair fresh_fmap_update)
   have ideal_deterministic: "e = Inj1 Unit" if "\<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], e\<ggreater>" for e
     apply (rule smallsteps_ideal_deterministic[OF that])
     unfolding i_def t_def Suc_eq_plus1 using fresh
     apply -
     apply (rule smallsteps.intros)+
          apply (rule s_Let1[rotated])
           apply (rule s_Unauth)
           apply (rule s_AuthI[rotated])
           apply simp
          apply simp
         apply (rule s_Let1[rotated])
          apply (rule s_UnauthI)
          apply simp
         apply simp
        apply (rule s_Let2)
         apply simp
        apply simp
       apply simp
       apply (rule s_Let1[rotated])
        apply (rule s_Unauth)
        apply (rule s_AuthI[rotated])
        apply simp
       apply simp
      apply (rule s_Let1[rotated])
       apply (rule s_UnauthI)
       apply simp
      apply simp
     apply (rule s_Let2[of Unit y _ "Inj1 Unit", simplified])
     apply simp
     done
   from agree[OF judge_imp_agree[OF judge] verifier2] collision prover verifier1 show False
   proof safe
     fix e' eP'
     assume agree: "{$$} \<turnstile> e', eP', Inj2 Unit : Sum One One"
     assume assm: "\<lless>[], t\<ggreater> I\<rightarrow>i \<lless>[], e'\<ggreater>"
     then have "e' = Inj1 Unit"
       by (simp add: ideal_deterministic)
     with agree show False
       by auto
   qed (auto dest!: no_collision_with_Unit[OF sym])
 qed
 
 subsection \<open>Corrected Theorem 1: Security\<close>
 
 lemma theorem1_security:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> \<pi>\<^sub>A, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>', eV' \<ggreater>"
 shows "(\<exists>e' eP' \<pi>. \<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater> \<and> \<lless> [], eP \<ggreater> P\<rightarrow>i \<lless> \<pi>, eP' \<ggreater> \<and> \<pi>\<^sub>A = \<pi> @ \<pi>' \<and> {$$} \<turnstile> e', eP', eV' : \<tau>) \<or>
        (\<exists>eP' j \<pi>\<^sub>0 \<pi>\<^sub>0' s s'. j \<le> i \<and> \<lless> [], eP \<ggreater> P\<rightarrow>j \<lless> \<pi>\<^sub>0 @ [s], eP' \<ggreater> \<and> \<pi>\<^sub>A = \<pi>\<^sub>0 @ [s'] @ \<pi>\<^sub>0' @ \<pi>' \<and> s \<noteq> s' \<and> hash s = hash s' \<and> closed s \<and> closed s')"
 using assms(2,1) proof (induct \<pi>\<^sub>A eV V i \<pi>' eV' rule: smallsteps.induct)
   case (s_Id \<pi> e)
   then show ?case by blast
 next
   case (s_Tr \<pi>\<^sub>1 eV\<^sub>1 i \<pi>\<^sub>2 eV\<^sub>2 \<pi>\<^sub>3 eV\<^sub>3)
   then obtain e\<^sub>2 \<pi> eP\<^sub>2 j \<pi>\<^sub>0 \<pi>\<^sub>0' s s'
     where "\<lless>[], e\<ggreater> I\<rightarrow>i \<lless>[], e\<^sub>2\<ggreater> \<and> \<lless>[], eP\<ggreater> P\<rightarrow>i \<lless>\<pi>, eP\<^sub>2\<ggreater> \<and> \<pi>\<^sub>1 = \<pi> @ \<pi>\<^sub>2 \<and> {$$} \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau> \<or>
             j \<le> i \<and> \<lless>[], eP\<ggreater> P\<rightarrow>j \<lless>\<pi>\<^sub>0 @ [s], eP\<^sub>2\<ggreater> \<and> closed s \<and> closed s' \<and> \<pi>\<^sub>1 = \<pi>\<^sub>0 @ [s'] @ \<pi>\<^sub>0' @ \<pi>\<^sub>2 \<and> s \<noteq> s' \<and> hash s = hash s'"
     by blast
   then show ?case
   proof (elim disjE conjE, goal_cases ok collision)
     case ok
     obtain e\<^sub>3 eP\<^sub>3 \<pi>' where
       "\<lless>[], e\<^sub>2\<ggreater> I\<rightarrow> \<lless>[], e\<^sub>3\<ggreater>" "\<lless>\<pi>\<^sub>P, eP\<^sub>2\<ggreater> P\<rightarrow> \<lless>\<pi>\<^sub>P @ \<pi>', eP\<^sub>3\<ggreater>"
       "{$$} \<turnstile> e\<^sub>3, eP\<^sub>3, eV\<^sub>3 : \<tau> \<and> \<pi>\<^sub>2 = \<pi>' @ \<pi>\<^sub>3 \<or>
       (\<exists>s s'. closed s \<and> closed s' \<and> \<pi>' = [s] \<and> \<pi>\<^sub>2 = [s'] @ \<pi>\<^sub>3 \<and> s \<noteq> s' \<and> hash s = hash s')"
     for \<pi>\<^sub>P using lemma6[OF ok(4) s_Tr(3), of thesis] by blast
     then show ?case
     proof (elim disjE conjE exE, goal_cases ok2 collision)
       case ok2
       with s_Tr(1,3-) ok show ?case
         by auto
     next
       case (collision s s')
       then show ?case
       proof (intro disjI2 exI conjI)
         from ok collision show "\<lless>[], eP\<ggreater> P\<rightarrow>i + 1 \<lless>\<pi> @ [s], eP\<^sub>3\<ggreater>"
           by (elim smallsteps.s_Tr) auto
         from ok collision show "\<pi>\<^sub>1 = \<pi> @ [s'] @ [] @ \<pi>\<^sub>3"
           by simp
       qed simp_all
     qed
   next
     case collision
     from s_Tr(3) collision show ?case
     proof (elim smallstepV_consumes_proofstream, intro disjI2 exI conjI)
       fix \<pi>\<^sub>0''
       assume *: "\<pi>\<^sub>2 = \<pi>\<^sub>0'' @ \<pi>\<^sub>3"
       from collision * show "\<pi>\<^sub>1 = \<pi>\<^sub>0 @ [s'] @ (\<pi>\<^sub>0' @ \<pi>\<^sub>0'') @ \<pi>\<^sub>3"
         by simp
     qed simp_all
   qed
 qed
 
 subsection \<open>Remark 1\<close>
 
 lemma remark1_single:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> \<pi>P, eP \<ggreater> P\<rightarrow> \<lless> \<pi>P @ \<pi>, eP' \<ggreater>"
   obtains e' eV' where "{$$} \<turnstile> e', eP', eV' : \<tau> \<and> \<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater> \<and> \<lless> \<pi>, eV \<ggreater> V\<rightarrow> \<lless> [], eV' \<ggreater>"
 proof (atomize_elim, insert assms, nominal_induct "{$$}::tyenv" e eP eV \<tau> avoiding: \<pi>P \<pi> eP' rule: agree.strong_induct)
   case (a_App e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_App(5) show ?case
   proof (cases rule: s_App_inv)
     case (App1 eP\<^sub>1')
     with a_App(2,3) show ?thesis by blast
   next
     case (App2 eP\<^sub>2')
     with a_App(1,4) show ?thesis by blast
   next
     case (AppLam x eP)
     from a_App(1)[unfolded \<open>eP\<^sub>1 = Lam x eP\<close>] show ?thesis
     proof (cases rule: a_Lam_inv_P[case_names Lam])
       case (Lam v' vV')
       with a_App(3) AppLam show ?thesis
         by (auto 0 4 simp: fresh_Pair del: s_AppLam intro!: s_AppLam lemma4)
     qed
   next
     case (AppRec x e)
     from a_App(1)[unfolded \<open>eP\<^sub>1 = Rec x e\<close>] show ?thesis
     proof (cases rule: a_Rec_inv_P[case_names _ Rec])
       case (Rec y e'' eP'' eV'')
       show ?thesis
       proof (intro exI conjI)
         let ?e = "App (Lam y (e''[Rec x (Lam y e'') / x])) e\<^sub>2"
         let ?eV = "App (Lam y (eV''[Rec x (Lam y eV'') / x])) eV\<^sub>2"
         from a_App(3) Rec AppRec show "{$$} \<turnstile> ?e, eP', ?eV : \<tau>\<^sub>2"
           by (auto intro!: agree.a_App[where \<Gamma>="{$$}"] lemma4
             simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric])
         from a_App(3) Rec AppRec show "\<lless>[], App e\<^sub>1 e\<^sub>2\<ggreater> I\<rightarrow> \<lless>[], ?e\<ggreater>"
           by (auto intro!: s_AppRec[where v=e\<^sub>2]
             simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
         from a_App(3) Rec AppRec show "\<lless>\<pi>, App eV\<^sub>1 eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>[], ?eV\<ggreater>"
           by (auto intro!: s_AppRec[where v=eV\<^sub>2]
             simp del: subst_term.simps(3) simp: subst_term.simps(3)[symmetric] fresh_Pair)
       qed
     qed simp
   qed
 next
   case (a_Let x e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   then have "atom x \<sharp> (eP\<^sub>1, \<pi>P)" by auto
   with a_Let(12) show ?case
   proof (cases rule: s_Let_inv)
     case Let1
     with a_Let show ?thesis
       by (intro exI[where P = "\<lambda>x. \<exists>y. (Q x y)" for Q, OF exI, of _ "e\<^sub>2[e\<^sub>1 / x]" "eV\<^sub>2[eV\<^sub>1 / x]"])
         (auto intro!: lemma4)
   next
     case (Let2 eP\<^sub>1')
     with a_Let(9) obtain e\<^sub>1' eV\<^sub>1'
       where ih: "{$$} \<turnstile> e\<^sub>1', eP\<^sub>1', eV\<^sub>1' : \<tau>\<^sub>1" "\<lless>[], e\<^sub>1\<ggreater> I\<rightarrow> \<lless>[], e\<^sub>1'\<ggreater>" "\<lless>\<pi>, eV\<^sub>1\<ggreater> V\<rightarrow> \<lless>[], eV\<^sub>1'\<ggreater>"
       by blast
     from a_Let Let2 have "\<not> value e\<^sub>1" "\<not> value eP\<^sub>1" "\<not> value eV\<^sub>1" by auto
     with Let2 a_Let(2,5,7,10) ih show ?thesis
       by (intro exI[where P = "\<lambda>x. \<exists>y. (Q x y)" for Q, OF exI, of _ "Let e\<^sub>1' x e\<^sub>2" "Let eV\<^sub>1' x eV\<^sub>2"])
        (fastforce simp: fresh_Pair del: agree.a_Let intro!: agree.a_Let)
   qed
 next
   case (a_Case e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau> e\<^sub>2 eP\<^sub>2 eV\<^sub>2)
   from a_Case(7) show ?case
   proof (cases rule: s_Case_inv)
     case (Case eP'')
     with a_Case(2,3,5) show ?thesis by blast
   next
     case (Inj1 v)
     with a_Case(1,3,5) show ?thesis by blast
   next
     case (Inj2 v)
     with a_Case(1,3,5) show ?thesis by blast
   qed
 next
   case (a_Prj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2 \<pi>P \<pi> eP')
   from a_Prj1(3) show ?case
   proof (cases rule: s_Prj1_inv)
     case (Prj1 eP'')
     with a_Prj1(2) show ?thesis by blast
   next
     case (PrjPair1 v\<^sub>2)
     with a_Prj1(1) show ?thesis by fastforce
   qed
 next
   case (a_Prj2 v vP vV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Prj2(3) show ?case
   proof (cases rule: s_Prj2_inv)
     case (Prj2 eP'')
     with a_Prj2(2) show ?thesis by blast
   next
     case (PrjPair2 v\<^sub>2)
     with a_Prj2(1) show ?thesis by fastforce
   qed
 next
   case (a_Roll \<alpha> e eP eV \<tau>)
   from a_Roll(7) show ?case
   proof (cases rule: s_Roll_inv)
     case (Roll eP'')
     with a_Roll(4,5,6) show ?thesis by blast
   qed
 next
   case (a_Unroll \<alpha> e eP eV \<tau>)
   from a_Unroll(7) show ?case
   proof (cases rule: s_Unroll_inv)
     case (Unroll eP'')
     with a_Unroll(5,6) show ?thesis by fastforce
   next
     case UnrollRoll
     with a_Unroll(5) show ?thesis by blast
   qed
 next
   case (a_Auth e eP eV \<tau>)
   from a_Auth(3) show ?case
   proof (cases rule: s_AuthP_inv)
     case (Auth eP'')
     with a_Auth(3) show ?thesis
       by (auto dest!: a_Auth(2)[of \<pi>P \<pi> eP''])
   next
     case AuthP
     with a_Auth(1) show ?thesis
       by (auto 0 4 simp: lemma2_1 intro: exI[of _ "Hash (hash \<lparr>eP\<rparr>)"] exI[of _ e])
   qed
 next
   case (a_Unauth e eP eV \<tau>)
   from a_Unauth(1) have eP_closed: "closed eP"
     using agree_empty_fresh by simp
   from a_Unauth(3) show ?case
   proof (cases rule: s_UnauthP_inv)
     case (Unauth e')
     with a_Unauth(2) show ?thesis
       by blast
   next
     case (UnauthP h)
     with a_Unauth(1,3) eP_closed show ?thesis
       by (force intro: a_AuthT_value_inv[OF a_Unauth(1)] simp: fresh_shallow)
   qed
 next
   case (a_Inj1 e eP eV \<tau>\<^sub>1 \<tau>\<^sub>2)
   from a_Inj1(3) show ?case
   proof (cases rule: s_Inj1_inv)
     case (Inj1 eP'')
     with a_Inj1(1,2) show ?thesis by blast
   qed
 next
   case (a_Inj2 e eP eV \<tau>\<^sub>2 \<tau>\<^sub>1)
   from a_Inj2(3) show ?case
   proof (cases rule: s_Inj2_inv)
     case (Inj2 eP'')
     with a_Inj2(1,2) show ?thesis by blast
   qed
 next
   case (a_Pair e\<^sub>1 eP\<^sub>1 eV\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 eP\<^sub>2 eV\<^sub>2 \<tau>\<^sub>2)
   from a_Pair(5) show ?case
   proof (cases rule: s_Pair_inv)
     case (Pair1 eP\<^sub>1')
     with a_Pair(1,2,3) show ?thesis by blast
   next
     case (Pair2 eP\<^sub>2')
     with a_Pair(1,3,4) show ?thesis by blast
   qed
 qed (auto dest: value_no_step)
 
 lemma remark1:
   assumes "{$$} \<turnstile> e, eP, eV : \<tau>"
   and     "\<lless> \<pi>\<^sub>P, eP \<ggreater> P\<rightarrow>i \<lless> \<pi>\<^sub>P @ \<pi>, eP' \<ggreater>"
   obtains e' eV'
   where "{$$} \<turnstile> e', eP', eV' : \<tau>" "\<lless> [], e \<ggreater> I\<rightarrow>i \<lless> [], e' \<ggreater>" "\<lless> \<pi>, eV \<ggreater> V\<rightarrow>i \<lless> [], eV' \<ggreater>"
   using assms(2,1)
 proof (atomize_elim, nominal_induct \<pi>\<^sub>P eP P i "\<pi>\<^sub>P @ \<pi>" eP' arbitrary: \<pi> rule: smallsteps.strong_induct)
   case (s_Id e \<pi>P)
   then show ?case
     using s_Id_inv by blast
 next
   case (s_Tr \<pi>\<^sub>1 eP\<^sub>1 i \<pi>\<^sub>2 eP\<^sub>2 eP\<^sub>3)
   from s_Tr obtain \<pi>' \<pi>'' where ps: "\<pi>\<^sub>2 = \<pi>\<^sub>1 @ \<pi>'" "\<pi> = \<pi>' @ \<pi>''"
     by (force elim: smallstepP_generates_proofstream smallstepsP_generates_proofstream)
   with s_Tr obtain e\<^sub>2 eV\<^sub>2 where ih: "{$$} \<turnstile> e\<^sub>2, eP\<^sub>2, eV\<^sub>2 : \<tau>"
     "\<lless>[], e\<ggreater> I\<rightarrow>i \<lless>[], e\<^sub>2\<ggreater>" "\<lless>\<pi>', eV\<ggreater> V\<rightarrow>i \<lless>[], eV\<^sub>2\<ggreater>"
     by atomize_elim (auto elim: s_Tr(2)[of \<pi>'])
   moreover
   obtain e\<^sub>3 eV\<^sub>3 where agree: "{$$} \<turnstile> e\<^sub>3, eP\<^sub>3, eV\<^sub>3 : \<tau>" and
     "\<lless>[], e\<^sub>2\<ggreater> I\<rightarrow> \<lless>[], e\<^sub>3\<ggreater>" "\<lless>\<pi>'', eV\<^sub>2\<ggreater> V\<rightarrow> \<lless>[], eV\<^sub>3\<ggreater>"
     by (rule remark1_single[OF ih(1) iffD2[OF smallstepP_ps_prepend s_Tr(3)[unfolded ps]]]) blast
   ultimately have "\<lless>[], e\<ggreater> I\<rightarrow>i + 1 \<lless>[], e\<^sub>3\<ggreater>" "\<lless>\<pi>, eV\<ggreater> V\<rightarrow>i + 1 \<lless>[], eV\<^sub>3\<ggreater>"
     by (auto simp: smallstepsV_ps_append[of _ _ _ "[]", simplified, symmetric] ps
        intro!: smallsteps.s_Tr[where m=V and \<pi>\<^sub>1="\<pi>' @ \<pi>''" and \<pi>\<^sub>2=\<pi>''])
   with agree show ?case
     by blast
 qed
 
 (*<*)
 end
 (*>*)
\ No newline at end of file
diff --git a/thys/LambdaAuth/Semantics.thy b/thys/LambdaAuth/Semantics.thy
--- a/thys/LambdaAuth/Semantics.thy
+++ b/thys/LambdaAuth/Semantics.thy
@@ -1,1140 +1,1140 @@
 (* Author: Matthias Brun,   ETH Zürich, 2019 *)
 (* Author: Dmitriy Traytel, ETH Zürich, 2019 *)
 
 section \<open>Semantics of $\lambda\bullet$\<close>
 
 (*<*)
 theory Semantics
   imports FMap_Lemmas Syntax
 begin
 (*>*)
 
 text \<open>Avoid clash with substitution notation.\<close>
 no_notation inverse_divide (infixl "'/" 70)
 
 text \<open>Help automated provers with smallsteps.\<close>
 declare One_nat_def[simp del]
 
 subsection \<open>Equivariant Hash Function\<close>
 
 consts hash_real :: "term \<Rightarrow> hash"
 
 nominal_function map_fixed :: "var \<Rightarrow> var list \<Rightarrow> term \<Rightarrow> term" where
   "map_fixed fp l Unit = Unit" |
   "map_fixed fp l (Var y) = (if y \<in> set l then (Var y) else (Var fp))" |
   "atom y \<sharp> (fp, l) \<Longrightarrow> map_fixed fp l (Lam y t) = (Lam y ((map_fixed fp (y # l) t)))" |
   "atom y \<sharp> (fp, l) \<Longrightarrow> 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 \<sharp> (fp, l) \<Longrightarrow> 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]]
   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 \<bullet> l = map (\<lambda>x. p \<bullet> x) l"
   by (induct l) auto
 
 lemma map_fixed_eqvt: "p \<bullet> l = l \<Longrightarrow> map_fixed v l (p \<bullet> 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 \<bullet> hash t = hash (p \<bullet> t)"
   unfolding permute_pure hash_def by (auto simp: map_fixed_eqvt)
 
 lemma map_fixed_idle: "{x. \<not> atom x \<sharp> t} \<subseteq> set l \<Longrightarrow> 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_inj_closed:
   "closed t \<Longrightarrow> closed u \<Longrightarrow> map_fixed undefined [] t = map_fixed undefined [] u \<Longrightarrow> t = u"
   by (erule box_equals[OF _ map_fixed_idle map_fixed_idle]) auto
 
 subsection \<open>Substitution\<close>
 
 nominal_function subst_term :: "term \<Rightarrow> term \<Rightarrow> var \<Rightarrow> term" ("_[_ '/ _]" [250, 200, 200] 250) where
   "Unit[t' / x] = Unit" |
   "(Var y)[t' / x] = (if x = y then t' else Var y)" |
   "atom y \<sharp> (x, t') \<Longrightarrow> (Lam y t)[t' / x] = Lam y (t[t' / x])" |
   "atom y \<sharp> (x, t') \<Longrightarrow> (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 \<sharp> (x, t') \<Longrightarrow> (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]]
   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 \<Rightarrow> tenv \<Rightarrow> term" where
   "psubst_term Unit f = Unit" |
   "psubst_term (Var y) f = (case f $$ y of Some t \<Rightarrow> t | None \<Rightarrow> Var y)" |
   "atom y \<sharp> f \<Longrightarrow> psubst_term (Lam y t) f = Lam y (psubst_term t f)" |
   "atom y \<sharp> f \<Longrightarrow> 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 \<sharp> f \<Longrightarrow> 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]]
   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 \<Rightarrow> ty \<Rightarrow> tvar \<Rightarrow> 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 \<sharp> (t', x) \<Longrightarrow> 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]]
   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 \<sharp> t[t' / x'] \<longleftrightarrow> (x = x' \<or> atom x \<sharp> t) \<and> (atom x' \<sharp> t \<or> atom x \<sharp> 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 \<sharp> t \<Longrightarrow> atom x \<sharp> s \<Longrightarrow> (atom (x::var)) \<sharp> t[s / y]"
   by (nominal_induct t avoiding: s y rule: term.strong_induct) (auto)
 
 lemma term_subst_idle[simp]: "atom y \<sharp> t \<Longrightarrow> 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 \<noteq> atom y2 \<Longrightarrow> atom y1 \<sharp> s2 \<Longrightarrow> 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 \<sharp> e" "atom x \<sharp> vs"
   shows   "atom x \<sharp> 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 \<alpha> \<sharp> subst_type \<tau> \<tau>' \<alpha>' \<longleftrightarrow> ((\<alpha> = \<alpha>' \<or> atom \<alpha> \<sharp> \<tau>) \<and> (atom \<alpha>' \<sharp> \<tau> \<or> atom \<alpha> \<sharp> \<tau>'))"
   by (nominal_induct \<tau> avoiding: \<alpha> \<alpha>' \<tau>' rule: ty.strong_induct) (auto simp add: fresh_at_base)
 
 lemma type_fresh_subst[simp]: "atom x \<sharp> t \<Longrightarrow> atom x \<sharp> s \<Longrightarrow> (atom (x::tvar)) \<sharp> subst_type t s y"
   by (nominal_induct t avoiding: s y rule: ty.strong_induct) (auto)
 
 lemma type_subst_idle[simp]: "atom y \<sharp> t \<Longrightarrow> 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 \<noteq> atom y2 \<Longrightarrow> atom y1 \<sharp> s2 \<Longrightarrow> 
+lemma type_subst_subst: "atom y1 \<noteq> atom y2 \<Longrightarrow> atom y1 \<sharp> s2 \<Longrightarrow>
   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 \<open>Weak Typing Judgement\<close>
 
 type_synonym tyenv = "(var, ty) fmap"
 
 inductive judge_weak :: "tyenv \<Rightarrow> term \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile>\<^sub>W _ : _" [150,0,150] 149) where
   jw_Unit:   "\<Gamma> \<turnstile>\<^sub>W Unit : One" |
   jw_Var:    "\<lbrakk> \<Gamma> $$ x = Some \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Var x : \<tau>" |
   jw_Lam:    "\<lbrakk> atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Lam x e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   jw_App:    "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile>\<^sub>W e' : \<tau>\<^sub>1 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W App e e' : \<tau>\<^sub>2" |
   jw_Let:    "\<lbrakk> atom x \<sharp> (\<Gamma>, e\<^sub>1); \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Let e\<^sub>1 x e\<^sub>2 : \<tau>\<^sub>2" |
   jw_Rec:    "\<lbrakk> atom x \<sharp> \<Gamma>; atom y \<sharp> (\<Gamma>,x); \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Rec x (Lam y e) : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   jw_Inj1:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : \<tau>\<^sub>1 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Inj1 e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   jw_Inj2:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Inj2 e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   jw_Case:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : Fun \<tau>\<^sub>2 \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Case e e\<^sub>1 e\<^sub>2 : \<tau>" |
   jw_Pair:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : \<tau>\<^sub>1; \<Gamma> \<turnstile>\<^sub>W e\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Pair e\<^sub>1 e\<^sub>2 : Prod \<tau>\<^sub>1 \<tau>\<^sub>2" |
   jw_Prj1:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Prj1 e : \<tau>\<^sub>1" |
   jw_Prj2:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Prj2 e : \<tau>\<^sub>2" |
   jw_Roll:   "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile>\<^sub>W e : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Roll e : Mu \<alpha> \<tau>" |
   jw_Unroll: "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile>\<^sub>W e : Mu \<alpha> \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Unroll e : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>" |
   jw_Auth:   "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Auth e : \<tau>" |
   jw_Unauth: "\<lbrakk> \<Gamma> \<turnstile>\<^sub>W e : \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>W Unauth e : \<tau>"
 
 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: \<alpha>
        | jw_Unroll: \<alpha>
   by (auto simp: fresh_subst_type fresh_Pair)
 
 text \<open>Inversion rules for typing judgment.\<close>
 
 inductive_cases jw_Unit_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Unit : \<tau>"
 inductive_cases jw_Var_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Var x : \<tau>"
 
 lemma jw_Lam_inv[elim]:
   assumes "\<Gamma> \<turnstile>\<^sub>W Lam x e : \<tau>"
   and     "atom x \<sharp> \<Gamma>"
   obtains \<tau>\<^sub>1 \<tau>\<^sub>2 where "\<tau> = Fun \<tau>\<^sub>1 \<tau>\<^sub>2" "(\<Gamma>(x $$:= \<tau>\<^sub>1)) \<turnstile>\<^sub>W e : \<tau>\<^sub>2"
   using assms proof (atomize_elim, nominal_induct \<Gamma> "Lam x e" \<tau> avoiding: x e rule: judge_weak.strong_induct)
   case (jw_Lam x \<Gamma> \<tau>\<^sub>1 t \<tau>\<^sub>2 y u)
   then show ?case
     by (auto simp: perm_supp_eq elim!:
         iffD1[OF Abs_lst1_fcb2'[where f = "\<lambda>x t (\<Gamma>, \<tau>\<^sub>1, \<tau>\<^sub>2). (\<Gamma>(x $$:= \<tau>\<^sub>1)) \<turnstile>\<^sub>W t : \<tau>\<^sub>2"
         and c = "(\<Gamma>, \<tau>\<^sub>1, \<tau>\<^sub>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 \<sharp> \<pi> \<Longrightarrow> atom y \<sharp> \<pi> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> \<pi> \<bullet> (x \<leftrightarrow> y) \<bullet> t = \<pi> \<bullet> t"
   by (subst permute_eqvt) (auto simp: flip_fresh_fresh)
 
 lemma jw_Rec_inv[elim]:
   assumes "\<Gamma> \<turnstile>\<^sub>W Rec x t : \<tau>"
   and     "atom x \<sharp> \<Gamma>"
   obtains y e \<tau>\<^sub>1 \<tau>\<^sub>2 where "atom y \<sharp> (\<Gamma>,x)" "t = Lam y e" "\<tau> = Fun \<tau>\<^sub>1 \<tau>\<^sub>2" "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
   using [[simproc del: alpha_lst]] assms
 proof (atomize_elim, nominal_induct \<Gamma> "Rec x t" \<tau> avoiding: x t rule: judge_weak.strong_induct)
   case (jw_Rec x \<Gamma> y \<tau>\<^sub>1 \<tau>\<^sub>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 \<sharp> (\<Gamma>, z)" by simp
       from Lam.hyps(1-3) Lam.prems show "Lam y' e' = Lam y ((y' \<leftrightarrow> y) \<bullet> 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 "\<Gamma>(z $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile>\<^sub>W Lam y ((y' \<leftrightarrow> y) \<bullet> e') : Fun \<tau>\<^sub>1 \<tau>\<^sub>2"
         by (elim judge_weak.eqvt[of "\<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2)" "Lam y e" "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" "(x \<leftrightarrow> 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]: "\<Gamma> \<turnstile>\<^sub>W Inj1 e : \<tau>"
 inductive_cases jw_Inj2_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Inj2 e : \<tau>"
 inductive_cases jw_Pair_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Pair e\<^sub>1 e\<^sub>2 : \<tau>"
 
 lemma jw_Let_inv[elim]:
   assumes "\<Gamma> \<turnstile>\<^sub>W Let e\<^sub>1 x e\<^sub>2 : \<tau>\<^sub>2"
   and     "atom x \<sharp> (e\<^sub>1, \<Gamma>)"
   obtains \<tau>\<^sub>1 where "\<Gamma> \<turnstile>\<^sub>W e\<^sub>1 : \<tau>\<^sub>1" "\<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W e\<^sub>2 : \<tau>\<^sub>2"
 using assms proof (atomize_elim, nominal_induct \<Gamma> "Let e\<^sub>1 x e\<^sub>2" \<tau>\<^sub>2 avoiding: e\<^sub>1 x e\<^sub>2 rule: judge_weak.strong_induct)
   case (jw_Let x \<Gamma> e\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 \<tau>\<^sub>2 x' e\<^sub>2')
   then show ?case
     by (auto simp: fresh_Pair perm_supp_eq elim!:
         iffD1[OF Abs_lst1_fcb2'[where f = "\<lambda>x t (\<Gamma>, \<tau>\<^sub>1, \<tau>\<^sub>2). \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile>\<^sub>W t : \<tau>\<^sub>2"
         and c = "(\<Gamma>, \<tau>\<^sub>1, \<tau>\<^sub>2)" and a = x and b = x' and x = e\<^sub>2 and y = e\<^sub>2', unfolded prod.case],
         rotated -1])
 qed
 
 inductive_cases jw_Prj1_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Prj1 e : \<tau>\<^sub>1"
 inductive_cases jw_Prj2_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Prj2 e : \<tau>\<^sub>2"
 inductive_cases jw_App_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W App e e' : \<tau>\<^sub>2"
 inductive_cases jw_Case_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Case e e\<^sub>1 e\<^sub>2 : \<tau>"
 inductive_cases jw_Auth_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Auth e : \<tau>"
 inductive_cases jw_Unauth_inv[elim]: "\<Gamma> \<turnstile>\<^sub>W Unauth e : \<tau>"
 
 lemma subst_type_perm_eq:
   assumes "atom b \<sharp> t"
   shows   "subst_type t (Mu a t) a = subst_type ((a \<leftrightarrow> b) \<bullet> t) (Mu b ((a \<leftrightarrow> b) \<bullet> t)) b"
   using assms proof -
   have f: "atom a \<sharp> subst_type t (Mu a t) a" by (rule iffD2[OF fresh_subst_type]) simp
   have    "atom b \<sharp> subst_type t (Mu a t) a" by (auto simp: assms)
   with f have "subst_type t (Mu a t) a = (a \<leftrightarrow> b) \<bullet> 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 \<leftrightarrow> b) \<bullet> t) (Mu b ((a \<leftrightarrow> b) \<bullet> t)) b"
     by simp
 qed
 
 lemma jw_Roll_inv[elim]:
   assumes "\<Gamma> \<turnstile>\<^sub>W Roll e : \<tau>"
   and     "atom \<alpha> \<sharp> (\<Gamma>, \<tau>)"
   obtains \<tau>' where "\<tau> = Mu \<alpha> \<tau>'" "\<Gamma> \<turnstile>\<^sub>W e : subst_type \<tau>' (Mu \<alpha> \<tau>') \<alpha>"
   using assms [[simproc del: alpha_lst]]
   proof (atomize_elim, nominal_induct \<Gamma> "Roll e" \<tau> avoiding: e \<alpha> rule: judge_weak.strong_induct)
   case (jw_Roll \<alpha> \<Gamma> e \<tau> \<alpha>')
   then show ?case
     by (auto simp: perm_supp_eq fresh_Pair fresh_at_base subst_type.eqvt
       intro!: exI[of _ "(\<alpha> \<leftrightarrow> \<alpha>') \<bullet> \<tau>"] Abs_lst_eq_flipI dest: judge_weak.eqvt[of _ _ _ "(\<alpha> \<leftrightarrow> \<alpha>')"])
 qed
 
 lemma jw_Unroll_inv[elim]:
   assumes "\<Gamma> \<turnstile>\<^sub>W Unroll e : \<tau>"
   and     "atom \<alpha> \<sharp> (\<Gamma>, \<tau>)"
   obtains \<tau>' where "\<tau> = subst_type \<tau>' (Mu \<alpha> \<tau>') \<alpha>" "\<Gamma> \<turnstile>\<^sub>W e : Mu \<alpha> \<tau>'"
   using assms proof (atomize_elim, nominal_induct \<Gamma> "Unroll e" \<tau> avoiding: e \<alpha> rule: judge_weak.strong_induct)
   case (jw_Unroll \<alpha> \<Gamma> e \<tau> \<alpha>')
   then show ?case
     by (auto simp: perm_supp_eq fresh_Pair subst_type_perm_eq fresh_subst_type
       intro!: exI[of _ "(\<alpha> \<leftrightarrow> \<alpha>') \<bullet> \<tau>"] dest: judge_weak.eqvt[of _ _ _ "(\<alpha> \<leftrightarrow> \<alpha>')"])
 qed
 
 text \<open>Additional inversion rules based on type rather than term.\<close>
 
 inductive_cases jw_Prod_inv[elim]: "{$$} \<turnstile>\<^sub>W e : Prod \<tau>\<^sub>1 \<tau>\<^sub>2"
 inductive_cases jw_Sum_inv[elim]: "{$$} \<turnstile>\<^sub>W e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2"
 
 lemma jw_Fun_inv[elim]:
   assumes "{$$} \<turnstile>\<^sub>W v : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" "value v"
   obtains e x where "v = Lam x e \<or> v = Rec x e" "atom x \<sharp> (c::term)"
   using assms [[simproc del: alpha_lst]]
 proof (atomize_elim, nominal_induct "{$$} :: tyenv" v "Fun \<tau>\<^sub>1 \<tau>\<^sub>2" avoiding: \<tau>\<^sub>1 \<tau>\<^sub>2 rule: judge_weak.strong_induct)
   case (jw_Lam x \<tau>\<^sub>1 e \<tau>\<^sub>2)
   then obtain x' where "atom (x'::var) \<sharp> (c, e)" using finite_supp obtain_fresh' by blast
   then have "[[atom x]]lst. e = [[atom x']]lst. (x \<leftrightarrow> x') \<bullet> e \<and> atom x' \<sharp> c"
     by (simp add: Abs_lst_eq_flipI fresh_Pair)
   then show ?case
     by auto
 next
   case (jw_Rec x y \<tau>\<^sub>1 \<tau>\<^sub>2 e')
   obtain x' where "atom (x'::var) \<sharp> (c, Lam y e')" using finite_supp obtain_fresh by blast
   then have "[[atom x]]lst. Lam y e' = [[atom x']]lst. (x \<leftrightarrow> x') \<bullet> (Lam y e') \<and> atom x' \<sharp> c"
     using Abs_lst_eq_flipI fresh_Pair by blast
   then show ?case
     by auto
 qed simp_all
 
 lemma jw_Mu_inv[elim]:
   assumes "{$$} \<turnstile>\<^sub>W v : Mu \<alpha> \<tau>" "value v"
   obtains v' where "v = Roll v'"
   using assms by (atomize_elim, nominal_induct "{$$} :: tyenv" v "Mu \<alpha> \<tau>" rule: judge_weak.strong_induct) simp_all
 
 
 subsection \<open>Erasure of Authenticated Types\<close>
 
 nominal_function erase :: "ty \<Rightarrow> ty" where
   "erase One = One" |
   "erase (Fun \<tau>\<^sub>1 \<tau>\<^sub>2) = Fun (erase \<tau>\<^sub>1) (erase \<tau>\<^sub>2)" |
   "erase (Sum \<tau>\<^sub>1 \<tau>\<^sub>2) = Sum (erase \<tau>\<^sub>1) (erase \<tau>\<^sub>2)" |
   "erase (Prod \<tau>\<^sub>1 \<tau>\<^sub>2) = Prod (erase \<tau>\<^sub>1) (erase \<tau>\<^sub>2)" |
   "erase (Mu \<alpha> \<tau>) = Mu \<alpha> (erase \<tau>)" |
   "erase (Alpha \<alpha>) = Alpha \<alpha>" |
   "erase (AuthT \<tau>) = erase \<tau>"
   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 \<sharp> \<tau>"
   shows   "atom x \<sharp> erase \<tau>"
   using assms by (induct \<tau> rule: ty.induct) auto
 
 lemma fresh_fmmap_erase_fresh:
   assumes "atom x \<sharp> \<Gamma>"
   shows   "atom x \<sharp> fmmap erase \<Gamma>"
   using assms by transfer simp
 
 lemma erase_subst_type_shift[simp]:
   "erase (subst_type \<tau> \<tau>' \<alpha>) = subst_type (erase \<tau>) (erase \<tau>') \<alpha>"
   by (induct \<tau> \<tau>' \<alpha> rule: subst_type.induct) (auto simp: fresh_Pair fresh_erase_fresh)
 
 definition erase_env :: "tyenv \<Rightarrow> tyenv" where
   "erase_env = fmmap erase"
 
 subsection \<open>Strong Typing Judgement\<close>
 
 inductive judge :: "tyenv \<Rightarrow> term \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [150,0,150] 149) where
   j_Unit:   "\<Gamma> \<turnstile> Unit : One" |
   j_Var:    "\<lbrakk> \<Gamma> $$ x = Some \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>" |
   j_Lam:    "\<lbrakk> atom x \<sharp> \<Gamma>; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Lam x e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   j_App:    "\<lbrakk> \<Gamma> \<turnstile> e : Fun \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile> e' : \<tau>\<^sub>1 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> App e e' : \<tau>\<^sub>2" |
   j_Let:    "\<lbrakk> atom x \<sharp> (\<Gamma>, e\<^sub>1); \<Gamma> \<turnstile> e\<^sub>1 : \<tau>\<^sub>1; \<Gamma>(x $$:= \<tau>\<^sub>1) \<turnstile> e\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Let e\<^sub>1 x e\<^sub>2 : \<tau>\<^sub>2" |
   j_Rec:    "\<lbrakk> atom x \<sharp> \<Gamma>; atom y \<sharp> (\<Gamma>,x); \<Gamma>(x $$:= Fun \<tau>\<^sub>1 \<tau>\<^sub>2) \<turnstile> Lam y e' : Fun \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Rec x (Lam y e') : Fun \<tau>\<^sub>1 \<tau>\<^sub>2" |
   j_Inj1:   "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>\<^sub>1 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Inj1 e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   j_Inj2:   "\<lbrakk> \<Gamma> \<turnstile> e : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Inj2 e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2" |
   j_Case:   "\<lbrakk> \<Gamma> \<turnstile> e : Sum \<tau>\<^sub>1 \<tau>\<^sub>2; \<Gamma> \<turnstile> e\<^sub>1 : Fun \<tau>\<^sub>1 \<tau>; \<Gamma> \<turnstile> e\<^sub>2 : Fun \<tau>\<^sub>2 \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Case e e\<^sub>1 e\<^sub>2 : \<tau>" |
   j_Pair:   "\<lbrakk> \<Gamma> \<turnstile> e\<^sub>1 : \<tau>\<^sub>1; \<Gamma> \<turnstile> e\<^sub>2 : \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Pair e\<^sub>1 e\<^sub>2 : Prod \<tau>\<^sub>1 \<tau>\<^sub>2" |
   j_Prj1:   "\<lbrakk> \<Gamma> \<turnstile> e : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Prj1 e : \<tau>\<^sub>1" |
   j_Prj2:   "\<lbrakk> \<Gamma> \<turnstile> e : Prod \<tau>\<^sub>1 \<tau>\<^sub>2 \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Prj2 e : \<tau>\<^sub>2" |
   j_Roll:   "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile> e : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Roll e : Mu \<alpha> \<tau>" |
   j_Unroll: "\<lbrakk> atom \<alpha> \<sharp> \<Gamma>; \<Gamma> \<turnstile> e : Mu \<alpha> \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Unroll e : subst_type \<tau> (Mu \<alpha> \<tau>) \<alpha>" |
   j_Auth:   "\<lbrakk> \<Gamma> \<turnstile> e : \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Auth e : AuthT \<tau>" |
   j_Unauth: "\<lbrakk> \<Gamma> \<turnstile> e : AuthT \<tau> \<rbrakk>
            \<Longrightarrow> \<Gamma> \<turnstile> Unauth e : \<tau>"
 
 declare judge.intros[intro]
 
 equivariance judge
 nominal_inductive judge
   avoids j_Lam: x
        | j_Rec: x and y
        | j_Let: x
        | j_Roll: \<alpha>
        | j_Unroll: \<alpha>
   by (auto simp: fresh_subst_type fresh_Pair)
 
 lemma judge_imp_judge_weak:
   assumes "\<Gamma> \<turnstile> e : \<tau>"
   shows   "erase_env \<Gamma> \<turnstile>\<^sub>W e : erase \<tau>"
   using assms unfolding erase_env_def
   by (induct \<Gamma> e \<tau> rule: judge.induct) (simp_all add: fresh_Pair fresh_fmmap_erase_fresh fmmap_fmupd)
 
 subsection \<open>Shallow Projection\<close>
 
 nominal_function shallow :: "term \<Rightarrow> term" ("\<lparr>_\<rparr>") where
   "\<lparr>Unit\<rparr>  = Unit" |
   "\<lparr>Var v\<rparr> = Var v" |
   "\<lparr>Lam x e\<rparr> = Lam x \<lparr>e\<rparr>" |
   "\<lparr>Rec x e\<rparr> = Rec x \<lparr>e\<rparr>" |
   "\<lparr>Inj1 e\<rparr> = Inj1 \<lparr>e\<rparr>" |
   "\<lparr>Inj2 e\<rparr> = Inj2 \<lparr>e\<rparr>" |
   "\<lparr>Pair e\<^sub>1 e\<^sub>2\<rparr> = Pair \<lparr>e\<^sub>1\<rparr> \<lparr>e\<^sub>2\<rparr>" |
   "\<lparr>Roll e\<rparr> = Roll \<lparr>e\<rparr>" |
   "\<lparr>Let e\<^sub>1 x e\<^sub>2\<rparr> = Let \<lparr>e\<^sub>1\<rparr> x \<lparr>e\<^sub>2\<rparr>" |
   "\<lparr>App e\<^sub>1 e\<^sub>2\<rparr> = App \<lparr>e\<^sub>1\<rparr> \<lparr>e\<^sub>2\<rparr>" |
   "\<lparr>Case e e\<^sub>1 e\<^sub>2\<rparr> = Case \<lparr>e\<rparr> \<lparr>e\<^sub>1\<rparr> \<lparr>e\<^sub>2\<rparr>" |
   "\<lparr>Prj1 e\<rparr> = Prj1 \<lparr>e\<rparr>" |
   "\<lparr>Prj2 e\<rparr> = Prj2 \<lparr>e\<rparr>" |
   "\<lparr>Unroll e\<rparr> = Unroll \<lparr>e\<rparr>" |
   "\<lparr>Auth e\<rparr> = Auth \<lparr>e\<rparr>" |
   "\<lparr>Unauth e\<rparr> = Unauth \<lparr>e\<rparr>" |
   \<comment> \<open>No rule is defined for Hash, but: "[..] preserving that structure in every case but that of <h, v> [..]"\<close>
   "\<lparr>Hash h\<rparr> = Hash h" |
   "\<lparr>Hashed h e\<rparr> = 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 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
 
 lemma fresh_shallow: "atom x \<sharp> e \<Longrightarrow> atom x \<sharp> \<lparr>e\<rparr>"
   by (induct e rule: term.induct) auto
 
 subsection \<open>Small-step Semantics\<close>
 
 datatype mode = I | P | V \<comment> \<open>Ideal, Prover and Verifier modes\<close>
 
 instantiation mode :: pure
 begin
 definition permute_mode :: "perm \<Rightarrow> mode \<Rightarrow> mode" where
   "permute_mode \<pi> h = h"
 instance proof qed (auto simp: permute_mode_def)
 end
 
 type_synonym proofstream = "term list"
 
 inductive smallstep :: "proofstream \<Rightarrow> term \<Rightarrow> mode \<Rightarrow> proofstream \<Rightarrow> term \<Rightarrow> bool" ("\<lless>_, _\<ggreater> _\<rightarrow> \<lless>_, _\<ggreater>") where
   s_App1:      "\<lbrakk> \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, App e\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', App e\<^sub>1' e\<^sub>2 \<ggreater>" |
   s_App2:      "\<lbrakk> value v\<^sub>1; \<lless> \<pi>, e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>2' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, App v\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', App v\<^sub>1 e\<^sub>2' \<ggreater>" |
   s_AppLam:    "\<lbrakk> value v; atom x \<sharp> (v,\<pi>) \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, App (Lam x e) v \<ggreater>  _\<rightarrow>  \<lless> \<pi>, e[v / x] \<ggreater>" |
   s_AppRec:    "\<lbrakk> value v; atom x \<sharp> (v,\<pi>) \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, App (Rec x e) v \<ggreater>  _\<rightarrow>  \<lless> \<pi>, App (e[(Rec x e) / x]) v \<ggreater>" |
   s_Let1:      "\<lbrakk> atom x \<sharp> (e\<^sub>1,e\<^sub>1',\<pi>,\<pi>'); \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Let e\<^sub>1 x e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Let e\<^sub>1' x e\<^sub>2 \<ggreater>" |
   s_Let2:      "\<lbrakk> value v; atom x \<sharp> (v,\<pi>) \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Let v x e \<ggreater>  _\<rightarrow>  \<lless> \<pi>, e[v / x] \<ggreater>" |
   s_Inj1:      "\<lbrakk> \<lless> \<pi>, e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Inj1 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Inj1 e' \<ggreater>" |
   s_Inj2:      "\<lbrakk> \<lless> \<pi>, e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Inj2 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Inj2 e' \<ggreater>" |
   s_Case:      "\<lbrakk> \<lless> \<pi>, e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Case e e\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Case e' e\<^sub>1 e\<^sub>2 \<ggreater>" |
   \<comment> \<open>Case rules are different from paper to account for recursive functions.\<close>
   s_CaseInj1:  "\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Case (Inj1 v) e\<^sub>1 e\<^sub>2 \<ggreater>  _\<rightarrow>  \<lless> \<pi>, App e\<^sub>1 v \<ggreater>" |
   s_CaseInj2:  "\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Case (Inj2 v) e\<^sub>1 e\<^sub>2 \<ggreater>  _\<rightarrow>  \<lless> \<pi>, App e\<^sub>2 v \<ggreater>" |
   s_Pair1:     "\<lbrakk> \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Pair e\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Pair e\<^sub>1' e\<^sub>2 \<ggreater>" |
   s_Pair2:     "\<lbrakk> value v\<^sub>1; \<lless> \<pi>, e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>2' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Pair v\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Pair v\<^sub>1 e\<^sub>2' \<ggreater>" |
   s_Prj1:      "\<lbrakk> \<lless> \<pi>, e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Prj1 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Prj1 e' \<ggreater>" |
   s_Prj2:      "\<lbrakk> \<lless> \<pi>, e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater> \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Prj2 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Prj2 e' \<ggreater>" |
   s_PrjPair1:  "\<lbrakk> value v\<^sub>1; value v\<^sub>2 \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Prj1 (Pair v\<^sub>1 v\<^sub>2) \<ggreater>  _\<rightarrow>  \<lless> \<pi>, v\<^sub>1 \<ggreater>" |
   s_PrjPair2:  "\<lbrakk> value v\<^sub>1; value v\<^sub>2 \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Prj2 (Pair v\<^sub>1 v\<^sub>2) \<ggreater>  _\<rightarrow>  \<lless> \<pi>, v\<^sub>2 \<ggreater>" |
   s_Unroll:    "\<lless> \<pi>, e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>
               \<Longrightarrow> \<lless> \<pi>, Unroll e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Unroll e' \<ggreater>" |
   s_Roll:      "\<lless> \<pi>, e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>
               \<Longrightarrow> \<lless> \<pi>, Roll e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', Roll e' \<ggreater>" |
   s_UnrollRoll:"\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Unroll (Roll v) \<ggreater>  _\<rightarrow>  \<lless> \<pi>, v \<ggreater>" |
   \<comment> \<open>Mode-specific rules\<close>
   s_Auth:      "\<lless> \<pi>, e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>
               \<Longrightarrow> \<lless> \<pi>, Auth e \<ggreater> m\<rightarrow> \<lless> \<pi>', Auth e' \<ggreater>" |
   s_Unauth:    "\<lless> \<pi>, e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>
               \<Longrightarrow> \<lless> \<pi>, Unauth e \<ggreater> m\<rightarrow> \<lless> \<pi>', Unauth e' \<ggreater>" |
   s_AuthI:     "\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Auth v \<ggreater> I\<rightarrow> \<lless> \<pi>, v \<ggreater>" |
   s_UnauthI:   "\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Unauth v \<ggreater> I\<rightarrow> \<lless> \<pi>, v \<ggreater>" |
   s_AuthP:     "\<lbrakk> closed \<lparr>v\<rparr>; value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Auth v \<ggreater> P\<rightarrow> \<lless> \<pi>, Hashed (hash \<lparr>v\<rparr>) v \<ggreater>" |
   s_UnauthP:   "\<lbrakk> value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Unauth (Hashed h v) \<ggreater> P\<rightarrow> \<lless> \<pi> @ [\<lparr>v\<rparr>], v \<ggreater>" |
   s_AuthV:     "\<lbrakk> closed v; value v \<rbrakk>
               \<Longrightarrow> \<lless> \<pi>, Auth v \<ggreater> V\<rightarrow> \<lless> \<pi>, Hash (hash v) \<ggreater>" |
   s_UnauthV:   "\<lbrakk> closed s\<^sub>0; hash s\<^sub>0 = h \<rbrakk>
               \<Longrightarrow> \<lless> s\<^sub>0#\<pi>, Unauth (Hash h) \<ggreater> V\<rightarrow> \<lless> \<pi>, s\<^sub>0 \<ggreater>"
 
 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 \<Rightarrow> term \<Rightarrow> mode \<Rightarrow> nat \<Rightarrow> proofstream \<Rightarrow> term \<Rightarrow> bool" ("\<lless>_, _\<ggreater> _\<rightarrow>_ \<lless>_, _\<ggreater>") where
   s_Id: "\<lless> \<pi>, e \<ggreater> _\<rightarrow>0 \<lless> \<pi>, e \<ggreater>" |
   s_Tr: "\<lbrakk> \<lless> \<pi>\<^sub>1, e\<^sub>1 \<ggreater> m\<rightarrow>i \<lless> \<pi>\<^sub>2, e\<^sub>2 \<ggreater>; \<lless> \<pi>\<^sub>2, e\<^sub>2 \<ggreater> m\<rightarrow> \<lless> \<pi>\<^sub>3, e\<^sub>3 \<ggreater> \<rbrakk>
        \<Longrightarrow> \<lless> \<pi>\<^sub>1, e\<^sub>1 \<ggreater> m\<rightarrow>(i+1) \<lless> \<pi>\<^sub>3, e\<^sub>3 \<ggreater>"
 
 declare smallsteps.intros[simp]
 declare smallsteps.intros[intro]
 
 equivariance smallsteps
 nominal_inductive smallsteps .
 
 lemma steps_1_step[simp]: "\<lless> \<pi>, e \<ggreater> m\<rightarrow>1 \<lless> \<pi>', e' \<ggreater> = \<lless> \<pi>, e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>" (is "?L \<longleftrightarrow> ?R")
 proof
   assume ?L
   then show ?R
   proof (induct \<pi> e m "1::nat" \<pi>' e' rule: smallsteps.induct)
     case (s_Tr \<pi>\<^sub>1 e\<^sub>1 m i \<pi>\<^sub>2 e\<^sub>2 \<pi>\<^sub>3 e\<^sub>3)
     then show ?case
       by (induct \<pi>\<^sub>1 e\<^sub>1 m i \<pi>\<^sub>2 e\<^sub>2 rule: smallsteps.induct) auto
   qed simp
 qed (auto intro: s_Tr[where i=0, simplified])
 
 text \<open>Inversion rules for smallstep(s) predicates.\<close>
 
 lemma value_no_step[intro]:
   assumes "\<lless> \<pi>\<^sub>1, v \<ggreater> m\<rightarrow> \<lless> \<pi>\<^sub>2, t \<ggreater>" "value v"
   shows   "False"
   using assms by (induct \<pi>\<^sub>1 v m \<pi>\<^sub>2 t rule: smallstep.induct) auto
 
 lemma subst_term_perm:
   assumes "atom x' \<sharp> (x, e)"
   shows "e[v / x] = ((x \<leftrightarrow> x') \<bullet> 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]: "\<lless> \<pi>\<^sub>1, Unit \<ggreater>  m\<rightarrow>  \<lless> \<pi>\<^sub>2, v \<ggreater>"
 
 inductive_cases s_App_inv[consumes 1, case_names App1 App2 AppLam AppRec, elim]: "\<lless> \<pi>, App v\<^sub>1 v\<^sub>2 \<ggreater> m\<rightarrow> \<lless> \<pi>', e \<ggreater>"
 
 lemma s_Let_inv':
   assumes "\<lless> \<pi>, Let e\<^sub>1 x e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
   and     "atom x \<sharp> (e\<^sub>1,\<pi>)"
   obtains e\<^sub>1' where "(e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>') \<or> (\<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<and> e' = Let e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1)"
   using assms [[simproc del: alpha_lst]]
   by (atomize_elim, induct \<pi> "Let e\<^sub>1 x e\<^sub>2" m \<pi>' 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 "\<lless> \<pi>, Let e\<^sub>1 x e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
   and     "atom x \<sharp> (e\<^sub>1,\<pi>)"
   and     "e' = e\<^sub>2[e\<^sub>1 / x] \<and> value e\<^sub>1 \<and> \<pi> = \<pi>' \<Longrightarrow> Q"
   and     "\<And>e\<^sub>1'. \<lless> \<pi>, e\<^sub>1 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e\<^sub>1' \<ggreater> \<and> e' = Let e\<^sub>1' x e\<^sub>2 \<and> \<not> value e\<^sub>1 \<Longrightarrow> Q"
   shows   "Q"
   using assms by (auto elim: s_Let_inv')
 
 inductive_cases s_Case_inv[consumes 1, case_names Case Inj1 Inj2, elim]:
   "\<lless> \<pi>, Case e e\<^sub>1 e\<^sub>2 \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_Prj1_inv[consumes 1, case_names Prj1 PrjPair1, elim]:
   "\<lless> \<pi>, Prj1 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', v \<ggreater>"
 inductive_cases s_Prj2_inv[consumes 1, case_names Prj2 PrjPair2, elim]:
   "\<lless> \<pi>, Prj2 e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', v \<ggreater>"
 inductive_cases s_Pair_inv[consumes 1, case_names Pair1 Pair2, elim]:
   "\<lless> \<pi>, Pair e\<^sub>1 e\<^sub>2 \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_Inj1_inv[consumes 1, case_names Inj1, elim]:
   "\<lless> \<pi>, Inj1 e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_Inj2_inv[consumes 1, case_names Inj2, elim]:
   "\<lless> \<pi>, Inj2 e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_Roll_inv[consumes 1, case_names Roll, elim]:
   "\<lless> \<pi>, Roll e \<ggreater> m\<rightarrow> \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_Unroll_inv[consumes 1, case_names Unroll UnrollRoll, elim]:
   "\<lless> \<pi>, Unroll e \<ggreater>  m\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_AuthI_inv[consumes 1, case_names Auth AuthI, elim]:
   "\<lless> \<pi>, Auth e \<ggreater>  I\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_UnauthI_inv[consumes 1, case_names Unauth UnauthI, elim]:
   "\<lless> \<pi>, Unauth e \<ggreater>  I\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_AuthP_inv[consumes 1, case_names Auth AuthP, elim]:
   "\<lless> \<pi>, Auth e \<ggreater>  P\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_UnauthP_inv[consumes 1, case_names Unauth UnauthP, elim]:
   "\<lless> \<pi>, Unauth e \<ggreater>  P\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_AuthV_inv[consumes 1, case_names Auth AuthV, elim]:
   "\<lless> \<pi>, Auth e \<ggreater>  V\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 inductive_cases s_UnauthV_inv[consumes 1, case_names Unauth UnauthV, elim]:
   "\<lless> \<pi>, Unauth e \<ggreater>  V\<rightarrow>  \<lless> \<pi>', e' \<ggreater>"
 
 inductive_cases s_Id_inv[elim]: "\<lless> \<pi>\<^sub>1, e\<^sub>1 \<ggreater> m\<rightarrow>0 \<lless> \<pi>\<^sub>2, e\<^sub>2 \<ggreater>"
 inductive_cases s_Tr_inv[elim]: "\<lless> \<pi>\<^sub>1, e\<^sub>1 \<ggreater> m\<rightarrow>i \<lless> \<pi>\<^sub>3, e\<^sub>3 \<ggreater>"
 
 text \<open>Freshness with smallstep.\<close>
 
 lemma fresh_smallstep_I:
   fixes x :: var
   assumes "\<lless> \<pi>, e \<ggreater> I\<rightarrow> \<lless> \<pi>', e' \<ggreater>" "atom x \<sharp> e"
   shows   "atom x \<sharp> e'"
   using assms by (induct \<pi> e I \<pi>' e' rule: smallstep.induct) (auto simp: fresh_subst_term)
 
 lemma fresh_smallstep_P:
   fixes x :: var
   assumes "\<lless> \<pi>, e \<ggreater> P\<rightarrow> \<lless> \<pi>', e' \<ggreater>" "atom x \<sharp> e"
   shows   "atom x \<sharp> e'"
   using assms by (induct \<pi> e P \<pi>' e' rule: smallstep.induct) (auto simp: fresh_subst_term)
 
 lemma fresh_smallsteps_I:
   fixes x :: var
   assumes "\<lless> \<pi>, e \<ggreater> I\<rightarrow>i \<lless> \<pi>', e' \<ggreater>" "atom x \<sharp> e"
   shows   "atom x \<sharp> e'"
   using assms by (induct \<pi> e I i \<pi>' e' rule: smallsteps.induct) (simp_all add: fresh_smallstep_I)
 
 lemma fresh_ps_smallstep_P:
   fixes x :: var
   assumes "\<lless> \<pi>, e \<ggreater> P\<rightarrow> \<lless> \<pi>', e' \<ggreater>" "atom x \<sharp> e" "atom x \<sharp> \<pi>"
   shows   "atom x \<sharp> \<pi>'"
   using assms proof (induct \<pi> e P \<pi>' e' rule: smallstep.induct)
   case (s_UnauthP v \<pi> h)
   then show ?case
     by (simp add: fresh_Cons fresh_append fresh_shallow)
   qed auto
 
 text \<open>Proofstream lemmas.\<close>
 
 lemma smallstepI_ps_eq:
   assumes "\<lless> \<pi>, e \<ggreater> I\<rightarrow> \<lless> \<pi>', e' \<ggreater>"
   shows   "\<pi> = \<pi>'"
   using assms by (induct \<pi> e I \<pi>' e' rule: smallstep.induct) auto
 
 lemma smallstepI_ps_emptyD:
   "\<lless>\<pi>, e\<ggreater> I\<rightarrow> \<lless>[], e'\<ggreater> \<Longrightarrow> \<lless>[], e\<ggreater> I\<rightarrow> \<lless>[], e'\<ggreater>"
   "\<lless>[], e\<ggreater> I\<rightarrow> \<lless>\<pi>, e'\<ggreater> \<Longrightarrow> \<lless>[], e\<ggreater> I\<rightarrow> \<lless>[], e'\<ggreater>"
   using smallstepI_ps_eq by force+
 
 lemma smallstepsI_ps_eq:
   assumes "\<lless>\<pi>, e\<ggreater> I\<rightarrow>i \<lless>\<pi>', e'\<ggreater>"
   shows   "\<pi> = \<pi>'"
   using assms by (induct \<pi> e I i \<pi>' e' rule: smallsteps.induct) (auto dest: smallstepI_ps_eq)
 
 lemma smallstepsI_ps_emptyD:
   "\<lless>\<pi>, e\<ggreater> I\<rightarrow>i \<lless>[], e'\<ggreater> \<Longrightarrow> \<lless>[], e\<ggreater> I\<rightarrow>i \<lless>[], e'\<ggreater>"
   "\<lless>[], e\<ggreater> I\<rightarrow>i \<lless>\<pi>, e'\<ggreater> \<Longrightarrow> \<lless>[], e\<ggreater> I\<rightarrow>i \<lless>[], e'\<ggreater>"
   using smallstepsI_ps_eq by force+
 
 lemma smallstepV_consumes_proofstream:
   assumes "\<lless> \<pi>\<^sub>1, eV \<ggreater> V\<rightarrow> \<lless> \<pi>\<^sub>2, eV' \<ggreater>"
   obtains \<pi> where "\<pi>\<^sub>1 = \<pi> @ \<pi>\<^sub>2"
   using assms by (induct \<pi>\<^sub>1 eV V \<pi>\<^sub>2 eV' rule: smallstep.induct) auto
 
 lemma smallstepsV_consumes_proofstream:
   assumes "\<lless> \<pi>\<^sub>1, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>\<^sub>2, eV' \<ggreater>"
   obtains \<pi> where "\<pi>\<^sub>1 = \<pi> @ \<pi>\<^sub>2"
   using assms by (induct \<pi>\<^sub>1 eV V i \<pi>\<^sub>2 eV' rule: smallsteps.induct)
                  (auto elim: smallstepV_consumes_proofstream)
 
 lemma smallstepP_generates_proofstream:
   assumes "\<lless> \<pi>\<^sub>1, eP \<ggreater> P\<rightarrow> \<lless> \<pi>\<^sub>2, eP' \<ggreater>"
   obtains \<pi> where "\<pi>\<^sub>2 = \<pi>\<^sub>1 @ \<pi>"
   using assms by (induct \<pi>\<^sub>1 eP P \<pi>\<^sub>2 eP' rule: smallstep.induct) auto
 
 lemma smallstepsP_generates_proofstream:
   assumes "\<lless> \<pi>\<^sub>1, eP \<ggreater> P\<rightarrow>i \<lless> \<pi>\<^sub>2, eP' \<ggreater>"
   obtains \<pi> where "\<pi>\<^sub>2 = \<pi>\<^sub>1 @ \<pi>"
   using assms by (induct \<pi>\<^sub>1 eP P i \<pi>\<^sub>2 eP' rule: smallsteps.induct)
                  (auto elim: smallstepP_generates_proofstream)
 
 lemma smallstepV_ps_append:
   "\<lless> \<pi>, eV \<ggreater> V\<rightarrow> \<lless> \<pi>', eV' \<ggreater> \<longleftrightarrow> \<lless> \<pi> @ X, eV \<ggreater> V\<rightarrow> \<lless> \<pi>' @ X, eV' \<ggreater>" (is "?L \<longleftrightarrow> ?R")
 proof (rule iffI)
   assume ?L then show ?R
     by (nominal_induct \<pi> eV V \<pi>' eV' avoiding: X rule: smallstep.strong_induct)
        (auto simp: fresh_append fresh_Pair)
 next
   assume ?R then show ?L
     by (nominal_induct "\<pi> @ X" eV V "\<pi>' @ X" eV' avoiding: X rule: smallstep.strong_induct)
        (auto simp: fresh_append fresh_Pair)
 qed
 
 lemma smallstepV_ps_to_suffix:
   assumes "\<lless>\<pi>, e\<ggreater> V\<rightarrow> \<lless>\<pi>' @ X, e'\<ggreater>"
   obtains \<pi>'' where "\<pi> = \<pi>'' @ X"
   using assms
   by (induct \<pi> e V "\<pi>' @ X" e' rule: smallstep.induct) auto
 
 lemma smallstepsV_ps_append:
   "\<lless> \<pi>, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>', eV' \<ggreater> \<longleftrightarrow> \<lless> \<pi> @ X, eV \<ggreater> V\<rightarrow>i \<lless> \<pi>' @ X, eV' \<ggreater>" (is "?L \<longleftrightarrow> ?R")
 proof (rule iffI)
   assume ?L then show ?R
   proof (induct \<pi> eV V i \<pi>' eV' rule: smallsteps.induct)
     case (s_Tr \<pi>\<^sub>1 e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 \<pi>\<^sub>3 e\<^sub>3)
     then show ?case
       by (auto simp: iffD1[OF smallstepV_ps_append])
   qed simp
 next
   assume ?R then show ?L
   proof (induct "\<pi> @ X" eV V i "\<pi>' @ X" eV' arbitrary: \<pi>' rule: smallsteps.induct)
     case (s_Tr e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 e\<^sub>3)
     from s_Tr(3) obtain \<pi>''' where "\<pi>\<^sub>2 = \<pi>''' @ 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:
   "\<lless> \<pi>, eP \<ggreater> P\<rightarrow> \<lless> \<pi>', eP' \<ggreater> \<longleftrightarrow> \<lless> X @ \<pi>, eP \<ggreater> P\<rightarrow> \<lless> X @ \<pi>', eP' \<ggreater>" (is "?L \<longleftrightarrow> ?R")
 proof (rule iffI)
   assume ?L then show ?R
   proof (nominal_induct \<pi> eP P \<pi>' eP' avoiding: X rule: smallstep.strong_induct)
     case (s_UnauthP v \<pi> h)
     then show ?case
       by (subst append_assoc[symmetric, of X \<pi> "[\<lparr>v\<rparr>]"]) (erule smallstep.s_UnauthP)
   qed (auto simp: fresh_append fresh_Pair)
 next
   assume ?R then show ?L
     by (nominal_induct "X @ \<pi>" eP P "X @ \<pi>'" eP' avoiding: X rule: smallstep.strong_induct)
        (auto simp: fresh_append fresh_Pair)
 qed
 
 lemma smallstepsP_ps_prepend:
   "\<lless> \<pi>, eP \<ggreater> P\<rightarrow>i \<lless> \<pi>', eP' \<ggreater> \<longleftrightarrow> \<lless> X @ \<pi>, eP \<ggreater> P\<rightarrow>i \<lless> X @ \<pi>', eP' \<ggreater>" (is "?L \<longleftrightarrow> ?R")
 proof (rule iffI)
   assume ?L then show ?R
   proof (induct \<pi> eP P i \<pi>' eP' rule: smallsteps.induct)
     case (s_Tr \<pi>\<^sub>1 e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 \<pi>\<^sub>3 e\<^sub>3)
     then show ?case
       by (auto simp: iffD1[OF smallstepP_ps_prepend])
   qed simp
 next
   assume ?R then show ?L
   proof (induct "X @ \<pi>" eP P i "X @ \<pi>'" eP' arbitrary: \<pi>' rule: smallsteps.induct)
     case (s_Tr e\<^sub>1 i \<pi>\<^sub>2 e\<^sub>2 e\<^sub>3)
     then obtain \<pi>'' where \<pi>'': "\<pi>\<^sub>2 = X @ \<pi> @ \<pi>''"
       by (auto elim: smallstepsP_generates_proofstream)
     then have "\<lless>\<pi>, e\<^sub>1\<ggreater> P\<rightarrow>i \<lless>\<pi> @ \<pi>'', e\<^sub>2\<ggreater>"
       by (auto dest: s_Tr(2))
     with \<pi>'' s_Tr(1,3) show ?case
       by (auto dest: iffD2[OF smallstepP_ps_prepend])
   qed simp
 qed
 
 subsection \<open>Type Progress\<close>
 
 lemma type_progress:
   assumes "{$$} \<turnstile>\<^sub>W e : \<tau>"
   shows   "value e \<or> (\<exists>e'. \<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater>)"
 using assms proof (nominal_induct "{$$} :: tyenv" e \<tau> rule: judge_weak.strong_induct)
   case (jw_Let x e\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 \<tau>\<^sub>2)
   then show ?case
     by (auto 0 3 simp: fresh_smallstep_I elim!: s_Let2[of e\<^sub>2]
       intro: exI[where P="\<lambda>e. \<lless>_, _\<ggreater> _\<rightarrow> \<lless>_, e\<ggreater>", OF s_Let1, rotated])
 next
   case (jw_Prj1 v \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
     by (auto elim!: jw_Prod_inv[of v \<tau>\<^sub>1 \<tau>\<^sub>2])
 next
   case (jw_Prj2 v \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
     by (auto elim!: jw_Prod_inv[of v \<tau>\<^sub>1 \<tau>\<^sub>2])
 next
   case (jw_App e \<tau>\<^sub>1 \<tau>\<^sub>2 e')
   then show ?case
     by (auto 0 4 elim: jw_Fun_inv[of _ _ _ e'])
 next
   case (jw_Case v v\<^sub>1 v\<^sub>2 \<tau>\<^sub>1 \<tau>\<^sub>2 \<tau>)
   then show ?case
     by (auto 0 4 elim: jw_Sum_inv[of _ v\<^sub>1 v\<^sub>2])
 qed fast+
 
 subsection \<open>Weak Type Preservation\<close>
 
 lemma fresh_tyenv_None:
   fixes \<Gamma> :: tyenv
   shows "atom x \<sharp> \<Gamma> \<longleftrightarrow> \<Gamma> $$ x = None" (is "?L \<longleftrightarrow> ?R")
 proof
   assume assm: ?L show ?R
   proof (rule ccontr)
     assume "\<Gamma> $$ x \<noteq> None"
     then obtain \<tau> where "\<Gamma> $$ x = Some \<tau>" by blast
     with assm have "\<forall>a :: var. atom a \<sharp> \<Gamma> \<longrightarrow> \<Gamma> $$ a = Some \<tau>"
       using fmap_freshness_lemma_unique[OF exI, of x \<Gamma>]
       by (simp add: fresh_Pair fresh_Some) metis
     then have "{a :: var. atom a \<sharp> \<Gamma>} \<subseteq> fmdom' \<Gamma>"
       by (auto simp: image_iff Ball_def fmlookup_dom'_iff)
     moreover
     { assume "infinite {a :: var. \<not> atom a \<sharp> \<Gamma>}"
       then have "infinite {a :: var. atom a \<in> supp \<Gamma>}"
         unfolding fresh_def by auto
       then have "infinite (supp \<Gamma>)"
         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 \<Gamma>] by blast
     }
     then have "infinite {a :: var. atom a \<sharp> \<Gamma>}"
       by auto
     ultimately show False
       using finite_subset[of "{a. atom a \<sharp> \<Gamma>}" "fmdom' \<Gamma>"] unfolding fmdom'_alt_def
       by auto
   qed
 next
   assume ?R then show ?L
   proof (induct \<Gamma> arbitrary: x)
     case (fmupd y z \<Gamma>)
     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 "\<Gamma> \<turnstile>\<^sub>W e : \<tau>" "atom a \<sharp> \<Gamma>"
   shows   "atom a \<sharp> e"
   using assms proof (nominal_induct \<Gamma> e \<tau> avoiding: a rule: judge_weak.strong_induct)
   case (jw_Var \<Gamma> x \<tau>)
   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 "\<Gamma> \<turnstile>\<^sub>W e : \<tau>" "atom y \<sharp> e"
   shows   "\<Gamma>(y $$:= \<tau>') \<turnstile>\<^sub>W e : \<tau>"
   using assms proof (nominal_induct \<Gamma> e \<tau> avoiding: y \<tau>' rule: judge_weak.strong_induct)
   case (jw_Lam x \<Gamma> \<tau>\<^sub>1 e \<tau>\<^sub>2)
   from jw_Lam(5)[of y \<tau>'] jw_Lam(1-4,6) show ?case
-    by (auto simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
+    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
 next
   case (jw_App v v' \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2)
   then show ?case
-    by (force simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
+    by (force simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
 next
   case (jw_Let x \<Gamma> e\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 \<tau>\<^sub>2)
   from jw_Let(6)[of y \<tau>'] jw_Let(8)[of y \<tau>'] jw_Let(1-5,7,9) show ?case
-    by (auto simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
+    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
 next
   case (jw_Rec x \<Gamma> z \<tau>\<^sub>1 \<tau>\<^sub>2 e')
   from jw_Rec(9)[of y \<tau>'] jw_Rec(1-8,10) show ?case
-    by (auto simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update fresh_Pair)
+    by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update fresh_Pair)
 next
   case (jw_Case v v\<^sub>1 v\<^sub>2 \<Gamma> \<tau>\<^sub>1 \<tau>\<^sub>2 \<tau>)
   then show ?case
-    by (fastforce simp add: fresh_at_base fmap_reorder_neq_updates fresh_fmap_update)
+    by (fastforce simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update)
 next
   case (jw_Roll \<alpha> \<Gamma> v \<tau>)
   then show ?case
     by (simp add: fresh_fmap_update)
 next
   case (jw_Unroll \<alpha> \<Gamma> v \<tau>)
   then show ?case
     by (simp add: fresh_fmap_update)
 qed auto
 
 lemma judge_weak_weakening_2:
   assumes "\<Gamma> \<turnstile>\<^sub>W e : \<tau>" "atom y \<sharp> \<Gamma>"
   shows   "\<Gamma>(y $$:= \<tau>') \<turnstile>\<^sub>W e : \<tau>"
   proof -
     from assms have "atom y \<sharp> e"
       by (rule judge_weak_fresh_env_fresh_term)
     with assms show "\<Gamma>(y $$:= \<tau>') \<turnstile>\<^sub>W e : \<tau>" by (simp add: judge_weak_weakening_1)
   qed
 
 lemma judge_weak_weakening_env:
   assumes "{$$} \<turnstile>\<^sub>W e : \<tau>"
   shows   "\<Gamma> \<turnstile>\<^sub>W e : \<tau>"
 using assms proof (induct \<Gamma>)
   case fmempty
   then show ?case by assumption
 next
   case (fmupd x y \<Gamma>)
   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 "\<Gamma>(a $$:= \<tau>') \<turnstile>\<^sub>W e : \<tau>" "{$$} \<turnstile>\<^sub>W e' : \<tau>'"
   shows   "\<Gamma> \<turnstile>\<^sub>W e[e' / a] : \<tau>"
   using assms proof (nominal_induct "\<Gamma>(a $$:= \<tau>')" e \<tau> avoiding: a e' \<Gamma> rule: judge_weak.strong_induct)
   case (jw_Var x \<tau>)
   then show ?case
     by (auto simp: judge_weak_weakening_env)
 next
   case (jw_Lam x \<tau>\<^sub>1 e \<tau>\<^sub>2)
   then show ?case
-    by (fastforce simp: fmap_reorder_neq_updates)
+    by (fastforce simp: fmupd_reorder_neq)
 next
   case (jw_Rec x y \<tau>\<^sub>1 \<tau>\<^sub>2 e)
   then show ?case
-    by (fastforce simp: fmap_reorder_neq_updates)
+    by (fastforce simp: fmupd_reorder_neq)
 next
   case (jw_Let x e\<^sub>1 \<tau>\<^sub>1 e\<^sub>2 \<tau>\<^sub>2)
   then show ?case
-    by (fastforce simp: fmap_reorder_neq_updates)
+    by (fastforce simp: fmupd_reorder_neq)
 qed fastforce+
 
 lemma type_preservation:
   assumes "\<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater>" "{$$} \<turnstile>\<^sub>W e : \<tau>"
   shows   "{$$} \<turnstile>\<^sub>W e' : \<tau>"
   using assms [[simproc del: alpha_lst]]
 proof (nominal_induct "[]::proofstream" e I "[]::proofstream" e' arbitrary: \<tau> 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\<^sub>1 e\<^sub>1' e\<^sub>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 \<alpha>::tvar where "atom \<alpha> \<sharp> \<tau>"
     using obtain_fresh by blast
   with s_Unroll show ?case
     by (auto elim: jw_Unroll_inv[where \<alpha> = \<alpha>])
 next
   case (s_Roll e e')
   then obtain \<alpha>::tvar where "atom \<alpha> \<sharp> \<tau>"
     using obtain_fresh by blast
   with s_Roll show ?case
     by (auto elim: jw_Roll_inv[where \<alpha> = \<alpha>])
 next
   case (s_UnrollRoll v)
   then obtain \<alpha>::tvar where "atom \<alpha> \<sharp> \<tau>"
     using obtain_fresh by blast
   with s_UnrollRoll show ?case
     by (fastforce simp: Abs1_eq(3) elim: jw_Roll_inv[where \<alpha> = \<alpha>] jw_Unroll_inv[where \<alpha> = \<alpha>])
 qed fastforce+
 
 subsection \<open>Corrected Lemma 1 from Miller et al.~\cite{adsg}: Weak Type Soundness\<close>
 
 lemma type_soundness:
   assumes "{$$} \<turnstile>\<^sub>W e : \<tau>"
   shows   "value e \<or> (\<exists>e'. \<lless> [], e \<ggreater> I\<rightarrow> \<lless> [], e' \<ggreater> \<and> {$$} \<turnstile>\<^sub>W e' : \<tau>)"
 proof (cases "value e")
   case True
   then show ?thesis by simp
 next
   case False
   with assms obtain e' where "\<lless>[], e\<ggreater> I\<rightarrow> \<lless>[], e'\<ggreater>" by (auto dest: type_progress)
   with assms show ?thesis
     by (auto simp: type_preservation)
 qed
 
 (*<*)
 end
 (*>*)