(* Title: HOL/IOA/meta_theory/Asig.thy ID: $Id: Asig.thy,v 1.7 2005/09/02 15:23:59 wenzelm Exp $ Author: Olaf Müller, Tobias Nipkow & Konrad Slind *) header {* Action signatures *} theory Asig imports Main begin types 'a signature = "('a set * 'a set * 'a set)" consts actions :: "'action signature => 'action set" inputs :: "'action signature => 'action set" outputs :: "'action signature => 'action set" internals :: "'action signature => 'action set" externals :: "'action signature => 'action set" locals :: "'action signature => 'action set" is_asig ::"'action signature => bool" mk_ext_asig ::"'action signature => 'action signature" defs asig_inputs_def: "inputs == fst" asig_outputs_def: "outputs == (fst o snd)" asig_internals_def: "internals == (snd o snd)" actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))" locals_def: "locals asig == ((internals asig) Un (outputs asig))" is_asig_def: "is_asig(triple) == ((inputs(triple) Int outputs(triple) = {}) & (outputs(triple) Int internals(triple) = {}) & (inputs(triple) Int internals(triple) = {}))" mk_ext_asig_def: "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" ML {* use_legacy_bindings (the_context ()) *} end
theorems asig_projections:
inputs == fst
outputs == fst o snd
internals == snd o snd
theorem asig_triple_proj:
outputs (a, b, c) = b ∧ inputs (a, b, c) = a ∧ internals (a, b, c) = c
theorem int_and_ext_is_act:
[| a ∉ internals S; a ∉ externals S |] ==> a ∉ actions S
theorem ext_is_act:
a ∈ externals S ==> a ∈ actions S
theorem int_is_act:
a ∈ internals S ==> a ∈ actions S
theorem inp_is_act:
a ∈ inputs S ==> a ∈ actions S
theorem out_is_act:
a ∈ outputs S ==> a ∈ actions S
theorem ext_and_act:
(x ∈ actions S ∧ x ∈ externals S) = (x ∈ externals S)
theorem not_ext_is_int:
[| is_asig S; x ∈ actions S |] ==> (x ∉ externals S) = (x ∈ internals S)
theorem not_ext_is_int_or_not_act:
is_asig S ==> (x ∉ externals S) = (x ∈ internals S ∨ x ∉ actions S)
theorem int_is_not_ext:
[| is_asig S; x ∈ internals S |] ==> x ∉ externals S