First version of global registration command.
authorballarin
Wed Mar 09 18:44:52 2005 +0100 (2005-03-09 ago)
changeset 155968665d08085df
parent 15595 dc8a41c7cefc
child 15597 b5f5722ed703
First version of global registration command.
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/FOL/IsaMakefile
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/delta_data.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/toplevel.ML
src/Pure/ROOT.ML
src/Pure/axclass.ML
src/Pure/logic.ML
     1.1 --- a/etc/isar-keywords-ZF.el	Tue Mar 08 16:02:52 2005 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Wed Mar 09 18:44:52 2005 +0100
     1.3 @@ -113,6 +113,7 @@
     1.4      "print_locale"
     1.5      "print_locales"
     1.6      "print_methods"
     1.7 +    "print_registrations"
     1.8      "print_rules"
     1.9      "print_simpset"
    1.10      "print_syntax"
    1.11 @@ -131,6 +132,7 @@
    1.12      "realizability"
    1.13      "realizers"
    1.14      "redo"
    1.15 +    "registration"
    1.16      "remove_thy"
    1.17      "rep_datatype"
    1.18      "sect"
    1.19 @@ -263,6 +265,7 @@
    1.20      "print_locale"
    1.21      "print_locales"
    1.22      "print_methods"
    1.23 +    "print_registrations"
    1.24      "print_rules"
    1.25      "print_simpset"
    1.26      "print_syntax"
    1.27 @@ -362,6 +365,7 @@
    1.28    '("corollary"
    1.29      "instance"
    1.30      "lemma"
    1.31 +    "registration"
    1.32      "theorem"))
    1.33  
    1.34  (defconst isar-keywords-qed
     2.1 --- a/etc/isar-keywords.el	Tue Mar 08 16:02:52 2005 +0100
     2.2 +++ b/etc/isar-keywords.el	Wed Mar 09 18:44:52 2005 +0100
     2.3 @@ -116,6 +116,7 @@
     2.4      "print_locale"
     2.5      "print_locales"
     2.6      "print_methods"
     2.7 +    "print_registrations"
     2.8      "print_rules"
     2.9      "print_simpset"
    2.10      "print_syntax"
    2.11 @@ -136,6 +137,7 @@
    2.12      "recdef_tc"
    2.13      "record"
    2.14      "redo"
    2.15 +    "registration"
    2.16      "refute"
    2.17      "refute_params"
    2.18      "remove_thy"
    2.19 @@ -288,6 +290,7 @@
    2.20      "print_locale"
    2.21      "print_locales"
    2.22      "print_methods"
    2.23 +    "print_registrations"
    2.24      "print_rules"
    2.25      "print_simpset"
    2.26      "print_syntax"
    2.27 @@ -394,6 +397,7 @@
    2.28      "instance"
    2.29      "lemma"
    2.30      "recdef_tc"
    2.31 +    "registration"
    2.32      "specification"
    2.33      "theorem"
    2.34      "typedef"))
     3.1 --- a/src/FOL/IsaMakefile	Tue Mar 08 16:02:52 2005 +0100
     3.2 +++ b/src/FOL/IsaMakefile	Wed Mar 09 18:44:52 2005 +0100
     3.3 @@ -46,6 +46,7 @@
     3.4  
     3.5  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
     3.6    ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
     3.7 +  ex/LocaleTest.thy \
     3.8    ex/LocaleInst.thy \
     3.9    ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
    3.10    ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Mar 09 18:44:52 2005 +0100
     4.3 @@ -0,0 +1,76 @@
     4.4 +(*  Title:      FOL/ex/LocaleTest.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Clemens Ballarin
     4.7 +    Copyright (c) 2005 by Clemens Ballarin
     4.8 +
     4.9 +Collection of regression tests for locales.
    4.10 +*)
    4.11 +
    4.12 +header {* Test of Locale instantiation *}
    4.13 +
    4.14 +theory LocaleTest = FOL:
    4.15 +
    4.16 +(* registration input syntax *)
    4.17 +
    4.18 +locale L
    4.19 +locale M = fixes a and b and c
    4.20 +
    4.21 +registration test [simp]: L + M a b c [x y z] .
    4.22 +
    4.23 +print_registrations L
    4.24 +print_registrations M
    4.25 +
    4.26 +registration test [simp]: L .
    4.27 +
    4.28 +registration L .
    4.29 +
    4.30 +(* processing of locale expression *)
    4.31 +
    4.32 +ML {* reset show_hyps *}
    4.33 +
    4.34 +locale A = fixes a assumes asm_A: "a = a"
    4.35 +
    4.36 +locale (open) B = fixes b assumes asm_B [simp]: "b = b"
    4.37 +
    4.38 +locale C = A + B + assumes asm_C: "c = c"
    4.39 +  (* TODO: independent type var in c, prohibit locale declaration *)
    4.40 +
    4.41 +locale D = A + B + fixes d defines def_D: "d == (a = b)"
    4.42 +
    4.43 +ML {* set show_sorts *}
    4.44 +
    4.45 +typedecl i
    4.46 +arities i :: "term"
    4.47 +
    4.48 +ML {* set Toplevel.debug *}
    4.49 +
    4.50 +registration p1: C ["X::'b" "Y"] by (auto intro: A.intro C_axioms.intro)
    4.51 +  (* both X and Y get type 'b since 'b is the internal type of parameter b,
    4.52 +     not wanted, but put up with for now. *)
    4.53 +
    4.54 +ML {* set show_hyps *}
    4.55 +
    4.56 +print_registrations A
    4.57 +
    4.58 +(* thm asm_A a.asm_A p1.a.asm_A *)
    4.59 +
    4.60 +(*
    4.61 +registration p2: D [X Y Z] sorry
    4.62 +
    4.63 +print_registrations D
    4.64 +*)
    4.65 +
    4.66 +registration p3: D [X Y] by (auto intro: A.intro)
    4.67 +
    4.68 +print_registrations A
    4.69 +print_registrations B
    4.70 +print_registrations C
    4.71 +print_registrations D
    4.72 +
    4.73 +(* not permitted
    4.74 +registration p4: A ["?x10"] apply (rule A.intro) apply rule done
    4.75 +
    4.76 +print_registrations A
    4.77 +*)
    4.78 +
    4.79 +end
     5.1 --- a/src/HOL/Algebra/UnivPoly.thy	Tue Mar 08 16:02:52 2005 +0100
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Mar 09 18:44:52 2005 +0100
     5.3 @@ -369,6 +369,29 @@
     5.4      done
     5.5  qed (simp_all add: R)
     5.6  
     5.7 +(*
     5.8 +Strange phenomenon in Isar:
     5.9 +
    5.10 +theorem (in UP_cring) UP_cring:
    5.11 +  "cring P"
    5.12 +proof (rule cringI)
    5.13 +  show "abelian_group P" proof (rule abelian_groupI)
    5.14 +  fix x y z
    5.15 +  assume "x \<in> carrier P" and "y \<in> carrier P" and "z \<in> carrier P"
    5.16 +  {
    5.17 +  show "x \<oplus>\<^bsub>P\<^esub> y \<in> carrier P" sorry
    5.18 +  next
    5.19 +  show "x \<oplus>\<^bsub>P\<^esub> y \<oplus>\<^bsub>P\<^esub> z = x \<oplus>\<^bsub>P\<^esub> (y \<oplus>\<^bsub>P\<^esub> z)" sorry
    5.20 +  next
    5.21 +  show "x \<oplus>\<^bsub>P\<^esub> y = y \<oplus>\<^bsub>P\<^esub> x" sorry
    5.22 +  next
    5.23 +  show "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> x = x" sorry
    5.24 +  next
    5.25 +  show "\<exists>y\<in>carrier P. y \<oplus>\<^bsub>P\<^esub> x = \<zero>\<^bsub>P\<^esub>" sorry
    5.26 +  next
    5.27 +  show "\<zero>\<^bsub>P\<^esub> \<in> carrier P" sorry  last goal rejected!!!
    5.28 +*)
    5.29 +
    5.30  theorem (in UP_cring) UP_cring:
    5.31    "cring P"
    5.32    by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
     6.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Tue Mar 08 16:02:52 2005 +0100
     6.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Mar 09 18:44:52 2005 +0100
     6.3 @@ -249,7 +249,6 @@
     6.4  instance up :: (ring) ring
     6.5  proof
     6.6    fix p q r :: "'a::ring up"
     6.7 -  fix n
     6.8    show "(p + q) + r = p + (q + r)"
     6.9      by (rule up_eqI) simp
    6.10    show "0 + p = p"
    6.11 @@ -318,6 +317,7 @@
    6.12      by (simp add: up_inverse_def)
    6.13    show "p / q = p * inverse q"
    6.14      by (simp add: up_divide_def)
    6.15 +  fix n
    6.16    show "p ^ n = nat_rec 1 (%u b. b * p) n"
    6.17      by (simp add: up_power_def)
    6.18    qed
     7.1 --- a/src/Pure/Isar/args.ML	Tue Mar 08 16:02:52 2005 +0100
     7.2 +++ b/src/Pure/Isar/args.ML	Wed Mar 09 18:44:52 2005 +0100
     7.3 @@ -43,11 +43,11 @@
     7.4    val global_typ: theory * T list -> typ * (theory * T list)
     7.5    val global_term: theory * T list -> term * (theory * T list)
     7.6    val global_prop: theory * T list -> term * (theory * T list)
     7.7 -  val local_typ_raw: Proof.context * T list -> typ * (Proof.context * T list)
     7.8 -  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
     7.9 -  val local_term: Proof.context * T list -> term * (Proof.context * T list)
    7.10 -  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    7.11 -  val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
    7.12 +  val local_typ_raw: ProofContext.context * T list -> typ * (ProofContext.context * T list)
    7.13 +  val local_typ: ProofContext.context * T list -> typ * (ProofContext.context * T list)
    7.14 +  val local_term: ProofContext.context * T list -> term * (ProofContext.context * T list)
    7.15 +  val local_prop: ProofContext.context * T list -> term * (ProofContext.context * T list)
    7.16 +  val bang_facts: ProofContext.context * T list -> thm list * (ProofContext.context * T list)
    7.17    val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
    7.18      -> ((int -> tactic) -> tactic) * ('a * T list)
    7.19    type src
     8.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 08 16:02:52 2005 +0100
     8.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 09 18:44:52 2005 +0100
     8.3 @@ -18,6 +18,7 @@
     8.4    exception ATTRIB_FAIL of (string * Position.T) * exn
     8.5    val global_attribute: theory -> Args.src -> theory attribute
     8.6    val local_attribute: theory -> Args.src -> Proof.context attribute
     8.7 +  val multi_attribute: theory -> Args.src -> Locale.multi_attribute
     8.8    val local_attribute': Proof.context -> Args.src -> Proof.context attribute
     8.9    val undef_global_attribute: theory attribute
    8.10    val undef_local_attribute: Proof.context attribute
    8.11 @@ -96,6 +97,8 @@
    8.12  
    8.13  val global_attribute = gen_attribute fst;
    8.14  val local_attribute = gen_attribute snd;
    8.15 +fun multi_attribute thy src =
    8.16 +      (global_attribute thy src, local_attribute thy src);
    8.17  val local_attribute' = local_attribute o ProofContext.theory_of;
    8.18  
    8.19  val undef_global_attribute: theory attribute =
     9.1 --- a/src/Pure/Isar/delta_data.ML	Tue Mar 08 16:02:52 2005 +0100
     9.2 +++ b/src/Pure/Isar/delta_data.ML	Wed Mar 09 18:44:52 2005 +0100
     9.3 @@ -1,4 +1,5 @@
     9.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory (06/01/05)
     9.5 +    $Id$
     9.6      Copyright 2004 University of Cambridge
     9.7  
     9.8  Used for delta_simpset and delta_claset
    10.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 08 16:02:52 2005 +0100
    10.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 09 18:44:52 2005 +0100
    10.3 @@ -49,6 +49,7 @@
    10.4    val print_locales: Toplevel.transition -> Toplevel.transition
    10.5    val print_locale: Locale.expr * Args.src Locale.element list
    10.6      -> Toplevel.transition -> Toplevel.transition
    10.7 +  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
    10.8    val print_attributes: Toplevel.transition -> Toplevel.transition
    10.9    val print_rules: Toplevel.transition -> Toplevel.transition
   10.10    val print_induct_rules: Toplevel.transition -> Toplevel.transition
   10.11 @@ -218,7 +219,12 @@
   10.12  
   10.13  fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   10.14    let val thy = Toplevel.theory_of state in
   10.15 -    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.local_attribute thy)) body)
   10.16 +    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body)
   10.17 +  end);
   10.18 +
   10.19 +fun print_registrations name = Toplevel.unknown_theory o
   10.20 +  Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in
   10.21 +    Locale.print_global_registrations thy name
   10.22    end);
   10.23  
   10.24  val print_attributes = Toplevel.unknown_theory o
    11.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Mar 08 16:02:52 2005 +0100
    11.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 09 18:44:52 2005 +0100
    11.3 @@ -310,6 +310,17 @@
    11.4          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    11.5        >> (Toplevel.theory o IsarThy.add_locale o (fn ((x, y), (z, w)) => (x, y, z, w))));
    11.6  
    11.7 +val uterm = P.underscore >> K NONE || P.term >> SOME;
    11.8 +
    11.9 +val view_val =
   11.10 +  Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") [];
   11.11 +
   11.12 +val registrationP =
   11.13 +  OuterSyntax.command "registration"
   11.14 +  "prove and register instance of locale expression" K.thy_goal
   11.15 +  ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val
   11.16 +     >> IsarThy.register_globally)
   11.17 +   >> (Toplevel.print oo Toplevel.theory_to_proof));
   11.18  
   11.19  
   11.20  (** proof commands **)
   11.21 @@ -579,9 +590,14 @@
   11.22      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   11.23  
   11.24  val print_localeP =
   11.25 -  OuterSyntax.improper_command "print_locale" "print named locale of this theory" K.diag
   11.26 +  OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   11.27      (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   11.28  
   11.29 +val print_registrationsP =
   11.30 +  OuterSyntax.improper_command "print_registrations"
   11.31 +    "print registrations of named locale in this theory" K.diag
   11.32 +    (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
   11.33 +
   11.34  val print_attributesP =
   11.35    OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
   11.36      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   11.37 @@ -784,10 +800,11 @@
   11.38    default_proofP, immediate_proofP, done_proofP, skip_proofP,
   11.39    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
   11.40    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
   11.41 -  redoP, undos_proofP, undoP, killP, instantiateP,
   11.42 +  redoP, undos_proofP, undoP, killP, registrationP, instantiateP,
   11.43    (*diagnostic commands*)
   11.44    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   11.45    print_syntaxP, print_theoremsP, print_localesP, print_localeP,
   11.46 +  print_registrationsP,
   11.47    print_attributesP, print_rulesP, print_induct_rulesP,
   11.48    print_trans_rulesP, print_methodsP, print_antiquotationsP,
   11.49    thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
    12.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Mar 08 16:02:52 2005 +0100
    12.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Mar 09 18:44:52 2005 +0100
    12.3 @@ -22,8 +22,8 @@
    12.4      ((bstring * Args.src list) * (thmref * Args.src list) list) list
    12.5      -> theory -> theory * (bstring * thm list) list
    12.6    val locale_theorems_i: string -> string ->
    12.7 -    ((bstring * Proof.context attribute list)
    12.8 -      * (thm list * Proof.context attribute list) list) list
    12.9 +    ((bstring * Locale.multi_attribute list)
   12.10 +      * (thm list * Locale.multi_attribute list) list) list
   12.11      -> theory -> theory * (string * thm list) list
   12.12    val smart_theorems: string -> xstring option ->
   12.13      ((bstring * Args.src list) * (thmref * Args.src list) list) list
   12.14 @@ -58,21 +58,21 @@
   12.15      -> bool -> theory -> ProofHistory.T
   12.16    val theorem_i: string -> (bstring * theory attribute list) *
   12.17      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
   12.18 -  val multi_theorem: string -> bstring * Args.src list
   12.19 +  val multi_theorem: string -> (theory -> theory) -> bstring * Args.src list
   12.20      -> Args.src Locale.element Locale.elem_expr list
   12.21      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
   12.22      -> bool -> theory -> ProofHistory.T
   12.23 -  val multi_theorem_i: string -> bstring * theory attribute list
   12.24 -    -> Proof.context attribute Locale.element_i Locale.elem_expr list
   12.25 +  val multi_theorem_i: string -> (theory -> theory) -> bstring * theory attribute list
   12.26 +    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
   12.27      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
   12.28      -> bool -> theory -> ProofHistory.T
   12.29    val locale_multi_theorem: string -> xstring
   12.30      -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
   12.31      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
   12.32      -> bool -> theory -> ProofHistory.T
   12.33 -  val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list
   12.34 -    -> Proof.context attribute Locale.element_i Locale.elem_expr list
   12.35 -    -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
   12.36 +  val locale_multi_theorem_i: string -> string -> bstring * Locale.multi_attribute list
   12.37 +    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
   12.38 +    -> ((bstring * Locale.multi_attribute list) * (term * (term list * term list)) list) list
   12.39      -> bool -> theory -> ProofHistory.T
   12.40    val smart_multi_theorem: string -> xstring option
   12.41      -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
   12.42 @@ -153,12 +153,16 @@
   12.43      -> Toplevel.transition -> Toplevel.transition
   12.44    val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
   12.45    val context: string -> Toplevel.transition -> Toplevel.transition
   12.46 +
   12.47 +  val register_globally:
   12.48 +    ((string * Args.src list) * Locale.expr) * string option list ->
   12.49 +    bool -> theory -> ProofHistory.T
   12.50 +
   12.51  end;
   12.52  
   12.53  structure IsarThy: ISAR_THY =
   12.54  struct
   12.55  
   12.56 -
   12.57  (** derived theory and proof operations **)
   12.58  
   12.59  (* name spaces *)
   12.60 @@ -213,6 +217,7 @@
   12.61  
   12.62  fun global_attribs thy = prep_attribs (Attrib.global_attribute thy);
   12.63  fun local_attribs thy = prep_attribs (Attrib.local_attribute thy);
   12.64 +fun multi_attribs thy = prep_attribs (Attrib.multi_attribute thy);
   12.65  
   12.66  end;
   12.67  
   12.68 @@ -236,13 +241,13 @@
   12.69    |> present_thmss k;
   12.70  
   12.71  fun locale_theorems k loc args thy = thy
   12.72 -  |> Locale.note_thmss k loc (local_attribs thy args)
   12.73 +  |> Locale.note_thmss k loc (multi_attribs thy args)
   12.74    |> present_thmss k;
   12.75  
   12.76  fun smart_theorems k opt_loc args thy = thy
   12.77    |> (case opt_loc of
   12.78      NONE => PureThy.note_thmss (Drule.kind k) (global_attribs thy args)
   12.79 -  | SOME loc => Locale.note_thmss k loc (local_attribs thy args))
   12.80 +  | SOME loc => Locale.note_thmss k loc (multi_attribs thy args))
   12.81    |> present_thmss k;
   12.82  
   12.83  fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
   12.84 @@ -370,27 +375,27 @@
   12.85  
   12.86  in
   12.87  
   12.88 -fun multi_theorem k a elems concl int thy =
   12.89 -  global_statement (Proof.multi_theorem k NONE (apsnd (map (Attrib.global_attribute thy)) a)
   12.90 -    (map (Locale.map_attrib_elem_or_expr (Attrib.local_attribute thy)) elems)) concl int thy;
   12.91 +fun multi_theorem k thy_mod a elems concl int thy =
   12.92 +  global_statement (Proof.multi_theorem k thy_mod NONE (apsnd (map (Attrib.global_attribute thy)) a)
   12.93 +    (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems)) concl int thy;
   12.94  
   12.95 -fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k NONE a;
   12.96 +fun multi_theorem_i k thy_mod a = global_statement_i o Proof.multi_theorem_i k thy_mod NONE a;
   12.97  
   12.98  fun locale_multi_theorem k locale (name, atts) elems concl int thy =
   12.99 -  global_statement (Proof.multi_theorem k
  12.100 -      (SOME (locale, (map (Attrib.local_attribute thy) atts,
  12.101 -          map (map (Attrib.local_attribute thy) o snd o fst) concl)))
  12.102 -      (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.local_attribute thy)) elems))
  12.103 +  global_statement (Proof.multi_theorem k I
  12.104 +      (SOME (locale, (map (Attrib.multi_attribute thy) atts,
  12.105 +          map (map (Attrib.multi_attribute thy) o snd o fst) concl)))
  12.106 +      (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.multi_attribute thy)) elems))
  12.107        (map (apfst (apsnd (K []))) concl) int thy;
  12.108  
  12.109  fun locale_multi_theorem_i k locale (name, atts) elems concl =
  12.110 -  global_statement_i (Proof.multi_theorem_i k (SOME (locale, (atts, map (snd o fst) concl)))
  12.111 +  global_statement_i (Proof.multi_theorem_i k I (SOME (locale, (atts, map (snd o fst) concl)))
  12.112        (name, []) elems) (map (apfst (apsnd (K []))) concl);
  12.113  
  12.114 -fun theorem k (a, t) = multi_theorem k a [] [(("", []), [t])];
  12.115 -fun theorem_i k (a, t) = multi_theorem_i k a [] [(("", []), [t])];
  12.116 +fun theorem k (a, t) = multi_theorem k I a [] [(("", []), [t])];
  12.117 +fun theorem_i k (a, t) = multi_theorem_i k I a [] [(("", []), [t])];
  12.118  
  12.119 -fun smart_multi_theorem k NONE a elems = multi_theorem k a elems
  12.120 +fun smart_multi_theorem k NONE a elems = multi_theorem k I a elems
  12.121    | smart_multi_theorem k (SOME locale) a elems = locale_multi_theorem k locale a elems;
  12.122  
  12.123  val assume      = local_statement Proof.assume I;
  12.124 @@ -582,8 +587,7 @@
  12.125  
  12.126  fun add_locale (do_pred, name, import, body) thy =
  12.127    Locale.add_locale do_pred name import
  12.128 -    (map (Locale.map_attrib_element (Attrib.local_attribute thy)) body) thy;
  12.129 -
  12.130 +    (map (Locale.map_attrib_element (Attrib.multi_attribute thy)) body) thy;
  12.131  
  12.132  (* theory init and exit *)
  12.133  
  12.134 @@ -621,4 +625,23 @@
  12.135  val context = init_context (ThyInfo.quiet_update_thy true);
  12.136  
  12.137  
  12.138 +(* global locale registration *)
  12.139 +
  12.140 +fun register_globally (((prfx, atts), expr), insts) b (* bool *) thy =
  12.141 +  let
  12.142 +    val (thy', propss, activate) =
  12.143 +          Locale.prep_registration (prfx, []) expr insts thy;
  12.144 +(* TODO: convert atts *)
  12.145 +    fun register id (thy, thm) = let
  12.146 +        val thm' = Drule.freeze_all thm;
  12.147 +      in
  12.148 +        (Locale.global_activate_thm id thm' thy, thm')
  12.149 +      end;
  12.150 +  in
  12.151 +    multi_theorem_i Drule.internalK activate ("", []) [] 
  12.152 +      (map (fn (id as (n, _), props) => ((NameSpace.base n, [register id]), 
  12.153 +        map (fn prop => (prop, ([], []))) props)) propss) b thy'
  12.154 +  end;
  12.155 +
  12.156 +
  12.157  end;
    13.1 --- a/src/Pure/Isar/locale.ML	Tue Mar 08 16:02:52 2005 +0100
    13.2 +++ b/src/Pure/Isar/locale.ML	Wed Mar 09 18:44:52 2005 +0100
    13.3 @@ -21,6 +21,7 @@
    13.4  signature LOCALE =
    13.5  sig
    13.6    type context
    13.7 +  type multi_attribute
    13.8  
    13.9    (* Constructors for elem, expr and elem_expr are
   13.10       currently only used for inputting locales (outer_parse.ML). *)
   13.11 @@ -43,43 +44,55 @@
   13.12    val intern: Sign.sg -> xstring -> string
   13.13    val cond_extern: Sign.sg -> string -> xstring
   13.14    val the_locale: theory -> string -> locale
   13.15 -  val map_attrib_element: ('att -> context attribute) -> 'att element ->
   13.16 -    context attribute element
   13.17 -  val map_attrib_element_i: ('att -> context attribute) -> 'att element_i ->
   13.18 -    context attribute element_i
   13.19 -  val map_attrib_elem_or_expr: ('att -> context attribute) ->
   13.20 -    'att element elem_expr -> context attribute element elem_expr
   13.21 -  val map_attrib_elem_or_expr_i: ('att -> context attribute) ->
   13.22 -    'att element_i elem_expr -> context attribute element_i elem_expr
   13.23 +  val map_attrib_element: ('att -> multi_attribute) -> 'att element ->
   13.24 +    multi_attribute element
   13.25 +  val map_attrib_element_i: ('att -> multi_attribute) -> 'att element_i ->
   13.26 +    multi_attribute element_i
   13.27 +  val map_attrib_elem_or_expr: ('att -> multi_attribute) ->
   13.28 +    'att element elem_expr -> multi_attribute element elem_expr
   13.29 +  val map_attrib_elem_or_expr_i: ('att -> multi_attribute) ->
   13.30 +    'att element_i elem_expr -> multi_attribute element_i elem_expr
   13.31  
   13.32 +  (* Processing of locale statements *)
   13.33    val read_context_statement: xstring option ->
   13.34 -    context attribute element elem_expr list ->
   13.35 +    multi_attribute element elem_expr list ->
   13.36      (string * (string list * string list)) list list -> context ->
   13.37      string option * (cterm list * cterm list) * context * context * 
   13.38        (term * (term list * term list)) list list
   13.39    val cert_context_statement: string option ->
   13.40 -    context attribute element_i elem_expr list ->
   13.41 +    multi_attribute element_i elem_expr list ->
   13.42      (term * (term list * term list)) list list -> context ->
   13.43      string option * (cterm list * cterm list) * context * context *
   13.44        (term * (term list * term list)) list list
   13.45 +
   13.46 +  (* Diagnostic functions *)
   13.47    val print_locales: theory -> unit
   13.48 -  val print_locale: theory -> expr -> context attribute element list -> unit
   13.49 -  val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
   13.50 -  val add_locale_i: bool -> bstring -> expr -> context attribute element_i list
   13.51 +  val print_locale: theory -> expr -> multi_attribute element list -> unit
   13.52 +  val print_global_registrations: theory -> string -> unit
   13.53 +
   13.54 +  val add_locale: bool -> bstring -> expr -> multi_attribute element list -> theory -> theory
   13.55 +  val add_locale_i: bool -> bstring -> expr -> multi_attribute element_i list
   13.56      -> theory -> theory
   13.57    val smart_note_thmss: string -> (string * 'a) option ->
   13.58      ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
   13.59      theory -> theory * (bstring * thm list) list
   13.60    val note_thmss: string -> xstring ->
   13.61 -    ((bstring * context attribute list) * (thmref * context attribute list) list) list ->
   13.62 +    ((bstring * multi_attribute list) * (thmref * multi_attribute list) list) list ->
   13.63      theory -> theory * (bstring * thm list) list
   13.64    val note_thmss_i: string -> string ->
   13.65 -    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
   13.66 +    ((bstring * multi_attribute list) * (thm list * multi_attribute list) list) list ->
   13.67      theory -> theory * (bstring * thm list) list
   13.68 -  val add_thmss: string -> ((string * thm list) * context attribute list) list ->
   13.69 +  val add_thmss: string -> ((string * thm list) * multi_attribute list) list ->
   13.70      theory * context -> (theory * context) * (string * thm list) list
   13.71 +
   13.72    val instantiate: string -> string * context attribute list
   13.73      -> thm list option -> context -> context
   13.74 +  val prep_registration:
   13.75 +    string * theory attribute list -> expr -> string option list -> theory ->
   13.76 +    theory * ((string * term list) * term list) list * (theory -> theory)
   13.77 +  val global_activate_thm:
   13.78 +    string * term list -> thm -> theory -> theory
   13.79 +
   13.80    val setup: (theory -> theory) list
   13.81  end;
   13.82  
   13.83 @@ -90,6 +103,10 @@
   13.84  
   13.85  type context = ProofContext.context;
   13.86  
   13.87 +(* Locales store theory attributes (for activation in theories)
   13.88 +   and context attributes (for activation in contexts) *)
   13.89 +type multi_attribute = theory attribute * context attribute;
   13.90 +
   13.91  datatype ('typ, 'term, 'fact, 'att) elem =
   13.92    Fixes of (string * 'typ option * mixfix option) list |
   13.93    Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
   13.94 @@ -121,29 +138,44 @@
   13.95         (cf. [1], normalisation of locale expressions.)
   13.96      *)
   13.97    import: expr,                                       (*dynamic import*)
   13.98 -  elems: (context attribute element_i * stamp) list,  (*static content*)
   13.99 +  elems: (multi_attribute element_i * stamp) list,  (*static content*)
  13.100    params: (string * typ option) list * string list}   (*all/local params*)
  13.101  
  13.102  
  13.103  (** theory data **)
  13.104  
  13.105 +structure Termlisttab = TableFun(type key = term list
  13.106 +  val ord = Library.list_ord Term.term_ord);
  13.107 +
  13.108  structure LocalesArgs =
  13.109  struct
  13.110    val name = "Isar/locales";
  13.111 -  type T = NameSpace.T * locale Symtab.table;
  13.112 +  type T = NameSpace.T * locale Symtab.table *
  13.113 +      ((string * theory attribute list) * thm list) Termlisttab.table
  13.114 +        Symtab.table;
  13.115 +    (* 1st entry: locale namespace,
  13.116 +       2nd entry: locales of the theory,
  13.117 +       3rd entry: registrations: theorems instantiating locale assumptions,
  13.118 +         with prefix and attributes, indexed by locale name and parameter
  13.119 +         instantiation *)
  13.120  
  13.121 -  val empty = (NameSpace.empty, Symtab.empty);
  13.122 +  val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
  13.123    val copy = I;
  13.124    val prep_ext = I;
  13.125  
  13.126 -  (*joining of locale elements: only facts may be added later!*)
  13.127 -  fun join ({predicate, import, elems, params}: locale, {elems = elems', ...}: locale) =
  13.128 -    SOME {predicate = predicate, import = import, elems = gen_merge_lists eq_snd elems elems',
  13.129 +  fun join_locs ({predicate, import, elems, params}: locale,
  13.130 +      {elems = elems', ...}: locale) =
  13.131 +    SOME {predicate = predicate, import = import,
  13.132 +      elems = gen_merge_lists eq_snd elems elems',
  13.133        params = params};
  13.134 -  fun merge ((space1, locs1), (space2, locs2)) =
  13.135 -    (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2));
  13.136 +  (* joining of registrations: prefix and attributes of left theory,
  13.137 +     thmsss are equal *)
  13.138 +  fun join_regs (reg, _) = SOME reg;
  13.139 +  fun merge ((space1, locs1, regs1), (space2, locs2, regs2)) =
  13.140 +    (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
  13.141 +     Symtab.join (SOME o Termlisttab.join join_regs) (regs1, regs2));
  13.142  
  13.143 -  fun print _ (space, locs) =
  13.144 +  fun print _ (space, locs, _) =
  13.145      Pretty.strs ("locales:" :: map (NameSpace.cond_extern space o #1) (Symtab.dest locs))
  13.146      |> Pretty.writeln;
  13.147  end;
  13.148 @@ -158,9 +190,13 @@
  13.149  (* access locales *)
  13.150  
  13.151  fun declare_locale name =
  13.152 -  LocalesData.map (apfst (fn space => (NameSpace.extend (space, [name]))));
  13.153 +  LocalesData.map (fn (space, locs, regs) =>
  13.154 +    (NameSpace.extend (space, [name]), locs, regs));
  13.155  
  13.156 -fun put_locale name loc = LocalesData.map (apsnd (fn locs => Symtab.update ((name, loc), locs)));
  13.157 +fun put_locale name loc =
  13.158 +  LocalesData.map (fn (space, locs, regs) =>
  13.159 +    (space, Symtab.update ((name, loc), locs), regs));
  13.160 +
  13.161  fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy), name);
  13.162  
  13.163  fun the_locale thy name =
  13.164 @@ -169,6 +205,38 @@
  13.165    | NONE => error ("Unknown locale " ^ quote name));
  13.166  
  13.167  
  13.168 +(* access registrations *)
  13.169 +
  13.170 +(* add registration to theory, ignored if already present *)
  13.171 +
  13.172 +fun global_put_registration (name, ps) attn =
  13.173 +  LocalesData.map (fn (space, locs, regs) =>
  13.174 +    (space, locs, let
  13.175 +        val tab = getOpt (Symtab.lookup (regs, name), Termlisttab.empty);
  13.176 +      in
  13.177 +        Symtab.update ((name, Termlisttab.update_new ((ps, (attn, [])), tab)),
  13.178 +          regs)
  13.179 +      end handle Termlisttab.DUP _ => regs));
  13.180 +
  13.181 +(* add theorem to registration in theory,
  13.182 +   ignored if registration not present *)
  13.183 +
  13.184 +fun global_put_registration_thm (name, ps) thm =
  13.185 +  LocalesData.map (fn (space, locs, regs) =>
  13.186 +    (space, locs, let
  13.187 +        val tab = valOf (Symtab.lookup (regs, name));
  13.188 +        val (x, thms) = valOf (Termlisttab.lookup (tab, ps));
  13.189 +      in
  13.190 +        Symtab.update ((name, Termlisttab.update ((ps, (x, thm::thms)), tab)),
  13.191 +          regs)
  13.192 +      end handle Option => regs))
  13.193 +
  13.194 +fun global_get_registration thy (name, ps) =
  13.195 +  case Symtab.lookup (#3 (LocalesData.get thy), name) of
  13.196 +      NONE => NONE
  13.197 +    | SOME tab => Termlisttab.lookup (tab, ps);
  13.198 +
  13.199 +
  13.200  (* import hierarchy
  13.201     implementation could be more efficient, eg. by maintaining a database
  13.202     of dependencies *)
  13.203 @@ -187,6 +255,29 @@
  13.204    end;
  13.205  
  13.206  
  13.207 +(* registrations *)
  13.208 +
  13.209 +fun print_global_registrations thy loc =
  13.210 +  let
  13.211 +    val sg = Theory.sign_of thy;
  13.212 +    val loc_int = intern sg loc;
  13.213 +    val (_, _, regs) = LocalesData.get thy;
  13.214 +    val prt_term = Pretty.quote o Sign.pretty_term sg;
  13.215 +    fun prt_inst (ts, ((prfx, _), thms)) = let
  13.216 +in
  13.217 +      Pretty.block [Pretty.str prfx, Pretty.str ":", Pretty.brk 1,
  13.218 +        Pretty.list "(" ")" (map prt_term ts)]
  13.219 +end;
  13.220 +    val loc_regs = Symtab.lookup (regs, loc_int);
  13.221 +  in
  13.222 +    (case loc_regs of
  13.223 +        NONE => Pretty.str "No registrations."
  13.224 +      | SOME r => Pretty.big_list "registrations:"
  13.225 +          (map prt_inst (Termlisttab.dest r)))
  13.226 +    |> Pretty.writeln
  13.227 +  end;
  13.228 +
  13.229 +
  13.230  (* diagnostics *)
  13.231  
  13.232  fun err_in_locale ctxt msg ids =
  13.233 @@ -425,9 +516,34 @@
  13.234              map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);
  13.235        in map inst (elemss ~~ envs) end;
  13.236  
  13.237 +(* flatten_expr:
  13.238 +   Extend list of identifiers by those new in locale expression expr.
  13.239 +   Compute corresponding list of lists of locale elements (one entry per
  13.240 +   identifier).
  13.241 +
  13.242 +   Identifiers represent locale fragments and are in an extended form:
  13.243 +     ((name, ps), (ax_ps, axs))
  13.244 +   (name, ps) is the locale name with all its parameters.
  13.245 +   (ax_ps, axs) is the locale axioms with its parameters;
  13.246 +     axs are always taken from the top level of the locale hierarchy,
  13.247 +     hence axioms may contain additional parameters from later fragments:
  13.248 +     ps subset of ax_ps.  axs is either singleton or empty.
  13.249 +
  13.250 +   Elements are enriched by identifier-like information:
  13.251 +     (((name, ax_ps), axs), elems)
  13.252 +   The parameters in ax_ps are the axiom parameters, but enriched by type
  13.253 +   info: now each entry is a pair of string and typ option.  Axioms are
  13.254 +   type-instantiated.
  13.255 +
  13.256 +*)
  13.257 +
  13.258  fun flatten_expr ctxt (prev_idents, expr) =
  13.259    let
  13.260      val thy = ProofContext.theory_of ctxt;
  13.261 +    (* thy used for retrieval of locale info,
  13.262 +       ctxt for error messages, parameter unification and instantiation
  13.263 +       of axioms *)
  13.264 +    (* TODO: consider err_in_locale with thy argument *)
  13.265  
  13.266      fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
  13.267        | renaming (NONE :: xs) (y :: ys) = renaming xs ys
  13.268 @@ -444,7 +560,7 @@
  13.269        end;
  13.270  
  13.271      fun identify top (Locale name) =
  13.272 -    (* CB: ids is a list of tuples of the form ((name, ps)  axs),
  13.273 +    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
  13.274         where name is a locale name, ps a list of parameter names and axs
  13.275         a list of axioms relating to the identifier, axs is empty unless
  13.276         identify at top level (top = true);
  13.277 @@ -519,6 +635,36 @@
  13.278  end;
  13.279  
  13.280  
  13.281 +(* attributes *)
  13.282 +
  13.283 +local
  13.284 +
  13.285 +fun read_att attrib (x, srcs) = (x, map attrib srcs)
  13.286 +
  13.287 +(* CB: Map attrib over
  13.288 +   * A context element: add attrib to attribute lists of assumptions,
  13.289 +     definitions and facts (on both sides for facts).
  13.290 +   * Locale expression: no effect. *)
  13.291 +
  13.292 +fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
  13.293 +  | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
  13.294 +  | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
  13.295 +  | gen_map_attrib_elem attrib (Notes facts) =
  13.296 +      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
  13.297 +
  13.298 +fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
  13.299 +  | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
  13.300 +
  13.301 +in
  13.302 +
  13.303 +val map_attrib_element = gen_map_attrib_elem;
  13.304 +val map_attrib_element_i = gen_map_attrib_elem;
  13.305 +val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
  13.306 +val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
  13.307 +
  13.308 +end;
  13.309 +
  13.310 +
  13.311  (* activate elements *)
  13.312  
  13.313  local
  13.314 @@ -534,6 +680,8 @@
  13.315        ((ctxt |> ProofContext.add_fixes fixes, axs), [])
  13.316    | activate_elem _ ((ctxt, axs), Assumes asms) =
  13.317        let
  13.318 +        (* extract context attributes *)
  13.319 +        val (Assumes asms) = map_attrib_element_i snd (Assumes asms);
  13.320          val ts = List.concat (map (map #1 o #2) asms);
  13.321          val (ps,qs) = splitAt (length ts, axs);
  13.322          val (ctxt', _) =
  13.323 @@ -541,14 +689,20 @@
  13.324            |> ProofContext.assume_i (export_axioms ps) asms;
  13.325        in ((ctxt', qs), []) end
  13.326    | activate_elem _ ((ctxt, axs), Defines defs) =
  13.327 -      let val (ctxt', _) =
  13.328 +      let
  13.329 +        (* extract context attributes *)
  13.330 +        val (Defines defs) = map_attrib_element_i snd (Defines defs);
  13.331 +        val (ctxt', _) =
  13.332          ctxt |> ProofContext.assume_i ProofContext.export_def
  13.333            (defs |> map (fn ((name, atts), (t, ps)) =>
  13.334              let val (c, t') = ProofContext.cert_def ctxt t
  13.335              in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
  13.336        in ((ctxt', axs), []) end
  13.337    | activate_elem is_ext ((ctxt, axs), Notes facts) =
  13.338 -      let val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
  13.339 +      let
  13.340 +        (* extract context attributes *)
  13.341 +        val (Notes facts) = map_attrib_element_i snd (Notes facts);
  13.342 +        val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
  13.343        in ((ctxt', axs), if is_ext then res else []) end;
  13.344  
  13.345  fun activate_elems (((name, ps), axs), elems) ctxt =
  13.346 @@ -591,36 +745,6 @@
  13.347    | intern_expr sg (Rename (expr, xs)) = Rename (intern_expr sg expr, xs);
  13.348  
  13.349  
  13.350 -(* attributes *)
  13.351 -
  13.352 -local
  13.353 -
  13.354 -fun read_att attrib (x, srcs) = (x, map attrib srcs)
  13.355 -
  13.356 -(* CB: Map attrib over
  13.357 -   * A context element: add attrib to attribute lists of assumptions,
  13.358 -     definitions and facts (on both sides for facts).
  13.359 -   * Locale expression: no effect. *)
  13.360 -
  13.361 -fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
  13.362 -  | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
  13.363 -  | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
  13.364 -  | gen_map_attrib_elem attrib (Notes facts) =
  13.365 -      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
  13.366 -
  13.367 -fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
  13.368 -  | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
  13.369 -
  13.370 -in
  13.371 -
  13.372 -val map_attrib_element = gen_map_attrib_elem;
  13.373 -val map_attrib_element_i = gen_map_attrib_elem;
  13.374 -val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
  13.375 -val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
  13.376 -
  13.377 -end;
  13.378 -
  13.379 -
  13.380  (* parameters *)
  13.381  
  13.382  local
  13.383 @@ -644,19 +768,20 @@
  13.384  
  13.385  datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
  13.386  
  13.387 -(* CB: flatten (ids, expr) normalises expr (which is either a locale
  13.388 +(* flatten (ids, expr) normalises expr (which is either a locale
  13.389     expression or a single context element) wrt.
  13.390     to the list ids of already accumulated identifiers.
  13.391     It returns (ids', elemss) where ids' is an extension of ids
  13.392     with identifiers generated for expr, and elemss is the list of
  13.393 -   context elements generated from expr, decorated with additional
  13.394 -   information (for expr it is the identifier, where parameters additionially
  13.395 -   contain type information (extracted from the locale record), for a Fixes
  13.396 -   element, it is an identifier with name = "" and parameters with type
  13.397 -   information NONE, for other elements it is simply ("", [])).
  13.398 +   context elements generated from expr.  For details, see flatten_expr.
  13.399 +   Additionally, for a locale expression, the elems are grouped into a single
  13.400 +   Int; individual context elements are marked Ext.  In this case, the
  13.401 +   identifier-like information of the element is as follows:
  13.402 +   - for Fixes: (("", ps), []) where the ps have type info NONE
  13.403 +   - for other elements: (("", []), []).
  13.404     The implementation of activate_facts relies on identifier names being
  13.405     empty strings for external elements.
  13.406 -TODO: correct this comment wrt axioms. *)
  13.407 +*)
  13.408  
  13.409  fun flatten _ (ids, Elem (Fixes fixes)) =
  13.410        (ids, [((("", map (rpair NONE o #1) fixes), []), Ext (Fixes fixes))])
  13.411 @@ -711,11 +836,13 @@
  13.412  
  13.413  local
  13.414  
  13.415 -(* CB: following code (norm_term, abstract_term, abstract_thm, bind_def)
  13.416 -   used in eval_text for defines elements. *)
  13.417 +(* CB: normalise Assumes and Defines wrt. previous definitions *)
  13.418  
  13.419  val norm_term = Envir.beta_norm oo Term.subst_atomic;
  13.420  
  13.421 +(* CB: following code (abstract_term, abstract_thm, bind_def)
  13.422 +   used in eval_text for Defines elements. *)
  13.423 +
  13.424  fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
  13.425    let
  13.426      val body = Term.strip_all_body eq;
  13.427 @@ -997,7 +1124,7 @@
  13.428        the_locale thy (intern sign loc_name);
  13.429      val fixed_params = param_types ps;
  13.430      val init = ProofContext.init thy;
  13.431 -    val (ids, raw_elemss) =
  13.432 +    val (_, raw_elemss) =
  13.433            flatten (init, intern_expr sign) ([], Expr (Locale loc_name));
  13.434      val ((parms, all_elemss, concl),
  13.435           (spec as (_, (ints, _)), (xs, env, defs))) =
  13.436 @@ -1127,7 +1254,9 @@
  13.437      fun inst_elem (ctxt, (Ext _)) = ctxt
  13.438        | inst_elem (ctxt, (Int (Notes facts))) =
  13.439                (* instantiate fact *)
  13.440 -          let val facts' =
  13.441 +          let (* extract context attributes *)
  13.442 +              val (Notes facts) = map_attrib_element_i snd (Notes facts);
  13.443 +              val facts' =
  13.444                  map (apsnd (map (apfst (map inst_thm')))) facts
  13.445  		handle THM (msg, n, thms) => error ("Exception THM " ^
  13.446  		  string_of_int n ^ " raised\n" ^
  13.447 @@ -1210,6 +1339,31 @@
  13.448    |>> hide_bound_names (map (#1 o #1) args)
  13.449    |>> Theory.parent_path;
  13.450  
  13.451 +fun note_thms_qualified' kind (arg as ((name, atts), thms)) thy =
  13.452 +  let
  13.453 +    val qname = NameSpace.unpack name
  13.454 +  in
  13.455 +    if length qname <= 1
  13.456 +    then PureThy.note_thmss_i kind [arg] thy
  13.457 +  else let val (prfx, n) = split_last qname
  13.458 +    in thy
  13.459 +      |> Theory.add_path (NameSpace.pack prfx)
  13.460 +      |> PureThy.note_thmss_i kind [((n, atts), thms)]
  13.461 +      |>> funpow (length prfx) Theory.parent_path
  13.462 +    end
  13.463 +  end;
  13.464 +
  13.465 +(* prfx may be empty (not yet), names (in args) may be qualified *)
  13.466 +
  13.467 +fun note_thmss_qualified' kind prfx args thy =
  13.468 +  thy
  13.469 +  |> Theory.add_path (Sign.base_name prfx)
  13.470 +  |> (fn thy => Library.foldl (fn ((thy, res), arg) =>
  13.471 +        let val (thy', res') = note_thms_qualified' (Drule.kind kind) arg thy
  13.472 +        in (thy', res @ res') end) ((thy, []), args))
  13.473 +(*  |>> hide_bound_names (map (#1 o #1) args) *)
  13.474 +  |>> Theory.parent_path;
  13.475 +
  13.476  fun smart_note_thmss kind NONE = PureThy.note_thmss_i (Drule.kind kind)
  13.477    | smart_note_thmss kind (SOME (loc, _)) = note_thmss_qualified kind loc;
  13.478    (* CB: only used in Proof.finish_global. *)
  13.479 @@ -1233,8 +1387,13 @@
  13.480      val (_, (stmt, _), loc_ctxt, _, _) =
  13.481        cert_context_statement (SOME loc) [] [] thy_ctxt;
  13.482      val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
  13.483 +    (* convert multi attributes to context attributes for
  13.484 +       ProofContext.note_thmss_i *)
  13.485 +    val args'' = args
  13.486 +          |> map (apfst (apsnd (map snd)))
  13.487 +          |> map (apsnd (map (apsnd (map snd))));
  13.488      val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
  13.489 -    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt));
  13.490 +    val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args'' loc_ctxt));
  13.491      val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
  13.492    in
  13.493      thy
  13.494 @@ -1264,7 +1423,7 @@
  13.495  
  13.496  
  13.497  (* predicate text *)
  13.498 -(* CB: generate locale predicates (and delta predicates) *)
  13.499 +(* CB: generate locale predicates and delta predicates *)
  13.500  
  13.501  local
  13.502  
  13.503 @@ -1403,8 +1562,8 @@
  13.504  local
  13.505  
  13.506  fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy =
  13.507 -  (* CB: do_pred = false means old-style locale, declared with (open).
  13.508 -     Old-style locales don't define predicates. *)
  13.509 +  (* CB: do_pred controls generation of predicates.
  13.510 +         true -> with, false -> without predicates. *)
  13.511    let
  13.512      val sign = Theory.sign_of thy;
  13.513      val name = Sign.full_name sign bname;
  13.514 @@ -1451,6 +1610,272 @@
  13.515  
  13.516  
  13.517  
  13.518 +(** Registration commands **)
  13.519 +
  13.520 +local
  13.521 +
  13.522 +(** instantiate free vars **)
  13.523 +
  13.524 +(* instantiate TFrees *)
  13.525 +
  13.526 +fun tinst_type tinst T = if Symtab.is_empty tinst
  13.527 +      then T
  13.528 +      else Term.map_type_tfree
  13.529 +        (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
  13.530 +
  13.531 +fun tinst_term tinst t = if Symtab.is_empty tinst
  13.532 +      then t
  13.533 +      else Term.map_term_types (tinst_type tinst) t;
  13.534 +
  13.535 +fun tinst_thm sg tinst thm = if Symtab.is_empty tinst
  13.536 +      then thm
  13.537 +      else let
  13.538 +          val cert = Thm.cterm_of sg;
  13.539 +          val certT = Thm.ctyp_of sg;
  13.540 +          val {hyps, prop, ...} = Thm.rep_thm thm;
  13.541 +          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
  13.542 +          val tinst' = Symtab.dest tinst |>
  13.543 +                List.filter (fn (a, _) => a mem_string tfrees);
  13.544 +        in
  13.545 +          if null tinst' then thm
  13.546 +          else thm |> Drule.implies_intr_list (map cert hyps)
  13.547 +            |> Drule.tvars_intr_list (map #1 tinst')
  13.548 +            |> (fn (th, al) => th |> Thm.instantiate
  13.549 +                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
  13.550 +                  []))
  13.551 +            |> (fn th => Drule.implies_elim_list th
  13.552 +                 (map (Thm.assume o cert o tinst_term tinst) hyps))
  13.553 +        end;
  13.554 +
  13.555 +fun tinst_elem _ tinst (Fixes fixes) =
  13.556 +      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
  13.557 +  | tinst_elem _ tinst (Assumes asms) =
  13.558 +      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  13.559 +        (tinst_term tinst t,
  13.560 +          (map (tinst_term tinst) ps, map (tinst_term tinst) qs))))) asms)
  13.561 +  | tinst_elem _ tinst (Defines defs) =
  13.562 +      Defines (map (apsnd (fn (t, ps) =>
  13.563 +        (tinst_term tinst t, map (tinst_term tinst) ps))) defs)
  13.564 +  | tinst_elem sg tinst (Notes facts) =
  13.565 +      Notes (map (apsnd (map (apfst (map (tinst_thm sg tinst))))) facts);
  13.566 +
  13.567 +(* instantiate TFrees and Frees *)
  13.568 +
  13.569 +fun inst_term (inst, tinst) = if Symtab.is_empty inst
  13.570 +      then tinst_term tinst
  13.571 +      else (* instantiate terms and types simultaneously *)
  13.572 +        let
  13.573 +          fun instf (Const (x, T)) = Const (x, tinst_type tinst T)
  13.574 +            | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
  13.575 +                 NONE => Free (x, tinst_type tinst T)
  13.576 +               | SOME t => t)
  13.577 +            | instf (Var (xi, T)) = Var (xi, tinst_type tinst T)
  13.578 +            | instf (b as Bound _) = b
  13.579 +            | instf (Abs (x, T, t)) = Abs (x, tinst_type tinst T, instf t)
  13.580 +            | instf (s $ t) = instf s $ instf t
  13.581 +        in instf end;
  13.582 +
  13.583 +fun inst_thm sg (inst, tinst) thm = if Symtab.is_empty inst
  13.584 +      then tinst_thm sg tinst thm
  13.585 +      else let
  13.586 +          val cert = Thm.cterm_of sg;
  13.587 +          val certT = Thm.ctyp_of sg;
  13.588 +          val {hyps, prop, ...} = Thm.rep_thm thm;
  13.589 +          (* type instantiations *)
  13.590 +          val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
  13.591 +          val tinst' = Symtab.dest tinst |>
  13.592 +                List.filter (fn (a, _) => a mem_string tfrees);
  13.593 +          (* term instantiations;
  13.594 +             note: lhss are type instantiated, because
  13.595 +                   type insts will be done first*)
  13.596 +          val frees = foldr Term.add_term_frees [] (prop :: hyps);
  13.597 +          val inst' = Symtab.dest inst |>
  13.598 +                List.mapPartial (fn (a, t) =>
  13.599 +                  get_first (fn (Free (x, T)) => 
  13.600 +                    if a = x then SOME (Free (x, tinst_type tinst T), t)
  13.601 +                    else NONE) frees);
  13.602 +        in
  13.603 +          if null tinst' andalso null inst' then tinst_thm sg tinst thm
  13.604 +          else thm |> Drule.implies_intr_list (map cert hyps)
  13.605 +            |> Drule.tvars_intr_list (map #1 tinst')
  13.606 +            |> (fn (th, al) => th |> Thm.instantiate
  13.607 +                ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'),
  13.608 +                  []))
  13.609 +            |> Drule.forall_intr_list (map (cert o #1) inst')
  13.610 +            |> Drule.forall_elim_list (map (cert o #2) inst') 
  13.611 +            |> (fn th => Drule.implies_elim_list th
  13.612 +                 (map (Thm.assume o cert o inst_term (inst, tinst)) hyps))
  13.613 +        end;
  13.614 +
  13.615 +fun inst_elem _ (_, tinst) (Fixes fixes) =
  13.616 +      Fixes (map (fn (x, T, mx) => (x, Option.map (tinst_type tinst) T, mx)) fixes)
  13.617 +  | inst_elem _ inst (Assumes asms) =
  13.618 +      Assumes (map (apsnd (map (fn (t, (ps, qs)) =>
  13.619 +        (inst_term inst t,
  13.620 +          (map (inst_term inst) ps, map (inst_term inst) qs))))) asms)
  13.621 +  | inst_elem _ inst (Defines defs) =
  13.622 +      Defines (map (apsnd (fn (t, ps) =>
  13.623 +        (inst_term inst t, map (inst_term inst) ps))) defs)
  13.624 +  | inst_elem sg inst (Notes facts) =
  13.625 +      Notes (map (apsnd (map (apfst (map (inst_thm sg inst))))) facts);
  13.626 +
  13.627 +fun inst_elems sign inst ((n, ps), elems) =
  13.628 +      ((n, map (inst_term inst) ps), map (inst_elem sign inst) elems);
  13.629 +
  13.630 +(* extract proof obligations (assms and defs) from elements *)
  13.631 +
  13.632 +(* check if defining equation has become t == t, these are dropped
  13.633 +   in extract_asms_elem, as they lead to trivial proof obligations *)
  13.634 +(* currently disabled *)
  13.635 +fun check_def (_, (def, _)) = SOME def;
  13.636 +(*
  13.637 +fun check_def (_, (def, _)) =
  13.638 +      if def |> Logic.dest_equals |> op aconv
  13.639 +      then NONE else SOME def;
  13.640 +*)
  13.641 +
  13.642 +fun extract_asms_elem (ts, Fixes _) = ts
  13.643 +  | extract_asms_elem (ts, Assumes asms) =
  13.644 +      ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
  13.645 +  | extract_asms_elem (ts, Defines defs) =
  13.646 +      ts @ List.mapPartial check_def defs
  13.647 +  | extract_asms_elem (ts, Notes _) = ts;
  13.648 +
  13.649 +fun extract_asms_elems (id, elems) =
  13.650 +      (id, Library.foldl extract_asms_elem ([], elems));
  13.651 +
  13.652 +fun extract_asms_elemss elemss =
  13.653 +      map extract_asms_elems elemss;
  13.654 +
  13.655 +(* add registration, without theorems, to theory *)
  13.656 +
  13.657 +fun prep_reg_global attn (thy, (id, _)) =
  13.658 +      global_put_registration id attn thy;
  13.659 +
  13.660 +(* activate instantiated facts in theory *)
  13.661 +
  13.662 +fun activate_facts_elem _ _ (thy, Fixes _) = thy
  13.663 +  | activate_facts_elem _ _ (thy, Assumes _) = thy
  13.664 +  | activate_facts_elem _ _ (thy, Defines _) = thy
  13.665 +  | activate_facts_elem disch (prfx, atts) (thy, Notes facts) =
  13.666 +      let
  13.667 +        (* extract theory attributes *)
  13.668 +        val (Notes facts) = map_attrib_element_i fst (Notes facts);
  13.669 +        val facts' = map (apfst (apsnd (fn a => a @ atts))) facts;
  13.670 +        val facts'' = map (apsnd (map (apfst (map disch)))) facts';
  13.671 +      in
  13.672 +        fst (note_thmss_qualified' "" prfx facts thy)
  13.673 +      end;
  13.674 +
  13.675 +fun activate_facts_elems disch (thy, (id, elems)) =
  13.676 +      let
  13.677 +        val ((prfx, atts2), _) = valOf (global_get_registration thy id)
  13.678 +          handle Option => error ("(internal) unknown registration of " ^
  13.679 +            quote (fst id) ^ " while activating facts.");
  13.680 +      in
  13.681 +        Library.foldl (activate_facts_elem disch (prfx, atts2)) (thy, elems)
  13.682 +      end;
  13.683 +
  13.684 +fun activate_facts_elemss all_elemss new_elemss thy =
  13.685 +      let
  13.686 +        val prems = List.concat (List.mapPartial (fn (id, _) =>
  13.687 +              Option.map snd (global_get_registration thy id)
  13.688 +                handle Option => error ("(internal) unknown registration of " ^
  13.689 +                  quote (fst id) ^ " while activating facts.")) all_elemss);
  13.690 +        fun disch thm = let
  13.691 +          in Drule.satisfy_hyps prems thm end;
  13.692 +      in Library.foldl (activate_facts_elems disch) (thy, new_elemss) end;
  13.693 +
  13.694 +in
  13.695 +
  13.696 +fun prep_registration attn expr insts thy =
  13.697 +  let
  13.698 +    val ctxt = ProofContext.init thy;
  13.699 +    val sign = Theory.sign_of thy;
  13.700 +    val tsig = Sign.tsig_of sign;
  13.701 +
  13.702 +    val (ids, raw_elemss) =
  13.703 +          flatten (ctxt, intern_expr sign) ([], Expr expr);
  13.704 +    val do_close = false;  (* effect unknown *)
  13.705 +    val ((parms, all_elemss, _), (spec, (xs, defs, _))) =
  13.706 +          read_elemss do_close ctxt [] raw_elemss [];
  13.707 +
  13.708 +
  13.709 +    (** compute instantiation **)
  13.710 +
  13.711 +    (* user input *)
  13.712 +    val insts = if length parms < length insts
  13.713 +         then error "More arguments than parameters in instantiation."
  13.714 +         else insts @ replicate (length parms - length insts) NONE;
  13.715 +    val (ps, pTs) = split_list parms;
  13.716 +    val pvTs = map Type.varifyT pTs;
  13.717 +    val given = List.mapPartial (fn (_, (NONE, _)) => NONE
  13.718 +         | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
  13.719 +    val (given_ps, given_insts) = split_list given;
  13.720 +    val tvars = foldr Term.add_typ_tvars [] pvTs;
  13.721 +    val used = foldr Term.add_typ_varnames [] pvTs;
  13.722 +    fun sorts (a, i) = assoc (tvars, (a, i));
  13.723 +    val (tvs, tvinst) = Sign.read_def_terms (sign, K NONE, sorts) used true
  13.724 +         given_insts;
  13.725 +    val tinst = Symtab.make (map (fn ((x, 0), T) => (x, Type.unvarifyT T)
  13.726 +                  | ((_, n), _) => error "Var in prep_registration") tvinst);
  13.727 +    val inst = Symtab.make (given_ps ~~ map Logic.unvarify tvs);
  13.728 +
  13.729 +    (* defined params without user input *)
  13.730 +    val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
  13.731 +         | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
  13.732 +    fun add_def ((inst, tinst), (p, pT)) =
  13.733 +      let
  13.734 +        val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
  13.735 +               NONE => error ("Instance missing for parameter " ^ quote p)
  13.736 +             | SOME (Free (_, T), t) => (t, T);
  13.737 +        val d = t |> inst_term (inst, tinst) |> Envir.beta_norm;
  13.738 +      in (Symtab.update_new ((p, d), inst), tinst) end;
  13.739 +    val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
  13.740 +  
  13.741 +
  13.742 +    (** compute proof obligations **)
  13.743 +
  13.744 +    (* restore small ids *)
  13.745 +    val ids' = map (fn ((n, ps), _) =>
  13.746 +          (n, map (fn p => Free (p, valOf (assoc (parms, p)))) ps)) ids;
  13.747 +
  13.748 +    (* instantiate ids and elements *)
  13.749 +    val inst_elemss = map
  13.750 +          (fn (id, (_, elems)) => inst_elems sign (inst, tinst) (id, 
  13.751 +            map (fn Int e => e) elems)) 
  13.752 +          (ids' ~~ all_elemss);
  13.753 +
  13.754 +(*
  13.755 +    (* varify ids, props are varified after they are proved *)
  13.756 +    val inst_elemss' = map (fn ((n, ps), elems) =>
  13.757 +          ((n, map Logic.varify ps), elems)) inst_elemss;
  13.758 +*)
  13.759 +
  13.760 +    (* remove fragments already registered with theory *)
  13.761 +    val new_inst_elemss = List.filter (fn (id, _) =>
  13.762 +          is_none (global_get_registration thy id)) inst_elemss;
  13.763 +
  13.764 +
  13.765 +    val propss = extract_asms_elemss new_inst_elemss;
  13.766 +
  13.767 +
  13.768 +    (** add registrations to theory,
  13.769 +        without theorems, these are added after the proof **)
  13.770 +
  13.771 +    val thy' = Library.foldl (prep_reg_global attn) (thy, new_inst_elemss);
  13.772 +
  13.773 +  in (thy', propss, activate_facts_elemss inst_elemss new_inst_elemss) end;
  13.774 +
  13.775 +
  13.776 +(* Add registrations and theorems to theory context *)
  13.777 +
  13.778 +val global_activate_thm = global_put_registration_thm
  13.779 +
  13.780 +end;  (* local *)
  13.781 +
  13.782 +
  13.783 +
  13.784  (** locale theory setup **)
  13.785  
  13.786  val setup =
    14.1 --- a/src/Pure/Isar/proof.ML	Tue Mar 08 16:02:52 2005 +0100
    14.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 09 18:44:52 2005 +0100
    14.3 @@ -90,15 +90,15 @@
    14.4    val def: string -> context attribute list -> string *  (string * string list) -> state -> state
    14.5    val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
    14.6    val invoke_case: string * string option list * context attribute list -> state -> state
    14.7 -  val multi_theorem: string
    14.8 -    -> (xstring * (context attribute list * context attribute list list)) option
    14.9 -    -> bstring * theory attribute list -> context attribute Locale.element Locale.elem_expr list
   14.10 +  val multi_theorem: string -> (theory -> theory)
   14.11 +    -> (xstring * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
   14.12 +    -> bstring * theory attribute list -> Locale.multi_attribute Locale.element Locale.elem_expr list
   14.13      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
   14.14      -> theory -> state
   14.15 -  val multi_theorem_i: string
   14.16 -    -> (string * (context attribute list * context attribute list list)) option
   14.17 +  val multi_theorem_i: string -> (theory -> theory)
   14.18 +    -> (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option
   14.19      -> bstring * theory attribute list
   14.20 -    -> context attribute Locale.element_i Locale.elem_expr list
   14.21 +    -> Locale.multi_attribute Locale.element_i Locale.elem_expr list
   14.22      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
   14.23      -> theory -> state
   14.24    val chain: state -> state
   14.25 @@ -153,9 +153,11 @@
   14.26  datatype kind =
   14.27    Theorem of {kind: string,
   14.28      theory_spec: (bstring * theory attribute list) * theory attribute list list,
   14.29 -    locale_spec: (string * (context attribute list * context attribute list list)) option,
   14.30 -    view: cterm list * cterm list} |
   14.31 -(* target view and includes view *)
   14.32 +    locale_spec: (string * (Locale.multi_attribute list * Locale.multi_attribute list list)) option,
   14.33 +    view: cterm list * cterm list, (* target view and includes view *)
   14.34 +    thy_mod: theory -> theory} |   (* used in finish_global to modify final
   14.35 +      theory, normally set to I;
   14.36 +      used by registration command to activate registrations *)
   14.37    Show of context attribute list list |
   14.38    Have of context attribute list list;
   14.39  
   14.40 @@ -163,9 +165,9 @@
   14.41     the proof state *)
   14.42  
   14.43  fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
   14.44 -        locale_spec = NONE, view = _}) = s ^ (if a = "" then "" else " " ^ a)
   14.45 +        locale_spec = NONE, ...}) = s ^ (if a = "" then "" else " " ^ a)
   14.46    | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
   14.47 -        locale_spec = SOME (name, _), view = _}) =
   14.48 +        locale_spec = SOME (name, _), ...}) =
   14.49        s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
   14.50    | kind_name _ (Show _) = "show"
   14.51    | kind_name _ (Have _) = "have";
   14.52 @@ -782,7 +784,7 @@
   14.53    end;
   14.54  
   14.55  (*global goals*)
   14.56 -fun global_goal prep kind raw_locale a elems concl thy =
   14.57 +fun global_goal prep kind thy_mod raw_locale a elems concl thy =
   14.58    let
   14.59      val init = init_state thy;
   14.60      val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
   14.61 @@ -799,7 +801,8 @@
   14.62        (Theorem {kind = kind,
   14.63          theory_spec = (a, map (snd o fst) concl),
   14.64          locale_spec = (case raw_locale of NONE => NONE | SOME (_, x) => SOME (valOf opt_name, x)),
   14.65 -        view = view})
   14.66 +        view = view,
   14.67 +        thy_mod = thy_mod})
   14.68        Seq.single true (map (fst o fst) concl) propp
   14.69    end;
   14.70  
   14.71 @@ -900,7 +903,7 @@
   14.72      val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
   14.73      val locale_ctxt = context_of (state |> close_block);
   14.74      val theory_ctxt = context_of (state |> close_block |> close_block);
   14.75 -    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view)} =
   14.76 +    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view), thy_mod} =
   14.77        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
   14.78  
   14.79      val ts = List.concat tss;
   14.80 @@ -926,7 +929,7 @@
   14.81        |> (fn (thy, res) => (thy, res)
   14.82            |>> (#1 o Locale.smart_note_thmss k locale_spec
   14.83              [((name, atts), [(List.concat (map #2 res), [])])]));
   14.84 -  in (theory', ((k, name), results')) end;
   14.85 +  in (thy_mod theory', ((k, name), results')) end;
   14.86  
   14.87  
   14.88  (*note: clients should inspect first result only, as backtracking may destroy theory*)
    15.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 08 16:02:52 2005 +0100
    15.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 09 18:44:52 2005 +0100
    15.3 @@ -635,7 +635,10 @@
    15.4  
    15.5  in
    15.6  
    15.7 +(* CB: for attribute where.  See attrib.ML. *)
    15.8  val read_termTs           = gen_read' (read_def_termTs false) (apfst o map) false false false;
    15.9 +
   15.10 +(* CB: for rule_tac etc.  See method.ML. *)
   15.11  val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true;
   15.12  
   15.13  fun read_term_pats T ctxt =
    16.1 --- a/src/Pure/Isar/toplevel.ML	Tue Mar 08 16:02:52 2005 +0100
    16.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 09 18:44:52 2005 +0100
    16.3 @@ -425,6 +425,11 @@
    16.4       then raised_msg "THEORY" (cat_lines ("" :: msg ::
    16.5         map (Pretty.string_of o Display.pretty_theory) thys))
    16.6       else msg
    16.7 +  | msg_on_debug (AST (msg, asts)) =
    16.8 +     if !debug
    16.9 +     then raised_msg "AST" (cat_lines ("" :: msg ::
   16.10 +       map (Pretty.string_of o Syntax.pretty_ast) asts))
   16.11 +     else msg
   16.12    | msg_on_debug (TERM (msg, ts)) =
   16.13       (case (!debug, Context.get_context ()) of
   16.14           (true, SOME thy) =>
   16.15 @@ -445,21 +450,6 @@
   16.16             end
   16.17         | _ => raised_msg "TYPE" msg)
   16.18  
   16.19 -(*
   16.20 -	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
   16.21 -	  seq print_thm thms)
   16.22 -   | THEORY (msg,thys) =>
   16.23 -	 (writeln ("Exception THEORY raised:\n" ^ msg);
   16.24 -	  seq (Pretty.writeln o Display.pretty_theory) thys)
   16.25 -   | TERM (msg,ts) =>
   16.26 -	 (writeln ("Exception TERM raised:\n" ^ msg);
   16.27 -	  seq (writeln o Sign.string_of_term sign) ts)
   16.28 -   | TYPE (msg,Ts,ts) =>
   16.29 -	 (writeln ("Exception TYPE raised:\n" ^ msg);
   16.30 -	  seq (writeln o Sign.string_of_typ sign) Ts;
   16.31 -	  seq (writeln o Sign.string_of_term sign) ts)
   16.32 -*)
   16.33 -
   16.34  fun exn_message TERMINATE = "Exit."
   16.35    | exn_message RESTART = "Restart."
   16.36    | exn_message (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   16.37 @@ -475,7 +465,7 @@
   16.38    | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
   16.39    | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
   16.40    | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info
   16.41 -  | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg
   16.42 +  | exn_message (Syntax.AST (msg, asts)) = msg_on_debug (AST (msg, asts))
   16.43    | exn_message (TYPE (msg, Ts, ts)) = msg_on_debug (TYPE (msg, Ts, ts))
   16.44    | exn_message (TERM (msg, ts)) = msg_on_debug (TERM (msg, ts))
   16.45    | exn_message (THM (msg, i, thms)) = msg_on_debug (THM (msg, i, thms))
    17.1 --- a/src/Pure/ROOT.ML	Tue Mar 08 16:02:52 2005 +0100
    17.2 +++ b/src/Pure/ROOT.ML	Wed Mar 09 18:44:52 2005 +0100
    17.3 @@ -11,6 +11,7 @@
    17.4  
    17.5  
    17.6  print_depth 10;
    17.7 +error_depth 30;
    17.8  
    17.9  (*fake hiding of private structures*)
   17.10  structure Hidden = struct end;
    18.1 --- a/src/Pure/axclass.ML	Tue Mar 08 16:02:52 2005 +0100
    18.2 +++ b/src/Pure/axclass.ML	Wed Mar 09 18:44:52 2005 +0100
    18.3 @@ -407,7 +407,7 @@
    18.4  
    18.5  fun inst_proof mk_prop add_thms inst int theory =
    18.6    theory
    18.7 -  |> IsarThy.multi_theorem_i Drule.internalK
    18.8 +  |> IsarThy.multi_theorem_i Drule.internalK I
    18.9      ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
   18.10      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
   18.11  
    19.1 --- a/src/Pure/logic.ML	Tue Mar 08 16:02:52 2005 +0100
    19.2 +++ b/src/Pure/logic.ML	Wed Mar 09 18:44:52 2005 +0100
    19.3 @@ -336,6 +336,7 @@
    19.4  
    19.5  (*Inverse of varify.  Converts axioms back to their original form.*)
    19.6  fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
    19.7 +  | unvarify (Free(a,T))     = Free(a, Type.unvarifyT T)  (* CB: added *)
    19.8    | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
    19.9    | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
   19.10    | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)