Theory Decl

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Class Declarations and Programs›

theory Decl imports Expr begin


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


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


definition "class" :: "prog ⇒ cname ⇀ class" where
  "class ≡ map_of"

definition is_class :: "prog ⇒ cname ⇒ bool" where
  "is_class P C ≡ class P C ≠ None"

definition baseClasses :: "base list ⇒ cname set" where
  "baseClasses Bs ≡ set ((map getbase) Bs)"

definition RepBases :: "base list ⇒ cname set" where
  "RepBases Bs ≡ set ((map getbase) (filter isRepBase Bs))"

definition SharedBases :: "base list ⇒ cname set" where
  "SharedBases Bs ≡ set ((map getbase) (filter isShBase Bs))"


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

lemma not_getbase_shares:
  "D ∉ set (map getbase xs) ⟹ Shares D ∉ set xs"
by (induct rule: list.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: list.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: list.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



definition is_type :: "prog ⇒ ty ⇒ bool" where
  "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