author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Mon, 12 Dec 2011 15:32:54 +0900 | |
changeset 45815 | 2b7eb46e70f9 |
child 47092 | fa3538d6004b |
permissions | -rw-r--r-- |
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 |
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
|
35 |
"0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>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
|
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 |
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
|
38 |
"1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>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
|
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 |
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
|
44 |
"(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw |
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 |
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
|
50 |
"(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw |
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
|
51 |
|
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 |
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
|
53 |
"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
|
54 |
|
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 |
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
|
56 |
"(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw" |
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
|
57 |
|
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 |
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
|
59 |
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
|
60 |
|
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 |
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
|
62 |
"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
|
63 |
|
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 |
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
|
65 |
"(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw" |
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 |
|
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
|
67 |
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
|
68 |
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
|
69 |
|
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
|
70 |
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
|
71 |
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
|
72 |
|
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
|
73 |
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
|
74 |
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
|
75 |
|
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
|
76 |
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
|
77 |
(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
|
78 |
|
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
|
79 |
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
|
80 |
|
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
|
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
|
85 |
quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is |
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
|
86 |
Fract_raw |
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
|
87 |
|
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
|
88 |
lemma [quot_respect]: |
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
|
89 |
"(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw" |
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
|
90 |
"(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw" |
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
|
91 |
"(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw" |
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
|
92 |
"(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw" |
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 |
by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2)) |
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 |
|
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 |
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
|
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 |
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
|
98 |
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
|
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 |
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
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
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
|
114 |
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
|
115 |
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
|
116 |
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
|
117 |
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
|
118 |
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
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
|
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 |
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
|
125 |
|
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 |
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
|
127 |
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
|
128 |
|
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 |
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
|
130 |
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
|
131 |
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
|
132 |
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
|
133 |
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
|
134 |
|
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 |
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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
|
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 |
instantiation rat :: number_ring |
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 |
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
|
144 |
|
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 |
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
|
146 |
rat_number_of_def: "number_of w = Fract w 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 |
|
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 |
instance apply default |
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 |
unfolding rat_number_of_def 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
|
150 |
|
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 |
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
|
152 |
|
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 |
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
|
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 |
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
|
156 |
"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
|
157 |
|
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 |
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
|
159 |
"inverse :: rat \<Rightarrow> rat" is rat_inverse_raw |
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 |
|
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 |
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
|
162 |
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
|
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 |
lemma [quot_respect]: |
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 |
"(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw" |
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 |
by (auto intro!: fun_relI simp add: 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
|
167 |
|
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
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
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
|
179 |
|
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 |
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
|
181 |
|
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 |
lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw" |
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 |
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
|
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 |
fix a b c d e f g h :: 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
|
186 |
assume "a * f * (b * f) \<le> e * b * (b * 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
|
187 |
then have le: "a * f * b * f \<le> e * b * b * f" 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
|
188 |
assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<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
|
189 |
then have b2: "b * b > 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
|
190 |
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
|
191 |
have f2: "f * f > 0" 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
|
192 |
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
|
193 |
assume eq: "a * d = c * b" "e * h = g * 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
|
194 |
have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2) |
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 |
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
|
196 |
then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq |
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 |
by (metis (no_types) mult_assoc 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
|
198 |
then have "c * f * f * d \<le> e * f * d * d" using b2 |
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 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
|
200 |
then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4) |
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 |
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
|
202 |
then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq |
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 |
by (metis (no_types) mult_assoc 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
|
204 |
then have "c * h * (d * h) \<le> g * d * (d * h)" using f2 |
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 |
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
|
206 |
} |
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 ?thesis by (auto intro!: fun_relI) |
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 |
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
|
209 |
|
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 |
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
|
211 |
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
|
212 |
|
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 |
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
|
214 |
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
|
215 |
{ |
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 |
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
|
217 |
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
|
218 |
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
|
219 |
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
|
220 |
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
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
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
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
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
|
236 |
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
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
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
|
242 |
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
|
243 |
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 |
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
|
245 |
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
|
246 |
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
|
247 |
} |
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 |
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
|
249 |
|
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 |
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
|
251 |
|
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 |
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
|
253 |
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
|
254 |
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
|
255 |
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
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
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
|
264 |
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
|
265 |
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
|
266 |
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
|
267 |
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
|
268 |
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
|
269 |
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
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
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
|
274 |
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
|
275 |
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
|
276 |
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
|
277 |
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
|
278 |
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
|
279 |
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
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
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
|
284 |
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
|
285 |
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
|
286 |
|
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
|
287 |
end |