author  webertj 
Fri, 10 Mar 2006 16:31:50 +0100  
changeset 19236  150e8b0fb991 
parent 17809  195045659c06 
child 20440  e6fe74eebda3 
permissions  rwrr 
17618  1 
(* Title: HOL/Tools/cnf_funcs.ML 
2 
ID: $Id$ 

3 
Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr) 

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

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

5 
Copyright 20052006 
17618  6 

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 

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

26 
x1', x2', ..., xn', ~ (x1  x2  ...  xn) ==> False  False , 
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 
Raw clauses may contain further hyps of the form "~ clause ==> False". 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

31 
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

32 
during SAT proof reconstruction. 
17618  33 
*) 
34 

35 
signature CNF = 

36 
sig 

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

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

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

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

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

41 

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

42 
val clause2raw_thm : Thm.thm > Thm.thm 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

43 
val rawhyps2clausehyps_thm : Thm.thm > Thm.thm 
17618  44 

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

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

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

47 
val make_cnf_thm : Theory.theory > Term.term > Thm.thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

48 
val make_cnfx_thm : Theory.theory > Term.term > Thm.thm 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

49 
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

50 
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

51 
end; 
17618  52 

53 
structure cnf : CNF = 

54 
struct 

55 

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

56 
(* string > Thm.thm *) 
17618  57 
fun thm_by_auto G = 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

58 
prove_goal (the_context ()) G (fn prems => [cut_facts_tac prems 1, Auto_tac]); 
17618  59 

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

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

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

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

63 
val clause2raw_not_not = thm_by_auto "P ==> ~~P"; 
17618  64 

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

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

66 
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

67 
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

68 
val disj_cong = thm_by_auto "[ P = P'; Q = Q' ] ==> (P  Q) = (P'  Q')"; 
17618  69 

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

70 
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

71 
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

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

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

74 
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

75 
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

76 
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

77 
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

78 
val make_nnf_not_not = thm_by_auto "P = P' ==> (~~P) = P'"; 
17618  79 

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

80 
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

81 
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

82 
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

83 
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

84 
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

85 
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

86 
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

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

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

89 
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

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

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

92 
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

93 
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

94 
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

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

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

97 
val weakening_thm = thm_by_auto "[ P; Q ] ==> Q"; 
17618  98 

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

99 
val cnftac_eq_imp = thm_by_auto "[ P = Q; P ] ==> Q"; 
17618  100 

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

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

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

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

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

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

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

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

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

109 
 is_atom _ = true; 
17618  110 

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

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

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

113 
 is_literal x = is_atom x; 
17618  114 

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

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

116 
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

117 
 is_clause x = is_literal x; 
17618  118 

17809
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 
(* 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

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

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

123 

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

124 
(* Term.term > bool *) 
17618  125 

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

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

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

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

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

130 
 collect_literals x ls = x :: ls 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

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

136 
 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

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

138 
has_duals (collect_literals c []) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

139 
end; 
17618  140 

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

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

142 
(* clause2raw_thm: translates a clause into a raw clause, i.e. *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

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

144 
(* (where each xi is a literal) is translated to *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

145 
(* ~(x1  ...  xn) ==> False, x1', ..., xn'  False , *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

147 
(*  *) 
17618  148 

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

149 
(* Thm.thm > Thm.thm *) 
17618  150 

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

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

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

153 
val disj = HOLogic.dest_Trueprop (prop_of c) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

154 
val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

155 
val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false) (* ~(x1  ...  xn) ==> False  ~(x1  ...  xn) ==> False *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

157 
(* adding new premises, then continues with the (i+1)th premise *) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

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

163 
not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

164 
val thm2 = not_disj_to_prem thm1 1 (* ~(x1  ...  xn) ==> False  ~x1 ==> ... ==> ~xn ==> False *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

165 
val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2) (* ~(x1  ...  xn) ==> False  x1' ==> ... ==> xn' ==> False *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

166 
val thy3 = theory_of_thm thm3 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

167 
val thm4 = fold (fn prem => fn thm => Thm.implies_elim thm (Thm.assume (cterm_of thy3 prem))) (prems_of thm3) thm3 (* ~(x1  ...  xn) ==> False, x1', ..., xn'  False *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

169 
thm4 
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 
(*  *) 
19236
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

173 
(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

174 
(* hyps of the form "P" *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

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

176 

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

177 
(* Thm.thm > Thm.thm *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

178 

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

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

180 
fold (fn hyp => fn thm => 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

181 
case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) => 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

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

183 
val cterm = cterm_of (theory_of_thm thm) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

184 
val thm1 = Thm.implies_intr (cterm hyp) thm (* hyps  (~P ==> False) ==> goal *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

185 
val varP = Var (("P", 0), HOLogic.boolT) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

186 
val notE = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE (* P ==> ~P ==> False *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

187 
val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P))) (* P  ~P ==> False *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

188 
val thm2 = Thm.implies_elim thm1 notE' (* hyps, P  goal *) 
150e8b0fb991
clauses now use (meta)hyps instead of (meta)implications; significant speedup
webertj
parents:
17809
diff
changeset

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

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

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

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

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

194 

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

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

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

197 
(*  *) 
17618  198 

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

199 
(* Theory.theory > Term.term list > Thm.thm > Thm.thm *) 
17618  200 

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

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

202 
instantiate' [] (map (SOME o cterm_of thy) ts) thm; 
17618  203 

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

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

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

206 
(*  *) 
17618  207 

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

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

209 
(* 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

210 
(* 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

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

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

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

214 

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

215 
(* Theory.theory > Term.term > Thm.thm *) 
17618  216 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

238 
 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

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

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

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

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

243 
val thm4 = 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_iff OF [thm1, thm2, thm3, thm4] 
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 ("False", _)) = 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

272 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

288 
inst_thm thy [t] iff_refl; 
17618  289 

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

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

291 
(* 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

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

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

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

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

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

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

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

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

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

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

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

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

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

305 
(*  *) 
17618  306 

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

307 
(* Theory.theory > Term.term > Thm.thm *) 
17618  308 

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

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

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

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

312 
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

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

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

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

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

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

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

319 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

334 
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

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

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

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

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

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

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

341 
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

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

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

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

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

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

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

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

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

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

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

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

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

354 
inst_thm thy [t] iff_refl; (* t = t *) 
17618  355 

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

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

357 
(* 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

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

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

360 
(*  *) 
17618  361 

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

362 
(* Theory.theory > Term.term > Thm.thm *) 
17618  363 

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

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

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

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

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

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

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

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

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

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

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

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

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

376 
(* 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

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

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

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

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

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

382 
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

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

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

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

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

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

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

389 
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

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

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

392 
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

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

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

395 
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

396 
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

397 
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

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

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

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

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

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

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

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

405 
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

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

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

408 
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

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

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

412 
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

413 
end; 
17618  414 

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

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

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

417 
(*  *) 
17618  418 

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

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

420 
(* 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

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

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

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

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

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

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

427 
(*  *) 
17618  428 

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

429 
(* Theory.theory > Term.term > Thm.thm *) 
17618  430 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

449 
(* 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

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

451 
fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) 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 = make_cnfx_disj_thm x1 y' 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

456 
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

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

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

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

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

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

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

463 
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

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

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

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

467 
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

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

469 
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

470 
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

471 
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

472 
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

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

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

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

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

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

478 
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

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

480 
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

481 
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

482 
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

483 
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

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

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

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

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

488 
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

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

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

491 
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

492 
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

493 
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

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

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

496 
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

497 
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

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

499 
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

500 
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

501 
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

502 
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

503 
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

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

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

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

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

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

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

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

511 
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

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

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

514 
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

515 
(* 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

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

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

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

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

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

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

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

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

524 
Int.max (max, getOpt (idx, 0)) 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

529 
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

530 
end; 
17618  531 

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

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

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

534 
(*  *) 
17618  535 

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

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

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

538 
(*  *) 
17618  539 

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

540 
(* int > Tactical.tactic *) 
17618  541 

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

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

543 
dtac weakening_thm i THEN atac (i+1); 
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 
(* 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

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

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

549 
(*  *) 
17618  550 

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

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

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

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

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

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

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

557 
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

558 
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

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

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

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

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

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

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

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

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

567 
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

568 
end) i; 
17618  569 

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

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

571 
(* 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

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

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

574 

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

575 
(* int > Tactical.tactic *) 
17618  576 

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

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

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

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

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

581 
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

582 
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

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

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

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

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

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

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

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

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

591 
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

592 
end) i; 
17618  593 

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

594 
end; (* of structure *) 