equal
deleted
inserted
replaced
1974 |
1974 |
1975 lemma abs_mult: |
1975 lemma abs_mult: |
1976 "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" |
1976 "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" |
1977 by (rule abs_eq_mult) auto |
1977 by (rule abs_eq_mult) auto |
1978 |
1978 |
1979 lemma abs_mult_self: |
1979 lemma abs_mult_self [simp]: |
1980 "\<bar>a\<bar> * \<bar>a\<bar> = a * a" |
1980 "\<bar>a\<bar> * \<bar>a\<bar> = a * a" |
1981 by (simp add: abs_if) |
1981 by (simp add: abs_if) |
1982 |
1982 |
1983 lemma abs_mult_less: |
1983 lemma abs_mult_less: |
1984 "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d" |
1984 "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d" |