theory RTree

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

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}. 

*}

text {*

  The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}.

*}

locale sgv = 

  fixes r

  assumes sgv: "single_valued r"

text {*

  The following @{text "rtree"} specifies that @{text "r"} is a 

  {\em Relational Tree}.

*}

locale rtree = sgv + 

  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^+}"

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

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}"

proof -

  { fix a b

    assume h: "(a, b) \<in> r" "b \<in> subtree r x"

    moreover have "a \<in> subtree r x"

    proof -

      from h(2)[unfolded subtree_def] have "(b, x) \<in> r^*" by simp

      with h(1) have "(a, x) \<in> r^*" by auto

      thus ?thesis by (auto simp:subtree_def)

    qed

    ultimately have "((a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x)" 

      by (auto)

  } thus ?thesis by (auto simp:edges_in_def)

qed

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 fbranch =

  fixes r

  assumes fb: "\<forall> x \<in> Range r . finite (children r x)"

begin

lemma finite_children: "finite (children r x)"

proof(cases "children r x = {}")

  case True

  thus ?thesis by auto

next

  case False

  then obtain y where "(y, x) \<in> r" by (auto simp:children_def)

  hence "x \<in> Range r" by auto

  from fb[rule_format, OF this]

  show ?thesis .

qed

end

locale fsubtree = fbranch + 

   assumes wf: "wf r"

(* ccc *)

subsection {* Auxiliary lemmas *}

lemma index_minimize:

  assumes "P (i::nat)"

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

using assms

proof -

  have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"

  using assms

  proof(induct i rule:less_induct)

    case (less t)

    show ?case

    proof(cases "\<forall> j < t. \<not> P j")

      case True

      with less (2) show ?thesis by blast

    next

      case False

      then obtain j where "j < t" "P j" by auto

      from less(1)[OF this]

      show ?thesis .

    qed

  qed 

  with that show ?thesis by metis

qed

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: 

  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

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

lemma rpath_appendI [intro]: 

  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]:

  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

-- {* This is a auxiliary lemmas used only in the proof of @{text "rpath_nnl_lastE"} *}

lemma rpath_nnl_last:

  assumes "rtrancl_path r x xs y"

  and "xs \<noteq> []"

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

proof -

  from append_butlast_last_id[OF `xs \<noteq> []`, symmetric] 

  obtain xs' y' where eq_xs: "xs = (xs' @ y' # [])" by simp

  with assms(1)

  have "rtrancl_path r x ... y" by simp

  hence "y = y'" by (rule rtrancl_path_appendE, auto)

  with eq_xs have "xs = xs'@[y]" by simp

  from that[OF this] show ?thesis .

qed

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: 

  assumes "rpath r x xs y"

  and "xs \<noteq> []"

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

  using assms[unfolded rpath_def]

  by (rule rpath_nnl_last, auto)

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

lemma rpath_appendE:

  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: 

  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:

  assumes "rpath r x xs x1"

  and "rpath r x xs x2"

  shows "x1 = x2"

  using assms

  by (induct, auto)

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

lemma edges_on_unfold:

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

proof -

  { fix c d

    assume "(c, d) \<in> ?L"

    then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2" 

        by (auto simp:edges_on_def)

    have "(c, d) \<in> ?R"

    proof(cases "l1")

      case Nil

      with h have "(c, d) = (a, b)" by auto

      thus ?thesis by auto

    next

      case (Cons e es)

      from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto

      thus ?thesis by (auto simp:edges_on_def)

    qed

  } moreover

  { fix c d

    assume "(c, d) \<in> ?R"

    moreover have "(a, b) \<in> ?L" 

    proof -

      have "(a # b # xs) = []@[a,b]@xs" by simp

      hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto

      thus ?thesis by (unfold edges_on_def, simp)

    qed

    moreover {

        assume "(c, d) \<in> edges_on (b#xs)"

        then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto)

        hence "a#b#xs = (a#l1)@[c,d]@l2" by simp

        hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis

        hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp)

    }

    ultimately have "(c, d) \<in> ?L" by auto

  } ultimately show ?thesis by auto

qed

lemma edges_on_len:

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

  shows "length l \<ge> 2"

  using assms

  by (unfold edges_on_def, 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"

proof -

  from assms obtain l1 l2 

  where h: "(x#xs) = l1 @ [a,b] @ l2" by (unfold edges_on_def, blast)

  have "(\<exists> xs'. x = a \<and> xs = b#xs') \<or> ((a,b) \<in> edges_on xs)"

  proof(cases "l1")

    case Nil with h 

    show ?thesis by auto

  next

    case (Cons e el)

    from h[unfolded this] 

    have "xs = el @ [a,b] @ l2" by auto

    thus ?thesis 

      by (unfold edges_on_def, auto)

  qed

  thus ?thesis 

  proof

    assume "(\<exists>xs'. x = a \<and> xs = b # xs')"

    then obtain xs' where "x = a" "xs = b#xs'" by blast

    from that(1)[OF this] show ?thesis .

  next

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

    from that(2)[OF this] show ?thesis .

  qed

qed

text {*

  Every edges on the path is a graph edges:

*}

lemma rpath_edges_on:

  assumes "rpath r x xs y"

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

  using assms

proof(induct arbitrary:y)

  case (rbase x)

  thus ?case by (unfold edges_on_def, auto)

next

  case (rstep x y ys z)

  show ?case

  proof -

    { fix a b

      assume "(a, b) \<in> edges_on (x # y # ys)"

      hence "(a, b) \<in> r" by (cases, insert rstep, auto)

    } thus ?thesis by auto

  qed

qed

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

lemma edges_on_Cons_mono:

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

proof -

  { fix a b

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

    then obtain l1 l2 where "xs = l1 @ [a,b] @ l2" 

      by (auto simp:edges_on_def)

    hence "x # xs = (x#l1) @ [a, b] @ l2" by auto

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

      by (unfold edges_on_def, blast)

  } thus ?thesis by auto

qed

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:

  assumes "rpath r1 x xs y"

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

  shows "rpath r2 x xs y"

  using assms

proof(induct)

  case (rstep x y ys z)

  show ?case 

  proof(rule rstepI)

    show "(x, y) \<in> r2"

    proof -

      have "(x, y) \<in> edges_on  (x # y # ys)"

          by (unfold edges_on_def, auto)

     with rstep(4) show ?thesis by auto

    qed

  next

    show "rpath r2 y ys z" 

     using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)

  qed

qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)

lemma edges_on_rpathI:

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

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

  using assms

proof(induct xs arbitrary: a b)

  case Nil

  moreover have "(a, b) \<in> edges_on (a # [] @ [b])"

      by (unfold edges_on_def, auto)

  ultimately have "(a, b) \<in> r" by auto

  thus ?case by auto

next

  case (Cons x xs a b)

  from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold)

  from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" .

  moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold)

  ultimately show ?case by (auto)

qed

text {*

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

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

*}

lemma star_rpath:

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

  obtains xs where "rpath r x xs y"

proof -

  have "\<exists> xs. rpath r x xs y"

  proof(unfold rpath_def, rule iffD1[OF rtranclp_eq_rtrancl_path])

    from assms

    show "(pred_of r)\<^sup>*\<^sup>* x y"

      apply (fold pred_of_star)

      by (auto simp:pred_of_def)

  qed

  from that and this show ?thesis by blast

qed

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: 

  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  

lemma subtree_transfer:

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

  and "r1 \<subseteq> r2"

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

proof -

  from assms(1)[unfolded subtree_def] 

  have "(a, a') \<in> r1^*" by auto

  from star_rpath[OF this]

  obtain xs where rp: "rpath r1 a xs a'" by blast

  hence "rpath r2 a xs a'"