src/ZF/UNITY/SubstAx.thy
author paulson
Wed Aug 08 14:33:10 2001 +0200 (2001-08-08)
changeset 11479 697dcaaf478f
child 12195 ed2893765a08
permissions -rw-r--r--
new ZF/UNITY theory
paulson@11479
     1
(*  Title:      ZF/UNITY/SubstAx.thy
paulson@11479
     2
    ID:         $Id$
paulson@11479
     3
    Author:     Sidi O Ehmety, Computer Laboratory
paulson@11479
     4
    Copyright   2001  University of Cambridge
paulson@11479
     5
paulson@11479
     6
Weak LeadsTo relation (restricted to the set of reachable states)
paulson@11479
     7
paulson@11479
     8
Theory ported from HOL.
paulson@11479
     9
*)
paulson@11479
    10
paulson@11479
    11
SubstAx = WFair + Constrains + 
paulson@11479
    12
paulson@11479
    13
constdefs
paulson@11479
    14
   Ensures :: "[i,i] => i"            (infixl 60)
paulson@11479
    15
    "A Ensures B == {F:program. F : (reachable(F) Int A) ensures B &
paulson@11479
    16
		                A:condition & B:condition}"
paulson@11479
    17
paulson@11479
    18
   LeadsTo :: "[i, i] => i"            (infixl 60)
paulson@11479
    19
    "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo B &
paulson@11479
    20
		                A:condition & B:condition}"
paulson@11479
    21
paulson@11479
    22
syntax (xsymbols)
paulson@11479
    23
  "op LeadsTo" :: "[i, i] => i" (infixl " \\<longmapsto>w " 60)
paulson@11479
    24
paulson@11479
    25
end