Theory Rooted_Tree

section ‹Rooted Trees›

theory Rooted_Tree
imports Tree_Graph "HOL-Library.FSet"
begin

datatype tree = Node "tree list"

fun tree_size :: "tree  nat" where
  "tree_size (Node ts) = Suc (tts. tree_size t)"

fun height :: "tree  nat" where
  "height (Node []) = 0"
| "height (Node ts) = Suc (Max (height ` set ts))"

text ‹Convenient case splitting and induction for trees›

lemma tree_cons_exhaust[case_names Nil Cons]:
  "(t = Node []  P)  (r ts. t = Node (r # ts)  P)  P"
  by (cases t) (metis list.exhaust)

lemma tree_rev_exhaust[case_names Nil Snoc]:
  "(t = Node []  P)  (ts r. t = Node (ts @ [r])  P)  P"
  by (cases t) (metis rev_exhaust)

lemma tree_cons_induct[case_names Nil Cons]:
  assumes "P (Node [])"
    and "t ts. P t  P (Node ts)  P (Node (t#ts))"
  shows "P t"
proof (induction "size_tree t" arbitrary: t rule: less_induct)
  case less
  then show ?case using assms by (cases t rule: tree_cons_exhaust) auto
qed

fun lexord_tree where
  "lexord_tree t (Node [])  False"
| "lexord_tree (Node []) r  True"
| "lexord_tree (Node (t#ts)) (Node (r#rs))  lexord_tree t r  (t = r  lexord_tree (Node ts) (Node rs))"

fun mirror :: "tree  tree" where
  "mirror (Node ts) = Node (map mirror (rev ts))"

instantiation tree :: linorder
begin

definition
  tree_less_def: "(t::tree) < r  lexord_tree (mirror t) (mirror r)"

definition
  tree_le_def: "(t :: tree)  r  t < r  t = r"  

lemma lexord_tree_empty2[simp]: "lexord_tree (Node []) r  r  Node []"
  by (cases r rule: tree_cons_exhaust) auto

lemma mirror_empty[simp]: "mirror t = Node []  t = Node []"
  by (cases t) auto

lemma mirror_not_empty[simp]: "mirror t  Node []  t  Node []"
  by (cases t) auto

lemma tree_le_empty[simp]: "Node []  t"
  unfolding tree_le_def tree_less_def using mirror_not_empty by auto

lemma tree_less_empty_iff: "Node [] < t  t  Node []"
  unfolding tree_less_def by simp

lemma not_tree_less_empty[simp]: "¬ t < Node []"
  unfolding tree_less_def by simp

lemma tree_le_empty2_iff[simp]: "t  Node []  t = Node []"
  unfolding tree_le_def by simp

lemma lexord_tree_antisym: "lexord_tree t r  ¬ lexord_tree r t"
  by (induction r t rule: lexord_tree.induct) auto

lemma tree_less_antisym: "(t::tree) < r  ¬ r < t"
  unfolding tree_less_def using lexord_tree_antisym by blast

lemma lexord_tree_not_eq: "lexord_tree t r  t  r"
  by (induction r t rule: lexord_tree.induct) auto

lemma tree_less_not_eq: "(t::tree) < r  t  r"
  unfolding tree_less_def using lexord_tree_not_eq by blast

lemma lexord_tree_irrefl: "¬ lexord_tree t t"
  using lexord_tree_not_eq by blast

lemma tree_less_irrefl: "¬ (t::tree) < t"
  unfolding tree_less_def using lexord_tree_irrefl by blast

lemma lexord_tree_eq_iff: "¬ lexord_tree t r  ¬ lexord_tree r t  t = r"
  using lexord_tree_empty2 by (induction t r rule: lexord_tree.induct, fastforce+)

lemma mirror_mirror: "mirror (mirror t) = t"
  by (induction t rule: mirror.induct) (simp add: map_idI rev_map)

lemma mirror_inj: "mirror t = mirror r  t = r"
  using mirror_mirror by metis

lemma tree_less_eq_iff: "¬ (t::tree) < r  ¬ r < t  t = r"
  unfolding tree_less_def using lexord_tree_eq_iff mirror_inj by blast

lemma lexord_tree_trans: "lexord_tree t r  lexord_tree r s  lexord_tree t s"
proof (induction t s arbitrary: r rule: lexord_tree.induct)
  case (1 t)
  then show ?case by auto
next
  case (2 va vb)
  then show ?case by auto
next
  case (3 t ts s ss)
  then show ?case by (cases r rule: tree_cons_exhaust) auto
qed

instance
proof
  fix t r s :: tree
  show "t < r  t  r  ¬ r  t" unfolding tree_le_def using tree_less_antisym tree_less_irrefl by auto
  show "t  t" unfolding tree_le_def by simp
  show "t  r  r  t  t = r" unfolding tree_le_def using tree_less_antisym by blast
  show "t  r  r  t" unfolding tree_le_def using tree_less_eq_iff by blast
  show "t  r  r  s  t  s" unfolding tree_le_def tree_less_def using lexord_tree_trans by blast
qed

end

lemma tree_size_children: "tree_size (Node ts) = Suc n  t  set ts  tree_size t  n"
  by (auto simp: le_add1 sum_list_map_remove1)

lemma tree_size_ge_1: "tree_size t  1"
  by (cases t) auto

lemma tree_size_ne_0: "tree_size t  0"
  by (cases t) auto

lemma tree_size_1_iff: "tree_size t = 1  t = Node []"
  using tree_size_ne_0 by (cases t rule: tree_cons_exhaust) auto

lemma length_children: "tree_size (Node ts) = Suc n  length ts  n"
  by (induction ts arbitrary: n, auto, metis add_mono plus_1_eq_Suc tree_size_ge_1)


lemma height_Node_cons: "height (Node (t#ts))  Suc (height t)"
  by auto

lemma height_0_iff: "height t = 0  t = Node []"
  using height.elims by blast

lemma height_children: "height (Node ts) = Suc n  t  set ts  height t  n"
  by (metis List.finite_set Max_ge diff_Suc_1 finite_imageI height.elims imageI nat.simps(3) tree.inject)

lemma height_children_le_height: "t  set ts. height t  n  height (Node ts)  Suc n"
  by (cases ts) auto


lemma mirror_iff: "mirror t = Node ts  t = Node (map mirror (rev ts))"
  by (metis mirror.simps mirror_mirror)

lemma mirror_append: "mirror (Node (ts@rs)) = Node (map mirror (rev rs) @ map mirror (rev ts))"
  by (induction ts) auto


lemma lexord_tree_snoc: "lexord_tree (Node ts) (Node (ts@[t]))"
  by (induction ts) auto

lemma tree_less_cons: "Node ts < Node (t#ts)"
  unfolding tree_less_def using lexord_tree_snoc by simp

lemma tree_le_cons: "Node ts  Node (t#ts)"
  unfolding tree_le_def using tree_less_cons by simp

lemma tree_less_cons': "t  Node rs  t < Node (r#rs)"
  using tree_less_cons by (simp add: order_le_less_trans)

lemma tree_less_snoc2_iff[simp]: "Node (ts@[t]) < Node (rs@[r])  t < r  (t = r  Node ts < Node rs)"
  unfolding tree_less_def using mirror_inj by auto

lemma tree_le_snoc2_iff[simp]: "Node (ts@[t])  Node (rs@[r])  t < r  (t = r  Node ts  Node rs)"
  unfolding tree_le_def by auto

lemma lexord_tree_cons2[simp]: "lexord_tree (Node (ts@[t])) (Node (ts@[r]))  lexord_tree t r"
  by (induction ts) (auto simp: lexord_tree_irrefl)

lemma tree_less_cons2[simp]: "Node (t#ts) < Node (r#ts)  t < r"
  unfolding tree_less_def using lexord_tree_cons2 by simp

lemma tree_le_cons2[simp]: "Node (t#ts)  Node (r#ts)  t  r"
  unfolding tree_le_def using tree_less_cons2 by blast

lemma tree_less_sorted_snoc: "sorted (ts@[r])  Node ts < Node (ts@[r])"
  unfolding tree_less_def by (induction ts rule: rev_induct, auto,
      metis leD lexord_tree_eq_iff sorted2 sorted_wrt_append tree_less_def,
      metis dual_order.strict_iff_not list.set_intros(2) nle_le sorted2 sorted_append tree_less_def)

lemma lexord_tree_comm_prefix[simp]: "lexord_tree (Node (ss@ts)) (Node (ss@rs))  lexord_tree (Node ts) (Node rs)"
  using lexord_tree_antisym by (induction ss) auto

lemma less_tree_comm_suffix[simp]: "Node (ts@ss) < Node (rs@ss)  Node ts < Node rs"
  unfolding tree_less_def by simp

lemma tree_le_comm_suffix[simp]: "Node (ts@ss)  Node (rs@ss)  Node ts  Node rs"
  unfolding tree_le_def by simp

lemma tree_less_comm_suffix2: "t < r  Node (ts@t#ss) < Node (r#ss)"
  unfolding tree_less_def using lexord_tree_comm_prefix by simp

lemma lexord_tree_append[simp]: "lexord_tree (Node ts) (Node (ts@rs))  rs  []"
  using lexord_tree_irrefl by (induction ts) auto

lemma tree_less_append[simp]: "Node ts < Node (rs@ts)  rs  []"
  unfolding tree_less_def by simp

lemma tree_le_append: "Node ts  Node (ss@ts)"
  unfolding tree_le_def by simp

lemma tree_less_singleton_iff[simp]: "Node (ts@[t]) < Node [r]  t < r"
  unfolding tree_less_def by simp

lemma tree_le_singleton_iff[simp]: "Node (ts@[t])  Node [r]  t < r  (t = r  ts = [])"
  unfolding tree_le_def by auto

lemma lexord_tree_nested: "lexord_tree t (Node [t])"
proof (induction t rule: tree_cons_induct)
  case Nil
  then show ?case by auto
next
  case (Cons t ts)
  then show ?case by (cases t rule: tree_cons_exhaust) auto
qed

lemma tree_less_nested: "t < Node [t]"
  unfolding tree_less_def using lexord_tree_nested by auto

lemma tree_le_nested: "t  Node [t]"
  unfolding tree_le_def using tree_less_nested by auto

lemma lexord_tree_iff:
  "lexord_tree t r  (ts t' ss rs r'. t = Node (ss @ t' # ts)  r = Node (ss @ r' # rs)  lexord_tree t' r')  (ts rs. rs  []  t = Node ts  r = Node (ts @ rs))" (is "?l  ?r")
proof
  show "?l  ?r"
  proof-
    assume lexord: "lexord_tree t r"
    obtain ts where ts: "t = Node ts" by (cases t) auto
    obtain rs where rs: "r = Node rs" by (cases r) auto
    obtain ss ts' rs' where prefix: "ts = ss @ ts'  rs = ss @ rs'  (ts' = []  rs' = []  hd ts'  hd rs')" using longest_common_prefix by blast
    then have "ts' = []  lexord_tree (hd ts') (hd rs')" using lexord unfolding ts rs
      by (auto, metis lexord_tree.simps(1) lexord_tree.simps(3) list.exhaust_sel)
    then show ?thesis using prefix
      by (metis append.right_neutral lexord lexord_tree.simps(1) lexord_tree_comm_prefix list.exhaust_sel rs ts)
  qed
  show "?r  ?l" by auto
qed

lemma tree_less_iff: "t < r  (ts t' ss rs r'. t = Node (ts @ t' # ss)  r = Node (rs @ r' # ss)  t' < r')  (ts rs. rs  []  t = Node ts  r = Node (rs @ ts))" (is "?l  ?r")
proof
  show "?l  ?r"
    unfolding tree_less_def using lexord_tree_iff[of "mirror t" "mirror r", unfolded mirror_iff] 
    by (simp, metis append_Nil lexord_tree_eq_iff mirror_mirror)
next
  show "?r  ?l"
    by (auto simp: order_le_neq_trans tree_le_append,
        meson dual_order.strict_trans1 tree_le_append tree_less_comm_suffix2)
qed

lemma tree_empty_cons_lt_le: "r < Node (Node [] # ts)  r  Node 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
  proof (cases r rule: tree_rev_exhaust)
    case Nil
    then show ?thesis by auto
  next
    case (Snoc rs r1)
    then show ?thesis using snoc by (auto, (metis append_Cons tree_less_snoc2_iff)+)
  qed
qed


fun regular :: "tree  bool" where
  "regular (Node ts)  sorted ts  (tset ts. regular t)"

definition n_trees :: "nat  tree set" where
  "n_trees n = {t. tree_size t = n}"

definition regular_n_trees :: "nat  tree set" where
  "regular_n_trees n = {t. tree_size t = n  regular t}"


subsection ‹Rooted Graphs›

type_synonym 'a rpregraph = "('a set) × ('a edge set) × 'a" 

locale rgraph = graph_system +
  fixes r
  assumes root_wf: "r  V"

locale rtree = tree + rgraph
begin

definition subtrees :: "'a rpregraph set" where
  "subtrees =
    (let (V',E') = remove_vertex r
    in (λC. (C, graph_system.induced_edges E' C, THE r'. r'  C  vert_adj r r')) ` ulgraph.connected_components V' E')"

lemma rtree_subtree:
  assumes subtree: "(S,ES,rS)  subtrees"
  shows "rtree S ES rS"
proof-
  obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce
  interpret subg: ulsubgraph V' E' V E unfolding ulsubgraph_def using subgraph_remove_vertex subtree ulgraph_axioms remove_vertex by blast
  interpret g': fin_ulgraph V' E'
    by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms)
  have conn_component: "S  g'.connected_components" using subtree remove_vertex unfolding subtrees_def by auto
  then interpret subg': subgraph S ES V' E' using g'.connected_component_subgraph subtree remove_vertex unfolding subtrees_def by auto
  interpret subg': ulsubgraph S ES V' E' by unfold_locales
  interpret S: connected_ulgraph S ES using g'.connected_components_connected_ulgraphs conn_component subtree remove_vertex unfolding subtrees_def by auto
  interpret S: fin_connected_ulgraph S ES using subg'.verts_ss g'.finV by unfold_locales (simp add: finite_subset)
  interpret S: tree S ES using subg.is_cycle2 subg'.is_cycle2 no_cycles by (unfold_locales, blast)
  show ?thesis using theI'[OF unique_adj_vert_removed[OF root_wf remove_vertex conn_component]]
      subtree remove_vertex by unfold_locales (auto simp: subtrees_def)
qed

lemma finite_subtrees: "finite subtrees"
proof-
  obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce
  then interpret subg: subgraph V' E' V E using subgraph_remove_vertex by auto
  interpret g': fin_ulgraph V' E'
    by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms)
  show ?thesis using g'.finite_connected_components remove_vertex unfolding subtrees_def by simp
qed

lemma remove_root_subtrees:
  assumes remove_vertex: "remove_vertex r = (V',E')"
    and conn_component: "C  ulgraph.connected_components V' E'"
  shows "rtree C (graph_system.induced_edges E' C) (THE r'. r'  C  vert_adj r r')"
proof-
  interpret subg: ulsubgraph V' E' V E unfolding ulsubgraph_def using subgraph_remove_vertex remove_vertex ulgraph_axioms by blast
  interpret g': fin_ulgraph V' E'
    by (simp add: fin_graph_system_axioms fin_ulgraph_def subg.is_finite_subgraph subg.is_subgraph_ulgraph ulgraph_axioms)
  interpret subg': ulsubgraph C "graph_system.induced_edges E' C" V' E'
    by (simp add: conn_component g'.connected_component_subgraph g'.ulgraph_axioms ulsubgraph.intro)
  interpret C: fin_connected_ulgraph C "graph_system.induced_edges E' C"
    by (simp add: fin_connected_ulgraph.intro fin_ulgraph.intro g'.fin_graph_system_axioms
        g'.ulgraph_axioms subg'.is_finite_subgraph subg'.is_subgraph_ulgraph conn_component
        g'.connected_components_connected_ulgraphs)
  interpret C: tree C "graph_system.induced_edges E' C" using subg.is_cycle2 subg'.is_cycle2 no_cycles by (unfold_locales, blast)
  show ?thesis using theI'[OF unique_adj_vert_removed[OF root_wf remove_vertex conn_component]] by unfold_locales simp
qed

end

subsection ‹Rooted Graph Isomorphism›

fun app_rgraph_isomorphism :: "('a  'b)  'a rpregraph  'b rpregraph" where
  "app_rgraph_isomorphism f (V,E,r) = (f ` V, ((`) f) ` E, f r)"

locale rgraph_isomorphism =
  G: rgraph VG EG rG + graph_isomorphism VG EG VH EH f for VG EG rG VH EH rH f +
  assumes root_preserving: "f rG = rH"
begin

interpretation H: graph_system VH EH using graph_system_H .

lemma rgraph_H: "rgraph VH EH rH"
  using root_preserving bij_f G.root_wf VH_def by unfold_locales blast

interpretation H: rgraph VH EH rH using rgraph_H .

lemma rgraph_isomorphism_inv: "rgraph_isomorphism VH EH rH VG EG rG inv_iso" 
proof-
  interpret iso: graph_isomorphism VH EH VG EG inv_iso using graph_isomorphism_inv .
  show ?thesis using G.root_wf inj_f inv_iso_def root_preserving the_inv_into_f_f
    by unfold_locales fastforce
qed

end

fun rgraph_isomorph :: "'a rpregraph  'b rpregraph  bool" (infix r 50) where
  "(VG,EG,rG) r (VH,EH,rH)  (f. rgraph_isomorphism VG EG rG VH EH rH f)"

lemma (in rgraph) rgraph_isomorphism_id: "rgraph_isomorphism V E r V E r id"
  using graph_isomorphism_id rgraph_isomorphism.intro rgraph_axioms
  unfolding rgraph_isomorphism_axioms_def by fastforce

lemma (in rgraph) rgraph_isomorph_refl: "(V,E,r) r (V,E,r)"
  using rgraph_isomorphism_id by auto

lemma rgraph_isomorph_sym: "G r H  H r G"
  using rgraph_isomorphism.rgraph_isomorphism_inv by (cases G, cases H) fastforce

lemma rgraph_isomorphism_trans: "rgraph_isomorphism VG EG rG VH EH rH f  rgraph_isomorphism VH EH rH VF EF rF g  rgraph_isomorphism VG EG rG VF EF rF (g o f)"
  using graph_isomorphism_trans unfolding rgraph_isomorphism_def rgraph_isomorphism_axioms_def by fastforce

lemma rgraph_isomorph_trans: "transp (≃r)"
  using rgraph_isomorphism_trans unfolding transp_def by fastforce

lemma (in rtree) rgraph_isomorphis_app_iso: "inj_on f V  app_rgraph_isomorphism f (V,E,r) = (V',E',r')  rgraph_isomorphism V E r V' E' r' f"
  by unfold_locales (auto simp: bij_betw_def)

lemma (in rtree) rgraph_isomorph_app_iso: "inj_on f V  (V, E, r) r app_rgraph_isomorphism f (V, E, r)"
  using rgraph_isomorphis_app_iso by fastforce

subsection ‹Conversion between unlabeled, ordered, rooted trees and tree graphs›

datatype 'a ltree = LNode 'a "'a ltree list"

fun ltree_size :: "'a ltree  nat" where
  "ltree_size (LNode r ts) = Suc (tts. ltree_size t)"

fun root_ltree :: "'a ltree  'a" where
  "root_ltree (LNode r ts) = r"

fun nodes_ltree :: "'a ltree  'a set" where
  "nodes_ltree (LNode r ts) = {r}  (tset ts. nodes_ltree t)"

fun relabel_ltree :: "('a  'b)  'a ltree  'b ltree" where
  "relabel_ltree f (LNode r ts) = LNode (f r) (map (relabel_ltree f) ts)"

fun distinct_ltree_nodes :: "'a ltree  bool" where
  "distinct_ltree_nodes (LNode a ts)  (tset ts. a  nodes_ltree t)  distinct ts  disjoint_family_on nodes_ltree (set ts)  (tset ts. distinct_ltree_nodes t)"

fun postorder_label_aux :: "nat  tree  nat × nat ltree" where
  "postorder_label_aux n (Node []) = (n, LNode n [])"
| "postorder_label_aux n (Node (t#ts)) =
  (let (n', t') = postorder_label_aux n t in
    case postorder_label_aux (Suc n') (Node ts) of
      (n'', LNode r ts')  (n'', LNode r (t'#ts')))"

definition postorder_label :: "tree  nat ltree" where
  "postorder_label t = snd (postorder_label_aux 0 t)"

fun tree_ltree :: "'a ltree  tree" where
  "tree_ltree (LNode r ts) = Node (map tree_ltree ts)"

fun regular_ltree :: "'a ltree  bool" where
  "regular_ltree (LNode r ts)  sorted_wrt (λt s. tree_ltree t  tree_ltree s) ts  (tset ts. regular_ltree t)"

datatype 'a stree = SNode 'a "'a stree fset"

lemma stree_size_child_lt[termination_simp]: "t |∈| ts  size t < Suc (sfset ts. Suc (size s))"
  using sum_nonneg_leq_bound zero_le finite_fset Suc_le_eq less_SucI by metis

lemma stree_size_child_lt'[termination_simp]: "t  fset ts  size t < Suc (sfset ts. Suc (size s))"
  using stree_size_child_lt by metis

fun stree_size :: "'a stree  nat" where
  "stree_size (SNode r ts) = Suc (fsum stree_size ts)"

definition n_strees :: "nat  'a stree set" where
  "n_strees n = {t. stree_size t = n}"

fun root_stree :: "'a stree  'a" where
  "root_stree (SNode a ts) = a"

fun nodes_stree :: "'a stree  'a set" where
  "nodes_stree (SNode a ts) = {a}  (tfset ts. nodes_stree t)"

fun tree_graph_edges :: "'a stree  'a edge set" where
  "tree_graph_edges (SNode a ts) = ((λt. {a, root_stree t}) ` fset ts)  (tfset ts. tree_graph_edges t)"

fun distinct_stree_nodes :: "'a stree  bool" where
  "distinct_stree_nodes (SNode a ts)  (tfset ts. a  nodes_stree t)  disjoint_family_on nodes_stree (fset ts)  (tfset ts. distinct_stree_nodes t)"

fun ltree_stree :: "'a stree  'a ltree" where
  "ltree_stree (SNode r ts) = LNode r (SOME xs. fset_of_list xs = ltree_stree |`| ts  distinct xs  sorted_wrt (λt s. tree_ltree t  tree_ltree s) xs)"

fun stree_ltree :: "'a ltree  'a stree" where
  "stree_ltree (LNode r ts) = SNode r (fset_of_list (map stree_ltree ts))"

definition tree_graph_stree :: "'a stree  'a rpregraph" where
  "tree_graph_stree t = (nodes_stree t, tree_graph_edges t, root_stree t)"

function stree_of_graph :: "'a rpregraph  'a stree" where
  "stree_of_graph (V,E,r) =
    (if ¬ rtree V E r then undefined else
    SNode r (Abs_fset (stree_of_graph ` rtree.subtrees V E r)))"
  by pat_completeness auto

termination
proof (relation "measure (λp. card (fst p))", auto)
  fix r :: 'a and V :: "'a set" and E :: "'a edge set" and S :: "'a set" and ES :: "'a edge set" and rS :: 'a
  assume rtree: "rtree V E r"
  assume subtree: "(S, ES, rS)  rtree.subtrees V E r"
  interpret rtree V E r using rtree .
  obtain V' E' where remove_vertex: "remove_vertex r = (V', E')" by fastforce
  then interpret subg: subgraph V' E' V E using subgraph_remove_vertex by simp
  interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph fin_graph_system_axioms subg.is_subgraph_ulgraph ulgraph_axioms by blast
  have "S  g'.connected_components" using subtree remove_vertex unfolding subtrees_def by auto
  then have card_C_V':"card S  card V'" using g'.connected_component_wf g'.finV card_mono by metis
  have "card V' < card V" using remove_vertex root_wf finV card_Diff1_less unfolding remove_vertex_def by fast
  then show "card S < card V" using card_C_V' by simp
qed

definition tree_graph :: "tree  nat rpregraph" where
  "tree_graph t = tree_graph_stree (stree_ltree (postorder_label t))"

fun relabel_stree :: "('a  'b)  'a stree  'b stree" where
  "relabel_stree f (SNode r ts) = SNode (f r) ((relabel_stree f) |`| ts)"

lemma root_ltree_wf: "root_ltree t  nodes_ltree t"
  by (cases t) auto

lemma root_relabel_ltree[simp]: "root_ltree (relabel_ltree f t) = f (root_ltree t)"
  by (cases t) simp

lemma nodes_relabel_ltree[simp]: "nodes_ltree (relabel_ltree f t) = f ` nodes_ltree t"
  by (induction t) auto

lemma finite_nodes_ltree: "finite (nodes_ltree t)"
  by (induction t) auto

lemma root_stree_wf: "root_stree t  nodes_stree t"
  by (cases t) auto

lemma tree_graph_edges_wf: "e  tree_graph_edges t  e  nodes_stree t"
  using root_stree_wf by (induction t rule: tree_graph_edges.induct) auto

lemma card_tree_graph_edges_distinct: "distinct_stree_nodes t  e  tree_graph_edges t  card e = 2"
  using root_stree_wf card_2_iff by (induction t rule: tree_graph_edges.induct) (auto, fast+)

lemma nodes_stree_non_empty: "nodes_stree t  {}"
  by (cases t rule: nodes_stree.cases) auto

lemma finite_nodes_stree: "finite (nodes_stree t)"
  by (induction t rule: nodes_stree.induct) auto

lemma finite_tree_graph_edges: "finite (tree_graph_edges t)"
  by (induction t rule: tree_graph_edges.induct) auto

lemma root_relabel_stree[simp]: "root_stree (relabel_stree f t) = f (root_stree t)"
  by (cases t) auto

lemma nodes_stree_relabel_stree[simp]: "nodes_stree (relabel_stree f t) = f ` nodes_stree t"
  by (induction t) auto

lemma tree_graph_edges_relabel_stree[simp]: "tree_graph_edges (relabel_stree f t) = ((`) f) ` tree_graph_edges t"
  by (induction t) (simp add: image_image image_Un image_Union)

lemma nodes_stree_ltree[simp]: "nodes_stree (stree_ltree t) = nodes_ltree t"
  by (induction t) (auto simp: fset_of_list.rep_eq)

lemma distinct_sorted_wrt_list: "xs. fset_of_list xs = A  distinct xs  sorted_wrt (λt s. (f t :: 'b::linorder)  f s) xs"
proof-
  obtain xs where "fset_of_list xs = A  distinct xs"
    by (metis finite_distinct_list finite_fset fset_cong fset_of_list.rep_eq)
  then have "fset_of_list (sort_key f xs) = A  distinct (sort_key f xs)  sorted_wrt (λt s. f t  f s) (sort_key f xs)"
    using sorted_sort_key sorted_wrt_map by (simp add: fset_of_list.abs_eq, blast)
  then show ?thesis by blast
qed

abbreviation "ltree_stree_subtrees ts  SOME xs. fset_of_list xs = ltree_stree |`| ts  distinct xs  sorted_wrt (λt s. tree_ltree t  tree_ltree s) xs"

lemma fset_of_list_ltree_stree_subtrees[simp]: "fset_of_list (ltree_stree_subtrees ts) = ltree_stree |`| ts"
  using someI_ex[OF distinct_sorted_wrt_list] by fast

lemma set_ltree_stree_subtrees[simp]: "set (ltree_stree_subtrees ts) = ltree_stree ` fset ts"
  using fset_of_list_ltree_stree_subtrees by (metis (mono_tags, lifting) fset.set_map fset_of_list.rep_eq)

lemma distinct_ltree_stree_subtrees: "distinct (ltree_stree_subtrees ts)"
  using someI_ex[OF distinct_sorted_wrt_list] by blast

lemma sorted_wrt_ltree_stree_subtrees: "sorted_wrt (λt s. tree_ltree t  tree_ltree s) (ltree_stree_subtrees ts)"
  using someI_ex[OF distinct_sorted_wrt_list] by blast

lemma nodes_ltree_stree[simp]: "nodes_ltree (ltree_stree t) = nodes_stree t"
  by (induction t) auto

lemma stree_ltree_stree[simp]: "stree_ltree (ltree_stree t) = t"
  by (induction t)  (simp add: fset.map_ident_strong)

lemma nodes_tree_graph_stree: "tree_graph_stree t = (V, E, r)  V = nodes_stree t"
  by (induction t) (simp add: tree_graph_stree_def)

lemma relabel_stree_stree_ltree: "relabel_stree f (stree_ltree t) = stree_ltree (relabel_ltree f t)"
  by (induction t) (auto simp add: fset_of_list_elem)

lemma relabel_stree_relabel_ltree: "relabel_ltree f t1 = t2  relabel_stree f (stree_ltree t1) = stree_ltree t2"
  using relabel_stree_stree_ltree by blast


lemma app_rgraph_iso_tree_graph_stree: "app_rgraph_isomorphism f (tree_graph_stree t) = tree_graph_stree (relabel_stree f t)"
  unfolding tree_graph_stree_def using image_iff mk_disjoint_insert
  by (induction t) (auto, fastforce+)

lemma (in rtree) root_stree_of_graph[simp]: "root_stree (stree_of_graph (V,E,r)) = r"
  using rtree_axioms by (simp split: prod.split)

lemma (in rtree) nodes_stree_stree_of_graph[simp]: "nodes_stree (stree_of_graph (V,E,r)) = V"
  using rtree_axioms
proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct)
  case (1 VT ET r)
  then interpret t: rtree VT ET r by simp
  obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def)
  interpret subg: subgraph V' E' VT ET using t.subgraph_remove_vertex VE' by metis
  interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast

  have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast
  then have "nodes_stree (stree_of_graph (VT, ET, r)) = {r}  V'"
    using 1 using VE' t.rtree_subtree g'.Union_connected_components by (simp add: Abs_fset_inverse t.subtrees_def)
  then show ?case using VE' t.root_wf unfolding t.remove_vertex_def by auto
qed

lemma (in rtree) tree_graph_edges_stree_of_graph[simp]: "tree_graph_edges (stree_of_graph (V,E,r)) = E"
  using rtree_axioms
proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct)
  case (1 VT ET r)
  then interpret t: rtree VT ET r by simp
  obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def)
  interpret subg: subgraph V' E' VT ET using t.subgraph_remove_vertex VE' by metis
  interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast

  have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast
  then have fset_Abs_fset_subtrees[simp]: "fset (Abs_fset (stree_of_graph ` t.subtrees)) = stree_of_graph ` t.subtrees" by (simp add: Abs_fset_inverse)

  have root_edges: "(λx. {r, root_stree x}) ` stree_of_graph ` t.subtrees = {eET. r  e}" (is "?l = ?r")
  proof-
    have "e  ?l" if "e  ?r" for e
    proof-
      obtain r' where e: "e = {r, r'}" using e?r
        by (metis (no_types, lifting) CollectD insert_commute insert_iff singleton_iff t.obtain_edge_pair_adj)
      then have "r'  r" using t.singleton_not_edge e?r by force
      then have "r'  V'" using e e?r VE' t.remove_vertex_def t.wellformed_alt_snd by fastforce
      then obtain C where C_conn_component: "C  g'.connected_components" and "r'  C" using g'.Union_connected_components by auto
      have "t.vert_adj r r'" unfolding t.vert_adj_def using e?r e by blast
      then have "(THE r'. r'  C  t.vert_adj r r') = r'" using t.unique_adj_vert_removed[OF t.root_wf VE' C_conn_component] r'C by auto
      then show ?thesis using e r'C C_conn_component rtree.root_stree_of_graph t.rtree_subtree VE' unfolding t.subtrees_def by (auto simp: image_comp)
    qed
    then show ?thesis using t.unique_adj_vert_removed[OF t.root_wf VE'] t.rtree_subtree VE'
      unfolding t.subtrees_def t.vert_adj_def by (auto, metis (no_types, lifting) theI)
  qed
  have "(St.subtrees. tree_graph_edges (stree_of_graph S)) = E'" 
    using 1 VE' t.rtree_subtree g'.Union_induced_edges_connected_components
    unfolding t.subtrees_def by simp
  then have "tree_graph_edges (stree_of_graph (VT,ET,r)) = {eET. r  e}  E'"
    using root_edges 1(2) by simp
  then show ?case using VE' unfolding t.remove_vertex_def t.vincident_def by blast
qed

lemma (in rtree) tree_graph_stree_of_graph[simp]: "tree_graph_stree (stree_of_graph (V,E,r)) = (V,E,r)"
  using nodes_stree_stree_of_graph tree_graph_edges_stree_of_graph root_stree_of_graph unfolding tree_graph_stree_def by blast


lemma postorder_label_aux_mono: "fst (postorder_label_aux n t)  n"
  by (induction n t rule: postorder_label_aux.induct) (auto split: prod.split ltree.split, fastforce)

lemma nodes_postorder_label_aux_ge: "postorder_label_aux n t = (n', t')  v  nodes_ltree t'  v  n"
  by (induction n t arbitrary: n' t' rule: postorder_label_aux.induct,
      auto split: prod.splits ltree.splits,
      (metis fst_conv le_SucI order.trans postorder_label_aux_mono)+)

lemma nodes_postorder_label_aux_le: "postorder_label_aux n t = (n', t')  v  nodes_ltree t'  v  n'"
  by (induction n t arbitrary: n' t' rule: postorder_label_aux.induct,
      auto split: prod.splits ltree.splits,
      metis Suc_leD fst_conv order_trans postorder_label_aux_mono,
      blast)

lemma distinct_nodes_postorder_label_aux: "distinct_ltree_nodes (snd (postorder_label_aux n t))"
proof (induction n t rule: postorder_label_aux.induct)
  case (1 n)
  then show ?case by (simp add: disjoint_family_on_def)
next
  case (2 n t ts)
  obtain n' t' where t': "postorder_label_aux n t = (n', t')" by fastforce
  obtain n'' r ts' where ts': "postorder_label_aux (Suc n') (Node ts) = (n'', LNode r ts')" by (metis eq_snd_iff ltree.exhaust)
  then have "r  Suc n'" using nodes_postorder_label_aux_ge by auto
  then have r_notin_t': "r  nodes_ltree t'" using nodes_postorder_label_aux_le[OF t'] by fastforce
  have distinct_subtrees: "distinct (t'#ts')" using 2 t' ts' nodes_postorder_label_aux_le[OF t']
      nodes_postorder_label_aux_ge[OF ts'] by (auto, meson not_less_eq_eq root_ltree_wf)
  have "disjoint_family_on nodes_ltree (set (t'#ts'))" using 2 t' ts' nodes_postorder_label_aux_le[OF t']
      nodes_postorder_label_aux_ge[OF ts'] by (simp add: disjoint_family_on_def, meson disjoint_iff not_less_eq_eq)
  then show ?case using 2 t' ts' r_notin_t' distinct_subtrees by simp
qed

lemma distinct_nodes_postorder_label: "distinct_ltree_nodes (postorder_label t)"
  unfolding postorder_label_def using distinct_nodes_postorder_label_aux by simp

lemma distinct_nodes_stree_ltree: "distinct_ltree_nodes t  distinct_stree_nodes (stree_ltree t)"
  by (induction t) (auto simp: fset_of_list.rep_eq disjoint_family_on_def, fast)

fun distinct_edges :: "'a stree  bool" where
  "distinct_edges (SNode a ts)  inj_on (λt. {a, root_stree t}) (fset ts)
     (tfset ts. disjnt ((λt. {a, root_stree t}) ` fset ts) (tree_graph_edges t))
     disjoint_family_on tree_graph_edges (fset ts)
     (tfset ts. distinct_edges t)"

lemma distinct_nodes_inj_on_root_stree: "distinct_stree_nodes (SNode r ts)  inj_on root_stree (fset ts)"
  by (auto simp: disjoint_family_on_def, metis IntI emptyE inj_onI root_stree_wf)

lemma distinct_nodes_disjoint_edges:
  assumes distinct_nodes: "distinct_stree_nodes (SNode a ts)"
  shows "disjoint_family_on tree_graph_edges (fset ts)"
proof-
  have "tree_graph_edges t1  tree_graph_edges t2 = {}"
    if t1_in_ts: "t1  fset ts" and t2_in_ts: "t2  fset ts" and "t1  t2" for t1 t2
  proof-
    have "etree_graph_edges t1. e  tree_graph_edges t2"
    proof
      fix e assume e_in_edges_t1: "e  tree_graph_edges t1"
      then have "e  {}" using t1_in_ts card_tree_graph_edges_distinct distinct_nodes by fastforce
      then have "vnodes_stree t1. v  e" using tree_graph_edges_wf e_in_edges_t1 by blast
      then show "e  tree_graph_edges t2" using t1t2 distinct_nodes t1_in_ts t2_in_ts tree_graph_edges_wf
        by (auto simp: disjoint_family_on_def, blast)
    qed
    then show ?thesis by blast
  qed
  then show ?thesis unfolding disjoint_family_on_def by blast
qed

lemma card_nodes_edges: "distinct_stree_nodes t  card (nodes_stree t) = Suc (card (tree_graph_edges t))"
proof (induction t rule: tree_graph_edges.induct)
  case (1 a ts)
  let ?t = "SNode a ts"
  have "inj_on (λt. {a, root_stree t}) (fset ts)" using distinct_nodes_inj_on_root_stree[OF 1(2)]
    unfolding inj_on_def doubleton_eq_iff by blast
  then have card_root_edges: "card ((λt. {a, root_stree t}) ` fset ts) = card (fset ts)"
    using card_image by blast
  have finite_Un: "finite (tfset ts. nodes_stree t)" using finite_Union finite_nodes_stree finite_fset by auto
  then have "card (nodes_stree ?t) = Suc (card (tfset ts. nodes_stree t))" using 1(2) card_insert_disjoint finite_Un by simp
  also have " = Suc (tfset ts. card (nodes_stree t))" using 1(2) card_UN_disjoint' finite_nodes_stree finite_fset by fastforce
  also have " = Suc (tfset ts. Suc (card (tree_graph_edges t)))" using 1 by simp
  also have " = Suc (card (fset ts) + (tfset ts. card (tree_graph_edges t)))" by (metis add.commute sum_Suc)
  also have " = Suc (card ((λt. {a, root_stree t}) ` fset ts) + (tfset ts. card (tree_graph_edges t)))"
    using card_root_edges by simp
  also have " = Suc (card ((λx. {a, root_stree x}) ` fset ts) + card ( (tree_graph_edges ` fset ts)))"
    using distinct_nodes_disjoint_edges[OF 1(2)] card_UN_disjoint' finite_tree_graph_edges by fastforce
  also have " = Suc (card ((λx. {a, root_stree x}) ` fset ts  ( (tree_graph_edges ` fset ts))))" (is "Suc (card ?r + card ?Un) = Suc (card (?r  ?Un))")
  proof-
    have "t  fset ts. e  tree_graph_edges t. a  e" using 1(2) tree_graph_edges_wf by auto
    then have disjnt: "disjnt ?r ?Un" using disjoint_UN_iff by (auto simp: disjnt_def)
    show ?thesis using card_Un_disjnt[OF _ _ disjnt] finite_tree_graph_edges by fastforce
  qed
  finally show ?case by simp
qed

lemma tree_tree_graph_edges: "distinct_stree_nodes t  tree (nodes_stree t) (tree_graph_edges t)"
proof (induction t rule: tree_graph_edges.induct)
  case (1 a ts)
  let ?t = "SNode a ts"
  have "e. e  tree_graph_edges ?t  0 < card e  card e  2" using card_tree_graph_edges_distinct 1 by (metis order_refl pos2)
  then interpret g: fin_ulgraph "nodes_stree ?t" "tree_graph_edges ?t" using tree_graph_edges_wf finite_nodes_stree by (unfold_locales) blast+
  have "g.vert_connected a v" if t: "t  fset ts" and v: "v  nodes_stree t" for t v
  proof-
    interpret t: tree "nodes_stree t" "tree_graph_edges t" using 1 t by auto
    interpret subg: ulsubgraph "nodes_stree t" "tree_graph_edges t" "nodes_stree ?t" "tree_graph_edges ?t" using t by unfold_locales auto
    have conn_root_v: "g.vert_connected (root_stree t) v" using subg.vert_connected v root_stree_wf t.vertices_connected by blast
    have "{a, root_stree t}  tree_graph_edges ?t" using t by auto
    then have "g.vert_connected a (root_stree t)" using g.vert_connected_neighbors by blast
    then show ?thesis using conn_root_v g.vert_connected_trans by blast
  qed
  then have "vnodes_stree ?t. g.vert_connected a v" using g.vert_connected_id by auto
  then have "g.is_connected_set (nodes_stree ?t)" using g.vert_connected_trans g.vert_connected_rev unfolding g.is_connected_set_def by blast 
  then interpret g: fin_connected_ulgraph "nodes_stree ?t" "tree_graph_edges ?t" by unfold_locales auto
  show ?case using card_E_treeI card_nodes_edges 1(2) g.fin_connected_ulgraph_axioms by blast
qed

lemma rtree_tree_graph_edges:
  assumes distinct_nodes: "distinct_stree_nodes t"
  shows "rtree (nodes_stree t) (tree_graph_edges t) (root_stree t)"
proof-
  interpret tree "nodes_stree t" "tree_graph_edges t" using distinct_nodes tree_tree_graph_edges by blast
  show ?thesis using root_stree_wf by unfold_locales blast
qed

lemma rtree_tree_graph_stree: "distinct_stree_nodes t  tree_graph_stree t = (V,E,r)  rtree V E r"
  using rtree_tree_graph_edges unfolding tree_graph_stree_def by blast

lemma rtree_tree_graph: "tree_graph t = (V,E,r)  rtree V E r"
  unfolding tree_graph_def using distinct_nodes_postorder_label rtree_tree_graph_stree distinct_nodes_stree_ltree by fast

text "Cardinality of the resulting rooted tree is correct"

lemma ltree_size_postorder_label_aux: "ltree_size (snd (postorder_label_aux n t)) = tree_size t"
  by (induction n t rule: postorder_label_aux.induct) (auto split: prod.split ltree.split)

lemma ltree_size_postorder_label: "ltree_size (postorder_label t) = tree_size t"
  unfolding postorder_label_def using ltree_size_postorder_label_aux by blast

lemma distinct_nodes_ltree_size_card_nodes: "distinct_ltree_nodes t  ltree_size t = card (nodes_ltree t)"
proof (induction t)
  case (LNode r ts)
  have "finite ( (nodes_ltree ` set ts))" using finite_nodes_ltree by blast
  then show ?case using LNode disjoint_family_on_disjoint_image
    by (auto simp: sum_list_distinct_conv_sum_set card_UN_disjoint')
qed

lemma distinct_nodes_stree_size_card_nodes: "distinct_stree_nodes t  stree_size t = card (nodes_stree t)"
proof (induction t)
  case (SNode r ts)
  have "finite ( (nodes_stree ` fset ts))" using finite_nodes_stree by auto
  then show ?case using SNode disjoint_family_on_disjoint_image
    by (auto simp: fsum.F.rep_eq card_UN_disjoint')
qed

lemma stree_size_stree_ltree: "distinct_ltree_nodes t  stree_size (stree_ltree t) = ltree_size t"
  by (simp add: distinct_nodes_ltree_size_card_nodes distinct_nodes_stree_ltree distinct_nodes_stree_size_card_nodes)

lemma card_tree_graph_stree: "distinct_stree_nodes t  tree_graph_stree t = (V,E,r)  card V = stree_size t"
  by (simp add: distinct_nodes_stree_size_card_nodes) (metis nodes_tree_graph_stree)

lemma card_tree_graph: "tree_graph t = (V,E,r)  card V = tree_size t"
  unfolding tree_graph_def using ltree_size_postorder_label stree_size_stree_ltree card_tree_graph_stree
  by (metis distinct_nodes_postorder_label distinct_nodes_stree_ltree)


lemma [termination_simp]: "(t, s)  set (zip ts ss)  size t < Suc (size_list size ts)"
  by (metis less_not_refl not_less_eq set_zip_leftD size_list_estimation)

fun obtain_ltree_isomorphism :: "'a ltree  'b ltree  ('a  'b)" where
  "obtain_ltree_isomorphism (LNode r1 ts) (LNode r2 ss) = fold (++) (map2 obtain_ltree_isomorphism ts ss) [r1r2]"

fun postorder_relabel_aux :: "nat  'a ltree  nat × (nat  'a)" where
  "postorder_relabel_aux n (LNode r []) = (n, [n  r])"
| "postorder_relabel_aux n (LNode r (t#ts)) =
  (let (n', ft) = postorder_relabel_aux n t;
      (n'', fts) = postorder_relabel_aux (Suc n') (LNode r ts) in
      (n'', ft ++ fts))"

definition postorder_relabel :: "'a ltree  (nat  'a)" where
  "postorder_relabel t = snd (postorder_relabel_aux 0 t)"

lemma fst_postorder_label_aux_tree_ltree: "fst (postorder_label_aux n (tree_ltree t)) = fst (postorder_relabel_aux n t)"
  by (induction n t rule: postorder_relabel_aux.induct) (auto split: prod.split ltree.split)

lemma dom_postorder_relabel_aux: "dom (snd (postorder_relabel_aux n t)) = nodes_ltree (snd (postorder_label_aux n (tree_ltree t)))"
proof (induction n t rule: postorder_relabel_aux.induct)
case (1 n r)
  then show ?case by (auto split: if_splits)
next
  case (2 n r t ts)
  obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce
  then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel)
  obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce
  then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust)
  show ?case using 2 f_t f_ts t' ts' by auto
qed

lemma ran_postorder_relabel_aux: "ran (snd (postorder_relabel_aux n t)) = nodes_ltree t"
proof (induction n t rule: postorder_relabel_aux.induct)
  case (1 n r)
  then show ?case by (simp add: ran_def)
next
  case (2 n r t ts)
  obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce
  obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce
  have "dom f_t  dom f_ts = {}" using dom_postorder_relabel_aux f_t f_ts
    by (metis disjoint_iff fst_eqD fst_postorder_label_aux_tree_ltree nodes_postorder_label_aux_ge
        nodes_postorder_label_aux_le not_less_eq_eq prod.exhaust_sel snd_conv)
  then show ?case using 2 f_t f_ts by (simp add: ran_map_add)
qed

lemma relabel_ltree_eq: "vnodes_ltree t. f v = g v  relabel_ltree f t = relabel_ltree g t"
  by (induction t) auto

lemma relabel_postorder_relabel_aux: "relabel_ltree (the o snd (postorder_relabel_aux n t)) (snd (postorder_label_aux n (tree_ltree t))) = t"
proof (induction n t rule: postorder_relabel_aux.induct)
  case (1 n r)
  then show ?case by auto
next
  case (2 n r t ts)
  obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce
  then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel)
  obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce
  then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust)
  have ts'_in_f_ts: "vnodes_ltree (LNode r' ts'). v  dom f_ts" using f_ts ts' dom_postorder_relabel_aux
    by (metis snd_conv)
  have "vnodes_ltree t'. v  dom f_ts" using f_ts t' ts' f_t dom_postorder_relabel_aux
    by (metis nodes_postorder_label_aux_ge nodes_postorder_label_aux_le not_less_eq_eq snd_conv)
  then show ?case using 2 f_t f_ts t' ts' ts'_in_f_ts
    by (auto intro!: relabel_ltree_eq simp: map_add_dom_app_simps(3) map_add_dom_app_simps(1),
        smt (verit, ccfv_threshold) map_add_dom_app_simps(1) map_eq_conv relabel_ltree_eq)
qed

lemma relabel_postorder_relabel: "relabel_ltree (the o postorder_relabel t) (postorder_label (tree_ltree t)) = t"
  unfolding postorder_relabel_def postorder_label_def using relabel_postorder_relabel_aux by auto

lemma relabel_postorder_aux_inj: "distinct_ltree_nodes t  inj_on (the o snd (postorder_relabel_aux n t)) (nodes_ltree (snd (postorder_label_aux n (tree_ltree t))))"
proof (induction n t rule: postorder_relabel_aux.induct)
  case (1 n r)
  then show ?case by auto
next
  case (2 n r t ts)
  have disjoint_family_on_ts: "disjoint_family_on nodes_ltree (set ts)" using 2(3) by (simp add: disjoint_family_on_def)
  obtain n' f_t where f_t: "postorder_relabel_aux n t = (n', f_t)" by fastforce
  then obtain t' where t': "postorder_label_aux n (tree_ltree t) = (n', t')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel)
  obtain n'' f_ts where f_ts: "postorder_relabel_aux (Suc n') (LNode r ts) = (n'', f_ts)" by fastforce
  then obtain ts' r' where ts': "postorder_label_aux (Suc n') (tree_ltree (LNode r ts)) = (n'', LNode r' ts')"
    using fst_postorder_label_aux_tree_ltree by (metis fst_eqD prod.exhaust_sel ltree.exhaust)

  have t'_in_dom_f_t: "nodes_ltree t'  dom f_t" using f_t t' dom_postorder_relabel_aux
    by (metis order_refl snd_conv)
  have "vnodes_ltree t'. v  dom f_ts" using f_ts ts' t' dom_postorder_relabel_aux
    by (metis nodes_postorder_label_aux_ge nodes_postorder_label_aux_le not_less_eq_eq snd_conv)
  then have f_t': "vnodes_ltree t'. the ((f_t ++ f_ts) v) = the (f_t v)"
    by (simp add: map_add_dom_app_simps(3))
  have "inj_on (λv. the (f_t v)) (nodes_ltree t')" using 2 ts' f_ts f_t t' disjoint_family_on_ts by auto
  then have inj_on_t': "inj_on (λv. the ((f_t ++ f_ts) v)) (nodes_ltree t')"
    by (metis (mono_tags, lifting) inj_on_cong f_t')
  have ts'_in_dom_f_ts: "vnodes_ltree (LNode r' ts'). v  dom f_ts" using f_ts ts' dom_postorder_relabel_aux
    by (metis snd_conv)
  then have f_ts': "vnodes_ltree (LNode r' ts'). the ((f_t ++ f_ts) v) = the (f_ts v)"
    by (simp add: map_add_dom_app_simps(1))
  have "inj_on (λv. the (f_ts v)) (nodes_ltree (LNode r' ts'))" using 2 ts' f_ts f_t disjoint_family_on_ts by simp
  then have inj_on_ts': "inj_on (λv. the ((f_t ++ f_ts) v)) (nodes_ltree (LNode r' ts'))" using f_ts' inj_on_cong by fast

  have "(λv. the ((f_t ++ f_ts) v)) ` nodes_ltree t'  (λv. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts') = {}"
  proof-
    have "(λv. the ((f_t ++ f_ts) v)) ` nodes_ltree t' = (λv. the (f_t v)) ` nodes_ltree t'" using f_t' by simp
    also have "  ran f_t" using t'_in_dom_f_t ran_def by fastforce
    also have " = nodes_ltree t" by (metis f_t ran_postorder_relabel_aux snd_conv)
    finally have f_nodes_t': "(λv. the ((f_t ++ f_ts) v)) ` nodes_ltree t'  nodes_ltree t" .

    have "(λv. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts') = (λv. the (f_ts v)) ` nodes_ltree (LNode r' ts')"
      using f_ts' by (simp del: nodes_ltree.simps)
    also have "  ran f_ts" using ts'_in_dom_f_ts ran_def by fastforce
    also have " = nodes_ltree (LNode r ts)" by (metis f_ts ran_postorder_relabel_aux snd_conv)
    finally have f_nodes_ts': "(λv. the ((f_t ++ f_ts) v)) ` nodes_ltree (LNode r' ts')  nodes_ltree (LNode r ts)" .

    have "nodes_ltree t  nodes_ltree (LNode r ts) = {}" using 2(3) by (auto simp add: disjoint_family_on_def)
    then show ?thesis using f_nodes_t' f_nodes_ts' by blast
  qed
  then have "inj_on (λv. the ((f_t ++ f_ts) v)) (nodes_ltree t'  nodes_ltree (LNode r' ts'))" using inj_on_t' inj_on_ts' inj_on_Un by fast
  then show ?case using f_t t' f_ts ts' by simp
qed

lemma relabel_postorder_inj: "distinct_ltree_nodes t  inj_on (the o postorder_relabel t) (nodes_ltree (postorder_label (tree_ltree t)))"
  unfolding postorder_relabel_def postorder_label_def using relabel_postorder_aux_inj by blast

lemma (in rtree) distinct_nodes_stree_of_graph: "distinct_stree_nodes (stree_of_graph (V,E,r))"
  using rtree_axioms
proof (induction "(V,E,r)" arbitrary: V E r rule: stree_of_graph.induct)
  case (1 VT ET r)
  then interpret t: rtree VT ET r by simp
  obtain V' E' where VE': "t.remove_vertex r = (V', E')" by (simp add: t.remove_vertex_def)
  interpret subg: subgraph V' E' VT ET using t.subgraph_remove_vertex VE' by metis
  interpret g': fin_ulgraph V' E' using fin_ulgraph.intro subg.is_finite_subgraph t.fin_graph_system_axioms subg.is_subgraph_ulgraph t.ulgraph_axioms by blast

  have "finite (stree_of_graph ` t.subtrees)" using t.finite_subtrees by blast
  then have fset_Abs_fset_subtrees[simp]: "fset (Abs_fset (stree_of_graph ` t.subtrees)) = stree_of_graph ` t.subtrees" by (simp add: Abs_fset_inverse)

  have r_notin_subtrees: "st.subtrees. r  nodes_stree (stree_of_graph s)"
  proof
    fix s assume subtree: "s  t.subtrees"
    then obtain S ES rS where s: "s = (S,ES,rS)" using prod.exhaust by metis
    then interpret s: rtree S ES rS using t.rtree_subtree subtree by blast
    have "S  g'.connected_components" using subtree VE' unfolding s t.subtrees_def by auto
    then have "nodes_stree (stree_of_graph (S,ES,rS))  V'" using s.nodes_stree_stree_of_graph g'.connected_component_wf by auto
    then show "r  nodes_stree (stree_of_graph s)" using VE' unfolding s t.remove_vertex_def by blast
  qed

  have "nodes_stree (stree_of_graph s1)  nodes_stree (stree_of_graph s2) = {}"
    if s1_subtree: "s1  t.subtrees" and s2_subtree: "s2  t.subtrees" and ne: "stree_of_graph s1  stree_of_graph s2" for s1 s2
  proof-
    obtain V1 E1 r1 where s1: "s1 = (V1,E1,r1)" using prod.exhaust by metis
    then interpret s1: rtree V1 E1 r1 using t.rtree_subtree s1_subtree by blast
    have V1_conn_comp: "V1  g'.connected_components" using s1_subtree VE' unfolding t.subtrees_def s1 by auto
    then have s1_conn_comp: "nodes_stree (stree_of_graph s1)  g'.connected_components" unfolding s1 using s1.nodes_stree_stree_of_graph by auto
    obtain V2 E2 r2 where s2: "s2 = (V2,E2,r2)" using prod.exhaust by metis
    then interpret s2: rtree V2 E2 r2 using t.rtree_subtree s2_subtree by blast
    have V2_conn_comp: "V2  g'.connected_components" using s2_subtree VE' unfolding t.subtrees_def s2 by auto
    have "V1  V2" using s1 s2 s1_subtree s2_subtree VE' ne unfolding t.subtrees_def by auto
    then have "V1  V2 = {}" using V1_conn_comp V2_conn_comp g'.disjoint_connected_components unfolding disjoint_def by blast
    then show ?thesis using s1 s2 s1.nodes_stree_stree_of_graph s2.nodes_stree_stree_of_graph by simp
  qed
  then have "disjoint_family_on nodes_stree (stree_of_graph ` t.subtrees)"
    unfolding disjoint_family_on_def by blast
  then show ?case using 1 t.rtree_subtree r_notin_subtrees by auto
qed

lemma disintct_nodes_ltree_stree: "distinct_stree_nodes t  distinct_ltree_nodes (ltree_stree t)"
  using distinct_ltree_stree_subtrees by (induction t) (auto simp: disjoint_family_on_def, metis disjoint_iff)

lemma (in rtree) tree_graph_tree_of_graph: "tree_graph (tree_ltree (ltree_stree (stree_of_graph (V,E,r)))) r (V,E,r)"
proof-
  define t where "t = (V,E,r)"
  define s where "s = stree_of_graph t"
  define l where "l = ltree_stree s"
  define l' where "l' = postorder_label (tree_ltree l)"
  define s' where "s' = stree_ltree l'"
  define t' where "t' = tree_graph_stree s'"
  obtain V' E' r' where t': "t' = (V',E',r')" using prod.exhaust by metis
  interpret t': rtree V' E' r' using t' rtree_tree_graph unfolding tree_graph_def t'_def s'_def l'_def by simp 
  have "distinct_ltree_nodes l" using distinct_nodes_stree_of_graph disintct_nodes_ltree_stree
    unfolding l_def s_def t_def by blast
  then obtain f where inj_on_l': "inj_on f (nodes_ltree l')" and relabel_l': "relabel_ltree f l' = l"
    unfolding l'_def using relabel_postorder_relabel relabel_postorder_inj by blast
  then have "relabel_stree f s' = s" unfolding l_def s'_def
    using relabel_stree_relabel_ltree by fastforce
  then have app_rgraph_iso: "app_rgraph_isomorphism f t' = t" unfolding s_def t'_def t_def
    using t' tree_graph_stree_of_graph by (simp add: app_rgraph_iso_tree_graph_stree)
  have "inj_on f (nodes_stree s')" unfolding s'_def using inj_on_l' by simp
  then have inj_on_V': "inj_on f V'" using t' nodes_tree_graph_stree unfolding t'_def by fast
  have "(V',E',r') r (V,E,r)" using app_rgraph_iso t'.rgraph_isomorph_app_iso inj_on_V' unfolding t' t_def by auto
  then show ?thesis using t' unfolding tree_graph_def t_def s_def l_def l'_def s'_def t'_def by auto
qed

lemma (in rtree) stree_size_stree_of_graph[simp]: "stree_size (stree_of_graph (V,E,r)) = card V"
  using distinct_nodes_stree_of_graph by (simp add: distinct_nodes_stree_size_card_nodes del: stree_of_graph.simps)

lemma inj_ltree_stree: "inj ltree_stree"
proof
  fix t1 :: "'a stree"
    and t2 :: "'a stree"
  assume "ltree_stree t1 =  ltree_stree t2"
  then show "t1 = t2"
  proof (induction t1 arbitrary: t2)
    case (SNode r1 ts1)
    obtain r2 ts2 where t2: "t2 = SNode r2 ts2" using stree.exhaust by blast
    then show ?case using SNode by (simp, metis SNode.prems stree.inject stree_ltree_stree)
  qed
qed

lemma ltree_size_ltree_stree[simp]: "ltree_size (ltree_stree t) = stree_size t"
  using inj_ltree_stree by (induction t) (auto simp: sum_list_distinct_conv_sum_set[OF distinct_ltree_stree_subtrees] fsum.F.rep_eq,
      smt (verit, best) inj_on_def stree_ltree_stree sum.reindex_cong)

lemma tree_size_tree_ltree[simp]: "tree_size (tree_ltree t) = ltree_size t"
  by (induction t) (auto, metis comp_eq_dest_lhs map_cong)

lemma regular_ltree_stree: "regular_ltree (ltree_stree t)"
  using sorted_wrt_ltree_stree_subtrees by (induction t) auto

lemma regular_tree_ltree: "regular_ltree t  regular (tree_ltree t)"
  by (induction t) (auto simp: sorted_map)

lemma (in rtree) tree_of_graph_regular_n_tree: "tree_ltree (ltree_stree (stree_of_graph (V,E,r)))  regular_n_trees (card V)" (is "?t  ?A")
proof-
  have size_t: "tree_size ?t = card V" by (simp del: stree_of_graph.simps)
  have "regular ?t" using regular_ltree_stree regular_tree_ltree by blast
  then show ?thesis using size_t unfolding regular_n_trees_def by blast
qed

lemma (in rtree) ex_regular_n_tree: "tregular_n_trees (card V). tree_graph t r (V,E,r)"
  using tree_graph_tree_of_graph tree_of_graph_regular_n_tree by blast

subsection "Injectivity with respect to isomorphism"

lemma app_rgraph_isomorphism_relabel_stree: "app_rgraph_isomorphism f (tree_graph_stree t) = tree_graph_stree (relabel_stree f t)"
  unfolding tree_graph_stree_def by simp

text ‹Lemmas relating the connected components of the tree graph with the root removed to the subtrees of an stree.›
context
  fixes t