# Theory Binary_Trees

Up to index of Isabelle/ZF/Induct

theory Binary_Trees
imports Main
begin

    (*  Title:      ZF/Induct/Binary_Trees.thy
        ID:         $Id: Binary_Trees.thy,v 1.3 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge
    *)

    header {* Binary trees *}

    theory Binary_Trees imports Main begin

    subsection {* Datatype definition *}

    consts
      bt :: "i => i"

    datatype "bt(A)" =
      Lf | Br ("a ∈ A", "t1 ∈ bt(A)", "t2 ∈ bt(A)")

    declare bt.intros [simp]

    lemma Br_neq_left: "l ∈ bt(A) ==> (!!x r. Br(x, l, r) ≠ l)"
      by (induct set: bt) auto

    lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
      -- "Proving a freeness theorem."
      by (fast elim!: bt.free_elims)

    inductive_cases BrE: "Br(a, l, r) ∈ bt(A)"
      -- "An elimination rule, for type-checking."

    text {*
      \medskip Lemmas to justify using @{term bt} in other recursive type
      definitions.
    *}

    lemma bt_mono: "A ⊆ B ==> bt(A) ⊆ bt(B)"
      apply (unfold bt.defs)
      apply (rule lfp_mono)
        apply (rule bt.bnd_mono)+
      apply (rule univ_mono basic_monos | assumption)+
      done

    lemma bt_univ: "bt(univ(A)) ⊆ univ(A)"
      apply (unfold bt.defs bt.con_defs)
      apply (rule lfp_lowerbound)
       apply (rule_tac [2] A_subset_univ [THEN univ_mono])
      apply (fast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
      done

    lemma bt_subset_univ: "A ⊆ univ(B) ==> bt(A) ⊆ univ(B)"
      apply (rule subset_trans)
       apply (erule bt_mono)
      apply (rule bt_univ)
      done

    lemma bt_rec_type:
      "[| t ∈ bt(A);
        c ∈ C(Lf);
        !!x y z r s. [| x ∈ A;  y ∈ bt(A);  z ∈ bt(A);  r ∈ C(y);  s ∈ C(z) |] ==>
        h(x, y, z, r, s) ∈ C(Br(x, y, z))
      |] ==> bt_rec(c, h, t) ∈ C(t)"
      -- {* Type checking for recursor -- example only; not really needed. *}
      apply (induct_tac t)
       apply simp_all
      done

    subsection {* Number of nodes, with an example of tail-recursion *}

    consts  n_nodes :: "i => i"
    primrec
      "n_nodes(Lf) = 0"
      "n_nodes(Br(a, l, r)) = succ(n_nodes(l) #+ n_nodes(r))"

    lemma n_nodes_type [simp]: "t ∈ bt(A) ==> n_nodes(t) ∈ nat"
      by (induct_tac t) auto

    consts  n_nodes_aux :: "i => i"
    primrec
      "n_nodes_aux(Lf) = (λk ∈ nat. k)"
      "n_nodes_aux(Br(a, l, r)) =
          (λk ∈ nat. n_nodes_aux(r) `  (n_nodes_aux(l) ` succ(k)))"

    lemma n_nodes_aux_eq [rule_format]:
         "t ∈ bt(A) ==> ∀k ∈ nat. n_nodes_aux(t)`k = n_nodes(t) #+ k"
      by (induct_tac t, simp_all)

    constdefs
      n_nodes_tail :: "i => i"
       "n_nodes_tail(t) == n_nodes_aux(t) ` 0"

    lemma "t ∈ bt(A) ==> n_nodes_tail(t) = n_nodes(t)"
     by (simp add: n_nodes_tail_def n_nodes_aux_eq)

    subsection {* Number of leaves *}

    consts
      n_leaves :: "i => i"
    primrec
      "n_leaves(Lf) = 1"
      "n_leaves(Br(a, l, r)) = n_leaves(l) #+ n_leaves(r)"

    lemma n_leaves_type [simp]: "t ∈ bt(A) ==> n_leaves(t) ∈ nat"
      by (induct_tac t) auto

    subsection {* Reflecting trees *}

    consts
      bt_reflect :: "i => i"
    primrec
      "bt_reflect(Lf) = Lf"
      "bt_reflect(Br(a, l, r)) = Br(a, bt_reflect(r), bt_reflect(l))"

    lemma bt_reflect_type [simp]: "t ∈ bt(A) ==> bt_reflect(t) ∈ bt(A)"
      by (induct_tac t) auto

    text {*
      \medskip Theorems about @{term n_leaves}.
    *}

    lemma n_leaves_reflect: "t ∈ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"
      by (induct_tac t) (simp_all add: add_commute n_leaves_type)

    lemma n_leaves_nodes: "t ∈ bt(A) ==> n_leaves(t) = succ(n_nodes(t))"
      by (induct_tac t) (simp_all add: add_succ_right)

    text {*
      Theorems about @{term bt_reflect}.
    *}

    lemma bt_reflect_bt_reflect_ident: "t ∈ bt(A) ==> bt_reflect(bt_reflect(t)) = t"
      by (induct_tac t) simp_all

    end

### Datatype definition

lemma Br_neq_left:

      l ∈ bt(A) ==> Br(x, l, r) ≠ l

lemma Br_iff:

      Br(a, l, r) = Br(a', l', r') <-> a = a' ∧ l = l' ∧ r = r'

lemmas BrE:

      [| Br(a, l, r) ∈ bt(A); [| a ∈ A; l ∈ bt(A); r ∈ bt(A) |] ==> Q |] ==> Q

lemma bt_mono:

      A ⊆ B ==> bt(A) ⊆ bt(B)

lemma bt_univ:

      bt(univ(A)) ⊆ univ(A)

lemma bt_subset_univ:

      A ⊆ univ(B) ==> bt(A) ⊆ univ(B)

lemma bt_rec_type:

      [| t ∈ bt(A); c ∈ C(Lf);
         !!x y z r s.
            [| x ∈ A; y ∈ bt(A); z ∈ bt(A); r ∈ C(y); s ∈ C(z) |]
            ==> h(x, y, z, r, s) ∈ C(Br(x, y, z)) |]
      ==> bt_rec(c, h, t) ∈ C(t)

### Number of nodes, with an example of tail-recursion

lemma n_nodes_type:

      t ∈ bt(A) ==> n_nodes(t) ∈ nat

lemma n_nodes_aux_eq:

      [| t ∈ bt(A); k ∈ nat |] ==> n_nodes_aux(t) ` k = n_nodes(t) #+ k

lemma

      t ∈ bt(A) ==> n_nodes_tail(t) = n_nodes(t)

### Number of leaves

lemma n_leaves_type:

      t ∈ bt(A) ==> n_leaves(t) ∈ nat

### Reflecting trees

lemma bt_reflect_type:

      t ∈ bt(A) ==> bt_reflect(t) ∈ bt(A)

lemma n_leaves_reflect:

      t ∈ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)

lemma n_leaves_nodes:

      t ∈ bt(A) ==> n_leaves(t) = succ(n_nodes(t))

lemma bt_reflect_bt_reflect_ident:

      t ∈ bt(A) ==> bt_reflect(bt_reflect(t)) = t