548 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, |
548 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, |
549 or just 5 (discarding nat) when n_sucs = 0 *) |
549 or just 5 (discarding nat) when n_sucs = 0 *) |
550 |
550 |
551 fun nat_get_Suc_simproc_fn n_sucs ctxt ct = |
551 fun nat_get_Suc_simproc_fn n_sucs ctxt ct = |
552 let |
552 let |
553 val thy = Proof_Context.theory_of ctxt; |
|
554 val (f $ arg) = Thm.term_of ct; |
553 val (f $ arg) = Thm.term_of ct; |
555 val n = (case arg of @{term nat} $ n => n | n => n) |
554 val n = (case arg of @{term nat} $ n => n | n => n) |
556 |> HOLogic.dest_number |> snd; |
555 |> HOLogic.dest_number |> snd; |
557 val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) |
556 val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) |
558 else (n, 0); |
557 else (n, 0); |
559 val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j) |
558 val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j) |
560 (replicate i @{term Suc}); |
559 (replicate i @{term Suc}); |
561 val _ = if arg = arg' then raise TERM ("", []) else (); |
560 val _ = if arg = arg' then raise TERM ("", []) else (); |
562 fun propfn g = HOLogic.mk_eq (g arg, g arg') |
561 fun propfn g = HOLogic.mk_eq (g arg, g arg') |
563 |> HOLogic.mk_Trueprop |> Thm.global_cterm_of thy; |
562 |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt; |
564 val eq1 = Goal.prove_internal ctxt [] (propfn I) |
563 val eq1 = Goal.prove_internal ctxt [] (propfn I) |
565 (K (simp_tac (put_simpset word_ss ctxt) 1)); |
564 (K (simp_tac (put_simpset word_ss ctxt) 1)); |
566 in Goal.prove_internal ctxt [] (propfn (curry (op $) f)) |
565 in Goal.prove_internal ctxt [] (propfn (curry (op $) f)) |
567 (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1)) |
566 (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1)) |
568 |> mk_meta_eq |> SOME end |
567 |> mk_meta_eq |> SOME end |