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.33  text{*Addition of ordinals*}
    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.40 -  "add i (Succ j) = Succ (add i j)"
    1.41 -  "add i (Lim f) = Lim (%n. add i (f n))"
    1.42 +| "add i (Succ j) = Succ (add i j)"
    1.43 +| "add i (Lim f) = Lim (%n. add i (f n))"
    1.44  
    1.45  lemma add_assoc: "add (add i j) k = add i (add j k)"
    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.60  lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    1.61    by (induct k) (auto simp add: add_assoc)
    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"
    1.84 -  "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    1.85 -  "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    1.86 -  (hints recdef_wf: wf_brouwer_order)
    1.87 +| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    1.88 +| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    1.89 +by pat_completeness auto
    1.90 +termination by (relation "inv_image brouwer_order snd") auto
    1.91  
    1.92  lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    1.93    by (induct k) auto