author | paulson |
Fri, 12 May 2000 15:05:02 +0200 | |
changeset 8862 | 78643f8449c6 |
parent 6535 | 880f31a62784 |
child 10064 | 1a77667b21ef |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/Reach.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Reachability in Directed Graphs. From Chandy and Misra, section 6.4. |
|
7 |
*) |
|
8 |
||
6535 | 9 |
Reach = FP + SubstAx + |
4776 | 10 |
|
11 |
types vertex |
|
12 |
state = "vertex=>bool" |
|
13 |
||
14 |
arities vertex :: term |
|
15 |
||
16 |
consts |
|
17 |
init :: "vertex" |
|
18 |
||
19 |
edges :: "(vertex*vertex) set" |
|
20 |
||
21 |
constdefs |
|
22 |
||
23 |
asgt :: "[vertex,vertex] => (state*state) set" |
|
5071
548f398d770b
Consequences of the change from [ := ] to ( := ) in theory Update.
nipkow
parents:
4896
diff
changeset
|
24 |
"asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
4776 | 25 |
|
5253 | 26 |
Rprg :: state program |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
27 |
"Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})" |
4776 | 28 |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
29 |
reach_invariant :: state set |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
30 |
"reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
4776 | 31 |
|
32 |
fixedpoint :: state set |
|
33 |
"fixedpoint == {s. ALL (u,v): edges. s u --> s v}" |
|
34 |
||
35 |
metric :: state => nat |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5253
diff
changeset
|
36 |
"metric s == card {v. ~ s v}" |
4776 | 37 |
|
38 |
rules |
|
39 |
||
40 |
(*We assume that the set of vertices is finite*) |
|
41 |
finite_graph "finite (UNIV :: vertex set)" |
|
42 |
||
43 |
end |