7 |
7 |
8 theory JType |
8 theory JType |
9 imports "../DFA/Semilattices" "../J/WellForm" |
9 imports "../DFA/Semilattices" "../J/WellForm" |
10 begin |
10 begin |
11 |
11 |
12 constdefs |
12 definition super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname" where |
13 super :: "'a prog \<Rightarrow> cname \<Rightarrow> cname" |
|
14 "super G C == fst (the (class G C))" |
13 "super G C == fst (the (class G C))" |
15 |
14 |
16 lemma superI: |
15 lemma superI: |
17 "G \<turnstile> C \<prec>C1 D \<Longrightarrow> super G C = D" |
16 "G \<turnstile> C \<prec>C1 D \<Longrightarrow> super G C = D" |
18 by (unfold super_def) (auto dest: subcls1D) |
17 by (unfold super_def) (auto dest: subcls1D) |
19 |
18 |
20 constdefs |
19 definition is_ref :: "ty \<Rightarrow> bool" where |
21 is_ref :: "ty \<Rightarrow> bool" |
|
22 "is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True" |
20 "is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True" |
23 |
21 |
24 sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err" |
22 definition sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err" where |
25 "sup G T1 T2 == |
23 "sup G T1 T2 == |
26 case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow> |
24 case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow> |
27 (if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err) |
25 (if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err) |
28 | RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow> |
26 | RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow> |
29 (case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C)) |
27 (case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C)) |
30 | ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C) |
28 | ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C) |
31 | ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))" |
29 | ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))" |
32 |
30 |
33 subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" |
31 definition subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" where |
34 "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2" |
32 "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2" |
35 |
33 |
36 is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool" |
34 definition is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool" where |
37 "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow> |
35 "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow> |
38 (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)" |
36 (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C, Object) \<in> (subcls1 G)^*)" |
39 |
37 |
40 abbreviation "types G == Collect (is_type G)" |
38 abbreviation "types G == Collect (is_type G)" |
41 |
39 |
42 constdefs |
40 definition esl :: "'c prog \<Rightarrow> ty esl" where |
43 esl :: "'c prog \<Rightarrow> ty esl" |
|
44 "esl G == (types G, subtype G, sup G)" |
41 "esl G == (types G, subtype G, sup G)" |
45 |
42 |
46 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)" |
43 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)" |
47 by (auto elim: widen.cases) |
44 by (auto elim: widen.cases) |
48 |
45 |