Theory SystemClasses

Up to index of Isabelle/HOL/objinit

(*  Title:      HOL/MicroJava/J/SystemClasses.thy
    ID:         $Id: SystemClasses.html,v 1.1 2002/11/28 14:12:09 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{System Classes} *}

theory SystemClasses = Decl:

text {*
  This theory provides definitions for the @{text Object} class,
  and the system exceptions. It leaves methods empty (to be instantiated
  later).
*}

constdefs
  ObjectC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ObjectC_decl ms \<equiv> (Object, (arbitrary,[],ms))"

  NullPointerC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "NullPointerC_decl ms \<equiv> (Xcpt NullPointer, (Object,[],ms))"

  ClassCastC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ClassCastC_decl ms \<equiv> (Xcpt ClassCast, (Object,[],ms))"

  OutOfMemoryC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "OutOfMemoryC_decl ms \<equiv> (Xcpt OutOfMemory, (Object,[],ms))"
  
  SystemClasses :: "cname list"
  "SystemClasses \<equiv> [Object, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory]"

lemmas SystemClass_decl_defs = ObjectC_decl_def NullPointerC_decl_def 
                               ClassCastC_decl_def OutOfMemoryC_decl_def

end

lemmas SystemClass_decl_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)