A rough implementation of full mixin inheritance; additional unit tests.

--- a/src/FOL/ex/LocaleTest.thy	Tue Feb 02 21:23:20 2010 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Thu Feb 11 21:00:36 2010 +0100
@@ -617,6 +617,88 @@
 lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
   by (rule le4.less_thm4')
 
+text {* Inherited mixin applied to new theorem *}
+
+locale mixin5_base = reflexive
+
+locale mixin5_inherited = mixin5_base
+
+interpretation le5: mixin5_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin5_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin5_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+interpretation le5: mixin5_inherited gle
+  by unfold_locales
+
+lemmas (in mixin5_inherited) less_thm5 = less_def
+
+thm le5.less_thm5  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le5.less_thm5)
+
+text {* Mixin pushed down to existing inherited locale *}
+
+locale mixin6_base = reflexive
+
+locale mixin6_inherited = mixin5_base
+
+interpretation le6: mixin6_base gle
+  by unfold_locales
+interpretation le6: mixin6_inherited gle
+  by unfold_locales
+interpretation le6: mixin6_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin6_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin6_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+lemmas (in mixin6_inherited) less_thm6 = less_def
+
+thm le6.less_thm6  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le6.less_thm6)
+
+text {* Existing mixin inherited through sublocale relation *}
+
+locale mixin7_base = reflexive
+
+locale mixin7_inherited = reflexive
+
+interpretation le7: mixin7_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin7_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin7_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+interpretation le7: mixin7_inherited gle
+  by unfold_locales
+
+lemmas (in mixin7_inherited) less_thm7 = less_def
+
+thm le7.less_thm7  (* before, mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+  by (rule le7.less_thm7)
+
+sublocale mixin7_inherited < mixin7_base
+  by unfold_locales
+
+lemmas (in mixin7_inherited) less_thm7b = less_def
+
+thm le7.less_thm7b  (* after, mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le7.less_thm7b)
+
 
 subsection {* Interpretation in proofs *}
 

--- a/src/Pure/Isar/locale.ML	Tue Feb 02 21:23:20 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Feb 11 21:00:36 2010 +0100
@@ -349,20 +349,6 @@
 
 (* Primitive operations *)
 
-fun compose_mixins mixins =
-  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
-
-fun reg_morph mixins ((name, (base, export)), serial) =
-  let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
-  in (name, base $> mix $> export) end;
-
-fun these_registrations thy name = Registrations.get thy
-  |>> filter (curry (op =) name o fst o fst)
-  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
-
-fun all_registrations thy = Registrations.get thy
-  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
-
 fun get_mixins thy (name, morph) =
   let
     val (regs, mixins) = Registrations.get thy;
@@ -378,6 +364,22 @@
     merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
   |> snd |> filter (snd o fst);  (* only inheritable mixins *)
 
+fun compose_mixins mixins =
+  fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
+
+fun reg_morph mixins ((name, (base, export)), serial) =
+  let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
+  in (name, base $> mix $> export) end;
+
+fun these_registrations thy name = Registrations.get thy
+  |>> filter (curry (op =) name o fst o fst)
+(*  |-> (fn regs => fn mixins => map (reg_morph mixins) regs); *)
+  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
+    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
+
+fun all_registrations thy = Registrations.get thy
+  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
+
 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   let
     val {notes, ...} = the_locale thy name;
@@ -463,7 +465,8 @@
       let
         fun add_reg (dep', morph') =
           let
-            val mixins = collect_mixins thy (dep', morph' $> export);
+(*            val mixins = collect_mixins thy (dep', morph' $> export); *)
+            val mixins = [];  (* FIXME *)
             val serial = serial ();
           in
             Registrations.map (apfst (cons ((dep', (morph', export)), serial))
@@ -510,6 +513,7 @@
                 Attrib.map_facts (Attrib.attribute_i thy)
             in PureThy.note_thmss kind args'' #> snd end)
         (these_registrations thy loc) thy))
+(* FIXME apply mixins *)
   in ctxt'' end;