# Theory Binary_Trees

theory Binary_Trees
imports ZF
```(*  Title:      ZF/Induct/Binary_Trees.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹Binary trees›

theory Binary_Trees imports ZF 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) ==> Br(x, l, r) ≠ l"
by (induct arbitrary: x r 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 set: bt) 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:
"t ∈ bt(A) ==> k ∈ nat ==> n_nodes_aux(t)`k = n_nodes(t) #+ k"
apply (induct arbitrary: k set: bt)
apply simp
apply (atomize, simp)
done

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

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

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 set: bt) 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 set: bt) auto

text ‹
›

lemma n_leaves_reflect: "t ∈ bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)"