author | blanchet |
Wed, 06 Oct 2010 12:01:55 +0200 | |
changeset 39959 | 12eb8fe15b00 |
parent 39958 | 88c9aa5666de |
child 39961 | 415556559fad |
permissions | -rw-r--r-- |
39958 | 1 |
(* Title: HOL/Tools/Metis/metis_tactics.ML |
38027 | 2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
Copyright Cambridge University 2007 |
23447 | 6 |
|
29266 | 7 |
HOL setup for the Metis prover. |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
|
35826 | 10 |
signature METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
sig |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
12 |
val trace : bool Unsynchronized.ref |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
13 |
val type_lits : bool Config.T |
39891
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
14 |
val new_skolemizer : bool Config.T |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
15 |
val metis_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
16 |
val metisF_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
17 |
val metisFT_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
18 |
val setup : theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
|
35826 | 21 |
structure Metis_Tactics : METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
|
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39450
diff
changeset
|
24 |
open Metis_Translate |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
25 |
open Metis_Reconstruct |
35826 | 26 |
|
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
27 |
structure Int_Pair_Graph = |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
28 |
Graph(type key = int * int val ord = prod_ord int_ord int_ord) |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
29 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
30 |
fun trace_msg msg = if !trace then tracing (msg ()) else () |
32955 | 31 |
|
39891
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
32 |
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) |
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
33 |
val (new_skolemizer, new_skolemizer_setup) = |
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
34 |
Attrib.config_bool "metis_new_skolemizer" (K false) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
35 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
36 |
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
37 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
38 |
fun have_common_thm ths1 ths2 = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
39 |
exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
40 |
|
32956 | 41 |
(*Determining which axiom clauses are actually used*) |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
42 |
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
32994 | 43 |
| used_axioms _ _ = NONE; |
24855 | 44 |
|
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
45 |
val clause_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
46 |
{ordering = Metis_KnuthBendixOrder.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
47 |
orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
48 |
orderTerms = true} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
49 |
val active_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
50 |
{clause = clause_params, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
51 |
prefactor = #prefactor Metis_Active.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
52 |
postfactor = #postfactor Metis_Active.default} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
53 |
val waiting_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
54 |
{symbolsWeight = 1.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
55 |
variablesWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
56 |
literalsWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
57 |
models = []} |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
58 |
val resolution_params = {active = active_params, waiting = waiting_params} |
37573 | 59 |
|
39959 | 60 |
(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *) |
61 |
||
62 |
(* FIXME ### try cterm_instantiate *) |
|
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
63 |
fun instantiate_theorem thy inst th = |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
64 |
let |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
65 |
val tyenv = Vartab.empty |> fold (Type.raw_unify o pairself fastype_of) inst |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
66 |
val instT = |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
67 |
[] |> Vartab.fold (fn (z, (S, T)) => |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
68 |
cons (TVar (z, S), Type.devar tyenv T)) tyenv |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
69 |
val inst = inst |> map (pairself (subst_atomic_types instT)) |
39952 | 70 |
val _ = trace_msg (fn () => cat_lines (map (fn (T, U) => |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
71 |
Syntax.string_of_typ @{context} T ^ " |-> " ^ |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
72 |
Syntax.string_of_typ @{context} U) instT)) |
39952 | 73 |
val _ = trace_msg (fn () => cat_lines (map (fn (t, u) => |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
74 |
Syntax.string_of_term @{context} t ^ " |-> " ^ |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
75 |
Syntax.string_of_term @{context} u) inst)) |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
76 |
val cinstT = instT |> map (pairself (ctyp_of thy)) |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
77 |
val cinst = inst |> map (pairself (cterm_of thy)) |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
78 |
in th |> Thm.instantiate (cinstT, cinst) end |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
79 |
|
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
80 |
(* In principle, it should be sufficient to apply "assume_tac" to unify the |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
81 |
conclusion with one of the premises. However, in practice, this is unreliable |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
82 |
because of the mildly higher-order nature of the unification problems. |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
83 |
Typical constraints are of the form |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
84 |
"?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x", |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
85 |
where the nonvariables are goal parameters. *) |
39959 | 86 |
(* FIXME: ### try Pattern.match instead *) |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
87 |
fun unify_first_prem_with_concl thy i th = |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
88 |
let |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
89 |
val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
90 |
val prem = goal |> Logic.strip_assums_hyp |> hd |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
91 |
val concl = goal |> Logic.strip_assums_concl |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
92 |
fun pair_untyped_aconv (t1, t2) (u1, u2) = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
93 |
untyped_aconv t1 u1 andalso untyped_aconv t2 u2 |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
94 |
fun add_terms tp inst = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
95 |
if exists (pair_untyped_aconv tp) inst then inst |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
96 |
else tp :: map (apsnd (subst_atomic [tp])) inst |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
97 |
fun is_flex t = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
98 |
case strip_comb t of |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
99 |
(Var _, args) => forall is_Bound args |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
100 |
| _ => false |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
101 |
fun unify_flex flex rigid = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
102 |
case strip_comb flex of |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
103 |
(Var (z as (_, T)), args) => |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
104 |
add_terms (Var z, |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
105 |
fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
106 |
| _ => raise TERM ("unify_flex: expected flex", [flex]) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
107 |
fun unify_potential_flex comb atom = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
108 |
if is_flex comb then unify_flex comb atom |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
109 |
else if is_Var atom then add_terms (atom, comb) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
110 |
else raise TERM ("unify_terms", [comb, atom]) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
111 |
fun unify_terms (t, u) = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
112 |
case (t, u) of |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
113 |
(t1 $ t2, u1 $ u2) => |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
114 |
if is_flex t then unify_flex t u |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
115 |
else if is_flex u then unify_flex u t |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
116 |
else fold unify_terms [(t1, u1), (t2, u2)] |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
117 |
| (_ $ _, _) => unify_potential_flex t u |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
118 |
| (_, _ $ _) => unify_potential_flex u t |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
119 |
| (Var _, _) => add_terms (t, u) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
120 |
| (_, Var _) => add_terms (u, t) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
121 |
| _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u]) |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
122 |
in th |> instantiate_theorem thy (unify_terms (prem, concl) []) end |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
123 |
|
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
124 |
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (index_no, axiom_no) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
125 |
fun shuffle_ord p = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
126 |
rev_order (prod_ord int_ord int_ord (pairself shuffle_key p)) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
127 |
|
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
128 |
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
129 |
|
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
130 |
fun copy_prems_tac [] ns i = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
131 |
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
132 |
| copy_prems_tac (1 :: ms) ns i = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
133 |
rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
134 |
| copy_prems_tac (m :: ms) ns i = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
135 |
etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
136 |
|
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
137 |
fun instantiate_forall_tac thy params t i = |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
138 |
let |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
139 |
fun repair (t as (Var ((s, _), _))) = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
140 |
(case find_index (fn ((s', _), _) => s' = s) params of |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
141 |
~1 => t |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
142 |
| j => Bound j) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
143 |
| repair (t $ u) = repair t $ repair u |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
144 |
| repair t = t |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
145 |
val t' = t |> repair |> fold (curry absdummy) (map snd params) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
146 |
fun do_instantiate th = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
147 |
let val var = Term.add_vars (prop_of th) [] |> the_single in |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
148 |
th |> instantiate_theorem thy [(Var var, t')] |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
149 |
end |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
150 |
in |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
151 |
etac @{thm allE} i |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
152 |
THEN rotate_tac ~1 i |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
153 |
THEN PRIMITIVE do_instantiate |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
154 |
end |
39897 | 155 |
|
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
156 |
fun release_clusters_tac _ _ _ _ [] = K all_tac |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
157 |
| release_clusters_tac thy ax_counts substs params |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
158 |
((ax_no, cluster_no) :: clusters) = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
159 |
let |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
160 |
fun in_right_cluster s = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
161 |
(s |> Meson_Clausify.cluster_of_zapped_var_name |> fst |> snd |> fst) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
162 |
= cluster_no |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
163 |
val cluster_substs = |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
164 |
substs |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
165 |
|> map_filter (fn (ax_no', (_, (_, tsubst))) => |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
166 |
if ax_no' = ax_no then |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
167 |
tsubst |> filter (in_right_cluster |
39959 | 168 |
o fst o fst o dest_Var o fst) |
169 |
|> map snd |> SOME |
|
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
170 |
else |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
171 |
NONE) |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
172 |
val n = length cluster_substs |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
173 |
fun do_cluster_subst cluster_subst = |
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
174 |
map (instantiate_forall_tac thy params) cluster_subst @ [rotate_tac 1] |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
175 |
val params' = params (* FIXME ### existentials! *) |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
176 |
val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
177 |
in |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
178 |
rotate_tac first_prem |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
179 |
THEN' (EVERY' (maps do_cluster_subst cluster_substs)) |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
180 |
THEN' rotate_tac (~ first_prem - length cluster_substs) |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
181 |
THEN' release_clusters_tac thy ax_counts substs params' clusters |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
182 |
end |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
183 |
|
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
184 |
val cluster_ord = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
185 |
prod_ord (prod_ord int_ord (prod_ord int_ord int_ord)) bool_ord |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
186 |
|
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
187 |
val tysubst_ord = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
188 |
list_ord (prod_ord Term_Ord.fast_indexname_ord |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
189 |
(prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
190 |
|
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
191 |
structure Int_Tysubst_Table = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
192 |
Table(type key = int * (indexname * (sort * typ)) list |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
193 |
val ord = prod_ord int_ord tysubst_ord) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
194 |
|
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
195 |
(* Attempts to derive the theorem "False" from a theorem of the form |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
196 |
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
197 |
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
198 |
must be eliminated first. *) |
39897 | 199 |
fun discharge_skolem_premises ctxt axioms prems_imp_false = |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
200 |
if prop_of prems_imp_false aconv @{prop False} then |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
201 |
prems_imp_false |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
202 |
else |
39897 | 203 |
let |
204 |
val thy = ProofContext.theory_of ctxt |
|
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
205 |
(* distinguish variables with same name but different types *) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
206 |
val prems_imp_false' = |
39936 | 207 |
prems_imp_false |> try (forall_intr_vars #> gen_all) |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
208 |
|> the_default prems_imp_false |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
209 |
val prems_imp_false = |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
210 |
if prop_of prems_imp_false aconv prop_of prems_imp_false' then |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
211 |
prems_imp_false |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
212 |
else |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
213 |
prems_imp_false' |
39897 | 214 |
fun match_term p = |
215 |
let |
|
216 |
val (tyenv, tenv) = |
|
217 |
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty) |
|
218 |
val tsubst = |
|
219 |
tenv |> Vartab.dest |
|
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
220 |
|> sort (cluster_ord |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
221 |
o pairself (Meson_Clausify.cluster_of_zapped_var_name |
39897 | 222 |
o fst o fst)) |
223 |
|> map (Meson.term_pair_of |
|
224 |
#> pairself (Envir.subst_term_types tyenv)) |
|
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
225 |
val tysubst = tyenv |> Vartab.dest |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
226 |
in (tysubst, tsubst) end |
39934
9f116d095e5e
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
blanchet
parents:
39933
diff
changeset
|
227 |
fun subst_info_for_prem subgoal_no prem = |
39897 | 228 |
case prem of |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39952
diff
changeset
|
229 |
_ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => |
39902 | 230 |
let val ax_no = HOLogic.dest_nat num in |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
231 |
(ax_no, (subgoal_no, |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
232 |
match_term (nth axioms ax_no |> the |> snd, t))) |
39897 | 233 |
end |
234 |
| _ => raise TERM ("discharge_skolem_premises: Malformed premise", |
|
235 |
[prem]) |
|
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
236 |
fun cluster_of_var_name skolem s = |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
237 |
let |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
238 |
val ((ax_no, (cluster_no, _)), skolem') = |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
239 |
Meson_Clausify.cluster_of_zapped_var_name s |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
240 |
in |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
241 |
if skolem' = skolem andalso cluster_no > 0 then |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
242 |
SOME (ax_no, cluster_no) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
243 |
else |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
244 |
NONE |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
245 |
end |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
246 |
fun clusters_in_term skolem t = |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
247 |
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
248 |
fun deps_for_term_subst (var, t) = |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
249 |
case clusters_in_term false var of |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
250 |
[] => NONE |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
251 |
| [(ax_no, cluster_no)] => |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
252 |
SOME ((ax_no, cluster_no), |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
253 |
clusters_in_term true t |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
254 |
|> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
255 |
| _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
256 |
val prems = Logic.strip_imp_prems (prop_of prems_imp_false) |
39934
9f116d095e5e
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
blanchet
parents:
39933
diff
changeset
|
257 |
val substs = prems |> map2 subst_info_for_prem (1 upto length prems) |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
258 |
|> sort (int_ord o pairself fst) |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
259 |
val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
260 |
val clusters = maps (op ::) depss |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
261 |
val ordered_clusters = |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
262 |
Int_Pair_Graph.empty |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
263 |
|> fold Int_Pair_Graph.default_node (map (rpair ()) clusters) |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
264 |
|> fold Int_Pair_Graph.add_deps_acyclic depss |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
265 |
|> Int_Pair_Graph.topological_order |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
266 |
handle Int_Pair_Graph.CYCLES _ => |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
267 |
error "Cannot replay Metis proof in Isabelle without axiom of \ |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
268 |
\choice." |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
269 |
val params0 = |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
270 |
[] |> fold (Term.add_vars o snd) (map_filter I axioms) |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
271 |
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
272 |
|> filter (fn (((_, (cluster_no, _)), skolem), _) => |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
273 |
cluster_no = 0 andalso skolem) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
274 |
|> sort shuffle_ord |> map snd |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
275 |
val ax_counts = |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
276 |
Int_Tysubst_Table.empty |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
277 |
|> fold (fn (ax_no, (_, (tysubst, _))) => |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
278 |
Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
279 |
(Integer.add 1)) substs |
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
280 |
|> Int_Tysubst_Table.dest |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
281 |
(* for debugging: |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
282 |
fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = |
39934
9f116d095e5e
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
blanchet
parents:
39933
diff
changeset
|
283 |
"ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
284 |
"; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^ |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
285 |
commas (map ((fn (s, t) => s ^ " |-> " ^ t) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
286 |
o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" |
39936 | 287 |
val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ |
288 |
cat_lines (map string_for_subst_info substs)) |
|
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
289 |
val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0) |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
290 |
val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters) |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
291 |
val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts) |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
292 |
*) |
39934
9f116d095e5e
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
blanchet
parents:
39933
diff
changeset
|
293 |
fun rotation_for_subgoal i = |
9f116d095e5e
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
blanchet
parents:
39933
diff
changeset
|
294 |
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs |
39897 | 295 |
in |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
296 |
Goal.prove ctxt [] [] @{prop False} |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
297 |
(K (cut_rules_tac |
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
298 |
(map (fst o the o nth axioms o fst o fst) ax_counts) 1 |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
299 |
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) |
39933
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
300 |
THEN copy_prems_tac (map snd ax_counts) [] 1 |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
301 |
THEN release_clusters_tac thy ax_counts substs params0 |
e764c5cf01fe
instantiate foralls and release exists in the order described by the topological order
blanchet
parents:
39914
diff
changeset
|
302 |
ordered_clusters 1 |
39897 | 303 |
THEN match_tac [prems_imp_false] 1 |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
304 |
THEN ALLGOALS (fn i => |
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39952
diff
changeset
|
305 |
rtac @{thm Meson.skolem_COMBK_I} i |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
306 |
THEN rotate_tac (rotation_for_subgoal i) i |
39937
4ee63a30194c
correctly handle multiple copies of the same axiom with the same types
blanchet
parents:
39936
diff
changeset
|
307 |
THEN PRIMITIVE (unify_first_prem_with_concl thy i) |
39935
56409c11195d
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
blanchet
parents:
39934
diff
changeset
|
308 |
THEN assume_tac i))) |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
309 |
end |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
310 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
311 |
(* Main function to start Metis proof and reconstruction *) |
32956 | 312 |
fun FOL_SOLVE mode ctxt cls ths0 = |
313 |
let val thy = ProofContext.theory_of ctxt |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
314 |
val type_lits = Config.get ctxt type_lits |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset
|
315 |
val new_skolemizer = |
39950 | 316 |
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
35826 | 317 |
val th_cls_pairs = |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
318 |
map2 (fn j => fn th => |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
319 |
(Thm.get_name_hint th, |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset
|
320 |
Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
321 |
(0 upto length ths0 - 1) ths0 |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
322 |
val thss = map (snd o snd) th_cls_pairs |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
323 |
val dischargers = map (fst o snd) th_cls_pairs |
32956 | 324 |
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
325 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls |
|
326 |
val _ = trace_msg (fn () => "THEOREM CLAUSES") |
|
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
327 |
val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
328 |
val (mode, {axioms, tfrees, old_skolems}) = |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
329 |
build_logic_map mode ctxt type_lits cls thss |
32956 | 330 |
val _ = if null tfrees then () |
331 |
else (trace_msg (fn () => "TFREE CLAUSES"); |
|
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37632
diff
changeset
|
332 |
app (fn TyLitFree ((s, _), (s', _)) => |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
333 |
trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) |
32956 | 334 |
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") |
335 |
val thms = map #1 axioms |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
336 |
val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms |
32956 | 337 |
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) |
338 |
val _ = trace_msg (fn () => "START METIS PROVE PROCESS") |
|
339 |
in |
|
33317 | 340 |
case filter (is_false o prop_of) cls of |
32956 | 341 |
false_th::_ => [false_th RS @{thm FalseE}] |
342 |
| [] => |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
343 |
case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
344 |
|> Metis_Resolution.loop of |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
345 |
Metis_Resolution.Contradiction mth => |
32956 | 346 |
let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
347 |
Metis_Thm.toString mth) |
32956 | 348 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
349 |
(*add constraints arising from converting goal to clause form*) |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
350 |
val proof = Metis_Proof.proof mth |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
351 |
val result = |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
352 |
fold (replay_one_inference ctxt' mode old_skolems) proof axioms |
32956 | 353 |
and used = map_filter (used_axioms axioms) proof |
354 |
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") |
|
355 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used |
|
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
356 |
val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
357 |
if have_common_thm used cls then NONE else SOME name) |
32956 | 358 |
in |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
359 |
if not (null cls) andalso not (have_common_thm used cls) then |
36383 | 360 |
warning "Metis: The assumptions are inconsistent." |
361 |
else |
|
362 |
(); |
|
363 |
if not (null unused) then |
|
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
364 |
warning ("Metis: Unused theorems: " ^ commas_quote unused |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
365 |
^ ".") |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
366 |
else |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
367 |
(); |
32956 | 368 |
case result of |
369 |
(_,ith)::_ => |
|
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
370 |
(trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
371 |
[discharge_skolem_premises ctxt dischargers ith]) |
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset
|
372 |
| _ => (trace_msg (fn () => "Metis: No result"); []) |
32956 | 373 |
end |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
374 |
| Metis_Resolution.Satisfiable _ => |
32956 | 375 |
(trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); |
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset
|
376 |
[]) |
32956 | 377 |
end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
378 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
379 |
(* Extensionalize "th", because that makes sense and that's what Sledgehammer |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
380 |
does, but also keep an unextensionalized version of "th" for backward |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
381 |
compatibility. *) |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
382 |
fun also_extensionalize_theorem th = |
39890 | 383 |
let val th' = Meson_Clausify.extensionalize_theorem th in |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
384 |
if Thm.eq_thm (th, th') then [th] |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
385 |
else th :: Meson.make_clauses_unsorted [th'] |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
386 |
end |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
387 |
|
38028 | 388 |
val neg_clausify = |
389 |
single |
|
390 |
#> Meson.make_clauses_unsorted |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
391 |
#> maps also_extensionalize_theorem |
39890 | 392 |
#> map Meson_Clausify.introduce_combinators_in_theorem |
38028 | 393 |
#> Meson.finish_cnf |
394 |
||
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:
39267
diff
changeset
|
395 |
fun preskolem_tac ctxt st0 = |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
396 |
(if exists (Meson.has_too_many_clauses ctxt) |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
397 |
(Logic.prems_of_goal (prop_of st0) 1) then |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
398 |
cnf.cnfx_rewrite_tac ctxt 1 |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
399 |
else |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
400 |
all_tac) st0 |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
401 |
|
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
402 |
val type_has_top_sort = |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
403 |
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
404 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
405 |
fun generic_metis_tac mode ctxt ths i st0 = |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
406 |
let |
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
407 |
val _ = trace_msg (fn () => |
32956 | 408 |
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
409 |
in |
|
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset
|
410 |
if exists_type type_has_top_sort (prop_of st0) then |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
411 |
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset
|
412 |
else |
39594
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
413 |
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) |
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
414 |
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
624d6c0e220d
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
blanchet
parents:
39560
diff
changeset
|
415 |
ctxt i st0 |
32956 | 416 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
417 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
418 |
val metis_tac = generic_metis_tac HO |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
419 |
val metisF_tac = generic_metis_tac FO |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
420 |
val metisFT_tac = generic_metis_tac FT |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
421 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
422 |
(* Whenever "X" has schematic type variables, we treat "using X by metis" as |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
423 |
"by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables. |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
424 |
We don't do it for nonschematic facts "X" because this breaks a few proofs |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
425 |
(in the rare and subtle case where a proof relied on extensionality not being |
38994 | 426 |
applied) and brings few benefits. *) |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
427 |
val has_tvar = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
428 |
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
429 |
fun method name mode = |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
430 |
Method.setup name (Attrib.thms >> (fn ths => fn ctxt => |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
431 |
METHOD (fn facts => |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
432 |
let |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
433 |
val (schem_facts, nonschem_facts) = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
434 |
List.partition has_tvar facts |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
435 |
in |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
436 |
HEADGOAL (Method.insert_tac nonschem_facts THEN' |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
437 |
CHANGED_PROP |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
438 |
o generic_metis_tac mode ctxt (schem_facts @ ths)) |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
439 |
end))) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
440 |
|
32956 | 441 |
val setup = |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
442 |
type_lits_setup |
39891
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
443 |
#> new_skolemizer_setup |
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
444 |
#> method @{binding metis} HO "Metis for FOL/HOL problems" |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
445 |
#> method @{binding metisF} FO "Metis for FOL problems" |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
446 |
#> method @{binding metisFT} FT |
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
447 |
"Metis for FOL/HOL problems with fully-typed translation" |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
448 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
449 |
end; |