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