author | wenzelm |
Mon, 11 Jan 2016 21:21:02 +0100 | |
changeset 62145 | 5b946c81dfbf |
parent 62042 | 6c6ccf573479 |
child 62390 | 842917225d56 |
permissions | -rw-r--r-- |
12517 | 1 |
(* Title: HOL/MicroJava/J/Example.thy |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
2 |
Author: David von Oheimb |
11372 | 3 |
Copyright 1999 Technische Universitaet Muenchen |
11070 | 4 |
*) |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
5 |
|
61361 | 6 |
section \<open>Example MicroJava Program\<close> |
11070 | 7 |
|
16417 | 8 |
theory Example imports SystemClasses Eval begin |
11070 | 9 |
|
61361 | 10 |
text \<open> |
11070 | 11 |
The following example MicroJava program includes: |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
12 |
class declarations with inheritance, hiding of fields, and overriding of |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
13 |
methods (with refined result type), |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
14 |
instance creation, local assignment, sequential composition, |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
15 |
method call with dynamic binding, literal values, |
11070 | 16 |
expression statement, local access, type cast, field assignment (in part), |
17 |
skip. |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
18 |
|
11070 | 19 |
\begin{verbatim} |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
20 |
class Base { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
21 |
boolean vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
22 |
Base foo(Base x) {return x;} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
23 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
24 |
|
10229 | 25 |
class Ext extends Base { |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
26 |
int vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
27 |
Ext foo(Base x) {((Ext)x).vee=1; return null;} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
28 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
29 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
30 |
class Example { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
31 |
public static void main (String args[]) { |
9498 | 32 |
Base e=new Ext(); |
33 |
e.foo(null); |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
34 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
35 |
} |
11070 | 36 |
\end{verbatim} |
61361 | 37 |
\<close> |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
38 |
|
58310 | 39 |
datatype cnam' = Base' | Ext' |
40 |
datatype vnam' = vee' | x' | e' |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
41 |
|
61361 | 42 |
text \<open> |
62042 | 43 |
\<open>cnam'\<close> and \<open>vnam'\<close> are intended to be isomorphic |
44 |
to \<open>cnam\<close> and \<open>vnam\<close> |
|
61361 | 45 |
\<close> |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
46 |
|
45827 | 47 |
axiomatization cnam' :: "cnam' => cname" |
48 |
where |
|
49 |
inj_cnam': "(cnam' x = cnam' y) = (x = y)" and |
|
50 |
surj_cnam': "\<exists>m. n = cnam' m" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
51 |
|
45827 | 52 |
axiomatization vnam' :: "vnam' => vnam" |
53 |
where |
|
54 |
inj_vnam': "(vnam' x = vnam' y) = (x = y)" and |
|
24783 | 55 |
surj_vnam': "\<exists>m. n = vnam' m" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
56 |
|
24783 | 57 |
declare inj_cnam' [simp] inj_vnam' [simp] |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
58 |
|
35102 | 59 |
abbreviation Base :: cname |
60 |
where "Base == cnam' Base'" |
|
61 |
abbreviation Ext :: cname |
|
62 |
where "Ext == cnam' Ext'" |
|
63 |
abbreviation vee :: vname |
|
64 |
where "vee == VName (vnam' vee')" |
|
65 |
abbreviation x :: vname |
|
66 |
where "x == VName (vnam' x')" |
|
67 |
abbreviation e :: vname |
|
68 |
where "e == VName (vnam' e')" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
69 |
|
45827 | 70 |
axiomatization where |
71 |
Base_not_Object: "Base \<noteq> Object" and |
|
72 |
Ext_not_Object: "Ext \<noteq> Object" and |
|
73 |
Base_not_Xcpt: "Base \<noteq> Xcpt z" and |
|
74 |
Ext_not_Xcpt: "Ext \<noteq> Xcpt z" and |
|
12951 | 75 |
e_not_This: "e \<noteq> This" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
76 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
77 |
declare Base_not_Object [simp] Ext_not_Object [simp] |
12951 | 78 |
declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp] |
11643
0b3a02daf7fb
Added axiom e~=This to reflect strengthened precond. in rule LAss
streckem
parents:
11372
diff
changeset
|
79 |
declare e_not_This [simp] |
12951 | 80 |
declare Base_not_Object [symmetric, simp] |
81 |
declare Ext_not_Object [symmetric, simp] |
|
82 |
declare Base_not_Xcpt [symmetric, simp] |
|
83 |
declare Ext_not_Xcpt [symmetric, simp] |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
84 |
|
62145 | 85 |
definition foo_Base :: java_mb |
86 |
where "foo_Base == ([x],[],Skip,LAcc x)" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
87 |
|
62145 | 88 |
definition foo_Ext :: java_mb |
89 |
where "foo_Ext == ([x],[],Expr( {Ext}Cast Ext |
|
90 |
(LAcc x)..vee:=Lit (Intg Numeral1)), |
|
91 |
Lit Null)" |
|
92 |
||
93 |
consts foo :: mname |
|
94 |
||
95 |
definition BaseC :: "java_mb cdecl" |
|
96 |
where "BaseC == (Base, (Object, |
|
12517 | 97 |
[(vee, PrimT Boolean)], |
98 |
[((foo,[Class Base]),Class Base,foo_Base)]))" |
|
62145 | 99 |
|
100 |
definition ExtC :: "java_mb cdecl" |
|
101 |
where "ExtC == (Ext, (Base , |
|
12517 | 102 |
[(vee, PrimT Integer)], |
103 |
[((foo,[Class Base]),Class Ext,foo_Ext)]))" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
104 |
|
62145 | 105 |
definition test :: stmt |
106 |
where "test == Expr(e::=NewC Ext);; |
|
10763 | 107 |
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
108 |
|
62145 | 109 |
consts |
110 |
a :: loc |
|
111 |
b :: loc |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
112 |
|
20768 | 113 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
114 |
NP :: xcpt where |
20768 | 115 |
"NP == NullPointer" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
116 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
117 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
118 |
tprg ::"java_mb prog" where |
20768 | 119 |
"tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
120 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
121 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
122 |
obj1 :: obj where |
20768 | 123 |
"obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
124 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
125 |
abbreviation "s0 == Norm (empty, empty)" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
126 |
abbreviation "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
127 |
abbreviation "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
128 |
abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
129 |
|
24074 | 130 |
lemmas map_of_Cons = map_of.simps(2) |
131 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
132 |
lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
133 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
134 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
135 |
lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
136 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
137 |
done |
62042 | 138 |
declare map_of_Cons [simp del] \<comment> "sic!" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
139 |
|
28524 | 140 |
lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
141 |
apply (unfold ObjectC_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
142 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
143 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
144 |
|
12951 | 145 |
lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])" |
146 |
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
|
147 |
apply (simp (no_asm)) |
|
148 |
done |
|
149 |
||
150 |
lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])" |
|
151 |
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
|
152 |
apply (simp (no_asm)) |
|
153 |
done |
|
154 |
||
155 |
lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])" |
|
156 |
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
|
157 |
apply (simp (no_asm)) |
|
158 |
done |
|
159 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
160 |
lemma class_tprg_Base [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
161 |
"class tprg Base = Some (Object, |
12517 | 162 |
[(vee, PrimT Boolean)], |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
163 |
[((foo, [Class Base]), Class Base, foo_Base)])" |
12951 | 164 |
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
165 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
166 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
167 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
168 |
lemma class_tprg_Ext [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
169 |
"class tprg Ext = Some (Base, |
12517 | 170 |
[(vee, PrimT Integer)], |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
171 |
[((foo, [Class Base]), Class Ext, foo_Ext)])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
172 |
apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
173 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
174 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
175 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
176 |
lemma not_Object_subcls [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ ==> R" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
177 |
apply (auto dest!: tranclD subcls1D) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
178 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
179 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
180 |
lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
181 |
apply (erule rtrancl_induct) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
182 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
183 |
apply (drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
184 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
185 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
186 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
187 |
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
188 |
apply (auto dest!: tranclD subcls1D) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
189 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
190 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
191 |
lemma class_tprgD: |
12951 | 192 |
"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory" |
193 |
apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
194 |
apply (auto split add: split_if_asm simp add: map_of_Cons) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
195 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
196 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
197 |
lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
198 |
apply (auto dest!: tranclD subcls1D) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
199 |
apply (frule class_tprgD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
200 |
apply (auto dest!:) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
201 |
apply (drule rtranclD) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
202 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
203 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
204 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
205 |
lemma unique_classes: "unique tprg" |
12951 | 206 |
apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
207 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
208 |
|
45605 | 209 |
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
210 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
211 |
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
212 |
apply (rule subcls_direct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
213 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
214 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
215 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
216 |
lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
217 |
apply (rule widen.subcls) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
218 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
219 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
220 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
221 |
declare ty_expr_ty_exprs_wt_stmt.intros [intro!] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
222 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
223 |
lemma acyclic_subcls1': "acyclic (subcls1 tprg)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
224 |
apply (rule acyclicI) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
225 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
226 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
227 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
228 |
lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]] |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
229 |
|
24783 | 230 |
lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma] |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
231 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
232 |
lemma fields_Object [simp]: "fields (tprg, Object) = []" |
24783 | 233 |
apply (subst fields_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
234 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
235 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
236 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
237 |
declare is_class_def [simp] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
238 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
239 |
lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]" |
24783 | 240 |
apply (subst fields_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
241 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
242 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
243 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
244 |
lemma fields_Ext [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
245 |
"fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
246 |
apply (rule trans) |
24783 | 247 |
apply (rule fields_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
248 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
249 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
250 |
|
24783 | 251 |
lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma] |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
252 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
253 |
lemma method_Object [simp]: "method (tprg,Object) = map_of []" |
24783 | 254 |
apply (subst method_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
255 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
256 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
257 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
258 |
lemma method_Base [simp]: "method (tprg, Base) = map_of |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
259 |
[((foo, [Class Base]), Base, (Class Base, foo_Base))]" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
260 |
apply (rule trans) |
24783 | 261 |
apply (rule method_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
262 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
263 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
264 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
265 |
lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
266 |
[((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
267 |
apply (rule trans) |
24783 | 268 |
apply (rule method_rec') |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
269 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
270 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
271 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
272 |
lemma wf_foo_Base: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
273 |
"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
274 |
apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
275 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
276 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
277 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
278 |
lemma wf_foo_Ext: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
279 |
"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
280 |
apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
281 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
282 |
apply (rule ty_expr_ty_exprs_wt_stmt.Cast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
283 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
284 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
285 |
apply (rule_tac [2] cast.subcls) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
286 |
apply (unfold field_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
287 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
288 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
289 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
290 |
lemma wf_ObjectC: |
14045 | 291 |
"ws_cdecl tprg ObjectC \<and> |
292 |
wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC" |
|
293 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
294 |
wf_mrT_def wf_fdecl_def ObjectC_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
295 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
296 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
297 |
|
12951 | 298 |
lemma wf_NP: |
14045 | 299 |
"ws_cdecl tprg NullPointerC \<and> |
300 |
wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC" |
|
301 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
302 |
wf_mrT_def wf_fdecl_def NullPointerC_def) |
|
12951 | 303 |
apply (simp add: class_def) |
304 |
apply (fold NullPointerC_def class_def) |
|
305 |
apply auto |
|
306 |
done |
|
307 |
||
308 |
lemma wf_OM: |
|
14045 | 309 |
"ws_cdecl tprg OutOfMemoryC \<and> |
310 |
wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC" |
|
311 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
312 |
wf_mrT_def wf_fdecl_def OutOfMemoryC_def) |
|
12951 | 313 |
apply (simp add: class_def) |
314 |
apply (fold OutOfMemoryC_def class_def) |
|
315 |
apply auto |
|
316 |
done |
|
317 |
||
318 |
lemma wf_CC: |
|
14045 | 319 |
"ws_cdecl tprg ClassCastC \<and> |
320 |
wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC" |
|
321 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
322 |
wf_mrT_def wf_fdecl_def ClassCastC_def) |
|
12951 | 323 |
apply (simp add: class_def) |
324 |
apply (fold ClassCastC_def class_def) |
|
325 |
apply auto |
|
326 |
done |
|
327 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
328 |
lemma wf_BaseC: |
14045 | 329 |
"ws_cdecl tprg BaseC \<and> |
330 |
wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC" |
|
331 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
332 |
wf_mrT_def wf_fdecl_def BaseC_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
333 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
334 |
apply (fold BaseC_def) |
14045 | 335 |
apply (rule mp) defer apply (rule wf_foo_Base) |
336 |
apply (auto simp add: wf_mdecl_def) |
|
337 |
done |
|
338 |
||
339 |
||
340 |
lemma wf_ExtC: |
|
341 |
"ws_cdecl tprg ExtC \<and> |
|
342 |
wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC" |
|
343 |
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
344 |
wf_mrT_def wf_fdecl_def ExtC_def) |
|
345 |
apply (simp (no_asm)) |
|
346 |
apply (fold ExtC_def) |
|
347 |
apply (rule mp) defer apply (rule wf_foo_Ext) |
|
348 |
apply (auto simp add: wf_mdecl_def) |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset
|
349 |
apply (drule rtranclD) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
350 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
351 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
352 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
353 |
|
12951 | 354 |
lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |
355 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
356 |
lemma wf_tprg: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
357 |
"wf_prog wf_java_mdecl tprg" |
14045 | 358 |
apply (unfold wf_prog_def ws_prog_def Let_def) |
12951 | 359 |
apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes) |
360 |
apply (rule wf_syscls) |
|
361 |
apply (simp add: SystemClasses_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
362 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
363 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
364 |
lemma appl_methds_foo_Base: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
365 |
"appl_methds tprg Base (foo, [NT]) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
366 |
{((Class Base, Class Base), [Class Base])}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
367 |
apply (unfold appl_methds_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
368 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
369 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
370 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
371 |
lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
372 |
{((Class Base, Class Base), [Class Base])}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
373 |
apply (unfold max_spec_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
374 |
apply (auto simp add: appl_methds_foo_Base) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
375 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
376 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59199
diff
changeset
|
377 |
lemmas t = ty_expr_ty_exprs_wt_stmt.intros |
61337 | 378 |
schematic_goal wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
379 |
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" |
62042 | 380 |
apply (rule ty_expr_ty_exprs_wt_stmt.intros) \<comment> ";;" |
381 |
apply (rule t) \<comment> "Expr" |
|
382 |
apply (rule t) \<comment> "LAss" |
|
383 |
apply simp \<comment> \<open>\<open>e \<noteq> This\<close>\<close> |
|
384 |
apply (rule t) \<comment> "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
385 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
386 |
apply (simp (no_asm)) |
62042 | 387 |
apply (rule t) \<comment> "NewC" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
388 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
389 |
apply (simp (no_asm)) |
62042 | 390 |
apply (rule t) \<comment> "Expr" |
391 |
apply (rule t) \<comment> "Call" |
|
392 |
apply (rule t) \<comment> "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
393 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
394 |
apply (simp (no_asm)) |
62042 | 395 |
apply (rule t) \<comment> "Cons" |
396 |
apply (rule t) \<comment> "Lit" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
397 |
apply (simp (no_asm)) |
62042 | 398 |
apply (rule t) \<comment> "Nil" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
399 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
400 |
apply (rule max_spec_foo_Base) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
401 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
402 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
403 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59199
diff
changeset
|
404 |
lemmas e = NewCI eval_evals_exec.intros |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
405 |
declare split_if [split del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
406 |
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp] |
61337 | 407 |
schematic_goal exec_test: |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
408 |
" [|new_Addr (heap (snd s0)) = (a, None)|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
409 |
tprg\<turnstile>s0 -test-> ?s" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
410 |
apply (unfold test_def) |
62042 | 411 |
\<comment> "?s = s3 " |
412 |
apply (rule e) \<comment> ";;" |
|
413 |
apply (rule e) \<comment> "Expr" |
|
414 |
apply (rule e) \<comment> "LAss" |
|
415 |
apply (rule e) \<comment> "NewC" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
416 |
apply force |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
417 |
apply force |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
418 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
419 |
apply (erule thin_rl) |
62042 | 420 |
apply (rule e) \<comment> "Expr" |
421 |
apply (rule e) \<comment> "Call" |
|
422 |
apply (rule e) \<comment> "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
423 |
apply force |
62042 | 424 |
apply (rule e) \<comment> "Cons" |
425 |
apply (rule e) \<comment> "Lit" |
|
426 |
apply (rule e) \<comment> "Nil" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
427 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
428 |
apply (force simp add: foo_Ext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
429 |
apply (simp (no_asm)) |
62042 | 430 |
apply (rule e) \<comment> "Expr" |
431 |
apply (rule e) \<comment> "FAss" |
|
432 |
apply (rule e) \<comment> "Cast" |
|
433 |
apply (rule e) \<comment> "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
434 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
435 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
436 |
apply (simp (no_asm)) |
62042 | 437 |
apply (rule e) \<comment> "XcptE" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
438 |
apply (simp (no_asm)) |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61361
diff
changeset
|
439 |
apply (rule surjective_pairing [symmetric, THEN[2]trans], subst prod.inject, force) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
440 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
441 |
apply (simp (no_asm)) |
62042 | 442 |
apply (rule e) \<comment> "XcptE" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
443 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
444 |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
445 |
end |