| author | haftmann |
| Sun, 31 Jan 2010 14:51:32 +0100 | |
| changeset 34977 | 27ceb64d41ea |
| parent 33954 | 1bc3b688548c |
| child 35416 | d8d7d1b785af |
| permissions | -rwxr-xr-x |
| 14045 | 1 |
(* Title: HOL/MicroJava/BV/Altern.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
26450
diff
changeset
|
5 |
header {* Alternative definition of well-typing of bytecode, used in compiler type correctness proof *}
|
| 14045 | 6 |
|
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
26450
diff
changeset
|
7 |
theory Altern |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
26450
diff
changeset
|
8 |
imports BVSpec |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
26450
diff
changeset
|
9 |
begin |
| 13672 | 10 |
|
11 |
constdefs |
|
| 26450 | 12 |
check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool" |
| 13672 | 13 |
"check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr" |
14 |
||
15 |
wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count, |
|
16 |
exception_table,p_count] \<Rightarrow> bool" |
|
17 |
"wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv> |
|
18 |
app i G mxs rT pc et (phi!pc) \<and> |
|
19 |
check_type G mxs mxr (OK (phi!pc)) \<and> |
|
20 |
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')" |
|
21 |
||
22 |
wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, |
|
23 |
exception_table,method_type] \<Rightarrow> bool" |
|
24 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv> |
|
25 |
let max_pc = length ins in |
|
26 |
0 < max_pc \<and> |
|
27 |
length phi = length ins \<and> |
|
28 |
check_bounded ins et \<and> |
|
29 |
wt_start G C pTs mxl phi \<and> |
|
30 |
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)" |
|
31 |
||
32 |
||
33 |
lemma wt_method_wt_method_altern : |
|
34 |
"wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi" |
|
35 |
apply (simp add: wt_method_def wt_method_altern_def) |
|
36 |
apply (intro strip) |
|
37 |
apply clarify |
|
38 |
apply (drule spec, drule mp, assumption) |
|
39 |
apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def) |
|
40 |
apply (auto intro: imageI) |
|
41 |
done |
|
42 |
||
43 |
||
44 |
lemma check_type_check_types [rule_format]: |
|
45 |
"(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc))) |
|
46 |
\<longrightarrow> check_types G mxs mxr (map OK phi)" |
|
47 |
apply (induct phi) |
|
48 |
apply (simp add: check_types_def) |
|
49 |
apply (simp add: check_types_def) |
|
50 |
apply clarify |
|
51 |
apply (frule_tac x=0 in spec) |
|
52 |
apply (simp add: check_type_def) |
|
53 |
apply auto |
|
54 |
done |
|
55 |
||
56 |
lemma wt_method_altern_wt_method [rule_format]: |
|
57 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi" |
|
58 |
apply (simp add: wt_method_def wt_method_altern_def) |
|
59 |
apply (intro strip) |
|
60 |
apply clarify |
|
61 |
apply (rule conjI) |
|
62 |
(* show check_types *) |
|
63 |
apply (rule check_type_check_types) |
|
64 |
apply (simp add: wt_instr_altern_def) |
|
65 |
||
66 |
(* show wt_instr *) |
|
67 |
apply (intro strip) |
|
68 |
apply (drule spec, drule mp, assumption) |
|
69 |
apply (simp add: wt_instr_def wt_instr_altern_def) |
|
70 |
done |
|
71 |
||
72 |
||
73 |
end |