1 (* Title: HOL/TPTP/ATP_Theory_Export.thy |
1 (* Title: HOL/TPTP/ATP_Theory_Export.thy |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* ATP Theory Exporter *} |
5 section \<open>ATP Theory Exporter\<close> |
6 |
6 |
7 theory ATP_Theory_Export |
7 theory ATP_Theory_Export |
8 imports Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
11 ML_file "atp_theory_export.ML" |
11 ML_file "atp_theory_export.ML" |
12 |
12 |
13 ML {* |
13 ML \<open> |
14 open ATP_Problem |
14 open ATP_Problem |
15 open ATP_Theory_Export |
15 open ATP_Theory_Export |
16 *} |
16 \<close> |
17 |
17 |
18 ML {* |
18 ML \<open> |
19 val do_it = false (* switch to "true" to generate the files *) |
19 val do_it = false (* switch to "true" to generate the files *) |
20 val ctxt = @{context} |
20 val ctxt = @{context} |
21 val thy = @{theory Complex_Main} |
21 val thy = @{theory Complex_Main} |
22 val infer_policy = (* Unchecked_Inferences *) No_Inferences |
22 val infer_policy = (* Unchecked_Inferences *) No_Inferences |
23 *} |
23 \<close> |
24 |
24 |
25 ML {* |
25 ML \<open> |
26 if do_it then |
26 if do_it then |
27 "/tmp/isa_filter" |
27 "/tmp/isa_filter" |
28 |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice)) |
28 |> generate_casc_lbt_isa_files_for_theory ctxt thy (THF (Polymorphic, THF_Without_Choice)) |
29 infer_policy "poly_native_higher" |
29 infer_policy "poly_native_higher" |
30 else |
30 else |
31 () |
31 () |
32 *} |
32 \<close> |
33 |
33 |
34 ML {* |
34 ML \<open> |
35 if do_it then |
35 if do_it then |
36 "/tmp/axs_tc_native.dfg" |
36 "/tmp/axs_tc_native.dfg" |
37 |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) |
37 |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) |
38 infer_policy "tc_native" |
38 infer_policy "tc_native" |
39 else |
39 else |
40 () |
40 () |
41 *} |
41 \<close> |
42 |
42 |
43 ML {* |
43 ML \<open> |
44 if do_it then |
44 if do_it then |
45 "/tmp/infs_poly_guards_query_query.tptp" |
45 "/tmp/infs_poly_guards_query_query.tptp" |
46 |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
46 |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
47 "poly_guards??" |
47 "poly_guards??" |
48 else |
48 else |
49 () |
49 () |
50 *} |
50 \<close> |
51 |
51 |
52 ML {* |
52 ML \<open> |
53 if do_it then |
53 if do_it then |
54 "/tmp/infs_poly_tags_query_query.tptp" |
54 "/tmp/infs_poly_tags_query_query.tptp" |
55 |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
55 |> generate_atp_inference_file_for_theory ctxt thy FOF infer_policy |
56 "poly_tags??" |
56 "poly_tags??" |
57 else |
57 else |
58 () |
58 () |
59 *} |
59 \<close> |
60 |
60 |
61 ML {* |
61 ML \<open> |
62 if do_it then |
62 if do_it then |
63 "/tmp/casc_ltb_isa" |
63 "/tmp/casc_ltb_isa" |
64 |> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy |
64 |> generate_casc_lbt_isa_files_for_theory ctxt thy FOF infer_policy |
65 "poly_tags??" |
65 "poly_tags??" |
66 else |
66 else |
67 () |
67 () |
68 *} |
68 \<close> |
69 |
69 |
70 end |
70 end |