154 ? introduce_lam_wrappers ctxt |
154 ? introduce_lam_wrappers ctxt |
155 val th_cls_pairs = |
155 val th_cls_pairs = |
156 map2 (fn j => fn th => |
156 map2 (fn j => fn th => |
157 (Thm.get_name_hint th, |
157 (Thm.get_name_hint th, |
158 th |> Drule.eta_contraction_rule |
158 th |> Drule.eta_contraction_rule |
159 |> Meson_Clausify.cnf_axiom ctxt new_skolem |
159 |> Meson_Clausify.cnf_axiom ctxt new_skolem (lam_trans = combsN) j |
160 (lam_trans = combsN) j |
|
161 ||> map do_lams)) |
160 ||> map do_lams)) |
162 (0 upto length ths0 - 1) ths0 |
161 (0 upto length ths0 - 1) ths0 |
163 val ths = maps (snd o snd) th_cls_pairs |
162 val ths = maps (snd o snd) th_cls_pairs |
164 val dischargers = map (fst o snd) th_cls_pairs |
163 val dischargers = map (fst o snd) th_cls_pairs |
165 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
164 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
166 val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") |
165 val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES") |
167 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
166 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
168 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
167 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
169 val type_enc = type_enc_of_string Strict type_enc |
168 val type_enc = type_enc_of_string Strict type_enc |
170 val (sym_tab, axioms, ord_info, concealed) = |
169 val (sym_tab, axioms, ord_info, concealed) = |
171 prepare_metis_problem ctxt type_enc lam_trans cls ths |
170 generate_metis_problem ctxt type_enc lam_trans cls ths |
172 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
171 fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
173 reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth |
172 reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth |
174 | get_isa_thm mth Isa_Lambda_Lifted = |
173 | get_isa_thm mth Isa_Lambda_Lifted = |
175 lam_lifted_of_metis ctxt type_enc sym_tab concealed mth |
174 lam_lifted_of_metis ctxt type_enc sym_tab concealed mth |
176 | get_isa_thm _ (Isa_Raw ith) = ith |
175 | get_isa_thm _ (Isa_Raw ith) = ith |