author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29265  5b4247055bd7 
child 30607  c3d1590debd8 
permissions  rwrr 
17618  1 
(* Title: HOL/Tools/cnf_funcs.ML 
2 
Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
26341
diff
changeset

3 
Author: Tjark Weber, TU Muenchen 
17618  4 

24958  5 
FIXME: major overlaps with the code in meson.ML 
6 

17618  7 
Description: 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

8 
This file contains functions and tactics to transform a formula into 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

9 
Conjunctive Normal Form (CNF). 
17618  10 
A formula in CNF is of the following form: 
11 

19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

12 
(x11  x12  ...  x1n) & ... & (xm1  xm2  ...  xmk) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

13 
False 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

14 
True 
17618  15 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

16 
where each xij is a literal (a positive or negative atomic Boolean term), 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

17 
i.e. the formula is a conjunction of disjunctions of literals, or 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

18 
"False", or "True". 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

19 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

20 
A (nonempty) disjunction of literals is referred to as "clause". 
17618  21 

22 
For the purpose of SAT proof reconstruction, we also make use of another 

23 
representation of clauses, which we call the "raw clauses". 

24 
Raw clauses are of the form 

25 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

26 
[..., x1', x2', ..., xn']  False , 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

27 

150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

28 
where each xi is a literal, and each xi' is the negation normal form of ~xi. 
17618  29 

19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

30 
Literals are successively removed from the hyps of raw clauses by resolution 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

31 
during SAT proof reconstruction. 
17618  32 
*) 
33 

34 
signature CNF = 

35 
sig 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

36 
val is_atom : Term.term > bool 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

37 
val is_literal : Term.term > bool 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

38 
val is_clause : Term.term > bool 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

39 
val clause_is_trivial : Term.term > bool 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

40 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

41 
val clause2raw_thm : Thm.thm > Thm.thm 
17618  42 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

43 
val weakening_tac : int > Tactical.tactic (* removes the first hypothesis of a subgoal *) 
17618  44 

20547  45 
val make_cnf_thm : theory > Term.term > Thm.thm 
46 
val make_cnfx_thm : theory > Term.term > Thm.thm 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

47 
val cnf_rewrite_tac : int > Tactical.tactic (* converts all prems of a subgoal to CNF *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

48 
val cnfx_rewrite_tac : int > Tactical.tactic (* converts all prems of a subgoal to (almost) definitional CNF *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

49 
end; 
17618  50 

51 
structure cnf : CNF = 

52 
struct 

53 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

54 
fun thm_by_auto (G : string) : thm = 
26341  55 
prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, CLASIMPSET auto_tac]); 
17618  56 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

57 
(* Thm.thm *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

58 
val clause2raw_notE = thm_by_auto "[ P; ~P ] ==> False"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

59 
val clause2raw_not_disj = thm_by_auto "[ ~P; ~Q ] ==> ~(P  Q)"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

60 
val clause2raw_not_not = thm_by_auto "P ==> ~~P"; 
17618  61 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

62 
val iff_refl = thm_by_auto "(P::bool) = P"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

63 
val iff_trans = thm_by_auto "[ (P::bool) = Q; Q = R ] ==> P = R"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

64 
val conj_cong = thm_by_auto "[ P = P'; Q = Q' ] ==> (P & Q) = (P' & Q')"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

65 
val disj_cong = thm_by_auto "[ P = P'; Q = Q' ] ==> (P  Q) = (P'  Q')"; 
17618  66 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

67 
val make_nnf_imp = thm_by_auto "[ (~P) = P'; Q = Q' ] ==> (P > Q) = (P'  Q')"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

68 
val make_nnf_iff = thm_by_auto "[ P = P'; (~P) = NP; Q = Q'; (~Q) = NQ ] ==> (P = Q) = ((P'  NQ) & (NP  Q'))"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

69 
val make_nnf_not_false = thm_by_auto "(~False) = True"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

70 
val make_nnf_not_true = thm_by_auto "(~True) = False"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

71 
val make_nnf_not_conj = thm_by_auto "[ (~P) = P'; (~Q) = Q' ] ==> (~(P & Q)) = (P'  Q')"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

72 
val make_nnf_not_disj = thm_by_auto "[ (~P) = P'; (~Q) = Q' ] ==> (~(P  Q)) = (P' & Q')"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

73 
val make_nnf_not_imp = thm_by_auto "[ P = P'; (~Q) = Q' ] ==> (~(P > Q)) = (P' & Q')"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

74 
val make_nnf_not_iff = thm_by_auto "[ P = P'; (~P) = NP; Q = Q'; (~Q) = NQ ] ==> (~(P = Q)) = ((P'  Q') & (NP  NQ))"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

75 
val make_nnf_not_not = thm_by_auto "P = P' ==> (~~P) = P'"; 
17618  76 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

77 
val simp_TF_conj_True_l = thm_by_auto "[ P = True; Q = Q' ] ==> (P & Q) = Q'"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

78 
val simp_TF_conj_True_r = thm_by_auto "[ P = P'; Q = True ] ==> (P & Q) = P'"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

79 
val simp_TF_conj_False_l = thm_by_auto "P = False ==> (P & Q) = False"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

80 
val simp_TF_conj_False_r = thm_by_auto "Q = False ==> (P & Q) = False"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

81 
val simp_TF_disj_True_l = thm_by_auto "P = True ==> (P  Q) = True"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

82 
val simp_TF_disj_True_r = thm_by_auto "Q = True ==> (P  Q) = True"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

83 
val simp_TF_disj_False_l = thm_by_auto "[ P = False; Q = Q' ] ==> (P  Q) = Q'"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

84 
val simp_TF_disj_False_r = thm_by_auto "[ P = P'; Q = False ] ==> (P  Q) = P'"; 
17618  85 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

86 
val make_cnf_disj_conj_l = thm_by_auto "[ (P  R) = PR; (Q  R) = QR ] ==> ((P & Q)  R) = (PR & QR)"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

87 
val make_cnf_disj_conj_r = thm_by_auto "[ (P  Q) = PQ; (P  R) = PR ] ==> (P  (Q & R)) = (PQ & PR)"; 
17618  88 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

89 
val make_cnfx_disj_ex_l = thm_by_auto "((EX (x::bool). P x)  Q) = (EX x. P x  Q)"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

90 
val make_cnfx_disj_ex_r = thm_by_auto "(P  (EX (x::bool). Q x)) = (EX x. P  Q x)"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

91 
val make_cnfx_newlit = thm_by_auto "(P  Q) = (EX x. (P  x) & (Q  ~x))"; 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

92 
val make_cnfx_ex_cong = thm_by_auto "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)"; 
17618  93 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

94 
val weakening_thm = thm_by_auto "[ P; Q ] ==> Q"; 
17618  95 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

96 
val cnftac_eq_imp = thm_by_auto "[ P = Q; P ] ==> Q"; 
17618  97 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

98 
(* Term.term > bool *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

99 
fun is_atom (Const ("False", _)) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

100 
 is_atom (Const ("True", _)) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

101 
 is_atom (Const ("op &", _) $ _ $ _) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

102 
 is_atom (Const ("op ", _) $ _ $ _) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

103 
 is_atom (Const ("op >", _) $ _ $ _) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

104 
 is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

105 
 is_atom (Const ("Not", _) $ _) = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

106 
 is_atom _ = true; 
17618  107 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

108 
(* Term.term > bool *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

109 
fun is_literal (Const ("Not", _) $ x) = is_atom x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

110 
 is_literal x = is_atom x; 
17618  111 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

112 
(* Term.term > bool *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

113 
fun is_clause (Const ("op ", _) $ x $ y) = is_clause x andalso is_clause y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

114 
 is_clause x = is_literal x; 
17618  115 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

116 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

117 
(* clause_is_trivial: a clause is trivially true if it contains both an atom *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

118 
(* and the atom's negation *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

119 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

120 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

121 
(* Term.term > bool *) 
17618  122 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

123 
fun clause_is_trivial c = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

124 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

125 
(* Term.term > Term.term *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

126 
fun dual (Const ("Not", _) $ x) = x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

127 
 dual x = HOLogic.Not $ x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

128 
(* Term.term list > bool *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

129 
fun has_duals [] = false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

130 
 has_duals (x::xs) = (dual x) mem xs orelse has_duals xs 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

131 
in 
24958  132 
has_duals (HOLogic.disjuncts c) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

133 
end; 
17618  134 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

135 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

136 
(* clause2raw_thm: translates a clause into a raw clause, i.e. *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

137 
(* [...]  x1  ...  xn *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

138 
(* (where each xi is a literal) is translated to *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

139 
(* [..., x1', ..., xn']  False , *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

140 
(* where each xi' is the negation normal form of ~xi *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

141 
(*  *) 
17618  142 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

143 
(* Thm.thm > Thm.thm *) 
17618  144 

20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

145 
fun clause2raw_thm clause = 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

146 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

147 
(* eliminates negated disjunctions from the ith premise, possibly *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

148 
(* adding new premises, then continues with the (i+1)th premise *) 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

149 
(* int > Thm.thm > Thm.thm *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

150 
fun not_disj_to_prem i thm = 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

151 
if i > nprems_of thm then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

152 
thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

153 
else 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

154 
not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

155 
(* moves all premises to hyps, i.e. "[...]  A1 ==> ... ==> An ==> B" *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

156 
(* becomes "[..., A1, ..., An]  B" *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

157 
(* Thm.thm > Thm.thm *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

158 
fun prems_to_hyps thm = 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

159 
fold (fn cprem => fn thm' => 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

160 
Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

161 
in 
20440
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

162 
(* [...]  ~(x1  ...  xn) ==> False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

163 
(clause2raw_notE OF [clause]) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

164 
(* [...]  ~x1 ==> ... ==> ~xn ==> False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

165 
> not_disj_to_prem 1 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

166 
(* [...]  x1' ==> ... ==> xn' ==> False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

167 
> Seq.hd o TRYALL (rtac clause2raw_not_not) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

168 
(* [..., x1', ..., xn']  False *) 
e6fe74eebda3
faster clause representation (again): full CNF formula as a hypothesis, instead of separate clauses
webertj
parents:
19236
diff
changeset

169 
> prems_to_hyps 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

170 
end; 
17618  171 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

172 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

173 
(* inst_thm: instantiates a theorem with a list of terms *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

174 
(*  *) 
17618  175 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

176 
fun inst_thm thy ts thm = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

177 
instantiate' [] (map (SOME o cterm_of thy) ts) thm; 
17618  178 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

179 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

180 
(* Naive CNF transformation *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

181 
(*  *) 
17618  182 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

183 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

184 
(* make_nnf_thm: produces a theorem of the form t = t', where t' is the *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

185 
(* negation normal form (i.e. negation only occurs in front of atoms) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

186 
(* of t; implications (">") and equivalences ("=" on bool) are *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

187 
(* eliminated (possibly causing an exponential blowup) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

188 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

189 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

190 
(* Theory.theory > Term.term > Thm.thm *) 
17618  191 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

192 
fun make_nnf_thm thy (Const ("op &", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

193 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

194 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

195 
val thm2 = make_nnf_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

196 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

197 
conj_cong OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

198 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

199 
 make_nnf_thm thy (Const ("op ", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

200 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

201 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

202 
val thm2 = make_nnf_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

203 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

204 
disj_cong OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

205 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

206 
 make_nnf_thm thy (Const ("op >", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

207 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

208 
val thm1 = make_nnf_thm thy (HOLogic.Not $ x) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

209 
val thm2 = make_nnf_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

210 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

211 
make_nnf_imp OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

212 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

213 
 make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

214 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

215 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

216 
val thm2 = make_nnf_thm thy (HOLogic.Not $ x) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

217 
val thm3 = make_nnf_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

218 
val thm4 = make_nnf_thm thy (HOLogic.Not $ y) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

219 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

220 
make_nnf_iff OF [thm1, thm2, thm3, thm4] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

221 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

222 
 make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

223 
make_nnf_not_false 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

224 
 make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

225 
make_nnf_not_true 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

226 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

227 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

228 
val thm1 = make_nnf_thm thy (HOLogic.Not $ x) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

229 
val thm2 = make_nnf_thm thy (HOLogic.Not $ y) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

230 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

231 
make_nnf_not_conj OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

232 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

233 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("op ", _) $ x $ y)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

234 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

235 
val thm1 = make_nnf_thm thy (HOLogic.Not $ x) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

236 
val thm2 = make_nnf_thm thy (HOLogic.Not $ y) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

237 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

238 
make_nnf_not_disj OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

239 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

240 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("op >", _) $ x $ y)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

241 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

242 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

243 
val thm2 = make_nnf_thm thy (HOLogic.Not $ y) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

244 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

245 
make_nnf_not_imp OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

246 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

247 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

248 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

249 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

250 
val thm2 = make_nnf_thm thy (HOLogic.Not $ x) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

251 
val thm3 = make_nnf_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

252 
val thm4 = make_nnf_thm thy (HOLogic.Not $ y) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

253 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

254 
make_nnf_not_iff OF [thm1, thm2, thm3, thm4] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

255 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

256 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

257 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

258 
val thm1 = make_nnf_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

259 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

260 
make_nnf_not_not OF [thm1] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

261 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

262 
 make_nnf_thm thy t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

263 
inst_thm thy [t] iff_refl; 
17618  264 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

265 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

266 
(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

267 
(* t, but simplified wrt. the following theorems: *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

268 
(* (True & x) = x *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

269 
(* (x & True) = x *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

270 
(* (False & x) = False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

271 
(* (x & False) = False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

272 
(* (True  x) = True *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

273 
(* (x  True) = True *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

274 
(* (False  x) = x *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

275 
(* (x  False) = x *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

276 
(* No simplification is performed below connectives other than & and . *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

277 
(* Optimization: The righthand side of a conjunction (disjunction) is *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

278 
(* simplified only if the lefthand side does not simplify to False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

279 
(* (True, respectively). *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

280 
(*  *) 
17618  281 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

282 
(* Theory.theory > Term.term > Thm.thm *) 
17618  283 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

284 
fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

285 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

286 
val thm1 = simp_True_False_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

287 
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

288 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

289 
if x' = HOLogic.false_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

290 
simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

291 
else 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

292 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

293 
val thm2 = simp_True_False_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

294 
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

295 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

296 
if x' = HOLogic.true_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

297 
simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

298 
else if y' = HOLogic.false_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

299 
simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

300 
else if y' = HOLogic.true_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

301 
simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

302 
else 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

303 
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

304 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

305 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

306 
 simp_True_False_thm thy (Const ("op ", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

307 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

308 
val thm1 = simp_True_False_thm thy x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

309 
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

310 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

311 
if x' = HOLogic.true_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

312 
simp_TF_disj_True_l OF [thm1] (* (x  y) = True *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

313 
else 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

314 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

315 
val thm2 = simp_True_False_thm thy y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

316 
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

317 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

318 
if x' = HOLogic.false_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

319 
simp_TF_disj_False_l OF [thm1, thm2] (* (x  y) = y' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

320 
else if y' = HOLogic.true_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

321 
simp_TF_disj_True_r OF [thm2] (* (x  y) = True *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

322 
else if y' = HOLogic.false_const then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

323 
simp_TF_disj_False_r OF [thm1, thm2] (* (x  y) = x' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

324 
else 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

325 
disj_cong OF [thm1, thm2] (* (x  y) = (x'  y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

326 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

327 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

328 
 simp_True_False_thm thy t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

329 
inst_thm thy [t] iff_refl; (* t = t *) 
17618  330 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

331 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

332 
(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

333 
(* is in conjunction normal form. May cause an exponential blowup *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

334 
(* in the length of the term. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

335 
(*  *) 
17618  336 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

337 
(* Theory.theory > Term.term > Thm.thm *) 
17618  338 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

339 
fun make_cnf_thm thy t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

340 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

341 
(* Term.term > Thm.thm *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

342 
fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

343 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

344 
val thm1 = make_cnf_thm_from_nnf x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

345 
val thm2 = make_cnf_thm_from_nnf y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

346 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

347 
conj_cong OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

348 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

349 
 make_cnf_thm_from_nnf (Const ("op ", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

350 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

351 
(* produces a theorem "(x'  y') = t'", where x', y', and t' are in CNF *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

352 
fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

353 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

354 
val thm1 = make_cnf_disj_thm x1 y' 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

355 
val thm2 = make_cnf_disj_thm x2 y' 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

356 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

357 
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2)  y') = ((x1  y')' & (x2  y')') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

358 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

359 
 make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

360 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

361 
val thm1 = make_cnf_disj_thm x' y1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

362 
val thm2 = make_cnf_disj_thm x' y2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

363 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

364 
make_cnf_disj_conj_r OF [thm1, thm2] (* (x'  (y1 & y2)) = ((x'  y1)' & (x'  y2)') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

365 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

366 
 make_cnf_disj_thm x' y' = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

367 
inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x'  y') = (x'  y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

368 
val thm1 = make_cnf_thm_from_nnf x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

369 
val thm2 = make_cnf_thm_from_nnf y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

370 
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

371 
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

372 
val disj_thm = disj_cong OF [thm1, thm2] (* (x  y) = (x'  y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

373 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

374 
iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

375 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

376 
 make_cnf_thm_from_nnf t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

377 
inst_thm thy [t] iff_refl 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

378 
(* convert 't' to NNF first *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

379 
val nnf_thm = make_nnf_thm thy t 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

380 
val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

381 
(* then simplify wrt. True/False (this should preserve NNF) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

382 
val simp_thm = simp_True_False_thm thy nnf 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

383 
val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

384 
(* finally, convert to CNF (this should preserve the simplification) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

385 
val cnf_thm = make_cnf_thm_from_nnf simp 
17618  386 
in 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

387 
iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

388 
end; 
17618  389 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

390 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

391 
(* CNF transformation by introducing new literals *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

392 
(*  *) 
17618  393 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

394 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

395 
(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

396 
(* t' is almost in conjunction normal form, except that conjunctions *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

397 
(* and existential quantifiers may be nested. (Use e.g. 'REPEAT_DETERM *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

398 
(* (etac exE i ORELSE etac conjE i)' afterwards to normalize.) May *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

399 
(* introduce new (existentially bound) literals. Note: the current *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

400 
(* implementation calls 'make_nnf_thm', causing an exponential blowup *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

401 
(* in the case of nested equivalences. *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

402 
(*  *) 
17618  403 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

404 
(* Theory.theory > Term.term > Thm.thm *) 
17618  405 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

406 
fun make_cnfx_thm thy t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

407 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

408 
val var_id = ref 0 (* properly initialized below *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

409 
(* unit > Term.term *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

410 
fun new_free () = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

411 
Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

412 
(* Term.term > Thm.thm *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

413 
fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

414 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

415 
val thm1 = make_cnfx_thm_from_nnf x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

416 
val thm2 = make_cnfx_thm_from_nnf y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

417 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

418 
conj_cong OF [thm1, thm2] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

419 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

420 
 make_cnfx_thm_from_nnf (Const ("op ", _) $ x $ y) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

421 
if is_clause x andalso is_clause y then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

422 
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

423 
else if is_literal y orelse is_literal x then let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

424 
(* produces a theorem "(x'  y') = t'", where x', y', and t' are *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

425 
(* almost in CNF, and x' or y' is a literal *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

426 
fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

427 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

428 
val thm1 = make_cnfx_disj_thm x1 y' 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

429 
val thm2 = make_cnfx_disj_thm x2 y' 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

430 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

431 
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2)  y') = ((x1  y')' & (x2  y')') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

432 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

433 
 make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

434 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

435 
val thm1 = make_cnfx_disj_thm x' y1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

436 
val thm2 = make_cnfx_disj_thm x' y2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

437 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

438 
make_cnf_disj_conj_r OF [thm1, thm2] (* (x'  (y1 & y2)) = ((x'  y1)' & (x'  y2)') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

439 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

440 
 make_cnfx_disj_thm (Const ("Ex", _) $ x') y' = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

441 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

442 
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x')  y') = (Ex (x'  y')) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

443 
val var = new_free () 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

444 
val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

445 
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

446 
val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

447 
val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x'  y')) = (EX v. body') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

448 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

449 
iff_trans OF [thm1, thm5] (* ((Ex x')  y') = (Ex v. body') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

450 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

451 
 make_cnfx_disj_thm x' (Const ("Ex", _) $ y') = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

452 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

453 
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x'  (Ex y')) = (Ex (x'  y')) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

454 
val var = new_free () 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

455 
val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

456 
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

457 
val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x'  y') = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

458 
val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x'  y')) = (EX v. body') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

459 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

460 
iff_trans OF [thm1, thm5] (* (x'  (Ex y')) = (EX v. body') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

461 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

462 
 make_cnfx_disj_thm x' y' = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

463 
inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x'  y') = (x'  y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

464 
val thm1 = make_cnfx_thm_from_nnf x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

465 
val thm2 = make_cnfx_thm_from_nnf y 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

466 
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

467 
val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

468 
val disj_thm = disj_cong OF [thm1, thm2] (* (x  y) = (x'  y') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

469 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

470 
iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

471 
end else let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

472 
val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x  y) = EX v. (x  v) & (y  ~v) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

473 
val var = new_free () 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

474 
val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

475 
val thm2 = make_cnfx_thm_from_nnf body (* (x  v) & (y  ~v) = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

476 
val thm3 = forall_intr (cterm_of thy var) thm2 (* !!v. (x  v) & (y  ~v) = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

477 
val thm4 = strip_shyps (thm3 COMP allI) (* ALL v. (x  v) & (y  ~v) = body' *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

478 
val thm5 = strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x  v) & (y  ~v)) = (EX v. body') *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

479 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

480 
iff_trans OF [thm1, thm5] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

481 
end 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

482 
 make_cnfx_thm_from_nnf t = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

483 
inst_thm thy [t] iff_refl 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

484 
(* convert 't' to NNF first *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

485 
val nnf_thm = make_nnf_thm thy t 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

486 
val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

487 
(* then simplify wrt. True/False (this should preserve NNF) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

488 
val simp_thm = simp_True_False_thm thy nnf 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

489 
val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

490 
(* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

491 
val _ = (var_id := fold (fn free => fn max => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

492 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

493 
val (name, _) = dest_Free free 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

494 
val idx = if String.isPrefix "cnfx_" name then 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

495 
(Int.fromString o String.extract) (name, String.size "cnfx_", NONE) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

496 
else 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

497 
NONE 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

498 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

499 
Int.max (max, getOpt (idx, 0)) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
26341
diff
changeset

500 
end) (OldTerm.term_frees simp) 0) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

501 
(* finally, convert to definitional CNF (this should preserve the simplification) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

502 
val cnfx_thm = make_cnfx_thm_from_nnf simp 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

503 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

504 
iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

505 
end; 
17618  506 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

507 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

508 
(* Tactics *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

509 
(*  *) 
17618  510 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

511 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

512 
(* weakening_tac: removes the first hypothesis of the 'i'th subgoal *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

513 
(*  *) 
17618  514 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

515 
(* int > Tactical.tactic *) 
17618  516 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

517 
fun weakening_tac i = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

518 
dtac weakening_thm i THEN atac (i+1); 
17618  519 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

520 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

521 
(* cnf_rewrite_tac: converts all premises of the 'i'th subgoal to CNF *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

522 
(* (possibly causing an exponential blowup in the length of each *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

523 
(* premise) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

524 
(*  *) 
17618  525 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

526 
(* int > Tactical.tactic *) 
17618  527 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

528 
fun cnf_rewrite_tac i = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

529 
(* cut the CNF formulas as new premises *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

530 
METAHYPS (fn prems => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

531 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

532 
val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

533 
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

534 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

535 
cut_facts_tac cut_thms 1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

536 
end) i 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

537 
(* remove the original premises *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

538 
THEN SELECT_GOAL (fn thm => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

539 
let 
21576  540 
val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

541 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

542 
PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

543 
end) i; 
17618  544 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

545 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

546 
(* cnfx_rewrite_tac: converts all premises of the 'i'th subgoal to CNF *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

547 
(* (possibly introducing new literals) *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

548 
(*  *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

549 

195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

550 
(* int > Tactical.tactic *) 
17618  551 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

552 
fun cnfx_rewrite_tac i = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

553 
(* cut the CNF formulas as new premises *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

554 
METAHYPS (fn prems => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

555 
let 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

556 
val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

557 
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

558 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

559 
cut_facts_tac cut_thms 1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

560 
end) i 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

561 
(* remove the original premises *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

562 
THEN SELECT_GOAL (fn thm => 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

563 
let 
21576  564 
val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

565 
in 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

566 
PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

567 
end) i; 
17618  568 

17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

569 
end; (* of structure *) 