src/HOL/UNITY/SubstAx.thy
author paulson
Thu Aug 13 18:06:40 1998 +0200 (1998-08-13)
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5620 3ac11c4af76a
permissions -rw-r--r--
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
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@5277
     6
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@4776
    11
constdefs
paulson@4776
    12
paulson@5253
    13
   LeadsTo :: "['a program, 'a set, 'a set] => bool"
paulson@5253
    14
    "LeadsTo prg A B ==
paulson@5253
    15
		 leadsTo (Acts prg)
paulson@5253
    16
                         (reachable prg  Int  A)
paulson@5253
    17
  		         (reachable prg  Int  B)"
paulson@4776
    18
end