1 (* Title: HOL/BCV/JVM.thy |
1 (* Title: HOL/MicroJava/BV/JVM.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Gerwin Klein |
3 Author: Gerwin Klein |
4 Copyright 2000 TUM |
4 Copyright 2000 TUM |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header "JVM Type System" |
8 header "The JVM Type System as Semilattice" |
9 |
9 |
10 theory JVMType = Opt + Product + Listn + JType: |
10 theory JVMType = Opt + Product + Listn + JType: |
11 |
11 |
12 types |
12 types |
13 locvars_type = "ty err list" |
13 locvars_type = "ty err list" |
14 opstack_type = "ty list" |
14 opstack_type = "ty list" |
15 state_type = "opstack_type \<times> locvars_type" |
15 state_type = "opstack_type \<times> locvars_type" |
16 state = "state_type option err" (* for Kildall *) |
16 state = "state_type option err" -- "for Kildall" |
17 method_type = "state_type option list" (* for BVSpec *) |
17 method_type = "state_type option list" -- "for BVSpec" |
18 class_type = "sig => method_type" |
18 class_type = "sig => method_type" |
19 prog_type = "cname => class_type" |
19 prog_type = "cname => class_type" |
20 |
20 |
21 |
21 |
22 constdefs |
22 constdefs |
48 |
48 |
49 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
49 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
50 ("_ |- _ <=l _" [71,71] 70) |
50 ("_ |- _ <=l _" [71,71] 70) |
51 "sup_loc G == Listn.le (sup_ty_opt G)" |
51 "sup_loc G == Listn.le (sup_ty_opt G)" |
52 |
52 |
53 sup_state :: "['code prog,state_type,state_type] => bool" |
53 sup_state :: "['code prog,state_type,state_type] => bool" |
54 ("_ |- _ <=s _" [71,71] 70) |
54 ("_ |- _ <=s _" [71,71] 70) |
55 "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)" |
55 "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)" |
56 |
56 |
57 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
57 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
58 ("_ |- _ <=' _" [71,71] 70) |
58 ("_ |- _ <=' _" [71,71] 70) |
62 syntax (xsymbols) |
62 syntax (xsymbols) |
63 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
63 sup_ty_opt :: "['code prog,ty err,ty err] => bool" |
64 ("_ \<turnstile> _ <=o _" [71,71] 70) |
64 ("_ \<turnstile> _ <=o _" [71,71] 70) |
65 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
65 sup_loc :: "['code prog,locvars_type,locvars_type] => bool" |
66 ("_ \<turnstile> _ <=l _" [71,71] 70) |
66 ("_ \<turnstile> _ <=l _" [71,71] 70) |
67 sup_state :: "['code prog,state_type,state_type] => bool" |
67 sup_state :: "['code prog,state_type,state_type] => bool" |
68 ("_ \<turnstile> _ <=s _" [71,71] 70) |
68 ("_ \<turnstile> _ <=s _" [71,71] 70) |
69 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
69 sup_state_opt :: "['code prog,state_type option,state_type option] => bool" |
70 ("_ \<turnstile> _ <=' _" [71,71] 70) |
70 ("_ \<turnstile> _ <=' _" [71,71] 70) |
71 |
71 |
72 |
72 |
96 "le G m n = Err.le (sup_state_opt G)" |
96 "le G m n = Err.le (sup_state_opt G)" |
97 by (unfold sup_state_opt_def sup_state_def sup_loc_def |
97 by (unfold sup_state_opt_def sup_state_def sup_loc_def |
98 sup_ty_opt_def JVM_le_unfold) simp |
98 sup_ty_opt_def JVM_le_unfold) simp |
99 |
99 |
100 lemma zip_map [rule_format]: |
100 lemma zip_map [rule_format]: |
101 "\<forall>a. length a = length b --> zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)" |
101 "\<forall>a. length a = length b --> |
|
102 zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)" |
102 apply (induct b) |
103 apply (induct b) |
103 apply simp |
104 apply simp |
104 apply clarsimp |
105 apply clarsimp |
105 apply (case_tac aa) |
106 apply (case_tac aa) |
106 apply simp+ |
107 apply simp+ |
146 done |
147 done |
147 qed |
148 qed |
148 |
149 |
149 |
150 |
150 lemma sup_state_conv: |
151 lemma sup_state_conv: |
151 "(G \<turnstile> s1 <=s s2) == (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)" |
152 "(G \<turnstile> s1 <=s s2) == |
|
153 (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)" |
152 by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta) |
154 by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta) |
153 |
155 |
154 |
156 |
155 lemma subtype_refl [simp]: |
157 lemma subtype_refl [simp]: |
156 "subtype G t t" |
158 "subtype G t t" |