author | wenzelm |
Sun, 02 Nov 2014 17:58:35 +0100 | |
changeset 58886 | 8a6cac7c7247 |
parent 35416 | d8d7d1b785af |
child 61361 | 8b5f00202e1a |
permissions | -rw-r--r-- |
14045 | 1 |
(* Title: HOL/MicroJava/BV/Altern.thy |
2 |
Author: Martin Strecker |
|
3 |
*) |
|
4 |
||
58886 | 5 |
section {* 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 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
11 |
definition check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool" where |
13672 | 12 |
"check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr" |
13 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
14 |
definition wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count, |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
15 |
exception_table,p_count] \<Rightarrow> bool" where |
13672 | 16 |
"wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv> |
17 |
app i G mxs rT pc et (phi!pc) \<and> |
|
18 |
check_type G mxs mxr (OK (phi!pc)) \<and> |
|
19 |
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')" |
|
20 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
21 |
definition wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list, |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
22 |
exception_table,method_type] \<Rightarrow> bool" where |
13672 | 23 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv> |
24 |
let max_pc = length ins in |
|
25 |
0 < max_pc \<and> |
|
26 |
length phi = length ins \<and> |
|
27 |
check_bounded ins et \<and> |
|
28 |
wt_start G C pTs mxl phi \<and> |
|
29 |
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)" |
|
30 |
||
31 |
||
32 |
lemma wt_method_wt_method_altern : |
|
33 |
"wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi" |
|
34 |
apply (simp add: wt_method_def wt_method_altern_def) |
|
35 |
apply (intro strip) |
|
36 |
apply clarify |
|
37 |
apply (drule spec, drule mp, assumption) |
|
38 |
apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def) |
|
39 |
apply (auto intro: imageI) |
|
40 |
done |
|
41 |
||
42 |
||
43 |
lemma check_type_check_types [rule_format]: |
|
44 |
"(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc))) |
|
45 |
\<longrightarrow> check_types G mxs mxr (map OK phi)" |
|
46 |
apply (induct phi) |
|
47 |
apply (simp add: check_types_def) |
|
48 |
apply (simp add: check_types_def) |
|
49 |
apply clarify |
|
50 |
apply (frule_tac x=0 in spec) |
|
51 |
apply (simp add: check_type_def) |
|
52 |
apply auto |
|
53 |
done |
|
54 |
||
55 |
lemma wt_method_altern_wt_method [rule_format]: |
|
56 |
"wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi" |
|
57 |
apply (simp add: wt_method_def wt_method_altern_def) |
|
58 |
apply (intro strip) |
|
59 |
apply clarify |
|
60 |
apply (rule conjI) |
|
61 |
(* show check_types *) |
|
62 |
apply (rule check_type_check_types) |
|
63 |
apply (simp add: wt_instr_altern_def) |
|
64 |
||
65 |
(* show wt_instr *) |
|
66 |
apply (intro strip) |
|
67 |
apply (drule spec, drule mp, assumption) |
|
68 |
apply (simp add: wt_instr_def wt_instr_altern_def) |
|
69 |
done |
|
70 |
||
71 |
||
72 |
end |