710 |
710 |
711 lemma "(-x < -y) = (y < (x::real))" |
711 lemma "(-x < -y) = (y < (x::real))" |
712 by arith |
712 by arith |
713 |
713 |
714 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
714 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
715 by (tactic "fast_arith_tac @{context} 1") |
715 by linarith |
716 |
716 |
717 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
717 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
718 by (tactic "fast_arith_tac @{context} 1") |
718 by linarith |
719 |
719 |
720 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
720 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
721 by (tactic "fast_arith_tac @{context} 1") |
721 by linarith |
722 |
722 |
723 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
723 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
724 by (tactic "fast_arith_tac @{context} 1") |
724 by linarith |
725 |
725 |
726 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
726 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
727 by (tactic "fast_arith_tac @{context} 1") |
727 by linarith |
728 |
728 |
729 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k" |
729 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k" |
730 by arith |
730 by arith |
731 |
731 |
732 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
732 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
733 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
733 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
734 by (tactic "fast_arith_tac @{context} 1") |
734 by linarith |
735 |
735 |
736 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
736 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
737 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
737 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
738 by (tactic "fast_arith_tac @{context} 1") |
738 by linarith |
739 |
739 |
740 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
740 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
741 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
741 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
742 by (tactic "fast_arith_tac @{context} 1") |
742 by linarith |
743 |
743 |
744 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
744 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
745 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l" |
745 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l" |
746 by (tactic "fast_arith_tac @{context} 1") |
746 by linarith |
747 |
747 |
748 |
748 |
749 subsection{*Complex Arithmetic*} |
749 subsection{*Complex Arithmetic*} |
750 |
750 |
751 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" |
751 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" |