# 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 ***}