Up to index of Isabelle/HOL/arrays
theory JVMSystemClasses = WellForm + JVMExec:(* Title: HOL/MicroJava/JVM/JVMSystemClasses.thy
ID: $Id: JVMSystemClasses.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Gerwin Klein
Copyright 2002 Technische Universitaet Muenchen
*)
header {* \isaheader{System Class Implementations (JVM)} *}
theory JVMSystemClasses = WellForm + JVMExec:
text {*
This theory provides bytecode implementations for the
system class library. Each class has a default constructor.
*}
constdefs
Object_ctor :: "jvm_method mdecl"
"Object_ctor \<equiv> ((init, []), PrimT Void, (1, 0, [LitPush Unit, Return], []))"
ObjectC :: "jvm_method cdecl"
"ObjectC \<equiv> ObjectC_decl [Object_ctor]"
Default_ctor :: "jvm_method mdecl"
"Default_ctor \<equiv>
((init, []), PrimT Void, (1,0,[Load 0, Invoke_special Object init [], Return], []))"
NullPointerC :: "jvm_method cdecl"
"NullPointerC \<equiv> NullPointerC_decl [Default_ctor]"
ClassCastC :: "jvm_method cdecl"
"ClassCastC \<equiv> ClassCastC_decl [Default_ctor]"
OutOfMemoryC :: "jvm_method cdecl"
"OutOfMemoryC \<equiv> OutOfMemoryC_decl [Default_ctor]"
NegativeArraySizeC :: "jvm_method cdecl"
"NegativeArraySizeC \<equiv> NegativeArraySizeC_decl [Default_ctor]"
ArrayIndexOutOfBoundsC :: "jvm_method cdecl"
"ArrayIndexOutOfBoundsC \<equiv> ArrayIndexOutOfBoundsC_decl [Default_ctor]"
ArrayStoreC :: "jvm_method cdecl"
"ArrayStoreC \<equiv> ArrayStoreC_decl [Default_ctor]"
JVMSystemClasses :: "jvm_method cdecl list"
"JVMSystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC, NegativeArraySizeC, ArrayIndexOutOfBoundsC, ArrayStoreC]"
lemmas SystemClassC_defs =
SystemClass_decl_defs ObjectC_def NullPointerC_def
OutOfMemoryC_def ClassCastC_def NegativeArraySizeC_def
ArrayStoreC_def ArrayIndexOutOfBoundsC_def Default_ctor_def Object_ctor_def
lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
locale sys_classes =
fixes G :: jvm_prog
assumes set: "set JVMSystemClasses \<subseteq> set G"
assumes unique: "unique G"
assumes wf: "wf ((subcls1 G)¯)"
notes fields_rec = fields_rec_lemma [OF _ wf]
notes method_rec = method_rec_lemma [OF _ wf]
lemma (in sys_classes) class_Object [simp]:
"class G Object = Some (arbitrary, [], [Object_ctor])"
proof -
from set have "(Object, arbitrary, [], [Object_ctor]) \<in> set G"
by (auto simp add: JVMSystemClasses_def ObjectC_def ObjectC_decl_def)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) fields_Object [simp]:
shows "fields (G,Object) = []"
proof -
from wf
show ?thesis by (unfold fields_def) (simp add: class_rec.simps)
qed
lemma (in sys_classes) wf_syscls [simp]:
"wf_syscls G"
apply (insert set)
apply (unfold wf_syscls_def SystemClasses_def JVMSystemClasses_def SystemClassC_defs)
apply (drule fst_mono)
apply simp
done
lemma (in sys_classes) class_NullPointer [simp]:
"class G (Xcpt NullPointer) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) class_OutOfMemory [simp]:
"class G (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) class_ClassCast [simp]:
"class G (Xcpt ClassCast) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) class_ArrayStore [simp]:
"class G (Xcpt ArrayStore) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) class_NegativeArraySize [simp]:
"class G (Xcpt NegativeArraySize) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) class_ArrayIndexOutOfBounds [simp]:
"class G (Xcpt ArrayIndexOutOfBounds) = Some (Object, [], [Default_ctor])"
(is "class G ?C = Some ?D")
proof -
from set have "(?C, ?D) \<in> set G"
by (auto simp add: JVMSystemClasses_def SystemClassC_defs)
with unique show ?thesis by (simp add: class_def map_of_SomeI)
qed
lemma (in sys_classes) fields_NullPointer [simp]:
"fields (G, Xcpt NullPointer) = []"
by (simp add: fields_rec [OF class_NullPointer])
lemma (in sys_classes) fields_ClassCast [simp]:
"fields (G, Xcpt ClassCast) = []"
by (simp add: fields_rec [OF class_ClassCast])
lemma (in sys_classes) fields_OutOfMemory [simp]:
"fields (G, Xcpt OutOfMemory) = []"
by (simp add: fields_rec [OF class_OutOfMemory])
lemma (in sys_classes) fields_ArrayIndexOutOfBounds [simp]:
"fields (G, Xcpt ArrayIndexOutOfBounds) = []"
by (simp add: fields_rec [OF class_ArrayIndexOutOfBounds])
lemma (in sys_classes) fields_NegativeArraySize [simp]:
"fields (G, Xcpt NegativeArraySize) = []"
by (simp add: fields_rec [OF class_NegativeArraySize])
lemma (in sys_classes) fields_ArrayStore [simp]:
"fields (G, Xcpt ArrayStore) = []"
by (simp add: fields_rec [OF class_ArrayStore])
lemma (in sys_classes) method_Object [simp]:
"method (G, Object) sig =
(if sig = (init,[]) then Some (Object, snd Object_ctor) else None)"
by (auto simp add: method_rec_lemma [OF class_Object wf] Object_ctor_def)
lemma (in sys_classes) method_NullPointer [simp]:
"method (G, Xcpt NullPointer) sig =
(if sig = (init,[]) then Some (Xcpt NullPointer, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_NullPointer] Default_ctor_def)
lemma (in sys_classes) method_ClassCast [simp]:
"method (G, Xcpt ClassCast) sig =
(if sig = (init,[]) then Some (Xcpt ClassCast, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_ClassCast] Default_ctor_def)
lemma (in sys_classes) method_OutOfMemory [simp]:
"method (G, Xcpt OutOfMemory) sig =
(if sig = (init,[]) then Some (Xcpt OutOfMemory, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_OutOfMemory] Default_ctor_def)
lemma (in sys_classes) method_ArrayIndexOutOfBounds [simp]:
"method (G, Xcpt ArrayIndexOutOfBounds) sig =
(if sig = (init,[]) then Some (Xcpt ArrayIndexOutOfBounds, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_ArrayIndexOutOfBounds] Default_ctor_def)
lemma (in sys_classes) method_NegativeArraySize [simp]:
"method (G, Xcpt NegativeArraySize) sig =
(if sig = (init,[]) then Some (Xcpt NegativeArraySize, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_NegativeArraySize] Default_ctor_def)
lemma (in sys_classes) method_ArrayStore [simp]:
"method (G, Xcpt ArrayStore) sig =
(if sig = (init,[]) then Some (Xcpt ArrayStore, snd Default_ctor) else None)"
by (auto simp add: method_rec [OF class_ArrayStore] Default_ctor_def)
lemmas sys_lemmas =
sys_classes.fields_Object
sys_classes.class_Object
sys_classes.wf_syscls
sys_classes.class_NullPointer
sys_classes.class_OutOfMemory
sys_classes.class_ClassCast
sys_classes.class_ArrayStore
sys_classes.class_NegativeArraySize
sys_classes.class_ArrayIndexOutOfBounds
sys_classes.fields_NullPointer
sys_classes.fields_ClassCast
sys_classes.fields_OutOfMemory
sys_classes.fields_ArrayIndexOutOfBounds
sys_classes.fields_NegativeArraySize
sys_classes.fields_ArrayStore
sys_classes.method_Object
sys_classes.method_NullPointer
sys_classes.method_ClassCast
sys_classes.method_OutOfMemory
sys_classes.method_ArrayIndexOutOfBounds
sys_classes.method_NegativeArraySize
sys_classes.method_ArrayStore
end
lemmas SystemClassC_defs:
ObjectC_decl ms == (Object, arbitrary, [], ms)
NullPointerC_decl ms == (Xcpt NullPointer, Object, [], ms)
ClassCastC_decl ms == (Xcpt ClassCast, Object, [], ms)
OutOfMemoryC_decl ms == (Xcpt OutOfMemory, Object, [], ms)
ArrayIndexOutOfBoundsC_decl ms == (Xcpt ArrayIndexOutOfBounds, Object, [], ms)
NegativeArraySizeC_decl ms == (Xcpt NegativeArraySize, Object, [], ms)
ArrayStoreC_decl ms == (Xcpt ArrayStore, Object, [], ms)
ObjectC == ObjectC_decl [Object_ctor]
NullPointerC == NullPointerC_decl [Default_ctor]
OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]
ClassCastC == ClassCastC_decl [Default_ctor]
NegativeArraySizeC == NegativeArraySizeC_decl [Default_ctor]
ArrayStoreC == ArrayStoreC_decl [Default_ctor]
ArrayIndexOutOfBoundsC == ArrayIndexOutOfBoundsC_decl [Default_ctor]
Default_ctor == ((init, []), PrimT Void, 1, 0, [Load 0, Invoke_special Object init [], Return], [])
Object_ctor == ((init, []), PrimT Void, 1, 0, [LitPush Unit, Return], [])
lemma fst_mono:
A <= B ==> fst ` A <= fst ` B
lemma class_Object:
sys_classes G ==> class G Object = Some (arbitrary, [], [Object_ctor])
lemma
sys_classes G ==> fields (G, Object) = []
lemma wf_syscls:
sys_classes G ==> wf_syscls G
lemma class_NullPointer:
sys_classes G ==> class G (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
lemma class_OutOfMemory:
sys_classes G ==> class G (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
lemma class_ClassCast:
sys_classes G ==> class G (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
lemma class_ArrayStore:
sys_classes G ==> class G (Xcpt ArrayStore) = Some (Object, [], [Default_ctor])
lemma class_NegativeArraySize:
sys_classes G ==> class G (Xcpt NegativeArraySize) = Some (Object, [], [Default_ctor])
lemma class_ArrayIndexOutOfBounds:
sys_classes G ==> class G (Xcpt ArrayIndexOutOfBounds) = Some (Object, [], [Default_ctor])
lemma fields_NullPointer:
sys_classes G ==> fields (G, Xcpt NullPointer) = []
lemma fields_ClassCast:
sys_classes G ==> fields (G, Xcpt ClassCast) = []
lemma fields_OutOfMemory:
sys_classes G ==> fields (G, Xcpt OutOfMemory) = []
lemma fields_ArrayIndexOutOfBounds:
sys_classes G ==> fields (G, Xcpt ArrayIndexOutOfBounds) = []
lemma fields_NegativeArraySize:
sys_classes G ==> fields (G, Xcpt NegativeArraySize) = []
lemma fields_ArrayStore:
sys_classes G ==> fields (G, Xcpt ArrayStore) = []
lemma method_Object:
sys_classes G
==> method (G, Object) sig =
(if sig = (init, []) then Some (Object, snd Object_ctor) else None)
lemma method_NullPointer:
sys_classes G
==> method (G, Xcpt NullPointer) sig =
(if sig = (init, []) then Some (Xcpt NullPointer, snd Default_ctor)
else None)
lemma method_ClassCast:
sys_classes G
==> method (G, Xcpt ClassCast) sig =
(if sig = (init, []) then Some (Xcpt ClassCast, snd Default_ctor) else None)
lemma method_OutOfMemory:
sys_classes G
==> method (G, Xcpt OutOfMemory) sig =
(if sig = (init, []) then Some (Xcpt OutOfMemory, snd Default_ctor)
else None)
lemma method_ArrayIndexOutOfBounds:
sys_classes G
==> method (G, Xcpt ArrayIndexOutOfBounds) sig =
(if sig = (init, [])
then Some (Xcpt ArrayIndexOutOfBounds, snd Default_ctor) else None)
lemma method_NegativeArraySize:
sys_classes G
==> method (G, Xcpt NegativeArraySize) sig =
(if sig = (init, []) then Some (Xcpt NegativeArraySize, snd Default_ctor)
else None)
lemma method_ArrayStore:
sys_classes G
==> method (G, Xcpt ArrayStore) sig =
(if sig = (init, []) then Some (Xcpt ArrayStore, snd Default_ctor)
else None)
lemmas sys_lemmas:
sys_classes G ==> fields (G, Object) = []
sys_classes G ==> class G Object = Some (arbitrary, [], [Object_ctor])
sys_classes G ==> wf_syscls G
sys_classes G ==> class G (Xcpt NullPointer) = Some (Object, [], [Default_ctor])
sys_classes G ==> class G (Xcpt OutOfMemory) = Some (Object, [], [Default_ctor])
sys_classes G ==> class G (Xcpt ClassCast) = Some (Object, [], [Default_ctor])
sys_classes G ==> class G (Xcpt ArrayStore) = Some (Object, [], [Default_ctor])
sys_classes G ==> class G (Xcpt NegativeArraySize) = Some (Object, [], [Default_ctor])
sys_classes G ==> class G (Xcpt ArrayIndexOutOfBounds) = Some (Object, [], [Default_ctor])
sys_classes G ==> fields (G, Xcpt NullPointer) = []
sys_classes G ==> fields (G, Xcpt ClassCast) = []
sys_classes G ==> fields (G, Xcpt OutOfMemory) = []
sys_classes G ==> fields (G, Xcpt ArrayIndexOutOfBounds) = []
sys_classes G ==> fields (G, Xcpt NegativeArraySize) = []
sys_classes G ==> fields (G, Xcpt ArrayStore) = []
sys_classes G
==> method (G, Object) sig =
(if sig = (init, []) then Some (Object, snd Object_ctor) else None)
sys_classes G
==> method (G, Xcpt NullPointer) sig =
(if sig = (init, []) then Some (Xcpt NullPointer, snd Default_ctor)
else None)
sys_classes G
==> method (G, Xcpt ClassCast) sig =
(if sig = (init, []) then Some (Xcpt ClassCast, snd Default_ctor) else None)
sys_classes G
==> method (G, Xcpt OutOfMemory) sig =
(if sig = (init, []) then Some (Xcpt OutOfMemory, snd Default_ctor)
else None)
sys_classes G
==> method (G, Xcpt ArrayIndexOutOfBounds) sig =
(if sig = (init, [])
then Some (Xcpt ArrayIndexOutOfBounds, snd Default_ctor) else None)
sys_classes G
==> method (G, Xcpt NegativeArraySize) sig =
(if sig = (init, []) then Some (Xcpt NegativeArraySize, snd Default_ctor)
else None)
sys_classes G
==> method (G, Xcpt ArrayStore) sig =
(if sig = (init, []) then Some (Xcpt ArrayStore, snd Default_ctor)
else None)