Interpretation in theories including interaction with subclass relation.

--- a/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 03 15:27:41 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Dec 05 11:26:07 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/NewLocaleSetup.thy
-    ID:         $Id$
     Author:     Clemens Ballarin, TU Muenchen
 
 Testing environment for locale expressions --- experimental.
@@ -40,6 +39,13 @@
    Toplevel.unknown_theory o Toplevel.keep (fn state =>
      NewLocale.print_locale (Toplevel.theory_of state) show_facts name))));
 
+val _ =
+  OuterSyntax.command "interpretation"
+    "prove and register interpretation of locale expression in theory" K.thy_goal
+    (P.!!! Expression.parse_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+
 end
 
 *}

--- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 03 15:27:41 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 11:26:07 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      FOL/ex/NewLocaleTest.thy
-    ID:         $Id$
     Author:     Clemens Ballarin, TU Muenchen
 
 Testing environment for locale expressions --- experimental.
@@ -19,6 +18,11 @@
   zero :: int ("0")
   minus :: "int => int" ("- _")
 
+axioms
+  int_assoc: "(x + y::int) + z = x + (y + z)"
+  int_zero: "0 + x = x"
+  int_minus: "(-x) + x = 0"
+  int_minus2: "-(-x) = x"
 
 text {* Inference of parameter types *}
 
@@ -30,7 +34,7 @@
 
 (*
 locale param_top = param2 r for r :: "'b :: {}"
-print_locale! param_top
+  Fails, cannot generalise parameter.
 *)
 
 locale param3 = fixes p (infix ".." 50)
@@ -298,4 +302,43 @@
 
 print_locale! trivial  (* No instance for y created (subsumed). *)
 
+
+text {* Sublocale, then interpretation in theory *}
+
+interpretation int: lgrp "op +" "0" "minus"
+proof unfold_locales
+qed (rule int_assoc int_zero int_minus)+
+
+thm int.assoc int.semi_axioms
+
+interpretation int2: semi "op +"
+  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
+
+thm int.lone int.right.rone
+  (* the latter comes through the sublocale relation *)
+
+
+text {* Interpretation in theory, then sublocale *}
+
+interpretation (* fol: *) logic "op +" "minus"
+(* FIXME declaration of qualified names *)
+  by unfold_locales (rule int_assoc int_minus2)+
+
+locale logic2 =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+begin
+(* FIXME
+definition lor (infixl "||" 50) where
+  "x || y = --(-- x && -- y)"
+*)
 end
+
+sublocale logic < two: logic2
+  by unfold_locales (rule assoc notnot)+
+
+thm two.assoc
+
+end

--- a/src/Pure/Isar/expression.ML	Wed Dec 03 15:27:41 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 05 11:26:07 2008 +0100
@@ -26,6 +26,12 @@
   (* 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 interpret_cmd: Morphism.morphism -> expression -> bool -> Proof.state -> Proof.state;
+  val interpret: Morphism.morphism -> expression_i -> bool -> Proof.state -> Proof.state;
+*)
 
   (* Debugging and development *)
   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
@@ -462,7 +468,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_idents ctxt);
+    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_local_idents ctxt);
     val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
 
@@ -539,7 +545,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
-      NewLocale.clear_idents |> fold (NewLocale.activate_facts thy) deps;
+      NewLocale.clear_local_idents |> fold (NewLocale.activate_local_facts thy) deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
@@ -811,7 +817,13 @@
     fun store_dep ((name, morph), thms) =
       NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
 
-    fun after_qed results = fold store_dep (deps ~~ prep_result propss results);
+    fun after_qed results =
+      ProofContext.theory (
+        (* store dependencies *)
+        fold store_dep (deps ~~ prep_result propss results) #>
+        (* propagate registrations *)
+        (fn thy => fold_rev (fn reg => NewLocale.activate_global_facts reg)
+          (NewLocale.get_global_registrations thy) thy));
   in
     goal_ctxt |>
       Proof.theorem_i NONE after_qed (prep_propp propss) |>
@@ -825,6 +837,39 @@
 
 end;
 
+(** Interpretation in theories **)
+
+local
+
+fun gen_interpretation prep_expr
+    expression thy =
+  let
+    val ctxt = ProofContext.init thy;
+
+    val ((propss, deps, export), goal_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;
+
+    fun after_qed results =
+      ProofContext.theory (fold store_reg (deps ~~ prep_result propss results));
+  in
+    goal_ctxt |>
+      Proof.theorem_i NONE after_qed (prep_propp propss) |>
+      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;
 
 end;
 
+end;
+

--- a/src/Pure/Isar/new_locale.ML	Wed Dec 03 15:27:41 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:26:07 2008 +0100
@@ -8,7 +8,6 @@
 sig
   type locale
 
-  val clear_idents: Proof.context -> Proof.context
   val test_locale: theory -> string -> bool
   val register_locale: string ->
     (string * sort) list * (Name.binding * typ option * mixfix) list ->
@@ -23,6 +22,7 @@
 
   (* Specification *)
   val params_of: theory -> string -> (Name.binding * typ option * mixfix) list
+  val instance_of: theory -> string -> Morphism.morphism -> term list
   val specification_of: theory -> string -> term option * term list
   val declarations_of: theory -> string -> declaration list * declaration list
 
@@ -32,12 +32,14 @@
   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
-  val add_dependency: string -> (string * Morphism.morphism) -> Proof.context -> Proof.context
+  val add_dependency: string -> (string * Morphism.morphism) -> theory -> theory
 
   (* Activation *)
   val activate_declarations: theory -> string * Morphism.morphism ->
     Proof.context -> Proof.context
-  val activate_facts: theory -> string * Morphism.morphism ->
+  val activate_global_facts: string * Morphism.morphism ->
+    theory -> theory
+  val activate_local_facts: theory -> string * Morphism.morphism ->
     Proof.context -> Proof.context
 (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
@@ -48,6 +50,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
+  val get_global_registrations: theory -> (string * Morphism.morphism) list
+
   (* Diagnostic *)
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> bstring -> unit
@@ -168,6 +175,10 @@
     val Loc {parameters = (_, params), ...} = the_locale thy name
   in params end;
 
+fun instance_of thy name morph =
+  params_of thy name |>
+    map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
+
 fun specification_of thy name =
   let
     val Loc {spec, ...} = the_locale thy name
@@ -193,19 +204,36 @@
 
 local
 
+datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
+
 structure IdentifiersData = GenericDataFun
 (
-  type T = identifiers;
-  val empty = empty;
+  type T = identifiers delayed;
+  val empty = Ready empty;
   val extend = I;
-  fun merge _ = Library.merge (op =);  (* FIXME cannot do this properly without theory context *)
+  fun merge _ = ToDo;
 );
 
 in
 
-val get_idents = IdentifiersData.get o Context.Proof;
-val put_idents = Context.proof_map o IdentifiersData.put;
-val clear_idents = put_idents empty;
+fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
+  | finish _ (Ready ids) = ids;
+
+val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
+  (case IdentifiersData.get (Context.Theory thy) of
+    Ready _ => NONE |
+    ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
+  )));
+  
+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;
 
@@ -222,8 +250,7 @@
   else
     let
       val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
-      val instance = params |>
-        map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
+      val instance = instance_of thy name morph;
     in
       if member (ident_eq thy) marked (name, instance)
       then (deps, marked)
@@ -242,9 +269,14 @@
 
 fun roundup thy activate_dep (name, morph) (marked, input) =
   let
-    val (dependencies', marked') = add thy 0 (name, morph) ([], marked);
+    (* Find all dependencies incuding new ones (which are dependencies enriching
+      existing registrations). *)
+    val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
+    (* Filter out exisiting fragments. *)
+    val dependencies' = filter_out (fn (name, morph) =>
+      member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   in
-    (marked', input |> fold_rev (activate_dep thy) dependencies')
+    (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
   end;
 
 end;
@@ -273,7 +305,7 @@
 
 fun activate_all name thy activ_elem (marked, input) =
   let
-    val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
+    val Loc {parameters = (_, params), spec = (asm, defs), ...} =
       the_locale thy name;
   in
     input |>
@@ -291,16 +323,21 @@
 
 local
 
-fun init_elem (Fixes fixes) ctxt = ctxt |>
+fun init_global_elem (Notes (kind, facts)) thy =
+      let
+        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+      in Locale.global_note_qualified kind facts' thy |> snd end
+
+fun init_local_elem (Fixes fixes) ctxt = ctxt |>
       ProofContext.add_fixes_i fixes |> snd
-  | init_elem (Assumes assms) ctxt =
+  | init_local_elem (Assumes assms) ctxt =
       let
         val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
       in
         ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
           ProofContext.add_assms_i Assumption.assume_export assms' |> snd
      end 
-  | init_elem (Defines defs) ctxt =
+  | init_local_elem (Defines defs) ctxt =
       let
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
       in
@@ -308,7 +345,7 @@
           ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
           snd
       end
-  | init_elem (Notes (kind, facts)) ctxt =
+  | init_local_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
       in Locale.local_note_qualified kind facts' ctxt |> snd end
@@ -319,13 +356,18 @@
 in
 
 fun activate_declarations thy dep ctxt =
-  roundup thy activate_decls dep (get_idents ctxt, ctxt) |> uncurry put_idents;
+  roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
   
-fun activate_facts thy dep ctxt =
-  roundup thy (activate_notes init_elem) dep (get_idents ctxt, ctxt) |> uncurry put_idents;
+fun activate_global_facts dep thy =
+  roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
+  uncurry put_global_idents;
 
-fun init name thy = activate_all name thy init_elem (empty, ProofContext.init thy) |>
-  uncurry put_idents;
+fun activate_local_facts thy dep ctxt =
+  roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |>
+  uncurry put_local_idents;
+
+fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
+  uncurry put_local_idents;
 
 fun print_locale thy show_facts name =
   let
@@ -379,9 +421,9 @@
 (* Dependencies *)
 
 fun add_dependency loc dep =
-  ProofContext.theory (change_locale loc
+  change_locale loc
     (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies)));
+      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
 
 
 (*** Reasoning about locales ***)
@@ -414,5 +456,22 @@
       "back-chain all introduction rules of locales")]));
 
 
+(*** Registrations: interpretations in theories and proof contexts ***)
+
+structure RegistrationsData = GenericDataFun
+(
+  type T = ((string * Morphism.morphism) * stamp) list;
+    (* registrations, in reverse order of declaration *)
+  val empty = [];
+  val extend = I;
+  fun merge _ = Library.merge (eq_snd (op =));
+    (* FIXME consolidate with dependencies, consider one data slot only *)
+);
+
+val get_global_registrations = map fst o RegistrationsData.get o Context.Theory;
+fun add_global_registration reg =
+  (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
+
+
 end;