equal
deleted
inserted
replaced
421 |
421 |
422 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
422 lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" |
423 by transfer (clarsimp simp add: of_nat_diff) |
423 by transfer (clarsimp simp add: of_nat_diff) |
424 |
424 |
425 end |
425 end |
|
426 |
|
427 lemma diff_nat_numeral [simp]: |
|
428 "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" |
|
429 by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) |
|
430 |
426 |
431 |
427 text {* For termination proofs: *} |
432 text {* For termination proofs: *} |
428 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. |
433 lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. |
429 |
434 |
430 |
435 |
745 lemmas int_int_eq = of_nat_eq_iff [where 'a=int] |
750 lemmas int_int_eq = of_nat_eq_iff [where 'a=int] |
746 lemmas numeral_1_eq_1 = numeral_One |
751 lemmas numeral_1_eq_1 = numeral_One |
747 |
752 |
748 subsection {* Setting up simplification procedures *} |
753 subsection {* Setting up simplification procedures *} |
749 |
754 |
|
755 lemmas of_int_simps = |
|
756 of_int_0 of_int_1 of_int_add of_int_mult |
|
757 |
750 lemmas int_arith_rules = |
758 lemmas int_arith_rules = |
751 neg_le_iff_le numeral_One |
759 numeral_One more_arith_simps of_nat_simps of_int_simps |
752 minus_zero left_minus right_minus |
|
753 mult_zero_left mult_zero_right mult_1_left mult_1_right |
|
754 mult_minus_left mult_minus_right |
|
755 minus_add_distrib minus_minus mult_assoc |
|
756 of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
|
757 of_int_0 of_int_1 of_int_add of_int_mult |
|
758 |
760 |
759 ML_file "Tools/int_arith.ML" |
761 ML_file "Tools/int_arith.ML" |
760 declaration {* K Int_Arith.setup *} |
762 declaration {* K Int_Arith.setup *} |
761 |
763 |
762 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
764 simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | |
873 (if z' < 0 then nat z |
875 (if z' < 0 then nat z |
874 else let d = z-z' in |
876 else let d = z-z' in |
875 if d < 0 then 0 else nat d)" |
877 if d < 0 then 0 else nat d)" |
876 by (simp add: Let_def nat_diff_distrib [symmetric]) |
878 by (simp add: Let_def nat_diff_distrib [symmetric]) |
877 |
879 |
878 lemma diff_nat_numeral [simp]: |
|
879 "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')" |
|
880 by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) |
|
881 |
|
882 lemma nat_numeral_diff_1 [simp]: |
880 lemma nat_numeral_diff_1 [simp]: |
883 "numeral v - (1::nat) = nat (numeral v - 1)" |
881 "numeral v - (1::nat) = nat (numeral v - 1)" |
884 using diff_nat_numeral [of v Num.One] by simp |
882 using diff_nat_numeral [of v Num.One] by simp |
885 |
|
886 lemmas nat_arith = diff_nat_numeral |
|
887 |
883 |
888 |
884 |
889 subsection "Induction principles for int" |
885 subsection "Induction principles for int" |
890 |
886 |
891 text{*Well-founded segments of the integers*} |
887 text{*Well-founded segments of the integers*} |