equal
deleted
inserted
replaced
12 val flexflex_first_order: thm -> thm |
12 val flexflex_first_order: thm -> thm |
13 val size_of_subgoals: thm -> int |
13 val size_of_subgoals: thm -> int |
14 val too_many_clauses: Proof.context option -> term -> bool |
14 val too_many_clauses: Proof.context option -> term -> bool |
15 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context |
15 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context |
16 val finish_cnf: thm list -> thm list |
16 val finish_cnf: thm list -> thm list |
|
17 val presimplify: thm -> thm |
17 val make_nnf: Proof.context -> thm -> thm |
18 val make_nnf: Proof.context -> thm -> thm |
18 val skolemize: Proof.context -> thm -> thm |
19 val skolemize: Proof.context -> thm -> thm |
19 val is_fol_term: theory -> term -> bool |
20 val is_fol_term: theory -> term -> bool |
20 val make_clauses_unsorted: thm list -> thm list |
21 val make_clauses_unsorted: thm list -> thm list |
21 val make_clauses: thm list -> thm list |
22 val make_clauses: thm list -> thm list |
527 |
528 |
528 val nnf_ss = |
529 val nnf_ss = |
529 HOL_basic_ss addsimps nnf_extra_simps |
530 HOL_basic_ss addsimps nnf_extra_simps |
530 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; |
531 addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; |
531 |
532 |
|
533 val presimplify = |
|
534 rewrite_rule (map safe_mk_meta_eq nnf_simps) |
|
535 #> simplify nnf_ss |
|
536 |
532 fun make_nnf ctxt th = case prems_of th of |
537 fun make_nnf ctxt th = case prems_of th of |
533 [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) |
538 [] => th |> presimplify |
534 |> simplify nnf_ss |
|
535 |> make_nnf1 ctxt |
539 |> make_nnf1 ctxt |
536 | _ => raise THM ("make_nnf: premises in argument", 0, [th]); |
540 | _ => raise THM ("make_nnf: premises in argument", 0, [th]); |
537 |
541 |
538 (*Pull existential quantifiers to front. This accomplishes Skolemization for |
542 (*Pull existential quantifiers to front. This accomplishes Skolemization for |
539 clauses that arise from a subgoal.*) |
543 clauses that arise from a subgoal.*) |