author | paulson |
Fri, 29 Jan 1999 16:23:56 +0100 | |
changeset 6161 | bc2a76ce1ea3 |
parent 5068 | fb28eaa07e01 |
child 12218 | 6597093b77e7 |
permissions | -rw-r--r-- |
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 |
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; |
|
10 |
||
5068 | 11 |
Goal |
3656 | 12 |
"(outputs (a,b,c) = b) & \ |
13 |
\ (inputs (a,b,c) = a) & \ |
|
14 |
\ (internals (a,b,c) = c)"; |
|
4098 | 15 |
by (simp_tac (simpset() addsimps asig_projections) 1); |
3656 | 16 |
qed "asig_triple_proj"; |
17 |
||
6161 | 18 |
Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; |
4098 | 19 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
3071 | 20 |
qed"int_and_ext_is_act"; |
21 |
||
6161 | 22 |
Goal "[|a:externals(S)|] ==> a:actions(S)"; |
4098 | 23 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
3071 | 24 |
qed"ext_is_act"; |
25 |
||
6161 | 26 |
Goal "[|a:internals S|] ==> a:actions S"; |
4098 | 27 |
by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1); |
3071 | 28 |
qed"int_is_act"; |
29 |
||
6161 | 30 |
Goal "[|a:inputs S|] ==> a:actions S"; |
4098 | 31 |
by (asm_full_simp_tac (simpset() addsimps [asig_inputs_def,actions_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
32 |
qed"inp_is_act"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
33 |
|
6161 | 34 |
Goal "[|a:outputs S|] ==> a:actions S"; |
4098 | 35 |
by (asm_full_simp_tac (simpset() addsimps [asig_outputs_def,actions_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
36 |
qed"out_is_act"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
37 |
|
5068 | 38 |
Goal "(x: actions S & x : externals S) = (x: externals S)"; |
4098 | 39 |
by (fast_tac (claset() addSIs [ext_is_act]) 1 ); |
3071 | 40 |
qed"ext_and_act"; |
41 |
||
6161 | 42 |
Goal "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"; |
4098 | 43 |
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1); |
6161 | 44 |
by (Blast_tac 1); |
3071 | 45 |
qed"not_ext_is_int"; |
46 |
||
6161 | 47 |
Goal "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)"; |
4098 | 48 |
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1); |
6161 | 49 |
by (Blast_tac 1); |
3275 | 50 |
qed"not_ext_is_int_or_not_act"; |
51 |
||
5068 | 52 |
Goalw [externals_def,actions_def,is_asig_def] |
6161 | 53 |
"[| is_asig (S); x:internals S |] ==> x~:externals S"; |
3071 | 54 |
by (Asm_full_simp_tac 1); |
6161 | 55 |
by (Blast_tac 1); |
3275 | 56 |
qed"int_is_not_ext"; |
57 |