author  paulson 
Wed, 09 Aug 2006 18:41:42 +0200  
changeset 20373  dcb321249aa9 
parent 20362  bbff23c3e2ca 
child 20419  df257a9cf0e9 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

5 
Transformation of axiom rules (elim/intro/etc) into CNF forms. 

6 
*) 

7 

15997  8 
signature RES_AXIOMS = 
9 
sig 

10 
val elimRule_tac : thm > Tactical.tactic 

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

14 
val meta_cnf_axiom : thm > thm list 

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

16 
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

17 
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

18 
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

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

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

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

24 

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

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

26 
val atpset_rules_of_ctxt : Proof.context > (string * thm) list 
15997  27 
end; 
15347  28 

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

29 
structure ResAxioms : RES_AXIOMS = 
15997  30 

31 
struct 

15347  32 

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

33 

15997  34 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  35 

15390  36 
(* a tactic used to prove an elimrule. *) 
16009  37 
fun elimRule_tac th = 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

38 
(resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(blast_tac HOL_cs 1); 
15347  39 

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

15347  42 

19894  43 
(*Checks for the premise ~P when the conclusion is P.*) 
44 
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) 

45 
(Const("Trueprop",_) $ Free(q,_)) = (p = q) 

15371  46 
 is_neg _ _ = false; 
47 

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

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

49 

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

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

51 
premises, so the final consequent must be kept.*) 
15371  52 
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = 
19894  53 
strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q 
15371  54 
 strip_concl' prems bvs P = 
15956  55 
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) 
19894  56 
in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; 
15371  57 

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

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

59 
is ignored, as it is the dummy "conclusion" variable.*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

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

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

64 
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

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

66 
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

67 
else raise ELIMR2FOL (*expected conclusion not found!*) 
15347  68 

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

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

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

71 
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

72 
in HOLogic.mk_imp (major, disjs) end; 
15347  73 

16012  74 
(* convert an elim rule into an equivalent formula, of type term. *) 
15347  75 
fun elimR2Fol elimR = 
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all  now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset

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

78 
val cv = case concl of (*conclusion variable*) 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

79 
Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

80 
 v as Free(_, Type("prop",[])) => v 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

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

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

83 
[] => raise ELIMR2FOL 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

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

85 
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

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

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

88 
end; 
15347  89 

15997  90 
(* convert an elimrule into an equivalent theorem that does not have the 
91 
predicate variable. Leave other theorems unchanged.*) 

16009  92 
fun transform_elim th = 
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

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

95 
handle ELIMR2FOL => th (*not an elimination rule*) 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

96 
 exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ 
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset

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

98 

15997  99 

100 

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

102 

15347  103 

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

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

106 

16563  107 
(*This will refer to the final version of theory Reconstruction.*) 
108 
val recon_thy_ref = Theory.self_ref (the_context ()); 

15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

109 

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

16009  112 
fun transfer_to_Reconstruction th = 
16563  113 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  114 

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

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

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

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

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

119 

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

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

121 
val rm_redundant_cls = List.filter (not o is_taut); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

122 

15997  123 

16009  124 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
125 

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

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

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

128 
fun declare_skofuns s th thy = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

129 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) = 
16009  130 
(*Existential: declare a Skolem function, then insert into body and continue*) 
131 
let val cname = s ^ "_" ^ Int.toString n 

16012  132 
val args = term_frees xtp (*get the formal parameter list*) 
16009  133 
val Ts = map type_of args 
134 
val cT = Ts > T 

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

135 
val c = Const (Sign.full_name thy cname, cT) 
16009  136 
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) 
16012  137 
(*Forms a lambdaabstraction over the formal parameters*) 
16009  138 
val def = equals cT $ c $ rhs 
139 
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy 

16012  140 
(*Theory is augmented with the constant, then its def*) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

141 
val cdef = cname ^ "_def" 
19630  142 
val thy'' = Theory.add_defs_i false false [(cdef, def)] thy' 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

143 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

144 
(n+1, (thy'', get_axiom thy'' cdef :: axs)) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

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

146 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = 
16012  147 
(*Universal quant: insert a free variable into body and continue*) 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20017
diff
changeset

148 
let val fname = Name.variant (add_term_names (p,[])) a 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

149 
in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

150 
 dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

151 
 dec_sko (Const ("op ", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

152 
 dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

153 
 dec_sko t nthx = nthx (*Do nothing otherwise*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

154 
in #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[]))) end; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

155 

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

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

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

158 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

159 
(*Existential: declare a Skolem function, then insert into body and continue*) 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20017
diff
changeset

160 
let val name = Name.variant (add_term_names (p,[])) (gensym "sko_") 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

161 
val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

162 
val args = term_frees xtp \\ skos (*the formal parameters*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

163 
val Ts = map type_of args 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

164 
val cT = Ts > T 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

165 
val c = Free (name, cT) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

166 
val rhs = list_abs_free (map dest_Free args, 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

167 
HOLogic.choice_const T $ xtp) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

168 
(*Forms a lambdaabstraction over the formal parameters*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

169 
val def = equals cT $ c $ rhs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

170 
in dec_sko (subst_bound (list_comb(c,args), p)) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

171 
(def :: defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

173 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

174 
(*Universal quant: insert a free variable into body and continue*) 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20017
diff
changeset

175 
let val fname = Name.variant (add_term_names (p,[])) a 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

176 
in dec_sko (subst_bound (Free(fname,T), p)) defs end 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

177 
 dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

178 
 dec_sko (Const ("op ", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

179 
 dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

180 
 dec_sko t defs = defs (*Do nothing otherwise*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

181 
in dec_sko (#prop (rep_thm th)) [] end; 
16009  182 

183 
(*cterms are used throughout for efficiency*) 

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

184 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  185 

186 
(*cterm version of mk_cTrueprop*) 

187 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

188 

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

190 
ones. Return the body, along with the list of free variables.*) 

191 
fun c_variant_abs_multi (ct0, vars) = 

192 
let val (cv,ct) = Thm.dest_abs NONE ct0 

193 
in c_variant_abs_multi (ct, cv::vars) end 

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

195 

196 
(*Given the definition of a Skolem function, return a theorem to replace 

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

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

198 
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) 
16588  199 
fun skolem_of_def def = 
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all  now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset

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

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

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

204 
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

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

208 
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

209 
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

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

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

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

214 
end; 
16009  215 

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

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

217 
(*It now works for HOL too. *) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

219 
th > transfer_to_Reconstruction 
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all  now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset

220 
> transform_elim > Drule.freeze_thaw > #1 
16588  221 
> ObjectLogic.atomize_thm > make_nnf; 
16009  222 

223 
(*The cache prevents repeated clausification of a theorem, 

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

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

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

226 
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

227 

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

228 

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

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

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

231 
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

232 

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

233 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
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

234 
(*also works for HOL*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

236 
let val nnfth = to_nnf th 
19175  237 
in rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

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

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

240 

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

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

242 
It returns a modified theory, unless skolemization fails.*) 
16009  243 
fun skolem thy (name,th) = 
20373  244 
let val cname = (case name of "" => gensym "sko_"  s => Sign.base_name s) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

245 
in Option.map 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

247 
let val (thy',defs) = declare_skofuns cname nnfth thy 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

248 
val skoths = map skolem_of_def defs 
19175  249 
in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end) 
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

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

251 
end; 
16009  252 

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

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

254 
and modified theory.*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

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

256 
case Symtab.lookup (!clause_cache) name of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

257 
NONE => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

258 
(case skolem thy (name, Thm.transfer thy th) of 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

259 
NONE => ([th],thy) 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

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

261 
(change clause_cache (Symtab.update (name, (th, cls))); (cls,thy'))) 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

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

263 
if eq_thm(th,th') then (cls,thy) 
19232  264 
else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); 
265 
Output.debug (string_of_thm th); 

266 
Output.debug (string_of_thm th'); 

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

267 
([th],thy)); 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

268 

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

269 
fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy)); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

270 

16009  271 

272 
(*Exported function to convert Isabelle theorems into axiom clauses*) 

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

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

276 
 s => case Symtab.lookup (!clause_cache) s of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

277 
NONE => 
19894  278 
let val cls = skolem_thm th 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

279 
in change clause_cache (Symtab.update (s, (th, cls))); cls end 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

280 
 SOME(th',cls) => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

281 
if eq_thm(th,th') then cls 
19232  282 
else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); 
283 
Output.debug (string_of_thm th); 

284 
Output.debug (string_of_thm th'); 

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

285 
cls); 
15347  286 

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

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

288 

15956  289 
fun meta_cnf_axiom th = 
290 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 

15499  291 

15347  292 

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

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

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

296 
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

297 

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

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

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

302 
in 
18680  303 
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

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

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

306 
end; 
15347  307 

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

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

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

310 
val simps = Net.entries rules 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

311 
in 
18680  312 
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

313 
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

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

315 

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

316 
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

317 
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

318 

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

319 
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

320 

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

321 

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

322 
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

323 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  324 

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

325 
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpSet.atp_rules_of_ctxt ctxt); 
15347  326 

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

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

331 
 cnf_rules ((name,th) :: ths) err_list = 

332 
let val (ts,es) = cnf_rules ths err_list 

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

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

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

337 

338 
fun cnf_rules_pairs_aux pairs [] = pairs 

339 
 cnf_rules_pairs_aux pairs ((name,th)::ths) = 

340 
let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) :: pairs 

341 
handle THM _ => pairs  ResClause.CLAUSE _ => pairs 

342 
 ResHolClause.LAM2COMB _ => pairs 

343 
in cnf_rules_pairs_aux pairs' ths end; 

19353  344 

19894  345 
val cnf_rules_pairs = cnf_rules_pairs_aux []; 
19353  346 

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

347 

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

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

16009  350 
(*Setup function: takes a theory and installs ALL simprules and claset rules 
351 
into the clause cache*) 

352 
fun clause_cache_setup thy = 

353 
let val simps = simpset_rules_of_thy thy 

354 
and clas = claset_rules_of_thy thy 

20362  355 
val thy1 = List.foldl skolem_cache thy clas 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

356 
in List.foldl skolem_cache thy1 simps end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

357 
(*Could be duplicate theorem names, due to multiple attributes*) 
16009  358 

16563  359 

360 
(*** meson proof methods ***) 

361 

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

363 

364 
fun meson_meth ths ctxt = 

365 
Method.SIMPLE_METHOD' HEADGOAL 

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

367 

368 
val meson_method_setup = 

18708  369 
Method.add_methods 
370 
[("meson", Method.thms_ctxt_args meson_meth, 

18833  371 
"MESON resolution proof procedure")]; 
15347  372 

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

373 

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

374 

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

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

376 

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

377 
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

378 

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

379 
(*Conjoin a list of clauses to recreate a single theorem*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

380 
val conj_rule = foldr1 conj2_rule; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

381 

18728  382 
fun skolem (Context.Theory thy, th) = 
383 
let 

384 
val name = Thm.name_of_thm th 

385 
val (cls, thy') = skolem_cache_thm ((name, th), thy) 

386 
in (Context.Theory thy', conj_rule cls) end 

387 
 skolem (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

388 

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

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

391 

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

393 

15347  394 
end; 