author | wenzelm |
Wed, 10 Feb 2010 00:45:16 +0100 | |
changeset 35067 | af4c18c30593 |
parent 33965 | f57c11db4ad4 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/WellType.thy |
12854 | 2 |
Author: David von Oheimb |
3 |
*) |
|
4 |
header {* Well-typedness of Java programs *} |
|
5 |
||
33965 | 6 |
theory WellType |
7 |
imports DeclConcepts |
|
8 |
begin |
|
12854 | 9 |
|
10 |
text {* |
|
11 |
improvements over Java Specification 1.0: |
|
12 |
\begin{itemize} |
|
13 |
\item methods of Object can be called upon references of interface or array type |
|
14 |
\end{itemize} |
|
15 |
simplifications: |
|
16 |
\begin{itemize} |
|
17 |
\item the type rules include all static checks on statements and expressions, |
|
18 |
e.g. definedness of names (of parameters, locals, fields, methods) |
|
19 |
\end{itemize} |
|
20 |
design issues: |
|
21 |
\begin{itemize} |
|
22 |
\item unified type judgment for statements, variables, expressions, |
|
23 |
expression lists |
|
24 |
\item statements are typed like expressions with dummy type Void |
|
25 |
\item the typing rules take an extra argument that is capable of determining |
|
26 |
the dynamic type of objects. Therefore, they can be used for both |
|
27 |
checking static types and determining runtime types in transition semantics. |
|
28 |
\end{itemize} |
|
29 |
*} |
|
30 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
31 |
types lenv |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
32 |
= "(lname, ty) table" --{* local variables, including This and Result*} |
12854 | 33 |
|
34 |
record env = |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
35 |
prg:: "prog" --{* program *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
36 |
cls:: "qtname" --{* current package and class name *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
37 |
lcl:: "lenv" --{* local environment *} |
12854 | 38 |
|
39 |
translations |
|
40 |
"lenv" <= (type) "(lname, ty) table" |
|
41 |
"lenv" <= (type) "lname \<Rightarrow> ty option" |
|
42 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>" |
|
43 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>" |
|
44 |
||
45 |
||
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
46 |
abbreviation |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
47 |
pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *} |
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
48 |
where "pkg e == pid (cls e)" |
12854 | 49 |
|
50 |
section "Static overloading: maximally specific methods " |
|
51 |
||
52 |
types |
|
53 |
emhead = "ref_ty \<times> mhead" |
|
54 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
55 |
--{* Some mnemotic selectors for emhead *} |
12854 | 56 |
constdefs |
57 |
"declrefT" :: "emhead \<Rightarrow> ref_ty" |
|
58 |
"declrefT \<equiv> fst" |
|
59 |
||
60 |
"mhd" :: "emhead \<Rightarrow> mhead" |
|
61 |
"mhd \<equiv> snd" |
|
62 |
||
63 |
lemma declrefT_simp[simp]:"declrefT (r,m) = r" |
|
64 |
by (simp add: declrefT_def) |
|
65 |
||
66 |
lemma mhd_simp[simp]:"mhd (r,m) = m" |
|
67 |
by (simp add: mhd_def) |
|
68 |
||
69 |
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m" |
|
70 |
by (cases m) (simp add: member_is_static_simp mhd_def) |
|
71 |
||
72 |
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m" |
|
73 |
by (cases m) simp |
|
74 |
||
75 |
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m" |
|
76 |
by (cases m) simp |
|
77 |
||
78 |
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m" |
|
79 |
by (cases m) simp |
|
80 |
||
81 |
consts |
|
82 |
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" |
|
83 |
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" |
|
84 |
accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" |
|
85 |
mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" |
|
86 |
defs |
|
87 |
cmheads_def: |
|
88 |
"cmheads G S C |
|
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
27239
diff
changeset
|
89 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig)" |
12854 | 90 |
Objectmheads_def: |
91 |
"Objectmheads G S |
|
92 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) |
|
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
27239
diff
changeset
|
93 |
` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)" |
12854 | 94 |
accObjectmheads_def: |
95 |
"accObjectmheads G S T |
|
96 |
\<equiv> if G\<turnstile>RefT T accessible_in (pid S) |
|
97 |
then Objectmheads G S |
|
98 |
else \<lambda>sig. {}" |
|
99 |
primrec |
|
100 |
"mheads G S NullT = (\<lambda>sig. {})" |
|
101 |
"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) |
|
102 |
` accimethds G (pid S) I sig \<union> |
|
103 |
accObjectmheads G S (IfaceT I) sig)" |
|
104 |
"mheads G S (ClassT C) = cmheads G S C" |
|
105 |
"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" |
|
106 |
||
107 |
constdefs |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
108 |
--{* applicable methods, cf. 15.11.2.1 *} |
12854 | 109 |
appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" |
110 |
"appl_methds G S rt \<equiv> \<lambda> sig. |
|
111 |
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> |
|
112 |
G\<turnstile>(parTs sig)[\<preceq>]pTs'}" |
|
113 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
114 |
--{* more specific methods, cf. 15.11.2.2 *} |
12854 | 115 |
more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" |
116 |
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'" |
|
117 |
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*) |
|
118 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
119 |
--{* maximally specific methods, cf. 15.11.2.2 *} |
12854 | 120 |
max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" |
121 |
||
122 |
"max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
123 |
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}" |
12854 | 124 |
|
125 |
||
126 |
lemma max_spec2appl_meths: |
|
127 |
"x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" |
|
128 |
by (auto simp: max_spec_def) |
|
129 |
||
130 |
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow> |
|
131 |
mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" |
|
132 |
by (auto simp: appl_methds_def) |
|
133 |
||
134 |
lemma max_spec2mheads: |
|
135 |
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A |
|
136 |
\<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" |
|
137 |
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD) |
|
138 |
done |
|
139 |
||
140 |
||
141 |
constdefs |
|
142 |
empty_dt :: "dyn_ty" |
|
143 |
"empty_dt \<equiv> \<lambda>a. None" |
|
144 |
||
145 |
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
146 |
"invmode m e \<equiv> if is_static m |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
147 |
then Static |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
148 |
else if e=Super then SuperM else IntVir" |
12854 | 149 |
|
150 |
lemma invmode_nonstatic [simp]: |
|
151 |
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" |
|
152 |
apply (unfold invmode_def) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
153 |
apply (simp (no_asm) add: member_is_static_simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
154 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
155 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
156 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
157 |
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
158 |
apply (unfold invmode_def) |
12854 | 159 |
apply (simp (no_asm)) |
160 |
done |
|
161 |
||
162 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
163 |
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" |
12854 | 164 |
apply (unfold invmode_def) |
165 |
apply (simp (no_asm)) |
|
166 |
done |
|
167 |
||
168 |
lemma Null_staticD: |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
169 |
"a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" |
12854 | 170 |
apply (clarsimp simp add: invmode_IntVir_eq) |
171 |
done |
|
172 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
173 |
section "Typing for unary operations" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
174 |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
175 |
consts unop_type :: "unop \<Rightarrow> prim_ty" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
176 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
177 |
"unop_type UPlus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
178 |
"unop_type UMinus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
179 |
"unop_type UBitNot = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
180 |
"unop_type UNot = Boolean" |
12854 | 181 |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
182 |
consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
183 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
184 |
"wt_unop UPlus t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
185 |
"wt_unop UMinus t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
186 |
"wt_unop UBitNot t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
187 |
"wt_unop UNot t = (t = PrimT Boolean)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
188 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
189 |
section "Typing for binary operations" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
190 |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
191 |
consts binop_type :: "binop \<Rightarrow> prim_ty" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
192 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
193 |
"binop_type Mul = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
194 |
"binop_type Div = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
195 |
"binop_type Mod = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
196 |
"binop_type Plus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
197 |
"binop_type Minus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
198 |
"binop_type LShift = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
199 |
"binop_type RShift = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
200 |
"binop_type RShiftU = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
201 |
"binop_type Less = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
202 |
"binop_type Le = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
203 |
"binop_type Greater = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
204 |
"binop_type Ge = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
205 |
"binop_type Eq = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
206 |
"binop_type Neq = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
207 |
"binop_type BitAnd = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
208 |
"binop_type And = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
209 |
"binop_type BitXor = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
210 |
"binop_type Xor = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
211 |
"binop_type BitOr = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
212 |
"binop_type Or = Boolean" |
13384 | 213 |
"binop_type CondAnd = Boolean" |
214 |
"binop_type CondOr = Boolean" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
215 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
216 |
consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
217 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
218 |
"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
219 |
"wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
220 |
"wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
221 |
"wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
222 |
"wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
223 |
"wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
224 |
"wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
225 |
"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
226 |
"wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
227 |
"wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
228 |
"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
229 |
"wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
230 |
"wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
231 |
"wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
232 |
"wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
233 |
"wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
234 |
"wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
235 |
"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
236 |
"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
237 |
"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
13384 | 238 |
"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
239 |
"wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
240 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
241 |
section "Typing for terms" |
13384 | 242 |
|
12854 | 243 |
types tys = "ty + ty list" |
244 |
translations |
|
245 |
"tys" <= (type) "ty + ty list" |
|
246 |
||
21765 | 247 |
|
23747 | 248 |
inductive |
21765 | 249 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) |
250 |
and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50) |
|
251 |
and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50) |
|
252 |
and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) |
|
253 |
and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" |
|
254 |
("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) |
|
255 |
where |
|
256 |
||
257 |
"E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" |
|
258 |
| "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T" |
|
259 |
| "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2 e\<Colon>Inl T" |
|
260 |
| "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3 e\<Colon>Inr T" |
|
261 |
||
262 |
--{* well-typed statements *} |
|
263 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
264 |
| Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" |
21765 | 265 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
266 |
| Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
267 |
E,dt\<Turnstile>Expr e\<Colon>\<surd>" |
21765 | 268 |
--{* cf. 14.6 *} |
269 |
| Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> |
|
270 |
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" |
|
271 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
272 |
| Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
273 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
274 |
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" |
21765 | 275 |
|
276 |
--{* cf. 14.8 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
277 |
| If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
278 |
E,dt\<Turnstile>c1\<Colon>\<surd>; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
279 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
280 |
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" |
21765 | 281 |
|
282 |
--{* cf. 14.10 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
283 |
| Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
284 |
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
285 |
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" |
21765 | 286 |
--{* cf. 14.13, 14.15, 14.16 *} |
287 |
| Jmp: "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>" |
|
12854 | 288 |
|
21765 | 289 |
--{* cf. 14.16 *} |
290 |
| Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn; |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
291 |
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
292 |
E,dt\<Turnstile>Throw e\<Colon>\<surd>" |
21765 | 293 |
--{* cf. 14.18 *} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
294 |
| Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
295 |
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> |
21765 | 296 |
\<Longrightarrow> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
297 |
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" |
21765 | 298 |
|
299 |
--{* cf. 14.18 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
300 |
| Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
301 |
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" |
21765 | 302 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
303 |
| Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
304 |
E,dt\<Turnstile>Init C\<Colon>\<surd>" |
21765 | 305 |
--{* @{term Init} is created on the fly during evaluation (see Eval.thy). |
306 |
The class isn't necessarily accessible from the points @{term Init} |
|
307 |
is called. Therefor we only demand @{term is_class} and not |
|
308 |
@{term is_acc_class} here. |
|
309 |
*} |
|
310 |
||
311 |
--{* well-typed expressions *} |
|
312 |
||
313 |
--{* cf. 15.8 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
314 |
| NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
315 |
E,dt\<Turnstile>NewC C\<Colon>-Class C" |
21765 | 316 |
--{* cf. 15.9 *} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
317 |
| NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
318 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
319 |
E,dt\<Turnstile>New T[i]\<Colon>-T.[]" |
21765 | 320 |
|
321 |
--{* cf. 15.15 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
322 |
| Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T'; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
323 |
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
324 |
E,dt\<Turnstile>Cast T' e\<Colon>-T'" |
21765 | 325 |
|
326 |
--{* cf. 15.19.2 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
327 |
| Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
328 |
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
329 |
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean" |
21765 | 330 |
|
331 |
--{* cf. 15.7.1 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
332 |
| Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
333 |
E,dt\<Turnstile>Lit x\<Colon>-T" |
12854 | 334 |
|
21765 | 335 |
| UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> |
336 |
\<Longrightarrow> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
337 |
E,dt\<Turnstile>UnOp unop e\<Colon>-T" |
21765 | 338 |
|
339 |
| BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; |
|
340 |
T=PrimT (binop_type binop)\<rbrakk> |
|
341 |
\<Longrightarrow> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
342 |
E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T" |
21765 | 343 |
|
344 |
--{* cf. 15.10.2, 15.11.1 *} |
|
345 |
| Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
346 |
class (prg E) C = Some c\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
347 |
E,dt\<Turnstile>Super\<Colon>-Class (super c)" |
21765 | 348 |
|
349 |
--{* cf. 15.13.1, 15.10.1, 15.12 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
350 |
| Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
351 |
E,dt\<Turnstile>Acc va\<Colon>-T" |
21765 | 352 |
|
353 |
--{* cf. 15.25, 15.25.1 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
354 |
| Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
355 |
E,dt\<Turnstile>v \<Colon>-T'; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
356 |
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
357 |
E,dt\<Turnstile>va:=v\<Colon>-T'" |
21765 | 358 |
|
359 |
--{* cf. 15.24 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
360 |
| Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
361 |
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
362 |
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
363 |
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T" |
21765 | 364 |
|
365 |
--{* cf. 15.11.1, 15.11.2, 15.11.3 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
366 |
| Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
367 |
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
368 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
21765 | 369 |
= {((statDeclT,m),pTs')} |
370 |
\<rbrakk> \<Longrightarrow> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
371 |
E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)" |
12854 | 372 |
|
21765 | 373 |
| Methd: "\<lbrakk>is_class (prg E) C; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
374 |
methd (prg E) C sig = Some m; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
375 |
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
376 |
E,dt\<Turnstile>Methd C sig\<Colon>-T" |
21765 | 377 |
--{* The class @{term C} is the dynamic class of the method call |
378 |
(cf. Eval.thy). |
|
379 |
It hasn't got to be directly accessible from the current package |
|
380 |
@{term "(pkg E)"}. |
|
381 |
Only the static class must be accessible (enshured indirectly by |
|
382 |
@{term Call}). |
|
383 |
Note that l is just a dummy value. It is only used in the smallstep |
|
384 |
semantics. To proof typesafety directly for the smallstep semantics |
|
385 |
we would have to assume conformance of l here! |
|
386 |
*} |
|
387 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
388 |
| Body: "\<lbrakk>is_class (prg E) D; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
389 |
E,dt\<Turnstile>blk\<Colon>\<surd>; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
390 |
(lcl E) Result = Some T; |
21765 | 391 |
is_type (prg E) T\<rbrakk> \<Longrightarrow> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
392 |
E,dt\<Turnstile>Body D blk\<Colon>-T" |
21765 | 393 |
--{* The class @{term D} implementing the method must not directly be |
394 |
accessible from the current package @{term "(pkg E)"}, but can also |
|
395 |
be indirectly accessible due to inheritance (enshured in @{term Call}) |
|
396 |
The result type hasn't got to be accessible in Java! (If it is not |
|
397 |
accessible you can only assign it to Object). |
|
398 |
For dummy value l see rule @{term Methd}. |
|
399 |
*} |
|
400 |
||
401 |
--{* well-typed variables *} |
|
402 |
||
403 |
--{* cf. 15.13.1 *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
404 |
| LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
405 |
E,dt\<Turnstile>LVar vn\<Colon>=T" |
21765 | 406 |
--{* cf. 15.10.1 *} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
407 |
| FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
408 |
accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
409 |
E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" |
21765 | 410 |
--{* cf. 15.12 *} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
411 |
| AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
412 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
413 |
E,dt\<Turnstile>e.[i]\<Colon>=T" |
21765 | 414 |
|
415 |
||
416 |
--{* well-typed expression lists *} |
|
417 |
||
418 |
--{* cf. 15.11.??? *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
419 |
| Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" |
21765 | 420 |
|
421 |
--{* cf. 15.11.??? *} |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
422 |
| Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
423 |
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
424 |
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" |
21765 | 425 |
|
12854 | 426 |
|
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
427 |
(* for purely static typing *) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
428 |
abbreviation |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
429 |
wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
430 |
where "E|-t::T == E,empty_dt\<Turnstile>t\<Colon> T" |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
431 |
|
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
432 |
abbreviation |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
433 |
wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
434 |
where "E|-s:<> == E|-In1r s :: Inl (PrimT Void)" |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
435 |
|
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
436 |
abbreviation |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
437 |
ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
438 |
where "E|-e:-T == E|-In1l e :: Inl T" |
12854 | 439 |
|
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
440 |
abbreviation |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
441 |
ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
442 |
where "E|-e:=T == E|-In2 e :: Inl T" |
12854 | 443 |
|
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
444 |
abbreviation |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
445 |
ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
446 |
where "E|-e:#T == E|-In3 e :: Inr T" |
12854 | 447 |
|
35067
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
448 |
notation (xsymbols) |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
449 |
wt_syntax ("_\<turnstile>_\<Colon>_" [51,51,51] 50) and |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
450 |
wt_stmt_syntax ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) and |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
451 |
ty_expr_syntax ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) and |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
452 |
ty_var_syntax ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) and |
af4c18c30593
modernized syntax translations, using mostly abbreviation/notation;
wenzelm
parents:
33965
diff
changeset
|
453 |
ty_exprs_syntax ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
454 |
|
12854 | 455 |
declare not_None_eq [simp del] |
456 |
declare split_if [split del] split_if_asm [split del] |
|
457 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
24019 | 458 |
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *} |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
459 |
|
23747 | 460 |
inductive_cases wt_elim_cases [cases set]: |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
461 |
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
462 |
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
463 |
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
464 |
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
465 |
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
466 |
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
467 |
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
468 |
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T" |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
469 |
"E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
470 |
"E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
471 |
"E,dt\<Turnstile>In1l (Super) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
472 |
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
473 |
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
474 |
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
475 |
"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
476 |
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
477 |
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
478 |
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
479 |
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
480 |
"E,dt\<Turnstile>In1r Skip \<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
481 |
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
482 |
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" |
12854 | 483 |
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
484 |
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
485 |
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
486 |
"E,dt\<Turnstile>In1r (Jmp jump) \<Colon>x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
487 |
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
488 |
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
489 |
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
490 |
"E,dt\<Turnstile>In1r (Init C) \<Colon>x" |
12854 | 491 |
declare not_None_eq [simp] |
492 |
declare split_if [split] split_if_asm [split] |
|
493 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
24019 | 494 |
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} |
12854 | 495 |
|
496 |
lemma is_acc_class_is_accessible: |
|
497 |
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" |
|
498 |
by (auto simp add: is_acc_class_def) |
|
499 |
||
500 |
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" |
|
501 |
by (auto simp add: is_acc_iface_def) |
|
502 |
||
13524 | 503 |
lemma is_acc_iface_Iface_is_accessible: |
12854 | 504 |
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" |
505 |
by (auto simp add: is_acc_iface_def) |
|
506 |
||
507 |
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" |
|
508 |
by (auto simp add: is_acc_type_def) |
|
509 |
||
13524 | 510 |
lemma is_acc_iface_is_accessible: |
511 |
"is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" |
|
12854 | 512 |
by (auto simp add: is_acc_type_def) |
513 |
||
514 |
lemma wt_Methd_is_methd: |
|
515 |
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" |
|
516 |
apply (erule_tac wt_elim_cases) |
|
517 |
apply clarsimp |
|
518 |
apply (erule is_methdI, assumption) |
|
519 |
done |
|
520 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
521 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
522 |
text {* Special versions of some typing rules, better suited to pattern |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
523 |
match the conclusion (no selectors in the conclusion) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
524 |
*} |
12854 | 525 |
|
526 |
lemma wt_Call: |
|
527 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
|
528 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
529 |
= {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
530 |
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT" |
12854 | 531 |
by (auto elim: wt.Call) |
532 |
||
533 |
||
534 |
lemma invocationTypeExpr_noClassD: |
|
535 |
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk> |
|
536 |
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" |
|
537 |
proof - |
|
538 |
assume wt: "E\<turnstile>e\<Colon>-RefT statT" |
|
539 |
show ?thesis |
|
540 |
proof (cases "e=Super") |
|
541 |
case True |
|
542 |
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) |
|
543 |
then show ?thesis by blast |
|
544 |
next |
|
545 |
case False then show ?thesis |
|
546 |
by (auto simp add: invmode_def split: split_if_asm) |
|
547 |
qed |
|
548 |
qed |
|
549 |
||
550 |
lemma wt_Super: |
|
551 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> |
|
552 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D" |
|
553 |
by (auto elim: wt.Super) |
|
554 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
555 |
lemma wt_FVar: |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
556 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
557 |
sf=is_static f; fT=(type f); accC=cls E\<rbrakk> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
558 |
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
559 |
by (auto dest: wt.FVar) |
12854 | 560 |
|
561 |
||
562 |
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" |
|
563 |
by (auto elim: wt_elim_cases intro: "wt.Init") |
|
564 |
||
565 |
declare wt.Skip [iff] |
|
566 |
||
567 |
lemma wt_StatRef: |
|
568 |
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt" |
|
569 |
apply (rule wt.Cast) |
|
570 |
apply (rule wt.Lit) |
|
571 |
apply (simp (no_asm)) |
|
572 |
apply (simp (no_asm_simp)) |
|
573 |
apply (rule cast.widen) |
|
574 |
apply (simp (no_asm)) |
|
575 |
done |
|
576 |
||
577 |
lemma wt_Inj_elim: |
|
578 |
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of |
|
579 |
In1 ec \<Rightarrow> (case ec of |
|
580 |
Inl e \<Rightarrow> \<exists>T. U=Inl T |
|
581 |
| Inr s \<Rightarrow> U=Inl (PrimT Void)) |
|
582 |
| In2 e \<Rightarrow> (\<exists>T. U=Inl T) |
|
583 |
| In3 e \<Rightarrow> (\<exists>T. U=Inr T)" |
|
584 |
apply (erule wt.induct) |
|
585 |
apply auto |
|
586 |
done |
|
587 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
588 |
--{* In the special syntax to distinguish the typing judgements for expressions, |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
589 |
statements, variables and expression lists the kind of term corresponds |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
590 |
to the kind of type in the end e.g. An statement (injection @{term In3} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
591 |
into terms, always has type void (injection @{term Inl} into the generalised |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
592 |
types. The following simplification procedures establish these kinds of |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
593 |
correlation. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
594 |
*} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
595 |
|
21765 | 596 |
lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)" |
597 |
by (auto, frule wt_Inj_elim, auto) |
|
598 |
||
599 |
lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)" |
|
600 |
by (auto, frule wt_Inj_elim, auto) |
|
601 |
||
602 |
lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)" |
|
603 |
by (auto, frule wt_Inj_elim, auto) |
|
604 |
||
605 |
lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)" |
|
606 |
by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto) |
|
607 |
||
24019 | 608 |
simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {* |
609 |
fn _ => fn _ => fn ct => |
|
610 |
(case Thm.term_of ct of |
|
611 |
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE |
|
612 |
| _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *} |
|
613 |
||
614 |
simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {* |
|
615 |
fn _ => fn _ => fn ct => |
|
616 |
(case Thm.term_of ct of |
|
617 |
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE |
|
618 |
| _ => SOME (mk_meta_eq @{thm wt_var_eq})) *} |
|
12854 | 619 |
|
24019 | 620 |
simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {* |
621 |
fn _ => fn _ => fn ct => |
|
622 |
(case Thm.term_of ct of |
|
623 |
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE |
|
624 |
| _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *} |
|
12854 | 625 |
|
24019 | 626 |
simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {* |
627 |
fn _ => fn _ => fn ct => |
|
628 |
(case Thm.term_of ct of |
|
629 |
(_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE |
|
630 |
| _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *} |
|
12854 | 631 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
632 |
lemma wt_elim_BinOp: |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
633 |
"\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
634 |
\<And>T1 T2 T3. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
635 |
\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
636 |
E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
637 |
T = Inl (PrimT (binop_type binop))\<rbrakk> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
638 |
\<Longrightarrow> P\<rbrakk> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
639 |
\<Longrightarrow> P" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
640 |
apply (erule wt_elim_cases) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
641 |
apply (cases b) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
642 |
apply auto |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
643 |
done |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13524
diff
changeset
|
644 |
|
12854 | 645 |
lemma Inj_eq_lemma [simp]: |
646 |
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" |
|
647 |
by auto |
|
648 |
||
649 |
(* unused *) |
|
650 |
lemma single_valued_tys_lemma [rule_format (no_asm)]: |
|
651 |
"\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> |
|
652 |
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" |
|
653 |
apply (cases "E", erule wt.induct) |
|
654 |
apply (safe del: disjE) |
|
655 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
|
656 |
apply (safe del: disjE) |
|
657 |
(* 17 subgoals *) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24783
diff
changeset
|
658 |
apply (tactic {* ALLGOALS (fn i => |
27239 | 659 |
if i = 11 then EVERY' |
660 |
[thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", |
|
661 |
thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1", |
|
662 |
thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i |
|
663 |
else thin_tac @{context} "All ?P" i) *}) |
|
12854 | 664 |
(*apply (safe del: disjE elim!: wt_elim_cases)*) |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24783
diff
changeset
|
665 |
apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) |
12854 | 666 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
667 |
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) |
12854 | 668 |
apply ((blast del: equalityCE dest: sym [THEN trans])+) |
669 |
done |
|
670 |
||
671 |
(* unused *) |
|
672 |
lemma single_valued_tys: |
|
673 |
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" |
|
674 |
apply (unfold single_valued_def) |
|
675 |
apply clarsimp |
|
676 |
apply (rule single_valued_tys_lemma) |
|
677 |
apply (auto intro!: widen_antisym) |
|
678 |
done |
|
679 |
||
680 |
lemma typeof_empty_is_type [rule_format (no_asm)]: |
|
681 |
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" |
|
682 |
apply (rule val.induct) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
683 |
apply auto |
12854 | 684 |
done |
685 |
||
686 |
(* unused *) |
|
687 |
lemma typeof_is_type [rule_format (no_asm)]: |
|
688 |
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)" |
|
689 |
apply (rule val.induct) |
|
690 |
prefer 5 |
|
691 |
apply fast |
|
692 |
apply (simp_all (no_asm)) |
|
693 |
done |
|
694 |
||
695 |
end |