isabelle: src/HOL/IOA/Asig.thy@952b2b102a0a (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	Author: Tobias Nipkow & Konrad Slind
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	3	Copyright 1994 TU Muenchen
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	4	*)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	5
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	6	header {* Action signatures *}
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	7
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	8	theory Asig
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	9	imports Main
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	10	begin
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	11
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	12	types
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	13	'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	14
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	15	consts
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	16	"actions" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	17	"inputs" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	18	"outputs" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	19	"internals" :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	20	externals :: "'action signature => 'action set"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	21
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	22	is_asig ::"'action signature => bool"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	23	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	24
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	defs
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	27
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	28	asig_inputs_def: "inputs == fst"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	29	asig_outputs_def: "outputs == (fst o snd)"
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	30	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	31
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	32	actions_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	33	"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	34
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	35	externals_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	36	"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	37
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	38	is_asig_def:
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	39	"is_asig(triple) ==
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	40	((inputs(triple) Int outputs(triple) = {}) &
aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	41	(outputs(triple) Int internals(triple) = {}) &
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	42	(inputs(triple) Int internals(triple) = {}))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	43
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	44
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	45	mk_ext_asig_def:
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	46	"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	47
19801 b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	48
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	49	lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	50
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	51	lemma int_and_ext_is_act: "[\| a~:internals(S) ;a~:externals(S)\|] ==> a~:actions(S)"
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	52	apply (simp add: externals_def actions_def)
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	53	done
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	54
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	55	lemma ext_is_act: "[\|a:externals(S)\|] ==> a:actions(S)"
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	56	apply (simp add: externals_def actions_def)
b2af2549efd1 removed obsolete ML files; wenzelm parents: 17288 diff changeset	57	done
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	58
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 11482 diff changeset	59	end

author	wenzelm
	Wed, 12 May 2010 14:17:26 +0200
changeset 36862	952b2b102a0a
parent 19801	b2af2549efd1
child 42174	d0be2722ce9f
permissions	-rw-r--r--