diff -r 92c43c96027e -r 4e0b89d886ac Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sat Jan 16 02:09:38 2010 +0100
@@ -108,44 +108,12 @@
 begin
 
 quotient_definition
-   "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
+  "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
 as
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end
 
-(* lemmas that need to be lifted *)
-lemma pi_var_eqvt1:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)"
-  by (simp add: alpha_refl)
-
-lemma pi_var_eqvt2:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rVar a) = rVar (pi \<bullet> a)"
-  by (simp)
-
-lemma pi_app_eqvt1:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rApp t1 t2) \<approx> rApp (pi \<bullet> t1) (pi \<bullet> t2)"
-  by (simp add: alpha_refl)
-
-lemma pi_app_eqvt2:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rApp t1 t2) = rApp (pi \<bullet> t1) (pi \<bullet> t2)"
-  by (simp)
-
-lemma pi_lam_eqvt1:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rLam a t) \<approx> rLam (pi \<bullet> a) (pi \<bullet> t)"
-  by (simp add: alpha_refl)
-
-lemma pi_lam_eqvt2:
-  fixes pi::"'x prm"
-  shows "(pi \<bullet> rLam a t) = rLam (pi \<bullet> a) (pi \<bullet> t)"
-  by (simp add: alpha)
-
-
 lemma real_alpha:
   assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
@@ -189,38 +157,35 @@
   apply (simp_all add: rlam.inject alpha_refl)
   done
 
-lemma pi_var1:
-  fixes pi::"'x prm"
-  shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
-  by (lifting pi_var_eqvt1)
 
-lemma pi_var2:
-  fixes pi::"'x prm"
-  shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
-  by (lifting pi_var_eqvt2)
-
-
-lemma pi_app: 
-  fixes pi::"'x prm"
-  shows "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
-  by (lifting pi_app_eqvt2)
+lemma lam_induct:
+  "\<lbrakk>\<And>name. P (Var name);
+    \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+    \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> 
+    \<Longrightarrow> P lam"
+  by (lifting rlam.induct)
 
-lemma pi_lam: 
-  fixes pi::"'x prm"
-  shows "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
-  by (lifting pi_lam_eqvt2)
+lemma perm_lam [simp]:
+  fixes pi::"'a prm"
+  shows "pi \<bullet> Var a = Var (pi \<bullet> a)"
+  and   "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"
+  and   "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"
+apply(lifting perm_rlam.simps)
+done
 
-lemma fv_var: 
+instance lam::pt_name
+apply(default)
+apply(induct_tac [!] x rule: lam_induct)
+apply(simp_all add: pt_name2 pt_name3)
+done
+
+lemma fv_lam [simp]: 
   shows "fv (Var a) = {a}"
-  by  (lifting rfv_var)
+  and   "fv (App t1 t2) = fv t1 \<union> fv t2"
+  and   "fv (Lam a t) = fv t - {a}"
+apply(lifting rfv_var rfv_app rfv_lam)
+done
 
-lemma fv_app: 
-  shows "fv (App t1 t2) = fv t1 \<union> fv t2"
-  by (lifting rfv_app)
-
-lemma fv_lam: 
-  shows "fv (Lam a t) = fv t - {a}"
-  by (lifting rfv_lam)
 
 lemma a1: 
   "a = b \<Longrightarrow> Var a = Var b"
@@ -260,7 +225,7 @@
 
 lemma var_supp1:
   shows "(supp (Var a)) = ((supp a)::name set)"
-apply(simp add: supp_def pi_var1 var_inject)
+apply(simp add: supp_def var_inject)
 done
 
 lemma var_supp:
@@ -271,37 +236,15 @@
 
 lemma app_supp:
   shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)"
-apply(simp only: supp_def pi_app app_inject)
+apply(simp only: perm_lam supp_def app_inject)
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
 
 lemma lam_supp:
   shows "supp (Lam x t) = ((supp ([x].t))::name set)"
-apply(simp add: supp_def pi_lam)
+apply(simp add: supp_def)
 sorry
 
-lemma lam_induct:
-  "\<lbrakk>\<And>name. P (Var name);
-    \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
-    \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> 
-    \<Longrightarrow> P lam"
-  by (lifting rlam.induct)
-
-instance lam::pt_name
-apply(default)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1)
-apply(simp add: pi_app)
-apply(simp add: pi_lam)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1 pt_name2)
-apply(simp add: pi_app)
-apply(simp add: pi_lam pt_name2)
-apply(induct_tac x rule: lam_induct)
-apply(simp add: pi_var1 pt_name3)
-apply(simp add: pi_app)
-apply(simp add: pi_lam pt_name3)
-done
 
 instance lam::fs_name
 apply(default)
@@ -328,7 +271,7 @@
   proof (induct lam rule: lam_induct)
     case (1 name pi)
     show "P a (pi \<bullet> Var name)"
-      apply (simp only: pi_var1)
+      apply (simp)
       apply (rule a1)
       done
   next
@@ -336,7 +279,7 @@
     have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact
     have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact
     show "P a (pi \<bullet> App lam1 lam2)"
-      apply (simp only: pi_app)
+      apply (simp)
       apply (rule a2)
       apply (rule b1)
       apply (rule b2)
@@ -361,10 +304,10 @@
       apply(simp add: fresh_lam)
       done
     show "P a (pi \<bullet> Lam name lam)" 
-      apply (simp add: pi_lam)
+      apply (simp)
       apply(subst eq[symmetric])
       using p
-      apply(simp only: pi_lam pt_name2 swap_simps)
+      apply(simp only: perm_lam pt_name2 swap_simps)
       done
   qed
   then have "P a (([]::name prm) \<bullet> lam)" by blast
@@ -477,7 +420,19 @@
 apply (lifting hom)
 done
 
-thm bex_reg_eqv_range[OF identity_equivp, of "alpha"]
+(* test test
+lemma raw_hom_correct: 
+  assumes f1: "f_var \<in> Respects (op= ===> op=)"
+  and     f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)"
+  and     f3: "f_lam \<in> Respects ((op= ===> alpha) ===> (op= ===> op=) ===> op=)"
+  shows "\<exists>!hom\<in>Respects (alpha ===> op =). 
+    ((\<forall>x. hom (rVar x) = f_var x) \<and>
+     (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+     (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
+unfolding Bex1_def
+apply(rule ex1I)
+sorry
+*)
 
 
 end