4559
|
1 |
(* Title: HOLCF/IOA/TrivEx.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Olaf Mueller
|
|
4 |
Copyright 1995 TU Muenchen
|
|
5 |
|
|
6 |
Trivial Abstraction Example
|
|
7 |
*)
|
|
8 |
|
|
9 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
|
5132
|
10 |
by (fast_tac (claset() addDs prems) 1);
|
4559
|
11 |
qed "imp_conj_lemma";
|
|
12 |
|
|
13 |
|
5068
|
14 |
Goalw [is_abstraction_def]
|
4559
|
15 |
"is_abstraction h_abs C_ioa A_ioa";
|
|
16 |
by (rtac conjI 1);
|
|
17 |
(* ------------- start states ------------ *)
|
|
18 |
by (simp_tac (simpset() addsimps
|
|
19 |
[h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
|
|
20 |
(* -------------- step case ---------------- *)
|
|
21 |
by (REPEAT (rtac allI 1));
|
|
22 |
by (rtac imp_conj_lemma 1);
|
|
23 |
by (simp_tac (simpset() addsimps [trans_of_def,
|
|
24 |
C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
|
|
25 |
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
|
5192
|
26 |
by (induct_tac "a" 1);
|
5132
|
27 |
by Auto_tac;
|
4559
|
28 |
qed"h_abs_is_abstraction";
|
|
29 |
|
|
30 |
|
5068
|
31 |
Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
|
5132
|
32 |
by (rtac AbsRuleT1 1);
|
|
33 |
by (rtac h_abs_is_abstraction 1);
|
|
34 |
by (rtac MC_result 1);
|
4559
|
35 |
by (abstraction_tac 1);
|
|
36 |
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
|
|
37 |
qed"TrivEx_abstraction";
|
|
38 |
|
|
39 |
|