Theory ClassRel

(*  Title:       CoreC++

    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at>

    Based on the Jinja theory Common/TypeRel.thy by Tobias Nipkow

section ‹The subclass relation›

theory ClassRel imports Decl begin

― ‹direct repeated subclass›
  subclsR :: "prog  (cname × cname) set"
  and subclsR' :: "prog  [cname, cname]  bool" ("_  _ R _" [71,71,71] 70)
  for P :: prog
  "P  C R D  (C,D)  subclsR P"
| subclsRI: "class P C = Some (Bs,rest); Repeats(D)  set Bs  P  C R D"

― ‹direct shared subclass›
  subclsS :: "prog  (cname × cname) set"
  and subclsS' :: "prog  [cname, cname]  bool" ("_  _ S _" [71,71,71] 70)
  for P :: prog
  "P  C S D  (C,D)  subclsS P"
| subclsSI: "class P C = Some (Bs,rest); Shares(D)  set Bs  P  C S D"

 ― ‹direct subclass›
  subcls1 :: "prog  (cname × cname) set"
  and subcls1' :: "prog  [cname, cname]  bool" ("_  _ 1 _" [71,71,71] 70)
  for P :: prog
  "P  C 1 D  (C,D)  subcls1 P"
| subcls1I: "class P C = Some (Bs,rest); D   baseClasses Bs  P  C 1 D"

  subcls    :: "prog  [cname, cname]  bool" ("_  _ * _"  [71,71,71] 70) where
  "P  C * D  (C,D)  (subcls1 P)*"

lemma subclsRD:
  "P  C R D  fs ms Bs. (class P C = Some (Bs,fs,ms))  (Repeats(D)  set Bs)"
by(auto elim: subclsR.cases)

lemma subclsSD:
  "P  C S D  fs ms Bs. (class P C = Some (Bs,fs,ms))  (Shares(D)  set Bs)"
by(auto elim: subclsS.cases)

lemma subcls1D:
  "P  C 1 D  fs ms Bs. (class P C = Some (Bs,fs,ms))  (D  baseClasses Bs)"
by(auto elim: subcls1.cases)

lemma subclsR_subcls1:
  "P  C R D  P  C 1 D"
by (auto elim!:subclsR.cases intro:subcls1I simp:RepBaseclass_isBaseclass)

lemma subclsS_subcls1:
  "P  C S D  P  C 1 D"
by (auto elim!:subclsS.cases intro:subcls1I simp:ShBaseclass_isBaseclass)

lemma subcls1_subclsR_or_subclsS:
  "P  C 1 D  P  C R D  P  C S D"
by (auto dest!:subcls1D intro:subclsRI 
  dest:baseClasses_repeats_or_shares subclsSI)

lemma finite_subcls1: "finite (subcls1 P)"

apply(subgoal_tac "subcls1 P = (SIGMA C: {C. is_class P C} . 
                     {D. D  baseClasses (fst(the(class P C)))})")
 prefer 2
 apply(fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
apply simp
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "baseClasses (fst (the (class P C)))" in finite_subset)
apply (auto intro:finite_baseClasses simp:is_class_def)

lemma finite_subclsR: "finite (subclsR P)"
by(rule_tac B = "subcls1 P" in finite_subset, 
  auto simp:subclsR_subcls1 finite_subcls1)

lemma finite_subclsS: "finite (subclsS P)"
by(rule_tac B = "subcls1 P" in finite_subset, 
  auto simp:subclsS_subcls1 finite_subcls1)

lemma subcls1_class:
  "P  C 1 D  is_class P C"
by (auto dest:subcls1D simp:is_class_def)

lemma subcls_is_class:
"P  D * C; is_class P C  is_class P D"
by (induct rule:rtrancl_induct,auto dest:subcls1_class)