src/HOL/UNITY/Constrains.thy
author paulson
Wed Oct 07 10:32:00 1998 +0200 (1998-10-07)
changeset 5620 3ac11c4af76a
parent 5313 1861a564d7e2
child 5648 fe887910e32e
permissions -rw-r--r--
tidying and renaming
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@5313
    13
  Constrains :: "['a program, 'a set, 'a set] => bool"
paulson@5620
    14
    "Constrains F A B == 
paulson@5620
    15
		 constrains (Acts F)
paulson@5620
    16
                            (reachable F  Int  A)
paulson@5620
    17
  		            (reachable F  Int  B)"
paulson@5313
    18
paulson@5313
    19
  Stable     :: "'a program => 'a set => bool"
paulson@5620
    20
    "Stable F A == Constrains F A A"
paulson@5313
    21
paulson@5313
    22
  Unless :: "['a program, 'a set, 'a set] => bool"
paulson@5620
    23
    "Unless F A B == Constrains F (A-B) (A Un B)"
paulson@5313
    24
paulson@5313
    25
  Invariant :: "['a program, 'a set] => bool"
paulson@5620
    26
  "Invariant F A == (Init F) <= A & Stable F A"
paulson@5313
    27
paulson@5313
    28
end