# Theory Trees

```section "Trees"

theory Trees
imports
"HOL-Library.Tree"
Common_Lemmas
(* "Catalan_Numbers.Catalan_Numbers" very big *)
begin

subsection"Definition"

text ‹The set of trees can be defined with the pre-existing @{term "tree"} datatype:›
definition trees :: "nat ⇒ unit tree set" where
"trees n = {t. size t = n}"

text "Cardinality: ‹Catalan number of n›"
text "Example: ‹trees 0 = {Leaf}›"

(*algorithm and cardinality proofs taken from what Tobias Nipkow send me*)

subsection"Algorithm"
fun tree_enum :: "nat ⇒ unit tree list" where
"tree_enum 0 = [Leaf]" |
"tree_enum (Suc n) = [⟨t1, (), t2⟩. i ← [0..<Suc n], t1 ← tree_enum i, t2 ← tree_enum (n-i)]"

subsection"Verification"

subsubsection"Cardinality"

lemma length_tree_enum:
"length (tree_enum(Suc n)) = (∑i≤n. length(tree_enum i) * length(tree_enum (n - i)))"
by (simp add: length_concat comp_def sum_list_triv atLeast_upt interv_sum_list_conv_sum_set_nat
flip: lessThan_Suc_atMost)
(*
lemma "length (tree_enum n) = catalan n"
apply(induction n rule: catalan.induct)
apply(auto simp: length_tree_enum catalan_Suc simp del: upt_Suc tree_enum.simps(2))
done
*)

subsubsection"Correctness"

lemma tree_enum_correct1: "t ∈ set (tree_enum n) ⟹ size t = n"
by (induct n arbitrary: t rule: tree_enum.induct) (simp, fastforce)

lemma tree_enum_correct2: "n = size t ⟹ t ∈ set (tree_enum n)"
proof (induct n arbitrary: t rule: tree_enum.induct)
case 1
then show ?case by simp
next
case (2 n)
show ?case proof(cases t)
case Leaf
then show ?thesis
next
case (Node l e r)

have i1: "(size l) < Suc n" using "2.prems" Node by auto
have i2: "(size r) < Suc n" using "2.prems" Node by auto

have t1: "l ∈ set (tree_enum (size l))"
apply(rule "2.hyps"(1) [of "(size l)"])
using i1 by auto

have t2: "r ∈ set (tree_enum (size r))"
apply(rule "2.hyps"(1) [of "(size r)"])
using i2 by auto

have "⟨l, (), r⟩ ∉ (λt1. ⟨t1, (), ⟨⟩⟩) ` set (tree_enum (size l + size r)) ⟹
∃x∈{0..<size l + size r}. ∃xa∈set (tree_enum x). ⟨l, (), r⟩ ∈ Node xa () ` set (tree_enum (size l + size r - x))"
using t1 t2 by fastforce
then have "⟨l, e, r⟩ ∈ set (tree_enum (size ⟨l, e, r⟩))"
by auto

then show ?thesis
using Node using "2.prems" by simp
qed
qed

theorem tree_enum_correct: "set(tree_enum n) = trees n"
proof(standard)
show "set (tree_enum n) ⊆ trees n"
unfolding trees_def using tree_enum_correct1 by auto
next
show "trees n ⊆ set (tree_enum n)"
unfolding trees_def using tree_enum_correct2 by auto
qed

subsubsection"Distinctness"

lemma tree_enum_Leaf: "⟨⟩ ∈ set (tree_enum n) ⟷ (n = 0)"
by(cases n) auto

lemma tree_enum_elem_injective: "n ≠ m ⟹ x ∈ set (tree_enum n) ⟹ y ∈ set (tree_enum m) ⟹ x ≠ y"
using tree_enum_correct1 by auto

lemma tree_enum_elem_injective2: "x ∈ set (tree_enum n) ⟹ y ∈ set (tree_enum m) ⟹ x = y ⟹ n = m"
using tree_enum_elem_injective by auto

lemma concat_map_Node_not_equal:
"xs ≠ [] ⟹ xs2 ≠ [] ⟹ ys ≠ [] ⟹ ys2 ≠ [] ⟹
∀ x∈ set xs. ∀ y ∈ set ys . x ≠ y ⟹
[⟨l, (), r⟩. l ← xs2, r ← xs] ≠ [⟨l, (), r⟩. l ← ys2, r ← ys]"
proof(induct xs)
case Nil
then show ?case by simp
next
case (Cons x xs)
then show ?case proof(induct ys)
case Nil
then show ?case by simp
next
case (Cons y ys)
obtain x2 x2s where o1: "xs2 = x2 # x2s"
by (meson Cons.prems(3) neq_Nil_conv)
obtain y2 y2s where o2: "ys2 = y2 # y2s"
by (meson Cons.prems(5) neq_Nil_conv)

have "[⟨l, (), r⟩. l ← x2#x2s, r ← x # xs] ≠ [⟨l, (), r⟩. l ← y2#y2s, r ← y # ys]"
using Cons.prems(6) by auto
then show ?case
using o1 o2 by simp
qed
qed

lemma tree_enum_not_empty: "tree_enum n ≠ []"
by(induct n) auto

lemma tree_enum_distinct_aux_outer:
assumes "∀i ≤ n. distinct (tree_enum i)"
and "distinct xs"
and "∀ i ∈ set xs. i < n"
and "sorted_wrt (<) xs"
shows "distinct (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) xs)"
using assms proof(induct xs arbitrary: n)
case Nil
then show ?case by simp
next
case (Cons x xs)
have b1: "x < n" using Cons by auto

have "∀ i ∈ set xs . x < i"
using Cons.prems(4) strict_sorted_simps(2) by simp
then have "∀ i ∈ set xs . (n - i) < (n - x)"
using b1 diff_less_mono2 by simp

then have "∀ i ∈ set xs. ∀ t1∈ set (tree_enum (n - x)). ∀ t2 ∈ set (tree_enum (n - i)) . t1 ≠ t2"
using tree_enum_correct1 by (metis less_irrefl_nat)
then have 1: "∀ i ∈ set xs. [⟨l, (), r⟩. l ← tree_enum x, r ← tree_enum (n-x)] ≠
[⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]"
using concat_map_Node_not_equal tree_enum_not_empty by simp

have 2: "distinct (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) xs)"
using Cons by auto

from 1 2 show ?case by auto
qed

lemma tree_enum_distinct_aux_left:
"∀ i < n. distinct (tree_enum i) ⟹ distinct ([⟨l, (), r⟩. i ← [0..< n], l ← tree_enum i])"
proof(induct "n")
case 0
then show ?case by simp
next
case (Suc n)
have 1:"distinct (tree_enum n)"
using Suc.prems by auto
have 2: "distinct ([⟨l, (), r⟩. i ← [0..< n], l ← tree_enum i])"
using Suc by simp
have 3: "distinct (map (λl. ⟨l, (), r⟩) (tree_enum n))"
using Node_left_distinct_map 1 by simp

have 4: "⟦⋀t n. t ∈ set (tree_enum n) ⟹ size t = n; m < n; y ∈ set (tree_enum n); y ∈ set (tree_enum m)⟧ ⟹ False" for m y
by blast

from 1 2 3 4 tree_enum_correct1 show ?case
by fastforce
qed

theorem tree_enum_distinct: "distinct(tree_enum n)"
proof(induct n rule: tree_enum.induct)
case 1
then show ?case by simp
next
case (2 n)
then have Ir: "i < Suc n ⟹ distinct (tree_enum i)" for i
by (metis atLeastLessThan_iff set_upt zero_le)

have c1: "distinct (concat (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) [0..<n]))"
proof(rule distinct_concat)
show "distinct (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) [0..<n])"
apply(rule tree_enum_distinct_aux_outer)
using Ir by auto
next
have "⋀x. x < n ⟹ distinct ([⟨l, (), r⟩. l ← tree_enum x, r ← tree_enum (n-x)])"
using Ir by (simp add: Node_right_distinct_concat_map)
then show "⋀ys. ys ∈ set (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) [0..<n]) ⟹ distinct ys"
by auto
next
have "⟦[⟨l, (), r⟩. l ← tree_enum x, r ← tree_enum (n-x)] ≠
[⟨l, (), r⟩. l ← tree_enum z, r ← tree_enum (n-z)];
y ∈ set (tree_enum x); y ∈ set (tree_enum z)⟧
⟹ False" for x z y
using tree_enum_elem_injective2 by auto
then show  "⋀ys zs.
⟦ys ∈ set (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) [0..<n]);
zs ∈ set (map (λi. [⟨l, (), r⟩. l ← tree_enum i, r ← tree_enum (n-i)]) [0..<n]); ys ≠ zs⟧
⟹ set ys ∩ set zs = {}"
by fastforce
qed

have "distinct (tree_enum n)"
using 2 by simp
then have c2: "distinct (map (λt1. ⟨t1, (), ⟨⟩⟩) (tree_enum n))"
using Node_left_distinct_map by fastforce

have c3: "⋀xa xb. ⟦xa < n; xb ∈ set (tree_enum xa); xb ∈ set (tree_enum n); ⟨⟩ ∈ set (tree_enum (n - xa))⟧ ⟹ False"