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