author | paulson |
Thu, 15 Oct 1998 11:35:07 +0200 | |
changeset 5648 | fe887910e32e |
parent 5620 | 3ac11c4af76a |
child 5784 | 54276fba8420 |
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 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
9 |
Constrains = UNITY + Traces + |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
10 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
11 |
constdefs |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
12 |
|
5648 | 13 |
Constrains :: "['a set, 'a set] => 'a program set" |
14 |
"Constrains A B == {F. F : constrains (reachable F Int A) |
|
15 |
(reachable F Int B)}" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
16 |
|
5648 | 17 |
Stable :: "'a set => 'a program set" |
18 |
"Stable A == Constrains A A" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
19 |
|
5648 | 20 |
Unless :: "['a set, 'a set] => 'a program set" |
21 |
"Unless A B == Constrains (A-B) (A Un B)" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
22 |
|
5648 | 23 |
Invariant :: "'a set => 'a program set" |
24 |
"Invariant A == {F. Init F <= A} Int Stable A" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
25 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
26 |
end |