equal
deleted
inserted
replaced
1368 if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>numeral\<close>)) |
1368 if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>numeral\<close>)) |
1369 then raise CTERM ("number_of", []) |
1369 then raise CTERM ("number_of", []) |
1370 else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; |
1370 else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; |
1371 in |
1371 in |
1372 K ( |
1372 K ( |
1373 Lin_Arith.add_simps |
1373 Lin_Arith.set_number_of number_of |
|
1374 #> Lin_Arith.add_simps |
1374 @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps |
1375 @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps |
1375 arith_special numeral_One of_nat_simps uminus_numeral_One} |
1376 arith_special numeral_One of_nat_simps uminus_numeral_One |
1376 #> Lin_Arith.add_simps |
1377 Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1 |
1377 @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1 |
|
1378 le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc |
1378 le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc |
1379 Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral} |
1379 Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}) |
1380 #> Lin_Arith.set_number_of number_of) |
|
1381 end |
1380 end |
1382 \<close> |
1381 \<close> |
1383 |
1382 |
1384 |
1383 |
1385 subsubsection \<open>Simplification of arithmetic when nested to the right\<close> |
1384 subsubsection \<open>Simplification of arithmetic when nested to the right\<close> |