# Theory Decl

Up to index of Isabelle/HOL/MicroJava

theory Decl
imports Type
begin

    (*  Title:      HOL/MicroJava/J/Decl.thy
        ID:         $Id: Decl.thy,v 1.13 2005/06/17 14:13:09 haftmann Exp $
        Author:     David von Oheimb
        Copyright   1999 Technische Universitaet Muenchen
    *)

    header {* \isaheader{Class Declarations and Programs} *}

    theory Decl imports Type begin

    types
      fdecl    = "vname × ty"        -- "field declaration, cf. 8.3 (, 9.3)"

      sig      = "mname × ty list"   -- "signature of a method, cf. 8.4.2"

      'c mdecl = "sig × ty × 'c"     -- "method declaration in a class"

      'c class = "cname × fdecl list × 'c mdecl list"
      -- "class = superclass, fields, methods"

      'c cdecl = "cname × 'c class"  -- "class declaration, cf. 8.1"

      'c prog  = "'c cdecl list"     -- "program"

    translations
      "fdecl"   <= (type) "vname × ty"
      "sig"     <= (type) "mname × ty list"
      "mdecl c" <= (type) "sig × ty × c"
      "class c" <= (type) "cname × fdecl list × (c mdecl) list"
      "cdecl c" <= (type) "cname × (c class)"
      "prog  c" <= (type) "(c cdecl) list"

    constdefs
      class :: "'c prog => (cname \<rightharpoonup> 'c class)"
      "class ≡ map_of"

      is_class :: "'c prog => cname => bool"
      "is_class G C ≡ class G C ≠ None"

    lemma finite_is_class: "finite {C. is_class G C}"
    apply (unfold is_class_def class_def)
    apply (fold dom_def)
    apply (rule finite_dom_map_of)
    done

    consts
      is_type :: "'c prog => ty    => bool"
    primrec
      "is_type G (PrimT pt) = True"
      "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"

    end

lemma finite_is_class:

      finite {C. is_class G C}