src/HOL/Quotient_Examples/Quotient_Rat.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa
permissions -rw-r--r--
more fundamental definition of div and mod on int
kaliszyk@45815
     1
(*  Title:      HOL/Quotient_Examples/Quotient_Rat.thy
kaliszyk@45815
     2
    Author:     Cezary Kaliszyk
kaliszyk@45815
     3
kaliszyk@45815
     4
Rational numbers defined with the quotient package, based on 'HOL/Rat.thy' by Makarius.
kaliszyk@45815
     5
*)
kaliszyk@45815
     6
wenzelm@66453
     7
theory Quotient_Rat imports HOL.Archimedean_Field
wenzelm@66453
     8
  "HOL-Library.Quotient_Product"
kaliszyk@45815
     9
begin
kaliszyk@45815
    10
kaliszyk@45815
    11
definition
kaliszyk@45815
    12
  ratrel :: "(int \<times> int) \<Rightarrow> (int \<times> int) \<Rightarrow> bool" (infix "\<approx>" 50)
kaliszyk@45815
    13
where
kaliszyk@45815
    14
  [simp]: "x \<approx> y \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
kaliszyk@45815
    15
kaliszyk@45815
    16
lemma ratrel_equivp:
kaliszyk@45815
    17
  "part_equivp ratrel"
kaliszyk@45815
    18
proof (auto intro!: part_equivpI reflpI sympI transpI exI[of _ "1 :: int"])
kaliszyk@45815
    19
  fix a b c d e f :: int
kaliszyk@45815
    20
  assume nz: "d \<noteq> 0" "b \<noteq> 0"
kaliszyk@45815
    21
  assume y: "a * d = c * b"
kaliszyk@45815
    22
  assume x: "c * f = e * d"
kaliszyk@45815
    23
  then have "c * b * f = e * d * b" using nz by simp
kaliszyk@45815
    24
  then have "a * d * f = e * d * b" using y by simp
kaliszyk@45815
    25
  then show "a * f = e * b" using nz by simp
kaliszyk@45815
    26
qed
kaliszyk@45815
    27
kaliszyk@45815
    28
quotient_type rat = "int \<times> int" / partial: ratrel
kaliszyk@45815
    29
 using ratrel_equivp .
kaliszyk@45815
    30
haftmann@64290
    31
instantiation rat :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
kaliszyk@45815
    32
begin
kaliszyk@45815
    33
kaliszyk@45815
    34
quotient_definition
wenzelm@61076
    35
  "0 :: rat" is "(0::int, 1::int)" by simp
kaliszyk@45815
    36
kaliszyk@45815
    37
quotient_definition
wenzelm@61076
    38
  "1 :: rat" is "(1::int, 1::int)" by simp
kaliszyk@45815
    39
kaliszyk@45815
    40
fun times_rat_raw where
kaliszyk@45815
    41
  "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
kaliszyk@45815
    42
kaliszyk@45815
    43
quotient_definition
haftmann@57512
    44
  "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute)
kaliszyk@45815
    45
kaliszyk@45815
    46
fun plus_rat_raw where
kaliszyk@45815
    47
  "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
kaliszyk@45815
    48
kaliszyk@45815
    49
quotient_definition
kuncar@47092
    50
  "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw 
haftmann@57512
    51
  by (auto simp add: mult.commute mult.left_commute int_distrib(2))
kaliszyk@45815
    52
kaliszyk@45815
    53
fun uminus_rat_raw where
kaliszyk@45815
    54
  "uminus_rat_raw (a :: int, b :: int) = (-a, b)"
kaliszyk@45815
    55
kaliszyk@45815
    56
quotient_definition
wenzelm@61076
    57
  "(uminus :: (rat \<Rightarrow> rat))" is "uminus_rat_raw" by fastforce
kaliszyk@45815
    58
kaliszyk@45815
    59
definition
wenzelm@61076
    60
  minus_rat_def: "a - b = a + (-b::rat)"
kaliszyk@45815
    61
kaliszyk@45815
    62
fun le_rat_raw where
kaliszyk@45815
    63
  "le_rat_raw (a :: int, b) (c, d) \<longleftrightarrow> (a * d) * (b * d) \<le> (c * b) * (b * d)"
kaliszyk@45815
    64
kaliszyk@45815
    65
quotient_definition
kaliszyk@45815
    66
  "(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
kuncar@47092
    67
proof -
kuncar@47092
    68
  {
kuncar@47092
    69
    fix a b c d e f g h :: int
kuncar@47092
    70
    assume "a * f * (b * f) \<le> e * b * (b * f)"
kuncar@47092
    71
    then have le: "a * f * b * f \<le> e * b * b * f" by simp
kuncar@47092
    72
    assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
kuncar@47092
    73
    then have b2: "b * b > 0"
kuncar@47092
    74
      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
kuncar@47092
    75
    have f2: "f * f > 0" using nz(3)
kuncar@47092
    76
      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
kuncar@47092
    77
    assume eq: "a * d = c * b" "e * h = g * f"
kuncar@47092
    78
    have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
kuncar@47092
    79
      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
kuncar@47092
    80
    then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
haftmann@57512
    81
      by (metis (no_types) mult.assoc mult.commute)
kuncar@47092
    82
    then have "c * f * f * d \<le> e * f * d * d" using b2
kuncar@47092
    83
      by (metis leD linorder_le_less_linear mult_strict_right_mono)
kuncar@47092
    84
    then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
kuncar@47092
    85
      by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
kuncar@47092
    86
    then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
haftmann@57512
    87
      by (metis (no_types) mult.assoc mult.commute)
kuncar@47092
    88
    then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
kuncar@47092
    89
      by (metis leD linorder_le_less_linear mult_strict_right_mono)
kuncar@47092
    90
  }
kuncar@47092
    91
  then show "\<And>x y xa ya. x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> le_rat_raw x xa = le_rat_raw y ya" by auto
kuncar@47092
    92
qed
kaliszyk@45815
    93
kaliszyk@45815
    94
definition
wenzelm@61076
    95
  less_rat_def: "(z::rat) < w = (z \<le> w \<and> z \<noteq> w)"
kaliszyk@45815
    96
kaliszyk@45815
    97
definition
wenzelm@61076
    98
  rabs_rat_def: "\<bar>i::rat\<bar> = (if i < 0 then - i else i)"
kaliszyk@45815
    99
kaliszyk@45815
   100
definition
wenzelm@61076
   101
  sgn_rat_def: "sgn (i::rat) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
kaliszyk@45815
   102
haftmann@64290
   103
instance ..
kaliszyk@45815
   104
kaliszyk@45815
   105
end
kaliszyk@45815
   106
kaliszyk@45815
   107
definition
kaliszyk@45815
   108
  Fract_raw :: "int \<Rightarrow> int \<Rightarrow> (int \<times> int)"
kaliszyk@45815
   109
where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
kaliszyk@45815
   110
kaliszyk@45815
   111
quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
kuncar@47092
   112
  Fract_raw by simp
kaliszyk@45815
   113
kaliszyk@45815
   114
lemmas [simp] = Respects_def
kaliszyk@45815
   115
huffman@48047
   116
(* FIXME: (partiality_)descending raises exception TYPE_MATCH
huffman@48047
   117
kaliszyk@45815
   118
instantiation rat :: comm_ring_1
kaliszyk@45815
   119
begin
kaliszyk@45815
   120
kaliszyk@45815
   121
instance proof
kaliszyk@45815
   122
  fix a b c :: rat
kaliszyk@45815
   123
  show "a * b * c = a * (b * c)"
kaliszyk@45815
   124
    by partiality_descending auto
kaliszyk@45815
   125
  show "a * b = b * a"
kaliszyk@45815
   126
    by partiality_descending auto
kaliszyk@45815
   127
  show "1 * a = a"
kaliszyk@45815
   128
    by partiality_descending auto
kaliszyk@45815
   129
  show "a + b + c = a + (b + c)"
haftmann@57512
   130
    by partiality_descending (auto simp add: mult.commute distrib_left)
kaliszyk@45815
   131
  show "a + b = b + a"
kaliszyk@45815
   132
    by partiality_descending auto
kaliszyk@45815
   133
  show "0 + a = a"
kaliszyk@45815
   134
    by partiality_descending auto
kaliszyk@45815
   135
  show "- a + a = 0"
kaliszyk@45815
   136
    by partiality_descending auto
kaliszyk@45815
   137
  show "a - b = a + - b"
kaliszyk@45815
   138
    by (simp add: minus_rat_def)
kaliszyk@45815
   139
  show "(a + b) * c = a * c + b * c"
haftmann@57512
   140
    by partiality_descending (auto simp add: mult.commute distrib_left)
kaliszyk@45815
   141
  show "(0 :: rat) \<noteq> (1 :: rat)"
kaliszyk@45815
   142
    by partiality_descending auto
kaliszyk@45815
   143
qed
kaliszyk@45815
   144
kaliszyk@45815
   145
end
kaliszyk@45815
   146
kaliszyk@45815
   147
lemma add_one_Fract: "1 + Fract (int k) 1 = Fract (1 + int k) 1"
kaliszyk@45815
   148
  by descending auto
kaliszyk@45815
   149
kaliszyk@45815
   150
lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
kaliszyk@45815
   151
  apply (induct k)
kaliszyk@45815
   152
  apply (simp add: zero_rat_def Fract_def)
kaliszyk@45815
   153
  apply (simp add: add_one_Fract)
kaliszyk@45815
   154
  done
kaliszyk@45815
   155
kaliszyk@45815
   156
lemma of_int_rat: "of_int k = Fract k 1"
kaliszyk@45815
   157
  apply (cases k rule: int_diff_cases)
kaliszyk@45815
   158
  apply (auto simp add: of_nat_rat minus_rat_def)
kaliszyk@45815
   159
  apply descending
kaliszyk@45815
   160
  apply auto
kaliszyk@45815
   161
  done
kaliszyk@45815
   162
haftmann@59867
   163
instantiation rat :: field begin
kaliszyk@45815
   164
kaliszyk@45815
   165
fun rat_inverse_raw where
kaliszyk@45815
   166
  "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
kaliszyk@45815
   167
kaliszyk@45815
   168
quotient_definition
haftmann@57512
   169
  "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw by (force simp add: mult.commute)
kaliszyk@45815
   170
kaliszyk@45815
   171
definition
kaliszyk@45815
   172
  divide_rat_def: "q / r = q * inverse (r::rat)"
kaliszyk@45815
   173
kaliszyk@45815
   174
instance proof
kaliszyk@45815
   175
  fix q :: rat
kaliszyk@45815
   176
  assume "q \<noteq> 0"
kaliszyk@45815
   177
  then show "inverse q * q = 1"
kaliszyk@45815
   178
    by partiality_descending auto
kaliszyk@45815
   179
next
kaliszyk@45815
   180
  fix q r :: rat
kaliszyk@45815
   181
  show "q / r = q * inverse r" by (simp add: divide_rat_def)
kaliszyk@45815
   182
next
kaliszyk@45815
   183
  show "inverse 0 = (0::rat)" by partiality_descending auto
kaliszyk@45815
   184
qed
kaliszyk@45815
   185
kaliszyk@45815
   186
end
kaliszyk@45815
   187
kaliszyk@45815
   188
instantiation rat :: linorder
kaliszyk@45815
   189
begin
kaliszyk@45815
   190
kaliszyk@45815
   191
instance proof
kaliszyk@45815
   192
  fix q r s :: rat
kaliszyk@45815
   193
  {
kaliszyk@45815
   194
    assume "q \<le> r" and "r \<le> s"
kaliszyk@45815
   195
    then show "q \<le> s"
haftmann@57512
   196
    proof (partiality_descending, auto simp add: mult.assoc[symmetric])
kaliszyk@45815
   197
      fix a b c d e f :: int
kaliszyk@45815
   198
      assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0"
kaliszyk@45815
   199
      then have d2: "d * d > 0"
kaliszyk@45815
   200
        by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
kaliszyk@45815
   201
      assume le: "a * d * b * d \<le> c * b * b * d" "c * f * d * f \<le> e * d * d * f"
kaliszyk@45815
   202
      then have a: "a * d * b * d * f * f \<le> c * b * b * d * f * f" using nz(3)
kaliszyk@45815
   203
        by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
kaliszyk@45815
   204
      have "c * f * d * f * b * b \<le> e * d * d * f * b * b" using nz(1) le
kaliszyk@45815
   205
        by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
kaliszyk@45815
   206
      then have "a * f * b * f * (d * d) \<le> e * b * b * f * (d * d)" using a
kaliszyk@45815
   207
        by (simp add: algebra_simps)
kaliszyk@45815
   208
      then show "a * f * b * f \<le> e * b * b * f" using d2
kaliszyk@45815
   209
        by (metis leD linorder_le_less_linear mult_strict_right_mono)
kaliszyk@45815
   210
    qed
kaliszyk@45815
   211
  next
kaliszyk@45815
   212
    assume "q \<le> r" and "r \<le> q"
kaliszyk@45815
   213
    then show "q = r"
kaliszyk@45815
   214
      apply (partiality_descending, auto)
kaliszyk@45815
   215
      apply (case_tac "b > 0", case_tac [!] "ba > 0")
kaliszyk@45815
   216
      apply simp_all
kaliszyk@45815
   217
      done
kaliszyk@45815
   218
  next
kaliszyk@45815
   219
    show "q \<le> q" by partiality_descending auto
kaliszyk@45815
   220
    show "(q < r) = (q \<le> r \<and> \<not> r \<le> q)"
kaliszyk@45815
   221
      unfolding less_rat_def
haftmann@57512
   222
      by partiality_descending (auto simp add: le_less mult.commute)
kaliszyk@45815
   223
    show "q \<le> r \<or> r \<le> q"
haftmann@57512
   224
      by partiality_descending (auto simp add: mult.commute linorder_linear)
kaliszyk@45815
   225
  }
kaliszyk@45815
   226
qed
kaliszyk@45815
   227
kaliszyk@45815
   228
end
kaliszyk@45815
   229
kaliszyk@45815
   230
instance rat :: archimedean_field
kaliszyk@45815
   231
proof
kaliszyk@45815
   232
  fix q r s :: rat
kaliszyk@45815
   233
  show "q \<le> r ==> s + q \<le> s + r"
haftmann@57512
   234
  proof (partiality_descending, auto simp add: algebra_simps, simp add: mult.assoc[symmetric])
kaliszyk@45815
   235
    fix a b c d e :: int
kaliszyk@45815
   236
    assume "e \<noteq> 0"
kaliszyk@45815
   237
    then have e2: "e * e > 0"
kaliszyk@45815
   238
      by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
kaliszyk@45815
   239
      assume "a * b * d * d \<le> b * b * c * d"
kaliszyk@45815
   240
      then show "a * b * d * d * e * e * e * e \<le> b * b * c * d * e * e * e * e"
haftmann@59557
   241
        using e2 by (metis mult_left_mono mult.commute linorder_le_cases
kaliszyk@45815
   242
          mult_left_mono_neg)
kaliszyk@45815
   243
    qed
kaliszyk@45815
   244
  show "q < r ==> 0 < s ==> s * q < s * r" unfolding less_rat_def
haftmann@57512
   245
    proof (partiality_descending, auto simp add: algebra_simps, simp add: mult.assoc[symmetric])
kaliszyk@45815
   246
    fix a b c d e f :: int
kaliszyk@45815
   247
    assume a: "e \<noteq> 0" "f \<noteq> 0" "0 \<le> e * f" "a * b * d * d \<le> b * b * c * d"
kaliszyk@45815
   248
    have "a * b * d * d * (e * f) \<le> b * b * c * d * (e * f)" using a
kaliszyk@45815
   249
      by (simp add: mult_right_mono)
kaliszyk@45815
   250
    then show "a * b * d * d * e * f * f * f \<le> b * b * c * d * e * f * f * f"
haftmann@59557
   251
      by (simp add: mult.assoc[symmetric]) (metis a(3) mult_left_mono
haftmann@57512
   252
        mult.commute mult_left_mono_neg zero_le_mult_iff)
kaliszyk@45815
   253
  qed
kaliszyk@45815
   254
  show "\<exists>z. r \<le> of_int z"
kaliszyk@45815
   255
    unfolding of_int_rat
kaliszyk@45815
   256
  proof (partiality_descending, auto)
kaliszyk@45815
   257
    fix a b :: int
kaliszyk@45815
   258
    assume "b \<noteq> 0"
kaliszyk@45815
   259
    then have "a * b \<le> (a div b + 1) * b * b"
haftmann@64240
   260
      by (metis mult.commute nonzero_mult_div_cancel_left less_int_def linorder_le_cases zdiv_mono1 zdiv_mono1_neg zle_add1_eq_le)
wenzelm@61076
   261
    then show "\<exists>z::int. a * b \<le> z * b * b" by auto
kaliszyk@45815
   262
  qed
kaliszyk@45815
   263
qed
huffman@48047
   264
*)
kaliszyk@45815
   265
kaliszyk@45815
   266
end