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