author  wenzelm 
Wed, 21 Oct 2009 00:36:12 +0200  
changeset 33035  15eab423e573 
parent 32960  69916a850301 
child 36614  b6c031ad3690 
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 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

5 
FIXME: major overlaps with the code in meson.ML 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

6 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

7 
Functions and tactics to transform a formula into Conjunctive Normal 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

8 
Form (CNF). 
24958  9 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

10 
A formula in CNF is of the following form: 
17618  11 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

12 
(x11  x12  ...  x1n) & ... & (xm1  xm2  ...  xmk) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

13 
False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

14 
True 
17618  15 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

16 
where each xij is a literal (a positive or negative atomic Boolean 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

17 
term), i.e. the formula is a conjunction of disjunctions of literals, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

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

19 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

22 
For the purpose of SAT proof reconstruction, we also make use of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

23 
another representation of clauses, which we call the "raw clauses". 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

24 
Raw clauses are of the form 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

25 

69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

26 
[..., x1', x2', ..., xn']  False , 
17618  27 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

28 
where each xi is a literal, and each xi' is the negation normal form 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

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

30 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

31 
Literals are successively removed from the hyps of raw clauses by 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32740
diff
changeset

32 
resolution during SAT proof reconstruction. 
17618  33 
*) 
34 

35 
signature CNF = 

36 
sig 

32232  37 
val is_atom: term > bool 
38 
val is_literal: term > bool 

39 
val is_clause: term > bool 

40 
val clause_is_trivial: term > bool 

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

41 

32232  42 
val clause2raw_thm: thm > thm 
17618  43 

32232  44 
val weakening_tac: int > tactic (* removes the first hypothesis of a subgoal *) 
17618  45 

32232  46 
val make_cnf_thm: theory > term > thm 
47 
val make_cnfx_thm: theory > term > thm 

48 
val cnf_rewrite_tac: Proof.context > int > tactic (* converts all prems of a subgoal to CNF *) 

49 
val cnfx_rewrite_tac: Proof.context > int > tactic 

50 
(* converts all prems of a subgoal to (almost) definitional CNF *) 

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

51 
end; 
17618  52 

53 
structure cnf : CNF = 

54 
struct 

55 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

56 
val clause2raw_notE = @{lemma "[ P; ~P ] ==> False" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

57 
val clause2raw_not_disj = @{lemma "[ ~P; ~Q ] ==> ~(P  Q)" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

58 
val clause2raw_not_not = @{lemma "P ==> ~~P" by auto}; 
17618  59 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

60 
val iff_refl = @{lemma "(P::bool) = P" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

61 
val iff_trans = @{lemma "[ (P::bool) = Q; Q = R ] ==> P = R" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

62 
val conj_cong = @{lemma "[ P = P'; Q = Q' ] ==> (P & Q) = (P' & Q')" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

63 
val disj_cong = @{lemma "[ P = P'; Q = Q' ] ==> (P  Q) = (P'  Q')" by auto}; 
17618  64 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

65 
val make_nnf_imp = @{lemma "[ (~P) = P'; Q = Q' ] ==> (P > Q) = (P'  Q')" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

66 
val make_nnf_iff = @{lemma "[ P = P'; (~P) = NP; Q = Q'; (~Q) = NQ ] ==> (P = Q) = ((P'  NQ) & (NP  Q'))" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

67 
val make_nnf_not_false = @{lemma "(~False) = True" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

68 
val make_nnf_not_true = @{lemma "(~True) = False" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

69 
val make_nnf_not_conj = @{lemma "[ (~P) = P'; (~Q) = Q' ] ==> (~(P & Q)) = (P'  Q')" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

70 
val make_nnf_not_disj = @{lemma "[ (~P) = P'; (~Q) = Q' ] ==> (~(P  Q)) = (P' & Q')" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

71 
val make_nnf_not_imp = @{lemma "[ P = P'; (~Q) = Q' ] ==> (~(P > Q)) = (P' & Q')" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

72 
val make_nnf_not_iff = @{lemma "[ P = P'; (~P) = NP; Q = Q'; (~Q) = NQ ] ==> (~(P = Q)) = ((P'  Q') & (NP  NQ))" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

73 
val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto}; 
17618  74 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

75 
val simp_TF_conj_True_l = @{lemma "[ P = True; Q = Q' ] ==> (P & Q) = Q'" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

76 
val simp_TF_conj_True_r = @{lemma "[ P = P'; Q = True ] ==> (P & Q) = P'" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

77 
val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

78 
val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

79 
val simp_TF_disj_True_l = @{lemma "P = True ==> (P  Q) = True" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

80 
val simp_TF_disj_True_r = @{lemma "Q = True ==> (P  Q) = True" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

81 
val simp_TF_disj_False_l = @{lemma "[ P = False; Q = Q' ] ==> (P  Q) = Q'" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

82 
val simp_TF_disj_False_r = @{lemma "[ P = P'; Q = False ] ==> (P  Q) = P'" by auto}; 
17618  83 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

84 
val make_cnf_disj_conj_l = @{lemma "[ (P  R) = PR; (Q  R) = QR ] ==> ((P & Q)  R) = (PR & QR)" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

85 
val make_cnf_disj_conj_r = @{lemma "[ (P  Q) = PQ; (P  R) = PR ] ==> (P  (Q & R)) = (PQ & PR)" by auto}; 
17618  86 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

87 
val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x)  Q) = (EX x. P x  Q)" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

88 
val make_cnfx_disj_ex_r = @{lemma "(P  (EX (x::bool). Q x)) = (EX x. P  Q x)" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

89 
val make_cnfx_newlit = @{lemma "(P  Q) = (EX x. (P  x) & (Q  ~x))" by auto}; 
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

90 
val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto}; 
17618  91 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

92 
val weakening_thm = @{lemma "[ P; Q ] ==> Q" by auto}; 
17618  93 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
29265
diff
changeset

94 
val cnftac_eq_imp = @{lemma "[ P = Q; P ] ==> Q" by auto}; 
17618  95 

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

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

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

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

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

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

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

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

103 
 is_atom _ = true; 
17618  104 

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

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

106 
 is_literal x = is_atom x; 
17618  107 

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

108 
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

109 
 is_clause x = is_literal x; 
17618  110 

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

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

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

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

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

115 

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

116 
(* Term.term > bool *) 
17618  117 

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

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

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

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

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

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

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

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

125 
 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

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

128 
end; 
17618  129 

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

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

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

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

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

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

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

136 
(*  *) 
17618  137 

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

138 
(* Thm.thm > Thm.thm *) 
17618  139 

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

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

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

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

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

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

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

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

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

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

149 
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

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

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

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

153 
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

154 
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

155 
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

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

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

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

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

160 
> 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

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

162 
> 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

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

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

165 
end; 
17618  166 

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

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

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

169 
(*  *) 
17618  170 

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

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

172 
instantiate' [] (map (SOME o cterm_of thy) ts) thm; 
17618  173 

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

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

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

176 
(*  *) 
17618  177 

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

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

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

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

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

182 
(* eliminated (possibly causing an exponential blowup) *) 
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 

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

185 
(* Theory.theory > Term.term > Thm.thm *) 
17618  186 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

208 
 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

242 
 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

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

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

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

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

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

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

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

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

251 
 make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) = 
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 x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

258 
inst_thm thy [t] iff_refl; 
17618  259 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

275 
(*  *) 
17618  276 

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

277 
(* Theory.theory > Term.term > Thm.thm *) 
17618  278 

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

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

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

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

282 
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

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

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

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

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

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

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

289 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

304 
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

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

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

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

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

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

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

311 
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

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

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

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

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

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

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

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

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

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

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

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

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

324 
inst_thm thy [t] iff_refl; (* t = t *) 
17618  325 

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

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

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

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

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

330 
(*  *) 
17618  331 

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

332 
(* Theory.theory > Term.term > Thm.thm *) 
17618  333 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

352 
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

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

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

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

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

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

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

359 
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

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

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

362 
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

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

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

365 
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

366 
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

367 
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

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

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

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

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

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

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

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

375 
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

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

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

378 
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

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

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

382 
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

383 
end; 
17618  384 

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

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

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

387 
(*  *) 
17618  388 

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

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

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

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

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

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

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

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

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

397 
(*  *) 
17618  398 

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

399 
(* Theory.theory > Term.term > Thm.thm *) 
17618  400 

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

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

402 
let 
32740  403 
val var_id = Unsynchronized.ref 0 (* properly initialized below *) 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

404 
fun new_free () = 
32740  405 
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT) 
406 
fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm = 

17809
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 thm1 = make_cnfx_thm_from_nnf x 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

424 
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

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

426 
 make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) = 
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 x' y1 
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

429 
val thm2 = make_cnfx_disj_thm x' y2 
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_r OF [thm1, thm2] (* (x'  (y1 & y2)) = ((x'  y1)' & (x'  y2)') *) 
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 (Const ("Ex", _) $ x') y' = 
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 = 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

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

437 
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

438 
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

439 
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

440 
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

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

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

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

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

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

446 
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

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

448 
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

449 
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

450 
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

451 
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

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

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

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

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

456 
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

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

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

459 
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

460 
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

461 
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

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

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

464 
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

465 
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

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

467 
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

468 
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

469 
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

470 
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

471 
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

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

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

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

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

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

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

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

479 
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

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

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

482 
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

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

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

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

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

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

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

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

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

491 
in 
33035  492 
Int.max (max, the_default 0 idx) 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
26341
diff
changeset

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

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

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

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

497 
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

498 
end; 
17618  499 

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

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

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

502 
(*  *) 
17618  503 

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

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

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

506 
(*  *) 
17618  507 

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

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

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

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

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

515 
(*  *) 
17618  516 

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

518 
(* cut the CNF formulas as new premises *) 
32283  519 
Subgoal.FOCUS (fn {prems, ...} => 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

520 
let 
32232  521 
val thy = ProofContext.theory_of ctxt 
522 
val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems 

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

523 
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

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

525 
cut_facts_tac cut_thms 1 
32232  526 
end) ctxt i 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

529 
let 
21576  530 
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

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

532 
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

533 
end) i; 
17618  534 

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

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

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

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

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

539 

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

541 
(* cut the CNF formulas as new premises *) 
32283  542 
Subgoal.FOCUS (fn {prems, ...} => 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

543 
let 
32232  544 
val thy = ProofContext.theory_of ctxt; 
545 
val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems 

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

546 
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

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

548 
cut_facts_tac cut_thms 1 
32232  549 
end) ctxt i 
17809
195045659c06
Tactics sat and satx reimplemented, several improvements
webertj
parents:
17618
diff
changeset

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

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

552 
let 
21576  553 
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

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

555 
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

556 
end) i; 
17618  557 

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

558 
end; (* of structure *) 