src/HOL/IOA/Asig.thy
author wenzelm
Fri, 22 Nov 2013 20:37:19 +0100
changeset 54560 7f36da77130d
parent 42174 d0be2722ce9f
child 58889 5b7a9633cfa8
permissions -rw-r--r--
more .hgignore;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
42174
d0be2722ce9f modernized specifications;
wenzelm
parents: 36862
diff changeset
    12
type_synonym
17288
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