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