author  wenzelm 
Mon, 09 Oct 2006 02:19:54 +0200  
changeset 20902  a0034e545c13 
parent 20867  e7b92a48e22b 
child 20969  341808e0b7f2 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

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 

20445  8 
(*FIXME: does this signature serve any purpose?*) 
15997  9 
signature RES_AXIOMS = 
10 
sig 

11 
val elimRule_tac : thm > Tactical.tactic 

16012  12 
val elimR2Fol : thm > term 
15997  13 
val transform_elim : thm > thm 
14 
val cnf_axiom : (string * thm) > thm list 

15 
val meta_cnf_axiom : thm > thm list 

16 
val claset_rules_of_thy : theory > (string * thm) list 

17 
val simpset_rules_of_thy : theory > (string * thm) list 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

18 
val claset_rules_of_ctxt: Proof.context > (string * thm) list 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

19 
val simpset_rules_of_ctxt : Proof.context > (string * thm) list 
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
17829
diff
changeset

20 
val pairname : thm > (string * thm) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

21 
val skolem_thm : thm > thm list 
20419  22 
val to_nnf : thm > thm 
19353  23 
val cnf_rules_pairs : (string * Thm.thm) list > (Thm.thm * (string * int)) list list; 
18708  24 
val meson_method_setup : theory > theory 
25 
val setup : theory > theory 

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

26 

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

27 
val atpset_rules_of_thy : theory > (string * thm) list 
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

28 
val atpset_rules_of_ctxt : Proof.context > (string * thm) list 
15997  29 
end; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

30 

20419  31 
structure ResAxioms = 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

32 

15997  33 
struct 
15347  34 

20419  35 
(*FIXME DELETE: For running the comparison between combinators and abstractions. 
36 
CANNOT be a ref, as the setting is used while Isabelle is built.*) 

37 
val abstract_lambdas = true; 

38 

39 
val trace_abs = ref false; 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

40 

20902  41 
(* FIXME legacy *) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

42 
fun freeze_thm th = #1 (Drule.freeze_thaw th); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

43 

20902  44 
val lhs_of = #1 o Logic.dest_equals o Thm.prop_of; 
45 
val rhs_of = #2 o Logic.dest_equals o Thm.prop_of; 

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

46 

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

47 

20445  48 
(*Store definitions of abstraction functions, ensuring that identical righthand 
49 
sides are denoted by the same functions and thereby reducing the need for 

50 
extensionality in proofs. 

51 
FIXME! Store in theory data!!*) 

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

52 

20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

53 
(*Populate the abstraction cache with common combinators.*) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

54 
fun seed th net = 
20902  55 
let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th) 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

56 
val t = Logic.legacy_varify (term_of ct) 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

57 
in Net.insert_term eq_thm (t, th) net end; 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

58 

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

59 
val abstraction_cache = ref 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

60 
(seed (thm"Reconstruction.I_simp") 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

61 
(seed (thm"Reconstruction.B_simp") 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

62 
(seed (thm"Reconstruction.K_simp") Net.empty))); 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

63 

20445  64 

15997  65 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  66 

15390  67 
(* a tactic used to prove an elimrule. *) 
16009  68 
fun elimRule_tac th = 
20419  69 
(resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1); 
15347  70 

15956  71 
fun add_EX tm [] = tm 
72 
 add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; 

15347  73 

19894  74 
(*Checks for the premise ~P when the conclusion is P.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

75 
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) 
19894  76 
(Const("Trueprop",_) $ Free(q,_)) = (p = q) 
15371  77 
 is_neg _ _ = false; 
78 

20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

79 
exception ELIMR2FOL; 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

80 

a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

81 
(*Handles the case where the dummy "conclusion" variable appears negated in the 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

82 
premises, so the final consequent must be kept.*) 
15371  83 
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = 
19894  84 
strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

85 
 strip_concl' prems bvs P = 
15956  86 
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) 
19894  87 
in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; 
15371  88 

20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

89 
(*Recurrsion over the minor premise of an elimination rule. Final consequent 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

90 
is ignored, as it is the dummy "conclusion" variable.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

91 
fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

92 
strip_concl prems ((x,xtp)::bvs) concl body 
15371  93 
 strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

94 
if (is_neg P concl) then (strip_concl' prems bvs Q) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

95 
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

96 
 strip_concl prems bvs concl Q = 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

97 
if concl aconv Q then add_EX (foldr1 HOLogic.mk_conj prems) bvs 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

98 
else raise ELIMR2FOL (*expected conclusion not found!*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

99 

20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

100 
fun trans_elim (major,[],_) = HOLogic.Not $ major 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

101 
 trans_elim (major,minors,concl) = 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

102 
let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors) 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

103 
in HOLogic.mk_imp (major, disjs) end; 
15347  104 

16012  105 
(* convert an elim rule into an equivalent formula, of type term. *) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

106 
fun elimR2Fol elimR = 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

107 
let val elimR' = freeze_thm elimR 
19894  108 
val (prems,concl) = (prems_of elimR', concl_of elimR') 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

109 
val cv = case concl of (*conclusion variable*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

110 
Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

111 
 v as Free(_, Type("prop",[])) => v 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

112 
 _ => raise ELIMR2FOL 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

113 
in case prems of 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

114 
[] => raise ELIMR2FOL 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

115 
 (Const("Trueprop",_) $ major) :: minors => 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

116 
if member (op aconv) (term_frees major) cv then raise ELIMR2FOL 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

117 
else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL) 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

118 
 _ => raise ELIMR2FOL 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

119 
end; 
15347  120 

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

121 
(* convert an elimrule into an equivalent theorem that does not have the 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

122 
predicate variable. Leave other theorems unchanged.*) 
16009  123 
fun transform_elim th = 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

124 
let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th)) 
18009  125 
in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

126 
handle ELIMR2FOL => th (*not an elimination rule*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

127 
 exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

128 
" for theorem " ^ string_of_thm th); th) 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

129 

15997  130 

131 
(**** Transformation of Clasets and Simpsets into FirstOrder Axioms ****) 

132 

16563  133 
(*Transfer a theorem into theory Reconstruction.thy if it is not already 
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

134 
inside that theory  because it's needed for Skolemization *) 
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

135 

16563  136 
(*This will refer to the final version of theory Reconstruction.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

137 
val recon_thy_ref = Theory.self_ref (the_context ()); 
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

138 

16563  139 
(*If called while Reconstruction is being created, it will transfer to the 
140 
current version. If called afterward, it will transfer to the final version.*) 

16009  141 
fun transfer_to_Reconstruction th = 
16563  142 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  143 

15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

144 
fun is_taut th = 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

145 
case (prop_of th) of 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

146 
(Const ("Trueprop", _) $ Const ("True", _)) => true 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

147 
 _ => false; 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

148 

87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

149 
(* remove tautologous clauses *) 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

150 
val rm_redundant_cls = List.filter (not o is_taut); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

151 

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

152 

16009  153 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
154 

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

155 
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

156 
prefix for the Skolem constant. Result is a new theory*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

157 
fun declare_skofuns s th thy = 
20419  158 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

159 
(*Existential: declare a Skolem function, then insert into body and continue*) 
20624
ba081ac0ed7e
sko/abs: Name.internal prevents choking of print_theory;
wenzelm
parents:
20567
diff
changeset

160 
let val cname = Name.internal (gensym ("sko_" ^ s ^ "_")) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

161 
val args = term_frees xtp (*get the formal parameter list*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

162 
val Ts = map type_of args 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

163 
val cT = Ts > T 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

164 
val c = Const (Sign.full_name thy cname, cT) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

165 
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

166 
(*Forms a lambdaabstraction over the formal parameters*) 
20783  167 
val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

168 
(*Theory is augmented with the constant, then its def*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

169 
val cdef = cname ^ "_def" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

170 
val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

171 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

172 
(thy'', get_axiom thy'' cdef :: axs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

174 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

175 
(*Universal quant: insert a free variable into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

176 
let val fname = Name.variant (add_term_names (p,[])) a 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

177 
in dec_sko (subst_bound (Free(fname,T), p)) thx end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

178 
 dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

179 
 dec_sko (Const ("op ", _) $ p $ q) thx = dec_sko q (dec_sko p thx) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

180 
 dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

181 
 dec_sko t thx = thx (*Do nothing otherwise*) 
20419  182 
in dec_sko (prop_of th) (thy,[]) end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

183 

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

184 
(*Traverse a theorem, accumulating Skolem function definitions.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

185 
fun assume_skofuns th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

186 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

187 
(*Existential: declare a Skolem function, then insert into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

188 
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

189 
val args = term_frees xtp \\ skos (*the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

190 
val Ts = map type_of args 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

191 
val cT = Ts > T 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

192 
val c = Free (gensym "sko_", cT) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

193 
val rhs = list_abs_free (map dest_Free args, 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

194 
HOLogic.choice_const T $ xtp) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

195 
(*Forms a lambdaabstraction over the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

196 
val def = equals cT $ c $ rhs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

197 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

198 
(def :: defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

200 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

201 
(*Universal quant: insert a free variable into body and continue*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

202 
let val fname = Name.variant (add_term_names (p,[])) a 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

203 
in dec_sko (subst_bound (Free(fname,T), p)) defs end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

204 
 dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

205 
 dec_sko (Const ("op ", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

206 
 dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

207 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  208 
in dec_sko (prop_of th) [] end; 
209 

210 

211 
(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) 

212 

213 
(*Returns the vars of a theorem*) 

214 
fun vars_of_thm th = 

20445  215 
map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []); 
20419  216 

217 
(*Make a version of fun_cong with a given variable name*) 

218 
local 

219 
val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) 

220 
val cx = hd (vars_of_thm fun_cong'); 

221 
val ty = typ_of (ctyp_of_term cx); 

20445  222 
val thy = theory_of_thm fun_cong; 
20419  223 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
224 
in 

225 
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' 

226 
end; 

227 

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

228 
(*Removes the lambdas from an equation of the form t = (%x. u). A nonnegative n, 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

229 
serves as an upper bound on how many to remove.*) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

230 
fun strip_lambdas 0 th = th 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

231 
 strip_lambdas n th = 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

232 
case prop_of th of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

233 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

234 
strip_lambdas (n1) (freeze_thm (th RS xfun_cong x)) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

235 
 _ => th; 
20419  236 

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

237 
(*Convert meta to objectequality. Fails for theorems like split_comp_eq, 
20419  238 
where some types have the empty sort.*) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

239 
fun mk_object_eq th = th RS def_imp_eq 
20419  240 
handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

241 

20419  242 
(*Apply a function definition to an argument, betareducing the result.*) 
243 
fun beta_comb cf x = 

244 
let val th1 = combination cf (reflexive x) 

20902  245 
val th2 = beta_conversion false (Drule.rhs_of th1) 
20419  246 
in transitive th1 th2 end; 
247 

248 
(*Apply a function definition to arguments, betareducing along the way.*) 

249 
fun list_combination cf [] = cf 

250 
 list_combination cf (x::xs) = list_combination (beta_comb cf x) xs; 

251 

252 
fun list_cabs ([] , t) = t 

253 
 list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); 

254 

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

255 
fun assert_eta_free ct = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

256 
let val t = term_of ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

257 
in if (t aconv Envir.eta_contract t) then () 
20419  258 
else error ("Eta redex in term: " ^ string_of_cterm ct) 
259 
end; 

260 

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

261 
fun eq_absdef (th1, th2) = 
20445  262 
Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso 
263 
rhs_of th1 aconv rhs_of th2; 

264 

265 
fun lambda_free (Abs _) = false 

266 
 lambda_free (t $ u) = lambda_free t andalso lambda_free u 

267 
 lambda_free _ = true; 

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

268 

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

269 
fun monomorphic t = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

270 
Term.fold_types (Term.fold_atyps (fn TVar _ => K false  _ => I)) t true; 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

271 

20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

272 
fun dest_abs_list ct = 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

273 
let val (cv,ct') = Thm.dest_abs NONE ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

274 
val (cvs,cu) = dest_abs_list ct' 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

275 
in (cv::cvs, cu) end 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

276 
handle CTERM _ => ([],ct); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

277 

384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

278 
fun lambda_list [] u = u 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

279 
 lambda_list (v::vs) u = lambda v (lambda_list vs u); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

280 

384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

281 
fun abstract_rule_list [] [] th = th 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

282 
 abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

283 
 abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]); 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

284 

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

285 

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

286 
val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

287 

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

288 
(*Does an existing abstraction definition have an RHS that matches the one we need now?*) 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

289 
fun match_rhs t th = 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

290 
let val thy = theory_of_thm th 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

291 
val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^ 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

292 
" against\n" ^ string_of_thm th) else (); 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

293 
val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

294 
val term_insts = map Meson.term_pair_of (Vartab.dest tenv) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

295 
val ct_pairs = if forall lambda_free (map #2 term_insts) then 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

296 
map (pairself (cterm_of thy)) term_insts 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

297 
else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

298 
fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

299 
val th' = cterm_instantiate ct_pairs th 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

300 
in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

301 
handle _ => NONE; 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

302 

20419  303 
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested 
304 
prefix for the constants. Resulting theory is returned in the first theorem. *) 

305 
fun declare_absfuns th = 

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

306 
let fun abstract thy ct = 
20445  307 
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) 
308 
else 

309 
case term_of ct of 

20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

310 
Abs _ => 
20624
ba081ac0ed7e
sko/abs: Name.internal prevents choking of print_theory;
wenzelm
parents:
20567
diff
changeset

311 
let val cname = Name.internal (gensym "abs_"); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

312 
val _ = assert_eta_free ct; 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

313 
val (cvs,cta) = dest_abs_list ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

314 
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

315 
val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else (); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

316 
val (u'_th,defs) = abstract thy cta 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

317 
val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else (); 
20902  318 
val cu' = Drule.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

319 
val u' = term_of cu' 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

320 
val abs_v_u = lambda_list (map term_of cvs) u' 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

321 
(*get the formal parameters: ALL variables free in the term*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

322 
val args = term_frees abs_v_u 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

323 
val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else (); 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

324 
val rhs = list_abs_free (map dest_Free args, abs_v_u) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

325 
(*Forms a lambdaabstraction over the formal parameters*) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

326 
val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

327 
val (ax,ax',thy) = 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

328 
case List.mapPartial (match_rhs abs_v_u) (Net.match_term (!abstraction_cache) u') 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

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

330 
(ax,ax')::_ => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

331 
(if !trace_abs then warning ("Reusing axiom " ^ string_of_thm ax) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

332 
(ax,ax',thy)) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

333 
 [] => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

334 
let val _ = if !trace_abs then warning "Lookup was empty" else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

335 
val Ts = map type_of args 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

336 
val cT = Ts > (Tvs > typ_of (ctyp_of_term cu')) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

337 
val thy = theory_of_thm u'_th 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

338 
val c = Const (Sign.full_name thy cname, cT) 
20783  339 
val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

340 
(*Theory is augmented with the constant, 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

341 
then its definition*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

342 
val cdef = cname ^ "_def" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

343 
val thy = Theory.add_defs_i false false 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

344 
[(cdef, equals cT $ c $ rhs)] thy 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

345 
val _ = if !trace_abs then (warning ("Definition is " ^ 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

346 
string_of_thm (get_axiom thy cdef))) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

347 
else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

348 
val ax = get_axiom thy cdef > freeze_thm 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

349 
> mk_object_eq > strip_lambdas (length args) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

350 
> mk_meta_eq > Meson.generalize 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

351 
val (_,ax') = Option.valOf (match_rhs abs_v_u ax) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

352 
val _ = if !trace_abs then 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

353 
(warning ("Declaring: " ^ string_of_thm ax); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

354 
warning ("Instance: " ^ string_of_thm ax')) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

355 
else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

356 
val _ = abstraction_cache := Net.insert_term eq_absdef 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

357 
((Logic.varify u'), ax) (!abstraction_cache) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

358 
handle Net.INSERT => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

359 
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

360 
in (ax,ax',thy) end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

361 
in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

362 
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

363 
 (t1$t2) => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

364 
let val (ct1,ct2) = Thm.dest_comb ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

365 
val (th1,defs1) = abstract thy ct1 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

366 
val (th2,defs2) = abstract (theory_of_thm th1) ct2 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

367 
in (combination th1 th2, defs1@defs2) end 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

368 
val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else (); 
20419  369 
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

370 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

371 
val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

372 
in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end; 
20419  373 

20902  374 
fun name_of def = try (#1 o dest_Free o lhs_of) def; 
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset

375 

20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

376 
(*A name is valid provided it isn't the name of a defined abstraction.*) 
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset

377 
fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs)) 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

378 
 valid_name defs _ = false; 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

379 

20419  380 
fun assume_absfuns th = 
20445  381 
let val thy = theory_of_thm th 
382 
val cterm = cterm_of thy 

20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

383 
fun abstract ct = 
20445  384 
if lambda_free (term_of ct) then (reflexive ct, []) 
385 
else 

386 
case term_of ct of 

20419  387 
Abs (_,T,u) => 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

388 
let val _ = assert_eta_free ct; 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

389 
val (cvs,cta) = dest_abs_list ct 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

390 
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

391 
val (u'_th,defs) = abstract cta 
20902  392 
val cu' = Drule.rhs_of u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

393 
val u' = term_of cu' 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

394 
(*Could use Thm.cabs instead of lambda to work at level of cterms*) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

395 
val abs_v_u = lambda_list (map term_of cvs) (term_of cu') 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

396 
(*get the formal parameters: free variables not present in the defs 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

397 
(to avoid taking abstraction function names as parameters) *) 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

398 
val args = filter (valid_name defs) (term_frees abs_v_u) 
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

399 
val crhs = list_cabs (map cterm args, cterm abs_v_u) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

400 
(*Forms a lambdaabstraction over the formal parameters*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

401 
val rhs = term_of crhs 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

402 
val (ax,ax') = 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

403 
case List.mapPartial (match_rhs abs_v_u) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

404 
(Net.match_term (!abstraction_cache) u') of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

405 
(ax,ax')::_ => 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

406 
(if !trace_abs then warning ("Reusing axiom " ^ string_of_thm ax) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

407 
(ax,ax')) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

408 
 [] => 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

409 
let val Ts = map type_of args 
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambdaexpression; also, strings of lambdas
paulson
parents:
20624
diff
changeset

410 
val const_ty = Ts > (Tvs > typ_of (ctyp_of_term cu')) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

411 
val c = Free (gensym "abs_", const_ty) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

412 
val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

413 
> mk_object_eq > strip_lambdas (length args) 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

414 
> mk_meta_eq > Meson.generalize 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

415 
val (_,ax') = Option.valOf (match_rhs abs_v_u ax) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

416 
val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

417 
(!abstraction_cache) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

418 
handle Net.INSERT => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

419 
raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

420 
in (ax,ax') end 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

421 
in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

422 
(transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

423 
 (t1$t2) => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

424 
let val (ct1,ct2) = Thm.dest_comb ct 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

425 
val (t1',defs1) = abstract ct1 
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

426 
val (t2',defs2) = abstract ct2 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

427 
in (combination t1' t2', defs1@defs2) end 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

428 
val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else (); 
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset

429 
val (eqth,defs) = abstract (cprop_of th) 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

430 
val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

431 
val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else (); 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

432 
in map Drule.eta_contraction_rule ths end; 
20419  433 

16009  434 

435 
(*cterms are used throughout for efficiency*) 

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

436 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  437 

438 
(*cterm version of mk_cTrueprop*) 

439 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

440 

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

442 
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

443 
fun c_variant_abs_multi (ct0, vars) = 
16009  444 
let val (cv,ct) = Thm.dest_abs NONE ct0 
445 
in c_variant_abs_multi (ct, cv::vars) end 

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

447 

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

448 
(*Given the definition of a Skolem function, return a theorem to replace 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

450 
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

451 
fun skolem_of_def def = 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

452 
let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def)) 
16009  453 
val (ch, frees) = c_variant_abs_multi (rhs, []) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

454 
val (chilbert,cabs) = Thm.dest_comb ch 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

455 
val {sign,t, ...} = rep_cterm chilbert 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

456 
val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

457 
 _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) 
16009  458 
val cex = Thm.cterm_of sign (HOLogic.exists_const T) 
459 
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) 

460 
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); 

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

461 
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

462 
in Goal.prove_raw [ex_tm] conc tacf 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

463 
> forall_intr_list frees 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

464 
> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

465 
> Thm.varifyT 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

466 
end; 
16009  467 

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

468 
(*Converts an Isabelle theorem (intro, elim or simp format, even higherorder) into NNF.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

469 
fun to_nnf th = 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

471 
> transform_elim > zero_var_indexes > freeze_thm 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

472 
> ObjectLogic.atomize_thm > make_nnf > strip_lambdas ~1; 
16009  473 

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

474 
(*The cache prevents repeated clausification of a theorem, 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

475 
and also repeated declaration of Skolem functions*) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

476 
(* FIXME better use Termtab!? No, we MUST use theory data!!*) 
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

477 
val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

478 

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

479 

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

480 
(*Generate Skolem functions for a theorem supplied in nnf*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

481 
fun skolem_of_nnf th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

482 
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

483 

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

484 
fun assert_lambda_free ths msg = 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

485 
case filter (not o lambda_free o prop_of) ths of 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

486 
[] => () 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

487 
 ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths')); 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

488 

20445  489 
fun assume_abstract th = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

490 
if lambda_free (prop_of th) then [th] 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

491 
else th > Drule.eta_contraction_rule > assume_absfuns 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

492 
> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") 
20445  493 

20419  494 
(*Replace lambdas by assumed function definitions in the theorems*) 
20445  495 
fun assume_abstract_list ths = 
496 
if abstract_lambdas then List.concat (map assume_abstract ths) 

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

497 
else map Drule.eta_contraction_rule ths; 
20419  498 

499 
(*Replace lambdas by declared function definitions in the theorems*) 

500 
fun declare_abstract' (thy, []) = (thy, []) 

501 
 declare_abstract' (thy, th::ths) = 

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

502 
let val (thy', th_defs) = 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

503 
if lambda_free (prop_of th) then (thy, [th]) 
20445  504 
else 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

505 
th > zero_var_indexes > freeze_thm 
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

506 
> Drule.eta_contraction_rule > transfer thy > declare_absfuns 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

507 
val _ = assert_lambda_free th_defs "declare_abstract: lambdas" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

508 
val (thy'', ths') = declare_abstract' (thy', ths) 
20419  509 
in (thy'', th_defs @ ths') end; 
510 

20421  511 
(*FIXME DELETE if we decide to switch to abstractions*) 
20419  512 
fun declare_abstract (thy, ths) = 
513 
if abstract_lambdas then declare_abstract' (thy, ths) 

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

514 
else (thy, map Drule.eta_contraction_rule ths); 
20419  515 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

516 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

517 
(*also works for HOL*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

518 
fun skolem_thm th = 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

519 
let val nnfth = to_nnf th 
20419  520 
in Meson.make_cnf (skolem_of_nnf nnfth) nnfth 
20445  521 
> assume_abstract_list > Meson.finish_cnf > rm_redundant_cls 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

522 
end 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

523 
handle THM _ => []; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

524 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

525 
(*Declare Skolem functions for a theorem, supplied in nnf and with its name. 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

526 
It returns a modified theory, unless skolemization fails.*) 
16009  527 
fun skolem thy (name,th) = 
20419  528 
let val cname = (case name of "" => gensym ""  s => Sign.base_name s) 
529 
val _ = Output.debug ("skolemizing " ^ name ^ ": ") 

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

530 
in Option.map 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

531 
(fn nnfth => 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

532 
let val (thy',defs) = declare_skofuns cname nnfth thy 
20419  533 
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth 
534 
val (thy'',cnfs') = declare_abstract (thy',cnfs) 

535 
in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs')) 

536 
end) 

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

537 
(SOME (to_nnf th) handle THM _ => NONE) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

538 
end; 
16009  539 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

540 
(*Populate the clause cache using the supplied theorem. Return the clausal form 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

541 
and modified theory.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

542 
fun skolem_cache_thm (name,th) thy = 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

543 
case Symtab.lookup (!clause_cache) name of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

544 
NONE => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

545 
(case skolem thy (name, Thm.transfer thy th) of 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

546 
NONE => ([th],thy) 
20473
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

547 
 SOME (thy',cls) => 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

548 
let val cls = map Drule.local_standard cls 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

549 
in 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

550 
if null cls then warning ("skolem_cache: empty clause set for " ^ name) 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

551 
else (); 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

552 
change clause_cache (Symtab.update (name, (th, cls))); 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

553 
(cls,thy') 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

554 
end) 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

555 
 SOME (th',cls) => 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

556 
if eq_thm(th,th') then (cls,thy) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

557 
else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

558 
Output.debug (string_of_thm th); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

559 
Output.debug (string_of_thm th'); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

560 
([th],thy)); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

561 

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

562 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
19894  563 
fun cnf_axiom (name,th) = 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

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

565 
"" => skolem_thm th (*no name, so can't cache*) 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

566 
 s => case Symtab.lookup (!clause_cache) s of 
20473
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

567 
NONE => 
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset

568 
let val cls = map Drule.local_standard (skolem_thm th) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

569 
in change clause_cache (Symtab.update (s, (th, cls))); cls end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

570 
 SOME(th',cls) => 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

571 
if eq_thm(th,th') then cls 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

572 
else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

573 
Output.debug (string_of_thm th); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

574 
Output.debug (string_of_thm th'); 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

575 
cls); 
15347  576 

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

577 
fun pairname th = (Thm.name_of_thm th, th); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

578 

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

579 
fun meta_cnf_axiom th = 
15956  580 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 
15499  581 

15347  582 

15872  583 
(**** Extract and Clausify theorems from a theory's claset and simpset ****) 
15347  584 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

585 
(*Preserve the name of "th" after the transformation "f"*) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

586 
fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th); 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

587 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

588 
fun rules_of_claset cs = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

589 
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs 
19175  590 
val intros = safeIs @ hazIs 
18532  591 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

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

593 
Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

594 
" elims: " ^ Int.toString(length elims)); 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

595 
map pairname (intros @ elims) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

596 
end; 
15347  597 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

598 
fun rules_of_simpset ss = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

599 
let val ({rules,...}, _) = rep_ss ss 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

600 
val simps = Net.entries rules 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

601 
in 
18680  602 
Output.debug ("rules_of_simpset: " ^ Int.toString(length simps)); 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

603 
map (fn r => (#name r, #thm r)) simps 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

604 
end; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

605 

f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

606 
fun claset_rules_of_thy thy = rules_of_claset (claset_of thy); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

607 
fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

608 

20774  609 
fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy)); 
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

610 

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

611 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

612 
fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

613 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  614 

20774  615 
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt)); 
616 

15347  617 

15872  618 
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) 
15347  619 

19894  620 
(* classical rules: works for both FOL and HOL *) 
621 
fun cnf_rules [] err_list = ([],err_list) 

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

622 
 cnf_rules ((name,th) :: ths) err_list = 
19894  623 
let val (ts,es) = cnf_rules ths err_list 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

624 
in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; 
15347  625 

19894  626 
fun pair_name_cls k (n, []) = [] 
627 
 pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) 

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

628 

19894  629 
fun cnf_rules_pairs_aux pairs [] = pairs 
630 
 cnf_rules_pairs_aux pairs ((name,th)::ths) = 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

631 
let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

632 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
19894  633 
in cnf_rules_pairs_aux pairs' ths end; 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

634 

19894  635 
val cnf_rules_pairs = cnf_rules_pairs_aux []; 
19353  636 

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

637 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

638 
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) 
15347  639 

20419  640 
(*Setup function: takes a theory and installs ALL known theorems into the clause cache*) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

641 

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

642 
fun skolem_cache (name,th) thy = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

643 
let val prop = Thm.prop_of th 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

644 
in 
20867
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

645 
if lambda_free prop 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

646 
(*orelse monomorphic prop? Monomorphic theorems can be Skolemized on demand, 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

647 
but there are problems with reuse of abstraction functions if we don't 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

648 
do them now, even for monomorphic theorems.*) 
e7b92a48e22b
Refinements to abstraction. Seeding with combinators K, I and B.
paulson
parents:
20863
diff
changeset

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

650 
else #2 (skolem_cache_thm (name,th) thy) 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

651 
end; 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

652 

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

653 
fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy; 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

654 

16563  655 

656 
(*** meson proof methods ***) 

657 

658 
fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) [])); 

659 

660 
fun meson_meth ths ctxt = 

661 
Method.SIMPLE_METHOD' HEADGOAL 

662 
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt)); 

663 

664 
val meson_method_setup = 

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

666 
[("meson", Method.thms_ctxt_args meson_meth, 
18833  667 
"MESON resolution proof procedure")]; 
15347  668 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

669 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

670 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

671 
(*** The Skolemization attribute ***) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

672 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

673 
fun conj2_rule (th1,th2) = conjI OF [th1,th2]; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

674 

20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

675 
(*Conjoin a list of theorems to form a single theorem*) 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

676 
fun conj_rule [] = TrueI 
20445  677 
 conj_rule ths = foldr1 conj2_rule ths; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

678 

20419  679 
fun skolem_attr (Context.Theory thy, th) = 
680 
let val name = Thm.name_of_thm th 

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

681 
val (cls, thy') = skolem_cache_thm (name, th) thy 
18728  682 
in (Context.Theory thy', conj_rule cls) end 
20419  683 
 skolem_attr (context, th) = (context, conj_rule (skolem_thm th)); 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

684 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

685 
val setup_attrs = Attrib.add_attributes 
20419  686 
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")]; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

687 

18708  688 
val setup = clause_cache_setup #> setup_attrs; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

689 

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

690 
end; 