Intro_locales_tac to simplify goals involving locale predicates.

--- a/src/FOL/ex/NewLocaleTest.thy	Fri Nov 28 12:26:14 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Nov 28 17:43:06 2008 +0100
@@ -167,7 +167,7 @@
 
 sublocale lgrp < right: rgrp
 print_facts
-proof (intro rgrp.intro semi.intro rgrp_axioms.intro)
+proof new_unfold_locales
   {
     fix x
     have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
@@ -180,7 +180,7 @@
       by (simp add: linv lone rone)
     then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   }
-qed (simp add: assoc)
+qed
 
 (* effect on printed locale *)
 
@@ -196,20 +196,20 @@
 (* circular interpretation *)
 
 sublocale rgrp < left: lgrp
-  proof (intro lgrp.intro semi.intro lgrp_axioms.intro)
-    {
-      fix x
-      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
-      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
-    }
-    note lone = this
-    {
-      fix x
-      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
-	by (simp add: rinv lone rone)
-      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
-    }
-  qed (simp add: assoc)
+proof new_unfold_locales
+  {
+    fix x
+    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
+    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+  }
+  note lone = this
+  {
+    fix x
+    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+      by (simp add: rinv lone rone)
+    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+  }
+qed
 
 (* effect on printed locale *)
 
@@ -225,7 +225,7 @@
     and trans: "[| x << y; y << z |] ==> x << z"
 
 sublocale order < dual: order "%x y. y << x"
-  apply (rule order.intro) apply (rule refl) apply (blast intro: trans)
+  apply new_unfold_locales apply (rule refl) apply (blast intro: trans)
   done
 
 print_locale! order  (* Only two instances of order. *)
@@ -244,7 +244,7 @@
 end
 
 sublocale order_with_def < dual: order' "op >>"
-  apply (intro order'.intro)
+  apply new_unfold_locales
   unfolding greater_def
   apply (rule refl) apply (blast intro: trans)
   done
@@ -291,14 +291,15 @@
 end
 
 sublocale trivial < x: trivial x _
-  apply (intro trivial.intro) using Q by fast
+  apply new_unfold_locales using Q by fast
 
 print_locale! trivial
 
 context trivial begin thm x.Q [where ?x = True] end
 
 sublocale trivial < y: trivial Q Q
-  apply (intro trivial.intro) using Q by fast
+  by new_unfold_locales
+  (* Succeeds since previous interpretation is more general. *)
 
 print_locale! trivial  (* No instance for y created (subsumed). *)
 

--- a/src/Pure/Isar/expression.ML	Fri Nov 28 12:26:14 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Nov 28 17:43:06 2008 +0100
@@ -598,15 +598,17 @@
 
 (*** Locale declarations ***)
 
+(* axiomsN: name of theorem set with destruct rules for locale predicates,
+     also name suffix of delta predicates and assumptions. *)
+
+val axiomsN = "axioms";
+
 local
 
 (* introN: name of theorems for introduction rules of locale and
-     delta predicates;
-   axiomsN: name of theorem set with destruct rules for locale predicates,
-     also name suffix of delta predicates. *)
+     delta predicates *)
 
 val introN = "intro";
-val axiomsN = "axioms";
 
 fun atomize_spec thy ts =
   let
@@ -695,7 +697,8 @@
             thy'
             |> Sign.add_path aname
             |> Sign.no_base_names
-            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
+            |> PureThy.note_thmss Thm.internalK
+              [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro, axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =
@@ -710,7 +713,7 @@
             |> Sign.add_path pname
             |> Sign.no_base_names
             |> PureThy.note_thmss Thm.internalK
-                 [((Name.binding introN, []), [([intro], [])]),
+                 [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
                   ((Name.binding axiomsN, []),
                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
             ||> Sign.restore_naming thy''';
@@ -757,20 +760,25 @@
       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
 
     val satisfy = Element.satisfy_morphism b_axioms;
+
     val params = fixed @
       (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
-    val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
-
+    val asm = if is_some b_statement then b_statement else a_statement;
+    val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
     val notes = body_elems' |>
       (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
       fst |> map (Element.morph_ctxt satisfy) |>
-      map_filter (fn Notes notes => SOME notes | _ => NONE);
+      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
+      (if is_some asm
+        then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
+          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
+        else I);
 
     val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
 
     val loc_ctxt = thy' |>
       NewLocale.register_locale name (extraTs, params)
-        (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], [])
+        (asm, map prop_of defs) ([], [])
         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
       NewLocale.init name
   in (name, loc_ctxt) end;
@@ -803,10 +811,10 @@
     val target = intern thy raw_target;
     val target_ctxt = NewLocale.init target thy;
 
-    val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
+    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     
     fun store_dep ((name, morph), thms) =
-      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
+      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
 
     fun after_qed' results =
       fold store_dep (deps ~~ prep_result propss results) #>
@@ -827,3 +835,4 @@
 
 
 end;
+

--- a/src/Pure/Isar/new_locale.ML	Fri Nov 28 12:26:14 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Nov 28 17:43:06 2008 +0100
@@ -37,7 +37,7 @@
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
   val add_dependency: string -> (string * Morphism.morphism) -> Proof.context -> Proof.context
 
-  (* Activate locales *)
+  (* Activation *)
   val activate_declarations: theory -> string * Morphism.morphism ->
     identifiers * Proof.context -> identifiers * Proof.context
   val activate_facts: theory -> string * Morphism.morphism ->
@@ -45,12 +45,36 @@
 (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
+  (* Reasoning about locales *)
+  val witness_attrib: attribute
+  val intro_attrib: attribute
+  val unfold_attrib: attribute
+  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
+
   (* Diagnostic *)
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> bstring -> unit
 end;
 
 
+(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
+functor ThmsFun() =
+struct
+
+structure Data = GenericDataFun
+(
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Thm.merge_thms;
+);
+
+val get = Data.get o Context.Proof;
+val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
+
+end;
+
+
 structure NewLocale: NEW_LOCALE =
 struct
 
@@ -340,5 +364,34 @@
     (fn (parameters, spec, decls, notes, dependencies) =>
       (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies)));
 
+
+(*** Reasoning about locales ***)
+
+(** Storage for witnesses, intro and unfold rules **)
+
+structure Witnesses = ThmsFun();
+structure Intros = ThmsFun();
+structure Unfolds = ThmsFun();
+
+val witness_attrib = Witnesses.add;
+val intro_attrib = Intros.add;
+val unfold_attrib = Unfolds.add;
+
+(** Tactic **)
+
+fun intro_locales_tac eager ctxt facts st =
+  Method.intros_tac
+    (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
+
+val _ = Context.>> (Context.map_theory
+  (Method.add_methods
+    [("new_intro_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+      "back-chain introduction rules of locales without unfolding predicates"),
+     ("new_unfold_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+      "back-chain all introduction rules of locales")]));
+
+
 end;