isabelle: src/HOL/IOA/meta_theory/Asig.thy@836950047d85 (annotated)

966 3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	1	(* Title: HOL/IOA/meta_theory/Asig.thy
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	2	ID: $Id$
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	4	Copyright 1994 TU Muenchen
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	5
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	6	Action signatures
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	7	*)
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	8
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	9	Asig = Option +
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	10
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	11	types
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	12
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	13	'a signature = "('a set * 'a set * 'a set)"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	14
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	15	consts
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	16	actions,inputs,outputs,internals,externals
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	17	::"'action signature => 'action set"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	18	is_asig ::"'action signature => bool"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	19	mk_ext_asig ::"'action signature => 'action signature"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	20
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	21
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	22	defs
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	23
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	24	asig_inputs_def "inputs == fst"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	25	asig_outputs_def "outputs == (fst o snd)"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	26	asig_internals_def "internals == (snd o snd)"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	27
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	28	actions_def
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	29	"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	30
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	31	externals_def
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	32	"externals(asig) == (inputs(asig) Un outputs(asig))"
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	33
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	34	is_asig_def
1151 c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 diff changeset	35	"is_asig(triple) ==
c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 diff changeset	36	((inputs(triple) Int outputs(triple) = {}) &
c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 diff changeset	37	(outputs(triple) Int internals(triple) = {}) &
c820b3cc3df0 removed \...\ inside strings clasohm parents: 972 diff changeset	38	(inputs(triple) Int internals(triple) = {}))"
966 3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	39
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	40
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	41	mk_ext_asig_def
972 e61b058d58d2 changed syntax of tuples from <..., ...> to (..., ...) clasohm parents: 966 diff changeset	42	"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
966 3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	43
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	44
3fd66f245ad7 converted IOA with curried function application clasohm parents: diff changeset	45	end

author	paulson
	Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868	836950047d85
parent 1151	c820b3cc3df0
child 2018	bcd69cc47cf0
permissions	-rw-r--r--