171 apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
171 apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
172 apply (simp (no_asm)) |
172 apply (simp (no_asm)) |
173 done |
173 done |
174 |
174 |
175 lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R" |
175 lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R" |
176 apply (auto dest!: tranclD' subcls1D) |
176 apply (auto dest!: tranclpD subcls1D) |
177 done |
177 done |
178 |
178 |
179 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" |
179 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" |
180 apply (erule rtrancl_induct') |
180 apply (erule rtranclp_induct) |
181 apply auto |
181 apply auto |
182 apply (drule subcls1D) |
182 apply (drule subcls1D) |
183 apply auto |
183 apply auto |
184 done |
184 done |
185 |
185 |
186 lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R" |
186 lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R" |
187 apply (auto dest!: tranclD' subcls1D) |
187 apply (auto dest!: tranclpD subcls1D) |
188 done |
188 done |
189 |
189 |
190 lemma class_tprgD: |
190 lemma class_tprgD: |
191 "class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory" |
191 "class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory" |
192 apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
192 apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
193 apply (auto split add: split_if_asm simp add: map_of_Cons) |
193 apply (auto split add: split_if_asm simp add: map_of_Cons) |
194 done |
194 done |
195 |
195 |
196 lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R" |
196 lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R" |
197 apply (auto dest!: tranclD' subcls1D) |
197 apply (auto dest!: tranclpD subcls1D) |
198 apply (frule class_tprgD) |
198 apply (frule class_tprgD) |
199 apply (auto dest!:) |
199 apply (auto dest!:) |
200 apply (drule rtranclD') |
200 apply (drule rtranclpD) |
201 apply auto |
201 apply auto |
202 done |
202 done |
203 |
203 |
204 lemma unique_classes: "unique tprg" |
204 lemma unique_classes: "unique tprg" |
205 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def) |
205 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def) |
206 done |
206 done |
207 |
207 |
208 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl' [where r="subcls1 G"], standard] |
208 lemmas subcls_direct = subcls1I [THEN r_into_rtranclp [where r="subcls1 G"], standard] |
209 |
209 |
210 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base" |
210 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base" |
211 apply (rule subcls_direct) |
211 apply (rule subcls_direct) |
212 apply auto |
212 apply auto |
213 done |
213 done |
343 wf_mrT_def wf_fdecl_def ExtC_def) |
343 wf_mrT_def wf_fdecl_def ExtC_def) |
344 apply (simp (no_asm)) |
344 apply (simp (no_asm)) |
345 apply (fold ExtC_def) |
345 apply (fold ExtC_def) |
346 apply (rule mp) defer apply (rule wf_foo_Ext) |
346 apply (rule mp) defer apply (rule wf_foo_Ext) |
347 apply (auto simp add: wf_mdecl_def) |
347 apply (auto simp add: wf_mdecl_def) |
348 apply (drule rtranclD') |
348 apply (drule rtranclpD) |
349 apply auto |
349 apply auto |
350 done |
350 done |
351 |
351 |
352 |
352 |
353 lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |
353 lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |