Quelle Asig.thy Sprache: Isabelle

(*  Title:      HOL/IOA/Asig.thy
    Author:     Tobias Nipkow & Konrad Slind
    Copyright   1994  TU Muenchen
*)

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_def: "actions(asig) \ (inputs(asig) \ outputs(asig) \ internals(asig))"

definition externals :: "'action signature \ 'action set"
  where externals_def: "externals(asig) \ (inputs(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 int_and_ext_is_act: "\a\internals(S); a\externals(S)\ \ a\actions(S)"
  apply (simp add: externals_def actions_def)
  done

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

end

quality100%

¤ Dauer der Verarbeitung: 0.2 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.