1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Nov 11 21:53:58 2009 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Sat Nov 21 17:35:55 2009 +0100
     1.3 @@ -515,6 +515,100 @@
     1.4    x.lor_triv
     1.5  
     1.6  
     1.7 +subsection {* Inheritance of mixins *}
     1.8 +
     1.9 +locale reflexive =
    1.10 +  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
    1.11 +  assumes refl: "x \<sqsubseteq> x"
    1.12 +begin
    1.13 +
    1.14 +definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
    1.15 +
    1.16 +end
    1.17 +
    1.18 +consts
    1.19 +  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
    1.20 +  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
    1.21 +
    1.22 +axioms
    1.23 +  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
    1.24 +  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
    1.25 +
    1.26 +text {* Mixin not applied to locales further up the hierachy. *}
    1.27 +
    1.28 +locale mixin = reflexive
    1.29 +begin
    1.30 +lemmas less_thm = less_def
    1.31 +end
    1.32 +
    1.33 +interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
    1.34 +proof -
    1.35 +  show "mixin(gle)" by unfold_locales (rule grefl)
    1.36 +  note reflexive = this[unfolded mixin_def]
    1.37 +  show "reflexive.less(gle, x, y) <-> gless(x, y)"
    1.38 +    by (simp add: reflexive.less_def[OF reflexive] gless_def)
    1.39 +qed
    1.40 +
    1.41 +thm le.less_def  (* mixin not applied *)
    1.42 +lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_def)
    1.43 +thm le.less_thm  (* mixin applied *)
    1.44 +lemma "gless(x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm)
    1.45 +
    1.46 +lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
    1.47 +  by (rule le.less_def)
    1.48 +lemma "gless(x, y) <-> gle(x, y) & x ~= y"
    1.49 +  by (rule le.less_thm)
    1.50 +
    1.51 +text {* Mixin propagated along the locale hierarchy *}
    1.52 +
    1.53 +locale mixin2 = mixin
    1.54 +begin
    1.55 +lemmas less_thm2 = less_def
    1.56 +end
    1.57 +
    1.58 +interpretation le: mixin2 gle
    1.59 +  by unfold_locales
    1.60 +
    1.61 +thm le.less_thm2  (* mixin applied *)
    1.62 +lemma "gless(x, y) <-> gle(x, y) & x ~= y"
    1.63 +  by (rule le.less_thm2)
    1.64 +
    1.65 +text {* Mixin only available in original context *}
    1.66 +
    1.67 +(* This section is not finished. *)
    1.68 +
    1.69 +locale mixin3 = mixin le' for le' :: "'a => 'a => o" (infix "\<sqsubseteq>''" 50)
    1.70 +
    1.71 +lemma (in mixin2) before:
    1.72 +  "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
    1.73 +proof -
    1.74 +  have "reflexive(gle)" by unfold_locales (rule grefl)
    1.75 +  note th = reflexive.less_def[OF this]
    1.76 +  then show ?thesis by (simp add: th)
    1.77 +qed
    1.78 +
    1.79 +interpretation le': mixin2 gle'
    1.80 +  apply unfold_locales apply (rule grefl') done
    1.81 +
    1.82 +lemma (in mixin2) after:
    1.83 +  "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
    1.84 +proof -
    1.85 +  have "reflexive(gle)" by unfold_locales (rule grefl)
    1.86 +  note th = reflexive.less_def[OF this]
    1.87 +  then show ?thesis by (simp add: th)
    1.88 +qed
    1.89 +
    1.90 +thm le'.less_def le'.less_thm le'.less_thm2 le'.before le'.after
    1.91 +
    1.92 +locale combined = le: reflexive le + le': mixin le'
    1.93 +  for le :: "'a => 'a => o" (infixl "\<sqsubseteq>" 50) and le' :: "'a => 'a => o" (infixl "\<sqsubseteq>''" 50)
    1.94 +
    1.95 +interpretation combined gle gle'
    1.96 +  apply unfold_locales done
    1.97 +
    1.98 +thm le.less_def le.less_thm le'.less_def le'.less_thm
    1.99 +
   1.100 +
   1.101  subsection {* Interpretation in proofs *}
   1.102  
   1.103  lemma True