236 |
236 |
237 fun cluster_of_zapped_var_name s = |
237 fun cluster_of_zapped_var_name s = |
238 ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)), |
238 ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)), |
239 String.isPrefix new_skolem_var_prefix s) |
239 String.isPrefix new_skolem_var_prefix s) |
240 |
240 |
241 fun zap_quantifiers ax_no = |
241 fun rename_vars_to_be_zapped ax_no = |
242 let |
242 let |
243 fun conv (cluster as (cluster_no, cluster_skolem)) pos ct = |
243 fun aux (cluster as (cluster_no, cluster_skolem)) pos t = |
|
244 case t of |
|
245 (t1 as Const (s, _)) $ Abs (s', T, t') => |
|
246 if s = @{const_name all} orelse s = @{const_name All} orelse |
|
247 s = @{const_name Ex} then |
|
248 let |
|
249 val skolem = (pos = (s = @{const_name Ex})) |
|
250 val cluster = |
|
251 if skolem = cluster_skolem then cluster |
|
252 else (cluster_no |> cluster_skolem ? Integer.add 1, skolem) |
|
253 val s' = zapped_var_name ax_no cluster s' |
|
254 in t1 $ Abs (s', T, aux cluster pos t') end |
|
255 else |
|
256 t |
|
257 | (t1 as Const (s, _)) $ t2 $ t3 => |
|
258 if s = @{const_name "==>"} orelse |
|
259 s = @{const_name HOL.implies} then |
|
260 t1 $ aux cluster (not pos) t2 $ aux cluster pos t3 |
|
261 else if s = @{const_name HOL.conj} orelse |
|
262 s = @{const_name HOL.disj} then |
|
263 t1 $ aux cluster pos t2 $ aux cluster pos t3 |
|
264 else |
|
265 t |
|
266 | (t1 as Const (s, _)) $ t2 => |
|
267 if s = @{const_name Trueprop} then t1 $ aux cluster pos t2 |
|
268 else if s = @{const_name Not} then t1 $ aux cluster (not pos) t2 |
|
269 else t |
|
270 | _ => t |
|
271 in aux (0, true) true end |
|
272 |
|
273 val zap_quantifiers = |
|
274 let |
|
275 fun conv pos ct = |
244 ct |> (case term_of ct of |
276 ct |> (case term_of ct of |
245 Const (s, _) $ Abs (s', _, _) => |
277 Const (s, _) $ Abs (s', _, _) => |
246 if s = @{const_name all} orelse s = @{const_name All} orelse |
278 if s = @{const_name all} orelse s = @{const_name All} orelse |
247 s = @{const_name Ex} then |
279 s = @{const_name Ex} then |
248 let |
280 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd |
249 val skolem = (pos = (s = @{const_name Ex})) |
281 #> conv pos |
250 val cluster = |
|
251 if skolem = cluster_skolem then cluster |
|
252 else (cluster_no |> cluster_skolem ? Integer.add 1, skolem) |
|
253 in |
|
254 Thm.dest_comb #> snd |
|
255 #> Thm.dest_abs (SOME (zapped_var_name ax_no cluster s')) |
|
256 #> snd #> conv cluster pos |
|
257 end |
|
258 else |
282 else |
259 Conv.all_conv |
283 Conv.all_conv |
260 | Const (s, _) $ _ $ _ => |
284 | Const (s, _) $ _ $ _ => |
261 if s = @{const_name "==>"} orelse |
285 if s = @{const_name "==>"} orelse |
262 s = @{const_name HOL.implies} then |
286 s = @{const_name HOL.implies} then |
263 Conv.combination_conv (Conv.arg_conv (conv cluster (not pos))) |
287 Conv.combination_conv (Conv.arg_conv (conv (not pos))) |
264 (conv cluster pos) |
288 (conv pos) |
265 else if s = @{const_name HOL.conj} orelse |
289 else if s = @{const_name HOL.conj} orelse |
266 s = @{const_name HOL.disj} then |
290 s = @{const_name HOL.disj} then |
267 Conv.combination_conv (Conv.arg_conv (conv cluster pos)) |
291 Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos) |
268 (conv cluster pos) |
|
269 else |
292 else |
270 Conv.all_conv |
293 Conv.all_conv |
271 | Const (s, _) $ _ => |
294 | Const (s, _) $ _ => |
272 if s = @{const_name Trueprop} then |
295 if s = @{const_name Trueprop} then Conv.arg_conv (conv pos) |
273 Conv.arg_conv (conv cluster pos) |
296 else if s = @{const_name Not} then Conv.arg_conv (conv (not pos)) |
274 else if s = @{const_name Not} then |
297 else Conv.all_conv |
275 Conv.arg_conv (conv cluster (not pos)) |
|
276 else |
|
277 Conv.all_conv |
|
278 | _ => Conv.all_conv) |
298 | _ => Conv.all_conv) |
279 in |
299 in |
280 conv (0, true) true #> Drule.export_without_context |
300 conv true #> Drule.export_without_context |
281 #> cprop_of #> Thm.dest_equals #> snd |
301 #> cprop_of #> Thm.dest_equals #> snd |
282 end |
302 end |
283 |
303 |
284 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths |
304 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths |
285 |
305 |