equal
deleted
inserted
replaced
16 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context |
16 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context |
17 val finish_cnf: thm list -> thm list |
17 val finish_cnf: thm list -> thm list |
18 val make_nnf: Proof.context -> thm -> thm |
18 val make_nnf: Proof.context -> thm -> thm |
19 val skolemize: Proof.context -> thm -> thm |
19 val skolemize: Proof.context -> thm -> thm |
20 val is_fol_term: theory -> term -> bool |
20 val is_fol_term: theory -> term -> bool |
|
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 |
22 val make_horns: thm list -> thm list |
23 val make_horns: thm list -> thm list |
23 val best_prolog_tac: (thm -> int) -> thm list -> tactic |
24 val best_prolog_tac: (thm -> int) -> thm list -> tactic |
24 val depth_prolog_tac: thm list -> tactic |
25 val depth_prolog_tac: thm list -> tactic |
25 val gocls: thm list -> thm list |
26 val gocls: thm list -> thm list |
558 val (cnfs, ctxt) = make_cnf [] th ctxt0 |
559 val (cnfs, ctxt) = make_cnf [] th ctxt0 |
559 in Variable.export ctxt ctxt0 cnfs @ cls end; |
560 in Variable.export ctxt ctxt0 cnfs @ cls end; |
560 |
561 |
561 (*Make clauses from a list of theorems, previously Skolemized and put into nnf. |
562 (*Make clauses from a list of theorems, previously Skolemized and put into nnf. |
562 The resulting clauses are HOL disjunctions.*) |
563 The resulting clauses are HOL disjunctions.*) |
563 fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []); |
564 fun make_clauses_unsorted ths = fold_rev add_clauses ths []; |
|
565 val make_clauses = sort_clauses o make_clauses_unsorted; |
564 |
566 |
565 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) |
567 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) |
566 fun make_horns ths = |
568 fun make_horns ths = |
567 name_thms "Horn#" |
569 name_thms "Horn#" |
568 (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); |
570 (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); |