src/HOL/TPTP/ATP_Theory_Export.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
blanchet@46321
     1
(*  Title:      HOL/TPTP/ATP_Theory_Export.thy
blanchet@46321
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@46321
     3
*)
blanchet@46321
     4
wenzelm@63167
     5
section \<open>ATP Theory Exporter\<close>
blanchet@46321
     6
blanchet@46321
     7
theory ATP_Theory_Export
blanchet@51648
     8
imports Complex_Main
blanchet@42602
     9
begin
blanchet@42602
    10
wenzelm@48891
    11
ML_file "atp_theory_export.ML"
wenzelm@48891
    12
wenzelm@63167
    13
ML \<open>
blanchet@48375
    14
open ATP_Problem
blanchet@48375
    15
open ATP_Theory_Export
wenzelm@63167
    16
\<close>
blanchet@45305
    17
wenzelm@63167
    18
ML \<open>
blanchet@51648
    19
val do_it = false (* switch to "true" to generate the files *)
blanchet@42602
    20
val ctxt = @{context}
blanchet@61323
    21
val thy = @{theory Complex_Main}
blanchet@61323
    22
val infer_policy = (* Unchecked_Inferences *) No_Inferences
wenzelm@63167
    23
\<close>
blanchet@61323
    24
wenzelm@63167
    25
ML \<open>
blanchet@61323
    26
if do_it then
blanchet@61323
    27
  "/tmp/isa_filter"
blanchet@61323
    28
  |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice))
blanchet@61323
    29
         infer_policy "poly_native_higher"
blanchet@61323
    30
else
blanchet@61323
    31
  ()
wenzelm@63167
    32
\<close>
blanchet@51648
    33
wenzelm@63167
    34
ML \<open>
blanchet@51648
    35
if do_it then
blanchet@51648
    36
  "/tmp/axs_tc_native.dfg"
blanchet@51648
    37
  |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic)
blanchet@51648
    38
         infer_policy "tc_native"
blanchet@51648
    39
else
blanchet@51648
    40
  ()
wenzelm@63167
    41
\<close>
blanchet@42602
    42
wenzelm@63167
    43
ML \<open>
blanchet@51648
    44
if do_it then
blanchet@51648
    45
  "/tmp/infs_poly_guards_query_query.tptp"
blanchet@51648
    46
  |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
blanchet@51648
    47
         "poly_guards??"
blanchet@51648
    48
else
blanchet@51648
    49
  ()
wenzelm@63167
    50
\<close>
blanchet@48301
    51
wenzelm@63167
    52
ML \<open>
blanchet@51648
    53
if do_it then
blanchet@51648
    54
  "/tmp/infs_poly_tags_query_query.tptp"
blanchet@51648
    55
  |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy
blanchet@51648
    56
         "poly_tags??"
blanchet@51648
    57
else
blanchet@51648
    58
  ()
wenzelm@63167
    59
\<close>
blanchet@51646
    60
wenzelm@63167
    61
ML \<open>
blanchet@51648
    62
if do_it then
blanchet@51648
    63
  "/tmp/casc_ltb_isa"
blanchet@51648
    64
  |> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy
blanchet@51648
    65
         "poly_tags??"
blanchet@51648
    66
else
blanchet@51648
    67
  ()
wenzelm@63167
    68
\<close>
blanchet@43400
    69
blanchet@42602
    70
end