76 val goal = goal_of_thm thy th |
76 val goal = goal_of_thm thy th |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
78 val isar_deps = isar_dependencies_of all_names th |> these |
78 val isar_deps = isar_dependencies_of all_names th |> these |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
80 val mepo_facts = |
80 val mepo_facts = |
81 Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
81 Sledgehammer_MePo.mepo_suggested_facts ctxt params prover |
82 slack_max_facts NONE hyp_ts concl_t facts |
82 slack_max_facts NONE hyp_ts concl_t facts |
83 val mash_facts = facts |> suggested_facts suggs |
83 |> Sledgehammer_MePo.weight_mepo_facts |
|
84 val mash_facts = suggested_facts suggs facts |
84 val mess = [(mepo_facts, []), (mash_facts, [])] |
85 val mess = [(mepo_facts, []), (mash_facts, [])] |
85 val mesh_facts = mesh_facts slack_max_facts mess |
86 val mesh_facts = mesh_facts slack_max_facts mess |
86 val isar_facts = suggested_facts isar_deps facts |
87 val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts |
87 fun prove ok heading facts = |
88 fun prove ok heading get facts = |
88 let |
89 let |
89 val facts = |
90 val facts = |
90 facts |
91 facts |> map get |
91 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t |
92 |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts |
92 |> take (the max_facts) |
93 concl_t |
|
94 |> take (the max_facts) |
93 val res as {outcome, ...} = |
95 val res as {outcome, ...} = |
94 run_prover_for_mash ctxt params prover facts goal |
96 run_prover_for_mash ctxt params prover facts goal |
95 val _ = if is_none outcome then ok := !ok + 1 else () |
97 val _ = if is_none outcome then ok := !ok + 1 else () |
96 in str_of_res heading facts res end |
98 in str_of_res heading facts res end |
97 val mepo_s = prove mepo_ok MePoN mepo_facts |
99 val mepo_s = prove mepo_ok MePoN fst mepo_facts |
98 val mash_s = prove mash_ok MaShN mash_facts |
100 val mash_s = prove mash_ok MaShN fst mash_facts |
99 val mesh_s = prove mesh_ok MeshN mesh_facts |
101 val mesh_s = prove mesh_ok MeshN I mesh_facts |
100 val isar_s = prove isar_ok IsarN isar_facts |
102 val isar_s = prove isar_ok IsarN fst isar_facts |
101 in |
103 in |
102 ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, |
104 ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, |
103 isar_s] |
105 isar_s] |
104 |> cat_lines |> tracing |
106 |> cat_lines |> tracing |
105 end |
107 end |