src/Pure/Isar/locale.ML
author haftmann
Tue, 03 Jan 2006 11:32:16 +0100
changeset 18550 59b89f625d68
parent 18546 d9b026de8333
child 18569 cf0edebe540c
permissions -rw-r--r--
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
     1
(*  Title:      Pure/Isar/locale.ML
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
     3
    Author:     Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
     4
12058
cc182b43dd55 fixes: optional typ;
wenzelm
parents: 12046
diff changeset
     5
Locales -- Isar proof contexts as meta-level predicates, with local
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     6
syntax and implicit structures.
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     7
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
     8
Draws some basic ideas from Florian Kammueller's original version of
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
     9
locales, but uses the richer infrastructure of Isar instead of the raw
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
    10
meta-logic.  Furthermore, we provide structured import of contexts
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
    11
(with merge and rename operations), as well as type-inference of the
13375
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
    12
signature parts, and predicate definitions of the specification text.
14446
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    13
17437
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    14
Interpretation enables the reuse of theorems of locales in other
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    15
contexts, namely those defined by theories, structured proofs and
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    16
locales themselves.
9deaf32c83be interpretation uses primitive goal interface
ballarin
parents: 17412
diff changeset
    17
14446
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    18
See also:
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    19
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    20
[1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
0bc2519e9990 *** empty log message ***
ballarin
parents: 14291
diff changeset
    21
    In Stefano Berardi et al., Types for Proofs and Programs: International
15099
6d8619440ea0 Some comments added.
ballarin
parents: 14981
diff changeset
    22
    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    23
*)
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    24
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    25
(* TODO:
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    26
- beta-eta normalisation of interpretation parameters
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    27
- dangling type frees in locales
16620
2a7f46324218 Proper treatment of beta-redexes in witness theorems.
ballarin
parents: 16458
diff changeset
    28
- test subsumption of interpretations when merging theories
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
    29
- var vs. fixes in locale to be interpreted (interpretation in locale)
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
    30
  (implicit locale expressions generated by multiple registrations)
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    31
*)
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
    32
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    33
signature LOCALE =
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
    34
sig
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    35
  datatype expr =
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    36
    Locale of string |
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
    37
    Rename of expr * (string * mixfix option) option list |
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    38
    Merge of expr list
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
    39
  val empty: expr
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    40
  datatype 'a element = Elem of 'a | Expr of expr
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    41
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    42
  (* Abstract interface to locales *)
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
    43
  type locale
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
    44
  val intern: theory -> xstring -> string
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
    45
  val extern: theory -> string -> xstring
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
    46
  val the_locale: theory -> string -> locale
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    47
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    48
  (* Processing of locale statements *)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    49
  val read_context_statement: xstring option -> Element.context element list ->
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    50
    (string * (string list * string list)) list list -> ProofContext.context ->
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    51
    string option * (cterm list * cterm list) * ProofContext.context * ProofContext.context *
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    52
      (term * (term list * term list)) list list
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    53
  val cert_context_statement: string option -> Element.context_i element list ->
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    54
    (term * (term list * term list)) list list -> ProofContext.context ->
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    55
    string option * (cterm list * cterm list) * ProofContext.context * ProofContext.context *
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
    56
      (term * (term list * term list)) list list
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    57
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    58
  (* Diagnostic functions *)
12758
f6aceb9d4b8e print_locale: allow full body specification;
wenzelm
parents: 12730
diff changeset
    59
  val print_locales: theory -> unit
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    60
  val print_locale: theory -> bool -> expr -> Element.context list -> unit
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
    61
  val print_global_registrations: bool -> string -> theory -> unit
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    62
  val print_local_registrations': bool -> string -> ProofContext.context -> unit
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    63
  val print_local_registrations: bool -> string -> ProofContext.context -> unit
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    64
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    65
  val add_locale_context: bool -> bstring -> expr -> Element.context list -> theory
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
    66
    -> ((Element.context_i list list * Element.context_i list list)
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
    67
         * ProofContext.context) * theory
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    68
  val add_locale_context_i: bool -> bstring -> expr -> Element.context_i list -> theory
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
    69
    -> ((Element.context_i list list * Element.context_i list list)
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
    70
         * ProofContext.context) * theory
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    71
  val add_locale: bool -> bstring -> expr -> Element.context list -> theory -> theory
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    72
  val add_locale_i: bool -> bstring -> expr -> Element.context_i list -> theory -> theory
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
    73
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
    74
  (* Storing results *)
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
    75
  val smart_note_thmss: string -> string option ->
12958
99f5c4a37b29 added smart_have_thmss (global storage);
wenzelm
parents: 12862
diff changeset
    76
    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
18421
464c93701351 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
    77
    theory -> (bstring * thm list) list * theory
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
    78
  val note_thmss: string -> xstring ->
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
    79
    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list ->
18421
464c93701351 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
    80
    theory -> (bstring * thm list) list * (theory * ProofContext.context)
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
    81
  val note_thmss_i: string -> string ->
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
    82
    ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
18421
464c93701351 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents: 18377
diff changeset
    83
    theory -> (bstring * thm list) list * (theory * ProofContext.context)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    84
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
    85
  val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    86
    string * Attrib.src list -> Element.context element list ->
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    87
    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    88
    theory -> Proof.state
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
    89
  val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    90
    string * theory attribute list -> Element.context_i element list ->
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    91
    ((string * theory attribute list) * (term * (term list * term list)) list) list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    92
    theory -> Proof.state
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
    93
  val theorem_in_locale: string -> Method.text option ->
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
    94
    (thm list list -> thm list list -> theory -> theory) ->
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
    95
    xstring -> string * Attrib.src list -> Element.context element list ->
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    96
    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
    97
    theory -> Proof.state
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
    98
  val theorem_in_locale_i: string -> Method.text option ->
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
    99
    (thm list list -> thm list list -> theory -> theory) ->
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   100
    string -> string * Attrib.src list -> Element.context_i element list ->
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   101
    ((string * Attrib.src list) * (term * (term list * term list)) list) list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   102
    theory -> Proof.state
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   103
  val smart_theorem: string -> xstring option ->
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   104
    string * Attrib.src list -> Element.context element list ->
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   105
    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   106
    theory -> Proof.state
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   107
  val interpretation: string * Attrib.src list -> expr -> string option list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   108
    theory -> Proof.state
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   109
  val interpretation_in_locale: xstring * expr -> theory -> Proof.state
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   110
  val interpret: string * Attrib.src list -> expr -> string option list ->
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   111
    bool -> Proof.state -> Proof.state
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   112
end;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   113
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   114
structure Locale: LOCALE =
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   115
struct
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   116
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   117
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   118
(** locale elements and expressions **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   119
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   120
datatype ctxt = datatype Element.ctxt;
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   121
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   122
datatype expr =
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   123
  Locale of string |
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   124
  Rename of expr * (string * mixfix option) option list |
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   125
  Merge of expr list;
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   126
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   127
val empty = Merge [];
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   128
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   129
datatype 'a element =
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   130
  Elem of 'a | Expr of expr;
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   131
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   132
fun map_elem f (Elem e) = Elem (f e)
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   133
  | map_elem _ (Expr e) = Expr e;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   134
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   135
type witness = term * thm;  (*hypothesis as fact*)
12070
c72fe1edc9e7 proper treatment of local syntax;
wenzelm
parents: 12063
diff changeset
   136
type locale =
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   137
 {predicate: cterm list * witness list,
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   138
    (* CB: For locales with "(open)" this entry is ([], []).
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   139
       For new-style locales, which declare predicates, if the locale declares
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   140
       no predicates, this is also ([], []).
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   141
       If the locale declares predicates, the record field is
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   142
       ([statement], axioms), where statement is the locale predicate applied
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   143
       to the (assumed) locale parameters.  Axioms contains the projections
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   144
       from the locale predicate to the normalised assumptions of the locale
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   145
       (cf. [1], normalisation of locale expressions.)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   146
    *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   147
  import: expr,                                       (*dynamic import*)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   148
  elems: (Element.context_i * stamp) list,            (*static content*)
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   149
  params: ((string * typ) * mixfix option) list * string list,
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   150
                                                      (*all/local params*)
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   151
  regs: ((string * string list) * (term * thm) list) list}
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   152
    (* Registrations: indentifiers and witness theorems of locales interpreted
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   153
       in the locale.
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   154
    *)
12063
4c16bdee47d4 added add_locale(_i) and store_thm;
wenzelm
parents: 12058
diff changeset
   155
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   156
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   157
(* CB: an internal (Int) locale element was either imported or included,
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   158
   an external (Ext) element appears directly in the locale text. *)
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   159
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   160
datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   161
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   162
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   163
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   164
(** management of registrations in theories and proof contexts **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   165
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   166
structure Registrations :
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   167
  sig
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   168
    type T
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   169
    val empty: T
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   170
    val join: T * T -> T
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   171
    val dest: T -> (term list * ((string * Attrib.src list) * witness list)) list
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   172
    val lookup: theory -> T * term list ->
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   173
      ((string * Attrib.src list) * witness list) option
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   174
    val insert: theory -> term list * (string * Attrib.src list) -> T ->
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   175
      T * (term list * ((string * Attrib.src list) * witness list)) list
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   176
    val add_witness: term list -> witness -> T -> T
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   177
  end =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   178
struct
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   179
  (* a registration consists of theorems instantiating locale assumptions
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   180
     and prefix and attributes, indexed by parameter instantiation *)
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   181
  type T = ((string * Attrib.src list) * witness list) Termtab.table;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   182
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   183
  val empty = Termtab.empty;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   184
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   185
  (* term list represented as single term, for simultaneous matching *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   186
  fun termify ts =
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   187
    Term.list_comb (Const ("", map fastype_of ts ---> propT), ts);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   188
  fun untermify t =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   189
    let fun ut (Const _) ts = ts
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   190
          | ut (s $ t) ts = ut s (t::ts)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   191
    in ut t [] end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   192
16620
2a7f46324218 Proper treatment of beta-redexes in witness theorems.
ballarin
parents: 16458
diff changeset
   193
  (* joining of registrations: prefix and attributes of left theory,
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   194
     thms are equal, no attempt to subsumption testing *)
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   195
  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   196
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   197
  fun dest regs = map (apfst untermify) (Termtab.dest regs);
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   198
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   199
  (* registrations that subsume t *)
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   200
  fun subsumers thy t regs =
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   201
    List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   202
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   203
  (* look up registration, pick one that subsumes the query *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   204
  fun lookup sign (regs, ts) =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   205
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   206
      val t = termify ts;
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   207
      val subs = subsumers sign t regs;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   208
    in (case subs of
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   209
        [] => NONE
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   210
      | ((t', (attn, thms)) :: _) => let
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   211
            val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   212
            (* thms contain Frees, not Vars *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   213
            val tinst' = tinst |> Vartab.dest
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   214
                 |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   215
                 |> Symtab.make;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   216
            val inst' = inst |> Vartab.dest
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   217
                 |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   218
                 |> Symtab.make;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   219
          in
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   220
            SOME (attn, map (fn (t, th) =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   221
             (Element.inst_term (tinst', inst') t,
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   222
              Element.inst_thm sign (tinst', inst') th)) thms)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   223
          end)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   224
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   225
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   226
  (* add registration if not subsumed by ones already present,
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   227
     additionally returns registrations that are strictly subsumed *)
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   228
  fun insert sign (ts, attn) regs =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   229
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   230
      val t = termify ts;
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   231
      val subs = subsumers sign t regs ;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   232
    in (case subs of
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   233
        [] => let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   234
                val sups =
17203
29b2563f5c11 refer to theory instead of low-level tsig;
wenzelm
parents: 17142
diff changeset
   235
                  List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   236
                val sups' = map (apfst untermify) sups
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   237
              in (Termtab.update (t, (attn, [])) regs, sups') end
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   238
      | _ => (regs, []))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   239
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   240
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   241
  (* add witness theorem to registration,
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   242
     only if instantiation is exact, otherwise exception Option raised *)
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   243
  fun add_witness ts thm regs =
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   244
    let
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   245
      val t = termify ts;
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   246
      val (x, thms) = the (Termtab.lookup regs t);
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   247
    in
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   248
      Termtab.update (t, (x, thm::thms)) regs
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   249
    end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   250
end;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   251
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   252
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   253
(** theory data **)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   254
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   255
structure GlobalLocalesData = TheoryDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   256
(struct
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   257
  val name = "Isar/locales";
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   258
  type T = NameSpace.T * locale Symtab.table * Registrations.T Symtab.table;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   259
    (* 1st entry: locale namespace,
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   260
       2nd entry: locales of the theory,
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   261
       3rd entry: registrations, indexed by locale name *)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   262
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   263
  val empty = (NameSpace.empty, Symtab.empty, Symtab.empty);
12063
4c16bdee47d4 added add_locale(_i) and store_thm;
wenzelm
parents: 12058
diff changeset
   264
  val copy = I;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   265
  val extend = I;
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   266
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   267
  fun join_locs _ ({predicate, import, elems, params, regs}: locale,
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   268
      {elems = elems', regs = regs', ...}: locale) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   269
    SOME {predicate = predicate, import = import,
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   270
      elems = gen_merge_lists (eq_snd (op =)) elems elems',
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   271
      params = params,
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   272
      regs = merge_alists regs regs'};
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   273
  fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   274
    (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   275
     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   276
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   277
  fun print _ (space, locs, _) =
16346
baa7b5324fc1 NameSpace.extern_table;
wenzelm
parents: 16325
diff changeset
   278
    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   279
    |> Pretty.writeln;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   280
end);
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   281
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   282
val _ = Context.add_setup [GlobalLocalesData.init];
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   283
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   284
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   285
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   286
(** context data **)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   287
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   288
structure LocalLocalesData = ProofDataFun
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   289
(struct
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   290
  val name = "Isar/locales";
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   291
  type T = Registrations.T Symtab.table;
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   292
    (* registrations, indexed by locale name *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   293
  fun init _ = Symtab.empty;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   294
  fun print _ _ = ();
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   295
end);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   296
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15798
diff changeset
   297
val _ = Context.add_setup [LocalLocalesData.init];
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   298
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   299
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   300
(* access locales *)
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   301
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   302
val print_locales = GlobalLocalesData.print;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   303
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   304
val intern = NameSpace.intern o #1 o GlobalLocalesData.get;
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   305
val extern = NameSpace.extern o #1 o GlobalLocalesData.get;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   306
16144
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   307
fun declare_locale name thy =
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   308
  thy |> GlobalLocalesData.map (fn (space, locs, regs) =>
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   309
    (Sign.declare_name thy name space, locs, regs));
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   310
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   311
fun put_locale name loc =
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   312
  GlobalLocalesData.map (fn (space, locs, regs) =>
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   313
    (space, Symtab.update (name, loc) locs, regs));
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   314
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   315
fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy)) name;
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   316
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   317
fun the_locale thy name =
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   318
  (case get_locale thy name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   319
    SOME loc => loc
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   320
  | NONE => error ("Unknown locale " ^ quote name));
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   321
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   322
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   323
(* access registrations *)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   324
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   325
(* Ids of global registrations are varified,
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   326
   Ids of local registrations are not.
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   327
   Thms of registrations are never varified. *)
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   328
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   329
(* retrieve registration from theory or context *)
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   330
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   331
fun gen_get_registrations get thy_ctxt name =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   332
  case Symtab.lookup (get thy_ctxt) name of
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   333
      NONE => []
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   334
    | SOME reg => Registrations.dest reg;
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   335
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   336
val get_global_registrations =
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   337
     gen_get_registrations (#3 o GlobalLocalesData.get);
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   338
val get_local_registrations =
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   339
     gen_get_registrations LocalLocalesData.get;
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   340
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   341
fun gen_get_registration get thy_of thy_ctxt (name, ps) =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   342
  case Symtab.lookup (get thy_ctxt) name of
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   343
      NONE => NONE
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   344
    | SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   345
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   346
val get_global_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   347
     gen_get_registration (#3 o GlobalLocalesData.get) I;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   348
val get_local_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   349
     gen_get_registration LocalLocalesData.get ProofContext.theory_of;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   350
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   351
val test_global_registration = is_some oo get_global_registration;
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   352
val test_local_registration = is_some oo get_local_registration;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   353
fun smart_test_registration ctxt id =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   354
  let
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   355
    val thy = ProofContext.theory_of ctxt;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   356
  in
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   357
    test_global_registration thy id orelse test_local_registration ctxt id
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   358
  end;
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   359
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   360
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   361
(* add registration to theory or context, ignored if subsumed *)
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   362
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   363
fun gen_put_registration map_data thy_of (name, ps) attn thy_ctxt =
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   364
  map_data (fn regs =>
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   365
    let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   366
      val thy = thy_of thy_ctxt;
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   367
      val reg = the_default Registrations.empty (Symtab.lookup regs name);
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   368
      val (reg', sups) = Registrations.insert thy (ps, attn) reg;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   369
      val _ = if not (null sups) then warning
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   370
                ("Subsumed interpretation(s) of locale " ^
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   371
                 quote (extern thy name) ^
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   372
                 "\nby interpretation(s) with the following prefix(es):\n" ^
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   373
                  commas_quote (map (fn (_, ((s, _), _)) => s) sups))
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   374
              else ();
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   375
    in Symtab.update (name, reg') regs end) thy_ctxt;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   376
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   377
val put_global_registration =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   378
     gen_put_registration (fn f =>
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   379
       GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, f regs))) I;
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   380
val put_local_registration =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   381
     gen_put_registration LocalLocalesData.map ProofContext.theory_of;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   382
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   383
fun put_registration_in_locale name id thy =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   384
    let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   385
      val {predicate, import, elems, params, regs} = the_locale thy name;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   386
    in
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   387
      put_locale name {predicate = predicate, import = import,
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   388
        elems = elems, params = params, regs = regs @ [(id, [])]} thy
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   389
    end;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   390
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   391
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   392
(* add witness theorem to registration in theory or context,
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   393
   ignored if registration not present *)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   394
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   395
fun add_witness (name, ps) thm =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   396
  Symtab.map_entry name (Registrations.add_witness ps thm);
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   397
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   398
fun add_global_witness id thm =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   399
  GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   400
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   401
val add_local_witness = LocalLocalesData.map oo add_witness;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   402
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   403
fun add_witness_in_locale name id thm thy =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   404
    let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   405
      val {predicate, import, elems, params, regs} = the_locale thy name;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   406
      fun add (id', thms) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   407
          if id = id' then (id', thm :: thms) else (id', thms);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   408
    in
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   409
      put_locale name {predicate = predicate, import = import,
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   410
        elems = elems, params = params, regs = map add regs} thy
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   411
    end;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   412
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   413
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   414
(* printing of registrations *)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   415
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   416
fun gen_print_registrations get_regs mk_ctxt msg show_wits loc thy_ctxt =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   417
  let
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   418
    val ctxt = mk_ctxt thy_ctxt;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   419
    val thy = ProofContext.theory_of ctxt;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   420
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   421
    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   422
    fun prt_inst ts =
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   423
        Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   424
    fun prt_attn (prfx, atts) =
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   425
        Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   426
    fun prt_thm (_, th) = Pretty.quote (ProofContext.pretty_thm ctxt th);
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   427
    fun prt_thms thms =
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   428
        Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms));
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   429
    fun prt_reg (ts, (("", []), thms)) =
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   430
        if show_wits
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   431
          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms]
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   432
          else prt_inst ts
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   433
      | prt_reg (ts, (attn, thms)) =
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   434
        if show_wits
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   435
          then Pretty.block ((prt_attn attn @
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   436
            [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   437
              prt_thms thms]))
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   438
          else Pretty.block ((prt_attn attn @
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   439
            [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   440
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   441
    val loc_int = intern thy loc;
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   442
    val regs = get_regs thy_ctxt;
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17384
diff changeset
   443
    val loc_regs = Symtab.lookup regs loc_int;
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   444
  in
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   445
    (case loc_regs of
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   446
        NONE => Pretty.str ("no interpretations in " ^ msg)
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   447
      | SOME r => let
15837
7a567dcd4cda Subsumption of locale interpretations.
ballarin
parents: 15801
diff changeset
   448
            val r' = Registrations.dest r;
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   449
            val r'' = Library.sort_wrt (fn (_, ((prfx, _), _)) => prfx) r';
17355
5b31131c0365 load late, after proof.ML;
wenzelm
parents: 17316
diff changeset
   450
          in Pretty.big_list ("interpretations in " ^ msg ^ ":")
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   451
            (map prt_reg r'')
15763
b901a127ac73 Interpretation supports statically scoped attributes; documentation.
ballarin
parents: 15749
diff changeset
   452
          end)
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   453
    |> Pretty.writeln
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   454
  end;
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   455
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   456
val print_global_registrations =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   457
     gen_print_registrations (#3 o GlobalLocalesData.get)
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   458
       ProofContext.init "theory";
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   459
val print_local_registrations' =
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   460
     gen_print_registrations LocalLocalesData.get
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   461
       I "context";
17138
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   462
fun print_local_registrations show_wits loc ctxt =
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   463
  (print_global_registrations show_wits loc (ProofContext.theory_of ctxt);
ad4c98fd367b Interpretation in locales: extended back end;
ballarin
parents: 17109
diff changeset
   464
   print_local_registrations' show_wits loc ctxt);
15624
484178635bd8 Further work on interpretation commands. New command `interpret' for
ballarin
parents: 15623
diff changeset
   465
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   466
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   467
(* diagnostics *)
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   468
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   469
fun err_in_locale ctxt msg ids =
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   470
  let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   471
    val thy = ProofContext.theory_of ctxt;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   472
    fun prt_id (name, parms) =
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   473
      [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   474
    val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   475
    val err_msg =
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   476
      if forall (equal "" o #1) ids then msg
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   477
      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   478
        (Pretty.str "The error(s) above occurred in locale:" :: Pretty.brk 1 :: prt_ids));
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   479
  in raise ProofContext.CONTEXT (err_msg, ctxt) end;
12063
4c16bdee47d4 added add_locale(_i) and store_thm;
wenzelm
parents: 12058
diff changeset
   480
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   481
fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
12277
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   482
2b28d7dd91f5 improved ordering of evaluated elements;
wenzelm
parents: 12273
diff changeset
   483
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   484
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   485
(** witnesses -- protected facts **)
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   486
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   487
fun assume_protected thy t =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   488
  (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   489
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   490
fun prove_protected thy t tac =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   491
  (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   492
    Tactic.rtac Drule.protectI 1 THEN tac));
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   493
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   494
val conclude_protected = Goal.conclude #> Goal.norm_hhf;
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   495
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   496
fun satisfy_protected pths thm =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   497
  let
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   498
    fun satisfy chyp =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   499
      (case find_first (fn (t, _) => Thm.term_of chyp aconv t) pths of
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   500
        NONE => I
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   501
      | SOME (_, th) => Drule.implies_intr_protected [chyp] #> Goal.comp_hhf th);
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   502
  in fold satisfy (#hyps (Thm.crep_thm thm)) thm end;
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   503
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   504
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   505
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   506
(** structured contexts: rename + merge + implicit type instantiation **)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   507
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   508
(* parameter types *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   509
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   510
fun frozen_tvars ctxt Ts =
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   511
  let
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
   512
    val tvars = rev (fold Term.add_tvarsT Ts []);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   513
    val tfrees = map TFree
14695
9c78044b99c3 improved Term.invent_names;
wenzelm
parents: 14643
diff changeset
   514
      (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   515
  in map (fn ((xi, S), T) => (xi, (S, T))) (tvars ~~ tfrees) end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   516
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   517
fun unify_frozen ctxt maxidx Ts Us =
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   518
  let
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   519
    fun paramify NONE i = (NONE, i)
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   520
      | paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   521
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   522
    val (Ts', maxidx') = fold_map paramify Ts maxidx;
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   523
    val (Us', maxidx'') = fold_map paramify Us maxidx';
16947
c6a90f04924e Sign.typ_unify;
wenzelm
parents: 16861
diff changeset
   524
    val thy = ProofContext.theory_of ctxt;
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   525
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   526
    fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   527
          handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   528
      | unify _ env = env;
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
   529
    val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   530
    val Vs = map (Option.map (Envir.norm_type unifier)) Us';
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   531
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   532
  in map (Option.map (Envir.norm_type unifier')) Vs end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   533
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   534
fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   535
fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   536
fun params_syn_of syn elemss =
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   537
  gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   538
    map (apfst (fn x => (x, the (Symtab.lookup syn x))));
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   539
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   540
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   541
(* CB: param_types has the following type:
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   542
  ('a * 'b option) list -> ('a * 'b) list *)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   543
fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   544
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   545
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   546
fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   547
  handle Symtab.DUPS xs => err_in_locale ctxt
16105
a44801c499cb SML/NJ compatibility.
ballarin
parents: 16103
diff changeset
   548
    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   549
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   550
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   551
(* Distinction of assumed vs. derived identifiers.
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   552
   The former may have axioms relating assumptions of the context to
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   553
   assumptions of the specification fragment (for locales with
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   554
   predicates).  The latter have witness theorems relating assumptions of the
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   555
   specification fragment to assumptions of other (assumed) specification
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   556
   fragments. *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   557
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   558
datatype 'a mode = Assumed of 'a | Derived of 'a;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   559
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   560
fun map_mode f (Assumed x) = Assumed (f x)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   561
  | map_mode f (Derived x) = Derived (f x);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   562
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   563
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   564
(* flatten expressions *)
11896
1ff33f896720 moved locale.ML to Isar/locale.ML;
wenzelm
parents:
diff changeset
   565
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   566
local
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   567
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   568
fun unique_parms ctxt elemss =
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   569
  let
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   570
    val param_decls =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   571
      List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   572
      |> Symtab.make_multi |> Symtab.dest;
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   573
  in
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   574
    (case find_first (fn (_, ids) => length ids > 1) param_decls of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   575
      SOME (q, ids) => err_in_locale ctxt ("Multiple declaration of parameter " ^ quote q)
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   576
          (map (apsnd (map fst)) ids)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   577
    | NONE => map (apfst (apfst (apsnd #1))) elemss)
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   578
  end;
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   579
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   580
fun unify_parms ctxt fixed_parms raw_parmss =
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   581
  let
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   582
    val thy = ProofContext.theory_of ctxt;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   583
    val maxidx = length raw_parmss;
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   584
    val idx_parmss = (0 upto maxidx - 1) ~~ raw_parmss;
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   585
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   586
    fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   587
    fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   588
    val parms = fixed_parms @ List.concat (map varify_parms idx_parmss);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   589
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   590
    fun unify T U envir = Sign.typ_unify thy (U, T) envir
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   591
      handle Type.TUNIFY =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   592
        let val prt = Sign.string_of_typ thy in
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   593
          raise TYPE ("unify_parms: failed to unify types " ^
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   594
            prt U ^ " and " ^ prt T, [U, T], [])
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   595
        end;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   596
    fun unify_list (T :: Us) = fold (unify T) Us
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   597
      | unify_list [] = I;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   598
    val (unifier, _) = fold unify_list (map #2 (Symtab.dest (Symtab.make_multi parms)))
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   599
      (Vartab.empty, maxidx);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   600
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   601
    val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   602
    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   603
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   604
    fun inst_parms (i, ps) =
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   605
      foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   606
      |> List.mapPartial (fn (a, S) =>
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   607
          let val T = Envir.norm_type unifier' (TVar ((a, i), S))
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   608
          in if T = TFree (a, S) then NONE else SOME (a, T) end)
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   609
      |> Symtab.make;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   610
  in map inst_parms idx_parmss end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   611
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   612
in
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   613
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   614
fun unify_elemss _ _ [] = []
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   615
  | unify_elemss _ [] [elems] = [elems]
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   616
  | unify_elemss ctxt fixed_parms elemss =
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   617
      let
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   618
        val thy = ProofContext.theory_of ctxt;
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17496
diff changeset
   619
        val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   620
        fun inst ((((name, ps), mode), elems), env) =
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   621
          (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   622
              map_mode (map (fn (t, th) =>
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   623
                (Element.instT_term env t, Element.instT_thm thy env th))) mode),
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   624
            map (Element.instT_ctxt thy env) elems);
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   625
      in map inst (elemss ~~ envs) end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   626
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   627
(* like unify_elemss, but does not touch mode, additional
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
   628
   parameter c_parms for enforcing further constraints (eg. syntax) *)
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   629
(* FIXME avoid code duplication *)
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   630
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   631
fun unify_elemss' _ _ [] [] = []
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   632
  | unify_elemss' _ [] [elems] [] = [elems]
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   633
  | unify_elemss' ctxt fixed_parms elemss c_parms =
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   634
      let
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   635
        val thy = ProofContext.theory_of ctxt;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   636
        val envs =
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   637
          unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms);
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   638
        fun inst ((((name, ps), (ps', mode)), elems), env) =
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   639
          (((name, map (apsnd (Option.map (Element.instT_type env))) ps), (ps', mode)),
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   640
           map (Element.instT_ctxt thy env) elems);
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   641
      in map inst (elemss ~~ Library.take (length elemss, envs)) end;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   642
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   643
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   644
(* flatten_expr:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   645
   Extend list of identifiers by those new in locale expression expr.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   646
   Compute corresponding list of lists of locale elements (one entry per
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   647
   identifier).
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   648
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   649
   Identifiers represent locale fragments and are in an extended form:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   650
     ((name, ps), (ax_ps, axs))
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   651
   (name, ps) is the locale name with all its parameters.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   652
   (ax_ps, axs) is the locale axioms with its parameters;
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   653
     axs are always taken from the top level of the locale hierarchy,
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   654
     hence axioms may contain additional parameters from later fragments:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   655
     ps subset of ax_ps.  axs is either singleton or empty.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   656
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   657
   Elements are enriched by identifier-like information:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   658
     (((name, ax_ps), axs), elems)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   659
   The parameters in ax_ps are the axiom parameters, but enriched by type
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   660
   info: now each entry is a pair of string and typ option.  Axioms are
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   661
   type-instantiated.
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   662
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   663
*)
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   664
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   665
fun flatten_expr ctxt ((prev_idents, prev_syntax), expr) =
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   666
  let
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   667
    val thy = ProofContext.theory_of ctxt;
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   668
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   669
    fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
   670
      | renaming (NONE :: xs) (y :: ys) = renaming xs ys
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   671
      | renaming [] _ = []
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   672
      | renaming xs [] = raise ERROR_MESSAGE ("Too many arguments in renaming: " ^
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   673
          commas (map (fn NONE => "_" | SOME x => quote (fst x)) xs));
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   674
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   675
    fun rename_parms top ren ((name, ps), (parms, mode)) =
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   676
      let val ps' = map (Element.rename ren) ps in
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   677
        (case duplicates ps' of
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   678
          [] => ((name, ps'),
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   679
                 if top then (map (Element.rename ren) parms,
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   680
                   map_mode (map (fn (t, th) =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   681
                     (Element.rename_term ren t, Element.rename_thm ren th))) mode)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   682
                 else (parms, mode))
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   683
        | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   684
      end;
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   685
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   686
    (* add registrations of (name, ps), recursively;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   687
       adjust hyps of witness theorems *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   688
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   689
    fun add_regs (name, ps) (ths, ids) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   690
        let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   691
          val {params, regs, ...} = the_locale thy name;
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   692
          val ps' = map #1 (#1 params);
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   693
          val ren = map #1 ps' ~~ map (fn (x, _) => (x, NONE)) ps;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   694
            (* dummy syntax, since required by rename *)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   695
          val ps'' = map (fn ((p, _), (_, T)) => (p, T)) (ps ~~ ps');
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   696
          val [env] = unify_parms ctxt ps [map (apsnd SOME) ps''];
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   697
            (* propagate parameter types, to keep them consistent *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   698
          val regs' = map (fn ((name, ps), ths) =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   699
              ((name, map (Element.rename ren) ps), ths)) regs;
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   700
          val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   701
          val new_ids = map fst new_regs;
17485
c39871c52977 introduced AList module
haftmann
parents: 17449
diff changeset
   702
          val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   703
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   704
          val new_ths = new_regs |> map (fn (_, ths') => ths' |> map (fn (t, th) =>
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   705
           (t |> Element.instT_term env |> Element.rename_term ren,
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   706
            th |> Element.instT_thm thy env |> Element.rename_thm ren |> satisfy_protected ths)));
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   707
          val new_ids' = map (fn (id, ths) =>
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   708
              (id, ([], Derived ths))) (new_ids ~~ new_ths);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   709
        in
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   710
          fold add_regs new_idTs (ths @ List.concat new_ths, ids @ new_ids')
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   711
        end;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   712
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   713
    (* distribute top-level axioms over assumed ids *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   714
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   715
    fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   716
        let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   717
          val {elems, ...} = the_locale thy name;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   718
          val ts = List.concat (map
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   719
            (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   720
              | _ => [])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   721
            elems);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   722
          val (axs1, axs2) = splitAt (length ts, axioms);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   723
        in (((name, parms), (all_ps, Assumed axs1)), axs2) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   724
      | axiomify all_ps (id, (_, Derived ths)) axioms =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   725
          ((id, (all_ps, Derived ths)), axioms);
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   726
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   727
    (* identifiers of an expression *)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   728
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   729
    fun identify top (Locale name) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   730
    (* CB: ids_ax is a list of tuples of the form ((name, ps), axs),
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   731
       where name is a locale name, ps a list of parameter names and axs
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   732
       a list of axioms relating to the identifier, axs is empty unless
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   733
       identify at top level (top = true);
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
   734
       parms is accumulated list of parameters *)
12289
ec2dafd0a6a9 clarified locale operations (rename, merge);
wenzelm
parents: 12277
diff changeset
   735
          let
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   736
            val {predicate = (_, axioms), import, params, ...} =
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   737
              the_locale thy name;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   738
            val ps = map (#1 o #1) (#1 params);
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   739
            val (ids', parms', _) = identify false import;
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   740
                (* acyclic import dependencies *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   741
            val ids'' = ids' @ [((name, ps), ([], Assumed []))];
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   742
            val (_, ids''') = add_regs (name, map #1 (#1 params)) ([], ids'');
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   743
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   744
            val ids_ax = if top then fst
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   745
                 (fold_map (axiomify ps) ids''' axioms)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   746
              else ids''';
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   747
            val syn = Symtab.make (map (apfst fst) (#1 params));
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   748
            in (ids_ax, merge_lists parms' ps, syn) end
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   749
      | identify top (Rename (e, xs)) =
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   750
          let
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   751
            val (ids', parms', syn') = identify top e;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   752
            val ren = renaming xs parms'
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   753
              handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   754
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   755
            val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   756
            val parms'' = distinct (List.concat (map (#2 o #1) ids''));
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   757
            val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   758
            (* check for conflicting syntax? *)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   759
          in (ids'', parms'', syn'') end
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   760
      | identify top (Merge es) =
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   761
          fold (fn e => fn (ids, parms, syn) =>
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   762
                   let
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   763
                     val (ids', parms', syn') = identify top e
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   764
                   in
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   765
                     (merge_alists ids ids',
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   766
                      merge_lists parms parms',
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   767
                      merge_syntax ctxt ids' (syn, syn'))
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   768
                   end)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   769
            es ([], [], Symtab.empty);
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   770
12014
035ab884b9e0 beginnings of new locales (not yet functional);
wenzelm
parents: 11896
diff changeset
   771
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   772
    (* CB: enrich identifiers by parameter types and
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   773
       the corresponding elements (with renamed parameters),
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   774
       also takes care of parameter syntax *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   775
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   776
    fun eval syn ((name, xs), axs) =
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   777
      let
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
   778
        val {params = (ps, qs), elems, ...} = the_locale thy name;
16620
2a7f46324218 Proper treatment of beta-redexes in witness theorems.
ballarin
parents: 16458
diff changeset
   779
        val ps' = map (apsnd SOME o #1) ps;
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   780
        val ren = map #1 ps' ~~
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   781
              map (fn x => (x, the (Symtab.lookup syn x))) xs;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
   782
        val (params', elems') =
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   783
          if null ren then ((ps', qs), map #1 elems)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   784
          else ((map (apfst (Element.rename ren)) ps', map (Element.rename ren) qs),
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   785
            map (Element.rename_ctxt ren o #1) elems);
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   786
        val elems'' = elems' |> map (Element.map_ctxt
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   787
          {var = I, typ = I, term = I, fact = I, attrib = I,
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   788
            name = NameSpace.qualified (space_implode "_" xs)});
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   789
      in (((name, params'), axs), elems'') end;
12307
459aa05af6be qualify imported facts;
wenzelm
parents: 12289
diff changeset
   790
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   791
    (* type constraint for renamed parameter with syntax *)
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   792
    fun mixfix_type mx =
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   793
      Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0));
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   794
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   795
    (* compute identifiers and syntax, merge with previous ones *)
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
   796
    val (ids, _, syn) = identify true expr;
17496
26535df536ae slight adaptions to library changes
haftmann
parents: 17485
diff changeset
   797
    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   798
    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   799
    (* add types to params, check for unique params and unify them *)
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   800
    val raw_elemss = unique_parms ctxt (map (eval syntax) idents);
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   801
    val elemss = unify_elemss' ctxt [] raw_elemss
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
   802
         (map (apsnd (Option.map mixfix_type)) (Symtab.dest syntax));
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   803
    (* replace params in ids by params from axioms,
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   804
       adjust types in mode *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   805
    val all_params' = params_of' elemss;
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   806
    val all_params = param_types all_params';
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   807
    val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
17485
c39871c52977 introduced AList module
haftmann
parents: 17449
diff changeset
   808
         (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems))
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   809
         elemss;
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   810
    fun inst_th (t, th) = let
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   811
         val {hyps, prop, ...} = Thm.rep_thm th;
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
   812
         val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   813
         val [env] = unify_parms ctxt all_params [ps];
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   814
         val t' = Element.instT_term env t;
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   815
         val th' = Element.instT_thm thy env th;
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   816
       in (t', th') end;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   817
    val final_elemss = map (fn ((id, mode), elems) =>
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   818
         ((id, map_mode (map inst_th) mode), elems)) elemss';
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   819
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   820
  in ((prev_idents @ idents, syntax), final_elemss) end;
12046
a404358fd965 locale elements;
wenzelm
parents: 12014
diff changeset
   821
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   822
end;
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   823
12070
c72fe1edc9e7 proper treatment of local syntax;
wenzelm
parents: 12063
diff changeset
   824
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   825
(* activate elements *)
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
   826
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   827
local
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   828
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   829
fun export_axioms axs _ hyps =
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   830
  satisfy_protected axs
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   831
  #> Drule.implies_intr_list (Library.drop (length axs, hyps))
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   832
  #> Seq.single;
12263
6f2acf10e2a2 locale expressions;
wenzelm
parents: 12143
diff changeset
   833
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   834
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   835
(* NB: derived ids contain only facts at this stage *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   836
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   837
fun activate_elem _ ((ctxt, mode), Fixes fixes) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   838
      ((ctxt |> ProofContext.add_fixes fixes, mode), [])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   839
  | activate_elem _ ((ctxt, mode), Constrains _) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   840
      ((ctxt, mode), [])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   841
  | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   842
      let
17109
606c269d1e26 added add_locale_context(_i), which returns the body context for presentation;
wenzelm
parents: 17096
diff changeset
   843
        val asms' = Attrib.map_specs (Attrib.context_attribute_i ctxt) asms;
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   844
        val ts = List.concat (map (map #1 o #2) asms');
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   845
        val (ps, qs) = splitAt (length ts, axs);
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   846
        val (_, ctxt') =
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   847
          ctxt |> ProofContext.fix_frees ts
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   848
          |> ProofContext.assume_i (export_axioms ps) asms';
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   849
      in ((ctxt', Assumed qs), []) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   850
  | activate_elem _ ((ctxt, Derived ths), Assumes asms) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   851
      ((ctxt, Derived ths), [])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   852
  | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   853
      let
17109
606c269d1e26 added add_locale_context(_i), which returns the body context for presentation;
wenzelm
parents: 17096
diff changeset
   854
        val defs' = Attrib.map_specs (Attrib.context_attribute_i ctxt) defs;
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   855
        val (_, ctxt') =
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   856
        ctxt |> ProofContext.assume_i ProofContext.export_def
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   857
          (defs' |> map (fn ((name, atts), (t, ps)) =>
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   858
            let val (c, t') = ProofContext.cert_def ctxt t
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   859
            in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   860
      in ((ctxt', Assumed axs), []) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   861
  | activate_elem _ ((ctxt, Derived ths), Defines defs) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   862
      ((ctxt, Derived ths), [])
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   863
  | activate_elem is_ext ((ctxt, mode), Notes facts) =
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   864
      let
17109
606c269d1e26 added add_locale_context(_i), which returns the body context for presentation;
wenzelm
parents: 17096
diff changeset
   865
        val facts' = Attrib.map_facts (Attrib.context_attribute_i ctxt) facts;
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   866
        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i facts';
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   867
      in ((ctxt', mode), if is_ext then res else []) end;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   868
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   869
fun activate_elems (((name, ps), mode), elems) ctxt =
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   870
  let
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   871
    val thy = ProofContext.theory_of ctxt;
17033
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   872
    val ((ctxt', _), res) =
f4c1ce91aa3c Release of interpretation in locale.
ballarin
parents: 17000
diff changeset
   873
        foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   874
      handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   875
    val ctxt'' = if name = "" then ctxt'
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   876
          else let
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   877
              val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   878
              val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   879
            in case mode of
18123
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   880
                Assumed axs =>
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   881
                  fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt''
1bb572e8cee9 avoid prove_plain, export_plain, simplified after_qed;
wenzelm
parents: 18038
diff changeset
   882
              | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   883
            end
16144
e339119f4261 renamed cond_extern to extern;
wenzelm
parents: 16105
diff changeset
   884
  in (ProofContext.restore_naming ctxt ctxt'', res) end;
13399
c136276dc847 support locale ``views'' (for cumulative predicates);
wenzelm
parents: 13394
diff changeset
   885
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   886
fun activate_elemss prep_facts =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   887
    fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   888
      let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   889
        val elems = map (prep_facts ctxt) raw_elems;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   890
        val (ctxt', res) = apsnd List.concat
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   891
            (activate_elems (((name, ps), mode), elems) ctxt);
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   892
        val elems' = elems |> map (Element.map_ctxt
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   893
          {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   894
      in ((((name, ps), elems'), res), ctxt') end);
12834
e5bec3268932 added locale_facts(_i) interface (useful for simple ML proof tools);
wenzelm
parents: 12806
diff changeset
   895
12546
wenzelm
parents: 12532
diff changeset
   896
in
wenzelm
parents: 12532
diff changeset
   897
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   898
(* CB: activate_facts prep_facts (ctxt, elemss),
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   899
   where elemss is a list of pairs consisting of identifiers and
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   900
   context elements, extends ctxt by the context elements yielding
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   901
   ctxt' and returns (ctxt', (elemss', facts)).
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   902
   Identifiers in the argument are of the form ((name, ps), axs) and
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   903
   assumptions use the axioms in the identifiers to set up exporters
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   904
   in ctxt'.  elemss' does not contain identifiers and is obtained
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   905
   from elemss and the intermediate context with prep_facts.
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   906
   If read_facts or cert_facts is used for prep_facts, these also remove
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   907
   the internal/external markers from elemss. *)
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   908
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   909
fun activate_facts prep_facts (ctxt, args) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   910
    let
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   911
      val (res, ctxt') = activate_elemss prep_facts args ctxt;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   912
    in
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   913
      (ctxt', apsnd List.concat (split_list res))
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   914
    end;
12546
wenzelm
parents: 12532
diff changeset
   915
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   916
fun activate_note prep_facts (ctxt, args) =
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   917
  let
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   918
    val (ctxt', ([(_, [Notes args'])], facts)) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   919
      activate_facts prep_facts (ctxt, [((("", []), Assumed []), [Ext (Notes args)])]);
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   920
  in (ctxt', (args', facts)) end;
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15696
diff changeset
   921
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   922
end;
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
   923
12307
459aa05af6be qualify imported facts;
wenzelm
parents: 12289
diff changeset
   924
15696
1da4ce092c0b First release of interpretation commands.
ballarin
parents: 15624
diff changeset
   925
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   926
(** prepare locale elements **)
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   927
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   928
(* expressions *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   929
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   930
fun intern_expr thy (Locale xname) = Locale (intern thy xname)
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   931
  | intern_expr thy (Merge exprs) = Merge (map (intern_expr thy) exprs)
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
   932
  | intern_expr thy (Rename (expr, xs)) = Rename (intern_expr thy expr, xs);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   933
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   934
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   935
(* parameters *)
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   936
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   937
local
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
   938
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   939
fun prep_parms prep_vars ctxt parms =
17856
0551978bfda5 goal statements: accomodate before_qed argument;
wenzelm
parents: 17756
diff changeset
   940
  let val vars = fst (fold_map prep_vars (map (fn (x, T) => ([x], T)) parms) ctxt)
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   941
  in map (fn ([x'], T') => (x', T')) vars end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   942
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   943
in
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   944
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   945
fun read_parms x = prep_parms ProofContext.read_vars x;
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   946
fun cert_parms x = prep_parms ProofContext.cert_vars x;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   947
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   948
end;
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   949
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   950
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   951
(* propositions and bindings *)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   952
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   953
(* flatten (ctxt, prep_expr) ((ids, syn), expr)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   954
   normalises expr (which is either a locale
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   955
   expression or a single context element) wrt.
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   956
   to the list ids of already accumulated identifiers.
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   957
   It returns (ids', syn', elemss) where ids' is an extension of ids
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   958
   with identifiers generated for expr, and elemss is the list of
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   959
   context elements generated from expr.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   960
   syn and syn' are symtabs mapping parameter names to their syntax.  syn'
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   961
   is an extension of syn.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   962
   For details, see flatten_expr.
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   963
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   964
   Additionally, for a locale expression, the elems are grouped into a single
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   965
   Int; individual context elements are marked Ext.  In this case, the
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   966
   identifier-like information of the element is as follows:
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   967
   - for Fixes: (("", ps), []) where the ps have type info NONE
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   968
   - for other elements: (("", []), []).
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   969
   The implementation of activate_facts relies on identifier names being
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
   970
   empty strings for external elements.
15596
8665d08085df First version of global registration command.
ballarin
parents: 15574
diff changeset
   971
*)
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   972
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   973
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   974
        val ids' = ids @ [(("", map #1 fixes), ([], Assumed []))]
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   975
      in
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   976
        ((ids',
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   977
         merge_syntax ctxt ids'
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   978
           (syn, Symtab.make (map (fn fx => (#1 fx, #3 fx)) fixes))
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   979
           handle Symtab.DUPS xs => err_in_locale ctxt
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   980
             ("Conflicting syntax for parameters: " ^ commas_quote xs)
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   981
             (map #1 ids')),
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
   982
         [((("", map (rpair NONE o #1) fixes), Assumed []), Ext (Fixes fixes))])
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   983
      end
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   984
  | flatten _ ((ids, syn), Elem elem) =
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
   985
      ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
16102
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   986
  | flatten (ctxt, prep_expr) ((ids, syn), Expr expr) =
c5f6726d9bb1 Locale expressions: rename with optional mixfix syntax.
ballarin
parents: 16028
diff changeset
   987
      apsnd (map (apsnd Int)) (flatten_expr ctxt ((ids, syn), prep_expr expr));
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
   988
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   989
local
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   990
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   991
local
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
   992
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
   993
fun declare_int_elem (ctxt, Fixes fixes) =
12575
34985eee55b1 fixed inst_thm: proper domain of env;
wenzelm
parents: 12546
diff changeset
   994
      (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   995
        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
   996
  | declare_int_elem (ctxt, _) = (ctxt, []);
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
   997
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   998
fun declare_ext_elem prep_parms (ctxt, Fixes fixes) =
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
   999
      let
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1000
        val parms = map (fn (x, T, _) => (x, T)) fixes;
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1001
        val parms' = prep_parms ctxt parms;
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1002
        val fixes' = map (fn ((x, T), (_, _, mx)) => (x, T, mx)) (parms' ~~ fixes);
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1003
      in (ctxt |> ProofContext.add_fixes fixes', []) end
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1004
  | declare_ext_elem prep_parms (ctxt, Constrains csts) =
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1005
      let
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1006
        val parms = map (fn (x, T) => (x, SOME T)) csts;
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1007
        val parms' = prep_parms ctxt parms;
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1008
        val ts = map (fn (x, SOME T) => Free (x, T)) parms';
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
  1009
      in (fold ProofContext.declare_term ts ctxt, []) end
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1010
  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1011
  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1012
  | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1013
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1014
fun declare_elems prep_parms (ctxt, (((name, ps), Assumed _), elems)) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1015
    let val (ctxt', propps) =
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1016
      (case elems of
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1017
        Int es => foldl_map declare_int_elem (ctxt, es)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1018
      | Ext e => foldl_map (declare_ext_elem prep_parms) (ctxt, [e]))
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1019
      handle ProofContext.CONTEXT (msg, ctxt) =>
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1020
        err_in_locale ctxt msg [(name, map fst ps)]
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1021
    in (ctxt', propps) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1022
  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1023
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1024
in
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1025
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1026
fun declare_elemss prep_parms fixed_params raw_elemss ctxt =
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1027
  let
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1028
    (* CB: fix of type bug of goal in target with context elements.
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1029
       Parameters new in context elements must receive types that are
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1030
       distinct from types of parameters in target (fixed_params).  *)
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1031
    val ctxt_with_fixed =
16028
a2c790d145ba fold ProofContext.declare_term;
wenzelm
parents: 15842
diff changeset
  1032
      fold ProofContext.declare_term (map Free fixed_params) ctxt;
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1033
    val int_elemss =
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1034
      raw_elemss
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1035
      |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
14215
ebf291f3b449 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents: 13629
diff changeset
  1036
      |> unify_elemss ctxt_with_fixed fixed_params;
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1037
    val (_, raw_elemss') =
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1038
      foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1039
        (int_elemss, raw_elemss);
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1040
  in foldl_map (declare_elems prep_parms) (ctxt, raw_elemss') end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1041
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1042
end;
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1043
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1044
local
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1045
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1046
val norm_term = Envir.beta_norm oo Term.subst_atomic;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1047
13336
1bd21b082466 tuned add_thmss;
wenzelm
parents: 13308
diff changeset
  1048
fun abstract_term eq =    (*assumes well-formedness according to ProofContext.cert_def*)
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1049
  let
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1050
    val body = Term.strip_all_body eq;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1051
    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1052
    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
18343
e36238ac5359 defines: beta/eta contract lhs;
wenzelm
parents: 18330
diff changeset
  1053
    val (f, xs) = Term.strip_comb (Pattern.beta_eta_contract lhs);
13336
1bd21b082466 tuned add_thmss;
wenzelm
parents: 13308
diff changeset
  1054
    val eq' = Term.list_abs_free (map Term.dest_Free xs, rhs);
1bd21b082466 tuned add_thmss;
wenzelm
parents: 13308
diff changeset
  1055
  in (Term.dest_Free f, eq') end;
1bd21b082466 tuned add_thmss;
wenzelm
parents: 13308
diff changeset
  1056
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1057
fun abstract_thm thy eq =
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1058
  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
  1059
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1060
fun bind_def ctxt (name, ps) eq (xs, env, ths) =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1061
  let
13336
1bd21b082466 tuned add_thmss;
wenzelm
parents: 13308
diff changeset
  1062
    val ((y, T), b) = abstract_term eq;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1063
    val b' = norm_term env b;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16346
diff changeset
  1064
    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1065
    fun err msg = err_in_locale ctxt (msg ^ ": " ^ quote y) [(name, map fst ps)];
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1066
  in
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1067
    conditional (exists (equal y o #1) xs) (fn () =>
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1068
      err "Attempt to define previously specified variable");
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1069
    conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1070
      err "Attempt to redefine variable");
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
  1071
    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1072
  end;
12575
34985eee55b1 fixed inst_thm: proper domain of env;
wenzelm
parents: 12546
diff changeset
  1073
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1074
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1075
(* CB: for finish_elems (Int and Ext),
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1076
   extracts specification, only of assumed elements *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1077
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1078
fun eval_text _ _ _ (Fixes _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1079
  | eval_text _ _ _ (Constrains _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1080
  | eval_text _ (_, Assumed _) is_ext (Assumes asms)
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1081
        (((exts, exts'), (ints, ints')), (xs, env, defs)) =
13394
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1082
      let
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1083
        val ts = List.concat (map (map #1 o #2) asms);
13394
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1084
        val ts' = map (norm_term env) ts;
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1085
        val spec' =
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1086
          if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
b39347206719 define cumulative predicate view;
wenzelm
parents: 13375
diff changeset
  1087
          else ((exts, exts'), (ints @ ts, ints' @ ts'));
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
  1088
      in (spec', (fold Term.add_frees ts' xs, env, defs)) end
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1089
  | eval_text _ (_, Derived _) _ (Assumes _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1090
  | eval_text ctxt (id, Assumed _) _ (Defines defs) (spec, binds) =
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1091
      (spec, fold (bind_def ctxt id o #1 o #2) defs binds)
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1092
  | eval_text _ (_, Derived _) _ (Defines _) text = text
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1093
  | eval_text _ _ _ (Notes _) text = text;
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1094
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1095
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1096
(* for finish_elems (Int),
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1097
   remove redundant elements of derived identifiers,
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1098
   turn assumptions and definitions into facts,
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1099
   adjust hypotheses of facts using witness theorems *)
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1100
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1101
fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1102
  | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1103
  | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1104
  | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1105
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1106
  | finish_derived _ _ (Derived _) (Fixes _) = NONE
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1107
  | finish_derived _ _ (Derived _) (Constrains _) = NONE
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1108
  | finish_derived sign wits (Derived _) (Assumes asms) = asms
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1109
      |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1110
      |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1111
  | finish_derived sign wits (Derived _) (Defines defs) = defs
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1112
      |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1113
      |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1114
17096
8327b71282ce Improved generation of witnesses in interpretation.
ballarin
parents: 17033
diff changeset
  1115
  | finish_derived _ wits _ (Notes facts) = (Notes facts)
18137
cb916659c89b moved datatype elem to element.ML;
wenzelm
parents: 18123
diff changeset
  1116
      |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1117
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1118
(* CB: for finish_elems (Ext) *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1119
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1120
fun closeup _ false elem = elem
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1121
  | closeup ctxt true elem =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1122
      let
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1123
        fun close_frees t =
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1124
          let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16850
diff changeset
  1125
            (Term.add_frees t []))
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1126
          in Term.list_all_free (frees, t) end;
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1127
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1128
        fun no_binds [] = []
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1129
          | no_binds _ =
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1130
              raise ProofContext.CONTEXT ("Illegal term bindings in locale element", ctxt);
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1131
      in
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1132
        (case elem of
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1133
          Assumes asms => Assumes (asms |> map (fn (a, propps) =>
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1134
            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1135
        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1136
            (a, (close_frees (#2 (ProofContext.cert_def ctxt t)), no_binds ps))))
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1137
        | e => e)
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1138
      end;
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1139
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
  1140
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1141
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (x, _, mx) =>
17271
2756a73f63a5 introduced some new-style AList operations
haftmann
parents: 17257
diff changeset
  1142
      (x, AList.lookup (op =) parms x, mx)) fixes)
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1143
  | finish_ext_elem parms _ (Constrains csts, _) =
17271
2756a73f63a5 introduced some new-style AList operations
haftmann
parents: 17257
diff changeset
  1144
      Constrains (map (fn (x, _) => (x, (the o AList.lookup (op =) parms) x)) csts)
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1145
  | finish_ext_elem _ close (Assumes asms, propp) =
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1146
      close (Assumes (map #1 asms ~~ propp))
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1147
  | finish_ext_elem _ close (Defines defs, propp) =
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1148
      close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1149
  | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1150
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1151
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1152
(* CB: finish_parms introduces type info from parms to identifiers *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15456
diff changeset
  1153
(* CB: only needed for types that have been NONE so far???
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1154
   If so, which are these??? *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1155
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1156
fun finish_parms parms (((name, ps), mode), elems) =
17485
c39871c52977 introduced AList module
haftmann
parents: 17449
diff changeset
  1157
  (((name, map (fn (x, _) => (x, AList.lookup (op =) parms x)) ps), mode), elems);
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1158
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1159
fun finish_elems ctxt parms _ ((text, wits), ((id, Int e), _)) =
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1160
      let
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1161
        val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1162
        val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1163
        val text' = fold (eval_text ctxt id' false) es text;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1164
        val es' = List.mapPartial
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1165
              (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1166
      in ((text', wits'), (id', map Int es')) end
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1167
  | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
13308
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1168
      let
1dbed9ea764b clarified text content of locale body;
wenzelm
parents: 13297
diff changeset
  1169
        val e' = finish_ext_elem parms (closeup ctxt do_close) (e, propp);
18190
b7748c77562f tuned Pattern.match/unify;
wenzelm
parents: 18137
diff changeset
  1170
        val text' = eval_text ctxt id true e' text;
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1171
      in ((text', wits), (id, [Ext e'])) end
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1172
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1173
in
12510
172d18ec3b54 proper treatment of internal parameters;
wenzelm
parents: 12502
diff changeset
  1174
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1175
(* CB: only called by prep_elemss *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1176
13375
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
  1177
fun finish_elemss ctxt parms do_close =
7cbf2dea46d0 proper predicate definitions of locale body;
wenzelm
parents: 13336
diff changeset
  1178
  foldl_map (apsnd (finish_parms parms) o finish_elems ctxt parms do_close);
12839
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1179
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1180
end;
584a3e0b00f2 reorganized code for predicate text;
wenzelm
parents: 12834
diff changeset
  1181
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1182
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1183
(* CB: type inference and consistency checks for locales.
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1184
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1185
   Works by building a context (through declare_elemss), extracting the
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1186
   required information and adjusting the context elements (finish_elemss).
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1187
   Can also universally close free vars in assms and defs.  This is only
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1188
   needed for Ext elements and controlled by parameter do_close.
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1189
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1190
   Only elements of assumed identifiers are considered.
16736
1e792b32abef Preparations for interpretation of locales in locales.
ballarin
parents: 16620
diff changeset
  1191
*)
15127
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1192
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1193
fun prep_elemss prep_parms prepp do_close context fixed_params raw_elemss raw_concl =
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1194
  let
15127
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1195
    (* CB: contexts computed in the course of this function are discarded.
2550a5578d39 Disallowed "includes" in locale declarations.
ballarin
parents: 15104
diff changeset
  1196
       They are used for type inference and consistency checks only. *)
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1197
    (* CB: fixed_params are the parameters (with types) of the target locale,
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1198
       empty list if there is no target. *)
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1199
    (* CB: raw_elemss are list of pairs consisting of identifiers and
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1200
       context elements, the latter marked as internal or external. *)
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1201
    val (raw_ctxt, raw_proppss) = declare_elemss prep_parms fixed_params raw_elemss context;
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1202
    (* CB: raw_ctxt is context with additional fixed variables derived from
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1203
       the fixes elements in raw_elemss,
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1204
       raw_proppss contains assumptions and definitions from the
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1205
       external elements in raw_elemss. *)
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
  1206
    fun prep_prop raw_propp (raw_ctxt, raw_concl)  =
18450
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1207
      let
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1208
        (* CB: add type information from fixed_params to context (declare_term) *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1209
        (* CB: process patterns (conclusion and external elements only) *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1210
        val (ctxt, all_propp) =
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1211
          prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1212
        (* CB: add type information from conclusion and external elements to context *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1213
        val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1214
        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1215
        val all_propp' = map2 (curry (op ~~))
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1216
          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
e57731ba01dd discontinued unflat in favour of burrow and burrow_split
haftmann
parents: 18421
diff changeset
  1217
        val (concl, propp) = splitAt (length raw_concl, all_propp')
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
  1218
      in (propp, (ctxt, concl)) end
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1219
18550
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
  1220
    val (proppss, (ctxt, concl)) =
59b89f625d68 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
haftmann
parents: 18546
diff changeset
  1221
      (fold_burrow o fold_burrow) prep_prop raw_proppss (raw_ctxt, raw_concl);
12502
9e7f72e25022 beginning support for type instantiation;
wenzelm
parents: 12323
diff changeset
  1222
15206
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1223
    (* CB: obtain all parameters from identifier part of raw_elemss *)
09d78ec709c7 Modified locales: improved implementation of "includes".
ballarin
parents: 15127
diff changeset
  1224
    val xs = map #1 (params_of' raw_elemss);
12727
330cb92aaea3 unify_frozen: proper use of maxidx';
wenzelm
parents: 12711
diff changeset
  1225
    val typing = unify_frozen ctxt 0
12529
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1226
      (map (ProofContext.default_type raw_ctxt) xs)
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1227
      (map (ProofContext.default_type ctxt) xs);
d99716a53f59 simultaneous type-inference of complete context/statement specifications;
wenzelm
parents: 12514
diff changeset
  1228
    val parms = param_types (xs ~~ typing);
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1229
    (* CB: parms are the parameters from raw_elemss, with correct typing. *)
12273
7fb9840d358d beginnings of actual locale expressions;
wenzelm
parents: 12263
diff changeset
  1230
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1231
    (* CB: extract information from assumes and defines elements
16169
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1232
       (fixes, constrains and notes in raw_elemss don't have an effect on
b59202511b8a Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 16144
diff changeset
  1233
       text and elemss), compute final form of context elements. *)
17000
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1234
    val ((text, _), elemss) = finish_elemss ctxt parms do_close
552df70f52c2 First version of interpretation in locales. Not yet fully functional.
ballarin
parents: 16947
diff changeset
  1235
      ((((([], []), ([], [])), ([], [], [])), []), raw_elemss ~~ proppss);
14508
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1236
    (* CB: text has the following structure:
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1237
           (((exts, exts'), (ints, ints')), (xs, env, defs))
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1238
       where
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1239
         exts: external assumptions (terms in external assumes elements)
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1240
         exts': dito, normalised wrt. env
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1241
         ints: internal assumptions (terms in internal assumes elements)
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1242
         ints': dito, normalised wrt. env
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1243
         xs: the free variables in exts' and ints' and rhss of definitions,
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1244
           this includes parameters except defined parameters
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1245
         env: list of term pairs encoding substitutions, where the first term
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1246
           is a free variable; substitutions represent defines elements and
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1247
           the rhs is normalised wrt. the previous env
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1248
         defs: theorems representing the substitutions from defines elements
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1249
           (thms are normalised wrt. env).
859b11514537 Experimental command for instantiation of locales in proof contexts:
ballarin
parents: 14446
diff changeset
  1250