src/ZF/Int_ZF.thy
author nipkow
Wed Aug 10 09:33:54 2016 +0200 (2016-08-10)
changeset 63648 f9f3006a5579
parent 61798 27f3c10b0b50
child 67443 3abf6a722518
permissions -rw-r--r--
"split add" -> "split"
     1 (*  Title:      ZF/Int_ZF.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 section\<open>The Integers as Equivalence Classes Over Pairs of Natural Numbers\<close>
     7 
     8 theory Int_ZF imports EquivClass ArithSimp begin
     9 
    10 definition
    11   intrel :: i  where
    12     "intrel == {p \<in> (nat*nat)*(nat*nat).
    13                 \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    14 
    15 definition
    16   int :: i  where
    17     "int == (nat*nat)//intrel"
    18 
    19 definition
    20   int_of :: "i=>i" \<comment>\<open>coercion from nat to int\<close>    ("$# _" [80] 80)  where
    21     "$# m == intrel `` {<natify(m), 0>}"
    22 
    23 definition
    24   intify :: "i=>i" \<comment>\<open>coercion from ANYTHING to int\<close>  where
    25     "intify(m) == if m \<in> int then m else $#0"
    26 
    27 definition
    28   raw_zminus :: "i=>i"  where
    29     "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"
    30 
    31 definition
    32   zminus :: "i=>i"                                 ("$- _" [80] 80)  where
    33     "$- z == raw_zminus (intify(z))"
    34 
    35 definition
    36   znegative   ::      "i=>o"  where
    37     "znegative(z) == \<exists>x y. x<y & y\<in>nat & <x,y>\<in>z"
    38 
    39 definition
    40   iszero      ::      "i=>o"  where
    41     "iszero(z) == z = $# 0"
    42 
    43 definition
    44   raw_nat_of  :: "i=>i"  where
    45   "raw_nat_of(z) == natify (\<Union><x,y>\<in>z. x#-y)"
    46 
    47 definition
    48   nat_of  :: "i=>i"  where
    49   "nat_of(z) == raw_nat_of (intify(z))"
    50 
    51 definition
    52   zmagnitude  ::      "i=>i"  where
    53   \<comment>\<open>could be replaced by an absolute value function from int to int?\<close>
    54     "zmagnitude(z) ==
    55      THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
    56                        (znegative(z) & $- z = $# m))"
    57 
    58 definition
    59   raw_zmult   ::      "[i,i]=>i"  where
    60     (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    61       Perhaps a "curried" or even polymorphic congruent predicate would be
    62       better.*)
    63      "raw_zmult(z1,z2) ==
    64        \<Union>p1\<in>z1. \<Union>p2\<in>z2.  split(%x1 y1. split(%x2 y2.
    65                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    66 
    67 definition
    68   zmult       ::      "[i,i]=>i"      (infixl "$*" 70)  where
    69      "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    70 
    71 definition
    72   raw_zadd    ::      "[i,i]=>i"  where
    73      "raw_zadd (z1, z2) ==
    74        \<Union>z1\<in>z1. \<Union>z2\<in>z2. let <x1,y1>=z1; <x2,y2>=z2
    75                            in intrel``{<x1#+x2, y1#+y2>}"
    76 
    77 definition
    78   zadd        ::      "[i,i]=>i"      (infixl "$+" 65)  where
    79      "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    80 
    81 definition
    82   zdiff        ::      "[i,i]=>i"      (infixl "$-" 65)  where
    83      "z1 $- z2 == z1 $+ zminus(z2)"
    84 
    85 definition
    86   zless        ::      "[i,i]=>o"      (infixl "$<" 50)  where
    87      "z1 $< z2 == znegative(z1 $- z2)"
    88 
    89 definition
    90   zle          ::      "[i,i]=>o"      (infixl "$\<le>" 50)  where
    91      "z1 $\<le> z2 == z1 $< z2 | intify(z1)=intify(z2)"
    92 
    93 
    94 declare quotientE [elim!]
    95 
    96 subsection\<open>Proving that @{term intrel} is an equivalence relation\<close>
    97 
    98 (** Natural deduction for intrel **)
    99 
   100 lemma intrel_iff [simp]:
   101     "<<x1,y1>,<x2,y2>>: intrel \<longleftrightarrow>
   102      x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
   103 by (simp add: intrel_def)
   104 
   105 lemma intrelI [intro!]:
   106     "[| x1#+y2 = x2#+y1; x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |]
   107      ==> <<x1,y1>,<x2,y2>>: intrel"
   108 by (simp add: intrel_def)
   109 
   110 lemma intrelE [elim!]:
   111   "[| p \<in> intrel;
   112       !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1;
   113                         x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] ==> Q |]
   114    ==> Q"
   115 by (simp add: intrel_def, blast)
   116 
   117 lemma int_trans_lemma:
   118      "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1"
   119 apply (rule sym)
   120 apply (erule add_left_cancel)+
   121 apply (simp_all (no_asm_simp))
   122 done
   123 
   124 lemma equiv_intrel: "equiv(nat*nat, intrel)"
   125 apply (simp add: equiv_def refl_def sym_def trans_def)
   126 apply (fast elim!: sym int_trans_lemma)
   127 done
   128 
   129 lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} \<in> int"
   130 by (simp add: int_def)
   131 
   132 declare equiv_intrel [THEN eq_equiv_class_iff, simp]
   133 declare conj_cong [cong]
   134 
   135 lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel]
   136 
   137 (** int_of: the injection from nat to int **)
   138 
   139 lemma int_of_type [simp,TC]: "$#m \<in> int"
   140 by (simp add: int_def quotient_def int_of_def, auto)
   141 
   142 lemma int_of_eq [iff]: "($# m = $# n) \<longleftrightarrow> natify(m)=natify(n)"
   143 by (simp add: int_of_def)
   144 
   145 lemma int_of_inject: "[| $#m = $#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
   146 by (drule int_of_eq [THEN iffD1], auto)
   147 
   148 
   149 (** intify: coercion from anything to int **)
   150 
   151 lemma intify_in_int [iff,TC]: "intify(x) \<in> int"
   152 by (simp add: intify_def)
   153 
   154 lemma intify_ident [simp]: "n \<in> int ==> intify(n) = n"
   155 by (simp add: intify_def)
   156 
   157 
   158 subsection\<open>Collapsing rules: to remove @{term intify}
   159             from arithmetic expressions\<close>
   160 
   161 lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
   162 by simp
   163 
   164 lemma int_of_natify [simp]: "$# (natify(m)) = $# m"
   165 by (simp add: int_of_def)
   166 
   167 lemma zminus_intify [simp]: "$- (intify(m)) = $- m"
   168 by (simp add: zminus_def)
   169 
   170 (** Addition **)
   171 
   172 lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y"
   173 by (simp add: zadd_def)
   174 
   175 lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y"
   176 by (simp add: zadd_def)
   177 
   178 (** Subtraction **)
   179 
   180 lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y"
   181 by (simp add: zdiff_def)
   182 
   183 lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y"
   184 by (simp add: zdiff_def)
   185 
   186 (** Multiplication **)
   187 
   188 lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y"
   189 by (simp add: zmult_def)
   190 
   191 lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y"
   192 by (simp add: zmult_def)
   193 
   194 (** Orderings **)
   195 
   196 lemma zless_intify1 [simp]:"intify(x) $< y \<longleftrightarrow> x $< y"
   197 by (simp add: zless_def)
   198 
   199 lemma zless_intify2 [simp]:"x $< intify(y) \<longleftrightarrow> x $< y"
   200 by (simp add: zless_def)
   201 
   202 lemma zle_intify1 [simp]:"intify(x) $\<le> y \<longleftrightarrow> x $\<le> y"
   203 by (simp add: zle_def)
   204 
   205 lemma zle_intify2 [simp]:"x $\<le> intify(y) \<longleftrightarrow> x $\<le> y"
   206 by (simp add: zle_def)
   207 
   208 
   209 subsection\<open>@{term zminus}: unary negation on @{term int}\<close>
   210 
   211 lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
   212 by (auto simp add: congruent_def add_ac)
   213 
   214 lemma raw_zminus_type: "z \<in> int ==> raw_zminus(z) \<in> int"
   215 apply (simp add: int_def raw_zminus_def)
   216 apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
   217 done
   218 
   219 lemma zminus_type [TC,iff]: "$-z \<in> int"
   220 by (simp add: zminus_def raw_zminus_type)
   221 
   222 lemma raw_zminus_inject:
   223      "[| raw_zminus(z) = raw_zminus(w);  z \<in> int;  w \<in> int |] ==> z=w"
   224 apply (simp add: int_def raw_zminus_def)
   225 apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe)
   226 apply (auto dest: eq_intrelD simp add: add_ac)
   227 done
   228 
   229 lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)"
   230 apply (simp add: zminus_def)
   231 apply (blast dest!: raw_zminus_inject)
   232 done
   233 
   234 lemma zminus_inject: "[| $-z = $-w;  z \<in> int;  w \<in> int |] ==> z=w"
   235 by auto
   236 
   237 lemma raw_zminus:
   238     "[| x\<in>nat;  y\<in>nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}"
   239 apply (simp add: raw_zminus_def UN_equiv_class [OF equiv_intrel zminus_congruent])
   240 done
   241 
   242 lemma zminus:
   243     "[| x\<in>nat;  y\<in>nat |]
   244      ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}"
   245 by (simp add: zminus_def raw_zminus image_intrel_int)
   246 
   247 lemma raw_zminus_zminus: "z \<in> int ==> raw_zminus (raw_zminus(z)) = z"
   248 by (auto simp add: int_def raw_zminus)
   249 
   250 lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)"
   251 by (simp add: zminus_def raw_zminus_type raw_zminus_zminus)
   252 
   253 lemma zminus_int0 [simp]: "$- ($#0) = $#0"
   254 by (simp add: int_of_def zminus)
   255 
   256 lemma zminus_zminus: "z \<in> int ==> $- ($- z) = z"
   257 by simp
   258 
   259 
   260 subsection\<open>@{term znegative}: the test for negative integers\<close>
   261 
   262 lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) \<longleftrightarrow> x<y"
   263 apply (cases "x<y")
   264 apply (auto simp add: znegative_def not_lt_iff_le)
   265 apply (subgoal_tac "y #+ x2 < x #+ y2", force)
   266 apply (rule add_le_lt_mono, auto)
   267 done
   268 
   269 (*No natural number is negative!*)
   270 lemma not_znegative_int_of [iff]: "~ znegative($# n)"
   271 by (simp add: znegative int_of_def)
   272 
   273 lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))"
   274 by (simp add: znegative int_of_def zminus natify_succ)
   275 
   276 lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0"
   277 by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym])
   278 
   279 
   280 subsection\<open>@{term nat_of}: Coercion of an Integer to a Natural Number\<close>
   281 
   282 lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
   283 by (simp add: nat_of_def)
   284 
   285 lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
   286 by (auto simp add: congruent_def split: nat_diff_split)
   287 
   288 lemma raw_nat_of:
   289     "[| x\<in>nat;  y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
   290 by (simp add: raw_nat_of_def UN_equiv_class [OF equiv_intrel nat_of_congruent])
   291 
   292 lemma raw_nat_of_int_of: "raw_nat_of($# n) = natify(n)"
   293 by (simp add: int_of_def raw_nat_of)
   294 
   295 lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)"
   296 by (simp add: raw_nat_of_int_of nat_of_def)
   297 
   298 lemma raw_nat_of_type: "raw_nat_of(z) \<in> nat"
   299 by (simp add: raw_nat_of_def)
   300 
   301 lemma nat_of_type [iff,TC]: "nat_of(z) \<in> nat"
   302 by (simp add: nat_of_def raw_nat_of_type)
   303 
   304 subsection\<open>zmagnitude: magnitide of an integer, as a natural number\<close>
   305 
   306 lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)"
   307 by (auto simp add: zmagnitude_def int_of_eq)
   308 
   309 lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n"
   310 apply (drule sym)
   311 apply (simp (no_asm_simp) add: int_of_eq)
   312 done
   313 
   314 lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)"
   315 apply (simp add: zmagnitude_def)
   316 apply (rule the_equality)
   317 apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
   318             iff del: int_of_eq, auto)
   319 done
   320 
   321 lemma zmagnitude_type [iff,TC]: "zmagnitude(z)\<in>nat"
   322 apply (simp add: zmagnitude_def)
   323 apply (rule theI2, auto)
   324 done
   325 
   326 lemma not_zneg_int_of:
   327      "[| z \<in> int; ~ znegative(z) |] ==> \<exists>n\<in>nat. z = $# n"
   328 apply (auto simp add: int_def znegative int_of_def not_lt_iff_le)
   329 apply (rename_tac x y)
   330 apply (rule_tac x="x#-y" in bexI)
   331 apply (auto simp add: add_diff_inverse2)
   332 done
   333 
   334 lemma not_zneg_mag [simp]:
   335      "[| z \<in> int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"
   336 by (drule not_zneg_int_of, auto)
   337 
   338 lemma zneg_int_of:
   339      "[| znegative(z); z \<in> int |] ==> \<exists>n\<in>nat. z = $- ($# succ(n))"
   340 by (auto simp add: int_def znegative zminus int_of_def dest!: less_imp_succ_add)
   341 
   342 lemma zneg_mag [simp]:
   343      "[| znegative(z); z \<in> int |] ==> $# (zmagnitude(z)) = $- z"
   344 by (drule zneg_int_of, auto)
   345 
   346 lemma int_cases: "z \<in> int ==> \<exists>n\<in>nat. z = $# n | z = $- ($# succ(n))"
   347 apply (case_tac "znegative (z) ")
   348 prefer 2 apply (blast dest: not_zneg_mag sym)
   349 apply (blast dest: zneg_int_of)
   350 done
   351 
   352 lemma not_zneg_raw_nat_of:
   353      "[| ~ znegative(z); z \<in> int |] ==> $# (raw_nat_of(z)) = z"
   354 apply (drule not_zneg_int_of)
   355 apply (auto simp add: raw_nat_of_type raw_nat_of_int_of)
   356 done
   357 
   358 lemma not_zneg_nat_of_intify:
   359      "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)"
   360 by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of)
   361 
   362 lemma not_zneg_nat_of: "[| ~ znegative(z); z \<in> int |] ==> $# (nat_of(z)) = z"
   363 apply (simp (no_asm_simp) add: not_zneg_nat_of_intify)
   364 done
   365 
   366 lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0"
   367 apply (subgoal_tac "intify(z) \<in> int")
   368 apply (simp add: int_def)
   369 apply (auto simp add: znegative nat_of_def raw_nat_of
   370             split: nat_diff_split)
   371 done
   372 
   373 
   374 subsection\<open>@{term zadd}: addition on int\<close>
   375 
   376 text\<open>Congruence Property for Addition\<close>
   377 lemma zadd_congruent2:
   378     "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2
   379                             in intrel``{<x1#+x2, y1#+y2>})
   380      respects2 intrel"
   381 apply (simp add: congruent2_def)
   382 (*Proof via congruent2_commuteI seems longer*)
   383 apply safe
   384 apply (simp (no_asm_simp) add: add_assoc Let_def)
   385 (*The rest should be trivial, but rearranging terms is hard
   386   add_ac does not help rewriting with the assumptions.*)
   387 apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst])
   388 apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst])
   389 apply (simp (no_asm_simp) add: add_assoc [symmetric])
   390 done
   391 
   392 lemma raw_zadd_type: "[| z \<in> int;  w \<in> int |] ==> raw_zadd(z,w) \<in> int"
   393 apply (simp add: int_def raw_zadd_def)
   394 apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
   395 apply (simp add: Let_def)
   396 done
   397 
   398 lemma zadd_type [iff,TC]: "z $+ w \<in> int"
   399 by (simp add: zadd_def raw_zadd_type)
   400 
   401 lemma raw_zadd:
   402   "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
   403    ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
   404        intrel `` {<x1#+x2, y1#+y2>}"
   405 apply (simp add: raw_zadd_def
   406              UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2])
   407 apply (simp add: Let_def)
   408 done
   409 
   410 lemma zadd:
   411   "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
   412    ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =
   413        intrel `` {<x1#+x2, y1#+y2>}"
   414 by (simp add: zadd_def raw_zadd image_intrel_int)
   415 
   416 lemma raw_zadd_int0: "z \<in> int ==> raw_zadd ($#0,z) = z"
   417 by (auto simp add: int_def int_of_def raw_zadd)
   418 
   419 lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)"
   420 by (simp add: zadd_def raw_zadd_int0)
   421 
   422 lemma zadd_int0: "z \<in> int ==> $#0 $+ z = z"
   423 by simp
   424 
   425 lemma raw_zminus_zadd_distrib:
   426      "[| z \<in> int;  w \<in> int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)"
   427 by (auto simp add: zminus raw_zadd int_def)
   428 
   429 lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w"
   430 by (simp add: zadd_def raw_zminus_zadd_distrib)
   431 
   432 lemma raw_zadd_commute:
   433      "[| z \<in> int;  w \<in> int |] ==> raw_zadd(z,w) = raw_zadd(w,z)"
   434 by (auto simp add: raw_zadd add_ac int_def)
   435 
   436 lemma zadd_commute: "z $+ w = w $+ z"
   437 by (simp add: zadd_def raw_zadd_commute)
   438 
   439 lemma raw_zadd_assoc:
   440     "[| z1: int;  z2: int;  z3: int |]
   441      ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))"
   442 by (auto simp add: int_def raw_zadd add_assoc)
   443 
   444 lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"
   445 by (simp add: zadd_def raw_zadd_type raw_zadd_assoc)
   446 
   447 (*For AC rewriting*)
   448 lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)"
   449 apply (simp add: zadd_assoc [symmetric])
   450 apply (simp add: zadd_commute)
   451 done
   452 
   453 (*Integer addition is an AC operator*)
   454 lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
   455 
   456 lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)"
   457 by (simp add: int_of_def zadd)
   458 
   459 lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)"
   460 by (simp add: int_of_add [symmetric] natify_succ)
   461 
   462 lemma int_of_diff:
   463      "[| m\<in>nat;  n \<le> m |] ==> $# (m #- n) = ($#m) $- ($#n)"
   464 apply (simp add: int_of_def zdiff_def)
   465 apply (frule lt_nat_in_nat)
   466 apply (simp_all add: zadd zminus add_diff_inverse2)
   467 done
   468 
   469 lemma raw_zadd_zminus_inverse: "z \<in> int ==> raw_zadd (z, $- z) = $#0"
   470 by (auto simp add: int_def int_of_def zminus raw_zadd add_commute)
   471 
   472 lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0"
   473 apply (simp add: zadd_def)
   474 apply (subst zminus_intify [symmetric])
   475 apply (rule intify_in_int [THEN raw_zadd_zminus_inverse])
   476 done
   477 
   478 lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0"
   479 by (simp add: zadd_commute zadd_zminus_inverse)
   480 
   481 lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)"
   482 by (rule trans [OF zadd_commute zadd_int0_intify])
   483 
   484 lemma zadd_int0_right: "z \<in> int ==> z $+ $#0 = z"
   485 by simp
   486 
   487 
   488 subsection\<open>@{term zmult}: Integer Multiplication\<close>
   489 
   490 text\<open>Congruence property for multiplication\<close>
   491 lemma zmult_congruent2:
   492     "(%p1 p2. split(%x1 y1. split(%x2 y2.
   493                     intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))
   494      respects2 intrel"
   495 apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
   496 (*Proof that zmult is congruent in one argument*)
   497 apply (rename_tac x y)
   498 apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context])
   499 apply (drule_tac t = "%u. y#*u" in subst_context)
   500 apply (erule add_left_cancel)+
   501 apply (simp_all add: add_mult_distrib_left)
   502 done
   503 
   504 
   505 lemma raw_zmult_type: "[| z \<in> int;  w \<in> int |] ==> raw_zmult(z,w) \<in> int"
   506 apply (simp add: int_def raw_zmult_def)
   507 apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
   508 apply (simp add: Let_def)
   509 done
   510 
   511 lemma zmult_type [iff,TC]: "z $* w \<in> int"
   512 by (simp add: zmult_def raw_zmult_type)
   513 
   514 lemma raw_zmult:
   515      "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
   516       ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
   517           intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   518 by (simp add: raw_zmult_def
   519            UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2])
   520 
   521 lemma zmult:
   522      "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
   523       ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =
   524           intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   525 by (simp add: zmult_def raw_zmult image_intrel_int)
   526 
   527 lemma raw_zmult_int0: "z \<in> int ==> raw_zmult ($#0,z) = $#0"
   528 by (auto simp add: int_def int_of_def raw_zmult)
   529 
   530 lemma zmult_int0 [simp]: "$#0 $* z = $#0"
   531 by (simp add: zmult_def raw_zmult_int0)
   532 
   533 lemma raw_zmult_int1: "z \<in> int ==> raw_zmult ($#1,z) = z"
   534 by (auto simp add: int_def int_of_def raw_zmult)
   535 
   536 lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)"
   537 by (simp add: zmult_def raw_zmult_int1)
   538 
   539 lemma zmult_int1: "z \<in> int ==> $#1 $* z = z"
   540 by simp
   541 
   542 lemma raw_zmult_commute:
   543      "[| z \<in> int;  w \<in> int |] ==> raw_zmult(z,w) = raw_zmult(w,z)"
   544 by (auto simp add: int_def raw_zmult add_ac mult_ac)
   545 
   546 lemma zmult_commute: "z $* w = w $* z"
   547 by (simp add: zmult_def raw_zmult_commute)
   548 
   549 lemma raw_zmult_zminus:
   550      "[| z \<in> int;  w \<in> int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)"
   551 by (auto simp add: int_def zminus raw_zmult add_ac)
   552 
   553 lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)"
   554 apply (simp add: zmult_def raw_zmult_zminus)
   555 apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto)
   556 done
   557 
   558 lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)"
   559 by (simp add: zmult_commute [of w])
   560 
   561 lemma raw_zmult_assoc:
   562     "[| z1: int;  z2: int;  z3: int |]
   563      ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))"
   564 by (auto simp add: int_def raw_zmult add_mult_distrib_left add_ac mult_ac)
   565 
   566 lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)"
   567 by (simp add: zmult_def raw_zmult_type raw_zmult_assoc)
   568 
   569 (*For AC rewriting*)
   570 lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)"
   571 apply (simp add: zmult_assoc [symmetric])
   572 apply (simp add: zmult_commute)
   573 done
   574 
   575 (*Integer multiplication is an AC operator*)
   576 lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
   577 
   578 lemma raw_zadd_zmult_distrib:
   579     "[| z1: int;  z2: int;  w \<in> int |]
   580      ==> raw_zmult(raw_zadd(z1,z2), w) =
   581          raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))"
   582 by (auto simp add: int_def raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac)
   583 
   584 lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"
   585 by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type
   586               raw_zadd_zmult_distrib)
   587 
   588 lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)"
   589 by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   590 
   591 lemmas int_typechecks =
   592   int_of_type zminus_type zmagnitude_type zadd_type zmult_type
   593 
   594 
   595 (*** Subtraction laws ***)
   596 
   597 lemma zdiff_type [iff,TC]: "z $- w \<in> int"
   598 by (simp add: zdiff_def)
   599 
   600 lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z"
   601 by (simp add: zdiff_def zadd_commute)
   602 
   603 lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)"
   604 apply (simp add: zdiff_def)
   605 apply (subst zadd_zmult_distrib)
   606 apply (simp add: zmult_zminus)
   607 done
   608 
   609 lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)"
   610 by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   611 
   612 lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z"
   613 by (simp add: zdiff_def zadd_ac)
   614 
   615 lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y"
   616 by (simp add: zdiff_def zadd_ac)
   617 
   618 
   619 subsection\<open>The "Less Than" Relation\<close>
   620 
   621 (*"Less than" is a linear ordering*)
   622 lemma zless_linear_lemma:
   623      "[| z \<in> int; w \<in> int |] ==> z$<w | z=w | w$<z"
   624 apply (simp add: int_def zless_def znegative_def zdiff_def, auto)
   625 apply (simp add: zadd zminus image_iff Bex_def)
   626 apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt)
   627 apply (force dest!: spec simp add: add_ac)+
   628 done
   629 
   630 lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z"
   631 apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma)
   632 apply auto
   633 done
   634 
   635 lemma zless_not_refl [iff]: "~ (z$<z)"
   636 by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
   637 
   638 lemma neq_iff_zless: "[| x \<in> int; y \<in> int |] ==> (x \<noteq> y) \<longleftrightarrow> (x $< y | y $< x)"
   639 by (cut_tac z = x and w = y in zless_linear, auto)
   640 
   641 lemma zless_imp_intify_neq: "w $< z ==> intify(w) \<noteq> intify(z)"
   642 apply auto
   643 apply (subgoal_tac "~ (intify (w) $< intify (z))")
   644 apply (erule_tac [2] ssubst)
   645 apply (simp (no_asm_use))
   646 apply auto
   647 done
   648 
   649 (*This lemma allows direct proofs of other <-properties*)
   650 lemma zless_imp_succ_zadd_lemma:
   651     "[| w $< z; w \<in> int; z \<in> int |] ==> (\<exists>n\<in>nat. z = w $+ $#(succ(n)))"
   652 apply (simp add: zless_def znegative_def zdiff_def int_def)
   653 apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
   654 apply (rule_tac x = k in bexI)
   655 apply (erule_tac i="succ (v)" for v in add_left_cancel, auto)
   656 done
   657 
   658 lemma zless_imp_succ_zadd:
   659      "w $< z ==> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   660 apply (subgoal_tac "intify (w) $< intify (z) ")
   661 apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma)
   662 apply auto
   663 done
   664 
   665 lemma zless_succ_zadd_lemma:
   666     "w \<in> int ==> w $< w $+ $# succ(n)"
   667 apply (simp add: zless_def znegative_def zdiff_def int_def)
   668 apply (auto simp add: zadd zminus int_of_def image_iff)
   669 apply (rule_tac x = 0 in exI, auto)
   670 done
   671 
   672 lemma zless_succ_zadd: "w $< w $+ $# succ(n)"
   673 by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
   674 
   675 lemma zless_iff_succ_zadd:
   676      "w $< z \<longleftrightarrow> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   677 apply (rule iffI)
   678 apply (erule zless_imp_succ_zadd, auto)
   679 apply (rename_tac "n")
   680 apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
   681 done
   682 
   683 lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) \<longleftrightarrow> (m<n)"
   684 apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
   685 apply (blast intro: sym)
   686 done
   687 
   688 lemma zless_trans_lemma:
   689     "[| x $< y; y $< z; x \<in> int; y \<in> int; z \<in> int |] ==> x $< z"
   690 apply (simp add: zless_def znegative_def zdiff_def int_def)
   691 apply (auto simp add: zadd zminus image_iff)
   692 apply (rename_tac x1 x2 y1 y2)
   693 apply (rule_tac x = "x1#+x2" in exI)
   694 apply (rule_tac x = "y1#+y2" in exI)
   695 apply (auto simp add: add_lt_mono)
   696 apply (rule sym)
   697 apply hypsubst_thin
   698 apply (erule add_left_cancel)+
   699 apply auto
   700 done
   701 
   702 lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z"
   703 apply (subgoal_tac "intify (x) $< intify (z) ")
   704 apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
   705 apply auto
   706 done
   707 
   708 lemma zless_not_sym: "z $< w ==> ~ (w $< z)"
   709 by (blast dest: zless_trans)
   710 
   711 (* [| z $< w; ~ P ==> w $< z |] ==> P *)
   712 lemmas zless_asym = zless_not_sym [THEN swap]
   713 
   714 lemma zless_imp_zle: "z $< w ==> z $\<le> w"
   715 by (simp add: zle_def)
   716 
   717 lemma zle_linear: "z $\<le> w | w $\<le> z"
   718 apply (simp add: zle_def)
   719 apply (cut_tac zless_linear, blast)
   720 done
   721 
   722 
   723 subsection\<open>Less Than or Equals\<close>
   724 
   725 lemma zle_refl: "z $\<le> z"
   726 by (simp add: zle_def)
   727 
   728 lemma zle_eq_refl: "x=y ==> x $\<le> y"
   729 by (simp add: zle_refl)
   730 
   731 lemma zle_anti_sym_intify: "[| x $\<le> y; y $\<le> x |] ==> intify(x) = intify(y)"
   732 apply (simp add: zle_def, auto)
   733 apply (blast dest: zless_trans)
   734 done
   735 
   736 lemma zle_anti_sym: "[| x $\<le> y; y $\<le> x; x \<in> int; y \<in> int |] ==> x=y"
   737 by (drule zle_anti_sym_intify, auto)
   738 
   739 lemma zle_trans_lemma:
   740      "[| x \<in> int; y \<in> int; z \<in> int; x $\<le> y; y $\<le> z |] ==> x $\<le> z"
   741 apply (simp add: zle_def, auto)
   742 apply (blast intro: zless_trans)
   743 done
   744 
   745 lemma zle_trans [trans]: "[| x $\<le> y; y $\<le> z |] ==> x $\<le> z"
   746 apply (subgoal_tac "intify (x) $\<le> intify (z) ")
   747 apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
   748 apply auto
   749 done
   750 
   751 lemma zle_zless_trans [trans]: "[| i $\<le> j; j $< k |] ==> i $< k"
   752 apply (auto simp add: zle_def)
   753 apply (blast intro: zless_trans)
   754 apply (simp add: zless_def zdiff_def zadd_def)
   755 done
   756 
   757 lemma zless_zle_trans [trans]: "[| i $< j; j $\<le> k |] ==> i $< k"
   758 apply (auto simp add: zle_def)
   759 apply (blast intro: zless_trans)
   760 apply (simp add: zless_def zdiff_def zminus_def)
   761 done
   762 
   763 lemma not_zless_iff_zle: "~ (z $< w) \<longleftrightarrow> (w $\<le> z)"
   764 apply (cut_tac z = z and w = w in zless_linear)
   765 apply (auto dest: zless_trans simp add: zle_def)
   766 apply (auto dest!: zless_imp_intify_neq)
   767 done
   768 
   769 lemma not_zle_iff_zless: "~ (z $\<le> w) \<longleftrightarrow> (w $< z)"
   770 by (simp add: not_zless_iff_zle [THEN iff_sym])
   771 
   772 
   773 subsection\<open>More subtraction laws (for \<open>zcompare_rls\<close>)\<close>
   774 
   775 lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
   776 by (simp add: zdiff_def zadd_ac)
   777 
   778 lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
   779 by (simp add: zdiff_def zadd_ac)
   780 
   781 lemma zdiff_zless_iff: "(x$-y $< z) \<longleftrightarrow> (x $< z $+ y)"
   782 by (simp add: zless_def zdiff_def zadd_ac)
   783 
   784 lemma zless_zdiff_iff: "(x $< z$-y) \<longleftrightarrow> (x $+ y $< z)"
   785 by (simp add: zless_def zdiff_def zadd_ac)
   786 
   787 lemma zdiff_eq_iff: "[| x \<in> int; z \<in> int |] ==> (x$-y = z) \<longleftrightarrow> (x = z $+ y)"
   788 by (auto simp add: zdiff_def zadd_assoc)
   789 
   790 lemma eq_zdiff_iff: "[| x \<in> int; z \<in> int |] ==> (x = z$-y) \<longleftrightarrow> (x $+ y = z)"
   791 by (auto simp add: zdiff_def zadd_assoc)
   792 
   793 lemma zdiff_zle_iff_lemma:
   794      "[| x \<in> int; z \<in> int |] ==> (x$-y $\<le> z) \<longleftrightarrow> (x $\<le> z $+ y)"
   795 by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
   796 
   797 lemma zdiff_zle_iff: "(x$-y $\<le> z) \<longleftrightarrow> (x $\<le> z $+ y)"
   798 by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
   799 
   800 lemma zle_zdiff_iff_lemma:
   801      "[| x \<in> int; z \<in> int |] ==>(x $\<le> z$-y) \<longleftrightarrow> (x $+ y $\<le> z)"
   802 apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
   803 apply (auto simp add: zdiff_def zadd_assoc)
   804 done
   805 
   806 lemma zle_zdiff_iff: "(x $\<le> z$-y) \<longleftrightarrow> (x $+ y $\<le> z)"
   807 by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
   808 
   809 text\<open>This list of rewrites simplifies (in)equalities by bringing subtractions
   810   to the top and then moving negative terms to the other side.
   811   Use with \<open>zadd_ac\<close>\<close>
   812 lemmas zcompare_rls =
   813      zdiff_def [symmetric]
   814      zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2
   815      zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff
   816      zdiff_eq_iff eq_zdiff_iff
   817 
   818 
   819 subsection\<open>Monotonicity and Cancellation Results for Instantiation
   820      of the CancelNumerals Simprocs\<close>
   821 
   822 lemma zadd_left_cancel:
   823      "[| w \<in> int; w': int |] ==> (z $+ w' = z $+ w) \<longleftrightarrow> (w' = w)"
   824 apply safe
   825 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   826 apply (simp add: zadd_ac)
   827 done
   828 
   829 lemma zadd_left_cancel_intify [simp]:
   830      "(z $+ w' = z $+ w) \<longleftrightarrow> intify(w') = intify(w)"
   831 apply (rule iff_trans)
   832 apply (rule_tac [2] zadd_left_cancel, auto)
   833 done
   834 
   835 lemma zadd_right_cancel:
   836      "[| w \<in> int; w': int |] ==> (w' $+ z = w $+ z) \<longleftrightarrow> (w' = w)"
   837 apply safe
   838 apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   839 apply (simp add: zadd_ac)
   840 done
   841 
   842 lemma zadd_right_cancel_intify [simp]:
   843      "(w' $+ z = w $+ z) \<longleftrightarrow> intify(w') = intify(w)"
   844 apply (rule iff_trans)
   845 apply (rule_tac [2] zadd_right_cancel, auto)
   846 done
   847 
   848 lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) \<longleftrightarrow> (w' $< w)"
   849 by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
   850 
   851 lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) \<longleftrightarrow> (w' $< w)"
   852 by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
   853 
   854 lemma zadd_right_cancel_zle [simp]: "(w' $+ z $\<le> w $+ z) \<longleftrightarrow> w' $\<le> w"
   855 by (simp add: zle_def)
   856 
   857 lemma zadd_left_cancel_zle [simp]: "(z $+ w' $\<le> z $+ w) \<longleftrightarrow>  w' $\<le> w"
   858 by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
   859 
   860 
   861 (*"v $\<le> w ==> v$+z $\<le> w$+z"*)
   862 lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2]
   863 
   864 (*"v $\<le> w ==> z$+v $\<le> z$+w"*)
   865 lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2]
   866 
   867 (*"v $\<le> w ==> v$+z $\<le> w$+z"*)
   868 lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2]
   869 
   870 (*"v $\<le> w ==> z$+v $\<le> z$+w"*)
   871 lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2]
   872 
   873 lemma zadd_zle_mono: "[| w' $\<le> w; z' $\<le> z |] ==> w' $+ z' $\<le> w $+ z"
   874 by (erule zadd_zle_mono1 [THEN zle_trans], simp)
   875 
   876 lemma zadd_zless_mono: "[| w' $< w; z' $\<le> z |] ==> w' $+ z' $< w $+ z"
   877 by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
   878 
   879 
   880 subsection\<open>Comparison laws\<close>
   881 
   882 lemma zminus_zless_zminus [simp]: "($- x $< $- y) \<longleftrightarrow> (y $< x)"
   883 by (simp add: zless_def zdiff_def zadd_ac)
   884 
   885 lemma zminus_zle_zminus [simp]: "($- x $\<le> $- y) \<longleftrightarrow> (y $\<le> x)"
   886 by (simp add: not_zless_iff_zle [THEN iff_sym])
   887 
   888 subsubsection\<open>More inequality lemmas\<close>
   889 
   890 lemma equation_zminus: "[| x \<in> int;  y \<in> int |] ==> (x = $- y) \<longleftrightarrow> (y = $- x)"
   891 by auto
   892 
   893 lemma zminus_equation: "[| x \<in> int;  y \<in> int |] ==> ($- x = y) \<longleftrightarrow> ($- y = x)"
   894 by auto
   895 
   896 lemma equation_zminus_intify: "(intify(x) = $- y) \<longleftrightarrow> (intify(y) = $- x)"
   897 apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
   898 apply auto
   899 done
   900 
   901 lemma zminus_equation_intify: "($- x = intify(y)) \<longleftrightarrow> ($- y = intify(x))"
   902 apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
   903 apply auto
   904 done
   905 
   906 
   907 subsubsection\<open>The next several equations are permutative: watch out!\<close>
   908 
   909 lemma zless_zminus: "(x $< $- y) \<longleftrightarrow> (y $< $- x)"
   910 by (simp add: zless_def zdiff_def zadd_ac)
   911 
   912 lemma zminus_zless: "($- x $< y) \<longleftrightarrow> ($- y $< x)"
   913 by (simp add: zless_def zdiff_def zadd_ac)
   914 
   915 lemma zle_zminus: "(x $\<le> $- y) \<longleftrightarrow> (y $\<le> $- x)"
   916 by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
   917 
   918 lemma zminus_zle: "($- x $\<le> y) \<longleftrightarrow> ($- y $\<le> x)"
   919 by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
   920 
   921 end