equal
deleted
inserted
replaced
1 theory RTree |
1 theory RTree |
2 imports "~~/src/HOL/Library/Transitive_Closure_Table" Max |
2 imports "~~/src/HOL/Library/Transitive_Closure_Table" |
3 (* "Lcrules" *) |
|
4 begin |
3 begin |
5 |
4 |
6 section {* A theory of relational trees *} |
5 section {* A theory of relational trees *} |
7 |
6 |
8 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y" |
7 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y" |
19 |
18 |
20 A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both |
19 A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both |
21 {\em single valued} and {\em acyclic}. |
20 {\em single valued} and {\em acyclic}. |
22 *} |
21 *} |
23 |
22 |
24 text {* |
23 |
25 The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}. |
24 locale rtree = |
26 *} |
|
27 locale sgv = |
|
28 fixes r |
25 fixes r |
29 assumes sgv: "single_valued r" |
26 assumes sgv: "single_valued r" |
30 |
|
31 text {* |
|
32 The following @{text "rtree"} specifies that @{text "r"} is a |
|
33 {\em Relational Tree}. |
|
34 *} |
|
35 locale rtree = sgv + |
|
36 assumes acl: "acyclic r" |
27 assumes acl: "acyclic r" |
37 |
28 |
38 text {* |
29 text {* |
39 The following two auxiliary functions @{text "rel_of"} and @{text "pred_of"} |
30 The following two auxiliary functions @{text "rel_of"} and @{text "pred_of"} |
40 transfer between the predicate and set representation of binary relations. |
31 transfer between the predicate and set representation of binary relations. |