author | mengj |
Tue, 07 Mar 2006 03:56:59 +0100 | |
changeset 19196 | 62ee8c10d796 |
parent 19175 | c6e4b073f6a5 |
child 19206 | 79053aa24abf |
permissions | -rw-r--r-- |
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 |
exception ELIMR2FOL of string |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
11 |
val tagging_enabled : bool |
15997 | 12 |
val elimRule_tac : thm -> Tactical.tactic |
16012 | 13 |
val elimR2Fol : thm -> term |
15997 | 14 |
val transform_elim : thm -> thm |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
16012
diff
changeset
|
15 |
val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list |
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
|
16 |
val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list |
15997 | 17 |
val cnf_axiom : (string * thm) -> thm list |
18 |
val meta_cnf_axiom : thm -> thm list |
|
19 |
val claset_rules_of_thy : theory -> (string * thm) list |
|
20 |
val simpset_rules_of_thy : theory -> (string * thm) list |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
21 |
val claset_rules_of_ctxt: Proof.context -> (string * thm) list |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
22 |
val simpset_rules_of_ctxt : Proof.context -> (string * thm) list |
17829 | 23 |
val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list |
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
|
24 |
val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list 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
|
25 |
val pairname : thm -> (string * thm) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
26 |
val skolem_thm : thm -> thm list |
18274
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
27 |
val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
28 |
val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list |
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
29 |
val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list |
18708 | 30 |
val meson_method_setup : theory -> theory |
31 |
val setup : theory -> theory |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
32 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
33 |
val atpset_rules_of_thy : theory -> (string * thm) list |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
34 |
val atpset_rules_of_ctxt : Proof.context -> (string * thm) list |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
35 |
|
15997 | 36 |
end; |
15347 | 37 |
|
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
|
38 |
structure ResAxioms : RES_AXIOMS = |
15997 | 39 |
|
40 |
struct |
|
15347 | 41 |
|
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
|
42 |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
43 |
val tagging_enabled = false (*compile_time option*) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
44 |
|
15997 | 45 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 46 |
|
15390 | 47 |
(* a tactic used to prove an elim-rule. *) |
16009 | 48 |
fun elimRule_tac th = |
49 |
((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN |
|
16588 | 50 |
REPEAT(fast_tac HOL_cs 1); |
15347 | 51 |
|
52 |
exception ELIMR2FOL of string; |
|
53 |
||
15390 | 54 |
(* functions used to construct a formula *) |
55 |
||
15347 | 56 |
fun make_disjs [x] = x |
15956 | 57 |
| make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs) |
15347 | 58 |
|
59 |
fun make_conjs [x] = x |
|
15956 | 60 |
| make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs) |
61 |
||
62 |
fun add_EX tm [] = tm |
|
63 |
| add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; |
|
15347 | 64 |
|
15956 | 65 |
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q) |
15371 | 66 |
| is_neg _ _ = false; |
67 |
||
15347 | 68 |
|
69 |
exception STRIP_CONCL; |
|
70 |
||
71 |
||
15371 | 72 |
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = |
15956 | 73 |
let val P' = HOLogic.dest_Trueprop P |
74 |
val prems' = P'::prems |
|
75 |
in |
|
15371 | 76 |
strip_concl' prems' bvs Q |
15956 | 77 |
end |
15371 | 78 |
| strip_concl' prems bvs P = |
15956 | 79 |
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) |
80 |
in |
|
15371 | 81 |
add_EX (make_conjs (P'::prems)) bvs |
15956 | 82 |
end; |
15371 | 83 |
|
84 |
||
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
85 |
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
|
86 |
strip_concl prems ((x,xtp)::bvs) concl body |
15371 | 87 |
| strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
88 |
if (is_neg P concl) then (strip_concl' prems bvs Q) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
89 |
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q |
15371 | 90 |
| strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs; |
15347 | 91 |
|
92 |
||
15371 | 93 |
fun trans_elim (main,others,concl) = |
94 |
let val others' = map (strip_concl [] [] concl) others |
|
15347 | 95 |
val disjs = make_disjs others' |
96 |
in |
|
15956 | 97 |
HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs) |
15347 | 98 |
end; |
99 |
||
100 |
||
15390 | 101 |
(* aux function of elim2Fol, take away predicate variable. *) |
15371 | 102 |
fun elimR2Fol_aux prems concl = |
15347 | 103 |
let val nprems = length prems |
104 |
val main = hd prems |
|
105 |
in |
|
15956 | 106 |
if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main) |
15371 | 107 |
else trans_elim (main, tl prems, concl) |
15347 | 108 |
end; |
109 |
||
15956 | 110 |
|
16012 | 111 |
(* convert an elim rule into an equivalent formula, of type term. *) |
15347 | 112 |
fun elimR2Fol elimR = |
113 |
let val elimR' = Drule.freeze_all elimR |
|
114 |
val (prems,concl) = (prems_of elimR', concl_of elimR') |
|
115 |
in |
|
116 |
case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) |
|
15956 | 117 |
=> HOLogic.mk_Trueprop (elimR2Fol_aux prems concl) |
118 |
| Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl) |
|
15347 | 119 |
| _ => raise ELIMR2FOL("Not an elimination rule!") |
120 |
end; |
|
121 |
||
122 |
||
15390 | 123 |
(* check if a rule is an elim rule *) |
16009 | 124 |
fun is_elimR th = |
125 |
case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true |
|
15347 | 126 |
| Var(indx,Type("prop",[])) => true |
127 |
| _ => false; |
|
128 |
||
15997 | 129 |
(* convert an elim-rule into an equivalent theorem that does not have the |
130 |
predicate variable. Leave other theorems unchanged.*) |
|
16009 | 131 |
fun transform_elim th = |
132 |
if is_elimR th then |
|
133 |
let val tm = elimR2Fol th |
|
134 |
val ctm = cterm_of (sign_of_thm th) tm |
|
18009 | 135 |
in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end |
16563 | 136 |
else th; |
15997 | 137 |
|
138 |
||
139 |
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
|
140 |
||
15347 | 141 |
|
16563 | 142 |
(*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
|
143 |
inside that theory -- because it's needed for Skolemization *) |
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset
|
144 |
|
16563 | 145 |
(*This will refer to the final version of theory Reconstruction.*) |
146 |
val recon_thy_ref = Theory.self_ref (the_context ()); |
|
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset
|
147 |
|
16563 | 148 |
(*If called while Reconstruction is being created, it will transfer to the |
149 |
current version. If called afterward, it will transfer to the final version.*) |
|
16009 | 150 |
fun transfer_to_Reconstruction th = |
16563 | 151 |
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; |
15347 | 152 |
|
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
153 |
fun is_taut th = |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
154 |
case (prop_of th) of |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
155 |
(Const ("Trueprop", _) $ Const ("True", _)) => true |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
156 |
| _ => false; |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
157 |
|
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
158 |
(* remove tautologous clauses *) |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
159 |
val rm_redundant_cls = List.filter (not o is_taut); |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
160 |
|
15997 | 161 |
|
16009 | 162 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
163 |
||
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
164 |
(*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
|
165 |
prefix for the Skolem constant. Result is a new theory*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
166 |
fun declare_skofuns s th thy = |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
167 |
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) = |
16009 | 168 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
169 |
let val cname = s ^ "_" ^ Int.toString n |
|
16012 | 170 |
val args = term_frees xtp (*get the formal parameter list*) |
16009 | 171 |
val Ts = map type_of args |
172 |
val cT = Ts ---> T |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
173 |
val c = Const (Sign.full_name thy cname, cT) |
16009 | 174 |
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
16012 | 175 |
(*Forms a lambda-abstraction over the formal parameters*) |
16009 | 176 |
val def = equals cT $ c $ rhs |
177 |
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy |
|
16012 | 178 |
(*Theory is augmented with the constant, then its def*) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
179 |
val cdef = cname ^ "_def" |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
180 |
val thy'' = Theory.add_defs_i false [(cdef, def)] thy' |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
181 |
in dec_sko (subst_bound (list_comb(c,args), p)) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
182 |
(n+1, (thy'', get_axiom thy'' cdef :: axs)) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
183 |
end |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
184 |
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = |
16012 | 185 |
(*Universal quant: insert a free variable into body and continue*) |
16009 | 186 |
let val fname = variant (add_term_names (p,[])) a |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
187 |
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
|
188 |
| 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
|
189 |
| 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
|
190 |
| dec_sko (Const ("HOL.tag", _) $ p) nthy = dec_sko p nthy |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
191 |
| 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
|
192 |
| dec_sko t nthx = nthx (*Do nothing otherwise*) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
193 |
in #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[]))) end; |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
194 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
195 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
196 |
fun assume_skofuns th = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
197 |
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
|
198 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
199 |
let val name = variant (add_term_names (p,[])) (gensym "sko_") |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
200 |
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
|
201 |
val args = term_frees xtp \\ skos (*the formal parameters*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
202 |
val Ts = map type_of args |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
203 |
val cT = Ts ---> T |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
204 |
val c = Free (name, cT) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
205 |
val rhs = list_abs_free (map dest_Free args, |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
206 |
HOLogic.choice_const T $ xtp) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
207 |
(*Forms a lambda-abstraction over the formal parameters*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
208 |
val def = equals cT $ c $ rhs |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
209 |
in dec_sko (subst_bound (list_comb(c,args), p)) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
210 |
(def :: defs) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
211 |
end |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
212 |
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
213 |
(*Universal quant: insert a free variable into body and continue*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
214 |
let val fname = variant (add_term_names (p,[])) a |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
215 |
in dec_sko (subst_bound (Free(fname,T), p)) defs end |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
216 |
| 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
|
217 |
| 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
|
218 |
| dec_sko (Const ("HOL.tag", _) $ p) defs = dec_sko p defs |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
219 |
| dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
220 |
| dec_sko t defs = defs (*Do nothing otherwise*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
221 |
in dec_sko (#prop (rep_thm th)) [] end; |
16009 | 222 |
|
223 |
(*cterms are used throughout for efficiency*) |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
224 |
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; |
16009 | 225 |
|
226 |
(*cterm version of mk_cTrueprop*) |
|
227 |
fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
228 |
||
229 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
230 |
ones. Return the body, along with the list of free variables.*) |
|
231 |
fun c_variant_abs_multi (ct0, vars) = |
|
232 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
|
233 |
in c_variant_abs_multi (ct, cv::vars) end |
|
234 |
handle CTERM _ => (ct0, rev vars); |
|
235 |
||
236 |
(*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
|
237 |
an existential formula by a use of that function. |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
238 |
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
16588 | 239 |
fun skolem_of_def def = |
16009 | 240 |
let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def)) |
241 |
val (ch, frees) = c_variant_abs_multi (rhs, []) |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
242 |
val (chilbert,cabs) = Thm.dest_comb ch |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
243 |
val {sign,t, ...} = rep_cterm chilbert |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
244 |
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
|
245 |
| _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) |
16009 | 246 |
val cex = Thm.cterm_of sign (HOLogic.exists_const T) |
247 |
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
|
248 |
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
|
249 |
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
|
250 |
in Goal.prove_raw [ex_tm] conc tacf |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
251 |
|> forall_intr_list frees |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
252 |
|> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
253 |
|> Thm.varifyT |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
254 |
end; |
16009 | 255 |
|
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
|
256 |
(*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
|
257 |
(*It now works for HOL too. *) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
258 |
fun to_nnf th = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
259 |
th |> transfer_to_Reconstruction |
16588 | 260 |
|> transform_elim |> Drule.freeze_all |
261 |
|> ObjectLogic.atomize_thm |> make_nnf; |
|
16009 | 262 |
|
263 |
(*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
|
264 |
and also repeated declaration of Skolem functions*) |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
265 |
(* 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
|
266 |
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
|
267 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
268 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
269 |
(*Generate Skolem functions for a theorem supplied in nnf*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
270 |
fun skolem_of_nnf th = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
271 |
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
|
272 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
273 |
(*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
|
274 |
(*also works for HOL*) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
275 |
fun skolem_thm th = |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
276 |
let val nnfth = to_nnf th |
19175 | 277 |
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
|
278 |
end |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
279 |
handle THM _ => []; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
280 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
281 |
(*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
|
282 |
It returns a modified theory, unless skolemization fails.*) |
16009 | 283 |
fun skolem thy (name,th) = |
16588 | 284 |
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
|
285 |
in Option.map |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
286 |
(fn nnfth => |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
287 |
let val (thy',defs) = declare_skofuns cname nnfth thy |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
288 |
val skoths = map skolem_of_def defs |
19175 | 289 |
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
|
290 |
(SOME (to_nnf th) handle THM _ => NONE) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
291 |
end; |
16009 | 292 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
293 |
(*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
|
294 |
and modified theory.*) |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
295 |
fun skolem_cache_thm ((name,th), thy) = |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
296 |
case Symtab.lookup (!clause_cache) name of |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
297 |
NONE => |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
298 |
(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
|
299 |
NONE => ([th],thy) |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
300 |
| SOME (thy',cls) => |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
301 |
(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
|
302 |
| SOME (th',cls) => |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
303 |
if eq_thm(th,th') then (cls,thy) |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
304 |
else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
305 |
warning (string_of_thm th); |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
306 |
warning (string_of_thm th'); |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
307 |
([th],thy)); |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
308 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
309 |
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
|
310 |
|
16009 | 311 |
|
312 |
(*Exported function to convert Isabelle theorems into axiom clauses*) |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
313 |
fun cnf_axiom_g cnf (name,th) = |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
314 |
case name of |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
315 |
"" => cnf th (*no name, so can't cache*) |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
316 |
| s => case Symtab.lookup (!clause_cache) s of |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
317 |
NONE => |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
318 |
let val cls = cnf th |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
319 |
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
|
320 |
| SOME(th',cls) => |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
321 |
if eq_thm(th,th') then cls |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
322 |
else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
323 |
warning (string_of_thm th); |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
324 |
warning (string_of_thm th'); |
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
325 |
cls); |
15347 | 326 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
327 |
fun pairname th = (Thm.name_of_thm th, th); |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
328 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
329 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
330 |
val cnf_axiom = cnf_axiom_g skolem_thm; |
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
|
331 |
|
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
|
332 |
|
15956 | 333 |
fun meta_cnf_axiom th = |
334 |
map Meson.make_meta_clause (cnf_axiom (pairname th)); |
|
15499 | 335 |
|
15347 | 336 |
|
337 |
||
15872 | 338 |
(**** Extract and Clausify theorems from a theory's claset and simpset ****) |
15347 | 339 |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
340 |
(*Preserve the name of "th" after the transformation "f"*) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
341 |
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
|
342 |
|
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
343 |
(*Tags identify the major premise or conclusion, as hints to resolution provers. |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
344 |
However, they don't appear to help in recent tests, and they complicate the code.*) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
345 |
val tagI = thm "tagI"; |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
346 |
val tagD = thm "tagD"; |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
347 |
|
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
348 |
val tag_intro = preserve_name (fn th => th RS tagI); |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
349 |
val tag_elim = preserve_name (fn th => tagD RS th); |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
350 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
351 |
fun rules_of_claset cs = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
352 |
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs |
19175 | 353 |
val intros = safeIs @ hazIs |
18532 | 354 |
val elims = map Classical.classical_rule (safeEs @ hazEs) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
355 |
in |
18680 | 356 |
Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
357 |
" elims: " ^ Int.toString(length elims)); |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
358 |
if tagging_enabled |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
359 |
then map pairname (map tag_intro intros @ map tag_elim elims) |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
360 |
else map pairname (intros @ elims) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
361 |
end; |
15347 | 362 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
363 |
fun rules_of_simpset ss = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
364 |
let val ({rules,...}, _) = rep_ss ss |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
365 |
val simps = Net.entries rules |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
366 |
in |
18680 | 367 |
Output.debug ("rules_of_simpset: " ^ Int.toString(length simps)); |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
368 |
map (fn r => (#name r, #thm r)) simps |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
369 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
370 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
371 |
fun claset_rules_of_thy thy = rules_of_claset (claset_of thy); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
372 |
fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
373 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
374 |
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
|
375 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
376 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
377 |
fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt); |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
378 |
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); |
15347 | 379 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
380 |
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpSet.atp_rules_of_ctxt ctxt); |
15347 | 381 |
|
15872 | 382 |
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) |
15347 | 383 |
|
384 |
(* classical rules *) |
|
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
|
385 |
fun cnf_rules_g cnf_axiom [] err_list = ([],err_list) |
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
|
386 |
| cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = |
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
|
387 |
let val (ts,es) = cnf_rules_g cnf_axiom ths err_list |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
388 |
in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; |
15347 | 389 |
|
390 |
||
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
|
391 |
(*works for both FOL and HOL*) |
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
|
392 |
val cnf_rules = cnf_rules_g cnf_axiom; |
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
|
393 |
|
18274
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
394 |
fun cnf_rules1 [] err_list = ([],err_list) |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
395 |
| cnf_rules1 ((name,th) :: ths) err_list = |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
396 |
let val (ts,es) = cnf_rules1 ths err_list |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
397 |
in |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
398 |
((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end; |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
399 |
|
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
400 |
fun cnf_rules2 [] err_list = ([],err_list) |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
401 |
| cnf_rules2 ((name,th) :: ths) err_list = |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
402 |
let val (ts,es) = cnf_rules2 ths err_list |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
403 |
in |
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset
|
404 |
((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) end; |
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
|
405 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
406 |
fun clausify_rules_pairs_abs_aux [] err_list = ([],err_list) |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
407 |
| clausify_rules_pairs_abs_aux ((name,th)::ths) err_list = |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
408 |
let val (ts,es) = clausify_rules_pairs_abs_aux ths err_list |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
409 |
fun pair_name_cls k (n, []) = [] |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
410 |
| pair_name_cls k (n, (cls::clss)) = |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
411 |
(prop_of cls,(n,k))::(pair_name_cls (k + 1) (n, clss)) |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
412 |
in |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
413 |
(pair_name_cls 0 (name,(cnf_axiom(name,th)))::ts,es) handle _ => (ts,(name::es)) |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
414 |
end; |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
415 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
416 |
fun clausify_rules_pairs_abs thms = fst (clausify_rules_pairs_abs_aux thms []); |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
417 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
418 |
|
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
|
419 |
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) |
15347 | 420 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
421 |
fun make_axiom_clauses _ _ [] = [] |
18920 | 422 |
| make_axiom_clauses name i (th::ths) = |
423 |
case ResClause.make_axiom_clause (prop_of th) (name,i) of |
|
424 |
SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths |
|
425 |
| NONE => make_axiom_clauses name i ths; |
|
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
|
426 |
|
17829 | 427 |
(* outputs a list of (clause,theorem) pairs *) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
428 |
fun clausify_axiom_pairs (name,th) = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
429 |
filter (fn (c,th) => not (ResClause.isTaut c)) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
430 |
(make_axiom_clauses name 0 (cnf_axiom (name,th))); |
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
|
431 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
432 |
fun make_axiom_clausesH _ _ [] = [] |
18920 | 433 |
| make_axiom_clausesH name i (th::ths) = |
434 |
(ResHolClause.make_axiom_clause (prop_of th) (name,i), th) :: |
|
435 |
(make_axiom_clausesH name (i+1) ths) |
|
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
|
436 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
437 |
fun clausify_axiom_pairsH (name,th) = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
438 |
filter (fn (c,th) => not (ResHolClause.isTaut c)) |
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
|
439 |
(make_axiom_clausesH name 0 (cnf_axiom (name,th))); |
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
|
440 |
|
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
|
441 |
|
17829 | 442 |
fun clausify_rules_pairs_aux result [] = result |
443 |
| clausify_rules_pairs_aux result ((name,th)::ths) = |
|
444 |
clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths |
|
445 |
handle THM (msg,_,_) => |
|
18680 | 446 |
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); |
17829 | 447 |
clausify_rules_pairs_aux result ths) |
448 |
| ResClause.CLAUSE (msg,t) => |
|
18680 | 449 |
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ |
17829 | 450 |
": " ^ TermLib.string_of_term t); |
451 |
clausify_rules_pairs_aux result ths) |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
452 |
|
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
|
453 |
|
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
|
454 |
fun clausify_rules_pairs_auxH result [] = result |
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
|
455 |
| clausify_rules_pairs_auxH result ((name,th)::ths) = |
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
|
456 |
clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths |
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
|
457 |
handle THM (msg,_,_) => |
18680 | 458 |
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); |
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
|
459 |
clausify_rules_pairs_auxH result ths) |
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
|
460 |
| ResHolClause.LAM2COMB (t) => |
18680 | 461 |
(Output.debug ("Cannot clausify " ^ TermLib.string_of_term t); |
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
|
462 |
clausify_rules_pairs_auxH result ths) |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
16012
diff
changeset
|
463 |
|
15347 | 464 |
|
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
|
465 |
|
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
|
466 |
val clausify_rules_pairs = clausify_rules_pairs_aux []; |
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
|
467 |
|
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
|
468 |
val clausify_rules_pairsH = clausify_rules_pairs_auxH []; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
469 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
470 |
(*These should include any plausibly-useful theorems, especially if they need |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
471 |
Skolem functions. FIXME: this list is VERY INCOMPLETE*) |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
472 |
val default_initial_thms = map pairname |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
473 |
[refl_def, antisym_def, sym_def, trans_def, single_valued_def, |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
474 |
subset_refl, Union_least, Inter_greatest]; |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
475 |
|
16009 | 476 |
(*Setup function: takes a theory and installs ALL simprules and claset rules |
477 |
into the clause cache*) |
|
478 |
fun clause_cache_setup thy = |
|
479 |
let val simps = simpset_rules_of_thy thy |
|
480 |
and clas = claset_rules_of_thy thy |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
481 |
and thy0 = List.foldl skolem_cache thy default_initial_thms |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
482 |
val thy1 = List.foldl skolem_cache thy0 clas |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
483 |
in List.foldl skolem_cache thy1 simps end; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
484 |
(*Could be duplicate theorem names, due to multiple attributes*) |
16009 | 485 |
|
16563 | 486 |
|
487 |
(*** meson proof methods ***) |
|
488 |
||
489 |
fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) [])); |
|
490 |
||
491 |
fun meson_meth ths ctxt = |
|
492 |
Method.SIMPLE_METHOD' HEADGOAL |
|
493 |
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt)); |
|
494 |
||
495 |
val meson_method_setup = |
|
18708 | 496 |
Method.add_methods |
497 |
[("meson", Method.thms_ctxt_args meson_meth, |
|
18833 | 498 |
"MESON resolution proof procedure")]; |
15347 | 499 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
500 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
501 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
502 |
(*** The Skolemization attribute ***) |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
503 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
504 |
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
|
505 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
506 |
(*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
|
507 |
val conj_rule = foldr1 conj2_rule; |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
508 |
|
18728 | 509 |
fun skolem (Context.Theory thy, th) = |
510 |
let |
|
511 |
val name = Thm.name_of_thm th |
|
512 |
val (cls, thy') = skolem_cache_thm ((name, th), thy) |
|
513 |
in (Context.Theory thy', conj_rule cls) end |
|
514 |
| 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
|
515 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
516 |
val setup_attrs = Attrib.add_attributes |
18728 | 517 |
[("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
|
518 |
|
18708 | 519 |
val setup = clause_cache_setup #> setup_attrs; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
520 |
|
15347 | 521 |
end; |