author | steckerm |
Sat, 20 Sep 2014 10:42:08 +0200 | |
changeset 58401 | b8ca69d9897b |
parent 58200 | d95055489fce |
child 58402 | 623645fdb047 |
permissions | -rw-r--r-- |
57262 | 1 |
(* Title: HOL/Tools/ATP/atp_waldmeister.ML |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Albert Steckermeier, TU Muenchen |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
General-purpose functions used by the Sledgehammer modules. |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
*) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
|
58142 | 8 |
exception FailureMessage of string |
9 |
exception FailureTerm of term * term |
|
10 |
exception FailureWM of (term * term list * (string * string) list) |
|
11 |
||
12 |
signature ATP_WALDMEISTER_SKOLEMIZER = |
|
13 |
sig |
|
14 |
val skolemize : bool -> Proof.context -> term -> (Proof.context * (term list * term)) |
|
15 |
end; |
|
16 |
||
17 |
signature ATP_WALDMEISTER_TYPE_ENCODER = |
|
18 |
sig |
|
19 |
val encode_type : typ -> string |
|
20 |
val decode_type_string : string -> typ |
|
21 |
val encode_types : typ list -> string |
|
22 |
val decode_types : string -> typ list |
|
23 |
val encode_const : string * typ list -> string |
|
24 |
val decode_const : string -> string * typ list |
|
25 |
end; |
|
26 |
||
57262 | 27 |
signature ATP_WALDMEISTER = |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
sig |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
type 'a atp_problem = 'a ATP_Problem.atp_problem |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
30 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
31 |
type 'a atp_proof = 'a ATP_Proof.atp_proof |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
32 |
type stature = ATP_Problem_Generate.stature |
58142 | 33 |
type waldmeister_info = (string * (term list * (term option * term))) list |
34 |
||
35 |
val waldmeister_skolemize_rule : string |
|
36 |
||
37 |
val generate_waldmeister_problem : Proof.context -> term list -> term -> |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
38 |
((string * stature) * term) list -> |
58142 | 39 |
string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * |
40 |
waldmeister_info |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
41 |
val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof -> |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
42 |
(term, string) atp_step list |
58142 | 43 |
val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> |
44 |
(term, string) atp_step list |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
end; |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
|
58142 | 47 |
structure ATP_Waldmeister_Skolemizer : ATP_WALDMEISTER_SKOLEMIZER = |
48 |
struct |
|
49 |
||
50 |
open HOLogic |
|
51 |
||
52 |
fun contains_quantor (Const (@{const_name Ex},_) $ _) = true |
|
53 |
| contains_quantor (Const (@{const_name All},_) $ _) = true |
|
54 |
| contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2 |
|
55 |
| contains_quantor _ = false |
|
56 |
||
57 |
fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name,ty) = |
|
58 |
let |
|
59 |
val fun_type = (map type_of arg_trms) ---> ty |
|
60 |
val (fun_name,_) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type) |
|
61 |
val (_,ctxt1_new) = Variable.add_fixes [fun_name] ctxt1 |
|
62 |
val (_,ctxt2_new) = Variable.add_fixes [fun_name] ctxt2 |
|
63 |
in |
|
64 |
(Term.list_comb (Free (fun_name,fun_type),arg_trms),ctxt1_new,ctxt2_new) |
|
65 |
end |
|
66 |
||
67 |
fun skolem_free ctxt1 ctxt2 vars (bound_name,ty,trm) = |
|
68 |
let |
|
69 |
val (fun_trm,ctxt1_new,ctxt2_new) = mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty) |
|
70 |
in |
|
71 |
(Term.subst_bounds ([fun_trm],trm),ctxt1_new,ctxt2_new) |
|
72 |
end |
|
73 |
||
74 |
fun skolem_var ctxt (bound_name,ty,trm) = |
|
75 |
let |
|
76 |
val (var_name,_) = singleton (Variable.variant_frees ctxt []) (bound_name,ty) |
|
77 |
val (_,ctxt') = Variable.add_fixes [var_name] ctxt |
|
78 |
val var = Var ((var_name,0),ty) |
|
79 |
in |
|
80 |
(Term.subst_bounds ([var],trm),ctxt',var) |
|
81 |
end |
|
82 |
||
83 |
fun skolem_bound is_free ctxt1 ctxt2 spets vars x = |
|
84 |
if is_free then |
|
85 |
let |
|
86 |
val (trm',ctxt1',ctxt2') = skolem_free ctxt1 ctxt2 vars x |
|
87 |
in |
|
88 |
(ctxt1',ctxt2',spets,trm',vars) |
|
89 |
end |
|
90 |
else |
|
91 |
let |
|
92 |
val (trm',ctxt2',var) = skolem_var ctxt2 x |
|
93 |
in |
|
94 |
(ctxt1,ctxt2',spets,trm',var::vars) |
|
95 |
end |
|
96 |
||
97 |
fun skolemize' pos ctxt1 ctxt2 spets vars (Const (@{const_name Not},_) $ trm') = |
|
98 |
let |
|
99 |
val (ctxt1',ctxt2',spets',trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm' |
|
100 |
in |
|
101 |
(ctxt1',ctxt2',map mk_not spets',mk_not trm'') |
|
102 |
end |
|
103 |
| skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq},_) $ a $ b)) = |
|
104 |
if contains_quantor trm then |
|
105 |
skolemize' pos ctxt1 ctxt2 (trm::spets) vars (mk_conj (mk_imp (a,b), mk_imp (b,a))) |
|
106 |
else |
|
107 |
(ctxt1,ctxt2,spets,trm) |
|
108 |
| skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name,_) $ Abs x)) = |
|
109 |
if name = @{const_name Ex} orelse name = @{const_name All} then |
|
110 |
let |
|
111 |
val is_free = (name = @{const_name Ex} andalso pos) |
|
112 |
orelse (name = @{const_name All} andalso not pos) |
|
113 |
val (ctxt1',ctxt2',spets',trm',vars') = |
|
114 |
skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x |
|
115 |
in |
|
116 |
skolemize' pos ctxt1' ctxt2' spets' vars' trm' |
|
117 |
end |
|
118 |
else |
|
119 |
(ctxt1,ctxt2,spets,trm) |
|
120 |
| skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name,_)) $ a $ b) = |
|
121 |
if name = @{const_name conj} orelse name = @{const_name disj} orelse |
|
122 |
name = @{const_name implies} then |
|
123 |
let |
|
124 |
val pos_a = if name = @{const_name implies} then not pos else pos |
|
125 |
val (ctxt1',ctxt2',spets',a') = skolemize' pos_a ctxt1 ctxt2 [] vars a |
|
126 |
val (ctxt1'',ctxt2'',spets'',b') = skolemize' pos ctxt1' ctxt2' [] vars b |
|
127 |
in |
|
128 |
(ctxt1'',ctxt2'', |
|
129 |
map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets, |
|
130 |
c $ a' $ b') |
|
131 |
end |
|
132 |
else |
|
133 |
(ctxt1,ctxt2,spets,c $ a $ b) |
|
134 |
| skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1,ctxt2,spets,trm) |
|
135 |
||
136 |
fun skolemize positve ctxt trm = |
|
137 |
let |
|
138 |
val (ctxt1,_,spets,skolemized_trm) = skolemize' positve ctxt ctxt [] [] trm |
|
139 |
in |
|
140 |
(ctxt1,(trm :: List.rev spets,skolemized_trm)) |
|
141 |
end |
|
142 |
||
143 |
end; |
|
144 |
||
145 |
structure ATP_Waldmeister_Type_Encoder : ATP_WALDMEISTER_TYPE_ENCODER = |
|
146 |
struct |
|
147 |
||
148 |
val delimiter = ";" |
|
149 |
val open_paranthesis = "[" |
|
150 |
val close_parathesis = "]" |
|
151 |
val type_prefix = "Type" |
|
152 |
val tfree_prefix = "TFree" |
|
153 |
val tvar_prefix = "TVar" |
|
154 |
||
155 |
val identifier_character = not o member (op =) [delimiter,open_paranthesis,close_parathesis] |
|
156 |
||
157 |
fun encode_type (Type (name,types)) = |
|
158 |
type_prefix ^ open_paranthesis ^ name ^ delimiter ^ |
|
159 |
(map encode_type types |> String.concatWith delimiter) ^ close_parathesis |
|
160 |
| encode_type (TFree (name,sorts)) = |
|
161 |
tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ (String.concatWith delimiter sorts) ^ delimiter |
|
162 |
| encode_type (TVar ((name,i),sorts)) = |
|
163 |
tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ |
|
164 |
close_parathesis ^ delimiter ^ (String.concatWith delimiter sorts) ^ close_parathesis |
|
165 |
||
166 |
fun encode_types types = (String.concatWith delimiter (map encode_type types)) |
|
167 |
||
168 |
fun parse_identifier x = |
|
169 |
(Scan.many identifier_character >> implode) x |
|
170 |
||
171 |
fun parse_star delim scanner x = (Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x |
|
172 |
||
173 |
fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --| |
|
174 |
$$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x |
|
175 |
and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --| |
|
176 |
$$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x |
|
177 |
and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis |
|
178 |
|-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ |
|
179 |
close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| |
|
180 |
$$ close_parathesis >> TVar) x |
|
181 |
and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x |
|
182 |
||
183 |
fun parse_types x = parse_star delimiter parse_any_type x |
|
184 |
||
185 |
fun decode_type_string s = Scan.finite Symbol.stopper |
|
186 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ |
|
187 |
quote s)) parse_type)) (Symbol.explode s) |> fst |
|
188 |
||
189 |
fun decode_types s = Scan.finite Symbol.stopper |
|
190 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ |
|
191 |
quote s))) parse_types) (Symbol.explode s) |> fst |
|
192 |
||
193 |
fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys |
|
194 |
||
195 |
fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s |
|
196 |
||
197 |
fun decode_const s = Scan.finite Symbol.stopper |
|
198 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^ |
|
199 |
quote s))) parse_const) (Symbol.explode s) |> fst |
|
200 |
||
201 |
end; |
|
202 |
||
203 |
structure ATP_Waldmeister : ATP_WALDMEISTER = |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
204 |
struct |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
205 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
206 |
open ATP_Util |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
207 |
open ATP_Problem |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
208 |
open ATP_Problem_Generate |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
open ATP_Proof |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
210 |
open ATP_Proof_Reconstruct |
58142 | 211 |
open ATP_Waldmeister_Skolemizer |
212 |
open ATP_Waldmeister_Type_Encoder |
|
213 |
open HOLogic |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
215 |
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
216 |
type atp_connective = ATP_Problem.atp_connective |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
217 |
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
218 |
type atp_format = ATP_Problem.atp_format |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
219 |
type atp_formula_role = ATP_Problem.atp_formula_role |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
220 |
type 'a atp_problem = 'a ATP_Problem.atp_problem |
58142 | 221 |
type waldmeister_info = (string * (term list * (term option * term))) list |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
222 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
223 |
val const_prefix = #"c" |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
224 |
val var_prefix = #"V" |
58142 | 225 |
val free_prefix = #"v" |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
226 |
val conjecture_condition_name = "condition" |
58142 | 227 |
val waldmeister_equals = "eq" |
228 |
val waldmeister_true = "true" |
|
229 |
val waldmeister_false = "false" |
|
230 |
val waldmeister_skolemize_rule = "waldmeister_skolemize" |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
231 |
val lam_lift_waldmeister_prefix = "lambda_wm" |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
233 |
val factsN = "Relevant facts" |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
234 |
val helpersN = "Helper facts" |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
235 |
val conjN = "Conjecture" |
58142 | 236 |
val conj_identifier = conjecture_prefix ^ "0" |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
58142 | 238 |
val WM_ERROR_MSG = "Waldmeister problem generator failed: " |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
240 |
(* |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
241 |
Some utilitary functions for translation. |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
242 |
*) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
243 |
|
58142 | 244 |
fun gen_ascii_tuple str = (str, ascii_of str) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
245 |
|
58142 | 246 |
fun mk_eq_true (trm as (Const (@{const_name HOL.eq}, _) $ _ $ _)) = (NONE,trm) |
247 |
| mk_eq_true trm = (SOME trm,HOLogic.mk_eq (trm, @{term True})) |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
249 |
val is_lambda_name = String.isPrefix lam_lifted_poly_prefix |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
250 |
|
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
251 |
fun lookup table k = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
252 |
List.find (fn (key, _) => key = k) table |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
253 |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
254 |
(* |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
255 |
Translation from Isabelle theorms and terms to ATP terms. |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
256 |
*) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
257 |
|
58142 | 258 |
fun trm_to_atp'' thy (Const (x, ty)) args = |
259 |
let |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
260 |
val ty_args = if is_lambda_name x then |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
261 |
[] else Sign.const_typargs thy (x,ty) |
58142 | 262 |
in |
263 |
[ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x,ty_args)), []), args)] |
|
264 |
end |
|
265 |
| trm_to_atp'' _ (Free (x, _)) args = |
|
266 |
[ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)] |
|
267 |
| trm_to_atp'' _ (Var ((x, _), _)) args = |
|
268 |
[ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)] |
|
269 |
| trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args) |
|
270 |
| trm_to_atp'' _ trm _ = raise FailureTerm (trm,trm) |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
271 |
|
58142 | 272 |
fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd |
273 |
||
274 |
fun eq_trm_to_atp thy (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = |
|
275 |
ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs]) |
|
276 |
| eq_trm_to_atp _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Non-eq term") |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
277 |
|
58142 | 278 |
fun thm_to_atps thy split_conj prop_term = |
279 |
if split_conj then map (eq_trm_to_atp thy) (prop_term |> HOLogic.dest_conj) |
|
280 |
else [prop_term |> eq_trm_to_atp thy] |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
281 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
282 |
(* Translation from ATP terms to Isabelle terms. *) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
283 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
284 |
fun construct_term thy (name, args) = |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
285 |
let |
57217 | 286 |
val prefix = String.sub (name, 0) |
58142 | 287 |
val encoded_name = String.extract(name,1,NONE) |
288 |
fun dummy_fun_type () = replicate (length args) dummyT ---> dummyT |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
289 |
in |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
290 |
if prefix = const_prefix then |
58142 | 291 |
let |
292 |
val (const_name,ty_args) = decode_const encoded_name |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
293 |
val const_trans_name = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
294 |
if is_lambda_name const_name then |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
295 |
lam_lift_waldmeister_prefix ^ |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
296 |
String.extract(const_name,size lam_lifted_poly_prefix,NONE) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
297 |
else |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
298 |
const_name |
58142 | 299 |
in |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
300 |
Const (const_trans_name, |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
301 |
if is_lambda_name const_name then |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
302 |
dummyT |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
303 |
else |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
304 |
Sign.const_instance thy (const_name, ty_args)) |
58142 | 305 |
end |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
306 |
else if prefix = free_prefix then |
58142 | 307 |
Free (encoded_name, dummy_fun_type ()) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
308 |
else if Char.isUpper prefix then |
58142 | 309 |
Var ((name, 0), dummy_fun_type ()) |
310 |
(* Use name instead of encoded_name because Waldmeister renames free variables. *) |
|
311 |
else if name = waldmeister_equals then |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
312 |
(case args of |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
313 |
[_, _] => eq_const dummyT |
58142 | 314 |
| _ => raise FailureMessage |
315 |
(WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
316 |
Int.toString (length args))) |
58142 | 317 |
else if name = waldmeister_true then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
318 |
@{term True} |
58142 | 319 |
else if name = waldmeister_false then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
320 |
@{term False} |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
321 |
else |
58142 | 322 |
raise FailureMessage |
323 |
(WM_ERROR_MSG ^ "Unknown name prefix when parsing Waldmeister proof: name = " ^ name) |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
324 |
end |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
325 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
326 |
and atp_to_trm' thy (ATerm ((name,_), args)) = |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
327 |
(case args of |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
328 |
[] => construct_term thy (name, args) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
329 |
| _ => Term.list_comb (construct_term thy (name, args), map (atp_to_trm' thy) args)) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
330 |
| atp_to_trm' _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm' expects ATerm") |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
331 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
332 |
fun atp_to_trm thy (ATerm (("equal", _), [lhs, rhs])) = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
333 |
mk_eq (atp_to_trm' thy lhs, atp_to_trm' thy rhs) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
334 |
| atp_to_trm _ (ATerm (("$true", _), _)) = @{term True} |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
335 |
| atp_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "atp_to_trm expects ATerm") |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
336 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
337 |
fun formula_to_trm thy (AAtom aterm) = aterm |> atp_to_trm thy |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
338 |
| formula_to_trm thy (AConn (ANot, [aterm])) = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
339 |
mk_not (formula_to_trm thy aterm) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
340 |
| formula_to_trm _ _ = raise FailureMessage (WM_ERROR_MSG ^ "formula_to_trm expects AAtom or AConn") |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
341 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
342 |
(* Abstract translation *) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
343 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
344 |
fun mk_formula prefix_name name atype aterm = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
345 |
Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, []) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
346 |
|
58142 | 347 |
fun problem_lines_of_fact thy prefix (s,(_,(_,t))) = |
348 |
map (mk_formula prefix s Axiom) (thm_to_atps thy false t) |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
349 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
350 |
fun make_nice problem = nice_atp_problem true CNF problem |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
351 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
352 |
fun mk_conjecture aterm = |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
353 |
let |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
354 |
val formula = mk_anot (AAtom aterm) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
355 |
in |
58142 | 356 |
Formula ((conj_identifier, ""), Hypothesis, formula, NONE, []) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
357 |
end |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
358 |
|
58401
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
359 |
fun generate_waldmeister_problem ctxt hyps_t0 concl_t0 facts0 = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
360 |
let |
57270 | 361 |
val thy = Proof_Context.theory_of ctxt |
362 |
||
363 |
val preproc = Object_Logic.atomize_term thy |
|
364 |
||
58401
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
365 |
val conditions = map preproc hyps_t0 |
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
366 |
val consequence = preproc concl_t0 |
58142 | 367 |
(*val hyp_ts = map preproc hyp_ts0 : term list *) |
368 |
val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list |
|
369 |
||
370 |
fun map_ctxt' _ ctxt [] ys = (ctxt,ys) |
|
371 |
| map_ctxt' f ctxt (x :: xs) ys = |
|
372 |
let |
|
373 |
val (ctxt',x') = f ctxt x |
|
374 |
in |
|
375 |
map_ctxt' f ctxt' xs (x'::ys) |
|
376 |
end |
|
377 |
||
378 |
fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs [] |
|
379 |
||
380 |
fun skolemize_fact ctxt (name,trm) = |
|
381 |
let |
|
382 |
val (ctxt',(steps,trm')) = skolemize true ctxt trm |
|
383 |
in |
|
384 |
(ctxt',(name,(steps,trm'))) |
|
385 |
end |
|
386 |
||
387 |
fun name_list' _ [] _ = [] |
|
388 |
| name_list' prefix (x :: xs) i = (prefix ^ Int.toString i,x) :: name_list' prefix xs (i+1) |
|
389 |
||
390 |
fun name_list prefix xs = name_list' prefix xs 0 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
391 |
|
58142 | 392 |
val (ctxt',sko_facts) = map_ctxt skolemize_fact ctxt facts : |
393 |
Proof.context * (string * (term list * term)) list |
|
58401
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
394 |
val (ctxt'',sko_conditions) = map_ctxt (skolemize true) ctxt' conditions : |
58142 | 395 |
Proof.context * (term list * term) list |
396 |
||
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
397 |
val post_skolem = do_cheaply_conceal_lambdas [] |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
398 |
|
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
399 |
val sko_eq_facts = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts : |
58142 | 400 |
(string * (term list * (term option * term))) list |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
401 |
val sko_eq_conditions = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions |
58142 | 402 |
|> name_list conjecture_condition_name : |
403 |
(string * (term list * (term option * term))) list |
|
404 |
val (_,eq_conseq as (_,(non_eq_consequence,eq_consequence))) = |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
405 |
skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) : |
58142 | 406 |
(Proof.context * (term list * (term option * term))) |
407 |
||
408 |
val sko_eq_info = |
|
409 |
(((conj_identifier,eq_conseq) :: sko_eq_conditions) @ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts) : |
|
410 |
(string * (term list * (term option * term))) list |
|
411 |
||
412 |
val fact_lines = maps (problem_lines_of_fact thy (fact_prefix ^ "0_" (* FIXME *))) sko_eq_facts |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
413 |
val condition_lines = |
58142 | 414 |
map (fn (name,(_,(_,trm))) => mk_formula fact_prefix name Hypothesis (eq_trm_to_atp thy trm)) sko_eq_conditions |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
415 |
val axiom_lines = fact_lines @ condition_lines |
58142 | 416 |
|
417 |
val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence) |
|
418 |
||
419 |
fun is_some (SOME _) = true |
|
420 |
| is_some NONE = false |
|
421 |
||
422 |
val helper_lemmas_needed = List.exists (snd #> snd #> fst #> is_some) sko_eq_facts |
|
423 |
orelse List.exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse |
|
424 |
is_some non_eq_consequence |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
425 |
|
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
426 |
val helper_lines = |
58142 | 427 |
if helper_lemmas_needed then |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
428 |
[(helpersN, |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
429 |
@{thms waldmeister_fol} |
57270 | 430 |
|> map (fn th => (("", (Global, General)), preproc (prop_of th))) |
58142 | 431 |
|> maps |
432 |
(fn ((s,_),t) => map (mk_formula helper_prefix s Axiom) (thm_to_atps thy false t)))] |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
433 |
else |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
434 |
[] |
58142 | 435 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
436 |
val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
437 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
438 |
val (nice_problem, pool) = make_nice problem |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
439 |
in |
58142 | 440 |
(nice_problem, Option.map snd pool |> the_default Symtab.empty, [], Symtab.empty, sko_eq_info) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
441 |
end |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
442 |
|
58142 | 443 |
fun termify_line ctxt (name, role, u, rule, deps) = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
444 |
let |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
445 |
val thy = Proof_Context.theory_of ctxt |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
446 |
val t = u |> formula_to_trm thy |
57699 | 447 |
|> singleton (infer_formulas_types ctxt) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
448 |
|> HOLogic.mk_Trueprop |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
449 |
in |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
450 |
(name, role, t, rule, deps) |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
451 |
end |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
452 |
|
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
453 |
fun termify_waldmeister_proof ctxt pool = |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
454 |
nasty_atp_proof pool |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
455 |
#> map (termify_line ctxt) |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
456 |
#> repair_waldmeister_endgame |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
457 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
458 |
|
58142 | 459 |
fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of |
460 |
SOME x => x | |
|
461 |
NONE => NONE |
|
462 |
||
463 |
fun fix_name name = |
|
464 |
if String.isPrefix "fact" name then |
|
465 |
String.extract(name,7,NONE) |> unascii_of |> curry (op ^) "fact_0_" |
|
466 |
else |
|
467 |
name |
|
468 |
||
469 |
fun skolemization_steps info |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
470 |
(proof_step as ((waldmeister_name,isabelle_names), role, trm, rule, _)) = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
471 |
case get_skolem_info info (map fix_name isabelle_names) of |
58142 | 472 |
NONE => [proof_step] | |
473 |
SOME (_,([],_)) => [proof_step] | |
|
474 |
SOME (_,(step :: steps,_)) => |
|
475 |
let |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
476 |
val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
477 |
|
58142 | 478 |
fun mk_steps _ [] = [] |
479 |
| mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]),Plain, |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
480 |
mk_Trueprop (if is_conjecture then mk_not x else x),waldmeister_skolemize_rule, |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
481 |
[(waldmeister_name ^ "_" ^ Int.toString (i-1),if i = 1 then isabelle_names else [])]) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
482 |
:: mk_steps (i+1) xs |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
483 |
val skolem_steps = ((waldmeister_name ^ "_0",isabelle_names),Unknown, |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
484 |
mk_Trueprop (if is_conjecture then mk_not step else step),rule,[]) :: |
58142 | 485 |
mk_steps 1 steps |
486 |
in |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
487 |
if role = Conjecture then |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
488 |
[proof_step] |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
489 |
else |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
490 |
skolem_steps @ [((waldmeister_name,[]), Unknown, trm, waldmeister_skolemize_rule, |
58142 | 491 |
[(waldmeister_name ^ "_" ^ Int.toString (length skolem_steps - 1),if length skolem_steps = 1 then isabelle_names else [])])] |
492 |
end |
|
493 |
||
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
494 |
fun introduce_waldmeister_skolems info (proof_steps : (term, string) atp_step list) = proof_steps |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
495 |
|> map (skolemization_steps info) |> List.concat |
58142 | 496 |
|
497 |
end; |