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 giving 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^*}"

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 means of @{term "edges_in"} from the other side, 

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

  it is sufficient if @{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)

subsection {* Auxiliary lemmas *}

lemma index_minimize:

  assumes "P (i::nat)"

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

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

print_statement rtrancl_path.induct

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)

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_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)

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

text {*

  The following lemmas establishes a relation from pathes in @{text "r"}

  to @{text "r^+"} relation.

*}

lemma rpath_plus: 

  assumes "rpath r x xs y"

  and "xs \<noteq> []"

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

proof -

  from assms(2) obtain e es where "xs = e#es" by (cases xs, auto)

  from assms(1)[unfolded this]

  show ?thesis

  proof(cases)

    case rstep

    show ?thesis

    proof -

      from rpath_star[OF rstep(2)] have "(e, y) \<in> r\<^sup>*" .

      with rstep(1) show "(x, y) \<in> r^+" by auto

    qed

  qed

qed

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

text {*

  @{text "subtree"} is mono with respect to the underlying graph.

*}

lemma subtree_mono:

  assumes "r1 \<subseteq> r2"

  shows "subtree r1 x \<subseteq> subtree r2 x"

proof

  fix c

  assume "c \<in> subtree r1 x"

  hence "(c, x) \<in> r1^*" by (auto simp:subtree_def)

  from star_rpath[OF this] obtain xs 

  where rp:"rpath r1 c xs x" by metis

  hence "rpath r2 c xs x"

  proof(rule rpath_transfer)

    from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r1" .

    with assms show "edges_on (c # xs) \<subseteq> r2" by auto

  qed

  thus "c \<in> subtree r2 x"

    by (rule rpath_star[elim_format], auto simp:subtree_def)

qed

text {*

  The following lemma characterizes the change of sub-tree of @{text "x"}

  with the removal of an outside edge @{text "(a,b)"}. 

  Note that, according to lemma @{thm edges_in_refutation}, the assumption

  @{term "b \<notin> subtree r x"} amounts to saying @{text "(a, b)"} 

  is outside the sub-tree of @{text "x"}.

*}

lemma subtree_del_outside: (* ddd *)

    assumes "b \<notin> subtree r x" 

    shows "subtree (r - {(a, b)}) x = (subtree r x)" 

proof -

  { fix c

    assume "c \<in> (subtree r x)"

    hence "(c, x) \<in> r^*" by (auto simp:subtree_def)

    hence "c \<in> subtree (r - {(a, b)}) x"

    proof(rule star_rpath)

      fix xs

      assume rp: "rpath r c xs x"

      show ?thesis

      proof -

        from rp

        have "rpath  (r - {(a, b)}) c xs x"

        proof(rule rpath_transfer)

          from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .

          moreover have "(a, b) \<notin> edges_on (c#xs)"

          proof

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

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

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

            then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)

            from rp[unfolded this]

            show False

            proof(rule rpath_appendE)

              assume "rpath r b l2 x"

              thus ?thesis

              by(rule rpath_star[elim_format], insert assms(1), auto simp:subtree_def)

            qed

          qed

          ultimately show "edges_on (c # xs) \<subseteq> r - {(a,b)}" by auto

        qed

        thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)

      qed

    qed

  } moreover {

    fix c

    assume "c \<in> subtree (r - {(a, b)}) x"

    moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)

    ultimately have "c \<in> (subtree r x)" by auto

  } ultimately show ?thesis by auto

qed

lemma subtree_insert_ext:

    assumes "b \<in> subtree r x"

    shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 

    using assms by (auto simp:subtree_def rtrancl_insert)

lemma subtree_insert_next:

    assumes "b \<notin> subtree r x"

    shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" 

    using assms

    by (auto simp:subtree_def rtrancl_insert)

subsubsection {* Properties about relational trees *}

context rtree