isabelle: src/HOL/UNITY/Comp.thy@b64d86018785 (annotated)

5597 a12b25c53df1 composition theory paulson parents: diff changeset	1	(* Title: HOL/UNITY/Comp.thy
a12b25c53df1 composition theory paulson parents: diff changeset	2	ID: $Id$
a12b25c53df1 composition theory paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a12b25c53df1 composition theory paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
a12b25c53df1 composition theory paulson parents: diff changeset	5
a12b25c53df1 composition theory paulson parents: diff changeset	6	Composition
a12b25c53df1 composition theory paulson parents: diff changeset	7
a12b25c53df1 composition theory paulson parents: diff changeset	8	From Chandy and Sanders, "Reasoning About Program Composition"
a12b25c53df1 composition theory paulson parents: diff changeset	9	*)
a12b25c53df1 composition theory paulson parents: diff changeset	10
a12b25c53df1 composition theory paulson parents: diff changeset	11	Comp = Union +
a12b25c53df1 composition theory paulson parents: diff changeset	12
7399 cf780c2bcccf changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < paulson parents: 7364 diff changeset	13	instance
cf780c2bcccf changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < paulson parents: 7364 diff changeset	14	program :: (term)ord
5597 a12b25c53df1 composition theory paulson parents: diff changeset	15
7399 cf780c2bcccf changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < paulson parents: 7364 diff changeset	16	defs
5597 a12b25c53df1 composition theory paulson parents: diff changeset	17
7399 cf780c2bcccf changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < paulson parents: 7364 diff changeset	18	component_def "F <= H == EX G. F Join G = H"
5597 a12b25c53df1 composition theory paulson parents: diff changeset	19
7399 cf780c2bcccf changed "component" infix in HOL/UNITY/Comp.thy to be overloaded < paulson parents: 7364 diff changeset	20	strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)"
5612 e981ca6f7332 Finished proofs to end of section 5.1 of Chandy and Sanders paulson parents: 5597 diff changeset	21
5597 a12b25c53df1 composition theory paulson parents: diff changeset	22	end

author	paulson
	Thu, 11 Nov 1999 10:25:17 +0100
changeset 8005	b64d86018785
parent 7399	cf780c2bcccf
child 8055	bb15396278fb
permissions	-rw-r--r--