author | paulson |
Sat, 31 Oct 1998 12:45:25 +0100 | |
changeset 5784 | 54276fba8420 |
parent 5648 | fe887910e32e |
child 6535 | 880f31a62784 |
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 |
|
5784 | 26 |
(*Polymorphic in both states and the meaning of <= *) |
27 |
Increasing :: "['a => 'b::{ord}] => 'a program set" |
|
28 |
"Increasing f == INT z. Stable {s. z <= f s}" |
|
29 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
30 |
end |