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
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@5313
    14
    "Constrains prg A B == 
paulson@5313
    15
		 constrains (Acts prg)
paulson@5313
    16
                            (reachable prg  Int  A)
paulson@5313
    17
  		            (reachable prg  Int  B)"
paulson@5313
    18
paulson@5313
    19
  Stable     :: "'a program => 'a set => bool"
paulson@5313
    20
    "Stable prg A == Constrains prg A A"
paulson@5313
    21
paulson@5313
    22
  Unless :: "['a program, 'a set, 'a set] => bool"
paulson@5313
    23
    "Unless prg A B == Constrains prg (A-B) (A Un B)"
paulson@5313
    24
paulson@5313
    25
  Invariant :: "['a program, 'a set] => bool"
paulson@5313
    26
  "Invariant prg A == (Init prg) <= A & Stable prg A"
paulson@5313
    27
paulson@5313
    28
end