src/Pure/Isar/specification.ML
author ballarin
Mon Nov 24 18:04:21 2008 +0100 (2008-11-24)
changeset 28880 f6a547c5dbbf
parent 28877 9ff624bd4fe1
child 28941 128459bd72d2
permissions -rw-r--r--
Enable switching to new locales during session.
wenzelm@18620
     1
(*  Title:      Pure/Isar/specification.ML
wenzelm@18620
     2
    ID:         $Id$
wenzelm@18620
     3
    Author:     Makarius
wenzelm@18620
     4
wenzelm@21036
     5
Derived local theory specifications --- with type-inference and
wenzelm@18810
     6
toplevel polymorphism.
wenzelm@18620
     7
*)
wenzelm@18620
     8
wenzelm@18620
     9
signature SPECIFICATION =
wenzelm@18620
    10
sig
wenzelm@20890
    11
  val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
wenzelm@28080
    12
  val check_specification: (Name.binding * typ option * mixfix) list ->
wenzelm@28084
    13
    (Attrib.binding * term list) list list -> Proof.context ->
wenzelm@28084
    14
    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
wenzelm@28080
    15
  val read_specification: (Name.binding * string option * mixfix) list ->
wenzelm@28084
    16
    (Attrib.binding * string list) list list -> Proof.context ->
wenzelm@28084
    17
    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
wenzelm@28080
    18
  val check_free_specification: (Name.binding * typ option * mixfix) list ->
wenzelm@28084
    19
    (Attrib.binding * term list) list -> Proof.context ->
wenzelm@28084
    20
    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
wenzelm@28080
    21
  val read_free_specification: (Name.binding * string option * mixfix) list ->
wenzelm@28084
    22
    (Attrib.binding * string list) list -> Proof.context ->
wenzelm@28084
    23
    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
wenzelm@28080
    24
  val axiomatization: (Name.binding * typ option * mixfix) list ->
wenzelm@28114
    25
    (Attrib.binding * term list) list -> theory ->
wenzelm@28114
    26
    (term list * (string * thm list) list) * theory
wenzelm@28080
    27
  val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
wenzelm@28114
    28
    (Attrib.binding * string list) list -> theory ->
wenzelm@28114
    29
    (term list * (string * thm list) list) * theory
wenzelm@18954
    30
  val definition:
wenzelm@28084
    31
    (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
wenzelm@28080
    32
    local_theory -> (term * (string * thm)) * local_theory
wenzelm@24927
    33
  val definition_cmd:
wenzelm@28084
    34
    (Name.binding * string option * mixfix) option * (Attrib.binding * string) ->
wenzelm@28080
    35
    local_theory -> (term * (string * thm)) * local_theory
wenzelm@28080
    36
  val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
wenzelm@21532
    37
    local_theory -> local_theory
wenzelm@28080
    38
  val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
wenzelm@24927
    39
    local_theory -> local_theory
wenzelm@24949
    40
  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
wenzelm@24949
    41
  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
wenzelm@28080
    42
  val theorems: string ->
wenzelm@28084
    43
    (Attrib.binding * (thm list * Attrib.src list) list) list ->
wenzelm@28080
    44
    local_theory -> (string * thm list) list * local_theory
wenzelm@26336
    45
  val theorems_cmd: string ->
wenzelm@28084
    46
    (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
wenzelm@28080
    47
    local_theory -> (string * thm list) list * local_theory
wenzelm@24986
    48
  val theorem: string -> Method.text option ->
wenzelm@28084
    49
    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
ballarin@28710
    50
    Element.context_i list -> Element.statement_i ->
berghofe@24452
    51
    bool -> local_theory -> Proof.state
wenzelm@24986
    52
  val theorem_cmd: string -> Method.text option ->
wenzelm@28084
    53
    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
ballarin@28710
    54
    Element.context list -> Element.statement ->
berghofe@24452
    55
    bool -> local_theory -> Proof.state
berghofe@24452
    56
  val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
wenzelm@18620
    57
end;
wenzelm@18620
    58
wenzelm@18620
    59
structure Specification: SPECIFICATION =
wenzelm@18620
    60
struct
wenzelm@18620
    61
ballarin@28880
    62
(* new locales *)
ballarin@28880
    63
ballarin@28880
    64
fun cert_stmt body concl ctxt =
ballarin@28880
    65
  let val (_, _, ctxt', concl') = Locale.cert_context_statement NONE body concl ctxt
ballarin@28880
    66
  in (concl', ctxt') end;
ballarin@28880
    67
fun read_stmt body concl ctxt =
ballarin@28880
    68
  let val (_, _, ctxt', concl') = Locale.read_context_statement NONE body concl ctxt
ballarin@28880
    69
  in (concl', ctxt') end;
ballarin@28880
    70
  
ballarin@28880
    71
fun cert_context_statement x = if !new_locales then Expression.cert_statement x else cert_stmt x;
ballarin@28880
    72
fun read_context_statement x = if !new_locales then Expression.read_statement x else read_stmt x;
wenzelm@21230
    73
wenzelm@20890
    74
(* diagnostics *)
wenzelm@20890
    75
wenzelm@20890
    76
fun print_consts _ _ [] = ()
wenzelm@24986
    77
  | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
wenzelm@20914
    78
wenzelm@19664
    79
wenzelm@18620
    80
(* prepare specification *)
wenzelm@18620
    81
wenzelm@24724
    82
local
wenzelm@24724
    83
wenzelm@24724
    84
fun close_forms ctxt i xs As =
wenzelm@24724
    85
  let
wenzelm@24724
    86
    fun add_free (Free (x, _)) = if Variable.is_fixed ctxt x then I else insert (op =) x
wenzelm@24724
    87
      | add_free _ = I;
wenzelm@24724
    88
wenzelm@24724
    89
    val commons = map #1 xs;
wenzelm@24724
    90
    val _ =
wenzelm@24724
    91
      (case duplicates (op =) commons of [] => ()
wenzelm@24724
    92
      | dups => error ("Duplicate local variables " ^ commas_quote dups));
wenzelm@24724
    93
    val frees = rev ((fold o fold_aterms) add_free As (rev commons));
wenzelm@24848
    94
    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
wenzelm@24724
    95
    val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
wenzelm@24724
    96
wenzelm@24724
    97
    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
wenzelm@24724
    98
      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
wenzelm@24724
    99
      | abs_body lev y (t as Free (x, T)) =
wenzelm@24724
   100
          if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
wenzelm@24724
   101
          else t
wenzelm@24724
   102
      | abs_body _ _ a = a;
wenzelm@24724
   103
    fun close (y, U) B =
wenzelm@24724
   104
      let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
wenzelm@24724
   105
      in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
wenzelm@24724
   106
    fun close_form A =
wenzelm@24724
   107
      let
wenzelm@24724
   108
        val occ_frees = rev (fold_aterms add_free A []);
wenzelm@24724
   109
        val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
wenzelm@24724
   110
      in fold_rev close bounds A end;
wenzelm@24724
   111
  in map close_form As end;
wenzelm@24724
   112
wenzelm@24724
   113
fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
wenzelm@18620
   114
  let
wenzelm@18670
   115
    val thy = ProofContext.theory_of ctxt;
wenzelm@18620
   116
wenzelm@18670
   117
    val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
wenzelm@18670
   118
    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
wenzelm@18620
   119
wenzelm@24724
   120
    val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
wenzelm@24734
   121
    val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
wenzelm@24734
   122
      |> fold Name.declare xs;
wenzelm@24734
   123
    val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
wenzelm@24734
   124
    val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1;
wenzelm@24724
   125
    val specs =
wenzelm@24724
   126
      (if do_close then
wenzelm@24734
   127
        #1 (fold_map
wenzelm@24734
   128
            (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx)
wenzelm@24734
   129
      else Asss')
wenzelm@24724
   130
      |> flat |> burrow (Syntax.check_props params_ctxt);
wenzelm@24724
   131
    val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
wenzelm@24724
   132
wenzelm@28080
   133
    val Ts = specs_ctxt |> fold_map ProofContext.inferred_param xs |> fst;
wenzelm@28080
   134
    val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
wenzelm@24724
   135
    val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
wenzelm@24724
   136
  in ((params, name_atts ~~ specs), specs_ctxt) end;
wenzelm@24724
   137
wenzelm@24724
   138
fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x;
wenzelm@24724
   139
fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x;
wenzelm@18620
   140
wenzelm@24724
   141
in
wenzelm@21370
   142
wenzelm@24724
   143
fun read_specification x = read_spec true x;
wenzelm@24724
   144
fun check_specification x = check_spec true x;
wenzelm@24724
   145
fun read_free_specification vars specs = read_spec false vars [specs];
wenzelm@24724
   146
fun check_free_specification vars specs = check_spec false vars [specs];
wenzelm@24724
   147
wenzelm@24724
   148
end;
wenzelm@18620
   149
wenzelm@18620
   150
wenzelm@28114
   151
(* axiomatization -- within global theory *)
wenzelm@18620
   152
wenzelm@28114
   153
fun gen_axioms do_print prep raw_vars raw_specs thy =
wenzelm@18620
   154
  let
wenzelm@28114
   155
    val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
wenzelm@28114
   156
    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
wenzelm@28114
   157
wenzelm@28114
   158
    (*consts*)
wenzelm@28114
   159
    val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
wenzelm@28114
   160
    val subst = Term.subst_atomic (map Free xs ~~ consts);
wenzelm@28114
   161
wenzelm@28114
   162
    (*axioms*)
wenzelm@28114
   163
    val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
wenzelm@28114
   164
        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
wenzelm@28114
   165
        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
wenzelm@28114
   166
    val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
wenzelm@28114
   167
      (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
wenzelm@26595
   168
    val _ =
wenzelm@26595
   169
      if not do_print then ()
wenzelm@28114
   170
      else print_consts (ProofContext.init thy') (K false) xs;
wenzelm@28114
   171
  in ((consts, facts), thy') end;
wenzelm@18786
   172
wenzelm@26595
   173
val axiomatization = gen_axioms false check_specification;
wenzelm@26595
   174
val axiomatization_cmd = gen_axioms true read_specification;
wenzelm@18620
   175
wenzelm@18786
   176
wenzelm@18786
   177
(* definition *)
wenzelm@18786
   178
wenzelm@26595
   179
fun gen_def do_print prep (raw_var, (raw_a, raw_prop)) lthy =
wenzelm@18786
   180
  let
wenzelm@21705
   181
    val (vars, [((raw_name, atts), [prop])]) =
wenzelm@21705
   182
      fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
wenzelm@21705
   183
    val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
wenzelm@28080
   184
    val name = Name.map_name (Thm.def_name_optional x) raw_name;
wenzelm@28080
   185
    val var =
wenzelm@28080
   186
      (case vars of
wenzelm@28080
   187
        [] => (Name.binding x, NoSyn)
wenzelm@28080
   188
      | [((b, _), mx)] =>
wenzelm@28080
   189
          let
wenzelm@28080
   190
            val y = Name.name_of b;
wenzelm@28080
   191
            val _ = x = y orelse
wenzelm@28080
   192
              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
wenzelm@28080
   193
                Position.str_of (Name.pos_of b));
wenzelm@28080
   194
          in (b, mx) end);
wenzelm@28080
   195
    val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
wenzelm@28080
   196
        (var, ((Name.map_name (suffix "_raw") name, []), rhs));
wenzelm@28080
   197
    val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
haftmann@28703
   198
        ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
wenzelm@18786
   199
wenzelm@21705
   200
    val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
wenzelm@26595
   201
    val _ =
wenzelm@26595
   202
      if not do_print then ()
wenzelm@26595
   203
      else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
wenzelm@28080
   204
  in ((lhs, (def_name, th')), lthy3) end;
wenzelm@18786
   205
wenzelm@26595
   206
val definition = gen_def false check_free_specification;
wenzelm@26595
   207
val definition_cmd = gen_def true read_free_specification;
wenzelm@18786
   208
wenzelm@19080
   209
wenzelm@19080
   210
(* abbreviation *)
wenzelm@19080
   211
wenzelm@26595
   212
fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
wenzelm@19080
   213
  let
wenzelm@21705
   214
    val ((vars, [(_, [prop])]), _) =
wenzelm@21705
   215
      prep (the_list raw_var) [(("", []), [raw_prop])]
wenzelm@24676
   216
        (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
wenzelm@21705
   217
    val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
wenzelm@28080
   218
    val var =
wenzelm@28080
   219
      (case vars of
wenzelm@28080
   220
        [] => (Name.binding x, NoSyn)
wenzelm@28080
   221
      | [((b, _), mx)] =>
wenzelm@28080
   222
          let
wenzelm@28080
   223
            val y = Name.name_of b;
wenzelm@28080
   224
            val _ = x = y orelse
wenzelm@28080
   225
              error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
wenzelm@28080
   226
                Position.str_of (Name.pos_of b));
wenzelm@28080
   227
          in (b, mx) end);
wenzelm@21705
   228
    val lthy' = lthy
wenzelm@24986
   229
      |> ProofContext.set_syntax_mode mode    (* FIXME ?!? *)
wenzelm@28080
   230
      |> LocalTheory.abbrev mode (var, rhs) |> snd
wenzelm@21705
   231
      |> ProofContext.restore_syntax_mode lthy;
wenzelm@24724
   232
wenzelm@26595
   233
    val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
wenzelm@21532
   234
  in lthy' end;
wenzelm@19080
   235
wenzelm@26595
   236
val abbreviation = gen_abbrev false check_free_specification;
wenzelm@26595
   237
val abbreviation_cmd = gen_abbrev true read_free_specification;
wenzelm@19080
   238
wenzelm@19664
   239
wenzelm@21230
   240
(* notation *)
wenzelm@19664
   241
wenzelm@24949
   242
fun gen_notation prep_const add mode args lthy =
wenzelm@25371
   243
  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
wenzelm@19664
   244
wenzelm@24927
   245
val notation = gen_notation (K I);
wenzelm@24927
   246
val notation_cmd = gen_notation ProofContext.read_const;
wenzelm@19664
   247
wenzelm@20914
   248
wenzelm@21036
   249
(* fact statements *)
wenzelm@20914
   250
wenzelm@26345
   251
fun gen_theorems prep_fact prep_att kind raw_facts lthy =
wenzelm@20914
   252
  let
wenzelm@20914
   253
    val attrib = prep_att (ProofContext.theory_of lthy);
wenzelm@20914
   254
    val facts = raw_facts |> map (fn ((name, atts), bs) =>
wenzelm@20914
   255
      ((name, map attrib atts),
wenzelm@26345
   256
        bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
wenzelm@21435
   257
    val (res, lthy') = lthy |> LocalTheory.notes kind facts;
wenzelm@28093
   258
    val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
wenzelm@20914
   259
  in (res, lthy') end;
wenzelm@20914
   260
wenzelm@24927
   261
val theorems = gen_theorems (K I) (K I);
wenzelm@26345
   262
val theorems_cmd = gen_theorems ProofContext.get_fact Attrib.intern_src;
wenzelm@20914
   263
wenzelm@21036
   264
wenzelm@21230
   265
(* complex goal statements *)
wenzelm@21036
   266
wenzelm@21036
   267
local
wenzelm@21036
   268
wenzelm@21450
   269
fun subtract_prems ctxt1 ctxt2 =
wenzelm@21450
   270
  Library.drop (length (Assumption.prems_of ctxt1), Assumption.prems_of ctxt2);
wenzelm@21450
   271
wenzelm@21236
   272
fun prep_statement prep_att prep_stmt elems concl ctxt =
wenzelm@21236
   273
  (case concl of
wenzelm@21236
   274
    Element.Shows shows =>
wenzelm@21230
   275
      let
ballarin@28880
   276
        val (propp, elems_ctxt) = prep_stmt elems (map snd shows) ctxt;
ballarin@28877
   277
        val prems = subtract_prems ctxt elems_ctxt;
wenzelm@21450
   278
        val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
wenzelm@21370
   279
        val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
wenzelm@21450
   280
      in ((prems, stmt, []), goal_ctxt) end
wenzelm@21236
   281
  | Element.Obtains obtains =>
wenzelm@21230
   282
      let
haftmann@28862
   283
        val case_names = obtains |> map_index (fn (i, (b, _)) =>
haftmann@28862
   284
          let val name = Name.name_of b
wenzelm@28080
   285
          in if name = "" then string_of_int (i + 1) else name end);
wenzelm@21236
   286
        val constraints = obtains |> map (fn (_, (vars, _)) =>
ballarin@28710
   287
          Element.Constrains
ballarin@28710
   288
            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
wenzelm@21036
   289
wenzelm@21236
   290
        val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
ballarin@28880
   291
        val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
wenzelm@21236
   292
wenzelm@21236
   293
        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) AutoBind.thesisN;
wenzelm@21036
   294
wenzelm@21236
   295
        fun assume_case ((name, (vars, _)), asms) ctxt' =
wenzelm@21236
   296
          let
wenzelm@28080
   297
            val bs = map fst vars;
wenzelm@28080
   298
            val xs = map Name.name_of bs;
wenzelm@21236
   299
            val props = map fst asms;
wenzelm@28080
   300
            val (Ts, _) = ctxt'
wenzelm@21236
   301
              |> fold Variable.declare_term props
wenzelm@21236
   302
              |> fold_map ProofContext.inferred_param xs;
wenzelm@28080
   303
            val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
wenzelm@21236
   304
          in
wenzelm@28080
   305
            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
wenzelm@21370
   306
            ctxt' |> Variable.auto_fixes asm
wenzelm@21236
   307
            |> ProofContext.add_assms_i Assumption.assume_export
wenzelm@21236
   308
              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
wenzelm@21236
   309
            |>> (fn [(_, [th])] => th)
wenzelm@21236
   310
          end;
wenzelm@21236
   311
wenzelm@21658
   312
        val atts = map (Attrib.internal o K)
wenzelm@21236
   313
          [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
ballarin@28877
   314
        val prems = subtract_prems ctxt elems_ctxt;
wenzelm@28080
   315
        val stmt = [((Name.no_binding, atts), [(thesis, [])])];
wenzelm@21236
   316
wenzelm@21236
   317
        val (facts, goal_ctxt) = elems_ctxt
wenzelm@28080
   318
          |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
wenzelm@21236
   319
          |> fold_map assume_case (obtains ~~ propp)
wenzelm@21435
   320
          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
wenzelm@28080
   321
                [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
wenzelm@21450
   322
      in ((prems, stmt, facts), goal_ctxt) end);
wenzelm@21036
   323
berghofe@24452
   324
structure TheoremHook = GenericDataFun
berghofe@24452
   325
(
berghofe@24452
   326
  type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
berghofe@24452
   327
  val empty = [];
berghofe@24452
   328
  val extend = I;
wenzelm@24464
   329
  fun merge _ hooks : T = Library.merge (eq_snd op =) hooks;
berghofe@24452
   330
);
berghofe@24452
   331
wenzelm@21036
   332
fun gen_theorem prep_att prep_stmt
wenzelm@28858
   333
    kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
wenzelm@21036
   334
  let
wenzelm@28858
   335
    val _ = LocalTheory.affirm lthy;
wenzelm@28858
   336
    val thy = ProofContext.theory_of lthy;
wenzelm@21036
   337
wenzelm@21435
   338
    val attrib = prep_att thy;
wenzelm@21435
   339
    val atts = map attrib raw_atts;
ballarin@28710
   340
    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
wenzelm@21450
   341
    val ((prems, stmt, facts), goal_ctxt) =
ballarin@28880
   342
      prep_statement attrib prep_stmt elems raw_concl lthy;
wenzelm@21036
   343
wenzelm@21036
   344
    fun after_qed' results goal_ctxt' =
wenzelm@21602
   345
      let val results' =
wenzelm@21602
   346
        burrow (map Goal.norm_result o ProofContext.export goal_ctxt' lthy) results
wenzelm@21602
   347
      in
wenzelm@21036
   348
        lthy
wenzelm@21435
   349
        |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
wenzelm@21036
   350
        |> (fn (res, lthy') =>
haftmann@28791
   351
          if Name.is_nothing name andalso null atts then
wenzelm@28093
   352
            (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
wenzelm@28080
   353
          else
wenzelm@28080
   354
            let
wenzelm@28080
   355
              val ([(res_name, _)], lthy'') = lthy'
wenzelm@28080
   356
                |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
wenzelm@28093
   357
              val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
wenzelm@28080
   358
            in lthy'' end)
wenzelm@21036
   359
        |> after_qed results'
wenzelm@21036
   360
      end;
wenzelm@21036
   361
  in
wenzelm@21036
   362
    goal_ctxt
wenzelm@28080
   363
    |> ProofContext.note_thmss_i Thm.assumptionK
wenzelm@28080
   364
      [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
wenzelm@21450
   365
    |> snd
wenzelm@21435
   366
    |> Proof.theorem_i before_qed after_qed' (map snd stmt)
wenzelm@24557
   367
    |> Proof.refine_insert facts
wenzelm@24542
   368
    |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
wenzelm@21036
   369
  end;
wenzelm@21036
   370
wenzelm@21230
   371
in
wenzelm@21230
   372
ballarin@28880
   373
val theorem = gen_theorem (K I) cert_context_statement;
ballarin@28880
   374
val theorem_cmd = gen_theorem Attrib.intern_src read_context_statement;
wenzelm@21036
   375
berghofe@24452
   376
fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
berghofe@24452
   377
wenzelm@18620
   378
end;
wenzelm@21036
   379
wenzelm@21036
   380
end;