author  haftmann 
Tue, 13 Jul 2010 12:05:20 +0200  
changeset 37797  96551d6b1414 
parent 37792  ba0bc31b90d7 
parent 37796  08bd610b2583 
child 37798  0b0570445a2a 
permissions  rwrr 
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  121 
definition 
122 
array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where 

123 
"array_ran a h = {e. Some e \<in> set (get_array a h)}" 

124 
 {*FIXME*} 

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  128 

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  131 
shows "cl \<in> array_ran a h \<or> cl = b" 
132 
proof  

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) 

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  136 
qed 
137 

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  140 
shows "cl \<in> array_ran a h" 
141 
proof  

142 
have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert) 

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  145 
qed 
146 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

147 
definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

148 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

149 
"correctArray rootcls a h = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

150 
(\<forall>cl \<in> array_ran a h. correctClause rootcls cl \<and> sorted cl \<and> distinct cl)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

151 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

152 
lemma correctArray_update: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

153 
assumes "correctArray rcs a h" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

154 
assumes "correctClause rcs c" "sorted c" "distinct c" 
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  174 
primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

175 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

176 
"res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" 
37792  177 
 "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

178 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

179 
fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

180 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

181 
"resolve1 l (x#xs) (y#ys) = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

182 
(if (x = l) then return (merge xs (y#ys)) 
37792  183 
else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) } 
184 
else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) } 

185 
else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))" 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

186 
 "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

187 
 "resolve1 l xs [] = res_mem l xs" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

188 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

189 
fun resolve2 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

190 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

191 
"resolve2 l (x#xs) (y#ys) = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

192 
(if (y = l) then return (merge (x#xs) ys) 
37792  193 
else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) } 
194 
else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) } 

195 
else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))" 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

196 
 "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

197 
 "resolve2 l [] ys = res_mem l ys" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

198 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

199 
fun res_thm' :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

200 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

201 
"res_thm' l (x#xs) (y#ys) = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

202 
(if (x = l \<or> x = compl l) then resolve2 (compl x) xs (y#ys) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

203 
else (if (y = l \<or> y = compl l) then resolve1 (compl y) (x#xs) ys 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

204 
else (if (x < y) then (res_thm' l xs (y#ys)) \<guillemotright>= (\<lambda>v. return (x # v)) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

205 
else (if (x > y) then (res_thm' l (x#xs) ys) \<guillemotright>= (\<lambda>v. return (y # v)) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

206 
else (res_thm' l xs ys) \<guillemotright>= (\<lambda>v. return (x # v))))))" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

207 
 "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

208 
 "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

209 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

210 
declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del] 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

211 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

212 
subsection {* Proofs about these functions *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

213 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

214 
lemma res_mem: 
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 = 
37792  416 
do { c \<leftarrow> nth a i; 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

417 
(case c of None \<Rightarrow> raise (''Clause not found'') 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

418 
 Some x \<Rightarrow> return x) 
37792  419 
}" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

420 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

421 

37726  422 
primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

423 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

424 
"res_thm2 a (l, j) cli = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

425 
( if l = 0 then raise(''Illegal literal'') 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

426 
else 
37792  427 
do { clj \<leftarrow> get_clause a j; 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

428 
res_thm' l cli clj 
37792  429 
})" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

430 

37709  431 
primrec 
432 
foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap" 

433 
where 

434 
"foldM f [] s = return s" 

435 
 "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs" 

436 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

437 
fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

438 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

439 
"doProofStep2 a (Conflict saveTo (i, rs)) rcs = 
37792  440 
do { 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

441 
cli \<leftarrow> get_clause a i; 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

442 
result \<leftarrow> foldM (res_thm2 a) rs cli; 
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 
37792  445 
}" 
446 
 "doProofStep2 a (Delete cid) rcs = do { upd cid None a; return rcs }" 

447 
 "doProofStep2 a (Root cid clause) rcs = do { upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }" 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

448 
 "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

449 
 "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

450 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

451 
definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

452 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

453 
"checker n p i = 
37792  454 
do { 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

455 
a \<leftarrow> Array.new n None; 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

456 
rcs \<leftarrow> foldM (doProofStep2 a) p []; 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

457 
ec \<leftarrow> Array.nth a i; 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

458 
(if ec = Some [] then return rcs 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

459 
else raise(''No empty clause'')) 
37792  460 
}" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

461 

37775  462 
lemma crel_option_case: 
463 
assumes "crel (case x of None \<Rightarrow> n  Some y \<Rightarrow> s y) h h' r" 

464 
obtains "x = None" "crel n h h' r" 

465 
 y where "x = Some y" "crel (s y) h h' r" 

466 
using assms unfolding crel_def by (auto split: option.splits) 

467 

36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

468 
lemma res_thm2_Inv: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

469 
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

470 
assumes correct_a: "correctArray r a h" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

471 
assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

472 
shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

473 
proof  
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

474 
from res_thm have l_not_zero: "l \<noteq> 0" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

475 
by (auto elim: crel_raiseE) 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

476 
{ 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

477 
fix clj 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

478 
let ?rs = "merge (remove l cli) (remove (compl l) clj)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

479 
let ?rs' = "merge (remove (compl l) cli) (remove l clj)" 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37717
diff
changeset

480 
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

481 
with correct_a have clj: "correctClause r clj" "sorted clj" "distinct clj" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

482 
unfolding correctArray_def by (auto intro: array_ranI) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

483 
with clj l_not_zero correct_cli 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

484 
have "(l \<in> set cli \<and> compl l \<in> set clj 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

485 
\<longrightarrow> correctClause r ?rs \<and> sorted ?rs \<and> distinct ?rs) \<and> 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

486 
(compl l \<in> set cli \<and> l \<in> set clj 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

487 
\<longrightarrow> correctClause r ?rs' \<and> sorted ?rs' \<and> distinct ?rs')" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

488 
apply (auto intro!: correctClause_resolvants) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

489 
apply (insert compl_exists [of l]) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

490 
by (auto intro!: correctClause_resolvants) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

491 
} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

492 
{ 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

493 
fix v clj 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
37717
diff
changeset

494 
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

495 
with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

496 
unfolding correctArray_def by (auto intro: array_ranI) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

497 
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

498 
from res_thm'_no_heap[OF this] res_thm'_Inv2[OF this l_not_zero clj correct_cli] 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

499 
have "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" by simp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

500 
} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

501 
with assms show ?thesis 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

502 
unfolding res_thm2.simps get_clause_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

503 
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

504 
qed 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

505 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

506 
lemma foldM_Inv2: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

507 
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

508 
assumes correct_a: "correctArray r a h" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

509 
assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

510 
shows "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

511 
using assms 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

512 
proof (induct rs arbitrary: h h' cli) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

513 
case Nil thus ?case 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

514 
unfolding foldM.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

515 
by (elim crel_returnE) auto 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

516 
next 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

517 
case (Cons x xs) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

518 
{ 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

519 
fix h1 ret 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

520 
obtain l j where x_is: "x = (l, j)" by fastsimp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

521 
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

522 
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

523 
note step = res_thm2_Inv [OF res_thm2' Cons.prems(2) Cons.prems(3)] 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

524 
from step have ret: "correctClause r ret \<and> sorted ret \<and> distinct ret" by simp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

525 
from step Cons.prems(2) have correct_a: "correctArray r a h1" by simp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

526 
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

527 
from step Cons.hyps [OF foldM correct_a ret] have 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

528 
"h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" by auto 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

529 
} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

530 
with Cons show ?case 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

531 
unfolding foldM.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

532 
by (elim crel_bindE) auto 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

533 
qed 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

534 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

535 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

536 
lemma step_correct2: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

537 
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

538 
assumes correctArray: "correctArray rcs a h" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

539 
shows "correctArray res a h'" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

540 
proof (cases "(a,step,rcs)" rule: doProofStep2.cases) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

541 
case (1 a saveTo i rs rcs) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

542 
with crel correctArray 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

543 
show ?thesis 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

544 
apply auto 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

545 
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

546 
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

547 
crel_returnE crel_updE) 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

548 
apply (frule foldM_Inv2) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

549 
apply assumption 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

550 
apply (simp add: correctArray_def) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

551 
apply (drule_tac x="y" in bspec) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

552 
apply (rule array_ranI[where i=i]) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

553 
by (auto intro: correctArray_update) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

554 
next 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

555 
case (2 a cid rcs) 
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 
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

559 
dest: array_ran_upd_array_None) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

560 
next 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

561 
case (3 a cid c rcs) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

562 
with crel correctArray 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

563 
show ?thesis 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

564 
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

565 
apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

566 
apply (auto intro: correctClause_mono) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

567 
by (auto simp: correctClause_def) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

568 
next 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

569 
case 4 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

570 
with crel correctArray 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

571 
show ?thesis by (auto elim: crel_raiseE) 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

572 
next 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

573 
case 5 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

574 
with crel correctArray 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

575 
show ?thesis by (auto elim: crel_raiseE) 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

576 
qed 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

577 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

578 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

579 
theorem fold_steps_correct: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

580 
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

581 
assumes "correctArray rcs a h" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

582 
shows "correctArray res a h'" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

583 
using assms 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

584 
by (induct steps arbitrary: rcs h h' res) 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

585 
(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

586 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

587 
theorem checker_soundness: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

588 
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

589 
shows "inconsistent cs" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

590 
using assms unfolding checker_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37726
diff
changeset

591 
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

592 
prefer 2 apply simp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

593 
apply auto 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

594 
apply (drule fold_steps_correct) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

595 
apply (simp add: correctArray_def array_ran_def) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

596 
apply (rule implies_empty_inconsistent) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

597 
apply (simp add:correctArray_def) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

598 
apply (drule bspec) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

599 
by (rule array_ranI, auto) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

600 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

601 
section {* Functional version with Lists as Array *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

602 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

603 
subsection {* List specific definitions *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

604 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

605 
definition list_ran :: "'a option list \<Rightarrow> 'a set" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

606 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

607 
"list_ran xs = {e. Some e \<in> set xs }" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

608 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

609 
lemma list_ranI: "\<lbrakk> i < List.length xs; xs ! i = Some b \<rbrakk> \<Longrightarrow> b \<in> list_ran xs" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

610 
unfolding list_ran_def by (drule sym, simp) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

611 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

612 
lemma list_ran_update_Some: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

613 
"cl \<in> list_ran (xs[i := (Some b)]) \<Longrightarrow> cl \<in> list_ran xs \<or> cl = b" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

614 
proof  
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

615 
assume assms: "cl \<in> list_ran (xs[i := (Some b)])" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

616 
have "set (xs[i := Some b]) \<subseteq> insert (Some b) (set xs)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

617 
by (simp only: set_update_subset_insert) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

618 
with assms have "Some cl \<in> insert (Some b) (set xs)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

619 
unfolding list_ran_def by fastsimp 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

620 
thus ?thesis 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

621 
unfolding list_ran_def by auto 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

622 
qed 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

623 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

624 
lemma list_ran_update_None: 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

625 
"cl \<in> list_ran (xs[i := None]) \<Longrightarrow> cl \<in> list_ran xs" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

626 
proof  
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

627 
assume assms: "cl \<in> list_ran (xs[i := None])" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

628 
have "set (xs[i := None]) \<subseteq> insert None (set xs)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

629 
by (simp only: set_update_subset_insert) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

630 
with assms show ?thesis 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

631 
unfolding list_ran_def by auto 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

632 
qed 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

633 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

634 
definition correctList :: "Clause list \<Rightarrow> Clause option list \<Rightarrow> bool" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

635 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

636 
"correctList rootcls xs = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

637 
(\<forall>cl \<in> list_ran xs. correctClause rootcls cl \<and> sorted cl \<and> distinct cl)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

638 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

639 
subsection {* Checker functions *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

640 

37726  641 
primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

642 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

643 
"lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

644 
None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

645 
 Some clj \<Rightarrow> res_thm' l cli clj 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

646 
) else raise ''Error'')" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

647 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

648 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

649 
fun ldoProofStep :: " ProofStep \<Rightarrow> (Clause option list * Clause list) \<Rightarrow> (Clause option list * Clause list) Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

650 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

651 
"ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) = 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

652 
(case (xs ! i) of 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

653 
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') 
37792  654 
 Some cli \<Rightarrow> do { 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

655 
result \<leftarrow> foldM (lres_thm xs) rs cli ; 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

656 
return ((xs[saveTo:=Some result]), rcl) 
37792  657 
})" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

658 
 "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

659 
 "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

660 
 "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

661 
 "ldoProofStep (ProofDone b) (xs, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

662 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

663 
definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

664 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

665 
"lchecker n p i = 
37792  666 
do { 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

667 
rcs \<leftarrow> foldM (ldoProofStep) p ([], []); 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

668 
(if (fst rcs ! i) = Some [] then return (snd rcs) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

669 
else raise(''No empty clause'')) 
37792  670 
}" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

671 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

672 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

673 
section {* Functional version with RedBlackTrees *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

674 

37726  675 
primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

676 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

677 
"tres_thm t (l, j) cli = 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

678 
(case (RBT_Impl.lookup t j) of 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

679 
None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'') 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

680 
 Some clj \<Rightarrow> res_thm' l cli clj)" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

681 

36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

682 
fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

683 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

684 
"tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) = 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

685 
(case (RBT_Impl.lookup t i) of 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

686 
None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'') 
37792  687 
 Some cli \<Rightarrow> do { 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

688 
result \<leftarrow> foldM (tres_thm t) rs cli; 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

689 
return ((RBT_Impl.insert saveTo result t), rcl) 
37792  690 
})" 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

691 
 "tdoProofStep (Delete cid) (t, rcl) = return ((RBT_Impl.delete cid t), rcl)" 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

692 
 "tdoProofStep (Root cid clause) (t, rcl) = return (RBT_Impl.insert cid (sort clause) t, (remdups(sort clause)) # rcl)" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

693 
 "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

694 
 "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

695 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

696 
definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap" 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

697 
where 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

698 
"tchecker n p i = 
37792  699 
do { 
36147
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

700 
rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []); 
b43b22f63665
theory RBT with abstract type of redblack trees backed by implementation RBT_Impl
haftmann
parents:
36098
diff
changeset

701 
(if (RBT_Impl.lookup (fst rcs) i) = Some [] then return (snd rcs) 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

702 
else raise(''No empty clause'')) 
37792  703 
}" 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

704 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

705 
section {* Code generation setup *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

706 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

707 
code_type ProofStep 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

708 
(SML "MinisatProofStep.ProofStep") 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

709 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

710 
code_const ProofDone and Root and Conflict and Delete and Xstep 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

711 
(SML "MinisatProofStep.ProofDone" and "MinisatProofStep.Root ((_),/ (_))" and "MinisatProofStep.Conflict ((_),/ (_))" and "MinisatProofStep.Delete" and "MinisatProofStep.Xstep ((_),/ (_))") 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

712 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

713 
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

714 
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

715 
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

716 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
diff
changeset

717 
end 