author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 14981 | e73f8140af78 |
child 22271 | 51a80e238b29 |
permissions | -rw-r--r-- |
13673 | 1 |
(* Title: HOL/MicroJava/Comp/LemmasComp.thy |
2 |
ID: $Id$ |
|
3 |
Author: Martin Strecker |
|
4 |
*) |
|
5 |
||
6 |
(* Lemmas for compiler correctness proof *) |
|
7 |
||
16417 | 8 |
theory LemmasComp imports TranslComp begin |
13673 | 9 |
|
14045 | 10 |
|
11 |
declare split_paired_All [simp del] |
|
12 |
declare split_paired_Ex [simp del] |
|
13 |
||
14 |
||
13673 | 15 |
(**********************************************************************) |
16 |
(* misc lemmas *) |
|
17 |
||
14045 | 18 |
|
19 |
||
13673 | 20 |
lemma split_pairs: "(\<lambda>(a,b). (F a b)) (ab) = F (fst ab) (snd ab)" |
21 |
proof - |
|
22 |
have "(\<lambda>(a,b). (F a b)) (fst ab,snd ab) = F (fst ab) (snd ab)" |
|
23 |
by (simp add: split_def) |
|
24 |
then show ?thesis by simp |
|
25 |
qed |
|
26 |
||
27 |
||
28 |
lemma c_hupd_conv: |
|
29 |
"c_hupd h' (xo, (h,l)) = (xo, (if xo = None then h' else h),l)" |
|
30 |
by (simp add: c_hupd_def) |
|
31 |
||
32 |
lemma gl_c_hupd [simp]: "(gl (c_hupd h xs)) = (gl xs)" |
|
33 |
by (simp add: gl_def c_hupd_def split_pairs) |
|
34 |
||
35 |
lemma c_hupd_xcpt_invariant [simp]: "gx (c_hupd h' (xo, st)) = xo" |
|
36 |
by (case_tac st, simp only: c_hupd_conv gx_conv) |
|
37 |
||
38 |
(* not added to simpset because of interference with c_hupd_conv *) |
|
39 |
lemma c_hupd_hp_invariant: "gh (c_hupd hp (None, st)) = hp" |
|
40 |
by (case_tac st, simp add: c_hupd_conv gh_def) |
|
41 |
||
42 |
||
14045 | 43 |
lemma unique_map_fst [rule_format]: "(\<forall> x \<in> set xs. (fst x = fst (f x) )) \<longrightarrow> |
44 |
unique (map f xs) = unique xs" |
|
45 |
proof (induct xs) |
|
46 |
case Nil show ?case by simp |
|
47 |
next |
|
48 |
case (Cons a list) |
|
49 |
show ?case |
|
50 |
proof |
|
51 |
assume fst_eq: "\<forall>x\<in>set (a # list). fst x = fst (f x)" |
|
52 |
||
53 |
have fst_set: "(fst a \<in> fst ` set list) = (fst (f a) \<in> fst ` f ` set list)" |
|
54 |
proof |
|
55 |
assume as: "fst a \<in> fst ` set list" |
|
56 |
then obtain x where fst_a_x: "x\<in>set list \<and> fst a = fst x" |
|
57 |
by (auto simp add: image_iff) |
|
58 |
then have "fst (f a) = fst (f x)" by (simp add: fst_eq) |
|
59 |
with as show "(fst (f a) \<in> fst ` f ` set list)" by (simp add: fst_a_x) |
|
60 |
next |
|
61 |
assume as: "fst (f a) \<in> fst ` f ` set list" |
|
62 |
then obtain x where fst_a_x: "x\<in>set list \<and> fst (f a) = fst (f x)" |
|
63 |
by (auto simp add: image_iff) |
|
64 |
then have "fst a = fst x" by (simp add: fst_eq) |
|
65 |
with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x) |
|
66 |
qed |
|
67 |
||
68 |
with fst_eq Cons |
|
69 |
show "unique (map f (a # list)) = unique (a # list)" |
|
70 |
by (simp add: unique_def fst_set) |
|
71 |
qed |
|
72 |
qed |
|
73 |
||
74 |
lemma comp_unique: "unique (comp G) = unique G" |
|
75 |
apply (simp add: comp_def) |
|
76 |
apply (rule unique_map_fst) |
|
77 |
apply (simp add: compClass_def split_beta) |
|
78 |
done |
|
79 |
||
80 |
||
13673 | 81 |
(**********************************************************************) |
82 |
(* invariance of properties under compilation *) |
|
83 |
||
84 |
lemma comp_class_imp: |
|
85 |
"(class G C = Some(D, fs, ms)) \<Longrightarrow> |
|
86 |
(class (comp G) C = Some(D, fs, map (compMethod G C) ms))" |
|
87 |
apply (simp add: class_def comp_def compClass_def) |
|
88 |
apply (rule HOL.trans) |
|
89 |
apply (rule map_of_map2) |
|
90 |
apply auto |
|
91 |
done |
|
92 |
||
93 |
lemma comp_class_None: |
|
94 |
"(class G C = None) = (class (comp G) C = None)" |
|
95 |
apply (simp add: class_def comp_def compClass_def) |
|
96 |
apply (simp add: map_of_in_set) |
|
97 |
apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose) |
|
98 |
done |
|
99 |
||
14045 | 100 |
lemma comp_is_class: "is_class (comp G) C = is_class G C" |
13673 | 101 |
by (case_tac "class G C", auto simp: is_class_def comp_class_None dest: comp_class_imp) |
102 |
||
103 |
||
14045 | 104 |
lemma comp_is_type: "is_type (comp G) T = is_type G T" |
13673 | 105 |
by ((cases T),simp,(induct G)) ((simp),(simp only: comp_is_class),(simp add: comp_is_class),(simp only: comp_is_class)) |
106 |
||
14045 | 107 |
lemma comp_classname: "is_class G C |
108 |
\<Longrightarrow> fst (the (class G C)) = fst (the (class (comp G) C))" |
|
13673 | 109 |
by (case_tac "class G C", auto simp: is_class_def dest: comp_class_imp) |
110 |
||
14045 | 111 |
lemma comp_subcls1: "subcls1 (comp G) = subcls1 G" |
14952
47455995693d
removal of x-symbol syntax <Sigma> for dependent products
paulson
parents:
14045
diff
changeset
|
112 |
by (auto simp add: subcls1_def2 comp_classname comp_is_class) |
13673 | 113 |
|
14045 | 114 |
lemma comp_widen: "((ty1,ty2) \<in> widen (comp G)) = ((ty1,ty2) \<in> widen G)" |
13673 | 115 |
apply rule |
14045 | 116 |
apply (cases "(ty1,ty2)" "comp G" rule: widen.cases) |
117 |
apply (simp_all add: comp_subcls1 widen.null) |
|
13673 | 118 |
apply (cases "(ty1,ty2)" G rule: widen.cases) |
14045 | 119 |
apply (simp_all add: comp_subcls1 widen.null) |
13673 | 120 |
done |
121 |
||
14045 | 122 |
lemma comp_cast: "((ty1,ty2) \<in> cast (comp G)) = ((ty1,ty2) \<in> cast G)" |
13673 | 123 |
apply rule |
14045 | 124 |
apply (cases "(ty1,ty2)" "comp G" rule: cast.cases) |
125 |
apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
|
126 |
apply (rule cast.widen) apply (simp add: comp_widen) |
|
13673 | 127 |
apply (cases "(ty1,ty2)" G rule: cast.cases) |
14045 | 128 |
apply (simp_all add: comp_subcls1 cast.widen cast.subcls) |
129 |
apply (rule cast.widen) apply (simp add: comp_widen) |
|
13673 | 130 |
done |
131 |
||
14045 | 132 |
lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G" |
13673 | 133 |
by (simp add: expand_fun_eq cast_ok_def comp_widen) |
134 |
||
135 |
||
14045 | 136 |
lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)" |
137 |
by (simp add: compClass_def split_beta) |
|
138 |
||
139 |
lemma compClass_fst_snd [simp]: "(fst (snd (compClass G C))) = (fst (snd C))" |
|
140 |
by (simp add: compClass_def split_beta) |
|
141 |
||
142 |
lemma compClass_fst_snd_snd [simp]: "(fst (snd (snd (compClass G C)))) = (fst (snd (snd C)))" |
|
143 |
by (simp add: compClass_def split_beta) |
|
144 |
||
145 |
lemma comp_wf_fdecl [simp]: "wf_fdecl (comp G) fd = wf_fdecl G fd" |
|
146 |
by (case_tac fd, simp add: wf_fdecl_def comp_is_type) |
|
147 |
||
148 |
||
149 |
lemma compClass_forall [simp]: " |
|
150 |
(\<forall>x\<in>set (snd (snd (snd (compClass G C)))). P (fst x) (fst (snd x))) = |
|
151 |
(\<forall>x\<in>set (snd (snd (snd C))). P (fst x) (fst (snd x)))" |
|
152 |
by (simp add: compClass_def compMethod_def split_beta) |
|
153 |
||
154 |
lemma comp_wf_mhead: "wf_mhead (comp G) S rT = wf_mhead G S rT" |
|
155 |
by (simp add: wf_mhead_def split_beta comp_is_type) |
|
156 |
||
157 |
lemma comp_ws_cdecl: " |
|
158 |
ws_cdecl (TranslComp.comp G) (compClass G C) = ws_cdecl G C" |
|
159 |
apply (simp add: ws_cdecl_def split_beta comp_is_class comp_subcls1) |
|
160 |
apply (simp (no_asm_simp) add: comp_wf_mhead) |
|
161 |
apply (simp add: compClass_def compMethod_def split_beta unique_map_fst) |
|
13673 | 162 |
done |
163 |
||
14045 | 164 |
|
165 |
lemma comp_wf_syscls: "wf_syscls (comp G) = wf_syscls G" |
|
13673 | 166 |
apply (simp add: wf_syscls_def comp_def compClass_def split_beta) |
167 |
apply (simp only: image_compose [THEN sym]) |
|
14045 | 168 |
apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls). |
169 |
(C, cno, fdls, map (compMethod G C) jmdls))) = fst") |
|
13673 | 170 |
apply (simp del: image_compose) |
171 |
apply (simp add: expand_fun_eq split_beta) |
|
172 |
done |
|
173 |
||
174 |
||
14045 | 175 |
lemma comp_ws_prog: "ws_prog (comp G) = ws_prog G" |
176 |
apply (rule sym) |
|
177 |
apply (simp add: ws_prog_def comp_ws_cdecl comp_unique) |
|
178 |
apply (simp add: comp_wf_syscls) |
|
179 |
apply (auto simp add: comp_ws_cdecl [THEN sym] TranslComp.comp_def) |
|
180 |
done |
|
13673 | 181 |
|
182 |
||
183 |
lemma comp_class_rec: " wf ((subcls1 G)^-1) \<Longrightarrow> |
|
184 |
class_rec (comp G) C t f = |
|
185 |
class_rec G C t (\<lambda> C' fs' ms' r'. f C' fs' (map (compMethod G C') ms') r')" |
|
186 |
apply (rule_tac a = C in wf_induct) apply assumption |
|
187 |
apply (subgoal_tac "wf ((subcls1 (comp G))\<inverse>)") |
|
188 |
apply (subgoal_tac "(class G x = None) \<or> (\<exists> D fs ms. (class G x = Some (D, fs, ms)))") |
|
189 |
apply (erule disjE) |
|
190 |
||
191 |
(* case class G x = None *) |
|
192 |
apply (simp (no_asm_simp) add: class_rec_def comp_subcls1 wfrec cut_apply) |
|
193 |
apply (simp add: comp_class_None) |
|
194 |
||
195 |
(* case \<exists> D fs ms. (class G x = Some (D, fs, ms)) *) |
|
196 |
apply (erule exE)+ |
|
197 |
apply (frule comp_class_imp) |
|
198 |
apply (frule_tac G="comp G" and C=x and t=t and f=f in class_rec_lemma) |
|
199 |
apply assumption |
|
200 |
apply (frule_tac G=G and C=x and t=t |
|
201 |
and f="(\<lambda>C' fs' ms'. f C' fs' (map (compMethod G C') ms'))" in class_rec_lemma) |
|
202 |
apply assumption |
|
203 |
apply (simp only:) |
|
204 |
||
205 |
apply (case_tac "x = Object") |
|
206 |
apply simp |
|
207 |
apply (frule subcls1I, assumption) |
|
208 |
apply (drule_tac x=D in spec, drule mp, simp) |
|
209 |
apply simp |
|
210 |
||
211 |
(* subgoals *) |
|
212 |
apply (case_tac "class G x") |
|
213 |
apply auto |
|
214 |
apply (simp add: comp_subcls1) |
|
215 |
done |
|
216 |
||
217 |
lemma comp_fields: "wf ((subcls1 G)^-1) \<Longrightarrow> |
|
14045 | 218 |
fields (comp G,C) = fields (G,C)" |
13673 | 219 |
by (simp add: fields_def comp_class_rec) |
220 |
||
221 |
lemma comp_field: "wf ((subcls1 G)^-1) \<Longrightarrow> |
|
14045 | 222 |
field (comp G,C) = field (G,C)" |
13673 | 223 |
by (simp add: field_def comp_fields) |
224 |
||
225 |
||
226 |
||
14045 | 227 |
lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk> ws_prog G; |
13673 | 228 |
\<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2); |
229 |
\<forall> C fs ms r1 r2. (R r1 r2) \<longrightarrow> (R (f1 C fs ms r1) (f2 C fs ms r2)) \<rbrakk> |
|
230 |
\<Longrightarrow> ((class G C) \<noteq> None) \<longrightarrow> |
|
231 |
R (class_rec G C t1 f1) (class_rec G C t2 f2)" |
|
232 |
apply (frule wf_subcls1) (* establish wf ((subcls1 G)^-1) *) |
|
233 |
apply (rule_tac a = C in wf_induct) apply assumption |
|
234 |
apply (intro strip) |
|
235 |
apply (subgoal_tac "(\<exists>D rT mb. class G x = Some (D, rT, mb))") |
|
236 |
apply (erule exE)+ |
|
237 |
apply (frule_tac C=x and t=t1 and f=f1 in class_rec_lemma) |
|
238 |
apply assumption |
|
239 |
apply (frule_tac C=x and t=t2 and f=f2 in class_rec_lemma) |
|
240 |
apply assumption |
|
241 |
apply (simp only:) |
|
242 |
||
243 |
apply (case_tac "x = Object") |
|
244 |
apply simp |
|
245 |
apply (frule subcls1I, assumption) |
|
246 |
apply (drule_tac x=D in spec, drule mp, simp) |
|
247 |
apply simp |
|
248 |
apply (subgoal_tac "(\<exists>D' rT' mb'. class G D = Some (D', rT', mb'))") |
|
249 |
apply blast |
|
250 |
||
251 |
(* subgoals *) |
|
252 |
||
14045 | 253 |
apply (frule class_wf_struct) apply assumption |
254 |
apply (simp add: ws_cdecl_def is_class_def) |
|
13673 | 255 |
|
256 |
apply (simp add: subcls1_def2 is_class_def) |
|
14045 | 257 |
apply auto |
13673 | 258 |
done |
259 |
||
260 |
||
261 |
syntax |
|
262 |
mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c" |
|
263 |
translations |
|
264 |
"mtd_mb" => "Fun.comp snd snd" |
|
265 |
||
14045 | 266 |
lemma map_of_map_fst: "\<lbrakk> inj f; |
13673 | 267 |
\<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk> |
14045 | 268 |
\<Longrightarrow> map_of (map g xs) k |
269 |
= option_map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)" |
|
13673 | 270 |
apply (induct xs) |
271 |
apply simp |
|
272 |
apply (simp del: split_paired_All) |
|
273 |
apply (case_tac "k = fst a") |
|
274 |
apply (simp del: split_paired_All) |
|
14045 | 275 |
apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp) |
276 |
apply (subgoal_tac "(fst a, snd (f a)) = f a", simp) |
|
277 |
apply (erule conjE)+ |
|
278 |
apply (drule_tac s ="fst (f a)" and t="fst a" in sym) |
|
13673 | 279 |
apply simp |
14045 | 280 |
apply (simp add: surjective_pairing) |
13673 | 281 |
done |
282 |
||
283 |
||
14045 | 284 |
lemma comp_method [rule_format (no_asm)]: "\<lbrakk> ws_prog G; is_class G C\<rbrakk> \<Longrightarrow> |
285 |
((method (comp G, C) S) = |
|
286 |
option_map (\<lambda> (D,rT,b). (D, rT, mtd_mb (compMethod G D (S, rT, b)))) |
|
287 |
(method (G, C) S))" |
|
13673 | 288 |
apply (simp add: method_def) |
289 |
apply (frule wf_subcls1) |
|
290 |
apply (simp add: comp_class_rec) |
|
291 |
apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose) |
|
14045 | 292 |
apply (rule_tac R="%x y. ((x S) = (option_map (\<lambda>(D, rT, b). |
293 |
(D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" |
|
294 |
in class_rec_relation) |
|
295 |
apply assumption |
|
13673 | 296 |
|
297 |
apply (intro strip) |
|
298 |
apply simp |
|
299 |
||
14045 | 300 |
apply (rule trans) |
301 |
||
302 |
apply (rule_tac f="(\<lambda>(s, m). (s, Object, m))" and |
|
303 |
g="(Fun.comp (\<lambda>(s, m). (s, Object, m)) (compMethod G Object))" |
|
304 |
in map_of_map_fst) |
|
305 |
defer (* inj \<dots> *) |
|
306 |
apply (simp add: inj_on_def split_beta) |
|
13673 | 307 |
apply (simp add: split_beta compMethod_def) |
14045 | 308 |
apply (simp add: map_of_map [THEN sym]) |
309 |
apply (simp add: split_beta) |
|
310 |
apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta) |
|
311 |
apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl. |
|
312 |
(fst x, Object, |
|
313 |
snd (compMethod G Object |
|
314 |
(inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr). |
|
315 |
(s, Object, m)) |
|
316 |
(S, Object, snd x))))) |
|
317 |
= (\<lambda>x. (fst x, Object, fst (snd x), |
|
318 |
snd (snd (compMethod G Object (S, snd x)))))") |
|
13673 | 319 |
apply (simp only:) |
14045 | 320 |
apply (simp add: expand_fun_eq) |
321 |
apply (intro strip) |
|
322 |
apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)") |
|
13673 | 323 |
apply (simp only:) |
324 |
apply (simp add: compMethod_def split_beta) |
|
14045 | 325 |
apply (rule inv_f_eq) |
326 |
defer |
|
327 |
defer |
|
13673 | 328 |
|
329 |
apply (intro strip) |
|
14025 | 330 |
apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex) |
14045 | 331 |
apply (simp add: map_add_def) |
332 |
apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))") |
|
333 |
apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms |
|
334 |
and k=S in map_of_map_fst) |
|
335 |
apply (simp add: split_beta) |
|
336 |
apply (simp add: compMethod_def split_beta) |
|
337 |
apply (case_tac "(map_of (map (\<lambda>(s, m). (s, Ca, m)) ms) S)") |
|
338 |
apply simp |
|
339 |
apply simp apply (simp add: split_beta map_of_map) apply (erule exE) apply (erule conjE)+ |
|
340 |
apply (drule_tac t=a in sym) |
|
341 |
apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Ca, m)) (S, a)) = (S, snd a)") |
|
342 |
apply simp |
|
13673 | 343 |
apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x") |
14045 | 344 |
prefer 2 apply (simp (no_asm_simp) add: compMethod_def split_beta) |
13673 | 345 |
apply (simp add: map_of_map2) |
346 |
apply (simp (no_asm_simp) add: compMethod_def split_beta) |
|
347 |
||
14045 | 348 |
-- "remaining subgoals" |
349 |
apply (auto intro: inv_f_eq simp add: inj_on_def is_class_def) |
|
13673 | 350 |
done |
351 |
||
352 |
||
353 |
||
14045 | 354 |
lemma comp_wf_mrT: "\<lbrakk> ws_prog G; is_class G D\<rbrakk> \<Longrightarrow> |
355 |
wf_mrT (TranslComp.comp G) (C, D, fs, map (compMethod G a) ms) = |
|
356 |
wf_mrT G (C, D, fs, ms)" |
|
357 |
apply (simp add: wf_mrT_def compMethod_def split_beta) |
|
358 |
apply (simp add: comp_widen) |
|
359 |
apply (rule iffI) |
|
13673 | 360 |
apply (intro strip) |
361 |
apply simp |
|
14045 | 362 |
apply (drule bspec) apply assumption |
363 |
apply (drule_tac x=D' in spec) apply (drule_tac x=rT' in spec) apply (drule mp) |
|
364 |
prefer 2 apply assumption |
|
365 |
apply (simp add: comp_method [of G D]) |
|
366 |
apply (erule exE)+ |
|
367 |
apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))") |
|
368 |
apply (rule exI) |
|
369 |
apply (simp) |
|
370 |
apply (simp add: split_paired_all) |
|
371 |
apply (intro strip) |
|
372 |
apply (simp add: comp_method) |
|
373 |
apply auto |
|
13673 | 374 |
done |
375 |
||
376 |
||
377 |
(**********************************************************************) |
|
378 |
(* DIVERSE OTHER LEMMAS *) |
|
379 |
(**********************************************************************) |
|
380 |
||
381 |
lemma max_spec_preserves_length: |
|
382 |
"max_spec G C (mn, pTs) = {((md,rT),pTs')} |
|
383 |
\<Longrightarrow> length pTs = length pTs'" |
|
384 |
apply (frule max_spec2mheads) |
|
385 |
apply (erule exE)+ |
|
386 |
apply (simp add: list_all2_def) |
|
387 |
done |
|
388 |
||
389 |
||
390 |
lemma ty_exprs_length [simp]: "(E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts)" |
|
391 |
apply (subgoal_tac "(E\<turnstile>e::T \<longrightarrow> True) \<and> (E\<turnstile>es[::]Ts \<longrightarrow> length es = length Ts) \<and> (E\<turnstile>s\<surd> \<longrightarrow> True)") |
|
392 |
apply blast |
|
393 |
apply (rule ty_expr_ty_exprs_wt_stmt.induct) |
|
394 |
apply auto |
|
395 |
done |
|
396 |
||
397 |
||
398 |
lemma max_spec_preserves_method_rT [simp]: |
|
399 |
"max_spec G C (mn, pTs) = {((md,rT),pTs')} |
|
400 |
\<Longrightarrow> method_rT (the (method (G, C) (mn, pTs'))) = rT" |
|
401 |
apply (frule max_spec2mheads) |
|
402 |
apply (erule exE)+ |
|
403 |
apply (simp add: method_rT_def) |
|
404 |
done |
|
405 |
||
14045 | 406 |
(**********************************************************************************) |
407 |
||
408 |
declare compClass_fst [simp del] |
|
409 |
declare compClass_fst_snd [simp del] |
|
410 |
declare compClass_fst_snd_snd [simp del] |
|
411 |
||
412 |
declare split_paired_All [simp add] |
|
413 |
declare split_paired_Ex [simp add] |
|
13673 | 414 |
|
415 |
end |