theory RTree

imports "~~/src/HOL/Library/Transitive_Closure_Table" 

begin

section {* A theory of relational trees *}

inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"

inductive_cases path_consE [elim!]: "rtrancl_path r x (z#zs) y"

subsection {* Definitions *}

text {*

  In this theory, we are going to give a notion of of `Relational Graph` and

  its derived notion `Relational Tree`. Given a binary relation @{text "r"},

  the `Relational Graph of @{text "r"}` is the graph, the edges of which

  are those in @{text "r"}. In this way, any binary relation can be viewed

  as a `Relational Graph`. Note, this notion of graph includes infinite graphs. 

  A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both

  {\em single valued} and {\em acyclic}. 

*}

locale forest = 

  fixes r

  assumes sgv: "single_valued r"

  assumes acl: "acyclic r"

text {* 

  The following two auxiliary functions @{text "rel_of"} and @{text "pred_of"} 

  transfer between the predicate and set representation of binary relations.

*}

definition "rel_of r = {(x, y) | x y. r x y}"

definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)"

text {*

  To reason about {\em Relational Graph}, a notion of path is needed,

  which is given by the following @{text "rpath"} (short for

  `relational path`).  The path @{text "xs"} in proposition @{text

  "rpath r x xs y"} is a path leading from @{text "x"} to @{text "y"},

  which serves as a witness of the fact @{text "(x, y) \<in> r^*"}.

  @{text "rpath"} is simply a wrapper of the @{text "rtrancl_path"}

  defined in the imported theory @{text "Transitive_Closure_Table"},

  which defines a notion of path for the predicate form of binary

  relations.  *}

definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y"

text {*

  Given a path @{text "ps"}, @{text "edges_on ps"} is the set of edges

  along the path, which is defined as follows: *}

definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}"

text {*

   The following @{text "indep"} defines a notion of independence.

   Two nodes @{text "x"} and @{text "y"} are said to be independent

   (expressed as @{text "indep x y"}), if neither one is reachable

   from the other in relational graph @{text "r"}.  *}

definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))"

text {*

 In relational tree @{text "r"}, the sub tree of node @{text "x"} is

  written @{text "subtree r x"}, which is defined to be the set of

  nodes (including itself) which can reach @{text "x"} by following

  some path in @{text "r"}: *}

definition "subtree r x = {y . (y, x) \<in> r^*}"

definition "ancestors r x = {y. (x, y) \<in> r^+}"

(* tmp *)

definition 

  "nancestors r x \<equiv> ancestors r x \<union> {x}"

lemma nancestors_def2:

  "nancestors r x \<equiv> {y. (x, y) \<in> r\<^sup>*}"

unfolding nancestors_def

apply(auto)

by (smt Collect_cong ancestors_def insert_compr mem_Collect_eq rtrancl_eq_or_trancl)

lemma nancestors2:

  "y \<in> ancestors r x \<Longrightarrow> y \<in> nancestors r x"

apply(auto simp add: nancestors_def)

done

lemma nancestors3:

  "\<lbrakk>y \<in> nancestors r x; x \<noteq> y\<rbrakk> \<Longrightarrow> y \<in> ancestors r x"

apply(auto simp add: nancestors_def)

done

(* end tmp *)

definition "root r x = (ancestors r x = {})"

lemma root_indep:

  assumes "root r x"

    and "root r y"

    and "y \<noteq> x"

  shows "indep r x y"

proof -

  { assume "(x, y) \<in> r^*"

    hence False using assms

      by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)

  } moreover {

    assume "(y, x) \<in> r^*"

    hence False using assms

      by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)

  } ultimately show ?thesis by (auto simp:indep_def)

qed

text {*

  The following @{text "edge_in r x"} is the set of edges contained in

  the sub-tree of @{text "x"}, with @{text "r"} as the underlying

  graph.  *}

definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}"

text {*

  The following lemma @{text "edges_in_meaning"} shows the intuitive

  meaning of `an edge @{text "(a, b)"} is in the sub-tree of @{text

  "x"}`, i.e., both @{text "a"} and @{text "b"} are in the sub-tree.

  *}

lemma edges_in_meaning: 

  "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"

 by (auto simp:edges_in_def subtree_def)

text {*

  The following lemma shows the meaning of @{term "edges_in"} from the other side, 

  which says: for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"}, 

  it is sufficient to show that @{text "b"} is.

*}

lemma edges_in_refutation:

  assumes "b \<notin> subtree r x"

  shows "(a, b) \<notin> edges_in r x"

  using assms by (unfold edges_in_def subtree_def, auto)

definition "children r x = {y. (y, x) \<in> r}"

locale fforest = forest +

  assumes fb: "finite (children r x)"

  assumes wf: "wf r"

begin

lemma finite_children: "finite (children r x)"

  using fb by (cases "children r x = {}", auto simp:children_def)

end

subsection {* Auxiliary lemmas *}

lemma index_minimize:

  assumes "P (i::nat)"

  obtains j where "P j" and "\<forall> k < j. \<not> P k" 

  using assms

  by (induct i rule:less_induct, auto)

subsection {* Properties of Relational Graphs and Relational Trees *}

subsubsection {* Properties of @{text "rel_of"} and @{text "pred_of"} *}

text {* The following lemmas establish bijectivity of the two functions *}

lemma pred_rel_eq: "pred_of (rel_of r) = r" by (auto simp:rel_of_def pred_of_def)

lemma rel_pred_eq: "rel_of (pred_of r) = r" by (auto simp:rel_of_def pred_of_def)

lemma rel_of_star: "rel_of (r^**) = (rel_of r)^*"

  by (unfold rel_of_def rtranclp_rtrancl_eq, auto)

lemma pred_of_star: "pred_of (r^*) = (pred_of r)^**"

proof -

  { fix x y

    have "pred_of (r^*) x y = (pred_of r)^** x y"

    by (unfold pred_of_def rtranclp_rtrancl_eq, auto)

  } thus ?thesis by auto

qed

lemma star_2_pstar: "(x, y) \<in> r^* = (pred_of (r^*)) x y"

  by (simp add: pred_of_def)

subsubsection {* Properties of @{text "rpath"} *}

text {* Induction rule for @{text "rpath"}: *}

lemma rpath_induct [consumes 1, case_names rbase rstep, induct pred: rpath]:

  assumes "rpath r x1 x2 x3"

    and "\<And>x. P x [] x"

    and "\<And>x y ys z. (x, y) \<in> r \<Longrightarrow> rpath r y ys z \<Longrightarrow> P y ys z \<Longrightarrow> P x (y # ys) z"

  shows "P x1 x2 x3"

  using assms[unfolded rpath_def]

  by (induct, auto simp:pred_of_def rpath_def)

lemma rpathE [elim]: 

  assumes "rpath r x xs y"

  obtains (base) "y = x" "xs = []"

     | (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"

  using assms

  by (induct, auto)

text {* Introduction rule for empty path *}

lemma rbaseI [intro!]: 

  assumes "x = y"

  shows "rpath r x [] y"

  by  (unfold rpath_def assms, 

         rule Transitive_Closure_Table.rtrancl_path.base)

text {* Introduction rule for non-empty path *}

lemma rstepI [intro!]: 

  assumes "(x, y) \<in> r"

    and "rpath r y ys z"

  shows "rpath r x (y#ys) z" 

proof(unfold rpath_def, rule Transitive_Closure_Table.rtrancl_path.step)

  from assms(1) show "pred_of r x y" by (auto simp:pred_of_def)

next

  from assms(2) show "rtrancl_path (pred_of r) y ys z"  

  by (auto simp:pred_of_def rpath_def)

qed

lemma rpath_stepI'[intro, simp]: 

  assumes "rpath r x xs y"

  and "(y, z) \<in> r"

  shows "rpath r x (xs@[z]) z"

  using assms

  by (induct, auto)

text {* Introduction rule for @{text "@"}-path *}

lemma rpath_appendI [intro,simp]: 

  assumes "rpath r x xs a" and "rpath r a ys y"

  shows "rpath r x (xs @ ys) y"

  using assms 

  by (unfold rpath_def, auto intro:rtrancl_path_trans)

text {* Elimination rule for empty path *}

lemma rpath_cases [cases pred:rpath,elim]:

  assumes "rpath r a1 a2 a3"

  obtains (rbase)  "a1 = a3" and "a2 = []"

    | (rstep)  y :: "'a" and ys :: "'a list"  

         where "(a1, y) \<in> r" and "a2 = y # ys" and "rpath r y ys a3"

  using assms [unfolded rpath_def]

  by (cases, auto simp:rpath_def pred_of_def)

lemma rpath_nilE [elim!, cases pred:rpath]: 

  assumes "rpath r x [] y"

  obtains "y = x"

  using assms[unfolded rpath_def] by auto

text {*

  Elimination rule for non-empty paths constructed with @{text "#"}.

*}

lemma rpath_ConsE [elim!, cases pred:rpath]:

  assumes "rpath r x (y # ys) x2"

  obtains (rstep) "(x, y) \<in> r" and "rpath r y ys x2"

  using assms[unfolded rpath_def]

  by (cases, auto simp:rpath_def pred_of_def)

text {*

  Elimination rule for non-empty path, where the destination node 

  @{text "y"} is shown to be at the end of the path.

*}

lemma rpath_nnl_lastE [elim]: 

  assumes "rpath r x xs y"

  and "xs \<noteq> []"

  obtains xs' where "xs = xs'@[y]"

  using assms

proof(induct)

    case (rstep x y ys z)

    thus ?case by (cases ys, auto)

qed auto

text {* Other elimination rules of @{text "rpath"} *}

lemma rpath_appendE [elim]:

  assumes "rpath r x (xs @ [a] @ ys) y"

  obtains "rpath r x (xs @ [a]) a" and "rpath r a ys y"

  using rtrancl_path_appendE[OF assms[unfolded rpath_def, simplified], folded rpath_def]

  by auto

lemma rpath_subE [elim]: 

  assumes "rpath r x (xs @ [a] @ ys @ [b] @ zs) y"

  obtains "rpath r x (xs @ [a]) a" and "rpath r a (ys @ [b]) b" and "rpath r b zs y" 

  using assms

 by (elim rpath_appendE, auto)

text {* Every path has a unique end point. *}

lemma rpath_dest_eq [simp]: 

  assumes "rpath r x xs x1"

  and "rpath r x xs x2"

  shows "x1 = x2"

  using assms

  by (induct, auto)

lemma rpath_dest_eq_simp[simp]: 

  assumes "rpath r x xs1 x1"

  and "rpath r x xs2 x2"

  and "xs1 = xs2"

  shows "x1 = x2"

  using assms

  by (induct, auto)

subsubsection {* Properites of @{text "edges_on"} *}

lemma edge_on_headI[simp, intro]: 

  assumes "(a, b) = (a', b')"

  shows "(a, b) \<in> edges_on (a' # b' # xs)"

  using assms

  by (unfold edges_on_def, auto)

lemma edges_on_ConsI[intro]:

  assumes "(a, b) \<in> edges_on xs" 

  shows "(a, b) \<in> edges_on (x#xs)"

  using assms

  apply (unfold edges_on_def, auto)

  by (meson Cons_eq_appendI)

lemma edges_on_appendI1[intro]:

  assumes "(a, b) \<in> edges_on xs" 

  shows "(a, b) \<in> edges_on (xs'@xs)"

  using assms 

  apply (unfold edges_on_def, auto simp:append_assoc)

  by (metis append_assoc)

lemma edges_on_appendI2[intro]:

  assumes "(a, b) \<in> edges_on xs" 

  shows "(a, b) \<in> edges_on (xs@xs')"

  using assms 

  apply (unfold edges_on_def, auto)

  by metis

lemma edges_onE [elim]:

  assumes "(a, b) \<in> edges_on xs"

  obtains a' b' xs' where "(a,b) = (a', b')" "xs = a'#b'#xs'"

        | a' b' xs' where "(a,b) \<noteq> (a', b')" "xs = a'#b'#xs'" "(a,b) \<in> edges_on (b'#xs')"

proof(cases xs)

  case Nil

  with assms show ?thesis

    by (unfold edges_on_def, auto)

next

  case cs1: (Cons a' xsa)

  show ?thesis

  proof(cases xsa)

    case Nil

    with cs1 and assms show ?thesis

      by (unfold edges_on_def, auto)

  next

    case (Cons b' xsb)

    show ?thesis

    proof(cases "(a,b) = (a', b')")

      case True

      with cs1 Cons show ?thesis using that by metis

    next

      case False

      from assms[unfolded cs1 Cons edges_on_def]

      obtain xs1 ys1 where "a' # b' # xsb = xs1 @ [a, b] @ ys1" by auto

      moreover with False obtain c xsc where "xs1 = Cons c xsc" by (cases xs1, auto)

      ultimately have h: "b' # xsb = xsc @ [a, b] @ ys1" by auto

      show ?thesis

        apply (rule that(2)[OF False], insert cs1 Cons, simp)

        using h by auto

    qed

  qed

qed

lemma edges_on_nil [simp]:

  "edges_on [] = {}" by auto

lemma edges_on_single [simp]:

  "edges_on [a] = {}" by auto

lemma edges_on_unfold [simp]:

  "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")

by (auto)

lemma edges_on_len:

  assumes "x \<in> edges_on l"

  shows "2 \<le> length l" using assms by (cases x, auto)

text {* Elimination of @{text "edges_on"} for non-empty path *}

lemma edges_on_consE [elim!, cases set:edges_on]:

  assumes "(a,b) \<in> edges_on (x#xs)"

  obtains (head)  xs' where "x = a" and "xs = b#xs'"

      |  (tail)  "(a,b) \<in> edges_on xs"

      using assms

      by auto

text {*

  Every edges on the path is a graph edges:

*}

lemma rpath_edges_on [intro]: 

  assumes "rpath r x xs y"

  shows "edges_on (x#xs) \<subseteq> r"

  using assms 

 by (induct arbitrary:y, auto)

text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}

lemma edges_on_Cons_mono [intro,simp]: 

   shows "edges_on xs \<subseteq> edges_on (x#xs)"

   by auto

lemma edges_on_append_mono [intro,simp]:

   shows "edges_on xs \<subseteq> edges_on (xs'@xs)"

   by auto

lemma edges_on_append_mono' [intro,simp]:

   shows "edges_on xs \<subseteq> edges_on (xs@xs')"

   by auto

text {*

  The following rule @{text "rpath_transfer"} is used to show 

  that one path is intact as long as all the edges on it are intact

  with the change of graph.

  If @{text "x#xs"} is path in graph @{text "r1"} and 

  every edges along the path is also in @{text "r2"}, 

  then @{text "x#xs"} is also a edge in graph @{text "r2"}:

*}

lemma rpath_transfer[intro]:

  assumes "rpath r1 x xs y"

  and "edges_on (x#xs) \<subseteq> r2"

  shows "rpath r2 x xs y"

  using assms

 by (induct, auto)

lemma edges_on_rpathI[intro, simp]:

  assumes "edges_on (a#xs@[b]) \<subseteq> r"

  shows "rpath r a (xs@[b]) b"

  using assms

 by (induct xs arbitrary: a b, auto) 

lemma list_nnl_appendE [elim]:

  assumes "xs \<noteq> []"

  obtains x xs' where "xs = xs'@[x]"

  by (insert assms, rule rev_exhaust, fastforce)

lemma edges_on_rpathI' [intro]:

  assumes "edges_on (a#xs) \<subseteq> r"

  and "xs \<noteq> []"

  and "last xs = b"

  shows "rpath r a xs b"

proof -

  obtain xs' where "xs = xs'@[b]"

  using assms by fastforce

  with assms show ?thesis by fastforce

qed

text {*

  The following lemma extracts the path from @{text "x"} to @{text "y"}

  from proposition @{text "(x, y) \<in> r^*"}

*}

lemma star_rpath [elim]:

  assumes "(x, y) \<in> r^*"

  obtains xs where "rpath r x xs y"

  using assms

  by (induct, auto)

text {*

  The following lemma uses the path @{text "xs"} from @{text "x"} to @{text "y"}

  as a witness to show @{text "(x, y) \<in> r^*"}.

*}

lemma rpath_star [simp]: 

  assumes "rpath r x xs y"

  shows "(x, y) \<in> r^*"

proof -

  from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]

  have "(pred_of r)\<^sup>*\<^sup>* x y" by metis

  thus ?thesis by (simp add: pred_of_star star_2_pstar)

qed  

declare rpath_star[elim_format]

lemma rpath_transfer' [intro]: 

  assumes "rpath r1 x xs y"

  and "r1 \<subseteq> r2"

  shows "rpath r2 x xs y"

  using assms

  by (induct, auto)

lemma subtree_transfer[intro]:

  assumes "a \<in> subtree r1 a'"

  and "r1 \<subseteq> r2"

  shows "a \<in> subtree r2 a'"

  using assms 

proof -

  from assms(1)