38 val is_literal: term -> bool |
38 val is_literal: term -> bool |
39 val is_clause: term -> bool |
39 val is_clause: term -> bool |
40 val clause_is_trivial: term -> bool |
40 val clause_is_trivial: term -> bool |
41 |
41 |
42 val clause2raw_thm: thm -> thm |
42 val clause2raw_thm: thm -> thm |
|
43 val make_nnf_thm: theory -> term -> thm |
43 |
44 |
44 val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) |
45 val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) |
45 |
46 |
46 val make_cnf_thm: theory -> term -> thm |
47 val make_cnf_thm: Proof.context -> term -> thm |
47 val make_cnfx_thm: theory -> term -> thm |
48 val make_cnfx_thm: Proof.context -> term -> thm |
48 val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *) |
49 val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *) |
49 val cnfx_rewrite_tac: Proof.context -> int -> tactic |
50 val cnfx_rewrite_tac: Proof.context -> int -> tactic |
50 (* converts all prems of a subgoal to (almost) definitional CNF *) |
51 (* converts all prems of a subgoal to (almost) definitional CNF *) |
51 end; |
52 end; |
52 |
53 |
250 in |
251 in |
251 make_nnf_not_not OF [thm1] |
252 make_nnf_not_not OF [thm1] |
252 end |
253 end |
253 | make_nnf_thm thy t = inst_thm thy [t] iff_refl; |
254 | make_nnf_thm thy t = inst_thm thy [t] iff_refl; |
254 |
255 |
|
256 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} |
|
257 val eq_reflection = @{thm eq_reflection} |
|
258 |
|
259 fun make_under_quantifiers ctxt make t = |
|
260 let |
|
261 val thy = ProofContext.theory_of ctxt |
|
262 fun conv ctxt ct = |
|
263 case term_of ct of |
|
264 (t1 as Const _) $ (t2 as Abs _) => |
|
265 Conv.comb_conv (conv ctxt) ct |
|
266 | Abs _ => Conv.abs_conv (conv o snd) ctxt ct |
|
267 | Const _ => Conv.all_conv ct |
|
268 | t => make t RS eq_reflection |
|
269 in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end |
|
270 |
|
271 fun make_nnf_thm_under_quantifiers ctxt = |
|
272 make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt)) |
|
273 |
255 (* ------------------------------------------------------------------------- *) |
274 (* ------------------------------------------------------------------------- *) |
256 (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) |
275 (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) |
257 (* t, but simplified wrt. the following theorems: *) |
276 (* t, but simplified wrt. the following theorems: *) |
258 (* (True & x) = x *) |
277 (* (True & x) = x *) |
259 (* (x & True) = x *) |
278 (* (x & True) = x *) |
321 (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) |
340 (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) |
322 (* is in conjunction normal form. May cause an exponential blowup *) |
341 (* is in conjunction normal form. May cause an exponential blowup *) |
323 (* in the length of the term. *) |
342 (* in the length of the term. *) |
324 (* ------------------------------------------------------------------------- *) |
343 (* ------------------------------------------------------------------------- *) |
325 |
344 |
326 fun make_cnf_thm thy t = |
345 fun make_cnf_thm ctxt t = |
327 let |
346 let |
|
347 val thy = ProofContext.theory_of ctxt |
328 fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = |
348 fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) = |
329 let |
349 let |
330 val thm1 = make_cnf_thm_from_nnf x |
350 val thm1 = make_cnf_thm_from_nnf x |
331 val thm2 = make_cnf_thm_from_nnf y |
351 val thm2 = make_cnf_thm_from_nnf y |
332 in |
352 in |
359 in |
379 in |
360 iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] |
380 iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] |
361 end |
381 end |
362 | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl |
382 | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl |
363 (* convert 't' to NNF first *) |
383 (* convert 't' to NNF first *) |
|
384 val nnf_thm = make_nnf_thm_under_quantifiers ctxt t |
|
385 (*### |
364 val nnf_thm = make_nnf_thm thy t |
386 val nnf_thm = make_nnf_thm thy t |
|
387 *) |
365 val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm |
388 val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm |
366 (* then simplify wrt. True/False (this should preserve NNF) *) |
389 (* then simplify wrt. True/False (this should preserve NNF) *) |
367 val simp_thm = simp_True_False_thm thy nnf |
390 val simp_thm = simp_True_False_thm thy nnf |
368 val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm |
391 val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm |
369 (* finally, convert to CNF (this should preserve the simplification) *) |
392 (* finally, convert to CNF (this should preserve the simplification) *) |
|
393 val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp |
|
394 (* ### |
370 val cnf_thm = make_cnf_thm_from_nnf simp |
395 val cnf_thm = make_cnf_thm_from_nnf simp |
|
396 *) |
371 in |
397 in |
372 iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] |
398 iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] |
373 end; |
399 end; |
374 |
400 |
375 (* ------------------------------------------------------------------------- *) |
401 (* ------------------------------------------------------------------------- *) |
384 (* introduce new (existentially bound) literals. Note: the current *) |
410 (* introduce new (existentially bound) literals. Note: the current *) |
385 (* implementation calls 'make_nnf_thm', causing an exponential blowup *) |
411 (* implementation calls 'make_nnf_thm', causing an exponential blowup *) |
386 (* in the case of nested equivalences. *) |
412 (* in the case of nested equivalences. *) |
387 (* ------------------------------------------------------------------------- *) |
413 (* ------------------------------------------------------------------------- *) |
388 |
414 |
389 fun make_cnfx_thm thy t = |
415 fun make_cnfx_thm ctxt t = |
390 let |
416 let |
|
417 val thy = ProofContext.theory_of ctxt |
391 val var_id = Unsynchronized.ref 0 (* properly initialized below *) |
418 val var_id = Unsynchronized.ref 0 (* properly initialized below *) |
392 fun new_free () = |
419 fun new_free () = |
393 Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) |
420 Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) |
394 fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = |
421 fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm = |
395 let |
422 let |
463 in |
490 in |
464 iff_trans OF [thm1, thm5] |
491 iff_trans OF [thm1, thm5] |
465 end |
492 end |
466 | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl |
493 | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl |
467 (* convert 't' to NNF first *) |
494 (* convert 't' to NNF first *) |
|
495 val nnf_thm = make_nnf_thm_under_quantifiers ctxt t |
|
496 (* ### |
468 val nnf_thm = make_nnf_thm thy t |
497 val nnf_thm = make_nnf_thm thy t |
|
498 *) |
469 val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm |
499 val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm |
470 (* then simplify wrt. True/False (this should preserve NNF) *) |
500 (* then simplify wrt. True/False (this should preserve NNF) *) |
471 val simp_thm = simp_True_False_thm thy nnf |
501 val simp_thm = simp_True_False_thm thy nnf |
472 val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm |
502 val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm |
473 (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *) |
503 (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *) |
481 NONE |
511 NONE |
482 in |
512 in |
483 Int.max (max, the_default 0 idx) |
513 Int.max (max, the_default 0 idx) |
484 end) (OldTerm.term_frees simp) 0) |
514 end) (OldTerm.term_frees simp) 0) |
485 (* finally, convert to definitional CNF (this should preserve the simplification) *) |
515 (* finally, convert to definitional CNF (this should preserve the simplification) *) |
|
516 val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp |
|
517 (*### |
486 val cnfx_thm = make_cnfx_thm_from_nnf simp |
518 val cnfx_thm = make_cnfx_thm_from_nnf simp |
|
519 *) |
487 in |
520 in |
488 iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] |
521 iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] |
489 end; |
522 end; |
490 |
523 |
491 (* ------------------------------------------------------------------------- *) |
524 (* ------------------------------------------------------------------------- *) |
507 |
540 |
508 fun cnf_rewrite_tac ctxt i = |
541 fun cnf_rewrite_tac ctxt i = |
509 (* cut the CNF formulas as new premises *) |
542 (* cut the CNF formulas as new premises *) |
510 Subgoal.FOCUS (fn {prems, ...} => |
543 Subgoal.FOCUS (fn {prems, ...} => |
511 let |
544 let |
512 val thy = ProofContext.theory_of ctxt |
545 val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems |
513 val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems |
|
514 val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) |
546 val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) |
515 in |
547 in |
516 cut_facts_tac cut_thms 1 |
548 cut_facts_tac cut_thms 1 |
517 end) ctxt i |
549 end) ctxt i |
518 (* remove the original premises *) |
550 (* remove the original premises *) |
530 |
562 |
531 fun cnfx_rewrite_tac ctxt i = |
563 fun cnfx_rewrite_tac ctxt i = |
532 (* cut the CNF formulas as new premises *) |
564 (* cut the CNF formulas as new premises *) |
533 Subgoal.FOCUS (fn {prems, ...} => |
565 Subgoal.FOCUS (fn {prems, ...} => |
534 let |
566 let |
535 val thy = ProofContext.theory_of ctxt; |
567 val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems |
536 val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems |
|
537 val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) |
568 val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) |
538 in |
569 in |
539 cut_facts_tac cut_thms 1 |
570 cut_facts_tac cut_thms 1 |
540 end) ctxt i |
571 end) ctxt i |
541 (* remove the original premises *) |
572 (* remove the original premises *) |