src/HOL/Induct/Tree.thy
author krauss
Mon Mar 01 18:49:55 2010 +0100 (2010-03-01)
changeset 35439 888993948a1d
parent 35419 d78659d1723e
child 39246 9e58f0499f57
permissions -rw-r--r--
tuned comment
     1 (*  Title:      HOL/Induct/Tree.thy
     2     Author:     Stefan Berghofer,  TU Muenchen
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header {* Infinitely branching trees *}
     7 
     8 theory Tree
     9 imports Main
    10 begin
    11 
    12 datatype 'a tree =
    13     Atom 'a
    14   | Branch "nat => 'a tree"
    15 
    16 primrec
    17   map_tree :: "('a => 'b) => 'a tree => 'b tree"
    18 where
    19   "map_tree f (Atom a) = Atom (f a)"
    20 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
    21 
    22 lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
    23   by (induct t) simp_all
    24 
    25 primrec
    26   exists_tree :: "('a => bool) => 'a tree => bool"
    27 where
    28   "exists_tree P (Atom a) = P a"
    29 | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
    30 
    31 lemma exists_map:
    32   "(!!x. P x ==> Q (f x)) ==>
    33     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
    34   by (induct ts) auto
    35 
    36 
    37 subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
    38 
    39 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
    40 
    41 text{*Addition of ordinals*}
    42 primrec
    43   add :: "[brouwer,brouwer] => brouwer"
    44 where
    45   "add i Zero = i"
    46 | "add i (Succ j) = Succ (add i j)"
    47 | "add i (Lim f) = Lim (%n. add i (f n))"
    48 
    49 lemma add_assoc: "add (add i j) k = add i (add j k)"
    50   by (induct k) auto
    51 
    52 text{*Multiplication of ordinals*}
    53 primrec
    54   mult :: "[brouwer,brouwer] => brouwer"
    55 where
    56   "mult i Zero = Zero"
    57 | "mult i (Succ j) = add (mult i j) i"
    58 | "mult i (Lim f) = Lim (%n. mult i (f n))"
    59 
    60 lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    61   by (induct k) (auto simp add: add_assoc)
    62 
    63 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    64   by (induct k) (auto simp add: add_mult_distrib)
    65 
    66 text{*We could probably instantiate some axiomatic type classes and use
    67 the standard infix operators.*}
    68 
    69 subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
    70 
    71 text{*To use the function package we need an ordering on the Brouwer
    72   ordinals.  Start with a predecessor relation and form its transitive 
    73   closure. *} 
    74 
    75 definition
    76   brouwer_pred :: "(brouwer * brouwer) set" where
    77   "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
    78 
    79 definition
    80   brouwer_order :: "(brouwer * brouwer) set" where
    81   "brouwer_order = brouwer_pred^+"
    82 
    83 lemma wf_brouwer_pred: "wf brouwer_pred"
    84   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
    85 
    86 lemma wf_brouwer_order[simp]: "wf brouwer_order"
    87   by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
    88 
    89 lemma [simp]: "(j, Succ j) : brouwer_order"
    90   by(auto simp add: brouwer_order_def brouwer_pred_def)
    91 
    92 lemma [simp]: "(f n, Lim f) : brouwer_order"
    93   by(auto simp add: brouwer_order_def brouwer_pred_def)
    94 
    95 text{*Example of a general function*}
    96 
    97 function
    98   add2 :: "(brouwer*brouwer) => brouwer"
    99 where
   100   "add2 (i, Zero) = i"
   101 | "add2 (i, (Succ j)) = Succ (add2 (i, j))"
   102 | "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
   103 by pat_completeness auto
   104 termination by (relation "inv_image brouwer_order snd") auto
   105 
   106 lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
   107   by (induct k) auto
   108 
   109 end