# HG changeset patch
# User wenzelm
# Date 1728392537 -7200
# Node ID 12990a6dddcb01059fc6660e2d97932b79411907
# Parent  ef362328b93167fea4a2e8424d91f64380fbf936
avoid syntax clashes;

diff -r ef362328b931 -r 12990a6dddcb src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Oct 08 13:13:53 2024 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Oct 08 15:02:17 2024 +0200
@@ -152,43 +152,43 @@
 equivariance val 
 
 inductive
-  machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" (\<open><_,_> \<mapsto> <_,_>\<close>)
+  machine :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" (\<open><_,_> \<leadsto> <_,_>\<close>)
 where
-  m1[intro]: "<APP e1 e2,Es> \<mapsto> <e1,(CAPPL \<box> e2)#Es>"
-| m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<mapsto> <e2,(CAPPR v \<box>)#Es>"
-| m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<mapsto> <e[y::=v],Es>"
-| m4[intro]: "<e1 -- e2, Es> \<mapsto> <e1,(CDIFFL \<box> e2)#Es>"
-| m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<mapsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>"
-| m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1 - n2),Es>"
-| m4'[intro]:"<e1 ++ e2, Es> \<mapsto> <e1,(CPLUSL \<box> e2)#Es>"
-| m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<mapsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>"
-| m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<mapsto> <NUM (n1+n2),Es>"
-| m7[intro]: "<IF e1 e2 e3,Es> \<mapsto> <e1,(CIF \<box> e2 e3)#Es>"
-| m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<mapsto> <e1,Es>"
-| m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<mapsto> <e2,Es>"
-| mA[intro]: "<FIX [x].t,Es> \<mapsto> <t[x::=FIX [x].t],Es>"
-| mB[intro]: "<ZET e,Es> \<mapsto> <e,(CZET \<box>)#Es>"
-| mC[intro]: "<NUM 0,(CZET \<box>)#Es> \<mapsto> <TRUE,Es>"
-| mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZET \<box>)#Es> \<mapsto> <FALSE,Es>"
-| mE[intro]: "<EQI e1 e2,Es> \<mapsto> <e1,(CEQIL \<box> e2)#Es>"
-| mF[intro]: "<NUM n1,(CEQIL \<box> e2)#Es> \<mapsto> <e2,(CEQIR (NUM n1) \<box>)#Es>"
-| mG[intro]: "<NUM n,(CEQIR (NUM n) \<box>)#Es> \<mapsto> <TRUE,Es>"
-| mH[intro]: "n1\<noteq>n2 \<Longrightarrow> <NUM n1,(CEQIR (NUM n2) \<box>)#Es> \<mapsto> <FALSE,Es>"
+  m1[intro]: "<APP e1 e2,Es> \<leadsto> <e1,(CAPPL \<box> e2)#Es>"
+| m2[intro]: "val v \<Longrightarrow> <v,(CAPPL \<box> e2)#Es> \<leadsto> <e2,(CAPPR v \<box>)#Es>"
+| m3[intro]: "val v \<Longrightarrow> <v,(CAPPR (LAM [y].e) \<box>)#Es> \<leadsto> <e[y::=v],Es>"
+| m4[intro]: "<e1 -- e2, Es> \<leadsto> <e1,(CDIFFL \<box> e2)#Es>"
+| m5[intro]: "<NUM n1,(CDIFFL \<box> e2)#Es> \<leadsto> <e2,(CDIFFR (NUM n1) \<box>)#Es>"
+| m6[intro]: "<NUM n2,(CDIFFR (NUM n1) \<box>)#Es> \<leadsto> <NUM (n1 - n2),Es>"
+| m4'[intro]:"<e1 ++ e2, Es> \<leadsto> <e1,(CPLUSL \<box> e2)#Es>"
+| m5'[intro]:"<NUM n1,(CPLUSL \<box> e2)#Es> \<leadsto> <e2,(CPLUSR (NUM n1) \<box>)#Es>"
+| m6'[intro]:"<NUM n2,(CPLUSR (NUM n1) \<box>)#Es> \<leadsto> <NUM (n1+n2),Es>"
+| m7[intro]: "<IF e1 e2 e3,Es> \<leadsto> <e1,(CIF \<box> e2 e3)#Es>"
+| m8[intro]: "<TRUE,(CIF \<box> e1 e2)#Es> \<leadsto> <e1,Es>"
+| m9[intro]: "<FALSE,(CIF \<box> e1 e2)#Es> \<leadsto> <e2,Es>"
+| mA[intro]: "<FIX [x].t,Es> \<leadsto> <t[x::=FIX [x].t],Es>"
+| mB[intro]: "<ZET e,Es> \<leadsto> <e,(CZET \<box>)#Es>"
+| mC[intro]: "<NUM 0,(CZET \<box>)#Es> \<leadsto> <TRUE,Es>"
+| mD[intro]: "0 < n \<Longrightarrow> <NUM n,(CZET \<box>)#Es> \<leadsto> <FALSE,Es>"
+| mE[intro]: "<EQI e1 e2,Es> \<leadsto> <e1,(CEQIL \<box> e2)#Es>"
+| mF[intro]: "<NUM n1,(CEQIL \<box> e2)#Es> \<leadsto> <e2,(CEQIR (NUM n1) \<box>)#Es>"
+| mG[intro]: "<NUM n,(CEQIR (NUM n) \<box>)#Es> \<leadsto> <TRUE,Es>"
+| mH[intro]: "n1\<noteq>n2 \<Longrightarrow> <NUM n1,(CEQIR (NUM n2) \<box>)#Es> \<leadsto> <FALSE,Es>"
 
 inductive 
-  "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" (\<open><_,_> \<mapsto>* <_,_>\<close>)
+  "machine_star" :: "lam\<Rightarrow>ctx list\<Rightarrow>lam\<Rightarrow>ctx list\<Rightarrow>bool" (\<open><_,_> \<leadsto>* <_,_>\<close>)
 where
-  ms1[intro]: "<e,Es> \<mapsto>* <e,Es>"
-| ms2[intro]: "\<lbrakk><e1,Es1> \<mapsto> <e2,Es2>; <e2,Es2> \<mapsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<mapsto>* <e3,Es3>"
+  ms1[intro]: "<e,Es> \<leadsto>* <e,Es>"
+| ms2[intro]: "\<lbrakk><e1,Es1> \<leadsto> <e2,Es2>; <e2,Es2> \<leadsto>* <e3,Es3>\<rbrakk> \<Longrightarrow> <e1,Es1> \<leadsto>* <e3,Es3>"
 
 lemma ms3[intro,trans]:
-  assumes a: "<e1,Es1> \<mapsto>* <e2,Es2>" "<e2,Es2> \<mapsto>* <e3,Es3>"
-  shows "<e1,Es1> \<mapsto>* <e3,Es3>"
+  assumes a: "<e1,Es1> \<leadsto>* <e2,Es2>" "<e2,Es2> \<leadsto>* <e3,Es3>"
+  shows "<e1,Es1> \<leadsto>* <e3,Es3>"
 using a by (induct) (auto) 
 
 lemma ms4[intro]:
-  assumes a: "<e1,Es1> \<mapsto> <e2,Es2>" 
-  shows "<e1,Es1> \<mapsto>* <e2,Es2>"
+  assumes a: "<e1,Es1> \<leadsto> <e2,Es2>" 
+  shows "<e1,Es1> \<leadsto>* <e2,Es2>"
 using a by (rule ms2) (rule ms1)
 
 section \<open>The Evaluation Relation (Big-Step Semantics)\<close>
@@ -238,14 +238,14 @@
 
 theorem eval_implies_machine_star_ctx:
   assumes a: "t \<Down> t'"
-  shows "<t,Es> \<mapsto>* <t',Es>"
+  shows "<t,Es> \<leadsto>* <t',Es>"
 using a
 by (induct arbitrary: Es)
    (metis eval_to machine.intros ms1 ms2 ms3 ms4 v_LAM)+
 
 corollary eval_implies_machine_star:
   assumes a: "t \<Down> t'"
-  shows "<t,[]> \<mapsto>* <t',[]>"
+  shows "<t,[]> \<leadsto>* <t',[]>"
 using a by (auto dest: eval_implies_machine_star_ctx)
 
 section \<open>The CBV Reduction Relation (Small-Step Semantics)\<close>
@@ -313,18 +313,18 @@
 using a by (induct E) (auto)
 
 lemma machine_implies_cbv_star_ctx:
-  assumes a: "<e,Es> \<mapsto> <e',Es'>"
+  assumes a: "<e,Es> \<leadsto> <e',Es'>"
   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
 using a by (induct) (auto simp add: ctx_compose intro: cbv_in_ctx)
 
 lemma machine_star_implies_cbv_star_ctx:
-  assumes a: "<e,Es> \<mapsto>* <e',Es'>"
+  assumes a: "<e,Es> \<leadsto>* <e',Es'>"
   shows "(Es\<down>)\<lbrakk>e\<rbrakk> \<longrightarrow>cbv* (Es'\<down>)\<lbrakk>e'\<rbrakk>"
 using a 
 by (induct) (auto dest: machine_implies_cbv_star_ctx)
 
 lemma machine_star_implies_cbv_star:
-  assumes a: "<e,[]> \<mapsto>* <e',[]>"
+  assumes a: "<e,[]> \<leadsto>* <e',[]>"
   shows "e \<longrightarrow>cbv* e'"
 using a by (auto dest: machine_star_implies_cbv_star_ctx)
 
@@ -350,7 +350,7 @@
 text \<open>The Soundness Property\<close>
 
 theorem machine_star_implies_eval:
-  assumes a: "<t1,[]> \<mapsto>* <t2,[]>" 
+  assumes a: "<t1,[]> \<leadsto>* <t2,[]>" 
   and     b: "val t2" 
   shows "t1 \<Down> t2"
 proof -
@@ -536,7 +536,7 @@
 section \<open>The Type-Preservation Property for the Machine and Evaluation Relation\<close>
 
 theorem machine_type_preservation:
-  assumes a: "<t,[]> \<mapsto>* <t',[]>"
+  assumes a: "<t,[]> \<leadsto>* <t',[]>"
   and     b: "\<Gamma> \<turnstile> t : T" 
   shows "\<Gamma> \<turnstile> t' : T"
 proof -
@@ -549,7 +549,7 @@
   and     b: "\<Gamma> \<turnstile> t : T" 
   shows "\<Gamma> \<turnstile> t' : T"
 proof -
-  from a have "<t,[]> \<mapsto>* <t',[]>" by (simp add: eval_implies_machine_star)
+  from a have "<t,[]> \<leadsto>* <t',[]>" by (simp add: eval_implies_machine_star)
   then show "\<Gamma> \<turnstile> t' : T" using b by (simp add: machine_type_preservation)
 qed
 
diff -r ef362328b931 -r 12990a6dddcb src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Tue Oct 08 13:13:53 2024 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Tue Oct 08 15:02:17 2024 +0200
@@ -41,7 +41,7 @@
   | IUnit
   | INat "nat"
   | ISucc "trmI"
-  | IAss "trmI" "trmI" (\<open>_\<mapsto>_\<close> [100,100] 100)
+  | IAss "trmI" "trmI" (\<open>_\<leadsto>_\<close> [100,100] 100)
   | IRef "trmI" 
   | ISeq "trmI" "trmI" (\<open>_;;_\<close> [100,100] 100)
   | Iif "trmI" "trmI" "trmI"
@@ -84,7 +84,7 @@
 | t4[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> I\<turnstile> INat(n) : DataI(NatI)"
 | t5[intro]: "\<Gamma> I\<turnstile> e : DataI(NatI) \<Longrightarrow> \<Gamma> I\<turnstile> ISucc(e) : DataI(NatI)"
 | t6[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> IRef e : DataI (NatI)"
-| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<mapsto>e2 : DataI(OneI)"
+| t7[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : DataI(NatI)\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1\<leadsto>e2 : DataI(OneI)"
 | t8[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e1 : DataI(NatI); \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> e1;;e2 : \<tau>"
 | t9[intro]: "\<lbrakk>\<Gamma> I\<turnstile> e: DataI(NatI); \<Gamma> I\<turnstile> e1 : \<tau>; \<Gamma> I\<turnstile> e2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> I\<turnstile> Iif e e1 e2 : \<tau>"
 
@@ -192,7 +192,7 @@
 | m3[intro]: "(m,INat(n))I\<Down>(m,INat(n))"
 | m4[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,ISucc(e))I\<Down>(m',INat(n+1))"
 | m5[intro]: "(m,e)I\<Down>(m',INat(n)) \<Longrightarrow> (m,IRef(e))I\<Down>(m',INat(m' n))"
-| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<mapsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
+| m6[intro]: "\<lbrakk>(m,e1)I\<Down>(m',INat(n1)); (m',e2)I\<Down>(m'',INat(n2))\<rbrakk> \<Longrightarrow> (m,e1\<leadsto>e2)I\<Down>(m''(n1:=n2),IUnit)"
 | m7[intro]: "\<lbrakk>(m,e1)I\<Down>(m',IUnit); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,e1;;e2)I\<Down>(m'',e)"
 | m8[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(n)); n\<noteq>0; (m',e1)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
 | m9[intro]: "\<lbrakk>(m,e)I\<Down>(m',INat(0)); (m',e2)I\<Down>(m'',e)\<rbrakk> \<Longrightarrow> (m,Iif e e1 e2)I\<Down>(m'',e)"
@@ -210,17 +210,17 @@
        (let limit = IRef(INat 0) in 
         let v1 = (trans e1) in 
         let v2 = (trans e2) in 
-        (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+        (((ISucc limit)\<leadsto>v1);;(ISucc(ISucc limit)\<leadsto>v2));;(INat 0 \<leadsto> ISucc(ISucc(limit))))"
 | "trans (Fst e) = IRef (ISucc (trans e))"
 | "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
 | "trans (InL e) = 
         (let limit = IRef(INat 0) in 
          let v = (trans e) in 
-         (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+         (((ISucc limit)\<leadsto>INat(0));;(ISucc(ISucc limit)\<leadsto>v));;(INat 0 \<leadsto> ISucc(ISucc(limit))))"
 | "trans (InR e) = 
         (let limit = IRef(INat 0) in 
          let v = (trans e) in 
-         (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+         (((ISucc limit)\<leadsto>INat(1));;(ISucc(ISucc limit)\<leadsto>v));;(INat 0 \<leadsto> ISucc(ISucc(limit))))"
 | "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
    trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
        (let v = (trans e) in
diff -r ef362328b931 -r 12990a6dddcb src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Tue Oct 08 13:13:53 2024 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Tue Oct 08 15:02:17 2024 +0200
@@ -16,9 +16,6 @@
 
 section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close>
 
-no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
-
 text \<open>The main point of this solution is to use names everywhere (be they bound, 
   binding or free). In System \FSUB{} there are two kinds of names corresponding to 
   type-variables and to term-variables. These two kinds of names are represented in 
@@ -386,183 +383,183 @@
   by (finite_guess | fresh_guess | simp)+
 
 nominal_primrec
-  subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" (\<open>_[_ \<mapsto> _]\<^sub>\<tau>\<close> [300, 0, 0] 300)
+  subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" (\<open>_[_ \<leadsto> _]\<^sub>\<tau>\<close> [300, 0, 0] 300)
 where
-  "(Tvar X)[Y \<mapsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)"
-| "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top"
-| "(T\<^sub>1 \<rightarrow> T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>"
-| "X\<sharp>(Y,T,T\<^sub>1) \<Longrightarrow> (\<forall>X<:T\<^sub>1. T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>)"
+  "(Tvar X)[Y \<leadsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)"
+| "(Top)[Y \<leadsto> T]\<^sub>\<tau> = Top"
+| "(T\<^sub>1 \<rightarrow> T\<^sub>2)[Y \<leadsto> T]\<^sub>\<tau> = T\<^sub>1[Y \<leadsto> T]\<^sub>\<tau> \<rightarrow> T\<^sub>2[Y \<leadsto> T]\<^sub>\<tau>"
+| "X\<sharp>(Y,T,T\<^sub>1) \<Longrightarrow> (\<forall>X<:T\<^sub>1. T\<^sub>2)[Y \<leadsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^sub>1[Y \<leadsto> T]\<^sub>\<tau>. T\<^sub>2[Y \<leadsto> T]\<^sub>\<tau>)"
   by (finite_guess | fresh_guess | simp add: abs_fresh)+
 
 lemma subst_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   T::"ty"
-  shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>"
+  shows "pi\<bullet>(T[X \<leadsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<leadsto> (pi\<bullet>T')]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_bij)+
 
 lemma subst_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   T::"ty"
-  shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>"
+  shows "pi\<bullet>(T[X \<leadsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<leadsto> (pi\<bullet>T')]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma type_subst_fresh:
   fixes X::"tyvrs"
   assumes "X\<sharp>T" and "X\<sharp>P"
-  shows   "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>"
+  shows   "X\<sharp>T[Y \<leadsto> P]\<^sub>\<tau>"
   using assms
   by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
     (auto simp: abs_fresh)
 
 lemma fresh_type_subst_fresh:
   assumes "X\<sharp>T'"
-  shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
+  shows "X\<sharp>T[X \<leadsto> T']\<^sub>\<tau>"
   using assms 
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (auto simp: fresh_atm abs_fresh) 
 
 lemma type_subst_identity: 
-  "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
+  "X\<sharp>T \<Longrightarrow> T[X \<leadsto> U]\<^sub>\<tau> = T"
   by (nominal_induct T avoiding: X U rule: ty.strong_induct)
     (simp_all add: fresh_atm abs_fresh)
 
 lemma type_substitution_lemma:  
-  "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
+  "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<leadsto> N]\<^sub>\<tau>[Y \<leadsto> L]\<^sub>\<tau> = M[Y \<leadsto> L]\<^sub>\<tau>[X \<leadsto> N[Y \<leadsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
   by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct)
     (auto simp: type_subst_fresh type_subst_identity)
 
 lemma type_subst_rename:
-  "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
+  "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<leadsto> U]\<^sub>\<tau> = T[X \<leadsto> U]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X Y U rule: ty.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux)
 
 nominal_primrec
-  subst_tyb :: "binding \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> binding" (\<open>_[_ \<mapsto> _]\<^sub>b\<close> [100,100,100] 100)
+  subst_tyb :: "binding \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> binding" (\<open>_[_ \<leadsto> _]\<^sub>b\<close> [100,100,100] 100)
 where
-  "(TVarB X U)[Y \<mapsto> T]\<^sub>b = TVarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
-| "(VarB  X U)[Y \<mapsto> T]\<^sub>b =  VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
+  "(TVarB X U)[Y \<leadsto> T]\<^sub>b = TVarB X (U[Y \<leadsto> T]\<^sub>\<tau>)"
+| "(VarB  X U)[Y \<leadsto> T]\<^sub>b =  VarB X (U[Y \<leadsto> T]\<^sub>\<tau>)"
 by auto
 
 lemma binding_subst_fresh:
   fixes X::"tyvrs"
   assumes "X\<sharp>a"
   and     "X\<sharp>P"
-  shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b"
+  shows "X\<sharp>a[Y \<leadsto> P]\<^sub>b"
 using assms
 by (nominal_induct a rule: binding.strong_induct)
    (auto simp: type_subst_fresh)
 
 lemma binding_subst_identity: 
-  shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
+  shows "X\<sharp>B \<Longrightarrow> B[X \<leadsto> U]\<^sub>b = B"
 by (induct B rule: binding.induct)
    (simp_all add: fresh_atm type_subst_identity)
 
-primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" (\<open>_[_ \<mapsto> _]\<^sub>e\<close> [100,100,100] 100) where
-  "([])[Y \<mapsto> T]\<^sub>e= []"
-| "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
+primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" (\<open>_[_ \<leadsto> _]\<^sub>e\<close> [100,100,100] 100) where
+  "([])[Y \<leadsto> T]\<^sub>e= []"
+| "(B#\<Gamma>)[Y \<leadsto> T]\<^sub>e = (B[Y \<leadsto> T]\<^sub>b)#(\<Gamma>[Y \<leadsto> T]\<^sub>e)"
 
 lemma ctxt_subst_fresh':
   fixes X::"tyvrs"
   assumes "X\<sharp>\<Gamma>"
   and     "X\<sharp>P"
-  shows   "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e"
+  shows   "X\<sharp>\<Gamma>[Y \<leadsto> P]\<^sub>e"
 using assms
 by (induct \<Gamma>)
    (auto simp: fresh_list_cons binding_subst_fresh)
 
-lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
+lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<leadsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<leadsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
-lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
+lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<leadsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<leadsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
-lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
+lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<leadsto> U]\<^sub>e = \<Gamma>"
   by (induct \<Gamma>) (simp_all add: fresh_list_cons binding_subst_identity)
 
-lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<mapsto> T]\<^sub>e = \<Delta>[X \<mapsto> T]\<^sub>e @ \<Gamma>[X \<mapsto> T]\<^sub>e"
+lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<leadsto> T]\<^sub>e = \<Delta>[X \<leadsto> T]\<^sub>e @ \<Gamma>[X \<leadsto> T]\<^sub>e"
   by (induct \<Delta>) simp_all
 
 nominal_primrec
-   subst_trm :: "trm \<Rightarrow> vrs \<Rightarrow> trm \<Rightarrow> trm"  (\<open>_[_ \<mapsto> _]\<close> [300, 0, 0] 300)
+   subst_trm :: "trm \<Rightarrow> vrs \<Rightarrow> trm \<Rightarrow> trm"  (\<open>_[_ \<leadsto> _]\<close> [300, 0, 0] 300)
 where
-  "(Var x)[y \<mapsto> t'] = (if x=y then t' else (Var x))"
-| "(t1 \<cdot> t2)[y \<mapsto> t'] = t1[y \<mapsto> t'] \<cdot> t2[y \<mapsto> t']"
-| "(t \<cdot>\<^sub>\<tau> T)[y \<mapsto> t'] = t[y \<mapsto> t'] \<cdot>\<^sub>\<tau> T"
-| "X\<sharp>(T,t') \<Longrightarrow> (\<lambda>X<:T. t)[y \<mapsto> t'] = (\<lambda>X<:T. t[y \<mapsto> t'])" 
-| "x\<sharp>(y,t') \<Longrightarrow> (\<lambda>x:T. t)[y \<mapsto> t'] = (\<lambda>x:T. t[y \<mapsto> t'])"
+  "(Var x)[y \<leadsto> t'] = (if x=y then t' else (Var x))"
+| "(t1 \<cdot> t2)[y \<leadsto> t'] = t1[y \<leadsto> t'] \<cdot> t2[y \<leadsto> t']"
+| "(t \<cdot>\<^sub>\<tau> T)[y \<leadsto> t'] = t[y \<leadsto> t'] \<cdot>\<^sub>\<tau> T"
+| "X\<sharp>(T,t') \<Longrightarrow> (\<lambda>X<:T. t)[y \<leadsto> t'] = (\<lambda>X<:T. t[y \<leadsto> t'])" 
+| "x\<sharp>(y,t') \<Longrightarrow> (\<lambda>x:T. t)[y \<leadsto> t'] = (\<lambda>x:T. t[y \<leadsto> t'])"
   by (finite_guess | simp add: abs_fresh | fresh_guess add: ty_vrs_fresh abs_fresh)+
 
 lemma subst_trm_fresh_tyvar:
   fixes X::"tyvrs"
-  shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]"
+  shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<leadsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (auto simp: abs_fresh)
 
 lemma subst_trm_fresh_var: 
-  "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]"
+  "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<leadsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_atm ty_vrs_fresh)
 
 lemma subst_trm_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   t::"trm"
-  shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]"
+  shows "pi\<bullet>(t[x \<leadsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<leadsto> (pi\<bullet>u)]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma subst_trm_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   t::"trm"
-  shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]"
+  shows "pi\<bullet>(t[x \<leadsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<leadsto> (pi\<bullet>u)]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma subst_trm_rename:
-  "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
+  "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<leadsto> u] = t[x \<leadsto> u]"
   by (nominal_induct t avoiding: x y u rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh)
 
 nominal_primrec (freshness_context: "T2::ty")
-  subst_trm_ty :: "trm \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> trm"  (\<open>_[_ \<mapsto>\<^sub>\<tau> _]\<close> [300, 0, 0] 300)
+  subst_trm_ty :: "trm \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> trm"  (\<open>_[_ \<leadsto>\<^sub>\<tau> _]\<close> [300, 0, 0] 300)
 where
-  "(Var x)[Y \<mapsto>\<^sub>\<tau> T2] = Var x"
-| "(t1 \<cdot> t2)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot> t2[Y \<mapsto>\<^sub>\<tau> T2]"
-| "(t1 \<cdot>\<^sub>\<tau> T)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot>\<^sub>\<tau> T[Y \<mapsto> T2]\<^sub>\<tau>"
-| "X\<sharp>(Y,T,T2) \<Longrightarrow> (\<lambda>X<:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>X<:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])" 
-| "(\<lambda>x:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>x:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])"
+  "(Var x)[Y \<leadsto>\<^sub>\<tau> T2] = Var x"
+| "(t1 \<cdot> t2)[Y \<leadsto>\<^sub>\<tau> T2] = t1[Y \<leadsto>\<^sub>\<tau> T2] \<cdot> t2[Y \<leadsto>\<^sub>\<tau> T2]"
+| "(t1 \<cdot>\<^sub>\<tau> T)[Y \<leadsto>\<^sub>\<tau> T2] = t1[Y \<leadsto>\<^sub>\<tau> T2] \<cdot>\<^sub>\<tau> T[Y \<leadsto> T2]\<^sub>\<tau>"
+| "X\<sharp>(Y,T,T2) \<Longrightarrow> (\<lambda>X<:T. t)[Y \<leadsto>\<^sub>\<tau> T2] = (\<lambda>X<:T[Y \<leadsto> T2]\<^sub>\<tau>. t[Y \<leadsto>\<^sub>\<tau> T2])" 
+| "(\<lambda>x:T. t)[Y \<leadsto>\<^sub>\<tau> T2] = (\<lambda>x:T[Y \<leadsto> T2]\<^sub>\<tau>. t[Y \<leadsto>\<^sub>\<tau> T2])"
 apply(finite_guess | simp add: abs_fresh ty_vrs_fresh type_subst_fresh)+
 apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
 done
 
 lemma subst_trm_ty_fresh:
   fixes X::"tyvrs"
-  shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]"
+  shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<leadsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: Y T rule: trm.strong_induct)
     (auto simp: abs_fresh type_subst_fresh)
 
 lemma subst_trm_ty_fresh':
-  "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]"
+  "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<leadsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm)
 
 lemma subst_trm_ty_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   t::"trm"
-  shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]"
+  shows "pi\<bullet>(t[X \<leadsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<leadsto>\<^sub>\<tau> (pi\<bullet>T)]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
      (perm_simp add: fresh_bij subst_eqvt)+
 
 lemma subst_trm_ty_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   t::"trm"
-  shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]"
+  shows "pi\<bullet>(t[X \<leadsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<leadsto>\<^sub>\<tau> (pi\<bullet>T)]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
      (perm_simp add: fresh_left subst_eqvt')+
 
 lemma subst_trm_ty_rename:
-  "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
+  "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<leadsto>\<^sub>\<tau> U] = t[X \<leadsto>\<^sub>\<tau> U]"
   by (nominal_induct t avoiding: X Y U rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename)
 
@@ -1024,14 +1021,14 @@
 | T_Abs[intro]: "\<lbrakk> VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^sub>1. t\<^sub>2) : T\<^sub>1 \<rightarrow> T\<^sub>2"
 | T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 | T_TAbs[intro]:"\<lbrakk> TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^sub>1. t\<^sub>2) : (\<forall>X<:T\<^sub>1. T\<^sub>2)"
-| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^sub>1,T\<^sub>2); \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T\<^sub>11. T\<^sub>12); \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 : (T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>)" 
+| T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^sub>1,T\<^sub>2); \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T\<^sub>11. T\<^sub>12); \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 : (T\<^sub>12[X \<leadsto> T\<^sub>2]\<^sub>\<tau>)" 
 
 equivariance typing
 
 lemma better_T_TApp:
   assumes H1: "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)"
   and H2: "\<Gamma> \<turnstile> T2 <: T11"
-  shows "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (T12[X \<mapsto> T2]\<^sub>\<tau>)"
+  shows "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (T12[X \<leadsto> T2]\<^sub>\<tau>)"
 proof -
   obtain Y::tyvrs where Y: "Y \<sharp> (X, T12, \<Gamma>, t\<^sub>1, T2)"
     by (rule exists_fresh) (rule fin_supp)
@@ -1039,7 +1036,7 @@
   moreover from Y have "(\<forall>X<:T11. T12) = (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)"
     by (auto simp: ty.inject alpha' fresh_prod fresh_atm)
   with H1 have "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)" by simp
-  ultimately have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (([(Y, X)] \<bullet> T12)[Y \<mapsto> T2]\<^sub>\<tau>)" using H2
+  ultimately have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (([(Y, X)] \<bullet> T12)[Y \<leadsto> T2]\<^sub>\<tau>)" using H2
     by (rule T_TApp)
   with Y show ?thesis by (simp add: type_subst_rename)
 qed
@@ -1058,20 +1055,20 @@
   shows "VarB x T \<in> set \<Gamma> \<Longrightarrow> T closed_in \<Gamma>" using ok
   by induct (auto simp: binding.inject closed_in_def)
 
-lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B"
+lemma tyvrs_of_subst: "tyvrs_of (B[X \<leadsto> T]\<^sub>b) = tyvrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
-lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_dom \<Gamma>"
+lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<leadsto> T]\<^sub>e) = ty_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: tyvrs_of_subst)
 
-lemma vrs_of_subst: "vrs_of (B[X \<mapsto> T]\<^sub>b) = vrs_of B"
+lemma vrs_of_subst: "vrs_of (B[X \<leadsto> T]\<^sub>b) = vrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
-lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_dom \<Gamma>"
+lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<leadsto> T]\<^sub>e) = trm_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: vrs_of_subst)
 
 lemma subst_closed_in:
-  "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)"
+  "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<leadsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<leadsto> U]\<^sub>e @ \<Gamma>)"
 proof (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
   case (Tvar tyvrs)
   then show ?case
@@ -1086,7 +1083,7 @@
     by (simp add: closed_in_def ty.supp)
 next
   case (Forall tyvrs ty1 ty2)
-  then have "supp (ty1[X \<mapsto> U]\<^sub>\<tau>) \<subseteq> ty_dom (\<Delta>[X \<mapsto> U]\<^sub>e @ TVarB tyvrs ty2 # \<Gamma>)"
+  then have "supp (ty1[X \<leadsto> U]\<^sub>\<tau>) \<subseteq> ty_dom (\<Delta>[X \<leadsto> U]\<^sub>e @ TVarB tyvrs ty2 # \<Gamma>)"
     apply (simp add: closed_in_def ty.supp abs_supp)
     by (metis Diff_subset_conv Un_left_commute doms_append(1) le_supI2 ty_dom.simps(2) tyvrs_of.simps(2))
   with Forall show ?case
@@ -1147,36 +1144,36 @@
 inductive 
   eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" (\<open>_ \<longmapsto> _\<close> [60,60] 60)
 where
-  E_Abs         : "\<lbrakk> x \<sharp> v\<^sub>2; val v\<^sub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^sub>11. t\<^sub>12) \<cdot> v\<^sub>2 \<longmapsto> t\<^sub>12[x \<mapsto> v\<^sub>2]"
+  E_Abs         : "\<lbrakk> x \<sharp> v\<^sub>2; val v\<^sub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^sub>11. t\<^sub>12) \<cdot> v\<^sub>2 \<longmapsto> t\<^sub>12[x \<leadsto> v\<^sub>2]"
 | E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
 | E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'"
-| E_TAbs        : "X \<sharp> (T\<^sub>11, T\<^sub>2) \<Longrightarrow> (\<lambda>X<:T\<^sub>11. t\<^sub>12) \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2]"
+| E_TAbs        : "X \<sharp> (T\<^sub>11, T\<^sub>2) \<Longrightarrow> (\<lambda>X<:T\<^sub>11. t\<^sub>12) \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t\<^sub>12[X \<leadsto>\<^sub>\<tau> T\<^sub>2]"
 | E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T"
 
 lemma better_E_Abs[intro]:
   assumes H: "val v2"
-  shows "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> t12[x \<mapsto> v2]"
+  shows "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> t12[x \<leadsto> v2]"
 proof -
   obtain y::vrs where y: "y \<sharp> (x, t12, v2)" by (rule exists_fresh) (rule fin_supp)
   then have "y \<sharp> v2" by simp
-  then have "(\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]" using H
+  then have "(\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<leadsto> v2]" using H
     by (rule E_Abs)
   moreover from y have "(\<lambda>x:T11. t12) \<cdot> v2 = (\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2"
     by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
-  ultimately have "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]"
+  ultimately have "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<leadsto> v2]"
     by simp
   with y show ?thesis by (simp add: subst_trm_rename)
 qed
 
-lemma better_E_TAbs[intro]: "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> t12[X \<mapsto>\<^sub>\<tau> T2]"
+lemma better_E_TAbs[intro]: "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> t12[X \<leadsto>\<^sub>\<tau> T2]"
 proof -
   obtain Y::tyvrs where Y: "Y \<sharp> (X, t12, T11, T2)" by (rule exists_fresh) (rule fin_supp)
   then have "Y \<sharp> (T11, T2)" by simp
-  then have "(\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
+  then have "(\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<leadsto>\<^sub>\<tau> T2]"
     by (rule E_TAbs)
   moreover from Y have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 = (\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2"
     by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
-  ultimately have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
+  ultimately have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<leadsto>\<^sub>\<tau> T2]"
     by simp
   with Y show ?thesis by (simp add: subst_trm_ty_rename)
 qed
@@ -1210,7 +1207,7 @@
 lemma valid_subst:
   assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok"
   and closed: "P closed_in \<Gamma>"
-  shows "\<turnstile> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed
+  shows "\<turnstile> (\<Delta>[X \<leadsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed
 proof (induct \<Delta>)
   case Nil
   then show ?case
@@ -1409,7 +1406,7 @@
 
 theorem subst_type: \<comment> \<open>A.8\<close>
   assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
-  shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
+  shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<leadsto> u] : T" using H
  proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
    case (T_Var y T x u D)
    show ?case
@@ -1431,7 +1428,7 @@
    then show ?case by force
  next
    case (T_Sub t S T x u D)
-   then have "D @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto
+   then have "D @ \<Gamma> \<turnstile> t[x \<leadsto> u] : S" by auto
    moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening)
    ultimately show ?case by auto 
  next
@@ -1442,7 +1439,7 @@
  next
    case (T_TApp X t1 T2 T11 T12 x u D)
    then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
-   then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp
+   then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<leadsto> u]) : (T12[X \<leadsto> T2]\<^sub>\<tau>))" using T_TApp
      by (force simp: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
 qed
 
@@ -1450,24 +1447,24 @@
 
 lemma substT_subtype: \<comment> \<open>A.10\<close>
   assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
-  shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" 
+  shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<leadsto> P]\<^sub>\<tau> <: T[X \<leadsto> P]\<^sub>\<tau>" 
   using H
 proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
   case (SA_Top S X P D)
   then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
   moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto 
-  ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
+  ultimately have "\<turnstile> (D[X \<leadsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
   moreover from SA_Top have "S closed_in (D @ TVarB X Q # \<Gamma>)" by simp
-  then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in  (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in)
+  then have "S[X \<leadsto> P]\<^sub>\<tau> closed_in  (D[X \<leadsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in)
   ultimately show ?case by auto
 next
   case (SA_trans_TVar Y S T X P D)
   have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
-  then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
+  then have ST: "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<leadsto> P]\<^sub>\<tau> <: T[X \<leadsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
   from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
   from G_ok and SA_trans_TVar have X_\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
     by (auto intro: validE_append)
-  show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
+  show "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<leadsto> P]\<^sub>\<tau><:T[X \<leadsto> P]\<^sub>\<tau>"
   proof (cases "X = Y")
     assume eq: "X = Y"
     from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
@@ -1476,13 +1473,13 @@
     from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
     then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
     note \<open>\<Gamma>\<turnstile>P<:Q\<close>
-    moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
-    moreover have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def)
-    ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening)
-    with QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:S" by simp
-    moreover from XQ and ST and QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S<:T[X \<mapsto> P]\<^sub>\<tau>"
+    moreover from ST have "\<turnstile> (D[X \<leadsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
+    moreover have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def)
+    ultimately have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening)
+    with QS have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:S" by simp
+    moreover from XQ and ST and QS have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S<:T[X \<leadsto> P]\<^sub>\<tau>"
       by (simp add: type_subst_identity)
-    ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:T[X \<mapsto> P]\<^sub>\<tau>"
+    ultimately have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:T[X \<leadsto> P]\<^sub>\<tau>"
       by (rule subtype_transitivity)
     with eq show ?case by simp
   next
@@ -1492,9 +1489,9 @@
     then show ?case
     proof
       assume "TVarB Y S \<in> set D"
-      then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e)"
+      then have "TVarB Y (S[X \<leadsto> P]\<^sub>\<tau>) \<in> set (D[X \<leadsto> P]\<^sub>e)"
         by (rule ctxt_subst_mem_TVarB)
-      then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
+      then have "TVarB Y (S[X \<leadsto> P]\<^sub>\<tau>) \<in> set (D[X \<leadsto> P]\<^sub>e @ \<Gamma>)" by simp
       with neq and ST show ?thesis by auto
     next
       assume Y: "TVarB Y S \<in> set \<Gamma>"
@@ -1502,9 +1499,9 @@
       then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
       with Y have "X \<sharp> S"
         by (induct \<Gamma>) (auto simp: fresh_list_nil fresh_list_cons)
-      with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>"
+      with ST have "(D[X \<leadsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<leadsto> P]\<^sub>\<tau>"
         by (simp add: type_subst_identity)
-      moreover from Y have "TVarB Y S \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
+      moreover from Y have "TVarB Y S \<in> set (D[X \<leadsto> P]\<^sub>e @ \<Gamma>)" by simp
       ultimately show ?thesis using neq by auto
     qed
   qed
@@ -1513,8 +1510,8 @@
   note \<open>\<turnstile> (D @ TVarB X Q # \<Gamma>) ok\<close>
   moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
     by (auto dest: subtype_implies_closed)
-  ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
-  from closed have closed': "P closed_in (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
+  ultimately have ok: "\<turnstile> (D[X \<leadsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
+  from closed have closed': "P closed_in (D[X \<leadsto> P]\<^sub>e @ \<Gamma>)"
     by (simp add: closed_in_weaken')
   show ?case
   proof (cases "X = Y")
@@ -1523,14 +1520,14 @@
       by (auto intro: subtype_reflexivity)
   next
     assume neq: "X \<noteq> Y"
-    with SA_refl_TVar have "Y \<in> ty_dom (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
+    with SA_refl_TVar have "Y \<in> ty_dom (D[X \<leadsto> P]\<^sub>e @ \<Gamma>)"
       by (simp add: ty_dom_subst doms_append)
     with neq and ok show ?thesis by auto
   qed
 next
   case (SA_arrow T1 S1 S2 T2 X P D)
-  then have h1:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
-  from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
+  then have h1:"(D[X \<leadsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<leadsto> P]\<^sub>\<tau><:S1[X \<leadsto> P]\<^sub>\<tau>" using SA_arrow by auto
+  from SA_arrow have h2:"(D[X \<leadsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<leadsto> P]\<^sub>\<tau><:T2[X \<leadsto> P]\<^sub>\<tau>" using SA_arrow by auto
   show ?case using subtype_of.SA_arrow h1 h2 by auto
 next
   case (SA_all T1 S1 Y S2 T2 X P D)
@@ -1550,19 +1547,19 @@
 theorem substT_type: \<comment> \<open>A.11\<close>
   assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
   shows "G \<turnstile> P <: Q \<Longrightarrow>
-    (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
+    (D[X \<leadsto> P]\<^sub>e @ G) \<turnstile> t[X \<leadsto>\<^sub>\<tau> P] : T[X \<leadsto> P]\<^sub>\<tau>" using H
 proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
   case (T_Var x T X P D')
   have "G\<turnstile>P<:Q" by fact
   then have "P closed_in G" using subtype_implies_closed by auto
   moreover note \<open>\<turnstile> (D' @ TVarB X Q # G) ok\<close>
-  ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
+  ultimately have "\<turnstile> (D'[X \<leadsto> P]\<^sub>e @ G) ok" using valid_subst by auto
   moreover note \<open>VarB x T \<in> set (D' @ TVarB X Q # G)\<close>
   then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
-  then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)"
+  then have "(VarB x (T[X \<leadsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<leadsto> P]\<^sub>e @ G)"
   proof
     assume "VarB x T \<in> set D'"
-    then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D'[X \<mapsto> P]\<^sub>e)"
+    then have "VarB x (T[X \<leadsto> P]\<^sub>\<tau>) \<in> set (D'[X \<leadsto> P]\<^sub>e)"
       by (rule ctxt_subst_mem_VarB)
     then show ?thesis by simp
   next
@@ -1571,7 +1568,7 @@
     then have "X \<sharp> ty_dom G" using T_Var by (auto dest: validE_append)
     with ok have "X \<sharp> G" by (simp add: valid_ty_dom_fresh)
     moreover from x have "VarB x T \<in> set (D' @ G)" by simp
-    then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<mapsto> P]\<^sub>e)"
+    then have "VarB x (T[X \<leadsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<leadsto> P]\<^sub>e)"
       by (rule ctxt_subst_mem_VarB)
     ultimately show ?thesis
       by (simp add: ctxt_subst_append ctxt_subst_identity)
@@ -1579,8 +1576,8 @@
   ultimately show ?case by auto
 next
   case (T_App t1 T1 T2 t2 X P D')
-  then have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<mapsto> P]\<^sub>\<tau>" by auto
-  moreover from T_App have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t2[X \<mapsto>\<^sub>\<tau> P] : T1[X \<mapsto> P]\<^sub>\<tau>" by auto
+  then have "D'[X \<leadsto> P]\<^sub>e @ G \<turnstile> t1[X \<leadsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<leadsto> P]\<^sub>\<tau>" by auto
+  moreover from T_App have "D'[X \<leadsto> P]\<^sub>e @ G \<turnstile> t2[X \<leadsto>\<^sub>\<tau> P] : T1[X \<leadsto> P]\<^sub>\<tau>" by auto
   ultimately show ?case by auto
 next
   case (T_Abs x T1 t2 T2 X P D')
@@ -1602,7 +1599,7 @@
   moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
     by (auto dest: subtype_implies_closed)
   ultimately have X': "X' \<sharp> T11" by (rule closed_in_fresh)
-  from T_TApp have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<mapsto> P]\<^sub>\<tau>"
+  from T_TApp have "D'[X \<leadsto> P]\<^sub>e @ G \<turnstile> t1[X \<leadsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<leadsto> P]\<^sub>\<tau>"
     by simp
   with X' and T_TApp show ?case
     by (auto simp: fresh_atm type_substitution_lemma
@@ -1723,9 +1720,9 @@
       by (rule Abs_type') blast
     from \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close>
     have "\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11'" using T\<^sub>11 by (rule T_Sub)
-    with t\<^sub>12 have "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : S'" 
+    with t\<^sub>12 have "\<Gamma> \<turnstile> t\<^sub>12[x \<leadsto> t\<^sub>2] : S'" 
       by (rule subst_type [where \<Delta>="[]", simplified])
-    hence "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : T\<^sub>12" using S' by (rule T_Sub)
+    hence "\<Gamma> \<turnstile> t\<^sub>12[x \<leadsto> t\<^sub>2] : T\<^sub>12" using S' by (rule T_Sub)
     with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod)
   next
     case (E_App1 t''' t'' u)
@@ -1759,14 +1756,14 @@
       and "(TVarB X T\<^sub>11 # \<Gamma>) \<turnstile> S' <: T\<^sub>12"
       by (rule TAbs_type') blast
     hence "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : T\<^sub>12" by (rule T_Sub)
-    hence "\<Gamma> \<turnstile> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2] : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
+    hence "\<Gamma> \<turnstile> t\<^sub>12[X \<leadsto>\<^sub>\<tau> T\<^sub>2] : T\<^sub>12[X \<leadsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
       by (rule substT_type [where D="[]", simplified])
     with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
   next
     case (E_TApp t''' t'' T)
     from E_TApp have "t\<^sub>1 \<longmapsto> t''" by (simp add: trm.inject)
     then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^sub>11. T\<^sub>12)" by (rule T_TApp)
-    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^sub>2 : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
+    then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^sub>2 : T\<^sub>12[X \<leadsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
       by (rule better_T_TApp)
     with E_TApp show ?thesis by (simp add: trm.inject)
   qed (simp_all add: fresh_prod)
@@ -1817,7 +1814,7 @@
     thus ?case
     proof
       assume "val t\<^sub>2"
-      with t\<^sub>1 have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t3[x \<mapsto> t\<^sub>2]" by auto
+      with t\<^sub>1 have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t3[x \<leadsto> t\<^sub>2]" by auto
       thus ?case by auto
     next
       assume "\<exists>t'. t\<^sub>2 \<longmapsto> t'"
@@ -1839,7 +1836,7 @@
     assume "val t\<^sub>1"
     with T_TApp obtain x t S where "t\<^sub>1 = (\<lambda>x<:S. t)"
       by (auto dest!: TyAll_canonical)
-    hence "t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t[x \<mapsto>\<^sub>\<tau> T\<^sub>2]" by auto
+    hence "t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t[x \<leadsto>\<^sub>\<tau> T\<^sub>2]" by auto
     thus ?case by auto
   next
     assume "\<exists>t'. t\<^sub>1 \<longmapsto> t'" thus ?case by auto
diff -r ef362328b931 -r 12990a6dddcb src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Tue Oct 08 13:13:53 2024 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Tue Oct 08 15:02:17 2024 +0200
@@ -4,9 +4,6 @@
 imports "HOL-Nominal.Nominal"
 begin
 
-no_syntax
-  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  (\<open>(\<open>indent=1 notation=\<open>mixfix map\<close>\<close>[_])\<close>)
-
 atom_decl name
 
 nominal_datatype ty =
@@ -320,14 +317,14 @@
     (simp_all add: eqvts fresh_bij)
 
 abbreviation 
-  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" (\<open>_[_\<mapsto>_]\<close> [100,0,0] 100)
+  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" (\<open>_[_\<leadsto>_]\<close> [100,0,0] 100)
 where 
-  "t[x\<mapsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
+  "t[x\<leadsto>t'] \<equiv> [(x,t')]\<lparr>t\<rparr>"
 
 abbreviation 
-  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" (\<open>_[_\<mapsto>_]\<^sub>b\<close> [100,0,0] 100)
+  substb :: "btrm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> btrm" (\<open>_[_\<leadsto>_]\<^sub>b\<close> [100,0,0] 100)
 where 
-  "t[x\<mapsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
+  "t[x\<leadsto>t']\<^sub>b \<equiv> [(x,t')]\<lparr>t\<rparr>\<^sub>b"
 
 lemma lookup_forget:
   "(supp (map fst \<theta>)::name set) \<sharp>* x \<Longrightarrow> lookup \<theta> x = Var x"
@@ -360,7 +357,7 @@
 
 lemma psubst_cons:
   assumes "(supp (map fst \<theta>)::name set) \<sharp>* u"
-  shows "((x, u) # \<theta>)\<lparr>t\<rparr> = \<theta>\<lparr>t[x\<mapsto>u]\<rparr>" and "((x, u) # \<theta>)\<lparr>t'\<rparr>\<^sub>b = \<theta>\<lparr>t'[x\<mapsto>u]\<^sub>b\<rparr>\<^sub>b"
+  shows "((x, u) # \<theta>)\<lparr>t\<rparr> = \<theta>\<lparr>t[x\<leadsto>u]\<rparr>" and "((x, u) # \<theta>)\<lparr>t'\<rparr>\<^sub>b = \<theta>\<lparr>t'[x\<leadsto>u]\<^sub>b\<rparr>\<^sub>b"
   using assms
   by (nominal_induct t and t' avoiding: x u \<theta> rule: trm_btrm.strong_inducts)
     (simp_all add: fresh_list_nil fresh_list_cons psubst_forget)
@@ -406,38 +403,38 @@
 lemma subst_type_aux:
   assumes a: "\<Delta> @ [(x, U)] @ \<Gamma> \<turnstile> t : T"
   and b: "\<Gamma> \<turnstile> u : U"
-  shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" using a b
+  shows "\<Delta> @ \<Gamma> \<turnstile> t[x\<leadsto>u] : T" using a b
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, U)] @ \<Gamma>" t T avoiding: x u \<Delta> rule: typing.strong_induct)
   case (Var y T x u \<Delta>)
   from \<open>valid (\<Delta> @ [(x, U)] @ \<Gamma>)\<close>
   have valid: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
-  show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T"
+  show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<leadsto>u] : T"
   proof cases
     assume eq: "x = y"
     from Var eq have "T = U" by (auto intro: context_unique)
-    with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" by (auto intro: weakening)
+    with Var eq valid show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<leadsto>u] : T" by (auto intro: weakening)
   next
     assume ineq: "x \<noteq> y"
     from Var ineq have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" by simp
-    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<mapsto>u] : T" using ineq valid by auto
+    then show "\<Delta> @ \<Gamma> \<turnstile> Var y[x\<leadsto>u] : T" using ineq valid by auto
   qed
 next
   case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2)
   from refl \<open>\<Gamma> \<turnstile> u : U\<close>
-  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T\<^sub>1" by (rule Tuple)
+  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<leadsto>u] : T\<^sub>1" by (rule Tuple)
   moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close>
-  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T\<^sub>2" by (rule Tuple)
-  ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^sub>1[x\<mapsto>u], t\<^sub>2[x\<mapsto>u]\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" ..
+  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<leadsto>u] : T\<^sub>2" by (rule Tuple)
+  ultimately have "\<Delta> @ \<Gamma> \<turnstile> \<langle>t\<^sub>1[x\<leadsto>u], t\<^sub>2[x\<leadsto>u]\<rangle> : T\<^sub>1 \<otimes> T\<^sub>2" ..
   then show ?case by simp
 next
   case (Let p t T \<Delta>' s S)
   from refl \<open>\<Gamma> \<turnstile> u : U\<close>
-  have "\<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : T" by (rule Let)
+  have "\<Delta> @ \<Gamma> \<turnstile> t[x\<leadsto>u] : T" by (rule Let)
   moreover note \<open>\<turnstile> p : T \<Rightarrow> \<Delta>'\<close>
   moreover have "\<Delta>' @ (\<Delta> @ [(x, U)] @ \<Gamma>) = (\<Delta>' @ \<Delta>) @ [(x, U)] @ \<Gamma>" by simp
-  then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" using \<open>\<Gamma> \<turnstile> u : U\<close> by (rule Let)
-  then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<mapsto>u] : S" by simp
-  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<mapsto>u] IN s[x\<mapsto>u]) : S"
+  then have "(\<Delta>' @ \<Delta>) @ \<Gamma> \<turnstile> s[x\<leadsto>u] : S" using \<open>\<Gamma> \<turnstile> u : U\<close> by (rule Let)
+  then have "\<Delta>' @ \<Delta> @ \<Gamma> \<turnstile> s[x\<leadsto>u] : S" by simp
+  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (LET p = t[x\<leadsto>u] IN s[x\<leadsto>u]) : S"
     by (rule better_T_Let)
   moreover from Let have "(supp p::name set) \<sharp>* [(x, u)]"
     by (simp add: fresh_star_def fresh_list_nil fresh_list_cons)
@@ -446,9 +443,9 @@
   case (Abs y T t S)
   have "(y, T) # \<Delta> @ [(x, U)] @ \<Gamma> = ((y, T) # \<Delta>) @ [(x, U)] @ \<Gamma>"
     by simp
-  then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" using \<open>\<Gamma> \<turnstile> u : U\<close> by (rule Abs)
-  then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<mapsto>u] : S" by simp
-  then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<mapsto>u]) : T \<rightarrow> S"
+  then have "((y, T) # \<Delta>) @ \<Gamma> \<turnstile> t[x\<leadsto>u] : S" using \<open>\<Gamma> \<turnstile> u : U\<close> by (rule Abs)
+  then have "(y, T) # \<Delta> @ \<Gamma> \<turnstile> t[x\<leadsto>u] : S" by simp
+  then have "\<Delta> @ \<Gamma> \<turnstile> (\<lambda>y:T. t[x\<leadsto>u]) : T \<rightarrow> S"
     by (rule typing.Abs)
   moreover from Abs have "y \<sharp> [(x, u)]"
     by (simp add: fresh_list_nil fresh_list_cons)
@@ -456,10 +453,10 @@
 next
   case (App t\<^sub>1 T S t\<^sub>2)
   from refl \<open>\<Gamma> \<turnstile> u : U\<close>
-  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<mapsto>u] : T \<rightarrow> S" by (rule App)
+  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>1[x\<leadsto>u] : T \<rightarrow> S" by (rule App)
   moreover from refl \<open>\<Gamma> \<turnstile> u : U\<close>
-  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<mapsto>u] : T" by (rule App)
-  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^sub>1[x\<mapsto>u]) \<cdot> (t\<^sub>2[x\<mapsto>u]) : S"
+  have "\<Delta> @ \<Gamma> \<turnstile> t\<^sub>2[x\<leadsto>u] : T" by (rule App)
+  ultimately have "\<Delta> @ \<Gamma> \<turnstile> (t\<^sub>1[x\<leadsto>u]) \<cdot> (t\<^sub>2[x\<leadsto>u]) : S"
     by (rule typing.App)
   then show ?case by simp
 qed
@@ -488,7 +485,7 @@
 proof (induct arbitrary: \<Gamma>\<^sub>1 \<Gamma>\<^sub>2 t u T \<theta>)
   case (PVar x U)
   from \<open>\<Gamma>\<^sub>1 @ [(x, U)] @ \<Gamma>\<^sub>2 \<turnstile> t : T\<close> \<open>\<Gamma>\<^sub>2 \<turnstile> u : U\<close>
-  have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t[x\<mapsto>u] : T" by (rule subst_type_aux)
+  have "\<Gamma>\<^sub>1 @ \<Gamma>\<^sub>2 \<turnstile> t[x\<leadsto>u] : T" by (rule subst_type_aux)
   moreover from \<open>\<turnstile> PVar x U \<rhd> u \<Rightarrow> \<theta>\<close> have "\<theta> = [(x, u)]"
     by cases simp_all
   ultimately show ?case by simp
@@ -532,7 +529,7 @@
 | Abs: "t \<longmapsto> t' \<Longrightarrow> (\<lambda>x:T. t) \<longmapsto> (\<lambda>x:T. t')"
 | AppL: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
 | AppR: "u \<longmapsto> u' \<Longrightarrow> t \<cdot> u \<longmapsto> t \<cdot> u'"
-| Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<mapsto>u]"
+| Beta: "x \<sharp> u \<Longrightarrow> (\<lambda>x:T. t) \<cdot> u \<longmapsto> t[x\<leadsto>u]"
 | Let: "((supp p)::name set) \<sharp>* t \<Longrightarrow> distinct (pat_vars p) \<Longrightarrow>
     \<turnstile> p \<rhd> t \<Rightarrow> \<theta> \<Longrightarrow> (LET p = t IN u) \<longmapsto> \<theta>\<lparr>u\<rparr>"
 
@@ -556,7 +553,7 @@
 | Beta: "{x}"
 | Let: "(supp p)::name set"
 proof (simp_all add: fresh_star_def abs_fresh fin_supp)
-  show "x \<sharp> t[x\<mapsto>u]" if "x \<sharp> u" for x t u
+  show "x \<sharp> t[x\<leadsto>u]" if "x \<sharp> u" for x t u
     by (simp add: \<open>x \<sharp> u\<close> psubst_fresh(1))
 next
   show "\<forall>x\<in>supp p. (x::name) \<sharp> \<theta>\<lparr>u\<rparr>" 
diff -r ef362328b931 -r 12990a6dddcb src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Oct 08 13:13:53 2024 +0200
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Oct 08 15:02:17 2024 +0200
@@ -27,11 +27,11 @@
   of the algorithm W.\<close>
 
 inductive
-  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" (\<open>_ \<mapsto> _,_\<close> [60,60,60] 60)
+  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" (\<open>_ \<leadsto> _,_\<close> [60,60,60] 60)
 where
-  u_var: "(Var a) \<mapsto> [],(Var a)"
-| u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
-| u_lam: "t\<mapsto>xs,t' \<Longrightarrow> (Lam [x].t) \<mapsto> (x#xs),t'"
+  u_var: "(Var a) \<leadsto> [],(Var a)"
+| u_app: "(App t1 t2) \<leadsto> [],(App t1 t2)"
+| u_lam: "t\<leadsto>xs,t' \<Longrightarrow> (Lam [x].t) \<leadsto> (x#xs),t'"
 
 text \<open>
   We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
@@ -39,19 +39,19 @@
   bit clumsy).\<close> 
 
 lemma unbind_lambda_lambda1: 
-  shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
+  shows "Lam [x].Lam [x].(Var x)\<leadsto>[x,x],(Var x)"
 by (auto intro: unbind.intros)
 
 lemma unbind_lambda_lambda2: 
-  shows "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)"
+  shows "Lam [x].Lam [x].(Var x)\<leadsto>[y,z],(Var z)"
 proof -
   have "Lam [x].Lam [x].(Var x) = Lam [y].Lam [z].(Var z)" 
     by (auto simp add: lam.inject alpha calc_atm abs_fresh fresh_atm)
   moreover
-  have "Lam [y].Lam [z].(Var z) \<mapsto> [y,z],(Var z)"
+  have "Lam [y].Lam [z].(Var z) \<leadsto> [y,z],(Var z)"
     by (auto intro: unbind.intros)
   ultimately 
-  show "Lam [x].Lam [x].(Var x)\<mapsto>[y,z],(Var z)" by simp
+  show "Lam [x].Lam [x].(Var x)\<leadsto>[y,z],(Var z)" by simp
 qed
 
 text \<open>Unbind is equivariant ...\<close>
@@ -86,7 +86,7 @@
   easily prove that bind undoes the unbinding.\<close>
 
 lemma bind_unbind:
-  assumes a: "t \<mapsto> xs,t'"
+  assumes a: "t \<leadsto> xs,t'"
   shows "t = bind xs t'"
 using a by (induct) (auto)
 
@@ -113,7 +113,7 @@
   the binder x is fresh w.r.t. to the xs unbound previously.\<close>   
 
 lemma faulty1:
-  assumes a: "t\<mapsto>(x#xs),t'"
+  assumes a: "t\<leadsto>(x#xs),t'"
   shows "\<not>(x\<sharp>t') \<Longrightarrow> \<not>(x\<sharp>bind xs t')"
 using a
 by (nominal_induct t xs'\<equiv>"x#xs" t' avoiding: xs rule: unbind.strong_induct)
@@ -121,14 +121,14 @@
 
 text \<open>
   Obviously this lemma is bogus. For example, in 
-  case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). 
+  case Lam [x].Lam [x].(Var x) \<leadsto> [x,x],(Var x). 
   As a result, we can prove False.\<close>
 
 lemma false1:
   shows "False"
 proof -
   fix x
-  have "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)" 
+  have "Lam [x].Lam [x].(Var x)\<leadsto>[x,x],(Var x)" 
   and  "\<not>(x\<sharp>Var x)" by (simp_all add: unbind_lambda_lambda1 fresh_atm)
   then have "\<not>(x\<sharp>(bind [x] (Var x)))" by (rule faulty1)
   moreover