Theory Decl

(*  Title:       CoreC++
    ID:          $Id: Decl.thy,v 1.13 2008-06-25 18:29:54 makarius Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Based on the Jinja theory Common/Decl.thy by David von Oheimb
*)

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

theory Decl imports Expr begin


types
  fdecl    = "vname × ty"                        -- "field declaration"
  method = "ty list × ty × (vname list × expr)"    -- {* arg.\ types, return type, params, body *}
  mdecl = "mname × method"                         -- "method declaration"
  "class" = "base list × fdecl list × mdecl list"  -- "class = superclasses, fields, methods"
  cdecl = "cname × class"                        -- "classa declaration"
  prog  = "cdecl list"                           -- "program"


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


constdefs
  "class" :: "prog => cname \<rightharpoonup> class"
  "class ≡ map_of"

  is_class :: "prog => cname => bool"
  "is_class P C ≡ class P C ≠ None"

  baseClasses :: "base list => cname set"
  "baseClasses Bs ≡ set ((map getbase) Bs)"

  RepBases :: "base list => cname set"
  "RepBases Bs ≡ set ((map getbase) (filter isRepBase Bs))"

  SharedBases :: "base list => cname set"
  "SharedBases Bs ≡ set ((map getbase) (filter isShBase Bs))"


lemma not_getbase_repeats:
  "D ∉ set (map getbase xs) ==> Repeats D ∉ set xs"
by (induct rule:set.induct, auto)

lemma not_getbase_shares:
  "D ∉ set (map getbase xs) ==> Shares D ∉ set xs"
by (induct rule:set.induct, auto)


lemma RepBaseclass_isBaseclass:
  "[|class P C = Some(Bs,fs,ms); Repeats D ∈ set Bs|]
==> D ∈ baseClasses Bs"
by (simp add:baseClasses_def, induct rule:set.induct, 
  auto simp:not_getbase_repeats)

lemma ShBaseclass_isBaseclass:
  "[|class P C = Some(Bs,fs,ms); Shares D ∈ set Bs|]
==> D ∈ baseClasses Bs"
by (simp add:baseClasses_def, induct rule:set.induct, 
  auto simp:not_getbase_shares)

lemma base_repeats_or_shares:
  "[|B ∈ set Bs; D = getbase B|] 
==> Repeats D ∈ set Bs ∨ Shares D ∈ set Bs"
by(induct B rule:base.induct) simp+

lemma baseClasses_repeats_or_shares:
  "D ∈ baseClasses Bs ==> Repeats D ∈ set Bs ∨ Shares D ∈ set Bs"
by (auto elim!:bexE base_repeats_or_shares 
  simp add:baseClasses_def image_def)


lemma finite_is_class: "finite {C. is_class P C}"

apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done


lemma finite_baseClasses: 
  "class P C = Some(Bs,fs,ms) ==> finite (baseClasses Bs)"

apply (unfold is_class_def class_def baseClasses_def)
apply clarsimp
done



constdefs
  is_type :: "prog => ty => bool"
  "is_type P T  ≡
  (case T of Void => True | Boolean => True | Integer => True | NT => True
   | Class C => is_class P C)"

lemma is_type_simps [simp]:
  "is_type P Void ∧ is_type P Boolean ∧ is_type P Integer ∧
  is_type P NT ∧ is_type P (Class C) = is_class P C"
by(simp add:is_type_def)

abbreviation
  "types P == Collect (CONST is_type P)"

lemma typeof_lit_is_type: 
  "typeof v = Some T ==> is_type P T"
 by (induct v) (auto)


end