author  haftmann 
Sat, 24 Dec 2011 16:14:58 +0100  
changeset 45981  4c629115e3ab 
parent 45740  132a3e1c0fe5 
child 46071  1613933e412c 
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 
42739
017e5dac8642
added unfold set constant functionality to Meson/Metis  disabled by default for now
blanchet
parents:
42616
diff
changeset

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

13 
val max_clauses : int Config.T 
24300  14 
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

15 
val first_order_resolve : thm > thm > thm 
24300  16 
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

17 
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

18 
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

19 
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

20 
> Proof.context > thm list * Proof.context 
24300  21 
val finish_cnf: thm list > thm list 
42739
017e5dac8642
added unfold set constant functionality to Meson/Metis  disabled by default for now
blanchet
parents:
42616
diff
changeset

22 
val unfold_set_const_simps : Proof.context > thm list 
43264
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

23 
val presimplified_consts : Proof.context > string list 
42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

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

39904  28 
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

29 
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

30 
val extensionalize_theorem : Proof.context > thm > thm 
24300  31 
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

32 
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

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

36 
val depth_prolog_tac: thm list > tactic 

37 
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

38 
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

39 
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

40 
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

41 
> int > tactic 
32262  42 
val best_meson_tac: (thm > int) > Proof.context > int > tactic 
43 
val safe_best_meson_tac: Proof.context > int > tactic 

44 
val depth_meson_tac: Proof.context > int > tactic 

24300  45 
val prolog_step_tac': thm list > int > tactic 
46 
val iter_deepen_prolog_tac: thm list > tactic 

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

32262  50 
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

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

52 

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

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

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

55 

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

56 
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

57 

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

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

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

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

61 
Attrib.setup_config_bool @{binding meson_unfold_set_consts} (K false) 
017e5dac8642
added unfold set constant functionality to Meson/Metis  disabled by default for now
blanchet
parents:
42616
diff
changeset

62 

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

63 
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

64 

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

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

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

67 

31454  68 
val disj_forward = @{thm disj_forward}; 
69 
val disj_forward2 = @{thm disj_forward2}; 

70 
val make_pos_rule = @{thm make_pos_rule}; 

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

72 
val make_pos_goal = @{thm make_pos_goal}; 

73 
val make_neg_rule = @{thm make_neg_rule}; 

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

75 
val make_neg_goal = @{thm make_neg_goal}; 

76 
val conj_forward = @{thm conj_forward}; 

77 
val all_forward = @{thm all_forward}; 

78 
val ex_forward = @{thm ex_forward}; 

79 

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

80 
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

81 
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

82 
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

83 
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

84 
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

85 
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

86 
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

87 
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

88 
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

89 
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

90 
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

91 
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

92 
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

93 
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

94 
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

95 
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

96 
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

97 
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

98 

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

99 

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

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

101 

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

102 

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

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

104 

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

105 
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

106 

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

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

108 
fun first_order_resolve thA thB = 
32262  109 
(case 
110 
try (fn () => 

111 
let val thy = theory_of_thm thA 

112 
val tmA = concl_of thA 

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

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

114 
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

115 
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

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

119 
SOME th => th 

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

120 
 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

121 

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

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

123 
"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

124 
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

125 

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

126 
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

127 
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

128 
 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

129 
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

130 
 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

131 

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

132 
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

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

134 
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

135 
 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

136 
 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

137 
 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

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

139 
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

140 
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

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

142 
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

143 
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

144 
 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

145 
 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

146 
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

147 
 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

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

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

150 
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

151 
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

152 
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

153 
? 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

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

155 
 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

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

157 
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

158 

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

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

160 
fun rename_bound_vars_RS th rl = 
39904  161 
let 
162 
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

163 
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

164 
val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl 
39904  165 
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

166 
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

167 

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

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

170 
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

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

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

173 
in tryall rls end; 
24300  174 

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

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

176 
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

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

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

180 
let fun forward_tacf [prem] = rtac (nf prem) 1 
24300  181 
 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

182 
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

183 
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: 
32262  184 
Display.string_of_thm ctxt st :: 
185 
"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

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

187 
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

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

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

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

191 

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

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

193 
fun has_conns bs = 
39328  194 
let fun has (Const _) = false 
38557  195 
 has (Const(@{const_name Trueprop},_) $ p) = has p 
196 
 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

197 
 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

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

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

202 
in has end; 
24300  203 

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

204 

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

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

206 

38557  207 
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

208 
 literals (Const(@{const_name HOL.disj},_) $ P $ Q) = literals P @ literals Q 
38557  209 
 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

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

211 

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

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

213 
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

214 

18389  215 

216 
(*** Tautology Checking ***) 

217 

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

218 
fun signed_lits_aux (Const (@{const_name HOL.disj}, _) $ P $ Q) (poslits, neglits) = 
18389  219 
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) 
38557  220 
 signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits) 
18389  221 
 signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); 
24300  222 

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

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

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

226 
fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u 
38557  227 
 taut_poslit (Const(@{const_name True},_)) = true 
18389  228 
 taut_poslit _ = false; 
229 

230 
fun is_taut th = 

231 
let val (poslits,neglits) = signed_lits th 

232 
in exists taut_poslit poslits 

233 
orelse 

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

238 

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

240 

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

242 
injectivity equivalences*) 

24300  243 

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

244 
val not_refl_disj_D = @{thm not_refl_disj_D}; 
18389  245 

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

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

249 
 eliminable _ = false; 

250 

18389  251 
fun refl_clause_aux 0 th = th 
252 
 refl_clause_aux n th = 

253 
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

254 
(Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) => 
18389  255 
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

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

259 
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

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

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

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

265 
 notequal_lits_count (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ _ $ _)) = 1 
18389  266 
 notequal_lits_count _ = 0; 
267 

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

24300  269 
fun refl_clause th = 
18389  270 
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th)) 
19894  271 
in zero_var_indexes (refl_clause_aux neqs th) end 
24300  272 
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) 
18389  273 

274 

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

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

276 

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

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

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

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

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

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

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

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

285 

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

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

287 
rls (initially []) accumulates assumptions of the form P==>False*) 
32262  288 
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

289 
handle THM _ => tryres(th,rls) 
39328  290 
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

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

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

293 

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

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

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

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

299 

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

300 

18389  301 
(*** The basic CNF transformation ***) 
302 

39328  303 
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

304 
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

305 
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

306 
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

307 

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

308 
(*Estimate the number of clauses in order to detect infeasible theorems*) 
38557  309 
fun signed_nclauses b (Const(@{const_name Trueprop},_) $ t) = signed_nclauses b t 
310 
 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

311 
 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

312 
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

313 
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

314 
 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

315 
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

316 
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

317 
 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

318 
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

319 
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

320 
 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

321 
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

322 
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

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

324 
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

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

326 
else 1 
38557  327 
 signed_nclauses b (Const(@{const_name Ex}, _) $ Abs (_,_,t)) = signed_nclauses b t 
328 
 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

329 
 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

330 
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

331 

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

332 
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

333 
let val max_cl = Config.get ctxt max_clauses in 
39328  334 
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

335 
end 
19894  336 

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

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

338 
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

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

340 
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

341 
val spec_varT = #T (Thm.rep_cterm spec_var); 
38557  342 
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

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

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

345 
let 
42361  346 
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

347 
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

348 
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

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

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

351 

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

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

353 
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

354 
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

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

356 
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

357 

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

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

359 
and "Pure.term"? *) 
38557  360 
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

361 

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

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

363 
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

364 
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

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

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

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

368 

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

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

370 
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

371 
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

372 
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

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

374 
fun cnf_aux (th,ths) = 
24300  375 
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

376 
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

377 
then nodups ctxt0 th :: ths (*no work to do, terminate*) 
24300  378 
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

379 
Const (@{const_name HOL.conj}, _) => (*conjunction*) 
24300  380 
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) 
38557  381 
 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

382 
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

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

386 
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

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

390 
let val tac = 

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

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

392 
(fn st' => st' > Misc_Legacy.METAHYPS (resop cnf_nil) 1) 
24300  393 
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

394 
 _ => nodups ctxt0 th :: ths (*no work to do*) 
19154  395 
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

396 
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

397 
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

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

399 
"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

400 
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

401 
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

402 
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

403 
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

404 
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

405 

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

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

407 
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

408 

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

409 

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

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

411 

38557  412 
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

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

414 
 is_left _ = false; 
24300  415 

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

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

418 
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

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

420 

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

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

422 
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

423 

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

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

425 
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

426 

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

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

428 
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

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

430 
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

431 

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

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

433 
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

434 

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

436 

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

437 
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

438 
 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

439 
 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

440 

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

441 
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

442 
 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

443 
 has_fun _ = false 
24300  444 

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

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

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

448 
[@{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

449 
@{const_name HOL.implies}, @{const_name Not}, 
38557  450 
@{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}]; 
15613  451 

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

453 
of any argument contains bool.*) 
24300  454 
val has_bool_arg_const = 
15613  455 
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

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

457 

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

461 
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

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

463 
 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

464 

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

467 
fun is_fol_term thy t = 
42833  468 
Term.is_first_order [@{const_name all}, @{const_name All}, 
469 
@{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

470 
not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T 
42833  471 
 _ => 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

472 
has_bool_arg_const t orelse 
24300  473 
exists_Const (higher_inst_const thy) t orelse 
474 
has_meta_conn t); 

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

475 

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

476 
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

477 

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

478 
fun ok4horn (Const (@{const_name Trueprop},_) $ (Const (@{const_name HOL.disj}, _) $ t $ _)) = rigid t 
38557  479 
 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

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

481 

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

482 
(*Create a metalevel Horn clause*) 
24300  483 
fun make_horn crules th = 
484 
if ok4horn (concl_of th) 

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

485 
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

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

487 

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

33339  490 
fun add_contras crules th hcs = 
39328  491 
let fun rots (0,_) = hcs 
24300  492 
 rots (k,th) = zero_var_indexes (make_horn crules th) :: 
493 
rots(k1, assoc_right (th RS disj_comm)) 

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

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

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

498 

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

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

500 
fun name_thms label = 
33339  501 
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

502 
(k1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) 
33339  503 
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

504 

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

506 
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

507 

33317  508 
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

509 

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

510 

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

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

512 

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

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

518 

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

519 
(*The stringtree detects repeated assumptions.*) 
33245  520 
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

521 

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

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

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

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

525 
 has_reps [t,u] = (t aconv u) 
33245  526 
 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

527 

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

528 
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) 
18508  529 
fun TRYING_eq_assume_tac 0 st = Seq.single st 
530 
 TRYING_eq_assume_tac i st = 

31945  531 
TRYING_eq_assume_tac (i1) (Thm.eq_assumption i st) 
18508  532 
handle THM _ => TRYING_eq_assume_tac (i1) st; 
533 

534 
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

535 

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

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

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

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

539 
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

540 
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

541 

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

542 

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

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

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

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

547 

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

548 
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) 
33339  549 
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

550 

33339  551 
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

552 

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

553 

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

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

555 
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, 
9869  556 
not_impD, not_iffD, not_allD, not_exD, not_notD]; 
15581  557 

38557  558 
fun ok4nnf (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ t)) = rigid t 
559 
 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

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

561 

32262  562 
fun make_nnf1 ctxt th = 
24300  563 
if ok4nnf (concl_of th) 
32262  564 
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

565 
handle THM ("tryres", _, _) => 
32262  566 
forward_res ctxt (make_nnf1 ctxt) 
9869  567 
(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

568 
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

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

570 

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

571 
fun unfold_set_const_simps ctxt = 
45981
4c629115e3ab
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
haftmann
parents:
45740
diff
changeset

572 
if Config.get ctxt unfold_set_consts then [] 
42739
017e5dac8642
added unfold set constant functionality to Meson/Metis  disabled by default for now
blanchet
parents:
42616
diff
changeset

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

574 

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

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

581 
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

582 

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

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

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

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

587 
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

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

589 

a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

590 
fun presimplified_consts ctxt = 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

591 
[@{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

592 
@{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

593 
@{const_name Let}] 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

594 
> Config.get ctxt unfold_set_consts 
a1a48c69d623
don't needlessly presimplify  makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset

595 
? append ([@{const_name Collect}, @{const_name Set.member}]) 
15872  596 

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

597 
fun presimplify ctxt = 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

598 
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

599 
#> simplify nnf_ss 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

600 
(* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and 
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

601 
when "metis_unfold_set_consts" becomes the only mode of operation. *) 
43821
048619bb1dc3
always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents:
43264
diff
changeset

602 
#> Raw_Simplifier.rewrite_rule 
048619bb1dc3
always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents:
43264
diff
changeset

603 
(@{thm Let_def_raw} :: unfold_set_const_simps ctxt) 
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

604 

32262  605 
fun make_nnf ctxt th = case prems_of th of 
42750
c8b1d9ee3758
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
blanchet
parents:
42747
diff
changeset

606 
[] => th > presimplify ctxt > make_nnf1 ctxt 
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset

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

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

611 

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

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

613 
clauses that arise from a subgoal. *) 
39950  614 
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

615 
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

616 
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

617 
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

618 
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

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

620 
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

621 
[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

622 
> 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

623 
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

624 
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

625 
> 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

626 
> 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

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

628 
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

629 
> 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

630 
in aux o make_nnf ctxt end 
29684  631 

39950  632 
fun skolemize ctxt = 
42361  633 
let val thy = Proof_Context.theory_of ctxt in 
39950  634 
skolemize_with_choice_theorems ctxt (choice_theorems thy) 
635 
end 

39904  636 

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

639 
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

640 
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

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

644 
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

645 
 _ $ _ => 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

646 
 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

647 
 _ => 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

648 

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

649 
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

650 

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

651 
(* "RS" can fail if "unify_search_bound" is too small. *) 
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

652 
fun try_skolemize_etc ctxt = 
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

653 
Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt) 
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

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

655 
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

656 
compatibility. *) 
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

657 
#> (fn th => insert Thm.eq_thm_prop (extensionalize_theorem ctxt th) [th]) 
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

658 
#> map_filter (fn th => try (skolemize ctxt) th 
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

659 
> tap (fn NONE => 
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

660 
trace_msg ctxt (fn () => 
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

661 
"Failed to skolemize " ^ 
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

662 
Display.string_of_thm ctxt th) 
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

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

664 

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

665 
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

666 
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

667 
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

668 
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

669 

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

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

671 
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

672 
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

673 
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

674 

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

677 
name_thms "Horn#" 
33339  678 
(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

679 

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

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

681 
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

682 

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

684 
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

685 

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

687 
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

688 

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

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

690 
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

691 

32262  692 
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

693 
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

694 

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

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

696 
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

697 
fun MESON preskolem_tac mkcl cltac ctxt i st = 
16588  698 
SELECT_GOAL 
35625  699 
(EVERY [Object_Logic.atomize_prems_tac 1, 
23552  700 
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

701 
preskolem_tac, 
32283  702 
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

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

706 

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

707 

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

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

709 

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

711 
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

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

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

714 
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

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

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

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

718 

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

719 
(*First, breaks the goal into independent units*) 
32262  720 
fun safe_best_meson_tac ctxt = 
42793  721 
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

722 

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

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

724 

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

725 
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

726 
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

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

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

729 

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

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

731 

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

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

733 
having only one eq_assume_tac speeds it up!*) 
9869  734 
fun prolog_step_tac' horns = 
39328  735 
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

736 
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

737 
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

738 
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

739 
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

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

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

742 

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

744 
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

745 

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

746 
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

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

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

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

750 
 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

751 
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

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

753 
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

754 
cat_lines ("meson method called:" :: 
32262  755 
map (Display.string_of_thm ctxt) (cls @ ths) @ 
756 
["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

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

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

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

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

761 

32262  762 
fun meson_tac ctxt ths = 
42793  763 
SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); 
9869  764 

765 

14813  766 
(**** Code to support ordinary resolution, rather than Model Elimination ****) 
14744  767 

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

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

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

773 
prevents a double negation.*) 

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

24300  777 
fun negated_asm_of_head th = 
14744  778 
th RS notEfalse handle THM _ => th RS notEfalse'; 
779 

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

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

781 
fun make_meta_clause th = 
33832  782 
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

783 
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

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

785 
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

786 
end; 
24300  787 

14744  788 
fun make_meta_clauses ths = 
789 
name_thms "MClause#" 

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

790 
(distinct Thm.eq_thm_prop (map make_meta_clause ths)); 
14744  791 

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

792 
end; 