# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263548208 -3600
# Node ID d2660637e7642f2bd872b9d622f7a9d139b25f8f
# Parent  eb84e8ca214fa57928b6c58231949597f60b956b
Incorrect version of the homomorphism lemma

diff -r eb84e8ca214f -r d2660637e764 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Thu Jan 14 23:51:17 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 10:36:48 2010 +0100
@@ -367,4 +367,17 @@
   apply(simp add: var_supp1)
   done
 
+(* TODO: make a proper definition of substitution *)
+definition
+  subs :: "rlam \<Rightarrow> (name \<times> rlam) \<Rightarrow> rlam" ("_ \<guillemotleft>\<guillemotright> _" [70, 71] 70)
+where
+  "x \<guillemotleft>\<guillemotright> S \<equiv> x"
+
+lemma "
+  \<exists>hom\<in>Respects(alpha ===> op =). (
+    (\<forall>x. hom (rVar x) = var x) \<and>
+    (\<forall>l r. hom (rApp l r) = app (hom l) (hom r)) \<and>
+    (\<forall>x a. hom (rLam a x) = lam (\<lambda>y. hom (a \<guillemotleft>\<guillemotright> (x, rVar y)) (\<lambda>y. a \<guillemotleft>\<guillemotright> (x, rVar y))))
+  )"
+
 end