src/HOL/Quotient_Examples/Quotient_Int.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40928 ace26e2cee91
child 41467 8fc17c5e11c0
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
kaliszyk@36524
     1
(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
kaliszyk@36524
     2
    Author:     Cezary Kaliszyk
kaliszyk@36524
     3
    Author:     Christian Urban
kaliszyk@36524
     4
kaliszyk@36524
     5
Integers based on Quotients, based on an older version by Larry Paulson.
kaliszyk@36524
     6
*)
kaliszyk@36524
     7
theory Quotient_Int
wenzelm@41413
     8
imports "~~/src/HOL/Library/Quotient_Product" Nat
kaliszyk@36524
     9
begin
kaliszyk@36524
    10
kaliszyk@36524
    11
fun
kaliszyk@36524
    12
  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
kaliszyk@36524
    13
where
kaliszyk@36524
    14
  "intrel (x, y) (u, v) = (x + v = u + y)"
kaliszyk@36524
    15
kaliszyk@36524
    16
quotient_type int = "nat \<times> nat" / intrel
nipkow@39302
    17
  by (auto simp add: equivp_def fun_eq_iff)
kaliszyk@36524
    18
kaliszyk@36524
    19
instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
kaliszyk@36524
    20
begin
kaliszyk@36524
    21
kaliszyk@36524
    22
quotient_definition
kaliszyk@36524
    23
  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
kaliszyk@36524
    24
kaliszyk@36524
    25
quotient_definition
kaliszyk@36524
    26
  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
kaliszyk@36524
    27
kaliszyk@36524
    28
fun
kaliszyk@36524
    29
  plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
kaliszyk@36524
    30
where
kaliszyk@36524
    31
  "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
kaliszyk@36524
    32
kaliszyk@36524
    33
quotient_definition
kaliszyk@36524
    34
  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
kaliszyk@36524
    35
kaliszyk@36524
    36
fun
kaliszyk@36524
    37
  uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
kaliszyk@36524
    38
where
kaliszyk@36524
    39
  "uminus_int_raw (x, y) = (y, x)"
kaliszyk@36524
    40
kaliszyk@36524
    41
quotient_definition
kaliszyk@36524
    42
  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
kaliszyk@36524
    43
kaliszyk@36524
    44
definition
haftmann@37767
    45
  minus_int_def:  "z - w = z + (-w\<Colon>int)"
kaliszyk@36524
    46
kaliszyk@36524
    47
fun
kaliszyk@36524
    48
  times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
kaliszyk@36524
    49
where
kaliszyk@36524
    50
  "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
kaliszyk@36524
    51
kaliszyk@36524
    52
quotient_definition
kaliszyk@36524
    53
  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
kaliszyk@36524
    54
kaliszyk@36524
    55
fun
kaliszyk@36524
    56
  le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
kaliszyk@36524
    57
where
kaliszyk@36524
    58
  "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
kaliszyk@36524
    59
kaliszyk@36524
    60
quotient_definition
kaliszyk@36524
    61
  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
kaliszyk@36524
    62
kaliszyk@36524
    63
definition
haftmann@37767
    64
  less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
kaliszyk@36524
    65
kaliszyk@36524
    66
definition
kaliszyk@36524
    67
  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
kaliszyk@36524
    68
kaliszyk@36524
    69
definition
kaliszyk@36524
    70
  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
kaliszyk@36524
    71
kaliszyk@36524
    72
instance ..
kaliszyk@36524
    73
kaliszyk@36524
    74
end
kaliszyk@36524
    75
kaliszyk@36524
    76
lemma [quot_respect]:
kaliszyk@36524
    77
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
kaliszyk@36524
    78
  and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
kaliszyk@36524
    79
  and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
haftmann@40468
    80
  by (auto intro!: fun_relI)
kaliszyk@36524
    81
kaliszyk@36524
    82
lemma times_int_raw_fst:
kaliszyk@36524
    83
  assumes a: "x \<approx> z"
kaliszyk@36524
    84
  shows "times_int_raw x y \<approx> times_int_raw z y"
kaliszyk@36524
    85
  using a
kaliszyk@36524
    86
  apply(cases x, cases y, cases z)
kaliszyk@36524
    87
  apply(auto simp add: times_int_raw.simps intrel.simps)
kaliszyk@36524
    88
  apply(rename_tac u v w x y z)
kaliszyk@36524
    89
  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
kaliszyk@36524
    90
  apply(simp add: mult_ac)
kaliszyk@36524
    91
  apply(simp add: add_mult_distrib [symmetric])
kaliszyk@36524
    92
  done
kaliszyk@36524
    93
kaliszyk@36524
    94
lemma times_int_raw_snd:
kaliszyk@36524
    95
  assumes a: "x \<approx> z"
kaliszyk@36524
    96
  shows "times_int_raw y x \<approx> times_int_raw y z"
kaliszyk@36524
    97
  using a
kaliszyk@36524
    98
  apply(cases x, cases y, cases z)
kaliszyk@36524
    99
  apply(auto simp add: times_int_raw.simps intrel.simps)
kaliszyk@36524
   100
  apply(rename_tac u v w x y z)
kaliszyk@36524
   101
  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
kaliszyk@36524
   102
  apply(simp add: mult_ac)
kaliszyk@36524
   103
  apply(simp add: add_mult_distrib [symmetric])
kaliszyk@36524
   104
  done
kaliszyk@36524
   105
kaliszyk@36524
   106
lemma [quot_respect]:
kaliszyk@36524
   107
  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
kaliszyk@36524
   108
  apply(simp only: fun_rel_def)
kaliszyk@36524
   109
  apply(rule allI | rule impI)+
kaliszyk@36524
   110
  apply(rule equivp_transp[OF int_equivp])
kaliszyk@36524
   111
  apply(rule times_int_raw_fst)
kaliszyk@36524
   112
  apply(assumption)
kaliszyk@36524
   113
  apply(rule times_int_raw_snd)
kaliszyk@36524
   114
  apply(assumption)
kaliszyk@36524
   115
  done
kaliszyk@36524
   116
kaliszyk@36524
   117
kaliszyk@36524
   118
text{* The integers form a @{text comm_ring_1}*}
kaliszyk@36524
   119
kaliszyk@36524
   120
instance int :: comm_ring_1
kaliszyk@36524
   121
proof
kaliszyk@36524
   122
  fix i j k :: int
kaliszyk@36524
   123
  show "(i + j) + k = i + (j + k)"
urbanc@37594
   124
    by (descending) (auto)
kaliszyk@36524
   125
  show "i + j = j + i"
urbanc@37594
   126
    by (descending) (auto)
kaliszyk@36524
   127
  show "0 + i = (i::int)"
urbanc@37594
   128
    by (descending) (auto)
kaliszyk@36524
   129
  show "- i + i = 0"
urbanc@37594
   130
    by (descending) (auto)
kaliszyk@36524
   131
  show "i - j = i + - j"
kaliszyk@36524
   132
    by (simp add: minus_int_def)
kaliszyk@36524
   133
  show "(i * j) * k = i * (j * k)"
urbanc@37594
   134
    by (descending) (auto simp add: algebra_simps)
kaliszyk@36524
   135
  show "i * j = j * i"
urbanc@37594
   136
    by (descending) (auto)
kaliszyk@36524
   137
  show "1 * i = i"
urbanc@37594
   138
    by (descending) (auto)
kaliszyk@36524
   139
  show "(i + j) * k = i * k + j * k"
urbanc@37594
   140
    by (descending) (auto simp add: algebra_simps)
kaliszyk@36524
   141
  show "0 \<noteq> (1::int)"
urbanc@37594
   142
    by (descending) (auto)
kaliszyk@36524
   143
qed
kaliszyk@36524
   144
kaliszyk@36524
   145
lemma plus_int_raw_rsp_aux:
kaliszyk@36524
   146
  assumes a: "a \<approx> b" "c \<approx> d"
kaliszyk@36524
   147
  shows "plus_int_raw a c \<approx> plus_int_raw b d"
kaliszyk@36524
   148
  using a
kaliszyk@36524
   149
  by (cases a, cases b, cases c, cases d)
kaliszyk@36524
   150
     (simp)
kaliszyk@36524
   151
kaliszyk@36524
   152
lemma add_abs_int:
kaliszyk@36524
   153
  "(abs_int (x,y)) + (abs_int (u,v)) =
kaliszyk@36524
   154
   (abs_int (x + u, y + v))"
kaliszyk@36524
   155
  apply(simp add: plus_int_def id_simps)
kaliszyk@36524
   156
  apply(fold plus_int_raw.simps)
kaliszyk@36524
   157
  apply(rule Quotient_rel_abs[OF Quotient_int])
kaliszyk@36524
   158
  apply(rule plus_int_raw_rsp_aux)
kaliszyk@36524
   159
  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
kaliszyk@36524
   160
  done
kaliszyk@36524
   161
kaliszyk@36524
   162
definition int_of_nat_raw:
kaliszyk@36524
   163
  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
kaliszyk@36524
   164
kaliszyk@36524
   165
quotient_definition
kaliszyk@36524
   166
  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
kaliszyk@36524
   167
kaliszyk@36524
   168
lemma[quot_respect]:
kaliszyk@36524
   169
  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
haftmann@40468
   170
  by (auto simp add: equivp_reflp [OF int_equivp])
kaliszyk@36524
   171
kaliszyk@36524
   172
lemma int_of_nat:
kaliszyk@36524
   173
  shows "of_nat m = int_of_nat m"
kaliszyk@36524
   174
  by (induct m)
kaliszyk@36524
   175
     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
kaliszyk@36524
   176
kaliszyk@36524
   177
instance int :: linorder
kaliszyk@36524
   178
proof
kaliszyk@36524
   179
  fix i j k :: int
kaliszyk@36524
   180
  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
urbanc@37594
   181
    by (descending) (auto)
kaliszyk@36524
   182
  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
kaliszyk@36524
   183
    by (auto simp add: less_int_def dest: antisym)
kaliszyk@36524
   184
  show "i \<le> i"
urbanc@37594
   185
    by (descending) (auto)
kaliszyk@36524
   186
  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
urbanc@37594
   187
    by (descending) (auto)
kaliszyk@36524
   188
  show "i \<le> j \<or> j \<le> i"
urbanc@37594
   189
    by (descending) (auto)
kaliszyk@36524
   190
qed
kaliszyk@36524
   191
kaliszyk@36524
   192
instantiation int :: distrib_lattice
kaliszyk@36524
   193
begin
kaliszyk@36524
   194
kaliszyk@36524
   195
definition
kaliszyk@36524
   196
  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
kaliszyk@36524
   197
kaliszyk@36524
   198
definition
kaliszyk@36524
   199
  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
kaliszyk@36524
   200
kaliszyk@36524
   201
instance
kaliszyk@36524
   202
  by default
kaliszyk@36524
   203
     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
kaliszyk@36524
   204
kaliszyk@36524
   205
end
kaliszyk@36524
   206
kaliszyk@36524
   207
instance int :: ordered_cancel_ab_semigroup_add
kaliszyk@36524
   208
proof
kaliszyk@36524
   209
  fix i j k :: int
kaliszyk@36524
   210
  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
urbanc@37594
   211
    by (descending) (auto)
kaliszyk@36524
   212
qed
kaliszyk@36524
   213
kaliszyk@36524
   214
abbreviation
kaliszyk@36524
   215
  "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
kaliszyk@36524
   216
kaliszyk@36524
   217
lemma zmult_zless_mono2_lemma:
kaliszyk@36524
   218
  fixes i j::int
kaliszyk@36524
   219
  and   k::nat
kaliszyk@36524
   220
  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
kaliszyk@36524
   221
  apply(induct "k")
kaliszyk@36524
   222
  apply(simp)
kaliszyk@36524
   223
  apply(case_tac "k = 0")
kaliszyk@36524
   224
  apply(simp_all add: left_distrib add_strict_mono)
kaliszyk@36524
   225
  done
kaliszyk@36524
   226
kaliszyk@36524
   227
lemma zero_le_imp_eq_int_raw:
kaliszyk@36524
   228
  fixes k::"(nat \<times> nat)"
kaliszyk@36524
   229
  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
kaliszyk@36524
   230
  apply(cases k)
kaliszyk@36524
   231
  apply(simp add:int_of_nat_raw)
kaliszyk@36524
   232
  apply(auto)
kaliszyk@36524
   233
  apply(rule_tac i="b" and j="a" in less_Suc_induct)
kaliszyk@36524
   234
  apply(auto)
kaliszyk@36524
   235
  done
kaliszyk@36524
   236
kaliszyk@36524
   237
lemma zero_le_imp_eq_int:
kaliszyk@36524
   238
  fixes k::int
kaliszyk@36524
   239
  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
kaliszyk@36524
   240
  unfolding less_int_def int_of_nat
urbanc@37594
   241
  by (descending) (rule zero_le_imp_eq_int_raw)
kaliszyk@36524
   242
kaliszyk@36524
   243
lemma zmult_zless_mono2:
kaliszyk@36524
   244
  fixes i j k::int
kaliszyk@36524
   245
  assumes a: "i < j" "0 < k"
kaliszyk@36524
   246
  shows "k * i < k * j"
kaliszyk@36524
   247
  using a
kaliszyk@36524
   248
  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
kaliszyk@36524
   249
kaliszyk@36524
   250
text{*The integers form an ordered integral domain*}
kaliszyk@36524
   251
kaliszyk@36524
   252
instance int :: linordered_idom
kaliszyk@36524
   253
proof
kaliszyk@36524
   254
  fix i j k :: int
kaliszyk@36524
   255
  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
kaliszyk@36524
   256
    by (rule zmult_zless_mono2)
kaliszyk@36524
   257
  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
kaliszyk@36524
   258
    by (simp only: zabs_def)
kaliszyk@36524
   259
  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
kaliszyk@36524
   260
    by (simp only: zsgn_def)
kaliszyk@36524
   261
qed
kaliszyk@36524
   262
kaliszyk@36524
   263
lemmas int_distrib =
kaliszyk@36524
   264
  left_distrib [of "z1::int" "z2" "w", standard]
kaliszyk@36524
   265
  right_distrib [of "w::int" "z1" "z2", standard]
kaliszyk@36524
   266
  left_diff_distrib [of "z1::int" "z2" "w", standard]
kaliszyk@36524
   267
  right_diff_distrib [of "w::int" "z1" "z2", standard]
kaliszyk@36524
   268
  minus_add_distrib[of "z1::int" "z2", standard]
kaliszyk@36524
   269
kaliszyk@36524
   270
lemma int_induct_raw:
kaliszyk@36524
   271
  assumes a: "P (0::nat, 0)"
kaliszyk@36524
   272
  and     b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
kaliszyk@36524
   273
  and     c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
kaliszyk@36524
   274
  shows      "P x"
kaliszyk@36524
   275
proof (cases x, clarify)
kaliszyk@36524
   276
  fix a b
kaliszyk@36524
   277
  show "P (a, b)"
krauss@40928
   278
  proof (induct a arbitrary: b rule: nat.induct)
kaliszyk@36524
   279
    case zero
kaliszyk@36524
   280
    show "P (0, b)" using assms by (induct b) auto
kaliszyk@36524
   281
  next
kaliszyk@36524
   282
    case (Suc n)
kaliszyk@36524
   283
    then show ?case using assms by auto
kaliszyk@36524
   284
  qed
kaliszyk@36524
   285
qed
kaliszyk@36524
   286
kaliszyk@36524
   287
lemma int_induct:
kaliszyk@36524
   288
  fixes x :: int
kaliszyk@36524
   289
  assumes a: "P 0"
kaliszyk@36524
   290
  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
kaliszyk@36524
   291
  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
kaliszyk@36524
   292
  shows      "P x"
kaliszyk@36524
   293
  using a b c unfolding minus_int_def
kaliszyk@36524
   294
  by (lifting int_induct_raw)
kaliszyk@36524
   295
kaliszyk@36524
   296
text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
kaliszyk@36524
   297
kaliszyk@36524
   298
definition
kaliszyk@36524
   299
  "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
kaliszyk@36524
   300
kaliszyk@36524
   301
quotient_definition
kaliszyk@36524
   302
  "int_to_nat::int \<Rightarrow> nat"
kaliszyk@36524
   303
is
kaliszyk@36524
   304
  "int_to_nat_raw"
kaliszyk@36524
   305
kaliszyk@36524
   306
lemma [quot_respect]:
kaliszyk@36524
   307
  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
kaliszyk@36524
   308
  by (auto iff: int_to_nat_raw_def)
kaliszyk@36524
   309
kaliszyk@36524
   310
lemma nat_le_eq_zle:
kaliszyk@36524
   311
  fixes w z::"int"
kaliszyk@36524
   312
  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
kaliszyk@36524
   313
  unfolding less_int_def
urbanc@37594
   314
  by (descending) (auto simp add: int_to_nat_raw_def)
kaliszyk@36524
   315
kaliszyk@36524
   316
end