Theory Rose_Tree

theory Rose_Tree
imports Main "HOL-Library.Sublist"
begin

text ‹For theory ‹Incredible_Trees› we need rose trees; this theory contains
the generally useful part of that development.›

subsubsection ‹The rose tree data type›


datatype 'a rose_tree = RNode (root: 'a) (children:  "'a rose_tree list")

subsubsection ‹The set of paths in a rose tree›

text ‹Too bad that @{command inductive_set} does not allow for varying parameters...›

inductive it_pathsP :: "'a rose_tree ⇒ nat list ⇒ bool"  where
   it_paths_Nil: "it_pathsP t []"
 | it_paths_Cons: "i < length (children t) ⟹ children t ! i = t' ⟹ it_pathsP t' is ⟹ it_pathsP t (i#is)"

inductive_cases it_pathP_ConsE: "it_pathsP t (i#is)"

inductive_cases it_pathP_RNodeE: "it_pathsP (RNode r ants) is"

definition it_paths:: "'a rose_tree ⇒ nat list set"  where
  "it_paths t = Collect (it_pathsP t)"

lemma it_paths_eq [pred_set_conv]: "it_pathsP t = (λx. x ∈ it_paths t)"
 by(simp add: it_paths_def)

lemmas it_paths_intros [intro?] = it_pathsP.intros[to_set]
lemmas it_paths_induct [consumes 1, induct set: it_paths] = it_pathsP.induct[to_set]
lemmas it_paths_cases [consumes 1, cases set: it_paths] = it_pathsP.cases[to_set]
lemmas it_paths_ConsE = it_pathP_ConsE[to_set]
lemmas it_paths_RNodeE = it_pathP_RNodeE[to_set]
lemmas it_paths_simps = it_pathsP.simps[to_set]

lemmas it_paths_intros(1)[simp]

lemma it_paths_RNode_Nil[simp]: "it_paths (RNode r []) = {[]}"
  by (auto elim: it_paths_cases)

lemma it_paths_Union: "it_paths t ⊆ insert [] (Union (((λ (i,t). ((#) i) ` it_paths t) ` set (List.enumerate (0::nat) (children t)))))"
  apply (rule)
  apply (erule it_paths_cases)
  apply (auto intro!: bexI simp add: in_set_enumerate_eq)
  done

lemma finite_it_paths[simp]: "finite (it_paths t)"
  by (induction t) (auto intro!:  finite_subset[OF it_paths_Union]  simp add: in_set_enumerate_eq)

subsubsection ‹Indexing into a rose tree›

fun tree_at :: "'a rose_tree ⇒ nat list ⇒ 'a rose_tree" where
  "tree_at t [] = t"
| "tree_at t (i#is) = tree_at (children t ! i) is"

lemma it_paths_SnocE[elim_format]:
  assumes "is @ [i] ∈ it_paths t"
  shows "is ∈ it_paths t ∧ i < length (children (tree_at t is))"
using assms
by (induction "is" arbitrary: t)(auto intro!: it_paths_intros elim!: it_paths_ConsE)


lemma it_paths_strict_prefix:
  assumes "is ∈ it_paths t"
  assumes "strict_prefix is' is"
  shows "is' ∈ it_paths t"
proof-
  from assms(2)
  obtain is'' where "is = is' @ is''" using strict_prefixE' by blast
  from assms(1)[unfolded this]
  show ?thesis
    by(induction is' arbitrary: t) (auto elim!: it_paths_ConsE intro!: it_paths_intros)
qed

lemma it_paths_prefix:
  assumes "is ∈ it_paths t"
  assumes "prefix is' is"
  shows "is' ∈ it_paths t"
using assms it_paths_strict_prefix strict_prefixI by fastforce

lemma it_paths_butlast:
  assumes "is ∈ it_paths t"
  shows "butlast is ∈ it_paths t"
using assms prefixeq_butlast by (rule it_paths_prefix)

lemma it_path_SnocI:
  assumes "is ∈ it_paths t" 
  assumes "i < length (children (tree_at t is))"
  shows "is @ [i] ∈ it_paths t"
  using assms
  by (induction t arbitrary: "is" i)
     (auto 4 4  elim!: it_paths_RNodeE intro: it_paths_intros)


end