author  paulson 
Mon, 04 Sep 2006 18:41:33 +0200  
changeset 20473  7ef72f030679 
parent 20461  d689ad772b2c 
child 20525  4b0fdb18ea9a 
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 

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

43 
extensionality in proofs. 

44 
FIXME! Store in theory data!!*) 

45 
val abstraction_cache = ref Net.empty : thm Net.net ref; 

46 

15997  47 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  48 

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

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

15347  55 

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

57 
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) 
19894  58 
(Const("Trueprop",_) $ Free(q,_)) = (p = q) 
15371  59 
 is_neg _ _ = false; 
60 

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

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

62 

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

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

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

67 
 strip_concl' prems bvs P = 
15956  68 
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) 
19894  69 
in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; 
15371  70 

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

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

72 
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

73 
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

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

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

77 
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

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

79 
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

80 
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

81 

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

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

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

84 
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

85 
in HOLogic.mk_imp (major, disjs) end; 
15347  86 

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

88 
fun elimR2Fol elimR = 
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all  now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset

89 
let val elimR' = #1 (Drule.freeze_thaw elimR) 
19894  90 
val (prems,concl) = (prems_of elimR', concl_of elimR') 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

91 
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

92 
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

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

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

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

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

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

98 
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

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

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

101 
end; 
15347  102 

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

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

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

106 
let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th)) 
18009  107 
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

108 
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

109 
 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

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

111 

15997  112 

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

114 

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

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

117 

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

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

120 

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

16009  123 
fun transfer_to_Reconstruction th = 
16563  124 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  125 

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

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

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

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

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

130 

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

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

132 
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

133 

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

134 

16009  135 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
136 

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

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

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

139 
fun declare_skofuns s th thy = 
20419  140 
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

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

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

143 
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

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

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

146 
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

147 
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

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

149 
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

152 
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

153 
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

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

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

156 
 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

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

158 
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

159 
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

160 
 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

161 
 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

162 
 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

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

165 

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

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

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

168 
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

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

170 
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

171 
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

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

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

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

175 
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

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

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

178 
val def = equals cT $ c $ rhs 
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 
(def :: defs) 
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))) defs = 
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)) defs 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) 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

187 
 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

188 
 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

189 
 dec_sko t defs = defs (*Do nothing otherwise*) 
20419  190 
in dec_sko (prop_of th) [] end; 
191 

192 

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

194 

195 
(*Returns the vars of a theorem*) 

196 
fun vars_of_thm th = 

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

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

200 
local 

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

202 
val cx = hd (vars_of_thm fun_cong'); 

203 
val ty = typ_of (ctyp_of_term cx); 

20445  204 
val thy = theory_of_thm fun_cong; 
20419  205 
fun mkvar a = cterm_of thy (Var((a,0),ty)); 
206 
in 

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

208 
end; 

209 

210 
(*Removes the lambdas from an equation of the form t = (%x. u)*) 

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

211 
fun strip_lambdas th = 
20419  212 
case prop_of th of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

213 
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => 
20419  214 
strip_lambdas (#1 (Drule.freeze_thaw (th RS xfun_cong x))) 
215 
 _ => th; 

216 

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

217 
(*Convert meta to objectequality. Fails for theorems like split_comp_eq, 
20419  218 
where some types have the empty sort.*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

219 
fun object_eq th = th RS def_imp_eq 
20419  220 
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

221 

20419  222 
fun valid_name vs (Free(x,T)) = x mem_string vs 
223 
 valid_name vs _ = false; 

224 

225 
(*Contract all etaredexes in the theorem, lest they give rise to needless abstractions*) 

226 
fun eta_conversion_rule th = 

227 
equal_elim (eta_conversion (cprop_of th)) th; 

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

228 

20445  229 
fun crhs_of th = 
20419  230 
case Drule.strip_comb (cprop_of th) of 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

231 
(f, [_, rhs]) => 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

232 
(case term_of f of Const ("==", _) => rhs 
20445  233 
 _ => raise THM ("crhs_of", 0, [th])) 
234 
 _ => raise THM ("crhs_of", 1, [th]); 

235 

236 
fun rhs_of th = 

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

237 
case prop_of th of (Const("==",_) $ _ $ rhs) => rhs 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

238 
 _ => raise THM ("rhs_of", 1, [th]); 
20419  239 

240 
(*Apply a function definition to an argument, betareducing the result.*) 

241 
fun beta_comb cf x = 

242 
let val th1 = combination cf (reflexive x) 

20445  243 
val th2 = beta_conversion false (crhs_of th1) 
20419  244 
in transitive th1 th2 end; 
245 

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

247 
fun list_combination cf [] = cf 

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

249 

250 
fun list_cabs ([] , t) = t 

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

252 

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

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

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

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

258 

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

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

262 

263 
fun lambda_free (Abs _) = false 

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

265 
 lambda_free _ = true; 

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

266 

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

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

268 
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

269 

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

272 
fun declare_absfuns th = 

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

273 
let fun abstract thy ct = 
20445  274 
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) 
275 
else 

276 
case term_of ct of 

20419  277 
Abs (_,T,u) => 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

278 
let val cname = gensym "abs_" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

280 
val (cv,cta) = Thm.dest_abs NONE ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

281 
val v = (#1 o dest_Free o term_of) cv 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

282 
val (u'_th,defs) = abstract thy cta 
20445  283 
val cu' = crhs_of u'_th 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

284 
val abs_v_u = lambda (term_of cv) (term_of cu') 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

286 
val args = term_frees abs_v_u 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

287 
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

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

289 
val v_rhs = Logic.varify rhs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

290 
val (ax,thy) = 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

291 
case List.find (fn ax => v_rhs aconv rhs_of ax) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

292 
(Net.match_term (!abstraction_cache) v_rhs) of 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

293 
SOME ax => (ax,thy) (*cached axiom, current theory*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

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

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

298 
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

299 
val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

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

303 
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

304 
[(cdef, equals cT $ c $ rhs)] thy 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

305 
val ax = get_axiom thy cdef 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

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

309 
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

310 
in (ax,thy) end 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

311 
val _ = assert (v_rhs aconv rhs_of ax) "declare_absfuns: rhs mismatch" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

312 
val def = #1 (Drule.freeze_thaw ax) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

313 
val def_args = list_combination def (map (cterm_of thy) args) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

314 
in (transitive (abstract_rule v cv u'_th) (symmetric def_args), 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

317 
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

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

319 
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

320 
in (combination th1 th2, defs1@defs2) end 
20419  321 
val _ = if !trace_abs then warning (string_of_thm th) else (); 
322 
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) 

323 
val ths = equal_elim eqth th :: 

324 
map (forall_intr_vars o strip_lambdas o object_eq) defs 

325 
in (theory_of_thm eqth, ths) end; 

326 

327 
fun assume_absfuns th = 

20445  328 
let val thy = theory_of_thm th 
329 
val cterm = cterm_of thy 

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

330 
fun abstract vs ct = 
20445  331 
if lambda_free (term_of ct) then (reflexive ct, []) 
332 
else 

333 
case term_of ct of 

20419  334 
Abs (_,T,u) => 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

335 
let val (cv,cta) = Thm.dest_abs NONE ct 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

337 
val v = (#1 o dest_Free o term_of) cv 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

338 
val (u'_th,defs) = abstract (v::vs) cta 
20445  339 
val cu' = crhs_of u'_th 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

340 
val abs_v_u = Thm.cabs cv cu' 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

341 
(*get the formal parameters: bound variables also present in the term*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

342 
val args = filter (valid_name vs) (term_frees (term_of abs_v_u)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

345 
val rhs = term_of crhs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

346 
val def = (*FIXME: can we also use the constabstractions?*) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

347 
case List.find (fn ax => rhs aconv rhs_of ax andalso 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

348 
Context.joinable (thy, theory_of_thm ax)) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

349 
(Net.match_term (!abstraction_cache) rhs) of 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

350 
SOME ax => ax 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

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

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

355 
val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

356 
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

357 
(!abstraction_cache) 
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 ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

361 
val _ = assert (rhs aconv rhs_of def) "assume_absfuns: rhs mismatch" 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

362 
val def_args = list_combination def (map cterm args) 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

363 
in (transitive (abstract_rule v cv u'_th) (symmetric def_args), 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

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

366 
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

367 
val (t1',defs1) = abstract vs ct1 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

369 
in (combination t1' t2', defs1@defs2) end 
20419  370 
val (eqth,defs) = abstract [] (cprop_of th) 
371 
in equal_elim eqth th :: 

372 
map (forall_intr_vars o strip_lambdas o object_eq) defs 

373 
end; 

374 

16009  375 

376 
(*cterms are used throughout for efficiency*) 

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

377 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  378 

379 
(*cterm version of mk_cTrueprop*) 

380 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

381 

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

383 
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

384 
fun c_variant_abs_multi (ct0, vars) = 
16009  385 
let val (cv,ct) = Thm.dest_abs NONE ct0 
386 
in c_variant_abs_multi (ct, cv::vars) end 

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

388 

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

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

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

391 
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

392 
fun skolem_of_def def = 
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all  now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset

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

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

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

397 
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

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

401 
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

402 
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

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

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

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

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

407 
end; 
16009  408 

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

409 
(*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) 
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

410 
(*It now works for HOL too. *) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

412 
th > transfer_to_Reconstruction 
20419  413 
> transform_elim > zero_var_indexes > Drule.freeze_thaw > #1 
16588  414 
> ObjectLogic.atomize_thm > make_nnf; 
16009  415 

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

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

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

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

419 
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

420 

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

421 

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

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

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

424 
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

425 

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

426 
fun assert_lambda_free ths = assert (forall (lambda_free o prop_of) ths); 
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

427 

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

429 
if lambda_free (prop_of th) then [th] 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

431 
> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") 
20445  432 

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

20419  436 
else map eta_conversion_rule ths; 
437 

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

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

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

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

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

442 
if lambda_free (prop_of th) then (thy, [th]) 
20445  443 
else 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

444 
th > zero_var_indexes > Drule.freeze_thaw > #1 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

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

446 
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

447 
val (thy'', ths') = declare_abstract' (thy', ths) 
20419  448 
in (thy'', th_defs @ ths') end; 
449 

20421  450 
(*FIXME DELETE if we decide to switch to abstractions*) 
20419  451 
fun declare_abstract (thy, ths) = 
452 
if abstract_lambdas then declare_abstract' (thy, ths) 

453 
else (thy, map eta_conversion_rule ths); 

454 

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

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

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

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

458 
let val nnfth = to_nnf th 
20419  459 
in Meson.make_cnf (skolem_of_nnf nnfth) nnfth 
20445  460 
> 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

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

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

463 

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

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

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

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

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

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

471 
let val (thy',defs) = declare_skofuns cname nnfth thy 
20419  472 
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth 
473 
val (thy'',cnfs') = declare_abstract (thy',cnfs) 

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

475 
end) 

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

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

477 
end; 
16009  478 

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

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

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

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

482 
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

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

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

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

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

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

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

489 
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

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

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

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

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

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

495 
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

496 
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

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

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

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

500 

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

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

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

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

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

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

507 
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

508 
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

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

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

511 
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

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

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

514 
cls); 
15347  515 

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

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

517 

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

518 
fun meta_cnf_axiom th = 
15956  519 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 
15499  520 

15347  521 

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

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

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

525 
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

526 

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

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

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

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

532 
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

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

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

535 
end; 
15347  536 

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

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

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

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

540 
in 
18680  541 
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

542 
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

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

544 

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

545 
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

546 
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

547 

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

548 
fun atpset_rules_of_thy thy = map pairname (ResAtpSet.atp_rules_of_thy thy); 
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset

549 

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

550 

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

551 
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

552 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  553 

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

554 
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpSet.atp_rules_of_ctxt ctxt); 
15347  555 

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

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

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

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

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

566 

19894  567 
fun cnf_rules_pairs_aux pairs [] = pairs 
568 
 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

569 
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

570 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

571 
 ResHolClause.LAM2COMB _ => pairs 
19894  572 
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

573 

19894  574 
val cnf_rules_pairs = cnf_rules_pairs_aux []; 
19353  575 

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

576 

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

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

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

580 

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

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

582 
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

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

584 
if lambda_free prop orelse monomorphic prop 
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset

585 
then thy (*monomorphic theorems can be Skolemized on demand*) 
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset

586 
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

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

588 

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

589 
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

590 

16563  591 

592 
(*** meson proof methods ***) 

593 

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

595 

596 
fun meson_meth ths ctxt = 

597 
Method.SIMPLE_METHOD' HEADGOAL 

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

599 

600 
val meson_method_setup = 

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

602 
[("meson", Method.thms_ctxt_args meson_meth, 
18833  603 
"MESON resolution proof procedure")]; 
15347  604 

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

605 

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

606 

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

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

608 

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

609 
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

610 

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

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

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

614 

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

617 
val (cls, thy') = skolem_cache_thm (name, th) thy 
18728  618 
in (Context.Theory thy', conj_rule cls) end 
20419  619 
 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

620 

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

621 
val setup_attrs = Attrib.add_attributes 
20419  622 
[("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

623 

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

625 

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

626 
end; 