# 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 \ set l \ size x < Suc (tree_list_size l)" + +lemma lem:"x \ set l \ size x < Suc (tree_list_size l)" by (induct l, auto) -fun treemap :: "('a \ 'a) \ 'a tree \ 'a tree" +function treemap :: "('a \ 'a) \ 'a tree \ '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 \ nat tree" where @@ -294,7 +299,6 @@ | "tinc (Branch l) = Branch (map tinc l)" - (* Pattern matching on records *) record point = Xcoord :: int