isabelle: src/HOL/UNITY/Comp.thy@78643f8449c6 (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
8055 bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	22	constdefs
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	23	preserves :: "('a=>'b) => 'a program set"
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	24	"preserves v == INT z. stable {s. v s = z}"
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	25
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	26	funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	27	"funPair f g == %x. (f x, g x)"
bb15396278fb abolition of localTo: instead "guarantees" has local vars as extra argument paulson parents: 7399 diff changeset	28
5597 a12b25c53df1 composition theory paulson parents: diff changeset	29	end

author	paulson
	Fri, 12 May 2000 15:05:02 +0200
changeset 8862	78643f8449c6
parent 8128	3a5864b465e2
child 11190	44e157622cb2
permissions	-rw-r--r--