# HG changeset patch
# User ballarin
# Date 1292694193 -3600
# Node ID dea60d05292387aed80aafe5d348ae788ab5e0be
# Parent  abe867c29e55232af39fa4fb7646633d1d2a2367
Add mixins to sublocale command.

diff -r abe867c29e55 -r dea60d052923 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -145,7 +145,7 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd name expr
+   |> Expression.sublocale_cmd name expr []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of
diff -r abe867c29e55 -r dea60d052923 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/Pure/Isar/class.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -232,7 +232,7 @@
       |> filter (is_class thy);
     val add_dependency = case some_dep_morph
      of SOME dep_morph => Locale.add_dependency sub
-          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
+          (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
       | NONE => I
   in
     thy
diff -r abe867c29e55 -r dea60d052923 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -39,12 +39,18 @@
     (term list list * (string * morphism) list * morphism) * Proof.context
   val read_goal_expression: expression -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context
-  val sublocale: string -> expression_i -> theory -> Proof.state
-  val sublocale_cmd: string -> expression -> theory -> Proof.state
-  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
-  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
-  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
-  val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state
+  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
+    theory -> Proof.state
+  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
+    theory -> Proof.state
+  val interpretation: expression_i -> (Attrib.binding * term) list ->
+    theory -> Proof.state
+  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
+    theory -> Proof.state
+  val interpret: expression_i -> (Attrib.binding * term) list ->
+    bool -> Proof.state -> Proof.state
+  val interpret_cmd: expression -> (Attrib.binding * string) list ->
+    bool -> Proof.state -> Proof.state
 end;
 
 structure Expression : EXPRESSION =
@@ -802,7 +808,7 @@
   in
     context
     |> Element.generic_note_thmss Thm.lemmaK
-      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn],[])]) eqns)
+      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
     |-> (fn facts => `(fn context => meta_rewrite context facts))
     |-> (fn eqns => fold (fn ((dep, morph), wits) =>
       fn context =>
@@ -868,20 +874,56 @@
 
 local
 
-fun gen_sublocale prep_expr intern raw_target expression thy =
+fun note_eqns_dependency target deps witss attrss eqns export export' ctxt =
+  let
+    fun meta_rewrite ctxt =
+      map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) o maps snd;
+    val facts =
+      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
+    val eqns' = ctxt |> Context.Proof
+      |> Element.generic_note_thmss Thm.lemmaK facts
+      |> apsnd Context.the_proof  (* FIXME Context.proof_map_result *)
+      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt facts))
+      |> fst;  (* FIXME duplication to add_thmss *)
+  in
+    ctxt
+    |> Locale.add_thmss target Thm.lemmaK facts
+    |> ProofContext.background_theory (fold (fn ((dep, morph), wits) =>
+      fn theory =>
+        Locale.add_dependency target
+          (dep, morph $> Element.satisfy_morphism
+            (map (Element.morph_witness export') wits))
+          (Element.eq_morphism theory eqns' |> Option.map (rpair true))
+          export theory) (deps ~~ witss))
+  end;
+
+fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
+    expression equations thy =
   let
     val target = intern thy raw_target;
     val target_ctxt = Named_Target.init target thy;
-    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
+
+    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+    val attrss = map ((apsnd o map) (prep_attr thy) o fst) equations;
+    val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
+    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
+
+    fun after_qed witss eqns =
+      note_eqns_dependency target deps witss attrss eqns export export';
+
+  in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
+(*
     fun after_qed witss = ProofContext.background_theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
         target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
   in Element.witness_proof after_qed propss goal_ctxt end;
-
+*)
 in
 
-fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
-fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
+fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
+fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
+  Syntax.parse_prop Attrib.intern_src x;
 
 end;
 
diff -r abe867c29e55 -r dea60d052923 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -414,19 +414,23 @@
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
+fun parse_interpretation_arguments mandatory =
+  Parse.!!! (Parse_Spec.locale_expression mandatory) --
+    Scan.optional
+      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+
 val _ =
   Outer_Syntax.command "sublocale"
     "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
     (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
-      Parse.!!! (Parse_Spec.locale_expression false)
-      >> (fn (loc, expr) =>
-          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
+      parse_interpretation_arguments false
+      >> (fn (loc, (expr, equations)) =>
+          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr equations)));
 
 val _ =
   Outer_Syntax.command "interpretation"
     "prove interpretation of locale expression in theory" Keyword.thy_goal
-    (Parse.!!! (Parse_Spec.locale_expression true) --
-      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+    (parse_interpretation_arguments true
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
 
@@ -434,8 +438,7 @@
   Outer_Syntax.command "interpret"
     "prove interpretation of locale expression in proof context"
     (Keyword.tag_proof Keyword.prf_goal)
-    (Parse.!!! (Parse_Spec.locale_expression true) --
-      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
+    (parse_interpretation_arguments true
       >> (fn (expr, equations) => Toplevel.print o
           Toplevel.proof' (Expression.interpret_cmd expr equations)));
 
diff -r abe867c29e55 -r dea60d052923 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Dec 18 14:02:14 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Dec 18 18:43:13 2010 +0100
@@ -71,7 +71,8 @@
   val amend_registration: string * morphism -> morphism * bool ->
     morphism -> Context.generic -> Context.generic
   val registrations_of: Context.generic -> string -> (string * morphism) list
-  val add_dependency: string -> string * morphism -> morphism -> theory -> theory
+  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
+    morphism -> theory -> theory
 
   (* Diagnostic *)
   val all_locales: theory -> string list
@@ -292,7 +293,7 @@
 (
   type T = ((morphism * morphism) * serial) Idtab.table *
     (* registrations, indexed by locale name and instance;
-       serial points to mixin list *)
+       unique serial, points to mixin list *)
     (((morphism * bool) * serial) list) Inttab.table;
     (* table of mixin lists, per list mixins in reverse order of declaration;
        lists indexed by registration serial,
@@ -484,7 +485,7 @@
 
 (*** Dependencies ***)
 
-fun add_dependency loc (name, morph) export thy =
+fun add_dependency loc (name, morph) mixin export thy =
   let
     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
     val context' = Context.Theory thy';