396 |> implies_intr (cprop_of case_hyp) |
396 |> implies_intr (cprop_of case_hyp) |
397 |> implies_intr z_eq_arg |
397 |> implies_intr z_eq_arg |
398 |
398 |
399 val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs)))) |
399 val zx_eq_arg_lhs = cterm_of thy (Trueprop (mk_eq (mk_prod (z,x), mk_prod (arg,lhs)))) |
400 |
400 |
401 val z_acc' = z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject) |
401 val z_acc' = (z_acc COMP (assume zx_eq_arg_lhs COMP Pair_inject)) |
|
402 |> FundefCtxTree.export_thm thy ([], (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes)) |
|
403 |
|
404 val occvars = fold (OrdList.insert Term.term_ord) (term_frees (prop_of z_acc')) [] |
|
405 val ordvars = fold (OrdList.insert Term.term_ord) (map Free fixes @ qs) [] (* FIXME... remove when inductive behaves nice *) |
|
406 |> OrdList.inter Term.term_ord occvars |
402 |
407 |
403 val ethm = z_acc' |
408 val ethm = z_acc' |
404 |> FundefCtxTree.export_thm thy (fixes, (term_of zx_eq_arg_lhs) :: map prop_of (ags @ assumes)) |
409 |> FundefCtxTree.export_thm thy (map dest_Free ordvars, []) |
405 |> fold_rev forall_intr cqs |
|
406 |
410 |
407 |
411 |
408 val sub' = sub @ [(([],[]), acc)] |
412 val sub' = sub @ [(([],[]), acc)] |
409 in |
413 in |
410 (sub', (hyp :: hyps, ethm :: thms)) |
414 (sub', (hyp :: hyps, ethm :: thms)) |