src/HOL/IntDiv.thy
changeset 29045 3c8f48333731
parent 28562 4e74209f113e
child 29403 fe17df4e4ab3
     1.1 --- a/src/HOL/IntDiv.thy	Wed Dec 10 06:34:10 2008 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Dec 10 07:52:54 2008 -0800
     1.3 @@ -1472,6 +1472,29 @@
     1.4    IntDiv.zpower_zmod
     1.5    zminus_zmod zdiff_zmod_left zdiff_zmod_right
     1.6  
     1.7 +text {* Distributive laws for function @{text nat}. *}
     1.8 +
     1.9 +lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
    1.10 +apply (rule linorder_cases [of y 0])
    1.11 +apply (simp add: div_nonneg_neg_le0)
    1.12 +apply simp
    1.13 +apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
    1.14 +done
    1.15 +
    1.16 +(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
    1.17 +lemma nat_mod_distrib:
    1.18 +  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
    1.19 +apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)
    1.20 +apply (simp add: nat_eq_iff zmod_int)
    1.21 +done
    1.22 +
    1.23 +text{*Suggested by Matthias Daum*}
    1.24 +lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
    1.25 +apply (subgoal_tac "nat x div nat k < nat x")
    1.26 + apply (simp (asm_lr) add: nat_div_distrib [symmetric])
    1.27 +apply (rule Divides.div_less_dividend, simp_all)
    1.28 +done
    1.29 +
    1.30  text {* code generator setup *}
    1.31  
    1.32  context ring_1