author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37629  a4f129820562 
child 37995  06f02b15ef8a 
permissions  rwrr 
37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/clausifier.ML 
33311  2 
Author: Jia Meng, Cambridge University Computer Laboratory 
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 

37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset

8 
signature CLAUSIFIER = 
21505  9 
sig 
37628  10 
val cnf_axiom: theory > bool > thm > thm list 
37620
537beae999d7
remove obsolete component of CNF clause tuple (and reorder it)
blanchet
parents:
37618
diff
changeset

11 
val cnf_rules_pairs : 
37628  12 
theory > bool > (string * thm) list > ((string * int) * thm) list 
36398
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset

13 
val neg_clausify: thm > thm list 
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset

14 
val neg_conjecture_clauses: 
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset

15 
Proof.context > thm > int > thm list list * (string * typ) list 
21505  16 
end; 
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

17 

37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset

18 
structure Clausifier : CLAUSIFIER = 
15997  19 
struct 
15347  20 

15997  21 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  22 

29064  23 
val cfalse = cterm_of @{theory HOL} HOLogic.false_const; 
24 
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

25 

21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

26 
(*Converts an elimrule into an equivalent theorem that does not have the 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

27 
predicate variable. Leaves other theorems unchanged. We simply instantiate the 
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

28 
conclusion variable to False.*) 
16009  29 
fun transform_elim th = 
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

30 
case concl_of th of (*conclusion variable*) 
35963  31 
@{const Trueprop} $ (v as Var (_, @{typ bool})) => 
29064  32 
Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th 
35963  33 
 v as Var(_, @{typ prop}) => 
29064  34 
Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th 
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset

35 
 _ => th; 
15997  36 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

37 
(*To enforce singlethreading*) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

38 
exception Clausify_failure of theory; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

39 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

40 

16009  41 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
42 

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

43 
fun mk_skolem_id t = 
37436  44 
let val T = fastype_of t in 
37496
9ae78e12e126
reintroduce new Sledgehammer polymorphic handling code;
blanchet
parents:
37488
diff
changeset

45 
Const (@{const_name skolem_id}, T > T) $ t 
37436  46 
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

47 

37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

48 
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

49 
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

50 
 beta_eta_under_lambdas t = Envir.beta_eta_contract t 
37512
ff72d3ddc898
this looks like the most appropriate place to do the betaetacontraction
blanchet
parents:
37511
diff
changeset

51 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

52 
(*Traverse a theorem, accumulating Skolem function definitions.*) 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

53 
fun assume_skolem_funs th = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset

54 
let 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

55 
fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset

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

57 
let 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

58 
val args = OldTerm.term_frees body 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset

59 
val Ts = map type_of args 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset

60 
val cT = Ts > T (* FIXME: use "skolem_type_and_args" *) 
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

61 
(* Forms a lambdaabstraction 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

62 
val rhs = 
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

63 
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

64 
HOLogic.choice_const T $ beta_eta_under_lambdas body) 
37518
efb0923cc098
use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents:
37512
diff
changeset

65 
> mk_skolem_id 
efb0923cc098
use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
blanchet
parents:
37512
diff
changeset

66 
val comb = list_comb (rhs, args) 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

67 
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

68 
 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

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

70 
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

71 
in dec_sko (subst_bound (Free(fname,T), p)) rhss end 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

72 
 dec_sko (@{const "op &"} $ p $ q) rhss = rhss > dec_sko p > dec_sko q 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

73 
 dec_sko (@{const "op "} $ p $ q) rhss = rhss > dec_sko p > dec_sko q 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

74 
 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

75 
 dec_sko _ rhss = rhss 
20419  76 
in dec_sko (prop_of th) [] end; 
77 

78 

24827  79 
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) 
20419  80 

81 
(*Returns the vars of a theorem*) 

82 
fun vars_of_thm th = 

22691  83 
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); 
20419  84 

37540
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

85 
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} 
20419  86 

37540
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

87 
(* Removes the lambdas from an equation of the form t = (%x. u). *) 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

88 
fun extensionalize th = 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

89 
case prop_of th of 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

90 
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _])) 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

91 
$ _ $ Abs (s, _, _)) => extensionalize (th RS fun_cong_all) 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

92 
 _ => th 
20419  93 

37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

94 
fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true 
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

95 
 is_quasi_lambda_free (t1 $ t2) = 
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

96 
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

97 
 is_quasi_lambda_free (Abs _) = false 
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

98 
 is_quasi_lambda_free _ = true 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

99 

32010  100 
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); 
101 
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); 

102 
val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

103 

24827  104 
(*FIXME: requires more use of cterm constructors*) 
105 
fun abstract ct = 

28544
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

106 
let 
26743a1591f5
improved performance of skolem cache, due to parallel map;
wenzelm
parents:
28262
diff
changeset

107 
val thy = theory_of_cterm ct 
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset

108 
val Abs(x,_,body) = term_of ct 
35963  109 
val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) 
24827  110 
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT 
27184  111 
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} 
24827  112 
in 
113 
case body of 

114 
Const _ => makeK() 

115 
 Free _ => makeK() 

116 
 Var _ => makeK() (*though Var isn't expected*) 

27184  117 
 Bound 0 => instantiate' [SOME cxT] [] @{thm abs_I} (*identity: I*) 
24827  118 
 rator$rand => 
27184  119 
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

120 
if loose_bvar1 (rand,0) then (*S*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

121 
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

122 
val crand = cterm_of thy (Abs(x,xT,rand)) 
27184  123 
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S} 
124 
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

125 
in 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

126 
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

127 
end 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

128 
else (*C*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

129 
let val crator = cterm_of thy (Abs(x,xT,rator)) 
27184  130 
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] @{thm abs_C} 
131 
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

132 
in 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

133 
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

134 
end 
27184  135 
else if loose_bvar1 (rand,0) then (*B or eta*) 
36945  136 
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

137 
else (*B*) 
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

138 
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

139 
val crator = cterm_of thy rator 
27184  140 
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B} 
141 
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') 

37349  142 
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

143 
else makeK() 
37349  144 
 _ => raise Fail "abstract: Bad term" 
24827  145 
end; 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

146 

37349  147 
(* Traverse a theorem, remplacing lambdaabstractions with combinators. *) 
148 
fun do_introduce_combinators ct = 

37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

149 
if is_quasi_lambda_free (term_of ct) then 
37349  150 
Thm.reflexive ct 
151 
else case term_of ct of 

152 
Abs _ => 

153 
let 

154 
val (cv, cta) = Thm.dest_abs NONE ct 

155 
val (v, _) = dest_Free (term_of cv) 

156 
val u_th = do_introduce_combinators cta 

157 
val cu = Thm.rhs_of u_th 

158 
val comb_eq = abstract (Thm.cabs cv cu) 

159 
in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end 

160 
 _ $ _ => 

161 
let val (ct1, ct2) = Thm.dest_comb ct in 

162 
Thm.combination (do_introduce_combinators ct1) 

163 
(do_introduce_combinators ct2) 

164 
end 

165 

166 
fun introduce_combinators th = 

37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

167 
if is_quasi_lambda_free (prop_of th) then 
37349  168 
th 
24827  169 
else 
37349  170 
let 
171 
val th = Drule.eta_contraction_rule th 

172 
val eqth = do_introduce_combinators (cprop_of th) 

173 
in Thm.equal_elim eqth th end 

174 
handle THM (msg, _, _) => 

175 
(warning ("Error in the combinator translation of " ^ 

176 
Display.string_of_thm_without_context th ^ 

177 
"\nException message: " ^ msg ^ "."); 

178 
(* A type variable of sort "{}" will make abstraction fail. *) 

179 
TrueI) 

16009  180 

181 
(*cterms are used throughout for efficiency*) 

29064  182 
val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop; 
16009  183 

184 
(*Given an abstraction over n variables, replace the bound variables by free 

185 
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

186 
fun c_variant_abs_multi (ct0, vars) = 
16009  187 
let val (cv,ct) = Thm.dest_abs NONE ct0 
188 
in c_variant_abs_multi (ct, cv::vars) end 

189 
handle CTERM _ => (ct0, rev vars); 

190 

37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

191 
val skolem_id_def_raw = @{thms skolem_id_def_raw} 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

192 

f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

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

194 
an existential formula by a use of that function. 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

195 
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) 
37628  196 
fun skolem_theorem_of_def thy cheat rhs0 = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37349
diff
changeset

197 
let 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

198 
val rhs = rhs0 > Type.legacy_freeze_thaw > #1 > Thm.cterm_of thy 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

199 
val rhs' = rhs > Thm.dest_comb > snd 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

200 
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

201 
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

202 
val T = 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

203 
case hilbert of 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

204 
Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

205 
 _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [hilbert]) 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

206 
val cex = Thm.cterm_of thy (HOLogic.exists_const T) 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

207 
val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs) 
37629  208 
val conc = 
37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

209 
Drule.list_comb (rhs, frees) 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

210 
> Drule.beta_conv cabs > Thm.capply cTrueprop 
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

211 
fun tacf [prem] = 
37629  212 
if cheat then 
213 
Skip_Proof.cheat_tac thy 

214 
else 

215 
rewrite_goals_tac skolem_id_def_raw 

216 
THEN rtac ((prem > rewrite_rule skolem_id_def_raw) 

217 
RS @{thm someI_ex}) 1 

37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

218 
in 
37629  219 
Goal.prove_internal [ex_tm] conc tacf 
220 
> forall_intr_list frees 

221 
> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) 

222 
> Thm.varifyT_global 

37617
f73cd4069f69
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
blanchet
parents:
37616
diff
changeset

223 
end 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24669
diff
changeset

224 

20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

225 
(*Converts an Isabelle theorem (intro, elim or simp format, even higherorder) into NNF.*) 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

226 
fun to_nnf th ctxt0 = 
27179
8f29fed3dc9a
ResAxioms.cnf_axiom/cnf_rules_pairs: pass explicit theory context;
wenzelm
parents:
27174
diff
changeset

227 
let val th1 = th > transform_elim > zero_var_indexes 
32262  228 
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0 
37540
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

229 
val th3 = th2 > Conv.fconv_rule Object_Logic.atomize 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

230 
> extensionalize 
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

231 
> Meson.make_nnf ctxt 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset

232 
in (th3, ctxt) end; 
16009  233 

27184  234 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
37628  235 
fun skolemize_theorem thy cheat th = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

236 
let 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

237 
val ctxt0 = Variable.global_thm_context th 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

238 
val (nnfth, ctxt) = to_nnf th ctxt0 
37628  239 
val sko_ths = map (skolem_theorem_of_def thy cheat) 
240 
(assume_skolem_funs nnfth) 

37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

241 
val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

242 
in 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

243 
cnfs > map introduce_combinators 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

244 
> Variable.export ctxt ctxt0 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

245 
> Meson.finish_cnf 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

246 
> map Thm.close_derivation 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

247 
end 
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

248 
handle THM _ => [] 
27184  249 

36228
df47dc6c0e03
got rid of somewhat pointless "pairname" function in Sledgehammer
blanchet
parents:
36106
diff
changeset

250 
(* Convert Isabelle theorems into axiom clauses. *) 
37618
fa57a87f92a0
get rid of Skolem cache by performing CNFconversion after fact selection
blanchet
parents:
37617
diff
changeset

251 
(* FIXME: is transfer necessary? *) 
37628  252 
fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy 
15347  253 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

254 

22471  255 
(**** Translate a set of theorems into CNF ****) 
15347  256 

21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset

257 
(*The combination of rev and tail recursion preserves the original order*) 
37628  258 
fun cnf_rules_pairs thy cheat = 
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

259 
let 
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

260 
fun do_one _ [] = [] 
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

261 
 do_one ((name, k), th) (cls :: clss) = 
37620
537beae999d7
remove obsolete component of CNF clause tuple (and reorder it)
blanchet
parents:
37618
diff
changeset

262 
((name, k), cls) :: do_one ((name, k + 1), th) clss 
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

263 
fun do_all pairs [] = pairs 
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

264 
 do_all pairs ((name, th) :: ths) = 
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

265 
let 
37628  266 
val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th) 
37570  267 
handle THM _ => [] 
37500
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

268 
in do_all (new_pairs @ pairs) ths end 
7587b6e63454
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
blanchet
parents:
37498
diff
changeset

269 
in do_all [] o rev end 
19353  270 

19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

271 

21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

272 
(*** Converting a subgoal into negated conjecture clauses. ***) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

273 

32262  274 
fun neg_skolemize_tac ctxt = 
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

275 
EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt] 
36398
de8522a5cbae
make "neg_clausify" return a list of lists of clauses, so that it's possible to see which clause comes from which theorem
blanchet
parents:
36394
diff
changeset

276 

35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35865
diff
changeset

277 
val neg_clausify = 
37349  278 
single 
279 
#> Meson.make_clauses_unsorted 

280 
#> map introduce_combinators 

281 
#> Meson.finish_cnf 

21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

282 

32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset

283 
fun neg_conjecture_clauses ctxt st0 n = 
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32231
diff
changeset

284 
let 
37332
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

285 
(* "Option" is thrown if the assumptions contain schematic variables. *) 
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

286 
val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0 
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

287 
val ({params, prems, ...}, _) = 
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

288 
Subgoal.focus (Variable.set_body false ctxt) n st 
51d99ba6fc4d
don't raise Option.Option if assumptions contain schematic variables
blanchet
parents:
37171
diff
changeset

289 
in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset

290 

27184  291 

20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

292 
end; 