1 theory IntEx2 |
1 theory IntEx2 |
2 imports "../QuotMain" |
2 imports "../QuotMain" Nat Presburger |
3 (*uses |
3 (*uses |
4 ("Tools/numeral.ML") |
4 ("Tools/numeral.ML") |
5 ("Tools/numeral_syntax.ML") |
5 ("Tools/numeral_syntax.ML") |
6 ("Tools/int_arith.ML")*) |
6 ("Tools/int_arith.ML")*) |
7 begin |
7 begin |
8 |
8 |
9 |
|
10 fun |
9 fun |
11 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
12 where |
11 where |
13 "intrel (x, y) (u, v) = (x + v = u + y)" |
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
14 |
13 |
95 |
93 |
96 lemma minus_raw_rsp[quot_respect]: |
94 lemma minus_raw_rsp[quot_respect]: |
97 shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw" |
95 shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw" |
98 by auto |
96 by auto |
99 |
97 |
|
98 lemma times_raw_fst: |
|
99 assumes a: "x \<approx> z" |
|
100 shows "times_raw x y \<approx> times_raw z y" |
|
101 using a |
|
102 apply(cases x, cases y, cases z) |
|
103 apply(auto simp add: times_raw.simps intrel.simps) |
|
104 apply(rename_tac u v w x y z) |
|
105 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
106 apply(simp add: mult_ac) |
|
107 apply(simp add: add_mult_distrib [symmetric]) |
|
108 done |
|
109 |
|
110 lemma times_raw_snd: |
|
111 assumes a: "x \<approx> z" |
|
112 shows "times_raw y x \<approx> times_raw y z" |
|
113 using a |
|
114 apply(cases x, cases y, cases z) |
|
115 apply(auto simp add: times_raw.simps intrel.simps) |
|
116 apply(rename_tac u v w x y z) |
|
117 apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") |
|
118 apply(simp add: mult_ac) |
|
119 apply(simp add: add_mult_distrib [symmetric]) |
|
120 done |
|
121 |
100 lemma mult_raw_rsp[quot_respect]: |
122 lemma mult_raw_rsp[quot_respect]: |
101 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw" |
123 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw" |
102 apply(auto) |
124 apply(simp only: fun_rel.simps) |
103 apply(simp add: algebra_simps) |
125 apply(rule allI | rule impI)+ |
104 sorry |
126 apply(rule equivp_transp[OF int_equivp]) |
|
127 apply(rule times_raw_fst) |
|
128 apply(assumption) |
|
129 apply(rule times_raw_snd) |
|
130 apply(assumption) |
|
131 done |
105 |
132 |
106 lemma less_eq_raw_rsp[quot_respect]: |
133 lemma less_eq_raw_rsp[quot_respect]: |
107 shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw" |
134 shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw" |
108 by auto |
135 by auto |
109 |
136 |
145 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
172 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
146 by simp |
173 by simp |
147 |
174 |
148 text{*The integers form a @{text comm_ring_1}*} |
175 text{*The integers form a @{text comm_ring_1}*} |
149 |
176 |
150 print_quotconsts |
|
151 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
177 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
152 |
178 |
153 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
179 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
154 ML {* @{term "0 :: int"} *} |
180 ML {* @{term "0 :: int"} *} |
155 |
181 |
260 text{*The integers form an ordered integral domain*} |
286 text{*The integers form an ordered integral domain*} |
261 instance int :: ordered_idom |
287 instance int :: ordered_idom |
262 proof |
288 proof |
263 fix i j k :: int |
289 fix i j k :: int |
264 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
290 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
265 unfolding less_int_def |
291 unfolding less_int_def by (lifting test) |
266 by (lifting test) |
|
267 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
292 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
268 by (simp only: abs_int_def) |
293 by (simp only: abs_int_def) |
269 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
294 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
270 by (simp only: sgn_int_def) |
295 by (simp only: sgn_int_def) |
271 qed |
296 qed |