author | wenzelm |
Fri, 02 Sep 2005 17:23:59 +0200 | |
changeset 17233 | 41eee2e7b465 |
parent 14981 | e73f8140af78 |
child 17244 | 0b2ff9541727 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOL/IOA/meta_theory/Asig.ML |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
3071 | 4 |
*) |
5 |
||
6 |
val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; |
|
7 |
||
5068 | 8 |
Goal |
3656 | 9 |
"(outputs (a,b,c) = b) & \ |
10 |
\ (inputs (a,b,c) = a) & \ |
|
11 |
\ (internals (a,b,c) = c)"; |
|
4098 | 12 |
by (simp_tac (simpset() addsimps asig_projections) 1); |
3656 | 13 |
qed "asig_triple_proj"; |
14 |
||
6161 | 15 |
Goal "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; |
4098 | 16 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
3071 | 17 |
qed"int_and_ext_is_act"; |
18 |
||
6161 | 19 |
Goal "[|a:externals(S)|] ==> a:actions(S)"; |
4098 | 20 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,actions_def]) 1); |
3071 | 21 |
qed"ext_is_act"; |
22 |
||
6161 | 23 |
Goal "[|a:internals S|] ==> a:actions S"; |
4098 | 24 |
by (asm_full_simp_tac (simpset() addsimps [asig_internals_def,actions_def]) 1); |
3071 | 25 |
qed"int_is_act"; |
26 |
||
6161 | 27 |
Goal "[|a:inputs S|] ==> a:actions S"; |
4098 | 28 |
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
|
29 |
qed"inp_is_act"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
30 |
|
6161 | 31 |
Goal "[|a:outputs S|] ==> a:actions S"; |
4098 | 32 |
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
|
33 |
qed"out_is_act"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
34 |
|
5068 | 35 |
Goal "(x: actions S & x : externals S) = (x: externals S)"; |
4098 | 36 |
by (fast_tac (claset() addSIs [ext_is_act]) 1 ); |
3071 | 37 |
qed"ext_and_act"; |
17233 | 38 |
|
6161 | 39 |
Goal "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"; |
4098 | 40 |
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1); |
6161 | 41 |
by (Blast_tac 1); |
3071 | 42 |
qed"not_ext_is_int"; |
43 |
||
6161 | 44 |
Goal "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)"; |
4098 | 45 |
by (asm_full_simp_tac (simpset() addsimps [actions_def,is_asig_def,externals_def]) 1); |
6161 | 46 |
by (Blast_tac 1); |
3275 | 47 |
qed"not_ext_is_int_or_not_act"; |
48 |
||
5068 | 49 |
Goalw [externals_def,actions_def,is_asig_def] |
6161 | 50 |
"[| is_asig (S); x:internals S |] ==> x~:externals S"; |
3071 | 51 |
by (Asm_full_simp_tac 1); |
6161 | 52 |
by (Blast_tac 1); |
3275 | 53 |
qed"int_is_not_ext"; |