author | wenzelm |
Thu, 29 Jan 2015 15:27:29 +0100 | |
changeset 59469 | fb393ecde29d |
parent 58670 | 97c6818f4696 |
child 59582 | 0fbed69ff081 |
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 |
||
10 |
signature ATP_WALDMEISTER_SKOLEMIZER = |
|
11 |
sig |
|
12 |
val skolemize : bool -> Proof.context -> term -> (Proof.context * (term list * term)) |
|
13 |
end; |
|
14 |
||
15 |
signature ATP_WALDMEISTER_TYPE_ENCODER = |
|
16 |
sig |
|
17 |
val encode_type : typ -> string |
|
18 |
val decode_type_string : string -> typ |
|
19 |
val encode_types : typ list -> string |
|
20 |
val decode_types : string -> typ list |
|
21 |
val encode_const : string * typ list -> string |
|
22 |
val decode_const : string -> string * typ list |
|
23 |
end; |
|
24 |
||
57262 | 25 |
signature ATP_WALDMEISTER = |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
sig |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
type 'a atp_problem = 'a ATP_Problem.atp_problem |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
28 |
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
29 |
type 'a atp_proof = 'a ATP_Proof.atp_proof |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
30 |
type stature = ATP_Problem_Generate.stature |
58142 | 31 |
type waldmeister_info = (string * (term list * (term option * term))) list |
59469 | 32 |
|
58142 | 33 |
val waldmeister_skolemize_rule : string |
59469 | 34 |
|
58142 | 35 |
val generate_waldmeister_problem : Proof.context -> term list -> term -> |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
36 |
((string * stature) * term) list -> |
59469 | 37 |
string atp_problem * string Symtab.table * (string * term) list * int Symtab.table * |
58142 | 38 |
waldmeister_info |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
39 |
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
|
40 |
(term, string) atp_step list |
59469 | 41 |
val introduce_waldmeister_skolems : waldmeister_info -> (term, string) atp_step list -> |
58142 | 42 |
(term, string) atp_step list |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
end; |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
|
58142 | 45 |
structure ATP_Waldmeister_Skolemizer : ATP_WALDMEISTER_SKOLEMIZER = |
46 |
struct |
|
47 |
||
48 |
open HOLogic |
|
49 |
||
58403 | 50 |
fun contains_quantor (Const (@{const_name Ex}, _) $ _) = true |
51 |
| contains_quantor (Const (@{const_name All}, _) $ _) = true |
|
58142 | 52 |
| contains_quantor (t1 $ t2) = contains_quantor t1 orelse contains_quantor t2 |
53 |
| contains_quantor _ = false |
|
54 |
||
58403 | 55 |
fun mk_fun_for_bvar ctxt1 ctxt2 arg_trms (bound_name, ty) = |
58142 | 56 |
let |
57 |
val fun_type = (map type_of arg_trms) ---> ty |
|
58403 | 58 |
val (fun_name, _) = singleton (Variable.variant_frees ctxt2 []) ("sko_" ^ bound_name,fun_type) |
59 |
val (_, ctxt1_new) = Variable.add_fixes [fun_name] ctxt1 |
|
60 |
val (_, ctxt2_new) = Variable.add_fixes [fun_name] ctxt2 |
|
58142 | 61 |
in |
58403 | 62 |
(Term.list_comb (Free (fun_name,fun_type), arg_trms), ctxt1_new, ctxt2_new) |
63 |
end |
|
64 |
||
65 |
fun skolem_free ctxt1 ctxt2 vars (bound_name, ty, trm) = |
|
66 |
let |
|
59469 | 67 |
val (fun_trm, ctxt1_new, ctxt2_new) = |
58403 | 68 |
mk_fun_for_bvar ctxt1 ctxt2 (List.rev vars) (bound_name,ty) |
69 |
in |
|
70 |
(Term.subst_bounds ([fun_trm], trm), ctxt1_new, ctxt2_new) |
|
58142 | 71 |
end |
72 |
||
58403 | 73 |
fun skolem_var ctxt (bound_name, ty, trm) = |
74 |
let |
|
75 |
val (var_name, _) = singleton (Variable.variant_frees ctxt []) (bound_name, ty) |
|
76 |
val (_, ctxt') = Variable.add_fixes [var_name] ctxt |
|
77 |
val var = Var ((var_name, 0), ty) |
|
78 |
in |
|
79 |
(Term.subst_bounds ([var], trm), ctxt', var) |
|
80 |
end |
|
58142 | 81 |
|
58403 | 82 |
fun skolem_bound is_free ctxt1 ctxt2 spets vars x = |
83 |
if is_free then |
|
59469 | 84 |
let |
58403 | 85 |
val (trm', ctxt1', ctxt2') = skolem_free ctxt1 ctxt2 vars x |
86 |
in |
|
87 |
(ctxt1', ctxt2',spets, trm', vars) |
|
88 |
end |
|
89 |
else |
|
58142 | 90 |
let |
58403 | 91 |
val (trm', ctxt2', var) = skolem_var ctxt2 x |
58142 | 92 |
in |
58403 | 93 |
(ctxt1, ctxt2', spets, trm', var :: vars) |
58142 | 94 |
end |
95 |
||
58403 | 96 |
fun skolemize' pos ctxt1 ctxt2 spets vars (Const (@{const_name Not}, _) $ trm') = |
97 |
let |
|
98 |
val (ctxt1', ctxt2', spets', trm'') = skolemize' (not pos) ctxt1 ctxt2 spets vars trm' |
|
99 |
in |
|
100 |
(ctxt1', ctxt2', map mk_not spets', mk_not trm'') |
|
101 |
end |
|
102 |
| skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (@{const_name HOL.eq}, t) $ a $ b)) = |
|
103 |
if t = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"} andalso contains_quantor trm then |
|
104 |
skolemize' pos ctxt1 ctxt2 (trm :: spets) vars (mk_conj (mk_imp (a, b), mk_imp (b, a))) |
|
58142 | 105 |
else |
58403 | 106 |
(ctxt1, ctxt2, spets, trm) |
107 |
| skolemize' pos ctxt1 ctxt2 spets vars (trm as (Const (name, _) $ Abs x)) = |
|
58142 | 108 |
if name = @{const_name Ex} orelse name = @{const_name All} then |
109 |
let |
|
59469 | 110 |
val is_free = (name = @{const_name Ex} andalso pos) |
58142 | 111 |
orelse (name = @{const_name All} andalso not pos) |
59469 | 112 |
val (ctxt1', ctxt2', spets', trm', vars') = |
58142 | 113 |
skolem_bound is_free ctxt1 ctxt2 (if is_free then trm :: spets else spets) vars x |
114 |
in |
|
115 |
skolemize' pos ctxt1' ctxt2' spets' vars' trm' |
|
116 |
end |
|
117 |
else |
|
58403 | 118 |
(ctxt1, ctxt2, spets, trm) |
119 |
| skolemize' pos ctxt1 ctxt2 spets vars ((c as Const (name, _)) $ a $ b) = |
|
59469 | 120 |
if name = @{const_name conj} orelse name = @{const_name disj} orelse |
58142 | 121 |
name = @{const_name implies} then |
122 |
let |
|
123 |
val pos_a = if name = @{const_name implies} then not pos else pos |
|
58403 | 124 |
val (ctxt1', ctxt2', spets', a') = skolemize' pos_a ctxt1 ctxt2 [] vars a |
125 |
val (ctxt1'', ctxt2'', spets'', b') = skolemize' pos ctxt1' ctxt2' [] vars b |
|
58142 | 126 |
in |
58403 | 127 |
(ctxt1'', ctxt2'', |
58142 | 128 |
map (fn trm => c $ a' $ trm) spets'' @ map (fn trm => c $ trm $ b) spets' @ spets, |
129 |
c $ a' $ b') |
|
130 |
end |
|
131 |
else |
|
132 |
(ctxt1,ctxt2,spets,c $ a $ b) |
|
58403 | 133 |
| skolemize' _ ctxt1 ctxt2 spets _ trm = (ctxt1, ctxt2, spets, trm) |
59469 | 134 |
|
58670 | 135 |
fun vars_of trm = |
136 |
rev (distinct (op =) (Term.fold_aterms (fn t as Var _ => cons t | _ => I) trm [])); |
|
58142 | 137 |
|
59469 | 138 |
fun skolemize positve ctxt trm = |
58142 | 139 |
let |
58670 | 140 |
val (ctxt1, _, spets, skolemized_trm) = skolemize' positve ctxt ctxt [] (vars_of trm) trm |
58142 | 141 |
in |
58403 | 142 |
(ctxt1, (trm :: List.rev spets, skolemized_trm)) |
58142 | 143 |
end |
144 |
||
145 |
end; |
|
146 |
||
147 |
structure ATP_Waldmeister_Type_Encoder : ATP_WALDMEISTER_TYPE_ENCODER = |
|
148 |
struct |
|
149 |
||
150 |
val delimiter = ";" |
|
151 |
val open_paranthesis = "[" |
|
152 |
val close_parathesis = "]" |
|
153 |
val type_prefix = "Type" |
|
154 |
val tfree_prefix = "TFree" |
|
155 |
val tvar_prefix = "TVar" |
|
156 |
||
58403 | 157 |
val identifier_character = not o member (op =) [delimiter, open_paranthesis, close_parathesis] |
58142 | 158 |
|
59469 | 159 |
fun encode_type (Type (name, types)) = |
160 |
type_prefix ^ open_paranthesis ^ name ^ delimiter ^ |
|
161 |
(map encode_type types |> space_implode delimiter) ^ close_parathesis |
|
162 |
| encode_type (TFree (name, sorts)) = |
|
163 |
tfree_prefix ^ open_paranthesis ^ name ^ delimiter ^ space_implode delimiter sorts ^ |
|
58403 | 164 |
close_parathesis |
165 |
| encode_type (TVar ((name, i), sorts)) = |
|
59469 | 166 |
tvar_prefix ^ open_paranthesis ^ open_paranthesis ^ name ^ delimiter ^ Int.toString i ^ |
167 |
close_parathesis ^ delimiter ^ space_implode delimiter sorts ^ close_parathesis |
|
58142 | 168 |
|
59469 | 169 |
fun encode_types types = space_implode delimiter (map encode_type types) |
58142 | 170 |
|
171 |
fun parse_identifier x = |
|
172 |
(Scan.many identifier_character >> implode) x |
|
59469 | 173 |
|
174 |
fun parse_star delim scanner x = |
|
58403 | 175 |
(Scan.optional (scanner ::: Scan.repeat ($$ delim |-- scanner)) []) x |
59469 | 176 |
|
58142 | 177 |
fun parse_type x = (Scan.this_string type_prefix |-- $$ open_paranthesis |-- parse_identifier --| |
178 |
$$ delimiter -- parse_star delimiter parse_any_type --| $$ close_parathesis >> Type) x |
|
179 |
and parse_tfree x = (Scan.this_string tfree_prefix |-- $$ open_paranthesis |-- parse_identifier --| |
|
180 |
$$ delimiter -- parse_star delimiter parse_identifier --| $$ close_parathesis >> TFree) x |
|
181 |
and parse_tvar x = (Scan.this_string tvar_prefix |-- $$ open_paranthesis |-- $$ open_paranthesis |
|
59469 | 182 |
|-- parse_identifier --| $$ delimiter -- (parse_identifier >> (Int.fromString #> the)) --| $$ |
183 |
close_parathesis --| $$ delimiter -- parse_star delimiter parse_identifier --| |
|
58142 | 184 |
$$ close_parathesis >> TVar) x |
185 |
and parse_any_type x = (parse_type || parse_tfree || parse_tvar) x |
|
186 |
||
187 |
fun parse_types x = parse_star delimiter parse_any_type x |
|
59469 | 188 |
|
58142 | 189 |
fun decode_type_string s = Scan.finite Symbol.stopper |
58403 | 190 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ |
191 |
quote s)) parse_type)) (Symbol.explode s) |> fst |
|
58142 | 192 |
|
193 |
fun decode_types s = Scan.finite Symbol.stopper |
|
58403 | 194 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized type encoding" ^ |
195 |
quote s))) parse_types) (Symbol.explode s) |> fst |
|
58142 | 196 |
|
197 |
fun encode_const (name,tys) = name ^ delimiter ^ encode_types tys |
|
198 |
||
199 |
fun parse_const s = (parse_identifier --| $$ delimiter -- parse_types) s |
|
200 |
||
201 |
fun decode_const s = Scan.finite Symbol.stopper |
|
58403 | 202 |
(Scan.error (!! (fn _ => raise FailureMessage ("unrecognized const encoding" ^ |
203 |
quote s))) parse_const) (Symbol.explode s) |> fst |
|
58142 | 204 |
|
205 |
end; |
|
206 |
||
58405 | 207 |
structure ATP_Waldmeister (*** : ATP_WALDMEISTER *) = |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
208 |
struct |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
210 |
open ATP_Util |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
211 |
open ATP_Problem |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
212 |
open ATP_Problem_Generate |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
213 |
open ATP_Proof |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
open ATP_Proof_Reconstruct |
58142 | 215 |
open ATP_Waldmeister_Skolemizer |
216 |
open ATP_Waldmeister_Type_Encoder |
|
217 |
open HOLogic |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
218 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
219 |
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
|
220 |
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
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
type 'a atp_problem = 'a ATP_Problem.atp_problem |
58142 | 225 |
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
|
226 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
227 |
val const_prefix = #"c" |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
val var_prefix = #"V" |
58142 | 229 |
val free_prefix = #"v" |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
val conjecture_condition_name = "condition" |
58142 | 231 |
val waldmeister_equals = "eq" |
232 |
val waldmeister_true = "true" |
|
233 |
val waldmeister_false = "false" |
|
234 |
val waldmeister_skolemize_rule = "waldmeister_skolemize" |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
235 |
val lam_lift_waldmeister_prefix = "lambda_wm" |
58403 | 236 |
val waldmeister_apply = "wm_apply" |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
238 |
val factsN = "Relevant facts" |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
239 |
val helpersN = "Helper facts" |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
240 |
val conjN = "Conjecture" |
58142 | 241 |
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
|
242 |
|
58142 | 243 |
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
|
244 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
245 |
(* |
58403 | 246 |
Some utilitary functions for translation. |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
247 |
*) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
248 |
|
58142 | 249 |
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
|
250 |
|
58142 | 251 |
fun mk_eq_true (trm as (Const (@{const_name HOL.eq}, _) $ _ $ _)) = (NONE,trm) |
252 |
| 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
|
253 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
254 |
val is_lambda_name = String.isPrefix lam_lifted_poly_prefix |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
255 |
|
59469 | 256 |
fun lookup table k = |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
257 |
List.find (fn (key, _) => key = k) table |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
258 |
|
58403 | 259 |
fun dest_list' (f $ t) = |
260 |
let |
|
261 |
val (function, trms) = dest_list' f |
|
262 |
in |
|
263 |
(function, t :: trms) |
|
264 |
end |
|
265 |
| dest_list' t = (t,[]); |
|
266 |
||
267 |
fun dest_list trm = dest_list' trm ||> List.rev |
|
268 |
||
269 |
fun list_update x [] = [x] |
|
270 |
| list_update (a,b) ((c,d) :: xs) = |
|
271 |
if a = c andalso b < d then |
|
272 |
(a,b) :: xs |
|
273 |
else |
|
274 |
(c,d) :: list_update (a,b) xs |
|
275 |
||
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
276 |
(* |
58403 | 277 |
Hiding partial applications in terms |
278 |
*) |
|
279 |
||
280 |
fun map_minimal_app' info (trm :: trms) = |
|
281 |
map_minimal_app' (minimal_app' info trm) trms |
|
282 |
| map_minimal_app' info _ = info |
|
283 |
||
284 |
and minimal_app' info (trm as _ $ _) = |
|
285 |
let |
|
286 |
val (function, trms) = dest_list trm |
|
287 |
val info' = map_minimal_app' info trms |
|
288 |
in |
|
59469 | 289 |
case function of |
58403 | 290 |
(Const _) => list_update (function, length trms) info' | |
291 |
(Free _) => list_update (function, length trms) info' | |
|
292 |
_ => info |
|
293 |
end |
|
294 |
| minimal_app' info (trm as Const _) = |
|
295 |
list_update (trm, 0) info |
|
296 |
| minimal_app' info (trm as Free _) = |
|
297 |
list_update (trm, 0) info |
|
298 |
| minimal_app' info _ = info; |
|
299 |
||
300 |
fun map_minimal_app trms = map_minimal_app' [] trms |
|
301 |
||
302 |
fun mk_waldmeister_app function [] = function |
|
59469 | 303 |
| mk_waldmeister_app function (a :: args) = |
58403 | 304 |
let |
305 |
val funT = type_of function |
|
306 |
val argT = type_of a |
|
58405 | 307 |
val resT = dest_funT funT |> snd |
308 |
val newT = funT --> argT --> resT |
|
58403 | 309 |
in |
59469 | 310 |
mk_waldmeister_app (Const (waldmeister_apply ^ "," ^ |
58406 | 311 |
encode_types [resT, argT], newT) $ function $ a) args |
58403 | 312 |
end |
313 |
||
314 |
fun hide_partial_applications info (trm as (_ $ _)) = |
|
315 |
let |
|
316 |
val (function, trms) = dest_list trm |
|
317 |
val trms' = map (hide_partial_applications info) trms |
|
318 |
in |
|
319 |
case function of |
|
320 |
Var _ => mk_waldmeister_app function trms' | |
|
59469 | 321 |
_ => |
322 |
let |
|
58403 | 323 |
val min_args = lookup info function |> the |> snd |
324 |
val args0 = List.take (trms',min_args) |
|
325 |
val args1 = List.drop (trms',min_args) |
|
326 |
val function' = list_comb (function,args0) |
|
327 |
in |
|
328 |
mk_waldmeister_app function' args1 |
|
329 |
end |
|
330 |
end |
|
331 |
| hide_partial_applications _ t = t; |
|
332 |
||
333 |
fun remove_waldmeister_app ((c as Const (name, _)) $ x $ y) = |
|
334 |
if String.isPrefix waldmeister_apply name then |
|
335 |
remove_waldmeister_app x $ remove_waldmeister_app y |
|
336 |
else |
|
337 |
c $ remove_waldmeister_app x $ remove_waldmeister_app y |
|
338 |
| remove_waldmeister_app (x $ y) = remove_waldmeister_app x $ remove_waldmeister_app y |
|
339 |
| remove_waldmeister_app x = x |
|
340 |
||
341 |
(* |
|
58406 | 342 |
Translation from Isabelle terms to ATP terms. |
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 |
|
58142 | 345 |
fun trm_to_atp'' thy (Const (x, ty)) args = |
346 |
let |
|
58403 | 347 |
val ty_args = if is_lambda_name x orelse String.isPrefix waldmeister_apply x then |
348 |
[] else Sign.const_typargs thy (x, ty) |
|
58142 | 349 |
in |
58403 | 350 |
[ATerm ((gen_ascii_tuple (String.str const_prefix ^ encode_const (x, ty_args)), []), args)] |
58142 | 351 |
end |
59469 | 352 |
| trm_to_atp'' _ (Free (x, _)) args = |
58142 | 353 |
[ATerm ((gen_ascii_tuple (String.str free_prefix ^ x), []), args)] |
59469 | 354 |
| trm_to_atp'' _ (Var ((x, _), _)) args = |
58142 | 355 |
[ATerm ((gen_ascii_tuple (String.str var_prefix ^ x), []), args)] |
356 |
| trm_to_atp'' thy (trm1 $ trm2) args = trm_to_atp'' thy trm1 (trm_to_atp'' thy trm2 [] @ args) |
|
58403 | 357 |
| trm_to_atp'' _ _ _ = raise FailureMessage (WM_ERROR_MSG ^ "Unexpected term") |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
358 |
|
58142 | 359 |
fun trm_to_atp' thy trm = trm_to_atp'' thy trm [] |> hd |
360 |
||
361 |
fun eq_trm_to_atp thy (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = |
|
362 |
ATerm ((("equal", "equal"), []), [trm_to_atp' thy lhs, trm_to_atp' thy rhs]) |
|
363 |
| 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
|
364 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
365 |
(* 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
|
366 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
367 |
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
|
368 |
let |
57217 | 369 |
val prefix = String.sub (name, 0) |
58403 | 370 |
val encoded_name = String.extract(name, 1, NONE) |
58142 | 371 |
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
|
372 |
in |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
373 |
if prefix = const_prefix then |
58142 | 374 |
let |
58403 | 375 |
val (const_name, ty_args) = if String.isPrefix waldmeister_apply encoded_name then |
376 |
(waldmeister_apply, []) else decode_const encoded_name |
|
59469 | 377 |
val const_trans_name = |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
378 |
if is_lambda_name const_name then |
58403 | 379 |
lam_lift_waldmeister_prefix ^ (* ?? *) |
380 |
String.extract(const_name, size lam_lifted_poly_prefix, NONE) |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
381 |
else |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
382 |
const_name |
58142 | 383 |
in |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
384 |
Const (const_trans_name, |
58403 | 385 |
if is_lambda_name const_name orelse String.isPrefix waldmeister_apply const_name then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
386 |
dummyT |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
387 |
else |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
388 |
Sign.const_instance thy (const_name, ty_args)) |
58142 | 389 |
end |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
390 |
else if prefix = free_prefix then |
58142 | 391 |
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
|
392 |
else if Char.isUpper prefix then |
59469 | 393 |
Var ((name, 0), dummy_fun_type ()) |
58142 | 394 |
(* Use name instead of encoded_name because Waldmeister renames free variables. *) |
395 |
else if name = waldmeister_equals then |
|
59469 | 396 |
(case args of |
58404 | 397 |
[_, _] => eq_const dummyT |
59469 | 398 |
| _ => raise FailureMessage |
399 |
(WM_ERROR_MSG ^ "waldmeister equals needs 2 arguments but has " ^ |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
400 |
Int.toString (length args))) |
58142 | 401 |
else if name = waldmeister_true then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
402 |
@{term True} |
58142 | 403 |
else if name = waldmeister_false then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
404 |
@{term False} |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
405 |
else |
59469 | 406 |
raise FailureMessage |
58142 | 407 |
(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
|
408 |
end |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
409 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
410 |
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
|
411 |
(case args of |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
412 |
[] => construct_term thy (name, args) |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
413 |
| _ => 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
|
414 |
| 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
|
415 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
416 |
fun atp_to_trm thy (ATerm (("equal", _), [lhs, rhs])) = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
417 |
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
|
418 |
| atp_to_trm _ (ATerm (("$true", _), _)) = @{term True} |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
419 |
| 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
|
420 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
421 |
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
|
422 |
| formula_to_trm thy (AConn (ANot, [aterm])) = |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
423 |
mk_not (formula_to_trm thy aterm) |
59469 | 424 |
| formula_to_trm _ _ = |
58403 | 425 |
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
|
426 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
427 |
(* Abstract translation *) |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
428 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
429 |
fun mk_formula prefix_name name atype aterm = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
430 |
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
|
431 |
|
58406 | 432 |
fun problem_lines_of_fact thy prefix (s, (_, (_, t))) = |
433 |
mk_formula (prefix ^ "0_") s Axiom (eq_trm_to_atp thy t) |
|
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
434 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
435 |
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
|
436 |
|
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
437 |
fun mk_conjecture aterm = |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
438 |
let |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
439 |
val formula = mk_anot (AAtom aterm) |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
440 |
in |
58142 | 441 |
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
|
442 |
end |
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
443 |
|
58401
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
444 |
fun generate_waldmeister_problem ctxt hyps_t0 concl_t0 facts0 = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
445 |
let |
57270 | 446 |
val thy = Proof_Context.theory_of ctxt |
447 |
||
448 |
val preproc = Object_Logic.atomize_term thy |
|
449 |
||
58401
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
450 |
val conditions = map preproc hyps_t0 |
b8ca69d9897b
Re-added hypothesis argument to problem generation
steckerm
parents:
58200
diff
changeset
|
451 |
val consequence = preproc concl_t0 |
58142 | 452 |
val facts = map (apsnd preproc #> apfst fst) facts0 : (string * term) list |
58403 | 453 |
|
454 |
fun map_ctxt' _ ctxt [] ys = (ctxt, ys) |
|
58142 | 455 |
| map_ctxt' f ctxt (x :: xs) ys = |
456 |
let |
|
58403 | 457 |
val (ctxt', x') = f ctxt x |
58142 | 458 |
in |
58403 | 459 |
map_ctxt' f ctxt' xs (x' :: ys) |
58142 | 460 |
end |
461 |
||
462 |
fun map_ctxt f ctxt xs = map_ctxt' f ctxt xs [] |
|
59469 | 463 |
|
464 |
fun skolemize_fact ctxt (name, trm) = |
|
465 |
let |
|
466 |
val (ctxt', (steps, trm')) = skolemize true ctxt trm |
|
467 |
in |
|
58403 | 468 |
(ctxt', (name, (steps, trm'))) |
58142 | 469 |
end |
58403 | 470 |
|
58142 | 471 |
fun name_list' _ [] _ = [] |
58403 | 472 |
| name_list' prefix (x :: xs) i = (prefix ^ Int.toString i, x) :: name_list' prefix xs (i + 1) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
473 |
|
58403 | 474 |
fun name_list prefix xs = name_list' prefix xs 0 |
59469 | 475 |
|
58406 | 476 |
(* Skolemization, hiding lambdas and translating formulas to equations *) |
58403 | 477 |
val (ctxt', sko_facts) = map_ctxt skolemize_fact ctxt facts |
478 |
val (ctxt'', sko_conditions) = map_ctxt (skolemize true) ctxt' conditions |
|
58142 | 479 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
480 |
val post_skolem = do_cheaply_conceal_lambdas [] |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
481 |
|
58403 | 482 |
val sko_eq_facts0 = map (apsnd (apsnd (mk_eq_true #> apsnd post_skolem))) sko_facts |
483 |
val sko_eq_conditions0 = map (apsnd (mk_eq_true #> apsnd post_skolem)) sko_conditions |
|
484 |
|> name_list conjecture_condition_name |
|
485 |
val (_, eq_conseq as (_, (non_eq_consequence0, eq_consequence0))) = |
|
486 |
skolemize false ctxt'' consequence |> apsnd (apsnd (mk_eq_true #> apsnd post_skolem)) |
|
58142 | 487 |
|
488 |
val sko_eq_info = |
|
59469 | 489 |
(((conj_identifier, eq_conseq) :: sko_eq_conditions0) |
58403 | 490 |
@ map (apfst (fn name => fact_prefix ^ "0_" ^ name)) sko_eq_facts0) |
491 |
||
58406 | 492 |
(* Translation of partial function applications *) |
58403 | 493 |
val fun_app_info = map_minimal_app (map (snd o snd o snd) sko_eq_info) |
494 |
||
59469 | 495 |
fun hide_partial_apps_in_last (x, (y, (z, term))) = |
58403 | 496 |
(x, (y, (z, hide_partial_applications fun_app_info term))) |
58142 | 497 |
|
58403 | 498 |
val sko_eq_facts = map hide_partial_apps_in_last sko_eq_facts0 |
499 |
val sko_eq_conditions = map hide_partial_apps_in_last sko_eq_conditions0 |
|
500 |
val eq_consequence = hide_partial_applications fun_app_info eq_consequence0 |
|
501 |
||
58406 | 502 |
(* Problem creation *) |
503 |
val fact_lines = map (problem_lines_of_fact thy fact_prefix) sko_eq_facts |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
504 |
val condition_lines = |
58403 | 505 |
map (fn (name, (_, (_, trm))) => |
506 |
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
|
507 |
val axiom_lines = fact_lines @ condition_lines |
58142 | 508 |
|
509 |
val conj_line = mk_conjecture (eq_trm_to_atp thy eq_consequence) |
|
58403 | 510 |
|
58412 | 511 |
val helper_lemmas_needed = exists (snd #> snd #> fst #> is_some) sko_eq_facts |
512 |
orelse exists (snd #> snd #> fst #> is_some) sko_eq_conditions orelse |
|
58403 | 513 |
is_some non_eq_consequence0 |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
514 |
|
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
515 |
val helper_lines = |
58142 | 516 |
if helper_lemmas_needed then |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
517 |
[(helpersN, |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
518 |
@{thms waldmeister_fol} |
57270 | 519 |
|> map (fn th => (("", (Global, General)), preproc (prop_of th))) |
58403 | 520 |
|> map (fn ((s, _) ,t) => mk_formula helper_prefix s Axiom (eq_trm_to_atp thy t)))] |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
521 |
else |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
522 |
[] |
58142 | 523 |
|
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
524 |
val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
525 |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
526 |
val (nice_problem, pool) = make_nice problem |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
527 |
in |
58142 | 528 |
(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
|
529 |
end |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
530 |
|
58142 | 531 |
fun termify_line ctxt (name, role, u, rule, deps) = |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
532 |
let |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
533 |
val thy = Proof_Context.theory_of ctxt |
58403 | 534 |
val t = u |> formula_to_trm thy |> remove_waldmeister_app |
57699 | 535 |
|> singleton (infer_formulas_types ctxt) |
57267
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
536 |
|> HOLogic.mk_Trueprop |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
537 |
in |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
538 |
(name, role, t, rule, deps) |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
539 |
end |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
540 |
|
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
541 |
fun termify_waldmeister_proof ctxt pool = |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
542 |
nasty_atp_proof pool |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
543 |
#> map (termify_line ctxt) |
8b87114357bd
integrated new Waldmeister code with 'sledgehammer' command
blanchet
parents:
57262
diff
changeset
|
544 |
#> repair_waldmeister_endgame |
57215
6fc0e3d4e1e5
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
blanchet
parents:
diff
changeset
|
545 |
|
58142 | 546 |
fun get_skolem_info info names = case map (lookup info) names |> List.find is_some of |
547 |
SOME x => x | |
|
548 |
NONE => NONE |
|
58404 | 549 |
|
59469 | 550 |
fun fix_name name = |
58408 | 551 |
if String.isPrefix fact_prefix name andalso String.isSuffix "_J" name then |
59469 | 552 |
String.extract(name, size fact_prefix + 2,NONE) |> unascii_of |> |
58406 | 553 |
(fn x => fact_prefix ^ "0_" ^ x) |
554 |
else |
|
555 |
name |
|
58142 | 556 |
|
58403 | 557 |
fun skolemization_steps info |
558 |
(proof_step as ((waldmeister_name, isabelle_names), _, trm, rule, _)) = |
|
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
559 |
case get_skolem_info info (map fix_name isabelle_names) of |
58142 | 560 |
NONE => [proof_step] | |
58403 | 561 |
SOME (_, ([], _)) => [proof_step] | |
562 |
SOME (_, (step :: steps,_)) => |
|
58142 | 563 |
let |
58403 | 564 |
val raw_trm = dest_Trueprop trm |
565 |
val is_narrowing = raw_trm = @{term "True = False"} orelse raw_trm = @{term "False = True"} |
|
566 |
val is_conjecture = String.isPrefix "1.0.0.0" waldmeister_name andalso not is_narrowing |
|
58142 | 567 |
in |
58403 | 568 |
if is_narrowing then |
58200
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
569 |
[proof_step] |
d95055489fce
Added translation for lambda expressions in terms.
steckerm
parents:
58142
diff
changeset
|
570 |
else |
58403 | 571 |
let |
572 |
fun mk_steps _ [] = [] |
|
573 |
| mk_steps i (x :: xs) = (((waldmeister_name ^ "_" ^ Int.toString i),[]), |
|
574 |
Plain, mk_Trueprop ((is_conjecture ? mk_not) x), waldmeister_skolemize_rule, |
|
575 |
[(waldmeister_name ^ "_" ^ Int.toString (i-1), |
|
59469 | 576 |
if i = 1 then isabelle_names else [])]) |
58403 | 577 |
:: mk_steps (i+1) xs |
578 |
||
579 |
val first_step = ((waldmeister_name ^ "_0", isabelle_names), Unknown, |
|
580 |
mk_Trueprop ((is_conjecture ? mk_not) step), rule, []) |
|
581 |
||
582 |
val sub_steps = mk_steps 1 steps |
|
583 |
||
584 |
val skolem_steps = first_step :: sub_steps |
|
585 |
val num_of_steps = length skolem_steps |
|
586 |
in |
|
59469 | 587 |
(skolem_steps @ |
58403 | 588 |
[((waldmeister_name, []), Unknown, trm, waldmeister_skolemize_rule, |
589 |
[(waldmeister_name ^ "_" ^ Int.toString (num_of_steps - 1), |
|
590 |
if num_of_steps = 1 then isabelle_names else [])])]) |
|
591 |
end |
|
58142 | 592 |
end |
59469 | 593 |
|
58403 | 594 |
fun introduce_waldmeister_skolems info proof_steps = proof_steps |
58411 | 595 |
|> maps (skolemization_steps info) |
58402 | 596 |
end; |