1 

     2 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}

     3 

     4 theory LarryInt

     5 imports Nat "../Quotient" "../Quotient_Product"

     6 begin

     7 

     8 fun

     9   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 

    10 where

    11   "intrel (x, y) (u, v) = (x + v = u + y)"

    12 

    13 quotient_type int = "nat \<times> nat" / intrel

    14   by (auto simp add: equivp_def expand_fun_eq)

    15 

    16 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"

    17 begin

    18 

    19 quotient_definition

    20   Zero_int_def: "0::int" is "(0::nat, 0::nat)"

    21 

    22 quotient_definition

    23   One_int_def: "1::int" is "(1::nat, 0::nat)"

    24 

    25 definition

    26   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"

    27 

    28 quotient_definition

    29   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 

    30 is

    31   "add_raw"

    32 

    33 definition

    34   "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"

    35 

    36 quotient_definition

    37   "uminus :: int \<Rightarrow> int" 

    38 is

    39   "uminus_raw"

    40 

    41 fun

    42   mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"

    43 where

    44   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    45 

    46 quotient_definition

    47   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 

    48 is

    49   "mult_raw"

    50 

    51 definition

    52   "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"

    53 

    54 quotient_definition 

    55   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 

    56 is

    57   "le_raw"

    58 

    59 definition

    60   less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"

    61 

    62 definition

    63   diff_int_def:  "z - (w::int) \<equiv> z + (-w)"

    64 

    65 instance ..

    66 

    67 end

    68 

    69 subsection{*Construction of the Integers*}

    70 

    71 lemma zminus_zminus_raw:

    72   "uminus_raw (uminus_raw z) = z"

    73   by (cases z) (simp add: uminus_raw_def)

    74 

    75 lemma [quot_respect]:

    76   shows "(intrel ===> intrel) uminus_raw uminus_raw"

    77   by (simp add: uminus_raw_def)

    78   

    79 lemma zminus_zminus:

    80   fixes z::"int"

    81   shows "- (- z) = z"

    82   by(lifting zminus_zminus_raw)

    83 

    84 lemma zminus_0_raw:

    85   shows "uminus_raw (0, 0) = (0, 0::nat)"

    86   by (simp add: uminus_raw_def)

    87 

    88 lemma zminus_0: 

    89   shows "- 0 = (0::int)"

    90   by (lifting zminus_0_raw)

    91 

    92 subsection{*Integer Addition*}

    93 

    94 lemma zminus_zadd_distrib_raw:

    95   shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"

    96 by (cases z, cases w)

    97    (auto simp add: add_raw_def uminus_raw_def)

    98 

    99 lemma [quot_respect]:

   100   shows "(intrel ===> intrel ===> intrel) add_raw add_raw"

   101 by (simp add: add_raw_def)

   102 

   103 lemma zminus_zadd_distrib: 

   104   fixes z w::"int"

   105   shows "- (z + w) = (- z) + (- w)"

   106   by(lifting zminus_zadd_distrib_raw)

   107 

   108 lemma zadd_commute_raw:

   109   shows "add_raw z w = add_raw w z"

   110 by (cases z, cases w)

   111    (simp add: add_raw_def)

   112 

   113 lemma zadd_commute:

   114   fixes z w::"int"

   115   shows "(z::int) + w = w + z"

   116   by (lifting zadd_commute_raw)

   117 

   118 lemma zadd_assoc_raw:

   119   shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"

   120   by (cases z1, cases z2, cases z3) (simp add: add_raw_def)

   121 

   122 lemma zadd_assoc: 

   123   fixes z1 z2 z3::"int"

   124   shows "(z1 + z2) + z3 = z1 + (z2 + z3)"

   125   by (lifting zadd_assoc_raw)

   126 

   127 lemma zadd_0_raw:

   128   shows "add_raw (0, 0) z = z"

   129   by (simp add: add_raw_def)

   130 

   131 

   132 text {*also for the instance declaration int :: plus_ac0*}

   133 lemma zadd_0: 

   134   fixes z::"int"

   135   shows "0 + z = z"

   136   by (lifting zadd_0_raw)

   137 

   138 lemma zadd_zminus_inverse_raw:

   139   shows "intrel (add_raw (uminus_raw z) z) (0, 0)"

   140   by (cases z) (simp add: add_raw_def uminus_raw_def)

   141 

   142 lemma zadd_zminus_inverse2: 

   143   fixes z::"int"

   144   shows "(- z) + z = 0"

   145   by (lifting zadd_zminus_inverse_raw)

   146 

   147 subsection{*Integer Multiplication*}

   148 

   149 lemma zmult_zminus_raw:

   150   shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"

   151 apply(cases z, cases w)

   152 apply(simp add: uminus_raw_def)

   153 done

   154 

   155 lemma mult_raw_fst:

   156   assumes a: "intrel x z"

   157   shows "intrel (mult_raw x y) (mult_raw z y)"

   158 using a

   159 apply(cases x, cases y, cases z)

   160 apply(auto simp add: mult_raw.simps intrel.simps)

   161 apply(rename_tac u v w x y z)

   162 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

   163 apply(simp add: mult_ac)

   164 apply(simp add: add_mult_distrib [symmetric])

   165 done

   166 

   167 lemma mult_raw_snd:

   168   assumes a: "intrel x z"

   169   shows "intrel (mult_raw y x) (mult_raw y z)"

   170 using a

   171 apply(cases x, cases y, cases z)

   172 apply(auto simp add: mult_raw.simps intrel.simps)

   173 apply(rename_tac u v w x y z)

   174 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")

   175 apply(simp add: mult_ac)

   176 apply(simp add: add_mult_distrib [symmetric])

   177 done

   178 

   179 lemma [quot_respect]:

   180   shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"

   181 apply(simp only: fun_rel_def)

   182 apply(rule allI | rule impI)+

   183 apply(rule equivp_transp[OF int_equivp])

   184 apply(rule mult_raw_fst)

   185 apply(assumption)

   186 apply(rule mult_raw_snd)

   187 apply(assumption)

   188 done

   189 

   190 lemma zmult_zminus: 

   191   fixes z w::"int"

   192   shows "(- z) * w = - (z * w)"

   193   by (lifting zmult_zminus_raw)

   194 

   195 lemma zmult_commute_raw: 

   196   shows "mult_raw z w = mult_raw w z"

   197 apply(cases z, cases w)

   198 apply(simp add: add_ac mult_ac)

   199 done

   200 

   201 lemma zmult_commute: 

   202   fixes z w::"int"

   203   shows "z * w = w * z"

   204   by (lifting zmult_commute_raw)

   205 

   206 lemma zmult_assoc_raw:

   207   shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"

   208 apply(cases z1, cases z2, cases z3)

   209 apply(simp add: add_mult_distrib2 mult_ac)

   210 done

   211 

   212 lemma zmult_assoc: 

   213   fixes z1 z2 z3::"int"

   214   shows "(z1 * z2) * z3 = z1 * (z2 * z3)"

   215   by (lifting zmult_assoc_raw)

   216 

   217 lemma zadd_mult_distrib_raw:

   218   shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"

   219 apply(cases z1, cases z2, cases w)

   220 apply(simp add: add_mult_distrib2 mult_ac add_raw_def)

   221 done

   222 

   223 lemma zadd_zmult_distrib: 

   224   fixes z1 z2 w::"int"

   225   shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"

   226   by(lifting zadd_mult_distrib_raw)

   227 

   228 lemma zadd_zmult_distrib2: 

   229   fixes w z1 z2::"int"

   230   shows "w * (z1 + z2) = (w * z1) + (w * z2)"

   231   by (simp add: zmult_commute [of w] zadd_zmult_distrib)

   232 

   233 lemma zdiff_zmult_distrib: 

   234   fixes w z1 z2::"int"

   235   shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"

   236   by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)

   237 

   238 lemma zdiff_zmult_distrib2: 

   239   fixes w z1 z2::"int"

   240   shows "w * (z1 - z2) = (w * z1) - (w * z2)"

   241   by (simp add: zmult_commute [of w] zdiff_zmult_distrib)

   242 

   243 lemmas int_distrib =

   244   zadd_zmult_distrib zadd_zmult_distrib2

   245   zdiff_zmult_distrib zdiff_zmult_distrib2

   246 

   247 lemma zmult_1_raw:

   248   shows "mult_raw (1, 0) z = z"

   249   by (cases z) (auto)

   250 

   251 lemma zmult_1:

   252   fixes z::"int"

   253   shows "1 * z = z"

   254   by (lifting zmult_1_raw)

   255 

   256 lemma zmult_1_right: 

   257   fixes z::"int"

   258   shows "z * 1 = z"

   259   by (rule trans [OF zmult_commute zmult_1])

   260 

   261 lemma zero_not_one:

   262   shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"

   263   by auto

   264 

   265 text{*The Integers Form A Ring*}

   266 instance int :: comm_ring_1

   267 proof

   268   fix i j k :: int

   269   show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)

   270   show "i + j = j + i" by (simp add: zadd_commute)

   271   show "0 + i = i" by (rule zadd_0)

   272   show "- i + i = 0" by (rule zadd_zminus_inverse2)

   273   show "i - j = i + (-j)" by (simp add: diff_int_def)

   274   show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)

   275   show "i * j = j * i" by (rule zmult_commute)

   276   show "1 * i = i" by (rule zmult_1) 

   277   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)

   278   show "0 \<noteq> (1::int)" by (lifting zero_not_one)

   279 qed

   280 

   281 

   282 subsection{*The @{text "\<le>"} Ordering*}

   283 

   284 lemma zle_refl_raw:

   285   shows "le_raw w w"

   286   by (cases w) (simp add: le_raw_def)

   287 

   288 lemma [quot_respect]:

   289   shows "(intrel ===> intrel ===> op =) le_raw le_raw"

   290   by (auto) (simp_all add: le_raw_def)

   291 

   292 lemma zle_refl: 

   293   fixes w::"int"

   294   shows "w \<le> w"

   295   by (lifting zle_refl_raw)

   296 

   297 

   298 lemma zle_trans_raw:

   299   shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"

   300 apply(cases i, cases j, cases k)

   301 apply(auto simp add: le_raw_def)

   302 done

   303 

   304 lemma zle_trans: 

   305   fixes i j k::"int"

   306   shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"

   307   by (lifting zle_trans_raw)

   308 

   309 lemma zle_anti_sym_raw:

   310   shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"

   311 apply(cases z, cases w)

   312 apply(auto iff: le_raw_def)

   313 done

   314 

   315 lemma zle_anti_sym: 

   316   fixes z w::"int"

   317   shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"

   318   by (lifting zle_anti_sym_raw)

   319 

   320 

   321 (* Axiom 'order_less_le' of class 'order': *)

   322 lemma zless_le: 

   323   fixes w z::"int"

   324   shows "(w < z) = (w \<le> z & w \<noteq> z)"

   325   by (simp add: less_int_def)

   326 

   327 instance int :: order

   328 apply (default)

   329 apply(auto simp add: zless_le zle_anti_sym)[1]

   330 apply(rule zle_refl)

   331 apply(erule zle_trans, assumption)

   332 apply(erule zle_anti_sym, assumption)

   333 done

   334 

   335 (* Axiom 'linorder_linear' of class 'linorder': *)

   336 

   337 lemma zle_linear_raw:

   338   shows "le_raw z w \<or> le_raw w z"

   339 apply(cases w, cases z)

   340 apply(auto iff: le_raw_def)

   341 done

   342 

   343 lemma zle_linear: 

   344   fixes z w::"int"

   345   shows "z \<le> w \<or> w \<le> z"

   346   by (lifting zle_linear_raw)

   347 

   348 instance int :: linorder

   349 apply(default)

   350 apply(rule zle_linear)

   351 done

   352 

   353 lemma zadd_left_mono_raw:

   354   shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"

   355 apply(cases k)

   356 apply(auto simp add: add_raw_def le_raw_def)

   357 done

   358 

   359 lemma zadd_left_mono: 

   360   fixes i j::"int"

   361   shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"

   362   by (lifting zadd_left_mono_raw)

   363 

   364 

   365 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}

   366 

   367 definition

   368   "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"

   369 

   370 quotient_definition

   371   "nat2::int \<Rightarrow> nat"

   372 is

   373   "nat_raw"

   374 

   375 abbreviation

   376   "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"

   377 

   378 lemma nat_le_eq_zle_raw:

   379   shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"

   380   apply (cases w)

   381   apply (cases z)

   382   apply (simp add: nat_raw_def le_raw_def)

   383   by auto

   384 

   385 lemma [quot_respect]:

   386   shows "(intrel ===> op =) nat_raw nat_raw"

   387   by (auto iff: nat_raw_def)

   388 

   389 lemma nat_le_eq_zle: 

   390   fixes w z::"int"

   391   shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"

   392   unfolding less_int_def

   393   by (lifting nat_le_eq_zle_raw)

   394 

   395 end