src/HOL/Fields.thy
author haftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70344 050104f01bf9
parent 70343 e54caaa38ad9
child 70356 4a327c061870
permissions -rw-r--r--
moved comment to approproiate place
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
     1
(*  Title:      HOL/Fields.thy
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     2
    Author:     Gertrud Bauer
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     3
    Author:     Steven Obua
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     4
    Author:     Tobias Nipkow
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     5
    Author:     Lawrence C Paulson
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     6
    Author:     Markus Wenzel
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30961
diff changeset
     7
    Author:     Jeremy Avigad
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
     8
*)
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff changeset
     9
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
    10
section \<open>Fields\<close>
25152
bfde2f8c0f63 partially localized
haftmann
parents: 25078
diff changeset
    11
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
    12
theory Fields
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    13
imports Nat
25186
f4d1ebffd025 localized further
haftmann
parents: 25152
diff changeset
    14
begin
14421
ee97b6463cb4 new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents: 14398
diff changeset
    15
69502
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    16
context idom
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    17
begin
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    18
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    19
lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    20
proof
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    21
  assume ?P
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    22
  show ?Q
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    23
  proof
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    24
    assume \<open>a = 0\<close>
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    25
    with \<open>?P\<close> have "inj ((*) 0)"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    26
      by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    27
    moreover have "0 * 0 = 0 * 1"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    28
      by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    29
    ultimately have "0 = 1"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    30
      by (rule injD)
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    31
    then show False
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    32
      by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    33
  qed
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    34
next
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    35
  assume ?Q then show ?P
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    36
    by (auto intro: injI)
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    37
qed
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    38
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    39
end
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    40
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
    41
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
    42
subsection \<open>Division rings\<close>
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    43
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
    44
text \<open>
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    45
  A division ring is like a field, but without the commutativity requirement.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
    46
\<close>
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    47
60352
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59867
diff changeset
    48
class inverse = divide +
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    49
  fixes inverse :: "'a \<Rightarrow> 'a"
58776
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58512
diff changeset
    50
begin
60352
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59867
diff changeset
    51
  
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59867
diff changeset
    52
abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59867
diff changeset
    53
where
d46de31a50c4 separate class for division operator, with particular syntax added in more specific classes
haftmann
parents: 59867
diff changeset
    54
  "inverse_divide \<equiv> divide"
58776
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58512
diff changeset
    55
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58512
diff changeset
    56
end
95e58e04e534 use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
hoelzl
parents: 58512
diff changeset
    57
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    58
text \<open>Setup for linear arithmetic prover\<close>
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    59
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    60
ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69593
diff changeset
    61
ML_file \<open>Tools/lin_arith.ML\<close>
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    62
setup \<open>Lin_Arith.global_setup\<close>
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    63
declaration \<open>K Lin_Arith.setup\<close>
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    64
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    65
simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    66
  \<open>K Lin_Arith.simproc\<close>
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    67
(* Because of this simproc, the arithmetic solver is really only
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    68
useful to detect inconsistencies among the premises for subgoals which are
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    69
*not* themselves (in)equalities, because the latter activate
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    70
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    71
solver all the time rather than add the additional check. *)
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    72
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    73
lemmas [arith_split] = nat_diff_split split_min split_max
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    74
67969
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    75
context linordered_nonzero_semiring
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    76
begin
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    77
lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    78
  by (auto simp: max_def)
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    79
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    80
lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    81
  by (auto simp: min_def)
83c8cafdebe8 Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents: 67091
diff changeset
    82
end
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
    83
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61238
diff changeset
    84
text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
    85
57950
59c17b0b870d updated to named_theorems;
wenzelm
parents: 57514
diff changeset
    86
named_theorems divide_simps "rewrite rules to eliminate divisions"
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
    87
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    88
class division_ring = ring_1 + inverse +
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    89
  assumes left_inverse [simp]:  "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    90
  assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    91
  assumes divide_inverse: "a / b = a * inverse b"
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59779
diff changeset
    92
  assumes inverse_zero [simp]: "inverse 0 = 0"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    93
begin
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    94
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    95
subclass ring_1_no_zero_divisors
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    96
proof
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    97
  fix a b :: 'a
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    98
  assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
    99
  show "a * b \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   100
  proof
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   101
    assume ab: "a * b = 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   102
    hence "0 = inverse a * (a * b) * inverse b" by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   103
    also have "\<dots> = (inverse a * a) * (b * inverse b)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   104
      by (simp only: mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   105
    also have "\<dots> = 1" using a b by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   106
    finally show False by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   107
  qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   108
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   109
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   110
lemma nonzero_imp_inverse_nonzero:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   111
  "a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   112
proof
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   113
  assume ianz: "inverse a = 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   114
  assume "a \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   115
  hence "1 = a * inverse a" by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   116
  also have "... = 0" by (simp add: ianz)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   117
  finally have "1 = 0" .
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   118
  thus False by (simp add: eq_commute)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   119
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   120
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   121
lemma inverse_zero_imp_zero:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   122
  "inverse a = 0 \<Longrightarrow> a = 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   123
apply (rule classical)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   124
apply (drule nonzero_imp_inverse_nonzero)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   125
apply auto
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   126
done
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   127
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   128
lemma inverse_unique:
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   129
  assumes ab: "a * b = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   130
  shows "inverse a = b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   131
proof -
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   132
  have "a \<noteq> 0" using ab by (cases "a = 0") simp_all
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   133
  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   134
  ultimately show ?thesis by (simp add: mult.assoc [symmetric])
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   135
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   136
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   137
lemma nonzero_inverse_minus_eq:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   138
  "a \<noteq> 0 \<Longrightarrow> inverse (- a) = - inverse a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   139
by (rule inverse_unique) simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   140
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   141
lemma nonzero_inverse_inverse_eq:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   142
  "a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   143
by (rule inverse_unique) simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   144
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   145
lemma nonzero_inverse_eq_imp_eq:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   146
  assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   147
  shows "a = b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   148
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   149
  from \<open>inverse a = inverse b\<close>
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   150
  have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   151
  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> show "a = b"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   152
    by (simp add: nonzero_inverse_inverse_eq)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   153
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   154
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   155
lemma inverse_1 [simp]: "inverse 1 = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   156
by (rule inverse_unique) simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   157
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   158
lemma nonzero_inverse_mult_distrib:
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   159
  assumes "a \<noteq> 0" and "b \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   160
  shows "inverse (a * b) = inverse b * inverse a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   161
proof -
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   162
  have "a * (b * inverse b) * inverse a = 1" using assms by simp
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   163
  hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   164
  thus ?thesis by (rule inverse_unique)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   165
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   166
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   167
lemma division_ring_inverse_add:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   168
  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   169
by (simp add: algebra_simps)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   170
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   171
lemma division_ring_inverse_diff:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   172
  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   173
by (simp add: algebra_simps)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   174
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   175
lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   176
proof
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   177
  assume neq: "b \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   178
  {
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   179
    hence "a = (a / b) * b" by (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   180
    also assume "a / b = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   181
    finally show "a = b" by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   182
  next
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   183
    assume "a = b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   184
    with neq show "a / b = 1" by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   185
  }
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   186
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   187
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   188
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   189
by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   190
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   191
lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   192
by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   193
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   194
lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   195
by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   196
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   197
lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   198
by (simp add: divide_inverse algebra_simps)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   199
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   200
lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   201
  by (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   202
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   203
lemma minus_divide_left: "- (a / b) = (-a) / b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   204
  by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   205
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   206
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   207
  by (simp add: divide_inverse nonzero_inverse_minus_eq)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   208
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   209
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   210
  by (simp add: divide_inverse nonzero_inverse_minus_eq)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   211
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56445
diff changeset
   212
lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   213
  by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   214
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   215
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56445
diff changeset
   216
  using add_divide_distrib [of a "- b" c] by simp
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   217
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   218
lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   219
proof -
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   220
  assume [simp]: "c \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   221
  have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   222
  also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   223
  finally show ?thesis .
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   224
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   225
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   226
lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   227
proof -
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   228
  assume [simp]: "c \<noteq> 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   229
  have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   230
  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   231
  finally show ?thesis .
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   232
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   233
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   234
lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b"
59535
9e7467829db5 less warnings
haftmann
parents: 58889
diff changeset
   235
  using nonzero_divide_eq_eq[of b "-a" c] by simp
56441
49e95c9ebb59 made field_simps "more complete"
nipkow
parents: 56414
diff changeset
   236
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   237
lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   238
  using nonzero_neg_divide_eq_eq[of b a c] by auto
56441
49e95c9ebb59 made field_simps "more complete"
nipkow
parents: 56414
diff changeset
   239
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   240
lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   241
  by (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   242
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   243
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   244
  by (drule sym) (simp add: divide_inverse mult.assoc)
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   245
56445
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   246
lemma add_divide_eq_iff [field_simps]:
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   247
  "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   248
  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   249
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   250
lemma divide_add_eq_iff [field_simps]:
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   251
  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   252
  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   253
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   254
lemma diff_divide_eq_iff [field_simps]:
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   255
  "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   256
  by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   257
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   258
lemma minus_divide_add_eq_iff [field_simps]:
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   259
  "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z"
59535
9e7467829db5 less warnings
haftmann
parents: 58889
diff changeset
   260
  by (simp add: add_divide_distrib diff_divide_eq_iff)
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   261
56445
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   262
lemma divide_diff_eq_iff [field_simps]:
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   263
  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   264
  by (simp add: field_simps)
82ce19612fe8 tuned lemmas: more general class
nipkow
parents: 56441
diff changeset
   265
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   266
lemma minus_divide_diff_eq_iff [field_simps]:
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   267
  "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
59535
9e7467829db5 less warnings
haftmann
parents: 58889
diff changeset
   268
  by (simp add: divide_diff_eq_iff[symmetric])
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   269
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   270
lemma division_ring_divide_zero [simp]:
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   271
  "a / 0 = 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   272
  by (simp add: divide_inverse)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   273
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   274
lemma divide_self_if [simp]:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   275
  "a / a = (if a = 0 then 0 else 1)"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   276
  by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   277
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   278
lemma inverse_nonzero_iff_nonzero [simp]:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   279
  "inverse a = 0 \<longleftrightarrow> a = 0"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   280
  by rule (fact inverse_zero_imp_zero, simp)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   281
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   282
lemma inverse_minus_eq [simp]:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   283
  "inverse (- a) = - inverse a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   284
proof cases
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   285
  assume "a=0" thus ?thesis by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   286
next
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   287
  assume "a\<noteq>0"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   288
  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   289
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   290
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   291
lemma inverse_inverse_eq [simp]:
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   292
  "inverse (inverse a) = a"
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   293
proof cases
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   294
  assume "a=0" thus ?thesis by simp
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   295
next
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   296
  assume "a\<noteq>0"
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   297
  thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   298
qed
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   299
44680
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   300
lemma inverse_eq_imp_eq:
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   301
  "inverse a = inverse b \<Longrightarrow> a = b"
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   302
  by (drule arg_cong [where f="inverse"], simp)
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   303
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   304
lemma inverse_eq_iff_eq [simp]:
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   305
  "inverse a = inverse b \<longleftrightarrow> a = b"
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   306
  by (force dest!: inverse_eq_imp_eq)
761f427ef1ab simplify proof
huffman
parents: 44064
diff changeset
   307
69791
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   308
lemma mult_commute_imp_mult_inverse_commute:
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   309
  assumes "y * x = x * y"
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   310
  shows   "inverse y * x = x * inverse y"
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   311
proof (cases "y=0")
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   312
  case False
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   313
  hence "x * inverse y = inverse y * y * x * inverse y"
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   314
    by simp
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   315
  also have "\<dots> = inverse y * (x * y * inverse y)"
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   316
    by (simp add: mult.assoc assms)
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   317
  finally show ?thesis by (simp add: mult.assoc False)
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   318
qed simp
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   319
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   320
lemmas mult_inverse_of_nat_commute =
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   321
  mult_commute_imp_mult_inverse_commute[OF mult_of_nat_commute]
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   322
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   323
lemma divide_divide_eq_left':
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   324
  "(a / b) / c = a / (c * b)"
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   325
  by (cases "b = 0 \<or> c = 0")
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   326
     (auto simp: divide_inverse mult.assoc nonzero_inverse_mult_distrib)
195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents: 69605
diff changeset
   327
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   328
lemma add_divide_eq_if_simps [divide_simps]:
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   329
    "a + b / z = (if z = 0 then a else (a * z + b) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   330
    "a / z + b = (if z = 0 then b else (a + b * z) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   331
    "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   332
    "a - b / z = (if z = 0 then a else (a * z - b) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   333
    "a / z - b = (if z = 0 then -b else (a - b * z) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   334
    "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   335
  by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   336
      minus_divide_diff_eq_iff)
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   337
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   338
lemma [divide_simps]:
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   339
  shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   340
    and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   341
    and minus_divide_eq_eq: "- (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then - b = a * c else a = 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   342
    and eq_minus_divide_eq: "a = - (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c = - b else a = 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   343
  by (auto simp add:  field_simps)
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
   344
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   345
end
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   346
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   347
subsection \<open>Fields\<close>
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 42904
diff changeset
   348
22987
550709aa8e66 instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents: 22842
diff changeset
   349
class field = comm_ring_1 + inverse +
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   350
  assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   351
  assumes field_divide_inverse: "a / b = a * inverse b"
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59779
diff changeset
   352
  assumes field_inverse_zero: "inverse 0 = 0"
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   353
begin
20496
23eb6034c06d added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents: 19404
diff changeset
   354
25267
1f745c599b5c proper reinitialisation after subclass
haftmann
parents: 25238
diff changeset
   355
subclass division_ring
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28559
diff changeset
   356
proof
22987
550709aa8e66 instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents: 22842
diff changeset
   357
  fix a :: 'a
550709aa8e66 instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents: 22842
diff changeset
   358
  assume "a \<noteq> 0"
550709aa8e66 instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents: 22842
diff changeset
   359
  thus "inverse a * a = 1" by (rule field_inverse)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   360
  thus "a * inverse a = 1" by (simp only: mult.commute)
35084
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   361
next
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   362
  fix a b :: 'a
e25eedfc15ce moved constants inverse and divide to Ring.thy
haftmann
parents: 35050
diff changeset
   363
  show "a / b = a * inverse b" by (rule field_divide_inverse)
59867
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59779
diff changeset
   364
next
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59779
diff changeset
   365
  show "inverse 0 = 0"
58043346ca64 given up separate type classes demanding `inverse 0 = 0`
haftmann
parents: 59779
diff changeset
   366
    by (fact field_inverse_zero) 
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14603
diff changeset
   367
qed
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   368
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   369
subclass idom_divide
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   370
proof
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   371
  fix b a
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   372
  assume "b \<noteq> 0"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   373
  then show "a * b / b = a"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   374
    by (simp add: divide_inverse ac_simps)
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   375
next
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   376
  fix a
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   377
  show "a / 0 = 0"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   378
    by (simp add: divide_inverse)
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   379
qed
25230
022029099a83 continued localization
haftmann
parents: 25193
diff changeset
   380
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   381
text\<open>There is no slick version using division by zero.\<close>
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   382
lemma inverse_add:
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   383
  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   384
  by (simp add: division_ring_inverse_add ac_simps)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   385
70147
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   386
lemma nonzero_mult_divide_mult_cancel_left [simp]:
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   387
  assumes [simp]: "c \<noteq> 0"
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   388
  shows "(c * a) / (c * b) = a / b"
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   389
proof (cases "b = 0")
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   390
  case True then show ?thesis by simp
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   391
next
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   392
  case False
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   393
  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   394
    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   395
  also have "... =  a * inverse b * (inverse c * c)"
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   396
    by (simp only: ac_simps)
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   397
  also have "... =  a * inverse b" by simp
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   398
    finally show ?thesis by (simp add: divide_inverse)
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   399
qed
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   400
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   401
lemma nonzero_mult_divide_mult_cancel_right [simp]:
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   402
  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   403
  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
1657688a6406 backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents: 70094
diff changeset
   404
36304
6984744e6b34 less special treatment of times_divide_eq [simp]
haftmann
parents: 36301
diff changeset
   405
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   406
  by (simp add: divide_inverse ac_simps)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   407
61238
e3d8a313a649 Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents: 61076
diff changeset
   408
lemma divide_inverse_commute: "a / b = inverse b * a"
e3d8a313a649 Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents: 61076
diff changeset
   409
  by (simp add: divide_inverse mult.commute)
e3d8a313a649 Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents: 61076
diff changeset
   410
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   411
lemma add_frac_eq:
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   412
  assumes "y \<noteq> 0" and "z \<noteq> 0"
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   413
  shows "x / y + w / z = (x * z + w * y) / (y * z)"
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   414
proof -
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   415
  have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   416
    using assms by simp
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   417
  also have "\<dots> = (x * z + y * w) / (y * z)"
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   418
    by (simp only: add_divide_distrib)
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   419
  finally show ?thesis
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   420
    by (simp only: mult.commute)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   421
qed
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   422
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   423
text\<open>Special Cancellation Simprules for Division\<close>
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   424
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   425
lemma nonzero_divide_mult_cancel_right [simp]:
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   426
  "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   427
  using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   428
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   429
lemma nonzero_divide_mult_cancel_left [simp]:
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   430
  "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   431
  using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   432
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   433
lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   434
  "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   435
  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   436
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   437
lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   438
  "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   439
  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   440
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   441
lemma diff_frac_eq:
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   442
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
36348
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 36343
diff changeset
   443
  by (simp add: field_simps)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   444
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   445
lemma frac_eq_eq:
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   446
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
36348
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 36343
diff changeset
   447
  by (simp add: field_simps)
89c54f51f55a dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents: 36343
diff changeset
   448
58512
dc4d76dfa8f0 moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents: 57950
diff changeset
   449
lemma divide_minus1 [simp]: "x / - 1 = - x"
dc4d76dfa8f0 moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents: 57950
diff changeset
   450
  using nonzero_minus_divide_right [of "1" x] by simp
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   451
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   452
text\<open>This version builds in division by zero while also re-orienting
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   453
      the right-hand side.\<close>
14270
342451d763f9 More re-organising of numerical theorems
paulson
parents: 14269
diff changeset
   454
lemma inverse_mult_distrib [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   455
  "inverse (a * b) = inverse a * inverse b"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   456
proof cases
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
   457
  assume "a \<noteq> 0 \<and> b \<noteq> 0"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   458
  thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   459
next
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
   460
  assume "\<not> (a \<noteq> 0 \<and> b \<noteq> 0)"
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   461
  thus ?thesis by force
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   462
qed
14270
342451d763f9 More re-organising of numerical theorems
paulson
parents: 14269
diff changeset
   463
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
   464
lemma inverse_divide [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   465
  "inverse (a / b) = b / a"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   466
  by (simp add: divide_inverse mult.commute)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
   467
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   468
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   469
text \<open>Calculations with fractions\<close>
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
   470
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61238
diff changeset
   471
text\<open>There is a whole bunch of simp-rules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   472
because the latter are covered by a simproc.\<close>
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23406
diff changeset
   473
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   474
lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   475
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   476
lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23406
diff changeset
   477
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   478
lemma divide_divide_eq_right [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   479
  "a / (b / c) = (a * c) / b"
57514
bdc2c6b40bf2 prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents: 57512
diff changeset
   480
  by (simp add: divide_inverse ac_simps)
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 14284
diff changeset
   481
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   482
lemma divide_divide_eq_left [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   483
  "(a / b) / c = a / (b * c)"
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   484
  by (simp add: divide_inverse mult.assoc)
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 14284
diff changeset
   485
56365
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   486
lemma divide_divide_times_eq:
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   487
  "(x / y) / (z / w) = (x * w) / (y * z)"
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   488
  by simp
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   489
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   490
text \<open>Special Cancellation Simprules for Division\<close>
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   491
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   492
lemma mult_divide_mult_cancel_left_if [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   493
  shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
60353
838025c6e278 implicit partial divison operation in integral domains
haftmann
parents: 60352
diff changeset
   494
  by simp
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23406
diff changeset
   495
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15229
diff changeset
   496
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   497
text \<open>Division and Unary Minus\<close>
14293
22542982bffd moving some division theorems to Ring_and_Field
paulson
parents: 14288
diff changeset
   498
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   499
lemma minus_divide_right:
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   500
  "- (a / b) = a / - b"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   501
  by (simp add: divide_inverse)
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14421
diff changeset
   502
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56445
diff changeset
   503
lemma divide_minus_right [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   504
  "a / - b = - (a / b)"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   505
  by (simp add: divide_inverse)
30630
4fbe1401bac2 move field lemmas into class locale context
huffman
parents: 30242
diff changeset
   506
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56445
diff changeset
   507
lemma minus_divide_divide:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   508
  "(- a) / (- b) = a / b"
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   509
  by (cases "b=0") (simp_all add: nonzero_minus_divide_divide)
14293
22542982bffd moving some division theorems to Ring_and_Field
paulson
parents: 14288
diff changeset
   510
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   511
lemma inverse_eq_1_iff [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   512
  "inverse x = 1 \<longleftrightarrow> x = 1"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   513
  by (insert inverse_eq_iff_eq [of x 1], simp)
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   514
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   515
lemma divide_eq_0_iff [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   516
  "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   517
  by (simp add: divide_inverse)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   518
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   519
lemma divide_cancel_right [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   520
  "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   521
  by (cases "c=0") (simp_all add: divide_inverse)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   522
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   523
lemma divide_cancel_left [simp]:
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   524
  "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   525
  by (cases "c=0") (simp_all add: divide_inverse)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   526
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   527
lemma divide_eq_1_iff [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   528
  "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   529
  by (cases "b=0") (simp_all add: right_inverse_eq)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   530
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   531
lemma one_eq_divide_iff [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   532
  "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   533
  by (simp add: eq_commute [of 1])
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   534
65057
799bbbb3a395 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents: 64591
diff changeset
   535
lemma divide_eq_minus_1_iff:
799bbbb3a395 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents: 64591
diff changeset
   536
   "(a / b = - 1) \<longleftrightarrow> b \<noteq> 0 \<and> a = - b"
799bbbb3a395 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents: 64591
diff changeset
   537
using divide_eq_1_iff by fastforce
799bbbb3a395 Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents: 64591
diff changeset
   538
36719
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   539
lemma times_divide_times_eq:
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   540
  "(x / y) * (z / w) = (x * z) / (y * w)"
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   541
  by simp
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   542
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   543
lemma add_frac_num:
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   544
  "y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y"
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   545
  by (simp add: add_divide_distrib)
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   546
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   547
lemma add_num_frac:
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   548
  "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   549
  by (simp add: add_divide_distrib add.commute)
d396f6f63d94 moved some lemmas from Groebner_Basis here
haftmann
parents: 36425
diff changeset
   550
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   551
lemma dvd_field_iff:
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   552
  "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   553
proof (cases "a = 0")
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   554
  case False
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   555
  then have "b = a * (b / a)"
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   556
    by (simp add: field_simps)
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   557
  then have "a dvd b" ..
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   558
  with False show ?thesis
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   559
    by simp
68527
2f4e2aab190a Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents: 67969
diff changeset
   560
qed simp
64591
240a39af9ec4 restructured matter on polynomials and normalized fractions
haftmann
parents: 64329
diff changeset
   561
69502
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   562
lemma inj_divide_right [simp]:
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   563
  "inj (\<lambda>b. b / a) \<longleftrightarrow> a \<noteq> 0"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   564
proof -
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   565
  have "(\<lambda>b. b / a) = (*) (inverse a)"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   566
    by (simp add: field_simps fun_eq_iff)
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   567
  then have "inj (\<lambda>y. y / a) \<longleftrightarrow> inj ((*) (inverse a))"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   568
    by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   569
  also have "\<dots> \<longleftrightarrow> inverse a \<noteq> 0"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   570
    by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   571
  also have "\<dots> \<longleftrightarrow> a \<noteq> 0"
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   572
    by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   573
  finally show ?thesis
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   574
    by simp
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   575
qed
0cf906072e20 more rules
haftmann
parents: 68547
diff changeset
   576
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
   577
end
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   578
62481
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
   579
class field_char_0 = field + ring_char_0
b5d8e57826df tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents: 62347
diff changeset
   580
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   581
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   582
subsection \<open>Ordered fields\<close>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   583
64290
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   584
class field_abs_sgn = field + idom_abs_sgn
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   585
begin
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   586
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   587
lemma sgn_inverse [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   588
  "sgn (inverse a) = inverse (sgn a)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   589
proof (cases "a = 0")
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   590
  case True then show ?thesis by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   591
next
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   592
  case False
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   593
  then have "a * inverse a = 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   594
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   595
  then have "sgn (a * inverse a) = sgn 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   596
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   597
  then have "sgn a * sgn (inverse a) = 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   598
    by (simp add: sgn_mult)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   599
  then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   600
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   601
  then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   602
    by (simp add: ac_simps)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   603
  with False show ?thesis
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   604
    by (simp add: sgn_eq_0_iff)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   605
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   606
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   607
lemma abs_inverse [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   608
  "\<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   609
proof -
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   610
  from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a]
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   611
  have "inverse (sgn a) * \<bar>inverse a\<bar> = inverse (sgn a * \<bar>a\<bar>)"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   612
    by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   613
  then show ?thesis by (auto simp add: sgn_eq_0_iff)
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   614
qed
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   615
    
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   616
lemma sgn_divide [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   617
  "sgn (a / b) = sgn a / sgn b"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   618
  unfolding divide_inverse sgn_mult by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   619
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   620
lemma abs_divide [simp]:
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   621
  "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   622
  unfolding divide_inverse abs_mult by simp
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   623
  
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   624
end
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
   625
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   626
class linordered_field = field + linordered_idom
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   627
begin
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   628
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   629
lemma positive_imp_inverse_positive:
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   630
  assumes a_gt_0: "0 < a"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   631
  shows "0 < inverse a"
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
   632
proof -
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   633
  have "0 < a * inverse a"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   634
    by (simp add: a_gt_0 [THEN less_imp_not_eq2])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   635
  thus "0 < inverse a"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   636
    by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
   637
qed
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   638
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   639
lemma negative_imp_inverse_negative:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   640
  "a < 0 \<Longrightarrow> inverse a < 0"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   641
  by (insert positive_imp_inverse_positive [of "-a"],
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   642
    simp add: nonzero_inverse_minus_eq less_imp_not_eq)
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   643
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   644
lemma inverse_le_imp_le:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   645
  assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   646
  shows "b \<le> a"
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
   647
proof (rule classical)
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
   648
  assume "\<not> b \<le> a"
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
   649
  hence "a < b"  by (simp add: linorder_not_le)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   650
  hence bpos: "0 < b"  by (blast intro: apos less_trans)
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   651
  hence "a * inverse a \<le> a * inverse b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   652
    by (simp add: apos invle less_imp_le mult_left_mono)
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   653
  hence "(a * inverse a) * b \<le> (a * inverse b) * b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   654
    by (simp add: bpos less_imp_le mult_right_mono)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
   655
  thus "b \<le> a"  by (simp add: mult.assoc apos bpos less_imp_not_eq2)
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
   656
qed
14268
5cf13e80be0e Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents: 14267
diff changeset
   657
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   658
lemma inverse_positive_imp_positive:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   659
  assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   660
  shows "0 < a"
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   661
proof -
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   662
  have "0 < inverse (inverse a)"
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   663
    using inv_gt_0 by (rule positive_imp_inverse_positive)
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   664
  thus "0 < a"
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   665
    using nz by (simp add: nonzero_inverse_inverse_eq)
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
   666
qed
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
   667
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   668
lemma inverse_negative_imp_negative:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   669
  assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   670
  shows "a < 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   671
proof -
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   672
  have "inverse (inverse a) < 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   673
    using inv_less_0 by (rule negative_imp_inverse_negative)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   674
  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   675
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   676
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   677
lemma linordered_field_no_lb:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   678
  "\<forall>x. \<exists>y. y < x"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   679
proof
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   680
  fix x::'a
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   681
  have m1: "- (1::'a) < 0" by simp
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   682
  from add_strict_right_mono[OF m1, where c=x]
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   683
  have "(- 1) + x < x" by simp
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   684
  thus "\<exists>y. y < x" by blast
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   685
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   686
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   687
lemma linordered_field_no_ub:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   688
  "\<forall> x. \<exists>y. y > x"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   689
proof
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   690
  fix x::'a
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   691
  have m1: " (1::'a) > 0" by simp
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   692
  from add_strict_right_mono[OF m1, where c=x]
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   693
  have "1 + x > x" by simp
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   694
  thus "\<exists>y. y > x" by blast
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   695
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   696
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   697
lemma less_imp_inverse_less:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   698
  assumes less: "a < b" and apos:  "0 < a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   699
  shows "inverse b < inverse a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   700
proof (rule ccontr)
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
   701
  assume "\<not> inverse b < inverse a"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   702
  hence "inverse a \<le> inverse b" by simp
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
   703
  hence "\<not> (a < b)"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   704
    by (simp add: not_less inverse_le_imp_le [OF _ apos])
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   705
  thus False by (rule notE [OF _ less])
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   706
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   707
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   708
lemma inverse_less_imp_less:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   709
  "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   710
apply (simp add: less_le [of "inverse a"] less_le [of "b"])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   711
apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   712
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   713
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   714
text\<open>Both premises are essential. Consider -1 and 1.\<close>
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   715
lemma inverse_less_iff_less [simp]:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   716
  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   717
  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   718
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   719
lemma le_imp_inverse_le:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   720
  "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   721
  by (force simp add: le_less less_imp_inverse_less)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   722
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   723
lemma inverse_le_iff_le [simp]:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   724
  "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   725
  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   726
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   727
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   728
text\<open>These results refer to both operands being negative.  The opposite-sign
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   729
case is trivial, since inverse preserves signs.\<close>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   730
lemma inverse_le_imp_le_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   731
  "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   732
apply (rule classical)
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   733
apply (subgoal_tac "a < 0")
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   734
 prefer 2 apply force
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   735
apply (insert inverse_le_imp_le [of "-b" "-a"])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   736
apply (simp add: nonzero_inverse_minus_eq)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   737
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   738
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   739
lemma less_imp_inverse_less_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   740
   "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   741
apply (subgoal_tac "a < 0")
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   742
 prefer 2 apply (blast intro: less_trans)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   743
apply (insert less_imp_inverse_less [of "-b" "-a"])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   744
apply (simp add: nonzero_inverse_minus_eq)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   745
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   746
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   747
lemma inverse_less_imp_less_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   748
   "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   749
apply (rule classical)
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   750
apply (subgoal_tac "a < 0")
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   751
 prefer 2
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   752
 apply force
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   753
apply (insert inverse_less_imp_less [of "-b" "-a"])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   754
apply (simp add: nonzero_inverse_minus_eq)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   755
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   756
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   757
lemma inverse_less_iff_less_neg [simp]:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   758
  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   759
apply (insert inverse_less_iff_less [of "-b" "-a"])
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   760
apply (simp del: inverse_less_iff_less
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   761
            add: nonzero_inverse_minus_eq)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   762
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   763
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   764
lemma le_imp_inverse_le_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   765
  "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   766
  by (force simp add: le_less less_imp_inverse_less_neg)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   767
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
   768
lemma inverse_le_iff_le_neg [simp]:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   769
  "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   770
  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   771
36774
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   772
lemma one_less_inverse:
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   773
  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   774
  using less_imp_inverse_less [of a 1, unfolded inverse_1] .
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   775
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   776
lemma one_le_inverse:
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   777
  "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   778
  using le_imp_inverse_le [of a 1, unfolded inverse_1] .
9e444b09fbef add lemmas one_less_inverse and one_le_inverse
huffman
parents: 36719
diff changeset
   779
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   780
lemma pos_le_divide_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   781
  assumes "0 < c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   782
  shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   783
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   784
  from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   785
    using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps)
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   786
  also have "... \<longleftrightarrow> a * c \<le> b"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   787
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   788
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   789
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   790
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   791
lemma pos_less_divide_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   792
  assumes "0 < c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   793
  shows "a < b / c \<longleftrightarrow> a * c < b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   794
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   795
  from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   796
    using mult_less_cancel_right [of a c "b / c"] by auto
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   797
  also have "... = (a*c < b)"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   798
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   799
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   800
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   801
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   802
lemma neg_less_divide_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   803
  assumes "c < 0"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   804
  shows "a < b / c \<longleftrightarrow> b < a * c"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   805
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   806
  from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   807
    using mult_less_cancel_right [of "b / c" c a] by auto
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   808
  also have "... \<longleftrightarrow> b < a * c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   809
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   810
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   811
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   812
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   813
lemma neg_le_divide_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   814
  assumes "c < 0"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   815
  shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   816
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   817
  from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   818
    using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps)
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   819
  also have "... \<longleftrightarrow> b \<le> a * c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   820
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   821
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   822
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   823
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   824
lemma pos_divide_le_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   825
  assumes "0 < c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   826
  shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   827
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   828
  from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   829
    using mult_le_cancel_right [of "b / c" c a] by auto
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   830
  also have "... \<longleftrightarrow> b \<le> a * c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   831
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   832
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   833
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   834
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   835
lemma pos_divide_less_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   836
  assumes "0 < c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   837
  shows "b / c < a \<longleftrightarrow> b < a * c"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   838
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   839
  from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   840
    using mult_less_cancel_right [of "b / c" c a] by auto
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   841
  also have "... \<longleftrightarrow> b < a * c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   842
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   843
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   844
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   845
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   846
lemma neg_divide_le_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   847
  assumes "c < 0"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   848
  shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   849
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   850
  from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   851
    using mult_le_cancel_right [of a c "b / c"] by auto
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   852
  also have "... \<longleftrightarrow> a * c \<le> b"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   853
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   854
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   855
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   856
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   857
lemma neg_divide_less_eq [field_simps]:
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   858
  assumes "c < 0"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   859
  shows "b / c < a \<longleftrightarrow> a * c < b"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   860
proof -
59546
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   861
  from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c"
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   862
    using mult_less_cancel_right [of a c "b / c"] by auto
3850a2d20f19 times_divide_eq rules are already [simp] despite of comment
haftmann
parents: 59535
diff changeset
   863
  also have "... \<longleftrightarrow> a * c < b"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   864
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   865
  finally show ?thesis .
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   866
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   867
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61238
diff changeset
   868
text\<open>The following \<open>field_simps\<close> rules are necessary, as minus is always moved atop of
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   869
division but we want to get rid of division.\<close>
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   870
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   871
lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   872
  unfolding minus_divide_left by (rule pos_le_divide_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   873
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   874
lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   875
  unfolding minus_divide_left by (rule neg_le_divide_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   876
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   877
lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   878
  unfolding minus_divide_left by (rule pos_less_divide_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   879
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   880
lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   881
  unfolding minus_divide_left by (rule neg_less_divide_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   882
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   883
lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   884
  unfolding minus_divide_left by (rule pos_divide_less_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   885
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   886
lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   887
  unfolding minus_divide_left by (rule neg_divide_less_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   888
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   889
lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   890
  unfolding minus_divide_left by (rule pos_divide_le_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   891
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   892
lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   893
  unfolding minus_divide_left by (rule neg_divide_le_eq)
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
   894
56365
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   895
lemma frac_less_eq:
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   896
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   897
  by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   898
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   899
lemma frac_le_eq:
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   900
  "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   901
  by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
713f9b9a7e51 New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents: 55718
diff changeset
   902
56541
0e3abadbef39 made divide_pos_pos a simp rule
nipkow
parents: 56481
diff changeset
   903
lemma divide_pos_pos[simp]:
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   904
  "0 < x ==> 0 < y ==> 0 < x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   905
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   906
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   907
lemma divide_nonneg_pos:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   908
  "0 <= x ==> 0 < y ==> 0 <= x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   909
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   910
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   911
lemma divide_neg_pos:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   912
  "x < 0 ==> 0 < y ==> x / y < 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   913
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   914
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   915
lemma divide_nonpos_pos:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   916
  "x <= 0 ==> 0 < y ==> x / y <= 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   917
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   918
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   919
lemma divide_pos_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   920
  "0 < x ==> y < 0 ==> x / y < 0"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   921
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   922
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   923
lemma divide_nonneg_neg:
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   924
  "0 <= x ==> y < 0 ==> x / y <= 0"
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   925
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   926
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   927
lemma divide_neg_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   928
  "x < 0 ==> y < 0 ==> 0 < x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   929
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   930
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   931
lemma divide_nonpos_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   932
  "x <= 0 ==> y < 0 ==> 0 <= x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   933
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   934
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   935
lemma divide_strict_right_mono:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   936
     "[|a < b; 0 < c|] ==> a / c < b / c"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   937
by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   938
              positive_imp_inverse_positive)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   939
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   940
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   941
lemma divide_strict_right_mono_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   942
     "[|b < a; c < 0|] ==> a / c < b / c"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   943
apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   944
apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   945
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   946
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69502
diff changeset
   947
text\<open>The last premise ensures that \<^term>\<open>a\<close> and \<^term>\<open>b\<close>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
   948
      have the same sign\<close>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   949
lemma divide_strict_left_mono:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   950
  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
44921
58eef4843641 tuned proofs
huffman
parents: 44680
diff changeset
   951
  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   952
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   953
lemma divide_left_mono:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   954
  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
44921
58eef4843641 tuned proofs
huffman
parents: 44680
diff changeset
   955
  by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   956
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   957
lemma divide_strict_left_mono_neg:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   958
  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
44921
58eef4843641 tuned proofs
huffman
parents: 44680
diff changeset
   959
  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   960
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   961
lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   962
    x / y <= z"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   963
by (subst pos_divide_le_eq, assumption+)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   964
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   965
lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   966
    z <= x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   967
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   968
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   969
lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   970
    x / y < z"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   971
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   972
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   973
lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   974
    z < x / y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   975
by(simp add:field_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   976
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   977
lemma frac_le: "0 <= x ==>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   978
    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   979
  apply (rule mult_imp_div_pos_le)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   980
  apply simp
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   981
  apply (subst times_divide_eq_left)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   982
  apply (rule mult_imp_le_div_pos, assumption)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   983
  apply (rule mult_mono)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   984
  apply simp_all
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   985
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   986
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   987
lemma frac_less: "0 <= x ==>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   988
    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   989
  apply (rule mult_imp_div_pos_less)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   990
  apply simp
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   991
  apply (subst times_divide_eq_left)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   992
  apply (rule mult_imp_less_div_pos, assumption)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   993
  apply (erule mult_less_le_imp_less)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   994
  apply simp_all
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   995
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   996
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
   997
lemma frac_less2: "0 < x ==>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   998
    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
   999
  apply (rule mult_imp_div_pos_less)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1000
  apply simp_all
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1001
  apply (rule mult_imp_less_div_pos, assumption)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1002
  apply (erule mult_le_less_imp_less)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1003
  apply simp_all
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1004
done
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1005
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1006
lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1007
by (simp add: field_simps zero_less_two)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1008
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1009
lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1010
by (simp add: field_simps zero_less_two)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1011
53215
5e47c31c6f7c renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents: 52435
diff changeset
  1012
subclass unbounded_dense_linorder
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1013
proof
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1014
  fix x y :: 'a
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1015
  from less_add_one show "\<exists>y. x < y" ..
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1016
  from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54147
diff changeset
  1017
  then have "x - 1 < x + 1 - 1" by simp
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1018
  then have "x - 1 < x" by (simp add: algebra_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1019
  then show "\<exists>y. y < x" ..
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1020
  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1021
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1022
64290
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1023
subclass field_abs_sgn ..
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1024
64329
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1025
lemma inverse_sgn [simp]:
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1026
  "inverse (sgn a) = sgn a"
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1027
  by (cases a 0 rule: linorder_cases) simp_all
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1028
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1029
lemma divide_sgn [simp]:
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1030
  "a / sgn b = a * sgn b"
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1031
  by (cases b 0 rule: linorder_cases) simp_all
8f9d27c89241 more on sgn in linear ordered fields
haftmann
parents: 64290
diff changeset
  1032
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1033
lemma nonzero_abs_inverse:
64290
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1034
  "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1035
  by (rule abs_inverse)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1036
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1037
lemma nonzero_abs_divide:
64290
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1038
  "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
fb5c74a58796 suitable logical type class for abs, sgn
haftmann
parents: 63952
diff changeset
  1039
  by (rule abs_divide)
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1040
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1041
lemma field_le_epsilon:
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1042
  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1043
  shows "x \<le> y"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1044
proof (rule dense_le)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1045
  fix t assume "t < x"
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1046
  hence "0 < x - t" by (simp add: less_diff_eq)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1047
  from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1048
  then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1049
  then show "t \<le> y" by (simp add: algebra_simps)
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1050
qed
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1051
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1052
lemma inverse_positive_iff_positive [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1053
  "(0 < inverse a) = (0 < a)"
21328
73bb86d0f483 dropped Inductive dependency
haftmann
parents: 21258
diff changeset
  1054
apply (cases "a = 0", simp)
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1055
apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1056
done
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1057
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1058
lemma inverse_negative_iff_negative [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1059
  "(inverse a < 0) = (a < 0)"
21328
73bb86d0f483 dropped Inductive dependency
haftmann
parents: 21258
diff changeset
  1060
apply (cases "a = 0", simp)
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1061
apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1062
done
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1063
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1064
lemma inverse_nonnegative_iff_nonnegative [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1065
  "0 \<le> inverse a \<longleftrightarrow> 0 \<le> a"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1066
  by (simp add: not_less [symmetric])
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1067
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1068
lemma inverse_nonpositive_iff_nonpositive [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1069
  "inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1070
  by (simp add: not_less [symmetric])
14277
ad66687ece6e more field division lemmas transferred from Real to Ring_and_Field
paulson
parents: 14272
diff changeset
  1071
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1072
lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1073
  using less_trans[of 1 x 0 for x]
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1074
  by (cases x 0 rule: linorder_cases) (auto simp add: field_simps)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
  1075
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1076
lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1077
proof (cases "x = 1")
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1078
  case True then show ?thesis by simp
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1079
next
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1080
  case False then have "inverse x \<noteq> 1" by simp
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1081
  then have "1 \<noteq> inverse x" by blast
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1082
  then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less)
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1083
  with False show ?thesis by (auto simp add: one_less_inverse_iff)
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1084
qed
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
  1085
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1086
lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1087
  by (simp add: not_le [symmetric] one_le_inverse_iff)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
  1088
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1089
lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1090
  by (simp add: not_less [symmetric] one_less_inverse_iff)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
  1091
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1092
lemma [divide_simps]:
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1093
  shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1094
    and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1095
    and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1096
    and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1097
    and le_minus_divide_eq: "a \<le> - (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le> - b else if c < 0 then - b \<le> a * c else a \<le> 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1098
    and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1099
    and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else  a < 0)"
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1100
    and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1101
  by (auto simp: field_simps not_less dest: antisym)
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 14284
diff changeset
  1102
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1103
text \<open>Division and Signs\<close>
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1104
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1105
lemma
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1106
  shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1107
    and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1108
    and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1109
    and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
56481
47500d0881f9 add divide_simps
hoelzl
parents: 56480
diff changeset
  1110
  by (auto simp add: divide_simps)
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1111
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1112
text \<open>Division and the Number One\<close>
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14348
diff changeset
  1113
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1114
text\<open>Simplify expressions equated with 1\<close>
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14348
diff changeset
  1115
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1116
lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1117
  by (cases "a = 0") (auto simp: field_simps)
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14348
diff changeset
  1118
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1119
lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1120
  using zero_eq_1_divide_iff[of a] by simp
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14348
diff changeset
  1121
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61238
diff changeset
  1122
text\<open>Simplify expressions such as \<open>0 < 1/x\<close> to \<open>0 < x\<close>\<close>
36423
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1123
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1124
lemma zero_le_divide_1_iff [simp]:
36423
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1125
  "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1126
  by (simp add: zero_le_divide_iff)
17085
5b57f995a179 more simprules now have names
paulson
parents: 16775
diff changeset
  1127
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1128
lemma zero_less_divide_1_iff [simp]:
36423
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1129
  "0 < 1 / a \<longleftrightarrow> 0 < a"
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1130
  by (simp add: zero_less_divide_iff)
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1131
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1132
lemma divide_le_0_1_iff [simp]:
36423
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1133
  "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1134
  by (simp add: divide_le_0_iff)
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1135
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1136
lemma divide_less_0_1_iff [simp]:
36423
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1137
  "1 / a < 0 \<longleftrightarrow> a < 0"
63fc238a7430 got rid of [simplified]
haftmann
parents: 36414
diff changeset
  1138
  by (simp add: divide_less_0_iff)
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14348
diff changeset
  1139
14293
22542982bffd moving some division theorems to Ring_and_Field
paulson
parents: 14288
diff changeset
  1140
lemma divide_right_mono:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1141
     "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1142
by (force simp add: divide_strict_right_mono le_less)
14293
22542982bffd moving some division theorems to Ring_and_Field
paulson
parents: 14288
diff changeset
  1143
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1144
lemma divide_right_mono_neg: "a <= b
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1145
    ==> c <= 0 ==> b / c <= a / c"
23482
2f4be6844f7c tuned and used field_simps
nipkow
parents: 23477
diff changeset
  1146
apply (drule divide_right_mono [of _ _ "- c"])
56479
91958d4b30f7 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents: 56445
diff changeset
  1147
apply auto
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1148
done
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1149
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1150
lemma divide_left_mono_neg: "a <= b
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1151
    ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1152
  apply (drule divide_left_mono [of _ _ "- c"])
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 56571
diff changeset
  1153
  apply (auto simp add: mult.commute)
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1154
done
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1155
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1156
lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1157
  by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1158
     (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff)
42904
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1159
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1160
lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
42904
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1161
  by (subst less_le) (auto simp: inverse_le_iff)
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1162
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1163
lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
42904
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1164
  by (simp add: divide_inverse mult_le_cancel_right)
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1165
56480
093ea91498e6 field_simps: better support for negation and division, and power
hoelzl
parents: 56479
diff changeset
  1166
lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
42904
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1167
  by (auto simp add: divide_inverse mult_less_cancel_right)
4aedcff42de6 add divide_.._cancel, inverse_.._iff
hoelzl
parents: 36774
diff changeset
  1168
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1169
text\<open>Simplify quotients that are compared with the value 1.\<close>
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1170
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1171
lemma le_divide_eq_1:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1172
  "(1 \<le> b / a) = ((0 < a \<and> a \<le> b) \<or> (a < 0 \<and> b \<le> a))"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1173
by (auto simp add: le_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1174
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1175
lemma divide_le_eq_1:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1176
  "(b / a \<le> 1) = ((0 < a \<and> b \<le> a) \<or> (a < 0 \<and> a \<le> b) \<or> a=0)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1177
by (auto simp add: divide_le_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1178
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1179
lemma less_divide_eq_1:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1180
  "(1 < b / a) = ((0 < a \<and> a < b) \<or> (a < 0 \<and> b < a))"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1181
by (auto simp add: less_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1182
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1183
lemma divide_less_eq_1:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1184
  "(b / a < 1) = ((0 < a \<and> b < a) \<or> (a < 0 \<and> a < b) \<or> a=0)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1185
by (auto simp add: divide_less_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1186
56571
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1187
lemma divide_nonneg_nonneg [simp]:
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1188
  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1189
  by (auto simp add: divide_simps)
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1190
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1191
lemma divide_nonpos_nonpos:
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1192
  "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1193
  by (auto simp add: divide_simps)
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1194
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1195
lemma divide_nonneg_nonpos:
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1196
  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1197
  by (auto simp add: divide_simps)
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1198
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1199
lemma divide_nonpos_nonneg:
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1200
  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56541
diff changeset
  1201
  by (auto simp add: divide_simps)
23389
aaca6a8e5414 tuned proofs: avoid implicit prems;
wenzelm
parents: 23326
diff changeset
  1202
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1203
text \<open>Conditional Simplification Rules: No Case Splits\<close>
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1204
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1205
lemma le_divide_eq_1_pos [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1206
  "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1207
by (auto simp add: le_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1208
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1209
lemma le_divide_eq_1_neg [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1210
  "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1211
by (auto simp add: le_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1212
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1213
lemma divide_le_eq_1_pos [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1214
  "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1215
by (auto simp add: divide_le_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1216
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1217
lemma divide_le_eq_1_neg [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1218
  "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1219
by (auto simp add: divide_le_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1220
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1221
lemma less_divide_eq_1_pos [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1222
  "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1223
by (auto simp add: less_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1224
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1225
lemma less_divide_eq_1_neg [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1226
  "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1227
by (auto simp add: less_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1228
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1229
lemma divide_less_eq_1_pos [simp]:
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36348
diff changeset
  1230
  "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
18649
bb99c2e705ca tidied, and added missing thm divide_less_eq_1_neg
paulson
parents: 18623
diff changeset
  1231
by (auto simp add: divide_less_eq)
bb99c2e705ca tidied, and added missing thm divide_less_eq_1_neg
paulson
parents: 18623
diff changeset
  1232
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1233
lemma divide_less_eq_1_neg [simp]:
61941
31f2105521ee discontinued ASCII replacement syntax <->;
wenzelm
parents: 61799
diff changeset
  1234
  "a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1235
by (auto simp add: divide_less_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1236
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1237
lemma eq_divide_eq_1 [simp]:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1238
  "(1 = b/a) = ((a \<noteq> 0 \<and> a = b))"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1239
by (auto simp add: eq_divide_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1240
54147
97a8ff4e4ac9 killed most "no_atp", to make Sledgehammer more complete
blanchet
parents: 53374
diff changeset
  1241
lemma divide_eq_eq_1 [simp]:
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1242
  "(b/a = 1) = ((a \<noteq> 0 \<and> a = b))"
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1243
by (auto simp add: divide_eq_eq)
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1244
59667
651ea265d568 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents: 59557
diff changeset
  1245
lemma abs_div_pos: "0 < y ==>
36301
72f4d079ebf8 more localization; factored out lemmas for division_ring
haftmann
parents: 35828
diff changeset
  1246
    \<bar>x\<bar> / y = \<bar>x / y\<bar>"
25304
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1247
  apply (subst abs_divide)
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1248
  apply (simp add: order_less_imp_le)
7491c00f0915 removed subclass edge ordered_ring < lordered_ring
haftmann
parents: 25267
diff changeset
  1249
done
16775
c1b87ef4a1c3 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents: 16568
diff changeset
  1250
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1251
lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a \<or> b = 0)"
55718
34618f031ba9 A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents: 54230
diff changeset
  1252
by (auto simp: zero_le_divide_iff)
34618f031ba9 A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents: 54230
diff changeset
  1253
67091
1393c2340eec more symbols;
wenzelm
parents: 65057
diff changeset
  1254
lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 \<or> b = 0)"
55718
34618f031ba9 A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents: 54230
diff changeset
  1255
by (auto simp: divide_le_0_iff)
34618f031ba9 A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents: 54230
diff changeset
  1256
35579
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1257
lemma field_le_mult_one_interval:
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1258
  assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1259
  shows "x \<le> y"
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1260
proof (cases "0 < x")
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1261
  assume "0 < x"
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1262
  thus ?thesis
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1263
    using dense_le_bounded[of 0 1 "y/x"] *
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60690
diff changeset
  1264
    unfolding le_divide_eq if_P[OF \<open>0 < x\<close>] by simp
35579
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1265
next
cc9a5a0ab5ea Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents: 35216
diff changeset
  1266
  assume "\<not>0 < x" hence "x \<le> 0" by simp
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
  1267
  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1::'a"] by auto