isabelle: src/HOL/IOA/Asig.thy@5d9c9e284d16 (annotated)

4530 ac1821645636 corrected Title oheimb parents: 3078 diff changeset	1	(* Title: HOL/IOA/Asig.thy
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	2	ID: $Id$
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	4	Copyright 1994 TU Muenchen
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	5	*)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	6
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	7	header {* Action signatures *}
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	8
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	9	theory Asig
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	10	imports Main
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	11	begin
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	12
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	13	types
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	14	'a signature = "('a set * 'a set * 'a set)"
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	15
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	16	consts
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	17	"actions" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	18	"inputs" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	19	"outputs" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	20	"internals" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	21	externals :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	22
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	23	is_asig ::"'action signature => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	24	mk_ext_asig ::"'action signature => 'action signature"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	25
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	26
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	27	defs
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	28
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	29	asig_inputs_def: "inputs == fst"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	30	asig_outputs_def: "outputs == (fst o snd)"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	31	asig_internals_def: "internals == (snd o snd)"
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	32
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	33	actions_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	34	"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	35
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	36	externals_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	37	"externals(asig) == (inputs(asig) Un outputs(asig))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	38
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	39	is_asig_def:
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	40	"is_asig(triple) ==
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	41	((inputs(triple) Int outputs(triple) = {}) &
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	42	(outputs(triple) Int internals(triple) = {}) &
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	43	(inputs(triple) Int internals(triple) = {}))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	44
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	45
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	46	mk_ext_asig_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	47	"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	48
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	49	ML {* use_legacy_bindings (the_context ()) *}
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	50
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	51	end

author	huffman
	Tue, 11 Oct 2005 23:47:29 +0200
changeset 17836	5d9c9e284d16
parent 17288	aa3833fb7bee
child 19801	b2af2549efd1
permissions	-rw-r--r--