Theory ClassRel

(*  Title:       CoreC++
    ID:          $Id: ClassRel.thy,v 1.8 2007-07-11 10:07:48 stefanberghofer Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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


header {* \isaheader{The subclass relation} *}

theory ClassRel imports Decl begin


-- "direct repeated subclass"
inductive_set
  subclsR :: "prog => (cname × cname) set"
  and subclsR' :: "prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>R _" [71,71,71] 70)
  for P :: prog
where
  "P \<turnstile> C \<prec>R D ≡ (C,D) ∈ subclsR P"
| subclsRI: "[|class P C = Some (Bs,rest); Repeats(D) ∈ set Bs|] ==> P \<turnstile> C \<prec>R D"

-- "direct shared subclass"
inductive_set
  subclsS :: "prog => (cname × cname) set"
  and subclsS' :: "prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>S _" [71,71,71] 70)
  for P :: prog
where
  "P \<turnstile> C \<prec>S D ≡ (C,D) ∈ subclsS P"
| subclsSI: "[|class P C = Some (Bs,rest); Shares(D) ∈ set Bs|] ==> P \<turnstile> C \<prec>S D"

 -- "direct subclass"
inductive_set
  subcls1 :: "prog => (cname × cname) set"
  and subcls1' :: "prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>1 _" [71,71,71] 70)
  for P :: prog
where
  "P \<turnstile> C \<prec>1 D ≡ (C,D) ∈ subcls1 P"
| subcls1I: "[|class P C = Some (Bs,rest); D ∈  baseClasses Bs|] ==> P \<turnstile> C \<prec>1 D"

abbreviation
  subcls    :: "prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>* _"  [71,71,71] 70) where
  "P \<turnstile> C \<preceq>* D ≡ (C,D) ∈ (subcls1 P)*"
 

lemma subclsRD:
  "P \<turnstile> C \<prec>R D ==> ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (Repeats(D) ∈ set Bs)"
by(auto elim: subclsR.cases)

lemma subclsSD:
  "P \<turnstile> C \<prec>S D ==> ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (Shares(D) ∈ set Bs)"
by(auto elim: subclsS.cases)

lemma subcls1D:
  "P \<turnstile> C \<prec>1 D ==> ∃fs ms Bs. (class P C = Some (Bs,fs,ms)) ∧ (D ∈ baseClasses Bs)"
by(auto elim: subcls1.cases)


lemma subclsR_subcls1:
  "P \<turnstile> C \<prec>R D ==> P \<turnstile> C \<prec>1 D"
by (auto elim!:subclsR.cases intro:subcls1I simp:RepBaseclass_isBaseclass)

lemma subclsS_subcls1:
  "P \<turnstile> C \<prec>S D ==> P \<turnstile> C \<prec>1 D"
by (auto elim!:subclsS.cases intro:subcls1I simp:ShBaseclass_isBaseclass)

lemma subcls1_subclsR_or_subclsS:
  "P \<turnstile> C \<prec>1 D ==> P \<turnstile> C \<prec>R D ∨ P \<turnstile> C \<prec>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(fastsimp 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 \<turnstile> C \<prec>1 D ==> is_class P C"
by (auto dest:subcls1D simp:is_class_def)

lemma subcls_is_class:
"[|P \<turnstile> D \<preceq>* C; is_class P C|] ==> is_class P D"
by (induct rule:rtrancl_induct,auto dest:subcls1_class)

end