author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29684  40bf9f4e7a4e 
child 30607  c3d1590debd8 
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 
24300  10 
val term_pair_of: indexname * (typ * 'a) > term * 'a 
11 
val first_order_resolve: thm > thm > thm 

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 
17 
val make_nnf: thm > thm 

18 
val skolemize: thm > thm 

19 
val is_fol_term: theory > term > bool 

20 
val make_clauses: thm list > thm list 

21 
val make_horns: thm list > thm list 

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

23 
val depth_prolog_tac: thm list > tactic 

24 
val gocls: thm list > thm list 

25 
val skolemize_prems_tac: thm list > int > tactic 

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

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

28 
val safe_best_meson_tac: int > tactic 

29 
val depth_meson_tac: int > tactic 

30 
val prolog_step_tac': thm list > int > tactic 

31 
val iter_deepen_prolog_tac: thm list > tactic 

32 
val iter_deepen_meson_tac: thm list > int > tactic 

33 
val make_meta_clause: thm > thm 

34 
val make_meta_clauses: thm list > thm list 

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

36 
val meson_tac: int > tactic 

37 
val negate_head: thm > thm 

38 
val select_literal: int > thm > thm 

39 
val skolemize_tac: int > tactic 

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

40 
val setup: Context.theory > Context.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 

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

46 
val max_clauses_default = 60; 
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

47 
val (max_clauses, setup) = Attrib.config_int "max_clauses" 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

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 
28397
389c5e494605
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents:
28174
diff
changeset

87 
handle _ => raise THM ("first_order_resolve", 0, [thA,thB]); (* FIXME avoid handle _ *) 
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) = 

30190  95 
List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs 
24300  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" ^ 
26928  120 
Display.string_of_thm st ^ 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

121 
"\nPremises:\n" ^ 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

122 
ML_Syntax.print_list Display.string_of_thm prems) 
21050
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 

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

240 
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

241 
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

242 
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

243 
 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

244 

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

245 
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

246 
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

247 

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

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

249 
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

250 
 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

251 
 signed_nclauses b (Const("op &",_) $ t $ u) = 
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

252 
if b then sum (signed_nclauses b t) (signed_nclauses b u) 
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

253 
else prod (signed_nclauses b t) (signed_nclauses b u) 
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

254 
 signed_nclauses b (Const("op ",_) $ t $ u) = 
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

255 
if b then prod (signed_nclauses b t) (signed_nclauses b u) 
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

256 
else sum (signed_nclauses b t) (signed_nclauses b u) 
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

257 
 signed_nclauses b (Const("op >",_) $ t $ u) = 
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

258 
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) 
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 
else sum (signed_nclauses (not b) t) (signed_nclauses b u) 
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 
 signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) = 
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 
if T = HOLogic.boolT then (*Boolean equality is ifandonlyif*) 
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 
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) 
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 
(prod (signed_nclauses (not b) u) (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

264 
else sum (prod (signed_nclauses b t) (signed_nclauses b u)) 
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 
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) 
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 
else 1 
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 
 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

268 
 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

269 
 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

270 
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

271 
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

272 
end; 
19894  273 

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

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

275 
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

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

277 
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

278 
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

279 
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

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

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

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

283 
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

284 
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

285 
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

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

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

288 

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

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

290 
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

291 
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

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

293 
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

294 

24300  295 
(*Any need to extend this list with 
26424  296 
"HOL.type_class","HOL.eq_class","Pure.term"?*) 
24300  297 
val has_meta_conn = 
29684  298 
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

299 

24300  300 
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

301 
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

302 
 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

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

304 

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

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

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

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

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

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

310 
fun cnf_aux (th,ths) = 
24300  311 
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*metalevel: ignore*) 
312 
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

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

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

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

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

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

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

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

323 
 Const ("op ", _) => 

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

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

326 
let val tac = 

327 
(METAHYPS (resop cnf_nil) 1) THEN 

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

329 
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

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

332 
val cls = 
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

333 
if too_many_clauses (SOME ctxt) (concl_of th) 
26928  334 
then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

337 

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

338 
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

339 

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

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

341 
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

342 

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

343 

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

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

345 

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

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

348 
 is_left _ = false; 
24300  349 

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

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

352 
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

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

354 

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

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

356 
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

357 

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

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

359 
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

360 

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

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

362 
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

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

364 
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

365 

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

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

367 
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

368 

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

370 

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

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

374 
 has_bool _ = false; 

24300  375 

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

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

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

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

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

387 

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

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

391 
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

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

393 
 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

394 

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

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

396 
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

397 
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

398 
Term.is_first_order ["all","All","Ex"] t andalso 
29267  399 
not (exists_subterm (fn Var (_, T) => has_bool T  _ => false) t orelse 
24300  400 
has_bool_arg_const t orelse 
401 
exists_Const (higher_inst_const thy) t orelse 

402 
has_meta_conn t); 

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

403 

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

404 
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

405 

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

406 
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

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

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

409 

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

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

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

413 
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

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

415 

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

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

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

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

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

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

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

426 

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

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

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

429 
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

430 
(k1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) 
30190  431 
in fn ths => #2 (List.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

432 

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

434 
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

435 

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

436 
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

437 

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 
(***** MESON PROOF PROCEDURE *****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

440 

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

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

443 
 rhyps (_, As) = As; 
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 
(** 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

446 

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

447 
(*The stringtree detects repeated assumptions.*) 
16801  448 
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

449 

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

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

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

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

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

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

456 

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

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

460 
TRYING_eq_assume_tac (i1) (eq_assumption i st) 

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

462 

463 
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

464 

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

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

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

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

468 
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

469 
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

470 

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

471 

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

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

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

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

476 

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

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

478 
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

479 

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

481 

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

482 

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

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

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

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

487 
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

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

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

490 

24300  491 
fun make_nnf1 th = 
492 
if ok4nnf (concl_of th) 

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

493 
then make_nnf1 (tryres(th, nnf_rls)) 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

494 
handle THM ("tryres", _, _) => 
15581  495 
forward_res make_nnf1 
9869  496 
(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

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

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

499 

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

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

507 
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

508 

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

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

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

513 
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

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

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

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

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

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

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

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

524 
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

525 
handle THM ("tryres", _, _) => 
29684  526 
skolemize1 (forward_res skolemize1 
9869  527 
(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

528 
handle THM ("tryres", _, _) => 
29684  529 
forward_res skolemize1 (rename_bvs_RS th ex_forward); 
530 

531 
fun skolemize th = skolemize1 (make_nnf th); 

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

532 

25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

533 
fun skolemize_nnf_list [] = [] 
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

534 
 skolemize_nnf_list (th::ths) = 
29684  535 
skolemize th :: skolemize_nnf_list ths 
25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25694
diff
changeset

536 
handle THM _ => (*RS can fail if Unify.search_bound is too small*) 
26928  537 
(warning ("Failed to Skolemize " ^ Display.string_of_thm th); 
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

538 
skolemize_nnf_list ths); 
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

539 

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

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

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

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

543 
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

544 

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

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

546 
The resulting clauses are HOL disjunctions.*) 
30190  547 
fun make_clauses ths = sort_clauses (List.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

548 

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

551 
name_thms "Horn#" 
30190  552 
(distinct Thm.eq_thm_prop (List.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

553 

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

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

555 
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

556 

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

558 
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

559 

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

561 
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

562 

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

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

564 
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

565 

15008  566 
fun skolemize_prems_tac prems = 
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

567 
cut_facts_tac (skolemize_nnf_list prems) THEN' 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

569 

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

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

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

574 
(EVERY [ObjectLogic.atomize_prems_tac 1, 
23552  575 
rtac ccontr 1, 
24300  576 
METAHYPS (fn negs => 
577 
EVERY1 [skolemize_prems_tac negs, 

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

579 
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

580 

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

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

582 

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

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

587 
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

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

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

590 

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

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

592 
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

593 
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

594 
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

595 

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

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

597 

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

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

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

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

601 

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

602 

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

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

604 

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

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

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

608 
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

609 
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

610 
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

611 
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

612 
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

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

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

615 

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

617 
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

618 

24300  619 
fun iter_deepen_meson_tac ths = MESON make_clauses 
21095  620 
(fn cls => 
621 
case (gocls (cls@ths)) of 

24300  622 
[] => no_tac (*no goal clauses*) 
623 
 goes => 

624 
let val horns = make_horns (cls@ths) 

625 
val _ = 

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

28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

627 
ML_Syntax.print_list Display.string_of_thm (cls@ths) ^ 
24300  628 
"\nclauses:\n" ^ 
28174
626f0a79a4b9
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
paulson
parents:
27865
diff
changeset

629 
ML_Syntax.print_list Display.string_of_thm horns)) 
24300  630 
in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) 
631 
end 

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

633 

16563  634 
fun meson_claset_tac ths cs = 
635 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); 

9869  636 

16563  637 
val meson_tac = CLASET' (meson_claset_tac []); 
9869  638 

639 

14813  640 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  641 

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

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

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

647 
prevents a double negation.*) 

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

24300  651 
fun negated_asm_of_head th = 
14744  652 
th RS notEfalse handle THM _ => th RS notEfalse'; 
653 

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

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

655 
fun make_meta_clause th = 
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

656 
let val (fth,thaw) = Drule.freeze_thaw_robust th 
19df083a2bbf
make_meta_clause bugfix: now works for higherorder clauses like LeastI_ex
paulson
parents:
25710
diff
changeset

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

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

659 
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

660 
end; 
24300  661 

14744  662 
fun make_meta_clauses ths = 
663 
name_thms "MClause#" 

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

664 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  665 

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

667 
fun make_last i th = 

24300  668 
let val n = nprems_of th 
669 
in if 1 <= i andalso i <= n 

14744  670 
then Thm.permute_prems (i1) 1 th 
15118  671 
else raise THM("select_literal", i, [th]) 
14744  672 
end; 
673 

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

675 
doublenegations.*) 

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

677 

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

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

680 

18508  681 

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

688 

24300  689 
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

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

692 
EVERY' [METAHYPS 
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

693 
(fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1 
14813  694 
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

695 
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

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

697 
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

698 

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

699 
end; 