# HG changeset patch
# User krauss
# Date 1180440229 -7200
# Node ID e2744f32641ea9e658ade8136873eb39157c23b2
# Parent  16e1401afe9174616f6c0c6d30a3362bca9e61ee
updated examples to include an instance of (lexicographic_order simp:...)

diff -r 16e1401afe91 -r e2744f32641e src/HOL/ex/Fundefs.thy
--- 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