author | haftmann |
Tue, 07 Oct 2008 16:07:50 +0200 | |
changeset 28524 | 644b62cf678f |
parent 24783 | 5a3e336a2e37 |
child 33954 | 1bc3b688548c |
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 |
ID: $Id$ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
3 |
Author: David von Oheimb |
11372 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
11070 | 5 |
*) |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
6 |
|
12911 | 7 |
header {* \isaheader{Example MicroJava Program} *} |
11070 | 8 |
|
16417 | 9 |
theory Example imports SystemClasses Eval begin |
11070 | 10 |
|
11 |
text {* |
|
12 |
The following example MicroJava program includes: |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
13 |
class declarations with inheritance, hiding of fields, and overriding of |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
14 |
methods (with refined result type), |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
15 |
instance creation, local assignment, sequential composition, |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
16 |
method call with dynamic binding, literal values, |
11070 | 17 |
expression statement, local access, type cast, field assignment (in part), |
18 |
skip. |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
19 |
|
11070 | 20 |
\begin{verbatim} |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
21 |
class Base { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
22 |
boolean vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
23 |
Base foo(Base x) {return x;} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
24 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
25 |
|
10229 | 26 |
class Ext extends Base { |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
27 |
int vee; |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
28 |
Ext foo(Base x) {((Ext)x).vee=1; return null;} |
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 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
31 |
class Example { |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
32 |
public static void main (String args[]) { |
9498 | 33 |
Base e=new Ext(); |
34 |
e.foo(null); |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
35 |
} |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
36 |
} |
11070 | 37 |
\end{verbatim} |
38 |
*} |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
39 |
|
24783 | 40 |
datatype cnam' = Base' | Ext' |
41 |
datatype vnam' = vee' | x' | e' |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
42 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
43 |
consts |
24783 | 44 |
cnam' :: "cnam' => cname" |
45 |
vnam' :: "vnam' => vnam" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
46 |
|
24783 | 47 |
-- "@{text cnam'} and @{text vnam'} are intended to be isomorphic |
12517 | 48 |
to @{text cnam} and @{text vnam}" |
49 |
axioms |
|
24783 | 50 |
inj_cnam': "(cnam' x = cnam' y) = (x = y)" |
51 |
inj_vnam': "(vnam' x = vnam' y) = (x = y)" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
52 |
|
24783 | 53 |
surj_cnam': "\<exists>m. n = cnam' m" |
54 |
surj_vnam': "\<exists>m. n = vnam' m" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
55 |
|
24783 | 56 |
declare inj_cnam' [simp] inj_vnam' [simp] |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
57 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
58 |
syntax |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
59 |
Base :: cname |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
60 |
Ext :: cname |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
61 |
vee :: vname |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
62 |
x :: vname |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
63 |
e :: vname |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
64 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
65 |
translations |
24783 | 66 |
"Base" == "cnam' Base'" |
67 |
"Ext" == "cnam' Ext'" |
|
68 |
"vee" == "VName (vnam' vee')" |
|
69 |
"x" == "VName (vnam' x')" |
|
70 |
"e" == "VName (vnam' e')" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
71 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
72 |
axioms |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
73 |
Base_not_Object: "Base \<noteq> Object" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
74 |
Ext_not_Object: "Ext \<noteq> Object" |
12951 | 75 |
Base_not_Xcpt: "Base \<noteq> Xcpt z" |
76 |
Ext_not_Xcpt: "Ext \<noteq> Xcpt z" |
|
77 |
e_not_This: "e \<noteq> This" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
78 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
79 |
declare Base_not_Object [simp] Ext_not_Object [simp] |
12951 | 80 |
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
|
81 |
declare e_not_This [simp] |
12951 | 82 |
declare Base_not_Object [symmetric, simp] |
83 |
declare Ext_not_Object [symmetric, simp] |
|
84 |
declare Base_not_Xcpt [symmetric, simp] |
|
85 |
declare Ext_not_Xcpt [symmetric, simp] |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
86 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
87 |
consts |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
88 |
foo_Base:: java_mb |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
89 |
foo_Ext :: java_mb |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
90 |
BaseC :: "java_mb cdecl" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
91 |
ExtC :: "java_mb cdecl" |
12517 | 92 |
test :: stmt |
93 |
foo :: mname |
|
94 |
a :: loc |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
95 |
b :: loc |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
96 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
97 |
defs |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
98 |
foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
99 |
BaseC_def:"BaseC == (Base, (Object, |
12517 | 100 |
[(vee, PrimT Boolean)], |
101 |
[((foo,[Class Base]),Class Base,foo_Base)]))" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
102 |
foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext |
12517 | 103 |
(LAcc x)..vee:=Lit (Intg Numeral1)), |
104 |
Lit Null)" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
105 |
ExtC_def: "ExtC == (Ext, (Base , |
12517 | 106 |
[(vee, PrimT Integer)], |
107 |
[((foo,[Class Base]),Class Ext,foo_Ext)]))" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
108 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
109 |
test_def:"test == Expr(e::=NewC Ext);; |
10763 | 110 |
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
111 |
|
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 |
12517 | 138 |
declare map_of_Cons [simp del] -- "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 |
|
22271 | 176 |
lemma not_Object_subcls [elim!]: "(subcls1 tprg)^++ Object C ==> R" |
23757 | 177 |
apply (auto dest!: tranclpD 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" |
23757 | 181 |
apply (erule rtranclp_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 |
|
22271 | 187 |
lemma not_Base_subcls_Ext [elim!]: "(subcls1 tprg)^++ Base Ext ==> R" |
23757 | 188 |
apply (auto dest!: tranclpD 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 |
|
22271 | 197 |
lemma not_class_subcls_class [elim!]: "(subcls1 tprg)^++ C C ==> R" |
23757 | 198 |
apply (auto dest!: tranclpD 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!:) |
23757 | 201 |
apply (drule rtranclpD) |
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 |
|
23757 | 209 |
lemmas subcls_direct = subcls1I [THEN r_into_rtranclp [where r="subcls1 G"], standard] |
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 |
|
24783 | 223 |
lemma acyclic_subcls1': "acyclicP (subcls1 tprg)" |
22271 | 224 |
apply (rule acyclicI [to_pred]) |
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 |
|
24783 | 228 |
lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]] |
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) |
|
23757 | 349 |
apply (drule rtranclpD) |
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 |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset
|
377 |
ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *} |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
378 |
lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
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>" |
12517 | 380 |
apply (tactic t) -- ";;" |
381 |
apply (tactic t) -- "Expr" |
|
382 |
apply (tactic t) -- "LAss" |
|
383 |
apply simp -- {* @{text "e \<noteq> This"} *} |
|
384 |
apply (tactic t) -- "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)) |
12517 | 387 |
apply (tactic t) -- "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)) |
12517 | 390 |
apply (tactic t) -- "Expr" |
391 |
apply (tactic t) -- "Call" |
|
392 |
apply (tactic t) -- "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)) |
12517 | 395 |
apply (tactic t) -- "Cons" |
396 |
apply (tactic t) -- "Lit" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
397 |
apply (simp (no_asm)) |
12517 | 398 |
apply (tactic t) -- "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 |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset
|
403 |
ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *} |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
404 |
|
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] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
407 |
lemma exec_test: |
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) |
12517 | 411 |
-- "?s = s3 " |
412 |
apply (tactic e) -- ";;" |
|
413 |
apply (tactic e) -- "Expr" |
|
414 |
apply (tactic e) -- "LAss" |
|
415 |
apply (tactic e) -- "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) |
12517 | 420 |
apply (tactic e) -- "Expr" |
421 |
apply (tactic e) -- "Call" |
|
422 |
apply (tactic e) -- "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
423 |
apply force |
12517 | 424 |
apply (tactic e) -- "Cons" |
425 |
apply (tactic e) -- "Lit" |
|
426 |
apply (tactic e) -- "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)) |
12517 | 430 |
apply (tactic e) -- "Expr" |
431 |
apply (tactic e) -- "FAss" |
|
432 |
apply (tactic e) -- "Cast" |
|
433 |
apply (tactic e) -- "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)) |
12517 | 437 |
apply (tactic e) -- "XcptE" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
438 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
439 |
apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force) |
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)) |
12517 | 442 |
apply (tactic e) -- "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 |