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
     1 (*  Title:      HOL/UNITY/Constrains
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Safety relations: restricted to the set of reachable states.
     7 *)
     8 
     9 Constrains = UNITY + Traces + 
    10 
    11 constdefs
    12 
    13   Constrains :: "['a program, 'a set, 'a set] => bool"
    14     "Constrains F A B == 
    15 		 constrains (Acts F)
    16                             (reachable F  Int  A)
    17   		            (reachable F  Int  B)"
    18 
    19   Stable     :: "'a program => 'a set => bool"
    20     "Stable F A == Constrains F A A"
    21 
    22   Unless :: "['a program, 'a set, 'a set] => bool"
    23     "Unless F A B == Constrains F (A-B) (A Un B)"
    24 
    25   Invariant :: "['a program, 'a set] => bool"
    26   "Invariant F A == (Init F) <= A & Stable F A"
    27 
    28 end