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