# HG changeset patch
# User ballarin
# Date 1229088621 -3600
# Node ID 242b0bc2172cad83d7362d6e699b033340a6d1b1
# Parent  95a239a5e0558ef6a17cc596dfeb32b60484d8d8# Parent  ab99da3854afecfb122b4a3e085383f6f05070e3
Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

diff -r 95a239a5e055 -r 242b0bc2172c src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 12 14:30:21 2008 +0100
@@ -44,9 +44,10 @@
 val _ =
   OuterSyntax.command "interpretation"
     "prove interpretation of locale expression in theory" K.thy_goal
-    (P.!!! SpecParse.locale_expression
-        >> (fn expr => Toplevel.print o
-            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+    (P.!!! SpecParse.locale_expression --
+      Scan.optional (P.$$$ "where" |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+        >> (fn (expr, mixin) => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr mixin)));
 
 val _ =
   OuterSyntax.command "interpret"
diff -r 95a239a5e055 -r 242b0bc2172c src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 12 14:30:21 2008 +0100
@@ -10,7 +10,6 @@
 
 ML_val {* set new_locales *}
 ML_val {* set Toplevel.debug *}
-ML_val {* set show_hyps *}
 
 
 typedecl int arities int :: "term"
@@ -24,7 +23,7 @@
   int_minus: "(-x) + x = 0"
   int_minus2: "-(-x) = x"
 
-text {* Inference of parameter types *}
+section {* Inference of parameter types *}
 
 locale param1 = fixes p
 print_locale! param1
@@ -44,7 +43,7 @@
 print_locale! param4
 
 
-text {* Incremental type constraints *}
+subsection {* Incremental type constraints *}
 
 locale constraint1 =
   fixes  prod (infixl "**" 65)
@@ -58,7 +57,7 @@
 print_locale! constraint2
 
 
-text {* Inheritance *}
+section {* Inheritance *}
 
 locale semi =
   fixes prod (infixl "**" 65)
@@ -94,7 +93,7 @@
 print_locale! pert_hom' thm pert_hom'_def
 
 
-text {* Syntax declarations *}
+section {* Syntax declarations *}
 
 locale logic =
   fixes land (infixl "&&" 55)
@@ -113,13 +112,13 @@
 print_locale! use_decl thm use_decl_def
 
 
-text {* Foundational versions of theorems *}
+section {* Foundational versions of theorems *}
 
 thm logic.assoc
 thm logic.lor_def
 
 
-text {* Defines *}
+section {* Defines *}
 
 locale logic_def =
   fixes land (infixl "&&" 55)
@@ -149,7 +148,7 @@
 end
 
 
-text {* Notes *}
+section {* Notes *}
 
 (* A somewhat arcane homomorphism example *)
 
@@ -169,7 +168,7 @@
   by (rule semi_hom_mult)
 
 
-text {* Theorem statements *}
+section {* Theorem statements *}
 
 lemma (in lgrp) lcancel:
   "x ** y = x ** z <-> y = z"
@@ -200,7 +199,7 @@
 print_locale! rgrp
 
 
-text {* Patterns *}
+subsection {* Patterns *}
 
 lemma (in rgrp)
   assumes "y ** x = z ** x" (is ?a)
@@ -218,7 +217,7 @@
 qed
 
 
-text {* Interpretation between locales: sublocales *}
+section {* Interpretation between locales: sublocales *}
 
 sublocale lgrp < right: rgrp
 print_facts
@@ -305,8 +304,7 @@
   done
 
 print_locale! order_with_def
-(* Note that decls come after theorems that make use of them.
-  Appears to be harmless at least in this example. *)
+(* Note that decls come after theorems that make use of them. *)
 
 
 (* locale with many parameters ---
@@ -359,7 +357,7 @@
 print_locale! trivial  (* No instance for y created (subsumed). *)
 
 
-text {* Sublocale, then interpretation in theory *}
+subsection {* Sublocale, then interpretation in theory *}
 
 interpretation int: lgrp "op +" "0" "minus"
 proof unfold_locales
@@ -374,7 +372,7 @@
   (* the latter comes through the sublocale relation *)
 
 
-text {* Interpretation in theory, then sublocale *}
+subsection {* Interpretation in theory, then sublocale *}
 
 interpretation (* fol: *) logic "op +" "minus"
 (* FIXME declaration of qualified names *)
@@ -386,10 +384,12 @@
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
 begin
-(* FIXME
+
+(* FIXME interpretation below fails
 definition lor (infixl "||" 50) where
   "x || y = --(-- x && -- y)"
 *)
+
 end
 
 sublocale logic < two: logic2
@@ -398,7 +398,45 @@
 thm two.assoc
 
 
-text {* Interpretation in proofs *}
+subsection {* Declarations and sublocale *}
+
+locale logic_a = logic
+locale logic_b = logic
+
+sublocale logic_a < logic_b
+  by unfold_locales
+
+
+subsection {* Equations *}
+
+locale logic_o =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
+    and notnot_o: "-- (-- x) <-> x"
+begin
+
+definition lor_o (infixl "||" 50) where
+  "x || y <-> --(-- x && -- y)"
+
+end
+
+interpretation x: logic_o "op &" "Not"
+  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+proof -
+  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
+  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
+qed
+
+thm x.lor_o_def bool_logic_o
+
+lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+
+(* thm x.lor_triv *)
+
+
+subsection {* Interpretation in proofs *}
 
 lemma True
 proof
diff -r 95a239a5e055 -r 242b0bc2172c src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/General/binding.ML	Fri Dec 12 14:30:21 2008 +0100
@@ -59,8 +59,8 @@
 val qualify = map_base o qualify_base;
   (*FIXME should all operations on bare names move here from name_space.ML ?*)
 
-fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
-  else (map_binding o apfst) (cons (prfx, sticky)) b;
+fun add_prefix sticky "" b = b
+  | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
 
 fun map_prefix f (Binding ((prefix, name), pos)) =
   f prefix (name_pos (name, pos));
diff -r 95a239a5e055 -r 242b0bc2172c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/IsaMakefile	Fri Dec 12 14:30:21 2008 +0100
@@ -26,7 +26,8 @@
   Concurrent/par_list_dummy.ML Concurrent/schedule.ML			\
   Concurrent/simple_thread.ML Concurrent/synchronized.ML		\
   Concurrent/task_queue.ML General/ROOT.ML General/alist.ML		\
-  General/balanced_tree.ML General/basics.ML General/buffer.ML		\
+  General/balanced_tree.ML General/basics.ML General/binding.ML         \
+  General/buffer.ML		\
   General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
   General/lazy.ML General/markup.ML General/name_space.ML		\
   General/ord_list.ML General/output.ML General/path.ML			\
diff -r 95a239a5e055 -r 242b0bc2172c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 12 14:30:21 2008 +0100
@@ -28,8 +28,8 @@
   (* Interpretation *)
   val sublocale_cmd: string -> expression -> theory -> Proof.state;
   val sublocale: string -> expression_i -> theory -> Proof.state;
-  val interpretation_cmd: expression -> theory -> Proof.state;
-  val interpretation: expression_i -> theory -> Proof.state;
+  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state;
+  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state;
   val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
   val interpret: expression_i -> bool -> Proof.state -> Proof.state;
 end;
@@ -175,7 +175,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.qualify prfx), ctxt')
+      Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
   end;
 
 
@@ -410,7 +410,7 @@
 
     val fors = prep_vars fixed context |> fst;
     val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
-    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt);
+    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], ctxt);
     val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
 
@@ -484,7 +484,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
-      NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
+      fold NewLocale.activate_local_facts deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
@@ -786,33 +786,63 @@
 
 local
 
-fun gen_interpretation prep_expr
-    expression thy =
+datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list;
+
+fun gen_interpretation prep_expr parse_prop prep_attr
+    expression equations thy =
   let
     val ctxt = ProofContext.init thy;
 
-    val ((propss, regs, export), goal_ctxt) = prep_expr expression ctxt;
+    val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
     
-    fun store_reg ((name, morph), thms) =
-      let
-        val morph' = morph $> Element.satisfy_morphism thms $> export;
-      in
-        NewLocale.add_global_registration (name, morph') #>
-        NewLocale.activate_global_facts (name, morph')
-      end;
+    val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
+    val eq_attns = 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 store (Reg (name, morph), thms) (regs, thy) =
+        let
+          val thms' = map (Element.morph_witness export') thms;
+          val morph' = morph $> Element.satisfy_morphism thms';
+          val add = NewLocale.add_global_registration (name, (morph', export));
+        in ((name, morph') :: regs, add thy) end
+      | store (Eqns [], []) (regs, thy) =
+        let val add = fold_rev (fn (name, morph) =>
+              NewLocale.activate_global_facts (name, morph $> export)) regs;
+        in (regs, add thy) end
+      | store (Eqns attns, thms) (regs, thy) =
+        let
+          val thms' = thms |> map (Element.conclude_witness #>
+            Morphism.thm (export' $> export) #>
+            LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+            Drule.abs_def);
+          val eq_morph =
+            Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
+            Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
+          val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
+          val add =
+            fold_rev (fn (name, morph) =>
+              NewLocale.amend_global_registration eq_morph (name, morph) #>
+              NewLocale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
+            PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
+            snd
+        in (regs, add thy) end;
 
     fun after_qed results =
-      ProofContext.theory (fold store_reg (regs ~~ prep_result propss results));
+      ProofContext.theory (fn thy =>
+        fold store (map Reg regs @ [Eqns eq_attns] ~~
+          prep_result (propss @ [eqns]) results) ([], thy) |> snd);
   in
     goal_ctxt |>
-      Proof.theorem_i NONE after_qed (prep_propp propss) |>
+      Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
       Element.refine_witness |> Seq.hd
   end;
 
 in
 
-fun interpretation_cmd x = gen_interpretation read_goal_expression x;
-fun interpretation x = gen_interpretation cert_goal_expression x;
+fun interpretation_cmd x = gen_interpretation read_goal_expression
+  Syntax.parse_prop Attrib.intern_src x;
+fun interpretation x = gen_interpretation cert_goal_expression (K I) (K I) x;
 
 end;
 
diff -r 95a239a5e055 -r 242b0bc2172c src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 12 14:30:21 2008 +0100
@@ -47,9 +47,11 @@
   val unfold_attrib: attribute
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
-  (* Identifiers and registrations *)
-  val clear_local_idents: Proof.context -> Proof.context
-  val add_global_registration: (string * Morphism.morphism) -> theory -> theory
+  (* Registrations *)
+  val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+    theory -> theory
+  val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
+    theory -> theory
   val get_global_registrations: theory -> (string * Morphism.morphism) list
 
   (* Diagnostic *)
@@ -223,12 +225,10 @@
 fun get_global_idents thy =
   let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
 val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
-val clear_global_idents = put_global_idents empty;
 
 fun get_local_idents ctxt =
   let val (Ready ids) = (IdentifiersData.get o Context.Proof) ctxt in ids end;
 val put_local_idents = Context.proof_map o IdentifiersData.put o Ready;
-val clear_local_idents = put_local_idents empty;
 
 end;
 
@@ -457,7 +457,8 @@
 (* FIXME only global variant needed *)
 structure RegistrationsData = GenericDataFun
 (
-  type T = ((string * Morphism.morphism) * stamp) list;
+  type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
+(* FIXME mixins need to be stamped *)
     (* registrations, in reverse order of declaration *)
   val empty = [];
   val extend = I;
@@ -465,9 +466,26 @@
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-val get_global_registrations = map fst o RegistrationsData.get o Context.Theory;
+val get_global_registrations =
+  Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
 fun add_global_registration reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
+fun amend_global_registration morph (name, base_morph) thy =
+  let
+    val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+    val base = instance_of thy name base_morph;
+    fun match (name', (morph', _)) =
+      name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
+    val i = find_index match (rev regs);
+    val _ = if i = ~1 then error ("No interpretation of locale " ^
+        quote (extern thy name) ^ " and parameter instantiation " ^
+        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+      else ();
+  in
+    (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+      (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
+  end;
+
 end;
 
diff -r 95a239a5e055 -r 242b0bc2172c src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 12 12:14:02 2008 +0100
+++ b/src/Pure/library.ML	Fri Dec 12 14:30:21 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/library.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Markus Wenzel, TU Muenchen
 
@@ -491,7 +490,7 @@
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
-(*find the position of an element in a list*)
+(*find position of first element satisfying a predicate*)
 fun find_index pred =
   let fun find (_: int) [] = ~1
         | find n (x :: xs) = if pred x then n else find (n + 1) xs;