equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/meta_theory/Asig.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Action signatures |
|
7 *) |
|
8 |
|
9 Asig = Option + |
|
10 |
|
11 types |
|
12 |
|
13 'a signature = "('a set * 'a set * 'a set)" |
|
14 |
|
15 consts |
|
16 actions,inputs,outputs,internals,externals |
|
17 ::"'action signature => 'action set" |
|
18 is_asig ::"'action signature => bool" |
|
19 mk_ext_asig ::"'action signature => 'action signature" |
|
20 |
|
21 |
|
22 defs |
|
23 |
|
24 asig_inputs_def "inputs == fst" |
|
25 asig_outputs_def "outputs == (fst o snd)" |
|
26 asig_internals_def "internals == (snd o snd)" |
|
27 |
|
28 actions_def |
|
29 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
|
30 |
|
31 externals_def |
|
32 "externals(asig) == (inputs(asig) Un outputs(asig))" |
|
33 |
|
34 is_asig_def |
|
35 "is_asig(triple) == \ |
|
36 \ ((inputs(triple) Int outputs(triple) = {}) & \ |
|
37 \ (outputs(triple) Int internals(triple) = {}) & \ |
|
38 \ (inputs(triple) Int internals(triple) = {}))" |
|
39 |
|
40 |
|
41 mk_ext_asig_def |
|
42 "mk_ext_asig(triple) == <inputs(triple), outputs(triple), {}>" |
|
43 |
|
44 |
|
45 end |