1 (* Title: HOL/Tools/Meson/meson_clausify.ML
2 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
3 Author: Jasmin Blanchette, TU Muenchen
5 Transformation of HOL theorems into CNF forms.
8 signature MESON_CLAUSIFY =
10 val new_skolem_var_prefix : string
11 val new_nonskolem_var_prefix : string
12 val is_zapped_var_name : string -> bool
13 val introduce_combinators_in_cterm : cterm -> thm
14 val introduce_combinators_in_theorem : thm -> thm
15 val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
16 val ss_only : thm list -> simpset
18 Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
21 structure Meson_Clausify : MESON_CLAUSIFY =
26 (* the extra "Meson" helps prevent clashes (FIXME) *)
27 val new_skolem_var_prefix = "MesonSK"
28 val new_nonskolem_var_prefix = "MesonV"
30 fun is_zapped_var_name s =
31 exists (fn prefix => String.isPrefix prefix s)
32 [new_skolem_var_prefix, new_nonskolem_var_prefix]
34 (**** Transformation of Elimination Rules into First-Order Formulas****)
36 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
37 val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
39 (* Converts an elim-rule into an equivalent theorem that does not have the
40 predicate variable. Leaves other theorems unchanged. We simply instantiate
41 the conclusion variable to False. (Cf. "transform_elim_prop" in
42 "Sledgehammer_Util".) *)
43 fun transform_elim_theorem th =
44 case concl_of th of (*conclusion variable*)
45 @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
46 Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
47 | v as Var(_, @{typ prop}) =>
48 Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
52 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
54 fun mk_old_skolem_term_wrapper t =
55 let val T = fastype_of t in
56 Const (@{const_name Meson.skolem}, T --> T) $ t
59 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
60 | beta_eta_in_abs_body t = Envir.beta_eta_contract t
62 (*Traverse a theorem, accumulating Skolem function definitions.*)
63 fun old_skolem_defs th =
65 fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
66 (*Existential: declare a Skolem function, then insert into body and continue*)
68 val args = OldTerm.term_frees body
69 (* Forms a lambda-abstraction over the formal parameters *)
71 list_abs_free (map dest_Free args,
72 HOLogic.choice_const T $ beta_eta_in_abs_body body)
73 |> mk_old_skolem_term_wrapper
74 val comb = list_comb (rhs, args)
75 in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
76 | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss =
77 (*Universal quant: insert a free variable into body and continue*)
78 let val fname = singleton (Name.variant_list (OldTerm.add_term_names (p, []))) a
79 in dec_sko (subst_bound (Free(fname,T), p)) rhss end
80 | dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
81 | dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
82 | dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss
83 | dec_sko _ rhss = rhss
84 in dec_sko (prop_of th) [] end;
87 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
89 fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true
90 | is_quasi_lambda_free (t1 $ t2) =
91 is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
92 | is_quasi_lambda_free (Abs _) = false
93 | is_quasi_lambda_free _ = true
95 val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
96 val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
97 val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
99 (* FIXME: Requires more use of cterm constructors. *)
102 val thy = theory_of_cterm ct
103 val Abs(x,_,body) = term_of ct
104 val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
105 val cxT = ctyp_of thy xT
106 val cbodyT = ctyp_of thy bodyT
108 instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
114 | Var _ => makeK() (*though Var isn't expected*)
115 | Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*)
117 if Term.is_dependent rator then (*C or S*)
118 if Term.is_dependent rand then (*S*)
119 let val crator = cterm_of thy (Abs(x,xT,rator))
120 val crand = cterm_of thy (Abs(x,xT,rand))
121 val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
122 val (_,rhs) = Thm.dest_equals (cprop_of abs_S')
124 Thm.transitive abs_S' (Conv.binop_conv abstract rhs)
127 let val crator = cterm_of thy (Abs(x,xT,rator))
128 val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C}
129 val (_,rhs) = Thm.dest_equals (cprop_of abs_C')
131 Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs)
133 else if Term.is_dependent rand then (*B or eta*)
134 if rand = Bound 0 then Thm.eta_conversion ct
136 let val crand = cterm_of thy (Abs(x,xT,rand))
137 val crator = cterm_of thy rator
138 val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
139 val (_,rhs) = Thm.dest_equals (cprop_of abs_B')
140 in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end
142 | _ => raise Fail "abstract: Bad term"
145 (* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
146 fun introduce_combinators_in_cterm ct =
147 if is_quasi_lambda_free (term_of ct) then
149 else case term_of ct of
152 val (cv, cta) = Thm.dest_abs NONE ct
153 val (v, _) = dest_Free (term_of cv)
154 val u_th = introduce_combinators_in_cterm cta
155 val cu = Thm.rhs_of u_th
156 val comb_eq = abstract (Thm.cabs cv cu)
157 in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
159 let val (ct1, ct2) = Thm.dest_comb ct in
160 Thm.combination (introduce_combinators_in_cterm ct1)
161 (introduce_combinators_in_cterm ct2)
164 fun introduce_combinators_in_theorem th =
165 if is_quasi_lambda_free (prop_of th) then
169 val th = Drule.eta_contraction_rule th
170 val eqth = introduce_combinators_in_cterm (cprop_of th)
171 in Thm.equal_elim eqth th end
172 handle THM (msg, _, _) =>
173 (warning ("Error in the combinator translation of " ^
174 Display.string_of_thm_without_context th ^
175 "\nException message: " ^ msg ^ ".");
176 (* A type variable of sort "{}" will make abstraction fail. *)
179 (*cterms are used throughout for efficiency*)
180 val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop;
182 (*Given an abstraction over n variables, replace the bound variables by free
183 ones. Return the body, along with the list of free variables.*)
184 fun c_variant_abs_multi (ct0, vars) =
185 let val (cv,ct) = Thm.dest_abs NONE ct0
186 in c_variant_abs_multi (ct, cv::vars) end
187 handle CTERM _ => (ct0, rev vars);
189 val skolem_def_raw = @{thms skolem_def_raw}
191 (* Given the definition of a Skolem function, return a theorem to replace
192 an existential formula by a use of that function.
193 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
194 fun old_skolem_theorem_from_def thy rhs0 =
196 val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
197 val rhs' = rhs |> Thm.dest_comb |> snd
198 val (ch, frees) = c_variant_abs_multi (rhs', [])
199 val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
202 Const (_, Type (@{type_name fun}, [_, T])) => T
203 | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
205 val cex = cterm_of thy (HOLogic.exists_const T)
206 val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
208 Drule.list_comb (rhs, frees)
209 |> Drule.beta_conv cabs |> Thm.capply cTrueprop
211 rewrite_goals_tac skolem_def_raw
212 THEN rtac ((prem |> rewrite_rule skolem_def_raw)
213 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
215 Goal.prove_internal [ex_tm] conc tacf
216 |> forall_intr_list frees
217 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
218 |> Thm.varifyT_global
221 fun to_definitional_cnf_with_quantifiers ctxt th =
223 val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
224 val eqth = eqth RS @{thm eq_reflection}
225 val eqth = eqth RS @{thm TruepropI}
226 in Thm.equal_elim eqth th end
228 fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s =
229 (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
230 "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^
231 string_of_int index_no ^ "_" ^ Name.desymbolize false s
233 fun cluster_of_zapped_var_name s =
234 let val get_int = the o Int.fromString o nth (space_explode "_" s) in
235 ((get_int 1, (get_int 2, get_int 3)),
236 String.isPrefix new_skolem_var_prefix s)
239 fun rename_bound_vars_to_be_zapped ax_no =
241 fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
243 (t1 as Const (s, _)) $ Abs (s', T, t') =>
244 if s = @{const_name all} orelse s = @{const_name All} orelse
245 s = @{const_name Ex} then
247 val skolem = (pos = (s = @{const_name Ex}))
248 val (cluster, index_no) =
249 if skolem = cluster_skolem then (cluster, index_no)
250 else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0)
251 val s' = zapped_var_name cluster index_no s'
252 in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end
255 | (t1 as Const (s, _)) $ t2 $ t3 =>
256 if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
257 t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
258 else if s = @{const_name HOL.conj} orelse
259 s = @{const_name HOL.disj} then
260 t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3
263 | (t1 as Const (s, _)) $ t2 =>
264 if s = @{const_name Trueprop} then
265 t1 $ aux cluster index_no pos t2
266 else if s = @{const_name Not} then
267 t1 $ aux cluster index_no (not pos) t2
271 in aux ((ax_no, 0), true) 0 true end
275 |> (case term_of ct of
276 Const (s, _) $ Abs (s', _, _) =>
277 if s = @{const_name all} orelse s = @{const_name All} orelse
278 s = @{const_name Ex} then
279 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
282 | Const (s, _) $ _ $ _ =>
283 if s = @{const_name "==>"} orelse s = @{const_name implies} then
284 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
285 else if s = @{const_name conj} orelse s = @{const_name disj} then
286 Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)
289 | Const (s, _) $ _ =>
290 if s = @{const_name Trueprop} then Conv.arg_conv (zap pos)
291 else if s = @{const_name Not} then Conv.arg_conv (zap (not pos))
293 | _ => Conv.all_conv)
295 fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths
298 @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
299 |> Logic.varify_global
300 |> Skip_Proof.make_thm @{theory}
302 (* Converts an Isabelle theorem into NNF. *)
303 fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt =
305 val thy = Proof_Context.theory_of ctxt
307 th |> transform_elim_theorem
309 |> new_skolemizer ? forall_intr_vars
310 val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
311 val th = th |> Conv.fconv_rule Object_Logic.atomize
312 |> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
313 |> extensionalize_theorem ctxt
316 if new_skolemizer then
318 fun skolemize choice_ths =
319 skolemize_with_choice_theorems ctxt choice_ths
320 #> simplify (ss_only @{thms all_simps[symmetric]})
321 val no_choice = null choice_ths
324 simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]})
327 val discharger_th = th |> pull_out
329 discharger_th |> has_too_many_clauses ctxt (concl_of discharger_th)
330 ? (to_definitional_cnf_with_quantifiers ctxt
333 discharger_th |> prop_of |> rename_bound_vars_to_be_zapped ax_no
334 |> (if no_choice then
335 Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of
340 [] |> Term.add_free_names (prop_of zapped_th)
341 |> filter is_zapped_var_name
342 val ctxt' = ctxt |> Variable.add_fixes_direct fixes
343 val fully_skolemized_t =
344 zapped_th |> singleton (Variable.export ctxt' ctxt)
345 |> cprop_of |> Thm.dest_equals |> snd |> term_of
347 if exists_subterm (fn Var ((s, _), _) =>
348 String.isPrefix new_skolem_var_prefix s
349 | _ => false) fully_skolemized_t then
351 val (fully_skolemized_ct, ctxt) =
352 Variable.import_terms true [fully_skolemized_t] ctxt
353 |>> the_single |>> cterm_of thy
355 (SOME (discharger_th, fully_skolemized_ct),
356 (Thm.assume fully_skolemized_ct, ctxt))
362 (NONE, (th |> has_too_many_clauses ctxt (concl_of th)
363 ? to_definitional_cnf_with_quantifiers ctxt, ctxt))
366 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
367 fun cnf_axiom ctxt0 new_skolemizer ax_no th =
369 val thy = Proof_Context.theory_of ctxt0
370 val choice_ths = choice_theorems thy
371 val (opt, (nnf_th, ctxt)) =
372 nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
374 make_cnf (if new_skolemizer orelse null choice_ths then []
375 else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
377 val (cnf_ths, ctxt) = clausify nnf_th
379 Thm.instantiate ([], map (pairself (cterm_of thy))
380 [(Var (("i", 0), @{typ nat}),
381 HOLogic.mk_nat ax_no)])
382 (zero_var_indexes @{thm skolem_COMBK_D})
383 RS Thm.implies_intr ct th
385 (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
386 ##> (term_of #> HOLogic.dest_Trueprop
387 #> singleton (Variable.export_terms ctxt ctxt0))),
388 cnf_ths |> map (introduce_combinators_in_theorem
389 #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
390 |> Variable.export ctxt ctxt0
392 |> map Thm.close_derivation)
394 handle THM _ => (NONE, [])