src/HOL/Induct/Tree.thy
 changeset 46914 c2ca2c3d23a6 parent 39246 9e58f0499f57 child 58249 180f1b3508ed
```     1.1 --- a/src/HOL/Induct/Tree.thy	Tue Mar 13 23:45:34 2012 +0100
1.2 +++ b/src/HOL/Induct/Tree.thy	Wed Mar 14 00:34:56 2012 +0100
1.3 @@ -13,8 +13,7 @@
1.4      Atom 'a
1.5    | Branch "nat => 'a tree"
1.6
1.7 -primrec
1.8 -  map_tree :: "('a => 'b) => 'a tree => 'b tree"
1.9 +primrec map_tree :: "('a => 'b) => 'a tree => 'b tree"
1.10  where
1.11    "map_tree f (Atom a) = Atom (f a)"
1.12  | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
1.13 @@ -22,8 +21,7 @@
1.14  lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
1.15    by (induct t) simp_all
1.16
1.17 -primrec
1.18 -  exists_tree :: "('a => bool) => 'a tree => bool"
1.19 +primrec exists_tree :: "('a => bool) => 'a tree => bool"
1.20  where
1.21    "exists_tree P (Atom a) = P a"
1.22  | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
1.23 @@ -39,8 +37,7 @@
1.24  datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
1.25
1.27 -primrec
1.28 -  add :: "[brouwer,brouwer] => brouwer"
1.29 +primrec add :: "[brouwer,brouwer] => brouwer"
1.30  where
1.31    "add i Zero = i"
1.33 @@ -50,8 +47,7 @@
1.34    by (induct k) auto
1.35
1.36  text{*Multiplication of ordinals*}
1.37 -primrec
1.38 -  mult :: "[brouwer,brouwer] => brouwer"
1.39 +primrec mult :: "[brouwer,brouwer] => brouwer"
1.40  where
1.41    "mult i Zero = Zero"
1.42  | "mult i (Succ j) = add (mult i j) i"
1.43 @@ -72,13 +68,11 @@
1.45    closure. *}
1.46
1.47 -definition
1.48 -  brouwer_pred :: "(brouwer * brouwer) set" where
1.49 -  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
1.50 +definition brouwer_pred :: "(brouwer * brouwer) set"
1.51 +  where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
1.52
1.53 -definition
1.54 -  brouwer_order :: "(brouwer * brouwer) set" where
1.55 -  "brouwer_order = brouwer_pred^+"
1.56 +definition brouwer_order :: "(brouwer * brouwer) set"
1.57 +  where "brouwer_order = brouwer_pred^+"
1.58
1.59  lemma wf_brouwer_pred: "wf brouwer_pred"
1.60    by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
1.61 @@ -94,8 +88,7 @@
1.62
1.63  text{*Example of a general function*}
1.64
1.65 -function
1.66 -  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
1.67 +function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
1.68  where
1.69    "add2 i Zero = i"