author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37539  c80e77e8d036 
child 37781  2fbbf0a48cef 
permissions  rwrr 
9869  1 
(* Title: HOL/Tools/meson.ML 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

3 

9869  4 
The MESON resolution proof procedure for HOL. 
29267  5 
When making clauses, avoids using the rewriter  instead uses RS recursively. 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

6 
*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

7 

24300  8 
signature MESON = 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

9 
sig 
32955  10 
val trace: bool Unsynchronized.ref 
24300  11 
val term_pair_of: indexname * (typ * 'a) > term * 'a 
12 
val flexflex_first_order: thm > thm 

13 
val size_of_subgoals: thm > int 

26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

14 
val too_many_clauses: Proof.context option > term > bool 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

15 
val make_cnf: thm list > thm > Proof.context > thm list * Proof.context 
24300  16 
val finish_cnf: thm list > thm list 
32262  17 
val make_nnf: Proof.context > thm > thm 
18 
val skolemize: Proof.context > thm > thm 

24300  19 
val is_fol_term: theory > term > bool 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35625
diff
changeset

20 
val make_clauses_unsorted: thm list > thm list 
24300  21 
val make_clauses: thm list > thm list 
22 
val make_horns: thm list > thm list 

23 
val best_prolog_tac: (thm > int) > thm list > tactic 

24 
val depth_prolog_tac: thm list > tactic 

25 
val gocls: thm list > thm list 

32262  26 
val skolemize_prems_tac: Proof.context > thm list > int > tactic 
27 
val MESON: (thm list > thm list) > (thm list > tactic) > Proof.context > int > tactic 

28 
val best_meson_tac: (thm > int) > Proof.context > int > tactic 

29 
val safe_best_meson_tac: Proof.context > int > tactic 

30 
val depth_meson_tac: Proof.context > int > tactic 

24300  31 
val prolog_step_tac': thm list > int > tactic 
32 
val iter_deepen_prolog_tac: thm list > tactic 

32262  33 
val iter_deepen_meson_tac: Proof.context > thm list > int > tactic 
24300  34 
val make_meta_clause: thm > thm 
35 
val make_meta_clauses: thm list > thm list 

32262  36 
val meson_tac: Proof.context > thm list > int > tactic 
24300  37 
val negate_head: thm > thm 
38 
val select_literal: int > thm > thm 

32262  39 
val skolemize_tac: Proof.context > int > tactic 
40 
val setup: theory > theory 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

41 
end 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

42 

24300  43 
structure Meson: MESON = 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

44 
struct 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

45 

32955  46 
val trace = Unsynchronized.ref false; 
47 
fun trace_msg msg = if ! trace then tracing (msg ()) else (); 

48 

26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

49 
val max_clauses_default = 60; 
36001  50 
val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default); 
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

51 

31454  52 
val disj_forward = @{thm disj_forward}; 
53 
val disj_forward2 = @{thm disj_forward2}; 

54 
val make_pos_rule = @{thm make_pos_rule}; 

55 
val make_pos_rule' = @{thm make_pos_rule'}; 

56 
val make_pos_goal = @{thm make_pos_goal}; 

57 
val make_neg_rule = @{thm make_neg_rule}; 

58 
val make_neg_rule' = @{thm make_neg_rule'}; 

59 
val make_neg_goal = @{thm make_neg_goal}; 

60 
val conj_forward = @{thm conj_forward}; 

61 
val all_forward = @{thm all_forward}; 

62 
val ex_forward = @{thm ex_forward}; 

63 
val choice = @{thm choice}; 

64 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

65 
val not_conjD = thm "meson_not_conjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

66 
val not_disjD = thm "meson_not_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

67 
val not_notD = thm "meson_not_notD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

68 
val not_allD = thm "meson_not_allD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

69 
val not_exD = thm "meson_not_exD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

70 
val imp_to_disjD = thm "meson_imp_to_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

71 
val not_impD = thm "meson_not_impD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

72 
val iff_to_disjD = thm "meson_iff_to_disjD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

73 
val not_iffD = thm "meson_not_iffD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

74 
val conj_exD1 = thm "meson_conj_exD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

75 
val conj_exD2 = thm "meson_conj_exD2"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

76 
val disj_exD = thm "meson_disj_exD"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

77 
val disj_exD1 = thm "meson_disj_exD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

78 
val disj_exD2 = thm "meson_disj_exD2"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

79 
val disj_assoc = thm "meson_disj_assoc"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

80 
val disj_comm = thm "meson_disj_comm"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

81 
val disj_FalseD1 = thm "meson_disj_FalseD1"; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

82 
val disj_FalseD2 = thm "meson_disj_FalseD2"; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

83 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

84 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

85 
(**** Operators for forward proof ****) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

86 

20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

87 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

88 
(** Firstorder Resolution **) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

89 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

90 
fun typ_pair_of (ix, (sort,ty)) = (TVar (ix,sort), ty); 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

91 
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t); 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

92 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

93 
(*FIXME: currently does not "rename variables apart"*) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

94 
fun first_order_resolve thA thB = 
32262  95 
(case 
96 
try (fn () => 

97 
let val thy = theory_of_thm thA 

98 
val tmA = concl_of thA 

99 
val Const("==>",_) $ tmB $ _ = prop_of thB 

37398
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

100 
val tenv = 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

101 
Pattern.first_order_match thy (tmB, tmA) 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

102 
(Vartab.empty, Vartab.empty) > snd 
32262  103 
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) 
104 
in thA RS (cterm_instantiate ct_pairs thB) end) () of 

105 
SOME th => th 

37398
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

106 
 NONE => raise THM ("first_order_resolve", 0, [thA, thB])) 
18175
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset

107 

24300  108 
fun flexflex_first_order th = 
23440
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

109 
case (tpairs_of th) of 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

110 
[] => th 
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

111 
 pairs => 
24300  112 
let val thy = theory_of_thm th 
32032  113 
val (tyenv, tenv) = 
114 
fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) 

24300  115 
val t_pairs = map term_pair_of (Vartab.dest tenv) 
116 
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th 

117 
in th' end 

118 
handle THM _ => th; 

23440
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

119 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

120 
(*Forward proof while preserving bound variables names*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

121 
fun rename_bvs_RS th rl = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

122 
let val th' = th RS rl 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

123 
in Thm.rename_boundvars (concl_of th') (concl_of th) th' end; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

124 

340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

125 
(*raises exception if no rules apply*) 
24300  126 
fun tryres (th, rls) = 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

127 
let fun tryall [] = raise THM("tryres", 0, th::rls) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

128 
 tryall (rl::rls) = (rename_bvs_RS th rl handle THM _ => tryall rls) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

129 
in tryall rls end; 
24300  130 

21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

131 
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st, 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

132 
e.g. from conj_forward, should have the form 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

133 
"[ P' ==> ?P; Q' ==> ?Q ] ==> ?P & ?Q" 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

134 
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) 
32262  135 
fun forward_res ctxt nf st = 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

136 
let fun forward_tacf [prem] = rtac (nf prem) 1 
24300  137 
 forward_tacf prems = 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

138 
error (cat_lines 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

139 
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: 
32262  140 
Display.string_of_thm ctxt st :: 
141 
"Premises:" :: map (Display.string_of_thm ctxt) prems)) 

21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

142 
in 
32231
95b8afcbb0ed
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
wenzelm
parents:
32091
diff
changeset

143 
case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st) 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

144 
of SOME(th,_) => th 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

145 
 NONE => raise THM("forward_res", 0, [st]) 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

146 
end; 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

147 

20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

148 
(*Are any of the logical connectives in "bs" present in the term?*) 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

149 
fun has_conns bs = 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

150 
let fun has (Const(a,_)) = false 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

151 
 has (Const("Trueprop",_) $ p) = has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

152 
 has (Const("Not",_) $ p) = has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

153 
 has (Const("op ",_) $ p $ q) = member (op =) bs "op " orelse has p orelse has q 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

154 
 has (Const("op &",_) $ p $ q) = member (op =) bs "op &" orelse has p orelse has q 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

155 
 has (Const("All",_) $ Abs(_,_,p)) = member (op =) bs "All" orelse has p 
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

156 
 has (Const("Ex",_) $ Abs(_,_,p)) = member (op =) bs "Ex" orelse has p 
24300  157 
 has _ = false 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

158 
in has end; 
24300  159 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

160 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

161 
(**** Clause handling ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

162 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

163 
fun literals (Const("Trueprop",_) $ P) = literals P 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

164 
 literals (Const("op ",_) $ P $ Q) = literals P @ literals Q 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

165 
 literals (Const("Not",_) $ P) = [(false,P)] 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

166 
 literals P = [(true,P)]; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

167 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

168 
(*number of literals in a term*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

169 
val nliterals = length o literals; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

170 

18389  171 

172 
(*** Tautology Checking ***) 

173 

24300  174 
fun signed_lits_aux (Const ("op ", _) $ P $ Q) (poslits, neglits) = 
18389  175 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 
176 
 signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) 

177 
 signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); 

24300  178 

18389  179 
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); 
180 

181 
(*Literals like X=X are tautologous*) 

182 
fun taut_poslit (Const("op =",_) $ t $ u) = t aconv u 

183 
 taut_poslit (Const("True",_)) = true 

184 
 taut_poslit _ = false; 

185 

186 
fun is_taut th = 

187 
let val (poslits,neglits) = signed_lits th 

188 
in exists taut_poslit poslits 

189 
orelse 

20073  190 
exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) 
19894  191 
end 
24300  192 
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) 
18389  193 

194 

195 
(*** To remove trivial negated equality literals from clauses ***) 

196 

197 
(*They are typically functional reflexivity axioms and are the converses of 

198 
injectivity equivalences*) 

24300  199 

18389  200 
val not_refl_disj_D = thm"meson_not_refl_disj_D"; 
201 

20119  202 
(*Is either term a Var that does not properly occur in the other term?*) 
203 
fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) 

204 
 eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) 

205 
 eliminable _ = false; 

206 

18389  207 
fun refl_clause_aux 0 th = th 
208 
 refl_clause_aux n th = 

209 
case HOLogic.dest_Trueprop (concl_of th) of 

24300  210 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _) => 
18389  211 
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) 
24300  212 
 (Const ("op ", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
213 
if eliminable(t,u) 

214 
then refl_clause_aux (n1) (th RS not_refl_disj_D) (*Var inequation: delete*) 

215 
else refl_clause_aux (n1) (th RS disj_comm) (*not between Vars: ignore*) 

216 
 (Const ("op ", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) 

217 
 _ => (*not a disjunction*) th; 

18389  218 

24300  219 
fun notequal_lits_count (Const ("op ", _) $ P $ Q) = 
18389  220 
notequal_lits_count P + notequal_lits_count Q 
221 
 notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 

222 
 notequal_lits_count _ = 0; 

223 

224 
(*Simplify a clause by applying reflexivity to its negated equality literals*) 

24300  225 
fun refl_clause th = 
18389  226 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 
19894  227 
in zero_var_indexes (refl_clause_aux neqs th) end 
24300  228 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 
18389  229 

230 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

231 
(*** Removal of duplicate literals ***) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

232 

340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

233 
(*Forward proof, passing extra assumptions as theorems to the tactic*) 
32262  234 
fun forward_res2 ctxt nf hyps st = 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

235 
case Seq.pull 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

236 
(REPEAT 
32231
95b8afcbb0ed
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
wenzelm
parents:
32091
diff
changeset

237 
(OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

238 
st) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

239 
of SOME(th,_) => th 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

240 
 NONE => raise THM("forward_res2", 0, [st]); 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

241 

340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

242 
(*Remove duplicates in PQ by assuming ~P in Q 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

243 
rls (initially []) accumulates assumptions of the form P==>False*) 
32262  244 
fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

245 
handle THM _ => tryres(th,rls) 
32262  246 
handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2), 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

247 
[disj_FalseD1, disj_FalseD2, asm_rl]) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

248 
handle THM _ => th; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

249 

340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

250 
(*Remove duplicate literals, if there are any*) 
32262  251 
fun nodups ctxt th = 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

252 
if has_duplicates (op =) (literals (prop_of th)) 
32262  253 
then nodups_aux ctxt [] th 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

254 
else th; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

255 

340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

256 

18389  257 
(*** The basic CNF transformation ***) 
258 

26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

259 
fun too_many_clauses ctxto t = 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

260 
let 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

261 
val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

262 
 NONE => max_clauses_default 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

263 

9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

264 
fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl; 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

265 
fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl; 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

266 

9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

267 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

268 
fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

269 
 signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

270 
 signed_nclauses b (Const("op &",_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

271 
if b then sum (signed_nclauses b t) (signed_nclauses b u) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

272 
else prod (signed_nclauses b t) (signed_nclauses b u) 
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

273 
 signed_nclauses b (Const("op ",_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

274 
if b then prod (signed_nclauses b t) (signed_nclauses b u) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

275 
else sum (signed_nclauses b t) (signed_nclauses b u) 
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

276 
 signed_nclauses b (Const("op >",_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

277 
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

278 
else sum (signed_nclauses (not b) t) (signed_nclauses b u) 
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

279 
 signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

280 
if T = HOLogic.boolT then (*Boolean equality is ifandonlyif*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

281 
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

282 
(prod (signed_nclauses (not b) u) (signed_nclauses b t)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

283 
else sum (prod (signed_nclauses b t) (signed_nclauses b u)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

284 
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

285 
else 1 
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

286 
 signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

287 
 signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

288 
 signed_nclauses _ _ = 1; (* literal *) 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

289 
in 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

290 
signed_nclauses true t >= max_cl 
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
26424
diff
changeset

291 
end; 
19894  292 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

293 
(*Replaces universally quantified variables by FREE variables  because 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

294 
assumptions may not contain scheme variables. Later, generalize using Variable.export. *) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

295 
local 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

296 
val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))); 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

297 
val spec_varT = #T (Thm.rep_cterm spec_var); 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

298 
fun name_of (Const ("All", _) $ Abs(x,_,_)) = x  name_of _ = Name.uu; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

299 
in 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

300 
fun freeze_spec th ctxt = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

301 
let 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

302 
val cert = Thm.cterm_of (ProofContext.theory_of ctxt); 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

303 
val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

304 
val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec; 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

305 
in (th RS spec', ctxt') end 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

306 
end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

307 

15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

308 
(*Used with METAHYPS below. There is one assumption, which gets bound to prem 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

309 
and then normalized via function nf. The normal form is given to resolve_tac, 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

310 
instantiate a Boolean variable created by resolution with disj_forward. Since 
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

311 
(nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

312 
fun resop nf [prem] = resolve_tac (nf prem) 1; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

313 

24300  314 
(*Any need to extend this list with 
26424  315 
"HOL.type_class","HOL.eq_class","Pure.term"?*) 
24300  316 
val has_meta_conn = 
29684  317 
exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1); 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

318 

37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

319 
fun apply_skolem_theorem (th, rls) = 
37398
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

320 
let 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

321 
fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) 
37398
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

322 
 tryall (rl :: rls) = 
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

323 
first_order_resolve th rl handle THM _ => tryall rls 
e194213451c9
betaetacontract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset

324 
in tryall rls end 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

325 

37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

326 
(* Conjunctive normal form, adding clauses from th in front of ths (for foldr). 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

327 
Strips universal quantifiers and breaks up conjunctions. 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

328 
Eliminates existential quantifiers using Skolemization theorems. *) 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

329 
fun cnf skolem_ths ctxt (th, ths) = 
33222  330 
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

331 
fun cnf_aux (th,ths) = 
24300  332 
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*metalevel: ignore*) 
333 
else if not (has_conns ["All","Ex","op &"] (prop_of th)) 

32262  334 
then nodups ctxt th :: ths (*no work to do, terminate*) 
24300  335 
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of 
336 
Const ("op &", _) => (*conjunction*) 

337 
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) 

338 
 Const ("All", _) => (*universal quantifier*) 

24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

339 
let val (th',ctxt') = freeze_spec th (!ctxtr) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

340 
in ctxtr := ctxt'; cnf_aux (th', ths) end 
24300  341 
 Const ("Ex", _) => 
342 
(*existential quantifier: Insert Skolem functions*) 

37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

343 
cnf_aux (apply_skolem_theorem (th, skolem_ths), ths) 
24300  344 
 Const ("op ", _) => 
345 
(*Disjunction of P, Q: Create new goal of proving ?P  ?Q and solve it using 

346 
all combinations of converting P, Q to CNF.*) 

347 
let val tac = 

32262  348 
OldGoals.METAHYPS (resop cnf_nil) 1 THEN 
32231
95b8afcbb0ed
moved METAHYPS to old_goals.ML (cf. SUBPROOF and FOCUS in subgoal.ML for properly localized versions of the same idea);
wenzelm
parents:
32091
diff
changeset

349 
(fn st' => st' > OldGoals.METAHYPS (resop cnf_nil) 1) 
24300  350 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 
32262  351 
 _ => nodups ctxt th :: ths (*no work to do*) 
19154  352 
and cnf_nil th = cnf_aux (th,[]) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

353 
val cls = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

354 
if too_many_clauses (SOME ctxt) (concl_of th) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

355 
then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

356 
else cnf_aux (th,ths) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

357 
in (cls, !ctxtr) end; 
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1letter identifiers.
paulson
parents:
22381
diff
changeset

358 

37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset

359 
fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []); 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

360 

c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

361 
(*Generalization, removal of redundant equalities, removal of tautologies.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

362 
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

363 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

364 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

365 
(**** Generation of contrapositives ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

366 

24300  367 
fun is_left (Const ("Trueprop", _) $ 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

368 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _)) = true 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

369 
 is_left _ = false; 
24300  370 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

371 
(*Associate disjuctions to right  make leftmost disjunct a LITERAL*) 
24300  372 
fun assoc_right th = 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

373 
if is_left (prop_of th) then assoc_right (th RS disj_assoc) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

374 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

375 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

376 
(*Must check for negative literal first!*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

377 
val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

378 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

379 
(*For ordinary resolution. *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

380 
val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

381 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

382 
(*Create a goal or support clause, conclusing False*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

383 
fun make_goal th = (*Must check for negative literal first!*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

384 
make_goal (tryres(th, clause_rules)) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

385 
handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

386 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

387 
(*Sort clauses by number of literals*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

388 
fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

389 

18389  390 
fun sort_clauses ths = sort (make_ord fewerlits) ths; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

391 

15581  392 
(*True if the given type contains bool anywhere*) 
393 
fun has_bool (Type("bool",_)) = true 

394 
 has_bool (Type(_, Ts)) = exists has_bool Ts 

395 
 has_bool _ = false; 

24300  396 

397 
(*Is the string the name of a connective? Really only  and Not can remain, 

398 
since this code expects to be called on a clause form.*) 

19875  399 
val is_conn = member (op =) 
24300  400 
["Trueprop", "op &", "op ", "op >", "Not", 
37388  401 
"All", "Ex", @{const_name Ball}, @{const_name Bex}]; 
15613  402 

24300  403 
(*True if the term contains a functionnot a logical connectivewhere the type 
20524
1493053fc111
Tweaks to is_fol_term, the firstorder test. We don't count "=" as a connective
paulson
parents:
20417
diff
changeset

404 
of any argument contains bool.*) 
24300  405 
val has_bool_arg_const = 
15613  406 
exists_Const 
407 
(fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); 

22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

408 

24300  409 
(*A higherorder instance of a firstorder constant? Example is the definition of 
34974
18b41bba42b5
new theory Algebras.thy for generic algebraic structures
haftmann
parents:
33832
diff
changeset

410 
one, 1, at a function type in theory SetsAndFunctions.*) 
24300  411 
fun higher_inst_const thy (c,T) = 
22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

412 
case binder_types T of 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

413 
[] => false (*not a function type, OK*) 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

414 
 Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts; 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

415 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24300
diff
changeset

416 
(*Returns false if any Vars in the theorem mention type bool. 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

417 
Also rejects functions whose arguments are Booleans or other functions.*) 
22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

418 
fun is_fol_term thy t = 
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

419 
Term.is_first_order ["all","All","Ex"] t andalso 
29267  420 
not (exists_subterm (fn Var (_, T) => has_bool T  _ => false) t orelse 
24300  421 
has_bool_arg_const t orelse 
422 
exists_Const (higher_inst_const thy) t orelse 

423 
has_meta_conn t); 

19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

424 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

425 
fun rigid t = not (is_Var (head_of t)); 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

426 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

427 
fun ok4horn (Const ("Trueprop",_) $ (Const ("op ", _) $ t $ _)) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

428 
 ok4horn (Const ("Trueprop",_) $ t) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

429 
 ok4horn _ = false; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

430 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

431 
(*Create a metalevel Horn clause*) 
24300  432 
fun make_horn crules th = 
433 
if ok4horn (concl_of th) 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

434 
then make_horn crules (tryres(th,crules)) handle THM _ => th 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

435 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

436 

16563  437 
(*Generate Horn clauses for all contrapositives of a clause. The input, th, 
438 
is a HOL disjunction.*) 

33339  439 
fun add_contras crules th hcs = 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

440 
let fun rots (0,th) = hcs 
24300  441 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
442 
rots(k1, assoc_right (th RS disj_comm)) 

15862  443 
in case nliterals(prop_of th) of 
24300  444 
1 => th::hcs 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

445 
 n => rots(n, assoc_right th) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

446 
end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

447 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

448 
(*Use "theorem naming" to label the clauses*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

449 
fun name_thms label = 
33339  450 
let fun name1 th (k, ths) = 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
27239
diff
changeset

451 
(k1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) 
33339  452 
in fn ths => #2 (fold_rev name1 ths (length ths, [])) end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

453 

16563  454 
(*Is the given disjunction an allnegative support clause?*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

455 
fun is_negative th = forall (not o #1) (literals (prop_of th)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

456 

33317  457 
val neg_clauses = filter is_negative; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

458 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

459 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

460 
(***** MESON PROOF PROCEDURE *****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

461 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

462 
fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, 
24300  463 
As) = rhyps(phi, A::As) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

464 
 rhyps (_, As) = As; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

465 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

466 
(** Detecting repeated assumptions in a subgoal **) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

467 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

468 
(*The stringtree detects repeated assumptions.*) 
33245  469 
fun ins_term t net = Net.insert_term (op aconv) (t, t) net; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

470 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

471 
(*detects repetitions in a list of terms*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

472 
fun has_reps [] = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

473 
 has_reps [_] = false 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

474 
 has_reps [t,u] = (t aconv u) 
33245  475 
 has_reps ts = (fold ins_term ts Net.empty; false) handle Net.INSERT => true; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

476 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

477 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  478 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
479 
 TRYING_eq_assume_tac i st = 

31945  480 
TRYING_eq_assume_tac (i1) (Thm.eq_assumption i st) 
18508  481 
handle THM _ => TRYING_eq_assume_tac (i1) st; 
482 

483 
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st; 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

484 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

485 
(*Loop checking: FAIL if trying to prove the same thing twice 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

486 
 if *ANY* subgoal has repeated literals*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

487 
fun check_tac st = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

488 
if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

489 
then Seq.empty else Seq.single st; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

490 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

491 

15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

492 
(* net_resolve_tac actually made it slower... *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

493 
fun prolog_step_tac horns i = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

494 
(assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN 
18508  495 
TRYALL_eq_assume_tac; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

496 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

497 
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) 
33339  498 
fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz; 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

499 

33339  500 
fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0; 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

501 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

502 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

503 
(*Negation Normal Form*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

504 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  505 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  506 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

507 
fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

508 
 ok4nnf (Const ("Trueprop",_) $ t) = rigid t 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

509 
 ok4nnf _ = false; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

510 

32262  511 
fun make_nnf1 ctxt th = 
24300  512 
if ok4nnf (concl_of th) 
32262  513 
then make_nnf1 ctxt (tryres(th, nnf_rls)) 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

514 
handle THM ("tryres", _, _) => 
32262  515 
forward_res ctxt (make_nnf1 ctxt) 
9869  516 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

517 
handle THM ("tryres", _, _) => th 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

518 
else th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

519 

24300  520 
(*The simplification removes defined quantifiers and occurrences of True and False. 
20018  521 
nnf_ss also includes the onepoint simprocs, 
18405
afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

522 
which are needed to avoid the various onepoint theorems from generating junk clauses.*) 
19894  523 
val nnf_simps = 
37539  524 
@{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel 
525 
if_eq_cancel cases_simp} 

526 
val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} 

18405
afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

527 

afb1a52a7011
removal of some redundancies (e.g. onepointrules) in clause production
paulson
parents:
18389
diff
changeset

528 
val nnf_ss = 
24300  529 
HOL_basic_ss addsimps nnf_extra_simps 
24040  530 
addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; 
15872  531 

32262  532 
fun make_nnf ctxt th = case prems_of th of 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

533 
[] => th > rewrite_rule (map safe_mk_meta_eq nnf_simps) 
24300  534 
> simplify nnf_ss 
32262  535 
> make_nnf1 ctxt 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

536 
 _ => raise THM ("make_nnf: premises in argument", 0, [th]); 
15581  537 

15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15946
diff
changeset

538 
(*Pull existential quantifiers to front. This accomplishes Skolemization for 
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15946
diff
changeset

539 
clauses that arise from a subgoal.*) 
32262  540 
fun skolemize1 ctxt th = 
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

541 
if not (has_conns ["Ex"] (prop_of th)) then th 
32262  542 
else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2, 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15653
diff
changeset

543 
disj_exD, disj_exD1, disj_exD2]))) 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

544 
handle THM ("tryres", _, _) => 
32262  545 
skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt) 
9869  546 
(tryres (th, [conj_forward, disj_forward, all_forward]))) 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

547 
handle THM ("tryres", _, _) => 
32262  548 
forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward); 
29684  549 

32262  550 
fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

551 

32262  552 
fun skolemize_nnf_list _ [] = [] 
553 
 skolemize_nnf_list ctxt (th::ths) = 

554 
skolemize ctxt th :: skolemize_nnf_list ctxt ths 

25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25694
diff
changeset

555 
handle THM _ => (*RS can fail if Unify.search_bound is too small*) 
32955  556 
(trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th); 
32262  557 
skolemize_nnf_list ctxt ths); 
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

558 

33339  559 
fun add_clauses th cls = 
36603
d5d6111761a6
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
wenzelm
parents:
36001
diff
changeset

560 
let val ctxt0 = Variable.global_thm_context th 
33339  561 
val (cnfs, ctxt) = make_cnf [] th ctxt0 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

562 
in Variable.export ctxt ctxt0 cnfs @ cls end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

563 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

564 
(*Make clauses from a list of theorems, previously Skolemized and put into nnf. 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

565 
The resulting clauses are HOL disjunctions.*) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35625
diff
changeset

566 
fun make_clauses_unsorted ths = fold_rev add_clauses ths []; 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35625
diff
changeset

567 
val make_clauses = sort_clauses o make_clauses_unsorted; 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

568 

16563  569 
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*) 
9869  570 
fun make_horns ths = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

571 
name_thms "Horn#" 
33339  572 
(distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths [])); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

573 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

574 
(*Could simply use nprems_of, which would count remaining subgoals  no 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

575 
discrimination as to their size! With BEST_FIRST, fails for problem 41.*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

576 

9869  577 
fun best_prolog_tac sizef horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

578 
BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

579 

9869  580 
fun depth_prolog_tac horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

581 
DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

582 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

583 
(*Return all negative clauses, as possible goal clauses*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

584 
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

585 

32262  586 
fun skolemize_prems_tac ctxt prems = 
587 
cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

588 
REPEAT o (etac exE); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

589 

22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

590 
(*Basis of all mesontactics. Supplies cltac with clauses: HOL disjunctions. 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

591 
Function mkcl converts theorems to clauses.*) 
32262  592 
fun MESON mkcl cltac ctxt i st = 
16588  593 
SELECT_GOAL 
35625  594 
(EVERY [Object_Logic.atomize_prems_tac 1, 
23552  595 
rtac ccontr 1, 
32283  596 
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => 
32262  597 
EVERY1 [skolemize_prems_tac ctxt negs, 
32283  598 
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st 
24300  599 
handle THM _ => no_tac st; (*probably from make_meta_clause, not firstorder*) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

600 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

601 
(** Bestfirst search versions **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

602 

16563  603 
(*ths is a list of additional clauses (HOL disjunctions) to use.*) 
9869  604 
fun best_meson_tac sizef = 
24300  605 
MESON make_clauses 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

606 
(fn cls => 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

607 
THEN_BEST_FIRST (resolve_tac (gocls cls) 1) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

608 
(has_fewer_prems 1, sizef) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

609 
(prolog_step_tac (make_horns cls) 1)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

610 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

611 
(*First, breaks the goal into independent units*) 
32262  612 
fun safe_best_meson_tac ctxt = 
613 
SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN 

614 
TRYALL (best_meson_tac size_of_subgoals ctxt)); 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

615 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

616 
(** Depthfirst search version **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

617 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

618 
val depth_meson_tac = 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

619 
MESON make_clauses 
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

620 
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

621 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

622 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

623 
(** Iterative deepening version **) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

624 

9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

625 
(*This version does only one inference per call; 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

626 
having only one eq_assume_tac speeds it up!*) 
9869  627 
fun prolog_step_tac' horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

628 
let val (horn0s, hornps) = (*0 subgoals vs 1 or more*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

629 
take_prefix Thm.no_prems horns 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

630 
val nrtac = net_resolve_tac horns 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

631 
in fn i => eq_assume_tac i ORELSE 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

632 
match_tac horn0s i ORELSE (*no backtracking if unit MATCHES*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

633 
((assume_tac i APPEND nrtac i) THEN check_tac) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

634 
end; 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

635 

9869  636 
fun iter_deepen_prolog_tac horns = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

637 
ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

638 

32262  639 
fun iter_deepen_meson_tac ctxt ths = ctxt > MESON make_clauses 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

640 
(fn cls => 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

641 
(case (gocls (cls @ ths)) of 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

642 
[] => no_tac (*no goal clauses*) 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

643 
 goes => 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

644 
let 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

645 
val horns = make_horns (cls @ ths) 
32955  646 
val _ = trace_msg (fn () => 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

647 
cat_lines ("meson method called:" :: 
32262  648 
map (Display.string_of_thm ctxt) (cls @ ths) @ 
649 
["clauses:"] @ map (Display.string_of_thm ctxt) horns)) 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

650 
in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

651 

32262  652 
fun meson_tac ctxt ths = 
653 
SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); 

9869  654 

655 

14813  656 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  657 

24300  658 
(*Convert a list of clauses (disjunctions) to metalevel clauses (==>), 
15008  659 
with no contrapositives, for ordinary resolution.*) 
14744  660 

661 
(*Rules to convert the head literal into a negated assumption. If the head 

662 
literal is already negated, then using notEfalse instead of notEfalse' 

663 
prevents a double negation.*) 

27239  664 
val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; 
14744  665 
val notEfalse' = rotate_prems 1 notEfalse; 
666 

24300  667 
fun negated_asm_of_head th = 
14744  668 
th RS notEfalse handle THM _ => th RS notEfalse'; 
669 

26066
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

670 
(*Converting one theorem from a disjunction to a metalevel clause*) 
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

671 
fun make_meta_clause th = 
33832  672 
let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th 
26066
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

673 
in 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35625
diff
changeset

674 
(zero_var_indexes o Thm.varifyT_global o thaw 0 o 
26066
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

675 
negated_asm_of_head o make_horn resolution_clause_rules) fth 
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

676 
end; 
24300  677 

14744  678 
fun make_meta_clauses ths = 
679 
name_thms "MClause#" 

22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
22130
diff
changeset

680 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  681 

682 
(*Permute a rule's premises to move the ith premise to the last position.*) 

683 
fun make_last i th = 

24300  684 
let val n = nprems_of th 
685 
in if 1 <= i andalso i <= n 

14744  686 
then Thm.permute_prems (i1) 1 th 
15118  687 
else raise THM("select_literal", i, [th]) 
14744  688 
end; 
689 

690 
(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing 

691 
doublenegations.*) 

35410  692 
val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]; 
14744  693 

694 
(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i1),P(i+1),...Pn] ==> ~P*) 

695 
fun select_literal i cl = negate_head (make_last i cl); 

696 

18508  697 

14813  698 
(*Toplevel Skolemization. Allows part of the conversion to clauses to be 
24300  699 
expressed as a tactic (or Isar method). Each assumption of the selected 
14813  700 
goal is converted to NNF and then its existential quantifiers are pulled 
24300  701 
to the front. Finally, all existential quantifiers are eliminated, 
14813  702 
leaving !!quantified variables. Perhaps Safe_tac should follow, but it 
703 
might generate many subgoals.*) 

18194
940515d2fa26
 removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
mengj
parents:
18175
diff
changeset

704 

32262  705 
fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) => 
706 
let val ts = Logic.strip_assums_hyp goal 

24300  707 
in 
32262  708 
EVERY' 
709 
[OldGoals.METAHYPS (fn hyps => 

710 
(cut_facts_tac (skolemize_nnf_list ctxt hyps) 1 

711 
THEN REPEAT (etac exE 1))), 

712 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] i 

713 
end); 

18194
940515d2fa26
 removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
mengj
parents:
18175
diff
changeset

714 

9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

715 
end; 