Quelle Asig.thy Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/Asig.thy
    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
*)

section \<open>Action signatures\<close>

theory Asig
imports Main
begin

type_synonym 'a signature = "'a set \<times> 'a set \<times> 'a set"

definition inputs :: "'action signature \ 'action set"
  where asig_inputs_def: "inputs = fst"

definition outputs :: "'action signature \ 'action set"
  where asig_outputs_def: "outputs = fst \ snd"

definition internals :: "'action signature \ 'action set"
  where asig_internals_def: "internals = snd \ snd"

definition actions :: "'action signature \ 'action set"
  where "actions asig = inputs asig \ outputs asig \ internals asig"

definition externals :: "'action signature \ 'action set"
  where "externals asig = inputs asig \ outputs asig"

definition locals :: "'action signature \ 'action set"
  where "locals asig = internals asig \ outputs asig"

definition is_asig :: "'action signature \ bool"
  where "is_asig triple \
    inputs triple \<inter> outputs triple = {} \<and>
    outputs triple \<inter> internals triple = {} \<and>
    inputs triple \<inter> internals triple = {}"

definition mk_ext_asig :: "'action signature \ 'action signature"
  where "mk_ext_asig triple = (inputs triple, outputs triple, {})"

lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def

lemma asig_triple_proj:
  "outputs (a, b, c) = b \
   inputs (a, b, c) = a \<and>
   internals (a, b, c) = c"
  by (simp add: asig_projections)

lemma int_and_ext_is_act: "a \ internals S \ a \ externals S \ a \ actions S"
  by (simp add: externals_def actions_def)

lemma ext_is_act: "a \ externals S \ a \ actions S"
  by (simp add: externals_def actions_def)

lemma int_is_act: "a \ internals S \ a \ actions S"
  by (simp add: asig_internals_def actions_def)

lemma inp_is_act: "a \ inputs S \ a \ actions S"
  by (simp add: asig_inputs_def actions_def)

lemma out_is_act: "a \ outputs S \ a \ actions S"
  by (simp add: asig_outputs_def actions_def)

lemma ext_and_act: "x \ actions S \ x \ externals S \ x \ externals S"
  by (fast intro!: ext_is_act)

lemma not_ext_is_int: "is_asig S \ x \ actions S \ x \ externals S \ x \ internals S"
  by (auto simp add: actions_def is_asig_def externals_def)

lemma not_ext_is_int_or_not_act: "is_asig S \ x \ externals S \ x \ internals S \ x \ actions S"
  by (auto simp add: actions_def is_asig_def externals_def)

lemma int_is_not_ext:"is_asig S \ x \ internals S \ x \ externals S"
  by (auto simp add: externals_def actions_def is_asig_def)

end

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.