src/HOL/Induct/Tree.thy
author paulson
Wed Jun 01 18:29:03 2005 +0200 (2005-06-01)
changeset 16174 a55c796b1f79
parent 16078 e1364521a250
child 16417 9bc16273c2d4
permissions -rw-r--r--
ordering for the ordinals
     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 = Main:
    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 apply (induct k) 
    61 apply (auto simp add: add_assoc) 
    62 done
    63 
    64 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    65 apply (induct k) 
    66 apply (auto simp add: add_mult_distrib) 
    67 done
    68 
    69 text{*We could probably instantiate some axiomatic type classes and use
    70 the standard infix operators.*}
    71 
    72 subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
    73 
    74 text{*To define recdef style functions we need an ordering on the Brouwer
    75   ordinals.  Start with a predecessor relation and form its transitive 
    76   closure. *} 
    77 
    78 constdefs
    79   brouwer_pred :: "(brouwer * brouwer) set"
    80   "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
    81 
    82   brouwer_order :: "(brouwer * brouwer) set"
    83   "brouwer_order == brouwer_pred^+"
    84 
    85 lemma wf_brouwer_pred: "wf brouwer_pred"
    86   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
    87 
    88 lemma wf_brouwer_order: "wf brouwer_order"
    89   by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
    90 
    91 lemma [simp]: "(j, Succ j) : brouwer_order"
    92   by(auto simp add: brouwer_order_def brouwer_pred_def)
    93 
    94 lemma [simp]: "(f n, Lim f) : brouwer_order"
    95   by(auto simp add: brouwer_order_def brouwer_pred_def)
    96 
    97 text{*Example of a recdef*}
    98 consts
    99   add2 :: "(brouwer*brouwer) => brouwer"
   100 recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
   101   "add2 (i, Zero) = i"
   102   "add2 (i, (Succ j)) = Succ (add2 (i, j))"
   103   "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
   104   (hints recdef_wf: wf_brouwer_order)
   105 
   106 lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
   107 by (induct k, auto)
   108 
   109 
   110 end