src/HOL/UNITY/Constrains.thy
author paulson
Sun Jun 13 13:53:33 1999 +0200 (1999-06-13)
changeset 6823 97babc436a41
parent 6705 b2662096ccd0
child 13797 baefae13ad37
permissions -rw-r--r--
new-style infix directives
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@6823
    35
  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co"     60)
paulson@6823
    36
  op_Unless  :: "['a set, 'a set] => 'a program set"  (infixl "Unless" 60)
paulson@6536
    37
paulson@6536
    38
defs
paulson@6536
    39
  Constrains_def
paulson@6575
    40
    "A Co B == {F. F : (reachable F Int A)  co  B}"
paulson@6536
    41
paulson@6536
    42
  Unless_def
paulson@6536
    43
    "A Unless B == (A-B) Co (A Un B)"
paulson@6536
    44
paulson@5313
    45
constdefs
paulson@5313
    46
paulson@5648
    47
  Stable     :: "'a set => 'a program set"
paulson@6536
    48
    "Stable A == A Co A"
paulson@5313
    49
paulson@6570
    50
  (*Always is the weak form of "invariant"*)
paulson@6570
    51
  Always :: "'a set => 'a program set"
paulson@6570
    52
    "Always A == {F. Init F <= A} Int Stable A"
paulson@5313
    53
paulson@5784
    54
  (*Polymorphic in both states and the meaning of <= *)
paulson@6705
    55
  Increasing :: "['a => 'b::{order}] => 'a program set"
paulson@5784
    56
    "Increasing f == INT z. Stable {s. z <= f s}"
paulson@5784
    57
paulson@5313
    58
end