equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* An efficient checker for proofs from a SAT solver *} |
5 header {* An efficient checker for proofs from a SAT solver *} |
6 |
6 |
7 theory SatChecker |
7 theory SatChecker |
8 imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL |
8 imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL" |
9 begin |
9 begin |
10 |
10 |
11 section{* General settings and functions for our representation of clauses *} |
11 section{* General settings and functions for our representation of clauses *} |
12 |
12 |
13 subsection{* Types for Literals, Clauses and ProofSteps *} |
13 subsection{* Types for Literals, Clauses and ProofSteps *} |
262 by (elim effect_raiseE) auto |
262 by (elim effect_raiseE) auto |
263 next |
263 next |
264 case (3 l v va r) |
264 case (3 l v va r) |
265 thus ?case |
265 thus ?case |
266 unfolding resolve2.simps |
266 unfolding resolve2.simps |
267 by (fastforce dest!: res_mem simp add: merge_Nil) |
267 by (fastforce dest!: res_mem) |
268 qed |
268 qed |
269 |
269 |
270 lemma res_thm'_Inv: |
270 lemma res_thm'_Inv: |
271 assumes "effect (res_thm' l xs ys) h h' r" |
271 assumes "effect (res_thm' l xs ys) h h' r" |
272 shows "\<exists>l'. (l' \<in> set xs \<and> compl l' \<in> set ys \<and> (l' = compl l \<or> l' = l)) \<and> r = merge (remove1 l' xs) (remove1 (compl l') ys)" |
272 shows "\<exists>l'. (l' \<in> set xs \<and> compl l' \<in> set ys \<and> (l' = compl l \<or> l' = l)) \<and> r = merge (remove1 l' xs) (remove1 (compl l') ys)" |
705 section {* Code generation setup *} |
705 section {* Code generation setup *} |
706 |
706 |
707 code_type ProofStep |
707 code_type ProofStep |
708 (SML "MinisatProofStep.ProofStep") |
708 (SML "MinisatProofStep.ProofStep") |
709 |
709 |
710 code_const ProofDone and Root and Conflict and Delete and Xstep |
710 code_const ProofDone and Root and Conflict and Delete and Xstep |
711 (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))") |
711 (SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))") |
712 |
712 |
713 export_code checker tchecker lchecker in SML |
713 export_code checker tchecker lchecker in SML |
714 |
714 |
715 end |
715 end |
|
716 |