Prog.thy

Back to the index of Bali_ASCII
(*  Title:      isabelle/Bali/Prog.thy
    ID:         $Id: Prog.thy,v 1.2 1997/10/22 12:00:09 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Whole Java programs

simplifications:
* no packages
* no main method yet

*)

Prog = Decl +

types prog = "idecl list * cdecl list"

consts

  iface		:: "prog => (tname, iface) table"
  class		:: "prog => (tname, class) table"

  is_iface	:: "prog => tname => bool"
  is_class	:: "prog => tname => bool"
  is_type	:: "prog => ty set"
syntax
  is_type	:: "prog => ty    => bool"
translations
 "is_type G T" == "T : is_type G"

defs

  iface_def	"iface        == table  o  fst"
  class_def	"class        == table  o  snd"

  is_iface_def	"is_iface G I == iface G I ~= None"
  is_class_def	"is_class G C == class G C ~= None"

inductive "is_type G" intrs (*####primrec?*)

  prim			     "is_type G (PrimT pt)"
  null			     "is_type G (RefT  NullT)"
  iface	"is_iface G tname ==> is_type G (Iface tname)"
  class	"is_class G tname ==> is_type G (Class tname)"
  array	"is_type  G T     ==> is_type G (T[.])"

end