909 thm numeral |
909 thm numeral |
910 |
910 |
911 |
911 |
912 subsection {* Simplification Procedures *} |
912 subsection {* Simplification Procedures *} |
913 |
913 |
914 text {* Reorientation of equalities *} |
914 subsubsection {* Reorientation of equalities *} |
915 |
915 |
916 setup {* |
916 setup {* |
917 ReorientProc.add |
917 ReorientProc.add |
918 (fn Const(@{const_name of_num}, _) $ _ => true |
918 (fn Const(@{const_name of_num}, _) $ _ => true |
919 | Const(@{const_name uminus}, _) $ |
919 | Const(@{const_name uminus}, _) $ |
921 | _ => false) |
921 | _ => false) |
922 *} |
922 *} |
923 |
923 |
924 simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc |
924 simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc |
925 |
925 |
|
926 subsubsection {* Constant folding for multiplication in semirings *} |
|
927 |
|
928 context semiring_numeral |
|
929 begin |
|
930 |
|
931 lemma mult_of_num_commute: "x * of_num n = of_num n * x" |
|
932 by (induct n) |
|
933 (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right) |
|
934 |
|
935 definition |
|
936 "commutes_with a b \<longleftrightarrow> a * b = b * a" |
|
937 |
|
938 lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a" |
|
939 unfolding commutes_with_def . |
|
940 |
|
941 lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)" |
|
942 unfolding commutes_with_def by (simp only: mult_assoc [symmetric]) |
|
943 |
|
944 lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x" |
|
945 unfolding commutes_with_def by (simp_all add: mult_of_num_commute) |
|
946 |
|
947 lemmas mult_ac_numeral = |
|
948 mult_assoc |
|
949 commutes_with_commute |
|
950 commutes_with_left_commute |
|
951 commutes_with_numeral |
|
952 |
|
953 end |
|
954 |
|
955 ML {* |
|
956 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = |
|
957 struct |
|
958 val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral} |
|
959 val eq_reflection = eq_reflection |
|
960 fun is_numeral (Const(@{const_name of_num}, _) $ _) = true |
|
961 | is_numeral _ = false; |
|
962 end; |
|
963 |
|
964 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); |
|
965 *} |
|
966 |
|
967 simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") = |
|
968 {* fn phi => fn ss => fn ct => |
|
969 Semiring_Times_Assoc.proc ss (Thm.term_of ct) *} |
|
970 |
926 |
971 |
927 subsection {* Toy examples *} |
972 subsection {* Toy examples *} |
928 |
973 |
929 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
974 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3" |
930 code_thms bar |
975 code_thms bar |