equal
deleted
inserted
replaced
75 |
75 |
76 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)" |
76 lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)" |
77 by (simp add: intrel_def) |
77 by (simp add: intrel_def) |
78 |
78 |
79 lemma equiv_intrel: "equiv UNIV intrel" |
79 lemma equiv_intrel: "equiv UNIV intrel" |
80 by (simp add: intrel_def equiv_def refl_def sym_def trans_def) |
80 by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def) |
81 |
81 |
82 text{*Reduces equality of equivalence classes to the @{term intrel} relation: |
82 text{*Reduces equality of equivalence classes to the @{term intrel} relation: |
83 @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *} |
83 @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *} |
84 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] |
84 lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] |
85 |
85 |
830 case (nonneg n) |
830 case (nonneg n) |
831 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
831 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
832 le_imp_0_less [THEN order_less_imp_le]) |
832 le_imp_0_less [THEN order_less_imp_le]) |
833 next |
833 next |
834 case (neg n) |
834 case (neg n) |
835 thus ?thesis by (simp del: of_nat_Suc of_nat_add |
835 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 |
836 add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric]) |
836 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) |
837 qed |
837 qed |
838 |
838 |
839 lemma bin_less_0_simps: |
839 lemma bin_less_0_simps: |
840 "Pls < 0 \<longleftrightarrow> False" |
840 "Pls < 0 \<longleftrightarrow> False" |
841 "Min < 0 \<longleftrightarrow> True" |
841 "Min < 0 \<longleftrightarrow> True" |
1163 case (nonneg n) |
1163 case (nonneg n) |
1164 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
1164 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
1165 le_imp_0_less [THEN order_less_imp_le]) |
1165 le_imp_0_less [THEN order_less_imp_le]) |
1166 next |
1166 next |
1167 case (neg n) |
1167 case (neg n) |
1168 thus ?thesis by (simp del: of_nat_Suc of_nat_add |
1168 thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 |
1169 add: algebra_simps of_nat_1 [symmetric] of_nat_add [symmetric]) |
1169 add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) |
1170 qed |
1170 qed |
1171 |
1171 |
1172 text {* Less-Than or Equals *} |
1172 text {* Less-Than or Equals *} |
1173 |
1173 |
1174 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
1174 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
1545 |
1545 |
1546 lemma abs_power_minus_one [simp]: |
1546 lemma abs_power_minus_one [simp]: |
1547 "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" |
1547 "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})" |
1548 by (simp add: power_abs) |
1548 by (simp add: power_abs) |
1549 |
1549 |
1550 lemma of_int_number_of_eq: |
1550 lemma of_int_number_of_eq [simp]: |
1551 "of_int (number_of v) = (number_of v :: 'a :: number_ring)" |
1551 "of_int (number_of v) = (number_of v :: 'a :: number_ring)" |
1552 by (simp add: number_of_eq) |
1552 by (simp add: number_of_eq) |
1553 |
1553 |
1554 text{*Lemmas for specialist use, NOT as default simprules*} |
1554 text{*Lemmas for specialist use, NOT as default simprules*} |
1555 lemma mult_2: "2 * z = (z+z::'a::number_ring)" |
1555 lemma mult_2: "2 * z = (z+z::'a::number_ring)" |
1783 subsection{*Intermediate value theorems*} |
1783 subsection{*Intermediate value theorems*} |
1784 |
1784 |
1785 lemma int_val_lemma: |
1785 lemma int_val_lemma: |
1786 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) --> |
1786 "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) --> |
1787 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))" |
1787 f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))" |
|
1788 unfolding One_nat_def |
1788 apply (induct n, simp) |
1789 apply (induct n, simp) |
1789 apply (intro strip) |
1790 apply (intro strip) |
1790 apply (erule impE, simp) |
1791 apply (erule impE, simp) |
1791 apply (erule_tac x = n in allE, simp) |
1792 apply (erule_tac x = n in allE, simp) |
1792 apply (case_tac "k = f (n+1) ") |
1793 apply (case_tac "k = f (Suc n)") |
1793 apply force |
1794 apply force |
1794 apply (erule impE) |
1795 apply (erule impE) |
1795 apply (simp add: abs_if split add: split_if_asm) |
1796 apply (simp add: abs_if split add: split_if_asm) |
1796 apply (blast intro: le_SucI) |
1797 apply (blast intro: le_SucI) |
1797 done |
1798 done |
1801 lemma nat_intermed_int_val: |
1802 lemma nat_intermed_int_val: |
1802 "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n; |
1803 "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n; |
1803 f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)" |
1804 f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)" |
1804 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k |
1805 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k |
1805 in int_val_lemma) |
1806 in int_val_lemma) |
|
1807 unfolding One_nat_def |
1806 apply simp |
1808 apply simp |
1807 apply (erule exE) |
1809 apply (erule exE) |
1808 apply (rule_tac x = "i+m" in exI, arith) |
1810 apply (rule_tac x = "i+m" in exI, arith) |
1809 done |
1811 done |
1810 |
1812 |