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.26  text{*Addition of ordinals*}
    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.32  | "add i (Succ j) = Succ (add i j)"
    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.44    ordinals.  Start with a predecessor relation and form its transitive 
    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"
    1.70  | "add2 i (Succ j) = Succ (add2 i j)"