author  wenzelm 
Thu, 16 Feb 2012 16:42:26 +0100  
changeset 46503  186f4cab2ba0 
parent 46093  4bf24b90703c 
child 46818  2a28e66e2e4c 
permissions  rwrr 
39941  1 
(* Title: HOL/Tools/Meson/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 
39941  3 
Author: Jasmin Blanchette, TU Muenchen 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

4 

9869  5 
The MESON resolution proof procedure for HOL. 
29267  6 
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

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

8 

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

10 
sig 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39953
diff
changeset

11 
val trace : bool Config.T 
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39953
diff
changeset

12 
val max_clauses : int Config.T 
24300  13 
val term_pair_of: indexname * (typ * 'a) > term * 'a 
45567
8e3891309a8e
avoid that var names get changed by resolution in Metis lambdalifting
blanchet
parents:
43964
diff
changeset

14 
val first_order_resolve : thm > thm > thm 
24300  15 
val size_of_subgoals: thm > int 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

16 
val has_too_many_clauses: Proof.context > term > bool 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

17 
val make_cnf: 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

18 
thm list > thm > Proof.context 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

19 
> Proof.context > thm list * Proof.context 
24300  20 
val finish_cnf: thm list > thm list 
46093  21 
val presimplified_consts : string list 
22 
val presimplify: thm > thm 

32262  23 
val make_nnf: Proof.context > thm > thm 
39950  24 
val choice_theorems : theory > thm list 
25 
val skolemize_with_choice_theorems : Proof.context > thm list > thm > thm 

39904  26 
val skolemize : Proof.context > thm > thm 
42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

27 
val extensionalize_conv : Proof.context > conv 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

28 
val extensionalize_theorem : Proof.context > thm > thm 
24300  29 
val is_fol_term: theory > term > bool 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

30 
val make_clauses_unsorted: Proof.context > thm list > thm list 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

31 
val make_clauses: Proof.context > thm list > thm list 
24300  32 
val make_horns: thm list > thm list 
33 
val best_prolog_tac: (thm > int) > thm list > tactic 

34 
val depth_prolog_tac: thm list > tactic 

35 
val gocls: thm list > thm list 

39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

36 
val skolemize_prems_tac : Proof.context > thm list > int > tactic 
39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38864
diff
changeset

37 
val MESON: 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

38 
tactic > (thm list > thm list) > (thm list > tactic) > Proof.context 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

39 
> int > tactic 
32262  40 
val best_meson_tac: (thm > int) > Proof.context > int > tactic 
41 
val safe_best_meson_tac: Proof.context > int > tactic 

42 
val depth_meson_tac: Proof.context > int > tactic 

24300  43 
val prolog_step_tac': thm list > int > tactic 
44 
val iter_deepen_prolog_tac: thm list > tactic 

32262  45 
val iter_deepen_meson_tac: Proof.context > thm list > int > tactic 
24300  46 
val make_meta_clause: thm > thm 
47 
val make_meta_clauses: thm list > thm list 

32262  48 
val meson_tac: Proof.context > thm list > int > tactic 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

50 

39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset

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

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

53 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42455
diff
changeset

54 
val trace = Attrib.setup_config_bool @{binding meson_trace} (K false) 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39953
diff
changeset

55 

b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39953
diff
changeset

56 
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () 
32955  57 

42739
017e5dac8642
added unfold set constant functionality to Meson/Metis  disabled by default for now
blanchet
parents:
42616
diff
changeset

58 
val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K 60) 
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

59 

38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

60 
(*No known example (on 152007) needs even thirty*) 
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

61 
val iter_deepen_limit = 50; 
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

62 

31454  63 
val disj_forward = @{thm disj_forward}; 
64 
val disj_forward2 = @{thm disj_forward2}; 

65 
val make_pos_rule = @{thm make_pos_rule}; 

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

67 
val make_pos_goal = @{thm make_pos_goal}; 

68 
val make_neg_rule = @{thm make_neg_rule}; 

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

70 
val make_neg_goal = @{thm make_neg_goal}; 

71 
val conj_forward = @{thm conj_forward}; 

72 
val all_forward = @{thm all_forward}; 

73 
val ex_forward = @{thm ex_forward}; 

74 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

75 
val not_conjD = @{thm not_conjD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

76 
val not_disjD = @{thm not_disjD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

77 
val not_notD = @{thm not_notD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

78 
val not_allD = @{thm not_allD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

79 
val not_exD = @{thm not_exD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

80 
val imp_to_disjD = @{thm imp_to_disjD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

81 
val not_impD = @{thm not_impD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

82 
val iff_to_disjD = @{thm iff_to_disjD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

83 
val not_iffD = @{thm not_iffD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

84 
val conj_exD1 = @{thm conj_exD1}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

85 
val conj_exD2 = @{thm conj_exD2}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

86 
val disj_exD = @{thm disj_exD}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

87 
val disj_exD1 = @{thm disj_exD1}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

88 
val disj_exD2 = @{thm disj_exD2}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

89 
val disj_assoc = @{thm disj_assoc}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

90 
val disj_comm = @{thm disj_comm}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

91 
val disj_FalseD1 = @{thm disj_FalseD1}; 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

92 
val disj_FalseD2 = @{thm disj_FalseD2}; 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

93 

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

94 

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

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

96 

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

97 

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

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

99 

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

100 
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

101 

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

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

103 
fun first_order_resolve thA thB = 
32262  104 
(case 
105 
try (fn () => 

106 
let val thy = theory_of_thm thA 

107 
val tmA = concl_of thA 

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

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

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

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

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

114 
SOME th => th 

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

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

116 

40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

117 
(* Hack to make it less likely that we lose our precious bound variable names in 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

118 
"rename_bound_vars_RS" below, because of a clash. *) 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

119 
val protect_prefix = "Meson_xyzzy" 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

120 

8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

121 
fun protect_bound_var_names (t $ u) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

122 
protect_bound_var_names t $ protect_bound_var_names u 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

123 
 protect_bound_var_names (Abs (s, T, t')) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

124 
Abs (protect_prefix ^ s, T, protect_bound_var_names t') 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

125 
 protect_bound_var_names t = t 
39930
61aa00205a88
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents:
39904
diff
changeset

126 

40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

127 
fun fix_bound_var_names old_t new_t = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

128 
let 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

129 
fun quant_of @{const_name All} = SOME true 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

130 
 quant_of @{const_name Ball} = SOME true 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

131 
 quant_of @{const_name Ex} = SOME false 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

132 
 quant_of @{const_name Bex} = SOME false 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

133 
 quant_of _ = NONE 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

134 
val flip_quant = Option.map not 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

135 
fun some_eq (SOME x) (SOME y) = x = y 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

136 
 some_eq _ _ = false 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

137 
fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

138 
add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

139 
 add_names quant (@{const Not} $ t) = add_names (flip_quant quant) t 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

140 
 add_names quant (@{const implies} $ t1 $ t2) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

141 
add_names (flip_quant quant) t1 #> add_names quant t2 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

142 
 add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2] 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

143 
 add_names _ _ = I 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

144 
fun lost_names quant = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

145 
subtract (op =) (add_names quant new_t []) (add_names quant old_t []) 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

146 
fun aux ((t1 as Const (quant_s, _)) $ (Abs (s, T, t'))) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

147 
t1 $ Abs (s > String.isPrefix protect_prefix s 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

148 
? perhaps (try (fn _ => hd (lost_names (quant_of quant_s)))), 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

149 
T, aux t') 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

150 
 aux (t1 $ t2) = aux t1 $ aux t2 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

151 
 aux t = t 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

152 
in aux new_t end 
39930
61aa00205a88
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents:
39904
diff
changeset

153 

40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

154 
(* Forward proof while preserving bound variables names *) 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

155 
fun rename_bound_vars_RS th rl = 
39904  156 
let 
157 
val t = concl_of th 

39930
61aa00205a88
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents:
39904
diff
changeset

158 
val r = concl_of rl 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

159 
val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl 
39904  160 
val t' = concl_of th' 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

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

162 

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

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

165 
let fun tryall [] = raise THM("tryres", 0, th::rls) 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

166 
 tryall (rl::rls) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

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

168 
in tryall rls end; 
24300  169 

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

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

171 
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

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

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

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

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

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

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

181 
in 
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37539
diff
changeset

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

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

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

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

186 

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

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

188 
fun has_conns bs = 
39328  189 
let fun has (Const _) = false 
38557  190 
 has (Const(@{const_name Trueprop},_) $ p) = has p 
191 
 has (Const(@{const_name Not},_) $ p) = has p 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

192 
 has (Const(@{const_name HOL.disj},_) $ p $ q) = member (op =) bs @{const_name HOL.disj} orelse has p orelse has q 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

193 
 has (Const(@{const_name HOL.conj},_) $ p $ q) = member (op =) bs @{const_name HOL.conj} orelse has p orelse has q 
38557  194 
 has (Const(@{const_name All},_) $ Abs(_,_,p)) = member (op =) bs @{const_name All} orelse has p 
195 
 has (Const(@{const_name Ex},_) $ Abs(_,_,p)) = member (op =) bs @{const_name Ex} orelse has p 

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

197 
in has end; 
24300  198 

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

199 

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

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

201 

38557  202 
fun literals (Const(@{const_name Trueprop},_) $ P) = literals P 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

203 
 literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q 
38557  204 
 literals (Const(@{const_name Not},_) $ P) = [(false,P)] 
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset

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

206 

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

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

208 
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

209 

18389  210 

211 
(*** Tautology Checking ***) 

212 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

213 
fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) = 
18389  214 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 
38557  215 
 signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits) 
18389  216 
 signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); 
24300  217 

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

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

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38806
diff
changeset

221 
fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u 
38557  222 
 taut_poslit (Const(@{const_name True},_)) = true 
18389  223 
 taut_poslit _ = false; 
224 

225 
fun is_taut th = 

226 
let val (poslits,neglits) = signed_lits th 

227 
in exists taut_poslit poslits 

228 
orelse 

45740  229 
exists (member (op aconv) neglits) (@{term False} :: poslits) 
19894  230 
end 
24300  231 
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) 
18389  232 

233 

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

235 

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

237 
injectivity equivalences*) 

24300  238 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

239 
val not_refl_disj_D = @{thm not_refl_disj_D}; 
18389  240 

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

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

244 
 eliminable _ = false; 

245 

18389  246 
fun refl_clause_aux 0 th = th 
247 
 refl_clause_aux n th = 

248 
case HOLogic.dest_Trueprop (concl_of th) of 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

249 
(Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) => 
18389  250 
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38806
diff
changeset

251 
 (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) => 
24300  252 
if eliminable(t,u) 
253 
then refl_clause_aux (n1) (th RS not_refl_disj_D) (*Var inequation: delete*) 

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

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

255 
 (Const (@{const_name HOL.disj}, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) 
24300  256 
 _ => (*not a disjunction*) th; 
18389  257 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

258 
fun notequal_lits_count (Const (@{const_name HOL.disj}, _) $ P $ Q) = 
18389  259 
notequal_lits_count P + notequal_lits_count Q 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38806
diff
changeset

260 
 notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1 
18389  261 
 notequal_lits_count _ = 0; 
262 

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

24300  264 
fun refl_clause th = 
18389  265 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 
19894  266 
in zero_var_indexes (refl_clause_aux neqs th) end 
24300  267 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 
18389  268 

269 

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

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

271 

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

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

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

275 
(REPEAT 
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37539
diff
changeset

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

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

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

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

280 

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

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

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

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

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

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

288 

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

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

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

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

294 

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

295 

18389  296 
(*** The basic CNF transformation ***) 
297 

39328  298 
fun estimated_num_clauses bound t = 
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

299 
let 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

300 
fun sum x y = if x < bound andalso y < bound then x+y else bound 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

301 
fun prod x y = if x < bound andalso y < bound then x*y else bound 
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

302 

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

303 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
38557  304 
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t 
305 
 signed_nclauses b (Const(@{const_name Not},_) $ t) = signed_nclauses (not b) t 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

306 
 signed_nclauses b (Const(@{const_name HOL.conj},_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

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

308 
else prod (signed_nclauses b t) (signed_nclauses b u) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

309 
 signed_nclauses b (Const(@{const_name HOL.disj},_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

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

311 
else sum (signed_nclauses b t) (signed_nclauses b u) 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38709
diff
changeset

312 
 signed_nclauses b (Const(@{const_name HOL.implies},_) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

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

314 
else sum (signed_nclauses (not b) t) (signed_nclauses b u) 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38806
diff
changeset

315 
 signed_nclauses b (Const(@{const_name HOL.eq}, Type ("fun", [T, _])) $ t $ u) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32955
diff
changeset

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

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

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

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

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

321 
else 1 
38557  322 
 signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t 
323 
 signed_nclauses b (Const(@{const_name All},_) $ Abs (_,_,t)) = signed_nclauses b t 

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

324 
 signed_nclauses _ _ = 1; (* literal *) 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

325 
in signed_nclauses true t end 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

326 

c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

327 
fun has_too_many_clauses ctxt t = 
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

328 
let val max_cl = Config.get ctxt max_clauses in 
39328  329 
estimated_num_clauses (max_cl + 1) t > max_cl 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

330 
end 
19894  331 

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

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

333 
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

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

335 
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

336 
val spec_varT = #T (Thm.rep_cterm spec_var); 
38557  337 
fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x  name_of _ = Name.uu; 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

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

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

340 
let 
42361  341 
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

342 
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

343 
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

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

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

346 

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

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

348 
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

349 
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

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

351 
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

352 

39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38864
diff
changeset

353 
(* Any need to extend this list with "HOL.type_class", "HOL.eq_class", 
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38864
diff
changeset

354 
and "Pure.term"? *) 
38557  355 
val has_meta_conn = 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

356 

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

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

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

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

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

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

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

363 

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

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

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

366 
Eliminates existential quantifiers using Skolemization theorems. *) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

367 
fun cnf old_skolem_ths ctxt ctxt0 (th, ths) = 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

368 
let val ctxt0r = Unsynchronized.ref ctxt0 (* FIXME ??? *) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset

369 
fun cnf_aux (th,ths) = 
24300  370 
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*metalevel: ignore*) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

371 
else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th)) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

372 
then nodups ctxt0 th :: ths (*no work to do, terminate*) 
24300  373 
else case head_of (HOLogic.dest_Trueprop (concl_of th)) of 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

374 
Const (@{const_name HOL.conj}, _) => (*conjunction*) 
24300  375 
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) 
38557  376 
 Const (@{const_name All}, _) => (*universal quantifier*) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

377 
let val (th',ctxt0') = freeze_spec th (!ctxt0r) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

378 
in ctxt0r := ctxt0'; cnf_aux (th', ths) end 
38557  379 
 Const (@{const_name Ex}, _) => 
24300  380 
(*existential quantifier: Insert Skolem functions*) 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39328
diff
changeset

381 
cnf_aux (apply_skolem_theorem (th, old_skolem_ths), ths) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

382 
 Const (@{const_name HOL.disj}, _) => 
24300  383 
(*Disjunction of P, Q: Create new goal of proving ?P  ?Q and solve it using 
384 
all combinations of converting P, Q to CNF.*) 

385 
let val tac = 

37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37539
diff
changeset

386 
Misc_Legacy.METAHYPS (resop cnf_nil) 1 THEN 
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37539
diff
changeset

387 
(fn st' => st' > Misc_Legacy.METAHYPS (resop cnf_nil) 1) 
24300  388 
in Seq.list_of (tac (th RS disj_forward)) @ ths end 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

389 
 _ => nodups ctxt0 th :: ths (*no work to do*) 
19154  390 
and cnf_nil th = cnf_aux (th,[]) 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

391 
val cls = 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

392 
if has_too_many_clauses ctxt (concl_of th) then 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

393 
(trace_msg ctxt (fn () => 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

394 
"cnf is ignoring: " ^ Display.string_of_thm ctxt0 th); ths) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

395 
else 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

396 
cnf_aux (th, ths) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

397 
in (cls, !ctxt0r) end 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

398 
fun make_cnf old_skolem_ths th ctxt ctxt0 = 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

399 
cnf old_skolem_ths ctxt ctxt0 (th, []) 
20417
c611b1412056
better skolemization, using firstorder resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset

400 

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

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

402 
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

403 

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

404 

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

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

406 

38557  407 
fun is_left (Const (@{const_name Trueprop}, _) $ 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

408 
(Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _)) = true 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

409 
 is_left _ = false; 
24300  410 

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

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

413 
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

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

415 

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

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

417 
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

418 

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

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

420 
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

421 

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

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

423 
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

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

425 
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

426 

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

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

428 
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

429 

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

431 

38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

432 
fun has_bool @{typ bool} = true 
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

433 
 has_bool (Type (_, Ts)) = exists has_bool Ts 
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

434 
 has_bool _ = false 
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

435 

e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

436 
fun has_fun (Type (@{type_name fun}, _)) = true 
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

437 
 has_fun (Type (_, Ts)) = exists has_fun Ts 
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

438 
 has_fun _ = false 
24300  439 

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

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

19875  442 
val is_conn = member (op =) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

443 
[@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38709
diff
changeset

444 
@{const_name HOL.implies}, @{const_name Not}, 
38557  445 
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}]; 
15613  446 

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

448 
of any argument contains bool.*) 
24300  449 
val has_bool_arg_const = 
15613  450 
exists_Const 
38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

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

452 

24300  453 
(*A higherorder instance of a firstorder constant? Example is the definition of 
38622  454 
one, 1, at a function type in theory Function_Algebras.*) 
24300  455 
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

456 
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

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

458 
 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

459 

42833  460 
(* Returns false if any Vars in the theorem mention type bool. 
461 
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

462 
fun is_fol_term thy t = 
42833  463 
Term.is_first_order [@{const_name all}, @{const_name All}, 
464 
@{const_name Ex}] t andalso 

38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

465 
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T 
42833  466 
 _ => false) t orelse 
38099
e3bb96b83807
fix Meson's definition of firstorderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents:
38089
diff
changeset

467 
has_bool_arg_const t orelse 
24300  468 
exists_Const (higher_inst_const thy) t orelse 
469 
has_meta_conn t); 

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

470 

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

471 
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

472 

38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

473 
fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t 
38557  474 
 ok4horn (Const (@{const_name Trueprop},_) $ t) = rigid t 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset

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

476 

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

477 
(*Create a metalevel Horn clause*) 
24300  478 
fun make_horn crules th = 
479 
if ok4horn (concl_of th) 

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

480 
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

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

482 

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

33339  485 
fun add_contras crules th hcs = 
39328  486 
let fun rots (0,_) = hcs 
24300  487 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
488 
rots(k1, assoc_right (th RS disj_comm)) 

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

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

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

493 

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

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

495 
fun name_thms label = 
33339  496 
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

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

499 

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

501 
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

502 

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

504 

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

505 

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

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

507 

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

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

511 

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

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

513 

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

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

516 

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

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

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

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

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

522 

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

523 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  524 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
525 
 TRYING_eq_assume_tac i st = 

31945  526 
TRYING_eq_assume_tac (i1) (Thm.eq_assumption i st) 
18508  527 
handle THM _ => TRYING_eq_assume_tac (i1) st; 
528 

529 
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

530 

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

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

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

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

534 
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

535 
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

536 

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

537 

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

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

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

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

542 

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

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

545 

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

547 

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

548 

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

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

550 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  551 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  552 

38557  553 
fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t 
554 
 ok4nnf (Const (@{const_name Trueprop},_) $ t) = rigid t 

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

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

556 

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

560 
handle THM ("tryres", _, _) => 
32262  561 
forward_res ctxt (make_nnf1 ctxt) 
9869  562 
(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

563 
handle THM ("tryres", _, _) => th 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

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

565 

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

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

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

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

573 

43821
048619bb1dc3
always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents:
43264
diff
changeset

574 
(* FIXME: "let_simp" is probably redundant now that we also rewrite with 
048619bb1dc3
always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents:
43264
diff
changeset

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

576 
val nnf_ss = 
24300  577 
HOL_basic_ss addsimps nnf_extra_simps 
43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

578 
addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

579 
@{simproc let_simp}] 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

580 

46093  581 
val presimplified_consts = 
43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

582 
[@{const_name simp_implies}, @{const_name False}, @{const_name True}, 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

583 
@{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If}, 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

584 
@{const_name Let}] 
15872  585 

46093  586 
val presimplify = 
42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

587 
rewrite_rule (map safe_mk_meta_eq nnf_simps) 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

588 
#> simplify nnf_ss 
46071
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

589 
#> Raw_Simplifier.rewrite_rule @{thms Let_def_raw} 
38089
ed65a0777e10
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
blanchet
parents:
37926
diff
changeset

590 

32262  591 
fun make_nnf ctxt th = case prems_of th of 
46093  592 
[] => th > presimplify > make_nnf1 ctxt 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

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

39950  595 
fun choice_theorems thy = 
596 
try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" > the_list 

597 

39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

598 
(* Pull existential quantifiers to front. This accomplishes Skolemization for 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

599 
clauses that arise from a subgoal. *) 
39950  600 
fun skolemize_with_choice_theorems ctxt choice_ths = 
39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

601 
let 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

602 
fun aux th = 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

603 
if not (has_conns [@{const_name Ex}] (prop_of th)) then 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

604 
th 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

605 
else 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset

606 
tryres (th, choice_ths @ 
39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

607 
[conj_exD1, conj_exD2, disj_exD, disj_exD1, disj_exD2]) 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

608 
> aux 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

609 
handle THM ("tryres", _, _) => 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

610 
tryres (th, [conj_forward, disj_forward, all_forward]) 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

611 
> forward_res ctxt aux 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

612 
> aux 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

613 
handle THM ("tryres", _, _) => 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset

614 
rename_bound_vars_RS th ex_forward 
39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

615 
> forward_res ctxt aux 
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

616 
in aux o make_nnf ctxt end 
29684  617 

39950  618 
fun skolemize ctxt = 
42361  619 
let val thy = Proof_Context.theory_of ctxt in 
39950  620 
skolemize_with_choice_theorems ctxt (choice_theorems thy) 
621 
end 

39904  622 

42760  623 
(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It 
624 
would be desirable to do this symmetrically but there's at least one existing 

625 
proof in "Tarski" that relies on the current behavior. *) 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

626 
fun extensionalize_conv ctxt ct = 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

627 
case term_of ct of 
42760  628 
Const (@{const_name HOL.eq}, _) $ _ $ Abs _ => 
629 
ct > (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]} 

630 
then_conv extensionalize_conv ctxt) 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

631 
 _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

632 
 Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

633 
 _ => Conv.all_conv ct 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

634 

f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

635 
val extensionalize_theorem = Conv.fconv_rule o extensionalize_conv 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

636 

39900
549c00e0e89b
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
blanchet
parents:
39893
diff
changeset

637 
(* "RS" can fail if "unify_search_bound" is too small. *) 
46071
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

638 
fun try_skolemize_etc ctxt th = 
42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

639 
(* Extensionalize "th", because that makes sense and that's what Sledgehammer 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

640 
does, but also keep an unextensionalized version of "th" for backward 
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

641 
compatibility. *) 
46071
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

642 
[th] > insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

643 
> map_filter (fn th => th > try (skolemize ctxt) 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

644 
> tap (fn NONE => 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

645 
trace_msg ctxt (fn () => 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

646 
"Failed to skolemize " ^ 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

647 
Display.string_of_thm ctxt th) 
1613933e412c
killed unfold_set_const option that makes no sense now that set is a type constructor again
blanchet
parents:
45981
diff
changeset

648 
 _ => ())) 
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset

649 

43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

651 
let val ctxt0 = Variable.global_thm_context th 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

653 
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

654 

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

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

656 
The resulting clauses are HOL disjunctions.*) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

657 
fun make_clauses_unsorted ctxt ths = fold_rev (add_clauses ctxt) ths []; 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

659 

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

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

664 

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

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

666 
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

667 

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

669 
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

670 

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

672 
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

673 

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

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

675 
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

676 

32262  677 
fun skolemize_prems_tac ctxt prems = 
42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42739
diff
changeset

678 
cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

679 

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

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

681 
Function mkcl converts theorems to clauses.*) 
39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38864
diff
changeset

682 
fun MESON preskolem_tac mkcl cltac ctxt i st = 
16588  683 
SELECT_GOAL 
35625  684 
(EVERY [Object_Logic.atomize_prems_tac 1, 
23552  685 
rtac ccontr 1, 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

686 
preskolem_tac, 
32283  687 
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => 
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39159
diff
changeset

688 
EVERY1 [skolemize_prems_tac ctxt negs, 
32283  689 
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st 
24300  690 
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

691 

39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
38864
diff
changeset

692 

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

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

694 

16563  695 
(*ths is a list of additional clauses (HOL disjunctions) to use.*) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

696 
fun best_meson_tac sizef ctxt = 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

697 
MESON all_tac (make_clauses ctxt) 
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset

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

699 
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

700 
(has_fewer_prems 1, sizef) 
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

701 
(prolog_step_tac (make_horns cls) 1)) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

703 

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

704 
(*First, breaks the goal into independent units*) 
32262  705 
fun safe_best_meson_tac ctxt = 
42793  706 
SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt)); 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

707 

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

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

709 

43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

710 
fun depth_meson_tac ctxt = 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

711 
MESON all_tac (make_clauses ctxt) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

712 
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]) 
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

714 

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

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

716 

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

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

718 
having only one eq_assume_tac speeds it up!*) 
9869  719 
fun prolog_step_tac' horns = 
39328  720 
let val (horn0s, _) = (*0 subgoals vs 1 or more*) 
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset

721 
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

722 
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

723 
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

724 
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

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

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

727 

9869  728 
fun iter_deepen_prolog_tac horns = 
38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

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

730 

43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43821
diff
changeset

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

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

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

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

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

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

737 
val horns = make_horns (cls @ ths) 
39979
b13515940b53
added "trace_meson" configuration option, replacing oldfashioned reference
blanchet
parents:
39953
diff
changeset

738 
val _ = trace_msg ctxt (fn () => 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset

739 
cat_lines ("meson method called:" :: 
32262  740 
map (Display.string_of_thm ctxt) (cls @ ths) @ 
741 
["clauses:"] @ map (Display.string_of_thm ctxt) horns)) 

38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

742 
in 
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

743 
THEN_ITER_DEEPEN iter_deepen_limit 
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

744 
(resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) 
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
38795
diff
changeset

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

746 

32262  747 
fun meson_tac ctxt ths = 
42793  748 
SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); 
9869  749 

750 

14813  751 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  752 

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

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

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

758 
prevents a double negation.*) 

46503  759 
val notEfalse = @{lemma "~ P ==> P ==> False" by (rule notE)}; 
760 
val notEfalse' = @{lemma "P ==> ~ P ==> False" by (rule notE)}; 

14744  761 

24300  762 
fun negated_asm_of_head th = 
14744  763 
th RS notEfalse handle THM _ => th RS notEfalse'; 
764 

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

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

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

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

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

770 
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

771 
end; 
24300  772 

14744  773 
fun make_meta_clauses ths = 
774 
name_thms "MClause#" 

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

775 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  776 

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

777 
end; 