Modified locales: improved implementation of "includes".
authorballarin
Mon Sep 27 10:27:34 2004 +0200 (2004-09-27)
changeset 1520609d78ec709c7
parent 15205 ecf9a884970d
child 15207 a383b0a412b0
Modified locales: improved implementation of "includes".
NEWS
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Set.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
     1.1 --- a/NEWS	Thu Sep 23 12:48:49 2004 +0200
     1.2 +++ b/NEWS	Mon Sep 27 10:27:34 2004 +0200
     1.3 @@ -146,7 +146,8 @@
     1.4  
     1.5  * Locales:
     1.6    - "includes" disallowed in declaration of named locales (command "locale").
     1.7 -
     1.8 +  - Fixed parameter management in theorem generation for goals with "includes".
     1.9 +    INCOMPATIBILITY: rarely, the generated theorem statement is different.
    1.10   
    1.11  *** HOL ***
    1.12  
     2.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Sep 23 12:48:49 2004 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Sep 27 10:27:34 2004 +0200
     2.3 @@ -82,7 +82,17 @@
     2.4    normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
     2.5  *}
     2.6  
     2.7 -lemma (in normed_vectorspace) fn_norm_works:   (* FIXME bug with "(in fn_norm)" !? *)
     2.8 +(* Alternative statement of the lemma as
     2.9 +     lemma (in fn_norm)
    2.10 +       includes normed_vectorspace + continuous
    2.11 +       shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    2.12 +   is not possible:
    2.13 +   fn_norm contrains parameter norm to type "'a::zero => real",
    2.14 +   normed_vectorspace and continuous contrain this parameter to
    2.15 +   "'a::{minus, plus, zero} => real, which is less general.
    2.16 +*)
    2.17 +
    2.18 +lemma (in normed_vectorspace) fn_norm_works:
    2.19    includes fn_norm + continuous
    2.20    shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    2.21  proof -
    2.22 @@ -154,7 +164,7 @@
    2.23    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    2.24  proof -
    2.25    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    2.26 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
    2.27 +    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
    2.28    from this and b show ?thesis ..
    2.29  qed
    2.30  
    2.31 @@ -164,7 +174,7 @@
    2.32    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
    2.33  proof -
    2.34    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    2.35 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
    2.36 +    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
    2.37    from this and b show ?thesis ..
    2.38  qed
    2.39  
    2.40 @@ -178,7 +188,7 @@
    2.41      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
    2.42      0"}, provided the supremum exists and @{text B} is not empty. *}
    2.43    have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    2.44 -    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF _ continuous.intro])
    2.45 +    by (unfold B_def fn_norm_def) (rule fn_norm_works [OF continuous.intro])
    2.46    moreover have "0 \<in> B V f" ..
    2.47    ultimately show ?thesis ..
    2.48  qed
    2.49 @@ -201,7 +211,7 @@
    2.50    also have "\<bar>\<dots>\<bar> = 0" by simp
    2.51    also have a: "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
    2.52        by (unfold B_def fn_norm_def)
    2.53 -        (rule fn_norm_ge_zero [OF _ continuous.intro])
    2.54 +        (rule fn_norm_ge_zero [OF continuous.intro])
    2.55      have "0 \<le> norm x" ..
    2.56    with a have "0 \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" by (simp add: zero_le_mult_iff)
    2.57    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
    2.58 @@ -215,7 +225,7 @@
    2.59      from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
    2.60        by (auto simp add: B_def real_divide_def)
    2.61      then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
    2.62 -      by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF _ continuous.intro])
    2.63 +      by (unfold B_def fn_norm_def) (rule fn_norm_ub [OF continuous.intro])
    2.64    qed
    2.65    finally show ?thesis .
    2.66  qed
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Sep 23 12:48:49 2004 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Sep 27 10:27:34 2004 +0200
     3.3 @@ -340,10 +340,10 @@
     3.4    have F: "vectorspace F" ..
     3.5    have linearform: "linearform F f" .
     3.6    have F_norm: "normed_vectorspace F norm"
     3.7 -    by (rule subspace_normed_vs [OF _ _ norm.intro])
     3.8 +    by (rule subspace_normed_vs [OF E_norm])
     3.9    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
    3.10      by (rule normed_vectorspace.fn_norm_ge_zero
    3.11 -      [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
    3.12 +      [OF F_norm continuous.intro, folded B_def fn_norm_def])
    3.13  
    3.14    txt {* We define a function @{text p} on @{text E} as follows:
    3.15      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
    3.16 @@ -393,7 +393,7 @@
    3.17      fix x assume "x \<in> F"
    3.18      show "\<bar>f x\<bar> \<le> p x"
    3.19        by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
    3.20 -        [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
    3.21 +        [OF F_norm continuous.intro, folded B_def fn_norm_def])
    3.22    qed
    3.23  
    3.24    txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
    3.25 @@ -442,7 +442,7 @@
    3.26        with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
    3.27          by (simp only: p_def)
    3.28      qed
    3.29 -    from linearformE g_cont this ge_zero
    3.30 +    from g_cont this ge_zero
    3.31      show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
    3.32        by (rule fn_norm_least [of g, folded B_def fn_norm_def])
    3.33  
    3.34 @@ -455,7 +455,7 @@
    3.35  	fix x assume x: "x \<in> F"
    3.36  	from a have "g x = f x" ..
    3.37  	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
    3.38 -	also from linearformE g_cont
    3.39 +	also from g_cont
    3.40  	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
    3.41  	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
    3.42  	  from FE x show "x \<in> E" ..
    3.43 @@ -463,7 +463,7 @@
    3.44  	finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
    3.45        qed
    3.46        show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
    3.47 -	using linearformE g_cont
    3.48 +	using g_cont
    3.49  	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
    3.50      next
    3.51        show "continuous F norm f" by (rule continuous.intro)
     4.1 --- a/src/HOL/Set.thy	Thu Sep 23 12:48:49 2004 +0200
     4.2 +++ b/src/HOL/Set.thy	Mon Sep 27 10:27:34 2004 +0200
     4.3 @@ -1086,18 +1086,11 @@
     4.4  
     4.5  text {* \medskip Monotonicity. *}
     4.6  
     4.7 -lemma mono_Un: includes mono shows "f A \<union> f B \<subseteq> f (A \<union> B)"
     4.8 -  apply (rule Un_least)
     4.9 -   apply (rule Un_upper1 [THEN mono])
    4.10 -  apply (rule Un_upper2 [THEN mono])
    4.11 -  done
    4.12 -
    4.13 -lemma mono_Int: includes mono shows "f (A \<inter> B) \<subseteq> f A \<inter> f B"
    4.14 -  apply (rule Int_greatest)
    4.15 -   apply (rule Int_lower1 [THEN mono])
    4.16 -  apply (rule Int_lower2 [THEN mono])
    4.17 -  done
    4.18 -
    4.19 +lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
    4.20 +  by (blast dest: monoD)
    4.21 +
    4.22 +lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    4.23 +  by (blast dest: monoD)
    4.24  
    4.25  subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
    4.26  
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Sep 23 12:48:49 2004 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Sep 27 10:27:34 2004 +0200
     5.3 @@ -215,7 +215,7 @@
     5.4  
     5.5  fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     5.6    let val thy = Toplevel.theory_of state in
     5.7 -    Locale.print_locale thy import (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body)
     5.8 +    Locale.print_locale thy import (map (Locale.map_attrib_element (Attrib.local_attribute thy)) body)
     5.9    end);
    5.10  
    5.11  val print_attributes = Toplevel.unknown_theory o
     6.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Sep 23 12:48:49 2004 +0200
     6.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Sep 27 10:27:34 2004 +0200
     6.3 @@ -59,23 +59,23 @@
     6.4    val theorem_i: string -> (bstring * theory attribute list) *
     6.5      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
     6.6    val multi_theorem: string -> bstring * Args.src list
     6.7 -    -> Args.src Locale.elem_or_expr list
     6.8 +    -> Args.src Locale.element Locale.elem_expr list
     6.9      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    6.10      -> bool -> theory -> ProofHistory.T
    6.11    val multi_theorem_i: string -> bstring * theory attribute list
    6.12 -    -> Proof.context attribute Locale.elem_or_expr_i list
    6.13 +    -> Proof.context attribute Locale.element_i Locale.elem_expr list
    6.14      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    6.15      -> bool -> theory -> ProofHistory.T
    6.16    val locale_multi_theorem: string -> xstring
    6.17 -    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
    6.18 +    -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
    6.19      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    6.20      -> bool -> theory -> ProofHistory.T
    6.21    val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list
    6.22 -    -> Proof.context attribute Locale.elem_or_expr_i list
    6.23 +    -> Proof.context attribute Locale.element_i Locale.elem_expr list
    6.24      -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
    6.25      -> bool -> theory -> ProofHistory.T
    6.26    val smart_multi_theorem: string -> xstring Library.option
    6.27 -    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
    6.28 +    -> bstring * Args.src list -> Args.src Locale.element Locale.elem_expr list
    6.29      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    6.30      -> bool -> theory -> ProofHistory.T
    6.31    val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
    6.32 @@ -372,7 +372,7 @@
    6.33  
    6.34  fun multi_theorem k a elems concl int thy =
    6.35    global_statement (Proof.multi_theorem k None (apsnd (map (Attrib.global_attribute thy)) a)
    6.36 -    (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems)) concl int thy;
    6.37 +    (map (Locale.map_attrib_elem_or_expr (Attrib.local_attribute thy)) elems)) concl int thy;
    6.38  
    6.39  fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k None a;
    6.40  
    6.41 @@ -380,7 +380,7 @@
    6.42    global_statement (Proof.multi_theorem k
    6.43        (Some (locale, (map (Attrib.local_attribute thy) atts,
    6.44            map (map (Attrib.local_attribute thy) o snd o fst) concl)))
    6.45 -      (name, []) (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems))
    6.46 +      (name, []) (map (Locale.map_attrib_elem_or_expr (Attrib.local_attribute thy)) elems))
    6.47        (map (apfst (apsnd (K []))) concl) int thy;
    6.48  
    6.49  fun locale_multi_theorem_i k locale (name, atts) elems concl =
    6.50 @@ -578,7 +578,7 @@
    6.51  
    6.52  fun add_locale (do_pred, name, import, body) thy =
    6.53    Locale.add_locale do_pred name import
    6.54 -    (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body) thy;
    6.55 +    (map (Locale.map_attrib_element (Attrib.local_attribute thy)) body) thy;
    6.56  
    6.57  
    6.58  (* theory init and exit *)
     7.1 --- a/src/Pure/Isar/locale.ML	Thu Sep 23 12:48:49 2004 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Mon Sep 27 10:27:34 2004 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      Pure/Isar/locale.ML
     7.5      ID:         $Id$
     7.6 -    Author:     Markus Wenzel, LMU/TU Muenchen
     7.7 +    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
     7.8  
     7.9  Locales -- Isar proof contexts as meta-level predicates, with local
    7.10  syntax and implicit structures.
    7.11 @@ -21,6 +21,9 @@
    7.12  signature LOCALE =
    7.13  sig
    7.14    type context
    7.15 +
    7.16 +  (* Constructors for elem, expr and elem_expr are
    7.17 +     currently only used for inputting locales (outer_parse.ML). *)
    7.18    datatype ('typ, 'term, 'fact, 'att) elem =
    7.19      Fixes of (string * 'typ option * mixfix option) list |
    7.20      Assumes of ((string * 'att list) * ('term * ('term list * 'term list)) list) list |
    7.21 @@ -31,26 +34,34 @@
    7.22      Rename of expr * string option list |
    7.23      Merge of expr list
    7.24    val empty: expr
    7.25 -  datatype ('typ, 'term, 'fact, 'att) elem_expr =
    7.26 -    Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr
    7.27 +  datatype 'a elem_expr = Elem of 'a | Expr of expr
    7.28 +
    7.29 +  (* Abstract interface to locales *)
    7.30    type 'att element
    7.31    type 'att element_i
    7.32 -  type 'att elem_or_expr
    7.33 -  type 'att elem_or_expr_i
    7.34    type locale
    7.35    val intern: Sign.sg -> xstring -> string
    7.36    val cond_extern: Sign.sg -> string -> xstring
    7.37    val the_locale: theory -> string -> locale
    7.38 -  val map_attrib_elem: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem
    7.39 -    -> ('typ, 'term, 'thm, context attribute) elem
    7.40 -  val map_attrib_elem_expr: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
    7.41 -    -> ('typ, 'term, 'thm, context attribute) elem_expr
    7.42 -  val read_context_statement: xstring option -> context attribute elem_or_expr list ->
    7.43 +  val map_attrib_element: ('att -> context attribute) -> 'att element ->
    7.44 +    context attribute element
    7.45 +  val map_attrib_element_i: ('att -> context attribute) -> 'att element_i ->
    7.46 +    context attribute element_i
    7.47 +  val map_attrib_elem_or_expr: ('att -> context attribute) ->
    7.48 +    'att element elem_expr -> context attribute element elem_expr
    7.49 +  val map_attrib_elem_or_expr_i: ('att -> context attribute) ->
    7.50 +    'att element_i elem_expr -> context attribute element_i elem_expr
    7.51 +
    7.52 +  val read_context_statement: xstring option ->
    7.53 +    context attribute element elem_expr list ->
    7.54      (string * (string list * string list)) list list -> context ->
    7.55 -    string option * cterm list * context * context * (term * (term list * term list)) list list
    7.56 -  val cert_context_statement: string option -> context attribute elem_or_expr_i list ->
    7.57 +    string option * (cterm list * cterm list) * context * context * 
    7.58 +      (term * (term list * term list)) list list
    7.59 +  val cert_context_statement: string option ->
    7.60 +    context attribute element_i elem_expr list ->
    7.61      (term * (term list * term list)) list list -> context ->
    7.62 -    string option * cterm list * context * context * (term * (term list * term list)) list list
    7.63 +    string option * (cterm list * cterm list) * context * context *
    7.64 +      (term * (term list * term list)) list list
    7.65    val print_locales: theory -> unit
    7.66    val print_locale: theory -> expr -> context attribute element list -> unit
    7.67    val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
    7.68 @@ -67,7 +78,6 @@
    7.69      theory -> theory * (bstring * thm list) list
    7.70    val add_thmss: string -> ((string * thm list) * context attribute list) list ->
    7.71      theory * context -> (theory * context) * (string * thm list) list
    7.72 -  val prune_prems: theory -> thm -> thm
    7.73    val instantiate: string -> string * context attribute list
    7.74      -> thm list option -> context -> context
    7.75    val setup: (theory -> theory) list
    7.76 @@ -93,37 +103,26 @@
    7.77  
    7.78  val empty = Merge [];
    7.79  
    7.80 -datatype ('typ, 'term, 'fact, 'att) elem_expr =
    7.81 -  Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr;
    7.82 +datatype 'a elem_expr =
    7.83 +  Elem of 'a | Expr of expr;
    7.84  
    7.85  type 'att element = (string, string, string, 'att) elem;
    7.86  type 'att element_i = (typ, term, thm list, 'att) elem;
    7.87 -type 'att elem_or_expr = (string, string, string, 'att) elem_expr;
    7.88 -type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr;
    7.89  
    7.90  type locale =
    7.91 - {view: cterm list * thm list,
    7.92 -    (* CB: If locale "loc" contains assumptions, either via import or in the
    7.93 -       locale body, a locale predicate "loc" is defined capturing all the
    7.94 -       assumptions.  If both import and body contain assumptions, additionally
    7.95 -       a delta predicate "loc_axioms" is defined that abbreviates the
    7.96 -       assumptions of the body.
    7.97 -       The context generated when entering "loc" contains not (necessarily) a
    7.98 -       single assumption "loc", but a list of assumptions of all locale
    7.99 -       predicates of locales without import and all delta predicates of
   7.100 -       locales with import from the import hierarchy (duplicates removed,
   7.101 -       cf. [1], normalisation of locale expressions).
   7.102 -
   7.103 -       The record entry view is either ([], []) or ([statement], axioms)
   7.104 -       where statement is the predicate "loc" applied to the parameters,
   7.105 -       and axioms contains projections from "loc" to the list of assumptions
   7.106 -       generated when entering the locale.
   7.107 -       It appears that an axiom of the form A [A] is never generated.
   7.108 -     *)
   7.109 -  import: expr,                                                         (*dynamic import*)
   7.110 -  elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
   7.111 -  params: (string * typ option) list * string list,                     (*all/local params*)
   7.112 -  typing: (string * typ) list};                                         (*inferred parameter types, currently unused*)
   7.113 + {predicate: cterm list * thm list,
   7.114 +    (* CB: For old-style locales with "(open)" this entry is ([], []).
   7.115 +       For new-style locales, which declare predicates, if the locale declares
   7.116 +       no predicates, this is also ([], []).
   7.117 +       If the locale declares predicates, the record field is
   7.118 +       ([statement], axioms), where statement is the locale predicate applied
   7.119 +       to the (assumed) locale parameters.  Axioms contains the projections
   7.120 +       from the locale predicate to the normalised assumptions of the locale
   7.121 +       (cf. [1], normalisation of locale expressions.)
   7.122 +    *)
   7.123 +  import: expr,                                       (*dynamic import*)
   7.124 +  elems: (context attribute element_i * stamp) list,  (*static content*)
   7.125 +  params: (string * typ option) list * string list}   (*all/local params*)
   7.126  
   7.127  
   7.128  (** theory data **)
   7.129 @@ -138,9 +137,9 @@
   7.130    val prep_ext = I;
   7.131  
   7.132    (*joining of locale elements: only facts may be added later!*)
   7.133 -  fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) =
   7.134 -    Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems',
   7.135 -      params = params, typing = typing};
   7.136 +  fun join ({predicate, import, elems, params}: locale, {elems = elems', ...}: locale) =
   7.137 +    Some {predicate = predicate, import = import, elems = gen_merge_lists eq_snd elems elems',
   7.138 +      params = params};
   7.139    fun merge ((space1, locs1), (space2, locs2)) =
   7.140      (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2));
   7.141  
   7.142 @@ -187,176 +186,6 @@
   7.143      imps (Locale (intern sign upper)) (intern sign lower)
   7.144    end;
   7.145  
   7.146 -(** Name suffix of internal delta predicates.
   7.147 -    These specify additional assumptions in a locale with import.
   7.148 -    Also name of theorem set with destruct rules for locale main
   7.149 -    predicates. **)
   7.150 -
   7.151 -val axiomsN = "axioms";
   7.152 -
   7.153 -local
   7.154 -
   7.155 -(* A trie-like structure is used to compute a cover of a normalised
   7.156 -   locale specification.  Entries of the trie will be identifiers:
   7.157 -   locale names with parameter lists. *)
   7.158 -
   7.159 -datatype 'a trie = Trie of ('a * 'a trie) list;
   7.160 -
   7.161 -(* Subsumption relation on identifiers *)
   7.162 -
   7.163 -fun subsumes thy ((name1, args1), (name2, args2)) =
   7.164 -  (name2 = "" andalso null args2) orelse
   7.165 -  ((name2 = name1 orelse imports thy (name1, name2)) andalso
   7.166 -    (args2 prefix args1));
   7.167 -
   7.168 -(* Insert into trie, wherever possible but avoiding branching *)
   7.169 -
   7.170 -fun insert_ident subs id (Trie trie) =
   7.171 -  let
   7.172 -    fun insert id [] = [(id, Trie [])]
   7.173 -      | insert id ((id', Trie t')::ts) =
   7.174 -          if subs (id, id')
   7.175 -          then if null ts
   7.176 -            then [(id', Trie (insert id t'))] (* avoid new branch *)
   7.177 -            else (id', Trie (insert id t'))::insert id ts
   7.178 -          else (id', Trie t')::insert id ts
   7.179 -  in Trie (insert id trie) end;
   7.180 -
   7.181 -(* List of leaves of a trie, removing duplicates *)
   7.182 -
   7.183 -fun leaves _ (Trie []) = []
   7.184 -  | leaves eq (Trie ((id, Trie [])::ts)) =
   7.185 -      gen_ins eq (id, leaves eq (Trie ts))
   7.186 -  | leaves eq (Trie ((id, ts')::ts)) =
   7.187 -      gen_merge_lists eq (leaves eq ts') (leaves eq (Trie ts));
   7.188 -
   7.189 -in 
   7.190 -
   7.191 -(** Prune premises:
   7.192 -   Remove internal delta predicates (generated by "includes") from the
   7.193 -   premises of a theorem.
   7.194 -
   7.195 -   Assumes no outer quantifiers and no flex-flex pairs.
   7.196 -   May change names of TVars.
   7.197 -   Performs compress and close_derivation on result, if modified. **)
   7.198 -
   7.199 -(* Note: reconstruction of the correct premises fails for subspace_normed_vs
   7.200 -   in HOL/Real/HahnBanach/NormedSpace.thy.  This cannot be fixed since in the
   7.201 -   current setup there is no way of distinguishing whether the theorem
   7.202 -   statement involved "includes subspace F E + normed_vectorspace E" or
   7.203 -   "includes subspace F E + vectorspace E + norm E norm".
   7.204 -*)
   7.205 -
   7.206 -fun prune_prems thy thm = let
   7.207 -  val sign = Theory.sign_of thy;
   7.208 -  fun analyse cprem =
   7.209 -    (* Returns None if head of premise is not a predicate defined by a locale,
   7.210 -       returns also None if locale has a view but predicate is not *_axioms
   7.211 -       since this is a premise that wasn't generated by includes.  *)
   7.212 -    case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of
   7.213 -	(Const (raw_name, T), args) => let
   7.214 -            val name = unsuffix ("_" ^ axiomsN) raw_name
   7.215 -              handle LIST _ => raw_name
   7.216 -          in case get_locale thy name of
   7.217 -		None => None
   7.218 -	      | Some {view = (_, axioms), ...} =>
   7.219 -                  if name = raw_name andalso not (null axioms)
   7.220 -                  then None
   7.221 -                  else Some (((name, args), T), name = raw_name)
   7.222 -          end
   7.223 -      | _ => None;
   7.224 -  val TFrees = add_term_tfree_names (prop_of thm, []);
   7.225 -    (* Ignores TFrees in flex-flex pairs ! *)
   7.226 -  val (frozen, thaw) = Drule.freeze_thaw thm;
   7.227 -  val cprop = cprop_of frozen;
   7.228 -  val cprems = Drule.strip_imp_prems cprop;
   7.229 -  val analysis = map analyse cprems;
   7.230 -in
   7.231 -  if foldl (fn (b, None) => b | (b, Some (_, b')) => b andalso b')
   7.232 -           (true, analysis)
   7.233 -  then thm   (* No premise contains *_axioms predicate
   7.234 -                ==> no changes necessary. *)
   7.235 -  else let
   7.236 -    val ids = map (apsome fst) analysis;
   7.237 -    (* Analyse dependencies of locale premises: store in trie. *)
   7.238 -    fun subs ((x, _), (y, _)) = subsumes thy (x, y);
   7.239 -    val Trie depcs = foldl (fn (trie, None) => trie
   7.240 -			     | (trie, Some id) => insert_ident subs id trie)
   7.241 -			   (Trie [], ids);
   7.242 -    (* Assemble new theorem; new prems will be hyps.
   7.243 -       Axioms is an intermediate list of locale axioms required to
   7.244 -       replace old premises by new ones. *)
   7.245 -    fun scan ((roots, thm, cprems', axioms), (cprem, id)) =
   7.246 -	  case id of
   7.247 -	      None => (roots, implies_elim thm (assume cprem),
   7.248 -		       cprems' @ [cprem], [])
   7.249 -					       (* Normal premise: keep *)
   7.250 -	    | Some id =>                       (* Locale premise *)
   7.251 -		let
   7.252 -		  fun elim_ax [] thm =  (* locale has no axioms *)
   7.253 -		      implies_elim thm (assume cprem)
   7.254 -		    | elim_ax axs thm = let
   7.255 -		    (* Eliminate first premise of thm, which is of the form
   7.256 -                       id.  Add hyp of the used axiom to thm. *)
   7.257 -		    val ax = the (assoc (axs, fst (fst id)))
   7.258 -	              handle _ => error ("Internal error in Locale.prune_\
   7.259 -                        \prems: axiom for premise" ^
   7.260 -                        fst (fst id) ^ " not found.");
   7.261 -		    val [ax_cprem] = Drule.strip_imp_prems (cprop_of ax)
   7.262 -		      handle _ => error ("Internal error in Locale.prune_\
   7.263 -                        \prems: exactly one premise in axiom expected.");
   7.264 -		    val ax_hyp = implies_elim ax (assume (ax_cprem))
   7.265 -		  in implies_elim thm ax_hyp
   7.266 -		  end
   7.267 -		in
   7.268 -		  if null roots
   7.269 -		  then (roots, elim_ax axioms thm, cprems', axioms)
   7.270 -					       (* Remaining premise: drop *)
   7.271 -		  else let
   7.272 -		      fun mk_cprem ((name, args), T) = cterm_of sign
   7.273 -                        (ObjectLogic.assert_propT sign
   7.274 -			  (Term.list_comb (Const (name, T), args)));
   7.275 -		      fun get_axs ((name, args), _) = let
   7.276 -			  val {view = (_, axioms), ...} = the_locale thy name;
   7.277 -			  fun inst ax =
   7.278 -			    let
   7.279 -			      val std = standard ax;
   7.280 -                              val (prem, concl) =
   7.281 -                                Logic.dest_implies (prop_of std);
   7.282 -			      val (Const (name2, _), _) = Term.strip_comb
   7.283 -				(ObjectLogic.drop_judgment sign concl);
   7.284 -                              val (_, vars) = Term.strip_comb
   7.285 -				(ObjectLogic.drop_judgment sign prem);
   7.286 -			      val cert = map (cterm_of sign);
   7.287 -			    in (unsuffix ("_" ^ axiomsN) name2
   7.288 -                                  handle LIST _ => name2,
   7.289 -			       cterm_instantiate (cert vars ~~ cert args) std)
   7.290 -			    end;
   7.291 -			in map inst axioms end;
   7.292 -		      val (id', trie) = hd roots;
   7.293 -		    in if id = id'
   7.294 -		      then                     (* Initial premise *)
   7.295 -			let
   7.296 -			  val lvs = leaves eq_fst (Trie [(id', trie)]);
   7.297 -			  val axioms' = flat (map get_axs lvs)
   7.298 -			in (tl roots, elim_ax axioms' thm,
   7.299 -                            cprems' @ map (mk_cprem) lvs, axioms')
   7.300 -			end
   7.301 -		      else (roots, elim_ax axioms thm, cprems', axioms)
   7.302 -					       (* Remaining premise: drop *)
   7.303 -		    end
   7.304 -		end;
   7.305 -    val (_, thm', cprems', _) =
   7.306 -      (foldl scan ((depcs, frozen, [], []), cprems ~~ ids));
   7.307 -    val thm'' = implies_intr_list cprems' thm';
   7.308 -  in
   7.309 -    fst (varifyT' TFrees (thaw thm''))
   7.310 -    |> Thm.compress |> Drule.close_derivation
   7.311 -  end
   7.312 -end;
   7.313 -
   7.314 -end (* local *)
   7.315 -
   7.316  
   7.317  (* diagnostics *)
   7.318  
   7.319 @@ -372,6 +201,9 @@
   7.320          (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
   7.321    in raise ProofContext.CONTEXT (err_msg, ctxt) end;
   7.322  
   7.323 +(* Version for identifiers with axioms *)
   7.324 +
   7.325 +fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
   7.326  
   7.327  
   7.328  (** primitives **)
   7.329 @@ -502,6 +334,7 @@
   7.330    in map (apsome (Envir.norm_type unifier')) Vs end;
   7.331  
   7.332  fun params_of elemss = gen_distinct eq_fst (flat (map (snd o fst) elemss));
   7.333 +fun params_of' elemss = gen_distinct eq_fst (flat (map (snd o fst o fst) elemss));
   7.334  
   7.335  (* CB: param_types has the following type:
   7.336    ('a * 'b Library.option) list -> ('a * 'b) list *)
   7.337 @@ -512,7 +345,7 @@
   7.338  
   7.339  local
   7.340  
   7.341 -(* CB: unique_parms has the following type:
   7.342 +(* CB: OUTDATED unique_parms has the following type:
   7.343       'a ->
   7.344       (('b * (('c * 'd) list * Symtab.key list)) * 'e) list ->
   7.345       (('b * ('c * 'd) list) * 'e) list  *)
   7.346 @@ -520,13 +353,13 @@
   7.347  fun unique_parms ctxt elemss =
   7.348    let
   7.349      val param_decls =
   7.350 -      flat (map (fn ((name, (ps, qs)), _) => map (rpair (name, ps)) qs) elemss)
   7.351 +      flat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)
   7.352        |> Symtab.make_multi |> Symtab.dest;
   7.353    in
   7.354      (case find_first (fn (_, ids) => length ids > 1) param_decls of
   7.355        Some (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)
   7.356            (map (apsnd (map fst)) ids)
   7.357 -    | None => map (apfst (apsnd #1)) elemss)
   7.358 +    | None => map (apfst (apfst (apsnd #1))) elemss)
   7.359    end;
   7.360  
   7.361  (* CB: unify_parms has the following type:
   7.362 @@ -537,7 +370,8 @@
   7.363  
   7.364  fun unify_parms ctxt fixed_parms raw_parmss =
   7.365    let
   7.366 -    val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
   7.367 +    val sign = ProofContext.sign_of ctxt;
   7.368 +    val tsig = Sign.tsig_of sign;
   7.369      val maxidx = length raw_parmss;
   7.370      val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
   7.371  
   7.372 @@ -545,8 +379,13 @@
   7.373      fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   7.374      val parms = fixed_parms @ flat (map varify_parms idx_parmss);
   7.375  
   7.376 -    fun unify T ((env, maxidx), U) = Type.unify tsig (env, maxidx) (U, T)
   7.377 -      handle Type.TUNIFY => raise TYPE ("unify_parms: failed to unify types", [U, T], []);
   7.378 +    fun unify T ((env, maxidx), U) =
   7.379 +      Type.unify tsig (env, maxidx) (U, T)
   7.380 +      handle Type.TUNIFY =>
   7.381 +        let val prt = Sign.string_of_typ sign
   7.382 +        in raise TYPE ("unify_parms: failed to unify types " ^
   7.383 +          prt U ^ " and " ^ prt T, [U, T], [])
   7.384 +        end
   7.385      fun unify_list (envir, T :: Us) = foldl (unify T) (envir, Us)
   7.386        | unify_list (envir, []) = envir;
   7.387      val (unifier, _) = foldl unify_list
   7.388 @@ -564,13 +403,26 @@
   7.389  
   7.390  in
   7.391  
   7.392 +(* like unify_elemss, but does not touch axioms *)
   7.393 +
   7.394 +fun unify_elemss' _ _ [] = []
   7.395 +  | unify_elemss' _ [] [elems] = [elems]
   7.396 +  | unify_elemss' ctxt fixed_parms elemss =
   7.397 +      let
   7.398 +        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
   7.399 +        fun inst ((((name, ps), axs), elems), env) =
   7.400 +          (((name, map (apsnd (apsome (inst_type env))) ps),  axs),
   7.401 +           map (inst_elem ctxt env) elems);
   7.402 +      in map inst (elemss ~~ envs) end;
   7.403 +
   7.404  fun unify_elemss _ _ [] = []
   7.405    | unify_elemss _ [] [elems] = [elems]
   7.406    | unify_elemss ctxt fixed_parms elemss =
   7.407        let
   7.408 -        val envs = unify_parms ctxt fixed_parms (map (#2 o #1) elemss);
   7.409 -        fun inst (((name, ps), elems), env) =
   7.410 -          ((name, map (apsnd (apsome (inst_type env))) ps), (map (inst_elem ctxt env) elems));
   7.411 +        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
   7.412 +        fun inst ((((name, ps), axs), elems), env) =
   7.413 +          (((name, map (apsnd (apsome (inst_type env))) ps), 
   7.414 +            map (inst_thm ctxt env) axs), map (inst_elem ctxt env) elems);
   7.415        in map inst (elemss ~~ envs) end;
   7.416  
   7.417  fun flatten_expr ctxt (prev_idents, expr) =
   7.418 @@ -583,35 +435,55 @@
   7.419        | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
   7.420            commas (map (fn None => "_" | Some x => quote x) xs));
   7.421  
   7.422 -    fun rename_parms ren (name, ps) =
   7.423 +    fun rename_parms top ren ((name, ps), (parms, axs)) =
   7.424        let val ps' = map (rename ren) ps in
   7.425 -        (case duplicates ps' of [] => (name, ps')
   7.426 +        (case duplicates ps' of [] => ((name, ps'),
   7.427 +          if top then (map (rename ren) parms, map (rename_thm ren) axs)
   7.428 +          else (parms, axs))
   7.429          | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
   7.430        end;
   7.431  
   7.432 -    fun identify ((ids, parms), Locale name) =
   7.433 -    (* CB: ids is list of pairs: locale name and list of parameter renamings,
   7.434 +    fun identify top (Locale name) =
   7.435 +    (* CB: ids is a list of tuples of the form ((name, ps), axs),
   7.436 +       where name is a locale name, ps a list of parameter names and axs
   7.437 +       a list of axioms relating to the identifier, axs is empty unless
   7.438 +       identify at top level (top = true);
   7.439         parms is accumulated list of parameters *)
   7.440            let
   7.441 -            val {import, params, ...} = the_locale thy name;
   7.442 +            val {predicate = (_, axioms), import, params, ...} =
   7.443 +              the_locale thy name;
   7.444              val ps = map #1 (#1 params);
   7.445 -          in
   7.446 -            if (name, ps) mem ids then (ids, parms)
   7.447 -            else
   7.448 -              let val (ids', parms') = identify ((ids, parms), import);  (*acyclic dependencies!*)
   7.449 -              in (ids' @ [(name, ps)], merge_lists parms' ps) end
   7.450 -          end
   7.451 -      | identify ((ids, parms), Rename (e, xs)) =
   7.452 +            val (ids', parms') = identify false import;
   7.453 +                (* acyclic import dependencies *)
   7.454 +            val ids'' = ids' @ [((name, ps), ([], []))];
   7.455 +            val ids_ax = if top then snd
   7.456 +                 (foldl_map (fn (axs, ((name, parms), _)) => let
   7.457 +                   val {elems, ...} = the_locale thy name;
   7.458 +                   val ts = flat (mapfilter (fn (Assumes asms, _) =>
   7.459 +                     Some (flat (map (map #1 o #2) asms)) | _ => None) elems);
   7.460 +                   val (axs1, axs2) = splitAt (length ts, axs);
   7.461 +                 in (axs2, ((name, parms), (ps, axs1))) end) (axioms, ids''))
   7.462 +               else ids'';
   7.463 +          in (ids_ax, merge_lists parms' ps) end
   7.464 +      | identify top (Rename (e, xs)) =
   7.465            let
   7.466 -            val (ids', parms') = identify (([], []), e);
   7.467 +            val (ids', parms') = identify top e;
   7.468              val ren = renaming xs parms'
   7.469 -              handle ERROR_MESSAGE msg => err_in_locale ctxt msg ids';
   7.470 -            val ids'' = distinct (map (rename_parms ren) ids');
   7.471 -            val parms'' = distinct (flat (map #2 ids''));
   7.472 -          in (merge_lists ids ids'', merge_lists parms parms'') end
   7.473 -      | identify (arg, Merge es) = foldl identify (arg, es);
   7.474 +              handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
   7.475 +            val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
   7.476 +            val parms'' = distinct (flat (map (#2 o #1) ids''));
   7.477 +          in (ids'', parms'') end
   7.478 +      | identify top (Merge es) =
   7.479 +          foldl (fn ((ids, parms), e) => let
   7.480 +                     val (ids', parms') = identify top e
   7.481 +                   in (gen_merge_lists eq_fst ids ids',
   7.482 +                       merge_lists parms parms') end)
   7.483 +            (([], []), es);
   7.484  
   7.485 -    fun eval (name, xs) =
   7.486 +    (* CB: enrich identifiers by parameter types and 
   7.487 +       the corresponding elements (with renamed parameters) *)
   7.488 +
   7.489 +    fun eval ((name, xs), axs) =
   7.490        let
   7.491          val {params = (ps, qs), elems, ...} = the_locale thy name;
   7.492          val ren = filter_out (op =) (map #1 ps ~~ xs);
   7.493 @@ -620,12 +492,29 @@
   7.494            else ((map (apfst (rename ren)) ps, map (rename ren) qs),
   7.495              map (rename_elem ren o #1) elems);
   7.496          val elems'' = map (rename_facts (space_implode "_" xs)) elems';
   7.497 -      in ((name, params'), elems'') end;
   7.498 +      in (((name, params'), axs), elems'') end;
   7.499  
   7.500 -    val idents = gen_rems (op =) (#1 (identify (([], []), expr)), prev_idents);
   7.501 +    (* compute identifiers, merge with previous ones *)
   7.502 +    val idents = gen_rems eq_fst (#1 (identify true expr), prev_idents);
   7.503 +    (* add types to params, check for unique params and unify them *)
   7.504      val raw_elemss = unique_parms ctxt (map eval idents);
   7.505 -    val elemss = unify_elemss ctxt [] raw_elemss;
   7.506 -  in (prev_idents @ idents, elemss) end;
   7.507 +    val elemss = unify_elemss' ctxt [] raw_elemss;
   7.508 +    (* replace params in ids by params from axioms,
   7.509 +       adjust types in axioms *)
   7.510 +    val all_params' = params_of' elemss;
   7.511 +    val all_params = param_types all_params';
   7.512 +    val elemss' = map (fn (((name, _), (ps, axs)), elems) =>
   7.513 +         (((name, map (fn p => (p, assoc (all_params, p))) ps), axs), elems))
   7.514 +         elemss;
   7.515 +    fun inst_ax th = let
   7.516 +         val {hyps, prop, ...} = Thm.rep_thm th;
   7.517 +         val ps = map (apsnd Some) (foldl Term.add_frees ([], prop :: hyps));
   7.518 +         val [env] = unify_parms ctxt all_params [ps];
   7.519 +         val th' = inst_thm ctxt env th;
   7.520 +       in th' end;
   7.521 +    val final_elemss = map (fn ((id, axs), elems) =>
   7.522 +         ((id, map inst_ax axs), elems)) elemss';
   7.523 +  in (prev_idents @ idents, final_elemss) end;
   7.524  
   7.525  end;
   7.526  
   7.527 @@ -636,15 +525,17 @@
   7.528  
   7.529  fun export_axioms axs _ hyps th =
   7.530    th |> Drule.satisfy_hyps axs
   7.531 +     (* CB: replace meta-hyps, using axs, by a single meta-hyp. *)
   7.532    |> Drule.implies_intr_list (Library.drop (length axs, hyps))
   7.533 -  |> Seq.single;
   7.534 +     (* CB: turn remaining hyps into assumptions. *)
   7.535 +  |> Seq.single
   7.536  
   7.537  fun activate_elem _ ((ctxt, axs), Fixes fixes) =
   7.538        ((ctxt |> ProofContext.add_fixes fixes, axs), [])
   7.539    | activate_elem _ ((ctxt, axs), Assumes asms) =
   7.540        let
   7.541          val ts = flat (map (map #1 o #2) asms);
   7.542 -        val (ps,qs) = splitAt (length ts, axs)
   7.543 +        val (ps,qs) = splitAt (length ts, axs);
   7.544          val (ctxt', _) =
   7.545            ctxt |> ProofContext.fix_frees ts
   7.546            |> ProofContext.assume_i (export_axioms ps) asms;
   7.547 @@ -660,27 +551,28 @@
   7.548        let val (ctxt', res) = ctxt |> ProofContext.note_thmss_i facts
   7.549        in ((ctxt', axs), if is_ext then res else []) end;
   7.550  
   7.551 -fun activate_elems ((name, ps), elems) (ctxt, axs) =
   7.552 -  let val ((ctxt', axs'), res) =
   7.553 +fun activate_elems (((name, ps), axs), elems) ctxt =
   7.554 +  let val ((ctxt', _), res) =
   7.555      foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems)
   7.556        handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
   7.557 -  in ((ProofContext.restore_qualified ctxt ctxt', axs'), res) end;
   7.558 +  in (ProofContext.restore_qualified ctxt ctxt', res) end;
   7.559  
   7.560 -fun activate_elemss prep_facts = foldl_map (fn ((ctxt, axs), ((name, ps), raw_elems)) =>
   7.561 +fun activate_elemss prep_facts = foldl_map (fn (ctxt, (((name, ps), axs), raw_elems)) =>
   7.562    let
   7.563      val elems = map (prep_facts ctxt) raw_elems;
   7.564 -    val ((ctxt', axs'), res) = apsnd flat (activate_elems ((name, ps), elems) (ctxt, axs));
   7.565 -  in ((ctxt', axs'), (((name, ps), elems), res)) end);
   7.566 +    val (ctxt', res) = apsnd flat (activate_elems (((name, ps), axs), elems) ctxt);
   7.567 +  in (ctxt', (((name, ps), elems), res)) end);
   7.568  
   7.569  in
   7.570  
   7.571 -(* CB: activate_facts prep_facts ((ctxt, axioms), elemss),
   7.572 -   where elemss is a list of pairs consisting of identifiers and context
   7.573 -   elements, extends ctxt by the context elements yielding ctxt' and returns
   7.574 -   ((ctxt', axioms'), (elemss', facts)).
   7.575 -   Assumptions use entries from axioms to set up exporters in ctxt'.  Unused
   7.576 -   axioms are returned as axioms'; elemss' is obtained from elemss (without
   7.577 -   identifier) and the intermediate context with prep_facts.
   7.578 +(* CB: activate_facts prep_facts (ctxt, elemss),
   7.579 +   where elemss is a list of pairs consisting of identifiers and
   7.580 +   context elements, extends ctxt by the context elements yielding
   7.581 +   ctxt' and returns (ctxt', (elemss', facts)).
   7.582 +   Identifiers in the argument are of the form ((name, ps), axs) and
   7.583 +   assumptions use the axioms in the identifiers to set up exporters
   7.584 +   in ctxt'.  elemss' does not contain identifiers and is obtained
   7.585 +   from elemss and the intermediate context with prep_facts.
   7.586     If get_facts or get_facts_i is used for prep_facts, these also remove
   7.587     the internal/external markers from elemss. *)
   7.588  
   7.589 @@ -701,22 +593,30 @@
   7.590  
   7.591  (* attributes *)
   7.592  
   7.593 -local fun read_att attrib (x, srcs) = (x, map attrib srcs) in
   7.594 +local
   7.595 +
   7.596 +fun read_att attrib (x, srcs) = (x, map attrib srcs)
   7.597  
   7.598  (* CB: Map attrib over
   7.599     * A context element: add attrib to attribute lists of assumptions,
   7.600       definitions and facts (on both sides for facts).
   7.601     * Locale expression: no effect. *)
   7.602  
   7.603 -
   7.604 -fun map_attrib_elem _ (Fixes fixes) = Fixes fixes
   7.605 -  | map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
   7.606 -  | map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
   7.607 -  | map_attrib_elem attrib (Notes facts) =
   7.608 +fun gen_map_attrib_elem _ (Fixes fixes) = Fixes fixes
   7.609 +  | gen_map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
   7.610 +  | gen_map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
   7.611 +  | gen_map_attrib_elem attrib (Notes facts) =
   7.612        Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
   7.613  
   7.614 -fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem)
   7.615 -  | map_attrib_elem_expr _ (Expr expr) = Expr expr;
   7.616 +fun gen_map_attrib_elem_expr attrib (Elem elem) = Elem (gen_map_attrib_elem attrib elem)
   7.617 +  | gen_map_attrib_elem_expr _ (Expr expr) = Expr expr;
   7.618 +
   7.619 +in
   7.620 +
   7.621 +val map_attrib_element = gen_map_attrib_elem;
   7.622 +val map_attrib_element_i = gen_map_attrib_elem;
   7.623 +val map_attrib_elem_or_expr = gen_map_attrib_elem_expr;
   7.624 +val map_attrib_elem_or_expr_i = gen_map_attrib_elem_expr;
   7.625  
   7.626  end;
   7.627  
   7.628 @@ -739,7 +639,7 @@
   7.629  
   7.630  (* propositions and bindings *)
   7.631  
   7.632 -(* CB: an internal locale (Int) element was either imported or included,
   7.633 +(* CB: an internal (Int) locale element was either imported or included,
   7.634     an external (Ext) element appears directly in the locale. *)
   7.635  
   7.636  datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
   7.637 @@ -750,13 +650,17 @@
   7.638     It returns (ids', elemss) where ids' is an extension of ids
   7.639     with identifiers generated for expr, and elemss is the list of
   7.640     context elements generated from expr, decorated with additional
   7.641 -   information (the identifiers?), including parameter names.
   7.642 -   It appears that the identifier name is empty for external elements
   7.643 -   (this is suggested by the implementation of activate_facts). *)
   7.644 +   information (for expr it is the identifier, where parameters additionially
   7.645 +   contain type information (extracted from the locale record), for a Fixes
   7.646 +   element, it is an identifier with name = "" and parameters with type
   7.647 +   information None, for other elements it is simply ("", [])).
   7.648 +   The implementation of activate_facts relies on identifier names being
   7.649 +   empty strings for external elements.
   7.650 +TODO: correct this comment wrt axioms. *)
   7.651  
   7.652  fun flatten _ (ids, Elem (Fixes fixes)) =
   7.653 -      (ids, [(("", map (rpair None o #1) fixes), Ext (Fixes fixes))])
   7.654 -  | flatten _ (ids, Elem elem) = (ids, [(("", []), Ext elem)])
   7.655 +      (ids, [((("", map (rpair None o #1) fixes), []), Ext (Fixes fixes))])
   7.656 +  | flatten _ (ids, Elem elem) = (ids, [((("", []), []), Ext elem)])
   7.657    | flatten (ctxt, prep_expr) (ids, Expr expr) =
   7.658        apsnd (map (apsnd Int)) (flatten_expr ctxt (ids, prep_expr expr));
   7.659  
   7.660 @@ -775,7 +679,7 @@
   7.661    | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   7.662    | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
   7.663  
   7.664 -fun declare_elems prep_fixes (ctxt, ((name, ps), elems)) =
   7.665 +fun declare_elems prep_fixes (ctxt, (((name, ps), _), elems)) =
   7.666    let val (ctxt', propps) =
   7.667      (case elems of
   7.668        Int es => foldl_map declare_int_elem (ctxt, es)
   7.669 @@ -838,6 +742,8 @@
   7.670      (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
   7.671    end;
   7.672  
   7.673 +(* CB: for finish_elems (Int and Ext) *)
   7.674 +
   7.675  fun eval_text _ _ _ (text, Fixes _) = text
   7.676    | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) =
   7.677        let
   7.678 @@ -847,10 +753,12 @@
   7.679            if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
   7.680            else ((exts, exts'), (ints @ ts, ints' @ ts'));
   7.681        in (spec', (foldl Term.add_frees (xs, ts'), env, defs)) end
   7.682 -  | eval_text ctxt id _ ((spec, binds), Defines defs) =
   7.683 +  | eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
   7.684        (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
   7.685    | eval_text _ _ _ (text, Notes _) = text;
   7.686  
   7.687 +(* CB: for finish_elems (Ext) *)
   7.688 +
   7.689  fun closeup _ false elem = elem
   7.690    | closeup ctxt true elem =
   7.691        let
   7.692 @@ -880,14 +788,18 @@
   7.693        close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
   7.694    | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   7.695  
   7.696 -fun finish_parms parms ((name, ps), elems) =
   7.697 -  ((name, map (fn (x, _) => (x, assoc (parms, x))) ps), elems);
   7.698 +(* CB: finish_parms introduces type info from parms to identifiers *)
   7.699 +(* CB: only needed for types that have been None so far???
   7.700 +   If so, which are these??? *)
   7.701 +
   7.702 +fun finish_parms parms (((name, ps), axs), elems) =
   7.703 +  (((name, map (fn (x, _) => (x, assoc (parms, x))) ps), axs), elems);
   7.704  
   7.705  fun finish_elems ctxt parms _ (text, ((id, Int e), _)) =
   7.706        let
   7.707 -        val [(_, es)] = unify_elemss ctxt parms [(id, e)];
   7.708 -        val text' = foldl (eval_text ctxt id false) (text, es);
   7.709 -      in (text', (id, map Int es)) end
   7.710 +        val [(id', es)] = unify_elemss ctxt parms [(id, e)];
   7.711 +        val text' = foldl (eval_text ctxt id' false) (text, es);
   7.712 +      in (text', (id', map Int es)) end
   7.713    | finish_elems ctxt parms do_close (text, ((id, Ext e), [propp])) =
   7.714        let
   7.715          val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
   7.716 @@ -896,6 +808,8 @@
   7.717  
   7.718  in
   7.719  
   7.720 +(* CB: only called by prep_elemss *)
   7.721 +
   7.722  fun finish_elemss ctxt parms do_close =
   7.723    foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
   7.724  
   7.725 @@ -907,30 +821,37 @@
   7.726    let
   7.727      (* CB: contexts computed in the course of this function are discarded.
   7.728         They are used for type inference and consistency checks only. *)
   7.729 +    (* CB: fixed_params are the parameters (with types) of the target locale,
   7.730 +       empty list if there is no target. *)
   7.731      (* CB: raw_elemss are list of pairs consisting of identifiers and
   7.732         context elements, the latter marked as internal or external. *)
   7.733      val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
   7.734      (* CB: raw_ctxt is context with additional fixed variables derived from
   7.735         the fixes elements in raw_elemss,
   7.736         raw_proppss contains assumptions and definitions from the
   7.737 -       (external?) elements in raw_elemss. *)
   7.738 +       external elements in raw_elemss. *)
   7.739      val raw_propps = map flat raw_proppss;
   7.740      val raw_propp = flat raw_propps;
   7.741 +
   7.742 +    (* CB: add type information from fixed_params to context (declare_terms) *)
   7.743 +    (* CB: process patterns (conclusion and external elements only) *)
   7.744      val (ctxt, all_propp) =
   7.745        prepp (ProofContext.declare_terms (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
   7.746 -    (* CB: read/cert entire proposition (conclusion and premises from
   7.747 -       the context elements). *)
   7.748 +    
   7.749 +    (* CB: add type information from conclusion and external elements
   7.750 +       to context *)
   7.751      val ctxt = ProofContext.declare_terms (flat (map (map fst) all_propp)) ctxt;
   7.752 -    (* CB: it appears that terms declared in the propositions are added
   7.753 -       to the context here. *)
   7.754  
   7.755 +    (* CB: resolve schematic variables (patterns) in conclusion and external
   7.756 +       elements. *)
   7.757      val all_propp' = map2 (op ~~)
   7.758        (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
   7.759      val (concl, propp) = splitAt(length raw_concl, all_propp');
   7.760      val propps = unflat raw_propps propp;
   7.761      val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
   7.762  
   7.763 -    val xs = map #1 (params_of raw_elemss);
   7.764 +    (* CB: obtain all parameters from identifier part of raw_elemss *)
   7.765 +    val xs = map #1 (params_of' raw_elemss);
   7.766      val typing = unify_frozen ctxt 0
   7.767        (map (ProofContext.default_type raw_ctxt) xs)
   7.768        (map (ProofContext.default_type ctxt) xs);
   7.769 @@ -977,7 +898,7 @@
   7.770  local
   7.771  
   7.772  fun prep_name ctxt (name, atts) =
   7.773 -  (* CB: reject qualified names in locale declarations *)
   7.774 +  (* CB: reject qualified theorem names in locale declarations *)
   7.775    if NameSpace.is_qualified name then
   7.776      raise ProofContext.CONTEXT ("Illegal qualified name: " ^ quote name, ctxt)
   7.777    else (name, atts);
   7.778 @@ -1002,7 +923,7 @@
   7.779  local
   7.780  
   7.781  fun prep_context_statement prep_expr prep_elemss prep_facts
   7.782 -    do_close axioms fixed_params import elements raw_concl context =
   7.783 +    do_close fixed_params import elements raw_concl context =
   7.784    let
   7.785      val sign = ProofContext.sign_of context;
   7.786  
   7.787 @@ -1014,14 +935,18 @@
   7.788         context elements obtained from import and elements. *)
   7.789      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
   7.790        context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
   7.791 +    (* CB: all_elemss and parms contain the correct parameter types *)
   7.792      val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
   7.793 -    val ((import_ctxt, axioms'), (import_elemss, _)) =
   7.794 -      activate_facts prep_facts ((context, axioms), ps);
   7.795 +    val (import_ctxt, (import_elemss, _)) =
   7.796 +      activate_facts prep_facts (context, ps);
   7.797  
   7.798 -    val ((ctxt, _), (elemss, _)) =
   7.799 -      activate_facts prep_facts ((import_ctxt, axioms'), qs);
   7.800 +    val (ctxt, (elemss, _)) =
   7.801 +      activate_facts prep_facts (import_ctxt, qs);
   7.802 +    val stmt = gen_duplicates Term.aconv
   7.803 +       (flat (map (fn ((_, axs), _) => flat (map (#hyps o Thm.rep_thm) axs)) qs));
   7.804 +    val cstmt = map (cterm_of sign) stmt;
   7.805    in
   7.806 -    ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), concl)
   7.807 +    ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl))
   7.808    end;
   7.809  
   7.810  val gen_context = prep_context_statement intern_expr read_elemss get_facts;
   7.811 @@ -1031,22 +956,22 @@
   7.812    let
   7.813      val thy = ProofContext.theory_of ctxt;
   7.814      val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
   7.815 -    val ((view_statement, view_axioms), fixed_params, import) =
   7.816 -(* CB: view_axioms are xxx.axioms of locale xxx *)
   7.817 -      (case locale of None => (([], []), [], empty)
   7.818 +    val (target_stmt, fixed_params, import) =
   7.819 +      (case locale of None => ([], [], empty)
   7.820        | Some name =>
   7.821 -          let val {view, params = (ps, _), ...} = the_locale thy name
   7.822 -          in (view, param_types ps, Locale name) end);
   7.823 -    val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
   7.824 -      prep_ctxt false view_axioms fixed_params import elems concl ctxt;
   7.825 -  in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end;
   7.826 +          let val {predicate = (stmt, _), params = (ps, _), ...} =
   7.827 +            the_locale thy name
   7.828 +          in (stmt, param_types ps, Locale name) end);
   7.829 +    val ((((locale_ctxt, _), (elems_ctxt, _)), _), (elems_stmt, concl')) =
   7.830 +      prep_ctxt false fixed_params import elems concl ctxt;
   7.831 +  in (locale, (target_stmt, elems_stmt), locale_ctxt, elems_ctxt, concl') end;
   7.832  
   7.833  in
   7.834  
   7.835  (* CB: processing of locales for add_locale(_i) and print_locale *)
   7.836    (* CB: arguments are: x->import, y->body (elements), z->context *)
   7.837 -fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z);
   7.838 -fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z);
   7.839 +fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z);
   7.840 +fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z);
   7.841  
   7.842  (* CB: processing of locales for note_thmss(_i),
   7.843     Proof.multi_theorem(_i) and antiquotations with option "locale" *)
   7.844 @@ -1067,7 +992,7 @@
   7.845  
   7.846      (** process the locale **)
   7.847  
   7.848 -    val {view = (_, axioms), params = (ps, _), ...} =
   7.849 +    val {predicate = (_, axioms), params = (ps, _), ...} =
   7.850        the_locale thy (intern sign loc_name);
   7.851      val fixed_params = param_types ps;
   7.852      val init = ProofContext.init thy;
   7.853 @@ -1294,19 +1219,20 @@
   7.854  
   7.855  fun put_facts loc args thy =
   7.856    let
   7.857 -    val {view, import, elems, params, typing} = the_locale thy loc;
   7.858 +    val {predicate, import, elems, params} = the_locale thy loc;
   7.859      val note = Notes (map (fn ((a, more_atts), th_atts) =>
   7.860        ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
   7.861 -  in thy |> put_locale loc {view = view, import = import, elems = elems @ [(note, stamp ())],
   7.862 -    params = params, typing = typing} end;
   7.863 +  in thy |> put_locale loc {predicate = predicate, import = import, elems = elems @ [(note, stamp ())],
   7.864 +    params = params} end;
   7.865  
   7.866  fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   7.867    let
   7.868      val thy_ctxt = ProofContext.init thy;
   7.869      val loc = prep_locale (Theory.sign_of thy) raw_loc;
   7.870 -    val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt;
   7.871 +    val (_, (stmt, _), loc_ctxt, _, _) =
   7.872 +      cert_context_statement (Some loc) [] [] thy_ctxt;
   7.873      val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
   7.874 -    val export = ProofContext.export_standard view loc_ctxt thy_ctxt;
   7.875 +    val export = ProofContext.export_standard stmt loc_ctxt thy_ctxt;
   7.876      val results = map (map export o #2) (#2 (ProofContext.note_thmss_i args loc_ctxt));
   7.877      val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   7.878    in
   7.879 @@ -1317,20 +1243,21 @@
   7.880  
   7.881  in
   7.882  
   7.883 +(* CB: note_thmss(_i) is the base for the Isar commands
   7.884 +   "theorems (in loc)" and "declare (in loc)". *)
   7.885 +
   7.886  val note_thmss = gen_note_thmss intern ProofContext.get_thms;
   7.887  val note_thmss_i = gen_note_thmss (K I) (K I);
   7.888 -  (* CB: note_thmss(_i) is the base for the Isar commands
   7.889 -     "theorems (in loc)" and "declare (in loc)". *)
   7.890 +
   7.891 +(* CB: only used in Proof.finish_global. *)
   7.892  
   7.893  fun add_thmss loc args (thy, ctxt) =
   7.894    let
   7.895      val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
   7.896      val thy' = put_facts loc args' thy;
   7.897 -    val {view = (_, view_axioms), ...} = the_locale thy loc;
   7.898 -    val ((ctxt', _), (_, facts')) =
   7.899 -      activate_facts (K I) ((ctxt, view_axioms), [(("", []), [Notes args'])]);
   7.900 +    val (ctxt', (_, facts')) =
   7.901 +      activate_facts (K I) (ctxt, [((("", []), []), [Notes args'])]);
   7.902    in ((thy', ctxt'), facts') end;
   7.903 -  (* CB: only used in Proof.finish_global. *)
   7.904  
   7.905  end;
   7.906  
   7.907 @@ -1340,7 +1267,13 @@
   7.908  
   7.909  local
   7.910  
   7.911 +(* introN: name of theorems for introduction rules of locale and
   7.912 +     delta predicates;
   7.913 +   axiomsN: name of theorem set with destruct rules for locale predicates,
   7.914 +     also name suffix of delta predicates. *)
   7.915 +
   7.916  val introN = "intro";
   7.917 +val axiomsN = "axioms";
   7.918  
   7.919  fun atomize_spec sign ts =
   7.920    let
   7.921 @@ -1419,6 +1352,8 @@
   7.922    | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts))
   7.923    | change_elem _ e = e;
   7.924  
   7.925 +(* CB: changes only "new" elems, these have identifier ("", _). *)
   7.926 +
   7.927  fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
   7.928    (fn (axms, (id as ("", _), es)) =>
   7.929      foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) |> apsnd (pair id)
   7.930 @@ -1444,7 +1379,7 @@
   7.931              [((introN, []), [([intro], [])])]
   7.932            |> #1 |> rpair (elemss', [statement])
   7.933          end;
   7.934 -    val (thy'', view) =
   7.935 +    val (thy'', predicate) =
   7.936        if Library.null ints then (thy', ([], []))
   7.937        else
   7.938          let
   7.939 @@ -1457,7 +1392,7 @@
   7.940               ((axiomsN, []), [(map Drule.standard axioms, [])])]
   7.941            |> #1 |> rpair ([cstatement], axioms)
   7.942          end;
   7.943 -  in (thy'', (elemss', view)) end;
   7.944 +  in (thy'', (elemss', predicate)) end;
   7.945  
   7.946  end;
   7.947  
   7.948 @@ -1478,25 +1413,31 @@
   7.949      val thy_ctxt = ProofContext.init thy;
   7.950      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) =
   7.951        prep_ctxt raw_import raw_body thy_ctxt;
   7.952 -    (* typing: all parameters with their types *)
   7.953 -    val (typing, _, _) = text;
   7.954      val elemss = import_elemss @ body_elemss;
   7.955  
   7.956 -    val (pred_thy, (elemss', view as (view_statement, view_axioms))) =
   7.957 +    val (pred_thy, (elemss', predicate as (predicate_statement, predicate_axioms))) =
   7.958        if do_pred then thy |> define_preds bname text elemss
   7.959        else (thy, (elemss, ([], [])));
   7.960      val pred_ctxt = ProofContext.init pred_thy;
   7.961  
   7.962 -    val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms), elemss');
   7.963 -    val export = ProofContext.export_standard view_statement ctxt pred_ctxt;
   7.964 +    fun axiomify axioms elemss = 
   7.965 +      (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
   7.966 +                   val ts = flat (mapfilter (fn (Assumes asms) =>
   7.967 +                     Some (flat (map (map #1 o #2) asms)) | _ => None) elems);
   7.968 +                   val (axs1, axs2) = splitAt (length ts, axs);
   7.969 +                 in (axs2, ((id, axs1), elems)) end)
   7.970 +        |> snd;
   7.971 +    val (ctxt, (_, facts)) = activate_facts (K I)
   7.972 +      (pred_ctxt, axiomify predicate_axioms elemss');
   7.973 +    val export = ProofContext.export_standard predicate_statement ctxt pred_ctxt;
   7.974      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
   7.975    in
   7.976      pred_thy
   7.977      |> note_thmss_qualified "" name facts' |> #1
   7.978      |> declare_locale name
   7.979 -    |> put_locale name {view = view, import = prep_expr sign raw_import,
   7.980 +    |> put_locale name {predicate = predicate, import = prep_expr sign raw_import,
   7.981          elems = map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))),
   7.982 -        params = (params_of elemss', map #1 (params_of body_elemss)), typing = typing}
   7.983 +        params = (params_of elemss', map #1 (params_of body_elemss))}
   7.984    end;
   7.985  
   7.986  in
     8.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Sep 23 12:48:49 2004 +0200
     8.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Sep 27 10:27:34 2004 +0200
     8.3 @@ -73,7 +73,7 @@
     8.4    val locale_expr: token list -> Locale.expr * token list
     8.5    val locale_keyword: token list -> string * token list
     8.6    val locale_element: token list -> Args.src Locale.element * token list
     8.7 -  val locale_elem_or_expr: token list -> Args.src Locale.elem_or_expr * token list
     8.8 +  val locale_elem_or_expr: token list -> Args.src Locale.element Locale.elem_expr * token list
     8.9    val method: token list -> Method.text * token list
    8.10  end;
    8.11  
     9.1 --- a/src/Pure/Isar/proof.ML	Thu Sep 23 12:48:49 2004 +0200
     9.2 +++ b/src/Pure/Isar/proof.ML	Mon Sep 27 10:27:34 2004 +0200
     9.3 @@ -92,13 +92,13 @@
     9.4    val invoke_case: string * string option list * context attribute list -> state -> state
     9.5    val multi_theorem: string
     9.6      -> (xstring * (context attribute list * context attribute list list)) option
     9.7 -    -> bstring * theory attribute list -> context attribute Locale.elem_or_expr list
     9.8 +    -> bstring * theory attribute list -> context attribute Locale.element Locale.elem_expr list
     9.9      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
    9.10      -> theory -> state
    9.11    val multi_theorem_i: string
    9.12      -> (string * (context attribute list * context attribute list list)) option
    9.13      -> bstring * theory attribute list
    9.14 -    -> context attribute Locale.elem_or_expr_i list
    9.15 +    -> context attribute Locale.element_i Locale.elem_expr list
    9.16      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    9.17      -> theory -> state
    9.18    val chain: state -> state
    9.19 @@ -154,7 +154,8 @@
    9.20    Theorem of {kind: string,
    9.21      theory_spec: (bstring * theory attribute list) * theory attribute list list,
    9.22      locale_spec: (string * (context attribute list * context attribute list list)) option,
    9.23 -    view: cterm list} |
    9.24 +    view: cterm list * cterm list} |
    9.25 +(* target view and includes view *)
    9.26    Show of context attribute list list |
    9.27    Have of context attribute list list;
    9.28  
    9.29 @@ -766,6 +767,8 @@
    9.30      |> map_context (K locale_ctxt)
    9.31      |> open_block
    9.32      |> map_context (K elems_ctxt)
    9.33 +(* CB: elems_ctxt is an extension of locale_ctxt, see prep_context_statement
    9.34 +   in locale.ML, naming there: ctxt and import_ctxt. *)
    9.35      |> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
    9.36        (Theorem {kind = kind,
    9.37          theory_spec = (a, map (snd o fst) concl),
    9.38 @@ -871,19 +874,23 @@
    9.39      val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
    9.40      val locale_ctxt = context_of (state |> close_block);
    9.41      val theory_ctxt = context_of (state |> close_block |> close_block);
    9.42 -    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view} =
    9.43 +    val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view = (target_view, elems_view)} =
    9.44        (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
    9.45  
    9.46      val ts = flat tss;
    9.47 -    val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt)
    9.48 +val _ = set show_hyps;
    9.49 +val _ = PolyML.print "finish_global";
    9.50 +val _ = PolyML.print "ts:";
    9.51 +val _ = PolyML.print ts;
    9.52 +val _ = PolyML.print "raw_thm:";
    9.53 +val _ = PolyML.print raw_thm;
    9.54 +val _ = PolyML.print "elems_view";
    9.55 +val _ = PolyML.print elems_view;
    9.56 +    val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
    9.57        (prep_result state ts raw_thm);
    9.58  
    9.59 -    val locale_results' = map
    9.60 -      (Locale.prune_prems (ProofContext.theory_of locale_ctxt))
    9.61 -      locale_results;
    9.62 -
    9.63      val results = map (Drule.strip_shyps_warning o
    9.64 -      ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results';
    9.65 +      ProofContext.export_standard target_view locale_ctxt theory_ctxt) locale_results;
    9.66  
    9.67      val (theory', results') =
    9.68        theory_of state
    9.69 @@ -891,7 +898,7 @@
    9.70          if length names <> length loc_attss then
    9.71            raise THEORY ("Bad number of locale attributes", [thy])
    9.72          else (thy, locale_ctxt)
    9.73 -          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results') ~~ loc_attss)
    9.74 +          |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
    9.75            |> (fn ((thy', ctxt'), res) =>
    9.76              if name = "" andalso null loc_atts then thy'
    9.77              else (thy', ctxt')