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
      by (simp add: "2.prems") 
  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"
    by (simp add: tree_enum_Leaf) 

  from c1 c2 c3 show ?case
    by fastforce
qed
end