author | blanchet |
Fri, 01 Oct 2010 17:52:20 +0200 | |
changeset 39906 | 864bfafcf251 |
parent 39905 | 0bfaaa81fc62 |
child 39907 | b0be1daf0667 |
permissions | -rw-r--r-- |
39890 | 1 |
(* Title: HOL/Tools/Sledgehammer/meson_clausify.ML |
38027 | 2 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
blanchet
parents:
36228
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
15347 | 4 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
5 |
Transformation of axiom rules (elim/intro/etc) into CNF forms. |
15347 | 6 |
*) |
7 |
||
39890 | 8 |
signature MESON_CLAUSIFY = |
21505 | 9 |
sig |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
10 |
val new_skolem_var_prefix : string |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38610
diff
changeset
|
11 |
val extensionalize_theorem : thm -> thm |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
12 |
val introduce_combinators_in_cterm : cterm -> thm |
38028 | 13 |
val introduce_combinators_in_theorem : thm -> thm |
39037
5146d640aa4a
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
blanchet
parents:
39036
diff
changeset
|
14 |
val to_definitional_cnf_with_quantifiers : theory -> thm -> thm |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
15 |
val cluster_of_zapped_var_name : string -> (int * int) * bool |
39897 | 16 |
val cnf_axiom : |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
17 |
Proof.context -> bool -> int -> thm -> (thm * term) option * thm list |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
18 |
val meson_general_tac : Proof.context -> thm list -> int -> tactic |
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
19 |
val setup: theory -> theory |
21505 | 20 |
end; |
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
21 |
|
39890 | 22 |
structure Meson_Clausify : MESON_CLAUSIFY = |
15997 | 23 |
struct |
15347 | 24 |
|
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
25 |
(* the extra "?" helps prevent clashes *) |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
26 |
val new_skolem_var_prefix = "?SK" |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
27 |
val new_nonskolem_var_prefix = "?V" |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
28 |
|
15997 | 29 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 30 |
|
29064 | 31 |
val cfalse = cterm_of @{theory HOL} HOLogic.false_const; |
32 |
val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const); |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
33 |
|
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
34 |
(* Converts an elim-rule into an equivalent theorem that does not have the |
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
35 |
predicate variable. Leaves other theorems unchanged. We simply instantiate |
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
36 |
the conclusion variable to False. (Cf. "transform_elim_term" in |
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
37 |
"Sledgehammer_Util".) *) |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
38 |
fun transform_elim_theorem th = |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
39 |
case concl_of th of (*conclusion variable*) |
35963 | 40 |
@{const Trueprop} $ (v as Var (_, @{typ bool})) => |
29064 | 41 |
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th |
35963 | 42 |
| v as Var(_, @{typ prop}) => |
29064 | 43 |
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
44 |
| _ => th |
15997 | 45 |
|
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
46 |
|
16009 | 47 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
48 |
||
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
49 |
fun mk_old_skolem_term_wrapper t = |
37436 | 50 |
let val T = fastype_of t in |
39355 | 51 |
Const (@{const_name skolem}, T --> T) $ t |
37436 | 52 |
end |
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37403
diff
changeset
|
53 |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
54 |
fun beta_eta_under_lambdas (Abs (s, T, t')) = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
55 |
Abs (s, T, beta_eta_under_lambdas t') |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
56 |
| beta_eta_under_lambdas t = Envir.beta_eta_contract t |
37512
ff72d3ddc898
this looks like the most appropriate place to do the beta-eta-contraction
blanchet
parents:
37511
diff
changeset
|
57 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
58 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
59 |
fun old_skolem_defs th = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
60 |
let |
39376 | 61 |
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
62 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
63 |
let |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
64 |
val args = OldTerm.term_frees body |
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
65 |
(* Forms a lambda-abstraction over the formal parameters *) |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
66 |
val rhs = |
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset
|
67 |
list_abs_free (map dest_Free args, |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
68 |
HOLogic.choice_const T $ beta_eta_under_lambdas body) |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
69 |
|> mk_old_skolem_term_wrapper |
37518
efb0923cc098
use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents:
37512
diff
changeset
|
70 |
val comb = list_comb (rhs, args) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
71 |
in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
72 |
| dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) rhss = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
73 |
(*Universal quant: insert a free variable into body and continue*) |
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
74 |
let val fname = Name.variant (OldTerm.add_term_names (p,[])) a |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
75 |
in dec_sko (subst_bound (Free(fname,T), p)) rhss end |
39906 | 76 |
| dec_sko (@{const conj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
77 |
| dec_sko (@{const disj} $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
78 |
| dec_sko (@{const Trueprop} $ p) rhss = dec_sko p rhss |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
79 |
| dec_sko _ rhss = rhss |
20419 | 80 |
in dec_sko (prop_of th) [] end; |
81 |
||
82 |
||
24827 | 83 |
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) |
20419 | 84 |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39268
diff
changeset
|
85 |
val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} |
20419 | 86 |
|
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
87 |
(* Removes the lambdas from an equation of the form "t = (%x. u)". |
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:
38282
diff
changeset
|
88 |
(Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) |
38000
c0b9efa8bfca
added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
blanchet
parents:
37995
diff
changeset
|
89 |
fun extensionalize_theorem th = |
37540
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
90 |
case prop_of th of |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
91 |
_ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) |
39376 | 92 |
$ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) |
37540
48273d1ea331
better eta-expansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset
|
93 |
| _ => th |
20419 | 94 |
|
39355 | 95 |
fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
96 |
| is_quasi_lambda_free (t1 $ t2) = |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
97 |
is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2 |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
98 |
| is_quasi_lambda_free (Abs _) = false |
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
99 |
| is_quasi_lambda_free _ = true |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
100 |
|
32010 | 101 |
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); |
102 |
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); |
|
103 |
val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
104 |
|
38282
319c59682c51
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38280
diff
changeset
|
105 |
(* FIXME: Requires more use of cterm constructors. *) |
24827 | 106 |
fun abstract ct = |
28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
107 |
let |
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset
|
108 |
val thy = theory_of_cterm ct |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
109 |
val Abs(x,_,body) = term_of ct |
35963 | 110 |
val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) |
38005
b6555e9c5de4
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
blanchet
parents:
38001
diff
changeset
|
111 |
val cxT = ctyp_of thy xT |
b6555e9c5de4
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
blanchet
parents:
38001
diff
changeset
|
112 |
val cbodyT = ctyp_of thy bodyT |
b6555e9c5de4
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
blanchet
parents:
38001
diff
changeset
|
113 |
fun makeK () = |
b6555e9c5de4
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
blanchet
parents:
38001
diff
changeset
|
114 |
instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] |
b6555e9c5de4
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
blanchet
parents:
38001
diff
changeset
|
115 |
@{thm abs_K} |
24827 | 116 |
in |
117 |
case body of |
|
118 |
Const _ => makeK() |
|
119 |
| Free _ => makeK() |
|
120 |
| Var _ => makeK() (*though Var isn't expected*) |
|
27184 | 121 |
| Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) |
24827 | 122 |
| rator$rand => |
27184 | 123 |
if loose_bvar1 (rator,0) then (*C or S*) |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
124 |
if loose_bvar1 (rand,0) then (*S*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
125 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
126 |
val crand = cterm_of thy (Abs(x,xT,rand)) |
27184 | 127 |
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} |
128 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
|
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
129 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
130 |
Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
131 |
end |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
132 |
else (*C*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
133 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
27184 | 134 |
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} |
135 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
|
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
136 |
in |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
137 |
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
138 |
end |
27184 | 139 |
else if loose_bvar1 (rand,0) then (*B or eta*) |
36945 | 140 |
if rand = Bound 0 then Thm.eta_conversion ct |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
141 |
else (*B*) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
142 |
let val crand = cterm_of thy (Abs(x,xT,rand)) |
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
143 |
val crator = cterm_of thy rator |
27184 | 144 |
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} |
145 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
|
37349 | 146 |
in Thm.transitive abs_B' (Conv.arg_conv abstract rhs) end |
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset
|
147 |
else makeK() |
37349 | 148 |
| _ => raise Fail "abstract: Bad term" |
24827 | 149 |
end; |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
150 |
|
37349 | 151 |
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *) |
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
152 |
fun introduce_combinators_in_cterm ct = |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
153 |
if is_quasi_lambda_free (term_of ct) then |
37349 | 154 |
Thm.reflexive ct |
155 |
else case term_of ct of |
|
156 |
Abs _ => |
|
157 |
let |
|
158 |
val (cv, cta) = Thm.dest_abs NONE ct |
|
159 |
val (v, _) = dest_Free (term_of cv) |
|
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
160 |
val u_th = introduce_combinators_in_cterm cta |
37349 | 161 |
val cu = Thm.rhs_of u_th |
162 |
val comb_eq = abstract (Thm.cabs cv cu) |
|
163 |
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end |
|
164 |
| _ $ _ => |
|
165 |
let val (ct1, ct2) = Thm.dest_comb ct in |
|
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
166 |
Thm.combination (introduce_combinators_in_cterm ct1) |
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
167 |
(introduce_combinators_in_cterm ct2) |
37349 | 168 |
end |
169 |
||
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
170 |
fun introduce_combinators_in_theorem th = |
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset
|
171 |
if is_quasi_lambda_free (prop_of th) then |
37349 | 172 |
th |
24827 | 173 |
else |
37349 | 174 |
let |
175 |
val th = Drule.eta_contraction_rule th |
|
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset
|
176 |
val eqth = introduce_combinators_in_cterm (cprop_of th) |
37349 | 177 |
in Thm.equal_elim eqth th end |
178 |
handle THM (msg, _, _) => |
|
179 |
(warning ("Error in the combinator translation of " ^ |
|
180 |
Display.string_of_thm_without_context th ^ |
|
181 |
"\nException message: " ^ msg ^ "."); |
|
182 |
(* A type variable of sort "{}" will make abstraction fail. *) |
|
183 |
TrueI) |
|
16009 | 184 |
|
185 |
(*cterms are used throughout for efficiency*) |
|
38280 | 186 |
val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; |
16009 | 187 |
|
188 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
189 |
ones. Return the body, along with the list of free variables.*) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
190 |
fun c_variant_abs_multi (ct0, vars) = |
16009 | 191 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
192 |
in c_variant_abs_multi (ct, cv::vars) end |
|
193 |
handle CTERM _ => (ct0, rev vars); |
|
194 |
||
39355 | 195 |
val skolem_def_raw = @{thms skolem_def_raw} |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
196 |
|
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
197 |
(* Given the definition of a Skolem function, return a theorem to replace |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
198 |
an existential formula by a use of that function. |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
199 |
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
200 |
fun old_skolem_theorem_from_def thy rhs0 = |
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset
|
201 |
let |
38280 | 202 |
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
203 |
val rhs' = rhs |> Thm.dest_comb |> snd |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
204 |
val (ch, frees) = c_variant_abs_multi (rhs', []) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
205 |
val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
206 |
val T = |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
207 |
case hilbert of |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
208 |
Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T |
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
209 |
| _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"", |
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset
|
210 |
[hilbert]) |
38280 | 211 |
val cex = cterm_of thy (HOLogic.exists_const T) |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
212 |
val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) |
37629 | 213 |
val conc = |
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
214 |
Drule.list_comb (rhs, frees) |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
215 |
|> Drule.beta_conv cabs |> Thm.capply cTrueprop |
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
216 |
fun tacf [prem] = |
39355 | 217 |
rewrite_goals_tac skolem_def_raw |
218 |
THEN rtac ((prem |> rewrite_rule skolem_def_raw) RS @{thm someI_ex}) 1 |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
219 |
in |
37629 | 220 |
Goal.prove_internal [ex_tm] conc tacf |
221 |
|> forall_intr_list frees |
|
222 |
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
|
223 |
|> Thm.varifyT_global |
|
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset
|
224 |
end |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
225 |
|
39036
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
226 |
fun to_definitional_cnf_with_quantifiers thy th = |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
227 |
let |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
228 |
val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
229 |
val eqth = eqth RS @{thm eq_reflection} |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
230 |
val eqth = eqth RS @{thm TruepropI} |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
231 |
in Thm.equal_elim eqth th end |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38864
diff
changeset
|
232 |
|
39897 | 233 |
fun zapped_var_name ax_no (cluster_no, skolem) s = |
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39894
diff
changeset
|
234 |
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ |
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
235 |
"_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s |
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39894
diff
changeset
|
236 |
|
39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
237 |
fun cluster_of_zapped_var_name s = |
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset
|
238 |
((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)), |
39897 | 239 |
String.isPrefix new_skolem_var_prefix s) |
240 |
||
39905
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
241 |
fun rename_vars_to_be_zapped ax_no = |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
242 |
let |
39905
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
243 |
fun aux (cluster as (cluster_no, cluster_skolem)) pos t = |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
244 |
case t of |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
245 |
(t1 as Const (s, _)) $ Abs (s', T, t') => |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
246 |
if s = @{const_name all} orelse s = @{const_name All} orelse |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
247 |
s = @{const_name Ex} then |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
248 |
let |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
249 |
val skolem = (pos = (s = @{const_name Ex})) |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
250 |
val cluster = |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
251 |
if skolem = cluster_skolem then cluster |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
252 |
else (cluster_no |> cluster_skolem ? Integer.add 1, skolem) |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
253 |
val s' = zapped_var_name ax_no cluster s' |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
254 |
in t1 $ Abs (s', T, aux cluster pos t') end |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
255 |
else |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
256 |
t |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
257 |
| (t1 as Const (s, _)) $ t2 $ t3 => |
39906 | 258 |
if s = @{const_name "==>"} orelse s = @{const_name implies} then |
39905
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
259 |
t1 $ aux cluster (not pos) t2 $ aux cluster pos t3 |
39906 | 260 |
else if s = @{const_name conj} orelse s = @{const_name disj} then |
39905
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
261 |
t1 $ aux cluster pos t2 $ aux cluster pos t3 |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
262 |
else |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
263 |
t |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
264 |
| (t1 as Const (s, _)) $ t2 => |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
265 |
if s = @{const_name Trueprop} then t1 $ aux cluster pos t2 |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
266 |
else if s = @{const_name Not} then t1 $ aux cluster (not pos) t2 |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
267 |
else t |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
268 |
| _ => t |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
269 |
in aux (0, true) true end |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
270 |
|
39906 | 271 |
fun zap pos ct = |
272 |
ct |
|
273 |
|> (case term_of ct of |
|
274 |
Const (s, _) $ Abs (s', _, _) => |
|
275 |
if s = @{const_name all} orelse s = @{const_name All} orelse |
|
276 |
s = @{const_name Ex} then |
|
277 |
Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos |
|
278 |
else |
|
279 |
Conv.all_conv |
|
280 |
| Const (s, _) $ _ $ _ => |
|
281 |
if s = @{const_name "==>"} orelse s = @{const_name implies} then |
|
282 |
Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |
|
283 |
else if s = @{const_name conj} orelse s = @{const_name disj} then |
|
284 |
Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) |
|
285 |
else |
|
286 |
Conv.all_conv |
|
287 |
| Const (s, _) $ _ => |
|
288 |
if s = @{const_name Trueprop} then Conv.arg_conv (zap pos) |
|
289 |
else if s = @{const_name Not} then Conv.arg_conv (zap (not pos)) |
|
290 |
else Conv.all_conv |
|
291 |
| _ => Conv.all_conv) |
|
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
292 |
|
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
293 |
fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
294 |
|
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
295 |
val no_choice = |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
296 |
@{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"} |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
297 |
|> Logic.varify_global |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
298 |
|> Skip_Proof.make_thm @{theory} |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
299 |
|
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
300 |
(* Converts an Isabelle theorem into NNF. *) |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
301 |
fun nnf_axiom choice_ths new_skolemizer ax_no th ctxt = |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
302 |
let |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
303 |
val thy = ProofContext.theory_of ctxt |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
304 |
val th = |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
305 |
th |> transform_elim_theorem |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
306 |
|> zero_var_indexes |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
307 |
|> new_skolemizer ? forall_intr_vars |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
308 |
val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
309 |
val th = th |> Conv.fconv_rule Object_Logic.atomize |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
310 |
|> extensionalize_theorem |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
311 |
|> Meson.make_nnf ctxt |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
312 |
in |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
313 |
if new_skolemizer then |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
314 |
let |
39905
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
315 |
val t = concl_of th |
0bfaaa81fc62
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
blanchet
parents:
39904
diff
changeset
|
316 |
val th = Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t) th |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
317 |
fun skolemize choice_ths = |
39904 | 318 |
Meson.skolemize_with_choice_thms ctxt choice_ths |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
319 |
#> simplify (ss_only @{thms all_simps[symmetric]}) |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
320 |
val pull_out = |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
321 |
simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
322 |
val (discharger_th, fully_skolemized_th) = |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
323 |
if null choice_ths then |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
324 |
(th |> pull_out, th |> skolemize [no_choice]) |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
325 |
else |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
326 |
th |> skolemize choice_ths |> `I |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
327 |
val t = |
39906 | 328 |
fully_skolemized_th |> cprop_of |
329 |
|> zap true |> Drule.export_without_context |
|
330 |
|> cprop_of |> Thm.dest_equals |> snd |> term_of |
|
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
331 |
in |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
332 |
if exists_subterm (fn Var ((s, _), _) => |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
333 |
String.isPrefix new_skolem_var_prefix s |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
334 |
| _ => false) t then |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
335 |
let |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
336 |
val (ct, ctxt) = |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
337 |
Variable.import_terms true [t] ctxt |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
338 |
|>> the_single |>> cterm_of thy |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
339 |
in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
340 |
else |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
341 |
(NONE, th, ctxt) |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
342 |
end |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
343 |
else |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
344 |
(NONE, th, ctxt) |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
345 |
end |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
346 |
|
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
347 |
(* Convert a theorem to CNF, with additional premises due to skolemization. *) |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
348 |
fun cnf_axiom ctxt0 new_skolemizer ax_no th = |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset
|
349 |
let |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
350 |
val thy = ProofContext.theory_of ctxt0 |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
351 |
val choice_ths = Meson_Choices.get ctxt0 |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
352 |
val (opt, nnf_th, ctxt) = nnf_axiom choice_ths new_skolemizer ax_no th ctxt0 |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
353 |
fun clausify th = |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
354 |
Meson.make_cnf (if new_skolemizer then |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
355 |
[] |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
356 |
else |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
357 |
map (old_skolem_theorem_from_def thy) |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
358 |
(old_skolem_defs th)) th ctxt |
39261
b1bfb3de88fd
add cutoff beyond which facts are handled using definitional CNF
blanchet
parents:
39198
diff
changeset
|
359 |
val (cnf_ths, ctxt) = |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
360 |
clausify nnf_th |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
361 |
|> (fn ([], _) => |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
362 |
clausify (to_definitional_cnf_with_quantifiers thy nnf_th) |
39268
a56f931fffff
use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way
blanchet
parents:
39261
diff
changeset
|
363 |
| p => p) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
364 |
fun intr_imp ct th = |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
365 |
Thm.instantiate ([], map (pairself (cterm_of @{theory})) |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
366 |
[(Var (("i", 1), @{typ nat}), |
39902 | 367 |
HOLogic.mk_nat ax_no)]) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
368 |
@{thm skolem_COMBK_D} |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
369 |
RS Thm.implies_intr ct th |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset
|
370 |
in |
39897 | 371 |
(opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) |
372 |
##> (term_of #> HOLogic.dest_Trueprop |
|
373 |
#> singleton (Variable.export_terms ctxt ctxt0))), |
|
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
374 |
cnf_ths |> map (introduce_combinators_in_theorem |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset
|
375 |
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |
39897 | 376 |
|> Variable.export ctxt ctxt0 |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
377 |
|> Meson.finish_cnf |
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
378 |
|> map Thm.close_derivation) |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset
|
379 |
end |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
380 |
handle THM _ => (NONE, []) |
27184 | 381 |
|
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
382 |
fun meson_general_tac ctxt ths = |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
383 |
let val ctxt = Classical.put_claset HOL_cs ctxt in |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
384 |
Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths) |
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset
|
385 |
end |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
386 |
|
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
387 |
val setup = |
39891
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
388 |
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt => |
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
389 |
SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths))) |
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
390 |
"MESON resolution proof procedure" |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39561
diff
changeset
|
391 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
392 |
end; |