1 

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

     3 

     4 theory LarryInt 

     5 imports Nat "../QuotMain"

     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 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_def 

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

    21 

    22 quotient_def

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

    24 

    25 quotient_def

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

    27 as 

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

    29 

    30 quotient_def

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

    32 as 

    33   "\<lambda>(x, y). (y::nat, x::nat)"

    34 

    35 fun

    36   mult_aux::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"

    37 where

    38   "mult_aux (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    39 

    40 quotient_def

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

    42 as 

    43   "mult_aux"

    44 

    45 quotient_def 

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

    47 as 

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

    49 

    50 definition

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

    52 

    53 definition

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

    55 

    56 instance ..

    57 

    58 end

    59 

    60 subsection{*Construction of the Integers*}

    61 

    62 abbreviation

    63   "uminus_aux \<equiv> \<lambda>(x, y). (y::nat, x::nat)"

    64 

    65 lemma zminus_zminus_aux:

    66   "uminus_aux (uminus_aux z) = z"

    67   by (cases z) (simp)

    68 

    69 lemma [quot_respect]:

    70   shows "(intrel ===> intrel) uminus_aux uminus_aux"

    71   by simp

    72   

    73 lemma zminus_zminus: 

    74   shows "- (- z) = (z::int)"

    75 apply(lifting zminus_zminus_aux)

    76 apply(injection)

    77 apply(rule quot_respect)

    78 apply(rule quot_respect)

    79 done

    80 (* PROBLEM *)

    81 

    82 lemma zminus_0_aux:

    83   shows "uminus_aux (0, 0) = (0, 0::nat)"

    84 by simp

    85 

    86 lemma zminus_0: "- 0 = (0::int)"

    87 apply(lifting zminus_0_aux)

    88 apply(injection)

    89 apply(rule quot_respect)

    90 done

    91 (* PROBLEM *)

    92 

    93 subsection{*Integer Addition*}

    94 

    95 definition

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

    97 

    98 lemma zminus_zadd_distrib_aux:

    99   shows "uminus_aux (add_aux z w) = add_aux (uminus_aux z) (uminus_aux w)"

   100 by (cases z, cases w)

   101    (auto simp add: add_aux_def)

   102 

   103 lemma [quot_respect]:

   104   shows "(intrel ===> intrel ===> intrel) 

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

   106 by simp

   107 

   108 lemma zminus_zadd_distrib: 

   109   shows "- (z + w) = (- z) + (- w::int)"

   110 apply(lifting zminus_zadd_distrib_aux[simplified add_aux_def])

   111 apply(injection)

   112 apply(rule quot_respect)+

   113 done

   114 (* PROBLEM *)

   115 

   116 lemma zadd_commute_aux:

   117   shows "add_aux z w = add_aux w z"

   118 by (cases z, cases w)

   119    (simp add: add_aux_def)

   120 

   121 lemma zadd_commute: 

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

   123 apply(lifting zadd_commute_aux[simplified add_aux_def])

   124 apply(injection)

   125 apply(rule quot_respect)+

   126 done

   127 (* PROBLEM *)

   128 

   129 lemma zadd_assoc_aux:

   130   shows "add_aux (add_aux z1 z2) z3 = add_aux z1 (add_aux z2 z3)"

   131 by (cases z1, cases z2, cases z3) (simp add: add_aux_def)

   132 

   133 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"

   134 apply(lifting zadd_assoc_aux[simplified add_aux_def])

   135 apply(injection)

   136 apply(rule quot_respect)+

   137 done

   138 (* PROBLEM *)

   139 

   140 lemma zadd_0_aux:

   141   fixes z::"nat \<times> nat"

   142   shows "add_aux (0, 0) z = z"

   143 by (simp add: add_aux_def)

   144 

   145 

   146 (*also for the instance declaration int :: plus_ac0*)

   147 lemma zadd_0: "(0::int) + z = z"

   148 apply(lifting zadd_0_aux[simplified add_aux_def])

   149 apply(injection)

   150 apply(rule quot_respect)+

   151 done

   152 

   153 lemma zadd_zminus_inverse_aux:

   154   shows "intrel (add_aux (uminus_aux z) z) (0, 0)"

   155 by (cases z) (simp add: add_aux_def)

   156 

   157 lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"

   158 apply(lifting zadd_zminus_inverse_aux[simplified add_aux_def])

   159 apply(injection)

   160 apply(rule quot_respect)+

   161 done

   162 

   163 subsection{*Integer Multiplication*}

   164 

   165 lemma zmult_zminus_aux:

   166   shows "mult_aux (uminus_aux z) w = uminus_aux (mult_aux z w)"

   167 apply(cases z, cases w)

   168 apply(simp)

   169 done

   170 

   171 lemma mult_aux_fst:

   172   assumes a: "intrel x z"

   173   shows "intrel (mult_aux x y) (mult_aux z y)"

   174 using a

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

   176 apply(auto simp add: mult_aux.simps intrel.simps)

   177 apply(rename_tac u v w x y z)

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

   179 apply(simp add: mult_ac)

   180 apply(simp add: add_mult_distrib [symmetric])

   181 done

   182 

   183 lemma mult_aux_snd:

   184   assumes a: "intrel x z"

   185   shows "intrel (mult_aux y x) (mult_aux y z)"

   186 using a

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

   188 apply(auto simp add: mult_aux.simps intrel.simps)

   189 apply(rename_tac u v w x y z)

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

   191 apply(simp add: mult_ac)

   192 apply(simp add: add_mult_distrib [symmetric])

   193 done

   194 

   195 lemma [quot_respect]:

   196   shows "(intrel ===> intrel ===> intrel) mult_aux mult_aux"

   197 apply(simp only: fun_rel.simps)

   198 apply(rule allI | rule impI)+

   199 apply(rule equivp_transp[OF int_equivp])

   200 apply(rule mult_aux_fst)

   201 apply(assumption)

   202 apply(rule mult_aux_snd)

   203 apply(assumption)

   204 done

   205 

   206 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"

   207 apply(lifting zmult_zminus_aux)

   208 apply(injection)

   209 apply(rule quot_respect)

   210 apply(rule quot_respect)

   211 done

   212 

   213 lemma zmult_commute_aux: 

   214   shows "mult_aux z w = mult_aux w z"

   215 apply(cases z, cases w)

   216 apply(simp add: add_ac mult_ac)

   217 done

   218 

   219 lemma zmult_commute: "(z::int) * w = w * z"

   220 by (lifting zmult_commute_aux)

   221 

   222 lemma zmult_assoc_aux:

   223   shows "mult_aux (mult_aux z1 z2) z3 = mult_aux z1 (mult_aux z2 z3)"

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

   225 apply(simp add: add_mult_distrib2 mult_ac)

   226 done

   227 

   228 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"

   229 by (lifting zmult_assoc_aux)

   230 

   231 lemma zadd_mult_distrib_aux:

   232   shows "mult_aux (add_aux z1 z2) w = add_aux (mult_aux z1 w) (mult_aux z2 w)"

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

   234 apply(simp add: add_mult_distrib2 mult_ac add_aux_def)

   235 done

   236 

   237 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"

   238 apply(lifting zadd_mult_distrib_aux[simplified add_aux_def])

   239 apply(injection)

   240 apply(rule quot_respect)+

   241 done

   242 

   243 lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"

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

   245 

   246 lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"

   247 by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)

   248 

   249 lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"

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

   251 

   252 lemmas int_distrib =

   253   zadd_zmult_distrib zadd_zmult_distrib2

   254   zdiff_zmult_distrib zdiff_zmult_distrib2

   255 

   256 lemma zmult_1_aux:

   257   shows "mult_aux (1, 0) z = z"

   258 apply(cases z)

   259 apply(auto)

   260 done

   261 

   262 lemma zmult_1: "(1::int) * z = z"

   263 apply(lifting zmult_1_aux)

   264 done

   265 

   266 lemma zmult_1_right: "z * (1::int) = z"

   267 by (rule trans [OF zmult_commute zmult_1])

   268 

   269 lemma zero_not_one:

   270   shows "(0, 0) \<noteq> (1::nat, 0::nat)"

   271 by simp

   272 

   273 text{*The Integers Form A Ring*}

   274 instance int :: comm_ring_1

   275 proof

   276   fix i j k :: int

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

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

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

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

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

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

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

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

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

   286   show "0 \<noteq> (1::int)" 

   287     by (lifting zero_not_one) (auto) (* PROBLEM? regularize failed *)

   288 qed

   289 

   290 

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

   292 

   293 abbreviation

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

   295 

   296 lemma zle_refl_aux:

   297   "le_aux w w"

   298 apply(cases w)

   299 apply(simp)

   300 done

   301 

   302 lemma [quot_respect]:

   303   shows "(intrel ===> intrel ===> op =) le_aux le_aux"

   304 by auto

   305 

   306 lemma zle_refl: "w \<le> (w::int)"

   307 apply(lifting zle_refl_aux)

   308 apply(injection)

   309 apply(rule quot_respect)

   310 done

   311 (* PROBLEM *)

   312 

   313 lemma zle_trans_aux:

   314   shows "\<lbrakk>le_aux i j; le_aux j k\<rbrakk> \<Longrightarrow> le_aux i k"

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

   316 apply(auto)

   317 done

   318 

   319 lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"

   320 apply(lifting zle_trans_aux)

   321 apply(injection)

   322 apply(rule quot_respect)+

   323 done

   324 (* PROBLEM *)

   325 

   326 lemma zle_anti_sym_aux:

   327   shows "\<lbrakk>le_aux z w; le_aux w z\<rbrakk> \<Longrightarrow> intrel z w"

   328 apply(cases z, cases w)

   329 apply(auto)

   330 done

   331 

   332 lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"

   333 apply(lifting zle_anti_sym_aux)

   334 apply(injection)

   335 apply(rule quot_respect)+

   336 done

   337 (* PROBLEM *)

   338 

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

   340 lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"

   341 by (simp add: less_int_def)

   342 

   343 instance int :: order

   344 apply(intro_classes)

   345 apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)

   346 done

   347 

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

   349 

   350 lemma zle_linear_aux:

   351   "le_aux z w \<or> le_aux w z"

   352 apply(cases w, cases z)

   353 apply(auto)

   354 done

   355 

   356 

   357 lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"

   358 apply(lifting zle_linear_aux)

   359 apply(injection)

   360 apply(rule quot_respect)+

   361 done

   362 

   363 instance int :: linorder

   364 proof qed (rule zle_linear)

   365 

   366 lemma zadd_left_mono_aux:

   367   shows "le_aux i j \<Longrightarrow> le_aux (add_aux k i) (add_aux k j)"

   368 apply(cases k)

   369 apply(auto simp add: add_aux_def)

   370 done

   371 

   372 lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"

   373 apply(lifting zadd_left_mono_aux[simplified add_aux_def])

   374 apply(injection)

   375 apply(rule quot_respect)+

   376 done

   377 (* PROBLEM *)

   378 

   379 

   380 

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

   382 

   383 (* PROBLEM: this has to be a definition, not an abbreviation *)

   384 (* otherwise the lemma nat_le_eq_zle cannot be lifted        *)

   385 fun

   386   nat_aux

   387 where

   388   "nat_aux (x, y) =  x - (y::nat)"

   389 

   390 quotient_def

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

   392 as

   393   "nat_aux"

   394 

   395 abbreviation

   396   "less_aux x y \<equiv> (le_aux x y \<and> \<not>(x = y))"

   397 

   398 lemma nat_le_eq_zle_aux:

   399   shows "less_aux (0, 0) w \<or> le_aux (0, 0) z \<Longrightarrow> (nat_aux w \<le> nat_aux z) = (le_aux w z)"

   400 apply(auto)

   401 sorry

   402 

   403 lemma [quot_respect]:

   404   shows "(intrel ===> op =) nat_aux nat_aux"

   405 apply(auto)

   406 done

   407 

   408 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"

   409 unfolding less_int_def

   410 apply(lifting nat_le_eq_zle_aux)

   411 apply(injection)

   412 apply(simp_all only: quot_respect)

   413 done

   414 (* PROBLEM *)

   415 

   416 end