src/HOL/ex/Simproc_Tests.thy
changeset 45530 0c4853bb77bf
parent 45464 5a5a6e6c6789
child 46240 933f35c4e126
equal deleted inserted replaced
45529:0e1037d4e049 45530:0c4853bb77bf
   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