--- a/src/HOL/ex/Fundefs.thy Mon May 28 16:30:28 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy Tue May 29 14:03:49 2007 +0200
@@ -280,13 +280,18 @@
datatype 'a tree =
Leaf 'a
| Branch "'a tree list"
-lemma [simp]:"x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
+
+lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
by (induct l, auto)
-fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
"treemap fn (Leaf n) = (Leaf (fn n))"
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
+by pat_completeness auto
+termination by (lexicographic_order simp:lem)
+
+declare lem[simp]
fun tinc :: "nat tree \<Rightarrow> nat tree"
where
@@ -294,7 +299,6 @@
| "tinc (Branch l) = Branch (map tinc l)"
-
(* Pattern matching on records *)
record point =
Xcoord :: int