49 fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp; |
49 fun mp_step n th = if n = 0 then th else mp_step (n - 1) th RS mp; |
50 |
50 |
51 val context_ss = simpset_of (the_context ()); |
51 val context_ss = simpset_of (the_context ()); |
52 |
52 |
53 fun ferrack_tac q i = ObjectLogic.atomize_tac i |
53 fun ferrack_tac q i = ObjectLogic.atomize_tac i |
54 THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, abs_split] i) |
54 THEN REPEAT_DETERM (split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}] i) |
55 THEN (fn st => |
55 THEN (fn st => |
56 let |
56 let |
57 val g = nth (prems_of st) (i - 1) |
57 val g = nth (prems_of st) (i - 1) |
58 val thy = Thm.theory_of_thm st |
58 val thy = Thm.theory_of_thm st |
59 (* Transform the term*) |
59 (* Transform the term*) |
60 val (t,np,nh) = prepare_for_linr q g |
60 val (t,np,nh) = prepare_for_linr q g |
61 (* Some simpsets for dealing with mod div abs and nat*) |
61 (* Some simpsets for dealing with mod div abs and nat*) |
62 val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}] |
62 val simpset0 = HOL_basic_ss addsimps comp_arith addsplits [@{thm split_min}, @{thm split_max}] |
63 (* simp rules for elimination of abs *) |
63 (* simp rules for elimination of abs *) |
64 val simpset3 = HOL_basic_ss addsplits [abs_split] |
64 val simpset3 = HOL_basic_ss addsplits [@{thm abs_split}] |
65 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
65 val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
66 (* Theorem for the nat --> int transformation *) |
66 (* Theorem for the nat --> int transformation *) |
67 val pre_thm = Seq.hd (EVERY |
67 val pre_thm = Seq.hd (EVERY |
68 [simp_tac simpset0 1, TRY (simp_tac context_ss 1)] |
68 [simp_tac simpset0 1, TRY (simp_tac context_ss 1)] |
69 (trivial ct)) |
69 (trivial ct)) |