products/Sources/formale Sprachen/Coq/test-suite/misc/deps/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Decl.thy   Sprache: Unknown

(*  Title:      HOL/MicroJava/J/Decl.thy
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section \<open>Class Declarations and Programs\<close>

theory Decl imports Type begin

type_synonym 
  fdecl    = "vname \ ty" \ \field declaration, cf. 8.3 (, 9.3)\

type_synonym
  sig      = "mname \ ty list" \ \signature of a method, cf. 8.4.2\

type_synonym
  'c mdecl = "sig \ ty \ 'c" \ \method declaration in a class\

type_synonym
  'c "class" = "cname \ fdecl list \ 'c mdecl list"
  \<comment> \<open>class = superclass, fields, methods\<close>

type_synonym
  'c cdecl = "cname \ 'c class" \ \class declaration, cf. 8.1\

type_synonym
  'c prog = "'c cdecl list" \ \program\


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


definition "class" :: "'c prog => (cname \ 'c class)" where
  "class \ map_of"

definition is_class :: "'c prog => cname => bool" where
  "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

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

end

[ zur Elbe Produktseite wechseln0.0Quellennavigators  Analyse erneut starten  ]