# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264227747 -3600
# Node ID 16082d0b8ac1c773d8627e242c9cb9c60e29819c
# Parent  b8e43414c5aad5bc6d4f675c4c7611ce3c8aad37
Trying to define hom for the lifted type directly.

diff -r b8e43414c5aa -r 16082d0b8ac1 Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 22 17:44:46 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sat Jan 23 07:22:27 2010 +0100
@@ -68,7 +68,7 @@
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
-| a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) 
+| a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b)
        \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 (* should be automatic with new version of eqvt-machinery *)
@@ -495,6 +495,20 @@
 apply(auto simp add: pi_size)
 done
 
+(*
+function
+  hom :: "(name \<Rightarrow> 'a) \<Rightarrow>
+                (lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow>
+                ((name \<Rightarrow> lam) \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a) \<Rightarrow> lam \<Rightarrow> 'a"
+where
+  "hom f_var f_app f_lam (Var x) = f_var x"
+| "hom f_var f_app f_lam (App l r) = f_app l r (hom f_var f_app f_lam l) (hom f_var f_app f_lam r)"
+| "hom f_var f_app f_lam (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom f_var f_app f_lam ([(a,b)] \<bullet> x))"
+apply(pat_completeness)
+apply(auto)
+done
+*)
+
 lemma term1_hom_rsp:
   "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk>
        \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)"