author  wenzelm 
Wed, 02 Aug 2006 22:26:40 +0200  
changeset 20288  8ff4a0ea49b2 
parent 20134  73cb53843190 
child 20361  1aaf9ebe248d 
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 
NEED TO SORT LITERALS BY # OF VARS, USING ==>I/E. ELIMINATES NEED FOR 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

11 
FUNCTION nodups  if done to goal clauses too! 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

13 

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

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

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

16 
val size_of_subgoals : thm > int 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

17 
val make_cnf : thm list > thm > thm list 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

18 
val make_nnf : thm > thm 
17849  19 
val make_nnf1 : thm > thm 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

21 
val make_clauses : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

22 
val make_horns : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

23 
val best_prolog_tac : (thm > int) > thm list > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

24 
val depth_prolog_tac : thm list > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

25 
val gocls : thm list > thm list 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

26 
val skolemize_prems_tac : thm list > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

27 
val MESON : (thm list > tactic) > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

28 
val best_meson_tac : (thm > int) > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

29 
val safe_best_meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

30 
val depth_meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

31 
val prolog_step_tac' : thm list > int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

32 
val iter_deepen_prolog_tac : thm list > tactic 
16563  33 
val iter_deepen_meson_tac : thm list > int > tactic 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

34 
val meson_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

36 
val select_literal : int > thm > thm 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

37 
val skolemize_tac : int > tactic 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

38 
val make_clauses_tac : int > tactic 
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

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

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

41 

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

42 

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

43 
structure Meson = 
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 

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

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

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

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

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

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

51 
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

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

53 
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

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

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

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

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

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

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

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

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

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

63 
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

64 

16563  65 
val depth_limit = ref 2000; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

66 

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

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

68 

18175
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset

69 
(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*) 
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset

70 
fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb); 
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset

71 

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

72 
(*raises exception if no rules apply  unlike RL*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

73 
fun tryres (th, rls) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

74 
let fun tryall [] = raise THM("tryres", 0, th::rls) 
19875  75 
 tryall (rl::rls) = (resolve1(th,rl) handle Option.Option => tryall rls) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

76 
in tryall rls end; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

77 

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

78 
(*Permits forward proof from rules that discharge assumptions*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

80 
case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

81 
of SOME(th,_) => th 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

82 
 NONE => raise THM("forward_res", 0, [st]); 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

83 

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

84 

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

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

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

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

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

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

90 
 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

91 
 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

92 
 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

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

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

95 
in has end; 
17716  96 

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

97 

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

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

99 

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

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

101 
 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

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

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

104 

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

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

106 
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

107 

18389  108 

109 
(*** Tautology Checking ***) 

110 

111 
fun signed_lits_aux (Const ("op ", _) $ P $ Q) (poslits, neglits) = 

112 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 

113 
 signed_lits_aux (Const("Not",_) $ P) (poslits, neglits) = (poslits, P::neglits) 

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

115 

116 
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]); 

117 

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

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

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

121 
 taut_poslit _ = false; 

122 

123 
fun is_taut th = 

124 
let val (poslits,neglits) = signed_lits th 

125 
in exists taut_poslit poslits 

126 
orelse 

20073  127 
exists (member (op aconv) neglits) (HOLogic.false_const :: poslits) 
19894  128 
end 
129 
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) 

18389  130 

131 

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

133 

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

135 
injectivity equivalences*) 

136 

137 
val not_refl_disj_D = thm"meson_not_refl_disj_D"; 

138 

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

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

142 
 eliminable _ = false; 

143 

18389  144 
fun refl_clause_aux 0 th = th 
145 
 refl_clause_aux n th = 

146 
case HOLogic.dest_Trueprop (concl_of th) of 

147 
(Const ("op ", _) $ (Const ("op ", _) $ _ $ _) $ _) => 

148 
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) 

149 
 (Const ("op ", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => 

20119  150 
if eliminable(t,u) 
151 
then refl_clause_aux (n1) (th RS not_refl_disj_D) (*Var inequation: delete*) 

18389  152 
else refl_clause_aux (n1) (th RS disj_comm) (*not between Vars: ignore*) 
153 
 (Const ("op ", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) 

18752
c9c6ae9e8b88
Clausification now handles some IFs in rewrite rules (ifsplit did not work)
paulson
parents:
18708
diff
changeset

154 
 _ => (*not a disjunction*) th; 
18389  155 

156 
fun notequal_lits_count (Const ("op ", _) $ P $ Q) = 

157 
notequal_lits_count P + notequal_lits_count Q 

158 
 notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 

159 
 notequal_lits_count _ = 0; 

160 

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

162 
fun refl_clause th = 

163 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 

19894  164 
in zero_var_indexes (refl_clause_aux neqs th) end 
165 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 

18389  166 

167 

168 
(*** The basic CNF transformation ***) 

169 

19894  170 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
171 
fun nclauses (Const("Trueprop",_) $ t) = nclauses t 

172 
 nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u 

173 
 nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t 

174 
 nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t 

175 
 nclauses (Const("op ",_) $ t $ u) = nclauses t * nclauses u 

176 
 nclauses _ = 1; (* literal *) 

177 

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

178 
(*Replaces universally quantified variables by FREE variables  because 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

179 
assumptions may not contain scheme variables. Later, call "generalize". *) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

180 
fun freeze_spec th = 
19728  181 
let val newname = gensym "A_" 
19154  182 
val spec' = read_instantiate [("x", newname)] spec 
183 
in th RS spec' end; 

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

184 

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

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

186 
and then normalized via function nf. The normal form is given to resolve_tac, 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

187 
presumably to instantiate a Boolean variable.*) 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

188 
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

189 

18389  190 
val has_meta_conn = 
191 
exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]); 

192 

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

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

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

195 
Eliminates existential quantifiers using skoths: Skolemization theorems.*) 
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

196 
fun cnf skoths (th,ths) = 
18389  197 
let fun cnf_aux (th,ths) = 
19894  198 
if has_meta_conn (prop_of th) then ths (*metalevel: ignore*) 
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the firstorder formula
paulson
parents:
20119
diff
changeset

199 
else if not (has_conns ["All","Ex","op &"] (prop_of th)) 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

200 
then th::ths (*no work to do, terminate*) 
16588  201 
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of 
202 
Const ("op &", _) => (*conjunction*) 

18389  203 
cnf_aux (th RS conjunct1, 
204 
cnf_aux (th RS conjunct2, ths)) 

16588  205 
 Const ("All", _) => (*universal quantifier*) 
18389  206 
cnf_aux (freeze_spec th, ths) 
16588  207 
 Const ("Ex", _) => 
208 
(*existential quantifier: Insert Skolem functions*) 

18389  209 
cnf_aux (tryres (th,skoths), ths) 
16588  210 
 Const ("op ", _) => (*disjunction*) 
211 
let val tac = 

18389  212 
(METAHYPS (resop cnf_nil) 1) THEN 
19154  213 
(fn st' => st' > METAHYPS (resop cnf_nil) 1) 
16588  214 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 
215 
 _ => (*no work to do*) th::ths 

19154  216 
and cnf_nil th = cnf_aux (th,[]) 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

217 
in 
19894  218 
if nclauses (concl_of th) > 20 
219 
then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths) 

220 
else cnf_aux (th,ths) 

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

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

222 

16012  223 
(*Convert all suitable free variables to schematic variables, 
224 
but don't discharge assumptions.*) 

16173  225 
fun generalize th = Thm.varifyT (forall_elim_vars 0 (forall_intr_frees th)); 
16012  226 

18389  227 
fun make_cnf skoths th = 
228 
filter (not o is_taut) 

229 
(map (refl_clause o generalize) (cnf skoths (th, []))); 

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

230 

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

231 

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

232 
(**** Removal of duplicate literals ****) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

233 

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

234 
(*Forward proof, passing extra assumptions as theorems to the tactic*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

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

238 
(METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

240 
of SOME(th,_) => th 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

241 
 NONE => raise THM("forward_res2", 0, [st]); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

242 

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

243 
(*Remove duplicates in PQ by assuming ~P in Q 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

244 
rls (initially []) accumulates assumptions of the form P==>False*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

245 
fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

246 
handle THM _ => tryres(th,rls) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

247 
handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

248 
[disj_FalseD1, disj_FalseD2, asm_rl]) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

249 
handle THM _ => th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

250 

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

251 
(*Remove duplicate literals, if there are any*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

253 
if null(findrep(literals(prop_of th))) then th 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

255 

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

256 

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

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

258 

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

259 
(*Associate disjuctions to right  make leftmost disjunct a LITERAL*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

260 
fun assoc_right th = assoc_right (th RS disj_assoc) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

261 
handle THM _ => th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

262 

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

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

264 
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

265 

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

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

267 
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

268 

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

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

270 
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

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

272 
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

273 

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

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

275 
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

276 

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

278 

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

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

282 
 has_bool _ = false; 

283 

15613  284 
(*Is the string the name of a connective? It doesn't matter if this list is 
285 
incomplete, since when actually called, the only connectives likely to 

286 
remain are &  Not.*) 

19875  287 
val is_conn = member (op =) 
20018  288 
["Trueprop", "op &", "op ", "op >", "op =", "Not", 
15613  289 
"All", "Ex", "Ball", "Bex"]; 
290 

291 
(*True if the term contains a function where the type of any argument contains 

292 
bool.*) 

293 
val has_bool_arg_const = 

294 
exists_Const 

295 
(fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); 

15908  296 

16588  297 
(*Raises an exception if any Vars in the theorem mention type bool; they 
298 
could cause make_horn to loop! Also rejects functions whose arguments are 

299 
Booleans or other functions.*) 

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

300 
fun is_fol_term t = 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

301 
not (exists (has_bool o fastype_of) (term_vars t) orelse 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

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

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

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

305 

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

306 
(*FIXME: replace this by the booleanvalued version above!*) 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

307 
fun check_is_fol_term t = 
b8f7de7ef629
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
paulson
parents:
19154
diff
changeset

308 
if is_fol_term t then t else raise TERM("check_is_fol_term",[t]); 
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

309 

18508  310 
fun check_is_fol th = (check_is_fol_term (prop_of th); th); 
311 

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

312 

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

313 
(*Create a metalevel Horn clause*) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

315 
handle THM _ => th; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

316 

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

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

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

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

321 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

322 
rots(k1, assoc_right (th RS disj_comm)) 
15862  323 
in case nliterals(prop_of th) of 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

324 
1 => th::hcs 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

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

327 

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

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

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

330 
let fun name1 (th, (k,ths)) = 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

331 
(k1, Thm.name_thm (label ^ string_of_int k, th) :: ths) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

332 

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

333 
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

334 

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

336 
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

337 

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

338 
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

339 

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

340 

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

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

342 

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

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

344 
As) = rhyps(phi, A::As) 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

346 

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

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

348 

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

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

351 

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

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

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

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

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

356 
 has_reps ts = (Library.foldl ins_term (Net.empty, ts); false) 
19875  357 
handle Net.INSERT => true; 
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 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  360 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
361 
 TRYING_eq_assume_tac i st = 

362 
TRYING_eq_assume_tac (i1) (eq_assumption i st) 

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

364 

365 
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

366 

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

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

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

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

370 
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

371 
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

372 

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

373 

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

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

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

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

378 

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

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

380 
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

381 

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

382 
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

383 

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

384 

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

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

386 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  387 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  388 

389 
fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls)) 

9869  390 
handle THM _ => 
15581  391 
forward_res make_nnf1 
9869  392 
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

393 
handle THM _ => th; 
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

394 

20018  395 
(*The simplification removes defined quantifiers and occurrences of True and False. 
396 
nnf_ss also includes the onepoint simprocs, 

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

397 
which are needed to avoid the various onepoint theorems from generating junk clauses.*) 
19894  398 
val nnf_simps = 
20018  399 
[simp_implies_def, Ex1_def, Ball_def, Bex_def, if_True, 
19894  400 
if_False, if_cancel, if_eq_cancel, cases_simp]; 
401 
val nnf_extra_simps = 

402 
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

403 

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

404 
val nnf_ss = 
19894  405 
HOL_basic_ss addsimps nnf_extra_simps 
406 
addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; 

15872  407 

19894  408 
fun make_nnf th = th > rewrite_rule (map safe_mk_meta_eq nnf_simps) 
409 
> simplify nnf_ss (*But this doesn't simplify premises...*) 

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

410 
> make_nnf1 
15581  411 

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

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

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

415 
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

416 
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

417 
disj_exD, disj_exD1, disj_exD2]))) 
9869  418 
handle THM _ => 
419 
skolemize (forward_res skolemize 

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

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

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

422 

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

423 

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

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

425 
The resulting clauses are HOL disjunctions.*) 
9869  426 
fun make_clauses ths = 
15998
bc916036cf84
new cnf function taking Skolemization theorems as an extra argument
paulson
parents:
15965
diff
changeset

427 
(sort_clauses (map (generalize o nodups) (foldr (cnf[]) [] ths))); 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

428 

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

429 

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

432 
name_thms "Horn#" 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18817
diff
changeset

433 
(distinct Drule.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

434 

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

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

436 
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

437 

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

439 
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

440 

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

442 
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

443 

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

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

445 
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

446 

15008  447 
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

448 
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

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

450 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

451 
(*Expand all definitions (presumably of Skolem functions) in a proof state.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

452 
fun expand_defs_tac st = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

453 
let val defs = filter (can dest_equals) (#hyps (crep_thm st)) 
20288  454 
in PRIMITIVE (LocalDefs.def_export false defs) st end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

455 

16588  456 
(*Basis of all mesontactics. Supplies cltac with clauses: HOL disjunctions*) 
457 
fun MESON cltac i st = 

458 
SELECT_GOAL 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

459 
(EVERY [rtac ccontr 1, 
16588  460 
METAHYPS (fn negs => 
461 
EVERY1 [skolemize_prems_tac negs, 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

462 
METAHYPS (cltac o make_clauses)]) 1, 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset

463 
expand_defs_tac]) i st 
18508  464 
handle TERM _ => no_tac st; (*probably from check_is_fol*) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

465 

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

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

467 

16563  468 
(*ths is a list of additional clauses (HOL disjunctions) to use.*) 
9869  469 
fun best_meson_tac sizef = 
470 
MESON (fn cls => 

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

471 
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

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

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

474 

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

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

476 
val safe_best_meson_tac = 
9869  477 
SELECT_GOAL (TRY Safe_tac THEN 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

478 
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

479 

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

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

481 

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

482 
val depth_meson_tac = 
9869  483 
MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

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

485 

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

486 

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

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

488 

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

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

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

492 
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

493 
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

494 
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

495 
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

496 
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

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

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

499 

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

501 
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

502 

16563  503 
fun iter_deepen_meson_tac ths = 
9869  504 
MESON (fn cls => 
16563  505 
case (gocls (cls@ths)) of 
506 
[] => no_tac (*no goal clauses*) 

507 
 goes => 

508 
(THEN_ITER_DEEPEN (resolve_tac goes 1) 

509 
(has_fewer_prems 1) 

510 
(prolog_step_tac' (make_horns (cls@ths))))); 

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

511 

16563  512 
fun meson_claset_tac ths cs = 
513 
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths)); 

9869  514 

16563  515 
val meson_tac = CLASET' (meson_claset_tac []); 
9869  516 

517 

14813  518 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  519 

15008  520 
(*Convert a list of clauses (disjunctions) to metalevel clauses (==>), 
521 
with no contrapositives, for ordinary resolution.*) 

14744  522 

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

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

525 
prevents a double negation.*) 

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

527 
val notEfalse' = rotate_prems 1 notEfalse; 

528 

15448  529 
fun negated_asm_of_head th = 
14744  530 
th RS notEfalse handle THM _ => th RS notEfalse'; 
531 

532 
(*Converting one clause*) 

15581  533 
fun make_meta_clause th = 
16588  534 
negated_asm_of_head (make_horn resolution_clause_rules (check_is_fol th)); 
14744  535 

536 
fun make_meta_clauses ths = 

537 
name_thms "MClause#" 

19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18817
diff
changeset

538 
(distinct Drule.eq_thm_prop (map make_meta_clause ths)); 
14744  539 

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

541 
fun make_last i th = 

542 
let val n = nprems_of th 

543 
in if 1 <= i andalso i <= n 

544 
then Thm.permute_prems (i1) 1 th 

15118  545 
else raise THM("select_literal", i, [th]) 
14744  546 
end; 
547 

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

549 
doublenegations.*) 

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

551 

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

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

554 

18508  555 

14813  556 
(*Toplevel Skolemization. Allows part of the conversion to clauses to be 
557 
expressed as a tactic (or Isar method). Each assumption of the selected 

558 
goal is converted to NNF and then its existential quantifiers are pulled 

559 
to the front. Finally, all existential quantifiers are eliminated, 

560 
leaving !!quantified variables. Perhaps Safe_tac should follow, but it 

561 
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

562 

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

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

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

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

566 
EVERY' [METAHYPS 
15773
f14ae2432710
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
quigley
parents:
15736
diff
changeset

567 
(fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1 
14813  568 
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

569 
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

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

571 
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

572 

15118  573 
(*Toplevel conversion to metalevel clauses. Each clause has 
574 
leading !!bound universal variables, to express generality. To get 

575 
disjunctions instead of metaclauses, remove "make_meta_clauses" below.*) 

15008  576 
val make_clauses_tac = 
577 
SUBGOAL 

578 
(fn (prop,_) => 

579 
let val ts = Logic.strip_assums_hyp prop 

580 
in EVERY1 

581 
[METAHYPS 

582 
(fn hyps => 

15151  583 
(Method.insert_tac 
15118  584 
(map forall_intr_vars 
585 
(make_meta_clauses (make_clauses hyps))) 1)), 

15008  586 
REPEAT_DETERM_N (length ts) o (etac thin_rl)] 
587 
end); 

16563  588 

589 

590 
(*** setup the special skoklemization methods ***) 

9869  591 

16563  592 
(*No CHANGED_PROP here, since these always appear in the preamble*) 
9869  593 

16563  594 
val skolemize_meth = Method.SIMPLE_METHOD' HEADGOAL skolemize_tac; 
595 

596 
val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac; 

14890  597 

16563  598 
val skolemize_setup = 
18708  599 
Method.add_methods 
600 
[("skolemize", Method.no_args skolemize_meth, 

601 
"Skolemization into existential quantifiers"), 

602 
("make_clauses", Method.no_args make_clauses_meth, 

603 
"Conversion to !!quantified metalevel clauses")]; 

9840
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 
end; 
9869  606 

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

607 
structure BasicMeson: BASIC_MESON = Meson; 
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

608 
open BasicMeson; 