--- a/RTree.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/RTree.thy Tue Jun 07 13:51:39 2016 +0100
@@ -45,40 +45,42 @@
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.
-*}
+ 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:
-*}
+
+ 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.
+
+ 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"}.
-*}
+ (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"}:
-*}
+
+ 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^*}"
@@ -87,17 +89,20 @@
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.
-*}
+
+ 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.
-*}
+
+ 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)
@@ -1735,12 +1740,6 @@
with h_b(2) and that show ?thesis by metis
qed
-(*
-lcrules crules
-
-declare crules(26,43,44,45,46,47)[rule del]
-*)
-
declare RTree.subtree_transfer[rule del]