src/HOL/UNITY/Constrains.thy
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
child 5620 3ac11c4af76a
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
     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 prg A B == 
    15 		 constrains (Acts prg)
    16                             (reachable prg  Int  A)
    17   		            (reachable prg  Int  B)"
    18 
    19   Stable     :: "'a program => 'a set => bool"
    20     "Stable prg A == Constrains prg A A"
    21 
    22   Unless :: "['a program, 'a set, 'a set] => bool"
    23     "Unless prg A B == Constrains prg (A-B) (A Un B)"
    24 
    25   Invariant :: "['a program, 'a set] => bool"
    26   "Invariant prg A == (Init prg) <= A & Stable prg A"
    27 
    28 end