src/Pure/Isar/local_theory.ML
author wenzelm
Tue Jan 31 18:19:31 2006 +0100 (2006-01-31 ago)
changeset 18876 ddb6803da197
parent 18823 916c493b7f0c
child 18951 4f5f6c632127
permissions -rw-r--r--
added consts_retricted;
pretty/print_consts: parameter restriction;
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@18744
     8
signature LOCAL_THEORY =
wenzelm@18744
     9
sig
wenzelm@18744
    10
  val params_of: Proof.context -> (string * typ) list
wenzelm@18767
    11
  val hyps_of: Proof.context -> term list
wenzelm@18781
    12
  val standard: Proof.context -> thm -> thm
wenzelm@18876
    13
  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
wenzelm@18876
    14
  val print_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@18781
    15
  val theory: (theory -> theory) -> Proof.context -> Proof.context
wenzelm@18781
    16
  val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
wenzelm@18781
    17
  val init: xstring option -> theory -> Proof.context
wenzelm@18781
    18
  val init_i: string option -> theory -> Proof.context
wenzelm@18805
    19
  val exit: Proof.context -> Proof.context * theory
wenzelm@18823
    20
  val consts: ((bstring * typ) * mixfix) list -> Proof.context -> term list * Proof.context
wenzelm@18876
    21
  val consts_restricted: (string * typ -> bool) ->
wenzelm@18876
    22
    ((bstring * typ) * mixfix) list -> Proof.context -> term list * Proof.context
wenzelm@18823
    23
  val axioms: ((bstring * Attrib.src list) * term list) list -> Proof.context ->
wenzelm@18781
    24
    (bstring * thm list) list * Proof.context
wenzelm@18805
    25
  val axioms_finish: (Proof.context -> thm -> thm) ->
wenzelm@18823
    26
    ((bstring * Attrib.src list) * term list) list -> Proof.context ->
wenzelm@18805
    27
    (bstring * thm list) list * Proof.context
wenzelm@18767
    28
  val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
wenzelm@18767
    29
    Proof.context -> (bstring * thm list) list * Proof.context
wenzelm@18781
    30
  val note: (bstring * Attrib.src list) * thm list -> Proof.context ->
wenzelm@18767
    31
    (bstring * thm list) * Proof.context
wenzelm@18823
    32
  val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
wenzelm@18781
    33
    Proof.context -> (term * (bstring * thm)) * Proof.context
wenzelm@18805
    34
  val def_finish: (Proof.context -> term -> thm -> thm) ->
wenzelm@18823
    35
    (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
wenzelm@18781
    36
    Proof.context -> (term * (bstring * thm)) * Proof.context
wenzelm@18744
    37
end;
wenzelm@18744
    38
wenzelm@18744
    39
structure LocalTheory: LOCAL_THEORY =
wenzelm@18744
    40
struct
wenzelm@18744
    41
wenzelm@18767
    42
(** local context data **)
wenzelm@18744
    43
wenzelm@18744
    44
structure Data = ProofDataFun
wenzelm@18744
    45
(
wenzelm@18876
    46
  val name = "Pure/local_theory";
wenzelm@18744
    47
  type T =
wenzelm@18805
    48
   {locale: (string * (cterm list * Proof.context)) option,
wenzelm@18744
    49
    params: (string * typ) list,
wenzelm@18744
    50
    hyps: term list,
wenzelm@18744
    51
    exit: theory -> theory};
wenzelm@18805
    52
  fun init thy = {locale = NONE, params = [], hyps = [], exit = I};
wenzelm@18744
    53
  fun print _ _ = ();
wenzelm@18744
    54
);
wenzelm@18744
    55
wenzelm@18744
    56
val _ = Context.add_setup Data.init;
wenzelm@18744
    57
wenzelm@18805
    58
fun map_locale f = Data.map (fn {locale, params, hyps, exit} =>
wenzelm@18805
    59
  {locale = Option.map (fn (loc, (view, ctxt)) => (loc, (view, f ctxt))) locale,
wenzelm@18805
    60
    params = params, hyps = hyps, exit = exit});
wenzelm@18805
    61
wenzelm@18767
    62
val locale_of = #locale o Data.get;
wenzelm@18767
    63
val params_of = #params o Data.get;
wenzelm@18767
    64
val hyps_of = #hyps o Data.get;
wenzelm@18805
    65
wenzelm@18805
    66
fun standard ctxt =
wenzelm@18805
    67
  (case #locale (Data.get ctxt) of
wenzelm@18805
    68
    NONE => Drule.standard
wenzelm@18805
    69
  | SOME (_, (_, loc_ctxt)) => ProofContext.export_standard ctxt loc_ctxt);
wenzelm@18744
    70
wenzelm@18767
    71
wenzelm@18823
    72
(* print consts *)
wenzelm@18767
    73
wenzelm@18767
    74
local
wenzelm@18767
    75
wenzelm@18767
    76
fun pretty_var ctxt (x, T) =
wenzelm@18767
    77
  Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
wenzelm@18767
    78
    Pretty.quote (ProofContext.pretty_typ ctxt T)];
wenzelm@18744
    79
wenzelm@18767
    80
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
wenzelm@18767
    81
wenzelm@18767
    82
in
wenzelm@18767
    83
wenzelm@18876
    84
fun pretty_consts ctxt pred cs =
wenzelm@18876
    85
  (case filter pred (params_of ctxt) of
wenzelm@18767
    86
    [] => pretty_vars ctxt "constants" cs
wenzelm@18767
    87
  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
wenzelm@18767
    88
wenzelm@18876
    89
fun print_consts _ _ [] = ()
wenzelm@18876
    90
  | print_consts ctxt pred cs = Pretty.writeln (pretty_consts ctxt pred cs);
wenzelm@18823
    91
wenzelm@18767
    92
end;
wenzelm@18767
    93
wenzelm@18767
    94
wenzelm@18805
    95
(* theory/locale substructures *)
wenzelm@18781
    96
wenzelm@18805
    97
fun transfer thy =
wenzelm@18805
    98
  ProofContext.transfer thy #> map_locale (ProofContext.transfer thy);
wenzelm@18805
    99
wenzelm@18805
   100
fun theory f ctxt = transfer (f (ProofContext.theory_of ctxt)) ctxt;
wenzelm@18781
   101
wenzelm@18781
   102
fun theory_result f ctxt =
wenzelm@18781
   103
  let val (res, thy') = f (ProofContext.theory_of ctxt)
wenzelm@18805
   104
  in (res, transfer thy' ctxt) end;
wenzelm@18805
   105
wenzelm@18805
   106
fun locale_result f ctxt =
wenzelm@18805
   107
  (case locale_of ctxt of
wenzelm@18805
   108
    NONE => error "Local theory: no locale context"
wenzelm@18805
   109
  | SOME (loc, (view, loc_ctxt)) =>
wenzelm@18805
   110
      let
wenzelm@18805
   111
        val (res, loc_ctxt') = f loc_ctxt;
wenzelm@18805
   112
        val thy' = ProofContext.theory_of loc_ctxt';
wenzelm@18805
   113
      in (res, ctxt |> map_locale (K loc_ctxt') |> transfer thy') end);
wenzelm@18805
   114
wenzelm@18805
   115
wenzelm@18805
   116
(* init -- exit *)
wenzelm@18781
   117
wenzelm@18781
   118
fun init_i NONE thy = ProofContext.init thy
wenzelm@18781
   119
  | init_i (SOME loc) thy =
wenzelm@18781
   120
      thy
wenzelm@18781
   121
      |> Locale.init loc
wenzelm@18805
   122
      ||>> ProofContext.inferred_fixes
wenzelm@18805
   123
      |> (fn ((view, params), ctxt) => Data.put
wenzelm@18805
   124
          {locale = SOME (loc, (view, ctxt)),
wenzelm@18781
   125
           params = params,
wenzelm@18781
   126
           hyps = ProofContext.assms_of ctxt,
wenzelm@18781
   127
           exit = Sign.restore_naming thy} ctxt)
wenzelm@18781
   128
      |> theory (Sign.add_path (Sign.base_name loc) #> Sign.no_base_names);
wenzelm@18781
   129
wenzelm@18805
   130
fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
wenzelm@18781
   131
wenzelm@18805
   132
fun exit ctxt = (ctxt, #exit (Data.get ctxt) (ProofContext.theory_of ctxt));
wenzelm@18781
   133
wenzelm@18781
   134
wenzelm@18781
   135
wenzelm@18781
   136
(** local theory **)
wenzelm@18781
   137
wenzelm@18767
   138
(* consts *)
wenzelm@18744
   139
wenzelm@18876
   140
fun consts_restricted pred decls ctxt =
wenzelm@18744
   141
  let
wenzelm@18744
   142
    val thy = ProofContext.theory_of ctxt;
wenzelm@18876
   143
    val params = filter pred (params_of ctxt);
wenzelm@18744
   144
    val ps = map Free params;
wenzelm@18805
   145
    val Ps = map #2 params;
wenzelm@18744
   146
  in
wenzelm@18744
   147
    ctxt
wenzelm@18781
   148
    |> theory (Sign.add_consts_i (decls |> map (fn ((c, T), mx) => (c, Ps ---> T, mx))))
wenzelm@18767
   149
    |> pair (decls |> map (fn ((c, T), _) =>
wenzelm@18767
   150
      Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps)))
wenzelm@18767
   151
  end;
wenzelm@18767
   152
wenzelm@18876
   153
val consts = consts_restricted (K true);
wenzelm@18876
   154
wenzelm@18767
   155
wenzelm@18805
   156
(* fact definitions *)
wenzelm@18767
   157
wenzelm@18767
   158
fun notes kind facts ctxt =
wenzelm@18805
   159
  let
wenzelm@18805
   160
    val attrib = Attrib.attribute_i (ProofContext.theory_of ctxt);
wenzelm@18805
   161
    val facts' = map (apsnd (map (apfst (map (standard ctxt))))) facts;
wenzelm@18805
   162
  in
wenzelm@18805
   163
    ctxt |>
wenzelm@18805
   164
    (case locale_of ctxt of
wenzelm@18805
   165
      NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts'))
wenzelm@18805
   166
    | SOME (loc, view_ctxt) =>
wenzelm@18805
   167
        locale_result (K (apfst #1 (Locale.add_thmss kind loc facts' view_ctxt))))
wenzelm@18805
   168
    ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts))
wenzelm@18805
   169
  end;
wenzelm@18767
   170
wenzelm@18781
   171
fun note (a, ths) ctxt =
wenzelm@18805
   172
  ctxt |> notes PureThy.theoremK [(a, [(ths, [])])] |>> hd;
wenzelm@18767
   173
wenzelm@18767
   174
wenzelm@18767
   175
(* axioms *)
wenzelm@18767
   176
wenzelm@18781
   177
local
wenzelm@18781
   178
wenzelm@18781
   179
fun add_axiom hyps (name, prop) thy =
wenzelm@18767
   180
  let
wenzelm@18781
   181
    val name' = if name = "" then "axiom_" ^ string_of_int (serial ()) else name;
wenzelm@18767
   182
    val frees = rev ([] |> Term.add_frees prop |> fold Term.add_frees hyps);
wenzelm@18767
   183
    val prop' = Term.list_all_free (frees, Logic.list_implies (hyps, prop));
wenzelm@18767
   184
    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
wenzelm@18781
   185
wenzelm@18781
   186
    val cert = Thm.cterm_of thy';
wenzelm@18781
   187
    fun all_polymorphic (x, T) th =
wenzelm@18781
   188
      let val var = cert (Var ((x, 0), #1 (Logic.dest_all (Thm.prop_of th))))
wenzelm@18781
   189
      in ((var, cert (Free (x, T))), Thm.forall_elim var th) end;
wenzelm@18781
   190
    fun implies_polymorphic hyp th = Thm.assume (cert hyp) COMP th;
wenzelm@18767
   191
    val th =
wenzelm@18767
   192
      Thm.get_axiom_i thy' (Sign.full_name thy' name')
wenzelm@18781
   193
      |> fold_map all_polymorphic frees |-> Drule.cterm_instantiate
wenzelm@18781
   194
      |> fold implies_polymorphic hyps
wenzelm@18767
   195
  in (th, thy') end;
wenzelm@18767
   196
wenzelm@18781
   197
in
wenzelm@18781
   198
wenzelm@18805
   199
fun axioms_finish finish = fold_map (fn ((name, atts), props) =>
wenzelm@18805
   200
  fold ProofContext.fix_frees props
wenzelm@18805
   201
  #> (fn ctxt => ctxt
wenzelm@18805
   202
    |> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props))
wenzelm@18805
   203
    |-> (fn ths => note ((name, atts), map (finish ctxt) ths))));
wenzelm@18805
   204
wenzelm@18805
   205
val axioms = axioms_finish (K I);
wenzelm@18744
   206
wenzelm@18744
   207
end;
wenzelm@18781
   208
wenzelm@18781
   209
wenzelm@18805
   210
(* constant definitions *)
wenzelm@18781
   211
wenzelm@18781
   212
local
wenzelm@18781
   213
wenzelm@18805
   214
fun add_def (name, prop) =
wenzelm@18805
   215
  Theory.add_defs_i false [(name, prop)] #> (fn thy =>
wenzelm@18805
   216
    let
wenzelm@18805
   217
      val th = Thm.get_axiom_i thy (Sign.full_name thy name);
wenzelm@18805
   218
      val cert = Thm.cterm_of thy;
wenzelm@18805
   219
      val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free)))
wenzelm@18805
   220
        (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []);
wenzelm@18805
   221
    in (Drule.cterm_instantiate subst th, thy) end);
wenzelm@18781
   222
wenzelm@18781
   223
in
wenzelm@18781
   224
wenzelm@18805
   225
fun def_finish finish (var, spec) ctxt =
wenzelm@18781
   226
  let
wenzelm@18781
   227
    val (x, mx) = var;
wenzelm@18781
   228
    val ((name, atts), rhs) = spec;
wenzelm@18781
   229
    val name' = if name = "" then Thm.def_name x else name;
wenzelm@18876
   230
    val rhs_frees = Term.add_frees rhs [];
wenzelm@18781
   231
  in
wenzelm@18781
   232
    ctxt
wenzelm@18876
   233
    |> consts_restricted (member (op =) rhs_frees) [((x, Term.fastype_of rhs), mx)]
wenzelm@18781
   234
    |-> (fn [lhs] =>
wenzelm@18781
   235
      theory_result (add_def (name', Logic.mk_equals (lhs, rhs)))
wenzelm@18781
   236
      #-> (fn th => fn ctxt' => note ((name', atts), [finish ctxt' lhs th]) ctxt')
wenzelm@18781
   237
      #> apfst (fn (b, [th]) => (lhs, (b, th))))
wenzelm@18781
   238
  end;
wenzelm@18781
   239
wenzelm@18805
   240
val def = def_finish (K (K I));
wenzelm@18805
   241
wenzelm@18781
   242
end;
wenzelm@18781
   243
wenzelm@18781
   244
end;