# 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