--- a/Quot/Examples/LamEx.thy	Wed Jan 20 12:20:18 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Jan 20 12:33:19 2010 +0100
@@ -467,24 +467,9 @@
 (* probably true *)
 sorry
 
-
-
-lemma hom: 
-  "\<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))))"
-apply(rule_tac x="rlam_rec f_var f_app XX" in bexI)
-apply(rule conjI)
-apply(simp)
-apply(rule conjI)
-apply(simp)
-apply(simp)
-sorry
-
 function
-  term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow> 
-                (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 
+  term1_hom :: "(name \<Rightarrow> 'a) \<Rightarrow>
+                (rlam \<Rightarrow> rlam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>
                 ((name \<Rightarrow> rlam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> rlam \<Rightarrow> 'a"
 where
   "term1_hom var app abs' (rVar x) = (var x)"
@@ -510,7 +495,12 @@
 apply(auto simp add: pi_size)
 done
 
-lemma hom_res: "
+lemma term1_hom_rsp:
+  "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>
+       \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)"
+sorry
+
+lemma hom: "
 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
 \<exists>hom\<in>Respects (alpha ===> op =). 
@@ -520,19 +510,18 @@
 apply(rule allI)
 apply(rule ballI)+
 apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI)
-apply(rule conjI)
-(* apply(simp add: term1_hom.psimps) *)
-prefer 2
-apply(rule conjI)
-(* apply(simp add: term1_hom.psimps) *)
-sorry
+apply(simp_all)
+apply(simp only: in_respects)
+apply(rule term1_hom_rsp)
+apply(assumption)+
+done
 
 lemma hom':
-"\<exists>hom. 
+"\<exists>hom.
   ((\<forall>x. hom (Var x) = f_var x) \<and>
    (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
    (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
-apply (lifting hom_res)
+apply (lifting hom)
 done
 
 (* test test