--- a/src/HOL/Induct/Tree.thy Mon Mar 01 16:42:45 2010 +0100
+++ b/src/HOL/Induct/Tree.thy Mon Mar 01 17:05:57 2010 +0100
@@ -13,20 +13,20 @@
Atom 'a
| Branch "nat => 'a tree"
-consts
+primrec
map_tree :: "('a => 'b) => 'a tree => 'b tree"
-primrec
+where
"map_tree f (Atom a) = Atom (f a)"
- "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
by (induct t) simp_all
-consts
+primrec
exists_tree :: "('a => bool) => 'a tree => bool"
-primrec
+where
"exists_tree P (Atom a) = P a"
- "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
lemma exists_map:
"(!!x. P x ==> Q (f x)) ==>
@@ -39,23 +39,23 @@
datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
text{*Addition of ordinals*}
-consts
+primrec
add :: "[brouwer,brouwer] => brouwer"
-primrec
+where
"add i Zero = i"
- "add i (Succ j) = Succ (add i j)"
- "add i (Lim f) = Lim (%n. add i (f n))"
+| "add i (Succ j) = Succ (add i j)"
+| "add i (Lim f) = Lim (%n. add i (f n))"
lemma add_assoc: "add (add i j) k = add i (add j k)"
by (induct k) auto
text{*Multiplication of ordinals*}
-consts
+primrec
mult :: "[brouwer,brouwer] => brouwer"
-primrec
+where
"mult i Zero = Zero"
- "mult i (Succ j) = add (mult i j) i"
- "mult i (Lim f) = Lim (%n. mult i (f n))"
+| "mult i (Succ j) = add (mult i j) i"
+| "mult i (Lim f) = Lim (%n. mult i (f n))"
lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
by (induct k) (auto simp add: add_assoc)
@@ -83,7 +83,7 @@
lemma wf_brouwer_pred: "wf brouwer_pred"
by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
-lemma wf_brouwer_order: "wf brouwer_order"
+lemma wf_brouwer_order[simp]: "wf brouwer_order"
by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
lemma [simp]: "(j, Succ j) : brouwer_order"
@@ -92,14 +92,16 @@
lemma [simp]: "(f n, Lim f) : brouwer_order"
by(auto simp add: brouwer_order_def brouwer_pred_def)
-text{*Example of a recdef*}
-consts
+text{*Example of a general function*}
+
+function
add2 :: "(brouwer*brouwer) => brouwer"
-recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
+where
"add2 (i, Zero) = i"
- "add2 (i, (Succ j)) = Succ (add2 (i, j))"
- "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
- (hints recdef_wf: wf_brouwer_order)
+| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
+| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
+by pat_completeness auto
+termination by (relation "inv_image brouwer_order snd") auto
lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
by (induct k) auto