src/ZF/Integ/Int.thy
changeset 23146 0bc590051d95
parent 23145 5d8faadf3ecf
child 23147 a5db2f7d7654
     1.1 --- a/src/ZF/Integ/Int.thy	Thu May 31 11:00:06 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,1057 +0,0 @@
     1.4 -(*  Title:      ZF/Integ/Int.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 -
     1.9 -*)
    1.10 -
    1.11 -header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
    1.12 -
    1.13 -theory Int imports EquivClass ArithSimp begin
    1.14 -
    1.15 -constdefs
    1.16 -  intrel :: i
    1.17 -    "intrel == {p : (nat*nat)*(nat*nat).                 
    1.18 -                \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    1.19 -
    1.20 -  int :: i
    1.21 -    "int == (nat*nat)//intrel"  
    1.22 -
    1.23 -  int_of :: "i=>i" --{*coercion from nat to int*}    ("$# _" [80] 80)
    1.24 -    "$# m == intrel `` {<natify(m), 0>}"
    1.25 -
    1.26 -  intify :: "i=>i" --{*coercion from ANYTHING to int*}
    1.27 -    "intify(m) == if m : int then m else $#0"
    1.28 -
    1.29 -  raw_zminus :: "i=>i"
    1.30 -    "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"
    1.31 -
    1.32 -  zminus :: "i=>i"                                 ("$- _" [80] 80)
    1.33 -    "$- z == raw_zminus (intify(z))"
    1.34 -
    1.35 -  znegative   ::      "i=>o"
    1.36 -    "znegative(z) == \<exists>x y. x<y & y\<in>nat & <x,y>\<in>z"
    1.37 -
    1.38 -  iszero      ::      "i=>o"
    1.39 -    "iszero(z) == z = $# 0"
    1.40 -    
    1.41 -  raw_nat_of  :: "i=>i"
    1.42 -  "raw_nat_of(z) == natify (\<Union><x,y>\<in>z. x#-y)"
    1.43 -
    1.44 -  nat_of  :: "i=>i"
    1.45 -  "nat_of(z) == raw_nat_of (intify(z))"
    1.46 -
    1.47 -  zmagnitude  ::      "i=>i"
    1.48 -  --{*could be replaced by an absolute value function from int to int?*}
    1.49 -    "zmagnitude(z) ==
    1.50 -     THE m. m\<in>nat & ((~ znegative(z) & z = $# m) |
    1.51 -		       (znegative(z) & $- z = $# m))"
    1.52 -
    1.53 -  raw_zmult   ::      "[i,i]=>i"
    1.54 -    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
    1.55 -      Perhaps a "curried" or even polymorphic congruent predicate would be
    1.56 -      better.*)
    1.57 -     "raw_zmult(z1,z2) == 
    1.58 -       \<Union>p1\<in>z1. \<Union>p2\<in>z2.  split(%x1 y1. split(%x2 y2.        
    1.59 -                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    1.60 -
    1.61 -  zmult       ::      "[i,i]=>i"      (infixl "$*" 70)
    1.62 -     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
    1.63 -
    1.64 -  raw_zadd    ::      "[i,i]=>i"
    1.65 -     "raw_zadd (z1, z2) == 
    1.66 -       \<Union>z1\<in>z1. \<Union>z2\<in>z2. let <x1,y1>=z1; <x2,y2>=z2                 
    1.67 -                           in intrel``{<x1#+x2, y1#+y2>}"
    1.68 -
    1.69 -  zadd        ::      "[i,i]=>i"      (infixl "$+" 65)
    1.70 -     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
    1.71 -
    1.72 -  zdiff        ::      "[i,i]=>i"      (infixl "$-" 65)
    1.73 -     "z1 $- z2 == z1 $+ zminus(z2)"
    1.74 -
    1.75 -  zless        ::      "[i,i]=>o"      (infixl "$<" 50)
    1.76 -     "z1 $< z2 == znegative(z1 $- z2)"
    1.77 -  
    1.78 -  zle          ::      "[i,i]=>o"      (infixl "$<=" 50)
    1.79 -     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    1.80 -  
    1.81 -
    1.82 -syntax (xsymbols)
    1.83 -  zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
    1.84 -  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)  --{*less than or equals*}
    1.85 -
    1.86 -syntax (HTML output)
    1.87 -  zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
    1.88 -  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)
    1.89 -
    1.90 -
    1.91 -declare quotientE [elim!]
    1.92 -
    1.93 -subsection{*Proving that @{term intrel} is an equivalence relation*}
    1.94 -
    1.95 -(** Natural deduction for intrel **)
    1.96 -
    1.97 -lemma intrel_iff [simp]: 
    1.98 -    "<<x1,y1>,<x2,y2>>: intrel <->  
    1.99 -     x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
   1.100 -by (simp add: intrel_def)
   1.101 -
   1.102 -lemma intrelI [intro!]: 
   1.103 -    "[| x1#+y2 = x2#+y1; x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |]   
   1.104 -     ==> <<x1,y1>,<x2,y2>>: intrel"
   1.105 -by (simp add: intrel_def)
   1.106 -
   1.107 -lemma intrelE [elim!]:
   1.108 -  "[| p: intrel;   
   1.109 -      !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1;  
   1.110 -                        x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] ==> Q |]  
   1.111 -   ==> Q"
   1.112 -by (simp add: intrel_def, blast) 
   1.113 -
   1.114 -lemma int_trans_lemma:
   1.115 -     "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1"
   1.116 -apply (rule sym)
   1.117 -apply (erule add_left_cancel)+
   1.118 -apply (simp_all (no_asm_simp))
   1.119 -done
   1.120 -
   1.121 -lemma equiv_intrel: "equiv(nat*nat, intrel)"
   1.122 -apply (simp add: equiv_def refl_def sym_def trans_def)
   1.123 -apply (fast elim!: sym int_trans_lemma)
   1.124 -done
   1.125 -
   1.126 -lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} : int"
   1.127 -by (simp add: int_def)
   1.128 -
   1.129 -declare equiv_intrel [THEN eq_equiv_class_iff, simp]
   1.130 -declare conj_cong [cong]
   1.131 -
   1.132 -lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel]
   1.133 -
   1.134 -(** int_of: the injection from nat to int **)
   1.135 -
   1.136 -lemma int_of_type [simp,TC]: "$#m : int"
   1.137 -by (simp add: int_def quotient_def int_of_def, auto)
   1.138 -
   1.139 -lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
   1.140 -by (simp add: int_of_def)
   1.141 -
   1.142 -lemma int_of_inject: "[| $#m = $#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
   1.143 -by (drule int_of_eq [THEN iffD1], auto)
   1.144 -
   1.145 -
   1.146 -(** intify: coercion from anything to int **)
   1.147 -
   1.148 -lemma intify_in_int [iff,TC]: "intify(x) : int"
   1.149 -by (simp add: intify_def)
   1.150 -
   1.151 -lemma intify_ident [simp]: "n : int ==> intify(n) = n"
   1.152 -by (simp add: intify_def)
   1.153 -
   1.154 -
   1.155 -subsection{*Collapsing rules: to remove @{term intify}
   1.156 -            from arithmetic expressions*}
   1.157 -
   1.158 -lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
   1.159 -by simp
   1.160 -
   1.161 -lemma int_of_natify [simp]: "$# (natify(m)) = $# m"
   1.162 -by (simp add: int_of_def)
   1.163 -
   1.164 -lemma zminus_intify [simp]: "$- (intify(m)) = $- m"
   1.165 -by (simp add: zminus_def)
   1.166 -
   1.167 -(** Addition **)
   1.168 -
   1.169 -lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y"
   1.170 -by (simp add: zadd_def)
   1.171 -
   1.172 -lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y"
   1.173 -by (simp add: zadd_def)
   1.174 -
   1.175 -(** Subtraction **)
   1.176 -
   1.177 -lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y"
   1.178 -by (simp add: zdiff_def)
   1.179 -
   1.180 -lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y"
   1.181 -by (simp add: zdiff_def)
   1.182 -
   1.183 -(** Multiplication **)
   1.184 -
   1.185 -lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y"
   1.186 -by (simp add: zmult_def)
   1.187 -
   1.188 -lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y"
   1.189 -by (simp add: zmult_def)
   1.190 -
   1.191 -(** Orderings **)
   1.192 -
   1.193 -lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
   1.194 -by (simp add: zless_def)
   1.195 -
   1.196 -lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
   1.197 -by (simp add: zless_def)
   1.198 -
   1.199 -lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
   1.200 -by (simp add: zle_def)
   1.201 -
   1.202 -lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
   1.203 -by (simp add: zle_def)
   1.204 -
   1.205 -
   1.206 -subsection{*@{term zminus}: unary negation on @{term int}*}
   1.207 -
   1.208 -lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
   1.209 -by (auto simp add: congruent_def add_ac)
   1.210 -
   1.211 -lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
   1.212 -apply (simp add: int_def raw_zminus_def)
   1.213 -apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
   1.214 -done
   1.215 -
   1.216 -lemma zminus_type [TC,iff]: "$-z : int"
   1.217 -by (simp add: zminus_def raw_zminus_type)
   1.218 -
   1.219 -lemma raw_zminus_inject: 
   1.220 -     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w"
   1.221 -apply (simp add: int_def raw_zminus_def)
   1.222 -apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe)
   1.223 -apply (auto dest: eq_intrelD simp add: add_ac)
   1.224 -done
   1.225 -
   1.226 -lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)"
   1.227 -apply (simp add: zminus_def)
   1.228 -apply (blast dest!: raw_zminus_inject)
   1.229 -done
   1.230 -
   1.231 -lemma zminus_inject: "[| $-z = $-w;  z: int;  w: int |] ==> z=w"
   1.232 -by auto
   1.233 -
   1.234 -lemma raw_zminus: 
   1.235 -    "[| x\<in>nat;  y\<in>nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}"
   1.236 -apply (simp add: raw_zminus_def UN_equiv_class [OF equiv_intrel zminus_congruent])
   1.237 -done
   1.238 -
   1.239 -lemma zminus: 
   1.240 -    "[| x\<in>nat;  y\<in>nat |]  
   1.241 -     ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}"
   1.242 -by (simp add: zminus_def raw_zminus image_intrel_int)
   1.243 -
   1.244 -lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z"
   1.245 -by (auto simp add: int_def raw_zminus)
   1.246 -
   1.247 -lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)"
   1.248 -by (simp add: zminus_def raw_zminus_type raw_zminus_zminus)
   1.249 -
   1.250 -lemma zminus_int0 [simp]: "$- ($#0) = $#0"
   1.251 -by (simp add: int_of_def zminus)
   1.252 -
   1.253 -lemma zminus_zminus: "z : int ==> $- ($- z) = z"
   1.254 -by simp
   1.255 -
   1.256 -
   1.257 -subsection{*@{term znegative}: the test for negative integers*}
   1.258 -
   1.259 -lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
   1.260 -apply (cases "x<y") 
   1.261 -apply (auto simp add: znegative_def not_lt_iff_le)
   1.262 -apply (subgoal_tac "y #+ x2 < x #+ y2", force) 
   1.263 -apply (rule add_le_lt_mono, auto) 
   1.264 -done
   1.265 -
   1.266 -(*No natural number is negative!*)
   1.267 -lemma not_znegative_int_of [iff]: "~ znegative($# n)"
   1.268 -by (simp add: znegative int_of_def) 
   1.269 -
   1.270 -lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))"
   1.271 -by (simp add: znegative int_of_def zminus natify_succ)
   1.272 -
   1.273 -lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0"
   1.274 -by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym])
   1.275 -
   1.276 -
   1.277 -subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*}
   1.278 -
   1.279 -lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
   1.280 -by (simp add: nat_of_def)
   1.281 -
   1.282 -lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
   1.283 -by (auto simp add: congruent_def split add: nat_diff_split)
   1.284 -
   1.285 -lemma raw_nat_of: 
   1.286 -    "[| x\<in>nat;  y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
   1.287 -by (simp add: raw_nat_of_def UN_equiv_class [OF equiv_intrel nat_of_congruent])
   1.288 -
   1.289 -lemma raw_nat_of_int_of: "raw_nat_of($# n) = natify(n)"
   1.290 -by (simp add: int_of_def raw_nat_of)
   1.291 -
   1.292 -lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)"
   1.293 -by (simp add: raw_nat_of_int_of nat_of_def)
   1.294 -
   1.295 -lemma raw_nat_of_type: "raw_nat_of(z) \<in> nat"
   1.296 -by (simp add: raw_nat_of_def)
   1.297 -
   1.298 -lemma nat_of_type [iff,TC]: "nat_of(z) \<in> nat"
   1.299 -by (simp add: nat_of_def raw_nat_of_type)
   1.300 -
   1.301 -subsection{*zmagnitude: magnitide of an integer, as a natural number*}
   1.302 -
   1.303 -lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)"
   1.304 -by (auto simp add: zmagnitude_def int_of_eq)
   1.305 -
   1.306 -lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n"
   1.307 -apply (drule sym)
   1.308 -apply (simp (no_asm_simp) add: int_of_eq)
   1.309 -done
   1.310 -
   1.311 -lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)"
   1.312 -apply (simp add: zmagnitude_def)
   1.313 -apply (rule the_equality)
   1.314 -apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
   1.315 -            iff del: int_of_eq, auto)
   1.316 -done
   1.317 -
   1.318 -lemma zmagnitude_type [iff,TC]: "zmagnitude(z)\<in>nat"
   1.319 -apply (simp add: zmagnitude_def)
   1.320 -apply (rule theI2, auto)
   1.321 -done
   1.322 -
   1.323 -lemma not_zneg_int_of: 
   1.324 -     "[| z: int; ~ znegative(z) |] ==> \<exists>n\<in>nat. z = $# n"
   1.325 -apply (auto simp add: int_def znegative int_of_def not_lt_iff_le)
   1.326 -apply (rename_tac x y) 
   1.327 -apply (rule_tac x="x#-y" in bexI) 
   1.328 -apply (auto simp add: add_diff_inverse2) 
   1.329 -done
   1.330 -
   1.331 -lemma not_zneg_mag [simp]:
   1.332 -     "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"
   1.333 -by (drule not_zneg_int_of, auto)
   1.334 -
   1.335 -lemma zneg_int_of: 
   1.336 -     "[| znegative(z); z: int |] ==> \<exists>n\<in>nat. z = $- ($# succ(n))"
   1.337 -by (auto simp add: int_def znegative zminus int_of_def dest!: less_imp_succ_add)
   1.338 -
   1.339 -lemma zneg_mag [simp]:
   1.340 -     "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"
   1.341 -by (drule zneg_int_of, auto)
   1.342 -
   1.343 -lemma int_cases: "z : int ==> \<exists>n\<in>nat. z = $# n | z = $- ($# succ(n))"
   1.344 -apply (case_tac "znegative (z) ")
   1.345 -prefer 2 apply (blast dest: not_zneg_mag sym)
   1.346 -apply (blast dest: zneg_int_of)
   1.347 -done
   1.348 -
   1.349 -lemma not_zneg_raw_nat_of:
   1.350 -     "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z"
   1.351 -apply (drule not_zneg_int_of)
   1.352 -apply (auto simp add: raw_nat_of_type raw_nat_of_int_of)
   1.353 -done
   1.354 -
   1.355 -lemma not_zneg_nat_of_intify:
   1.356 -     "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)"
   1.357 -by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of)
   1.358 -
   1.359 -lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z"
   1.360 -apply (simp (no_asm_simp) add: not_zneg_nat_of_intify)
   1.361 -done
   1.362 -
   1.363 -lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0"
   1.364 -apply (subgoal_tac "intify(z) \<in> int")
   1.365 -apply (simp add: int_def) 
   1.366 -apply (auto simp add: znegative nat_of_def raw_nat_of 
   1.367 -            split add: nat_diff_split) 
   1.368 -done
   1.369 -
   1.370 -
   1.371 -subsection{*@{term zadd}: addition on int*}
   1.372 -
   1.373 -text{*Congruence Property for Addition*}
   1.374 -lemma zadd_congruent2: 
   1.375 -    "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2                  
   1.376 -                            in intrel``{<x1#+x2, y1#+y2>})
   1.377 -     respects2 intrel"
   1.378 -apply (simp add: congruent2_def)
   1.379 -(*Proof via congruent2_commuteI seems longer*)
   1.380 -apply safe
   1.381 -apply (simp (no_asm_simp) add: add_assoc Let_def)
   1.382 -(*The rest should be trivial, but rearranging terms is hard
   1.383 -  add_ac does not help rewriting with the assumptions.*)
   1.384 -apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst])
   1.385 -apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst])
   1.386 -apply (simp (no_asm_simp) add: add_assoc [symmetric])
   1.387 -done
   1.388 -
   1.389 -lemma raw_zadd_type: "[| z: int;  w: int |] ==> raw_zadd(z,w) : int"
   1.390 -apply (simp add: int_def raw_zadd_def)
   1.391 -apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
   1.392 -apply (simp add: Let_def)
   1.393 -done
   1.394 -
   1.395 -lemma zadd_type [iff,TC]: "z $+ w : int"
   1.396 -by (simp add: zadd_def raw_zadd_type)
   1.397 -
   1.398 -lemma raw_zadd: 
   1.399 -  "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]               
   1.400 -   ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =   
   1.401 -       intrel `` {<x1#+x2, y1#+y2>}"
   1.402 -apply (simp add: raw_zadd_def 
   1.403 -             UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2])
   1.404 -apply (simp add: Let_def)
   1.405 -done
   1.406 -
   1.407 -lemma zadd: 
   1.408 -  "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]          
   1.409 -   ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =   
   1.410 -       intrel `` {<x1#+x2, y1#+y2>}"
   1.411 -by (simp add: zadd_def raw_zadd image_intrel_int)
   1.412 -
   1.413 -lemma raw_zadd_int0: "z : int ==> raw_zadd ($#0,z) = z"
   1.414 -by (auto simp add: int_def int_of_def raw_zadd)
   1.415 -
   1.416 -lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)"
   1.417 -by (simp add: zadd_def raw_zadd_int0)
   1.418 -
   1.419 -lemma zadd_int0: "z: int ==> $#0 $+ z = z"
   1.420 -by simp
   1.421 -
   1.422 -lemma raw_zminus_zadd_distrib: 
   1.423 -     "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)"
   1.424 -by (auto simp add: zminus raw_zadd int_def)
   1.425 -
   1.426 -lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w"
   1.427 -by (simp add: zadd_def raw_zminus_zadd_distrib)
   1.428 -
   1.429 -lemma raw_zadd_commute:
   1.430 -     "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)"
   1.431 -by (auto simp add: raw_zadd add_ac int_def)
   1.432 -
   1.433 -lemma zadd_commute: "z $+ w = w $+ z"
   1.434 -by (simp add: zadd_def raw_zadd_commute)
   1.435 -
   1.436 -lemma raw_zadd_assoc: 
   1.437 -    "[| z1: int;  z2: int;  z3: int |]    
   1.438 -     ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))"
   1.439 -by (auto simp add: int_def raw_zadd add_assoc)
   1.440 -
   1.441 -lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"
   1.442 -by (simp add: zadd_def raw_zadd_type raw_zadd_assoc)
   1.443 -
   1.444 -(*For AC rewriting*)
   1.445 -lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)"
   1.446 -apply (simp add: zadd_assoc [symmetric])
   1.447 -apply (simp add: zadd_commute)
   1.448 -done
   1.449 -
   1.450 -(*Integer addition is an AC operator*)
   1.451 -lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
   1.452 -
   1.453 -lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)"
   1.454 -by (simp add: int_of_def zadd)
   1.455 -
   1.456 -lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)"
   1.457 -by (simp add: int_of_add [symmetric] natify_succ)
   1.458 -
   1.459 -lemma int_of_diff: 
   1.460 -     "[| m\<in>nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)"
   1.461 -apply (simp add: int_of_def zdiff_def)
   1.462 -apply (frule lt_nat_in_nat)
   1.463 -apply (simp_all add: zadd zminus add_diff_inverse2)
   1.464 -done
   1.465 -
   1.466 -lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, $- z) = $#0"
   1.467 -by (auto simp add: int_def int_of_def zminus raw_zadd add_commute)
   1.468 -
   1.469 -lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0"
   1.470 -apply (simp add: zadd_def)
   1.471 -apply (subst zminus_intify [symmetric])
   1.472 -apply (rule intify_in_int [THEN raw_zadd_zminus_inverse])
   1.473 -done
   1.474 -
   1.475 -lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0"
   1.476 -by (simp add: zadd_commute zadd_zminus_inverse)
   1.477 -
   1.478 -lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)"
   1.479 -by (rule trans [OF zadd_commute zadd_int0_intify])
   1.480 -
   1.481 -lemma zadd_int0_right: "z:int ==> z $+ $#0 = z"
   1.482 -by simp
   1.483 -
   1.484 -
   1.485 -subsection{*@{term zmult}: Integer Multiplication*}
   1.486 -
   1.487 -text{*Congruence property for multiplication*}
   1.488 -lemma zmult_congruent2:
   1.489 -    "(%p1 p2. split(%x1 y1. split(%x2 y2.      
   1.490 -                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))
   1.491 -     respects2 intrel"
   1.492 -apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
   1.493 -(*Proof that zmult is congruent in one argument*)
   1.494 -apply (rename_tac x y)
   1.495 -apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context])
   1.496 -apply (drule_tac t = "%u. y#*u" in subst_context)
   1.497 -apply (erule add_left_cancel)+
   1.498 -apply (simp_all add: add_mult_distrib_left)
   1.499 -done
   1.500 -
   1.501 -
   1.502 -lemma raw_zmult_type: "[| z: int;  w: int |] ==> raw_zmult(z,w) : int"
   1.503 -apply (simp add: int_def raw_zmult_def)
   1.504 -apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
   1.505 -apply (simp add: Let_def)
   1.506 -done
   1.507 -
   1.508 -lemma zmult_type [iff,TC]: "z $* w : int"
   1.509 -by (simp add: zmult_def raw_zmult_type)
   1.510 -
   1.511 -lemma raw_zmult: 
   1.512 -     "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]     
   1.513 -      ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =      
   1.514 -          intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   1.515 -by (simp add: raw_zmult_def 
   1.516 -           UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2])
   1.517 -
   1.518 -lemma zmult: 
   1.519 -     "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]     
   1.520 -      ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =      
   1.521 -          intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
   1.522 -by (simp add: zmult_def raw_zmult image_intrel_int)
   1.523 -
   1.524 -lemma raw_zmult_int0: "z : int ==> raw_zmult ($#0,z) = $#0"
   1.525 -by (auto simp add: int_def int_of_def raw_zmult)
   1.526 -
   1.527 -lemma zmult_int0 [simp]: "$#0 $* z = $#0"
   1.528 -by (simp add: zmult_def raw_zmult_int0)
   1.529 -
   1.530 -lemma raw_zmult_int1: "z : int ==> raw_zmult ($#1,z) = z"
   1.531 -by (auto simp add: int_def int_of_def raw_zmult)
   1.532 -
   1.533 -lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)"
   1.534 -by (simp add: zmult_def raw_zmult_int1)
   1.535 -
   1.536 -lemma zmult_int1: "z : int ==> $#1 $* z = z"
   1.537 -by simp
   1.538 -
   1.539 -lemma raw_zmult_commute:
   1.540 -     "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)"
   1.541 -by (auto simp add: int_def raw_zmult add_ac mult_ac)
   1.542 -
   1.543 -lemma zmult_commute: "z $* w = w $* z"
   1.544 -by (simp add: zmult_def raw_zmult_commute)
   1.545 -
   1.546 -lemma raw_zmult_zminus: 
   1.547 -     "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)"
   1.548 -by (auto simp add: int_def zminus raw_zmult add_ac)
   1.549 -
   1.550 -lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)"
   1.551 -apply (simp add: zmult_def raw_zmult_zminus)
   1.552 -apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto)
   1.553 -done
   1.554 -
   1.555 -lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)"
   1.556 -by (simp add: zmult_commute [of w])
   1.557 -
   1.558 -lemma raw_zmult_assoc: 
   1.559 -    "[| z1: int;  z2: int;  z3: int |]    
   1.560 -     ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))"
   1.561 -by (auto simp add: int_def raw_zmult add_mult_distrib_left add_ac mult_ac)
   1.562 -
   1.563 -lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)"
   1.564 -by (simp add: zmult_def raw_zmult_type raw_zmult_assoc)
   1.565 -
   1.566 -(*For AC rewriting*)
   1.567 -lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)"
   1.568 -apply (simp add: zmult_assoc [symmetric])
   1.569 -apply (simp add: zmult_commute)
   1.570 -done
   1.571 -
   1.572 -(*Integer multiplication is an AC operator*)
   1.573 -lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
   1.574 -
   1.575 -lemma raw_zadd_zmult_distrib: 
   1.576 -    "[| z1: int;  z2: int;  w: int |]   
   1.577 -     ==> raw_zmult(raw_zadd(z1,z2), w) =  
   1.578 -         raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))"
   1.579 -by (auto simp add: int_def raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac)
   1.580 -
   1.581 -lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"
   1.582 -by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type 
   1.583 -              raw_zadd_zmult_distrib)
   1.584 -
   1.585 -lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)"
   1.586 -by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   1.587 -
   1.588 -lemmas int_typechecks = 
   1.589 -  int_of_type zminus_type zmagnitude_type zadd_type zmult_type
   1.590 -
   1.591 -
   1.592 -(*** Subtraction laws ***)
   1.593 -
   1.594 -lemma zdiff_type [iff,TC]: "z $- w : int"
   1.595 -by (simp add: zdiff_def)
   1.596 -
   1.597 -lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z"
   1.598 -by (simp add: zdiff_def zadd_commute)
   1.599 -
   1.600 -lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)"
   1.601 -apply (simp add: zdiff_def)
   1.602 -apply (subst zadd_zmult_distrib)
   1.603 -apply (simp add: zmult_zminus)
   1.604 -done
   1.605 -
   1.606 -lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)"
   1.607 -by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   1.608 -
   1.609 -lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z"
   1.610 -by (simp add: zdiff_def zadd_ac)
   1.611 -
   1.612 -lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y"
   1.613 -by (simp add: zdiff_def zadd_ac)
   1.614 -
   1.615 -
   1.616 -subsection{*The "Less Than" Relation*}
   1.617 -
   1.618 -(*"Less than" is a linear ordering*)
   1.619 -lemma zless_linear_lemma: 
   1.620 -     "[| z: int; w: int |] ==> z$<w | z=w | w$<z"
   1.621 -apply (simp add: int_def zless_def znegative_def zdiff_def, auto)
   1.622 -apply (simp add: zadd zminus image_iff Bex_def)
   1.623 -apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt)
   1.624 -apply (force dest!: spec simp add: add_ac)+
   1.625 -done
   1.626 -
   1.627 -lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z"
   1.628 -apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma)
   1.629 -apply auto
   1.630 -done
   1.631 -
   1.632 -lemma zless_not_refl [iff]: "~ (z$<z)"
   1.633 -by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
   1.634 -
   1.635 -lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)"
   1.636 -by (cut_tac z = x and w = y in zless_linear, auto)
   1.637 -
   1.638 -lemma zless_imp_intify_neq: "w $< z ==> intify(w) ~= intify(z)"
   1.639 -apply auto
   1.640 -apply (subgoal_tac "~ (intify (w) $< intify (z))")
   1.641 -apply (erule_tac [2] ssubst)
   1.642 -apply (simp (no_asm_use))
   1.643 -apply auto
   1.644 -done
   1.645 -
   1.646 -(*This lemma allows direct proofs of other <-properties*)
   1.647 -lemma zless_imp_succ_zadd_lemma: 
   1.648 -    "[| w $< z; w: int; z: int |] ==> (\<exists>n\<in>nat. z = w $+ $#(succ(n)))"
   1.649 -apply (simp add: zless_def znegative_def zdiff_def int_def)
   1.650 -apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
   1.651 -apply (rule_tac x = k in bexI)
   1.652 -apply (erule add_left_cancel, auto)
   1.653 -done
   1.654 -
   1.655 -lemma zless_imp_succ_zadd:
   1.656 -     "w $< z ==> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   1.657 -apply (subgoal_tac "intify (w) $< intify (z) ")
   1.658 -apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma)
   1.659 -apply auto
   1.660 -done
   1.661 -
   1.662 -lemma zless_succ_zadd_lemma: 
   1.663 -    "w : int ==> w $< w $+ $# succ(n)"
   1.664 -apply (simp add: zless_def znegative_def zdiff_def int_def)
   1.665 -apply (auto simp add: zadd zminus int_of_def image_iff)
   1.666 -apply (rule_tac x = 0 in exI, auto)
   1.667 -done
   1.668 -
   1.669 -lemma zless_succ_zadd: "w $< w $+ $# succ(n)"
   1.670 -by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
   1.671 -
   1.672 -lemma zless_iff_succ_zadd:
   1.673 -     "w $< z <-> (\<exists>n\<in>nat. w $+ $#(succ(n)) = intify(z))"
   1.674 -apply (rule iffI)
   1.675 -apply (erule zless_imp_succ_zadd, auto)
   1.676 -apply (rename_tac "n")
   1.677 -apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
   1.678 -done
   1.679 -
   1.680 -lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> ($#m $< $#n) <-> (m<n)"
   1.681 -apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
   1.682 -apply (blast intro: sym)
   1.683 -done
   1.684 -
   1.685 -lemma zless_trans_lemma: 
   1.686 -    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"
   1.687 -apply (simp add: zless_def znegative_def zdiff_def int_def)
   1.688 -apply (auto simp add: zadd zminus image_iff)
   1.689 -apply (rename_tac x1 x2 y1 y2)
   1.690 -apply (rule_tac x = "x1#+x2" in exI)
   1.691 -apply (rule_tac x = "y1#+y2" in exI)
   1.692 -apply (auto simp add: add_lt_mono)
   1.693 -apply (rule sym)
   1.694 -apply (erule add_left_cancel)+
   1.695 -apply auto
   1.696 -done
   1.697 -
   1.698 -lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
   1.699 -apply (subgoal_tac "intify (x) $< intify (z) ")
   1.700 -apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
   1.701 -apply auto
   1.702 -done
   1.703 -
   1.704 -lemma zless_not_sym: "z $< w ==> ~ (w $< z)"
   1.705 -by (blast dest: zless_trans)
   1.706 -
   1.707 -(* [| z $< w; ~ P ==> w $< z |] ==> P *)
   1.708 -lemmas zless_asym = zless_not_sym [THEN swap, standard]
   1.709 -
   1.710 -lemma zless_imp_zle: "z $< w ==> z $<= w"
   1.711 -by (simp add: zle_def)
   1.712 -
   1.713 -lemma zle_linear: "z $<= w | w $<= z"
   1.714 -apply (simp add: zle_def)
   1.715 -apply (cut_tac zless_linear, blast)
   1.716 -done
   1.717 -
   1.718 -
   1.719 -subsection{*Less Than or Equals*}
   1.720 -
   1.721 -lemma zle_refl: "z $<= z"
   1.722 -by (simp add: zle_def)
   1.723 -
   1.724 -lemma zle_eq_refl: "x=y ==> x $<= y"
   1.725 -by (simp add: zle_refl)
   1.726 -
   1.727 -lemma zle_anti_sym_intify: "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)"
   1.728 -apply (simp add: zle_def, auto)
   1.729 -apply (blast dest: zless_trans)
   1.730 -done
   1.731 -
   1.732 -lemma zle_anti_sym: "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"
   1.733 -by (drule zle_anti_sym_intify, auto)
   1.734 -
   1.735 -lemma zle_trans_lemma:
   1.736 -     "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z"
   1.737 -apply (simp add: zle_def, auto)
   1.738 -apply (blast intro: zless_trans)
   1.739 -done
   1.740 -
   1.741 -lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
   1.742 -apply (subgoal_tac "intify (x) $<= intify (z) ")
   1.743 -apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
   1.744 -apply auto
   1.745 -done
   1.746 -
   1.747 -lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
   1.748 -apply (auto simp add: zle_def)
   1.749 -apply (blast intro: zless_trans)
   1.750 -apply (simp add: zless_def zdiff_def zadd_def)
   1.751 -done
   1.752 -
   1.753 -lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
   1.754 -apply (auto simp add: zle_def)
   1.755 -apply (blast intro: zless_trans)
   1.756 -apply (simp add: zless_def zdiff_def zminus_def)
   1.757 -done
   1.758 -
   1.759 -lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
   1.760 -apply (cut_tac z = z and w = w in zless_linear)
   1.761 -apply (auto dest: zless_trans simp add: zle_def)
   1.762 -apply (auto dest!: zless_imp_intify_neq)
   1.763 -done
   1.764 -
   1.765 -lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
   1.766 -by (simp add: not_zless_iff_zle [THEN iff_sym])
   1.767 -
   1.768 -
   1.769 -subsection{*More subtraction laws (for @{text zcompare_rls})*}
   1.770 -
   1.771 -lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
   1.772 -by (simp add: zdiff_def zadd_ac)
   1.773 -
   1.774 -lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
   1.775 -by (simp add: zdiff_def zadd_ac)
   1.776 -
   1.777 -lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
   1.778 -by (simp add: zless_def zdiff_def zadd_ac)
   1.779 -
   1.780 -lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
   1.781 -by (simp add: zless_def zdiff_def zadd_ac)
   1.782 -
   1.783 -lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
   1.784 -by (auto simp add: zdiff_def zadd_assoc)
   1.785 -
   1.786 -lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
   1.787 -by (auto simp add: zdiff_def zadd_assoc)
   1.788 -
   1.789 -lemma zdiff_zle_iff_lemma:
   1.790 -     "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
   1.791 -by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
   1.792 -
   1.793 -lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
   1.794 -by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
   1.795 -
   1.796 -lemma zle_zdiff_iff_lemma:
   1.797 -     "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
   1.798 -apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
   1.799 -apply (auto simp add: zdiff_def zadd_assoc)
   1.800 -done
   1.801 -
   1.802 -lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
   1.803 -by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
   1.804 -
   1.805 -text{*This list of rewrites simplifies (in)equalities by bringing subtractions
   1.806 -  to the top and then moving negative terms to the other side.  
   1.807 -  Use with @{text zadd_ac}*}
   1.808 -lemmas zcompare_rls =
   1.809 -     zdiff_def [symmetric]
   1.810 -     zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 
   1.811 -     zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff 
   1.812 -     zdiff_eq_iff eq_zdiff_iff
   1.813 -
   1.814 -
   1.815 -subsection{*Monotonicity and Cancellation Results for Instantiation
   1.816 -     of the CancelNumerals Simprocs*}
   1.817 -
   1.818 -lemma zadd_left_cancel:
   1.819 -     "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
   1.820 -apply safe
   1.821 -apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   1.822 -apply (simp add: zadd_ac)
   1.823 -done
   1.824 -
   1.825 -lemma zadd_left_cancel_intify [simp]:
   1.826 -     "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
   1.827 -apply (rule iff_trans)
   1.828 -apply (rule_tac [2] zadd_left_cancel, auto)
   1.829 -done
   1.830 -
   1.831 -lemma zadd_right_cancel:
   1.832 -     "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
   1.833 -apply safe
   1.834 -apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
   1.835 -apply (simp add: zadd_ac)
   1.836 -done
   1.837 -
   1.838 -lemma zadd_right_cancel_intify [simp]:
   1.839 -     "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
   1.840 -apply (rule iff_trans)
   1.841 -apply (rule_tac [2] zadd_right_cancel, auto)
   1.842 -done
   1.843 -
   1.844 -lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
   1.845 -by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc)
   1.846 -
   1.847 -lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
   1.848 -by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
   1.849 -
   1.850 -lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
   1.851 -by (simp add: zle_def)
   1.852 -
   1.853 -lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <->  w' $<= w"
   1.854 -by (simp add: zadd_commute [of z]  zadd_right_cancel_zle)
   1.855 -
   1.856 -
   1.857 -(*"v $<= w ==> v$+z $<= w$+z"*)
   1.858 -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
   1.859 -
   1.860 -(*"v $<= w ==> z$+v $<= z$+w"*)
   1.861 -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
   1.862 -
   1.863 -(*"v $<= w ==> v$+z $<= w$+z"*)
   1.864 -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
   1.865 -
   1.866 -(*"v $<= w ==> z$+v $<= z$+w"*)
   1.867 -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
   1.868 -
   1.869 -lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"
   1.870 -by (erule zadd_zle_mono1 [THEN zle_trans], simp)
   1.871 -
   1.872 -lemma zadd_zless_mono: "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z"
   1.873 -by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
   1.874 -
   1.875 -
   1.876 -subsection{*Comparison laws*}
   1.877 -
   1.878 -lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
   1.879 -by (simp add: zless_def zdiff_def zadd_ac)
   1.880 -
   1.881 -lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
   1.882 -by (simp add: not_zless_iff_zle [THEN iff_sym])
   1.883 -
   1.884 -subsubsection{*More inequality lemmas*}
   1.885 -
   1.886 -lemma equation_zminus: "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)"
   1.887 -by auto
   1.888 -
   1.889 -lemma zminus_equation: "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)"
   1.890 -by auto
   1.891 -
   1.892 -lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
   1.893 -apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
   1.894 -apply auto
   1.895 -done
   1.896 -
   1.897 -lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
   1.898 -apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
   1.899 -apply auto
   1.900 -done
   1.901 -
   1.902 -
   1.903 -subsubsection{*The next several equations are permutative: watch out!*}
   1.904 -
   1.905 -lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
   1.906 -by (simp add: zless_def zdiff_def zadd_ac)
   1.907 -
   1.908 -lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
   1.909 -by (simp add: zless_def zdiff_def zadd_ac)
   1.910 -
   1.911 -lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
   1.912 -by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
   1.913 -
   1.914 -lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
   1.915 -by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
   1.916 -
   1.917 -ML
   1.918 -{*
   1.919 -val zdiff_def = thm "zdiff_def";
   1.920 -val int_of_type = thm "int_of_type";
   1.921 -val int_of_eq = thm "int_of_eq";
   1.922 -val int_of_inject = thm "int_of_inject";
   1.923 -val intify_in_int = thm "intify_in_int";
   1.924 -val intify_ident = thm "intify_ident";
   1.925 -val intify_idem = thm "intify_idem";
   1.926 -val int_of_natify = thm "int_of_natify";
   1.927 -val zminus_intify = thm "zminus_intify";
   1.928 -val zadd_intify1 = thm "zadd_intify1";
   1.929 -val zadd_intify2 = thm "zadd_intify2";
   1.930 -val zdiff_intify1 = thm "zdiff_intify1";
   1.931 -val zdiff_intify2 = thm "zdiff_intify2";
   1.932 -val zmult_intify1 = thm "zmult_intify1";
   1.933 -val zmult_intify2 = thm "zmult_intify2";
   1.934 -val zless_intify1 = thm "zless_intify1";
   1.935 -val zless_intify2 = thm "zless_intify2";
   1.936 -val zle_intify1 = thm "zle_intify1";
   1.937 -val zle_intify2 = thm "zle_intify2";
   1.938 -val zminus_congruent = thm "zminus_congruent";
   1.939 -val zminus_type = thm "zminus_type";
   1.940 -val zminus_inject_intify = thm "zminus_inject_intify";
   1.941 -val zminus_inject = thm "zminus_inject";
   1.942 -val zminus = thm "zminus";
   1.943 -val zminus_zminus_intify = thm "zminus_zminus_intify";
   1.944 -val zminus_int0 = thm "zminus_int0";
   1.945 -val zminus_zminus = thm "zminus_zminus";
   1.946 -val not_znegative_int_of = thm "not_znegative_int_of";
   1.947 -val znegative_zminus_int_of = thm "znegative_zminus_int_of";
   1.948 -val not_znegative_imp_zero = thm "not_znegative_imp_zero";
   1.949 -val nat_of_intify = thm "nat_of_intify";
   1.950 -val nat_of_int_of = thm "nat_of_int_of";
   1.951 -val nat_of_type = thm "nat_of_type";
   1.952 -val zmagnitude_int_of = thm "zmagnitude_int_of";
   1.953 -val natify_int_of_eq = thm "natify_int_of_eq";
   1.954 -val zmagnitude_zminus_int_of = thm "zmagnitude_zminus_int_of";
   1.955 -val zmagnitude_type = thm "zmagnitude_type";
   1.956 -val not_zneg_int_of = thm "not_zneg_int_of";
   1.957 -val not_zneg_mag = thm "not_zneg_mag";
   1.958 -val zneg_int_of = thm "zneg_int_of";
   1.959 -val zneg_mag = thm "zneg_mag";
   1.960 -val int_cases = thm "int_cases";
   1.961 -val not_zneg_nat_of_intify = thm "not_zneg_nat_of_intify";
   1.962 -val not_zneg_nat_of = thm "not_zneg_nat_of";
   1.963 -val zneg_nat_of = thm "zneg_nat_of";
   1.964 -val zadd_congruent2 = thm "zadd_congruent2";
   1.965 -val zadd_type = thm "zadd_type";
   1.966 -val zadd = thm "zadd";
   1.967 -val zadd_int0_intify = thm "zadd_int0_intify";
   1.968 -val zadd_int0 = thm "zadd_int0";
   1.969 -val zminus_zadd_distrib = thm "zminus_zadd_distrib";
   1.970 -val zadd_commute = thm "zadd_commute";
   1.971 -val zadd_assoc = thm "zadd_assoc";
   1.972 -val zadd_left_commute = thm "zadd_left_commute";
   1.973 -val zadd_ac = thms "zadd_ac";
   1.974 -val int_of_add = thm "int_of_add";
   1.975 -val int_succ_int_1 = thm "int_succ_int_1";
   1.976 -val int_of_diff = thm "int_of_diff";
   1.977 -val zadd_zminus_inverse = thm "zadd_zminus_inverse";
   1.978 -val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2";
   1.979 -val zadd_int0_right_intify = thm "zadd_int0_right_intify";
   1.980 -val zadd_int0_right = thm "zadd_int0_right";
   1.981 -val zmult_congruent2 = thm "zmult_congruent2";
   1.982 -val zmult_type = thm "zmult_type";
   1.983 -val zmult = thm "zmult";
   1.984 -val zmult_int0 = thm "zmult_int0";
   1.985 -val zmult_int1_intify = thm "zmult_int1_intify";
   1.986 -val zmult_int1 = thm "zmult_int1";
   1.987 -val zmult_commute = thm "zmult_commute";
   1.988 -val zmult_zminus = thm "zmult_zminus";
   1.989 -val zmult_zminus_right = thm "zmult_zminus_right";
   1.990 -val zmult_assoc = thm "zmult_assoc";
   1.991 -val zmult_left_commute = thm "zmult_left_commute";
   1.992 -val zmult_ac = thms "zmult_ac";
   1.993 -val zadd_zmult_distrib = thm "zadd_zmult_distrib";
   1.994 -val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
   1.995 -val int_typechecks = thms "int_typechecks";
   1.996 -val zdiff_type = thm "zdiff_type";
   1.997 -val zminus_zdiff_eq = thm "zminus_zdiff_eq";
   1.998 -val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
   1.999 -val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
  1.1000 -val zadd_zdiff_eq = thm "zadd_zdiff_eq";
  1.1001 -val zdiff_zadd_eq = thm "zdiff_zadd_eq";
  1.1002 -val zless_linear = thm "zless_linear";
  1.1003 -val zless_not_refl = thm "zless_not_refl";
  1.1004 -val neq_iff_zless = thm "neq_iff_zless";
  1.1005 -val zless_imp_intify_neq = thm "zless_imp_intify_neq";
  1.1006 -val zless_imp_succ_zadd = thm "zless_imp_succ_zadd";
  1.1007 -val zless_succ_zadd = thm "zless_succ_zadd";
  1.1008 -val zless_iff_succ_zadd = thm "zless_iff_succ_zadd";
  1.1009 -val zless_int_of = thm "zless_int_of";
  1.1010 -val zless_trans = thm "zless_trans";
  1.1011 -val zless_not_sym = thm "zless_not_sym";
  1.1012 -val zless_asym = thm "zless_asym";
  1.1013 -val zless_imp_zle = thm "zless_imp_zle";
  1.1014 -val zle_linear = thm "zle_linear";
  1.1015 -val zle_refl = thm "zle_refl";
  1.1016 -val zle_eq_refl = thm "zle_eq_refl";
  1.1017 -val zle_anti_sym_intify = thm "zle_anti_sym_intify";
  1.1018 -val zle_anti_sym = thm "zle_anti_sym";
  1.1019 -val zle_trans = thm "zle_trans";
  1.1020 -val zle_zless_trans = thm "zle_zless_trans";
  1.1021 -val zless_zle_trans = thm "zless_zle_trans";
  1.1022 -val not_zless_iff_zle = thm "not_zless_iff_zle";
  1.1023 -val not_zle_iff_zless = thm "not_zle_iff_zless";
  1.1024 -val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
  1.1025 -val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
  1.1026 -val zdiff_zless_iff = thm "zdiff_zless_iff";
  1.1027 -val zless_zdiff_iff = thm "zless_zdiff_iff";
  1.1028 -val zdiff_eq_iff = thm "zdiff_eq_iff";
  1.1029 -val eq_zdiff_iff = thm "eq_zdiff_iff";
  1.1030 -val zdiff_zle_iff = thm "zdiff_zle_iff";
  1.1031 -val zle_zdiff_iff = thm "zle_zdiff_iff";
  1.1032 -val zcompare_rls = thms "zcompare_rls";
  1.1033 -val zadd_left_cancel = thm "zadd_left_cancel";
  1.1034 -val zadd_left_cancel_intify = thm "zadd_left_cancel_intify";
  1.1035 -val zadd_right_cancel = thm "zadd_right_cancel";
  1.1036 -val zadd_right_cancel_intify = thm "zadd_right_cancel_intify";
  1.1037 -val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
  1.1038 -val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
  1.1039 -val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
  1.1040 -val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
  1.1041 -val zadd_zless_mono1 = thm "zadd_zless_mono1";
  1.1042 -val zadd_zless_mono2 = thm "zadd_zless_mono2";
  1.1043 -val zadd_zle_mono1 = thm "zadd_zle_mono1";
  1.1044 -val zadd_zle_mono2 = thm "zadd_zle_mono2";
  1.1045 -val zadd_zle_mono = thm "zadd_zle_mono";
  1.1046 -val zadd_zless_mono = thm "zadd_zless_mono";
  1.1047 -val zminus_zless_zminus = thm "zminus_zless_zminus";
  1.1048 -val zminus_zle_zminus = thm "zminus_zle_zminus";
  1.1049 -val equation_zminus = thm "equation_zminus";
  1.1050 -val zminus_equation = thm "zminus_equation";
  1.1051 -val equation_zminus_intify = thm "equation_zminus_intify";
  1.1052 -val zminus_equation_intify = thm "zminus_equation_intify";
  1.1053 -val zless_zminus = thm "zless_zminus";
  1.1054 -val zminus_zless = thm "zminus_zless";
  1.1055 -val zle_zminus = thm "zle_zminus";
  1.1056 -val zminus_zle = thm "zminus_zle";
  1.1057 -*}
  1.1058 -
  1.1059 -
  1.1060 -end