Theory Rooted_Tree_Enumeration
section ‹Enumeration of Rooted Trees›
theory Rooted_Tree_Enumeration
imports Rooted_Tree
begin
text ‹Algorithm inspired by works of Beyer and Hedetniemi~\cite{beyer}, performing the same
operations but directly on a recursive tree data structure instead of level sequences.›
definition n_rtree_graphs :: "nat ⇒ nat rpregraph set" where
"n_rtree_graphs n = {(V,E,r). rtree V E r ∧ card V = n}"
text ‹Recursive definition on the tree structure without using level sequences›
fun trim_tree :: "nat ⇒ tree ⇒ nat × tree" where
"trim_tree 0 t = (0, t)"
| "trim_tree (Suc 0) t = (0, Node [])"
| "trim_tree (Suc n) (Node []) = (n, Node [])"
| "trim_tree n (Node (t#ts)) =
(case trim_tree n (Node ts) of
(0, t') ⇒ (0, t') |
(n1, Node ts') ⇒
let (n2, t') = trim_tree n1 t
in (n2, Node (t'#ts')))"
lemma fst_trim_tree_lt[termination_simp]: "n ≠ 0 ⟹ fst (trim_tree n t) < n"
by (induction n t rule: trim_tree.induct, auto split: prod.split nat.split tree.split, fastforce)
fun fill_tree :: "nat ⇒ tree ⇒ tree list" where
"fill_tree 0 _ = []"
| "fill_tree n t =
(let (n', t') = trim_tree n t
in fill_tree n' t' @ [t'])"
fun next_tree_aux :: "nat ⇒ tree ⇒ tree option" where
"next_tree_aux n (Node []) = None"
| "next_tree_aux n (Node (Node [] # ts)) = next_tree_aux (Suc n) (Node ts)"
| "next_tree_aux n (Node (Node (Node [] # rs) # ts)) = Some (Node (fill_tree (Suc n) (Node rs) @ (Node rs) # ts))"
| "next_tree_aux n (Node (t # ts)) = Some (Node (the (next_tree_aux n t) # ts))"
fun next_tree :: "tree ⇒ tree option" where
"next_tree t = next_tree_aux 0 t"
lemma next_tree_aux_None_iff: "next_tree_aux n t = None ⟷ height t < 2"
proof (induction n t rule: next_tree_aux.induct)
case (1 n)
then show ?case by auto
next
case (2 n ts)
then show ?case by (cases ts) auto
next
case (3 n rs ts)
then show ?case by (auto simp: Max_gr_iff)
next
case (4 n vc vd vb ts)
then show ?case
by (metis One_nat_def Suc_n_not_le_n dual_order.trans height_Node_cons le_add1 less_2_cases
next_tree_aux.simps(4) option.simps(3) plus_1_eq_Suc)
qed
lemma next_tree_Some_iff: "(∃t'. next_tree t = Some t') ⟷ height t ≥ 2"
using next_tree_aux_None_iff by (metis linorder_not_less next_tree.simps not_Some_eq)
subsection ‹Enumeration is monotonically decreasing›
lemma trim_id: "trim_tree n t = (Suc n', t') ⟹ t = t'"
by (induction n t arbitrary: n' t' rule: trim_tree.induct) (auto split: prod.splits nat.splits tree.splits)
lemma trim_tree_le: "(n', t') = trim_tree n t ⟹ t' ≤ t"
using trim_id by (induction n t arbitrary: n' t' rule: trim_tree.induct)
(auto split: prod.splits tree.splits nat.splits simp: order_less_imp_le tree_less_cons', fastforce)
lemma fill_tree_le: "r ∈ set (fill_tree n t) ⟹ r ≤ t"
using trim_tree_le by (induction n t rule: fill_tree.induct) (auto, fastforce)
lemma next_tree_aux_lt: "height t ≥ 2 ⟹ the (next_tree_aux n t) < t"
proof (induction n t rule: next_tree_aux.induct)
case (1 n)
then show ?case by auto
next
case (2 n ts)
then show ?case using tree_less_cons' by (cases ts) auto
next
case (3 n rs ts)
then show ?case using tree_less_comm_suffix2 tree_less_cons by simp
next
case (4 n vc vd vb ts)
have "height (Node (Node (vc # vd) # vb)) ≥ 2" unfolding numeral_2_eq_2
by (metis dual_order.antisym height_Node_cons less_eq_nat.simps(1) not_less_eq_eq)
then show ?case using 4 tree_less_cons2 by simp
qed
lemma next_tree_lt: "height t ≥ 2 ⟹ the (next_tree t) < t"
using next_tree_aux_lt by simp
lemma next_tree_lt': "next_tree t = Some t' ⟹ t' < t"
using next_tree_lt next_tree_Some_iff by fastforce
subsection ‹Size preservation›
lemma size_trim_tree: "n ≠ 0 ⟹ trim_tree n t = (n', t') ⟹ n' + tree_size t' = n"
by (induction n t arbitrary: n' t' rule: trim_tree.induct) (auto split: prod.splits nat.splits tree.splits)
lemma size_fill_tree: "sum_list (map tree_size (fill_tree n t)) = n"
using size_trim_tree by (induction n t rule: fill_tree.induct) (auto split: prod.split)
lemma size_next_tree_aux: "height t ≥ 2 ⟹ tree_size (the (next_tree_aux n t)) = tree_size t + n"
proof (induction n t rule: next_tree_aux.induct)
case (1 n)
then show ?case by auto
next
case (2 n ts)
then show ?case by (cases ts) auto
next
case (3 n rs ts)
then show ?case using size_fill_tree by (auto simp del: fill_tree.simps)
next
case (4 n vc vd vb ts)
have height_t: "height (Node (Node (vc # vd) # vb)) ≥ 2" unfolding numeral_2_eq_2
by (metis dual_order.antisym height_Node_cons less_eq_nat.simps(1) not_less_eq_eq)
then show ?case using 4 by auto
qed
lemma size_next_tree: "height t ≥ 2 ⟹ tree_size (the (next_tree t)) = tree_size t"
using size_next_tree_aux by simp
lemma size_next_tree': "next_tree t = Some t' ⟹ tree_size t' = tree_size t"
using size_next_tree next_tree_Some_iff by fastforce
subsection ‹Setup for termination proof›
definition "lt_n_trees n ≡ {t. tree_size t ≤ n}"
lemma n_trees_eq: "n_trees n = Node ` {ts. tree_size (Node ts) = n}"
proof-
have "n_trees n = {Node ts | ts. tree_size (Node ts) = n}" unfolding n_trees_def by (metis tree_size.cases)
then show ?thesis by blast
qed
lemma lt_n_trees_eq: "lt_n_trees (Suc n) = Node ` {ts. tree_size (Node ts) ≤ Suc n}"
proof-
have "lt_n_trees (Suc n) = {Node ts | ts. tree_size (Node ts) ≤ Suc n}" unfolding lt_n_trees_def by (metis tree_size.cases)
then show ?thesis by blast
qed
lemma finite_lt_n_trees: "finite (lt_n_trees n)"
proof (induction n)
case 0
then show ?case unfolding lt_n_trees_def using not_finite_existsD not_less_eq_eq tree_size_ge_1 by auto
next
case (Suc n)
have "∀ts∈{ts. tree_size (Node ts) ≤ Suc n}. set ts ⊆ lt_n_trees n" unfolding lt_n_trees_def using tree_size_children by fastforce
have "{ts. tree_size (Node ts) ≤ Suc n} = {ts. tree_size (Node ts) ≤ Suc n ∧ set ts ⊆ lt_n_trees n ∧ length ts ≤ n}" unfolding lt_n_trees_def using tree_size_children length_children by fastforce
then have "finite {ts. tree_size (Node ts) ≤ Suc n}" using finite_lists_length_le[OF Suc.IH] by auto
then show ?case unfolding lt_n_trees_eq by blast
qed
lemma n_trees_subset_lt_n_trees: "n_trees n ⊆ lt_n_trees n"
unfolding n_trees_def lt_n_trees_def by blast
lemma finite_n_trees: "finite (n_trees n)"
using n_trees_subset_lt_n_trees finite_lt_n_trees rev_finite_subset by metis
subsection ‹Algorithms for enumeration›
fun greatest_tree :: "nat ⇒ tree" where
"greatest_tree (Suc 0) = Node []"
| "greatest_tree (Suc n) = Node [greatest_tree n]"
function n_tree_enum_aux :: "tree ⇒ tree list" where
"n_tree_enum_aux t =
(case next_tree t of None ⇒ [t] | Some t' ⇒ t # n_tree_enum_aux t')"
by pat_completeness auto
fun n_tree_enum :: "nat ⇒ tree list" where
"n_tree_enum 0 = []"
| "n_tree_enum n = n_tree_enum_aux (greatest_tree n)"
termination n_tree_enum_aux
proof (relation "measure (λt. card {r. r < t ∧ tree_size r = tree_size t})", auto)
fix t t' assume t_t': "next_tree_aux 0 t = Some t'"
then have height_t: "height t ≥ 2" using next_tree_Some_iff by auto
then have "t' < t" using t_t' next_tree_lt by fastforce
have size_t'_t: "tree_size t' = tree_size t" using size_next_tree height_t t_t' by fastforce
let ?meas_t' = "{r. r < t' ∧ tree_size r = tree_size t'}"
let ?meas_t = "{r. r < t ∧ tree_size r = tree_size t}"
have fin: "finite ?meas_t" using finite_n_trees unfolding n_trees_def by auto
have "?meas_t' ⊆ ?meas_t" using ‹t' < t› size_t'_t by auto
then show "card {r. r < t' ∧ tree_size r = tree_size t'} < card {r. r < t ∧ tree_size r = tree_size t}"
using fin ‹t' < t› psubset_card_mono size_t'_t by auto
qed
definition n_rtree_graph_enum :: "nat ⇒ nat rpregraph list" where
"n_rtree_graph_enum n = map tree_graph (n_tree_enum n)"
subsection ‹Regularity›
lemma regular_trim_tree: "regular t ⟹ regular (snd (trim_tree n t))"
by (induction n t rule: trim_tree.induct, auto split: prod.split nat.split tree.split,
metis dual_order.trans tree.inject trim_id trim_tree_le)
lemma regular_trim_tree': "regular t ⟹ (n', t') = trim_tree n t ⟹ regular t'"
using regular_trim_tree by (metis snd_eqD)
lemma sorted_fill_tree: "sorted (fill_tree n t)"
using fill_tree_le by (induction n t rule: fill_tree.induct) (auto simp: sorted_append split: prod.split)
lemma regular_fill_tree: "regular t ⟹ r ∈ set (fill_tree n t) ⟹ regular r"
using regular_trim_tree' by (induction n t rule: fill_tree.induct) auto
lemma regular_next_tree_aux: "regular t ⟹ height t ≥ 2 ⟹ regular (the (next_tree_aux n t))"
proof (induction n t rule: next_tree_aux.induct)
case (1 n)
then show ?case by auto
next
case (2 n ts)
then show ?case by (cases ts) auto
next
case (3 n rs ts)
then have regular_rs: "regular (Node rs)" by simp
have "∀t ∈ set ts. Node (rs) < t" using 3(1) tree_less_cons[of rs "Node []"] by auto
then show ?case using 3 sorted_fill_tree regular_fill_tree[OF regular_rs] fill_tree_le
by (auto simp del: fill_tree.simps simp: sorted_append, meson dual_order.trans tree_le_cons)
next
case (4 n vc vd vb ts)
have height_t: "height (Node (Node (vc # vd) # vb)) ≥ 2" unfolding numeral_2_eq_2
by (metis dual_order.antisym height_Node_cons less_eq_nat.simps(1) not_less_eq_eq)
then show ?case using 4 by (auto, meson height_t dual_order.strict_trans1 next_tree_aux_lt nless_le)
qed
lemma regular_next_tree: "regular t ⟹ height t ≥ 2 ⟹ regular (the (next_tree t))"
using regular_next_tree_aux by simp
lemma regular_next_tree': "regular t ⟹ next_tree t = Some t' ⟹ regular t'"
using regular_next_tree next_tree_Some_iff by fastforce
lemma regular_n_tree_enum_aux: "regular t ⟹ r ∈ set (n_tree_enum_aux t) ⟹ regular r"
proof (induction t rule: n_tree_enum_aux.induct)
case (1 t)
then show ?case
proof (cases "next_tree_aux 0 t")
case None
then show ?thesis using 1 by auto
next
case (Some a)
then show ?thesis using 1 regular_next_tree' by auto
qed
qed
lemma regular_n_tree_greatest_tree: "n ≠ 0 ⟹ greatest_tree n ∈ regular_n_trees n"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case unfolding regular_n_trees_def n_trees_def by (cases n) auto
qed
lemma regular_n_tree_enum: "t ∈ set (n_tree_enum n) ⟹ regular t"
using regular_n_tree_enum_aux regular_n_tree_greatest_tree unfolding regular_n_trees_def by (cases n) auto
lemma size_n_tree_enum_aux: "n ≠ 0 ⟹ r ∈ set (n_tree_enum_aux t) ⟹ tree_size r = tree_size t"
proof (induction t rule: n_tree_enum_aux.induct)
case (1 t)
then show ?case
proof (cases "next_tree_aux 0 t")
case None
then show ?thesis using 1 by auto
next
case (Some a)
then show ?thesis using 1 size_next_tree' by auto
qed
qed
lemma size_greatest_tree[simp]: "n ≠ 0 ⟹ tree_size (greatest_tree n) = n"
by (induction n rule: greatest_tree.induct) auto
lemma size_n_tree_enum: "t ∈ set (n_tree_enum n) ⟹ tree_size t = n"
using size_n_tree_enum_aux size_greatest_tree by (cases n, auto, fastforce)
subsection ‹Totality›
lemma "set (n_tree_enum n) ⊆ regular_n_trees n"
using regular_n_tree_enum size_n_tree_enum unfolding regular_n_trees_def n_trees_def by blast
lemma greatest_tree_lt_Suc: "n ≠ 0 ⟹ greatest_tree n < greatest_tree (Suc n)"
by (induction n rule: greatest_tree.induct) (auto simp: tree_less_nested)
lemma greatest_tree_ge: "tree_size t ≤ n ⟹ t ≤ greatest_tree n"
proof (induction n arbitrary: t rule: greatest_tree.induct)
case 1
then show ?case by (cases t rule: tree_cons_exhaust) (auto simp: tree_size_ne_0)
next
case (2 v)
then show ?case
proof (cases t rule: tree_rev_exhaust)
case Nil
then show ?thesis by simp
next
case (Snoc ts r)
then have r_le_greatest_Suc_v: "r ≤ greatest_tree (Suc v)" using 2 by auto
then show ?thesis
proof (cases "r = greatest_tree (Suc v)")
case True
then have "ts = []" using 2(2) Snoc by (simp add: tree_size_ne_0)
then show ?thesis using Snoc r_le_greatest_Suc_v by auto
next
case False
then show ?thesis using r_le_greatest_Suc_v Snoc by auto
qed
qed
next
case 3
then show ?case by (simp add: tree_size_ne_0)
qed
fun least_tree :: "nat ⇒ tree" where
"least_tree (Suc n) = Node (replicate n (Node []))"
lemma regular_n_tree_least_tree: "n ≠ 0 ⟹ least_tree n ∈ regular_n_trees n"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case unfolding regular_n_trees_def n_trees_def by (cases n) auto
qed
lemma height_lt_2_least_tree: "t ∈ regular_n_trees n ⟹ height t < 2 ⟹ t = least_tree n"
proof (induction n arbitrary: t)
case 0
have "regular_n_trees 0 = {}" unfolding regular_n_trees_def n_trees_def using tree_size.elims by auto
then show ?case using 0 by blast
next
case (Suc n)
then show ?case
proof (cases "n = 0")
case True
then show ?thesis using Suc tree_size.elims unfolding regular_n_trees_def n_trees_def
by (auto, metis leD length_children length_greater_0_conv)
next
case False
then have t_non_empty: "t ≠ Node []" using Suc(2) unfolding regular_n_trees_def n_trees_def by auto
then have height_t: "height t = 1" using Suc(3)
by (metis One_nat_def gr0_conv_Suc height.elims less_2_cases less_numeral_extra(3))
obtain s ts where s_ts: "t = Node (s # ts)" using t_non_empty by (meson height.elims)
then have "height s = 0" by (metis Suc_le_eq height_Node_cons less_one height_t)
then have s: "s = Node []" using height_0_iff by simp
then have regular_ts: "Node ts ∈ regular_n_trees n" using Suc(2) unfolding s_ts regular_n_trees_def n_trees_def by auto
have "height (Node ts) < 2" using height_t height_children height_children_le_height unfolding s_ts One_nat_def by fastforce
then have "Node ts = least_tree n" using Suc(1) regular_ts by blast
then show ?thesis using False gr0_conv_Suc s s_ts by auto
qed
qed
lemma least_tree_le: "n ≠ 0 ⟹ tree_size t ≥ n ⟹ least_tree n ≤ t"
proof (induction n arbitrary: t rule: less_induct)
case (less n)
then obtain n' where n: "n = Suc n'" using least_tree.cases by blast
then obtain ts where t: "t = Node ts" by (cases t) auto
then show ?case
proof (cases n')
case 0
then show ?thesis using n by simp
next
case (Suc n'')
then show ?thesis
proof (cases ts rule: rev_exhaust)
case Nil
then show ?thesis using less t n by auto
next
case (snoc rs r)
then show ?thesis
proof (cases "r = Node []")
case True
then have "tree_size (Node rs) ≥ n''" using less(3) unfolding n t Suc snoc by auto
then show ?thesis using less True unfolding n t Suc snoc
by (auto simp: simp: replicate_append_same[symmetric], force)
next
case False
then show ?thesis using less False unfolding n t Suc snoc
by (auto simp: replicate_append_same[symmetric] tree_less_empty_iff)
qed
qed
qed
qed
lemma trim_id': "n ≥ tree_size t ⟹ trim_tree n t = (n', t') ⟹ t' = t"
proof (induction n t arbitrary: n' t' rule: trim_tree.induct)
case (1 t)
then show ?case by auto
next
case (2 t)
then have "t = Node []" using le_Suc_eq tree_size_1_iff tree_size_ne_0 by simp
then show ?case using 2 by auto
next
case (3 v)
then show ?case by auto
next
case (4 va t ts)
then show ?case using size_trim_tree[OF _ 4(4)] size_trim_tree
by (auto split: prod.splits nat.splits simp: tree_size_ne_0, fastforce)
qed
lemma tree_ge_lt_suffix: "Node ts ≤ r ⟹ r < Node (t#ts) ⟹ ∃ss. r = Node (ss @ ts)"
proof (induction ts arbitrary: r rule: rev_induct)
case Nil
then show ?case by (cases r rule: tree_rev_exhaust) auto
next
case (snoc x xs)
then show ?case using tree_le_empty2_iff
by (cases r rule: tree_rev_exhaust)
(simp_all, metis Cons_eq_appendI tree.inject tree_less_antisym tree_less_snoc2_iff)
qed
lemma trim_tree_0_iff: "fst (trim_tree n t) = 0 ⟷ n ≤ tree_size t"
using size_trim_tree trim_id tree_size_ge_1
by (induction n t rule: trim_tree.induct, auto split: prod.split nat.split tree.split, fastforce+)
lemma trim_tree_greatest_le: "tree_size r ≤ n ⟹ r ≤ t ⟹ r ≤ snd (trim_tree n t)"
proof (induction n t arbitrary: r rule: trim_tree.induct)
case (1 t)
then show ?case by auto
next
case (2 t)
then show ?case using tree_size_ne_0 tree_size_1_iff by (simp add: le_Suc_eq)
next
case (3 v)
then show ?case by auto
next
case (4 va t ts)
obtain n1 t1 where nt1: "trim_tree (Suc (Suc va)) (Node ts) = (n1, t1)" by fastforce
then show ?case
proof (cases n1)
case 0
then show ?thesis
proof (cases "r ≤ Node ts")
case True
then show ?thesis using 4 0 nt1 by simp
next
case False
then obtain ss s where r: "r = Node (ss @ s # ts)" using 4(4) tree_ge_lt_suffix
by (metis append.assoc append_Cons append_Nil nle_le rev_exhaust tree_le_def)
then have "tree_size (Node ts) ≥ Suc (Suc va)" using nt1 trim_tree_0_iff unfolding 0 by fastforce
then have "tree_size r > Suc (Suc va)" using tree_size_ne_0 unfolding r
by (auto simp: add_strict_increasing trans_less_add2)
then show ?thesis using 4(3) by auto
qed
next
case (Suc nat)
then have t1: "t1 = Node ts" using trim_id nt1 by blast
then obtain n2 t2 where nt2: "trim_tree n1 t = (n2, t2)" by fastforce
then show ?thesis
proof (cases "r ≤ Node ts")
case True
then show ?thesis using 4 Suc nt1 t1
by (auto split: prod.split simp: tree_le_cons, meson dual_order.trans tree_le_cons)
next
case False
then obtain ss s where r: "r = Node (ss @ s # ts)" using 4(4) tree_ge_lt_suffix
by (metis append.assoc append_Cons append_Nil nle_le rev_exhaust tree_le_def)
have size_s: "tree_size s ≤ Suc nat" using 4(3) Suc size_trim_tree[OF _ nt1] t1 unfolding r by auto
have "s ≤ t" using 4(4) unfolding r by (meson order.trans tree_le_append tree_le_cons2)
have "s ≤ t2" using "4.IH"(2)[OF nt1[symmetric] Suc t1 size_s ‹s≤t›] nt2 unfolding Suc by auto
then show ?thesis
proof (cases "s = t2")
case True
then have "ss = []"
proof (cases "t2 = t")
case True
then show ?thesis using 4(4) nle_le tree_le_append unfolding r ‹s=t2› True by auto
next
case False
then have "n2 = 0" using nt2 trim_id by (cases n2) auto
then show ?thesis using size_trim_tree[OF _ nt1] size_trim_tree[OF _ nt2] Suc 4(3) tree_size_ne_0 unfolding r t1 ‹s=t2› by auto
qed
then show ?thesis using nt1 Suc t1 nt2 unfolding r True by auto
next
case False
then show ?thesis using ‹s≤t2› nt1 nt2 t1 Suc unfolding r
by (auto simp: order_less_imp_le tree_less_comm_suffix2)
qed
qed
qed
qed
lemma fill_tree_next_smallest: "tree_size (Node rs) ≤ Suc n ⟹ ∀r∈set rs. r ≤ t ⟹ Node rs ≤ Node (fill_tree n t)"
proof (induction n t arbitrary: rs rule: fill_tree.induct)
case (1 uu)
have "rs = []" using tree_size_1_iff 1(1) tree.inject by fastforce
then show ?case by auto
next
case (2 v t)
obtain n' t' where nt': "trim_tree (Suc v) t = (n', t')" by fastforce
then show ?case
proof (cases rs rule: rev_exhaust)
case Nil
then show ?thesis by auto
next
case (snoc rs' r')
then show ?thesis
proof (cases n')
case 0
then show ?thesis
proof (cases "r' = t'")
case True
then have "rs' = []" using 0 2(2) size_trim_tree[OF _ nt'] unfolding snoc by (auto simp: tree_size_ne_0)
then show ?thesis using nt' 0 unfolding snoc True by simp
next
case False
then show ?thesis using 2 trim_tree_greatest_le nt' 0 tree_less_comm_suffix2 unfolding snoc
by (auto, metis nless_le not_less_eq_eq snd_eqD trans_le_add2)
qed
next
case (Suc nat)
then show ?thesis using 2 nt' trim_id[OF nt'[unfolded Suc]] size_trim_tree[OF _ nt'] unfolding snoc by auto
qed
qed
qed
fun fill_twos :: "nat ⇒ tree ⇒ tree" where
"fill_twos n (Node ts) = Node (replicate n (Node []) @ ts)"
lemma size_fill_twos: "tree_size (fill_twos n t) = n + tree_size t"
by (cases t) (auto simp: sum_list_replicate)
lemma regular_fill_twos: "regular t ⟹ regular (fill_twos n t)"
by (cases t) (auto simp: sorted_append)
lemma fill_twos_lt: "n ≠ 0 ⟹ t < fill_twos n t"
using tree_less_append by (cases t) auto
lemma fill_twos_less: "r < Node (t#ts) ⟹ t ≠ Node [] ⟹ fill_twos n r < Node (t#ts)"
proof (induction n)
case 0
then show ?case by (cases r) auto
next
case (Suc n)
then show ?case by (cases r rule: tree.exhaust, simp,
meson leD linorder_less_linear list.inject tree.inject tree_empty_cons_lt_le)
qed
lemma next_tree_aux_successor: "tree_size r = tree_size t + n ⟹ regular r ⟹ r < t ⟹ height t ≥ 2 ⟹ r ≤ the (next_tree_aux n t)"
proof (induction n t arbitrary: r rule: next_tree_aux.induct)
case (1 n)
then show ?case by auto
next
case (2 n ts)
have size_r: "tree_size r ≤ tree_size (Node ts) + Suc n" using 2(2) by auto
have height_ts: "height (Node ts) ≥ 2" using 2(5) by (cases ts) auto
then show ?case using 2 size_r tree_empty_cons_lt_le by fastforce
next
case (3 n rs ts)
then show ?case
proof (cases "r < Node ts")
case True
then show ?thesis by (auto, meson dual_order.trans order.strict_implies_order tree_le_append tree_le_cons)
next
case False
then obtain ss where r: "r = Node (ss @ ts)" using 3(3) tree_ge_lt_suffix by fastforce
show ?thesis
proof (cases ss rule: rev_exhaust)
case Nil
then show ?thesis unfolding r by (simp, meson order_trans tree_le_append tree_le_cons)
next
case (snoc ss' s')
have s'_le_rs: "s' ≤ Node rs" using 3(3) tree_empty_cons_lt_le unfolding r snoc
by (metis (mono_tags, lifting) append.assoc append_Cons append_self_conv2
dual_order.order_iff_strict linorder_not_less order_less_le_trans tree_le_append tree_less_cons2)
show ?thesis
proof (cases "s' = Node rs")
case True
then show ?thesis using 3(1,2) fill_tree_next_smallest unfolding r snoc
by (auto simp del: fill_tree.simps simp: sorted_append)
next
case False
then show ?thesis using s'_le_rs unfolding r snoc by (auto, meson tree_le_def tree_less_iff)
qed
qed
qed
next
case (4 n vc vd vb ts)
define t where "t = Node (Node (vc # vd) # vb)"
have height_t: "height t ≥ 2" unfolding numeral_2_eq_2 t_def
by (metis dual_order.antisym height_Node_cons less_eq_nat.simps(1) not_less_eq_eq)
then show ?case
proof (cases "r < Node ts")
case True
then show ?thesis by (auto, meson dual_order.trans order.strict_implies_order tree_le_append tree_le_cons)
next
case False
then obtain ss where r: "r = Node (ss @ ts)" using 4(4) tree_ge_lt_suffix by fastforce
then show ?thesis
proof (cases ss rule: rev_exhaust)
case Nil
then show ?thesis using tree_le_cons unfolding r by auto
next
case (snoc ss' s')
have "s' < t" using 4(4)[folded t_def] unfolding r snoc
by (auto, metis antisym_conv3 append.left_neutral dual_order.strict_trans less_tree_comm_suffix not_tree_less_empty tree_less_cons2)
show ?thesis
proof (cases "tree_size s' = tree_size t + n")
case True
then have "ss' = []" using 4(2)[folded t_def] tree_size_ne_0 unfolding r snoc by auto
then show ?thesis using "4.IH" True 4(3) ‹s'<t› height_t tree_le_cons2 unfolding r snoc t_def by auto
next
case False
obtain us where s': "s' = Node us" using tree.exhaust by blast
define s'' where "s'' = fill_twos (tree_size t + n - tree_size s') s'"
have size_s': "tree_size s' ≤ tree_size t + n" using 4(2)[folded t_def] unfolding r snoc by simp
then have size_s'': "tree_size s'' = tree_size t + n" unfolding s''_def using size_fill_twos by auto
have regular_s'': "regular s''" using regular_fill_twos 4(3) unfolding s''_def r snoc by auto
have "s'' < t" using fill_twos_less ‹s'<t› unfolding t_def s''_def by auto
have "s' < s''" using fill_twos_lt False size_fill_twos size_s'' unfolding s''_def by auto
then show ?thesis using "4.IH"[folded t_def, OF size_s'' regular_s'' ‹s''<t› height_t]
unfolding r snoc t_def by (simp add: order_less_imp_le tree_less_comm_suffix2)
qed
qed
qed
qed
lemma next_tree_successor: "tree_size r = tree_size t ⟹ regular r ⟹ r < t ⟹ next_tree t = Some t' ⟹ r ≤ t'"
using next_tree_aux_successor next_tree_Some_iff by force
lemma set_n_tree_enum_aux: "t ∈ regular_n_trees n ⟹ set (n_tree_enum_aux t) = {r∈regular_n_trees n. r ≤ t}"
proof (induction t rule: n_tree_enum_aux.induct)
case (1 t)
then show ?case
proof (cases "next_tree t")
case None
have "n ≠ 0" using 1(2) tree_size_ne_0 unfolding regular_n_trees_def n_trees_def by auto
have "t = least_tree n" using height_lt_2_least_tree next_tree_aux_None_iff 1 None by simp
then show ?thesis using next_tree_Some_iff 1 None least_tree_le ‹n≠0›
unfolding regular_n_trees_def n_trees_def by (auto simp: antisym)
next
case (Some t')
then have "set (n_tree_enum_aux t) = insert t {r ∈ regular_n_trees n. r ≤ t'}"
using 1 regular_next_tree' size_next_tree' unfolding regular_n_trees_def n_trees_def by auto
also have "… = {r∈regular_n_trees n. r ≤ t}" using next_tree_successor 1(2) Some unfolding regular_n_trees_def n_trees_def
by (auto, meson Some less_le_not_le next_tree_lt' order.trans)
finally show ?thesis .
qed
qed
theorem set_n_tree_enum: "set (n_tree_enum n) = regular_n_trees n"
proof (cases n)
case 0
then show ?thesis unfolding regular_n_trees_def n_trees_def using tree_size_ne_0 by simp
next
case (Suc nat)
then show ?thesis using set_n_tree_enum_aux regular_n_tree_greatest_tree greatest_tree_ge
unfolding regular_n_trees_def n_trees_def by auto
qed
theorem n_rtree_graph_enum_n_rtree_graphs: "G ∈ set (n_rtree_graph_enum n) ⟹ G ∈ n_rtree_graphs n"
using set_n_tree_enum rtree_tree_graph card_tree_graph
unfolding n_rtree_graph_enum_def n_rtree_graphs_def regular_n_trees_def n_trees_def
by (auto, metis)
theorem n_rtree_graph_enum_surj:
assumes n_rtree_graph: "G ∈ n_rtree_graphs n"
shows "∃G' ∈ set (n_rtree_graph_enum n). G' ≃⇩r G"
proof-
obtain V E r where "G = (V,E,r)" using prod.exhaust by metis
then show ?thesis using n_rtree_graph set_n_tree_enum rtree.ex_regular_n_tree
unfolding n_rtree_graphs_def n_rtree_graph_enum_def by (auto simp: rtree.ex_regular_n_tree)
qed
subsection ‹Distinctness›
lemma n_tree_enum_aux_le: "r ∈ set (n_tree_enum_aux t) ⟹ r ≤ t"
proof (induction t rule: n_tree_enum_aux.induct)
case (1 t)
then show ?case
proof (cases "next_tree t")
case None
then show ?thesis using 1 by auto
next
case (Some a)
then show ?thesis using next_tree_lt' 1 by fastforce
qed
qed
lemma sorted_n_tree_enum_aux: "sorted_wrt (>) (n_tree_enum_aux t)"
proof (induction t rule: n_tree_enum_aux.induct)
case (1 t)
then show ?case
proof (cases "next_tree t")
case None
then show ?thesis by simp
next
case (Some a)
then show ?thesis using 1 Some next_tree_lt' n_tree_enum_aux_le by fastforce
qed
qed
lemma distinct_n_tree_enum_aux: "distinct (n_tree_enum_aux t)"
using sorted_n_tree_enum_aux strict_sorted_iff distinct_rev sorted_wrt_rev by blast
theorem distinct_n_tree_enum: "distinct (n_tree_enum n)"
using distinct_n_tree_enum_aux by (cases n) auto
theorem distinct_n_rtree_graph_enum: "distinct (n_rtree_graph_enum n)"
using tree_graph_inj distinct_n_tree_enum set_n_tree_enum unfolding n_rtree_graph_enum_def regular_n_trees_def
by (simp add: distinct_map inj_on_def)
theorem inj_iso_n_rtree_graph_enum:
assumes G_in_n_rtree_graph_enum: "G ∈ set (n_rtree_graph_enum n)"
and H_in_n_rtree_graph_enum: "H ∈ set (n_rtree_graph_enum n)"
and "G ≃⇩r H"
shows "G = H"
proof-
obtain t⇩G where t_G: "regular t⇩G" "tree_graph t⇩G = G" using G_in_n_rtree_graph_enum regular_n_tree_enum
unfolding n_rtree_graph_enum_def by auto
obtain t⇩H where t_H: "regular t⇩H" "tree_graph t⇩H = H" using H_in_n_rtree_graph_enum regular_n_tree_enum
unfolding n_rtree_graph_enum_def by auto
then show ?thesis using t_G tree_graph_inj_iso ‹G ≃⇩r H› by auto
qed
theorem ex1_iso_n_rtree_graph_enum: "G ∈ n_rtree_graphs n ⟹ ∃!G' ∈ set (n_rtree_graph_enum n). G' ≃⇩r G"
using inj_iso_n_rtree_graph_enum rgraph_isomorph_trans rgraph_isomorph_sym n_rtree_graph_enum_surj unfolding transp_def by blast
end