src/HOL/UNITY/Constrains.thy
author paulson
Sat Oct 31 12:45:25 1998 +0100 (1998-10-31)
changeset 5784 54276fba8420
parent 5648 fe887910e32e
child 6535 880f31a62784
permissions -rw-r--r--
the Increasing operator
paulson@5313
     1
(*  Title:      HOL/UNITY/Constrains
paulson@5313
     2
    ID:         $Id$
paulson@5313
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5313
     4
    Copyright   1998  University of Cambridge
paulson@5313
     5
paulson@5313
     6
Safety relations: restricted to the set of reachable states.
paulson@5313
     7
*)
paulson@5313
     8
paulson@5313
     9
Constrains = UNITY + Traces + 
paulson@5313
    10
paulson@5313
    11
constdefs
paulson@5313
    12
paulson@5648
    13
  Constrains :: "['a set, 'a set] => 'a program set"
paulson@5648
    14
    "Constrains A B == {F. F : constrains (reachable F  Int  A)
paulson@5648
    15
  		                          (reachable F  Int  B)}"
paulson@5313
    16
paulson@5648
    17
  Stable     :: "'a set => 'a program set"
paulson@5648
    18
    "Stable A == Constrains A A"
paulson@5313
    19
paulson@5648
    20
  Unless :: "['a set, 'a set] => 'a program set"
paulson@5648
    21
    "Unless A B == Constrains (A-B) (A Un B)"
paulson@5313
    22
paulson@5648
    23
  Invariant :: "'a set => 'a program set"
paulson@5648
    24
    "Invariant A == {F. Init F <= A} Int Stable A"
paulson@5313
    25
paulson@5784
    26
  (*Polymorphic in both states and the meaning of <= *)
paulson@5784
    27
  Increasing :: "['a => 'b::{ord}] => 'a program set"
paulson@5784
    28
    "Increasing f == INT z. Stable {s. z <= f s}"
paulson@5784
    29
paulson@5313
    30
end