3071
|
1 |
(* Title: HOL/IOA/meta_theory/Asig.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
|
|
4 |
Copyright 1994,1996 TU Muenchen
|
|
5 |
|
|
6 |
Action signatures
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Asig;
|
|
10 |
|
|
11 |
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
|
|
12 |
|
|
13 |
goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
|
|
14 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
|
|
15 |
qed"int_and_ext_is_act";
|
|
16 |
|
|
17 |
goal thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
|
|
18 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
|
|
19 |
qed"ext_is_act";
|
|
20 |
|
|
21 |
goal thy "!!a.[|a:internals S|] ==> a:actions S";
|
|
22 |
by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
|
|
23 |
qed"int_is_act";
|
|
24 |
|
|
25 |
goal thy "(x: actions S & x : externals S) = (x: externals S)";
|
|
26 |
by (fast_tac (!claset addSIs [ext_is_act]) 1 );
|
|
27 |
qed"ext_and_act";
|
|
28 |
|
|
29 |
goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
|
|
30 |
by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
|
|
31 |
by (best_tac (set_cs addEs [equalityCE]) 1);
|
|
32 |
qed"not_ext_is_int";
|
|
33 |
|
|
34 |
goalw thy [externals_def,actions_def,is_asig_def]
|
|
35 |
"!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
|
|
36 |
by (Asm_full_simp_tac 1);
|
|
37 |
by (best_tac (set_cs addEs [equalityCE]) 1);
|
|
38 |
qed"int_is_not_ext"; |