8 end |
8 end |
9 |
9 |
10 structure Cooper_Tac: COOPER_TAC = |
10 structure Cooper_Tac: COOPER_TAC = |
11 struct |
11 struct |
12 |
12 |
13 val cooper_ss = simpset_of @{context}; |
13 val cooper_ss = simpset_of \<^context>; |
14 |
14 |
15 fun prepare_for_linz q fm = |
15 fun prepare_for_linz q fm = |
16 let |
16 let |
17 val ps = Logic.strip_params fm |
17 val ps = Logic.strip_params fm |
18 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
18 val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm) |
24 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
24 fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; |
25 val rhs = hs |
25 val rhs = hs |
26 val np = length ps |
26 val np = length ps |
27 val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) |
27 val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) |
28 (List.foldr HOLogic.mk_imp c rhs, np) ps |
28 (List.foldr HOLogic.mk_imp c rhs, np) ps |
29 val (vs, _) = List.partition (fn t => q orelse (type_of t) = @{typ nat}) |
29 val (vs, _) = List.partition (fn t => q orelse (type_of t) = \<^typ>\<open>nat\<close>) |
30 (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm'); |
30 (Misc_Legacy.term_frees fm' @ Misc_Legacy.term_vars fm'); |
31 val fm2 = List.foldr mk_all2 fm' vs |
31 val fm2 = List.foldr mk_all2 fm' vs |
32 in (fm2, np + length vs, length rhs) end; |
32 in (fm2, np + length vs, length rhs) end; |
33 |
33 |
34 (*Object quantifier to meta --*) |
34 (*Object quantifier to meta --*) |
51 mod_self |
51 mod_self |
52 div_by_0 mod_by_0 div_0 mod_0 |
52 div_by_0 mod_by_0 div_0 mod_0 |
53 div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0 |
53 div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0 |
54 Suc_eq_plus1} |
54 Suc_eq_plus1} |
55 addsimps @{thms ac_simps} |
55 addsimps @{thms ac_simps} |
56 addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}] |
56 addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>] |
57 val simpset0 = |
57 val simpset0 = |
58 put_simpset HOL_basic_ss ctxt |
58 put_simpset HOL_basic_ss ctxt |
59 addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms} |
59 addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms} |
60 |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max} |
60 |> fold Splitter.add_split @{thms split_zdiv split_zmod split_div' split_min split_max} |
61 (* Simp rules for changing (n::int) to int n *) |
61 (* Simp rules for changing (n::int) to int n *) |
82 (Thm.trivial ct)) |
82 (Thm.trivial ct)) |
83 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) |
83 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i) |
84 (* The result of the quantifier elimination *) |
84 (* The result of the quantifier elimination *) |
85 val (th, tac) = |
85 val (th, tac) = |
86 (case Thm.prop_of pre_thm of |
86 (case Thm.prop_of pre_thm of |
87 Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ => |
87 Const (\<^const_name>\<open>Pure.imp\<close>, _) $ (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t1) $ _ => |
88 let |
88 let |
89 val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1) |
89 val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1) |
90 in |
90 in |
91 ((pth RS iffD2) RS pre_thm, |
91 ((pth RS iffD2) RS pre_thm, |
92 assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i)) |
92 assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i)) |