src/Pure/Isar/isar_thy.ML
author ballarin
Fri Apr 02 14:08:30 2004 +0200 (2004-04-02)
changeset 14508 859b11514537
parent 14503 255ad604e08e
child 14528 1457584110ac
permissions -rw-r--r--
Experimental command for instantiation of locales in proof contexts:
instantiate <label>: <loc>
wenzelm@5830
     1
(*  Title:      Pure/Isar/isar_thy.ML
wenzelm@5830
     2
    ID:         $Id$
wenzelm@5830
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8804
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5830
     5
wenzelm@6371
     6
Pure/Isar derived theory operations.
wenzelm@5830
     7
*)
wenzelm@5830
     8
wenzelm@5830
     9
signature ISAR_THY =
wenzelm@5830
    10
sig
wenzelm@12876
    11
  val hide_space: string * xstring list -> theory -> theory
wenzelm@12876
    12
  val hide_space_i: string * string list -> theory -> theory
wenzelm@12876
    13
  val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
wenzelm@12876
    14
  val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
wenzelm@12876
    15
  val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory
wenzelm@12876
    16
  val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory
wenzelm@12876
    17
  val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
wenzelm@12876
    18
  val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
wenzelm@12876
    19
  val theorems: string -> ((bstring * Args.src list) * (xstring * Args.src list) list) list
wenzelm@12713
    20
    -> theory -> theory * (string * thm list) list
wenzelm@12713
    21
  val theorems_i: string ->
wenzelm@12876
    22
    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list
wenzelm@12713
    23
    -> theory -> theory * (string * thm list) list
wenzelm@12713
    24
  val locale_theorems: string -> xstring ->
wenzelm@12876
    25
    ((bstring * Args.src list) * (xstring * Args.src list) list) list
wenzelm@12713
    26
    -> theory -> theory * (bstring * thm list) list
wenzelm@12713
    27
  val locale_theorems_i: string -> string ->
wenzelm@12876
    28
    ((bstring * Proof.context attribute list)
wenzelm@12876
    29
      * (thm list * Proof.context attribute list) list) list
wenzelm@12713
    30
    -> theory -> theory * (string * thm list) list
wenzelm@12713
    31
  val smart_theorems: string -> xstring option ->
wenzelm@12876
    32
    ((bstring * Args.src list) * (xstring * Args.src list) list) list
wenzelm@12713
    33
    -> theory -> theory * (string * thm list) list
wenzelm@12876
    34
  val declare_theorems: xstring option -> (xstring * Args.src list) list -> theory -> theory
wenzelm@6371
    35
  val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
wenzelm@12713
    36
  val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list
wenzelm@12876
    37
  val have_facts: ((string * Args.src list) * (string * Args.src list) list) list
wenzelm@10464
    38
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    39
  val have_facts_i: ((string * Proof.context attribute list) *
wenzelm@12876
    40
    (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    41
  val from_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    42
  val from_facts_i: (thm * Proof.context attribute list) list list
wenzelm@6728
    43
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    44
  val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    45
  val with_facts_i: (thm * Proof.context attribute list) list list
wenzelm@6879
    46
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12929
    47
  val using_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T
wenzelm@12929
    48
  val using_facts_i: (thm * Proof.context attribute list) list list
wenzelm@12929
    49
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    50
  val chain: ProofHistory.T -> ProofHistory.T
ballarin@14508
    51
  val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    52
  val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    53
  val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    54
  val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    55
  val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    56
  val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    57
  val invoke_case_i: string * string option list * Proof.context attribute list
wenzelm@11793
    58
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    59
  val theorem: string -> (bstring * Args.src list) * (string * (string list * string list))
wenzelm@12141
    60
    -> bool -> theory -> ProofHistory.T
wenzelm@12876
    61
  val theorem_i: string -> (bstring * theory attribute list) *
wenzelm@12876
    62
    (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
wenzelm@12957
    63
  val multi_theorem: string -> bstring * Args.src list
wenzelm@12957
    64
    -> Args.src Locale.element list
wenzelm@12957
    65
    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12876
    66
    -> bool -> theory -> ProofHistory.T
wenzelm@12957
    67
  val multi_theorem_i: string -> bstring * theory attribute list
wenzelm@12957
    68
    -> Proof.context attribute Locale.element_i list
wenzelm@12957
    69
    -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
wenzelm@12876
    70
    -> bool -> theory -> ProofHistory.T
wenzelm@12957
    71
  val locale_multi_theorem: string -> xstring
wenzelm@12957
    72
    -> bstring * Args.src list -> Args.src Locale.element list
wenzelm@12957
    73
    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12876
    74
    -> bool -> theory -> ProofHistory.T
wenzelm@12957
    75
  val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list
wenzelm@12957
    76
    -> Proof.context attribute Locale.element_i list
wenzelm@12957
    77
    -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
wenzelm@12876
    78
    -> bool -> theory -> ProofHistory.T
wenzelm@12957
    79
  val smart_multi_theorem: string -> xstring Library.option
wenzelm@12957
    80
    -> bstring * Args.src list -> Args.src Locale.element list
wenzelm@12957
    81
    -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12876
    82
    -> bool -> theory -> ProofHistory.T
wenzelm@12876
    83
  val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12141
    84
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    85
  val assume_i:
wenzelm@12876
    86
    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
wenzelm@12876
    87
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    88
  val presume: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12876
    89
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    90
  val presume_i:
wenzelm@12876
    91
    ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
wenzelm@12141
    92
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    93
  val have: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12141
    94
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    95
  val have_i: ((string * Proof.context attribute list) *
wenzelm@12876
    96
    (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    97
  val hence: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12141
    98
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
    99
  val hence_i: ((string * Proof.context attribute list) *
wenzelm@12876
   100
    (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   101
  val show: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12141
   102
    -> bool -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   103
  val show_i: ((string * Proof.context attribute list) *
wenzelm@12876
   104
    (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   105
  val thus: ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12141
   106
    -> bool -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   107
  val thus_i: ((string * Proof.context attribute list)
wenzelm@12876
   108
    * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   109
  val local_def: (string * Args.src list) * (string * (string * string list))
wenzelm@12876
   110
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   111
  val local_def_i: (string * Args.src list) * (string * (term * term list))
wenzelm@12876
   112
    -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   113
  val obtain: (string list * string option) list
wenzelm@12876
   114
    * ((string * Args.src list) * (string * (string list * string list)) list) list
wenzelm@12969
   115
    -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   116
  val obtain_i: (string list * typ option) list
wenzelm@12876
   117
    * ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
wenzelm@12969
   118
    -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   119
  val begin_block: ProofHistory.T -> ProofHistory.T
wenzelm@12876
   120
  val next_block: ProofHistory.T -> ProofHistory.T
wenzelm@12876
   121
  val end_block: ProofHistory.T -> ProofHistory.T
wenzelm@12876
   122
  val defer: int option -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   123
  val prefer: int -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   124
  val apply: Method.text -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   125
  val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   126
  val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
wenzelm@12876
   127
  val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   128
  val terminal_proof: Method.text * Method.text option
wenzelm@6937
   129
    -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   130
  val default_proof: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   131
  val immediate_proof: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   132
  val done_proof: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   133
  val skip_proof: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   134
  val forget_proof: Toplevel.transition -> Toplevel.transition
wenzelm@7012
   135
  val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
wenzelm@12876
   136
  val also: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   137
  val also_i: thm list option -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   138
  val finally: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   139
  val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition
wenzelm@12876
   140
  val moreover: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   141
  val ultimately: Toplevel.transition -> Toplevel.transition
wenzelm@12876
   142
  val parse_ast_translation: string -> theory -> theory
wenzelm@12876
   143
  val parse_translation: string -> theory -> theory
wenzelm@12876
   144
  val print_translation: string -> theory -> theory
wenzelm@12876
   145
  val typed_print_translation: string -> theory -> theory
wenzelm@12876
   146
  val print_ast_translation: string -> theory -> theory
wenzelm@12876
   147
  val token_translation: string -> theory -> theory
wenzelm@12876
   148
  val method_setup: bstring * string * string -> theory -> theory
wenzelm@12876
   149
  val add_oracle: bstring * string -> theory -> theory
wenzelm@13393
   150
  val add_locale: bool * bstring * Locale.expr * Args.src Locale.element list -> theory -> theory
wenzelm@6331
   151
  val begin_theory: string -> string list -> (string * bool) list -> theory
wenzelm@6331
   152
  val end_theory: theory -> theory
wenzelm@7932
   153
  val kill_theory: string -> unit
wenzelm@6246
   154
  val theory: string * string list * (string * bool) list
wenzelm@6246
   155
    -> Toplevel.transition -> Toplevel.transition
wenzelm@7960
   156
  val init_context: ('a -> unit) -> 'a -> Toplevel.transition -> Toplevel.transition
wenzelm@6246
   157
  val context: string -> Toplevel.transition -> Toplevel.transition
wenzelm@5830
   158
end;
wenzelm@5830
   159
wenzelm@5830
   160
structure IsarThy: ISAR_THY =
wenzelm@5830
   161
struct
wenzelm@5830
   162
wenzelm@5830
   163
wenzelm@5830
   164
(** derived theory and proof operations **)
wenzelm@5830
   165
wenzelm@8724
   166
(* name spaces *)
wenzelm@8724
   167
wenzelm@8885
   168
local
wenzelm@8885
   169
wenzelm@8885
   170
val kinds =
wenzelm@10449
   171
 [(Sign.classK, can o Sign.certify_class),
wenzelm@8885
   172
  (Sign.typeK, fn sg => fn c =>
wenzelm@10449
   173
    can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c),
wenzelm@10449
   174
  (Sign.constK, can o Sign.certify_const)];
wenzelm@8724
   175
wenzelm@12876
   176
fun gen_hide intern (kind, xnames) thy =
wenzelm@8885
   177
  (case assoc (kinds, kind) of
wenzelm@8885
   178
    Some check =>
wenzelm@8885
   179
      let
wenzelm@8885
   180
        val sg = Theory.sign_of thy;
wenzelm@8885
   181
        val names = map (intern sg kind) xnames;
wenzelm@8885
   182
        val bads = filter_out (check sg) names;
wenzelm@8885
   183
      in
wenzelm@12589
   184
        if null bads then Theory.hide_space_i true (kind, names) thy
wenzelm@8885
   185
        else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
wenzelm@8885
   186
      end
wenzelm@8885
   187
  | None => error ("Bad name space specification: " ^ quote kind));
wenzelm@8885
   188
wenzelm@8885
   189
in
wenzelm@8885
   190
wenzelm@8885
   191
fun hide_space x = gen_hide Sign.intern x;
wenzelm@8885
   192
fun hide_space_i x = gen_hide (K (K I)) x;
wenzelm@8885
   193
wenzelm@8885
   194
end;
wenzelm@8724
   195
wenzelm@8724
   196
wenzelm@5830
   197
(* axioms and defs *)
wenzelm@5830
   198
wenzelm@5915
   199
fun add_axms f args thy =
wenzelm@5915
   200
  f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
wenzelm@5915
   201
wenzelm@12876
   202
val add_axioms = add_axms (#1 oo PureThy.add_axioms);
wenzelm@12876
   203
val add_axioms_i = #1 oo PureThy.add_axioms_i;
wenzelm@12876
   204
fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args;
wenzelm@12876
   205
fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args;
wenzelm@6371
   206
wenzelm@6371
   207
wenzelm@6371
   208
(* constdefs *)
wenzelm@6371
   209
wenzelm@6371
   210
fun gen_add_constdefs consts defs args thy =
wenzelm@6371
   211
  thy
wenzelm@12876
   212
  |> consts (map fst args)
wenzelm@12876
   213
  |> defs (false, map (fn ((c, _, mx), s) =>
wenzelm@12876
   214
    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
wenzelm@6371
   215
wenzelm@12876
   216
val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
wenzelm@12876
   217
val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
wenzelm@5915
   218
wenzelm@5915
   219
wenzelm@12713
   220
(* attributes *)
wenzelm@12713
   221
wenzelm@12713
   222
local
wenzelm@12713
   223
wenzelm@12713
   224
fun prep_attribs f = map (fn ((name, more_srcs), th_srcs) =>
wenzelm@12713
   225
  ((name, map f more_srcs), map (apsnd (map f)) th_srcs));
wenzelm@12713
   226
wenzelm@12713
   227
in
wenzelm@12713
   228
wenzelm@12713
   229
fun global_attribs thy = prep_attribs (Attrib.global_attribute thy);
wenzelm@12713
   230
fun local_attribs thy = prep_attribs (Attrib.local_attribute thy);
wenzelm@12713
   231
wenzelm@12713
   232
end;
wenzelm@12713
   233
wenzelm@12713
   234
wenzelm@5915
   235
(* theorems *)
wenzelm@5915
   236
wenzelm@12705
   237
local
wenzelm@12705
   238
wenzelm@12713
   239
fun present_thmss kind (thy, named_thmss) =
wenzelm@13529
   240
 (conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
wenzelm@13529
   241
    Context.setmp (Some thy) (Present.results (kind ^ "s")) named_thmss);
wenzelm@13529
   242
  (thy, named_thmss));
wenzelm@5915
   243
wenzelm@12705
   244
in
wenzelm@12705
   245
wenzelm@12876
   246
fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k);
wenzelm@12876
   247
fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc;
wenzelm@5915
   248
wenzelm@12713
   249
fun theorems k args thy = thy
wenzelm@12876
   250
  |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
wenzelm@12713
   251
  |> present_thmss k;
wenzelm@12713
   252
wenzelm@12713
   253
fun locale_theorems k loc args thy = thy
wenzelm@12876
   254
  |> Locale.have_thmss k loc (local_attribs thy args)
wenzelm@12713
   255
  |> present_thmss k;
wenzelm@6371
   256
wenzelm@12713
   257
fun smart_theorems k opt_loc args thy = thy
wenzelm@12713
   258
  |> (case opt_loc of
wenzelm@12876
   259
    None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args)
wenzelm@12876
   260
  | Some loc => Locale.have_thmss k loc (local_attribs thy args))
wenzelm@12713
   261
  |> present_thmss k;
wenzelm@9590
   262
wenzelm@12876
   263
fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)];
wenzelm@9590
   264
wenzelm@12876
   265
fun apply_theorems args = apsnd (flat o map snd) o theorems "" [(("", []), args)];
wenzelm@12876
   266
fun apply_theorems_i args = apsnd (flat o map snd) o theorems_i "" [(("", []), args)];
wenzelm@6371
   267
wenzelm@12705
   268
end;
wenzelm@12705
   269
wenzelm@5915
   270
wenzelm@12713
   271
(* facts and forward chaining *)
wenzelm@6371
   272
wenzelm@12713
   273
fun local_thmss f args state = f (local_attribs (Proof.theory_of state) args) state;
wenzelm@12713
   274
fun local_thmss_i f args = f (map (fn ((name, more_atts), th_atts) =>
wenzelm@12713
   275
  ((name, more_atts), map (apfst single) th_atts)) args);
wenzelm@6371
   276
wenzelm@12713
   277
fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args));
wenzelm@6879
   278
wenzelm@12876
   279
val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss;
wenzelm@12876
   280
val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i;
wenzelm@12876
   281
val from_facts = chain_thmss (local_thmss Proof.have_thmss);
wenzelm@12876
   282
val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i);
wenzelm@12876
   283
val with_facts = chain_thmss (local_thmss Proof.with_thmss);
wenzelm@12876
   284
val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i);
wenzelm@12929
   285
wenzelm@12929
   286
fun using_facts args = ProofHistory.apply (fn state =>
wenzelm@12929
   287
  Proof.using_thmss (map (map (apsnd (map
wenzelm@12929
   288
    (Attrib.local_attribute (Proof.theory_of state))))) args) state);
wenzelm@12929
   289
wenzelm@12929
   290
val using_facts_i = ProofHistory.apply o Proof.using_thmss_i o map (map (apfst single));
wenzelm@12929
   291
wenzelm@12876
   292
val chain = ProofHistory.apply Proof.chain;
wenzelm@5830
   293
ballarin@14508
   294
(* locale instantiation *)
ballarin@14508
   295
ballarin@14508
   296
fun instantiate_locale (prfx, loc) =
ballarin@14508
   297
  ProofHistory.apply (Proof.instantiate_locale (loc, prfx));
wenzelm@5830
   298
wenzelm@5830
   299
(* context *)
wenzelm@5830
   300
wenzelm@12876
   301
val fix = ProofHistory.apply o Proof.fix;
wenzelm@12876
   302
val fix_i = ProofHistory.apply o Proof.fix_i;
wenzelm@12876
   303
val let_bind = ProofHistory.apply o Proof.let_bind;
wenzelm@12876
   304
val let_bind_i = ProofHistory.apply o Proof.let_bind_i;
wenzelm@8450
   305
wenzelm@12876
   306
fun invoke_case (name, xs, src) = ProofHistory.apply (fn state =>
wenzelm@11793
   307
  Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
wenzelm@12876
   308
val invoke_case_i = ProofHistory.apply o Proof.invoke_case;
wenzelm@5830
   309
wenzelm@5830
   310
wenzelm@10935
   311
(* local results *)
wenzelm@10935
   312
wenzelm@10935
   313
local
wenzelm@10935
   314
wenzelm@12244
   315
fun prt_facts ctxt =
wenzelm@13276
   316
  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@13276
   317
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@12244
   318
wenzelm@12244
   319
fun pretty_results ctxt ((kind, ""), facts) =
wenzelm@12244
   320
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts)
wenzelm@12244
   321
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
wenzelm@12244
   322
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
wenzelm@12244
   323
        Pretty.blk (1, Pretty.str "(" :: prt_facts ctxt facts @ [Pretty.str ")"])]);
wenzelm@10935
   324
wenzelm@12055
   325
fun pretty_rule s ctxt thm =
wenzelm@10935
   326
  Pretty.block [Pretty.str (s ^ " to solve goal by exported rule:"),
wenzelm@12055
   327
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@10935
   328
wenzelm@10935
   329
in
wenzelm@10935
   330
wenzelm@12244
   331
val print_result = Pretty.writeln oo pretty_results;
wenzelm@12244
   332
fun print_result' ctxt (k, res) = print_result ctxt ((k, ""), res);
wenzelm@10935
   333
nipkow@13686
   334
fun cond_print_result_rule int = if int
nipkow@13686
   335
  then (print_result',
nipkow@13686
   336
        priority oo (Pretty.string_of oo pretty_rule "Successful attempt"))
wenzelm@12055
   337
  else (K (K ()), K (K ()));
wenzelm@10935
   338
wenzelm@10935
   339
fun proof'' f = Toplevel.proof' (f o cond_print_result_rule);
wenzelm@10935
   340
wenzelm@10935
   341
fun check_goal false state = state
wenzelm@10935
   342
  | check_goal true state =
wenzelm@10935
   343
      let
wenzelm@10935
   344
        val rule = ref (None: thm option);
wenzelm@13529
   345
        fun fail exn =
wenzelm@10935
   346
          (["Problem! Local statement will fail to solve any pending goal"] @
wenzelm@10935
   347
          (case exn of None => [] | Some e => [Toplevel.exn_message e]) @
wenzelm@10935
   348
          (case ! rule of None => [] | Some thm =>
wenzelm@12055
   349
            [Pretty.string_of (pretty_rule "Failed attempt" (Proof.context_of state) thm)]))
wenzelm@13529
   350
          |> cat_lines |> error;
wenzelm@10935
   351
        val check =
wenzelm@12055
   352
          (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
wenzelm@12318
   353
            fn _ => fn thm => rule := Some thm) true state))
wenzelm@11932
   354
          |> Library.setmp proofs 0
wenzelm@10935
   355
          |> Library.transform_error;
wenzelm@10935
   356
        val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
wenzelm@13529
   357
      in (case result of (Some _, None) => () | (_, exn) => fail exn); state end;
wenzelm@12244
   358
wenzelm@10935
   359
end;
wenzelm@10935
   360
wenzelm@10935
   361
wenzelm@5830
   362
(* statements *)
wenzelm@5830
   363
wenzelm@7271
   364
local
wenzelm@7271
   365
wenzelm@12141
   366
fun global_attributes thy ((name, src), s) = ((name, map (Attrib.global_attribute thy) src), s);
wenzelm@12697
   367
fun local_attributes thy ((name, src), s) = ((name, map (Attrib.local_attribute thy) src), s);
wenzelm@12697
   368
fun local_attributes' state = local_attributes (Proof.theory_of state);
wenzelm@6371
   369
wenzelm@12141
   370
fun global_statement f args int thy =
wenzelm@12141
   371
  ProofHistory.init (Toplevel.undo_limit int) (f (map (global_attributes thy) args) thy);
wenzelm@12141
   372
fun global_statement_i f args int thy = ProofHistory.init (Toplevel.undo_limit int) (f args thy);
wenzelm@10935
   373
wenzelm@12141
   374
fun local_statement' f g args int = ProofHistory.apply (fn state =>
wenzelm@12697
   375
  f (map (local_attributes' state) args) int (g state));
wenzelm@12141
   376
fun local_statement_i' f g args int = ProofHistory.apply (f args int o g);
wenzelm@12141
   377
fun local_statement f g args = local_statement' (K o f) g args ();
wenzelm@12141
   378
fun local_statement_i f g args = local_statement_i' (K o f) g args ();
wenzelm@7271
   379
wenzelm@12701
   380
in
wenzelm@12701
   381
wenzelm@12957
   382
fun multi_theorem k a elems concl int thy =
wenzelm@12957
   383
  global_statement (Proof.multi_theorem k None (apsnd (map (Attrib.global_attribute thy)) a)
wenzelm@12957
   384
    (map (Locale.attribute (Attrib.local_attribute thy)) elems)) concl int thy;
wenzelm@12697
   385
wenzelm@12957
   386
fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k None a;
wenzelm@12697
   387
wenzelm@12957
   388
fun locale_multi_theorem k locale (name, atts) elems concl int thy =
wenzelm@12957
   389
  global_statement (Proof.multi_theorem k
wenzelm@12957
   390
      (Some (locale, (map (Attrib.local_attribute thy) atts,
wenzelm@12957
   391
          map (map (Attrib.local_attribute thy) o snd o fst) concl)))
wenzelm@12957
   392
      (name, []) (map (Locale.attribute (Attrib.local_attribute thy)) elems))
wenzelm@12957
   393
      (map (apfst (apsnd (K []))) concl) int thy;
wenzelm@12697
   394
wenzelm@12957
   395
fun locale_multi_theorem_i k locale (name, atts) elems concl =
wenzelm@12957
   396
  global_statement_i (Proof.multi_theorem_i k (Some (locale, (atts, map (snd o fst) concl)))
wenzelm@12957
   397
      (name, []) elems) (map (apfst (apsnd (K []))) concl);
wenzelm@12697
   398
wenzelm@12876
   399
fun theorem k (a, t) = multi_theorem k a [] [(("", []), [t])];
wenzelm@12876
   400
fun theorem_i k (a, t) = multi_theorem_i k a [] [(("", []), [t])];
wenzelm@11742
   401
wenzelm@12957
   402
fun smart_multi_theorem k None a elems = multi_theorem k a elems
wenzelm@12957
   403
  | smart_multi_theorem k (Some locale) a elems = locale_multi_theorem k locale a elems;
wenzelm@11742
   404
wenzelm@12876
   405
val assume      = local_statement Proof.assume I;
wenzelm@12876
   406
val assume_i    = local_statement_i Proof.assume_i I;
wenzelm@12876
   407
val presume     = local_statement Proof.presume I;
wenzelm@12876
   408
val presume_i   = local_statement_i Proof.presume_i I;
wenzelm@12969
   409
val have        = local_statement (Proof.have Seq.single true) I;
wenzelm@12969
   410
val have_i      = local_statement_i (Proof.have_i Seq.single true) I;
wenzelm@12969
   411
val hence       = local_statement (Proof.have Seq.single true) Proof.chain;
wenzelm@12969
   412
val hence_i     = local_statement_i (Proof.have_i Seq.single true) Proof.chain;
wenzelm@12969
   413
val show        = local_statement' (Proof.show check_goal Seq.single true) I;
wenzelm@12969
   414
val show_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) I;
wenzelm@12969
   415
val thus        = local_statement' (Proof.show check_goal Seq.single true) Proof.chain;
wenzelm@12969
   416
val thus_i      = local_statement_i' (Proof.show_i check_goal Seq.single true) Proof.chain;
wenzelm@12141
   417
wenzelm@12141
   418
fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state =>
wenzelm@12141
   419
  f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state);
wenzelm@12141
   420
wenzelm@12876
   421
val local_def = gen_def Proof.def;
wenzelm@12876
   422
val local_def_i = gen_def Proof.def_i;
wenzelm@5830
   423
wenzelm@12969
   424
fun obtain (xs, asms) = proof'' (ProofHistory.applys o (fn print => fn state =>
wenzelm@12969
   425
  Obtain.obtain xs (map (local_attributes' state) asms) print state));
wenzelm@11890
   426
wenzelm@12969
   427
fun obtain_i (xs, asms) = proof'' (ProofHistory.applys o Obtain.obtain_i xs asms);
wenzelm@11890
   428
wenzelm@7271
   429
end;
wenzelm@7271
   430
wenzelm@5830
   431
wenzelm@5830
   432
(* blocks *)
wenzelm@5830
   433
wenzelm@12876
   434
val begin_block = ProofHistory.apply Proof.begin_block;
wenzelm@12876
   435
val next_block = ProofHistory.apply Proof.next_block;
wenzelm@12876
   436
val end_block = ProofHistory.applys Proof.end_block;
wenzelm@5830
   437
wenzelm@5830
   438
wenzelm@8165
   439
(* shuffle state *)
wenzelm@8165
   440
wenzelm@8236
   441
fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain;
wenzelm@8204
   442
wenzelm@12876
   443
fun defer i = ProofHistory.applys (shuffle Method.defer i);
wenzelm@12876
   444
fun prefer i = ProofHistory.applys (shuffle Method.prefer i);
wenzelm@8165
   445
wenzelm@8165
   446
wenzelm@5830
   447
(* backward steps *)
wenzelm@5830
   448
wenzelm@12876
   449
fun apply m = ProofHistory.applys
wenzelm@8881
   450
  (Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward);
wenzelm@12876
   451
fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
wenzelm@12876
   452
val proof = ProofHistory.applys o Method.proof;
wenzelm@6404
   453
wenzelm@6404
   454
wenzelm@6404
   455
(* local endings *)
wenzelm@6404
   456
wenzelm@12876
   457
val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
wenzelm@12876
   458
val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof);
wenzelm@8966
   459
val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof);
wenzelm@6904
   460
val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof);
wenzelm@8966
   461
val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof);
wenzelm@12318
   462
val local_skip_proof = Toplevel.proof' (fn int =>
wenzelm@12318
   463
  ProofHistory.applys (SkipProof.local_skip_proof (cond_print_result_rule int) int));
wenzelm@6404
   464
wenzelm@6404
   465
wenzelm@6404
   466
(* global endings *)
wenzelm@6404
   467
wenzelm@12318
   468
fun global_result finish = Toplevel.proof_to_theory' (fn int => fn prf =>
wenzelm@6404
   469
  let
wenzelm@6404
   470
    val state = ProofHistory.current prf;
wenzelm@6404
   471
    val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
wenzelm@12318
   472
    val (thy, ((kind, name), res)) = finish int state;
wenzelm@11742
   473
  in
wenzelm@11742
   474
    if kind = "" orelse kind = Drule.internalK then ()
wenzelm@12244
   475
    else (print_result (Proof.context_of state) ((kind, name), res);
wenzelm@13529
   476
      Context.setmp (Some thy) (Present.results kind) res);
wenzelm@11742
   477
    thy
wenzelm@11742
   478
  end);
wenzelm@6404
   479
wenzelm@12876
   480
fun global_qed m = global_result (K (Method.global_qed true m));
wenzelm@12876
   481
fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m));
wenzelm@12318
   482
val global_default_proof = global_result (K Method.global_default_proof);
wenzelm@12318
   483
val global_immediate_proof = global_result (K Method.global_immediate_proof);
wenzelm@6888
   484
val global_skip_proof = global_result SkipProof.global_skip_proof;
wenzelm@12318
   485
val global_done_proof = global_result (K Method.global_done_proof);
wenzelm@6404
   486
wenzelm@6404
   487
wenzelm@6404
   488
(* common endings *)
wenzelm@6404
   489
wenzelm@12876
   490
fun qed meth = local_qed meth o global_qed meth;
wenzelm@12876
   491
fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths;
wenzelm@12876
   492
val default_proof = local_default_proof o global_default_proof;
wenzelm@12876
   493
val immediate_proof = local_immediate_proof o global_immediate_proof;
wenzelm@12876
   494
val done_proof = local_done_proof o global_done_proof;
wenzelm@12876
   495
val skip_proof = local_skip_proof o global_skip_proof;
wenzelm@12876
   496
val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
wenzelm@8210
   497
wenzelm@5830
   498
wenzelm@6774
   499
(* calculational proof commands *)
wenzelm@6774
   500
wenzelm@6879
   501
local
wenzelm@6879
   502
wenzelm@12055
   503
fun cond_print_calc int ctxt thms =
wenzelm@12055
   504
  if int then
wenzelm@12055
   505
    Pretty.writeln (Pretty.big_list "calculation:" (map (ProofContext.pretty_thm ctxt) thms))
wenzelm@6774
   506
  else ();
wenzelm@6774
   507
wenzelm@6774
   508
fun proof''' f = Toplevel.proof' (f o cond_print_calc);
wenzelm@6774
   509
wenzelm@12876
   510
fun gen_calc get f args prt state =
wenzelm@12876
   511
  f (apsome (fn srcs => get srcs state) args) prt state;
wenzelm@6879
   512
wenzelm@6879
   513
in
wenzelm@6879
   514
wenzelm@12713
   515
fun get_thmss srcs = Proof.the_facts o local_thmss Proof.have_thmss [(("", []), srcs)];
wenzelm@7012
   516
fun get_thmss_i thms _ = thms;
wenzelm@7012
   517
wenzelm@6879
   518
fun also x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.also x);
wenzelm@6879
   519
fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
wenzelm@6879
   520
fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
wenzelm@6879
   521
fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
wenzelm@12876
   522
val moreover = proof''' (ProofHistory.apply o Calculation.moreover);
wenzelm@12876
   523
val ultimately = proof''' (ProofHistory.apply o Calculation.ultimately);
wenzelm@6879
   524
wenzelm@6879
   525
end;
wenzelm@6774
   526
wenzelm@6774
   527
wenzelm@5830
   528
(* translation functions *)
wenzelm@5830
   529
wenzelm@5830
   530
val parse_ast_translation =
wenzelm@9590
   531
  Context.use_let "val parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
wenzelm@12876
   532
    "Theory.add_trfuns (parse_ast_translation, [], [], [])";
wenzelm@5830
   533
wenzelm@5830
   534
val parse_translation =
wenzelm@9590
   535
  Context.use_let "val parse_translation: (string * (term list -> term)) list"
wenzelm@12876
   536
    "Theory.add_trfuns ([], parse_translation, [], [])";
wenzelm@5830
   537
wenzelm@5830
   538
val print_translation =
wenzelm@9590
   539
  Context.use_let "val print_translation: (string * (term list -> term)) list"
wenzelm@12876
   540
    "Theory.add_trfuns ([], [], print_translation, [])";
wenzelm@5830
   541
wenzelm@5830
   542
val print_ast_translation =
wenzelm@9590
   543
  Context.use_let "val print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
wenzelm@12876
   544
    "Theory.add_trfuns ([], [], [], print_ast_translation)";
wenzelm@5830
   545
wenzelm@5830
   546
val typed_print_translation =
wenzelm@9590
   547
  Context.use_let "val typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
wenzelm@12876
   548
    "Theory.add_trfunsT typed_print_translation";
wenzelm@5830
   549
wenzelm@5830
   550
val token_translation =
berghofe@11717
   551
  Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
wenzelm@12876
   552
    "Theory.add_tokentrfuns token_translation";
wenzelm@5830
   553
wenzelm@5830
   554
wenzelm@9193
   555
(* add method *)
wenzelm@9193
   556
wenzelm@12876
   557
fun method_setup (name, txt, cmt) =
wenzelm@9193
   558
  Context.use_let
wenzelm@9810
   559
    "val thm = PureThy.get_thm_closure (Context.the_context ());\n\
wenzelm@9810
   560
    \val thms = PureThy.get_thms_closure (Context.the_context ());\n\
wenzelm@9810
   561
    \val method: bstring * (Args.src -> Proof.context -> Proof.method) * string"
wenzelm@9193
   562
    "PureIsar.Method.add_method method"
wenzelm@9193
   563
    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")");
wenzelm@9193
   564
wenzelm@9193
   565
wenzelm@5830
   566
(* add_oracle *)
wenzelm@5830
   567
wenzelm@12876
   568
fun add_oracle (name, txt) =
wenzelm@8349
   569
  Context.use_let
wenzelm@9590
   570
    "val oracle: bstring * (Sign.sg * Object.T -> term)"
wenzelm@5830
   571
    "Theory.add_oracle oracle"
wenzelm@5830
   572
    ("(" ^ quote name ^ ", " ^ txt ^ ")");
wenzelm@5830
   573
wenzelm@5830
   574
wenzelm@12062
   575
(* add_locale *)
wenzelm@12062
   576
wenzelm@13393
   577
fun add_locale (do_pred, name, import, body) thy =
wenzelm@13393
   578
  Locale.add_locale do_pred name import
wenzelm@13374
   579
    (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
wenzelm@12062
   580
wenzelm@12062
   581
wenzelm@6688
   582
(* theory init and exit *)
wenzelm@5830
   583
wenzelm@8804
   584
fun gen_begin_theory upd name parents files =
skalberg@14503
   585
  let val ml_filename = Path.pack (ThyLoad.ml_path name);
skalberg@14503
   586
      val () = if exists (equal ml_filename o #1) files
skalberg@14503
   587
               then error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name)
skalberg@14503
   588
               else ()
skalberg@14503
   589
  in ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files) end;
wenzelm@5830
   590
wenzelm@8804
   591
val begin_theory = gen_begin_theory false;
wenzelm@7909
   592
wenzelm@7909
   593
fun end_theory thy =
wenzelm@7932
   594
  if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
wenzelm@7909
   595
  else thy;
wenzelm@7909
   596
wenzelm@7932
   597
val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
wenzelm@6688
   598
wenzelm@7103
   599
wenzelm@8804
   600
fun bg_theory (name, parents, files) int = gen_begin_theory int name parents files;
wenzelm@6331
   601
fun en_theory thy = (end_theory thy; ());
wenzelm@6331
   602
wenzelm@7932
   603
fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name);
wenzelm@6246
   604
wenzelm@6246
   605
wenzelm@6246
   606
(* context switch *)
wenzelm@6246
   607
wenzelm@7960
   608
fun fetch_context f x =
wenzelm@7960
   609
  (case Context.pass None f x of
wenzelm@7960
   610
    ((), None) => raise Toplevel.UNDEF
wenzelm@7960
   611
  | ((), Some thy) => thy);
wenzelm@7960
   612
wenzelm@7960
   613
fun init_context f x = Toplevel.init_theory (fn _ => fetch_context f x) (K ()) (K ());
wenzelm@7953
   614
wenzelm@7953
   615
val context = init_context (ThyInfo.quiet_update_thy true);
wenzelm@6246
   616
wenzelm@5830
   617
wenzelm@5830
   618
end;