author | wenzelm |
Sun, 18 May 2008 15:04:09 +0200 | |
changeset 26939 | 1035c89b4c02 |
parent 26928 | ca87aff1ad2d |
child 27174 | c2c484480f40 |
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 |
||
15997 | 8 |
signature RES_AXIOMS = |
21505 | 9 |
sig |
24669 | 10 |
val cnf_axiom: thm -> thm list |
11 |
val pairname: thm -> string * thm |
|
24854 | 12 |
val multi_base_blacklist: string list |
25243 | 13 |
val bad_for_atp: thm -> bool |
25761 | 14 |
val type_has_empty_sort: typ -> bool |
24669 | 15 |
val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list |
16 |
val cnf_rules_of_ths: thm list -> thm list |
|
17 |
val neg_clausify: thm list -> thm list |
|
18 |
val expand_defs_tac: thm -> tactic |
|
24827 | 19 |
val combinators: thm -> thm |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
20 |
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
21 |
val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
22 |
val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) |
21505 | 23 |
val atpset_rules_of: Proof.context -> (string * thm) list |
24669 | 24 |
val meson_method_setup: theory -> theory |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
25 |
val clause_cache_endtheory: theory -> theory option |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
26 |
val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) |
24669 | 27 |
val setup: theory -> theory |
21505 | 28 |
end; |
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
29 |
|
24669 | 30 |
structure ResAxioms: RES_AXIOMS = |
15997 | 31 |
struct |
15347 | 32 |
|
20902 | 33 |
(* FIXME legacy *) |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
34 |
fun freeze_thm th = #1 (Drule.freeze_thaw th); |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
35 |
|
25761 | 36 |
fun type_has_empty_sort (TFree (_, [])) = true |
37 |
| type_has_empty_sort (TVar (_, [])) = true |
|
38 |
| type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts |
|
39 |
| type_has_empty_sort _ = false; |
|
40 |
||
15997 | 41 |
(**** Transformation of Elimination Rules into First-Order Formulas****) |
15347 | 42 |
|
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
43 |
val cfalse = cterm_of HOL.thy HOLogic.false_const; |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
44 |
val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
45 |
|
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
46 |
(*Converts an elim-rule into an equivalent theorem that does not have the |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
47 |
predicate variable. Leaves other theorems unchanged. We simply instantiate the |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
48 |
conclusion variable to False.*) |
16009 | 49 |
fun transform_elim th = |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
50 |
case concl_of th of (*conclusion variable*) |
24669 | 51 |
Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
52 |
Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th |
24669 | 53 |
| v as Var(_, Type("prop",[])) => |
21430
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
54 |
Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th |
77651b6d9d6c
New transformation of eliminatino rules: we simply replace the final conclusion variable by False
paulson
parents:
21290
diff
changeset
|
55 |
| _ => th; |
15997 | 56 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
57 |
(*To enforce single-threading*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
58 |
exception Clausify_failure of theory; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
59 |
|
16009 | 60 |
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
61 |
||
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
62 |
fun rhs_extra_types lhsT rhs = |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
63 |
let val lhs_vars = Term.add_tfreesT lhsT [] |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
64 |
fun add_new_TFrees (TFree v) = |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
65 |
if member (op =) lhs_vars v then I else insert (op =) (TFree v) |
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
66 |
| add_new_TFrees _ = I |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
67 |
val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs [] |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
68 |
in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end; |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
69 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
70 |
(*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
|
71 |
prefix for the Skolem constant. Result is a new theory*) |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
72 |
fun declare_skofuns s th thy = |
21071 | 73 |
let val nref = ref 0 |
74 |
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
|
75 |
(*Existential: declare a Skolem function, then insert into body and continue*) |
24785 | 76 |
let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref) |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
77 |
val args0 = term_frees xtp (*get the formal parameter list*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
78 |
val Ts = map type_of args0 |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
79 |
val extraTs = rhs_extra_types (Ts ---> T) xtp |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
80 |
val _ = if null extraTs then () else |
24785 | 81 |
warning ("Skolemization: extra type vars: " ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset
|
82 |
commas_quote (map (Syntax.string_of_typ_global thy) extraTs)); |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
83 |
val argsx = map (fn T => Free(gensym"vsk", T)) extraTs |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
84 |
val args = argsx @ args0 |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
85 |
val cT = extraTs ---> Ts ---> T |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
86 |
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
|
87 |
(*Forms a lambda-abstraction over the formal parameters*) |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
88 |
val _ = Output.debug (fn () => "declaring the constant " ^ cname) |
24959
119793c84647
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24937
diff
changeset
|
89 |
val (c, thy') = |
119793c84647
replaced Sign.add_consts_authentic by Sign.declare_const;
wenzelm
parents:
24937
diff
changeset
|
90 |
Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
91 |
(*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
|
92 |
val cdef = cname ^ "_def" |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
93 |
val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy' |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
94 |
handle ERROR _ => raise Clausify_failure thy' |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
95 |
in dec_sko (subst_bound (list_comb(c,args), p)) |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
96 |
(thy'', Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef) :: axs) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
97 |
end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
98 |
| 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
|
99 |
(*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
|
100 |
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
|
101 |
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
|
102 |
| 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
|
103 |
| 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
|
104 |
| 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
|
105 |
| dec_sko t thx = thx (*Do nothing otherwise*) |
20419 | 106 |
in dec_sko (prop_of th) (thy,[]) end; |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
107 |
|
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
108 |
(*Traverse a theorem, accumulating Skolem function definitions.*) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
109 |
fun assume_skofuns s th = |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
110 |
let val sko_count = ref 0 |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
111 |
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
|
112 |
(*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
|
113 |
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
|
114 |
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
|
115 |
val Ts = map type_of args |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
116 |
val cT = Ts ---> T |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
117 |
val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
118 |
val c = Free (id, cT) |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
119 |
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
|
120 |
HOLogic.choice_const T $ xtp) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
121 |
(*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
|
122 |
val def = equals cT $ c $ rhs |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
123 |
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
|
124 |
(def :: defs) |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
125 |
end |
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
126 |
| 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
|
127 |
(*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
|
128 |
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
|
129 |
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
|
130 |
| 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
|
131 |
| 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
|
132 |
| 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
|
133 |
| dec_sko t defs = defs (*Do nothing otherwise*) |
20419 | 134 |
in dec_sko (prop_of th) [] end; |
135 |
||
136 |
||
24827 | 137 |
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****) |
20419 | 138 |
|
139 |
(*Returns the vars of a theorem*) |
|
140 |
fun vars_of_thm th = |
|
22691 | 141 |
map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
20419 | 142 |
|
143 |
(*Make a version of fun_cong with a given variable name*) |
|
144 |
local |
|
145 |
val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
|
146 |
val cx = hd (vars_of_thm fun_cong'); |
|
147 |
val ty = typ_of (ctyp_of_term cx); |
|
20445 | 148 |
val thy = theory_of_thm fun_cong; |
20419 | 149 |
fun mkvar a = cterm_of thy (Var((a,0),ty)); |
150 |
in |
|
151 |
fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' |
|
152 |
end; |
|
153 |
||
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
154 |
(*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n, |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
155 |
serves as an upper bound on how many to remove.*) |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
156 |
fun strip_lambdas 0 th = th |
24669 | 157 |
| strip_lambdas n th = |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
158 |
case prop_of th of |
24669 | 159 |
_ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => |
160 |
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) |
|
161 |
| _ => th; |
|
20419 | 162 |
|
24669 | 163 |
val lambda_free = not o Term.has_abs; |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
164 |
|
24669 | 165 |
val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
166 |
|
24827 | 167 |
val abs_S = @{thm"abs_S"}; |
168 |
val abs_K = @{thm"abs_K"}; |
|
169 |
val abs_I = @{thm"abs_I"}; |
|
170 |
val abs_B = @{thm"abs_B"}; |
|
171 |
val abs_C = @{thm"abs_C"}; |
|
20710
384bfce59254
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson
parents:
20624
diff
changeset
|
172 |
|
24827 | 173 |
val [f_B,g_B] = map (cterm_of @{theory}) (term_vars (prop_of abs_B)); |
174 |
val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C)); |
|
175 |
val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S)); |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
176 |
|
24827 | 177 |
(*FIXME: requires more use of cterm constructors*) |
178 |
fun abstract ct = |
|
26928 | 179 |
let val _ = Output.debug (fn()=>" abstraction: " ^ Display.string_of_cterm ct) |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
180 |
val Abs(x,_,body) = term_of ct |
24827 | 181 |
val thy = theory_of_cterm ct |
182 |
val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) |
|
183 |
val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT |
|
184 |
fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K |
|
185 |
in |
|
186 |
case body of |
|
187 |
Const _ => makeK() |
|
188 |
| Free _ => makeK() |
|
189 |
| Var _ => makeK() (*though Var isn't expected*) |
|
190 |
| Bound 0 => instantiate' [SOME cxT] [] abs_I (*identity: I*) |
|
191 |
| rator$rand => |
|
192 |
if loose_bvar1 (rator,0) then (*C or S*) |
|
193 |
if loose_bvar1 (rand,0) then (*S*) |
|
194 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
|
195 |
val crand = cterm_of thy (Abs(x,xT,rand)) |
|
196 |
val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] abs_S |
|
197 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_S') |
|
198 |
in |
|
199 |
Thm.transitive abs_S' (Conv.binop_conv abstract rhs) |
|
200 |
end |
|
201 |
else (*C*) |
|
202 |
let val crator = cterm_of thy (Abs(x,xT,rator)) |
|
203 |
val abs_C' = cterm_instantiate [(f_C,crator),(g_C,cterm_of thy rand)] abs_C |
|
204 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_C') |
|
205 |
in |
|
206 |
Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv abstract) rhs) |
|
207 |
end |
|
208 |
else if loose_bvar1 (rand,0) then (*B or eta*) |
|
209 |
if rand = Bound 0 then eta_conversion ct |
|
210 |
else (*B*) |
|
211 |
let val crand = cterm_of thy (Abs(x,xT,rand)) |
|
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
212 |
val crator = cterm_of thy rator |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
213 |
val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] abs_B |
24827 | 214 |
val (_,rhs) = Thm.dest_equals (cprop_of abs_B') |
215 |
in |
|
216 |
Thm.transitive abs_B' (Conv.arg_conv abstract rhs) |
|
217 |
end |
|
218 |
else makeK() |
|
219 |
| _ => error "abstract: Bad term" |
|
220 |
end; |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
221 |
|
20419 | 222 |
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested |
223 |
prefix for the constants. Resulting theory is returned in the first theorem. *) |
|
24827 | 224 |
fun combinators_aux ct = |
225 |
if lambda_free (term_of ct) then reflexive ct |
|
226 |
else |
|
227 |
case term_of ct of |
|
228 |
Abs _ => |
|
25007 | 229 |
let val (cv,cta) = Thm.dest_abs NONE ct |
24827 | 230 |
val (v,Tv) = (dest_Free o term_of) cv |
26928 | 231 |
val _ = Output.debug (fn()=>" recursion: " ^ Display.string_of_cterm cta); |
24827 | 232 |
val u_th = combinators_aux cta |
26928 | 233 |
val _ = Output.debug (fn()=>" returned " ^ Display.string_of_thm u_th); |
24827 | 234 |
val cu = Thm.rhs_of u_th |
235 |
val comb_eq = abstract (Thm.cabs cv cu) |
|
26928 | 236 |
in Output.debug (fn()=>" abstraction result: " ^ Display.string_of_thm comb_eq); |
24827 | 237 |
(transitive (abstract_rule v cv u_th) comb_eq) end |
238 |
| t1 $ t2 => |
|
239 |
let val (ct1,ct2) = Thm.dest_comb ct |
|
240 |
in combination (combinators_aux ct1) (combinators_aux ct2) end; |
|
241 |
||
242 |
fun combinators th = |
|
243 |
if lambda_free (prop_of th) then th |
|
244 |
else |
|
26928 | 245 |
let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); |
24827 | 246 |
val th = Drule.eta_contraction_rule th |
247 |
val eqth = combinators_aux (cprop_of th) |
|
26928 | 248 |
val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
249 |
in equal_elim eqth th end |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
250 |
handle THM (msg,_,_) => |
26928 | 251 |
(warning ("Error in the combinator translation of " ^ Display.string_of_thm th); |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
252 |
warning (" Exception message: " ^ msg); |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
253 |
TrueI); (*A type variable of sort {} will cause make abstraction fail.*) |
16009 | 254 |
|
255 |
(*cterms are used throughout for efficiency*) |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
256 |
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; |
16009 | 257 |
|
258 |
(*cterm version of mk_cTrueprop*) |
|
259 |
fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
260 |
||
261 |
(*Given an abstraction over n variables, replace the bound variables by free |
|
262 |
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
|
263 |
fun c_variant_abs_multi (ct0, vars) = |
16009 | 264 |
let val (cv,ct) = Thm.dest_abs NONE ct0 |
265 |
in c_variant_abs_multi (ct, cv::vars) end |
|
266 |
handle CTERM _ => (ct0, rev vars); |
|
267 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
268 |
(*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
|
269 |
an existential formula by a use of that function. |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
270 |
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
|
271 |
fun skolem_of_def def = |
22902
ac833b4bb7ee
moved some Drule operations to Thm (see more_thm.ML);
wenzelm
parents:
22846
diff
changeset
|
272 |
let val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def)) |
16009 | 273 |
val (ch, frees) = c_variant_abs_multi (rhs, []) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
274 |
val (chilbert,cabs) = Thm.dest_comb ch |
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
275 |
val thy = Thm.theory_of_cterm chilbert |
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
276 |
val t = Thm.term_of chilbert |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
277 |
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
|
278 |
| _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) |
22596 | 279 |
val cex = Thm.cterm_of thy (HOLogic.exists_const T) |
16009 | 280 |
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) |
281 |
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
|
282 |
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 |
23352 | 283 |
in Goal.prove_internal [ex_tm] conc tacf |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
284 |
|> forall_intr_list frees |
26653 | 285 |
|> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
286 |
|> Thm.varifyT |
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
287 |
end; |
16009 | 288 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
289 |
|
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
290 |
(*This will refer to the final version of theory ATP_Linkup.*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
291 |
val atp_linkup_thy_ref = Theory.check_thy @{theory} |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
292 |
|
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
293 |
(*Transfer a theorem into theory ATP_Linkup.thy if it is not already |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
294 |
inside that theory -- because it's needed for Skolemization. |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
295 |
If called while ATP_Linkup is being created, it will transfer to the |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
296 |
current version. If called afterward, it will transfer to the final version.*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
297 |
fun transfer_to_ATP_Linkup th = |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
298 |
transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th; |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
299 |
|
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
300 |
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
301 |
fun to_nnf th ctxt0 = |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
302 |
let val th1 = th |> transfer_to_ATP_Linkup |> transform_elim |> zero_var_indexes |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
303 |
val ((_,[th2]),ctxt) = Variable.import_thms false [th1] ctxt0 |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
304 |
val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1 |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
305 |
in (th3, ctxt) end; |
16009 | 306 |
|
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
307 |
(*Generate Skolem functions for a theorem supplied in nnf*) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
308 |
fun assume_skolem_of_def s th = |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
309 |
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
310 |
|
24669 | 311 |
fun assert_lambda_free ths msg = |
20863
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
312 |
case filter (not o lambda_free o prop_of) ths of |
4ee61dbf192d
improvements to abstraction, ensuring more re-use of abstraction functions
paulson
parents:
20789
diff
changeset
|
313 |
[] => () |
26928 | 314 |
| ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths')); |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
315 |
|
25007 | 316 |
|
317 |
(*** Blacklisting (duplicated in ResAtp? ***) |
|
318 |
||
319 |
val max_lambda_nesting = 3; |
|
320 |
||
321 |
fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) |
|
322 |
| excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) |
|
323 |
| excessive_lambdas _ = false; |
|
324 |
||
325 |
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT); |
|
326 |
||
327 |
(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) |
|
328 |
fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t |
|
329 |
| excessive_lambdas_fm Ts t = |
|
330 |
if is_formula_type (fastype_of1 (Ts, t)) |
|
331 |
then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) |
|
332 |
else excessive_lambdas (t, max_lambda_nesting); |
|
333 |
||
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
334 |
(*The max apply_depth of any metis call in MetisExamples (on 31-10-2007) was 11.*) |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
335 |
val max_apply_depth = 15; |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
336 |
|
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
337 |
fun apply_depth (f$t) = Int.max (apply_depth f, apply_depth t + 1) |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
338 |
| apply_depth (Abs(_,_,t)) = apply_depth t |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
339 |
| apply_depth _ = 0; |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
340 |
|
25007 | 341 |
fun too_complex t = |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
342 |
apply_depth t > max_apply_depth orelse |
26562
9d25ef112cf6
* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
paulson
parents:
25761
diff
changeset
|
343 |
Meson.too_many_clauses NONE t orelse |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
344 |
excessive_lambdas_fm [] t; |
25007 | 345 |
|
25243 | 346 |
fun is_strange_thm th = |
347 |
case head_of (concl_of th) of |
|
348 |
Const (a,_) => (a <> "Trueprop" andalso a <> "==") |
|
349 |
| _ => false; |
|
350 |
||
351 |
fun bad_for_atp th = |
|
25761 | 352 |
PureThy.is_internal th |
353 |
orelse too_complex (prop_of th) |
|
354 |
orelse exists_type type_has_empty_sort (prop_of th) |
|
355 |
orelse is_strange_thm th; |
|
25243 | 356 |
|
25007 | 357 |
val multi_base_blacklist = |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
358 |
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm", |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
359 |
"cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*) |
25007 | 360 |
|
21071 | 361 |
(*Keep the full complexity of the original name*) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21646
diff
changeset
|
362 |
fun flatten_name s = space_implode "_X" (NameSpace.explode s); |
21071 | 363 |
|
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
364 |
fun fake_name th = |
24669 | 365 |
if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
366 |
else gensym "unknown_thm_"; |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
367 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
368 |
fun name_or_string th = |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
369 |
if PureThy.has_name_hint th then PureThy.get_name_hint th |
26928 | 370 |
else Display.string_of_thm th; |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
371 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
372 |
(*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
|
373 |
It returns a modified theory, unless skolemization fails.*) |
22471 | 374 |
fun skolem thy th = |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
375 |
let val ctxt0 = Variable.thm_context th |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
376 |
val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
377 |
in |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
378 |
Option.map |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
379 |
(fn (nnfth,ctxt1) => |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
380 |
let |
26928 | 381 |
val _ = Output.debug (fn () => " initial nnf: " ^ Display.string_of_thm nnfth) |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
382 |
val s = fake_name th |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
383 |
val (thy',defs) = declare_skofuns s nnfth thy |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
384 |
val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
385 |
val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded") |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
386 |
val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
387 |
|> Meson.finish_cnf |> map Thm.close_derivation |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
388 |
in (cnfs', thy') end |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
389 |
handle Clausify_failure thy_e => ([],thy_e) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
390 |
) |
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
391 |
(try (to_nnf th) ctxt0) |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
392 |
end; |
16009 | 393 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
394 |
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
395 |
Skolem functions.*) |
22516 | 396 |
structure ThmCache = TheoryDataFun |
22846 | 397 |
( |
26618 | 398 |
type T = thm list Thmtab.table; |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
399 |
val empty = Thmtab.empty; |
26618 | 400 |
val copy = I; |
401 |
val extend = I; |
|
402 |
fun merge _ tabs : T = Thmtab.merge (K true) tabs; |
|
22846 | 403 |
); |
22516 | 404 |
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
405 |
(*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
|
406 |
and modified theory.*) |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
407 |
fun skolem_cache_thm th thy = |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
408 |
case Thmtab.lookup (ThmCache.get thy) th of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
409 |
NONE => |
22471 | 410 |
(case skolem thy (Thm.transfer thy th) of |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
411 |
NONE => ([th],thy) |
24669 | 412 |
| SOME (cls,thy') => |
24785 | 413 |
(Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
414 |
" clauses inserted into cache: " ^ name_or_string th); |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
415 |
(cls, ThmCache.map (Thmtab.update (th,cls)) thy'))) |
22471 | 416 |
| SOME cls => (cls,thy); |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
417 |
|
25007 | 418 |
(*Skolemize a named theorem, with Skolem functions as additional premises.*) |
419 |
fun skolem_thm (s,th) = |
|
25243 | 420 |
if (Sign.base_name s) mem_string multi_base_blacklist orelse bad_for_atp th then [] |
25007 | 421 |
else |
422 |
let val ctxt0 = Variable.thm_context th |
|
423 |
val (nnfth,ctxt1) = to_nnf th ctxt0 |
|
424 |
val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 |
|
425 |
in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end |
|
426 |
handle THM _ => []; |
|
427 |
||
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
428 |
(*Exported function to convert Isabelle theorems into axiom clauses*) |
22471 | 429 |
fun cnf_axiom th = |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
430 |
let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th) |
22516 | 431 |
in |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
432 |
case Thmtab.lookup (ThmCache.get thy) th of |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
433 |
NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); |
26627
dac6d56b7c8d
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26618
diff
changeset
|
434 |
map Thm.close_derivation (skolem_thm (fake_name th, th))) |
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
435 |
| SOME cls => cls |
22516 | 436 |
end; |
15347 | 437 |
|
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
21602
diff
changeset
|
438 |
fun pairname th = (PureThy.get_name_hint th, th); |
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset
|
439 |
|
15872 | 440 |
(**** Extract and Clausify theorems from a theory's claset and simpset ****) |
15347 | 441 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
442 |
fun rules_of_claset cs = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
443 |
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs |
19175 | 444 |
val intros = safeIs @ hazIs |
18532 | 445 |
val elims = map Classical.classical_rule (safeEs @ hazEs) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
446 |
in |
22130 | 447 |
Output.debug (fn () => "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
|
448 |
" elims: " ^ Int.toString(length elims)); |
20017
a2070352371c
made the conversion of elimination rules more robust
paulson
parents:
19894
diff
changeset
|
449 |
map pairname (intros @ elims) |
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset
|
450 |
end; |
15347 | 451 |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
452 |
fun rules_of_simpset ss = |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
453 |
let val ({rules,...}, _) = rep_ss ss |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
454 |
val simps = Net.entries rules |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
455 |
in |
22130 | 456 |
Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps)); |
457 |
map (fn r => (#name r, #thm r)) simps |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
458 |
end; |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
459 |
|
21505 | 460 |
fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); |
461 |
fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt); |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
462 |
|
24042 | 463 |
fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt); |
20774 | 464 |
|
15347 | 465 |
|
22471 | 466 |
(**** Translate a set of theorems into CNF ****) |
15347 | 467 |
|
19894 | 468 |
fun pair_name_cls k (n, []) = [] |
469 |
| 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
|
470 |
|
19894 | 471 |
fun cnf_rules_pairs_aux pairs [] = pairs |
472 |
| cnf_rules_pairs_aux pairs ((name,th)::ths) = |
|
22471 | 473 |
let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs |
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
474 |
handle THM _ => pairs | ResClause.CLAUSE _ => pairs |
19894 | 475 |
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
|
476 |
|
21290
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
477 |
(*The combination of rev and tail recursion preserves the original order*) |
33b6bb5d6ab8
Improvement to classrel clauses: now outputs the minimum needed.
paulson
parents:
21254
diff
changeset
|
478 |
fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l); |
19353 | 479 |
|
19196
62ee8c10d796
Added functions to retrieve local and global atpset rules.
mengj
parents:
19175
diff
changeset
|
480 |
|
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
|
481 |
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) |
15347 | 482 |
|
20419 | 483 |
(*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
|
484 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
485 |
val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
486 |
|
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
487 |
fun skolem_cache th thy = |
25243 | 488 |
if bad_for_atp th then thy else #2 (skolem_cache_thm th thy); |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
489 |
|
24854 | 490 |
fun skolem_cache_list (a,ths) thy = |
491 |
if (Sign.base_name a) mem_string multi_base_blacklist then thy |
|
492 |
else fold skolem_cache ths thy; |
|
493 |
||
494 |
val skolem_cache_theorems_of = Symtab.fold skolem_cache_list o #2 o PureThy.theorems_of; |
|
24821
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
495 |
fun skolem_cache_node thy = skolem_cache_theorems_of thy thy; |
cc55041ca8ba
skolem_cache: ignore internal theorems -- major speedup;
wenzelm
parents:
24785
diff
changeset
|
496 |
fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy; |
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
497 |
|
22516 | 498 |
(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are |
499 |
lambda_free, but then the individual theory caches become much bigger.*) |
|
21071 | 500 |
|
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
501 |
val suppress_endtheory = ref false; |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
502 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
503 |
(*The new constant is a hack to prevent multiple execution*) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
504 |
fun clause_cache_endtheory thy = |
25256
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
505 |
if !suppress_endtheory then NONE |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
506 |
else |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
507 |
(Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy); |
fe467fdf129a
Catch exceptions arising during the abstraction operation.
paulson
parents:
25243
diff
changeset
|
508 |
Option.map skolem_cache_node (try mark_skolemized thy) ); |
16563 | 509 |
|
510 |
(*** meson proof methods ***) |
|
511 |
||
22516 | 512 |
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths); |
16563 | 513 |
|
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
514 |
(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) |
24827 | 515 |
fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
516 |
| is_absko _ = false; |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
517 |
|
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
518 |
fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
519 |
is_Free t andalso not (member (op aconv) xs t) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
520 |
| is_okdef _ _ = false |
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset
|
521 |
|
24215 | 522 |
(*This function tries to cope with open locales, which introduce hypotheses of the form |
523 |
Free == t, conjecture clauses, which introduce various hypotheses, and also definitions |
|
24827 | 524 |
of sko_ functions. *) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
525 |
fun expand_defs_tac st0 st = |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
526 |
let val hyps0 = #hyps (rep_thm st0) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
527 |
val hyps = #hyps (crep_thm st) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
528 |
val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
529 |
val defs = filter (is_absko o Thm.term_of) newhyps |
24669 | 530 |
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
531 |
(map Thm.term_of hyps) |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
532 |
val fixed = term_frees (concl_of st) @ |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
533 |
foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps) |
26928 | 534 |
in Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st); |
535 |
Output.debug (fn _ => " st0: " ^ Display.string_of_thm st0); |
|
536 |
Output.debug (fn _ => " defs: " ^ commas (map Display.string_of_cterm defs)); |
|
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
537 |
Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] |
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
538 |
end; |
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset
|
539 |
|
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
540 |
|
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
541 |
fun meson_general_tac ths i st0 = |
26928 | 542 |
let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths)) |
22731
abfdccaed085
trying to make single-step proofs work better, especially if they contain
paulson
parents:
22724
diff
changeset
|
543 |
in (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end; |
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset
|
544 |
|
21588 | 545 |
val meson_method_setup = Method.add_methods |
546 |
[("meson", Method.thms_args (fn ths => |
|
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset
|
547 |
Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)), |
21588 | 548 |
"MESON resolution proof procedure")]; |
15347 | 549 |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
550 |
(** Attribute for converting a theorem into clauses **) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
551 |
|
22471 | 552 |
fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th); |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
553 |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
554 |
fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i) |
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
555 |
|
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
556 |
val clausify = Attrib.syntax (Scan.lift Args.nat |
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
557 |
>> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); |
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
558 |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
559 |
|
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
560 |
(*** Converting a subgoal into negated conjecture clauses. ***) |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
561 |
|
24300 | 562 |
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac]; |
22471 | 563 |
|
24937
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
564 |
fun neg_clausify sts = |
340523598914
context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24854
diff
changeset
|
565 |
sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf; |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
566 |
|
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
567 |
fun neg_conjecture_clauses st0 n = |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
568 |
let val st = Seq.hd (neg_skolemize_tac n st0) |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
569 |
val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st)) |
22516 | 570 |
in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end |
571 |
handle Option => raise ERROR "unable to Skolemize subgoal"; |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
572 |
|
24669 | 573 |
(*Conversion of a subgoal to conjecture clauses. Each clause has |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
574 |
leading !!-bound universal variables, to express generality. *) |
24669 | 575 |
val neg_clausify_tac = |
576 |
neg_skolemize_tac THEN' |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
577 |
SUBGOAL |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
578 |
(fn (prop,_) => |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
579 |
let val ts = Logic.strip_assums_hyp prop |
24669 | 580 |
in EVERY1 |
581 |
[METAHYPS |
|
582 |
(fn hyps => |
|
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
583 |
(Method.insert_tac |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
584 |
(map forall_intr_vars (neg_clausify hyps)) 1)), |
24669 | 585 |
REPEAT_DETERM_N (length ts) o (etac thin_rl)] |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
586 |
end); |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
587 |
|
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
588 |
(** The Skolemization attribute **) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
589 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
590 |
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
|
591 |
|
20457
85414caac94a
refinements to conversion into clause form, esp for the HO case
paulson
parents:
20445
diff
changeset
|
592 |
(*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
|
593 |
fun conj_rule [] = TrueI |
20445 | 594 |
| conj_rule ths = foldr1 conj2_rule ths; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
595 |
|
20419 | 596 |
fun skolem_attr (Context.Theory thy, th) = |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
597 |
let val (cls, thy') = skolem_cache_thm th thy |
18728 | 598 |
in (Context.Theory thy', conj_rule cls) end |
22724
3002683a6e0f
Fixes for proof reconstruction, especially involving abstractions and definitions
paulson
parents:
22691
diff
changeset
|
599 |
| skolem_attr (context, th) = (context, th) |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
600 |
|
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
601 |
val setup_attrs = Attrib.add_attributes |
21102
7f2ebe5c5b72
Conversion to clause form now tolerates Boolean variables without looping.
paulson
parents:
21096
diff
changeset
|
602 |
[("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"), |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
603 |
("clausify", clausify, "conversion of theorem to clauses")]; |
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
604 |
|
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
605 |
val setup_methods = Method.add_methods |
24669 | 606 |
[("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac), |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21900
diff
changeset
|
607 |
"conversion of goal to conjecture clauses")]; |
24669 | 608 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24669
diff
changeset
|
609 |
val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods; |
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset
|
610 |
|
20461
d689ad772b2c
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
wenzelm
parents:
20457
diff
changeset
|
611 |
end; |