Theory JVMSystemClasses

Up to index of Isabelle/HOL/jsr

(*  Title:      HOL/MicroJava/JVM/JVMSystemClasses.thy
    ID:         $Id: JVMSystemClasses.html,v 1.1 2002/11/28 14:17:20 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]"
  
  JVMSystemClasses :: "jvm_method cdecl list"
  "JVMSystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"

lemmas SystemClassC_defs = SystemClass_decl_defs ObjectC_def NullPointerC_def
  OutOfMemoryC_def ClassCastC_def Default_ctor_def Object_ctor_def

lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast

lemma wf_syscls:
  "set JVMSystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
  apply (unfold wf_syscls_def SystemClasses_def JVMSystemClasses_def SystemClassC_defs)
  apply (drule fst_mono)
  apply simp    
  done 

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)

  ObjectC == ObjectC_decl [Object_ctor]

  NullPointerC == NullPointerC_decl [Default_ctor]

  OutOfMemoryC == OutOfMemoryC_decl [Default_ctor]

  ClassCastC == ClassCastC_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 wf_syscls:

  set JVMSystemClasses <= set G ==> wf_syscls G