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