# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265118907 -3600
# Node ID 41fc4d3fc76465077b5a35828e53faae26a5b510
# Parent 163d6917af629721c640fcac4a7295eb71e2549c
First experiments in Terms.
diff -r 163d6917af62 -r 41fc4d3fc764 Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy Tue Feb 02 13:10:46 2010 +0100
+++ b/Quot/Nominal/LamEx.thy Tue Feb 02 14:55:07 2010 +0100
@@ -619,5 +619,5 @@
-end
+end<
diff -r 163d6917af62 -r 41fc4d3fc764 Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy Tue Feb 02 13:10:46 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy Tue Feb 02 14:55:07 2010 +0100
@@ -4,6 +4,7 @@
(* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)
+(* Currently not used, still needed needed? *)
lemma supp_finite_set:
fixes S::"atom set"
assumes "finite S"
diff -r 163d6917af62 -r 41fc4d3fc764 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy Tue Feb 02 13:10:46 2010 +0100
+++ b/Quot/Nominal/Terms.thy Tue Feb 02 14:55:07 2010 +0100
@@ -1,5 +1,5 @@
theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs"
begin
atom_decl name
@@ -8,11 +8,11 @@
section {*** lets with binding patterns ***}
-datatype trm1 =
- Vr1 "name"
-| Ap1 "trm1" "trm1"
-| Lm1 "name" "trm1" --"name is bound in trm1"
-| Lt1 "bp" "trm1" "trm1" --"all variables in bp are bound in the 2nd trm1"
+datatype rtrm1 =
+ rVr1 "name"
+| rAp1 "rtrm1" "rtrm1"
+| rLm1 "name" "rtrm1" --"name is bound in trm1"
+| rLt1 "bp" "rtrm1" "rtrm1" --"all variables in bp are bound in the 2nd trm1"
and bp =
BUnit
| BVr "name"
@@ -28,78 +28,96 @@
(* needs to be calculated by the package *)
primrec
- fv_trm1 and fv_bp
+ rfv_trm1 and rfv_bp
where
- "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) - {atom x}"
-| "fv_trm1 (Lt1 bp t1 t2) = (fv_trm1 t1) \<union> (fv_trm1 t2 - bv1 bp)"
-| "fv_bp (BUnit) = {}"
-| "fv_bp (BVr x) = {atom x}"
-| "fv_bp (BPr b1 b2) = (fv_bp b1) \<union> (fv_bp b2)"
+ "rfv_trm1 (rVr1 x) = {atom x}"
+| "rfv_trm1 (rAp1 t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2)"
+| "rfv_trm1 (rLm1 x t) = (rfv_trm1 t) - {atom x}"
+| "rfv_trm1 (rLt1 bp t1 t2) = (rfv_trm1 t1) \<union> (rfv_trm1 t2 - bv1 bp)"
+| "rfv_bp (BUnit) = {}"
+| "rfv_bp (BVr x) = {atom x}"
+| "rfv_bp (BPr b1 b2) = (rfv_bp b1) \<union> (rfv_bp b2)"
(* needs to be stated by the package *)
instantiation
- trm1 and bp :: pt
+ rtrm1 and bp :: pt
begin
primrec
- permute_trm1 and permute_bp
+ permute_rtrm1 and permute_bp
where
- "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_rtrm1 pi (rVr1 a) = rVr1 (pi \<bullet> a)"
+| "permute_rtrm1 pi (rAp1 t1 t2) = rAp1 (permute_rtrm1 pi t1) (permute_rtrm1 pi t2)"
+| "permute_rtrm1 pi (rLm1 a t) = rLm1 (pi \<bullet> a) (permute_rtrm1 pi t)"
+| "permute_rtrm1 pi (rLt1 bp t1 t2) = rLt1 (permute_bp pi bp) (permute_rtrm1 pi t1) (permute_rtrm1 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
+lemma pt_rtrm1_bp_zero:
+ fixes t::rtrm1
and b::bp
shows "0 \<bullet> t = t"
and "0 \<bullet> b = b"
-apply(induct t and b rule: trm1_bp.inducts)
+apply(induct t and b rule: rtrm1_bp.inducts)
apply(simp_all)
done
-lemma pt_trm1_bp_plus:
- fixes t::trm1
+lemma pt_rtrm1_bp_plus:
+ fixes t::rtrm1
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(induct t and b rule: rtrm1_bp.inducts)
apply(simp_all)
done
instance
apply default
-apply(simp_all add: pt_trm1_bp_zero pt_trm1_bp_plus)
+apply(simp_all add: pt_rtrm1_bp_zero pt_rtrm1_bp_plus)
done
end
inductive
- alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
+ alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
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. (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.(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"
+ a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"
+| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"
+| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"
+| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"
+
+lemma alpha_inj:
+"(rVr1 a \<approx>1 rVr1 b) = (a = b)"
+"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"
+"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))"
+"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))"
+apply -
+apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
+done
+
+lemma rfv1_eqvt[eqvt]:
+ shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
+ sorry
+
+lemma alpha1_eqvt:
+ shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"
+ sorry
lemma alpha1_equivp: "equivp alpha1"
sorry
-quotient_type qtrm1 = trm1 / alpha1
+quotient_type trm1 = rtrm1 / alpha1
by (rule alpha1_equivp)
+quotient_definition
+ "Vr1 :: name \<Rightarrow> trm1"
+as
+ "rVr1"
+
section {*** lets with single assignments ***}