author  paulson 
Tue, 09 Oct 2007 18:14:00 +0200  
changeset 24937  340523598914 
parent 24827  646bdc51eb7d 
child 25694  cbb59ba6bf0c 
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 
ID: $Id$ 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

3 
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

4 
Copyright 1992 University of Cambridge 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

5 

9869  6 
The MESON resolution proof procedure for HOL. 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

7 

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

8 
When making clauses, avoids using the rewriter  instead uses RS recursively 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

10 

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

12 
sig 
24300  13 
val term_pair_of: indexname * (typ * 'a) > term * 'a 
14 
val first_order_resolve: thm > thm > thm 

15 
val flexflex_first_order: thm > thm 

16 
val size_of_subgoals: thm > int 

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

18 
val make_cnf: thm list > thm > Proof.context > thm list * Proof.context 
24300  19 
val finish_cnf: thm list > thm list 
20 
val make_nnf: thm > thm 

21 
val make_nnf1: thm > thm 

22 
val skolemize: thm > thm 

23 
val is_fol_term: theory > term > bool 

24 
val make_clauses: thm list > thm list 

25 
val make_horns: thm list > thm list 

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

27 
val depth_prolog_tac: thm list > tactic 

28 
val gocls: thm list > thm list 

29 
val skolemize_prems_tac: thm list > int > tactic 

30 
val MESON: (thm list > thm list) > (thm list > tactic) > int > tactic 

31 
val best_meson_tac: (thm > int) > int > tactic 

32 
val safe_best_meson_tac: int > tactic 

33 
val depth_meson_tac: int > tactic 

34 
val prolog_step_tac': thm list > int > tactic 

35 
val iter_deepen_prolog_tac: thm list > tactic 

36 
val iter_deepen_meson_tac: thm list > int > tactic 

37 
val make_meta_clause: thm > thm 

38 
val make_meta_clauses: thm list > thm list 

39 
val meson_claset_tac: thm list > claset > int > tactic 

40 
val meson_tac: int > tactic 

41 
val negate_head: thm > thm 

42 
val select_literal: int > thm > thm 

43 
val skolemize_tac: int > tactic 

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

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

45 

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

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

48 

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

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

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

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

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

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

54 
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

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

56 
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

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

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

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

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

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

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

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

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

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

66 
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

67 

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

68 

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

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

70 

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

71 

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

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

73 

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

74 
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

75 
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

76 

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

77 
val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

78 

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

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

80 
fun first_order_resolve thA thB = 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

81 
let val thy = theory_of_thm thA 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

82 
val tmA = concl_of thA 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

83 
val Const("==>",_) $ tmB $ _ = prop_of thB 
23440
37860871f241
Added flexflex_first_order and tidied first_order_resolution
paulson
parents:
23262
diff
changeset

84 
val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0) 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

85 
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

86 
in thA RS (cterm_instantiate ct_pairs thB) end 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

87 
handle _ => 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

88 

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

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

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

92 
 pairs => 
24300  93 
let val thy = theory_of_thm th 
94 
val (tyenv,tenv) = 

95 
foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs 

96 
val t_pairs = map term_pair_of (Vartab.dest tenv) 

97 
val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th 

98 
in th' end 

99 
handle THM _ => th; 

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

100 

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

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

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

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

104 
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

105 

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

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

108 
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

109 
 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

110 
in tryall rls end; 
24300  111 

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

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

113 
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

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

115 
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

116 
fun forward_res nf st = 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

117 
let fun forward_tacf [prem] = rtac (nf prem) 1 
24300  118 
 forward_tacf prems = 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

119 
error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

120 
string_of_thm st ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

121 
"\nPremises:\n" ^ 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

122 
cat_lines (map string_of_thm prems)) 
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

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

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

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

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

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

128 

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

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

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

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

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

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

134 
 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

135 
 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

136 
 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

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

139 
in has end; 
24300  140 

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

141 

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

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

143 

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

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

145 
 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

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

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

148 

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

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

150 
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

151 

18389  152 

153 
(*** Tautology Checking ***) 

154 

24300  155 
fun signed_lits_aux (Const ("op ", _) $ P $ Q) (poslits, neglits) = 
18389  156 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 
157 
 signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) 

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

24300  159 

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

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

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

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

165 
 taut_poslit _ = false; 

166 

167 
fun is_taut th = 

168 
let val (poslits,neglits) = signed_lits th 

169 
in exists taut_poslit poslits 

170 
orelse 

20073  171 
exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) 
19894  172 
end 
24300  173 
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) 
18389  174 

175 

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

177 

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

179 
injectivity equivalences*) 

24300  180 

18389  181 
val not_refl_disj_D = thm"meson_not_refl_disj_D"; 
182 

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

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

186 
 eliminable _ = false; 

187 

18389  188 
fun refl_clause_aux 0 th = th 
189 
 refl_clause_aux n th = 

190 
case HOLogic.dest_Trueprop (concl_of th) of 

24300  191 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _) => 
18389  192 
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) 
24300  193 
 (Const ("op ", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 
194 
if eliminable(t,u) 

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

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

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

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

18389  199 

24300  200 
fun notequal_lits_count (Const ("op ", _) $ P $ Q) = 
18389  201 
notequal_lits_count P + notequal_lits_count Q 
202 
 notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 

203 
 notequal_lits_count _ = 0; 

204 

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

24300  206 
fun refl_clause th = 
18389  207 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 
19894  208 
in zero_var_indexes (refl_clause_aux neqs th) end 
24300  209 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 
18389  210 

211 

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

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

213 

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

214 
(*Forward proof, passing extra assumptions as theorems to the tactic*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

215 
fun forward_res2 nf hyps st = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

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

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

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

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

222 

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

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

224 
rls (initially []) accumulates assumptions of the form P==>False*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

225 
fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

226 
handle THM _ => tryres(th,rls) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

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

230 

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

231 
(*Remove duplicate literals, if there are any*) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

233 
if has_duplicates (op =) (literals (prop_of th)) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

234 
then nodups_aux [] th 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

236 

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

237 

18389  238 
(*** The basic CNF transformation ***) 
239 

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

240 
val max_clauses = 40; 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

241 

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

242 
fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses; 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24300
diff
changeset

243 
fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses; 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

244 

19894  245 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

246 
fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

247 
 signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t 
24300  248 
 signed_nclauses b (Const("op &",_) $ t $ u) = 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

249 
if b then sum (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

250 
else prod (signed_nclauses b t) (signed_nclauses b u) 
24300  251 
 signed_nclauses b (Const("op ",_) $ t $ u) = 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

252 
if b then prod (signed_nclauses b t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

253 
else sum (signed_nclauses b t) (signed_nclauses b u) 
24300  254 
 signed_nclauses b (Const("op >",_) $ t $ u) = 
21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

255 
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

256 
else sum (signed_nclauses (not b) t) (signed_nclauses b u) 
24300  257 
 signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
21616
296e0c318c3e
Fixed a MAJOR BUG in clausecounting: only Boolean equalities now count as iffs
paulson
parents:
21588
diff
changeset

258 
if T = HOLogic.boolT then (*Boolean equality is ifandonlyif*) 
24300  259 
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) 
260 
(prod (signed_nclauses (not b) u) (signed_nclauses b t)) 

261 
else sum (prod (signed_nclauses b t) (signed_nclauses b u)) 

262 
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) 

263 
else 1 

21069
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

264 
 signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

265 
 signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

266 
 signed_nclauses _ _ = 1; (* literal *) 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

267 

e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

268 
val nclauses = signed_nclauses true; 
e55b507d0c61
nclauses no longer requires its input to be in NNF
paulson
parents:
21050
diff
changeset

269 

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

270 
fun too_many_clauses t = nclauses t >= max_clauses; 
19894  271 

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

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

273 
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

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

275 
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

276 
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

277 
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

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

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

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

281 
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

282 
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

283 
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

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

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

286 

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

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

288 
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

289 
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

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

291 
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

292 

24300  293 
(*Any need to extend this list with 
23262  294 
"HOL.type_class","HOL.eq_class","ProtoPure.term"?*) 
24300  295 
val has_meta_conn = 
22871  296 
exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1); 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

297 

24300  298 
fun apply_skolem_ths (th, rls) = 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

299 
let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

300 
 tryall (rl::rls) = (first_order_resolve th rl handle THM _ => tryall rls) 
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

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

302 

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

303 
(*Conjunctive normal form, adding clauses from th in front of ths (for foldr). 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

304 
Strips universal quantifiers and breaks up conjunctions. 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

305 
Eliminates existential quantifiers using skoths: Skolemization theorems.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

306 
fun cnf skoths ctxt (th,ths) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

307 
let val ctxtr = ref ctxt 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

311 
then nodups th :: ths (*no work to do, terminate*) 
24300  312 
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of 
313 
Const ("op &", _) => (*conjunction*) 

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

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

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

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

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

320 
cnf_aux (apply_skolem_ths (th,skoths), ths) 

321 
 Const ("op ", _) => 

322 
(*Disjunction of P, Q: Create new goal of proving ?P  ?Q and solve it using 

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

324 
let val tac = 

325 
(METAHYPS (resop cnf_nil) 1) THEN 

326 
(fn st' => st' > METAHYPS (resop cnf_nil) 1) 

327 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 

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

328 
 _ => nodups th :: ths (*no work to do*) 
19154  329 
and cnf_nil th = cnf_aux (th,[]) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

331 
if too_many_clauses (concl_of th) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

332 
then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths) 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

335 

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

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

337 

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

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

339 
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

340 

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

341 

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

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

343 

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

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

346 
 is_left _ = false; 
24300  347 

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

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

350 
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

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

352 

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

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

354 
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

355 

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

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

357 
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

358 

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

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

360 
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

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

362 
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

363 

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

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

365 
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

366 

18389  367 
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

368 

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

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

372 
 has_bool _ = false; 

24300  373 

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

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

19875  376 
val is_conn = member (op =) 
24300  377 
["Trueprop", "op &", "op ", "op >", "Not", 
15613  378 
"All", "Ex", "Ball", "Bex"]; 
379 

24300  380 
(*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

381 
of any argument contains bool.*) 
24300  382 
val has_bool_arg_const = 
15613  383 
exists_Const 
384 
(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

385 

24300  386 
(*A higherorder instance of a firstorder constant? Example is the definition of 
22381
cb145d434284
The firstorder test now tests for the obscure case of a polymorphic constant like 1 being
paulson
parents:
22360
diff
changeset

387 
HOL.one, 1, at a function type in theory SetsAndFunctions.*) 
24300  388 
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

389 
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

390 
[] => 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

391 
 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

392 

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

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

394 
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

395 
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

396 
Term.is_first_order ["all","All","Ex"] t andalso 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

397 
not (exists (has_bool o fastype_of) (term_vars t) orelse 
24300  398 
has_bool_arg_const t orelse 
399 
exists_Const (higher_inst_const thy) t orelse 

400 
has_meta_conn t); 

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

401 

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

402 
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

403 

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

404 
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

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

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

407 

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

408 
(*Create a metalevel Horn clause*) 
24300  409 
fun make_horn crules th = 
410 
if ok4horn (concl_of th) 

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

411 
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

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

413 

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

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

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

417 
let fun rots (0,th) = hcs 
24300  418 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
419 
rots(k1, assoc_right (th RS disj_comm)) 

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

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

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

424 

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

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

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

427 
let fun name1 (th, (k,ths)) = 
24300  428 
(k1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

429 
in fn ths => #2 (foldr name1 (length ths, []) ths) end; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

430 

16563  431 
(*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

432 
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

433 

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

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

435 

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

436 

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

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

438 

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

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

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

442 

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

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

444 

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

445 
(*The stringtree detects repeated assumptions.*) 
16801  446 
fun ins_term (net,t) = 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

447 

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

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

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

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

451 
 has_reps [t,u] = (t aconv u) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

452 
 has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) 
24300  453 
handle Net.INSERT => true; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

454 

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

455 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  456 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
457 
 TRYING_eq_assume_tac i st = 

458 
TRYING_eq_assume_tac (i1) (eq_assumption i st) 

459 
handle THM _ => TRYING_eq_assume_tac (i1) st; 

460 

461 
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

462 

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

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

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

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

466 
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

467 
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

468 

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

469 

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

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

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

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

474 

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

475 
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

476 
fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

477 

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

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

479 

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

480 

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

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

482 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  483 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  484 

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

485 
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

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

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

488 

24300  489 
fun make_nnf1 th = 
490 
if ok4nnf (concl_of th) 

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

491 
then make_nnf1 (tryres(th, nnf_rls)) 
9869  492 
handle THM _ => 
15581  493 
forward_res make_nnf1 
9869  494 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

495 
handle THM _ => th 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

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

497 

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

500 
which are needed to avoid the various onepoint theorems from generating junk clauses.*) 
19894  501 
val nnf_simps = 
24300  502 
[simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
19894  503 
if_False, if_cancel, if_eq_cancel, cases_simp]; 
504 
val nnf_extra_simps = 

505 
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

506 

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

507 
val nnf_ss = 
24300  508 
HOL_basic_ss addsimps nnf_extra_simps 
24040  509 
addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; 
15872  510 

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

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

512 
[] => th > rewrite_rule (map safe_mk_meta_eq nnf_simps) 
24300  513 
> simplify nnf_ss 
514 
> make_nnf1 

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

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

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

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

518 
clauses that arise from a subgoal.*) 
9869  519 
fun skolemize th = 
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

520 
if not (has_conns ["Ex"] (prop_of th)) then th 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

521 
else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2, 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15653
diff
changeset

522 
disj_exD, disj_exD1, disj_exD2]))) 
9869  523 
handle THM _ => 
524 
skolemize (forward_res skolemize 

525 
(tryres (th, [conj_forward, disj_forward, all_forward]))) 

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

526 
handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

527 

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

528 
fun add_clauses (th,cls) = 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

529 
let val ctxt0 = Variable.thm_context th 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

530 
val (cnfs,ctxt) = make_cnf [] th ctxt0 
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

531 
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

532 

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

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

534 
The resulting clauses are HOL disjunctions.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

535 
fun make_clauses ths = sort_clauses (foldr add_clauses [] ths); 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

536 

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

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

540 
(distinct Thm.eq_thm_prop (foldr (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

541 

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

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

543 
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

544 

9869  545 
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

546 
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

547 

9869  548 
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

549 
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

550 

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

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

552 
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

553 

15008  554 
fun skolemize_prems_tac prems = 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

555 
cut_facts_tac (map (skolemize o make_nnf) prems) THEN' 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

557 

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

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

559 
Function mkcl converts theorems to clauses.*) 
24300  560 
fun MESON mkcl cltac i st = 
16588  561 
SELECT_GOAL 
23590
ad95084a5c63
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
wenzelm
parents:
23552
diff
changeset

562 
(EVERY [ObjectLogic.atomize_prems_tac 1, 
23552  563 
rtac ccontr 1, 
24300  564 
METAHYPS (fn negs => 
565 
EVERY1 [skolemize_prems_tac negs, 

566 
METAHYPS (cltac o mkcl)]) 1]) i st 

567 
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

568 

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

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

570 

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

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

575 
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

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

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

578 

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

579 
(*First, breaks the goal into independent units*) 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

580 
val safe_best_meson_tac = 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23590
diff
changeset

581 
SELECT_GOAL (TRY (CLASET safe_tac) THEN 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

582 
TRYALL (best_meson_tac size_of_subgoals)); 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

583 

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

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

585 

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

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

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

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

589 

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

590 

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

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

592 

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

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

594 
having only one eq_assume_tac speeds it up!*) 
9869  595 
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

596 
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

597 
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

598 
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

599 
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

600 
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

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

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

603 

9869  604 
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

605 
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

606 

24300  607 
fun iter_deepen_meson_tac ths = MESON make_clauses 
21095  608 
(fn cls => 
609 
case (gocls (cls@ths)) of 

24300  610 
[] => no_tac (*no goal clauses*) 
611 
 goes => 

612 
let val horns = make_horns (cls@ths) 

613 
val _ = 

614 
Output.debug (fn () => ("meson method called:\n" ^ 

615 
space_implode "\n" (map string_of_thm (cls@ths)) ^ 

616 
"\nclauses:\n" ^ 

617 
space_implode "\n" (map string_of_thm horns))) 

618 
in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) 

619 
end 

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

621 

16563  622 
fun meson_claset_tac ths cs = 
623 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); 

9869  624 

16563  625 
val meson_tac = CLASET' (meson_claset_tac []); 
9869  626 

627 

14813  628 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  629 

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

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

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

635 
prevents a double negation.*) 

636 
val notEfalse = read_instantiate [("R","False")] notE; 

637 
val notEfalse' = rotate_prems 1 notEfalse; 

638 

24300  639 
fun negated_asm_of_head th = 
14744  640 
th RS notEfalse handle THM _ => th RS notEfalse'; 
641 

642 
(*Converting one clause*) 

24300  643 
val make_meta_clause = 
22646  644 
zero_var_indexes o negated_asm_of_head o make_horn resolution_clause_rules; 
24300  645 

14744  646 
fun make_meta_clauses ths = 
647 
name_thms "MClause#" 

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

648 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  649 

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

651 
fun make_last i th = 

24300  652 
let val n = nprems_of th 
653 
in if 1 <= i andalso i <= n 

14744  654 
then Thm.permute_prems (i1) 1 th 
15118  655 
else raise THM("select_literal", i, [th]) 
14744  656 
end; 
657 

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

659 
doublenegations.*) 

660 
val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection]; 

661 

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

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

664 

18508  665 

14813  666 
(*Toplevel Skolemization. Allows part of the conversion to clauses to be 
24300  667 
expressed as a tactic (or Isar method). Each assumption of the selected 
14813  668 
goal is converted to NNF and then its existential quantifiers are pulled 
24300  669 
to the front. Finally, all existential quantifiers are eliminated, 
14813  670 
leaving !!quantified variables. Perhaps Safe_tac should follow, but it 
671 
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

672 

24300  673 
fun skolemize_tac i st = 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

674 
let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i1)) 
24300  675 
in 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

676 
EVERY' [METAHYPS 
24300  677 
(fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 
14813  678 
THEN REPEAT (etac exE 1))), 
19204
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

679 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

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

681 
handle Subscript => Seq.empty; 
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

682 

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

683 
end; 
9869  684 