65 val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1 |
65 val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1 |
66 val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth |
66 val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth |
67 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
67 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
68 in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end |
68 in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end |
69 |
69 |
|
70 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u] |
|
71 | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t |
|
72 | add_vars_and_frees (t as Var _) = insert (op =) t |
|
73 | add_vars_and_frees (t as Free _) = insert (op =) t |
|
74 | add_vars_and_frees _ = I |
|
75 |
70 fun introduce_lam_wrappers ctxt th = |
76 fun introduce_lam_wrappers ctxt th = |
71 if Meson_Clausify.is_quasi_lambda_free (prop_of th) then |
77 if Meson_Clausify.is_quasi_lambda_free (prop_of th) then |
72 th |
78 th |
73 else |
79 else |
74 let |
80 let |
75 fun conv wrap ctxt ct = |
81 val thy = Proof_Context.theory_of ctxt |
|
82 fun conv first ctxt ct = |
76 if Meson_Clausify.is_quasi_lambda_free (term_of ct) then |
83 if Meson_Clausify.is_quasi_lambda_free (term_of ct) then |
77 Thm.reflexive ct |
84 Thm.reflexive ct |
78 else case term_of ct of |
85 else case term_of ct of |
79 Abs _ => |
86 t as Abs (_, _, u) => |
80 Conv.abs_conv (conv false o snd) ctxt ct |
87 if first then |
81 |> wrap |
88 case add_vars_and_frees u [] of |
82 ? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) |
89 [] => |
|
90 Conv.abs_conv (conv false o snd) ctxt ct |
|
91 |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) |
|
92 | v :: _ => |
|
93 Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v |
|
94 |> cterm_of thy |
|
95 |> Conv.comb_conv (conv true ctxt) |
|
96 else |
|
97 Conv.abs_conv (conv false o snd) ctxt ct |
|
98 | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct |
83 | _ => Conv.comb_conv (conv true ctxt) ct |
99 | _ => Conv.comb_conv (conv true ctxt) ct |
84 val eqth = conv true ctxt (cprop_of th) |
100 val eq_th = conv true ctxt (cprop_of th) |
85 in Thm.equal_elim eqth th end |
101 (* We replace the equation's left-hand side with a beta-equivalent term |
|
102 so that "Thm.equal_elim" works below. *) |
|
103 val t0 $ _ $ t2 = prop_of eq_th |
|
104 val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy |
|
105 val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1)) |
|
106 in Thm.equal_elim eq_th' th end |
86 |
107 |
87 val clause_params = |
108 val clause_params = |
88 {ordering = Metis_KnuthBendixOrder.default, |
109 {ordering = Metis_KnuthBendixOrder.default, |
89 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
110 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
90 orderTerms = true} |
111 orderTerms = true} |
102 (* Main function to start Metis proof and reconstruction *) |
123 (* Main function to start Metis proof and reconstruction *) |
103 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
124 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
104 let val thy = Proof_Context.theory_of ctxt |
125 let val thy = Proof_Context.theory_of ctxt |
105 val new_skolemizer = |
126 val new_skolemizer = |
106 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
127 Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
107 val preproc = |
128 val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt |
108 Drule.eta_contraction_rule |
|
109 #> lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt |
|
110 val cls = cls |> map preproc |
|
111 val ths0 = ths0 |> map preproc |
|
112 val th_cls_pairs = |
129 val th_cls_pairs = |
113 map2 (fn j => fn th => |
130 map2 (fn j => fn th => |
114 (Thm.get_name_hint th, |
131 (Thm.get_name_hint th, |
115 Meson_Clausify.cnf_axiom ctxt new_skolemizer |
132 th |> Drule.eta_contraction_rule |
116 (lam_trans = combinatorsN) j th)) |
133 |> Meson_Clausify.cnf_axiom ctxt new_skolemizer |
|
134 (lam_trans = combinatorsN) j |
|
135 ||> map do_lams)) |
117 (0 upto length ths0 - 1) ths0 |
136 (0 upto length ths0 - 1) ths0 |
118 val ths = maps (snd o snd) th_cls_pairs |
137 val ths = maps (snd o snd) th_cls_pairs |
119 val dischargers = map (fst o snd) th_cls_pairs |
138 val dischargers = map (fst o snd) th_cls_pairs |
|
139 val cls = cls |> map (Drule.eta_contraction_rule #> do_lams) |
120 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
140 val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
121 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
141 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
122 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
142 val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
123 val type_enc = type_enc_from_string Sound type_enc |
143 val type_enc = type_enc_from_string Sound type_enc |
124 val (sym_tab, axioms, concealed) = |
144 val (sym_tab, axioms, concealed) = |