author  blanchet 
Wed, 23 Mar 2011 10:18:42 +0100  
changeset 42072  1492ee6b8085 
parent 41225  bd4ecd48c21f 
child 42083  e1209fc7ecdc 
child 42098  f978caf60bbe 
permissions  rwrr 
39941  1 
(* Title: HOL/Tools/Meson/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 

39941  5 
Transformation of HOL theorems 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 
39932
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

15 
val cluster_of_zapped_var_name : string > (int * (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 
21505  18 
end; 
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

19 

39890  20 
structure Meson_Clausify : MESON_CLAUSIFY = 
15997  21 
struct 
15347  22 

39950  23 
open Meson 
24 

42072
1492ee6b8085
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents:
41225
diff
changeset

25 
(* the extra "Meson" helps prevent clashes (FIXME) *) 
1492ee6b8085
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents:
41225
diff
changeset

26 
val new_skolem_var_prefix = "MesonSK" 
1492ee6b8085
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet
parents:
41225
diff
changeset

27 
val new_nonskolem_var_prefix = "MesonV" 
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 FirstOrder 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 elimrule 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 etaexpansion 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 
39962
d42ddd7407ca
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet
parents:
39950
diff
changeset

51 
Const (@{const_name Meson.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 

39931  54 
fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') 
55 
 beta_eta_in_abs_body t = Envir.beta_eta_contract t 

37512
ff72d3ddc898
this looks like the most appropriate place to do the betaetacontraction
blanchet
parents:
37511
diff
changeset

56 

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

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

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

59 
let 
39376  60 
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

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

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

63 
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

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

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

66 
list_abs_free (map dest_Free args, 
39931  67 
HOLogic.choice_const T $ beta_eta_in_abs_body body) 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset

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

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

70 
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

71 
 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

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

73 
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

74 
in dec_sko (subst_bound (Free(fname,T), p)) rhss end 
39906  75 
 dec_sko (@{const conj} $ p $ q) rhss = rhss > dec_sko p > dec_sko q 
76 
 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

77 
 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

78 
 dec_sko _ rhss = rhss 
20419  79 
in dec_sko (prop_of th) [] end; 
80 

81 

24827  82 
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) 
20419  83 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39268
diff
changeset

84 
val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]} 
20419  85 

38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset

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

87 
(Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) 
38000
c0b9efa8bfca
added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
blanchet
parents:
37995
diff
changeset

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

89 
case prop_of th of 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset

90 
_ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _])) 
39376  91 
$ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all) 
37540
48273d1ea331
better etaexpansion in Sledgehammer's clausification;
blanchet
parents:
37518
diff
changeset

92 
 _ => th 
20419  93 

39962
d42ddd7407ca
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet
parents:
39950
diff
changeset

94 
fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true 
37416
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 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38280
diff
changeset

104 
(* FIXME: Requires more use of cterm constructors. *) 
24827  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) 
38005
b6555e9c5de4
prevent schematic variable clash in combinatorintroduction code, when invoked from Sledgehammer (another consequence of the CNF > FOF transition)
blanchet
parents:
38001
diff
changeset

110 
val cxT = ctyp_of thy xT 
b6555e9c5de4
prevent schematic variable clash in combinatorintroduction code, when invoked from Sledgehammer (another consequence of the CNF > FOF transition)
blanchet
parents:
38001
diff
changeset

111 
val cbodyT = ctyp_of thy bodyT 
b6555e9c5de4
prevent schematic variable clash in combinatorintroduction code, when invoked from Sledgehammer (another consequence of the CNF > FOF transition)
blanchet
parents:
38001
diff
changeset

112 
fun makeK () = 
b6555e9c5de4
prevent schematic variable clash in combinatorintroduction code, when invoked from Sledgehammer (another consequence of the CNF > FOF transition)
blanchet
parents:
38001
diff
changeset

113 
instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] 
b6555e9c5de4
prevent schematic variable clash in combinatorintroduction code, when invoked from Sledgehammer (another consequence of the CNF > FOF transition)
blanchet
parents:
38001
diff
changeset

114 
@{thm abs_K} 
24827  115 
in 
116 
case body of 

117 
Const _ => makeK() 

118 
 Free _ => makeK() 

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

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

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

124 
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

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

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

129 
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

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

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

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

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

136 
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

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

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

141 
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

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

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

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

149 

37349  150 
(* Traverse a theorem, remplacing lambdaabstractions with combinators. *) 
38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset

151 
fun introduce_combinators_in_cterm ct = 
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

152 
if is_quasi_lambda_free (term_of ct) then 
37349  153 
Thm.reflexive ct 
154 
else case term_of ct of 

155 
Abs _ => 

156 
let 

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

158 
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

159 
val u_th = introduce_combinators_in_cterm cta 
37349  160 
val cu = Thm.rhs_of u_th 
161 
val comb_eq = abstract (Thm.cabs cv cu) 

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

163 
 _ $ _ => 

164 
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

165 
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

166 
(introduce_combinators_in_cterm ct2) 
37349  167 
end 
168 

38001
a9b47b85ca24
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents:
38000
diff
changeset

169 
fun introduce_combinators_in_theorem th = 
37416
d5ac8280497e
no point in introducing combinators for inlined Skolem functions
blanchet
parents:
37410
diff
changeset

170 
if is_quasi_lambda_free (prop_of th) then 
37349  171 
th 
24827  172 
else 
37349  173 
let 
174 
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

175 
val eqth = introduce_combinators_in_cterm (cprop_of th) 
37349  176 
in Thm.equal_elim eqth th end 
177 
handle THM (msg, _, _) => 

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

179 
Display.string_of_thm_without_context th ^ 

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

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

182 
TrueI) 

16009  183 

184 
(*cterms are used throughout for efficiency*) 

38280  185 
val cTrueprop = cterm_of @{theory HOL} HOLogic.Trueprop; 
16009  186 

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

188 
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

189 
fun c_variant_abs_multi (ct0, vars) = 
16009  190 
let val (cv,ct) = Thm.dest_abs NONE ct0 
191 
in c_variant_abs_multi (ct, cv::vars) end 

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

193 

39355  194 
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

195 

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

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

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

198 
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

199 
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

200 
let 
38280  201 
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

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

203 
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

204 
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

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

206 
case hilbert of 
39941  207 
Const (_, Type (@{type_name fun}, [_, T])) => T 
39886
8a9f0c97d550
first step towards a new skolemizer that doesn't require "Eps"
blanchet
parents:
39721
diff
changeset

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

209 
[hilbert]) 
38280  210 
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

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

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

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

215 
fun tacf [prem] = 
39355  216 
rewrite_goals_tac skolem_def_raw 
39941  217 
THEN rtac ((prem > rewrite_rule skolem_def_raw) 
39949  218 
RS Global_Theory.get_thm thy "Hilbert_Choice.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 sideeffect 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 

39932
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

233 
fun zapped_var_name ((ax_no, cluster_no), skolem) index_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

234 
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ 
39932
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

235 
"_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40260
diff
changeset

236 
string_of_int index_no ^ "_" ^ Name.desymbolize false s 
39896
13b3a2ba9ea7
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
blanchet
parents:
39894
diff
changeset

237 

39899
608b108ec979
compute quantifier dependency graph in new skolemizer
blanchet
parents:
39897
diff
changeset

238 
fun cluster_of_zapped_var_name s = 
39932
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

239 
let val get_int = the o Int.fromString o nth (space_explode "_" s) in 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

240 
((get_int 1, (get_int 2, get_int 3)), 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

241 
String.isPrefix new_skolem_var_prefix s) 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

242 
end 
39897  243 

40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

244 
fun rename_bound_vars_to_be_zapped ax_no = 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

245 
let 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

246 
fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t = 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

247 
case t of 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

248 
(t1 as Const (s, _)) $ Abs (s', T, t') => 
39906  249 
if s = @{const_name all} orelse s = @{const_name All} orelse 
250 
s = @{const_name Ex} then 

39932
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

251 
let 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

252 
val skolem = (pos = (s = @{const_name Ex})) 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

253 
val (cluster, index_no) = 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

254 
if skolem = cluster_skolem then (cluster, index_no) 
acde1b606b0e
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
blanchet
parents:
39931
diff
changeset

255 
else ((cluster_no > cluster_skolem ? Integer.add 1, skolem), 0) 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

256 
val s' = zapped_var_name cluster index_no s' 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

257 
in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

258 
else 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

259 
t 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

260 
 (t1 as Const (s, _)) $ t2 $ t3 => 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

261 
if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

262 
t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

263 
else if s = @{const_name HOL.conj} orelse 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

264 
s = @{const_name HOL.disj} then 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

265 
t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

266 
else 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

267 
t 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

268 
 (t1 as Const (s, _)) $ t2 => 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

269 
if s = @{const_name Trueprop} then 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

270 
t1 $ aux cluster index_no pos t2 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

271 
else if s = @{const_name Not} then 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

272 
t1 $ aux cluster index_no (not pos) t2 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

273 
else 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

274 
t 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

275 
 _ => t 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

276 
in aux ((ax_no, 0), true) 0 true end 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

277 

73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

278 
fun zap pos ct = 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

279 
ct 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

280 
> (case term_of ct of 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

281 
Const (s, _) $ Abs (s', _, _) => 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

282 
if s = @{const_name all} orelse s = @{const_name All} orelse 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

283 
s = @{const_name Ex} then 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

284 
Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos 
39906  285 
else 
286 
Conv.all_conv 

287 
 Const (s, _) $ _ $ _ => 

288 
if s = @{const_name "==>"} orelse s = @{const_name implies} then 

40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

289 
Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) 
39906  290 
else if s = @{const_name conj} orelse s = @{const_name disj} then 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

291 
Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) 
39906  292 
else 
293 
Conv.all_conv 

294 
 Const (s, _) $ _ => 

40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

295 
if s = @{const_name Trueprop} then Conv.arg_conv (zap pos) 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

296 
else if s = @{const_name Not} then Conv.arg_conv (zap (not pos)) 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

297 
else Conv.all_conv 
39906  298 
 _ => Conv.all_conv) 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

299 

41225  300 
fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths 
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset

301 

40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40260
diff
changeset

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

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

304 
> Logic.varify_global 
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39900
diff
changeset

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

306 

74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

308 
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

309 
let 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

310 
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

311 
val th = 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

312 
th > transform_elim_theorem 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

313 
> zero_var_indexes 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

315 
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

316 
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

317 
> extensionalize_theorem 
39950  318 
> make_nnf ctxt 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

319 
in 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

320 
if new_skolemizer then 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

322 
fun skolemize choice_ths = 
39950  323 
skolemize_with_choice_theorems 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

324 
#> 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

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

326 
simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40260
diff
changeset

327 
val no_choice = null choice_ths 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

328 
val discharger_th = 
40261
7a02144874f3
more work on new Skolemizer without Hilbert_Choice
blanchet
parents:
40260
diff
changeset

329 
th > (if no_choice then pull_out else skolemize choice_ths) 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

330 
val fully_skolemized_t = 
40263  331 
discharger_th > prop_of > rename_bound_vars_to_be_zapped ax_no 
332 
> (if no_choice then 

333 
Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> cprop_of 

334 
else 

335 
cterm_of thy) 

336 
> zap true > Drule.export_without_context 

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

338 
in 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

339 
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

340 
String.isPrefix new_skolem_var_prefix s 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

341 
 _ => false) fully_skolemized_t then 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

342 
let 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

343 
val (fully_skolemized_ct, ctxt) = 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

344 
Variable.import_terms true [fully_skolemized_t] ctxt 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

345 
>> the_single >> cterm_of thy 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

346 
in 
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

347 
(SOME (discharger_th, fully_skolemized_ct), 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
40261
diff
changeset

348 
(Thm.assume fully_skolemized_ct, ctxt)) 
40260
73ecbe2d432b
fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62)
blanchet
parents:
39962
diff
changeset

349 
end 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

351 
(NONE, (th, ctxt)) 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

352 
end 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

354 
(NONE, (th, ctxt)) 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

355 
end 
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

356 

74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

358 
fun cnf_axiom ctxt0 new_skolemizer ax_no th = 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

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

360 
val thy = ProofContext.theory_of ctxt0 
39950  361 
val choice_ths = choice_theorems thy 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
40261
diff
changeset

362 
val (opt, (nnf_th, ctxt)) = 
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
40261
diff
changeset

363 
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

364 
fun clausify th = 
39950  365 
make_cnf (if new_skolemizer orelse null choice_ths then 
366 
[] 

367 
else 

368 
map (old_skolem_theorem_from_def thy) 

369 
(old_skolem_defs th)) th ctxt 

39261
b1bfb3de88fd
add cutoff beyond which facts are handled using definitional CNF
blanchet
parents:
39198
diff
changeset

370 
val (cnf_ths, ctxt) = 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset

371 
clausify nnf_th 
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset

372 
> (fn ([], _) => 
40262
8403085384eb
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
blanchet
parents:
40261
diff
changeset

373 
(* FIXME: This probably doesn't work with the new Skolemizer *) 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset

374 
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

375 
 p => p) 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset

376 
fun intr_imp ct th = 
39950  377 
Thm.instantiate ([], map (pairself (cterm_of thy)) 
39962
d42ddd7407ca
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet
parents:
39950
diff
changeset

378 
[(Var (("i", 0), @{typ nat}), 
39902  379 
HOLogic.mk_nat ax_no)]) 
39962
d42ddd7407ca
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet
parents:
39950
diff
changeset

380 
(zero_var_indexes @{thm skolem_COMBK_D}) 
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39891
diff
changeset

381 
RS Thm.implies_intr ct th 
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37620
diff
changeset

382 
in 
39897  383 
(opt > Option.map (I #>> singleton (Variable.export ctxt ctxt0) 
384 
##> (term_of #> HOLogic.dest_Trueprop 

385 
#> 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

386 
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

387 
#> (case opt of SOME (_, ct) => intr_imp ct  NONE => I)) 
39897  388 
> Variable.export ctxt ctxt0 
39950  389 
> finish_cnf 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

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

391 
end 
39887
74939e2afb95
second step in introducing the new Skolemizer  notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset

392 
handle THM _ => (NONE, []) 
27184  393 

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

394 
end; 