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