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