src/HOL/UNITY/Constrains.thy
author paulson
Thu Apr 29 10:51:58 1999 +0200 (1999-04-29)
changeset 6536 281d44905cab
parent 6535 880f31a62784
child 6570 a7d7985050a9
permissions -rw-r--r--
made many specification operators infix
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@6535
     9
Constrains = UNITY + 
paulson@6535
    10
paulson@6535
    11
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
paulson@6535
    12
paulson@6535
    13
  (*Initial states and program => (final state, reversed trace to it)...
paulson@6535
    14
    Arguments MUST be curried in an inductive definition*)
paulson@6535
    15
paulson@6535
    16
inductive "traces init acts"  
paulson@6535
    17
  intrs 
paulson@6535
    18
         (*Initial trace is empty*)
paulson@6535
    19
    Init  "s: init ==> (s,[]) : traces init acts"
paulson@6535
    20
paulson@6535
    21
    Acts  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
paulson@6535
    22
	   ==> (s', s#evs) : traces init acts"
paulson@6535
    23
paulson@6535
    24
paulson@6535
    25
consts reachable :: "'a program => 'a set"
paulson@6535
    26
paulson@6535
    27
inductive "reachable F"
paulson@6535
    28
  intrs 
paulson@6535
    29
    Init  "s: Init F ==> s : reachable F"
paulson@6535
    30
paulson@6535
    31
    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
paulson@6535
    32
	   ==> s' : reachable F"
paulson@5313
    33
paulson@6536
    34
consts
paulson@6536
    35
  Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
paulson@6536
    36
paulson@6536
    37
defs
paulson@6536
    38
  Constrains_def
paulson@6536
    39
    "A Co B == {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
paulson@6536
    40
paulson@6536
    41
  Unless_def
paulson@6536
    42
    "A Unless B == (A-B) Co (A Un B)"
paulson@6536
    43
paulson@5313
    44
constdefs
paulson@5313
    45
paulson@5648
    46
  Stable     :: "'a set => 'a program set"
paulson@6536
    47
    "Stable A == A Co A"
paulson@5313
    48
paulson@5648
    49
  Invariant :: "'a set => 'a program set"
paulson@5648
    50
    "Invariant A == {F. Init F <= A} Int Stable A"
paulson@5313
    51
paulson@5784
    52
  (*Polymorphic in both states and the meaning of <= *)
paulson@5784
    53
  Increasing :: "['a => 'b::{ord}] => 'a program set"
paulson@5784
    54
    "Increasing f == INT z. Stable {s. z <= f s}"
paulson@5784
    55
paulson@5313
    56
end