10782
|
1 |
(* Title: HOL/UNITY/PriorityAux
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
|
|
6 |
Auxiliary definitions needed in Priority.thy
|
|
7 |
*)
|
|
8 |
|
|
9 |
PriorityAux = Main +
|
|
10 |
|
|
11 |
types vertex
|
|
12 |
arities vertex::term
|
|
13 |
|
|
14 |
constdefs
|
|
15 |
(* symmetric closure: removes the orientation of a relation *)
|
|
16 |
symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
|
|
17 |
"symcl r == r Un (r^-1)"
|
|
18 |
|
|
19 |
(* Neighbors of a vertex i *)
|
|
20 |
neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
|
10834
|
21 |
"neighbors i r == ((r Un r^-1)``{i}) - {i}"
|
10782
|
22 |
|
|
23 |
R :: "[vertex, (vertex*vertex)set]=>vertex set"
|
10834
|
24 |
"R i r == r``{i}"
|
10782
|
25 |
|
|
26 |
A :: "[vertex, (vertex*vertex)set]=>vertex set"
|
10834
|
27 |
"A i r == (r^-1)``{i}"
|
10782
|
28 |
|
|
29 |
(* reachable and above vertices: the original notation was R* and A* *)
|
|
30 |
reach :: "[vertex, (vertex*vertex)set]=> vertex set"
|
10834
|
31 |
"reach i r == (r^+)``{i}"
|
10782
|
32 |
|
|
33 |
above :: "[vertex, (vertex*vertex)set]=> vertex set"
|
10834
|
34 |
"above i r == ((r^-1)^+)``{i}"
|
10782
|
35 |
|
|
36 |
reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
|
|
37 |
"reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
|
|
38 |
|
|
39 |
(* The original definition *)
|
|
40 |
derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
|
|
41 |
"derive1 i r q == symcl r = symcl q &
|
|
42 |
(ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
|
|
43 |
A i r = {} & R i q = {}"
|
|
44 |
|
|
45 |
(* Our alternative definition *)
|
|
46 |
derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
|
|
47 |
"derive i r q == A i r = {} & (q = reverse i r)"
|
|
48 |
|
|
49 |
rules
|
|
50 |
(* we assume that the universe of vertices is finite *)
|
|
51 |
finite_vertex_univ "finite (UNIV :: vertex set)"
|
|
52 |
|
|
53 |
end
|