15 val add_simps: thm list -> Context.generic -> Context.generic |
15 val add_simps: thm list -> Context.generic -> Context.generic |
16 val add_simprocs: simproc list -> Context.generic -> Context.generic |
16 val add_simprocs: simproc list -> Context.generic -> Context.generic |
17 val add_inj_const: string * typ -> Context.generic -> Context.generic |
17 val add_inj_const: string * typ -> Context.generic -> Context.generic |
18 val add_discrete_type: string -> Context.generic -> Context.generic |
18 val add_discrete_type: string -> Context.generic -> Context.generic |
19 val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic |
19 val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic |
20 val setup: Context.generic -> Context.generic |
|
21 val global_setup: theory -> theory |
20 val global_setup: theory -> theory |
|
21 val init_arith_data: Context.generic -> Context.generic |
22 val split_limit: int Config.T |
22 val split_limit: int Config.T |
23 val neq_limit: int Config.T |
23 val neq_limit: int Config.T |
24 val trace: bool Config.T |
24 val trace: bool Config.T |
25 end; |
25 end; |
26 |
26 |
971 (Method.insert_tac ctxt |
971 (Method.insert_tac ctxt |
972 (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>arith\<close>) @ facts) |
972 (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>arith\<close>) @ facts) |
973 THEN' tac ctxt)))) "linear arithmetic" #> |
973 THEN' tac ctxt)))) "linear arithmetic" #> |
974 Arith_Data.add_tactic "linear arithmetic" tac; |
974 Arith_Data.add_tactic "linear arithmetic" tac; |
975 |
975 |
976 val setup = |
|
977 init_arith_data |
|
978 #> add_discrete_type \<^type_name>\<open>nat\<close> |
|
979 #> add_lessD @{thm Suc_leI} |
|
980 #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False}, |
|
981 @{thm minus_diff_eq}, |
|
982 @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl}, |
|
983 @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one}, |
|
984 @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}]) |
|
985 #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject}, |
|
986 @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc}, |
|
987 @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}] |
|
988 #> add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>, |
|
989 \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>, |
|
990 \<^simproc>\<open>group_cancel_less\<close>] |
|
991 (*abel_cancel helps it work in abstract algebraic domains*) |
|
992 #> add_simprocs [\<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>, |
|
993 \<^simproc>\<open>natle_cancel_sums\<close>]; |
|
994 |
|
995 end; |
976 end; |