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