equal
deleted
inserted
replaced
3 Author: Martin Strecker |
3 Author: Martin Strecker |
4 *) |
4 *) |
5 |
5 |
6 (* Lemmas for compiler correctness proof *) |
6 (* Lemmas for compiler correctness proof *) |
7 |
7 |
8 theory LemmasComp imports TranslComp begin |
8 theory LemmasComp |
|
9 imports TranslComp |
|
10 begin |
9 |
11 |
10 |
12 |
11 declare split_paired_All [simp del] |
13 declare split_paired_All [simp del] |
12 declare split_paired_Ex [simp del] |
14 declare split_paired_Ex [simp del] |
13 |
15 |
220 fields (comp G,C) = fields (G,C)" |
222 fields (comp G,C) = fields (G,C)" |
221 by (simp add: fields_def comp_class_rec) |
223 by (simp add: fields_def comp_class_rec) |
222 |
224 |
223 lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow> |
225 lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow> |
224 field (comp G,C) = field (G,C)" |
226 field (comp G,C) = field (G,C)" |
225 by (simp add: field_def comp_fields) |
227 by (simp add: TypeRel.field_def comp_fields) |
226 |
228 |
227 |
229 |
228 |
230 |
229 lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk> ws_prog G; |
231 lemma class_rec_relation [rule_format (no_asm)]: "\<lbrakk> ws_prog G; |
230 \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2); |
232 \<forall> fs ms. R (f1 Object fs ms t1) (f2 Object fs ms t2); |