src/Pure/Isar/isar_thy.ML
author wenzelm
Mon Nov 09 15:34:23 1998 +0100 (1998-11-09 ago)
changeset 5830 95b619c7289b
child 5882 c8096461f5c8
permissions -rw-r--r--
Derived theory operations.
     1 (*  Title:      Pure/Isar/isar_thy.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Derived theory operations.
     6 
     7 TODO:
     8   - add_defs: handle empty name (pure_thy.ML (!?));
     9   - add_constdefs (atomic!);
    10   - have_theorems, have_lemmas;
    11   - load theory;
    12   - 'methods' section (proof macros, ML method defs) (!?);
    13   - now_block: ProofHistory open / close (!?);
    14   - from_facts: attribs, args (!?) (beware of termination!!);
    15 *)
    16 
    17 signature ISAR_THY =
    18 sig
    19   val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    20   val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    21   val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    22   val match_bind: (string * string) list -> ProofHistory.T -> ProofHistory.T
    23   val theorem: string -> Args.src list -> string -> theory -> ProofHistory.T
    24   val lemma: string -> Args.src list -> string -> theory -> ProofHistory.T
    25   val assume: string -> Args.src list -> string list -> ProofHistory.T -> ProofHistory.T
    26   val show: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    27   val have: string -> Args.src list -> string -> ProofHistory.T -> ProofHistory.T
    28   val chain: ProofHistory.T -> ProofHistory.T
    29   val from_facts: string list -> ProofHistory.T -> ProofHistory.T
    30   val begin_block: ProofHistory.T -> ProofHistory.T
    31   val next_block: ProofHistory.T -> ProofHistory.T
    32   val end_block: ProofHistory.T -> ProofHistory.T
    33   val qed_with: bstring option * Args.src list option -> ProofHistory.T -> theory
    34   val qed: ProofHistory.T -> theory
    35   val kill_proof: ProofHistory.T -> theory
    36   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    37   val etac: Method.text -> ProofHistory.T -> ProofHistory.T
    38   val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    39   val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
    40   val trivial_proof: ProofHistory.T -> ProofHistory.T
    41   val default_proof: ProofHistory.T -> ProofHistory.T
    42   val use_mltext: string -> theory option -> theory option
    43   val use_mltext_theory: string -> theory -> theory
    44   val use_setup: string -> theory -> theory
    45   val parse_ast_translation: string -> theory -> theory
    46   val parse_translation: string -> theory -> theory
    47   val print_translation: string -> theory -> theory
    48   val typed_print_translation: string -> theory -> theory
    49   val print_ast_translation: string -> theory -> theory
    50   val token_translation: string -> theory -> theory
    51   val add_oracle: bstring * string -> theory -> theory
    52   val the_theory: string -> unit -> theory
    53   val begin_theory: string * string list -> unit -> theory
    54   val end_theory: theory -> unit
    55 end;
    56 
    57 structure IsarThy: ISAR_THY =
    58 struct
    59 
    60 
    61 (** derived theory and proof operations **)
    62 
    63 (* axioms and defs *)
    64 
    65 fun attributize thy (x, srcs) = (x, map (Attrib.global_attribute thy) srcs);
    66 
    67 fun add_axioms axms thy = PureThy.add_axioms (map (attributize thy) axms) thy;
    68 fun add_defs defs thy = PureThy.add_defs (map (attributize thy) defs) thy;
    69 
    70 
    71 (* context *)
    72 
    73 val fix = ProofHistory.apply o Proof.fix;
    74 
    75 val match_bind = ProofHistory.apply o Proof.match_bind;
    76 
    77 
    78 (* statements *)
    79 
    80 fun global_statement f name tags s thy =
    81   ProofHistory.init (f name (map (Attrib.global_attribute thy) tags) s thy);
    82 
    83 fun local_statement f name tags s = ProofHistory.apply_open (fn state =>
    84   f name (map (Attrib.local_attribute (Proof.theory_of state)) tags) s state);
    85 
    86 val theorem = global_statement Proof.theorem;
    87 val lemma = global_statement Proof.lemma;
    88 val assume = local_statement Proof.assume;
    89 val show = local_statement Proof.show;
    90 val have = local_statement Proof.have;
    91 
    92 
    93 (* forward chaining *)
    94 
    95 val chain = ProofHistory.apply Proof.chain;
    96 
    97 fun from_facts names = ProofHistory.apply (fn state =>
    98   state
    99   |> Proof.from_facts (ProofContext.get_tthmss (Proof.context_of state) names));
   100 
   101 
   102 (* end proof *)
   103 
   104 fun qed_with (alt_name, alt_tags) prf =
   105   let
   106     val state = ProofHistory.current prf;
   107     val thy = Proof.theory_of state;
   108     val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags;
   109     val (thy', (kind, name, tthm)) = Method.qed alt_name alt_atts state;
   110 
   111     val prt_result = Pretty.block
   112       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Attribute.pretty_tthm tthm];
   113   in Pretty.writeln prt_result; thy end;
   114 
   115 val qed = qed_with (None, None);
   116 
   117 val kill_proof = Proof.theory_of o ProofHistory.current;
   118 
   119 
   120 (* blocks *)
   121 
   122 val begin_block = ProofHistory.apply_open Proof.begin_block;
   123 val next_block = ProofHistory.apply Proof.next_block;
   124 
   125 
   126 (* backward steps *)
   127 
   128 val tac = ProofHistory.applys o Method.tac;
   129 val etac = ProofHistory.applys o Method.etac;
   130 val proof = ProofHistory.applys o Method.proof;
   131 val end_block = ProofHistory.applys_close Method.end_block;
   132 val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
   133 val trivial_proof = ProofHistory.applys_close Method.trivial_proof;
   134 val default_proof = ProofHistory.applys_close Method.default_proof;
   135 
   136 
   137 (* use ML text *)
   138 
   139 fun use_mltext txt opt_thy =
   140   let
   141     val save_context = Context.get_context ();
   142     val _ = Context.set_context opt_thy;
   143     val opt_exn = (transform_error (use_text false) txt; None) handle exn => Some exn;
   144     val opt_thy' = Context.get_context ();
   145   in
   146     Context.set_context save_context;
   147     (case opt_exn of
   148       None => opt_thy'
   149     | Some exn => raise exn)
   150   end;
   151 
   152 fun use_mltext_theory txt thy =
   153   (case use_mltext txt (Some thy) of
   154     Some thy' => thy'
   155   | None => error "Missing result ML theory context");
   156 
   157 
   158 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
   159 
   160 fun use_let name body txt =
   161   use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   162 
   163 val use_setup =
   164   use_let "setup: (theory -> theory) list" "Theory.apply setup";
   165 
   166 
   167 (* translation functions *)
   168 
   169 val parse_ast_translation =
   170   use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   171     "Theory.add_trfuns (parse_ast_translation, [], [], [])";
   172 
   173 val parse_translation =
   174   use_let "parse_translation: (string * (term list -> term)) list"
   175     "Theory.add_trfuns ([], parse_translation, [], [])";
   176 
   177 val print_translation =
   178   use_let "print_translation: (string * (term list -> term)) list"
   179     "Theory.add_trfuns ([], [], print_translation, [])";
   180 
   181 val print_ast_translation =
   182   use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   183     "Theory.add_trfuns ([], [], [], print_ast_translation)";
   184 
   185 val typed_print_translation =
   186   use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
   187     "Theory.add_trfunsT typed_print_translation";
   188 
   189 val token_translation =
   190   use_let "token_translation: (string * string * (string -> string * int)) list"
   191     "Theory.add_tokentrfuns token_translation";
   192 
   193 
   194 (* add_oracle *)
   195 
   196 fun add_oracle (name, txt) =
   197   use_let
   198     "oracle: bstring * (Sign.sg * Object.T -> term)"
   199     "Theory.add_oracle oracle"
   200     ("(" ^ quote name ^ ", " ^ txt ^ ")");
   201 
   202 
   203 (* theory init and exit *)
   204 
   205 fun the_theory name () = ThyInfo.theory name;
   206 
   207 fun begin_theory (name, names) () =
   208   PureThy.begin_theory name (map ThyInfo.theory names);
   209 
   210 
   211 fun end_theory thy =
   212   let val thy' = PureThy.end_theory thy in
   213     transform_error ThyInfo.store_theory thy'
   214       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   215   end;
   216 
   217 
   218 end;