src/HOL/Induct/Tree.thy
author wenzelm
Thu Nov 24 00:00:20 2005 +0100 (2005-11-24)
changeset 18242 2215049cd29c
parent 16417 9bc16273c2d4
child 19736 d8d0f8f51d69
permissions -rw-r--r--
tuned induct proofs;
     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 constdefs
    75   brouwer_pred :: "(brouwer * brouwer) set"
    76   "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
    77 
    78   brouwer_order :: "(brouwer * brouwer) set"
    79   "brouwer_order == brouwer_pred^+"
    80 
    81 lemma wf_brouwer_pred: "wf brouwer_pred"
    82   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)
    83 
    84 lemma wf_brouwer_order: "wf brouwer_order"
    85   by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred])
    86 
    87 lemma [simp]: "(j, Succ j) : brouwer_order"
    88   by(auto simp add: brouwer_order_def brouwer_pred_def)
    89 
    90 lemma [simp]: "(f n, Lim f) : brouwer_order"
    91   by(auto simp add: brouwer_order_def brouwer_pred_def)
    92 
    93 text{*Example of a recdef*}
    94 consts
    95   add2 :: "(brouwer*brouwer) => brouwer"
    96 recdef add2 "inv_image brouwer_order (\<lambda> (x,y). y)"
    97   "add2 (i, Zero) = i"
    98   "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    99   "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
   100   (hints recdef_wf: wf_brouwer_order)
   101 
   102 lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
   103   by (induct k) auto
   104 
   105 end