116 by auto |
116 by auto |
117 |
117 |
118 lemma mult_raw_rsp[quotient_rsp]: |
118 lemma mult_raw_rsp[quotient_rsp]: |
119 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
119 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
120 apply(auto) |
120 apply(auto) |
121 apply(simp add: mult algebra_simps) |
121 apply(simp add: algebra_simps) |
122 sorry |
122 sorry |
123 |
123 |
124 lemma le_raw_rsp[quotient_rsp]: |
124 lemma le_raw_rsp[quotient_rsp]: |
125 shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw" |
125 shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw" |
126 by auto |
126 by auto |
142 by (cases i) (simp) |
142 by (cases i) (simp) |
143 |
143 |
144 lemma mult_assoc_raw: |
144 lemma mult_assoc_raw: |
145 shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)" |
145 shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)" |
146 by (cases i, cases j, cases k) |
146 by (cases i, cases j, cases k) |
147 (simp add: mult algebra_simps) |
147 (simp add: algebra_simps) |
148 |
148 |
149 lemma mult_sym_raw: |
149 lemma mult_sym_raw: |
150 shows "mult_raw i j \<approx> mult_raw j i" |
150 shows "mult_raw i j \<approx> mult_raw j i" |
151 by (cases i, cases j) (simp) |
151 by (cases i, cases j) (simp add: algebra_simps) |
152 |
152 |
153 lemma mult_one_raw: |
153 lemma mult_one_raw: |
154 shows "mult_raw (1, 0) i \<approx> i" |
154 shows "mult_raw (1, 0) i \<approx> i" |
155 by (cases i) (simp) |
155 by (cases i) (simp) |
156 |
156 |
157 lemma mult_plus_comm_raw: |
157 lemma mult_plus_comm_raw: |
158 shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)" |
158 shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)" |
159 by (cases i, cases j, cases k) |
159 by (cases i, cases j, cases k) |
160 (simp add: mult algebra_simps) |
160 (simp add: algebra_simps) |
161 |
161 |
162 lemma one_zero_distinct: |
162 lemma one_zero_distinct: |
163 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
163 shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))" |
164 by simp |
164 by simp |
165 |
165 |
295 |
295 |
296 lemma test: |
296 lemma test: |
297 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
297 "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk> |
298 \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j" |
298 \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j" |
299 apply(cases i, cases j, cases k) |
299 apply(cases i, cases j, cases k) |
300 apply(auto simp add: mult algebra_simps) |
300 apply(auto simp add: algebra_simps) |
301 sorry |
301 sorry |
302 |
302 |
303 |
303 |
304 text{*The integers form an ordered integral domain*} |
304 text{*The integers form an ordered integral domain*} |
305 instance int :: ordered_idom |
305 instance int :: ordered_idom |
381 [code del]: "Bit1 k = 1 + k + k" |
381 [code del]: "Bit1 k = 1 + k + k" |
382 |
382 |
383 class number = -- {* for numeric types: nat, int, real, \dots *} |
383 class number = -- {* for numeric types: nat, int, real, \dots *} |
384 fixes number_of :: "int \<Rightarrow> 'a" |
384 fixes number_of :: "int \<Rightarrow> 'a" |
385 |
385 |
386 use "~~/src/HOL/Tools/numeral.ML" |
386 (*use "~~/src/HOL/Tools/numeral.ML" |
387 |
387 |
388 syntax |
388 syntax |
389 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") |
389 "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") |
390 |
390 |
391 use "~~/src/HOL/Tools/numeral_syntax.ML" |
391 use "~~/src/HOL/Tools/numeral_syntax.ML" |
392 (* |
392 |
393 setup NumeralSyntax.setup |
393 setup NumeralSyntax.setup |
394 |
394 |
395 abbreviation |
395 abbreviation |
396 "Numeral0 \<equiv> number_of Pls" |
396 "Numeral0 \<equiv> number_of Pls" |
397 |
397 |