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