isabelle: src/HOLCF/IOA/meta_theory/Asig.thy@a15748c3b7e4 (annotated)

3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	1	(* Title: HOL/IOA/meta_theory/Asig.thy
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	2	ID: $Id$
3275 3f53f2c876f4 changes for release 94-8 mueller parents: 3071 diff changeset	3	Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
3f53f2c876f4 changes for release 94-8 mueller parents: 3071 diff changeset	4	Copyright 1994, 1996 TU Muenchen
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	5
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	6	Action signatures
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	7	*)
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	8
7661 8c3190b173aa depend on Main; wenzelm parents: 3433 diff changeset	9	Asig = Main +
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	10
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	11	types
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	12
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	13	'a signature = "('a set * 'a set * 'a set)"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	14
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	15	consts
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	16	actions,inputs,outputs,internals,externals,locals
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	17	::"'action signature => 'action set"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	18	is_asig ::"'action signature => bool"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	19	mk_ext_asig ::"'action signature => 'action signature"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	20
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	21
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	22	defs
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	23
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	24	asig_inputs_def "inputs == fst"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	25	asig_outputs_def "outputs == (fst o snd)"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	26	asig_internals_def "internals == (snd o snd)"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	27
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	28	actions_def
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	29	"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	30
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	31	externals_def
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	32	"externals(asig) == (inputs(asig) Un outputs(asig))"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	33
3433 2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	34	locals_def
2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	35	"locals asig == ((internals asig) Un (outputs asig))"
2de17c994071 added deadlock freedom, polished definitions and proofs mueller parents: 3275 diff changeset	36
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	37	is_asig_def
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	38	"is_asig(triple) ==
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	39	((inputs(triple) Int outputs(triple) = {}) &
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	40	(outputs(triple) Int internals(triple) = {}) &
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	41	(inputs(triple) Int internals(triple) = {}))"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	42
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	43
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	44	mk_ext_asig_def
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	45	"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	46
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	47
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	48	end

author	wenzelm
	Fri, 29 Oct 1999 12:45:14 +0200
changeset 7970	a15748c3b7e4
parent 7661	8c3190b173aa
child 12218	6597093b77e7
permissions	-rw-r--r--