src/HOL/Divides.thy
changeset 66817 0b12755ccbb2
parent 66816 212a3334e7da
child 66837 6ba663ff2b1c
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  section \<open>More on quotient and remainder\<close>
     1.5  
     1.6  theory Divides
     1.7 -imports Parity Nat_Transfer
     1.8 +imports Parity
     1.9  begin
    1.10  
    1.11  subsection \<open>Numeral division with a pragmatic type class\<close>
    1.12 @@ -273,7 +273,7 @@
    1.13  hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
    1.14  
    1.15  
    1.16 -subsection \<open>Division on @{typ nat}\<close>
    1.17 +subsection \<open>More on division\<close>
    1.18  
    1.19  instantiation nat :: unique_euclidean_semiring_numeral
    1.20  begin
    1.21 @@ -1094,6 +1094,24 @@
    1.22  
    1.23  subsubsection \<open>Further properties\<close>
    1.24  
    1.25 +lemma div_int_pos_iff:
    1.26 +  "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
    1.27 +    \<or> k < 0 \<and> l < 0"
    1.28 +  for k l :: int
    1.29 +  apply (cases "k = 0 \<or> l = 0")
    1.30 +   apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
    1.31 +  apply (rule ccontr)
    1.32 +  apply (simp add: neg_imp_zdiv_nonneg_iff)
    1.33 +  done
    1.34 +
    1.35 +lemma mod_int_pos_iff:
    1.36 +  "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
    1.37 +  for k l :: int
    1.38 +  apply (cases "l > 0")
    1.39 +   apply (simp_all add: dvd_eq_mod_eq_0)
    1.40 +  apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
    1.41 +  done
    1.42 +
    1.43  text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
    1.44  
    1.45  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
    1.46 @@ -1139,42 +1157,6 @@
    1.47  apply (simp add: nat_eq_iff zmod_int)
    1.48  done
    1.49  
    1.50 -text  \<open>transfer setup\<close>
    1.51 -
    1.52 -lemma transfer_nat_int_functions:
    1.53 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    1.54 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    1.55 -  by (auto simp add: nat_div_distrib nat_mod_distrib)
    1.56 -
    1.57 -lemma transfer_nat_int_function_closures:
    1.58 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    1.59 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    1.60 -  apply (cases "y = 0")
    1.61 -  apply (auto simp add: pos_imp_zdiv_nonneg_iff)
    1.62 -  apply (cases "y = 0")
    1.63 -  apply auto
    1.64 -done
    1.65 -
    1.66 -declare transfer_morphism_nat_int [transfer add return:
    1.67 -  transfer_nat_int_functions
    1.68 -  transfer_nat_int_function_closures
    1.69 -]
    1.70 -
    1.71 -lemma transfer_int_nat_functions:
    1.72 -    "(int x) div (int y) = int (x div y)"
    1.73 -    "(int x) mod (int y) = int (x mod y)"
    1.74 -  by (auto simp add: zdiv_int zmod_int)
    1.75 -
    1.76 -lemma transfer_int_nat_function_closures:
    1.77 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
    1.78 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
    1.79 -  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
    1.80 -
    1.81 -declare transfer_morphism_int_nat [transfer add return:
    1.82 -  transfer_int_nat_functions
    1.83 -  transfer_int_nat_function_closures
    1.84 -]
    1.85 -
    1.86  text\<open>Suggested by Matthias Daum\<close>
    1.87  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
    1.88  apply (subgoal_tac "nat x div nat k < nat x")
    1.89 @@ -1352,8 +1334,4 @@
    1.90    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    1.91    by auto
    1.92  
    1.93 -text \<open>Tool setup\<close>
    1.94 -
    1.95 -declare transfer_morphism_int_nat [transfer add return: even_int_iff]
    1.96 -
    1.97  end