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