src/HOL/Number_Theory/Normalization_Semidom.thy
author haftmann
Thu Jul 02 10:06:47 2015 +0200 (2015-07-02)
changeset 60634 e3b6e516608b
permissions -rw-r--r--
separate (semi)ring with normalization
haftmann@60634
     1
theory Normalization_Semidom
haftmann@60634
     2
imports Main
haftmann@60634
     3
begin
haftmann@60634
     4
haftmann@60634
     5
context algebraic_semidom
haftmann@60634
     6
begin
haftmann@60634
     7
haftmann@60634
     8
lemma is_unit_divide_mult_cancel_left:
haftmann@60634
     9
  assumes "a \<noteq> 0" and "is_unit b"
haftmann@60634
    10
  shows "a div (a * b) = 1 div b"
haftmann@60634
    11
proof -
haftmann@60634
    12
  from assms have "a div (a * b) = a div a div b"
haftmann@60634
    13
    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
haftmann@60634
    14
  with assms show ?thesis by simp
haftmann@60634
    15
qed
haftmann@60634
    16
haftmann@60634
    17
lemma is_unit_divide_mult_cancel_right:
haftmann@60634
    18
  assumes "a \<noteq> 0" and "is_unit b"
haftmann@60634
    19
  shows "a div (b * a) = 1 div b"
haftmann@60634
    20
  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
haftmann@60634
    21
haftmann@60634
    22
end
haftmann@60634
    23
haftmann@60634
    24
class normalization_semidom = algebraic_semidom +
haftmann@60634
    25
  fixes normalize :: "'a \<Rightarrow> 'a"
haftmann@60634
    26
    and unit_factor :: "'a \<Rightarrow> 'a"
haftmann@60634
    27
  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
haftmann@60634
    28
  assumes normalize_0 [simp]: "normalize 0 = 0"
haftmann@60634
    29
    and unit_factor_0 [simp]: "unit_factor 0 = 0"
haftmann@60634
    30
  assumes is_unit_normalize:
haftmann@60634
    31
    "is_unit a  \<Longrightarrow> normalize a = 1"
haftmann@60634
    32
  assumes unit_factor_is_unit [iff]: 
haftmann@60634
    33
    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
haftmann@60634
    34
  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
haftmann@60634
    35
begin
haftmann@60634
    36
haftmann@60634
    37
lemma unit_factor_dvd [simp]:
haftmann@60634
    38
  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
haftmann@60634
    39
  by (rule unit_imp_dvd) simp
haftmann@60634
    40
haftmann@60634
    41
lemma unit_factor_self [simp]:
haftmann@60634
    42
  "unit_factor a dvd a"
haftmann@60634
    43
  by (cases "a = 0") simp_all 
haftmann@60634
    44
  
haftmann@60634
    45
lemma normalize_mult_unit_factor [simp]:
haftmann@60634
    46
  "normalize a * unit_factor a = a"
haftmann@60634
    47
  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
haftmann@60634
    48
haftmann@60634
    49
lemma normalize_eq_0_iff [simp]:
haftmann@60634
    50
  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
haftmann@60634
    51
proof
haftmann@60634
    52
  assume ?P
haftmann@60634
    53
  moreover have "unit_factor a * normalize a = a" by simp
haftmann@60634
    54
  ultimately show ?Q by simp 
haftmann@60634
    55
next
haftmann@60634
    56
  assume ?Q then show ?P by simp
haftmann@60634
    57
qed
haftmann@60634
    58
haftmann@60634
    59
lemma unit_factor_eq_0_iff [simp]:
haftmann@60634
    60
  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
haftmann@60634
    61
proof
haftmann@60634
    62
  assume ?P
haftmann@60634
    63
  moreover have "unit_factor a * normalize a = a" by simp
haftmann@60634
    64
  ultimately show ?Q by simp 
haftmann@60634
    65
next
haftmann@60634
    66
  assume ?Q then show ?P by simp
haftmann@60634
    67
qed
haftmann@60634
    68
haftmann@60634
    69
lemma is_unit_unit_factor:
haftmann@60634
    70
  assumes "is_unit a" shows "unit_factor a = a"
haftmann@60634
    71
proof - 
haftmann@60634
    72
  from assms have "normalize a = 1" by (rule is_unit_normalize)
haftmann@60634
    73
  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
haftmann@60634
    74
  ultimately show ?thesis by simp
haftmann@60634
    75
qed
haftmann@60634
    76
haftmann@60634
    77
lemma unit_factor_1 [simp]:
haftmann@60634
    78
  "unit_factor 1 = 1"
haftmann@60634
    79
  by (rule is_unit_unit_factor) simp
haftmann@60634
    80
haftmann@60634
    81
lemma normalize_1 [simp]:
haftmann@60634
    82
  "normalize 1 = 1"
haftmann@60634
    83
  by (rule is_unit_normalize) simp
haftmann@60634
    84
haftmann@60634
    85
lemma normalize_1_iff:
haftmann@60634
    86
  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
haftmann@60634
    87
proof
haftmann@60634
    88
  assume ?Q then show ?P by (rule is_unit_normalize)
haftmann@60634
    89
next
haftmann@60634
    90
  assume ?P
haftmann@60634
    91
  then have "a \<noteq> 0" by auto
haftmann@60634
    92
  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
haftmann@60634
    93
    by simp
haftmann@60634
    94
  then have "unit_factor a = a"
haftmann@60634
    95
    by simp
haftmann@60634
    96
  moreover have "is_unit (unit_factor a)"
haftmann@60634
    97
    using \<open>a \<noteq> 0\<close> by simp
haftmann@60634
    98
  ultimately show ?Q by simp
haftmann@60634
    99
qed
haftmann@60634
   100
  
haftmann@60634
   101
lemma div_normalize [simp]:
haftmann@60634
   102
  "a div normalize a = unit_factor a"
haftmann@60634
   103
proof (cases "a = 0")
haftmann@60634
   104
  case True then show ?thesis by simp
haftmann@60634
   105
next
haftmann@60634
   106
  case False then have "normalize a \<noteq> 0" by simp 
haftmann@60634
   107
  with nonzero_mult_divide_cancel_right
haftmann@60634
   108
  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
haftmann@60634
   109
  then show ?thesis by simp
haftmann@60634
   110
qed
haftmann@60634
   111
haftmann@60634
   112
lemma div_unit_factor [simp]:
haftmann@60634
   113
  "a div unit_factor a = normalize a"
haftmann@60634
   114
proof (cases "a = 0")
haftmann@60634
   115
  case True then show ?thesis by simp
haftmann@60634
   116
next
haftmann@60634
   117
  case False then have "unit_factor a \<noteq> 0" by simp 
haftmann@60634
   118
  with nonzero_mult_divide_cancel_left
haftmann@60634
   119
  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
haftmann@60634
   120
  then show ?thesis by simp
haftmann@60634
   121
qed
haftmann@60634
   122
haftmann@60634
   123
lemma normalize_div [simp]:
haftmann@60634
   124
  "normalize a div a = 1 div unit_factor a"
haftmann@60634
   125
proof (cases "a = 0")
haftmann@60634
   126
  case True then show ?thesis by simp
haftmann@60634
   127
next
haftmann@60634
   128
  case False
haftmann@60634
   129
  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
haftmann@60634
   130
    by simp
haftmann@60634
   131
  also have "\<dots> = 1 div unit_factor a"
haftmann@60634
   132
    using False by (subst is_unit_divide_mult_cancel_right) simp_all
haftmann@60634
   133
  finally show ?thesis .
haftmann@60634
   134
qed
haftmann@60634
   135
haftmann@60634
   136
lemma mult_one_div_unit_factor [simp]:
haftmann@60634
   137
  "a * (1 div unit_factor b) = a div unit_factor b"
haftmann@60634
   138
  by (cases "b = 0") simp_all
haftmann@60634
   139
haftmann@60634
   140
lemma normalize_mult:
haftmann@60634
   141
  "normalize (a * b) = normalize a * normalize b"
haftmann@60634
   142
proof (cases "a = 0 \<or> b = 0")
haftmann@60634
   143
  case True then show ?thesis by auto
haftmann@60634
   144
next
haftmann@60634
   145
  case False
haftmann@60634
   146
  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
haftmann@60634
   147
  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
haftmann@60634
   148
  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
haftmann@60634
   149
  also have "\<dots> = a * b div unit_factor b div unit_factor a"
haftmann@60634
   150
    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
haftmann@60634
   151
  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
haftmann@60634
   152
    using False by (subst unit_div_mult_swap) simp_all
haftmann@60634
   153
  also have "\<dots> = normalize a * normalize b"
haftmann@60634
   154
    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
haftmann@60634
   155
  finally show ?thesis .
haftmann@60634
   156
qed
haftmann@60634
   157
 
haftmann@60634
   158
lemma unit_factor_idem [simp]:
haftmann@60634
   159
  "unit_factor (unit_factor a) = unit_factor a"
haftmann@60634
   160
  by (cases "a = 0") (auto intro: is_unit_unit_factor)
haftmann@60634
   161
haftmann@60634
   162
lemma normalize_unit_factor [simp]:
haftmann@60634
   163
  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
haftmann@60634
   164
  by (rule is_unit_normalize) simp
haftmann@60634
   165
  
haftmann@60634
   166
lemma normalize_idem [simp]:
haftmann@60634
   167
  "normalize (normalize a) = normalize a"
haftmann@60634
   168
proof (cases "a = 0")
haftmann@60634
   169
  case True then show ?thesis by simp
haftmann@60634
   170
next
haftmann@60634
   171
  case False
haftmann@60634
   172
  have "normalize a = normalize (unit_factor a * normalize a)" by simp
haftmann@60634
   173
  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
haftmann@60634
   174
    by (simp only: normalize_mult)
haftmann@60634
   175
  finally show ?thesis using False by simp_all
haftmann@60634
   176
qed
haftmann@60634
   177
haftmann@60634
   178
lemma unit_factor_normalize [simp]:
haftmann@60634
   179
  assumes "a \<noteq> 0"
haftmann@60634
   180
  shows "unit_factor (normalize a) = 1"
haftmann@60634
   181
proof -
haftmann@60634
   182
  from assms have "normalize a \<noteq> 0" by simp
haftmann@60634
   183
  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
haftmann@60634
   184
    by (simp only: unit_factor_mult_normalize)
haftmann@60634
   185
  then have "unit_factor (normalize a) * normalize a = normalize a"
haftmann@60634
   186
    by simp
haftmann@60634
   187
  with \<open>normalize a \<noteq> 0\<close>
haftmann@60634
   188
  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
haftmann@60634
   189
    by simp
haftmann@60634
   190
  with \<open>normalize a \<noteq> 0\<close>
haftmann@60634
   191
  show ?thesis by simp
haftmann@60634
   192
qed
haftmann@60634
   193
haftmann@60634
   194
lemma dvd_unit_factor_div:
haftmann@60634
   195
  assumes "b dvd a"
haftmann@60634
   196
  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
haftmann@60634
   197
proof -
haftmann@60634
   198
  from assms have "a = a div b * b"
haftmann@60634
   199
    by simp
haftmann@60634
   200
  then have "unit_factor a = unit_factor (a div b * b)"
haftmann@60634
   201
    by simp
haftmann@60634
   202
  then show ?thesis
haftmann@60634
   203
    by (cases "b = 0") (simp_all add: unit_factor_mult)
haftmann@60634
   204
qed
haftmann@60634
   205
haftmann@60634
   206
lemma dvd_normalize_div:
haftmann@60634
   207
  assumes "b dvd a"
haftmann@60634
   208
  shows "normalize (a div b) = normalize a div normalize b"
haftmann@60634
   209
proof -
haftmann@60634
   210
  from assms have "a = a div b * b"
haftmann@60634
   211
    by simp
haftmann@60634
   212
  then have "normalize a = normalize (a div b * b)"
haftmann@60634
   213
    by simp
haftmann@60634
   214
  then show ?thesis
haftmann@60634
   215
    by (cases "b = 0") (simp_all add: normalize_mult)
haftmann@60634
   216
qed
haftmann@60634
   217
haftmann@60634
   218
lemma normalize_dvd_iff [simp]:
haftmann@60634
   219
  "normalize a dvd b \<longleftrightarrow> a dvd b"
haftmann@60634
   220
proof -
haftmann@60634
   221
  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
haftmann@60634
   222
    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
haftmann@60634
   223
      by (cases "a = 0") simp_all
haftmann@60634
   224
  then show ?thesis by simp
haftmann@60634
   225
qed
haftmann@60634
   226
haftmann@60634
   227
lemma dvd_normalize_iff [simp]:
haftmann@60634
   228
  "a dvd normalize b \<longleftrightarrow> a dvd b"
haftmann@60634
   229
proof -
haftmann@60634
   230
  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
haftmann@60634
   231
    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
haftmann@60634
   232
      by (cases "b = 0") simp_all
haftmann@60634
   233
  then show ?thesis by simp
haftmann@60634
   234
qed
haftmann@60634
   235
haftmann@60634
   236
lemma associated_normalize_left [simp]:
haftmann@60634
   237
  "associated (normalize a) b \<longleftrightarrow> associated a b"
haftmann@60634
   238
  by (auto simp add: associated_def)
haftmann@60634
   239
haftmann@60634
   240
lemma associated_normalize_right [simp]:
haftmann@60634
   241
  "associated a (normalize b) \<longleftrightarrow> associated a b"
haftmann@60634
   242
  by (auto simp add: associated_def)
haftmann@60634
   243
haftmann@60634
   244
lemma associated_iff_normalize:
haftmann@60634
   245
  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
haftmann@60634
   246
proof (cases "a = 0 \<or> b = 0")
haftmann@60634
   247
  case True then show ?thesis by auto
haftmann@60634
   248
next
haftmann@60634
   249
  case False
haftmann@60634
   250
  show ?thesis
haftmann@60634
   251
  proof
haftmann@60634
   252
    assume ?P then show ?Q
haftmann@60634
   253
      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
haftmann@60634
   254
  next
haftmann@60634
   255
    from False have *: "is_unit (unit_factor a div unit_factor b)"
haftmann@60634
   256
      by auto
haftmann@60634
   257
    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
haftmann@60634
   258
      by simp
haftmann@60634
   259
    then have "a = unit_factor a * (b div unit_factor b)"
haftmann@60634
   260
      by simp
haftmann@60634
   261
    with False have "a = (unit_factor a div unit_factor b) * b"
haftmann@60634
   262
      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
haftmann@60634
   263
    with * show ?P 
haftmann@60634
   264
      by (rule is_unit_associatedI)
haftmann@60634
   265
  qed
haftmann@60634
   266
qed
haftmann@60634
   267
haftmann@60634
   268
lemma normalize_power:
haftmann@60634
   269
  "normalize (a ^ n) = normalize a ^ n"
haftmann@60634
   270
  by (induct n) (simp_all add: normalize_mult)
haftmann@60634
   271
haftmann@60634
   272
lemma unit_factor_power:
haftmann@60634
   273
  "unit_factor (a ^ n) = unit_factor a ^ n"
haftmann@60634
   274
  by (induct n) (simp_all add: unit_factor_mult)
haftmann@60634
   275
haftmann@60634
   276
lemma associated_eqI:
haftmann@60634
   277
  assumes "associated a b"
haftmann@60634
   278
  assumes "unit_factor a \<in> {0, 1}" and "unit_factor b \<in> {0, 1}"
haftmann@60634
   279
  shows "a = b"
haftmann@60634
   280
proof (cases "a = 0")
haftmann@60634
   281
  case True with assms show ?thesis by simp
haftmann@60634
   282
next
haftmann@60634
   283
  case False with assms have "b \<noteq> 0" by auto
haftmann@60634
   284
  with False assms have "unit_factor a = unit_factor b"
haftmann@60634
   285
    by simp
haftmann@60634
   286
  moreover from assms have "normalize a = normalize b"
haftmann@60634
   287
    by (simp add: associated_iff_normalize)
haftmann@60634
   288
  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
haftmann@60634
   289
    by simp
haftmann@60634
   290
  then show ?thesis
haftmann@60634
   291
    by simp
haftmann@60634
   292
qed
haftmann@60634
   293
haftmann@60634
   294
end
haftmann@60634
   295
haftmann@60634
   296
instantiation nat :: normalization_semidom
haftmann@60634
   297
begin
haftmann@60634
   298
haftmann@60634
   299
definition normalize_nat
haftmann@60634
   300
  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
haftmann@60634
   301
haftmann@60634
   302
definition unit_factor_nat
haftmann@60634
   303
  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
haftmann@60634
   304
haftmann@60634
   305
lemma unit_factor_simps [simp]:
haftmann@60634
   306
  "unit_factor 0 = (0::nat)"
haftmann@60634
   307
  "unit_factor (Suc n) = 1"
haftmann@60634
   308
  by (simp_all add: unit_factor_nat_def)
haftmann@60634
   309
haftmann@60634
   310
instance
haftmann@60634
   311
  by default (simp_all add: unit_factor_nat_def)
haftmann@60634
   312
  
haftmann@60634
   313
end
haftmann@60634
   314
haftmann@60634
   315
instantiation int :: normalization_semidom
haftmann@60634
   316
begin
haftmann@60634
   317
haftmann@60634
   318
definition normalize_int
haftmann@60634
   319
  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
haftmann@60634
   320
haftmann@60634
   321
definition unit_factor_int
haftmann@60634
   322
  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
haftmann@60634
   323
haftmann@60634
   324
instance
haftmann@60634
   325
proof
haftmann@60634
   326
  fix k :: int
haftmann@60634
   327
  assume "k \<noteq> 0"
haftmann@60634
   328
  then have "\<bar>sgn k\<bar> = 1"
haftmann@60634
   329
    by (cases "0::int" k rule: linorder_cases) simp_all
haftmann@60634
   330
  then show "is_unit (unit_factor k)"
haftmann@60634
   331
    by simp
haftmann@60634
   332
qed (simp_all add: sgn_times mult_sgn_abs)
haftmann@60634
   333
  
haftmann@60634
   334
end
haftmann@60634
   335
haftmann@60634
   336
end