author | paulson |
Wed, 05 Oct 2005 11:18:06 +0200 | |
changeset 17764 | fde495b9e24b |
parent 17596 | cd555d5a3254 |
child 17828 | c82fb51ee18d |
permissions | -rw-r--r-- |
16795 | 1 |
(* ID: $Id$ |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
2 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
3 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
4 |
*) |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
5 |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
6 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
7 |
structure ReduceAxiomsN = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
8 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
17234 | 9 |
Remove irrelevant axioms used for a proof of a goal, with with iteration control |
10 |
||
11 |
Initial version. Needs elaboration. *) |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
12 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
13 |
struct |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
14 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
15 |
fun add_term_consts_rm ncs (Const(c, _)) cs = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
16 |
if (c mem ncs) then cs else (c ins_string cs) |
16795 | 17 |
| add_term_consts_rm ncs (t $ u) cs = |
18 |
add_term_consts_rm ncs t (add_term_consts_rm ncs u cs) |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
19 |
| add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
20 |
| add_term_consts_rm ncs _ cs = cs; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
21 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
22 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
23 |
fun term_consts_rm ncs t = add_term_consts_rm ncs t []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
24 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
25 |
fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm); |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
26 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
27 |
fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
28 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
29 |
fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
30 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
31 |
fun make_pairs [] _ = [] |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
32 |
| make_pairs (x::xs) y = (x,y)::(make_pairs xs y); |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
33 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
34 |
fun const_thm_list_aux [] cthms = cthms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
35 |
| const_thm_list_aux (thm::thms) cthms = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
36 |
let val consts = consts_of_thm thm |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
37 |
val cthms' = make_pairs consts thm |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
38 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
39 |
const_thm_list_aux thms (cthms' @ cthms) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
40 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
41 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
42 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
43 |
fun const_thm_list thms = const_thm_list_aux thms []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
44 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
45 |
fun make_thm_table thms = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
46 |
let val consts_thms = const_thm_list thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
47 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
48 |
Symtab.make_multi consts_thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
49 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
50 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
51 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
52 |
fun consts_in_goal goal = consts_of_term goal; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
53 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
54 |
fun axioms_having_consts_aux [] tab thms = thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
55 |
| axioms_having_consts_aux (c::cs) tab thms = |
17412 | 56 |
let val thms1 = Symtab.lookup tab c |
17261 | 57 |
val thms2 = |
58 |
case thms1 of (SOME x) => x |
|
59 |
| NONE => [] |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
60 |
in |
17261 | 61 |
axioms_having_consts_aux cs tab (thms2 union thms) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
62 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
63 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
64 |
fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
65 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
66 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
67 |
fun relevant_axioms goal thmTab n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
68 |
let val consts = consts_in_goal goal |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
69 |
fun relevant_axioms_aux1 cs k = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
70 |
let val thms1 = axioms_having_consts cs thmTab |
17764 | 71 |
val cs1 = foldl (op union_string) [] (map consts_of_thm thms1) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
72 |
in |
16795 | 73 |
if ((cs1 subset cs) orelse n <= k) then (k,thms1) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
74 |
else (relevant_axioms_aux1 (cs1 union cs) (k+1)) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
75 |
end |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
76 |
|
16795 | 77 |
in relevant_axioms_aux1 consts 1 end; |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
78 |
|
16795 | 79 |
fun relevant_filter n goal thms = |
80 |
if n<=0 then thms |
|
81 |
else #2 (relevant_axioms goal (make_thm_table thms) n); |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
82 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
83 |
(* find the thms from thy that contain relevant constants, n is the iteration number *) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
84 |
fun find_axioms_n thy goal n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
85 |
let val clasetR = ResAxioms.claset_rules_of_thy thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
86 |
val simpsetR = ResAxioms.simpset_rules_of_thy thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
87 |
val table = make_thm_table (clasetR @ simpsetR) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
88 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
89 |
relevant_axioms goal table n |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
90 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
91 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
92 |
fun find_axioms_n_c thy goal n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
93 |
let val current_thms = PureThy.thms_of thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
94 |
val table = make_thm_table current_thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
95 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
96 |
relevant_axioms goal table n |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
97 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
98 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
99 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
100 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
101 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
102 |
signature RES_CLASIMP = |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
103 |
sig |
16795 | 104 |
val relevant : int ref |
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
105 |
val use_simpset: bool ref |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
106 |
val use_nameless: bool ref |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
107 |
val get_clasimp_lemmas : |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
108 |
Proof.context -> term -> |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
109 |
(ResClause.clause * thm) Array.array * ResClause.clause list |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
110 |
end; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
111 |
|
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
112 |
structure ResClasimp : RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
113 |
struct |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
114 |
val use_simpset = ref false; (*Performance is much better without simprules*) |
17596 | 115 |
val use_nameless = ref true; |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
116 |
|
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
117 |
val relevant = ref 0; (*Relevance filtering is off by default*) |
16795 | 118 |
|
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
119 |
(*The "name" of a theorem is its statement, if nothing else is available.*) |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
120 |
val plain_string_of_thm = |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
121 |
setmp show_question_marks false |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
122 |
(setmp print_mode [] |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
123 |
(Pretty.setmp_margin 999 string_of_thm)); |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
124 |
|
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
125 |
fun fake_thm_name th = |
17525
ae5bb6001afb
tidying, and support for axclass/classrel clauses
paulson
parents:
17484
diff
changeset
|
126 |
Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th); |
16061 | 127 |
|
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
128 |
fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th) |
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
129 |
else ("HOL.TrueI",TrueI) |
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
130 |
| put_name_pair (a,th) = (a,th); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
131 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
132 |
(* outputs a list of (thm,clause) pairs *) |
15643 | 133 |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
134 |
fun multi x 0 xlist = xlist |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
135 |
|multi x n xlist = multi x (n-1) (x::xlist); |
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
136 |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
137 |
fun clause_numbering ((clause, theorem), num_of_cls) = |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
138 |
let val numbers = 0 upto (num_of_cls - 1) |
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset
|
139 |
in |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
140 |
multi (clause, theorem) num_of_cls [] |
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset
|
141 |
end; |
17234 | 142 |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
143 |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
144 |
(*Write out the claset and simpset rules of the supplied theory. |
16906 | 145 |
FIXME: argument "goal" is a hack to allow relevance filtering. |
146 |
To reduce the number of clauses produced, set ResClasimp.relevant:=1*) |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
147 |
fun get_clasimp_lemmas ctxt goal = |
16795 | 148 |
let val claset_rules = |
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
149 |
map put_name_pair |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
150 |
(ReduceAxiomsN.relevant_filter (!relevant) goal |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
151 |
(ResAxioms.claset_rules_of_ctxt ctxt)); |
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
152 |
val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs claset_rules []); |
15643 | 153 |
|
16795 | 154 |
val simpset_rules = |
155 |
ReduceAxiomsN.relevant_filter (!relevant) goal |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
156 |
(ResAxioms.simpset_rules_of_ctxt ctxt); |
17234 | 157 |
val named_simpset = map put_name_pair simpset_rules |
16061 | 158 |
val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []); |
15643 | 159 |
|
17234 | 160 |
val cls_thms = if !use_simpset then (claset_cls_thms@simpset_cls_thms) |
161 |
else claset_cls_thms; |
|
16061 | 162 |
val cls_thms_list = List.concat cls_thms; |
163 |
(*************************************************) |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
164 |
(* Identify the set of clauses to be written out *) |
16061 | 165 |
(*************************************************) |
166 |
val clauses = map #1(cls_thms_list); |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
167 |
val cls_nums = map ResClause.num_of_clauses clauses; |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
168 |
val whole_list = List.concat |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
169 |
(map clause_numbering (ListPair.zip (cls_thms_list, cls_nums))); |
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
170 |
|
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
171 |
(*********************************************************) |
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
172 |
(* create array and put clausename, number pairs into it *) |
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
173 |
(*********************************************************) |
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
174 |
val clause_arr = Array.fromList whole_list; |
16061 | 175 |
in |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
176 |
(clause_arr, clauses) |
16061 | 177 |
end; |
15643 | 178 |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
179 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
180 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
181 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
182 |
|
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
183 |