src/HOL/Code_Numeral.thy
changeset 66817 0b12755ccbb2
parent 66815 93c6632ddf44
child 66836 4eb431c3f974
     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)