equal
deleted
inserted
replaced
1 theory IntEx2 |
1 theory IntEx2 |
2 imports "../QuotMain" Nat Presburger |
2 imports "../QuotMain" Nat |
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 |
87 |
87 |
88 lemma plus_raw_rsp[quot_respect]: |
88 lemma plus_raw_rsp[quot_respect]: |
89 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
89 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw" |
90 by auto |
90 by auto |
91 |
91 |
92 lemma minus_raw_rsp[quot_respect]: |
92 lemma uminus_raw_rsp[quot_respect]: |
93 shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw" |
93 shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw" |
94 by auto |
94 by auto |
95 |
95 |
96 lemma times_raw_fst: |
96 lemma times_raw_fst: |
97 assumes a: "x \<approx> z" |
97 assumes a: "x \<approx> z" |
169 lemma one_zero_distinct: |
169 lemma one_zero_distinct: |
170 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
170 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
171 by simp |
171 by simp |
172 |
172 |
173 text{* The integers form a @{text comm_ring_1}*} |
173 text{* The integers form a @{text comm_ring_1}*} |
174 |
|
175 ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *} |
|
176 ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *} |
|
177 ML {* @{term "0 :: int"} *} |
|
178 |
174 |
179 instance int :: comm_ring_1 |
175 instance int :: comm_ring_1 |
180 proof |
176 proof |
181 fix i j k :: int |
177 fix i j k :: int |
182 show "(i + j) + k = i + (j + k)" |
178 show "(i + j) + k = i + (j + k)" |