author | paulson |
Tue, 04 May 1999 10:26:00 +0200 | |
changeset 6570 | a7d7985050a9 |
parent 6536 | 281d44905cab |
child 6575 | 70d758762c50 |
permissions | -rw-r--r-- |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Constrains |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
5 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
6 |
Safety relations: restricted to the set of reachable states. |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
7 |
*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
8 |
|
6535 | 9 |
Constrains = UNITY + |
10 |
||
11 |
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
|
12 |
||
13 |
(*Initial states and program => (final state, reversed trace to it)... |
|
14 |
Arguments MUST be curried in an inductive definition*) |
|
15 |
||
16 |
inductive "traces init acts" |
|
17 |
intrs |
|
18 |
(*Initial trace is empty*) |
|
19 |
Init "s: init ==> (s,[]) : traces init acts" |
|
20 |
||
21 |
Acts "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] |
|
22 |
==> (s', s#evs) : traces init acts" |
|
23 |
||
24 |
||
25 |
consts reachable :: "'a program => 'a set" |
|
26 |
||
27 |
inductive "reachable F" |
|
28 |
intrs |
|
29 |
Init "s: Init F ==> s : reachable F" |
|
30 |
||
31 |
Acts "[| act: Acts F; s : reachable F; (s,s'): act |] |
|
32 |
==> s' : reachable F" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
33 |
|
6536 | 34 |
consts |
35 |
Co, Unless :: "['a set, 'a set] => 'a program set" (infixl 60) |
|
36 |
||
37 |
defs |
|
38 |
Constrains_def |
|
39 |
"A Co B == {F. F : (reachable F Int A) co (reachable F Int B)}" |
|
40 |
||
41 |
Unless_def |
|
42 |
"A Unless B == (A-B) Co (A Un B)" |
|
43 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
44 |
constdefs |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
45 |
|
5648 | 46 |
Stable :: "'a set => 'a program set" |
6536 | 47 |
"Stable A == A Co A" |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
48 |
|
6570 | 49 |
(*Always is the weak form of "invariant"*) |
50 |
Always :: "'a set => 'a program set" |
|
51 |
"Always A == {F. Init F <= A} Int Stable A" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
52 |
|
5784 | 53 |
(*Polymorphic in both states and the meaning of <= *) |
54 |
Increasing :: "['a => 'b::{ord}] => 'a program set" |
|
55 |
"Increasing f == INT z. Stable {s. z <= f s}" |
|
56 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
57 |
end |