src/Pure/Isar/local_theory.ML
author wenzelm
Tue May 16 21:33:14 2006 +0200 (2006-05-16 ago)
changeset 19661 baab85f25e0e
parent 19630 d370c3f5d3b2
child 19680 6a34b1b1f540
permissions -rw-r--r--
added syntax interface;
tuned interface;
wenzelm@18744
     1
(*  Title:      Pure/Isar/local_theory.ML
wenzelm@18744
     2
    ID:         $Id$
wenzelm@18744
     3
    Author:     Makarius
wenzelm@18744
     4
wenzelm@18744
     5
Local theory operations, with optional target locale.
wenzelm@18744
     6
*)
wenzelm@18744
     7
wenzelm@18951
     8
type local_theory = Proof.context;
wenzelm@18951
     9
wenzelm@18744
    10
signature LOCAL_THEORY =
wenzelm@18744
    11
sig
wenzelm@18951
    12
  val params_of: local_theory -> (string * typ) list
wenzelm@18951
    13
  val hyps_of: local_theory -> term list
wenzelm@18951
    14
  val standard: local_theory -> thm -> thm
wenzelm@18951
    15
  val pretty_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
wenzelm@18951
    16
  val quiet_mode: bool ref
wenzelm@18951
    17
  val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@18951
    18
  val theory: (theory -> theory) -> local_theory -> local_theory
wenzelm@18951
    19
  val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
wenzelm@18951
    20
  val init: xstring option -> theory -> local_theory
wenzelm@18951
    21
  val init_i: string option -> theory -> local_theory
wenzelm@19017
    22
  val restore: local_theory -> local_theory
wenzelm@18951
    23
  val exit: local_theory -> local_theory * theory
wenzelm@19059
    24
  val restore_naming: local_theory -> local_theory
wenzelm@19059
    25
  val naming: local_theory -> local_theory
wenzelm@19059
    26
  val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory
wenzelm@19661
    27
  val syntax: string * bool -> (string * mixfix) list -> local_theory -> local_theory
wenzelm@19661
    28
  val abbrevs: string * bool -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
wenzelm@18951
    29
  val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
wenzelm@18876
    30
  val consts_restricted: (string * typ -> bool) ->
wenzelm@18951
    31
    ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory
wenzelm@18951
    32
  val axioms: ((bstring * Attrib.src list) * term list) list -> local_theory ->
wenzelm@18951
    33
    (bstring * thm list) list * local_theory
wenzelm@18951
    34
  val axioms_finish: (local_theory -> thm -> thm) ->
wenzelm@18951
    35
    ((bstring * Attrib.src list) * term list) list -> local_theory ->
wenzelm@18951
    36
    (bstring * thm list) list * local_theory
wenzelm@18767
    37
  val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
wenzelm@18951
    38
    local_theory -> (bstring * thm list) list * local_theory
wenzelm@18951
    39
  val note: (bstring * Attrib.src list) * thm list -> local_theory ->
wenzelm@18951
    40
    (bstring * thm list) * local_theory
wenzelm@18823
    41
  val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
wenzelm@18951
    42
    local_theory -> (term * (bstring * thm)) * local_theory
wenzelm@18951
    43
  val def_finish: (local_theory -> term -> thm -> thm) ->
wenzelm@18823
    44
    (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
wenzelm@18951
    45
    local_theory -> (term * (bstring * thm)) * local_theory
wenzelm@18744
    46
end;
wenzelm@18744
    47
wenzelm@18744
    48
structure LocalTheory: LOCAL_THEORY =
wenzelm@18744
    49
struct
wenzelm@18744
    50
wenzelm@19059
    51
wenzelm@18767
    52
(** local context data **)
wenzelm@18744
    53
wenzelm@18744
    54
structure Data = ProofDataFun
wenzelm@18744
    55
(
wenzelm@18876
    56
  val name = "Pure/local_theory";
wenzelm@18744
    57
  type T =
wenzelm@18805
    58
   {locale: (string * (cterm list * Proof.context)) option,
wenzelm@18744
    59
    params: (string * typ) list,
wenzelm@18744
    60
    hyps: term list,
wenzelm@19059
    61
    restore_naming: theory -> theory};
wenzelm@19059
    62
  fun init thy = {locale = NONE, params = [], hyps = [], restore_naming = I};
wenzelm@18744
    63
  fun print _ _ = ();
wenzelm@18744
    64
);
wenzelm@18744
    65
val _ = Context.add_setup Data.init;
wenzelm@18744
    66
wenzelm@19059
    67
fun map_locale f = Data.map (fn {locale, params, hyps, restore_naming} =>
wenzelm@18805
    68
  {locale = Option.map (fn (loc, (view, ctxt)) => (loc, (view, f ctxt))) locale,
wenzelm@19059
    69
    params = params, hyps = hyps, restore_naming = restore_naming});
wenzelm@18805
    70
wenzelm@18767
    71
val locale_of = #locale o Data.get;
wenzelm@18767
    72
val params_of = #params o Data.get;
wenzelm@18767
    73
val hyps_of = #hyps o Data.get;
wenzelm@18805
    74
wenzelm@18805
    75
fun standard ctxt =
wenzelm@18805
    76
  (case #locale (Data.get ctxt) of
wenzelm@18805
    77
    NONE => Drule.standard
wenzelm@18805
    78
  | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt);
wenzelm@18744
    79
wenzelm@18767
    80
wenzelm@18823
    81
(* print consts *)
wenzelm@18767
    82
wenzelm@18951
    83
val quiet_mode = ref false;
wenzelm@18951
    84
wenzelm@18767
    85
local
wenzelm@18767
    86
wenzelm@18767
    87
fun pretty_var ctxt (x, T) =
wenzelm@18767
    88
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@18767
    89
    Pretty.quote (ProofContext.pretty_typ ctxt T)];
wenzelm@18744
    90
wenzelm@18767
    91
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@18767
    92
wenzelm@18767
    93
in
wenzelm@18767
    94
wenzelm@18876
    95
fun pretty_consts ctxt pred cs =
wenzelm@18876
    96
  (case filter pred (params_of ctxt) of
wenzelm@18767
    97
    [] => pretty_vars ctxt "constants" cs
wenzelm@18767
    98
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@18767
    99
wenzelm@18876
   100
fun print_consts _ _ [] = ()
wenzelm@18951
   101
  | print_consts ctxt pred cs =
wenzelm@18951
   102
      if ! quiet_mode then () else Pretty.writeln (pretty_consts ctxt pred cs);
wenzelm@18823
   103
wenzelm@18767
   104
end;
wenzelm@18767
   105
wenzelm@18767
   106
wenzelm@18805
   107
(* theory/locale substructures *)
wenzelm@18781
   108
wenzelm@18781
   109
fun theory_result f ctxt =
wenzelm@18781
   110
  let val (res, thy') = f (ProofContext.theory_of ctxt)
wenzelm@19032
   111
  in (res, ctxt |> map_locale (ProofContext.transfer thy') |> ProofContext.transfer thy') end;
wenzelm@19032
   112
wenzelm@19032
   113
fun theory f ctxt = #2 (theory_result (f #> pair ()) ctxt);
wenzelm@18805
   114
wenzelm@18805
   115
fun locale_result f ctxt =
wenzelm@18805
   116
  (case locale_of ctxt of
wenzelm@18805
   117
    NONE => error "Local theory: no locale context"
wenzelm@19017
   118
  | SOME (_, view_ctxt) =>
wenzelm@18805
   119
      let
wenzelm@19017
   120
        val (res, loc_ctxt') = f view_ctxt;
wenzelm@18805
   121
        val thy' = ProofContext.theory_of loc_ctxt';
wenzelm@19032
   122
      in (res, ctxt |> map_locale (K loc_ctxt') |> ProofContext.transfer thy') end);
wenzelm@18805
   123
wenzelm@19017
   124
fun locale f ctxt =
wenzelm@19017
   125
  if is_none (locale_of ctxt) then ctxt
wenzelm@19017
   126
  else #2 (locale_result (f #> pair ()) ctxt);
wenzelm@18805
   127
wenzelm@19017
   128
wenzelm@19017
   129
(* init -- restore -- exit *)
wenzelm@18781
   130
wenzelm@18781
   131
fun init_i NONE thy = ProofContext.init thy
wenzelm@18781
   132
  | init_i (SOME loc) thy =
wenzelm@18781
   133
      thy
wenzelm@18781
   134
      |> Locale.init loc
wenzelm@18805
   135
      ||>> ProofContext.inferred_fixes
wenzelm@18805
   136
      |> (fn ((view, params), ctxt) => Data.put
wenzelm@18805
   137
          {locale = SOME (loc, (view, ctxt)),
wenzelm@18781
   138
           params = params,
wenzelm@18781
   139
           hyps = ProofContext.assms_of ctxt,
wenzelm@19059
   140
           restore_naming = Sign.restore_naming thy} ctxt);
wenzelm@18781
   141
wenzelm@18805
   142
fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
wenzelm@18781
   143
wenzelm@19017
   144
fun restore ctxt =
wenzelm@19017
   145
  (case locale_of ctxt of
wenzelm@19017
   146
    NONE => ctxt
wenzelm@19017
   147
  | SOME (_, (_, loc_ctxt)) => loc_ctxt |> Data.put (Data.get ctxt));
wenzelm@19017
   148
wenzelm@19059
   149
fun exit ctxt = (ctxt, ProofContext.theory_of ctxt);
wenzelm@19059
   150
wenzelm@19059
   151
wenzelm@19059
   152
(* local naming *)
wenzelm@19059
   153
wenzelm@19059
   154
fun naming ctxt =
wenzelm@19059
   155
  (case locale_of ctxt of
wenzelm@19059
   156
    NONE => ctxt
wenzelm@19059
   157
  | SOME (loc, _) => ctxt |> theory (Sign.sticky_prefix (Sign.base_name loc)));
wenzelm@19059
   158
wenzelm@19059
   159
fun restore_naming ctxt = theory (#restore_naming (Data.get ctxt)) ctxt;
wenzelm@19059
   160
wenzelm@19059
   161
fun mapping loc f =
wenzelm@19059
   162
  init loc #> naming #> f #> restore_naming #> exit;
wenzelm@18781
   163
wenzelm@18781
   164
wenzelm@18781
   165
wenzelm@18781
   166
(** local theory **)
wenzelm@18781
   167
wenzelm@19661
   168
(* term syntax *)
wenzelm@19661
   169
wenzelm@19661
   170
fun term_syntax add_thy add_ctxt prmode args ctxt = ctxt |>
wenzelm@19661
   171
  (case locale_of ctxt of
wenzelm@19661
   172
    NONE => theory (add_thy prmode args)
wenzelm@19661
   173
  | SOME (loc, _) =>
wenzelm@19661
   174
      locale (Locale.add_term_syntax loc (add_ctxt prmode args)) #>
wenzelm@19661
   175
      add_ctxt prmode args);
wenzelm@19661
   176
wenzelm@19661
   177
val syntax = term_syntax Sign.add_const_syntax ProofContext.add_const_syntax;
wenzelm@19661
   178
wenzelm@19661
   179
fun abbrevs prmode args =
wenzelm@19661
   180
  term_syntax Sign.add_abbrevs ProofContext.add_abbrevs
wenzelm@19661
   181
    prmode (map (fn ((x, mx), rhs) => (x, rhs, mx)) args);
wenzelm@19661
   182
wenzelm@19661
   183
wenzelm@18767
   184
(* consts *)
wenzelm@18744
   185
wenzelm@18876
   186
fun consts_restricted pred decls ctxt =
wenzelm@18744
   187
  let
wenzelm@18744
   188
    val thy = ProofContext.theory_of ctxt;
wenzelm@18876
   189
    val params = filter pred (params_of ctxt);
wenzelm@18744
   190
    val ps = map Free params;
wenzelm@18805
   191
    val Ps = map #2 params;
wenzelm@19661
   192
    val abbrs = decls |> map (fn ((c, T), mx) =>
wenzelm@19661
   193
      ((c, mx), Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps)));
wenzelm@18744
   194
  in
wenzelm@19017
   195
    ctxt |>
wenzelm@19017
   196
    (case locale_of ctxt of
wenzelm@19661
   197
      NONE => theory (Sign.add_consts_authentic (map (fn ((c, T), mx) => (c, T, mx)) decls))
wenzelm@19017
   198
    | SOME (loc, _) =>
wenzelm@19017
   199
        theory (Sign.add_consts_i (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #>
wenzelm@19661
   200
        abbrevs Syntax.default_mode abbrs)
wenzelm@19661
   201
    |> pair (map #2 abbrs)
wenzelm@18767
   202
  end;
wenzelm@18767
   203
wenzelm@18876
   204
val consts = consts_restricted (K true);
wenzelm@18876
   205
wenzelm@18767
   206
wenzelm@18805
   207
(* fact definitions *)
wenzelm@18767
   208
wenzelm@18767
   209
fun notes kind facts ctxt =
wenzelm@18805
   210
  let
wenzelm@18805
   211
    val attrib = Attrib.attribute_i (ProofContext.theory_of ctxt);
wenzelm@18805
   212
    val facts' = map (apsnd (map (apfst (map (standard ctxt))))) facts;
wenzelm@18805
   213
  in
wenzelm@18805
   214
    ctxt |>
wenzelm@18805
   215
    (case locale_of ctxt of
wenzelm@18805
   216
      NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts'))
wenzelm@19017
   217
    | SOME (loc, _) =>
wenzelm@19017
   218
        locale_result (apfst #1 o Locale.add_thmss kind loc facts'))
wenzelm@18805
   219
    ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts))
wenzelm@18805
   220
  end;
wenzelm@18767
   221
wenzelm@18781
   222
fun note (a, ths) ctxt =
wenzelm@18805
   223
  ctxt |> notes PureThy.theoremK [(a, [(ths, [])])] |>> hd;
wenzelm@18767
   224
wenzelm@18767
   225
wenzelm@18767
   226
(* axioms *)
wenzelm@18767
   227
wenzelm@18781
   228
local
wenzelm@18781
   229
wenzelm@18781
   230
fun add_axiom hyps (name, prop) thy =
wenzelm@18767
   231
  let
wenzelm@19517
   232
    val name' = if name = "" then "axiom_" ^ serial_string () else name;
wenzelm@18767
   233
    val frees = rev ([] |> Term.add_frees prop |> fold Term.add_frees hyps);
wenzelm@18767
   234
    val prop' = Term.list_all_free (frees, Logic.list_implies (hyps, prop));
wenzelm@18767
   235
    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
wenzelm@18781
   236
wenzelm@18781
   237
    val cert = Thm.cterm_of thy';
wenzelm@18781
   238
    fun all_polymorphic (x, T) th =
wenzelm@18781
   239
      let val var = cert (Var ((x, 0), #1 (Logic.dest_all (Thm.prop_of th))))
wenzelm@18781
   240
      in ((var, cert (Free (x, T))), Thm.forall_elim var th) end;
wenzelm@18781
   241
    fun implies_polymorphic hyp th = Thm.assume (cert hyp) COMP th;
wenzelm@18767
   242
    val th =
wenzelm@18767
   243
      Thm.get_axiom_i thy' (Sign.full_name thy' name')
wenzelm@18781
   244
      |> fold_map all_polymorphic frees |-> Drule.cterm_instantiate
wenzelm@18781
   245
      |> fold implies_polymorphic hyps
wenzelm@18767
   246
  in (th, thy') end;
wenzelm@18767
   247
wenzelm@18781
   248
in
wenzelm@18781
   249
wenzelm@18805
   250
fun axioms_finish finish = fold_map (fn ((name, atts), props) =>
wenzelm@18805
   251
  fold ProofContext.fix_frees props
wenzelm@18805
   252
  #> (fn ctxt => ctxt
wenzelm@18805
   253
    |> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props))
wenzelm@18805
   254
    |-> (fn ths => note ((name, atts), map (finish ctxt) ths))));
wenzelm@18805
   255
wenzelm@18805
   256
val axioms = axioms_finish (K I);
wenzelm@18744
   257
wenzelm@18744
   258
end;
wenzelm@18781
   259
wenzelm@18781
   260
wenzelm@18805
   261
(* constant definitions *)
wenzelm@18781
   262
wenzelm@18781
   263
local
wenzelm@18781
   264
wenzelm@18805
   265
fun add_def (name, prop) =
wenzelm@19630
   266
  Theory.add_defs_i false false [(name, prop)] #> (fn thy =>
wenzelm@18805
   267
    let
wenzelm@18805
   268
      val th = Thm.get_axiom_i thy (Sign.full_name thy name);
wenzelm@18805
   269
      val cert = Thm.cterm_of thy;
wenzelm@18805
   270
      val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free)))
wenzelm@18805
   271
        (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []);
wenzelm@18805
   272
    in (Drule.cterm_instantiate subst th, thy) end);
wenzelm@18781
   273
wenzelm@18781
   274
in
wenzelm@18781
   275
wenzelm@18805
   276
fun def_finish finish (var, spec) ctxt =
wenzelm@18781
   277
  let
wenzelm@18781
   278
    val (x, mx) = var;
wenzelm@18781
   279
    val ((name, atts), rhs) = spec;
wenzelm@18781
   280
    val name' = if name = "" then Thm.def_name x else name;
wenzelm@18876
   281
    val rhs_frees = Term.add_frees rhs [];
wenzelm@18781
   282
  in
wenzelm@18781
   283
    ctxt
wenzelm@18876
   284
    |> consts_restricted (member (op =) rhs_frees) [((x, Term.fastype_of rhs), mx)]
wenzelm@18781
   285
    |-> (fn [lhs] =>
wenzelm@18781
   286
      theory_result (add_def (name', Logic.mk_equals (lhs, rhs)))
wenzelm@18781
   287
      #-> (fn th => fn ctxt' => note ((name', atts), [finish ctxt' lhs th]) ctxt')
wenzelm@18781
   288
      #> apfst (fn (b, [th]) => (lhs, (b, th))))
wenzelm@18781
   289
  end;
wenzelm@18781
   290
wenzelm@18805
   291
val def = def_finish (K (K I));
wenzelm@18805
   292
wenzelm@18781
   293
end;
wenzelm@18781
   294
wenzelm@18781
   295
end;