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