src/HOL/UNITY/Constrains.thy
author paulson
Mon May 24 15:46:20 1999 +0200 (1999-05-24)
changeset 6705 b2662096ccd0
parent 6575 70d758762c50
child 6823 97babc436a41
permissions -rw-r--r--
Increasing makes sense only for partial orderings
     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 + 
    10 
    11 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    12 
    13   (*Initial states and program => (final state, reversed trace to it)...
    14     Arguments MUST be curried in an inductive definition*)
    15 
    16 inductive "traces init acts"  
    17   intrs 
    18          (*Initial trace is empty*)
    19     Init  "s: init ==> (s,[]) : traces init acts"
    20 
    21     Acts  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
    22 	   ==> (s', s#evs) : traces init acts"
    23 
    24 
    25 consts reachable :: "'a program => 'a set"
    26 
    27 inductive "reachable F"
    28   intrs 
    29     Init  "s: Init F ==> s : reachable F"
    30 
    31     Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
    32 	   ==> s' : reachable F"
    33 
    34 consts
    35   Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
    36 
    37 defs
    38   Constrains_def
    39     "A Co B == {F. F : (reachable F Int A)  co  B}"
    40 
    41   Unless_def
    42     "A Unless B == (A-B) Co (A Un B)"
    43 
    44 constdefs
    45 
    46   Stable     :: "'a set => 'a program set"
    47     "Stable A == A Co A"
    48 
    49   (*Always is the weak form of "invariant"*)
    50   Always :: "'a set => 'a program set"
    51     "Always A == {F. Init F <= A} Int Stable A"
    52 
    53   (*Polymorphic in both states and the meaning of <= *)
    54   Increasing :: "['a => 'b::{order}] => 'a program set"
    55     "Increasing f == INT z. Stable {s. z <= f s}"
    56 
    57 end