src/HOL/UNITY/SubstAx.thy
author paulson
Thu Aug 24 12:39:24 2000 +0200 (2000-08-24)
changeset 9685 6d123a7e30bd
parent 8122 b43ad07660b9
child 13796 19f50fa807ae
permissions -rw-r--r--
xsymbols for leads-to and Join
paulson@4776
     1
(*  Title:      HOL/UNITY/SubstAx
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@6536
     6
Weak LeadsTo relation (restricted to the set of reachable states)
paulson@4776
     7
*)
paulson@4776
     8
paulson@5313
     9
SubstAx = WFair + Constrains + 
paulson@4776
    10
paulson@8041
    11
constdefs
paulson@8122
    12
   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
paulson@8122
    13
    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
paulson@8122
    14
paulson@8041
    15
   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
paulson@8041
    16
    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
paulson@4776
    17
paulson@9685
    18
syntax (xsymbols)
paulson@9685
    19
  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
paulson@9685
    20
paulson@4776
    21
end