author  paulson 
Thu, 26 Oct 2006 10:48:35 +0200  
changeset 21102  7f2ebe5c5b72 
parent 21096  8f3dffd52db2 
child 21254  d53f76357f41 
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 

20996  8 
(*unused during debugging*) 
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 

21071  15 
val cnf_name : string > thm list 
15997  16 
val meta_cnf_axiom : thm > thm list 
17 
val claset_rules_of_thy : theory > (string * thm) list 

18 
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

19 
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

20 
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

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

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

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

27 

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

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

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

31 

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

33 

15997  34 
struct 
15347  35 

20996  36 
(*For running the comparison between combinators and abstractions. 
37 
CANNOT be a ref, as the setting is used while Isabelle is built. 

38 
Currently FALSE, i.e. all the "abstraction" code below is unused, but so far 

39 
it seems to be inferior to combinators...*) 

40 
val abstract_lambdas = false; 

20419  41 

42 
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

43 

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

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

46 

20902  47 
val lhs_of = #1 o Logic.dest_equals o Thm.prop_of; 
48 
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

49 

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

50 

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

53 
extensionality in proofs. 

54 
FIXME! Store in theory data!!*) 

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

55 

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

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

57 
fun seed th net = 
20902  58 
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

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

60 
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

61 

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

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

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

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

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

66 

20445  67 

15997  68 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  69 

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

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

15347  76 

19894  77 
(*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

78 
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) 
19894  79 
(Const("Trueprop",_) $ Free(q,_)) = (p = q) 
15371  80 
 is_neg _ _ = false; 
81 

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

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

83 

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

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

85 
premises, so the final consequent must be kept.*) 
15371  86 
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = 
19894  87 
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

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

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

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

93 
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

94 
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

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

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

98 
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

99 
 strip_concl prems bvs concl Q = 
21071  100 
if concl aconv Q andalso not (null prems) 
101 
then add_EX (foldr1 HOLogic.mk_conj prems) bvs 

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

102 
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

103 

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

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

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

106 
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

107 
in HOLogic.mk_imp (major, disjs) end; 
15347  108 

16012  109 
(* 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

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

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

113 
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

114 
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

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

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

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

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

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

120 
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

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

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

123 
end; 
15347  124 

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

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

126 
predicate variable. Leave other theorems unchanged.*) 
16009  127 
fun transform_elim th = 
21071  128 
let val t = HOLogic.mk_Trueprop (elimR2Fol th) 
129 
in 

130 
if Meson.too_many_clauses t then TrueI 

131 
else Goal.prove_raw [] (cterm_of (sign_of_thm th) t) (fn _ => elimRule_tac th) 

132 
end 

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

133 
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

134 
 exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ 
21071  135 
" for theorem " ^ Thm.name_of_thm th ^ ": " ^ string_of_thm th); th) 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

136 

15997  137 

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

139 

16563  140 
(*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

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

142 

16563  143 
(*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

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

145 

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

16009  148 
fun transfer_to_Reconstruction th = 
16563  149 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  150 

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

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

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

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

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

155 

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

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

157 
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

158 

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

159 

16009  160 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
161 

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

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

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

164 
fun declare_skofuns s th thy = 
21071  165 
let val nref = ref 0 
166 
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

167 
(*Existential: declare a Skolem function, then insert into body and continue*) 
21071  168 
let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref)) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

169 
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

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

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

172 
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

173 
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

174 
(*Forms a lambdaabstraction over the formal parameters*) 
20783  175 
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

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

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

178 
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

179 
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

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

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

182 
 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

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

184 
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

185 
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

186 
 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

187 
 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

188 
 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

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

191 

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

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

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

194 
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

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

196 
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

197 
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

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

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

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

201 
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

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

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

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

205 
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

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

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

208 
 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

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

210 
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

211 
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

212 
 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

213 
 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

214 
 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

215 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  216 
in dec_sko (prop_of th) [] end; 
217 

218 

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

220 

221 
(*Returns the vars of a theorem*) 

222 
fun vars_of_thm th = 

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

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

226 
local 

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

228 
val cx = hd (vars_of_thm fun_cong'); 

229 
val ty = typ_of (ctyp_of_term cx); 

20445  230 
val thy = theory_of_thm fun_cong; 
20419  231 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
232 
in 

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

234 
end; 

235 

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

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

237 
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

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

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

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

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

242 
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

243 
 _ => th; 
20419  244 

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

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

247 
fun mk_object_eq th = th RS def_imp_eq 
20419  248 
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

249 

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

252 
let val th1 = combination cf (reflexive x) 

20902  253 
val th2 = beta_conversion false (Drule.rhs_of th1) 
20419  254 
in transitive th1 th2 end; 
255 

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

257 
fun list_combination cf [] = cf 

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

259 

260 
fun list_cabs ([] , t) = t 

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

262 

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

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

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

265 
in if (t aconv Envir.eta_contract t) then () 
20419  266 
else error ("Eta redex in term: " ^ string_of_cterm ct) 
267 
end; 

268 

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

269 
fun eq_absdef (th1, th2) = 
20445  270 
Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso 
271 
rhs_of th1 aconv rhs_of th2; 

272 

273 
fun lambda_free (Abs _) = false 

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

275 
 lambda_free _ = true; 

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

276 

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

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

278 
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

279 

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

280 
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

281 
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

282 
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

283 
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

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

285 

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

286 
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

287 
 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

288 

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

289 
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

290 
 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

291 
 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

292 

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

293 

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

294 
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

295 

20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

296 
(*Does an existing abstraction definition have an RHS that matches the one we need now? 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

297 
thy is the current theory, which must extend that of theorem th.*) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

298 
fun match_rhs thy t th = 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

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

301 
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

302 
val term_insts = map Meson.term_pair_of (Vartab.dest tenv) 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

303 
val ct_pairs = if subthy (theory_of_thm th, thy) andalso 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

304 
forall lambda_free (map #2 term_insts) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

306 
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

307 
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

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

309 
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

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

311 

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

314 
fun declare_absfuns th = 

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

315 
let fun abstract thy ct = 
20445  316 
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) 
317 
else 

318 
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

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

320 
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

321 
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

322 
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

323 
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

324 
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

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

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

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

329 
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

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

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

332 
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

333 
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

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

335 
val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else (); 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

336 
val thy = theory_of_thm u'_th 
20863
4ee61dbf192d
improvements to abstraction, ensuring more reuse of abstraction functions
paulson
parents:
20789
diff
changeset

337 
val (ax,ax',thy) = 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

338 
case List.mapPartial (match_rhs thy abs_v_u) 
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

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

341 
(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

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

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

344 
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

345 
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

346 
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

347 
val c = Const (Sign.full_name thy cname, cT) 
20783  348 
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

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

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

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

352 
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

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

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

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

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

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

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

359 
> mk_meta_eq > Meson.generalize 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

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

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

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

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

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

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

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

368 
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

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

370 
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

371 
(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

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

373 
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

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

375 
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

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

377 
val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else (); 
20419  378 
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

379 
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

380 
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

381 
in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end; 
20419  382 

20902  383 
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

384 

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

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

386 
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

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

388 

20419  389 
fun assume_absfuns th = 
20445  390 
let val thy = theory_of_thm th 
391 
val cterm = cterm_of thy 

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

392 
fun abstract ct = 
20445  393 
if lambda_free (term_of ct) then (reflexive ct, []) 
394 
else 

395 
case term_of ct of 

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

397 
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

398 
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

399 
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

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

402 
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

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

404 
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

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

406 
(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

407 
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

408 
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

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

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

411 
val (ax,ax') = 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

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

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

415 
(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

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

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

418 
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

419 
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

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

421 
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

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

423 
> mk_meta_eq > Meson.generalize 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

425 
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

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

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

428 
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

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

430 
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

431 
(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

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

433 
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

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

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

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

437 
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

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

439 
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

440 
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

441 
in map Drule.eta_contraction_rule ths end; 
20419  442 

16009  443 

444 
(*cterms are used throughout for efficiency*) 

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

445 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  446 

447 
(*cterm version of mk_cTrueprop*) 

448 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

449 

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

451 
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

452 
fun c_variant_abs_multi (ct0, vars) = 
16009  453 
let val (cv,ct) = Thm.dest_abs NONE ct0 
454 
in c_variant_abs_multi (ct, cv::vars) end 

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

456 

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

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

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

459 
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

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

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

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

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

465 
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

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

469 
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

470 
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

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

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

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

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

475 
end; 
16009  476 

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

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

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

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

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

481 
> ObjectLogic.atomize_thm > make_nnf > strip_lambdas ~1; 
16009  482 

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

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

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

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

486 
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

487 

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

488 

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

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

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

491 
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

492 

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

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

494 
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

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

496 
 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

497 

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

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

500 
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

501 
> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") 
20445  502 

20419  503 
(*Replace lambdas by assumed function definitions in the theorems*) 
20445  504 
fun assume_abstract_list ths = 
505 
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

506 
else map Drule.eta_contraction_rule ths; 
20419  507 

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

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

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

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

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

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

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

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

516 
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

517 
val (thy'', ths') = declare_abstract' (thy', ths) 
20419  518 
in (thy'', th_defs @ ths') end; 
519 

520 
fun declare_abstract (thy, ths) = 

521 
if abstract_lambdas then declare_abstract' (thy, ths) 

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

522 
else (thy, map Drule.eta_contraction_rule ths); 
20419  523 

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

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

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

526 
let val nnfth = to_nnf th 
20419  527 
in Meson.make_cnf (skolem_of_nnf nnfth) nnfth 
20445  528 
> 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

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

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

531 

21071  532 
(*Keep the full complexity of the original name*) 
533 
fun flatten_name s = space_implode "_X" (NameSpace.unpack s); 

534 

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

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

536 
It returns a modified theory, unless skolemization fails.*) 
16009  537 
fun skolem thy (name,th) = 
21071  538 
let val cname = (case name of "" => gensym ""  s => flatten_name s) 
20419  539 
val _ = Output.debug ("skolemizing " ^ name ^ ": ") 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

542 
let val (thy',defs) = declare_skofuns cname nnfth thy 
20419  543 
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth 
544 
val (thy'',cnfs') = declare_abstract (thy',cnfs) 

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

546 
end) 

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

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

548 
end; 
16009  549 

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

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

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

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

553 
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

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

555 
(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

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

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

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

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

560 
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

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

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

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

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

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

566 
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

567 
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

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

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

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

571 

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

572 
(*Exported function to convert Isabelle theorems into axiom clauses*) 
19894  573 
fun cnf_axiom (name,th) = 
21071  574 
(Output.debug ("cnf_axiom called, theorem name = " ^ name); 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

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

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

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

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

579 
let val cls = map Drule.local_standard (skolem_thm th) 
21071  580 
in Output.debug "inserted into cache"; 
581 
change clause_cache (Symtab.update (s, (th, cls))); cls 

582 
end 

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

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

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

585 
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

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

587 
Output.debug (string_of_thm th'); 
21071  588 
cls) 
589 
); 

15347  590 

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

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

592 

21071  593 
(*Principally for debugging*) 
594 
fun cnf_name s = 

595 
let val th = thm s 

596 
in cnf_axiom (Thm.name_of_thm th, th) end; 

15347  597 

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

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

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

601 
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

602 

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

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

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

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

608 
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

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

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

611 
end; 
15347  612 

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

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

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

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

616 
in 
18680  617 
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

618 
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

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

620 

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

621 
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

622 
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

623 

20774  624 
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

625 

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

626 

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

627 
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

628 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  629 

20774  630 
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt)); 
631 

15347  632 

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

19894  635 
(* classical rules: works for both FOL and HOL *) 
636 
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

637 
 cnf_rules ((name,th) :: ths) err_list = 
19894  638 
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

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

19894  641 
fun pair_name_cls k (n, []) = [] 
642 
 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

643 

19894  644 
fun cnf_rules_pairs_aux pairs [] = pairs 
645 
 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

646 
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

647 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
19894  648 
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

649 

19894  650 
val cnf_rules_pairs = cnf_rules_pairs_aux []; 
19353  651 

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

652 

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

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

20419  655 
(*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

656 

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

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

658 
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

659 
in 
21071  660 
if lambda_free prop 
20969
341808e0b7f2
Abstraction reuse code now checks that the abstraction function can be used in the current
paulson
parents:
20902
diff
changeset

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

662 
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

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

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

665 
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

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

667 

21071  668 
(*The cache can be kept smaller by augmenting the condition above with 
669 
orelse (not abstract_lambdas andalso monomorphic prop). 

670 
However, while this step does not reduce the time needed to build HOL, 

671 
it doubles the time taken by the first call to the ATP linkup.*) 

672 

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

673 
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

674 

16563  675 

676 
(*** meson proof methods ***) 

677 

21071  678 
fun skolem_use_cache_thm th = 
679 
case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of 

680 
NONE => skolem_thm th 

681 
 SOME (th',cls) => 

682 
if eq_thm(th,th') then cls else skolem_thm th; 

683 

684 
fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths); 

16563  685 

686 
fun meson_meth ths ctxt = 

687 
Method.SIMPLE_METHOD' HEADGOAL 

21096
8f3dffd52db2
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
paulson
parents:
21071
diff
changeset

688 
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs); 
16563  689 

690 
val meson_method_setup = 

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

692 
[("meson", Method.thms_ctxt_args meson_meth, 
18833  693 
"MESON resolution proof procedure")]; 
15347  694 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

695 
(** Attribute for converting a theorem into clauses **) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

696 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

697 
fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

698 

21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

699 
fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i) 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

700 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

701 
val clausify = Attrib.syntax (Scan.lift Args.nat 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

702 
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

703 

7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

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

705 

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

706 
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

707 

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

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

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

711 

20419  712 
fun skolem_attr (Context.Theory thy, th) = 
713 
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

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

717 

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

718 
val setup_attrs = Attrib.add_attributes 
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

719 
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

720 
("clausify", clausify, "conversion to clauses")]; 
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset

721 

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

723 

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

724 
end; 