43 definition "rel_of r = {(x, y) | x y. r x y}" |
43 definition "rel_of r = {(x, y) | x y. r x y}" |
44 |
44 |
45 definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)" |
45 definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)" |
46 |
46 |
47 text {* |
47 text {* |
48 To reason about {\em Relational Graph}, a notion of path is |
48 |
49 needed, which is given by the following @{text "rpath"} (short |
49 To reason about {\em Relational Graph}, a notion of path is needed, |
50 for `relational path`). |
50 which is given by the following @{text "rpath"} (short for |
51 The path @{text "xs"} in proposition @{text "rpath r x xs y"} is |
51 `relational path`). The path @{text "xs"} in proposition @{text |
52 a path leading from @{text "x"} to @{text "y"}, which serves as a |
52 "rpath r x xs y"} is a path leading from @{text "x"} to @{text "y"}, |
53 witness of the fact @{text "(x, y) \<in> r^*"}. |
53 which serves as a witness of the fact @{text "(x, y) \<in> r^*"}. |
54 |
54 |
55 @{text "rpath"} |
55 @{text "rpath"} is simply a wrapper of the @{text "rtrancl_path"} |
56 is simply a wrapper of the @{text "rtrancl_path"} defined in the imported |
56 defined in the imported theory @{text "Transitive_Closure_Table"}, |
57 theory @{text "Transitive_Closure_Table"}, which defines |
57 which defines a notion of path for the predicate form of binary |
58 a notion of path for the predicate form of binary relations. |
58 relations. *} |
59 *} |
59 |
60 definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y" |
60 definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y" |
61 |
61 |
62 text {* |
62 text {* |
63 Given a path @{text "ps"}, @{text "edges_on ps"} is the |
63 |
64 set of edges along the path, which is defined as follows: |
64 Given a path @{text "ps"}, @{text "edges_on ps"} is the set of edges |
65 *} |
65 along the path, which is defined as follows: *} |
66 |
66 |
67 definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}" |
67 definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}" |
68 |
68 |
69 text {* |
69 text {* |
70 The following @{text "indep"} defines a notion of independence. |
70 |
|
71 The following @{text "indep"} defines a notion of independence. |
71 Two nodes @{text "x"} and @{text "y"} are said to be independent |
72 Two nodes @{text "x"} and @{text "y"} are said to be independent |
72 (expressed as @{text "indep x y"}), if neither one is reachable |
73 (expressed as @{text "indep x y"}), if neither one is reachable |
73 from the other in relational graph @{text "r"}. |
74 from the other in relational graph @{text "r"}. *} |
74 *} |
75 |
75 definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))" |
76 definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))" |
76 |
77 |
77 text {* |
78 text {* |
78 In relational tree @{text "r"}, the sub tree of node @{text "x"} is written |
79 |
79 @{text "subtree r x"}, which is defined to be the set of nodes (including itself) |
80 In relational tree @{text "r"}, the sub tree of node @{text "x"} is |
80 which can reach @{text "x"} by following some path in @{text "r"}: |
81 written @{text "subtree r x"}, which is defined to be the set of |
81 *} |
82 nodes (including itself) which can reach @{text "x"} by following |
|
83 some path in @{text "r"}: *} |
82 |
84 |
83 definition "subtree r x = {y . (y, x) \<in> r^*}" |
85 definition "subtree r x = {y . (y, x) \<in> r^*}" |
84 |
86 |
85 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
87 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
86 |
88 |
87 definition "root r x = (ancestors r x = {})" |
89 definition "root r x = (ancestors r x = {})" |
88 |
90 |
89 text {* |
91 text {* |
90 The following @{text "edge_in r x"} is the set of edges |
92 |
91 contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph. |
93 The following @{text "edge_in r x"} is the set of edges contained in |
92 *} |
94 the sub-tree of @{text "x"}, with @{text "r"} as the underlying |
|
95 graph. *} |
93 |
96 |
94 definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}" |
97 definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}" |
95 |
98 |
96 text {* |
99 text {* |
97 The following lemma @{text "edges_in_meaning"} shows the intuitive meaning |
100 |
98 of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`, |
101 The following lemma @{text "edges_in_meaning"} shows the intuitive |
99 i.e., both @{text "a"} and @{text "b"} are in the sub-tree. |
102 meaning of `an edge @{text "(a, b)"} is in the sub-tree of @{text |
100 *} |
103 "x"}`, i.e., both @{text "a"} and @{text "b"} are in the sub-tree. |
|
104 *} |
|
105 |
101 lemma edges_in_meaning: |
106 lemma edges_in_meaning: |
102 "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}" |
107 "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}" |
103 by (auto simp:edges_in_def subtree_def) |
108 by (auto simp:edges_in_def subtree_def) |
104 |
109 |
105 text {* |
110 text {* |