63 prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ |
63 prefix ATP_Translate.fact_prefix (ascii_of name) ^ ": " ^ |
64 commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ |
64 commas (theorems_mentioned_in_proof_term thm) ^ "; " ^ |
65 commas (map (prefix ATP_Translate.const_prefix o ascii_of) |
65 commas (map (prefix ATP_Translate.const_prefix o ascii_of) |
66 (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" |
66 (interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" |
67 in File.append path s end |
67 in File.append path s end |
68 val thms = facts_of thy |> map (snd o snd) |
68 val thms = facts_of thy |> map snd |
69 val _ = map do_thm thms |
69 val _ = map do_thm thms |
70 in () end |
70 in () end |
71 |
71 |
72 fun inference_term [] = NONE |
72 fun inference_term [] = NONE |
73 | inference_term ss = |
73 | inference_term ss = |
98 ATP_Translate.Heavyweight) |
98 ATP_Translate.Heavyweight) |
99 val path = file_name |> Path.explode |
99 val path = file_name |> Path.explode |
100 val _ = File.write path "" |
100 val _ = File.write path "" |
101 val facts0 = facts_of thy |
101 val facts0 = facts_of thy |
102 val facts = |
102 val facts = |
103 facts0 |> map (fn ((_, loc), (_, th)) => |
103 facts0 |> map (fn ((_, loc), th) => |
104 ((Thm.get_name_hint th, loc), prop_of th)) |
104 ((Thm.get_name_hint th, loc), prop_of th)) |
105 val explicit_apply = NONE |
105 val explicit_apply = NONE |
106 val (atp_problem, _, _, _, _, _, _) = |
106 val (atp_problem, _, _, _, _, _, _) = |
107 ATP_Translate.prepare_atp_problem ctxt format |
107 ATP_Translate.prepare_atp_problem ctxt format |
108 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true |
108 ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true |
109 [] @{prop False} facts |
109 [] @{prop False} facts |
110 val infers = |
110 val infers = |
111 facts0 |> map (fn (_, (_, th)) => |
111 facts0 |> map (fn (_, th) => |
112 (fact_name_of (Thm.get_name_hint th), |
112 (fact_name_of (Thm.get_name_hint th), |
113 theorems_mentioned_in_proof_term th)) |
113 theorems_mentioned_in_proof_term th)) |
114 val infers = |
114 val infers = |
115 infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) |
115 infers |> map (apsnd (filter (member (op = o apsnd fst) infers))) |
116 val atp_problem = atp_problem |> add_inferences_to_problem infers |
116 val atp_problem = atp_problem |> add_inferences_to_problem infers |