# Theory Tree

Up to index of Isabelle/HOL/Induct

theory Tree
imports Main
begin

    (*  Title:      HOL/Induct/Tree.thy
        ID:         $Id: Tree.thy,v 1.8 2005/06/17 14:13:07 haftmann Exp $
        Author:     Stefan Berghofer,  TU Muenchen
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    *)

    header {* Infinitely branching trees *}

    theory Tree imports Main begin

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

    consts
      map_tree :: "('a => 'b) => 'a tree => 'b tree"
    primrec
      "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 o f) t"
      by (induct t) simp_all

    consts
      exists_tree :: "('a => bool) => 'a tree => bool"
    primrec
      "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"

    text{*Addition of ordinals*}
    consts
      add :: "[brouwer,brouwer] => brouwer"
    primrec
      "add i Zero = i"
      "add i (Succ j) = Succ (add i j)"
      "add i (Lim f) = Lim (%n. add i (f n))"

    lemma add_assoc: "add (add i j) k = add i (add j k)"
    by (induct k, auto)

    text{*Multiplication of ordinals*}
    consts
      mult :: "[brouwer,brouwer] => brouwer"
    primrec
      "mult i Zero = Zero"
      "mult i (Succ j) = add (mult i j) i"
      "mult i (Lim f) = Lim (%n. mult i (f n))"

    lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
    apply (induct k)
    apply (auto simp add: add_assoc)
    done

    lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
    apply (induct k)
    apply (auto simp add: add_mult_distrib)
    done

    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 define recdef style functions we need an ordering on the Brouwer
      ordinals.  Start with a predecessor relation and form its transitive
      closure. *}

    constdefs
      brouwer_pred :: "(brouwer * brouwer) set"
      "brouwer_pred == \<Union>i. {(m,n). n = Succ m ∨ (EX f. n = Lim f & m = f i)}"

      brouwer_order :: "(brouwer * brouwer) set"
      "brouwer_order == brouwer_pred^+"

    lemma wf_brouwer_pred: "wf brouwer_pred"
      by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)

    lemma wf_brouwer_order: "wf brouwer_order"
      by(unfold brouwer_order_def, 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 recdef*}
    consts
      add2 :: "(brouwer*brouwer) => brouwer"
    recdef add2 "inv_image brouwer_order (λ (x,y). y)"
      "add2 (i, Zero) = i"
      "add2 (i, (Succ j)) = Succ (add2 (i, j))"
      "add2 (i, (Lim f)) = Lim (λ n. add2 (i, (f n)))"
      (hints recdef_wf: wf_brouwer_order)

    lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    by (induct k, auto)

    end

lemma tree_map_compose:

      map_tree g (map_tree f t) = map_tree (g o f) t

lemma exists_map:

      [| !!x. P x ==> Q (f x); exists_tree P ts |] ==> exists_tree Q (map_tree f ts)

### The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.

lemma add_assoc:

      add (add i j) k = add i (add j k)

lemma add_mult_distrib:

      mult i (add j k) = add (mult i j) (mult i k)

lemma mult_assoc:

      mult (mult i j) k = mult i (mult j k)

### A WF Ordering for The Brouwer ordinals (Michael Compton)

lemma wf_brouwer_pred:

      wf brouwer_pred

lemma wf_brouwer_order:

      wf brouwer_order

lemma

      (j, Succ j) ∈ brouwer_order

lemma

      (f n, Lim f) ∈ brouwer_order

lemma add2_assoc:

      add2 (add2 (i, j), k) = add2 (i, add2 (j, k))