# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263568429 -3600
# Node ID 1d80641a4302a9bfe4ece25e5e45c6a67efd2672
# Parent  1fc2b6f6ea2a64918038a6c7bf4dafbf8c486b7e
tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

diff -r 1fc2b6f6ea2a -r 1d80641a4302 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 15:56:25 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 16:13:49 2010 +0100
@@ -362,12 +362,17 @@
 
 (* lemma hom_reg: *)
 
-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)))
-  )"
+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
 
 lemma hom_reg:"
@@ -381,7 +386,6 @@
  (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))"
 by(regularize)
 
-thm impE[OF hom_reg]
 lemma hom_pre:"
 (\<exists>hom.
  (\<forall>x. hom (rVar x) = f_var x) \<and>
@@ -393,11 +397,10 @@
 done
 
 lemma 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)))
-  )"
+"\<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)
 done