38 fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp; |
38 fun mp_step n th = if n = 0 then th else (mp_step (n - 1) th) RS mp; |
39 |
39 |
40 |
40 |
41 fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) => |
41 fun linz_tac ctxt q = Object_Logic.atomize_prems_tac ctxt THEN' SUBGOAL (fn (g, i) => |
42 let |
42 let |
43 val thy = Proof_Context.theory_of ctxt; |
|
44 (* Transform the term*) |
43 (* Transform the term*) |
45 val (t, np, nh) = prepare_for_linz q g; |
44 val (t, np, nh) = prepare_for_linz q g; |
46 (* Some simpsets for dealing with mod div abs and nat*) |
45 (* Some simpsets for dealing with mod div abs and nat*) |
47 val mod_div_simpset = |
46 val mod_div_simpset = |
48 put_simpset HOL_basic_ss ctxt |
47 put_simpset HOL_basic_ss ctxt |
71 put_simpset HOL_basic_ss ctxt |
70 put_simpset HOL_basic_ss ctxt |
72 addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}] |
71 addsimps [@{thm nat_0_le}, @{thm all_nat}, @{thm ex_nat}, @{thm zero_le_numeral}, @{thm order_refl}(* FIXME: necessary? *), @{thm int_0}, @{thm int_1}] |
73 |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong} |
72 |> fold Simplifier.add_cong @{thms conj_le_cong imp_le_cong} |
74 (* simp rules for elimination of abs *) |
73 (* simp rules for elimination of abs *) |
75 val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split} |
74 val simpset3 = put_simpset HOL_basic_ss ctxt |> Splitter.add_split @{thm abs_split} |
76 val ct = Thm.global_cterm_of thy (HOLogic.mk_Trueprop t) |
75 val ct = Thm.cterm_of ctxt (HOLogic.mk_Trueprop t) |
77 (* Theorem for the nat --> int transformation *) |
76 (* Theorem for the nat --> int transformation *) |
78 val pre_thm = Seq.hd (EVERY |
77 val pre_thm = Seq.hd (EVERY |
79 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
78 [simp_tac mod_div_simpset 1, simp_tac simpset0 1, |
80 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
79 TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1), |
81 TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)] |
80 TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)] |
84 (* The result of the quantifier elimination *) |
83 (* The result of the quantifier elimination *) |
85 val (th, tac) = |
84 val (th, tac) = |
86 (case Thm.prop_of pre_thm of |
85 (case Thm.prop_of pre_thm of |
87 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
86 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
88 let |
87 let |
89 val pth = linzqe_oracle (Thm.global_cterm_of thy (Envir.eta_long [] t1)) |
88 val pth = linzqe_oracle (Thm.cterm_of ctxt (Envir.eta_long [] t1)) |
90 in |
89 in |
91 ((pth RS iffD2) RS pre_thm, |
90 ((pth RS iffD2) RS pre_thm, |
92 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
91 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) |
93 end |
92 end |
94 | _ => (pre_thm, assm_tac i)) |
93 | _ => (pre_thm, assm_tac i)) |