# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263549861 -3600
# Node ID cff21786d952097bcd0af65d8cb34e1f673d9dde
# Parent  31c02dac5dd4c1bf2817c7bca598655460161964
Appropriate respects and a statement of the lifted hom lemma

diff -r 31c02dac5dd4 -r cff21786d952 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 10:48:49 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 11:04:21 2010 +0100
@@ -361,11 +361,22 @@
   done
 
 
-lemma "
+lemma hom: "
+\<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
+\<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
   \<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)))
   )"
+sorry
+
+lemma hom':
+"\<forall>f_lam. \<forall>f_app. \<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)
 
 end