715
|
1 |
|
|
2 |
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
|
|
3 |
|
|
4 |
theory LarryInt
|
790
|
5 |
imports Nat "../QuotMain" "../QuotProd"
|
715
|
6 |
begin
|
|
7 |
|
|
8 |
fun
|
|
9 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
|
|
10 |
where
|
|
11 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
|
12 |
|
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
quotient_type int = "nat \<times> nat" / intrel
|
715
|
14 |
by (auto simp add: equivp_def expand_fun_eq)
|
|
15 |
|
|
16 |
instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
|
|
17 |
begin
|
|
18 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
quotient_definition
|
715
|
20 |
Zero_int_def: "0::int" as "(0::nat, 0::nat)"
|
|
21 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
quotient_definition
|
715
|
23 |
One_int_def: "1::int" as "(1::nat, 0::nat)"
|
|
24 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
25 |
definition
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
26 |
"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
27 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
quotient_definition
|
715
|
29 |
"(op +) :: int \<Rightarrow> int \<Rightarrow> int"
|
|
30 |
as
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
31 |
"add_raw"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
32 |
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
33 |
definition
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
34 |
"uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
|
715
|
35 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
quotient_definition
|
715
|
37 |
"uminus :: int \<Rightarrow> int"
|
|
38 |
as
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
39 |
"uminus_raw"
|
715
|
40 |
|
|
41 |
fun
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
42 |
mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
|
715
|
43 |
where
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
44 |
"mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
|
715
|
45 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
quotient_definition
|
715
|
47 |
"(op *) :: int \<Rightarrow> int \<Rightarrow> int"
|
|
48 |
as
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
49 |
"mult_raw"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
50 |
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
51 |
definition
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
52 |
"le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
|
715
|
53 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
quotient_definition
|
715
|
55 |
le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
|
|
56 |
as
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
57 |
"le_raw"
|
715
|
58 |
|
|
59 |
definition
|
|
60 |
less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
|
|
61 |
|
|
62 |
definition
|
|
63 |
diff_int_def: "z - (w::int) \<equiv> z + (-w)"
|
|
64 |
|
|
65 |
instance ..
|
|
66 |
|
|
67 |
end
|
|
68 |
|
|
69 |
subsection{*Construction of the Integers*}
|
|
70 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
lemma zminus_zminus_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
72 |
"uminus_raw (uminus_raw z) = z"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
73 |
by (cases z) (simp add: uminus_raw_def)
|
715
|
74 |
|
|
75 |
lemma [quot_respect]:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
76 |
shows "(intrel ===> intrel) uminus_raw uminus_raw"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
77 |
by (simp add: uminus_raw_def)
|
715
|
78 |
|
804
|
79 |
lemma zminus_zminus:
|
|
80 |
fixes z::"int"
|
|
81 |
shows "- (- z) = z"
|
|
82 |
by(lifting zminus_zminus_raw)
|
715
|
83 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
84 |
lemma zminus_0_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
85 |
shows "uminus_raw (0, 0) = (0, 0::nat)"
|
804
|
86 |
by (simp add: uminus_raw_def)
|
715
|
87 |
|
804
|
88 |
lemma zminus_0:
|
|
89 |
shows "- 0 = (0::int)"
|
|
90 |
by (lifting zminus_0_raw)
|
715
|
91 |
|
|
92 |
subsection{*Integer Addition*}
|
|
93 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
94 |
lemma zminus_zadd_distrib_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
95 |
shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
|
715
|
96 |
by (cases z, cases w)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
97 |
(auto simp add: add_raw_def uminus_raw_def)
|
715
|
98 |
|
|
99 |
lemma [quot_respect]:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
100 |
shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
101 |
by (simp add: add_raw_def)
|
715
|
102 |
|
|
103 |
lemma zminus_zadd_distrib:
|
804
|
104 |
fixes z w::"int"
|
|
105 |
shows "- (z + w) = (- z) + (- w)"
|
|
106 |
by(lifting zminus_zadd_distrib_raw)
|
715
|
107 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
108 |
lemma zadd_commute_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
109 |
shows "add_raw z w = add_raw w z"
|
715
|
110 |
by (cases z, cases w)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
111 |
(simp add: add_raw_def)
|
715
|
112 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
113 |
lemma zadd_commute:
|
804
|
114 |
fixes z w::"int"
|
715
|
115 |
shows "(z::int) + w = w + z"
|
804
|
116 |
by (lifting zadd_commute_raw)
|
715
|
117 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
118 |
lemma zadd_assoc_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
119 |
shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
|
804
|
120 |
by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
|
715
|
121 |
|
804
|
122 |
lemma zadd_assoc:
|
|
123 |
fixes z1 z2 z3::"int"
|
|
124 |
shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
|
|
125 |
by (lifting zadd_assoc_raw)
|
715
|
126 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
127 |
lemma zadd_0_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
128 |
shows "add_raw (0, 0) z = z"
|
804
|
129 |
by (simp add: add_raw_def)
|
715
|
130 |
|
|
131 |
|
804
|
132 |
text {*also for the instance declaration int :: plus_ac0*}
|
|
133 |
lemma zadd_0:
|
|
134 |
fixes z::"int"
|
|
135 |
shows "0 + z = z"
|
|
136 |
by (lifting zadd_0_raw)
|
715
|
137 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
138 |
lemma zadd_zminus_inverse_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
139 |
shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
|
804
|
140 |
by (cases z) (simp add: add_raw_def uminus_raw_def)
|
715
|
141 |
|
804
|
142 |
lemma zadd_zminus_inverse2:
|
|
143 |
fixes z::"int"
|
|
144 |
shows "(- z) + z = 0"
|
|
145 |
by (lifting zadd_zminus_inverse_raw)
|
715
|
146 |
|
|
147 |
subsection{*Integer Multiplication*}
|
|
148 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
149 |
lemma zmult_zminus_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
150 |
shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
|
715
|
151 |
apply(cases z, cases w)
|
804
|
152 |
apply(simp add: uminus_raw_def)
|
715
|
153 |
done
|
|
154 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
155 |
lemma mult_raw_fst:
|
715
|
156 |
assumes a: "intrel x z"
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
157 |
shows "intrel (mult_raw x y) (mult_raw z y)"
|
715
|
158 |
using a
|
|
159 |
apply(cases x, cases y, cases z)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
160 |
apply(auto simp add: mult_raw.simps intrel.simps)
|
715
|
161 |
apply(rename_tac u v w x y z)
|
|
162 |
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
|
|
163 |
apply(simp add: mult_ac)
|
|
164 |
apply(simp add: add_mult_distrib [symmetric])
|
|
165 |
done
|
|
166 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
167 |
lemma mult_raw_snd:
|
715
|
168 |
assumes a: "intrel x z"
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
169 |
shows "intrel (mult_raw y x) (mult_raw y z)"
|
715
|
170 |
using a
|
|
171 |
apply(cases x, cases y, cases z)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
172 |
apply(auto simp add: mult_raw.simps intrel.simps)
|
715
|
173 |
apply(rename_tac u v w x y z)
|
|
174 |
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
|
|
175 |
apply(simp add: mult_ac)
|
|
176 |
apply(simp add: add_mult_distrib [symmetric])
|
|
177 |
done
|
|
178 |
|
|
179 |
lemma [quot_respect]:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
|
715
|
181 |
apply(simp only: fun_rel.simps)
|
|
182 |
apply(rule allI | rule impI)+
|
|
183 |
apply(rule equivp_transp[OF int_equivp])
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
184 |
apply(rule mult_raw_fst)
|
715
|
185 |
apply(assumption)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
186 |
apply(rule mult_raw_snd)
|
715
|
187 |
apply(assumption)
|
|
188 |
done
|
|
189 |
|
804
|
190 |
lemma zmult_zminus:
|
|
191 |
fixes z w::"int"
|
|
192 |
shows "(- z) * w = - (z * w)"
|
|
193 |
by (lifting zmult_zminus_raw)
|
715
|
194 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
195 |
lemma zmult_commute_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
196 |
shows "mult_raw z w = mult_raw w z"
|
715
|
197 |
apply(cases z, cases w)
|
|
198 |
apply(simp add: add_ac mult_ac)
|
|
199 |
done
|
|
200 |
|
804
|
201 |
lemma zmult_commute:
|
|
202 |
fixes z w::"int"
|
|
203 |
shows "z * w = w * z"
|
|
204 |
by (lifting zmult_commute_raw)
|
715
|
205 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
206 |
lemma zmult_assoc_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
207 |
shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
|
715
|
208 |
apply(cases z1, cases z2, cases z3)
|
|
209 |
apply(simp add: add_mult_distrib2 mult_ac)
|
|
210 |
done
|
|
211 |
|
804
|
212 |
lemma zmult_assoc:
|
|
213 |
fixes z1 z2 z3::"int"
|
|
214 |
shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
|
|
215 |
by (lifting zmult_assoc_raw)
|
715
|
216 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
217 |
lemma zadd_mult_distrib_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
218 |
shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
|
715
|
219 |
apply(cases z1, cases z2, cases w)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
220 |
apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
|
715
|
221 |
done
|
|
222 |
|
804
|
223 |
lemma zadd_zmult_distrib:
|
|
224 |
fixes z1 z2 w::"int"
|
|
225 |
shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
|
|
226 |
by(lifting zadd_mult_distrib_raw)
|
|
227 |
|
|
228 |
lemma zadd_zmult_distrib2:
|
|
229 |
fixes w z1 z2::"int"
|
|
230 |
shows "w * (z1 + z2) = (w * z1) + (w * z2)"
|
|
231 |
by (simp add: zmult_commute [of w] zadd_zmult_distrib)
|
715
|
232 |
|
804
|
233 |
lemma zdiff_zmult_distrib:
|
|
234 |
fixes w z1 z2::"int"
|
|
235 |
shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
|
|
236 |
by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
|
715
|
237 |
|
804
|
238 |
lemma zdiff_zmult_distrib2:
|
|
239 |
fixes w z1 z2::"int"
|
|
240 |
shows "w * (z1 - z2) = (w * z1) - (w * z2)"
|
|
241 |
by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
|
715
|
242 |
|
|
243 |
lemmas int_distrib =
|
|
244 |
zadd_zmult_distrib zadd_zmult_distrib2
|
|
245 |
zdiff_zmult_distrib zdiff_zmult_distrib2
|
|
246 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
247 |
lemma zmult_1_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
248 |
shows "mult_raw (1, 0) z = z"
|
804
|
249 |
by (cases z) (auto)
|
715
|
250 |
|
804
|
251 |
lemma zmult_1:
|
|
252 |
fixes z::"int"
|
|
253 |
shows "1 * z = z"
|
|
254 |
by (lifting zmult_1_raw)
|
715
|
255 |
|
804
|
256 |
lemma zmult_1_right:
|
|
257 |
fixes z::"int"
|
|
258 |
shows "z * 1 = z"
|
|
259 |
by (rule trans [OF zmult_commute zmult_1])
|
715
|
260 |
|
|
261 |
lemma zero_not_one:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
262 |
shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
|
804
|
263 |
by auto
|
715
|
264 |
|
|
265 |
text{*The Integers Form A Ring*}
|
|
266 |
instance int :: comm_ring_1
|
|
267 |
proof
|
|
268 |
fix i j k :: int
|
|
269 |
show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
|
|
270 |
show "i + j = j + i" by (simp add: zadd_commute)
|
|
271 |
show "0 + i = i" by (rule zadd_0)
|
|
272 |
show "- i + i = 0" by (rule zadd_zminus_inverse2)
|
|
273 |
show "i - j = i + (-j)" by (simp add: diff_int_def)
|
|
274 |
show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
|
|
275 |
show "i * j = j * i" by (rule zmult_commute)
|
|
276 |
show "1 * i = i" by (rule zmult_1)
|
|
277 |
show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
278 |
show "0 \<noteq> (1::int)" by (lifting zero_not_one)
|
715
|
279 |
qed
|
|
280 |
|
|
281 |
|
|
282 |
subsection{*The @{text "\<le>"} Ordering*}
|
|
283 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
284 |
lemma zle_refl_raw:
|
804
|
285 |
shows "le_raw w w"
|
|
286 |
by (cases w) (simp add: le_raw_def)
|
715
|
287 |
|
|
288 |
lemma [quot_respect]:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
289 |
shows "(intrel ===> intrel ===> op =) le_raw le_raw"
|
804
|
290 |
by (auto) (simp_all add: le_raw_def)
|
715
|
291 |
|
804
|
292 |
lemma zle_refl:
|
|
293 |
fixes w::"int"
|
|
294 |
shows "w \<le> w"
|
|
295 |
by (lifting zle_refl_raw)
|
|
296 |
|
715
|
297 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
298 |
lemma zle_trans_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
299 |
shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
|
715
|
300 |
apply(cases i, cases j, cases k)
|
804
|
301 |
apply(auto simp add: le_raw_def)
|
715
|
302 |
done
|
|
303 |
|
804
|
304 |
lemma zle_trans:
|
|
305 |
fixes i j k::"int"
|
|
306 |
shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
|
|
307 |
by (lifting zle_trans_raw)
|
715
|
308 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
309 |
lemma zle_anti_sym_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
310 |
shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
|
715
|
311 |
apply(cases z, cases w)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
312 |
apply(auto iff: le_raw_def)
|
715
|
313 |
done
|
|
314 |
|
804
|
315 |
lemma zle_anti_sym:
|
|
316 |
fixes z w::"int"
|
|
317 |
shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
|
|
318 |
by (lifting zle_anti_sym_raw)
|
|
319 |
|
715
|
320 |
|
|
321 |
(* Axiom 'order_less_le' of class 'order': *)
|
804
|
322 |
lemma zless_le:
|
|
323 |
fixes w z::"int"
|
|
324 |
shows "(w < z) = (w \<le> z & w \<noteq> z)"
|
|
325 |
by (simp add: less_int_def)
|
715
|
326 |
|
|
327 |
instance int :: order
|
804
|
328 |
apply (default)
|
|
329 |
apply(auto simp add: zless_le zle_anti_sym)[1]
|
|
330 |
apply(rule zle_refl)
|
|
331 |
apply(erule zle_trans, assumption)
|
|
332 |
apply(erule zle_anti_sym, assumption)
|
715
|
333 |
done
|
|
334 |
|
|
335 |
(* Axiom 'linorder_linear' of class 'linorder': *)
|
|
336 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
337 |
lemma zle_linear_raw:
|
804
|
338 |
shows "le_raw z w \<or> le_raw w z"
|
715
|
339 |
apply(cases w, cases z)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
340 |
apply(auto iff: le_raw_def)
|
715
|
341 |
done
|
|
342 |
|
804
|
343 |
lemma zle_linear:
|
|
344 |
fixes z w::"int"
|
|
345 |
shows "z \<le> w \<or> w \<le> z"
|
|
346 |
by (lifting zle_linear_raw)
|
715
|
347 |
|
|
348 |
instance int :: linorder
|
804
|
349 |
apply(default)
|
|
350 |
apply(rule zle_linear)
|
|
351 |
done
|
715
|
352 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
353 |
lemma zadd_left_mono_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
354 |
shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
|
715
|
355 |
apply(cases k)
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
356 |
apply(auto simp add: add_raw_def le_raw_def)
|
715
|
357 |
done
|
|
358 |
|
804
|
359 |
lemma zadd_left_mono:
|
|
360 |
fixes i j::"int"
|
|
361 |
shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
|
|
362 |
by (lifting zadd_left_mono_raw)
|
715
|
363 |
|
|
364 |
|
|
365 |
subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
|
|
366 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
367 |
definition
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
368 |
"nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
|
715
|
369 |
|
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
370 |
quotient_definition
|
804
|
371 |
"nat2::int \<Rightarrow> nat"
|
715
|
372 |
as
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
373 |
"nat_raw"
|
715
|
374 |
|
|
375 |
abbreviation
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
376 |
"less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"
|
715
|
377 |
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
378 |
lemma nat_le_eq_zle_raw:
|
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
379 |
shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
|
715
|
380 |
apply(auto)
|
|
381 |
sorry
|
|
382 |
|
|
383 |
lemma [quot_respect]:
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
384 |
shows "(intrel ===> op =) nat_raw nat_raw"
|
804
|
385 |
by (auto iff: nat_raw_def)
|
715
|
386 |
|
804
|
387 |
lemma nat_le_eq_zle:
|
|
388 |
fixes w z::"int"
|
|
389 |
shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
|
|
390 |
unfolding less_int_def
|
|
391 |
by (lifting nat_le_eq_zle_raw)
|
715
|
392 |
|
|
393 |
end
|