3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/RefMappings.ML
|
3275
|
2 |
ID: $Id$
|
3071
|
3 |
Author: Olaf Mueller
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
|
|
6 |
Refinement Mappings in HOLCF/IOA
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
goal thy "laststate (s,UU) = s";
|
|
12 |
by (simp_tac (!simpset addsimps [laststate_def]) 1);
|
|
13 |
qed"laststate_UU";
|
|
14 |
|
|
15 |
goal thy "laststate (s,nil) = s";
|
|
16 |
by (simp_tac (!simpset addsimps [laststate_def]) 1);
|
|
17 |
qed"laststate_nil";
|
|
18 |
|
|
19 |
goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
|
|
20 |
by (simp_tac (!simpset addsimps [laststate_def]) 1);
|
|
21 |
by (case_tac "ex=nil" 1);
|
|
22 |
by (Asm_simp_tac 1);
|
|
23 |
by (Asm_simp_tac 1);
|
|
24 |
bd (Finite_Last1 RS mp) 1;
|
|
25 |
ba 1;
|
|
26 |
by (def_tac 1);
|
|
27 |
qed"laststate_cons";
|
|
28 |
|
|
29 |
Addsimps [laststate_UU,laststate_nil,laststate_cons];
|
|
30 |
|
|
31 |
(* ---------------------------------------------------------------------------- *)
|
|
32 |
|
|
33 |
section "transitions and moves";
|
|
34 |
|
|
35 |
|
|
36 |
goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
|
|
37 |
|
|
38 |
by (res_inst_tac [("x","(s,(a,t)>>nil)")] exI 1);
|
|
39 |
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
|
|
40 |
qed"transition_is_ex";
|
|
41 |
|
|
42 |
|
|
43 |
goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
|
|
44 |
|
|
45 |
by (res_inst_tac [("x","(s,nil)")] exI 1);
|
|
46 |
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
|
|
47 |
qed"nothing_is_ex";
|
|
48 |
|
|
49 |
|
|
50 |
goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
|
|
51 |
\ ==> ? ex. move A ex s a s''";
|
|
52 |
|
|
53 |
by (res_inst_tac [("x","(s,(a,s')>>(a',s'')>>nil)")] exI 1);
|
|
54 |
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
|
|
55 |
qed"ei_transitions_are_ex";
|
|
56 |
|
|
57 |
|
|
58 |
goal thy
|
|
59 |
"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
|
|
60 |
\ (~a2:ext A) & (~a3:ext A) ==> \
|
|
61 |
\ ? ex. move A ex s1 a1 s4";
|
|
62 |
|
|
63 |
by (res_inst_tac [("x","(s1,(a1,s2)>>(a2,s3)>>(a3,s4)>>nil)")] exI 1);
|
|
64 |
by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
|
|
65 |
qed"eii_transitions_are_ex";
|
|
66 |
|
|
67 |
|
|
68 |
(* ---------------------------------------------------------------------------- *)
|
|
69 |
|
|
70 |
section "weak_ref_map and ref_map";
|
|
71 |
|
|
72 |
|
|
73 |
goalw thy [is_weak_ref_map_def,is_ref_map_def]
|
|
74 |
"!!f. [| ext C = ext A; \
|
|
75 |
\ is_weak_ref_map f C A |] ==> is_ref_map f C A";
|
|
76 |
by (safe_tac set_cs);
|
|
77 |
by (case_tac "a:ext A" 1);
|
|
78 |
by (rtac transition_is_ex 1);
|
|
79 |
by (Asm_simp_tac 1);
|
|
80 |
by (rtac nothing_is_ex 1);
|
|
81 |
by (Asm_simp_tac 1);
|
|
82 |
qed"weak_ref_map2ref_map";
|
|
83 |
|
|
84 |
|
|
85 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
|
|
86 |
by(fast_tac (!claset addDs prems) 1);
|
|
87 |
qed "imp_conj_lemma";
|
|
88 |
|
|
89 |
goal thy "!!f.[| is_weak_ref_map f C A |]\
|
|
90 |
\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
|
|
91 |
by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
|
|
92 |
by (rtac conjI 1);
|
|
93 |
(* 1: start states *)
|
|
94 |
by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
|
|
95 |
(* 2: reachable transitions *)
|
|
96 |
by (REPEAT (rtac allI 1));
|
|
97 |
by (rtac imp_conj_lemma 1);
|
|
98 |
by (simp_tac (!simpset addsimps [rename_def]) 1);
|
|
99 |
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
|
|
100 |
asig_outputs_def,asig_of_def,trans_of_def]) 1);
|
|
101 |
by (safe_tac (!claset));
|
|
102 |
by (rtac (expand_if RS ssubst) 1);
|
|
103 |
by (rtac conjI 1);
|
|
104 |
by (rtac impI 1);
|
|
105 |
by (etac disjE 1);
|
|
106 |
by (etac exE 1);
|
|
107 |
by (etac conjE 1);
|
|
108 |
(* x is input *)
|
|
109 |
by (dtac sym 1);
|
|
110 |
by (dtac sym 1);
|
|
111 |
by (Asm_full_simp_tac 1);
|
|
112 |
by (REPEAT (hyp_subst_tac 1));
|
|
113 |
by (forward_tac [reachable_rename] 1);
|
|
114 |
by (Asm_full_simp_tac 1);
|
|
115 |
(* x is output *)
|
|
116 |
by (etac exE 1);
|
|
117 |
by (etac conjE 1);
|
|
118 |
by (dtac sym 1);
|
|
119 |
by (dtac sym 1);
|
|
120 |
by (Asm_full_simp_tac 1);
|
|
121 |
by (REPEAT (hyp_subst_tac 1));
|
|
122 |
by (forward_tac [reachable_rename] 1);
|
|
123 |
by (Asm_full_simp_tac 1);
|
|
124 |
(* x is internal *)
|
|
125 |
by (simp_tac (!simpset addcongs [conj_cong]) 1);
|
|
126 |
by (rtac impI 1);
|
|
127 |
by (etac conjE 1);
|
|
128 |
by (forward_tac [reachable_rename] 1);
|
|
129 |
by (Auto_tac());
|
|
130 |
qed"rename_through_pmap";
|
|
131 |
|
|
132 |
|