author | wenzelm |
Tue, 21 Sep 2021 20:56:23 +0200 | |
changeset 74346 | 55007a70bd96 |
parent 74282 | c2ee8d993d6a |
child 74375 | ba880f3a4e52 |
permissions | -rw-r--r-- |
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 |
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
11 |
type simp_options = {if_simps : bool, let_simps : bool} |
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
12 |
val simp_options_all_true : simp_options |
39979
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39953
diff
changeset
|
13 |
val trace : bool Config.T |
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39953
diff
changeset
|
14 |
val max_clauses : int Config.T |
60362 | 15 |
val first_order_resolve : Proof.context -> 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 |
59165 | 18 |
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context |
24300 | 19 |
val finish_cnf: thm list -> thm list |
46093 | 20 |
val presimplified_consts : string list |
74051 | 21 |
val presimplify: simp_options -> Proof.context -> thm -> thm |
22 |
val make_nnf: simp_options -> Proof.context -> thm -> thm |
|
39950 | 23 |
val choice_theorems : theory -> thm list |
74051 | 24 |
val skolemize_with_choice_theorems : simp_options -> Proof.context -> thm list -> thm -> thm |
25 |
val skolemize : simp_options -> Proof.context -> thm -> thm |
|
59632 | 26 |
val cong_extensionalize_thm : Proof.context -> thm -> thm |
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
27 |
val abs_extensionalize_conv : Proof.context -> conv |
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
28 |
val abs_extensionalize_thm : Proof.context -> thm -> thm |
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
|
29 |
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
|
30 |
val make_clauses: Proof.context -> thm list -> thm list |
24300 | 31 |
val make_horns: thm list -> thm list |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
32 |
val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
33 |
val depth_prolog_tac: Proof.context -> thm list -> tactic |
24300 | 34 |
val gocls: thm list -> thm list |
74051 | 35 |
val skolemize_prems_tac : simp_options -> 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
|
36 |
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
|
37 |
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
|
38 |
-> int -> tactic |
32262 | 39 |
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic |
40 |
val safe_best_meson_tac: Proof.context -> int -> tactic |
|
41 |
val depth_meson_tac: Proof.context -> int -> tactic |
|
58957 | 42 |
val prolog_step_tac': Proof.context -> thm list -> int -> tactic |
43 |
val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic |
|
32262 | 44 |
val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic |
60358 | 45 |
val make_meta_clause: Proof.context -> thm -> thm |
46 |
val make_meta_clauses: Proof.context -> thm list -> thm list |
|
32262 | 47 |
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
|
48 |
end |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
49 |
|
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
50 |
structure Meson : MESON = |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
51 |
struct |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
52 |
|
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
53 |
type simp_options = {if_simps : bool, let_simps : bool} |
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
54 |
val simp_options_all_true = {if_simps = true, let_simps = true} |
74051 | 55 |
|
67149 | 56 |
val trace = Attrib.setup_config_bool \<^binding>\<open>meson_trace\<close> (K false) |
39979
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39953
diff
changeset
|
57 |
|
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39953
diff
changeset
|
58 |
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () |
32955 | 59 |
|
67149 | 60 |
val max_clauses = Attrib.setup_config_int \<^binding>\<open>meson_max_clauses\<close> (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
|
61 |
|
38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
62 |
(*No known example (on 1-5-2007) needs even thirty*) |
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
63 |
val iter_deepen_limit = 50; |
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
64 |
|
31454 | 65 |
val disj_forward = @{thm disj_forward}; |
66 |
val disj_forward2 = @{thm disj_forward2}; |
|
67 |
val make_pos_rule = @{thm make_pos_rule}; |
|
68 |
val make_pos_rule' = @{thm make_pos_rule'}; |
|
69 |
val make_pos_goal = @{thm make_pos_goal}; |
|
70 |
val make_neg_rule = @{thm make_neg_rule}; |
|
71 |
val make_neg_rule' = @{thm make_neg_rule'}; |
|
72 |
val make_neg_goal = @{thm make_neg_goal}; |
|
73 |
val conj_forward = @{thm conj_forward}; |
|
74 |
val all_forward = @{thm all_forward}; |
|
75 |
val ex_forward = @{thm ex_forward}; |
|
76 |
||
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset
|
77 |
val not_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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
96 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
97 |
(**** Operators for forward proof ****) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
98 |
|
20417
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
99 |
|
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
100 |
(** First-order Resolution **) |
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
101 |
|
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
102 |
(*FIXME: currently does not "rename variables apart"*) |
60362 | 103 |
fun first_order_resolve ctxt thA thB = |
32262 | 104 |
(case |
73551 | 105 |
\<^try>\<open> |
60362 | 106 |
let val thy = Proof_Context.theory_of ctxt |
59582 | 107 |
val tmA = Thm.concl_of thA |
74346 | 108 |
val \<^Const_>\<open>Pure.imp for tmB _\<close> = Thm.prop_of thB |
37398
e194213451c9
beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset
|
109 |
val tenv = |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset
|
110 |
Pattern.first_order_match thy (tmB, tmA) |
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset
|
111 |
(Vartab.empty, Vartab.empty) |> snd |
60781 | 112 |
val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv []; |
73551 | 113 |
in thA RS (infer_instantiate ctxt insts thB) end\<close> of |
32262 | 114 |
SOME th => th |
37398
e194213451c9
beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset
|
115 |
| NONE => raise THM ("first_order_resolve", 0, [thA, thB])) |
18175
7858b777569a
new version of "tryres" allowing multiple unifiers (apparently needed for
paulson
parents:
18141
diff
changeset
|
116 |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
117 |
(* Hack to make it less likely that we lose our precious bound variable names in |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
118 |
"rename_bound_vars_RS" below, because of a clash. *) |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
119 |
val protect_prefix = "Meson_xyzzy" |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
120 |
|
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
121 |
fun protect_bound_var_names (t $ u) = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
122 |
protect_bound_var_names t $ protect_bound_var_names u |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
123 |
| protect_bound_var_names (Abs (s, T, t')) = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
124 |
Abs (protect_prefix ^ s, T, protect_bound_var_names t') |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
125 |
| protect_bound_var_names t = t |
39930
61aa00205a88
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents:
39904
diff
changeset
|
126 |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
127 |
fun fix_bound_var_names old_t new_t = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
128 |
let |
67149 | 129 |
fun quant_of \<^const_name>\<open>All\<close> = SOME true |
130 |
| quant_of \<^const_name>\<open>Ball\<close> = SOME true |
|
131 |
| quant_of \<^const_name>\<open>Ex\<close> = SOME false |
|
132 |
| quant_of \<^const_name>\<open>Bex\<close> = SOME false |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
133 |
| quant_of _ = NONE |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
134 |
val flip_quant = Option.map not |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
135 |
fun some_eq (SOME x) (SOME y) = x = y |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
136 |
| some_eq _ _ = false |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
137 |
fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
138 |
add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s |
74346 | 139 |
| add_names quant \<^Const_>\<open>Not for t\<close> = add_names (flip_quant quant) t |
140 |
| add_names quant \<^Const_>\<open>implies for t1 t2\<close> = |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
141 |
add_names (flip_quant quant) t1 #> add_names quant t2 |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
142 |
| add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2] |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
143 |
| add_names _ _ = I |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
144 |
fun lost_names quant = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
145 |
subtract (op =) (add_names quant new_t []) (add_names quant old_t []) |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
146 |
fun aux ((t1 as Const (quant_s, _)) $ (Abs (s, T, t'))) = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
147 |
t1 $ Abs (s |> String.isPrefix protect_prefix s |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
148 |
? perhaps (try (fn _ => hd (lost_names (quant_of quant_s)))), |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
149 |
T, aux t') |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
150 |
| aux (t1 $ t2) = aux t1 $ aux t2 |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
151 |
| aux t = t |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
152 |
in aux new_t end |
39930
61aa00205a88
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
blanchet
parents:
39904
diff
changeset
|
153 |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
154 |
(* Forward proof while preserving bound variables names *) |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
155 |
fun rename_bound_vars_RS th rl = |
39904 | 156 |
let |
59582 | 157 |
val t = Thm.concl_of th |
158 |
val r = Thm.concl_of rl |
|
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
159 |
val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl |
59582 | 160 |
val t' = Thm.concl_of th' |
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
161 |
in Thm.rename_boundvars t' (fix_bound_var_names t t') th' end |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
162 |
|
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
163 |
(*raises exception if no rules apply*) |
24300 | 164 |
fun tryres (th, rls) = |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset
|
165 |
let fun tryall [] = raise THM("tryres", 0, th::rls) |
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
166 |
| tryall (rl::rls) = |
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
167 |
(rename_bound_vars_RS th rl handle THM _ => tryall rls) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18024
diff
changeset
|
168 |
in tryall rls end; |
24300 | 169 |
|
58839 | 170 |
(* Special version of "resolve_tac" that works around an explosion in the unifier. |
50702 | 171 |
If the goal has the form "?P c", the danger is that resolving it against a |
172 |
property of the form "... c ... c ... c ..." will lead to a huge unification |
|
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
173 |
problem, due to the (spurious) choices between projection and imitation. The |
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
174 |
workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
175 |
fun quant_resolve_tac ctxt th i st = |
59582 | 176 |
case (Thm.concl_of st, Thm.prop_of th) of |
74346 | 177 |
(\<^Const_>\<open>Trueprop for \<open>Var _ $ (c as Free _)\<close>\<close>, \<^Const_>\<open>Trueprop for _\<close>) => |
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
178 |
let |
59632 | 179 |
val cc = Thm.cterm_of ctxt c |
59582 | 180 |
val ct = Thm.dest_arg (Thm.cprop_of th) |
60801 | 181 |
in resolve_tac ctxt [th] i (Thm.instantiate' [] [SOME (Thm.lambda cc ct)] st) end |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
182 |
| _ => resolve_tac ctxt [th] i st |
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
183 |
|
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset
|
184 |
(*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
|
185 |
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
|
186 |
"[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q" |
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset
|
187 |
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*) |
32262 | 188 |
fun forward_res ctxt nf st = |
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
189 |
let |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
190 |
fun tacf [prem] = quant_resolve_tac ctxt (nf prem) 1 |
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
191 |
| tacf prems = |
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
192 |
error (cat_lines |
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
193 |
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" :: |
61268 | 194 |
Thm.string_of_thm ctxt st :: |
195 |
"Premises:" :: map (Thm.string_of_thm ctxt) prems)) |
|
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset
|
196 |
in |
59165 | 197 |
case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of |
50695
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
198 |
SOME (th, _) => th |
cace30ea5a2c
avoid explosion in higher-order unification algorithm
blanchet
parents:
47956
diff
changeset
|
199 |
| NONE => raise THM ("forward_res", 0, [st]) |
21050
d0447a511edb
More robust error handling in make_nnf and forward_res
paulson
parents:
21046
diff
changeset
|
200 |
end; |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
201 |
|
20134
73cb53843190
has_consts renamed to has_conn, now actually parses the first-order formula
paulson
parents:
20119
diff
changeset
|
202 |
(*Are any of the logical connectives in "bs" present in the term?*) |
73cb53843190
has_consts renamed to has_conn, now actually parses the first-order formula
paulson
parents:
20119
diff
changeset
|
203 |
fun has_conns bs = |
39328 | 204 |
let fun has (Const _) = false |
74346 | 205 |
| has \<^Const_>\<open>Trueprop for p\<close> = has p |
206 |
| has \<^Const_>\<open>Not for p\<close> = has p |
|
207 |
| has \<^Const_>\<open>disj for p q\<close> = member (op =) bs \<^const_name>\<open>disj\<close> orelse has p orelse has q |
|
208 |
| has \<^Const_>\<open>conj for p q\<close> = member (op =) bs \<^const_name>\<open>conj\<close> orelse has p orelse has q |
|
209 |
| has \<^Const_>\<open>All _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>All\<close> orelse has p |
|
210 |
| has \<^Const_>\<open>Ex _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>Ex\<close> orelse has p |
|
24300 | 211 |
| has _ = false |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
212 |
in has end; |
24300 | 213 |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
214 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
215 |
(**** Clause handling ****) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
216 |
|
74346 | 217 |
fun literals \<^Const_>\<open>Trueprop for P\<close> = literals P |
218 |
| literals \<^Const_>\<open>disj for P Q\<close> = literals P @ literals Q |
|
219 |
| literals \<^Const_>\<open>Not for P\<close> = [(false,P)] |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
220 |
| literals P = [(true,P)]; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
221 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
222 |
(*number of literals in a term*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
223 |
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
|
224 |
|
18389 | 225 |
|
226 |
(*** Tautology Checking ***) |
|
227 |
||
74346 | 228 |
fun signed_lits_aux \<^Const_>\<open>disj for P Q\<close> (poslits, neglits) = |
18389 | 229 |
signed_lits_aux Q (signed_lits_aux P (poslits, neglits)) |
74346 | 230 |
| signed_lits_aux \<^Const_>\<open>Not for P\<close> (poslits, neglits) = (poslits, P::neglits) |
18389 | 231 |
| signed_lits_aux P (poslits, neglits) = (P::poslits, neglits); |
24300 | 232 |
|
59582 | 233 |
fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (Thm.concl_of th)) ([],[]); |
18389 | 234 |
|
235 |
(*Literals like X=X are tautologous*) |
|
74346 | 236 |
fun taut_poslit \<^Const_>\<open>HOL.eq _ for t u\<close> = t aconv u |
237 |
| taut_poslit \<^Const_>\<open>True\<close> = true |
|
18389 | 238 |
| taut_poslit _ = false; |
239 |
||
240 |
fun is_taut th = |
|
241 |
let val (poslits,neglits) = signed_lits th |
|
242 |
in exists taut_poslit poslits |
|
243 |
orelse |
|
67149 | 244 |
exists (member (op aconv) neglits) (\<^term>\<open>False\<close> :: poslits) |
19894 | 245 |
end |
24300 | 246 |
handle TERM _ => false; (*probably dest_Trueprop on a weird theorem*) |
18389 | 247 |
|
248 |
||
249 |
(*** To remove trivial negated equality literals from clauses ***) |
|
250 |
||
251 |
(*They are typically functional reflexivity axioms and are the converses of |
|
252 |
injectivity equivalences*) |
|
24300 | 253 |
|
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset
|
254 |
val not_refl_disj_D = @{thm not_refl_disj_D}; |
18389 | 255 |
|
20119 | 256 |
(*Is either term a Var that does not properly occur in the other term?*) |
257 |
fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) |
|
258 |
| eliminable (u, t as Var _) = t aconv u orelse not (Logic.occs(t,u)) |
|
259 |
| eliminable _ = false; |
|
260 |
||
18389 | 261 |
fun refl_clause_aux 0 th = th |
262 |
| refl_clause_aux n th = |
|
59582 | 263 |
case HOLogic.dest_Trueprop (Thm.concl_of th) of |
74346 | 264 |
\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> => |
18389 | 265 |
refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) |
74346 | 266 |
| \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> => |
24300 | 267 |
if eliminable(t,u) |
268 |
then refl_clause_aux (n-1) (th RS not_refl_disj_D) (*Var inequation: delete*) |
|
269 |
else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) |
|
74346 | 270 |
| \<^Const>\<open>disj for _ _\<close> => refl_clause_aux n (th RS disj_comm) |
24300 | 271 |
| _ => (*not a disjunction*) th; |
18389 | 272 |
|
74346 | 273 |
fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q |
274 |
| notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1 |
|
18389 | 275 |
| notequal_lits_count _ = 0; |
276 |
||
277 |
(*Simplify a clause by applying reflexivity to its negated equality literals*) |
|
24300 | 278 |
fun refl_clause th = |
59582 | 279 |
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (Thm.concl_of th)) |
19894 | 280 |
in zero_var_indexes (refl_clause_aux neqs th) end |
24300 | 281 |
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*) |
18389 | 282 |
|
283 |
||
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
284 |
(*** Removal of duplicate literals ***) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
285 |
|
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
286 |
(*Forward proof, passing extra assumptions as theorems to the tactic*) |
59165 | 287 |
fun forward_res2 ctxt nf hyps st = |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
288 |
case Seq.pull |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
289 |
(REPEAT |
59165 | 290 |
(Misc_Legacy.METAHYPS ctxt |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
291 |
(fn major::minors => resolve_tac ctxt [nf (minors @ hyps) major] 1) 1) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
292 |
st) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
293 |
of SOME(th,_) => th |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
294 |
| NONE => raise THM("forward_res2", 0, [st]); |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
295 |
|
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
296 |
(*Remove duplicates in P|Q by assuming ~P in Q |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
297 |
rls (initially []) accumulates assumptions of the form P==>False*) |
32262 | 298 |
fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
299 |
handle THM _ => tryres(th,rls) |
59165 | 300 |
handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2), |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
301 |
[disj_FalseD1, disj_FalseD2, asm_rl]) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
302 |
handle THM _ => th; |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
303 |
|
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
304 |
(*Remove duplicate literals, if there are any*) |
32262 | 305 |
fun nodups ctxt th = |
59582 | 306 |
if has_duplicates (op =) (literals (Thm.prop_of th)) |
32262 | 307 |
then nodups_aux ctxt [] th |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
308 |
else th; |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
309 |
|
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
310 |
|
18389 | 311 |
(*** The basic CNF transformation ***) |
312 |
||
39328 | 313 |
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
|
314 |
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
|
315 |
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
|
316 |
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
|
317 |
|
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
|
318 |
(*Estimate the number of clauses in order to detect infeasible theorems*) |
74346 | 319 |
fun signed_nclauses b \<^Const_>\<open>Trueprop for t\<close> = signed_nclauses b t |
320 |
| signed_nclauses b \<^Const_>\<open>Not for t\<close> = signed_nclauses (not b) t |
|
321 |
| signed_nclauses b \<^Const_>\<open>conj for t u\<close> = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
322 |
if b then sum (signed_nclauses b t) (signed_nclauses b u) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
323 |
else prod (signed_nclauses b t) (signed_nclauses b u) |
74346 | 324 |
| signed_nclauses b \<^Const_>\<open>disj for t u\<close> = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
325 |
if b then prod (signed_nclauses b t) (signed_nclauses b u) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
326 |
else sum (signed_nclauses b t) (signed_nclauses b u) |
74346 | 327 |
| signed_nclauses b \<^Const_>\<open>implies for t u\<close> = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
328 |
if b then prod (signed_nclauses (not b) t) (signed_nclauses b u) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
329 |
else sum (signed_nclauses (not b) t) (signed_nclauses b u) |
74346 | 330 |
| signed_nclauses b \<^Const_>\<open>HOL.eq \<open>T\<close> for t u\<close> = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
331 |
if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
332 |
if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
333 |
(prod (signed_nclauses (not b) u) (signed_nclauses b t)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
334 |
else sum (prod (signed_nclauses b t) (signed_nclauses b u)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
335 |
(prod (signed_nclauses (not b) t) (signed_nclauses (not b) u)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32955
diff
changeset
|
336 |
else 1 |
74346 | 337 |
| signed_nclauses b \<^Const_>\<open>Ex _ for \<open>Abs (_,_,t)\<close>\<close> = signed_nclauses b t |
338 |
| signed_nclauses b \<^Const_>\<open>All _ for \<open>Abs (_,_,t)\<close>\<close> = 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
|
339 |
| 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
|
340 |
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
|
341 |
|
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
|
342 |
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
|
343 |
let val max_cl = Config.get ctxt max_clauses in |
39328 | 344 |
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
|
345 |
end |
19894 | 346 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
347 |
(*Replaces universally quantified variables by FREE variables -- because |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
348 |
assumptions may not contain scheme variables. Later, generalize using Variable.export. *) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
349 |
local |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60362
diff
changeset
|
350 |
val spec_var = |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60362
diff
changeset
|
351 |
Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec)))) |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60362
diff
changeset
|
352 |
|> Thm.term_of |> dest_Var; |
74346 | 353 |
fun name_of \<^Const_>\<open>All _ for \<open>Abs(x, _, _)\<close>\<close> = x | name_of _ = Name.uu; |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
354 |
in |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
355 |
fun freeze_spec th ctxt = |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
356 |
let |
59582 | 357 |
val ([x], ctxt') = |
358 |
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt; |
|
59617 | 359 |
val spec' = spec |
74282 | 360 |
|> Thm.instantiate |
361 |
(TVars.empty, Vars.make [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]); |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
362 |
in (th RS spec', ctxt') end |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
363 |
end; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
364 |
|
60362 | 365 |
fun apply_skolem_theorem ctxt (th, rls) = |
37398
e194213451c9
beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset
|
366 |
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
|
367 |
fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls) |
60362 | 368 |
| tryall (rl :: rls) = first_order_resolve ctxt th rl handle THM _ => tryall rls |
37398
e194213451c9
beta-eta-contract, to respect "first_order_match"'s specification;
blanchet
parents:
37388
diff
changeset
|
369 |
in tryall rls end |
22515
f4061faa5fda
"generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
paulson
parents:
22381
diff
changeset
|
370 |
|
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37398
diff
changeset
|
371 |
(* 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
|
372 |
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
|
373 |
Eliminates existential quantifiers using Skolemization theorems. *) |
59165 | 374 |
fun cnf old_skolem_ths ctxt (th, ths) = |
375 |
let val ctxt_ref = Unsynchronized.ref ctxt (* FIXME ??? *) |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
376 |
fun cnf_aux (th,ths) = |
59582 | 377 |
if not (can HOLogic.dest_Trueprop (Thm.prop_of th)) then ths (*meta-level: ignore*) |
67149 | 378 |
else if not (has_conns [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>, \<^const_name>\<open>HOL.conj\<close>] (Thm.prop_of th)) |
59165 | 379 |
then nodups ctxt th :: ths (*no work to do, terminate*) |
59582 | 380 |
else case head_of (HOLogic.dest_Trueprop (Thm.concl_of th)) of |
74346 | 381 |
\<^Const_>\<open>conj\<close> => (*conjunction*) |
24300 | 382 |
cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths)) |
74346 | 383 |
| \<^Const_>\<open>All _\<close> => (*universal quantifier*) |
59165 | 384 |
let val (th', ctxt') = freeze_spec th (! ctxt_ref) |
385 |
in ctxt_ref := ctxt'; cnf_aux (th', ths) end |
|
74346 | 386 |
| \<^Const_>\<open>Ex _\<close> => |
24300 | 387 |
(*existential quantifier: Insert Skolem functions*) |
60362 | 388 |
cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths) |
74346 | 389 |
| \<^Const_>\<open>disj\<close> => |
24300 | 390 |
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using |
391 |
all combinations of converting P, Q to CNF.*) |
|
59171 | 392 |
(*There is one assumption, which gets bound to prem and then normalized via |
393 |
cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean |
|
394 |
variable created by resolution with disj_forward. Since (cnf_nil prem) |
|
395 |
returns a LIST of theorems, we can backtrack to get all combinations.*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
396 |
let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac ctxt (cnf_nil prem) 1) 1 |
59171 | 397 |
in Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths end |
59165 | 398 |
| _ => nodups ctxt th :: ths (*no work to do*) |
399 |
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
|
400 |
val cls = |
59582 | 401 |
if has_too_many_clauses ctxt (Thm.concl_of th) then |
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
|
402 |
(trace_msg ctxt (fn () => |
61268 | 403 |
"cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths) |
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
|
404 |
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
|
405 |
cnf_aux (th, ths) |
59165 | 406 |
in (cls, !ctxt_ref) end |
407 |
||
408 |
fun make_cnf old_skolem_ths th ctxt = |
|
409 |
cnf old_skolem_ths ctxt (th, []) |
|
20417
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
410 |
|
c611b1412056
better skolemization, using first-order resolution rather than hoping for the right result
paulson
parents:
20361
diff
changeset
|
411 |
(*Generalization, removal of redundant equalities, removal of tautologies.*) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24827
diff
changeset
|
412 |
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
|
413 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
414 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
415 |
(**** Generation of contrapositives ****) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
416 |
|
74346 | 417 |
fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true |
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
418 |
| is_left _ = false; |
24300 | 419 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
420 |
(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) |
24300 | 421 |
fun assoc_right th = |
59582 | 422 |
if is_left (Thm.prop_of th) then assoc_right (th RS disj_assoc) |
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
423 |
else th; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
424 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
425 |
(*Must check for negative literal first!*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
426 |
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
|
427 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
428 |
(*For ordinary resolution. *) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
429 |
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
|
430 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
431 |
(*Create a goal or support clause, conclusing False*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
432 |
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
|
433 |
make_goal (tryres(th, clause_rules)) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
434 |
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
|
435 |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
436 |
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
|
437 |
|
74346 | 438 |
fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t |
439 |
| ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
440 |
| ok4horn _ = false; |
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
441 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
442 |
(*Create a meta-level Horn clause*) |
24300 | 443 |
fun make_horn crules th = |
59582 | 444 |
if ok4horn (Thm.concl_of th) |
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
445 |
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
|
446 |
else th; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
447 |
|
16563 | 448 |
(*Generate Horn clauses for all contrapositives of a clause. The input, th, |
449 |
is a HOL disjunction.*) |
|
33339 | 450 |
fun add_contras crules th hcs = |
39328 | 451 |
let fun rots (0,_) = hcs |
24300 | 452 |
| rots (k,th) = zero_var_indexes (make_horn crules th) :: |
453 |
rots(k-1, assoc_right (th RS disj_comm)) |
|
59582 | 454 |
in case nliterals(Thm.prop_of th) of |
24300 | 455 |
1 => th::hcs |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
456 |
| n => rots(n, assoc_right th) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
457 |
end; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
458 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
459 |
(*Use "theorem naming" to label the clauses*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
460 |
fun name_thms label = |
33339 | 461 |
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
|
462 |
(k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) |
33339 | 463 |
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
|
464 |
|
16563 | 465 |
(*Is the given disjunction an all-negative support clause?*) |
59582 | 466 |
fun is_negative th = forall (not o #1) (literals (Thm.prop_of th)); |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
467 |
|
33317 | 468 |
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
|
469 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
470 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
471 |
(***** MESON PROOF PROCEDURE *****) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
472 |
|
74346 | 473 |
fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As) |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
474 |
| rhyps (_, As) = As; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
475 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
476 |
(** 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
|
477 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
478 |
(*The stringtree detects repeated assumptions.*) |
33245 | 479 |
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
|
480 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
481 |
(*detects repetitions in a list of terms*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
482 |
fun has_reps [] = false |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
483 |
| has_reps [_] = false |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
484 |
| has_reps [t,u] = (t aconv u) |
33245 | 485 |
| 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
|
486 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
487 |
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*) |
18508 | 488 |
fun TRYING_eq_assume_tac 0 st = Seq.single st |
489 |
| TRYING_eq_assume_tac i st = |
|
31945 | 490 |
TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st) |
18508 | 491 |
handle THM _ => TRYING_eq_assume_tac (i-1) st; |
492 |
||
59582 | 493 |
fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (Thm.nprems_of st) st; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
494 |
|
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
495 |
(*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
|
496 |
-- if *ANY* subgoal has repeated literals*) |
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
497 |
fun check_tac st = |
59582 | 498 |
if exists (fn prem => has_reps (rhyps(prem,[]))) (Thm.prems_of st) |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
499 |
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
|
500 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
501 |
|
59164 | 502 |
(* resolve_from_net_tac actually made it slower... *) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
503 |
fun prolog_step_tac ctxt horns i = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
504 |
(assume_tac ctxt i APPEND resolve_tac ctxt horns i) THEN check_tac THEN |
18508 | 505 |
TRYALL_eq_assume_tac; |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
506 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
507 |
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) |
33339 | 508 |
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
|
509 |
|
59582 | 510 |
fun size_of_subgoals st = fold_rev addconcl (Thm.prems_of st) 0; |
15579
32bee18c675f
Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents:
15574
diff
changeset
|
511 |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
512 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
513 |
(*Negation Normal Form*) |
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
514 |
val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, |
9869 | 515 |
not_impD, not_iffD, not_allD, not_exD, not_notD]; |
15581 | 516 |
|
74346 | 517 |
fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t |
518 |
| ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
519 |
| ok4nnf _ = false; |
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21095
diff
changeset
|
520 |
|
32262 | 521 |
fun make_nnf1 ctxt th = |
59582 | 522 |
if ok4nnf (Thm.concl_of th) |
32262 | 523 |
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
|
524 |
handle THM ("tryres", _, _) => |
32262 | 525 |
forward_res ctxt (make_nnf1 ctxt) |
9869 | 526 |
(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
|
527 |
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
|
528 |
else th |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
529 |
|
24300 | 530 |
(*The simplification removes defined quantifiers and occurrences of True and False. |
20018 | 531 |
nnf_ss also includes the one-point simprocs, |
18405
afb1a52a7011
removal of some redundancies (e.g. one-point-rules) in clause production
paulson
parents:
18389
diff
changeset
|
532 |
which are needed to avoid the various one-point theorems from generating junk clauses.*) |
19894 | 533 |
val nnf_simps = |
37539 | 534 |
@{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel |
535 |
if_eq_cancel cases_simp} |
|
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
536 |
fun nnf_extra_simps ({if_simps, ...} : simp_options) = |
74051 | 537 |
(if if_simps then @{thms split_ifs} else []) @ @{thms ex_simps all_simps simp_thms} |
18405
afb1a52a7011
removal of some redundancies (e.g. one-point-rules) in clause production
paulson
parents:
18389
diff
changeset
|
538 |
|
43821
048619bb1dc3
always unfold "Let"s is Sledgehammer, Metis, and MESON
blanchet
parents:
43264
diff
changeset
|
539 |
(* FIXME: "let_simp" is probably redundant now that we also rewrite with |
46904 | 540 |
"Let_def [abs_def]". *) |
74051 | 541 |
fun nnf_ss simp_options = |
69593 | 542 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
74051 | 543 |
addsimps (nnf_extra_simps simp_options) |
67149 | 544 |
addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>, \<^simproc>\<open>neq\<close>, \<^simproc>\<open>let_simp\<close>]) |
43264
a1a48c69d623
don't needlessly presimplify -- makes ATP problem preparation much faster
blanchet
parents:
42833
diff
changeset
|
545 |
|
46093 | 546 |
val presimplified_consts = |
67149 | 547 |
[\<^const_name>\<open>simp_implies\<close>, \<^const_name>\<open>False\<close>, \<^const_name>\<open>True\<close>, |
548 |
\<^const_name>\<open>Ex1\<close>, \<^const_name>\<open>Ball\<close>, \<^const_name>\<open>Bex\<close>, \<^const_name>\<open>If\<close>, |
|
549 |
\<^const_name>\<open>Let\<close>] |
|
15872 | 550 |
|
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
551 |
fun presimplify (simp_options as {let_simps, ...} : simp_options) ctxt = |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
552 |
rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps) |
74051 | 553 |
#> simplify (put_simpset (nnf_ss simp_options) ctxt) |
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
554 |
#> let_simps ? rewrite_rule ctxt @{thms Let_def [abs_def]} |
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
|
555 |
|
74051 | 556 |
fun make_nnf simp_options ctxt th = |
59582 | 557 |
(case Thm.prems_of th of |
74051 | 558 |
[] => th |> presimplify simp_options ctxt |> make_nnf1 ctxt |
59582 | 559 |
| _ => raise THM ("make_nnf: premises in argument", 0, [th])); |
15581 | 560 |
|
39950 | 561 |
fun choice_theorems thy = |
562 |
try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list |
|
563 |
||
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
|
564 |
(* 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
|
565 |
clauses that arise from a subgoal. *) |
74051 | 566 |
fun skolemize_with_choice_theorems simp_options 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
|
567 |
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
|
568 |
fun aux th = |
67149 | 569 |
if not (has_conns [\<^const_name>\<open>Ex\<close>] (Thm.prop_of th)) then |
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
|
570 |
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
|
571 |
else |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
572 |
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
|
573 |
[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
|
574 |
|> 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
|
575 |
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
|
576 |
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
|
577 |
|> 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
|
578 |
|> 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
|
579 |
handle THM ("tryres", _, _) => |
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
39979
diff
changeset
|
580 |
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
|
581 |
|> forward_res ctxt aux |
74051 | 582 |
in aux o make_nnf simp_options ctxt end |
29684 | 583 |
|
74051 | 584 |
fun skolemize simp_options ctxt = |
42361 | 585 |
let val thy = Proof_Context.theory_of ctxt in |
74051 | 586 |
skolemize_with_choice_theorems simp_options ctxt (choice_theorems thy) |
39950 | 587 |
end |
39904 | 588 |
|
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
589 |
exception NO_F_PATTERN of unit |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
590 |
|
47956 | 591 |
fun get_F_pattern T t u = |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
592 |
let |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
593 |
fun pat t u = |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
594 |
let |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58963
diff
changeset
|
595 |
val ((head1, args1), (head2, args2)) = (t, u) |> apply2 strip_comb |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
596 |
in |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
597 |
if head1 = head2 then |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
598 |
let val pats = map2 pat args1 args2 in |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
599 |
case filter (is_some o fst) pats of |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
600 |
[(SOME T, _)] => (SOME T, list_comb (head1, map snd pats)) |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
601 |
| [] => (NONE, t) |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
602 |
| _ => raise NO_F_PATTERN () |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
603 |
end |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
604 |
else |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
605 |
let val T = fastype_of t in |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
606 |
if can dest_funT T then (SOME T, Bound 0) else raise NO_F_PATTERN () |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
607 |
end |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
608 |
end |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
609 |
in |
74346 | 610 |
if T = \<^Type>\<open>bool\<close> then |
47956 | 611 |
NONE |
612 |
else case pat t u of |
|
613 |
(SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p)) |
|
614 |
| _ => NONE |
|
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
615 |
end |
47956 | 616 |
handle NO_F_PATTERN () => NONE |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
617 |
|
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
618 |
val ext_cong_neq = @{thm ext_cong_neq} |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
619 |
|
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
620 |
(* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *) |
59632 | 621 |
fun cong_extensionalize_thm ctxt th = |
59582 | 622 |
(case Thm.concl_of th of |
74346 | 623 |
\<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> => |
624 |
(case get_F_pattern T t u of |
|
625 |
SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq |
|
626 |
| NONE => th) |
|
59582 | 627 |
| _ => th) |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
628 |
|
42760 | 629 |
(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It |
630 |
would be desirable to do this symmetrically but there's at least one existing |
|
631 |
proof in "Tarski" that relies on the current behavior. *) |
|
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
632 |
fun abs_extensionalize_conv ctxt ct = |
59582 | 633 |
(case Thm.term_of ct of |
74346 | 634 |
\<^Const_>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close> => |
635 |
ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]} |
|
636 |
then_conv abs_extensionalize_conv ctxt) |
|
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
637 |
| _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct |
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
638 |
| Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct |
59582 | 639 |
| _ => Conv.all_conv ct) |
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 |
|
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
641 |
val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv |
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
47035
diff
changeset
|
642 |
|
74051 | 643 |
fun try_skolemize_etc simp_options ctxt th = |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
644 |
let |
59632 | 645 |
val th = th |> cong_extensionalize_thm ctxt |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
646 |
in |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
647 |
[th] |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
648 |
(* Extensionalize lambdas in "th", because that makes sense and that's what |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
649 |
Sledgehammer does, but also keep an unextensionalized version of "th" for |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
650 |
backward compatibility. *) |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
651 |
|> insert Thm.eq_thm_prop (abs_extensionalize_thm ctxt th) |
74051 | 652 |
|> map_filter (fn th => th |> try (skolemize simp_options ctxt) |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
653 |
|> tap (fn NONE => |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
654 |
trace_msg ctxt (fn () => |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
655 |
"Failed to skolemize " ^ |
61268 | 656 |
Thm.string_of_thm ctxt th) |
47954
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
657 |
| _ => ())) |
aada9fd08b58
make higher-order goals more first-order via extensionality
blanchet
parents:
47953
diff
changeset
|
658 |
end |
25694
cbb59ba6bf0c
Skolemization now catches exception THM, which may be raised if unification fails.
paulson
parents:
24937
diff
changeset
|
659 |
|
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
|
660 |
fun add_clauses ctxt th cls = |
59165 | 661 |
let |
662 |
val (cnfs, ctxt') = ctxt |
|
663 |
|> Variable.declare_thm th |
|
664 |
|> make_cnf [] th; |
|
665 |
in Variable.export ctxt' ctxt cnfs @ cls end; |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
666 |
|
47035 | 667 |
(*Sort clauses by number of literals*) |
59582 | 668 |
fun fewerlits (th1, th2) = nliterals (Thm.prop_of th1) < nliterals (Thm.prop_of th2) |
47035 | 669 |
|
9840
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 []; |
47035 | 673 |
val make_clauses = sort (make_ord fewerlits) 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 |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
683 |
fun best_prolog_tac ctxt sizef horns = |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
684 |
BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1); |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
685 |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
686 |
fun depth_prolog_tac ctxt horns = |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
687 |
DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1); |
9840
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 |
|
74051 | 692 |
fun skolemize_prems_tac simp_options ctxt prems = |
693 |
cut_facts_tac (maps (try_skolemize_etc simp_options ctxt) prems) THEN' |
|
694 |
REPEAT o eresolve_tac ctxt [exE] |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
695 |
|
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset
|
696 |
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. |
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset
|
697 |
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
|
698 |
fun MESON preskolem_tac mkcl cltac ctxt i st = |
16588 | 699 |
SELECT_GOAL |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52230
diff
changeset
|
700 |
(EVERY [Object_Logic.atomize_prems_tac ctxt 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
701 |
resolve_tac ctxt @{thms 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
|
702 |
preskolem_tac, |
32283 | 703 |
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} => |
74075
a5bab59d580b
added support for TFX $let to Sledgehammer's TPTP output
desharna
parents:
74051
diff
changeset
|
704 |
EVERY1 [skolemize_prems_tac simp_options_all_true ctxt' negs, |
32283 | 705 |
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st |
24300 | 706 |
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
707 |
|
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
|
708 |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
709 |
(** Best-first search versions **) |
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
710 |
|
16563 | 711 |
(*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
|
712 |
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
|
713 |
MESON all_tac (make_clauses ctxt) |
22546
c40d7ab8cbc5
MESON tactical takes an additional argument: the clausification function.
paulson
parents:
22515
diff
changeset
|
714 |
(fn cls => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
715 |
THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
716 |
(has_fewer_prems 1, sizef) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
717 |
(prolog_step_tac ctxt (make_horns cls) 1)) |
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
|
718 |
ctxt |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
719 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
720 |
(*First, breaks the goal into independent units*) |
32262 | 721 |
fun safe_best_meson_tac ctxt = |
42793 | 722 |
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
|
723 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
724 |
(** Depth-first search version **) |
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
725 |
|
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
|
726 |
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
|
727 |
MESON all_tac (make_clauses ctxt) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
728 |
(fn cls => EVERY [resolve_tac ctxt (gocls cls) 1, depth_prolog_tac ctxt (make_horns 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
|
729 |
ctxt |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
730 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
731 |
(** Iterative deepening version **) |
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
732 |
|
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
733 |
(*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
|
734 |
having only one eq_assume_tac speeds it up!*) |
58957 | 735 |
fun prolog_step_tac' ctxt horns = |
67522 | 736 |
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
|
737 |
take_prefix Thm.no_prems horns |
59164 | 738 |
val nrtac = resolve_from_net_tac ctxt (Tactic.build_net horns) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
739 |
in fn i => eq_assume_tac i ORELSE |
58957 | 740 |
match_tac ctxt horn0s i ORELSE (*no backtracking if unit MATCHES*) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
741 |
((assume_tac ctxt i APPEND nrtac i) THEN check_tac) |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
742 |
end; |
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
743 |
|
58957 | 744 |
fun iter_deepen_prolog_tac ctxt horns = |
745 |
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns); |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
746 |
|
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
|
747 |
fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt) |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
748 |
(fn cls => |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
749 |
(case (gocls (cls @ ths)) of |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
750 |
[] => no_tac (*no goal clauses*) |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
751 |
| goes => |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
752 |
let |
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
753 |
val horns = make_horns (cls @ ths) |
39979
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39953
diff
changeset
|
754 |
val _ = trace_msg ctxt (fn () => |
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32032
diff
changeset
|
755 |
cat_lines ("meson method called:" :: |
61268 | 756 |
map (Thm.string_of_thm ctxt) (cls @ ths) @ |
757 |
["clauses:"] @ map (Thm.string_of_thm ctxt) horns)) |
|
38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
758 |
in |
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
759 |
THEN_ITER_DEEPEN iter_deepen_limit |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59171
diff
changeset
|
760 |
(resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns) |
38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
wenzelm
parents:
38795
diff
changeset
|
761 |
end)); |
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
762 |
|
32262 | 763 |
fun meson_tac ctxt ths = |
42793 | 764 |
SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths)); |
9869 | 765 |
|
766 |
||
14813 | 767 |
(**** Code to support ordinary resolution, rather than Model Elimination ****) |
14744 | 768 |
|
24300 | 769 |
(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), |
15008 | 770 |
with no contrapositives, for ordinary resolution.*) |
14744 | 771 |
|
772 |
(*Rules to convert the head literal into a negated assumption. If the head |
|
773 |
literal is already negated, then using notEfalse instead of notEfalse' |
|
774 |
prevents a double negation.*) |
|
67091 | 775 |
val notEfalse = @{lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> False" by (rule notE)}; |
776 |
val notEfalse' = @{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}; |
|
14744 | 777 |
|
24300 | 778 |
fun negated_asm_of_head th = |
14744 | 779 |
th RS notEfalse handle THM _ => th RS notEfalse'; |
780 |
||
26066
19df083a2bbf
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents:
25710
diff
changeset
|
781 |
(*Converting one theorem from a disjunction to a meta-level clause*) |
60358 | 782 |
fun make_meta_clause ctxt th = |
783 |
let val (fth, thaw) = Misc_Legacy.freeze_thaw_robust ctxt th |
|
26066
19df083a2bbf
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents:
25710
diff
changeset
|
784 |
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
|
785 |
(zero_var_indexes o Thm.varifyT_global o thaw 0 o |
26066
19df083a2bbf
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents:
25710
diff
changeset
|
786 |
negated_asm_of_head o make_horn resolution_clause_rules) fth |
19df083a2bbf
make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex
paulson
parents:
25710
diff
changeset
|
787 |
end; |
24300 | 788 |
|
60358 | 789 |
fun make_meta_clauses ctxt ths = |
14744 | 790 |
name_thms "MClause#" |
60358 | 791 |
(distinct Thm.eq_thm_prop (map (make_meta_clause ctxt) ths)); |
14744 | 792 |
|
9840
9dfcb0224f8c
meson.ML moved from HOL/ex to HOL/Tools: meson_tac installed by default
paulson
parents:
diff
changeset
|
793 |
end; |