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