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