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 |
1 Asig = Option + |
9 Asig = Option + |
2 |
10 |
3 types |
11 types |
4 |
12 |
5 'a signature = "('a set * 'a set * 'a set)" |
13 'a signature = "('a set * 'a set * 'a set)" |
9 ::"'action signature => 'action set" |
17 ::"'action signature => 'action set" |
10 is_asig ::"'action signature => bool" |
18 is_asig ::"'action signature => bool" |
11 mk_ext_asig ::"'action signature => 'action signature" |
19 mk_ext_asig ::"'action signature => 'action signature" |
12 |
20 |
13 |
21 |
14 rules |
22 defs |
15 |
23 |
16 asig_projections_def |
24 asig_inputs_def "inputs == fst" |
17 "inputs = fst & outputs = (fst o snd) & internals = (snd o snd)" |
25 asig_outputs_def "outputs == (fst o snd)" |
|
26 asig_internals_def "internals == (snd o snd)" |
18 |
27 |
19 actions_def |
28 actions_def |
20 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
29 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
21 |
30 |
22 externals_def |
31 externals_def |