equal
deleted
inserted
replaced
289 in |
289 in |
290 fst (fold_map (project induct_inst) parts 0) |
290 fst (fold_map (project induct_inst) parts 0) |
291 end |
291 end |
292 |
292 |
293 |
293 |
294 fun forall_elim s (Const ("all", _) $ Abs (_, _, t)) = subst_bound (s, t) |
294 fun forall_elim s (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = subst_bound (s, t) |
295 | forall_elim _ t = t |
295 | forall_elim _ t = t |
296 |
296 |
297 val forall_elim_list = fold forall_elim |
297 val forall_elim_list = fold forall_elim |
298 |
298 |
299 fun split_conj_thm th = |
299 fun split_conj_thm th = |
314 |
314 |
315 (* extracting the acc-premises from the induction theorems *) |
315 (* extracting the acc-premises from the induction theorems *) |
316 val acc_prems = |
316 val acc_prems = |
317 map prop_of induct_thms |
317 map prop_of induct_thms |
318 |> map2 forall_elim_list argss |
318 |> map2 forall_elim_list argss |
319 |> map (strip_qnt_body "all") |
319 |> map (strip_qnt_body @{const_name Pure.all}) |
320 |> map (curry Logic.nth_prem 1) |
320 |> map (curry Logic.nth_prem 1) |
321 |> map HOLogic.dest_Trueprop |
321 |> map HOLogic.dest_Trueprop |
322 |
322 |
323 fun mk_goal acc_prem (f, args) = |
323 fun mk_goal acc_prem (f, args) = |
324 let |
324 let |