# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265378989 -3600
# Node ID 53350d409473a4a44a4aa384dd3a59d4b6c1298a
# Parent  6deecec6795f3e35111260f0e555cf63a823ea88
Cleaned Terms using [lifted] and found a workaround for the instantiation problem.

diff -r 6deecec6795f -r 53350d409473 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Fri Feb 05 11:37:18 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 05 15:09:49 2010 +0100
@@ -203,36 +203,8 @@
 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)
+lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
+lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 
 instantiation trm1 and bp :: pt
 begin
@@ -242,49 +214,21 @@
 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)
+apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted])
 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
+lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
+
+lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted]
 
-lemma fv_trm1_eqvt:
-  shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)"
-apply(lifting rfv_trm1_eqvt)
-done
+lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted]
 
-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
+lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemma lm1_supp_pre:
   shows "(supp (atom x, t)) supports (Lm1 x t) "
@@ -827,6 +771,8 @@
   shows "(alphalts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)
 
+lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]
+
 instantiation trm5 and lts :: pt
 begin
 
@@ -840,23 +786,19 @@
 as
   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"
 
-lemma permute_trm5_lts:
-"pi \<bullet> (Vr5 a) = Vr5 (pi \<bullet> a)"
-"pi \<bullet> (Ap5 t1 t2) = Ap5 (pi \<bullet> t1) (pi \<bullet> t2)"
-"pi \<bullet> (Lt5 ls t) = Lt5 (pi \<bullet> ls) (pi \<bullet> t)"
-"pi \<bullet> Lnil = Lnil"
-"pi \<bullet> (Lcons n t ls) = Lcons (pi \<bullet> n) (pi \<bullet> t) (pi \<bullet> ls)"
-by (lifting permute_rtrm5_permute_rlts.simps)
-
 lemma trm5_lts_zero:
   "0 \<bullet> (x\<Colon>trm5) = x"
   "0 \<bullet> (y\<Colon>lts) = y"
-sorry
+apply(induct x and y rule: trm5_lts_inducts)
+apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
+done
 
 lemma trm5_lts_plus:
   "(p + q) \<bullet> (x\<Colon>trm5) = p \<bullet> q \<bullet> x"
   "(p + q) \<bullet> (y\<Colon>lts) = p \<bullet> q \<bullet> y"
-sorry
+apply(induct x and y rule: trm5_lts_inducts)
+apply(simp_all add: permute_rtrm5_permute_rlts.simps[quot_lifted])
+done
 
 instance
 apply default
@@ -865,30 +807,13 @@
 
 end
 
-lemma alpha5_INJ:
-  "((Vr5 a) = (Vr5 b)) = (a = b)"
-  "(Ap5 t1 s1 = Ap5 t2 s2) = (t1 = t2 \<and> s1 = s2)"
-  "(Lt5 l1 t1 = Lt5 l2 t2) =
-     ((\<exists>pi. ((bv5 l1, t1) \<approx>gen (op =) fv_trm5 pi (bv5 l2, t2))) \<and>
-      (\<exists>pi. ((bv5 l1, l1) \<approx>gen (op =) fv_lts pi (bv5 l2, l2))))"
-  "Lnil = Lnil"
-  "(Lcons n1 t1 ls1 = Lcons n2 t2 ls2) = (n1 = n2 \<and> ls1 = ls2 \<and> t1 = t2)"
-unfolding alpha_gen
-apply(lifting alpha5_inj[unfolded alpha_gen])
-done
+lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]
+
+lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemma bv5[simp]:
-  "bv5 Lnil = {}"
-  "bv5 (Lcons n t ltl) = {atom n} \<union> bv5 ltl"
-by (lifting rbv5.simps)
+lemmas bv5[simp] = rbv5.simps[quot_lifted]
 
-lemma fv_trm5_lts[simp]:
-  "fv_trm5 (Vr5 n) = {atom n}"
-  "fv_trm5 (Ap5 t s) = fv_trm5 t \<union> fv_trm5 s"
-  "fv_trm5 (Lt5 lts t) = fv_trm5 t - bv5 lts \<union> (fv_lts lts - bv5 lts)"
-  "fv_lts Lnil = {}"
-  "fv_lts (Lcons n t ltl) = fv_trm5 t \<union> fv_lts ltl"
-by (lifting rfv_trm5_rfv_lts.simps)
+lemmas fv_trm5_lts[simp] = rfv_trm5_rfv_lts.simps[quot_lifted]
 
 lemma lets_ok:
   "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"