isabelle: src/HOL/UNITY/SubstAx.thy@226873bffa3a (annotated)

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

author	nipkow
	Thu, 20 Dec 2001 16:53:51 +0100
changeset 12564	226873bffa3a
parent 9685	6d123a7e30bd
child 13796	19f50fa807ae
permissions	-rw-r--r--