--- 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
--- 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
--- 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
--- 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>"
--- 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