6 |
6 |
7 header {* \isaheader{Relations between Java Types} *} |
7 header {* \isaheader{Relations between Java Types} *} |
8 |
8 |
9 theory TypeRel imports Decl begin |
9 theory TypeRel imports Decl begin |
10 |
10 |
11 consts |
11 -- "direct subclass, cf. 8.1.3" |
12 subcls1 :: "'c prog => (cname \<times> cname) set" -- "subclass" |
12 inductive2 |
13 widen :: "'c prog => (ty \<times> ty ) set" -- "widening" |
|
14 cast :: "'c prog => (ty \<times> ty ) set" -- "casting" |
|
15 |
|
16 syntax (xsymbols) |
|
17 subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) |
13 subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70) |
|
14 for G :: "'c prog" |
|
15 where |
|
16 subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D" |
|
17 |
|
18 abbreviation |
18 subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) |
19 subcls :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70) |
19 widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) |
20 where "G\<turnstile>C \<preceq>C D \<equiv> (subcls1 G)^** C D" |
20 cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) |
|
21 |
|
22 syntax |
|
23 subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70) |
|
24 subcls :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C _" [71,71,71] 70) |
|
25 widen :: "'c prog => [ty , ty ] => bool" ("_ |- _ <= _" [71,71,71] 70) |
|
26 cast :: "'c prog => [ty , ty ] => bool" ("_ |- _ <=? _" [71,71,71] 70) |
|
27 |
|
28 translations |
|
29 "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G" |
|
30 "G\<turnstile>C \<preceq>C D" == "(C,D) \<in> (subcls1 G)^*" |
|
31 "G\<turnstile>S \<preceq> T" == "(S,T) \<in> widen G" |
|
32 "G\<turnstile>C \<preceq>? D" == "(C,D) \<in> cast G" |
|
33 |
|
34 -- "direct subclass, cf. 8.1.3" |
|
35 inductive "subcls1 G" intros |
|
36 subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D" |
|
37 |
21 |
38 lemma subcls1D: |
22 lemma subcls1D: |
39 "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))" |
23 "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))" |
40 apply (erule subcls1.elims) |
24 apply (erule subcls1.cases) |
41 apply auto |
25 apply auto |
42 done |
26 done |
43 |
27 |
44 lemma subcls1_def2: |
28 lemma subcls1_def2: |
45 "subcls1 G = |
29 "subcls1 G = member2 |
46 (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" |
30 (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})" |
47 by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) |
31 by (auto simp add: is_class_def expand_fun_eq dest: subcls1D intro: subcls1I) |
48 |
32 |
49 lemma finite_subcls1: "finite (subcls1 G)" |
33 lemma finite_subcls1: "finite (Collect2 (subcls1 G))" |
50 apply(subst subcls1_def2) |
34 apply(simp add: subcls1_def2) |
51 apply(rule finite_SigmaI [OF finite_is_class]) |
35 apply(rule finite_SigmaI [OF finite_is_class]) |
52 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) |
36 apply(rule_tac B = "{fst (the (class G C))}" in finite_subset) |
53 apply auto |
37 apply auto |
54 done |
38 done |
55 |
39 |
56 lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C" |
40 lemma subcls_is_class: "(subcls1 G)^++ C D ==> is_class G C" |
57 apply (unfold is_class_def) |
41 apply (unfold is_class_def) |
58 apply(erule trancl_trans_induct) |
42 apply(erule trancl_trans_induct') |
59 apply (auto dest!: subcls1D) |
43 apply (auto dest!: subcls1D) |
60 done |
44 done |
61 |
45 |
62 lemma subcls_is_class2 [rule_format (no_asm)]: |
46 lemma subcls_is_class2 [rule_format (no_asm)]: |
63 "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" |
47 "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C" |
64 apply (unfold is_class_def) |
48 apply (unfold is_class_def) |
65 apply (erule rtrancl_induct) |
49 apply (erule rtrancl_induct') |
66 apply (drule_tac [2] subcls1D) |
50 apply (drule_tac [2] subcls1D) |
67 apply auto |
51 apply auto |
68 done |
52 done |
69 |
53 |
70 constdefs |
54 constdefs |
71 class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow> |
55 class_rec :: "'c prog \<Rightarrow> cname \<Rightarrow> 'a \<Rightarrow> |
72 (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" |
56 (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a" |
73 "class_rec G == wfrec ((subcls1 G)^-1) |
57 "class_rec G == wfrec (Collect2 ((subcls1 G)^--1)) |
74 (\<lambda>r C t f. case class G C of |
58 (\<lambda>r C t f. case class G C of |
75 None \<Rightarrow> arbitrary |
59 None \<Rightarrow> arbitrary |
76 | Some (D,fs,ms) \<Rightarrow> |
60 | Some (D,fs,ms) \<Rightarrow> |
77 f C fs ms (if C = Object then t else r D t f))" |
61 f C fs ms (if C = Object then t else r D t f))" |
78 |
62 |
79 lemma class_rec_lemma: "wf ((subcls1 G)^-1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow> |
63 lemma class_rec_lemma: "wfP ((subcls1 G)^--1) \<Longrightarrow> class G C = Some (D,fs,ms) \<Longrightarrow> |
80 class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)" |
64 class_rec G C t f = f C fs ms (if C=Object then t else class_rec G D t f)" |
81 by (simp add: class_rec_def wfrec cut_apply [OF converseI [OF subcls1I]]) |
65 by (simp add: class_rec_def wfrec [to_pred] |
|
66 cut_apply [OF Collect2I [where P="(subcls1 G)^--1"], OF conversepI, OF subcls1I]) |
82 |
67 |
83 definition |
68 definition |
84 "wf_class G = wf ((subcls1 G)^-1)" |
69 "wf_class G = wfP ((subcls1 G)^--1)" |
85 |
70 |
86 lemma class_rec_func [code func]: |
71 lemma class_rec_func [code func]: |
87 "class_rec G C t f = (if wf_class G then |
72 "class_rec G C t f = (if wf_class G then |
88 (case class G C |
73 (case class G C |
89 of None \<Rightarrow> arbitrary |
74 of None \<Rightarrow> arbitrary |
119 |
105 |
120 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" |
106 -- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" |
121 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts. |
107 defs method_def: "method \<equiv> \<lambda>(G,C). class_rec G C empty (\<lambda>C fs ms ts. |
122 ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))" |
108 ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))" |
123 |
109 |
124 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> |
110 lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==> |
125 method (G,C) = (if C = Object then empty else method (G,D)) ++ |
111 method (G,C) = (if C = Object then empty else method (G,D)) ++ |
126 map_of (map (\<lambda>(s,m). (s,(C,m))) ms)" |
112 map_of (map (\<lambda>(s,m). (s,(C,m))) ms)" |
127 apply (unfold method_def) |
113 apply (unfold method_def) |
128 apply (simp split del: split_if) |
114 apply (simp split del: split_if) |
129 apply (erule (1) class_rec_lemma [THEN trans]); |
115 apply (erule (1) class_rec_lemma [THEN trans]); |
133 |
119 |
134 -- "list of fields of a class, including inherited and hidden ones" |
120 -- "list of fields of a class, including inherited and hidden ones" |
135 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts. |
121 defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec G C [] (\<lambda>C fs ms ts. |
136 map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)" |
122 map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)" |
137 |
123 |
138 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==> |
124 lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wfP ((subcls1 G)^--1)|] ==> |
139 fields (G,C) = |
125 fields (G,C) = |
140 map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))" |
126 map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))" |
141 apply (unfold fields_def) |
127 apply (unfold fields_def) |
142 apply (simp split del: split_if) |
128 apply (simp split del: split_if) |
143 apply (erule (1) class_rec_lemma [THEN trans]); |
129 apply (erule (1) class_rec_lemma [THEN trans]); |
154 apply simp |
140 apply simp |
155 done |
141 done |
156 |
142 |
157 |
143 |
158 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping" |
144 -- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping" |
159 inductive "widen G" intros |
145 inductive2 |
|
146 widen :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70) |
|
147 for G :: "'c prog" |
|
148 where |
160 refl [intro!, simp]: "G\<turnstile> T \<preceq> T" -- "identity conv., cf. 5.1.1" |
149 refl [intro!, simp]: "G\<turnstile> T \<preceq> T" -- "identity conv., cf. 5.1.1" |
161 subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D" |
150 | subcls : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D" |
162 null [intro!]: "G\<turnstile> NT \<preceq> RefT R" |
151 | null [intro!]: "G\<turnstile> NT \<preceq> RefT R" |
163 |
152 |
164 -- "casting conversion, cf. 5.5 / 5.1.5" |
153 -- "casting conversion, cf. 5.5 / 5.1.5" |
165 -- "left out casts on primitve types" |
154 -- "left out casts on primitve types" |
166 inductive "cast G" intros |
155 inductive2 |
|
156 cast :: "'c prog => [ty , ty ] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70) |
|
157 for G :: "'c prog" |
|
158 where |
167 widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D" |
159 widen: "G\<turnstile> C\<preceq> D ==> G\<turnstile>C \<preceq>? D" |
168 subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D" |
160 | subcls: "G\<turnstile> D\<preceq>C C ==> G\<turnstile>Class C \<preceq>? Class D" |
169 |
161 |
170 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False" |
162 lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False" |
171 apply (rule iffI) |
163 apply (rule iffI) |
172 apply (erule widen.elims) |
164 apply (erule widen.cases) |
173 apply auto |
165 apply auto |
174 done |
166 done |
175 |
167 |
176 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t" |
168 lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t" |
177 apply (ind_cases "G\<turnstile>S\<preceq>T") |
169 apply (ind_cases2 "G\<turnstile>RefT R\<preceq>T") |
178 apply auto |
170 apply auto |
179 done |
171 done |
180 |
172 |
181 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t" |
173 lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t" |
182 apply (ind_cases "G\<turnstile>S\<preceq>T") |
174 apply (ind_cases2 "G\<turnstile>S\<preceq>RefT R") |
183 apply auto |
175 apply auto |
184 done |
176 done |
185 |
177 |
186 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D" |
178 lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D" |
187 apply (ind_cases "G\<turnstile>S\<preceq>T") |
179 apply (ind_cases2 "G\<turnstile>Class C\<preceq>T") |
188 apply auto |
180 apply auto |
189 done |
181 done |
190 |
182 |
191 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False" |
183 lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False" |
192 apply (rule iffI) |
184 apply (rule iffI) |
193 apply (ind_cases "G\<turnstile>S\<preceq>T") |
185 apply (ind_cases2 "G\<turnstile>Class C\<preceq>NT") |
194 apply auto |
186 apply auto |
195 done |
187 done |
196 |
188 |
197 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)" |
189 lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)" |
198 apply (rule iffI) |
190 apply (rule iffI) |
199 apply (ind_cases "G\<turnstile>S\<preceq>T") |
191 apply (ind_cases2 "G\<turnstile>Class C \<preceq> Class D") |
200 apply (auto elim: widen.subcls) |
192 apply (auto elim: widen.subcls) |
201 done |
193 done |
202 |
194 |
203 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D" |
195 lemma widen_NT_Class [simp]: "G \<turnstile> T \<preceq> NT \<Longrightarrow> G \<turnstile> T \<preceq> Class D" |
204 by (ind_cases "G \<turnstile> T \<preceq> NT", auto) |
196 by (ind_cases2 "G \<turnstile> T \<preceq> NT", auto) |
205 |
197 |
206 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False" |
198 lemma cast_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>? RefT rT) = False" |
207 apply (rule iffI) |
199 apply (rule iffI) |
208 apply (erule cast.elims) |
200 apply (erule cast.cases) |
209 apply auto |
201 apply auto |
210 done |
202 done |
211 |
203 |
212 lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT" |
204 lemma cast_RefT: "G \<turnstile> C \<preceq>? Class D \<Longrightarrow> \<exists> rT. C = RefT rT" |
213 apply (erule cast.cases) |
205 apply (erule cast.cases) |