src/HOL/Divides.thy
changeset 60685 cb21b7022b00
parent 60562 24af00b010cf
child 60690 a9e45c9588c3
     1.1 --- a/src/HOL/Divides.thy	Wed Jul 08 00:04:15 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jul 08 14:01:34 2015 +0200
     1.3 @@ -1034,6 +1034,25 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation nat :: normalization_semidom
     1.8 +begin
     1.9 +
    1.10 +definition normalize_nat
    1.11 +  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
    1.12 +
    1.13 +definition unit_factor_nat
    1.14 +  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
    1.15 +
    1.16 +lemma unit_factor_simps [simp]:
    1.17 +  "unit_factor 0 = (0::nat)"
    1.18 +  "unit_factor (Suc n) = 1"
    1.19 +  by (simp_all add: unit_factor_nat_def)
    1.20 +
    1.21 +instance
    1.22 +  by standard (simp_all add: unit_factor_nat_def)
    1.23 +  
    1.24 +end
    1.25 +
    1.26  lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
    1.27    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
    1.28    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    1.29 @@ -1890,6 +1909,27 @@
    1.30    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    1.31    by auto
    1.32  
    1.33 +instantiation int :: normalization_semidom
    1.34 +begin
    1.35 +
    1.36 +definition normalize_int
    1.37 +  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
    1.38 +
    1.39 +definition unit_factor_int
    1.40 +  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
    1.41 +
    1.42 +instance
    1.43 +proof
    1.44 +  fix k :: int
    1.45 +  assume "k \<noteq> 0"
    1.46 +  then have "\<bar>sgn k\<bar> = 1"
    1.47 +    by (cases "0::int" k rule: linorder_cases) simp_all
    1.48 +  then show "is_unit (unit_factor k)"
    1.49 +    by simp
    1.50 +qed (simp_all add: sgn_times mult_sgn_abs)
    1.51 +  
    1.52 +end
    1.53 +  
    1.54  text{*Basic laws about division and remainder*}
    1.55  
    1.56  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"