euclidean rings need no normalization
authorhaftmann
Sun Oct 08 22:28:22 2017 +0200 (18 months ago)
changeset 668170b12755ccbb2
parent 66816 212a3334e7da
child 66825 9f6ec65f7a6e
euclidean rings need no normalization
src/HOL/Code_Numeral.thy
src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
src/HOL/Computational_Algebra/Field_as_Ring.thy
src/HOL/Computational_Algebra/Formal_Power_Series.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Euclidean_Division.thy
src/HOL/Main.thy
src/HOL/Nat_Transfer.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/SMT.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -220,36 +220,15 @@
     1.4    "of_nat (nat_of_integer k) = max 0 k"
     1.5    by transfer auto
     1.6  
     1.7 -instantiation integer :: normalization_semidom
     1.8 +instantiation integer :: unique_euclidean_ring
     1.9  begin
    1.10  
    1.11 -lift_definition normalize_integer :: "integer \<Rightarrow> integer"
    1.12 -  is "normalize :: int \<Rightarrow> int"
    1.13 -  .
    1.14 -
    1.15 -declare normalize_integer.rep_eq [simp]
    1.16 -
    1.17 -lift_definition unit_factor_integer :: "integer \<Rightarrow> integer"
    1.18 -  is "unit_factor :: int \<Rightarrow> int"
    1.19 -  .
    1.20 -
    1.21 -declare unit_factor_integer.rep_eq [simp]
    1.22 -
    1.23  lift_definition divide_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.24    is "divide :: int \<Rightarrow> int \<Rightarrow> int"
    1.25    .
    1.26  
    1.27  declare divide_integer.rep_eq [simp]
    1.28 -  
    1.29 -instance
    1.30 -  by (standard; transfer)
    1.31 -    (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
    1.32  
    1.33 -end
    1.34 -
    1.35 -instantiation integer :: unique_euclidean_ring
    1.36 -begin
    1.37 -  
    1.38  lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
    1.39    is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
    1.40    .
    1.41 @@ -279,7 +258,7 @@
    1.42    by (simp add: fun_eq_iff nat_of_integer.rep_eq)
    1.43  
    1.44  lemma [code]:
    1.45 -  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> unit_factor k = unit_factor l"
    1.46 +  "uniqueness_constraint (k :: integer) l \<longleftrightarrow> sgn k = sgn l"
    1.47    by (simp add: integer_eq_iff)
    1.48  
    1.49  instance integer :: ring_parity
    1.50 @@ -458,14 +437,6 @@
    1.51    "Neg m * Neg n = Pos (m * n)"
    1.52    by simp_all
    1.53  
    1.54 -lemma normalize_integer_code [code]:
    1.55 -  "normalize = (abs :: integer \<Rightarrow> integer)"
    1.56 -  by transfer simp
    1.57 -
    1.58 -lemma unit_factor_integer_code [code]:
    1.59 -  "unit_factor = (sgn :: integer \<Rightarrow> integer)"
    1.60 -  by transfer simp
    1.61 -
    1.62  definition divmod_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer \<times> integer"
    1.63  where
    1.64    "divmod_integer k l = (k div l, k mod l)"
    1.65 @@ -880,18 +851,6 @@
    1.66  instantiation natural :: unique_euclidean_semiring
    1.67  begin
    1.68  
    1.69 -lift_definition normalize_natural :: "natural \<Rightarrow> natural"
    1.70 -  is "normalize :: nat \<Rightarrow> nat"
    1.71 -  .
    1.72 -
    1.73 -declare normalize_natural.rep_eq [simp]
    1.74 -
    1.75 -lift_definition unit_factor_natural :: "natural \<Rightarrow> natural"
    1.76 -  is "unit_factor :: nat \<Rightarrow> nat"
    1.77 -  .
    1.78 -
    1.79 -declare unit_factor_natural.rep_eq [simp]
    1.80 -
    1.81  lift_definition divide_natural :: "natural \<Rightarrow> natural \<Rightarrow> natural"
    1.82    is "divide :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.83    .
    1.84 @@ -1068,31 +1027,6 @@
    1.85    "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n"
    1.86    by transfer simp
    1.87  
    1.88 -lemma [code]:
    1.89 -  "normalize n = n" for n :: natural
    1.90 -  by transfer simp
    1.91 -
    1.92 -lemma [code]:
    1.93 -  "unit_factor n = of_bool (n \<noteq> 0)" for n :: natural
    1.94 -proof (cases "n = 0")
    1.95 -  case True
    1.96 -  then show ?thesis
    1.97 -    by simp
    1.98 -next
    1.99 -  case False
   1.100 -  then have "unit_factor n = 1"
   1.101 -  proof transfer
   1.102 -    fix n :: nat
   1.103 -    assume "n \<noteq> 0"
   1.104 -    then obtain m where "n = Suc m"
   1.105 -      by (cases n) auto
   1.106 -    then show "unit_factor n = 1"
   1.107 -      by simp
   1.108 -  qed
   1.109 -  with False show ?thesis
   1.110 -    by simp
   1.111 -qed
   1.112 -
   1.113  lemma [code abstract]:
   1.114    "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n"
   1.115    by transfer (simp add: zdiv_int)
     2.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
     2.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Sun Oct 08 22:28:22 2017 +0200
     2.3 @@ -9,10 +9,26 @@
     2.4  begin
     2.5  
     2.6  subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
     2.7 -  
     2.8 -context euclidean_semiring
     2.9 +
    2.10 +class normalization_euclidean_semiring = euclidean_semiring + normalization_semidom
    2.11  begin
    2.12  
    2.13 +lemma euclidean_size_normalize [simp]:
    2.14 +  "euclidean_size (normalize a) = euclidean_size a"
    2.15 +proof (cases "a = 0")
    2.16 +  case True
    2.17 +  then show ?thesis
    2.18 +    by simp
    2.19 +next
    2.20 +  case [simp]: False
    2.21 +  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    2.22 +    by (rule size_mult_mono) simp
    2.23 +  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    2.24 +    by (rule size_mult_mono) simp
    2.25 +  ultimately show ?thesis
    2.26 +    by simp
    2.27 +qed
    2.28 +
    2.29  context
    2.30  begin
    2.31  
    2.32 @@ -282,7 +298,7 @@
    2.33    
    2.34  subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
    2.35    
    2.36 -class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
    2.37 +class euclidean_semiring_gcd = normalization_euclidean_semiring + gcd + Gcd +
    2.38    assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
    2.39      and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
    2.40    assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
    2.41 @@ -400,7 +416,7 @@
    2.42  end
    2.43  
    2.44  lemma factorial_euclidean_semiring_gcdI:
    2.45 -  "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
    2.46 +  "OFCLASS('a::{factorial_semiring_gcd, normalization_euclidean_semiring}, euclidean_semiring_gcd_class)"
    2.47  proof
    2.48    interpret semiring_Gcd 1 0 times
    2.49      Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
    2.50 @@ -502,7 +518,7 @@
    2.51          also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
    2.52            by (simp add: algebra_simps)
    2.53          finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
    2.54 -      qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
    2.55 +      qed (auto simp: algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
    2.56        finally show ?thesis .
    2.57      qed
    2.58    qed
    2.59 @@ -552,6 +568,8 @@
    2.60  
    2.61  subsection \<open>Typical instances\<close>
    2.62  
    2.63 +instance nat :: normalization_euclidean_semiring ..
    2.64 +
    2.65  instance nat :: euclidean_semiring_gcd
    2.66  proof
    2.67    interpret semiring_Gcd 1 0 times
    2.68 @@ -584,6 +602,8 @@
    2.69      by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
    2.70  qed
    2.71  
    2.72 +instance int :: normalization_euclidean_semiring ..
    2.73 +
    2.74  instance int :: euclidean_ring_gcd
    2.75  proof
    2.76    interpret semiring_Gcd 1 0 times
     3.1 --- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
     3.2 +++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Sun Oct 08 22:28:22 2017 +0200
     3.3 @@ -24,7 +24,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -instantiation real :: unique_euclidean_ring
     3.8 +instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
     3.9  begin
    3.10  
    3.11  definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
    3.12 @@ -55,7 +55,7 @@
    3.13  
    3.14  end
    3.15  
    3.16 -instantiation rat :: unique_euclidean_ring
    3.17 +instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
    3.18  begin
    3.19  
    3.20  definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
    3.21 @@ -86,7 +86,7 @@
    3.22  
    3.23  end
    3.24  
    3.25 -instantiation complex :: unique_euclidean_ring
    3.26 +instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
    3.27  begin
    3.28  
    3.29  definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
     4.1 --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
     4.2 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Oct 08 22:28:22 2017 +0200
     4.3 @@ -1425,6 +1425,8 @@
     4.4  
     4.5  end
     4.6  
     4.7 +instance fps :: (field) normalization_euclidean_semiring ..
     4.8 +
     4.9  instantiation fps :: (field) euclidean_ring_gcd
    4.10  begin
    4.11  definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
     5.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
     5.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:22 2017 +0200
     5.3 @@ -416,14 +416,12 @@
     5.4  begin
     5.5  
     5.6  interpretation field_poly: 
     5.7 -  unique_euclidean_ring where zero = "0 :: 'a :: field poly"
     5.8 -    and one = 1 and plus = plus
     5.9 -    and uminus = uminus and minus = minus
    5.10 +  normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
    5.11 +    and one = 1 and plus = plus and minus = minus
    5.12      and times = times
    5.13      and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
    5.14      and unit_factor = "\<lambda>p. [:lead_coeff p:]"
    5.15      and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
    5.16 -    and uniqueness_constraint = top
    5.17      and divide = divide and modulo = modulo
    5.18    rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
    5.19      and "comm_monoid_mult.prod_mset times 1 = prod_mset"
    5.20 @@ -438,9 +436,9 @@
    5.21      by (simp add: irreducible_dict)
    5.22    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
    5.23      by (simp add: prime_elem_dict)
    5.24 -  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
    5.25 -    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
    5.26 -    (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
    5.27 +  show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
    5.28 +    modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
    5.29 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
    5.30    proof (standard, fold dvd_dict)
    5.31      fix p :: "'a poly"
    5.32      show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
    5.33 @@ -453,23 +451,6 @@
    5.34      fix p :: "'a poly" assume "p \<noteq> 0"
    5.35      then show "is_unit [:lead_coeff p:]"
    5.36        by (simp add: is_unit_pCons_iff)
    5.37 -  next
    5.38 -    fix p q s :: "'a poly" assume "s \<noteq> 0"
    5.39 -    moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)"
    5.40 -    ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
    5.41 -      by (auto simp add: degree_mult_eq)
    5.42 -  next
    5.43 -    fix p q r :: "'a poly"
    5.44 -    assume "p \<noteq> 0"
    5.45 -    with eucl_rel_poly [of r p] have "eucl_rel_poly (r + q * p) p (q + r div p, r mod p)"
    5.46 -      by (simp add: eucl_rel_poly_iff distrib_right)
    5.47 -    then have "(r + q * p) div p = q + r div p"
    5.48 -      by (rule div_poly_eq)
    5.49 -    moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
    5.50 -      < (if p = 0 then 0 else 2 ^ degree p)"
    5.51 -    ultimately show "(q * p + r) div p = q"
    5.52 -      using \<open>p \<noteq> 0\<close>
    5.53 -      by (cases "r = 0") (simp_all add: div_poly_less ac_simps)
    5.54    qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    5.55  qed
    5.56  
    5.57 @@ -758,7 +739,7 @@
    5.58  
    5.59  end
    5.60  
    5.61 -instantiation poly :: ("{field,factorial_ring_gcd}") unique_euclidean_ring
    5.62 +instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
    5.63  begin
    5.64  
    5.65  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
    5.66 @@ -783,9 +764,8 @@
    5.67  
    5.68  end
    5.69  
    5.70 -instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
    5.71 -  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI)
    5.72 -    standard
    5.73 +instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
    5.74 +  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
    5.75  
    5.76    
    5.77  subsection \<open>Polynomial GCD\<close>
     6.1 --- a/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     6.2 +++ b/src/HOL/Divides.thy	Sun Oct 08 22:28:22 2017 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  section \<open>More on quotient and remainder\<close>
     6.5  
     6.6  theory Divides
     6.7 -imports Parity Nat_Transfer
     6.8 +imports Parity
     6.9  begin
    6.10  
    6.11  subsection \<open>Numeral division with a pragmatic type class\<close>
    6.12 @@ -273,7 +273,7 @@
    6.13  hide_fact (open) div_less mod_less mod_less_eq_dividend mod_mult2_eq div_mult2_eq
    6.14  
    6.15  
    6.16 -subsection \<open>Division on @{typ nat}\<close>
    6.17 +subsection \<open>More on division\<close>
    6.18  
    6.19  instantiation nat :: unique_euclidean_semiring_numeral
    6.20  begin
    6.21 @@ -1094,6 +1094,24 @@
    6.22  
    6.23  subsubsection \<open>Further properties\<close>
    6.24  
    6.25 +lemma div_int_pos_iff:
    6.26 +  "k div l \<ge> 0 \<longleftrightarrow> k = 0 \<or> l = 0 \<or> k \<ge> 0 \<and> l \<ge> 0
    6.27 +    \<or> k < 0 \<and> l < 0"
    6.28 +  for k l :: int
    6.29 +  apply (cases "k = 0 \<or> l = 0")
    6.30 +   apply (auto simp add: pos_imp_zdiv_nonneg_iff neg_imp_zdiv_nonneg_iff)
    6.31 +  apply (rule ccontr)
    6.32 +  apply (simp add: neg_imp_zdiv_nonneg_iff)
    6.33 +  done
    6.34 +
    6.35 +lemma mod_int_pos_iff:
    6.36 +  "k mod l \<ge> 0 \<longleftrightarrow> l dvd k \<or> l = 0 \<and> k \<ge> 0 \<or> l > 0"
    6.37 +  for k l :: int
    6.38 +  apply (cases "l > 0")
    6.39 +   apply (simp_all add: dvd_eq_mod_eq_0)
    6.40 +  apply (use neg_mod_conj [of l k] in \<open>auto simp add: le_less not_less\<close>)
    6.41 +  done
    6.42 +
    6.43  text \<open>Simplify expresions in which div and mod combine numerical constants\<close>
    6.44  
    6.45  lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
    6.46 @@ -1139,42 +1157,6 @@
    6.47  apply (simp add: nat_eq_iff zmod_int)
    6.48  done
    6.49  
    6.50 -text  \<open>transfer setup\<close>
    6.51 -
    6.52 -lemma transfer_nat_int_functions:
    6.53 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    6.54 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    6.55 -  by (auto simp add: nat_div_distrib nat_mod_distrib)
    6.56 -
    6.57 -lemma transfer_nat_int_function_closures:
    6.58 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    6.59 -    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    6.60 -  apply (cases "y = 0")
    6.61 -  apply (auto simp add: pos_imp_zdiv_nonneg_iff)
    6.62 -  apply (cases "y = 0")
    6.63 -  apply auto
    6.64 -done
    6.65 -
    6.66 -declare transfer_morphism_nat_int [transfer add return:
    6.67 -  transfer_nat_int_functions
    6.68 -  transfer_nat_int_function_closures
    6.69 -]
    6.70 -
    6.71 -lemma transfer_int_nat_functions:
    6.72 -    "(int x) div (int y) = int (x div y)"
    6.73 -    "(int x) mod (int y) = int (x mod y)"
    6.74 -  by (auto simp add: zdiv_int zmod_int)
    6.75 -
    6.76 -lemma transfer_int_nat_function_closures:
    6.77 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
    6.78 -    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
    6.79 -  by (simp_all only: is_nat_def transfer_nat_int_function_closures)
    6.80 -
    6.81 -declare transfer_morphism_int_nat [transfer add return:
    6.82 -  transfer_int_nat_functions
    6.83 -  transfer_int_nat_function_closures
    6.84 -]
    6.85 -
    6.86  text\<open>Suggested by Matthias Daum\<close>
    6.87  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
    6.88  apply (subgoal_tac "nat x div nat k < nat x")
    6.89 @@ -1352,8 +1334,4 @@
    6.90    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
    6.91    by auto
    6.92  
    6.93 -text \<open>Tool setup\<close>
    6.94 -
    6.95 -declare transfer_morphism_int_nat [transfer add return: even_int_iff]
    6.96 -
    6.97  end
     7.1 --- a/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
     7.2 +++ b/src/HOL/Enum.thy	Sun Oct 08 22:28:22 2017 +0200
     7.3 @@ -712,7 +712,7 @@
     7.4    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> y = a\<^sub>1"
     7.5    by (auto simp add: dvd_def times_finite_2_def split: finite_2.splits)
     7.6  
     7.7 -instantiation finite_2 :: unique_euclidean_semiring begin
     7.8 +instantiation finite_2 :: "{normalization_semidom, unique_euclidean_semiring}" begin
     7.9  definition [simp]: "normalize = (id :: finite_2 \<Rightarrow> _)"
    7.10  definition [simp]: "unit_factor = (id :: finite_2 \<Rightarrow> _)"
    7.11  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | a\<^sub>2 \<Rightarrow> 1)"
    7.12 @@ -864,7 +864,7 @@
    7.13    "x dvd y \<longleftrightarrow> x = a\<^sub>2 \<or> x = a\<^sub>3 \<or> y = a\<^sub>1"
    7.14    by (cases x) (auto simp add: dvd_def times_finite_3_def split: finite_3.splits)
    7.15  
    7.16 -instantiation finite_3 :: unique_euclidean_semiring begin
    7.17 +instantiation finite_3 :: "{normalization_semidom, unique_euclidean_semiring}" begin
    7.18  definition [simp]: "normalize x = (case x of a\<^sub>3 \<Rightarrow> a\<^sub>2 | _ \<Rightarrow> x)"
    7.19  definition [simp]: "unit_factor = (id :: finite_3 \<Rightarrow> _)"
    7.20  definition [simp]: "euclidean_size x = (case x of a\<^sub>1 \<Rightarrow> 0 | _ \<Rightarrow> 1)"
     8.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     8.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:22 2017 +0200
     8.3 @@ -3,15 +3,15 @@
     8.4      Author:     Florian Haftmann, TU Muenchen
     8.5  *)
     8.6  
     8.7 -section \<open>Uniquely determined division in euclidean (semi)rings\<close>
     8.8 +section \<open>Division in euclidean (semi)rings\<close>
     8.9  
    8.10  theory Euclidean_Division
    8.11 -  imports Nat_Transfer Lattices_Big
    8.12 +  imports Int Lattices_Big
    8.13  begin
    8.14  
    8.15  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
    8.16    
    8.17 -class euclidean_semiring = semidom_modulo + normalization_semidom + 
    8.18 +class euclidean_semiring = semidom_modulo + 
    8.19    fixes euclidean_size :: "'a \<Rightarrow> nat"
    8.20    assumes size_0 [simp]: "euclidean_size 0 = 0"
    8.21    assumes mod_size_less: 
    8.22 @@ -23,22 +23,6 @@
    8.23  lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
    8.24    by (subst mult.commute) (rule size_mult_mono)
    8.25  
    8.26 -lemma euclidean_size_normalize [simp]:
    8.27 -  "euclidean_size (normalize a) = euclidean_size a"
    8.28 -proof (cases "a = 0")
    8.29 -  case True
    8.30 -  then show ?thesis
    8.31 -    by simp
    8.32 -next
    8.33 -  case [simp]: False
    8.34 -  have "euclidean_size (normalize a) \<le> euclidean_size (normalize a * unit_factor a)"
    8.35 -    by (rule size_mult_mono) simp
    8.36 -  moreover have "euclidean_size a \<le> euclidean_size (a * (1 div unit_factor a))"
    8.37 -    by (rule size_mult_mono) simp
    8.38 -  ultimately show ?thesis
    8.39 -    by simp
    8.40 -qed
    8.41 -
    8.42  lemma dvd_euclidean_size_eq_imp_dvd:
    8.43    assumes "a \<noteq> 0" and "euclidean_size a = euclidean_size b"
    8.44      and "b dvd a" 
     9.1 --- a/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
     9.2 +++ b/src/HOL/Main.thy	Sun Oct 08 22:28:22 2017 +0200
     9.3 @@ -6,7 +6,16 @@
     9.4  \<close>
     9.5  
     9.6  theory Main
     9.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Nunchaku BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices Binomial GCD
     9.8 +  imports
     9.9 +    Predicate_Compile
    9.10 +    Quickcheck_Narrowing 
    9.11 +    Extraction
    9.12 +    Nunchaku
    9.13 +    BNF_Greatest_Fixpoint Filter
    9.14 +    Conditionally_Complete_Lattices
    9.15 +    Binomial
    9.16 +    GCD
    9.17 +    Nat_Transfer
    9.18  begin
    9.19  
    9.20  text \<open>
    10.1 --- a/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
    10.2 +++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4  section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
    10.5  
    10.6  theory Nat_Transfer
    10.7 -imports Int
    10.8 +imports Int Divides
    10.9  begin
   10.10  
   10.11  subsection \<open>Generic transfer machinery\<close>
   10.12 @@ -21,7 +21,8 @@
   10.13  
   10.14  text \<open>set up transfer direction\<close>
   10.15  
   10.16 -lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
   10.17 +lemma transfer_morphism_nat_int [no_atp]:
   10.18 +  "transfer_morphism nat (op <= (0::int))" ..
   10.19  
   10.20  declare transfer_morphism_nat_int [transfer add
   10.21    mode: manual
   10.22 @@ -31,7 +32,7 @@
   10.23  
   10.24  text \<open>basic functions and relations\<close>
   10.25  
   10.26 -lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
   10.27 +lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
   10.28      "(0::nat) = nat 0"
   10.29      "(1::nat) = nat 1"
   10.30      "(2::nat) = nat 2"
   10.31 @@ -46,15 +47,17 @@
   10.32  lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   10.33    by (simp add: tsub_def)
   10.34  
   10.35 -lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
   10.36 +lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
   10.37      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
   10.38      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
   10.39      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
   10.40      "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
   10.41 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
   10.42 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   10.43    by (auto simp add: eq_nat_nat_iff nat_mult_distrib
   10.44 -      nat_power_eq tsub_def)
   10.45 +      nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
   10.46  
   10.47 -lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
   10.48 +lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
   10.49      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
   10.50      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
   10.51      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
   10.52 @@ -64,9 +67,16 @@
   10.53      "(2::int) >= 0"
   10.54      "(3::int) >= 0"
   10.55      "int z >= 0"
   10.56 -  by (auto simp add: zero_le_mult_iff tsub_def)
   10.57 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
   10.58 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
   10.59 +            apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
   10.60 +   apply (cases "y = 0")
   10.61 +    apply (auto simp add: pos_imp_zdiv_nonneg_iff)
   10.62 +  apply (cases "y = 0")
   10.63 +   apply auto
   10.64 +  done
   10.65  
   10.66 -lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
   10.67 +lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
   10.68      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   10.69        (nat (x::int) = nat y) = (x = y)"
   10.70      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
   10.71 @@ -94,7 +104,7 @@
   10.72    then show "\<exists>x. P x" by auto
   10.73  qed
   10.74  
   10.75 -lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
   10.76 +lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
   10.77      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
   10.78      "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   10.79    by (rule all_nat, rule ex_nat)
   10.80 @@ -126,7 +136,7 @@
   10.81  where
   10.82    "nat_set S = (ALL x:S. x >= 0)"
   10.83  
   10.84 -lemma transfer_nat_int_set_functions:
   10.85 +lemma transfer_nat_int_set_functions [no_atp]:
   10.86      "card A = card (int ` A)"
   10.87      "{} = nat ` ({}::int set)"
   10.88      "A Un B = nat ` (int ` A Un int ` B)"
   10.89 @@ -144,7 +154,7 @@
   10.90    apply auto
   10.91  done
   10.92  
   10.93 -lemma transfer_nat_int_set_function_closures:
   10.94 +lemma transfer_nat_int_set_function_closures [no_atp]:
   10.95      "nat_set {}"
   10.96      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   10.97      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   10.98 @@ -154,7 +164,7 @@
   10.99    unfolding nat_set_def apply auto
  10.100  done
  10.101  
  10.102 -lemma transfer_nat_int_set_relations:
  10.103 +lemma transfer_nat_int_set_relations [no_atp]:
  10.104      "(finite A) = (finite (int ` A))"
  10.105      "(x : A) = (int x : int ` A)"
  10.106      "(A = B) = (int ` A = int ` B)"
  10.107 @@ -169,11 +179,11 @@
  10.108    apply (drule_tac x = "int x" in spec, auto)
  10.109  done
  10.110  
  10.111 -lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
  10.112 +lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
  10.113      (int ` nat ` A = A)"
  10.114    by (auto simp add: nat_set_def image_def)
  10.115  
  10.116 -lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
  10.117 +lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
  10.118      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
  10.119    by auto
  10.120  
  10.121 @@ -189,7 +199,7 @@
  10.122  text \<open>sum and prod\<close>
  10.123  
  10.124  (* this handles the case where the *domain* of f is nat *)
  10.125 -lemma transfer_nat_int_sum_prod:
  10.126 +lemma transfer_nat_int_sum_prod [no_atp]:
  10.127      "sum f A = sum (%x. f (nat x)) (int ` A)"
  10.128      "prod f A = prod (%x. f (nat x)) (int ` A)"
  10.129    apply (subst sum.reindex)
  10.130 @@ -199,14 +209,14 @@
  10.131  done
  10.132  
  10.133  (* this handles the case where the *range* of f is nat *)
  10.134 -lemma transfer_nat_int_sum_prod2:
  10.135 +lemma transfer_nat_int_sum_prod2 [no_atp]:
  10.136      "sum f A = nat(sum (%x. int (f x)) A)"
  10.137      "prod f A = nat(prod (%x. int (f x)) A)"
  10.138    apply (simp only: int_sum [symmetric] nat_int)
  10.139    apply (simp only: int_prod [symmetric] nat_int)
  10.140    done
  10.141  
  10.142 -lemma transfer_nat_int_sum_prod_closure:
  10.143 +lemma transfer_nat_int_sum_prod_closure [no_atp]:
  10.144      "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
  10.145      "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
  10.146    unfolding nat_set_def
  10.147 @@ -236,7 +246,7 @@
  10.148     Also, why aren't sum.cong and prod.cong enough,
  10.149     with the previously mentioned rule turned on? *)
  10.150  
  10.151 -lemma transfer_nat_int_sum_prod_cong:
  10.152 +lemma transfer_nat_int_sum_prod_cong [no_atp]:
  10.153      "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  10.154        sum f A = sum g B"
  10.155      "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
  10.156 @@ -257,7 +267,7 @@
  10.157  
  10.158  text \<open>set up transfer direction\<close>
  10.159  
  10.160 -lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
  10.161 +lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
  10.162  
  10.163  declare transfer_morphism_int_nat [transfer add
  10.164    mode: manual
  10.165 @@ -273,21 +283,23 @@
  10.166  where
  10.167    "is_nat x = (x >= 0)"
  10.168  
  10.169 -lemma transfer_int_nat_numerals:
  10.170 +lemma transfer_int_nat_numerals [no_atp]:
  10.171      "0 = int 0"
  10.172      "1 = int 1"
  10.173      "2 = int 2"
  10.174      "3 = int 3"
  10.175    by auto
  10.176  
  10.177 -lemma transfer_int_nat_functions:
  10.178 +lemma transfer_int_nat_functions [no_atp]:
  10.179      "(int x) + (int y) = int (x + y)"
  10.180      "(int x) * (int y) = int (x * y)"
  10.181      "tsub (int x) (int y) = int (x - y)"
  10.182      "(int x)^n = int (x^n)"
  10.183 -  by (auto simp add: tsub_def)
  10.184 +    "(int x) div (int y) = int (x div y)"
  10.185 +    "(int x) mod (int y) = int (x mod y)"
  10.186 +  by (auto simp add: zdiv_int zmod_int tsub_def)
  10.187  
  10.188 -lemma transfer_int_nat_function_closures:
  10.189 +lemma transfer_int_nat_function_closures [no_atp]:
  10.190      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
  10.191      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
  10.192      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
  10.193 @@ -297,9 +309,11 @@
  10.194      "is_nat 2"
  10.195      "is_nat 3"
  10.196      "is_nat (int z)"
  10.197 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
  10.198 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
  10.199    by (simp_all only: is_nat_def transfer_nat_int_function_closures)
  10.200  
  10.201 -lemma transfer_int_nat_relations:
  10.202 +lemma transfer_int_nat_relations [no_atp]:
  10.203      "(int x = int y) = (x = y)"
  10.204      "(int x < int y) = (x < y)"
  10.205      "(int x <= int y) = (x <= y)"
  10.206 @@ -316,7 +330,7 @@
  10.207  
  10.208  text \<open>first-order quantifiers\<close>
  10.209  
  10.210 -lemma transfer_int_nat_quantifiers:
  10.211 +lemma transfer_int_nat_quantifiers [no_atp]:
  10.212      "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
  10.213      "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
  10.214    apply (subst all_nat)
  10.215 @@ -341,7 +355,7 @@
  10.216  
  10.217  text \<open>operations with sets\<close>
  10.218  
  10.219 -lemma transfer_int_nat_set_functions:
  10.220 +lemma transfer_int_nat_set_functions [no_atp]:
  10.221      "nat_set A \<Longrightarrow> card A = card (nat ` A)"
  10.222      "{} = int ` ({}::nat set)"
  10.223      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
  10.224 @@ -353,7 +367,7 @@
  10.225            transfer_nat_int_set_return_embed nat_0_le
  10.226            cong: transfer_nat_int_set_cong)
  10.227  
  10.228 -lemma transfer_int_nat_set_function_closures:
  10.229 +lemma transfer_int_nat_set_function_closures [no_atp]:
  10.230      "nat_set {}"
  10.231      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
  10.232      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
  10.233 @@ -362,7 +376,7 @@
  10.234      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
  10.235    by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
  10.236  
  10.237 -lemma transfer_int_nat_set_relations:
  10.238 +lemma transfer_int_nat_set_relations [no_atp]:
  10.239      "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
  10.240      "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
  10.241      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
  10.242 @@ -371,12 +385,12 @@
  10.243    by (simp_all only: is_nat_def transfer_nat_int_set_relations
  10.244      transfer_nat_int_set_return_embed nat_0_le)
  10.245  
  10.246 -lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
  10.247 +lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
  10.248    by (simp only: transfer_nat_int_set_relations
  10.249      transfer_nat_int_set_function_closures
  10.250      transfer_nat_int_set_return_embed nat_0_le)
  10.251  
  10.252 -lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
  10.253 +lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
  10.254      {(x::nat). P x} = {x. P' x}"
  10.255    by auto
  10.256  
  10.257 @@ -392,7 +406,7 @@
  10.258  text \<open>sum and prod\<close>
  10.259  
  10.260  (* this handles the case where the *domain* of f is int *)
  10.261 -lemma transfer_int_nat_sum_prod:
  10.262 +lemma transfer_int_nat_sum_prod [no_atp]:
  10.263      "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
  10.264      "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
  10.265    apply (subst sum.reindex)
  10.266 @@ -403,7 +417,7 @@
  10.267  done
  10.268  
  10.269  (* this handles the case where the *range* of f is int *)
  10.270 -lemma transfer_int_nat_sum_prod2:
  10.271 +lemma transfer_int_nat_sum_prod2 [no_atp]:
  10.272      "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
  10.273      "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
  10.274        prod f A = int(prod (%x. nat (f x)) A)"
  10.275 @@ -414,4 +428,6 @@
  10.276    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
  10.277    cong: sum.cong prod.cong]
  10.278  
  10.279 +declare transfer_morphism_int_nat [transfer add return: even_int_iff]
  10.280 +
  10.281  end
    11.1 --- a/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
    11.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sun Oct 08 22:28:22 2017 +0200
    11.3 @@ -86,8 +86,7 @@
    11.4    "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)"
    11.5    for x y m :: int
    11.6    unfolding cong_int_def cong_nat_def
    11.7 -  by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib)
    11.8 -
    11.9 +  by (metis int_nat_eq nat_mod_distrib zmod_int)
   11.10  
   11.11  declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong]
   11.12  
    12.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
    12.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 08 22:28:22 2017 +0200
    12.3 @@ -196,7 +196,8 @@
    12.4    moreover have "int y = 0 \<or> 0 < int y" for y
    12.5      by linarith
    12.6    ultimately show "0 < x mod int p"
    12.7 -    by (metis (no_types) B_greater_zero Divides.transfer_int_nat_functions(2) zero_less_imp_eq_int)
    12.8 +    using B_greater_zero [of x]
    12.9 +    by (auto simp add: mod_int_pos_iff intro: neq_le_trans)
   12.10  qed
   12.11  
   12.12  lemma F_subset: "F \<subseteq> {x. 0 < x \<and> x \<le> ((int p - 1) div 2)}"
    13.1 --- a/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
    13.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sun Oct 08 22:28:22 2017 +0200
    13.3 @@ -365,8 +365,7 @@
    13.4      done
    13.5    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
    13.6    then show ?thesis
    13.7 -    by (metis of_nat_fact Divides.transfer_int_nat_functions(2)
    13.8 -        cong_int_def res_neg_eq res_one_eq)
    13.9 +    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
   13.10  qed
   13.11  
   13.12  lemma wilson_theorem:
    14.1 --- a/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
    14.2 +++ b/src/HOL/SMT.thy	Sun Oct 08 22:28:22 2017 +0200
    14.3 @@ -124,8 +124,14 @@
    14.4  lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
    14.5  lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
    14.6  
    14.7 -lemmas nat_zero_as_int = transfer_nat_int_numerals(1)
    14.8 -lemmas nat_one_as_int = transfer_nat_int_numerals(2)
    14.9 +lemma nat_zero_as_int:
   14.10 +  "0 = nat 0"
   14.11 +  by simp
   14.12 +
   14.13 +lemma nat_one_as_int:
   14.14 +  "1 = nat 1"
   14.15 +  by simp
   14.16 +
   14.17  lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
   14.18  lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
   14.19  lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a \<le> int b)" by simp