src/HOL/UNITY/SubstAx.thy
author paulson
Thu, 24 Aug 2000 12:39:24 +0200
changeset 9685 6d123a7e30bd
parent 8122 b43ad07660b9
child 13796 19f50fa807ae
permissions -rw-r--r--
xsymbols for leads-to and Join
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/SubstAx
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
6536
281d44905cab made many specification operators infix
paulson
parents: 5648
diff changeset
     6
Weak LeadsTo relation (restricted to the set of reachable states)
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
5313
1861a564d7e2 Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents: 5277
diff changeset
     9
SubstAx = WFair + Constrains + 
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 6575
diff changeset
    11
constdefs
8122
b43ad07660b9 working version, with Alloc now working on the same state space as the whole
paulson
parents: 8041
diff changeset
    12
   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
b43ad07660b9 working version, with Alloc now working on the same state space as the whole
paulson
parents: 8041
diff changeset
    13
    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
b43ad07660b9 working version, with Alloc now working on the same state space as the whole
paulson
parents: 8041
diff changeset
    14
8041
e3237d8c18d6 working version with new theory ELT
paulson
parents: 6575
diff changeset
    15
   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
e3237d8c18d6 working version with new theory ELT
paulson
parents: 6575
diff changeset
    16
    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
9685
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8122
diff changeset
    18
syntax (xsymbols)
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8122
diff changeset
    19
  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
6d123a7e30bd xsymbols for leads-to and Join
paulson
parents: 8122
diff changeset
    20
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
end