author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45827  66c68453455c 
child 58249  180f1b3508ed 
permissions  rwrr 
12517  1 
(* Title: HOL/MicroJava/J/Example.thy 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

2 
Author: David von Oheimb 
11372  3 
Copyright 1999 Technische Universitaet Muenchen 
11070  4 
*) 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

5 

12911  6 
header {* \isaheader{Example MicroJava Program} *} 
11070  7 

16417  8 
theory Example imports SystemClasses Eval begin 
11070  9 

10 
text {* 

11 
The following example MicroJava program includes: 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

12 
class declarations with inheritance, hiding of fields, and overriding of 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

13 
methods (with refined result type), 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

14 
instance creation, local assignment, sequential composition, 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

15 
method call with dynamic binding, literal values, 
11070  16 
expression statement, local access, type cast, field assignment (in part), 
17 
skip. 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

18 

11070  19 
\begin{verbatim} 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

20 
class Base { 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

21 
boolean vee; 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

22 
Base foo(Base x) {return x;} 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

23 
} 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

24 

10229  25 
class Ext extends Base { 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

26 
int vee; 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

27 
Ext foo(Base x) {((Ext)x).vee=1; return null;} 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

28 
} 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

29 

297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

30 
class Example { 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

31 
public static void main (String args[]) { 
9498  32 
Base e=new Ext(); 
33 
e.foo(null); 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

34 
} 
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

35 
} 
11070  36 
\end{verbatim} 
37 
*} 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

38 

24783  39 
datatype cnam' = Base'  Ext' 
40 
datatype vnam' = vee'  x'  e' 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

41 

45827  42 
text {* 
43 
@{text cnam'} and @{text vnam'} are intended to be isomorphic 

44 
to @{text cnam} and @{text vnam} 

45 
*} 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

46 

45827  47 
axiomatization cnam' :: "cnam' => cname" 
48 
where 

49 
inj_cnam': "(cnam' x = cnam' y) = (x = y)" and 

50 
surj_cnam': "\<exists>m. n = cnam' m" 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

51 

45827  52 
axiomatization vnam' :: "vnam' => vnam" 
53 
where 

54 
inj_vnam': "(vnam' x = vnam' y) = (x = y)" and 

24783  55 
surj_vnam': "\<exists>m. n = vnam' m" 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

56 

24783  57 
declare inj_cnam' [simp] inj_vnam' [simp] 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

58 

35102  59 
abbreviation Base :: cname 
60 
where "Base == cnam' Base'" 

61 
abbreviation Ext :: cname 

62 
where "Ext == cnam' Ext'" 

63 
abbreviation vee :: vname 

64 
where "vee == VName (vnam' vee')" 

65 
abbreviation x :: vname 

66 
where "x == VName (vnam' x')" 

67 
abbreviation e :: vname 

68 
where "e == VName (vnam' e')" 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

69 

45827  70 
axiomatization where 
71 
Base_not_Object: "Base \<noteq> Object" and 

72 
Ext_not_Object: "Ext \<noteq> Object" and 

73 
Base_not_Xcpt: "Base \<noteq> Xcpt z" and 

74 
Ext_not_Xcpt: "Ext \<noteq> Xcpt z" and 

12951  75 
e_not_This: "e \<noteq> This" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

76 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

77 
declare Base_not_Object [simp] Ext_not_Object [simp] 
12951  78 
declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp] 
11643
0b3a02daf7fb
Added axiom e~=This to reflect strengthened precond. in rule LAss
streckem
parents:
11372
diff
changeset

79 
declare e_not_This [simp] 
12951  80 
declare Base_not_Object [symmetric, simp] 
81 
declare Ext_not_Object [symmetric, simp] 

82 
declare Base_not_Xcpt [symmetric, simp] 

83 
declare Ext_not_Xcpt [symmetric, simp] 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

84 

297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

85 
consts 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

86 
foo_Base:: java_mb 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

87 
foo_Ext :: java_mb 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

88 
BaseC :: "java_mb cdecl" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

89 
ExtC :: "java_mb cdecl" 
12517  90 
test :: stmt 
91 
foo :: mname 

92 
a :: loc 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

93 
b :: loc 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

94 

297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

95 
defs 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

96 
foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

97 
BaseC_def:"BaseC == (Base, (Object, 
12517  98 
[(vee, PrimT Boolean)], 
99 
[((foo,[Class Base]),Class Base,foo_Base)]))" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

100 
foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext 
12517  101 
(LAcc x)..vee:=Lit (Intg Numeral1)), 
102 
Lit Null)" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

103 
ExtC_def: "ExtC == (Ext, (Base , 
12517  104 
[(vee, PrimT Integer)], 
105 
[((foo,[Class Base]),Class Ext,foo_Ext)]))" 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

106 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

107 
test_def:"test == Expr(e::=NewC Ext);; 
10763  108 
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

109 

297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

110 

20768  111 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

112 
NP :: xcpt where 
20768  113 
"NP == NullPointer" 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

114 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

115 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

116 
tprg ::"java_mb prog" where 
20768  117 
"tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]" 
118 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

119 
abbreviation 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

120 
obj1 :: obj where 
20768  121 
"obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))" 
9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

122 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

123 
abbreviation "s0 == Norm (empty, empty)" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset

124 
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

125 
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

126 
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

127 

24074  128 
lemmas map_of_Cons = map_of.simps(2) 
129 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

130 
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

131 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

132 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

133 
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

134 
apply (simp (no_asm_simp)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

135 
done 
12517  136 
declare map_of_Cons [simp del]  "sic!" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

137 

28524  138 
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

139 
apply (unfold ObjectC_def class_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

140 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

141 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

142 

12951  143 
lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])" 
144 
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) 

145 
apply (simp (no_asm)) 

146 
done 

147 

148 
lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])" 

149 
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) 

150 
apply (simp (no_asm)) 

151 
done 

152 

153 
lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])" 

154 
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def) 

155 
apply (simp (no_asm)) 

156 
done 

157 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

158 
lemma class_tprg_Base [simp]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

159 
"class tprg Base = Some (Object, 
12517  160 
[(vee, PrimT Boolean)], 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

161 
[((foo, [Class Base]), Class Base, foo_Base)])" 
12951  162 
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

163 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

164 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

165 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

166 
lemma class_tprg_Ext [simp]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

167 
"class tprg Ext = Some (Base, 
12517  168 
[(vee, PrimT Integer)], 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

169 
[((foo, [Class Base]), Class Ext, foo_Ext)])" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

170 
apply (unfold ObjectC_def BaseC_def ExtC_def class_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

171 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

172 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

173 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

174 
lemma not_Object_subcls [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ ==> R" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

175 
apply (auto dest!: tranclD subcls1D) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

176 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

177 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

178 
lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object" 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

179 
apply (erule rtrancl_induct) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

180 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

181 
apply (drule subcls1D) 
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 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

184 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

185 
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

186 
apply (auto dest!: tranclD subcls1D) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

187 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

188 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

189 
lemma class_tprgD: 
12951  190 
"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" 
191 
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

192 
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

193 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

194 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

195 
lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

196 
apply (auto dest!: tranclD subcls1D) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

197 
apply (frule class_tprgD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

198 
apply (auto dest!:) 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

199 
apply (drule rtranclD) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

200 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

201 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

202 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

203 
lemma unique_classes: "unique tprg" 
12951  204 
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

205 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

206 

45605  207 
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

208 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

209 
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

210 
apply (rule subcls_direct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

211 
apply auto 
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 
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

215 
apply (rule widen.subcls) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

216 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

217 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

218 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

219 
declare ty_expr_ty_exprs_wt_stmt.intros [intro!] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

220 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

221 
lemma acyclic_subcls1': "acyclic (subcls1 tprg)" 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

222 
apply (rule acyclicI) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

223 
apply safe 
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 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

226 
lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]] 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

227 

24783  228 
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

229 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

230 
lemma fields_Object [simp]: "fields (tprg, Object) = []" 
24783  231 
apply (subst fields_rec') 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

232 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

233 
done 
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 
declare is_class_def [simp] 
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_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]" 
24783  238 
apply (subst fields_rec') 
11026
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 
lemma fields_Ext [simp]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

243 
"fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

244 
apply (rule trans) 
24783  245 
apply (rule fields_rec') 
11026
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 

24783  249 
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

250 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

251 
lemma method_Object [simp]: "method (tprg,Object) = map_of []" 
24783  252 
apply (subst method_rec') 
11026
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 
lemma method_Base [simp]: "method (tprg, Base) = map_of 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

257 
[((foo, [Class Base]), Base, (Class Base, foo_Base))]" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

258 
apply (rule trans) 
24783  259 
apply (rule method_rec') 
11026
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_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

264 
[((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

265 
apply (rule trans) 
24783  266 
apply (rule method_rec') 
11026
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 wf_foo_Base: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

271 
"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

272 
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

273 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

274 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

275 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

276 
lemma wf_foo_Ext: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

277 
"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

278 
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

279 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

280 
apply (rule ty_expr_ty_exprs_wt_stmt.Cast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

281 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

282 
apply (simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

283 
apply (rule_tac [2] cast.subcls) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

284 
apply (unfold field_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

285 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

286 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

287 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

288 
lemma wf_ObjectC: 
14045  289 
"ws_cdecl tprg ObjectC \<and> 
290 
wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC" 

291 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

292 
wf_mrT_def wf_fdecl_def ObjectC_def) 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

293 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

294 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

295 

12951  296 
lemma wf_NP: 
14045  297 
"ws_cdecl tprg NullPointerC \<and> 
298 
wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC" 

299 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

300 
wf_mrT_def wf_fdecl_def NullPointerC_def) 

12951  301 
apply (simp add: class_def) 
302 
apply (fold NullPointerC_def class_def) 

303 
apply auto 

304 
done 

305 

306 
lemma wf_OM: 

14045  307 
"ws_cdecl tprg OutOfMemoryC \<and> 
308 
wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC" 

309 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

310 
wf_mrT_def wf_fdecl_def OutOfMemoryC_def) 

12951  311 
apply (simp add: class_def) 
312 
apply (fold OutOfMemoryC_def class_def) 

313 
apply auto 

314 
done 

315 

316 
lemma wf_CC: 

14045  317 
"ws_cdecl tprg ClassCastC \<and> 
318 
wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC" 

319 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

320 
wf_mrT_def wf_fdecl_def ClassCastC_def) 

12951  321 
apply (simp add: class_def) 
322 
apply (fold ClassCastC_def class_def) 

323 
apply auto 

324 
done 

325 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

326 
lemma wf_BaseC: 
14045  327 
"ws_cdecl tprg BaseC \<and> 
328 
wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC" 

329 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

330 
wf_mrT_def wf_fdecl_def BaseC_def) 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

331 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

332 
apply (fold BaseC_def) 
14045  333 
apply (rule mp) defer apply (rule wf_foo_Base) 
334 
apply (auto simp add: wf_mdecl_def) 

335 
done 

336 

337 

338 
lemma wf_ExtC: 

339 
"ws_cdecl tprg ExtC \<and> 

340 
wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC" 

341 
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 

342 
wf_mrT_def wf_fdecl_def ExtC_def) 

343 
apply (simp (no_asm)) 

344 
apply (fold ExtC_def) 

345 
apply (rule mp) defer apply (rule wf_foo_Ext) 

346 
apply (auto simp add: wf_mdecl_def) 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
28524
diff
changeset

347 
apply (drule rtranclD) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

348 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

349 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

350 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

351 

12951  352 
lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) 
353 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

354 
lemma wf_tprg: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

355 
"wf_prog wf_java_mdecl tprg" 
14045  356 
apply (unfold wf_prog_def ws_prog_def Let_def) 
12951  357 
apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes) 
358 
apply (rule wf_syscls) 

359 
apply (simp add: SystemClasses_def) 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

360 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

361 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

362 
lemma appl_methds_foo_Base: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

363 
"appl_methds tprg Base (foo, [NT]) = 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

364 
{((Class Base, Class Base), [Class Base])}" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

365 
apply (unfold appl_methds_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

366 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

367 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

368 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

369 
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

370 
{((Class Base, Class Base), [Class Base])}" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

371 
apply (unfold max_spec_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

372 
apply (auto simp add: appl_methds_foo_Base) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

373 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

374 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset

375 
ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *} 
36319  376 
schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

377 
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>" 
12517  378 
apply (tactic t)  ";;" 
379 
apply (tactic t)  "Expr" 

380 
apply (tactic t)  "LAss" 

381 
apply simp  {* @{text "e \<noteq> This"} *} 

382 
apply (tactic t)  "LAcc" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

383 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

384 
apply (simp (no_asm)) 
12517  385 
apply (tactic t)  "NewC" 
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)  "Expr" 
389 
apply (tactic t)  "Call" 

390 
apply (tactic t)  "LAcc" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

391 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

392 
apply (simp (no_asm)) 
12517  393 
apply (tactic t)  "Cons" 
394 
apply (tactic t)  "Lit" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

395 
apply (simp (no_asm)) 
12517  396 
apply (tactic t)  "Nil" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

397 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

398 
apply (rule max_spec_foo_Base) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

399 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

400 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset

401 
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

402 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

403 
declare split_if [split del] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

404 
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp] 
36319  405 
schematic_lemma exec_test: 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

406 
" [new_Addr (heap (snd s0)) = (a, None)] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

407 
tprg\<turnstile>s0 test> ?s" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

408 
apply (unfold test_def) 
12517  409 
 "?s = s3 " 
410 
apply (tactic e)  ";;" 

411 
apply (tactic e)  "Expr" 

412 
apply (tactic e)  "LAss" 

413 
apply (tactic e)  "NewC" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

414 
apply force 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

415 
apply force 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

416 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

417 
apply (erule thin_rl) 
12517  418 
apply (tactic e)  "Expr" 
419 
apply (tactic e)  "Call" 

420 
apply (tactic e)  "LAcc" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

421 
apply force 
12517  422 
apply (tactic e)  "Cons" 
423 
apply (tactic e)  "Lit" 

424 
apply (tactic e)  "Nil" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

425 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

426 
apply (force simp add: foo_Ext_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

427 
apply (simp (no_asm)) 
12517  428 
apply (tactic e)  "Expr" 
429 
apply (tactic e)  "FAss" 

430 
apply (tactic e)  "Cast" 

431 
apply (tactic e)  "LAcc" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

432 
apply (simp (no_asm)) 
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 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

437 
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

438 
apply (simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

439 
apply (simp (no_asm)) 
12517  440 
apply (tactic e)  "XcptE" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

441 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

442 

9346
297dcbf64526
restructuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
diff
changeset

443 
end 