Theory Tree

theory Tree
imports Main
(*  Title:      HOL/Induct/Tree.thy
Author:     Stefan Berghofer,  TU Muenchen
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹Infinitely branching trees›

theory Tree
imports Main
begin

datatype 'a tree =
Atom 'a
| Branch "nat ⇒ 'a tree"

primrec map_tree :: "('a ⇒ 'b) ⇒ 'a tree ⇒ 'b tree"
where
"map_tree f (Atom a) = Atom (f a)"
| "map_tree f (Branch ts) = Branch (λx. map_tree f (ts x))"

lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g ∘ f) t"
by (induct t) simp_all

primrec exists_tree :: "('a ⇒ bool) ⇒ 'a tree ⇒ bool"
where
"exists_tree P (Atom a) = P a"
| "exists_tree P (Branch ts) = (∃x. exists_tree P (ts x))"

lemma exists_map:
"(⋀x. P x ⟹ Q (f x)) ⟹
exists_tree P ts ⟹ exists_tree Q (map_tree f ts)"
by (induct ts) auto

subsection‹The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.›

datatype brouwer = Zero | Succ brouwer | Lim "nat ⇒ brouwer"

primrec add :: "brouwer ⇒ brouwer ⇒ brouwer"
where
| "add i (Lim f) = Lim (λn. add i (f n))"

by (induct k) auto

text ‹Multiplication of ordinals›
primrec mult :: "brouwer ⇒ brouwer ⇒ brouwer"
where
"mult i Zero = Zero"
| "mult i (Succ j) = add (mult i j) i"
| "mult i (Lim f) = Lim (λn. mult i (f n))"

lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"

text ‹We could probably instantiate some axiomatic type classes and use
the standard infix operators.›

subsection ‹A WF Ordering for The Brouwer ordinals (Michael Compton)›

text ‹To use the function package we need an ordering on the Brouwer
closure.›

definition brouwer_pred :: "(brouwer × brouwer) set"
where "brouwer_pred = (⋃i. {(m, n). n = Succ m ∨ (∃f. n = Lim f ∧ m = f i)})"

definition brouwer_order :: "(brouwer × brouwer) set"
where "brouwer_order = brouwer_pred^+"

lemma wf_brouwer_pred: "wf brouwer_pred"
unfolding wf_def brouwer_pred_def
apply clarify
apply (induct_tac x)
apply blast+
done

lemma wf_brouwer_order[simp]: "wf brouwer_order"
unfolding brouwer_order_def
by (rule wf_trancl[OF wf_brouwer_pred])

lemma [simp]: "(j, Succ j) ∈ brouwer_order"
by (auto simp add: brouwer_order_def brouwer_pred_def)

lemma [simp]: "(f n, Lim f) ∈ brouwer_order"
by (auto simp add: brouwer_order_def brouwer_pred_def)

text ‹Example of a general function›
function add2 :: "brouwer ⇒ brouwer ⇒ brouwer"
where