774 |
774 |
775 lemma nat_mult_div_cancel_disj: |
775 lemma nat_mult_div_cancel_disj: |
776 "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" |
776 "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" |
777 by (simp add: nat_mult_div_cancel1) |
777 by (simp add: nat_mult_div_cancel1) |
778 |
778 |
|
779 |
779 subsection {* code generator setup *} |
780 subsection {* code generator setup *} |
780 |
781 |
781 lemma elim_nat [code inline]: |
782 lemma number_of_is_nat_rep_bin [code inline]: |
782 "(number_of n :: nat) = nat (number_of n)" |
783 "(number_of b :: nat) = nat (Rep_Bin b)" |
783 by simp |
784 unfolding nat_number_of_def int_number_of_def by simp |
784 |
785 |
785 lemma elim_zero [code inline]: |
|
786 "(0::int) = number_of (Numeral.Pls)" |
|
787 by simp |
|
788 |
|
789 lemma elim_one [code inline]: |
|
790 "(1::int) = number_of (Numeral.Pls BIT bit.B1)" |
|
791 by simp |
|
792 |
|
793 lemma elim_one_nat [code inline]: |
|
794 "1 = Suc 0" |
|
795 by simp |
|
796 |
|
797 lemmas [code inline] = |
|
798 bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0 |
|
799 bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0 |
|
800 |
|
801 lemma elim_negate: |
|
802 "(number_of n :: int) == - number_of (bin_minus n)" |
|
803 unfolding number_of_minus IntDef.zminus_zminus by (rule reflexive) |
|
804 |
|
805 ML {* |
|
806 local |
|
807 val elim_negate_thm = thm "elim_negate"; |
|
808 in fun elim_negate thy thms = |
|
809 let |
|
810 fun bins_of (Const _) = |
|
811 I |
|
812 | bins_of (Var _) = |
|
813 I |
|
814 | bins_of (Free _) = |
|
815 I |
|
816 | bins_of (Bound _) = |
|
817 I |
|
818 | bins_of (Abs (_, _, t)) = |
|
819 bins_of t |
|
820 | bins_of (t as _ $ _) = |
|
821 case strip_comb t |
|
822 of (Const ("Numeral.number_of", _), [bin]) => cons bin |
|
823 | (t', ts) => bins_of t' #> fold bins_of ts; |
|
824 fun is_negative bin = case try HOLogic.dest_binum bin |
|
825 of SOME i => i < 0 |
|
826 | _ => false; |
|
827 fun instantiate_with bin = |
|
828 Drule.instantiate' [] [(SOME o cterm_of thy) bin] elim_negate_thm; |
|
829 val rewrites = |
|
830 [] |
|
831 |> fold (bins_of o prop_of) thms |
|
832 |> filter is_negative |
|
833 |> map instantiate_with |
|
834 in |
|
835 thms |
|
836 |> map (rewrite_rule rewrites) |
|
837 end; |
|
838 end; (*local*) |
|
839 *} |
|
840 |
|
841 setup {* |
|
842 CodegenTheorems.add_preproc elim_negate |
|
843 *} |
|
844 |
786 |
845 subsection {* legacy ML bindings *} |
787 subsection {* legacy ML bindings *} |
846 |
788 |
847 ML |
789 ML |
848 {* |
790 {* |