author | kleing |
Tue, 26 Feb 2002 15:45:32 +0100 | |
changeset 12951 | a9fdcb71d252 |
parent 12911 | 704713ca07ea |
child 14045 | a34d89ce6097 |
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 |
|
12951 | 9 |
theory Example = SystemClasses + Eval: |
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 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
40 |
datatype cnam_ = Base_ | Ext_ |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
41 |
datatype vnam_ = vee_ | x_ | e_ |
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 |
10042 | 44 |
cnam_ :: "cnam_ => cname" |
45 |
vnam_ :: "vnam_ => vnam" |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
46 |
|
12517 | 47 |
-- "@{text cnam_} and @{text vnam_} are intended to be isomorphic |
48 |
to @{text cnam} and @{text vnam}" |
|
49 |
axioms |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
50 |
inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
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 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
53 |
surj_cnam_: "\<exists>m. n = cnam_ m" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
54 |
surj_vnam_: "\<exists>m. n = vnam_ m" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
55 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
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 |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
66 |
"Base" == "cnam_ Base_" |
12517 | 67 |
"Ext" == "cnam_ Ext_" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
68 |
"vee" == "VName (vnam_ vee_)" |
12517 | 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 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
113 |
syntax |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
114 |
|
12517 | 115 |
NP :: xcpt |
116 |
tprg ::"java_mb prog" |
|
117 |
obj1 :: obj |
|
118 |
obj2 :: obj |
|
119 |
s0 :: state |
|
120 |
s1 :: state |
|
121 |
s2 :: state |
|
122 |
s3 :: state |
|
123 |
s4 :: state |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
124 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
125 |
translations |
9498 | 126 |
"NP" == "NullPointer" |
12951 | 127 |
"tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
128 |
"obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False) |
12517 | 129 |
((vee, Ext )\<mapsto>Intg 0))" |
9793 | 130 |
"s0" == " Norm (empty, empty)" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
131 |
"s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
132 |
"s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
133 |
"s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
134 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
135 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
136 |
ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *} |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
137 |
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
|
138 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
139 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
140 |
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
|
141 |
apply (simp (no_asm_simp)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
142 |
done |
12517 | 143 |
declare map_of_Cons [simp del] -- "sic!" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
144 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
145 |
lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
146 |
apply (unfold ObjectC_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
147 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
148 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
149 |
|
12951 | 150 |
lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = 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_OM [simp]: "class tprg (Xcpt OutOfMemory) = 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 |
||
160 |
lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])" |
|
161 |
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) |
|
162 |
apply (simp (no_asm)) |
|
163 |
done |
|
164 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
165 |
lemma class_tprg_Base [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
166 |
"class tprg Base = Some (Object, |
12517 | 167 |
[(vee, PrimT Boolean)], |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
168 |
[((foo, [Class Base]), Class Base, foo_Base)])" |
12951 | 169 |
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
|
170 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
171 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
172 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
173 |
lemma class_tprg_Ext [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
174 |
"class tprg Ext = Some (Base, |
12517 | 175 |
[(vee, PrimT Integer)], |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
176 |
[((foo, [Class Base]), Class Ext, foo_Ext)])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
177 |
apply (unfold ObjectC_def BaseC_def ExtC_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
178 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
179 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
180 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
181 |
lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
182 |
apply (auto dest!: tranclD subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
183 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
184 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
185 |
lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
186 |
apply (erule rtrancl_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
187 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
188 |
apply (drule subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
189 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
190 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
191 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
192 |
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
193 |
apply (auto dest!: tranclD subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
194 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
195 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
196 |
lemma class_tprgD: |
12951 | 197 |
"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" |
198 |
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
|
199 |
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
|
200 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
201 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
202 |
lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
203 |
apply (auto dest!: tranclD subcls1D) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
204 |
apply (frule class_tprgD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
205 |
apply (auto dest!:) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
206 |
apply (drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
207 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
208 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
209 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
210 |
lemma unique_classes: "unique tprg" |
12951 | 211 |
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
|
212 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
213 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
214 |
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl] |
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_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
217 |
apply (rule subcls_direct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
218 |
apply auto |
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 |
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
|
222 |
apply (rule widen.subcls) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
223 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
224 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
225 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
226 |
declare ty_expr_ty_exprs_wt_stmt.intros [intro!] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
227 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
228 |
lemma acyclic_subcls1_: "acyclic (subcls1 tprg)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
229 |
apply (rule acyclicI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
230 |
apply safe |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
231 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
232 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
233 |
lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
234 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
235 |
lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma] |
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 |
lemma fields_Object [simp]: "fields (tprg, Object) = []" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
238 |
apply (subst fields_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
239 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
240 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
241 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
242 |
declare is_class_def [simp] |
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_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
245 |
apply (subst fields_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
246 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
247 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
248 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
249 |
lemma fields_Ext [simp]: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
250 |
"fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
251 |
apply (rule trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
252 |
apply (rule fields_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
253 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
254 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
255 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
256 |
lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma] |
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_Object [simp]: "method (tprg,Object) = map_of []" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
259 |
apply (subst method_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
260 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
261 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
262 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
263 |
lemma method_Base [simp]: "method (tprg, Base) = map_of |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
264 |
[((foo, [Class Base]), Base, (Class Base, foo_Base))]" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
265 |
apply (rule trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
266 |
apply (rule method_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
267 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
268 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
269 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
270 |
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
|
271 |
[((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
272 |
apply (rule trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
273 |
apply (rule method_rec_) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
274 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
275 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
276 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
277 |
lemma wf_foo_Base: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
278 |
"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
|
279 |
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
|
280 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
281 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
282 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
283 |
lemma wf_foo_Ext: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
284 |
"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
|
285 |
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
|
286 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
287 |
apply (rule ty_expr_ty_exprs_wt_stmt.Cast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
288 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
289 |
apply (simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
290 |
apply (rule_tac [2] cast.subcls) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
291 |
apply (unfold field_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
292 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
293 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
294 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
295 |
lemma wf_ObjectC: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
296 |
"wf_cdecl wf_java_mdecl tprg ObjectC" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
297 |
apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
298 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
299 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
300 |
|
12951 | 301 |
lemma wf_NP: |
302 |
"wf_cdecl wf_java_mdecl tprg NullPointerC" |
|
303 |
apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def) |
|
304 |
apply (simp add: class_def) |
|
305 |
apply (fold NullPointerC_def class_def) |
|
306 |
apply auto |
|
307 |
done |
|
308 |
||
309 |
lemma wf_OM: |
|
310 |
"wf_cdecl wf_java_mdecl tprg OutOfMemoryC" |
|
311 |
apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def) |
|
312 |
apply (simp add: class_def) |
|
313 |
apply (fold OutOfMemoryC_def class_def) |
|
314 |
apply auto |
|
315 |
done |
|
316 |
||
317 |
lemma wf_CC: |
|
318 |
"wf_cdecl wf_java_mdecl tprg ClassCastC" |
|
319 |
apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def) |
|
320 |
apply (simp add: class_def) |
|
321 |
apply (fold ClassCastC_def class_def) |
|
322 |
apply auto |
|
323 |
done |
|
324 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
325 |
lemma wf_BaseC: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
326 |
"wf_cdecl wf_java_mdecl tprg BaseC" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
327 |
apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
328 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
329 |
apply (fold BaseC_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
330 |
apply (rule wf_foo_Base [THEN conjI]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
331 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
332 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
333 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
334 |
lemma wf_ExtC: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
335 |
"wf_cdecl wf_java_mdecl tprg ExtC" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
336 |
apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
337 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
338 |
apply (fold ExtC_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
339 |
apply (rule wf_foo_Ext [THEN conjI]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
340 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
341 |
apply (drule rtranclD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
342 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
343 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
344 |
|
12951 | 345 |
lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |
346 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
347 |
lemma wf_tprg: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
348 |
"wf_prog wf_java_mdecl tprg" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
349 |
apply (unfold wf_prog_def Let_def) |
12951 | 350 |
apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes) |
351 |
apply (rule wf_syscls) |
|
352 |
apply (simp add: SystemClasses_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
353 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
354 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
355 |
lemma appl_methds_foo_Base: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
356 |
"appl_methds tprg Base (foo, [NT]) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
357 |
{((Class Base, Class Base), [Class Base])}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
358 |
apply (unfold appl_methds_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
359 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
360 |
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
361 |
apply (auto simp add: map_of_Cons foo_Base_def) |
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 max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
365 |
{((Class Base, Class Base), [Class Base])}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
366 |
apply (unfold max_spec_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
367 |
apply (auto simp add: appl_methds_foo_Base) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
368 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
369 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
370 |
ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *} |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
371 |
lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
372 |
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" |
12517 | 373 |
apply (tactic t) -- ";;" |
374 |
apply (tactic t) -- "Expr" |
|
375 |
apply (tactic t) -- "LAss" |
|
376 |
apply simp -- {* @{text "e \<noteq> This"} *} |
|
377 |
apply (tactic t) -- "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
378 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
379 |
apply (simp (no_asm)) |
12517 | 380 |
apply (tactic t) -- "NewC" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
381 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
382 |
apply (simp (no_asm)) |
12517 | 383 |
apply (tactic t) -- "Expr" |
384 |
apply (tactic t) -- "Call" |
|
385 |
apply (tactic t) -- "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
386 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
387 |
apply (simp (no_asm)) |
12517 | 388 |
apply (tactic t) -- "Cons" |
389 |
apply (tactic t) -- "Lit" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
390 |
apply (simp (no_asm)) |
12517 | 391 |
apply (tactic t) -- "Nil" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
392 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
393 |
apply (rule max_spec_foo_Base) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
394 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
395 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
396 |
ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *} |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
397 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
398 |
declare split_if [split del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
399 |
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
|
400 |
lemma exec_test: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
401 |
" [|new_Addr (heap (snd s0)) = (a, None)|] ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
402 |
tprg\<turnstile>s0 -test-> ?s" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
403 |
apply (unfold test_def) |
12517 | 404 |
-- "?s = s3 " |
405 |
apply (tactic e) -- ";;" |
|
406 |
apply (tactic e) -- "Expr" |
|
407 |
apply (tactic e) -- "LAss" |
|
408 |
apply (tactic e) -- "NewC" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
409 |
apply force |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
410 |
apply force |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
411 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
412 |
apply (erule thin_rl) |
12517 | 413 |
apply (tactic e) -- "Expr" |
414 |
apply (tactic e) -- "Call" |
|
415 |
apply (tactic e) -- "LAcc" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
416 |
apply force |
12517 | 417 |
apply (tactic e) -- "Cons" |
418 |
apply (tactic e) -- "Lit" |
|
419 |
apply (tactic e) -- "Nil" |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
420 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
421 |
apply (force simp add: foo_Ext_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
422 |
apply (simp (no_asm)) |
12517 | 423 |
apply (tactic e) -- "Expr" |
424 |
apply (tactic e) -- "FAss" |
|
425 |
apply (tactic e) -- "Cast" |
|
426 |
apply (tactic e) -- "LAcc" |
|
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 (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
429 |
apply (simp (no_asm)) |
12517 | 430 |
apply (tactic e) -- "XcptE" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
431 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
432 |
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
|
433 |
apply (simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
434 |
apply (simp (no_asm)) |
12517 | 435 |
apply (tactic e) -- "XcptE" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
436 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset
|
437 |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset
|
438 |
end |