src/HOL/Induct/Tree.thy
changeset 35419 d78659d1723e
parent 31602 59df8222c204
child 35439 888993948a1d
--- 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