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