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"; |
|
10 by (fast_tac (claset() addDs prems) 1); |
|
11 qed "imp_conj_lemma"; |
|
12 |
|
13 |
|
14 Goalw [is_abstraction_def] |
|
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); |
|
26 by (induct_tac "a" 1); |
|
27 by Auto_tac; |
|
28 qed"h_abs_is_abstraction"; |
|
29 |
|
30 |
|
31 (* |
|
32 Goalw [xt2_def,plift,option_lift] |
|
33 "(xt2 (plift afun)) (s,a,t) = (afun a)"; |
|
34 (* !!!!!!!!!!!!! Occurs check !!!! *) |
|
35 by (induct_tac "a" 1); |
|
36 |
|
37 *) |
|
38 |
|
39 Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def, |
|
40 C_trans_def,trans_of_def] |
|
41 "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"; |
|
42 by Auto_tac; |
|
43 qed"Enabled_implication"; |
|
44 |
|
45 |
|
46 Goalw [is_live_abstraction_def] |
|
47 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"; |
|
48 by Auto_tac; |
|
49 (* is_abstraction *) |
|
50 by (rtac h_abs_is_abstraction 1); |
|
51 (* temp_weakening *) |
|
52 by (abstraction_tac 1); |
|
53 by (etac Enabled_implication 1); |
|
54 qed"h_abs_is_liveabstraction"; |
|
55 |
|
56 |
|
57 Goalw [C_live_ioa_def] |
|
58 "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"; |
|
59 by (rtac AbsRuleT2 1); |
|
60 by (rtac h_abs_is_liveabstraction 1); |
|
61 by (rtac MC_result 1); |
|
62 by (abstraction_tac 1); |
|
63 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1); |
|
64 qed"TrivEx2_abstraction"; |
|
65 |
|
66 |
|
67 (* |
|
68 Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) |
|
69 IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))"; |
|
70 |
|
71 *) |
|
72 |
|