equal
deleted
inserted
replaced
240 fun rename_bound_vars_to_be_zapped ax_no = |
240 fun rename_bound_vars_to_be_zapped ax_no = |
241 let |
241 let |
242 fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t = |
242 fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t = |
243 case t of |
243 case t of |
244 (t1 as Const (s, _)) $ Abs (s', T, t') => |
244 (t1 as Const (s, _)) $ Abs (s', T, t') => |
245 if s = @{const_name all} orelse s = @{const_name All} orelse |
245 if s = @{const_name Pure.all} orelse s = @{const_name All} orelse |
246 s = @{const_name Ex} then |
246 s = @{const_name Ex} then |
247 let |
247 let |
248 val skolem = (pos = (s = @{const_name Ex})) |
248 val skolem = (pos = (s = @{const_name Ex})) |
249 val (cluster, index_no) = |
249 val (cluster, index_no) = |
250 if skolem = cluster_skolem then (cluster, index_no) |
250 if skolem = cluster_skolem then (cluster, index_no) |
252 val s' = zapped_var_name cluster index_no s' |
252 val s' = zapped_var_name cluster index_no s' |
253 in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end |
253 in t1 $ Abs (s', T, aux cluster (index_no + 1) pos t') end |
254 else |
254 else |
255 t |
255 t |
256 | (t1 as Const (s, _)) $ t2 $ t3 => |
256 | (t1 as Const (s, _)) $ t2 $ t3 => |
257 if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then |
257 if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then |
258 t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3 |
258 t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3 |
259 else if s = @{const_name HOL.conj} orelse |
259 else if s = @{const_name HOL.conj} orelse |
260 s = @{const_name HOL.disj} then |
260 s = @{const_name HOL.disj} then |
261 t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3 |
261 t1 $ aux cluster index_no pos t2 $ aux cluster index_no pos t3 |
262 else |
262 else |
273 |
273 |
274 fun zap pos ct = |
274 fun zap pos ct = |
275 ct |
275 ct |
276 |> (case term_of ct of |
276 |> (case term_of ct of |
277 Const (s, _) $ Abs (s', _, _) => |
277 Const (s, _) $ Abs (s', _, _) => |
278 if s = @{const_name all} orelse s = @{const_name All} orelse |
278 if s = @{const_name Pure.all} orelse s = @{const_name All} orelse |
279 s = @{const_name Ex} then |
279 s = @{const_name Ex} then |
280 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos |
280 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos |
281 else |
281 else |
282 Conv.all_conv |
282 Conv.all_conv |
283 | Const (s, _) $ _ $ _ => |
283 | Const (s, _) $ _ $ _ => |
284 if s = @{const_name "==>"} orelse s = @{const_name implies} then |
284 if s = @{const_name Pure.imp} orelse s = @{const_name implies} then |
285 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |
285 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |
286 else if s = @{const_name conj} orelse s = @{const_name disj} then |
286 else if s = @{const_name conj} orelse s = @{const_name disj} then |
287 Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) |
287 Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) |
288 else |
288 else |
289 Conv.all_conv |
289 Conv.all_conv |