--- a/Quot/Nominal/Terms.thy	Tue Feb 02 14:55:07 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 02 16:51:00 2010 +0100
@@ -19,6 +19,7 @@
 | BPr "bp" "bp"
 
 (* to be given by the user *)
+
 primrec 
   bv1
 where
@@ -87,7 +88,7 @@
 | 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:
+lemma alpha1_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)))"
@@ -99,7 +100,7 @@
 apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)
 done
 
-lemma rfv1_eqvt[eqvt]:
+lemma rfv_trm1_eqvt[eqvt]:
   shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)"
   sorry
 
@@ -118,6 +119,148 @@
 as
   "rVr1"
 
+quotient_definition
+  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+as
+  "rAp1"
+
+quotient_definition
+  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
+as
+  "rLm1"
+
+quotient_definition
+  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
+as
+  "rLt1"
+
+quotient_definition
+  "fv_trm1 :: trm1 \<Rightarrow> atom set"
+as
+  "rfv_trm1"
+
+lemma alpha_rfv1:
+  shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s"
+  apply(induct rule: alpha1.induct)
+  apply(simp_all add: alpha_gen.simps)
+  done
+
+lemma [quot_respect]:
+ "(op = ===> alpha1) rVr1 rVr1"
+ "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
+ "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
+ "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
+apply (auto intro: alpha1.intros)
+apply(rule a3) apply (rule_tac x="0" in exI)
+apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
+apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+done
+
+lemma [quot_respect]:
+  "(op = ===> alpha1 ===> alpha1) permute permute"
+apply auto
+apply (rule alpha1_eqvt)
+apply simp
+done
+
+lemma [quot_respect]:
+  "(alpha1 ===> op =) rfv_trm1 rfv_trm1"
+apply (simp add: alpha_rfv1)
+done
+
+lemma trm1_bp_induct: "
+\<lbrakk>\<And>name. P1 (Vr1 name);
+ \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ \<And>bp rtrm11 rtrm12.
+    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ P2 BUnit; \<And>name. P2 (BVr name);
+ \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+\<Longrightarrow> P1 rtrma \<and> P2 bpa"
+apply (lifting rtrm1_bp.induct)
+done
+
+lemma trm1_bp_inducts: "
+\<lbrakk>\<And>name. P1 (Vr1 name);
+ \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ \<And>bp rtrm11 rtrm12.
+    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ P2 BUnit; \<And>name. P2 (BVr name);
+ \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+\<Longrightarrow> P1 rtrma"
+"\<lbrakk>\<And>name. P1 (Vr1 name);
+ \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12);
+ \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1);
+ \<And>bp rtrm11 rtrm12.
+    \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12);
+ P2 BUnit; \<And>name. P2 (BVr name);
+ \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk>
+\<Longrightarrow> P2 bpa"
+by (lifting rtrm1_bp.inducts)
+
+instantiation trm1 and bp :: pt
+begin
+
+quotient_definition
+  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
+as
+  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
+
+lemma permute_trm1 [simp]:
+  shows "pi \<bullet> Vr1 a = Vr1 (pi \<bullet> a)"
+  and   "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)"
+  and   "pi \<bullet> Lm1 a t = Lm1 (pi \<bullet> a) (pi \<bullet> t)"
+  and   "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)"
+apply -
+apply(lifting permute_rtrm1_permute_bp.simps(1))
+apply(lifting permute_rtrm1_permute_bp.simps(2))
+apply(lifting permute_rtrm1_permute_bp.simps(3))
+apply(lifting permute_rtrm1_permute_bp.simps(4))
+done
+instance
+apply default
+apply(induct_tac [!] x rule: trm1_bp_inducts(1))
+apply(simp_all)
+done
+
+end
+
+lemma fv_trm1:
+"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)"
+apply -
+apply (lifting rfv_trm1_rfv_bp.simps(1))
+apply (lifting rfv_trm1_rfv_bp.simps(2))
+apply (lifting rfv_trm1_rfv_bp.simps(3))
+apply (lifting rfv_trm1_rfv_bp.simps(4))
+done
+
+lemma fv_trm1_eqvt:
+  shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)"
+apply(lifting rfv_trm1_eqvt)
+done
+
+lemma alpha1_INJ:
+"(Vr1 a = Vr1 b) = (a = b)"
+"(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)"
+"(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))"
+"(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))"
+unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen])
+done
+
+lemma supp_fv:
+  shows "supp t = fv_trm1 t"
+apply(induct t rule: trm1_bp_inducts(1))
+apply(simp_all add: supp_def permute_trm1 alpha1_INJ fv_trm1)
+apply(simp_all only: supp_at_base[simplified supp_def])
+apply(simp_all add: Collect_imp_eq Collect_neg_eq)
+sorry (* Lam & Let still to do *)
+
+
 
 section {*** lets with single assignments ***}