src/Pure/Isar/isar_thy.ML
author berghofe
Mon May 17 16:58:34 1999 +0200 (1999-05-17 ago)
changeset 6650 808a3d9e2404
parent 6552 28553eba1913
child 6688 f33c89103fb4
permissions -rw-r--r--
Present.begin_theory now needs an additional argument of type
theory to store information about session identifiers.
     1 (*  Title:      Pure/Isar/isar_thy.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Pure/Isar derived theory operations.
     6 
     7 TODO:
     8   - 'methods' section (proof macros, ML method defs) (!?);
     9   - next_block: ProofHistory open / close (!?);
    10 *)
    11 
    12 signature ISAR_THY =
    13 sig
    14   val add_text: Comment.text -> theory -> theory
    15   val add_title: Comment.text -> Comment.text -> Comment.text -> theory -> theory
    16   val add_chapter: Comment.text -> theory -> theory
    17   val add_section: Comment.text -> theory -> theory
    18   val add_subsection: Comment.text -> theory -> theory
    19   val add_subsubsection: Comment.text -> theory -> theory
    20   val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory
    21   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    22   val add_defs: ((bstring * string) * Args.src list) list -> theory -> theory
    23   val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    24   val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory
    25   val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory
    26   val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list
    27   val apply_theorems_i: (thm * theory attribute list) list -> theory -> theory * thm list
    28   val have_theorems: (bstring * Args.src list) * (xstring * Args.src list) list
    29     -> theory -> theory
    30   val have_theorems_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    31     -> theory -> theory
    32   val have_lemmas: (bstring * Args.src list) * (xstring * Args.src list) list
    33     -> theory -> theory
    34   val have_lemmas_i: (bstring * theory attribute list) * (thm * theory attribute list) list
    35     -> theory -> theory
    36   val have_facts: (string * Args.src list) * (string * Args.src list) list
    37     -> ProofHistory.T -> ProofHistory.T
    38   val have_facts_i: (string * Proof.context attribute list) *
    39     (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    40   val from_facts: (string * Args.src list) list -> ProofHistory.T -> ProofHistory.T
    41   val from_facts_i: (thm * Proof.context attribute list) list -> ProofHistory.T -> ProofHistory.T
    42   val chain: ProofHistory.T -> ProofHistory.T
    43   val fix: (string * string option) list -> ProofHistory.T -> ProofHistory.T
    44   val fix_i: (string * typ) list -> ProofHistory.T -> ProofHistory.T
    45   val match_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T
    46   val match_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T
    47   val theorem: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    48   val theorem_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T
    49   val lemma: string -> Args.src list -> string * string list -> theory -> ProofHistory.T
    50   val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> ProofHistory.T
    51   val assume: string -> Args.src list -> (string * string list) list
    52     -> ProofHistory.T -> ProofHistory.T
    53   val assume_i: string -> Proof.context attribute list -> (term * term list) list
    54     -> ProofHistory.T -> ProofHistory.T
    55   val show: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    56   val show_i: string -> Proof.context attribute list -> term * term list
    57     -> ProofHistory.T -> ProofHistory.T
    58   val have: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    59   val have_i: string -> Proof.context attribute list -> term * term list
    60     -> ProofHistory.T -> ProofHistory.T
    61   val thus: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    62   val thus_i: string -> Proof.context attribute list -> term * term list
    63     -> ProofHistory.T -> ProofHistory.T
    64   val hence: string -> Args.src list -> string * string list -> ProofHistory.T -> ProofHistory.T
    65   val hence_i: string -> Proof.context attribute list -> term * term list
    66     -> ProofHistory.T -> ProofHistory.T
    67   val begin_block: ProofHistory.T -> ProofHistory.T
    68   val next_block: ProofHistory.T -> ProofHistory.T
    69   val end_block: ProofHistory.T -> ProofHistory.T
    70   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
    71   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
    72   val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
    73   val kill_proof: ProofHistory.T -> theory
    74   val global_qed_with: bstring option * Args.src list option -> Method.text option
    75     -> Toplevel.transition -> Toplevel.transition
    76   val global_qed_with_i: bstring option * theory attribute list option -> Method.text option
    77     -> Toplevel.transition -> Toplevel.transition
    78   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    79   val terminal_proof: Method.text -> Toplevel.transition -> Toplevel.transition
    80   val immediate_proof: Toplevel.transition -> Toplevel.transition
    81   val default_proof: Toplevel.transition -> Toplevel.transition
    82   val use_mltext: string -> theory option -> theory option
    83   val use_mltext_theory: string -> theory -> theory
    84   val use_setup: string -> theory -> theory
    85   val parse_ast_translation: string -> theory -> theory
    86   val parse_translation: string -> theory -> theory
    87   val print_translation: string -> theory -> theory
    88   val typed_print_translation: string -> theory -> theory
    89   val print_ast_translation: string -> theory -> theory
    90   val token_translation: string -> theory -> theory
    91   val add_oracle: bstring * string -> theory -> theory
    92   val begin_theory: string -> string list -> (string * bool) list -> theory
    93   val end_theory: theory -> theory
    94   val theory: string * string list * (string * bool) list
    95     -> Toplevel.transition -> Toplevel.transition
    96   val context: string -> Toplevel.transition -> Toplevel.transition
    97   val update_context: string -> Toplevel.transition -> Toplevel.transition
    98 end;
    99 
   100 structure IsarThy: ISAR_THY =
   101 struct
   102 
   103 
   104 (** derived theory and proof operations **)
   105 
   106 (* formal comments *)   (* FIXME dummy *)
   107 
   108 fun add_text _ thy = thy;
   109 fun add_title title author date thy = thy;
   110 val add_chapter = add_text;
   111 val add_section = add_text;
   112 val add_subsection = add_text;
   113 val add_subsubsection = add_text;
   114 
   115 
   116 (* axioms and defs *)
   117 
   118 fun add_axms f args thy =
   119   f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
   120 
   121 val add_axioms = add_axms PureThy.add_axioms;
   122 val add_axioms_i = PureThy.add_axioms_i;
   123 val add_defs = add_axms PureThy.add_defs;
   124 val add_defs_i = PureThy.add_defs_i;
   125 
   126 
   127 (* constdefs *)
   128 
   129 fun gen_add_constdefs consts defs args thy =
   130   thy
   131   |> consts (map fst args)
   132   |> defs (map (fn ((c, _, mx), s) => ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
   133 
   134 val add_constdefs = gen_add_constdefs Theory.add_consts add_defs;
   135 val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i;
   136 
   137 
   138 (* theorems *)
   139 
   140 fun gen_have_thmss get attrib f ((name, more_srcs), th_srcs) x =
   141   f name (map (attrib x) more_srcs)
   142     (map (fn (s, srcs) => (get x s, map (attrib x) srcs)) th_srcs) x;
   143 
   144 fun global_have_thmss x = gen_have_thmss PureThy.get_thms Attrib.global_attribute x;
   145 
   146 fun local_have_thmss x =
   147   gen_have_thmss (ProofContext.get_thms o Proof.context_of)
   148     (Attrib.local_attribute o Proof.theory_of) x;
   149 
   150 fun have_thmss_i f ((name, more_atts), th_atts) =
   151   f name more_atts (map (apfst single) th_atts);
   152 
   153 fun have_lemss name atts = PureThy.have_thmss name (atts @ [Drule.tag_lemma]);
   154 
   155 
   156 fun apply_theorems th_srcs = global_have_thmss PureThy.have_thmss ((None, []), th_srcs);
   157 fun apply_theorems_i th_srcs = have_thmss_i PureThy.have_thmss ((None, []), th_srcs);
   158 val have_theorems = #1 oo global_have_thmss (PureThy.have_thmss o Some);
   159 val have_theorems_i = #1 oo have_thmss_i (PureThy.have_thmss o Some);
   160 val have_lemmas = #1 oo global_have_thmss (have_lemss o Some);
   161 val have_lemmas_i = #1 oo have_thmss_i (have_lemss o Some);
   162 val have_facts = ProofHistory.apply o local_have_thmss Proof.have_thmss;
   163 val have_facts_i = ProofHistory.apply o have_thmss_i Proof.have_thmss;
   164 
   165 
   166 (* forward chaining *)
   167 
   168 val from_facts =
   169   ProofHistory.apply o (Proof.chain oo curry (local_have_thmss Proof.have_thmss) ("", []));
   170 
   171 val from_facts_i =
   172   ProofHistory.apply o (Proof.chain oo curry (have_thmss_i Proof.have_thmss) ("", []));
   173 
   174 val chain = ProofHistory.apply Proof.chain;
   175 
   176 
   177 (* context *)
   178 
   179 val fix = ProofHistory.apply o Proof.fix;
   180 val fix_i = ProofHistory.apply o Proof.fix_i;
   181 val match_bind = ProofHistory.apply o Proof.match_bind;
   182 val match_bind_i = ProofHistory.apply o Proof.match_bind_i;
   183 
   184 
   185 (* statements *)
   186 
   187 fun global_statement f name src s thy =
   188   ProofHistory.init (f name (map (Attrib.global_attribute thy) src) s thy);
   189 
   190 fun global_statement_i f name atts t thy = ProofHistory.init (f name atts t thy);
   191 
   192 fun local_statement do_open f g name src s = ProofHistory.apply_cond_open do_open (fn state =>
   193   f name (map (Attrib.local_attribute (Proof.theory_of state)) src) s (g state));
   194 
   195 fun local_statement_i do_open f g name atts t =
   196   ProofHistory.apply_cond_open do_open (f name atts t o g);
   197 
   198 val theorem   = global_statement Proof.theorem;
   199 val theorem_i = global_statement_i Proof.theorem_i;
   200 val lemma     = global_statement Proof.lemma;
   201 val lemma_i   = global_statement_i Proof.lemma_i;
   202 val assume    = local_statement false Proof.assume I;
   203 val assume_i  = local_statement_i false Proof.assume_i I;
   204 val show      = local_statement true Proof.show I;
   205 val show_i    = local_statement_i true Proof.show_i I;
   206 val have      = local_statement true Proof.have I;
   207 val have_i    = local_statement_i true Proof.have_i I;
   208 val thus      = local_statement true Proof.show Proof.chain;
   209 val thus_i    = local_statement_i true Proof.show_i Proof.chain;
   210 val hence     = local_statement true Proof.have Proof.chain;
   211 val hence_i   = local_statement_i true Proof.have_i Proof.chain;
   212 
   213 
   214 (* blocks *)
   215 
   216 val begin_block = ProofHistory.apply_open Proof.begin_block;
   217 val next_block = ProofHistory.apply Proof.next_block;
   218 val end_block = ProofHistory.apply_close Proof.end_block;
   219 
   220 
   221 (* backward steps *)
   222 
   223 val tac = ProofHistory.applys o Method.tac;
   224 val then_tac = ProofHistory.applys o Method.then_tac;
   225 val proof = ProofHistory.applys o Method.proof;
   226 
   227 
   228 (* local endings *)
   229 
   230 (* FIXME
   231 val print_proof = Toplevel.print oo Toplevel.proof;
   232 *)
   233 val print_proof = Toplevel.proof;
   234 
   235 val local_qed = print_proof o ProofHistory.applys_close o Method.local_qed;
   236 val local_terminal_proof = print_proof o ProofHistory.applys_close o Method.local_terminal_proof;
   237 val local_immediate_proof = print_proof (ProofHistory.applys_close Method.local_immediate_proof);
   238 val local_default_proof = print_proof (ProofHistory.applys_close Method.local_default_proof);
   239 
   240 
   241 (* global endings *)
   242 
   243 val kill_proof = Proof.theory_of o ProofHistory.current;
   244 
   245 fun global_result finish = Toplevel.proof_to_theory (fn prf =>
   246   let
   247     val state = ProofHistory.current prf;
   248     val _ = if Proof.at_bottom state then () else raise Toplevel.UNDEF;
   249     val (thy, {kind, name, thm}) = finish state;
   250 
   251     val prt_result = Pretty.block
   252       [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
   253   in Pretty.writeln prt_result; thy end);
   254 
   255 fun gen_global_qed_with prep_att (alt_name, raw_atts) opt_text state =
   256   let
   257     val thy = Proof.theory_of state;
   258     val alt_atts = apsome (map (prep_att thy)) raw_atts;
   259   in Method.global_qed alt_name alt_atts opt_text state end;
   260 
   261 val global_qed_with = global_result oo gen_global_qed_with Attrib.global_attribute;
   262 val global_qed_with_i = global_result oo gen_global_qed_with (K I);
   263 val global_qed = global_qed_with (None, None);
   264 
   265 val global_terminal_proof = global_result o Method.global_terminal_proof;
   266 val global_immediate_proof = global_result Method.global_immediate_proof;
   267 val global_default_proof = global_result Method.global_default_proof;
   268 
   269 
   270 (* common endings *)
   271 
   272 fun qed opt_text = local_qed opt_text o global_qed opt_text;
   273 fun terminal_proof opt_text = local_terminal_proof opt_text o global_terminal_proof opt_text;
   274 val immediate_proof = local_immediate_proof o global_immediate_proof;
   275 val default_proof = local_default_proof o global_default_proof;
   276 
   277 
   278 (* use ML text *)
   279 
   280 fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);
   281 fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);
   282 
   283 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
   284 
   285 fun use_let name body txt =
   286   use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   287 
   288 val use_setup =
   289   use_let "setup: (theory -> theory) list" "Library.apply setup";
   290 
   291 
   292 (* translation functions *)
   293 
   294 val parse_ast_translation =
   295   use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   296     "Theory.add_trfuns (parse_ast_translation, [], [], [])";
   297 
   298 val parse_translation =
   299   use_let "parse_translation: (string * (term list -> term)) list"
   300     "Theory.add_trfuns ([], parse_translation, [], [])";
   301 
   302 val print_translation =
   303   use_let "print_translation: (string * (term list -> term)) list"
   304     "Theory.add_trfuns ([], [], print_translation, [])";
   305 
   306 val print_ast_translation =
   307   use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
   308     "Theory.add_trfuns ([], [], [], print_ast_translation)";
   309 
   310 val typed_print_translation =
   311   use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
   312     "Theory.add_trfunsT typed_print_translation";
   313 
   314 val token_translation =
   315   use_let "token_translation: (string * string * (string -> string * int)) list"
   316     "Theory.add_tokentrfuns token_translation";
   317 
   318 
   319 (* add_oracle *)
   320 
   321 fun add_oracle (name, txt) =
   322   use_let
   323     "oracle: bstring * (Sign.sg * Object.T -> term)"
   324     "Theory.add_oracle oracle"
   325     ("(" ^ quote name ^ ", " ^ txt ^ ")");
   326 
   327 
   328 (* theory init and exit *)      (* FIXME move? rearrange? *)
   329 
   330 fun begin_theory name parents files =
   331   let
   332     val paths = map (apfst Path.unpack) files;
   333     val thy = ThyInfo.begin_theory name parents paths;
   334   in Present.begin_theory name parents paths thy end;
   335 
   336 
   337 (* FIXME
   338 fun end_theory thy =
   339   let val thy' = PureThy.end_theory thy in
   340     Present.end_theory (PureThy.get_name thy');
   341     transform_error ThyInfo.put_theory thy'
   342       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   343   end;
   344 *)
   345 
   346 fun end_theory thy =
   347   (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
   348 
   349 fun bg_theory (name, parents, files) () = begin_theory name parents files;
   350 fun en_theory thy = (end_theory thy; ());
   351 
   352 fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory;
   353 
   354 
   355 (* context switch *)
   356 
   357 fun switch_theory load s =
   358   Toplevel.init_theory (fn () => (the (#2 (Context.pass None load s)))) (K ());
   359 
   360 val context = switch_theory ThyInfo.use_thy;
   361 val update_context = switch_theory ThyInfo.update_thy;
   362 
   363 
   364 end;