src/HOL/UNITY/SubstAx.thy
author paulson
Thu, 15 Oct 1998 11:35:07 +0200
changeset 5648 fe887910e32e
parent 5620 3ac11c4af76a
child 6536 281d44905cab
permissions -rw-r--r--
specifications as sets of programs
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
5277
e4297d03e5d2 A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents: 5253
diff changeset
     6
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
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
5648
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    13
   LeadsTo :: "['a set, 'a set] => 'a program set"
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    14
    "LeadsTo A B == {F. F : leadsTo (reachable F  Int  A)
fe887910e32e specifications as sets of programs
paulson
parents: 5620
diff changeset
    15
	   	                    (reachable F  Int  B)}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
end