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