author | wenzelm |
Fri, 29 Sep 2006 22:46:59 +0200 | |
changeset 20783 | 17114542d2d4 |
parent 20774 | 8f947ffb5eb8 |
child 20789 | e279499c4f80 |
permissions | -rw-r--r-- |
15347 | 1 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
2 |
ID: $Id$ |
|
3 |
Copyright 2004 University of Cambridge |
|
4 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
5 |
Transformation of axiom rules (elim/intro/etc) into CNF forms. |
15347 | 6 |
*) |
7 |
||
20445 | 8 |
(*FIXME: does this signature serve any purpose?*) |
15997 | 9 |
signature RES_AXIOMS = |
10 |
sig |
|
11 |
val elimRule_tac : thm -> Tactical.tactic |
|
16012 | 12 |
val elimR2Fol : thm -> term |
15997 | 13 |
val transform_elim : thm -> thm |
14 |
val cnf_axiom : (string * thm) -> thm list |
|
15 |
val meta_cnf_axiom : thm -> thm list |
|
16 |
val claset_rules_of_thy : theory -> (string * thm) list |
|
17 |
val simpset_rules_of_thy : theory -> (string * thm) list |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
18 |
val claset_rules_of_ctxt: Proof.context -> (string * thm) list |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
19 |
val simpset_rules_of_ctxt : Proof.context -> (string * thm) list |
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
17829
diff
changeset
|
20 |
val pairname : thm -> (string * thm) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
21 |
val skolem_thm : thm -> thm list |
20419 | 22 |
val to_nnf : thm -> thm |
19353 | 23 |
val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list; |
18708 | 24 |
val meson_method_setup : theory -> theory |
25 |
val setup : theory -> theory |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
26 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
27 |
val atpset_rules_of_thy : theory -> (string * thm) list |
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
28 |
val atpset_rules_of_ctxt : Proof.context -> (string * thm) list |
15997 | 29 |
end; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
30 |
|
20419 | 31 |
structure ResAxioms = |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
32 |
|
15997 | 33 |
struct |
15347 | 34 |
|
20419 | 35 |
(*FIXME DELETE: For running the comparison between combinators and abstractions. |
36 |
CANNOT be a ref, as the setting is used while Isabelle is built.*) |
|
37 |
val abstract_lambdas = true; |
|
38 |
||
39 |
val trace_abs = ref false; |
|
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset
|
40 |
|
20445 | 41 |
(*Store definitions of abstraction functions, ensuring that identical right-hand |
42 |
sides are denoted by the same functions and thereby reducing the need for |
|
43 |
extensionality in proofs. |
|
44 |
FIXME! Store in theory data!!*) |
|
45 |
val abstraction_cache = ref Net.empty : thm Net.net ref; |
|
46 |
||
15997 | 47 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 48 |
|
15390 | 49 |
(* a tactic used to prove an elim-rule. *) |
16009 | 50 |
fun elimRule_tac th = |
20419 | 51 |
(resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1); |
15347 | 52 |
|
15956 | 53 |
fun add_EX tm [] = tm |
54 |
| add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; |
|
15347 | 55 |
|
19894 | 56 |
(*Checks for the premise ~P when the conclusion is P.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
57 |
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) |
19894 | 58 |
(Const("Trueprop",_) $ Free(q,_)) = (p = q) |
15371 | 59 |
| is_neg _ _ = false; |
60 |
||
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
61 |
exception ELIMR2FOL; |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
62 |
|
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
63 |
(*Handles the case where the dummy "conclusion" variable appears negated in the |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
64 |
premises, so the final consequent must be kept.*) |
15371 | 65 |
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = |
19894 | 66 |
strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
67 |
| strip_concl' prems bvs P = |
15956 | 68 |
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) |
19894 | 69 |
in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; |
15371 | 70 |
|
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
71 |
(*Recurrsion over the minor premise of an elimination rule. Final consequent |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
72 |
is ignored, as it is the dummy "conclusion" variable.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
73 |
fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
74 |
strip_concl prems ((x,xtp)::bvs) concl body |
15371 | 75 |
| strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
76 |
if (is_neg P concl) then (strip_concl' prems bvs Q) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
77 |
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
78 |
| strip_concl prems bvs concl Q = |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
79 |
if concl aconv Q then add_EX (foldr1 HOLogic.mk_conj prems) bvs |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
80 |
else raise ELIMR2FOL (*expected conclusion not found!*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
81 |
|
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
82 |
fun trans_elim (major,[],_) = HOLogic.Not $ major |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
83 |
| trans_elim (major,minors,concl) = |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
84 |
let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors) |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
85 |
in HOLogic.mk_imp (major, disjs) end; |
15347 | 86 |
|
16012 | 87 |
(* convert an elim rule into an equivalent formula, of type term. *) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
88 |
fun elimR2Fol elimR = |
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset
|
89 |
let val elimR' = #1 (Drule.freeze_thaw elimR) |
19894 | 90 |
val (prems,concl) = (prems_of elimR', concl_of elimR') |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
91 |
val cv = case concl of (*conclusion variable*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
92 |
Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
93 |
| v as Free(_, Type("prop",[])) => v |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
94 |
| _ => raise ELIMR2FOL |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
95 |
in case prems of |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
96 |
[] => raise ELIMR2FOL |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
97 |
| (Const("Trueprop",_) $ major) :: minors => |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
98 |
if member (op aconv) (term_frees major) cv then raise ELIMR2FOL |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
99 |
else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL) |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
100 |
| _ => raise ELIMR2FOL |
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
101 |
end; |
15347 | 102 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
103 |
(* convert an elim-rule into an equivalent theorem that does not have the |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
104 |
predicate variable. Leave other theorems unchanged.*) |
16009 | 105 |
fun transform_elim th = |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
106 |
let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th)) |
18009 | 107 |
in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
108 |
handle ELIMR2FOL => th (*not an elimination rule*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
109 |
| exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
110 |
" for theorem " ^ string_of_thm th); th) |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
111 |
|
15997 | 112 |
|
113 |
(**** Transformation of Clasets and Simpsets into First-Order Axioms ****) |
|
114 |
||
16563 | 115 |
(*Transfer a theorem into theory Reconstruction.thy if it is not already |
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset
|
116 |
inside that theory -- because it's needed for Skolemization *) |
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset
|
117 |
|
16563 | 118 |
(*This will refer to the final version of theory Reconstruction.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
119 |
val recon_thy_ref = Theory.self_ref (the_context ()); |
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset
|
120 |
|
16563 | 121 |
(*If called while Reconstruction is being created, it will transfer to the |
122 |
current version. If called afterward, it will transfer to the final version.*) |
|
16009 | 123 |
fun transfer_to_Reconstruction th = |
16563 | 124 |
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; |
15347 | 125 |
|
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
126 |
fun is_taut th = |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
127 |
case (prop_of th) of |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
128 |
(Const ("Trueprop", _) $ Const ("True", _)) => true |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
129 |
| _ => false; |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
130 |
|
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
131 |
(* remove tautologous clauses *) |
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset
|
132 |
val rm_redundant_cls = List.filter (not o is_taut); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
133 |
|
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
134 |
|
16009 | 135 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
136 |
||
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
137 |
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
138 |
prefix for the Skolem constant. Result is a new theory*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
139 |
fun declare_skofuns s th thy = |
20419 | 140 |
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
141 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
20624
ba081ac0ed7e
sko/abs: Name.internal prevents choking of print_theory;
wenzelm
parents:
20567
diff
changeset
|
142 |
let val cname = Name.internal (gensym ("sko_" ^ s ^ "_")) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
143 |
val args = term_frees xtp (*get the formal parameter list*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
144 |
val Ts = map type_of args |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
145 |
val cT = Ts ---> T |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
146 |
val c = Const (Sign.full_name thy cname, cT) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
147 |
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
148 |
(*Forms a lambda-abstraction over the formal parameters*) |
20783 | 149 |
val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
150 |
(*Theory is augmented with the constant, then its def*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
151 |
val cdef = cname ^ "_def" |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
152 |
val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
153 |
in dec_sko (subst_bound (list_comb(c,args), p)) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
154 |
(thy'', get_axiom thy'' cdef :: axs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
155 |
end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
156 |
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
157 |
(*Universal quant: insert a free variable into body and continue*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
158 |
let val fname = Name.variant (add_term_names (p,[])) a |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
159 |
in dec_sko (subst_bound (Free(fname,T), p)) thx end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
160 |
| dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
161 |
| dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
162 |
| dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
163 |
| dec_sko t thx = thx (*Do nothing otherwise*) |
20419 | 164 |
in dec_sko (prop_of th) (thy,[]) end; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
165 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
166 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
167 |
fun assume_skofuns th = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
168 |
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
169 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
170 |
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
171 |
val args = term_frees xtp \\ skos (*the formal parameters*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
172 |
val Ts = map type_of args |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
173 |
val cT = Ts ---> T |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
174 |
val c = Free (gensym "sko_", cT) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
175 |
val rhs = list_abs_free (map dest_Free args, |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
176 |
HOLogic.choice_const T $ xtp) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
177 |
(*Forms a lambda-abstraction over the formal parameters*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
178 |
val def = equals cT $ c $ rhs |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
179 |
in dec_sko (subst_bound (list_comb(c,args), p)) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
180 |
(def :: defs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
181 |
end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
182 |
| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
183 |
(*Universal quant: insert a free variable into body and continue*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
184 |
let val fname = Name.variant (add_term_names (p,[])) a |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
185 |
in dec_sko (subst_bound (Free(fname,T), p)) defs end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
186 |
| dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
187 |
| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
188 |
| dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
189 |
| dec_sko t defs = defs (*Do nothing otherwise*) |
20419 | 190 |
in dec_sko (prop_of th) [] end; |
191 |
||
192 |
||
193 |
(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) |
|
194 |
||
195 |
(*Returns the vars of a theorem*) |
|
196 |
fun vars_of_thm th = |
|
20445 | 197 |
map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []); |
20419 | 198 |
|
199 |
(*Make a version of fun_cong with a given variable name*) |
|
200 |
local |
|
201 |
val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
|
202 |
val cx = hd (vars_of_thm fun_cong'); |
|
203 |
val ty = typ_of (ctyp_of_term cx); |
|
20445 | 204 |
val thy = theory_of_thm fun_cong; |
20419 | 205 |
fun mkvar a = cterm_of thy (Var((a,0),ty)); |
206 |
in |
|
207 |
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' |
|
208 |
end; |
|
209 |
||
210 |
(*Removes the lambdas from an equation of the form t = (%x. u)*) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
211 |
fun strip_lambdas th = |
20419 | 212 |
case prop_of th of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
213 |
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => |
20419 | 214 |
strip_lambdas (#1 (Drule.freeze_thaw (th RS xfun_cong x))) |
215 |
| _ => th; |
|
216 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
217 |
(*Convert meta- to object-equality. Fails for theorems like split_comp_eq, |
20419 | 218 |
where some types have the empty sort.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
219 |
fun object_eq th = th RS def_imp_eq |
20419 | 220 |
handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
221 |
|
20419 | 222 |
(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*) |
223 |
fun eta_conversion_rule th = |
|
224 |
equal_elim (eta_conversion (cprop_of th)) th; |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
225 |
|
20445 | 226 |
fun crhs_of th = |
20419 | 227 |
case Drule.strip_comb (cprop_of th) of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
228 |
(f, [_, rhs]) => |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
229 |
(case term_of f of Const ("==", _) => rhs |
20445 | 230 |
| _ => raise THM ("crhs_of", 0, [th])) |
231 |
| _ => raise THM ("crhs_of", 1, [th]); |
|
232 |
||
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
233 |
fun lhs_of th = |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
234 |
case prop_of th of (Const("==",_) $ lhs $ _) => lhs |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
235 |
| _ => raise THM ("lhs_of", 1, [th]); |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
236 |
|
20445 | 237 |
fun rhs_of th = |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
238 |
case prop_of th of (Const("==",_) $ _ $ rhs) => rhs |
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
239 |
| _ => raise THM ("rhs_of", 1, [th]); |
20419 | 240 |
|
241 |
(*Apply a function definition to an argument, beta-reducing the result.*) |
|
242 |
fun beta_comb cf x = |
|
243 |
let val th1 = combination cf (reflexive x) |
|
20445 | 244 |
val th2 = beta_conversion false (crhs_of th1) |
20419 | 245 |
in transitive th1 th2 end; |
246 |
||
247 |
(*Apply a function definition to arguments, beta-reducing along the way.*) |
|
248 |
fun list_combination cf [] = cf |
|
249 |
| list_combination cf (x::xs) = list_combination (beta_comb cf x) xs; |
|
250 |
||
251 |
fun list_cabs ([] , t) = t |
|
252 |
| list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); |
|
253 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
254 |
fun assert_eta_free ct = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
255 |
let val t = term_of ct |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
256 |
in if (t aconv Envir.eta_contract t) then () |
20419 | 257 |
else error ("Eta redex in term: " ^ string_of_cterm ct) |
258 |
end; |
|
259 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
260 |
fun eq_absdef (th1, th2) = |
20445 | 261 |
Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso |
262 |
rhs_of th1 aconv rhs_of th2; |
|
263 |
||
264 |
fun lambda_free (Abs _) = false |
|
265 |
| lambda_free (t $ u) = lambda_free t andalso lambda_free u |
|
266 |
| lambda_free _ = true; |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
267 |
|
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
268 |
fun monomorphic t = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
269 |
Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true; |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
270 |
|
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
271 |
fun dest_abs_list ct = |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
272 |
let val (cv,ct') = Thm.dest_abs NONE ct |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
273 |
val (cvs,cu) = dest_abs_list ct' |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
274 |
in (cv::cvs, cu) end |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
275 |
handle CTERM _ => ([],ct); |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
276 |
|
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
277 |
fun lambda_list [] u = u |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
278 |
| lambda_list (v::vs) u = lambda v (lambda_list vs u); |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
279 |
|
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
280 |
fun abstract_rule_list [] [] th = th |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
281 |
| abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th) |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
282 |
| abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]); |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
283 |
|
20419 | 284 |
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested |
285 |
prefix for the constants. Resulting theory is returned in the first theorem. *) |
|
286 |
fun declare_absfuns th = |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
287 |
let fun abstract thy ct = |
20445 | 288 |
if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) |
289 |
else |
|
290 |
case term_of ct of |
|
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
291 |
Abs _ => |
20624
ba081ac0ed7e
sko/abs: Name.internal prevents choking of print_theory;
wenzelm
parents:
20567
diff
changeset
|
292 |
let val cname = Name.internal (gensym "abs_"); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
293 |
val _ = assert_eta_free ct; |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
294 |
val (cvs,cta) = dest_abs_list ct |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
295 |
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
296 |
val (u'_th,defs) = abstract thy cta |
20445 | 297 |
val cu' = crhs_of u'_th |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
298 |
val abs_v_u = lambda_list (map term_of cvs) (term_of cu') |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
299 |
(*get the formal parameters: ALL variables free in the term*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
300 |
val args = term_frees abs_v_u |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
301 |
val rhs = list_abs_free (map dest_Free args, abs_v_u) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
302 |
(*Forms a lambda-abstraction over the formal parameters*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
303 |
val v_rhs = Logic.varify rhs |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
304 |
val (ax,thy) = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
305 |
case List.find (fn ax => v_rhs aconv rhs_of ax) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
306 |
(Net.match_term (!abstraction_cache) v_rhs) of |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
307 |
SOME ax => (ax,thy) (*cached axiom, current theory*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
308 |
| NONE => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
309 |
let val Ts = map type_of args |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
310 |
val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
311 |
val thy = theory_of_thm u'_th |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
312 |
val c = Const (Sign.full_name thy cname, cT) |
20783 | 313 |
val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
314 |
(*Theory is augmented with the constant, |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
315 |
then its definition*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
316 |
val cdef = cname ^ "_def" |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
317 |
val thy = Theory.add_defs_i false false |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
318 |
[(cdef, equals cT $ c $ rhs)] thy |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
319 |
val ax = get_axiom thy cdef |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
320 |
val _ = abstraction_cache := Net.insert_term eq_absdef (v_rhs,ax) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
321 |
(!abstraction_cache) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
322 |
handle Net.INSERT => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
323 |
raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
324 |
in (ax,thy) end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
325 |
val _ = assert (v_rhs aconv rhs_of ax) "declare_absfuns: rhs mismatch" |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
326 |
val def = #1 (Drule.freeze_thaw ax) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
327 |
val def_args = list_combination def (map (cterm_of thy) args) |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
328 |
in (transitive (abstract_rule_list vs cvs u'_th) (symmetric def_args), |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
329 |
def :: defs) end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
330 |
| (t1$t2) => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
331 |
let val (ct1,ct2) = Thm.dest_comb ct |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
332 |
val (th1,defs1) = abstract thy ct1 |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
333 |
val (th2,defs2) = abstract (theory_of_thm th1) ct2 |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
334 |
in (combination th1 th2, defs1@defs2) end |
20419 | 335 |
val _ = if !trace_abs then warning (string_of_thm th) else (); |
336 |
val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) |
|
337 |
val ths = equal_elim eqth th :: |
|
338 |
map (forall_intr_vars o strip_lambdas o object_eq) defs |
|
339 |
in (theory_of_thm eqth, ths) end; |
|
340 |
||
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset
|
341 |
fun name_of def = SOME (#1 (dest_Free (lhs_of def))) handle _ => NONE; |
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset
|
342 |
|
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
343 |
(*A name is valid provided it isn't the name of a defined abstraction.*) |
20567
93ae490fe02c
Bug fix to prevent exception dest_Free from escaping
paulson
parents:
20525
diff
changeset
|
344 |
fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs)) |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
345 |
| valid_name defs _ = false; |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
346 |
|
20419 | 347 |
fun assume_absfuns th = |
20445 | 348 |
let val thy = theory_of_thm th |
349 |
val cterm = cterm_of thy |
|
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
350 |
fun abstract ct = |
20445 | 351 |
if lambda_free (term_of ct) then (reflexive ct, []) |
352 |
else |
|
353 |
case term_of ct of |
|
20419 | 354 |
Abs (_,T,u) => |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
355 |
let val _ = assert_eta_free ct; |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
356 |
val (cvs,cta) = dest_abs_list ct |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
357 |
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs) |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
358 |
val (u'_th,defs) = abstract cta |
20445 | 359 |
val cu' = crhs_of u'_th |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
360 |
(*Could use Thm.cabs instead of lambda to work at level of cterms*) |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
361 |
val abs_v_u = lambda_list (map term_of cvs) (term_of cu') |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
362 |
(*get the formal parameters: free variables not present in the defs |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
363 |
(to avoid taking abstraction function names as parameters) *) |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
364 |
val args = filter (valid_name defs) (term_frees abs_v_u) |
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
365 |
val crhs = list_cabs (map cterm args, cterm abs_v_u) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
366 |
(*Forms a lambda-abstraction over the formal parameters*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
367 |
val rhs = term_of crhs |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
368 |
val def = (*FIXME: can we also reuse the const-abstractions?*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
369 |
case List.find (fn ax => rhs aconv rhs_of ax andalso |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
370 |
Context.joinable (thy, theory_of_thm ax)) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
371 |
(Net.match_term (!abstraction_cache) rhs) of |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
372 |
SOME ax => ax |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
373 |
| NONE => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
374 |
let val Ts = map type_of args |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
375 |
val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu')) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
376 |
val c = Free (gensym "abs_", const_ty) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
377 |
val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
378 |
val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
379 |
(!abstraction_cache) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
380 |
handle Net.INSERT => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
381 |
raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
382 |
in ax end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
383 |
val _ = assert (rhs aconv rhs_of def) "assume_absfuns: rhs mismatch" |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
384 |
val def_args = list_combination def (map cterm args) |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
385 |
in (transitive (abstract_rule_list vs cvs u'_th) (symmetric def_args), |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
386 |
def :: defs) end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
387 |
| (t1$t2) => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
388 |
let val (ct1,ct2) = Thm.dest_comb ct |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
389 |
val (t1',defs1) = abstract ct1 |
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
390 |
val (t2',defs2) = abstract ct2 |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
391 |
in (combination t1' t2', defs1@defs2) end |
20525
4b0fdb18ea9a
bug fix to abstractions: free variables in theorem can be abstracted over.
paulson
parents:
20473
diff
changeset
|
392 |
val (eqth,defs) = abstract (cprop_of th) |
20419 | 393 |
in equal_elim eqth th :: |
394 |
map (forall_intr_vars o strip_lambdas o object_eq) defs |
|
395 |
end; |
|
396 |
||
16009 | 397 |
|
398 |
(*cterms are used throughout for efficiency*) |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
399 |
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; |
16009 | 400 |
|
401 |
(*cterm version of mk_cTrueprop*) |
|
402 |
fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
403 |
||
404 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
405 |
ones. Return the body, along with the list of free variables.*) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
406 |
fun c_variant_abs_multi (ct0, vars) = |
16009 | 407 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
408 |
in c_variant_abs_multi (ct, cv::vars) end |
|
409 |
handle CTERM _ => (ct0, rev vars); |
|
410 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
411 |
(*Given the definition of a Skolem function, return a theorem to replace |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
412 |
an existential formula by a use of that function. |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
413 |
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
414 |
fun skolem_of_def def = |
20292
6f2b8ed987ec
removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
wenzelm
parents:
20071
diff
changeset
|
415 |
let val (c,rhs) = Drule.dest_equals (cprop_of (#1 (Drule.freeze_thaw def))) |
16009 | 416 |
val (ch, frees) = c_variant_abs_multi (rhs, []) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
417 |
val (chilbert,cabs) = Thm.dest_comb ch |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
418 |
val {sign,t, ...} = rep_cterm chilbert |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
419 |
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
|
420 |
| _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) |
16009 | 421 |
val cex = Thm.cterm_of sign (HOLogic.exists_const T) |
422 |
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
|
423 |
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
|
424 |
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
425 |
in Goal.prove_raw [ex_tm] conc tacf |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
426 |
|> forall_intr_list frees |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
427 |
|> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
428 |
|> Thm.varifyT |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
429 |
end; |
16009 | 430 |
|
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
|
431 |
(*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
|
432 |
(*It now works for HOL too. *) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
433 |
fun to_nnf th = |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
434 |
th |> transfer_to_Reconstruction |
20419 | 435 |
|> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1 |
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
436 |
|> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas; |
16009 | 437 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
438 |
(*The cache prevents repeated clausification of a theorem, |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
439 |
and also repeated declaration of Skolem functions*) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
440 |
(* 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
|
441 |
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
|
442 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
443 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
444 |
(*Generate Skolem functions for a theorem supplied in nnf*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
445 |
fun skolem_of_nnf th = |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
446 |
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
|
447 |
|
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
448 |
fun assert_lambda_free ths = assert (forall (lambda_free o prop_of) ths); |
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
449 |
|
20445 | 450 |
fun assume_abstract th = |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
451 |
if lambda_free (prop_of th) then [th] |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
452 |
else th |> eta_conversion_rule |> assume_absfuns |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
453 |
|> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") |
20445 | 454 |
|
20419 | 455 |
(*Replace lambdas by assumed function definitions in the theorems*) |
20445 | 456 |
fun assume_abstract_list ths = |
457 |
if abstract_lambdas then List.concat (map assume_abstract ths) |
|
20419 | 458 |
else map eta_conversion_rule ths; |
459 |
||
460 |
(*Replace lambdas by declared function definitions in the theorems*) |
|
461 |
fun declare_abstract' (thy, []) = (thy, []) |
|
462 |
| declare_abstract' (thy, th::ths) = |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
463 |
let val (thy', th_defs) = |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
464 |
if lambda_free (prop_of th) then (thy, [th]) |
20445 | 465 |
else |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
466 |
th |> zero_var_indexes |> Drule.freeze_thaw |> #1 |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
467 |
|> eta_conversion_rule |> transfer thy |> declare_absfuns |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
468 |
val _ = assert_lambda_free th_defs "declare_abstract: lambdas" |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
469 |
val (thy'', ths') = declare_abstract' (thy', ths) |
20419 | 470 |
in (thy'', th_defs @ ths') end; |
471 |
||
20421 | 472 |
(*FIXME DELETE if we decide to switch to abstractions*) |
20419 | 473 |
fun declare_abstract (thy, ths) = |
474 |
if abstract_lambdas then declare_abstract' (thy, ths) |
|
475 |
else (thy, map eta_conversion_rule ths); |
|
476 |
||
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
477 |
(*Skolemize a named theorem, with Skolem functions as additional premises.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
478 |
(*also works for HOL*) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
479 |
fun skolem_thm th = |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
480 |
let val nnfth = to_nnf th |
20419 | 481 |
in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |
20445 | 482 |
|> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
483 |
end |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
484 |
handle THM _ => []; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
485 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
486 |
(*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
|
487 |
It returns a modified theory, unless skolemization fails.*) |
16009 | 488 |
fun skolem thy (name,th) = |
20419 | 489 |
let val cname = (case name of "" => gensym "" | s => Sign.base_name s) |
490 |
val _ = Output.debug ("skolemizing " ^ name ^ ": ") |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
491 |
in Option.map |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
492 |
(fn nnfth => |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
493 |
let val (thy',defs) = declare_skofuns cname nnfth thy |
20419 | 494 |
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth |
495 |
val (thy'',cnfs') = declare_abstract (thy',cnfs) |
|
496 |
in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs')) |
|
497 |
end) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
498 |
(SOME (to_nnf th) handle THM _ => NONE) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
499 |
end; |
16009 | 500 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
501 |
(*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
|
502 |
and modified theory.*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
503 |
fun skolem_cache_thm (name,th) thy = |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
504 |
case Symtab.lookup (!clause_cache) name of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
505 |
NONE => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
506 |
(case skolem thy (name, Thm.transfer thy th) of |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
507 |
NONE => ([th],thy) |
20473
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
508 |
| SOME (thy',cls) => |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
509 |
let val cls = map Drule.local_standard cls |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
510 |
in |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
511 |
if null cls then warning ("skolem_cache: empty clause set for " ^ name) |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
512 |
else (); |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
513 |
change clause_cache (Symtab.update (name, (th, cls))); |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
514 |
(cls,thy') |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
515 |
end) |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
516 |
| SOME (th',cls) => |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
517 |
if eq_thm(th,th') then (cls,thy) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
518 |
else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
519 |
Output.debug (string_of_thm th); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
520 |
Output.debug (string_of_thm th'); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
521 |
([th],thy)); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
522 |
|
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
523 |
(*Exported function to convert Isabelle theorems into axiom clauses*) |
19894 | 524 |
fun cnf_axiom (name,th) = |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
525 |
case name of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
526 |
"" => skolem_thm th (*no name, so can't cache*) |
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset
|
527 |
| s => case Symtab.lookup (!clause_cache) s of |
20473
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
528 |
NONE => |
7ef72f030679
Using Drule.local_standard to reduce the space usage
paulson
parents:
20461
diff
changeset
|
529 |
let val cls = map Drule.local_standard (skolem_thm th) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
530 |
in change clause_cache (Symtab.update (s, (th, cls))); cls end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
531 |
| SOME(th',cls) => |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
532 |
if eq_thm(th,th') then cls |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
533 |
else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
534 |
Output.debug (string_of_thm th); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
535 |
Output.debug (string_of_thm th'); |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
536 |
cls); |
15347 | 537 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
538 |
fun pairname th = (Thm.name_of_thm th, th); |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
539 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
540 |
fun meta_cnf_axiom th = |
15956 | 541 |
map Meson.make_meta_clause (cnf_axiom (pairname th)); |
15499 | 542 |
|
15347 | 543 |
|
15872 | 544 |
(**** Extract and Clausify theorems from a theory's claset and simpset ****) |
15347 | 545 |
|
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
546 |
(*Preserve the name of "th" after the transformation "f"*) |
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
547 |
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
|
548 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
549 |
fun rules_of_claset cs = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
550 |
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs |
19175 | 551 |
val intros = safeIs @ hazIs |
18532 | 552 |
val elims = map Classical.classical_rule (safeEs @ hazEs) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
553 |
in |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
554 |
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
|
555 |
" elims: " ^ Int.toString(length elims)); |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
556 |
map pairname (intros @ elims) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
557 |
end; |
15347 | 558 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
559 |
fun rules_of_simpset ss = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
560 |
let val ({rules,...}, _) = rep_ss ss |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
561 |
val simps = Net.entries rules |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
562 |
in |
18680 | 563 |
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
|
564 |
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
|
565 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
566 |
|
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
567 |
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
|
568 |
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
|
569 |
|
20774 | 570 |
fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy)); |
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
571 |
|
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
572 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
573 |
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
|
574 |
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); |
15347 | 575 |
|
20774 | 576 |
fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt)); |
577 |
||
15347 | 578 |
|
15872 | 579 |
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) |
15347 | 580 |
|
19894 | 581 |
(* classical rules: works for both FOL and HOL *) |
582 |
fun cnf_rules [] err_list = ([],err_list) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
583 |
| cnf_rules ((name,th) :: ths) err_list = |
19894 | 584 |
let val (ts,es) = cnf_rules ths err_list |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
585 |
in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; |
15347 | 586 |
|
19894 | 587 |
fun pair_name_cls k (n, []) = [] |
588 |
| pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
589 |
|
19894 | 590 |
fun cnf_rules_pairs_aux pairs [] = pairs |
591 |
| cnf_rules_pairs_aux pairs ((name,th)::ths) = |
|
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
592 |
let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
593 |
handle THM _ => pairs | ResClause.CLAUSE _ => pairs |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
594 |
| ResHolClause.LAM2COMB _ => pairs |
19894 | 595 |
in cnf_rules_pairs_aux pairs' ths end; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
596 |
|
19894 | 597 |
val cnf_rules_pairs = cnf_rules_pairs_aux []; |
19353 | 598 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
599 |
|
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
|
600 |
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) |
15347 | 601 |
|
20419 | 602 |
(*Setup function: takes a theory and installs ALL known theorems into the clause cache*) |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
603 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
604 |
fun skolem_cache (name,th) thy = |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
605 |
let val prop = Thm.prop_of th |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
606 |
in |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
607 |
if lambda_free prop orelse monomorphic prop |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
608 |
then thy (*monomorphic theorems can be Skolemized on demand*) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
609 |
else #2 (skolem_cache_thm (name,th) thy) |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
610 |
end; |
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
611 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
612 |
fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy; |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
613 |
|
16563 | 614 |
|
615 |
(*** meson proof methods ***) |
|
616 |
||
617 |
fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) [])); |
|
618 |
||
619 |
fun meson_meth ths ctxt = |
|
620 |
Method.SIMPLE_METHOD' HEADGOAL |
|
621 |
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt)); |
|
622 |
||
623 |
val meson_method_setup = |
|
18708 | 624 |
Method.add_methods |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
625 |
[("meson", Method.thms_ctxt_args meson_meth, |
18833 | 626 |
"MESON resolution proof procedure")]; |
15347 | 627 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
628 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
629 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
630 |
(*** The Skolemization attribute ***) |
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
631 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
632 |
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
|
633 |
|
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
634 |
(*Conjoin a list of theorems to form a single theorem*) |
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
635 |
fun conj_rule [] = TrueI |
20445 | 636 |
| conj_rule ths = foldr1 conj2_rule ths; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
637 |
|
20419 | 638 |
fun skolem_attr (Context.Theory thy, th) = |
639 |
let val name = Thm.name_of_thm th |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
640 |
val (cls, thy') = skolem_cache_thm (name, th) thy |
18728 | 641 |
in (Context.Theory thy', conj_rule cls) end |
20419 | 642 |
| skolem_attr (context, th) = (context, conj_rule (skolem_thm th)); |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
643 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
644 |
val setup_attrs = Attrib.add_attributes |
20419 | 645 |
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")]; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
646 |
|
18708 | 647 |
val setup = clause_cache_setup #> setup_attrs; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
648 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
649 |
end; |