# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263983432 -3600
# Node ID 28e084a66c7fe72f718aa412ed63eb2e789e8a3b
# Parent  3bd2847cfda73e209b143c74a4af09db21c8d9aa
term1_hom as a function

diff -r 3bd2847cfda7 -r 28e084a66c7f Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Tue Jan 19 18:17:42 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Jan 20 11:30:32 2010 +0100
@@ -467,6 +467,8 @@
 (* probably true *)
 sorry
 
+
+
 lemma hom: 
   "\<exists>hom\<in>Respects (alpha ===> op =). 
     ((\<forall>x. hom (rVar x) = f_var x) \<and>
@@ -480,6 +482,18 @@
 apply(simp)
 sorry
 
+function
+  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)"
+| "term1_hom var app abs' (rApp t u) =
+     app t u (term1_hom var app abs' t) (term1_hom var app abs' u)"
+| "term1_hom var app abs' (rLam x u) =
+     abs' (\<lambda>y. [(x, y)] \<bullet> u) (\<lambda>y. term1_hom var app abs' ([(x, y)] \<bullet> u))"
+sorry
+
+print_theorems
+
 lemma hom_res: "
 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
@@ -489,12 +503,12 @@
      (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))"
 apply(rule allI)
 apply(rule ballI)+
-apply(rule_tac x="rlam_rec f_var f_app XX" in bexI)
+apply(rule_tac x="term1_hom f_var f_app f_lam" in bexI)
 apply(rule conjI)
-apply(simp)
+(* apply(simp add: term1_hom.psimps) *)
+prefer 2
 apply(rule conjI)
-apply(simp)
-apply(simp_all only: in_respects)
+(* apply(simp add: term1_hom.psimps) *)
 sorry
 
 lemma hom':