equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/BV/JVM.thy |
1 (* Title: HOL/MicroJava/BV/JVM.thy |
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Gerwin Klein |
2 Author: Tobias Nipkow, Gerwin Klein |
4 Copyright 2000 TUM |
3 Copyright 2000 TUM |
5 *) |
4 *) |
6 |
5 |
7 header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *} |
6 header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *} |
35 (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" |
34 (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" |
36 apply (unfold kiljvm_def sl_triple_conv) |
35 apply (unfold kiljvm_def sl_triple_conv) |
37 apply (rule is_bcv_kildall) |
36 apply (rule is_bcv_kildall) |
38 apply (simp (no_asm) add: sl_triple_conv [symmetric]) |
37 apply (simp (no_asm) add: sl_triple_conv [symmetric]) |
39 apply (force intro!: semilat_JVM_slI dest: wf_acyclic |
38 apply (force intro!: semilat_JVM_slI dest: wf_acyclic |
40 simp add: symmetric sl_triple_conv) |
39 simp add: symmetric sl_triple_conv) |
41 apply (simp (no_asm) add: JVM_le_unfold) |
40 apply (simp (no_asm) add: JVM_le_unfold) |
42 apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype |
41 apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype |
43 dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog) |
42 dest: wf_subcls1 wfP_acyclicP wf_prog_ws_prog) |
44 apply (simp add: JVM_le_unfold) |
43 apply (simp add: JVM_le_unfold) |
45 apply (erule exec_pres_type) |
44 apply (erule exec_pres_type) |