src/HOL/TPTP/MaSh_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
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/TPTP/MaSh_Export.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 *)
     4 
     5 section \<open>MaSh Exporter\<close>
     6 
     7 theory MaSh_Export
     8 imports MaSh_Export_Base
     9 begin
    10 
    11 ML \<open>
    12 if do_it then
    13   Isabelle_System.mkdir (Path.explode prefix)
    14 else
    15   ()
    16 \<close>
    17 
    18 ML \<open>
    19 if do_it then
    20   generate_mash_suggestions "nb" @{context} params (range, step) thys max_suggestions
    21     (prefix ^ "mash_nb_suggestions")
    22 else
    23   ()
    24 \<close>
    25 
    26 ML \<open>
    27 if do_it then
    28   generate_mash_suggestions "knn" @{context} params (range, step) thys max_suggestions
    29     (prefix ^ "mash_knn_suggestions")
    30 else
    31   ()
    32 \<close>
    33 
    34 ML \<open>
    35 if do_it then
    36   generate_mepo_suggestions @{context} params (range, step) thys max_suggestions
    37     (prefix ^ "mepo_suggestions")
    38 else
    39   ()
    40 \<close>
    41 
    42 ML \<open>
    43 if do_it then
    44   generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_suggestions")
    45     (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_suggestions")
    46 else
    47   ()
    48 \<close>
    49 
    50 ML \<open>
    51 if do_it then
    52   generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_suggestions")
    53     (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_suggestions")
    54 else
    55   ()
    56 \<close>
    57 
    58 ML \<open>
    59 if do_it then
    60   generate_prover_dependencies @{context} params range thys
    61     (prefix ^ "mash_nb_prover_dependencies")
    62 else
    63   ()
    64 \<close>
    65 
    66 ML \<open>
    67 if do_it then
    68   generate_prover_dependencies @{context} params range thys
    69     (prefix ^ "mash_knn_prover_dependencies")
    70 else
    71   ()
    72 \<close>
    73 
    74 ML \<open>
    75 if do_it then
    76   generate_mesh_suggestions max_suggestions (prefix ^ "mash_nb_prover_suggestions")
    77     (prefix ^ "mepo_suggestions") (prefix ^ "mesh_nb_prover_suggestions")
    78 else
    79   ()
    80 \<close>
    81 
    82 ML \<open>
    83 if do_it then
    84   generate_mesh_suggestions max_suggestions (prefix ^ "mash_knn_prover_suggestions")
    85     (prefix ^ "mepo_suggestions") (prefix ^ "mesh_knn_prover_suggestions")
    86 else
    87   ()
    88 \<close>
    89 
    90 ML \<open>
    91 if do_it then
    92   generate_accessibility @{context} thys (prefix ^ "mash_accessibility")
    93 else
    94   ()
    95 \<close>
    96 
    97 ML \<open>
    98 if do_it then
    99   generate_features @{context} thys (prefix ^ "mash_features")
   100 else
   101   ()
   102 \<close>
   103 
   104 ML \<open>
   105 if do_it then
   106   generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies")
   107 else
   108   ()
   109 \<close>
   110 
   111 ML \<open>
   112 if do_it then
   113   generate_isar_commands @{context} prover (range, step) thys max_suggestions
   114     (prefix ^ "mash_commands")
   115 else
   116   ()
   117 \<close>
   118 
   119 ML \<open>
   120 if do_it then
   121   generate_prover_commands @{context} params (range, step) thys max_suggestions
   122     (prefix ^ "mash_prover_commands")
   123 else
   124   ()
   125 \<close>
   126 
   127 end