--- a/Quot/Nominal/Terms.thy Wed Jan 27 12:19:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy Wed Jan 27 12:21:40 2010 +0100
@@ -23,37 +23,59 @@
bv1
where
"bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {x}"
+| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
(* needs to be calculated by the package *)
primrec
fv_trm1 and fv_bp
where
- "fv_trm1 (Vr1 x) = {x}"
+ "fv_trm1 (Vr1 x) = {atom x}"
| "fv_trm1 (Ap1 t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2)"
-| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {x}"
+| "fv_trm1 (Lm1 x t) = (fv_trm1 t) - {atom x}"
| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)"
| "fv_bp (BUnit) = {}"
-| "fv_bp (BVr x) = {x}"
+| "fv_bp (BVr x) = {atom x}"
| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"
(* needs to be stated by the package *)
instantiation
- trm1 :: pt
- bp :: pt
+ trm1 and bp :: pt
begin
primrec
- perm_trm1 and perm_bp
+ permute_trm1 and permute_bp
where
- "perm_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)"
-| "perm_trm1 pi (Ap1 t1 t2) = Ap1 (perm_trm1 pi t1) (perm_trm1 pi t2)"
-| "perm_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (perm_trm1 pi t)"
-| "perm_trm1 pi (Lt1 bp t1 t2) = Lt1 (perm_bp pi bp) (perm_trm1 pi t1) (perm_trm1 pi t2)"
-| "perm_bp pi (BUnit) = BUnit"
-| "perm_bp pi (BVr a) = BVr (pi \<bullet> a)"
-| "perm_bp pi (BPr bp1 bp2) = BPr (perm_bp pi bp1) (perm_bp pi bp2)"
+ "permute_trm1 pi (Vr1 a) = Vr1 (pi \<bullet> a)"
+| "permute_trm1 pi (Ap1 t1 t2) = Ap1 (permute_trm1 pi t1) (permute_trm1 pi t2)"
+| "permute_trm1 pi (Lm1 a t) = Lm1 (pi \<bullet> a) (permute_trm1 pi t)"
+| "permute_trm1 pi (Lt1 bp t1 t2) = Lt1 (permute_bp pi bp) (permute_trm1 pi t1) (permute_trm1 pi t2)"
+| "permute_bp pi (BUnit) = BUnit"
+| "permute_bp pi (BVr a) = BVr (pi \<bullet> a)"
+| "permute_bp pi (BPr bp1 bp2) = BPr (permute_bp pi bp1) (permute_bp pi bp2)"
+
+lemma pt_trm1_bp_zero:
+ fixes t::trm1
+ and b::bp
+ shows "0 \<bullet> t = t"
+ and "0 \<bullet> b = b"
+apply(induct t and b rule: trm1_bp.inducts)
+apply(simp_all)
+done
+
+lemma pt_trm1_bp_plus:
+ fixes t::trm1
+ and b::bp
+ shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+apply(induct t and b rule: trm1_bp.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_trm1_bp_zero pt_trm1_bp_plus)
+done
end
@@ -62,18 +84,18 @@
where
a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)"
| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2"
-| a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and>
- (fv_trm1 t - {a})\<sharp>* pi \<and>
- (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)
+| a3: "\<exists>pi. (fv_trm1 t - {atom a} = fv_trm1 s - {atom b} \<and>
+ (fv_trm1 t - {atom a})\<sharp>* pi \<and>
+ (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)
\<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s"
-| a4: "\<exists>pi::name prm.(
- t1 \<approx>1 t2 \<and>
- (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and>
- (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and>
- (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *)
- ) \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2"
+| a4: "\<exists>pi.(t1 \<approx>1 t2 \<and>
+ (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and>
+ (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and>
+ (pi \<bullet> s1 = s2) (* Optional: \<and> (pi \<bullet> b1 = b2) *))
+ \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2"
-lemma alpha1_equivp: "equivp alpha1" sorry
+lemma alpha1_equivp: "equivp alpha1"
+ sorry
quotient_type qtrm1 = trm1 / alpha1
by (rule alpha1_equivp)
@@ -93,32 +115,55 @@
primrec
bv2
where
- "bv2 (As x t) = {x}"
+ "bv2 (As x t) = {atom x}"
(* needs to be calculated by the package *)
primrec
fv_trm2 and fv_assign
where
- "fv_trm2 (Vr2 x) = {x}"
+ "fv_trm2 (Vr2 x) = {atom x}"
| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
-| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {x}"
+| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
| "fv_assign (As x t) = (fv_trm2 t)"
(* needs to be stated by the package *)
-overloading
- perm_trm2 \<equiv> "perm :: 'x prm \<Rightarrow> trm2 \<Rightarrow> trm2" (unchecked)
- perm_assign \<equiv> "perm :: 'x prm \<Rightarrow> assign \<Rightarrow> assign" (unchecked)
+instantiation
+ trm2 and assign :: pt
begin
primrec
- perm_trm2 and perm_assign
+ permute_trm2 and permute_assign
where
- "perm_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
-| "perm_trm2 pi (Ap2 t1 t2) = Ap2 (perm_trm2 pi t1) (perm_trm2 pi t2)"
-| "perm_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (perm_trm2 pi t)"
-| "perm_trm2 pi (Lt2 as t) = Lt2 (perm_assign pi as) (perm_trm2 pi t)"
-| "perm_assign pi (As a t) = As (pi \<bullet> a) (perm_trm2 pi t)"
+ "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
+| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
+| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
+| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
+| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+
+lemma pt_trm2_assign_zero:
+ fixes t::trm2
+ and b::assign
+ shows "0 \<bullet> t = t"
+ and "0 \<bullet> b = b"
+apply(induct t and b rule: trm2_assign.inducts)
+apply(simp_all)
+done
+
+lemma pt_trm2_assign_plus:
+ fixes t::trm2
+ and b::assign
+ shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+apply(induct t and b rule: trm2_assign.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+done
+
end
@@ -127,18 +172,19 @@
where
a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
-| a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and>
- (fv_trm2 t - {a})\<sharp>* pi \<and>
- (pi \<bullet> t) \<approx>2 s \<and>
- (pi \<bullet> a) = b)
+| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and>
+ (fv_trm2 t - {atom a})\<sharp>* pi \<and>
+ (pi \<bullet> t) \<approx>2 s \<and>
+ (pi \<bullet> a) = b)
\<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
-| a4: "\<exists>pi::name prm. (
+| a4: "\<exists>pi. (
fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
(fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *)
) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
-lemma alpha2_equivp: "equivp alpha2" sorry
+lemma alpha2_equivp: "equivp alpha2"
+ sorry
quotient_type qtrm2 = trm2 / alpha2
by (rule alpha2_equivp)
@@ -159,33 +205,56 @@
bv3
where
"bv3 ANil = {}"
-| "bv3 (ACons x t as) = {x} \<union> (bv3 as)"
+| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
primrec
fv_trm3 and fv_assigns
where
- "fv_trm3 (Vr3 x) = {x}"
+ "fv_trm3 (Vr3 x) = {atom x}"
| "fv_trm3 (Ap3 t1 t2) = (fv_trm3 t1) \<union> (fv_trm3 t2)"
-| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {x}"
+| "fv_trm3 (Lm3 x t) = (fv_trm3 t) - {atom x}"
| "fv_trm3 (Lt3 as t) = (fv_trm3 t - bv3 as) \<union> (fv_assigns as)"
| "fv_assigns (ANil) = {}"
| "fv_assigns (ACons x t as) = (fv_trm3 t) \<union> (fv_assigns as)"
(* needs to be stated by the package *)
-overloading
- perm_trm3 \<equiv> "perm :: 'x prm \<Rightarrow> trm3 \<Rightarrow> trm3" (unchecked)
- perm_assigns \<equiv> "perm :: 'x prm \<Rightarrow> assigns \<Rightarrow> assigns" (unchecked)
+instantiation
+ trm3 and assigns :: pt
begin
primrec
- perm_trm3 and perm_assigns
+ permute_trm3 and permute_assigns
where
- "perm_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
-| "perm_trm3 pi (Ap3 t1 t2) = Ap3 (perm_trm3 pi t1) (perm_trm3 pi t2)"
-| "perm_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (perm_trm3 pi t)"
-| "perm_trm3 pi (Lt3 as t) = Lt3 (perm_assigns pi as) (perm_trm3 pi t)"
-| "perm_assigns pi (ANil) = ANil"
-| "perm_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (perm_trm3 pi t) (perm_assigns pi as)"
+ "permute_trm3 pi (Vr3 a) = Vr3 (pi \<bullet> a)"
+| "permute_trm3 pi (Ap3 t1 t2) = Ap3 (permute_trm3 pi t1) (permute_trm3 pi t2)"
+| "permute_trm3 pi (Lm3 a t) = Lm3 (pi \<bullet> a) (permute_trm3 pi t)"
+| "permute_trm3 pi (Lt3 as t) = Lt3 (permute_assigns pi as) (permute_trm3 pi t)"
+| "permute_assigns pi (ANil) = ANil"
+| "permute_assigns pi (ACons a t as) = ACons (pi \<bullet> a) (permute_trm3 pi t) (permute_assigns pi as)"
+
+lemma pt_trm3_assigns_zero:
+ fixes t::trm3
+ and b::assigns
+ shows "0 \<bullet> t = t"
+ and "0 \<bullet> b = b"
+apply(induct t and b rule: trm3_assigns.inducts)
+apply(simp_all)
+done
+
+lemma pt_trm3_assigns_plus:
+ fixes t::trm3
+ and b::assigns
+ shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+ and "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
+apply(induct t and b rule: trm3_assigns.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_trm3_assigns_zero pt_trm3_assigns_plus)
+done
+
end
@@ -194,18 +263,19 @@
where
a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"
| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"
-| a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and>
- (fv_trm3 t - {a})\<sharp>* pi \<and>
- (pi \<bullet> t) \<approx>3 s \<and>
- (pi \<bullet> a) = b)
+| a3: "\<exists>pi. (fv_trm3 t - {atom a} = fv_trm3 s - {atom b} \<and>
+ (fv_trm3 t - {atom a})\<sharp>* pi \<and>
+ (pi \<bullet> t) \<approx>3 s \<and>
+ (pi \<bullet> a) = b)
\<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
-| a4: "\<exists>pi::name prm. (
+| a4: "\<exists>pi. (
fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
(fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *)
) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
-lemma alpha3_equivp: "equivp alpha3" sorry
+lemma alpha3_equivp: "equivp alpha3"
+ sorry
quotient_type qtrm3 = trm3 / alpha3
by (rule alpha3_equivp)
@@ -223,26 +293,27 @@
primrec
fv_trm4 and fv_trm4_list
where
- "fv_trm4 (Vr4 x) = {x}"
+ "fv_trm4 (Vr4 x) = {atom x}"
| "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
-| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {x}"
+| "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {atom x}"
| "fv_trm4_list ([]) = {}"
| "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)"
(* needs to be stated by the package *)
(* there cannot be a clause for lists, as *)
-(* permutations are already defined in Nominal (also functions, options, and so on) *)
-overloading
- perm_trm4 \<equiv> "perm :: 'x prm \<Rightarrow> trm4 \<Rightarrow> trm4" (unchecked)
+(* permuteutations are already defined in Nominal (also functions, options, and so on) *)
+instantiation
+ trm4 :: pt
begin
+(* does not work yet *)
primrec
- perm_trm4
+ permute_trm4
where
- "perm_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
-| "perm_trm4 pi (Ap4 t ts) = Ap4 (perm_trm4 pi t) (pi \<bullet> ts)"
-| "perm_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (perm_trm4 pi t)"
+ "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)"
+| "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute pi ts)"
+| "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)"
end