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