author | wenzelm |
Sat, 23 Apr 2011 13:00:19 +0200 | |
changeset 42463 | f270e3e18be5 |
parent 41413 | 64cd30d6b0b8 |
child 44890 | 22f665a2e91c |
permissions | -rw-r--r-- |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Imperative_HOL/ex/SatChecker.thy |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
3 |
*) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
4 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
5 |
header {* An efficient checker for proofs from a SAT solver *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
6 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
7 |
theory SatChecker |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40671
diff
changeset
|
8 |
imports "~~/src/HOL/Library/RBT_Impl" Sorted_List Imperative_HOL |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
9 |
begin |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
10 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
11 |
section{* General settings and functions for our representation of clauses *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
12 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
13 |
subsection{* Types for Literals, Clauses and ProofSteps *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
14 |
text {* We encode Literals as integers and Clauses as sorted Lists. *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
15 |
|
42463 | 16 |
type_synonym ClauseId = nat |
17 |
type_synonym Lit = int |
|
18 |
type_synonym Clause = "Lit list" |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
19 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
20 |
text {* This resembles exactly to Isat's Proof Steps *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
21 |
|
42463 | 22 |
type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
23 |
datatype ProofStep = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
24 |
ProofDone bool |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
25 |
| Root ClauseId Clause |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
26 |
| Conflict ClauseId Resolvants |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
27 |
| Delete ClauseId |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
28 |
| Xstep ClauseId ClauseId |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
29 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
30 |
subsection{* Interpretation of Literals, Clauses, and an array of Clauses *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
31 |
text {* Specific definitions for Literals as integers *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
32 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
33 |
definition compl :: "Lit \<Rightarrow> Lit" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
34 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
35 |
"compl a = -a" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
36 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
37 |
definition interpLit :: "(nat \<Rightarrow> bool) \<Rightarrow> Lit \<Rightarrow> bool" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
38 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
39 |
"interpLit assgnmt lit = (if lit > 0 then assgnmt (nat lit) else (if (lit < 0) then \<not> (assgnmt (nat (- lit))) else undefined))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
40 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
41 |
lemma interpLit_compl[simp]: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
42 |
assumes lit_not_zero: "lit \<noteq> 0" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
43 |
shows "interpLit a (compl lit) = (\<not> interpLit a lit)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
44 |
unfolding interpLit_def compl_def using lit_not_zero by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
45 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
46 |
lemma compl_compl_is_id[simp]: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
47 |
"compl (compl x) = x" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
48 |
unfolding compl_def by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
49 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
50 |
lemma compl_not_zero[simp]: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
51 |
"(compl x \<noteq> 0) = (x \<noteq> 0)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
52 |
unfolding compl_def by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
53 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
54 |
lemma compl_exists: "\<exists>l'. l = compl l'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
55 |
unfolding compl_def by arith |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
56 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
57 |
text {* Specific definitions for Clauses as sorted lists *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
58 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
59 |
definition interpClause :: "(nat \<Rightarrow> bool) \<Rightarrow> Clause \<Rightarrow> bool" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
60 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
61 |
"interpClause assgnmt cl = (\<exists> l \<in> set cl. interpLit assgnmt l)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
62 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
63 |
lemma interpClause_empty[simp]: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
64 |
"interpClause a [] = False" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
65 |
unfolding interpClause_def by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
66 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
67 |
lemma interpClause_sort[simp]: "interpClause a (sort clause) = interpClause a clause" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
68 |
unfolding interpClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
69 |
by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
70 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
71 |
lemma interpClause_remdups[simp]: "interpClause a (remdups clause) = interpClause a clause" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
72 |
unfolding interpClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
73 |
by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
74 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
75 |
definition |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
76 |
"inconsistent cs = (\<forall>a.\<exists>c\<in>set cs. \<not> interpClause a c)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
77 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
78 |
lemma interpClause_resolvants': |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
79 |
assumes lit_not_zero: "lit \<noteq> 0" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
80 |
assumes resolv_clauses: "lit \<in> cli" "compl lit \<in> clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
81 |
assumes interp: "\<exists>x \<in> cli. interpLit a x" "\<exists>x \<in> clj. interpLit a x" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
82 |
shows "\<exists>x \<in> (cli - {lit} \<union> (clj - {compl lit})). interpLit a x" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
83 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
84 |
from resolv_clauses interp have "(\<exists>l \<in> cli - {lit}. interpLit a l) \<or> interpLit a lit" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
85 |
"(\<exists>l \<in> clj - {compl lit}. interpLit a l) \<or> interpLit a (compl lit)" by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
86 |
with lit_not_zero show ?thesis by (fastsimp simp add: bex_Un) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
87 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
88 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
89 |
lemma interpClause_resolvants: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
90 |
assumes lit_not_zero: "lit \<noteq> 0" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
91 |
assumes sorted_and_distinct: "sorted cli" "distinct cli" "sorted clj" "distinct clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
92 |
assumes resolv_clauses: "lit \<in> set cli" "compl lit \<in> set clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
93 |
assumes interp: "interpClause a cli" "interpClause a clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
94 |
shows "interpClause a (merge (remove lit cli) (remove (compl lit) clj))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
95 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
96 |
from lit_not_zero resolv_clauses interp sorted_and_distinct show ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
97 |
unfolding interpClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
98 |
using interpClause_resolvants' by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
99 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
100 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
101 |
definition correctClause :: "Clause list \<Rightarrow> Clause \<Rightarrow> bool" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
102 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
103 |
"correctClause rootcls cl = (\<forall>a. (\<forall>rcl \<in> set rootcls. interpClause a rcl) \<longrightarrow> (interpClause a cl))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
104 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
105 |
lemma correctClause_resolvants: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
106 |
assumes lit_not_zero: "lit \<noteq> 0" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
107 |
assumes sorted_and_distinct: "sorted cli" "distinct cli" "sorted clj" "distinct clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
108 |
assumes resolv_clauses: "lit \<in> set cli" "compl lit \<in> set clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
109 |
assumes correct: "correctClause r cli" "correctClause r clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
110 |
shows "correctClause r (merge (remove lit cli) (remove (compl lit) clj))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
111 |
using assms interpClause_resolvants unfolding correctClause_def by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
112 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
113 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
114 |
lemma implies_empty_inconsistent: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
115 |
"correctClause cs [] \<Longrightarrow> inconsistent cs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
116 |
unfolding inconsistent_def correctClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
117 |
by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
118 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
119 |
text {* Specific definition for derived clauses in the Array *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
120 |
|
37717 | 121 |
definition |
122 |
array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
123 |
"array_ran a h = {e. Some e \<in> set (Array.get h a)}" |
37717 | 124 |
-- {*FIXME*} |
125 |
||
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
126 |
lemma array_ranI: "\<lbrakk> Some b = Array.get h a ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h" |
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37717
diff
changeset
|
127 |
unfolding array_ran_def Array.length_def by simp |
37717 | 128 |
|
129 |
lemma array_ran_upd_array_Some: |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
130 |
assumes "cl \<in> array_ran a (Array.update a i (Some b) h)" |
37717 | 131 |
shows "cl \<in> array_ran a h \<or> cl = b" |
132 |
proof - |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
133 |
have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert) |
37717 | 134 |
with assms show ?thesis |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
135 |
unfolding array_ran_def Array.update_def by fastsimp |
37717 | 136 |
qed |
137 |
||
138 |
lemma array_ran_upd_array_None: |
|
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
139 |
assumes "cl \<in> array_ran a (Array.update a i None h)" |
37717 | 140 |
shows "cl \<in> array_ran a h" |
141 |
proof - |
|
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
142 |
have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert) |
37717 | 143 |
with assms show ?thesis |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
144 |
unfolding array_ran_def Array.update_def by auto |
37717 | 145 |
qed |
146 |
||
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
147 |
definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
148 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
149 |
"correctArray rootcls a h = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
150 |
(\<forall>cl \<in> array_ran a h. correctClause rootcls cl \<and> sorted cl \<and> distinct cl)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
151 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
152 |
lemma correctArray_update: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
153 |
assumes "correctArray rcs a h" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
154 |
assumes "correctClause rcs c" "sorted c" "distinct c" |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
155 |
shows "correctArray rcs a (Array.update a i (Some c) h)" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
156 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
157 |
unfolding correctArray_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
158 |
by (auto dest:array_ran_upd_array_Some) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
159 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
160 |
lemma correctClause_mono: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
161 |
assumes "correctClause rcs c" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
162 |
assumes "set rcs \<subseteq> set rcs'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
163 |
shows "correctClause rcs' c" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
164 |
using assms unfolding correctClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
165 |
by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
166 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
167 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
168 |
section{* Improved version of SatChecker *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
169 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
170 |
text{* This version just uses a single list traversal. *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
171 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
172 |
subsection{* Function definitions *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
173 |
|
37726 | 174 |
primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
175 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
176 |
"res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" |
37792 | 177 |
| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
178 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
179 |
fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
180 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
181 |
"resolve1 l (x#xs) (y#ys) = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
182 |
(if (x = l) then return (merge xs (y#ys)) |
37792 | 183 |
else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) } |
184 |
else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) } |
|
185 |
else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))" |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
186 |
| "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
187 |
| "resolve1 l xs [] = res_mem l xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
188 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
189 |
fun resolve2 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
190 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
191 |
"resolve2 l (x#xs) (y#ys) = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
192 |
(if (y = l) then return (merge (x#xs) ys) |
37792 | 193 |
else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) } |
194 |
else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) } |
|
195 |
else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))" |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
196 |
| "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
197 |
| "resolve2 l [] ys = res_mem l ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
198 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
199 |
fun res_thm' :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
200 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
201 |
"res_thm' l (x#xs) (y#ys) = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
202 |
(if (x = l \<or> x = compl l) then resolve2 (compl x) xs (y#ys) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
203 |
else (if (y = l \<or> y = compl l) then resolve1 (compl y) (x#xs) ys |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
204 |
else (if (x < y) then (res_thm' l xs (y#ys)) \<guillemotright>= (\<lambda>v. return (x # v)) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
205 |
else (if (x > y) then (res_thm' l (x#xs) ys) \<guillemotright>= (\<lambda>v. return (y # v)) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
206 |
else (res_thm' l xs ys) \<guillemotright>= (\<lambda>v. return (x # v))))))" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
207 |
| "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
208 |
| "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
209 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
210 |
declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del] |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
211 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
212 |
subsection {* Proofs about these functions *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
213 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
214 |
lemma res_mem: |
40671 | 215 |
assumes "effect (res_mem l xs) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
216 |
shows "l \<in> set xs \<and> r = remove1 l xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
217 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
218 |
proof (induct xs arbitrary: r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
219 |
case Nil |
40671 | 220 |
thus ?case unfolding res_mem.simps by (auto elim: effect_raiseE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
221 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
222 |
case (Cons x xs') |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
223 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
224 |
unfolding res_mem.simps |
40671 | 225 |
by (elim effect_raiseE effect_returnE effect_ifE effect_bindE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
226 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
227 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
228 |
lemma resolve1_Inv: |
40671 | 229 |
assumes "effect (resolve1 l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
230 |
shows "l \<in> set xs \<and> r = merge (remove1 l xs) ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
231 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
232 |
proof (induct xs ys arbitrary: r rule: resolve1.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
233 |
case (1 l x xs y ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
234 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
235 |
unfolding resolve1.simps |
40671 | 236 |
by (elim effect_bindE effect_ifE effect_returnE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
237 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
238 |
case (2 l ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
239 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
240 |
unfolding resolve1.simps |
40671 | 241 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
242 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
243 |
case (3 l v va r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
244 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
245 |
unfolding resolve1.simps |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
246 |
by (fastsimp dest!: res_mem) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
247 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
248 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
249 |
lemma resolve2_Inv: |
40671 | 250 |
assumes "effect (resolve2 l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
251 |
shows "l \<in> set ys \<and> r = merge xs (remove1 l ys)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
252 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
253 |
proof (induct xs ys arbitrary: r rule: resolve2.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
254 |
case (1 l x xs y ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
255 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
256 |
unfolding resolve2.simps |
40671 | 257 |
by (elim effect_bindE effect_ifE effect_returnE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
258 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
259 |
case (2 l ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
260 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
261 |
unfolding resolve2.simps |
40671 | 262 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
263 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
264 |
case (3 l v va r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
265 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
266 |
unfolding resolve2.simps |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
267 |
by (fastsimp dest!: res_mem simp add: merge_Nil) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
268 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
269 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
270 |
lemma res_thm'_Inv: |
40671 | 271 |
assumes "effect (res_thm' l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
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)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
273 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
274 |
proof (induct xs ys arbitrary: r rule: res_thm'.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
275 |
case (1 l x xs y ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
276 |
(* There are five cases for res_thm: We will consider them one after another: *) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
277 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
278 |
assume cond: "x = l \<or> x = compl l" |
40671 | 279 |
assume resolve2: "effect (resolve2 (compl x) xs (y # ys)) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
280 |
from resolve2_Inv [OF resolve2] cond have ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
281 |
apply - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
282 |
by (rule exI[of _ "x"]) fastsimp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
283 |
} moreover |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
284 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
285 |
assume cond: "\<not> (x = l \<or> x = compl l)" "y = l \<or> y = compl l" |
40671 | 286 |
assume resolve1: "effect (resolve1 (compl y) (x # xs) ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
287 |
from resolve1_Inv [OF resolve1] cond have ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
288 |
apply - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
289 |
by (rule exI[of _ "compl y"]) fastsimp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
290 |
} moreover |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
291 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
292 |
fix r' |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
293 |
assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "x < y" |
40671 | 294 |
assume res_thm: "effect (res_thm' l xs (y # ys)) h h' r'" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
295 |
assume return: "r = x # r'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
296 |
from "1.hyps"(1) [OF cond res_thm] cond return have ?case by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
297 |
} moreover |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
298 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
299 |
fix r' |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
300 |
assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "y < x" |
40671 | 301 |
assume res_thm: "effect (res_thm' l (x # xs) ys) h h' r'" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
302 |
assume return: "r = y # r'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
303 |
from "1.hyps"(2) [OF cond res_thm] cond return have ?case by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
304 |
} moreover |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
305 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
306 |
fix r' |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
307 |
assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "\<not> y < x" |
40671 | 308 |
assume res_thm: "effect (res_thm' l xs ys) h h' r'" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
309 |
assume return: "r = x # r'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
310 |
from "1.hyps"(3) [OF cond res_thm] cond return have ?case by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
311 |
} moreover |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
312 |
note "1.prems" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
313 |
ultimately show ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
314 |
unfolding res_thm'.simps |
40671 | 315 |
apply (elim effect_bindE effect_ifE effect_returnE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
316 |
apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
317 |
apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
318 |
apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
319 |
apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
320 |
apply fastsimp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
321 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
322 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
323 |
case (2 l ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
324 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
325 |
unfolding res_thm'.simps |
40671 | 326 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
327 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
328 |
case (3 l v va r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
329 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
330 |
unfolding res_thm'.simps |
40671 | 331 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
332 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
333 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
334 |
lemma res_mem_no_heap: |
40671 | 335 |
assumes "effect (res_mem l xs) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
336 |
shows "h = h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
337 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
338 |
apply (induct xs arbitrary: r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
339 |
unfolding res_mem.simps |
40671 | 340 |
apply (elim effect_raiseE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
341 |
apply auto |
40671 | 342 |
apply (elim effect_ifE effect_bindE effect_raiseE effect_returnE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
343 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
344 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
345 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
346 |
lemma resolve1_no_heap: |
40671 | 347 |
assumes "effect (resolve1 l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
348 |
shows "h = h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
349 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
350 |
apply (induct xs ys arbitrary: r rule: resolve1.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
351 |
unfolding resolve1.simps |
40671 | 352 |
apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
353 |
apply (auto simp add: res_mem_no_heap) |
40671 | 354 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
355 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
356 |
lemma resolve2_no_heap: |
40671 | 357 |
assumes "effect (resolve2 l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
358 |
shows "h = h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
359 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
360 |
apply (induct xs ys arbitrary: r rule: resolve2.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
361 |
unfolding resolve2.simps |
40671 | 362 |
apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
363 |
apply (auto simp add: res_mem_no_heap) |
40671 | 364 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
365 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
366 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
367 |
lemma res_thm'_no_heap: |
40671 | 368 |
assumes "effect (res_thm' l xs ys) h h' r" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
369 |
shows "h = h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
370 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
371 |
proof (induct xs ys arbitrary: r rule: res_thm'.induct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
372 |
case (1 l x xs y ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
373 |
thus ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
374 |
unfolding res_thm'.simps |
40671 | 375 |
by (elim effect_bindE effect_ifE effect_returnE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
376 |
(auto simp add: resolve1_no_heap resolve2_no_heap) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
377 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
378 |
case (2 l ys r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
379 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
380 |
unfolding res_thm'.simps |
40671 | 381 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
382 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
383 |
case (3 l v va r) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
384 |
thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
385 |
unfolding res_thm'.simps |
40671 | 386 |
by (elim effect_raiseE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
387 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
388 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
389 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
390 |
lemma res_thm'_Inv2: |
40671 | 391 |
assumes res_thm: "effect (res_thm' l xs ys) h h' rcl" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
392 |
assumes l_not_null: "l \<noteq> 0" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
393 |
assumes ys: "correctClause r ys \<and> sorted ys \<and> distinct ys" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
394 |
assumes xs: "correctClause r xs \<and> sorted xs \<and> distinct xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
395 |
shows "correctClause r rcl \<and> sorted rcl \<and> distinct rcl" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
396 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
397 |
from res_thm'_Inv [OF res_thm] xs ys l_not_null show ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
398 |
apply (auto simp add: sorted_remove1) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
399 |
unfolding correctClause_def |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
400 |
apply (auto simp add: remove1_eq_remove) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
401 |
prefer 2 |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
402 |
apply (rule interpClause_resolvants) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
403 |
apply simp_all |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
404 |
apply (insert compl_exists [of l]) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
405 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
406 |
apply (rule interpClause_resolvants) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
407 |
apply simp_all |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
408 |
done |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
409 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
410 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
411 |
subsection {* res_thm and doProofStep *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
412 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
413 |
definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
414 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
415 |
"get_clause a i = |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
416 |
do { c \<leftarrow> Array.nth a i; |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
417 |
(case c of None \<Rightarrow> raise (''Clause not found'') |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
418 |
| Some x \<Rightarrow> return x) |
37792 | 419 |
}" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
420 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
421 |
|
37726 | 422 |
primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
423 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
424 |
"res_thm2 a (l, j) cli = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
425 |
( if l = 0 then raise(''Illegal literal'') |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
426 |
else |
37792 | 427 |
do { clj \<leftarrow> get_clause a j; |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
428 |
res_thm' l cli clj |
37792 | 429 |
})" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
430 |
|
37709 | 431 |
primrec |
432 |
foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap" |
|
433 |
where |
|
434 |
"foldM f [] s = return s" |
|
435 |
| "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs" |
|
436 |
||
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
437 |
fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
438 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
439 |
"doProofStep2 a (Conflict saveTo (i, rs)) rcs = |
37792 | 440 |
do { |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
441 |
cli \<leftarrow> get_clause a i; |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
442 |
result \<leftarrow> foldM (res_thm2 a) rs cli; |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
443 |
Array.upd saveTo (Some result) a; |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
444 |
return rcs |
37792 | 445 |
}" |
37798
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
446 |
| "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }" |
0b0570445a2a
proper merge of operation changes and generic do-syntax
haftmann
parents:
37797
diff
changeset
|
447 |
| "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
448 |
| "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
449 |
| "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
450 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
451 |
definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
452 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
453 |
"checker n p i = |
37792 | 454 |
do { |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
455 |
a \<leftarrow> Array.new n None; |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
456 |
rcs \<leftarrow> foldM (doProofStep2 a) p []; |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
457 |
ec \<leftarrow> Array.nth a i; |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
458 |
(if ec = Some [] then return rcs |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
459 |
else raise(''No empty clause'')) |
37792 | 460 |
}" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
461 |
|
40671 | 462 |
lemma effect_option_case: |
463 |
assumes "effect (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r" |
|
464 |
obtains "x = None" "effect n h h' r" |
|
465 |
| y where "x = Some y" "effect (s y) h h' r" |
|
466 |
using assms unfolding effect_def by (auto split: option.splits) |
|
37775 | 467 |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
468 |
lemma res_thm2_Inv: |
40671 | 469 |
assumes res_thm: "effect (res_thm2 a (l, j) cli) h h' rs" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
470 |
assumes correct_a: "correctArray r a h" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
471 |
assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
472 |
shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
473 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
474 |
from res_thm have l_not_zero: "l \<noteq> 0" |
40671 | 475 |
by (auto elim: effect_raiseE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
476 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
477 |
fix clj |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
478 |
let ?rs = "merge (remove l cli) (remove (compl l) clj)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
479 |
let ?rs' = "merge (remove (compl l) cli) (remove l clj)" |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
480 |
assume "h = h'" "Some clj = Array.get h' a ! j" "j < Array.length h' a" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
481 |
with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
482 |
unfolding correctArray_def by (auto intro: array_ranI) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
483 |
with clj l_not_zero correct_cli |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
484 |
have "(l \<in> set cli \<and> compl l \<in> set clj |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
485 |
\<longrightarrow> correctClause r ?rs \<and> sorted ?rs \<and> distinct ?rs) \<and> |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
486 |
(compl l \<in> set cli \<and> l \<in> set clj |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
487 |
\<longrightarrow> correctClause r ?rs' \<and> sorted ?rs' \<and> distinct ?rs')" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
488 |
apply (auto intro!: correctClause_resolvants) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
489 |
apply (insert compl_exists [of l]) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
490 |
by (auto intro!: correctClause_resolvants) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
491 |
} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
492 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
493 |
fix v clj |
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset
|
494 |
assume "Some clj = Array.get h a ! j" "j < Array.length h a" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
495 |
with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
496 |
unfolding correctArray_def by (auto intro: array_ranI) |
40671 | 497 |
assume "effect (res_thm' l cli clj) h h' rs" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
498 |
from res_thm'_no_heap[OF this] res_thm'_Inv2[OF this l_not_zero clj correct_cli] |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
499 |
have "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
500 |
} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
501 |
with assms show ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
502 |
unfolding res_thm2.simps get_clause_def |
40671 | 503 |
by (elim effect_bindE effect_ifE effect_nthE effect_raiseE effect_returnE effect_option_case) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
504 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
505 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
506 |
lemma foldM_Inv2: |
40671 | 507 |
assumes "effect (foldM (res_thm2 a) rs cli) h h' rcl" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
508 |
assumes correct_a: "correctArray r a h" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
509 |
assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
510 |
shows "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
511 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
512 |
proof (induct rs arbitrary: h h' cli) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
513 |
case Nil thus ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
514 |
unfolding foldM.simps |
40671 | 515 |
by (elim effect_returnE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
516 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
517 |
case (Cons x xs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
518 |
{ |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
519 |
fix h1 ret |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
520 |
obtain l j where x_is: "x = (l, j)" by fastsimp |
40671 | 521 |
assume res_thm2: "effect (res_thm2 a x cli) h h1 ret" |
522 |
with x_is have res_thm2': "effect (res_thm2 a (l, j) cli) h h1 ret" by simp |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
523 |
note step = res_thm2_Inv [OF res_thm2' Cons.prems(2) Cons.prems(3)] |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
524 |
from step have ret: "correctClause r ret \<and> sorted ret \<and> distinct ret" by simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
525 |
from step Cons.prems(2) have correct_a: "correctArray r a h1" by simp |
40671 | 526 |
assume foldM: "effect (foldM (res_thm2 a) xs ret) h1 h' rcl" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
527 |
from step Cons.hyps [OF foldM correct_a ret] have |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
528 |
"h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
529 |
} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
530 |
with Cons show ?case |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
531 |
unfolding foldM.simps |
40671 | 532 |
by (elim effect_bindE) auto |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
533 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
534 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
535 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
536 |
lemma step_correct2: |
40671 | 537 |
assumes effect: "effect (doProofStep2 a step rcs) h h' res" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
538 |
assumes correctArray: "correctArray rcs a h" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
539 |
shows "correctArray res a h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
540 |
proof (cases "(a,step,rcs)" rule: doProofStep2.cases) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
541 |
case (1 a saveTo i rs rcs) |
40671 | 542 |
with effect correctArray |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
543 |
show ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
544 |
apply auto |
40671 | 545 |
apply (auto simp: get_clause_def elim!: effect_bindE effect_nthE) |
546 |
apply (auto elim!: effect_bindE effect_nthE effect_option_case effect_raiseE |
|
547 |
effect_returnE effect_updE) |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
548 |
apply (frule foldM_Inv2) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
549 |
apply assumption |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
550 |
apply (simp add: correctArray_def) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
551 |
apply (drule_tac x="y" in bspec) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
552 |
apply (rule array_ranI[where i=i]) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
553 |
by (auto intro: correctArray_update) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
554 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
555 |
case (2 a cid rcs) |
40671 | 556 |
with effect correctArray |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
557 |
show ?thesis |
40671 | 558 |
by (auto simp: correctArray_def elim!: effect_bindE effect_updE effect_returnE |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
559 |
dest: array_ran_upd_array_None) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
560 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
561 |
case (3 a cid c rcs) |
40671 | 562 |
with effect correctArray |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
563 |
show ?thesis |
40671 | 564 |
apply (auto elim!: effect_bindE effect_updE effect_returnE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
565 |
apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
566 |
apply (auto intro: correctClause_mono) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
567 |
by (auto simp: correctClause_def) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
568 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
569 |
case 4 |
40671 | 570 |
with effect correctArray |
571 |
show ?thesis by (auto elim: effect_raiseE) |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
572 |
next |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
573 |
case 5 |
40671 | 574 |
with effect correctArray |
575 |
show ?thesis by (auto elim: effect_raiseE) |
|
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
576 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
577 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
578 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
579 |
theorem fold_steps_correct: |
40671 | 580 |
assumes "effect (foldM (doProofStep2 a) steps rcs) h h' res" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
581 |
assumes "correctArray rcs a h" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
582 |
shows "correctArray res a h'" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
583 |
using assms |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
584 |
by (induct steps arbitrary: rcs h h' res) |
40671 | 585 |
(auto elim!: effect_bindE effect_returnE dest:step_correct2) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
586 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
587 |
theorem checker_soundness: |
40671 | 588 |
assumes "effect (checker n p i) h h' cs" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
589 |
shows "inconsistent cs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
590 |
using assms unfolding checker_def |
40671 | 591 |
apply (elim effect_bindE effect_nthE effect_ifE effect_returnE effect_raiseE effect_newE) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
592 |
prefer 2 apply simp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
593 |
apply auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
594 |
apply (drule fold_steps_correct) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
595 |
apply (simp add: correctArray_def array_ran_def) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
596 |
apply (rule implies_empty_inconsistent) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
597 |
apply (simp add:correctArray_def) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
598 |
apply (drule bspec) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
599 |
by (rule array_ranI, auto) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
600 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
601 |
section {* Functional version with Lists as Array *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
602 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
603 |
subsection {* List specific definitions *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
604 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
605 |
definition list_ran :: "'a option list \<Rightarrow> 'a set" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
606 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
607 |
"list_ran xs = {e. Some e \<in> set xs }" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
608 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
609 |
lemma list_ranI: "\<lbrakk> i < List.length xs; xs ! i = Some b \<rbrakk> \<Longrightarrow> b \<in> list_ran xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
610 |
unfolding list_ran_def by (drule sym, simp) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
611 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
612 |
lemma list_ran_update_Some: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
613 |
"cl \<in> list_ran (xs[i := (Some b)]) \<Longrightarrow> cl \<in> list_ran xs \<or> cl = b" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
614 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
615 |
assume assms: "cl \<in> list_ran (xs[i := (Some b)])" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
616 |
have "set (xs[i := Some b]) \<subseteq> insert (Some b) (set xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
617 |
by (simp only: set_update_subset_insert) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
618 |
with assms have "Some cl \<in> insert (Some b) (set xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
619 |
unfolding list_ran_def by fastsimp |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
620 |
thus ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
621 |
unfolding list_ran_def by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
622 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
623 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
624 |
lemma list_ran_update_None: |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
625 |
"cl \<in> list_ran (xs[i := None]) \<Longrightarrow> cl \<in> list_ran xs" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
626 |
proof - |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
627 |
assume assms: "cl \<in> list_ran (xs[i := None])" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
628 |
have "set (xs[i := None]) \<subseteq> insert None (set xs)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
629 |
by (simp only: set_update_subset_insert) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
630 |
with assms show ?thesis |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
631 |
unfolding list_ran_def by auto |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
632 |
qed |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
633 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
634 |
definition correctList :: "Clause list \<Rightarrow> Clause option list \<Rightarrow> bool" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
635 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
636 |
"correctList rootcls xs = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
637 |
(\<forall>cl \<in> list_ran xs. correctClause rootcls cl \<and> sorted cl \<and> distinct cl)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
638 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
639 |
subsection {* Checker functions *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
640 |
|
37726 | 641 |
primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
642 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
643 |
"lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
644 |
None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
645 |
| Some clj \<Rightarrow> res_thm' l cli clj |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
646 |
) else raise ''Error'')" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
647 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
648 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
649 |
fun ldoProofStep :: " ProofStep \<Rightarrow> (Clause option list * Clause list) \<Rightarrow> (Clause option list * Clause list) Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
650 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
651 |
"ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) = |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
652 |
(case (xs ! i) of |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
653 |
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') |
37792 | 654 |
| Some cli \<Rightarrow> do { |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
655 |
result \<leftarrow> foldM (lres_thm xs) rs cli ; |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
656 |
return ((xs[saveTo:=Some result]), rcl) |
37792 | 657 |
})" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
658 |
| "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
659 |
| "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
660 |
| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
661 |
| "ldoProofStep (ProofDone b) (xs, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
662 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
663 |
definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
664 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
665 |
"lchecker n p i = |
37792 | 666 |
do { |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
667 |
rcs \<leftarrow> foldM (ldoProofStep) p ([], []); |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
668 |
(if (fst rcs ! i) = Some [] then return (snd rcs) |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
669 |
else raise(''No empty clause'')) |
37792 | 670 |
}" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
671 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
672 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
673 |
section {* Functional version with RedBlackTrees *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
674 |
|
37726 | 675 |
primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
676 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
677 |
"tres_thm t (l, j) cli = |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
678 |
(case (RBT_Impl.lookup t j) of |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
679 |
None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
680 |
| Some clj \<Rightarrow> res_thm' l cli clj)" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
681 |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
682 |
fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
683 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
684 |
"tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
685 |
(case (RBT_Impl.lookup t i) of |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
686 |
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') |
37792 | 687 |
| Some cli \<Rightarrow> do { |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
688 |
result \<leftarrow> foldM (tres_thm t) rs cli; |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
689 |
return ((RBT_Impl.insert saveTo result t), rcl) |
37792 | 690 |
})" |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
691 |
| "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)" |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
692 |
| "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
693 |
| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
694 |
| "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
695 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
696 |
definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
697 |
where |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
698 |
"tchecker n p i = |
37792 | 699 |
do { |
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
700 |
rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []); |
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset
|
701 |
(if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
702 |
else raise(''No empty clause'')) |
37792 | 703 |
}" |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
704 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
705 |
section {* Code generation setup *} |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
706 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
707 |
code_type ProofStep |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
708 |
(SML "MinisatProofStep.ProofStep") |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
709 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
710 |
code_const ProofDone and Root and Conflict and Delete and Xstep |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
711 |
(SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))") |
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
712 |
|
37826 | 713 |
export_code checker tchecker lchecker in SML |
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
714 |
|
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset
|
715 |
end |