418 fix i j k m n u :: nat 
418 fix i j k m n u :: nat 
419 { 
419 { 
420 assume "4*k = u" have "k + 3*k = u" 
420 assume "4*k = u" have "k + 3*k = u" 
421 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
421 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
422 next 
422 next 

423 (* FIXME "Suc (i + 3) \<equiv> i + 4" *) 
423 assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" 
424 assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" 
424 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
425 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
425 next 
426 next 

427 (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *) 
426 assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" 
428 assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u" 
427 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
429 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
428 next 
430 next 
429 assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" 
431 assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u" 
430 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
432 by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact 
710 assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)" 
712 assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)" 
711 by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact 
713 by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact 
712 } 
714 } 
713 end 
715 end 
714 
716 
715 end 
717 subsection {* Integer numeral div/mod simprocs *} 

718 

719 notepad begin 

720 have "(10::int) div 3 = 3" 

721 by (tactic {* test [@{simproc binary_int_div}] *}) 

722 have "(10::int) mod 3 = 1" 

723 by (tactic {* test [@{simproc binary_int_mod}] *}) 

724 have "(10::int) div 3 = 4" 

725 by (tactic {* test [@{simproc binary_int_div}] *}) 

726 have "(10::int) mod 3 = 2" 

727 by (tactic {* test [@{simproc binary_int_mod}] *}) 

728 have "(10::int) div 3 = 4" 

729 by (tactic {* test [@{simproc binary_int_div}] *}) 

730 have "(10::int) mod 3 = 2" 

731 by (tactic {* test [@{simproc binary_int_mod}] *}) 

732 have "(10::int) div 3 = 3" 

733 by (tactic {* test [@{simproc binary_int_div}] *}) 

734 have "(10::int) mod 3 = 1" 

735 by (tactic {* test [@{simproc binary_int_mod}] *}) 

736 have "(8452::int) mod 3 = 1" 

737 by (tactic {* test [@{simproc binary_int_mod}] *}) 

738 have "(59485::int) div 434 = 137" 

739 by (tactic {* test [@{simproc binary_int_div}] *}) 

740 have "(1000006::int) mod 10 = 6" 

741 by (tactic {* test [@{simproc binary_int_mod}] *}) 

742 have "10000000 div 2 = (5000000::int)" 

743 by (tactic {* test [@{simproc binary_int_div}] *}) 

744 have "10000001 mod 2 = (1::int)" 

745 by (tactic {* test [@{simproc binary_int_mod}] *}) 

746 have "10000055 div 32 = (312501::int)" 

747 by (tactic {* test [@{simproc binary_int_div}] *}) 

748 have "10000055 mod 32 = (23::int)" 

749 by (tactic {* test [@{simproc binary_int_mod}] *}) 

750 have "100094 div 144 = (695::int)" 

751 by (tactic {* test [@{simproc binary_int_div}] *}) 

752 have "100094 mod 144 = (14::int)" 

753 by (tactic {* test [@{simproc binary_int_mod}] *}) 

754 end 

755 

756 end 