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