src/HOL/Imperative_HOL/ex/SatChecker.thy
author haftmann
Mon, 12 Jul 2010 16:05:08 +0200
changeset 37771 1bec64044b5e
parent 37726 17b05b104390
child 37775 7371534297a9
permissions -rw-r--r--
spelt out relational framework in a consistent way
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
     8
imports 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
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
    16
types ClauseId = nat
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
    17
types Lit = int
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
    18
types Clause = "Lit list"
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
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
    22
types Resolvants = "ClauseId * (Lit * ClauseId) list"
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
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   121
definition
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   122
  array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   123
  "array_ran a h = {e. Some e \<in> set (get_array a h)}"
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   124
    -- {*FIXME*}
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   125
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   126
lemma array_ranI: "\<lbrakk> Some b = get_array a h ! i; i < Array.length a h \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
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
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   128
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   129
lemma array_ran_upd_array_Some:
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   130
  assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
37717
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   131
  shows "cl \<in> array_ran a h \<or> cl = b"
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   132
proof -
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   133
  have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   134
  with assms show ?thesis 
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   135
    unfolding array_ran_def Array.change_def by fastsimp
37717
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   136
qed
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   137
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   138
lemma array_ran_upd_array_None:
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   139
  assumes "cl \<in> array_ran a (Array.change a i None h)"
37717
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   140
  shows "cl \<in> array_ran a h"
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   141
proof -
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   142
  have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   143
  with assms show ?thesis
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   144
    unfolding array_ran_def Array.change_def by auto
37717
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   145
qed
ede4b8397e01 moved special operation array_ran here
haftmann
parents: 37709
diff changeset
   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"
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   155
  shows "correctArray rcs a (Array.change 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
17b05b104390 even more fun with primrec
haftmann
parents: 37719
diff changeset
   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''"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   177
| "res_mem l (x#xs) = (if (x = l) then return xs else (do v \<leftarrow> res_mem l xs; return (x # v) done))"
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))
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   183
  else (if (x < y) then (do v \<leftarrow> resolve1 l xs (y#ys); return (x # v) done)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   184
  else (if (x > y) then (do v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) done)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   185
  else (do v \<leftarrow> resolve1 l xs ys; return (x # v) done))))"
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)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   193
  else (if (x < y) then (do v \<leftarrow> resolve2 l xs (y#ys); return (x # v) done)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   194
  else (if (x > y) then (do v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) done) 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   195
  else (do v \<leftarrow> resolve2 l xs ys; return (x # v) done))))"
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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   215
assumes "crel (res_mem l xs) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   220
  thus ?case unfolding res_mem.simps by (auto elim: crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   225
    by (elim crel_raiseE crel_returnE crel_ifE crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   229
assumes "crel (resolve1 l xs ys) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   236
    by (elim crel_bindE crel_ifE crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   241
    by (elim crel_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: 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   250
  assumes "crel (resolve2 l xs ys) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   257
    by (elim crel_bindE crel_ifE crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   262
    by (elim crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   271
assumes "crel (res_thm' l xs ys) h h' r"
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"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   279
    assume resolve2: "crel (resolve2 (compl x) xs (y # ys)) h h' r"   
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" 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   286
    assume resolve1: "crel (resolve1 (compl y) (x # xs) ys) h h' r"
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"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   294
    assume res_thm: "crel (res_thm' l xs (y # ys)) h h' r'"
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"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   301
    assume res_thm: "crel (res_thm' l (x # xs) ys) h h' r'"
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"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   308
    assume res_thm: "crel (res_thm' l xs ys) h h' r'"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   315
    apply (elim crel_bindE crel_ifE crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   326
    by (elim crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   331
    by (elim crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   335
assumes "crel (res_mem l xs) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   340
apply (elim crel_raiseE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   341
apply auto
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   342
apply (elim crel_ifE crel_bindE crel_raiseE crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   347
assumes "crel (resolve1 l xs ys) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   352
apply (elim crel_bindE crel_ifE crel_returnE crel_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)
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   354
by (elim crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   357
assumes "crel (resolve2 l xs ys) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   362
apply (elim crel_bindE crel_ifE crel_returnE crel_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)
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   364
by (elim crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   368
  assumes "crel (res_thm' l xs ys) h h' r"
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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   375
    by (elim crel_bindE crel_ifE crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   381
    by (elim crel_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
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   386
    by (elim crel_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:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   391
  assumes res_thm: "crel (res_thm' l xs ys) h h' rcl"
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 = 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   416
       (do c \<leftarrow> nth a i;
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)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   419
        done)"
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
17b05b104390 even more fun with primrec
haftmann
parents: 37719
diff changeset
   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
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   427
     (do clj \<leftarrow> get_clause a j;
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   428
         res_thm' l cli clj
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   429
      done))"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   430
37709
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   431
primrec
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   432
  foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   433
where
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   434
  "foldM f [] s = return s"
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   435
  | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
70fafefbcc98 simplified representation of monad type
haftmann
parents: 37456
diff changeset
   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 =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   440
  (do
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;
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   443
     upd saveTo (Some result) a; 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   444
     return rcs
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   445
   done)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   446
| "doProofStep2 a (Delete cid) rcs = (do upd cid None a; return rcs done)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   447
| "doProofStep2 a (Root cid clause) rcs = (do upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
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 =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   454
  (do 
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''))
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   460
   done)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   461
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   462
lemma res_thm2_Inv:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   463
  assumes res_thm: "crel (res_thm2 a (l, j) cli) h h' rs"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   464
  assumes correct_a: "correctArray r a h"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   465
  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
   466
  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
   467
proof -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   468
  from res_thm have l_not_zero: "l \<noteq> 0" 
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   469
    by (auto elim: crel_raiseE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   470
  {
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   471
    fix clj
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   472
    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
   473
    let ?rs' = "merge (remove (compl l) cli) (remove l clj)"
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   474
    assume "h = h'" "Some clj = get_array a h' ! j" "j < Array.length a h'"
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   475
    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
   476
      unfolding correctArray_def by (auto intro: array_ranI)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   477
    with clj l_not_zero correct_cli
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   478
    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
   479
      \<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
   480
      (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
   481
      \<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
   482
      apply (auto intro!: correctClause_resolvants)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   483
      apply (insert compl_exists [of l])
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   484
      by (auto intro!: correctClause_resolvants)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   485
  }
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   486
  {
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   487
    fix v clj
37719
271ecd4fb9f9 moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents: 37717
diff changeset
   488
    assume "Some clj = get_array a h ! j" "j < Array.length a h"
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   489
    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
   490
      unfolding correctArray_def by (auto intro: array_ranI)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   491
    assume "crel (res_thm' l cli clj) h h' rs"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   492
    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
   493
    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
   494
  }
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   495
  with assms show ?thesis
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   496
    unfolding res_thm2.simps get_clause_def
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   497
    by (elim crel_bindE crel_ifE crel_nthE crel_raiseE crel_returnE crel_option_case) auto
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   498
qed
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   499
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   500
lemma foldM_Inv2:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   501
  assumes "crel (foldM (res_thm2 a) rs cli) h h' rcl"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   502
  assumes correct_a: "correctArray r a h"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   503
  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
   504
  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
   505
using assms
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   506
proof (induct rs arbitrary: h h' cli)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   507
  case Nil thus ?case
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   508
    unfolding foldM.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   509
    by (elim crel_returnE) auto
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   510
next
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   511
  case (Cons x xs)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   512
  {
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   513
    fix h1 ret
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   514
    obtain l j where x_is: "x = (l, j)" by fastsimp
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   515
    assume res_thm2: "crel (res_thm2 a x cli) h h1 ret"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   516
    with x_is have res_thm2': "crel (res_thm2 a (l, j) cli) h h1 ret" by simp
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   517
    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
   518
    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
   519
    from step Cons.prems(2) have correct_a: "correctArray r a h1"  by simp
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   520
    assume foldM: "crel (foldM (res_thm2 a) xs ret) h1 h' rcl"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   521
    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
   522
    "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
   523
  }
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   524
  with Cons show ?case
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   525
    unfolding foldM.simps
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   526
    by (elim crel_bindE) auto
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   527
qed
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   528
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
lemma step_correct2:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   531
  assumes crel: "crel (doProofStep2 a step rcs) h h' res"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   532
  assumes correctArray: "correctArray rcs a h"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   533
  shows "correctArray res a h'"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   534
proof (cases "(a,step,rcs)" rule: doProofStep2.cases)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   535
  case (1 a saveTo i rs rcs)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   536
  with crel correctArray
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   537
  show ?thesis
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   538
    apply auto
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   539
    apply (auto simp: get_clause_def elim!: crel_bindE crel_nthE)
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   540
    apply (auto elim!: crel_bindE crel_nthE crel_option_case crel_raiseE
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   541
      crel_returnE crel_updE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   542
    apply (frule foldM_Inv2)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   543
    apply assumption
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   544
    apply (simp add: correctArray_def)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   545
    apply (drule_tac x="y" in bspec)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   546
    apply (rule array_ranI[where i=i])
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   547
    by (auto intro: correctArray_update)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   548
next
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   549
  case (2 a cid rcs)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   550
  with crel correctArray
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   551
  show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   552
    by (auto simp: correctArray_def elim!: crel_bindE crel_updE crel_returnE
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   553
     dest: array_ran_upd_array_None)
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 (3 a cid c rcs)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   556
  with crel correctArray
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   557
  show ?thesis
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   558
    apply (auto elim!: crel_bindE crel_updE crel_returnE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   559
    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
   560
    apply (auto intro: correctClause_mono)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   561
    by (auto simp: correctClause_def)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   562
next
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   563
  case 4
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   564
  with crel correctArray
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   565
  show ?thesis by (auto elim: crel_raiseE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   566
next
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   567
  case 5
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   568
  with crel correctArray
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   569
  show ?thesis by (auto elim: crel_raiseE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   570
qed
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   571
  
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   572
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   573
theorem fold_steps_correct:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   574
  assumes "crel (foldM (doProofStep2 a) steps rcs) h h' res"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   575
  assumes "correctArray rcs a h"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   576
  shows "correctArray res a h'"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   577
using assms
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   578
by (induct steps arbitrary: rcs h h' res)
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   579
 (auto elim!: crel_bindE crel_returnE dest:step_correct2)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   580
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   581
theorem checker_soundness:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   582
  assumes "crel (checker n p i) h h' cs"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   583
  shows "inconsistent cs"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   584
using assms unfolding checker_def
37771
1bec64044b5e spelt out relational framework in a consistent way
haftmann
parents: 37726
diff changeset
   585
apply (elim crel_bindE crel_nthE crel_ifE crel_returnE crel_raiseE crel_newE)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   586
prefer 2 apply simp
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   587
apply auto
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   588
apply (drule fold_steps_correct)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   589
apply (simp add: correctArray_def array_ran_def)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   590
apply (rule implies_empty_inconsistent)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   591
apply (simp add:correctArray_def)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   592
apply (drule bspec)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   593
by (rule array_ranI, auto)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   594
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   595
section {* Functional version with Lists as Array *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   596
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   597
subsection {* List specific definitions *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   598
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   599
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
   600
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   601
  "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
   602
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   603
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
   604
unfolding list_ran_def by (drule sym, simp)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   605
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   606
lemma list_ran_update_Some:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   607
  "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
   608
proof -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   609
  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
   610
  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
   611
    by (simp only: set_update_subset_insert)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   612
  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
   613
    unfolding list_ran_def by fastsimp
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   614
  thus ?thesis
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   615
    unfolding list_ran_def by auto
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   616
qed
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   617
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   618
lemma list_ran_update_None:
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   619
  "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
   620
proof -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   621
  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
   622
  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
   623
    by (simp only: set_update_subset_insert)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   624
  with assms show ?thesis
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   625
    unfolding list_ran_def by auto
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   626
qed
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   627
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   628
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
   629
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   630
  "correctList rootcls xs =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   631
  (\<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
   632
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   633
subsection {* Checker functions *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   634
37726
17b05b104390 even more fun with primrec
haftmann
parents: 37719
diff changeset
   635
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
   636
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   637
  "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
   638
  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
   639
  | Some clj \<Rightarrow> res_thm' l cli clj
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   640
 ) else raise ''Error'')"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   641
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   642
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   643
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
   644
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   645
  "ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   646
     (case (xs ! i) of
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   647
       None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   648
     | Some cli \<Rightarrow> (do
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   649
                      result \<leftarrow> foldM (lres_thm xs) rs cli ;
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   650
                      return ((xs[saveTo:=Some result]), rcl)
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   651
                    done))"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   652
| "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
   653
| "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
   654
| "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
   655
| "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
   656
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   657
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
   658
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   659
  "lchecker n p i =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   660
  (do 
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   661
     rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   662
     (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
   663
                else raise(''No empty clause''))
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   664
   done)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   665
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   666
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   667
section {* Functional version with RedBlackTrees *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   668
37726
17b05b104390 even more fun with primrec
haftmann
parents: 37719
diff changeset
   669
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
   670
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   671
  "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
   672
  (case (RBT_Impl.lookup t j) of 
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   673
     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
   674
   | Some clj \<Rightarrow> res_thm' l cli clj)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   675
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36098
diff changeset
   676
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
   677
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   678
  "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
   679
     (case (RBT_Impl.lookup t i) of
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   680
       None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   681
     | Some cli \<Rightarrow> (do
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   682
                      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
   683
                      return ((RBT_Impl.insert saveTo result t), rcl)
36098
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   684
                    done))"
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36098
diff changeset
   685
| "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
   686
| "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
   687
| "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
   688
| "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
   689
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   690
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
   691
where
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   692
  "tchecker n p i =
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   693
  (do 
36147
b43b22f63665 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents: 36098
diff changeset
   694
     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
   695
     (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
   696
                else raise(''No empty clause''))
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   697
   done)"
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   698
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   699
section {* Code generation setup *}
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   700
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   701
code_type ProofStep
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   702
  (SML "MinisatProofStep.ProofStep")
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   703
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   704
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
   705
     (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
   706
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   707
export_code checker in SML module_name SAT file -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   708
export_code tchecker in SML module_name SAT file -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   709
export_code lchecker in SML module_name SAT file -
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   710
53992c639da5 added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff changeset
   711
end