Theory JSystemClasses

Up to index of Isabelle/HOL/verificard

(*  Title:      HOL/MicroJava/J/JSystemClasses.thy
    ID:         $Id: JSystemClasses.thy,v 1.1.2.1 2002/03/02 23:00:24 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{System Class Implementations (Java)} *}

theory JSystemClasses = WellForm:

text {*
  This theory provides source language implementations for the
  system class library. At the moment no system classes have any
  methods
*}

constdefs
  ObjectC :: "'c cdecl"
  "ObjectC \<equiv> ObjectC_decl []"

  NullPointerC :: "'c cdecl"
  "NullPointerC \<equiv> NullPointerC_decl []"

  ClassCastC :: "'c cdecl"
  "ClassCastC \<equiv> ClassCastC_decl []"

  OutOfMemoryC :: "'c cdecl"
  "OutOfMemoryC \<equiv> OutOfMemoryC_decl []"
  
  JSystemClasses :: "'c cdecl list"
  "JSystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"

lemmas SystemClassC_defs = SystemClass_decl_defs ObjectC_def 
                           NullPointerC_def OutOfMemoryC_def ClassCastC_def

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

lemma wf_syscls:
  "set JSystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
  apply (unfold wf_syscls_def SystemClasses_def JSystemClasses_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 []

  NullPointerC == NullPointerC_decl []

  OutOfMemoryC == OutOfMemoryC_decl []

  ClassCastC == ClassCastC_decl []

lemma fst_mono:

  A <= B ==> fst ` A <= fst ` B

lemma wf_syscls:

  set JSystemClasses <= set G ==> wf_syscls G