149 val thy = Proof_Context.theory_of ctxt |
149 val thy = Proof_Context.theory_of ctxt |
150 |
150 |
151 val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) |
151 val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy) |
152 val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt |
152 val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt |
153 val th_cls_pairs = |
153 val th_cls_pairs = |
154 map2 (fn j => fn th => |
154 map_index (fn (j, th) => |
155 (Thm.get_name_hint th, |
155 (Thm.get_name_hint th, |
156 th |
156 th |
157 |> Drule.eta_contraction_rule |
157 |> Drule.eta_contraction_rule |
158 |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem |
158 |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem |
159 (lam_trans = combsN) j |
159 (lam_trans = combsN) j |
160 ||> map do_lams)) |
160 ||> map do_lams)) |
161 (0 upto length ths0 - 1) ths0 |
161 ths0 |
162 val ths = maps (snd o snd) th_cls_pairs |
162 val ths = maps (snd o snd) th_cls_pairs |
163 val dischargers = map (fst o snd) th_cls_pairs |
163 val dischargers = map (fst o snd) th_cls_pairs |
164 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
164 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
165 val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") |
165 val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") |
166 val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls |
166 val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls |