src/HOL/Induct/Tree.thy
 changeset 35419 d78659d1723e parent 31602 59df8222c204 child 35439 888993948a1d
```     1.1 --- a/src/HOL/Induct/Tree.thy	Mon Mar 01 16:42:45 2010 +0100
1.2 +++ b/src/HOL/Induct/Tree.thy	Mon Mar 01 17:05:57 2010 +0100
1.3 @@ -13,20 +13,20 @@
1.4      Atom 'a
1.5    | Branch "nat => 'a tree"
1.6
1.7 -consts
1.8 +primrec
1.9    map_tree :: "('a => 'b) => 'a tree => 'b tree"
1.10 -primrec
1.11 +where
1.12    "map_tree f (Atom a) = Atom (f a)"
1.13 -  "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
1.14 +| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
1.15
1.16  lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
1.17    by (induct t) simp_all
1.18
1.19 -consts
1.20 +primrec
1.21    exists_tree :: "('a => bool) => 'a tree => bool"
1.22 -primrec
1.23 +where
1.24    "exists_tree P (Atom a) = P a"
1.25 -  "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
1.26 +| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
1.27
1.28  lemma exists_map:
1.29    "(!!x. P x ==> Q (f x)) ==>
1.30 @@ -39,23 +39,23 @@
1.31  datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
1.32
1.34 -consts
1.35 +primrec
1.36    add :: "[brouwer,brouwer] => brouwer"
1.37 -primrec
1.38 +where
1.39    "add i Zero = i"
1.41 -  "add i (Lim f) = Lim (%n. add i (f n))"
1.43 +| "add i (Lim f) = Lim (%n. add i (f n))"
1.44
1.46    by (induct k) auto
1.47
1.48  text{*Multiplication of ordinals*}
1.49 -consts
1.50 +primrec
1.51    mult :: "[brouwer,brouwer] => brouwer"
1.52 -primrec
1.53 +where
1.54    "mult i Zero = Zero"
1.55 -  "mult i (Succ j) = add (mult i j) i"
1.56 -  "mult i (Lim f) = Lim (%n. mult i (f n))"
1.57 +| "mult i (Succ j) = add (mult i j) i"
1.58 +| "mult i (Lim f) = Lim (%n. mult i (f n))"
1.59
1.62 @@ -83,7 +83,7 @@
1.63  lemma wf_brouwer_pred: "wf brouwer_pred"
1.64    by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
1.65
1.66 -lemma wf_brouwer_order: "wf brouwer_order"
1.67 +lemma wf_brouwer_order[simp]: "wf brouwer_order"
1.68    by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
1.69
1.70  lemma [simp]: "(j, Succ j) : brouwer_order"
1.71 @@ -92,14 +92,16 @@
1.72  lemma [simp]: "(f n, Lim f) : brouwer_order"
1.73    by(auto simp add: brouwer_order_def brouwer_pred_def)
1.74
1.75 -text{*Example of a recdef*}
1.76 -consts
1.77 +text{*Example of a general function*}
1.78 +
1.79 +function
1.80    add2 :: "(brouwer*brouwer) => brouwer"
1.81 -recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
1.82 +where
1.83    "add2 (i, Zero) = i"