Theory ClassRel

(*  Title:       CoreC++

    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹The subclass relation›

theory ClassRel imports Decl begin


― ‹direct repeated subclass›
inductive_set
  subclsR :: "prog ⇒ (cname × cname) set"
  and subclsR' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇩R _" [71,71,71] 70)
  for P :: prog
where
  "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›
inductive_set
  subclsS :: "prog ⇒ (cname × cname) set"
  and subclsS' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇩S _" [71,71,71] 70)
  for P :: prog
where
  "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›
inductive_set
  subcls1 :: "prog ⇒ (cname × cname) set"
  and subcls1' :: "prog ⇒ [cname, cname] ⇒ bool" ("_ ⊢ _ ≺⇧1 _" [71,71,71] 70)
  for P :: prog
where
  "P ⊢ C ≺⇧1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "⟦class P C = Some (Bs,rest); D ∈  baseClasses Bs⟧ ⟹ P ⊢ C ≺⇧1 D"

abbreviation
  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)
done


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)

end