equal
deleted
inserted
replaced
650 |
650 |
651 lemma nat_of_bool [simp]: |
651 lemma nat_of_bool [simp]: |
652 "nat (of_bool P) = of_bool P" |
652 "nat (of_bool P) = of_bool P" |
653 by auto |
653 by auto |
654 |
654 |
655 lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))" |
655 lemma split_nat [linarith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))" |
656 (is "?P = (?L \<and> ?R)") |
656 (is "?P = (?L \<and> ?R)") |
657 for i :: int |
657 for i :: int |
658 proof (cases "i < 0") |
658 proof (cases "i < 0") |
659 case True |
659 case True |
660 then show ?thesis |
660 then show ?thesis |
737 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" |
737 lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" |
738 by simp |
738 by simp |
739 |
739 |
740 text \<open> |
740 text \<open> |
741 This version is proved for all ordered rings, not just integers! |
741 This version is proved for all ordered rings, not just integers! |
742 It is proved here because attribute \<open>arith_split\<close> is not available |
742 It is proved here because attribute \<open>linarith_split\<close> is not available |
743 in theory \<open>Rings\<close>. |
743 in theory \<open>Rings\<close>. |
744 But is it really better than just rewriting with \<open>abs_if\<close>? |
744 But is it really better than just rewriting with \<open>abs_if\<close>? |
745 \<close> |
745 \<close> |
746 lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))" |
746 lemma abs_split [linarith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))" |
747 for a :: "'a::linordered_idom" |
747 for a :: "'a::linordered_idom" |
748 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) |
748 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) |
749 |
749 |
750 lemma negD: |
750 lemma negD: |
751 assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))" |
751 assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))" |