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