# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263986418 -3600
# Node ID 82cdc3755c2c30a04401d74f9cd98256f1a3ebc5
# Parent  28e084a66c7fe72f718aa412ed63eb2e789e8a3b
proved that the function is a function

diff -r 28e084a66c7f -r 82cdc3755c2c Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Wed Jan 20 11:30:32 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Jan 20 12:20:18 2010 +0100
@@ -483,16 +483,32 @@
 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"
+  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
+apply(pat_completeness)
+apply(auto)
+done
 
-print_theorems
+lemma pi_size:
+  fixes pi::"name prm"
+  and   t::"rlam"
+  shows "size (pi \<bullet> t) = size t"
+apply(induct t)
+apply(auto)
+done
+
+termination term1_hom
+  apply -
+  apply(relation "measure (\<lambda>(f1, f2, f3, t). size t)")
+apply(auto simp add: pi_size)
+done
 
 lemma hom_res: "
 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).