src/ZF/IntDiv_ZF.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46993 7371429c527d
child 51686 532e0ac5a66d
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:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
     1
(*  Title:      ZF/IntDiv_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   1999  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
Here is the division algorithm in ML:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     6
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     7
    fun posDivAlg (a,b) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     8
      if a<b then (0,a)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
     9
      else let val (q,r) = posDivAlg(a, 2*b)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    10
               in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    11
           end
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    12
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    13
    fun negDivAlg (a,b) =
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    14
      if 0<=a+b then (~1,a+b)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    15
      else let val (q,r) = negDivAlg(a, 2*b)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    16
               in  if 0<=r-b then (2*q+1, r-b) else (2*q, r)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    17
           end;
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
    fun negateSnd (q,r:int) = (q,~r);
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    20
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    21
    fun divAlg (a,b) = if 0<=a then
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    22
                          if b>0 then posDivAlg (a,b)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    23
                           else if a=0 then (0,0)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    24
                                else negateSnd (negDivAlg (~a,~b))
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    25
                       else
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    26
                          if 0<b then negDivAlg (a,b)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    27
                          else        negateSnd (posDivAlg (~a,~b));
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    28
*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    29
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    30
header{*The Division Operators Div and Mod*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    31
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    32
theory IntDiv_ZF imports IntArith OrderArith begin
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    33
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    34
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    35
  quorem :: "[i,i] => o"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    36
    "quorem == %<a,b> <q,r>.
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    37
                      a = b$*q $+ r &
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    38
                      (#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    39
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    40
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    41
  adjust :: "[i,i] => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    42
    "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    43
                          else <#2$*q,r>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    44
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    45
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    46
(** the division algorithm **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    47
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    48
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    49
  posDivAlg :: "i => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    50
(*for the case a>=0, b>0*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    51
(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    52
    "posDivAlg(ab) ==
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    53
       wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    54
             ab,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    55
             %<a,b> f. if (a$<b | b$<=#0) then <#0,a>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    56
                       else adjust(b, f ` <a,#2$*b>))"
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    59
(*for the case a<0, b>0*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    60
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    61
  negDivAlg :: "i => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    62
(*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    63
    "negDivAlg(ab) ==
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    64
       wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    65
             ab,
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32149
diff changeset
    66
             %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    67
                       else adjust(b, f ` <a,#2$*b>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    68
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    69
(*for the general case @{term"b\<noteq>0"}*)
26056
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
  negateSnd :: "i => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    73
    "negateSnd == %<q,r>. <q, $-r>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    74
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    75
  (*The full division algorithm considers all possible signs for a, b
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    76
    including the special case a=0, b<0, because negDivAlg requires a<0*)
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
  divAlg :: "i => i"  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    79
    "divAlg ==
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    80
       %<a,b>. if #0 $<= a then
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    81
                  if #0 $<= b then posDivAlg (<a,b>)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    82
                  else if a=#0 then <#0,#0>
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    83
                       else negateSnd (negDivAlg (<$-a,$-b>))
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    84
               else
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    85
                  if #0$<b then negDivAlg (<a,b>)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    86
                  else         negateSnd (posDivAlg (<$-a,$-b>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    87
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    88
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    89
  zdiv  :: "[i,i]=>i"                    (infixl "zdiv" 70)  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    90
    "a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    91
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    92
definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    93
  zmod  :: "[i,i]=>i"                    (infixl "zmod" 70)  where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    94
    "a zmod b == snd (divAlg (<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    95
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    96
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    97
(** Some basic laws by Sidi Ehmety (need linear arithmetic!) **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    98
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
    99
lemma zspos_add_zspos_imp_zspos: "[| #0 $< x;  #0 $< y |] ==> #0 $< x $+ y"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   100
apply (rule_tac y = "y" in zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   101
apply (rule_tac [2] zdiff_zless_iff [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   102
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   103
done
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
lemma zpos_add_zpos_imp_zpos: "[| #0 $<= x;  #0 $<= y |] ==> #0 $<= x $+ y"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   106
apply (rule_tac y = "y" in zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   107
apply (rule_tac [2] zdiff_zle_iff [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   108
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   109
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   110
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   111
lemma zneg_add_zneg_imp_zneg: "[| x $< #0;  y $< #0 |] ==> x $+ y $< #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   112
apply (rule_tac y = "y" in zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   113
apply (rule zless_zdiff_iff [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   114
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   115
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   116
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   117
(* this theorem is used below *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   118
lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   119
     "[| x $<= #0;  y $<= #0 |] ==> x $+ y $<= #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   120
apply (rule_tac y = "y" in zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   121
apply (rule zle_zdiff_iff [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   122
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   123
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   124
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   125
lemma zero_lt_zmagnitude: "[| #0 $< k; k \<in> int |] ==> 0 < zmagnitude(k)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   126
apply (drule zero_zless_imp_znegative_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   127
apply (drule_tac [2] zneg_int_of)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   128
apply (auto simp add: zminus_equation [of k])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   129
apply (subgoal_tac "0 < zmagnitude ($# succ (n))")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   130
 apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   131
apply (simp only: zmagnitude_int_of)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   132
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   133
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   134
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   135
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   136
(*** Inequality lemmas involving $#succ(m) ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   137
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   138
lemma zless_add_succ_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   139
     "(w $< z $+ $# succ(m)) \<longleftrightarrow> (w $< z $+ $#m | intify(w) = z $+ $#m)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   140
apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   141
apply (rule_tac [3] x = "0" in bexI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   142
apply (cut_tac m = "m" in int_succ_int_1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   143
apply (cut_tac m = "n" in int_succ_int_1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   144
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   145
apply (erule natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   146
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   147
apply (rule_tac x = "succ (n) " in bexI)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   148
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   149
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   150
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   151
lemma zadd_succ_lemma:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   152
     "z \<in> int ==> (w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   153
apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   154
apply (auto intro: zle_anti_sym elim: zless_asym
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   155
            simp add: zless_imp_zle not_zless_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   156
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   157
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   158
lemma zadd_succ_zle_iff: "(w $+ $# succ(m) $<= z) \<longleftrightarrow> (w $+ $#m $< z)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   159
apply (cut_tac z = "intify (z)" in zadd_succ_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   160
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   161
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   162
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   163
(** Inequality reasoning **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   164
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   165
lemma zless_add1_iff_zle: "(w $< z $+ #1) \<longleftrightarrow> (w$<=z)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   166
apply (subgoal_tac "#1 = $# 1")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   167
apply (simp only: zless_add_succ_iff zle_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   168
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   169
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   170
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   171
lemma add1_zle_iff: "(w $+ #1 $<= z) \<longleftrightarrow> (w $< z)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   172
apply (subgoal_tac "#1 = $# 1")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   173
apply (simp only: zadd_succ_zle_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   174
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   175
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   176
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   177
lemma add1_left_zle_iff: "(#1 $+ w $<= z) \<longleftrightarrow> (w $< z)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   178
apply (subst zadd_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   179
apply (rule add1_zle_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   180
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   181
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   182
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   183
(*** Monotonicity of Multiplication ***)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   184
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   185
lemma zmult_mono_lemma: "k \<in> nat ==> i $<= j ==> i $* $#k $<= j $* $#k"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   186
apply (induct_tac "k")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   187
 prefer 2 apply (subst int_succ_int_1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   188
apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   189
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   190
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   191
lemma zmult_zle_mono1: "[| i $<= j;  #0 $<= k |] ==> i$*k $<= j$*k"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   192
apply (subgoal_tac "i $* intify (k) $<= j $* intify (k) ")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   193
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
   194
apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   195
apply (rule_tac [3] zmult_mono_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   196
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   197
apply (simp add: znegative_iff_zless_0 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
   198
done
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_zle_mono1_neg: "[| i $<= j;  k $<= #0 |] ==> j$*k $<= i$*k"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   201
apply (rule zminus_zle_zminus [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   202
apply (simp del: zmult_zminus_right
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   203
            add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   204
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   205
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   206
lemma zmult_zle_mono2: "[| i $<= j;  #0 $<= k |] ==> k$*i $<= k$*j"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   207
apply (drule zmult_zle_mono1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   208
apply (simp_all add: zmult_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   209
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   210
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   211
lemma zmult_zle_mono2_neg: "[| i $<= j;  k $<= #0 |] ==> k$*j $<= k$*i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   212
apply (drule zmult_zle_mono1_neg)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   213
apply (simp_all add: zmult_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   214
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   215
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   216
(* $<= monotonicity, BOTH arguments*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   217
lemma zmult_zle_mono:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   218
     "[| i $<= j;  k $<= l;  #0 $<= j;  #0 $<= k |] ==> i$*k $<= j$*l"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   219
apply (erule zmult_zle_mono1 [THEN zle_trans])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   220
apply assumption
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   221
apply (erule zmult_zle_mono2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   222
apply assumption
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   223
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   224
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   225
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   226
(** strict, in 1st argument; proof is by induction on k>0 **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   227
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   228
lemma zmult_zless_mono2_lemma [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   229
     "[| i$<j; k \<in> nat |] ==> 0<k \<longrightarrow> $#k $* i $< $#k $* j"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   230
apply (induct_tac "k")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   231
 prefer 2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   232
 apply (subst int_succ_int_1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   233
 apply (erule natE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   234
apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   235
apply (frule nat_0_le)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   236
apply (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j) ")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   237
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
   238
apply (rule zadd_zless_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   239
apply (simp_all (no_asm_simp) add: zle_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   240
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   241
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   242
lemma zmult_zless_mono2: "[| i$<j;  #0 $< k |] ==> k$*i $< k$*j"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   243
apply (subgoal_tac "intify (k) $* i $< intify (k) $* j")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   244
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
   245
apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   246
apply (rule_tac [3] zmult_zless_mono2_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   247
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   248
apply (simp add: znegative_iff_zless_0)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   249
apply (drule zless_trans, assumption)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   250
apply (auto simp add: zero_lt_zmagnitude)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   251
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   252
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   253
lemma zmult_zless_mono1: "[| i$<j;  #0 $< k |] ==> i$*k $< j$*k"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   254
apply (drule zmult_zless_mono2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   255
apply (simp_all add: zmult_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   256
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   257
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   258
(* < monotonicity, BOTH arguments*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   259
lemma zmult_zless_mono:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   260
     "[| i $< j;  k $< l;  #0 $< j;  #0 $< k |] ==> i$*k $< j$*l"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   261
apply (erule zmult_zless_mono1 [THEN zless_trans])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   262
apply assumption
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   263
apply (erule zmult_zless_mono2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   264
apply assumption
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   265
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   266
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   267
lemma zmult_zless_mono1_neg: "[| i $< j;  k $< #0 |] ==> j$*k $< i$*k"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   268
apply (rule zminus_zless_zminus [THEN iffD1])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   269
apply (simp del: zmult_zminus_right
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   270
            add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   271
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   272
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   273
lemma zmult_zless_mono2_neg: "[| i $< j;  k $< #0 |] ==> k$*j $< k$*i"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   274
apply (rule zminus_zless_zminus [THEN iffD1])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   275
apply (simp del: zmult_zminus
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   276
            add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   277
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   278
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   279
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   280
(** Products of zeroes **)
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 zmult_eq_lemma:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   283
     "[| m \<in> int; n \<in> int |] ==> (m = #0 | n = #0) \<longleftrightarrow> (m$*n = #0)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   284
apply (case_tac "m $< #0")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   285
apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   286
apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   287
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   288
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   289
lemma zmult_eq_0_iff [iff]: "(m$*n = #0) \<longleftrightarrow> (intify(m) = #0 | intify(n) = #0)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   290
apply (simp add: zmult_eq_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   291
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   292
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   293
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   294
(** Cancellation laws for k*m < k*n and m*k < n*k, also for @{text"\<le>"} and =,
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   295
    but not (yet?) for k*m < n*k. **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   296
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   297
lemma zmult_zless_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   298
     "[| k \<in> int; m \<in> int; n \<in> int |]
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   299
      ==> (m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   300
apply (case_tac "k = #0")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   301
apply (auto simp add: neq_iff_zless zmult_zless_mono1 zmult_zless_mono1_neg)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   302
apply (auto simp add: not_zless_iff_zle
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   303
                      not_zle_iff_zless [THEN iff_sym, of "m$*k"]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   304
                      not_zle_iff_zless [THEN iff_sym, of m])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   305
apply (auto elim: notE
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   306
            simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   307
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   308
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   309
lemma zmult_zless_cancel2:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   310
     "(m$*k $< n$*k) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   311
apply (cut_tac k = "intify (k)" and m = "intify (m)" and n = "intify (n)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   312
       in zmult_zless_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   313
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   314
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   315
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   316
lemma zmult_zless_cancel1:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   317
     "(k$*m $< k$*n) \<longleftrightarrow> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   318
by (simp add: zmult_commute [of k] zmult_zless_cancel2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   319
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   320
lemma zmult_zle_cancel2:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   321
     "(m$*k $<= n$*k) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   322
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   323
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   324
lemma zmult_zle_cancel1:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   325
     "(k$*m $<= k$*n) \<longleftrightarrow> ((#0 $< k \<longrightarrow> m$<=n) & (k $< #0 \<longrightarrow> n$<=m))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   326
by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   327
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   328
lemma int_eq_iff_zle: "[| m \<in> int; n \<in> int |] ==> m=n \<longleftrightarrow> (m $<= n & n $<= m)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   329
apply (blast intro: zle_refl zle_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   330
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   331
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   332
lemma zmult_cancel2_lemma:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   333
     "[| k \<in> int; m \<in> int; n \<in> int |] ==> (m$*k = n$*k) \<longleftrightarrow> (k=#0 | m=n)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   334
apply (simp add: int_eq_iff_zle [of "m$*k"] int_eq_iff_zle [of m])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   335
apply (auto simp add: zmult_zle_cancel2 neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   336
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   337
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   338
lemma zmult_cancel2 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   339
     "(m$*k = n$*k) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   340
apply (rule iff_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   341
apply (rule_tac [2] zmult_cancel2_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   342
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   343
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   344
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   345
lemma zmult_cancel1 [simp]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   346
     "(k$*m = k$*n) \<longleftrightarrow> (intify(k) = #0 | intify(m) = intify(n))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   347
by (simp add: zmult_commute [of k] zmult_cancel2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   348
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   349
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   350
subsection{* Uniqueness and monotonicity of quotients and remainders *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   351
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   352
lemma unique_quotient_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   353
     "[| b$*q' $+ r' $<= b$*q $+ r;  #0 $<= r';  #0 $< b;  r $< b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   354
      ==> q' $<= q"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   355
apply (subgoal_tac "r' $+ b $* (q'$-q) $<= r")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   356
 prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   357
apply (subgoal_tac "#0 $< b $* (#1 $+ q $- q') ")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   358
 prefer 2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   359
 apply (erule zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   360
 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   361
 apply (erule zle_zless_trans)
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   362
 apply simp
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   363
apply (subgoal_tac "b $* q' $< b $* (#1 $+ q)")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   364
 prefer 2
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   365
 apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   366
apply (auto elim: zless_asym
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   367
        simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   368
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   369
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   370
lemma unique_quotient_lemma_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   371
     "[| b$*q' $+ r' $<= b$*q $+ r;  r $<= #0;  b $< #0;  b $< r' |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   372
      ==> q $<= q'"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   373
apply (rule_tac b = "$-b" and r = "$-r'" and r' = "$-r"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   374
       in unique_quotient_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   375
apply (auto simp del: zminus_zadd_distrib
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   376
            simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   377
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   378
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   379
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   380
lemma unique_quotient:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   381
     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   382
         q \<in> int; q' \<in> int |] ==> q = q'"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   383
apply (simp add: split_ifs quorem_def neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   384
apply safe
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   385
apply simp_all
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   386
apply (blast intro: zle_anti_sym
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   387
             dest: zle_eq_refl [THEN unique_quotient_lemma]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   388
                   zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   389
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   390
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   391
lemma unique_remainder:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   392
     "[| quorem (<a,b>, <q,r>);  quorem (<a,b>, <q',r'>);  b \<in> int; b \<noteq> #0;
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   393
         q \<in> int; q' \<in> int;
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   394
         r \<in> int; r' \<in> int |] ==> r = r'"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   395
apply (subgoal_tac "q = q'")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   396
 prefer 2 apply (blast intro: unique_quotient)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   397
apply (simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   398
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   399
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   400
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   401
subsection{*Correctness of posDivAlg,
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   402
           the Division Algorithm for @{text "a\<ge>0"} and @{text "b>0"} *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   403
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   404
lemma adjust_eq [simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   405
     "adjust(b, <q,r>) = (let diff = r$-b in
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   406
                          if #0 $<= diff then <#2$*q $+ #1,diff>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   407
                                         else <#2$*q,r>)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   408
by (simp add: Let_def adjust_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   409
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   410
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   411
lemma posDivAlg_termination:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   412
     "[| #0 $< b; ~ a $< b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   413
      ==> nat_of(a $- #2 $\<times> b $+ #1) < nat_of(a $- b $+ #1)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   414
apply (simp (no_asm) add: zless_nat_conj)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   415
apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   416
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   417
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   418
lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   419
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   420
lemma posDivAlg_eqn:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   421
     "[| #0 $< b; a \<in> int; b \<in> int |] ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   422
      posDivAlg(<a,b>) =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   423
       (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   424
apply (rule posDivAlg_unfold [THEN trans])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   425
apply (simp add: vimage_iff 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
   426
apply (blast intro: posDivAlg_termination)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   427
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   428
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   429
lemma posDivAlg_induct_lemma [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   430
  assumes prem:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   431
        "!!a b. [| a \<in> int; b \<in> int;
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   432
                   ~ (a $< b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |] ==> P(<a,b>)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   433
  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   434
using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of (a $- b $+ #1)"]
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   435
proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   436
  case (step x)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   437
  hence uv: "u \<in> int" "v \<in> int" by auto
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   438
  thus ?case
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   439
    apply (rule prem) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   440
    apply (rule impI) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   441
    apply (rule step) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   442
    apply (auto simp add: step uv not_zle_iff_zless posDivAlg_termination)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   443
    done
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   444
qed
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   445
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   446
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   447
lemma posDivAlg_induct [consumes 2]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   448
  assumes u_int: "u \<in> int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   449
      and v_int: "v \<in> int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   450
      and ih: "!!a b. [| a \<in> int; b \<in> int;
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   451
                     ~ (a $< b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |] ==> P(a,b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   452
  shows "P(u,v)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   453
apply (subgoal_tac "(%<x,y>. P (x,y)) (<u,v>)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   454
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   455
apply (rule posDivAlg_induct_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   456
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
   457
apply (rule ih)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   458
apply (auto simp add: u_int v_int)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   459
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   460
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   461
(*FIXME: use intify in integ_of so that we always have @{term"integ_of w \<in> int"}.
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   462
    then this rewrite can work for all constants!!*)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   463
lemma intify_eq_0_iff_zle: "intify(m) = #0 \<longleftrightarrow> (m $<= #0 & #0 $<= m)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   464
  by (simp add: int_eq_iff_zle)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   465
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   466
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   467
subsection{* Some convenient biconditionals for products of signs *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   468
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   469
lemma zmult_pos: "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   470
  by (drule zmult_zless_mono1, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   471
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   472
lemma zmult_neg: "[| i $< #0; j $< #0 |] ==> #0 $< i $* j"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   473
  by (drule zmult_zless_mono1_neg, auto)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   474
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   475
lemma zmult_pos_neg: "[| #0 $< i; j $< #0 |] ==> i $* j $< #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   476
  by (drule zmult_zless_mono1_neg, auto)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   477
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   478
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   479
(** Inequality reasoning **)
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 int_0_less_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   482
     "[| x \<in> int; y \<in> int |]
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   483
      ==> (#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   484
apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   485
apply (rule ccontr)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   486
apply (rule_tac [2] ccontr)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   487
apply (auto simp add: zle_def not_zless_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   488
apply (erule_tac P = "#0$< x$* y" in rev_mp)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   489
apply (erule_tac [2] P = "#0$< x$* y" in rev_mp)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   490
apply (drule zmult_pos_neg, assumption)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   491
 prefer 2
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   492
 apply (drule zmult_pos_neg, assumption)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   493
apply (auto dest: zless_not_sym simp add: zmult_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   494
done
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
lemma int_0_less_mult_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   497
     "(#0 $< x $* y) \<longleftrightarrow> (#0 $< x & #0 $< y | x $< #0 & y $< #0)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   498
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   499
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   500
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   501
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   502
lemma int_0_le_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   503
     "[| x \<in> int; y \<in> int |]
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   504
      ==> (#0 $<= x $* y) \<longleftrightarrow> (#0 $<= x & #0 $<= y | x $<= #0 & y $<= #0)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   505
by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   506
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   507
lemma int_0_le_mult_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   508
     "(#0 $<= x $* y) \<longleftrightarrow> ((#0 $<= x & #0 $<= y) | (x $<= #0 & y $<= #0))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   509
apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   510
apply auto
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
lemma zmult_less_0_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   514
     "(x $* y $< #0) \<longleftrightarrow> (#0 $< x & y $< #0 | x $< #0 & #0 $< y)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   515
apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   516
apply (auto dest: zless_not_sym simp add: not_zle_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   517
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   518
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   519
lemma zmult_le_0_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   520
     "(x $* y $<= #0) \<longleftrightarrow> (#0 $<= x & y $<= #0 | x $<= #0 & #0 $<= y)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   521
by (auto dest: zless_not_sym
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   522
         simp add: int_0_less_mult_iff 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
   523
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   524
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   525
(*Typechecking for posDivAlg*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   526
lemma posDivAlg_type [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   527
     "[| a \<in> int; b \<in> int |] ==> posDivAlg(<a,b>) \<in> int * int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   528
apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   529
apply assumption+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   530
apply (case_tac "#0 $< ba")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   531
 apply (simp add: posDivAlg_eqn adjust_def integ_of_type
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   532
             split add: split_if_asm)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   533
 apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   534
 apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   535
apply (simp add: not_zless_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   536
apply (subst posDivAlg_unfold)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   537
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   538
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   539
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   540
(*Correctness of posDivAlg: it computes quotients correctly*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   541
lemma posDivAlg_correct [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   542
     "[| a \<in> int; b \<in> int |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   543
      ==> #0 $<= a \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, posDivAlg(<a,b>))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   544
apply (rule_tac u = "a" and v = "b" in posDivAlg_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   545
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   546
   apply (simp_all add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   547
   txt{*base case: a<b*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   548
   apply (simp add: posDivAlg_eqn)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   549
  apply (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
   550
 apply (simp add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   551
txt{*main argument*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   552
apply (subst posDivAlg_eqn)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   553
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
   554
apply (erule splitE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   555
apply (rule posDivAlg_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   556
apply (simp_all add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   557
apply (auto simp add: zadd_zmult_distrib2 Let_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   558
txt{*now just linear arithmetic*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   559
apply (simp add: not_zle_iff_zless zdiff_zless_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   560
done
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   563
subsection{*Correctness of negDivAlg, the division algorithm for a<0 and b>0*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   564
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   565
lemma negDivAlg_termination:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   566
     "[| #0 $< b; a $+ b $< #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   567
      ==> nat_of($- a $- #2 $* b) < nat_of($- a $- b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   568
apply (simp (no_asm) add: zless_nat_conj)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   569
apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   570
                 zless_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   571
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   572
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   573
lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure]
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 negDivAlg_eqn:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   576
     "[| #0 $< b; a \<in> int; b \<in> int |] ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   577
      negDivAlg(<a,b>) =
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   578
       (if #0 $<= a$+b then <#-1,a$+b>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   579
                       else adjust(b, negDivAlg (<a, #2$*b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   580
apply (rule negDivAlg_unfold [THEN trans])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   581
apply (simp (no_asm_simp) add: vimage_iff 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
   582
apply (blast intro: negDivAlg_termination)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   583
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   584
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   585
lemma negDivAlg_induct_lemma [rule_format]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   586
  assumes prem:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   587
        "!!a b. [| a \<in> int; b \<in> int;
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   588
                   ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(<a, #2 $* b>) |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   589
                ==> P(<a,b>)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   590
  shows "<u,v> \<in> int*int \<Longrightarrow> P(<u,v>)"
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   591
using wf_measure [where A = "int*int" and f = "%<a,b>.nat_of ($- a $- b)"]
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   592
proof (induct "<u,v>" arbitrary: u v rule: wf_induct)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   593
  case (step x)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   594
  hence uv: "u \<in> int" "v \<in> int" by auto
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   595
  thus ?case
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   596
    apply (rule prem) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   597
    apply (rule impI) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   598
    apply (rule step) 
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   599
    apply (auto simp add: step uv not_zle_iff_zless negDivAlg_termination)
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   600
    done
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   601
qed
26056
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
lemma negDivAlg_induct [consumes 2]:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   604
  assumes u_int: "u \<in> int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   605
      and v_int: "v \<in> int"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   606
      and ih: "!!a b. [| a \<in> int; b \<in> int;
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   607
                         ~ (#0 $<= a $+ b | b $<= #0) \<longrightarrow> P(a, #2 $* b) |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   608
                      ==> P(a,b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   609
  shows "P(u,v)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   610
apply (subgoal_tac " (%<x,y>. P (x,y)) (<u,v>)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   611
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   612
apply (rule negDivAlg_induct_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   613
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
   614
apply (rule ih)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   615
apply (auto simp add: u_int v_int)
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   619
(*Typechecking for negDivAlg*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   620
lemma negDivAlg_type:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   621
     "[| a \<in> int; b \<in> int |] ==> negDivAlg(<a,b>) \<in> int * int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   622
apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   623
apply assumption+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   624
apply (case_tac "#0 $< ba")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   625
 apply (simp add: negDivAlg_eqn adjust_def integ_of_type
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   626
             split add: split_if_asm)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   627
 apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   628
 apply (simp add: int_0_less_mult_iff not_zle_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   629
apply (simp add: not_zless_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   630
apply (subst negDivAlg_unfold)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   631
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   632
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   633
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   634
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   635
(*Correctness of negDivAlg: it computes quotients correctly
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   636
  It doesn't work if a=0 because the 0/b=0 rather than -1*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   637
lemma negDivAlg_correct [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   638
     "[| a \<in> int; b \<in> int |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   639
      ==> a $< #0 \<longrightarrow> #0 $< b \<longrightarrow> quorem (<a,b>, negDivAlg(<a,b>))"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   640
apply (rule_tac u = "a" and v = "b" in negDivAlg_induct)
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
   apply (simp_all add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   643
   txt{*base case: @{term "0$<=a$+b"}*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   644
   apply (simp add: negDivAlg_eqn)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   645
  apply (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
   646
 apply (simp add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   647
txt{*main argument*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   648
apply (subst negDivAlg_eqn)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   649
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
   650
apply (erule splitE)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   651
apply (rule negDivAlg_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   652
apply (simp_all add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   653
apply (auto simp add: zadd_zmult_distrib2 Let_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   654
txt{*now just linear arithmetic*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   655
apply (simp add: not_zle_iff_zless zdiff_zless_iff)
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   659
subsection{* Existence shown by proving the division algorithm to be correct *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   660
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   661
(*the case a=0*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   662
lemma quorem_0: "[|b \<noteq> #0;  b \<in> int|] ==> quorem (<#0,b>, <#0,#0>)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   663
by (force simp add: quorem_def neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   664
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   665
lemma posDivAlg_zero_divisor: "posDivAlg(<a,#0>) = <#0,a>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   666
apply (subst posDivAlg_unfold)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   667
apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   668
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   669
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   670
lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   671
apply (subst posDivAlg_unfold)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   672
apply (simp add: not_zle_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   673
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   674
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   675
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   676
(*Needed below.  Actually it's an equivalence.*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   677
lemma linear_arith_lemma: "~ (#0 $<= #-1 $+ b) ==> (b $<= #0)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   678
apply (simp add: not_zle_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   679
apply (drule zminus_zless_zminus [THEN iffD2])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   680
apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   681
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   682
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   683
lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b$-#1>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   684
apply (subst negDivAlg_unfold)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   685
apply (simp add: linear_arith_lemma integ_of_type vimage_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   686
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   687
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   688
lemma negateSnd_eq [simp]: "negateSnd (<q,r>) = <q, $-r>"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   689
apply (unfold negateSnd_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   690
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   691
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   692
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   693
lemma negateSnd_type: "qr \<in> int * int ==> negateSnd (qr) \<in> int * int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   694
apply (unfold negateSnd_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   695
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   696
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   697
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   698
lemma quorem_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   699
     "[|quorem (<$-a,$-b>, qr);  a \<in> int;  b \<in> int;  qr \<in> int * int|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   700
      ==> quorem (<a,b>, negateSnd(qr))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   701
apply clarify
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   702
apply (auto elim: zless_asym simp add: quorem_def zless_zminus)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   703
txt{*linear arithmetic from here on*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   704
apply (simp_all add: zminus_equation [of a] zminus_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   705
apply (cut_tac [2] z = "b" and w = "#0" in zless_linear)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   706
apply (cut_tac [1] z = "b" and w = "#0" in zless_linear)
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
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   709
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   710
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   711
lemma divAlg_correct:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   712
     "[|b \<noteq> #0;  a \<in> int;  b \<in> int|] ==> quorem (<a,b>, divAlg(<a,b>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   713
apply (auto simp add: quorem_0 divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   714
apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   715
                    posDivAlg_type negDivAlg_type)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   716
apply (auto simp add: quorem_def neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   717
txt{*linear arithmetic from here on*}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   718
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
   719
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   720
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   721
lemma divAlg_type: "[|a \<in> int;  b \<in> int|] ==> divAlg(<a,b>) \<in> int * int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   722
apply (auto simp add: divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   723
apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   724
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   725
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   726
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   727
(** intify cancellation **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   728
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   729
lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   730
  by (simp add: zdiv_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   731
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   732
lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   733
  by (simp add: zdiv_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   734
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   735
lemma zdiv_type [iff,TC]: "z zdiv w \<in> int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   736
apply (unfold zdiv_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   737
apply (blast intro: fst_type divAlg_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   738
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   739
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   740
lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   741
  by (simp add: zmod_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   742
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   743
lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   744
  by (simp add: zmod_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   745
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   746
lemma zmod_type [iff,TC]: "z zmod w \<in> int"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   747
apply (unfold zmod_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   748
apply (rule snd_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   749
apply (blast intro: divAlg_type)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   750
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   751
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   752
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   753
(** Arbitrary definitions for division by zero.  Useful to simplify
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   754
    certain equations **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   755
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   756
lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   757
  by (simp add: zdiv_def divAlg_def posDivAlg_zero_divisor)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   758
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   759
lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
   760
  by (simp add: zmod_def divAlg_def posDivAlg_zero_divisor)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   761
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   762
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   763
(** Basic laws about division and remainder **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   764
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   765
lemma raw_zmod_zdiv_equality:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   766
     "[| a \<in> int; b \<in> int |] ==> a = b $* (a zdiv b) $+ (a zmod b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   767
apply (case_tac "b = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   768
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   769
apply (cut_tac a = "a" and b = "b" in divAlg_correct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   770
apply (auto simp add: quorem_def zdiv_def zmod_def split_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   771
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   772
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   773
lemma zmod_zdiv_equality: "intify(a) = b $* (a zdiv b) $+ (a zmod b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   774
apply (rule trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   775
apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   776
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   777
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   778
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   779
lemma pos_mod: "#0 $< b ==> #0 $<= a zmod b & a zmod b $< b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   780
apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   781
apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   782
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   783
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   784
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   785
lemmas pos_mod_sign = pos_mod [THEN conjunct1]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   786
  and pos_mod_bound = pos_mod [THEN conjunct2]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   787
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   788
lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   789
apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   790
apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   791
apply (blast dest: zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   792
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
   793
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   794
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   795
lemmas neg_mod_sign = neg_mod [THEN conjunct1]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   796
  and neg_mod_bound = neg_mod [THEN conjunct2]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   797
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   798
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   799
(** proving general properties of zdiv and zmod **)
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 quorem_div_mod:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   802
     "[|b \<noteq> #0;  a \<in> int;  b \<in> int |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   803
      ==> quorem (<a,b>, <a zdiv b, a zmod b>)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   804
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   805
apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   806
                      neg_mod_sign neg_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   807
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   808
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   809
(*Surely quorem(<a,b>,<q,r>) implies @{term"a \<in> int"}, but it doesn't matter*)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   810
lemma quorem_div:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   811
     "[| quorem(<a,b>,<q,r>);  b \<noteq> #0;  a \<in> int;  b \<in> int;  q \<in> int |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   812
      ==> a zdiv b = q"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   813
by (blast intro: quorem_div_mod [THEN unique_quotient])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   814
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   815
lemma quorem_mod:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   816
     "[| quorem(<a,b>,<q,r>); b \<noteq> #0; a \<in> int; b \<in> int; q \<in> int; r \<in> int |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   817
      ==> a zmod b = r"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   818
by (blast intro: quorem_div_mod [THEN unique_remainder])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   819
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   820
lemma zdiv_pos_pos_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   821
     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zdiv b = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   822
apply (rule quorem_div)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   823
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   824
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   825
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   826
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   827
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   828
lemma zdiv_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zdiv b = #0"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   829
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   830
       in zdiv_pos_pos_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   831
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   832
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   833
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   834
lemma zdiv_neg_neg_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   835
     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zdiv b = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   836
apply (rule_tac r = "a" in quorem_div)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   837
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   838
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   839
apply (blast dest: zle_zless_trans zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   840
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   841
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   842
lemma zdiv_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zdiv b = #0"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   843
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   844
       in zdiv_neg_neg_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   845
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   846
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   847
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   848
lemma zadd_le_0_lemma: "[| a$+b $<= #0;  #0 $< a;  #0 $< b |] ==> False"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   849
apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   850
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
   851
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
   852
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   853
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   854
lemma zdiv_pos_neg_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   855
     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   856
apply (rule_tac r = "a $+ b" in quorem_div)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   857
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   858
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   859
apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   860
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   861
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   862
lemma zdiv_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zdiv b = #-1"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   863
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   864
       in zdiv_pos_neg_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   865
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   866
done
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
(*There is no zdiv_neg_pos_trivial because  #0 zdiv b = #0 would supersede it*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   869
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   870
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   871
lemma zmod_pos_pos_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   872
     "[| a \<in> int;  b \<in> int;  #0 $<= a;  a $< b |] ==> a zmod b = a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   873
apply (rule_tac q = "#0" in quorem_mod)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   874
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   875
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   876
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   877
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   878
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   879
lemma zmod_pos_pos_trivial: "[| #0 $<= a;  a $< b |] ==> a zmod b = intify(a)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   880
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   881
       in zmod_pos_pos_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   882
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   883
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   884
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   885
lemma zmod_neg_neg_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   886
     "[| a \<in> int;  b \<in> int;  a $<= #0;  b $< a |] ==> a zmod b = a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   887
apply (rule_tac q = "#0" in quorem_mod)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   888
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   889
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   890
apply (blast dest: zle_zless_trans zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   891
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   892
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   893
lemma zmod_neg_neg_trivial: "[| a $<= #0;  b $< a |] ==> a zmod b = intify(a)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   894
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   895
       in zmod_neg_neg_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   896
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   897
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   898
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   899
lemma zmod_pos_neg_trivial_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   900
     "[| a \<in> int;  b \<in> int;  #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   901
apply (rule_tac q = "#-1" in quorem_mod)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   902
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   903
(*linear arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   904
apply (blast dest: zadd_le_0_lemma zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   905
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   906
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   907
lemma zmod_pos_neg_trivial: "[| #0 $< a;  a$+b $<= #0 |] ==> a zmod b = a$+b"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   908
apply (cut_tac a = "intify (a)" and b = "intify (b)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   909
       in zmod_pos_neg_trivial_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   910
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   911
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   912
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   913
(*There is no zmod_neg_pos_trivial...*)
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
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   916
(*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   917
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   918
lemma zdiv_zminus_zminus_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   919
     "[|a \<in> int;  b \<in> int|] ==> ($-a) zdiv ($-b) = a zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   920
apply (case_tac "b = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   921
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   922
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   923
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   924
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   925
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   926
lemma zdiv_zminus_zminus [simp]: "($-a) zdiv ($-b) = a zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   927
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   928
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   929
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   930
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   931
(*Simpler laws such as -a zmod b = -(a zmod b) FAIL*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   932
lemma zmod_zminus_zminus_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   933
     "[|a \<in> int;  b \<in> int|] ==> ($-a) zmod ($-b) = $- (a zmod b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   934
apply (case_tac "b = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   935
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   936
apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   937
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   938
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   939
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   940
lemma zmod_zminus_zminus [simp]: "($-a) zmod ($-b) = $- (a zmod b)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   941
apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   942
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   943
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   944
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   945
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   946
subsection{* division of a number by itself *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   947
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   948
lemma self_quotient_aux1: "[| #0 $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   949
apply (subgoal_tac "#0 $< a$*q")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   950
apply (cut_tac w = "#0" and z = "q" in add1_zle_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   951
apply (simp add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   952
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
   953
(*linear arithmetic...*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   954
apply (drule_tac t = "%x. x $- r" in subst_context)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   955
apply (drule sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   956
apply (simp add: zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   957
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   958
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   959
lemma self_quotient_aux2: "[| #0 $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   960
apply (subgoal_tac "#0 $<= a$* (#1$-q)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   961
 apply (simp add: int_0_le_mult_iff zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   962
 apply (blast dest: zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   963
apply (simp add: zdiff_zmult_distrib2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   964
apply (drule_tac t = "%x. x $- a $* q" in subst_context)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   965
apply (simp add: zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   966
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   967
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   968
lemma self_quotient:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   969
     "[| quorem(<a,a>,<q,r>);  a \<in> int;  q \<in> int;  a \<noteq> #0|] ==> q = #1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   970
apply (simp add: split_ifs quorem_def neq_iff_zless)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   971
apply (rule zle_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   972
apply safe
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   973
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   974
prefer 4 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
   975
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
   976
apply (rule_tac [3] a = "$-a" and r = "$-r" in self_quotient_aux1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   977
apply (rule_tac a = "$-a" and r = "$-r" in self_quotient_aux2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   978
apply (rule_tac [6] zminus_equation [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   979
apply (rule_tac [2] zminus_equation [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   980
apply (force intro: self_quotient_aux1 self_quotient_aux2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   981
  simp add: zadd_commute zmult_zminus)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   982
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   983
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   984
lemma self_remainder:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   985
     "[|quorem(<a,a>,<q,r>); a \<in> int; q \<in> int; r \<in> int; a \<noteq> #0|] ==> r = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   986
apply (frule self_quotient)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   987
apply (auto simp add: quorem_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   988
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   989
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   990
lemma zdiv_self_raw: "[|a \<noteq> #0; a \<in> int|] ==> a zdiv a = #1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   991
apply (blast intro: quorem_div_mod [THEN self_quotient])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   992
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   993
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   994
lemma zdiv_self [simp]: "intify(a) \<noteq> #0 ==> a zdiv a = #1"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   995
apply (drule zdiv_self_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   996
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   997
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   998
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
   999
(*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1000
lemma zmod_self_raw: "a \<in> int ==> a zmod a = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1001
apply (case_tac "a = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1002
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1003
apply (blast intro: quorem_div_mod [THEN self_remainder])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1004
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1005
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1006
lemma zmod_self [simp]: "a zmod a = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1007
apply (cut_tac a = "intify (a)" in zmod_self_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1008
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1009
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1010
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1011
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1012
subsection{* Computation of division and remainder *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1013
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1014
lemma zdiv_zero [simp]: "#0 zdiv b = #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1015
  by (simp add: zdiv_def divAlg_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1016
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1017
lemma zdiv_eq_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1018
  by (simp (no_asm_simp) add: zdiv_def divAlg_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1019
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1020
lemma zmod_zero [simp]: "#0 zmod b = #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1021
  by (simp add: zmod_def divAlg_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1022
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1023
lemma zdiv_minus1: "#0 $< b ==> #-1 zdiv b = #-1"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1024
  by (simp add: zdiv_def divAlg_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1025
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1026
lemma zmod_minus1: "#0 $< b ==> #-1 zmod b = b $- #1"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1027
  by (simp add: zmod_def divAlg_def)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1028
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1029
(** a positive, b positive **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1030
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1031
lemma zdiv_pos_pos: "[| #0 $< a;  #0 $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1032
      ==> a zdiv b = fst (posDivAlg(<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1033
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1034
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
  1035
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1036
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1037
lemma zmod_pos_pos:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1038
     "[| #0 $< a;  #0 $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1039
      ==> a zmod b = snd (posDivAlg(<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1040
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1041
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
  1042
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1043
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1044
(** a negative, b positive **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1045
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1046
lemma zdiv_neg_pos:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1047
     "[| a $< #0;  #0 $< b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1048
      ==> a zdiv b = fst (negDivAlg(<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1049
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1050
apply (blast dest: zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1051
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1052
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1053
lemma zmod_neg_pos:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1054
     "[| a $< #0;  #0 $< b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1055
      ==> a zmod b = snd (negDivAlg(<intify(a), intify(b)>))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1056
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1057
apply (blast dest: zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1058
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1059
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1060
(** a positive, b negative **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1061
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1062
lemma zdiv_pos_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1063
     "[| #0 $< a;  b $< #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1064
      ==> a zdiv b = fst (negateSnd(negDivAlg (<$-a, $-b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1065
apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1066
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1067
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1068
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
  1069
apply (blast intro: zless_imp_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1070
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1071
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1072
lemma zmod_pos_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1073
     "[| #0 $< a;  b $< #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1074
      ==> a zmod b = snd (negateSnd(negDivAlg (<$-a, $-b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1075
apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1076
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1077
apply (blast dest: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1078
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
  1079
apply (blast intro: zless_imp_zle)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1080
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1081
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1082
(** a negative, b negative **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1083
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1084
lemma zdiv_neg_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1085
     "[| a $< #0;  b $<= #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1086
      ==> a zdiv b = fst (negateSnd(posDivAlg(<$-a, $-b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1087
apply (simp (no_asm_simp) add: zdiv_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1088
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1089
apply (blast dest!: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1090
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1091
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1092
lemma zmod_neg_neg:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1093
     "[| a $< #0;  b $<= #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1094
      ==> a zmod b = snd (negateSnd(posDivAlg(<$-a, $-b>)))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1095
apply (simp (no_asm_simp) add: zmod_def divAlg_def)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1096
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1097
apply (blast dest!: zle_zless_trans)+
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1098
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1099
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1100
declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1101
declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1102
declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1103
declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1104
declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1105
declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1106
declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1107
declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1108
declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
  1109
declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1110
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1111
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1112
(** Special-case simplification **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1113
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1114
lemma zmod_1 [simp]: "a zmod #1 = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1115
apply (cut_tac a = "a" and b = "#1" in pos_mod_sign)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1116
apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1117
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1118
(*arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1119
apply (drule add1_zle_iff [THEN iffD2])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1120
apply (rule zle_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1121
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1122
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1123
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1124
lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1125
apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1126
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1127
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1128
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1129
lemma zmod_minus1_right [simp]: "a zmod #-1 = #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1130
apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1131
apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1132
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1133
(*arithmetic*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1134
apply (drule add1_zle_iff [THEN iffD2])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1135
apply (rule zle_anti_sym)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1136
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1137
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1138
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1139
lemma zdiv_minus1_right_raw: "a \<in> int ==> a zdiv #-1 = $-a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1140
apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1141
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1142
apply (rule equation_zminus [THEN iffD2])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1143
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1144
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1145
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1146
lemma zdiv_minus1_right: "a zdiv #-1 = $-a"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1147
apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1148
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1149
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1150
declare zdiv_minus1_right [simp]
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1151
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1152
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1153
subsection{* Monotonicity in the first argument (divisor) *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1154
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1155
lemma zdiv_mono1: "[| a $<= a';  #0 $< b |] ==> a zdiv b $<= a' zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1156
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1157
apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1158
apply (rule unique_quotient_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1159
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1160
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1161
apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1162
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1163
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1164
lemma zdiv_mono1_neg: "[| a $<= a';  b $< #0 |] ==> a' zdiv b $<= a zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1165
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1166
apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1167
apply (rule unique_quotient_lemma_neg)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1168
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1169
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1170
apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1171
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1172
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1173
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1174
subsection{* Monotonicity in the second argument (dividend) *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1175
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1176
lemma q_pos_lemma:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1177
     "[| #0 $<= b'$*q' $+ r'; r' $< b';  #0 $< b' |] ==> #0 $<= q'"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1178
apply (subgoal_tac "#0 $< b'$* (q' $+ #1)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1179
 apply (simp add: int_0_less_mult_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1180
 apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1181
apply (simp add: zadd_zmult_distrib2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1182
apply (erule zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1183
apply (erule zadd_zless_mono2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1184
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1185
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1186
lemma zdiv_mono2_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1187
     "[| b$*q $+ r = b'$*q' $+ r';  #0 $<= b'$*q' $+ r';
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1188
         r' $< b';  #0 $<= r;  #0 $< b';  b' $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1189
      ==> q $<= q'"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1190
apply (frule q_pos_lemma, assumption+)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1191
apply (subgoal_tac "b$*q $< b$* (q' $+ #1)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1192
 apply (simp add: zmult_zless_cancel1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1193
 apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1194
apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1195
 prefer 2 apply (simp add: zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1196
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1197
apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1198
 prefer 2 apply (blast intro: zmult_zle_mono1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1199
apply (subgoal_tac "r' $+ #0 $< b $+ r")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1200
 apply (simp add: zcompare_rls)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1201
apply (rule zadd_zless_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1202
 apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1203
apply (blast dest: zless_zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1204
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1205
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1206
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1207
lemma zdiv_mono2_raw:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1208
     "[| #0 $<= a;  #0 $< b';  b' $<= b;  a \<in> int |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1209
      ==> a zdiv b $<= a zdiv b'"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1210
apply (subgoal_tac "#0 $< b")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1211
 prefer 2 apply (blast dest: zless_zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1212
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1213
apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1214
apply (rule zdiv_mono2_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1215
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1216
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1217
apply (simp_all add: pos_mod_sign pos_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1218
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1219
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1220
lemma zdiv_mono2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1221
     "[| #0 $<= a;  #0 $< b';  b' $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1222
      ==> a zdiv b $<= a zdiv b'"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1223
apply (cut_tac a = "intify (a)" in zdiv_mono2_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1224
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1225
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1226
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1227
lemma q_neg_lemma:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1228
     "[| b'$*q' $+ r' $< #0;  #0 $<= r';  #0 $< b' |] ==> q' $< #0"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1229
apply (subgoal_tac "b'$*q' $< #0")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1230
 prefer 2 apply (force intro: zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1231
apply (simp add: zmult_less_0_iff)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1232
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
  1233
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1234
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1235
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1236
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1237
lemma zdiv_mono2_neg_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1238
     "[| b$*q $+ r = b'$*q' $+ r';  b'$*q' $+ r' $< #0;
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1239
         r $< b;  #0 $<= r';  #0 $< b';  b' $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1240
      ==> q' $<= q"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1241
apply (subgoal_tac "#0 $< b")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1242
 prefer 2 apply (blast dest: zless_zle_trans)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1243
apply (frule q_neg_lemma, assumption+)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1244
apply (subgoal_tac "b$*q' $< b$* (q $+ #1)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1245
 apply (simp add: zmult_zless_cancel1)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1246
 apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1247
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1248
apply (subgoal_tac "b$*q' $<= b'$*q'")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1249
 prefer 2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1250
 apply (simp add: zmult_zle_cancel2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1251
 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
  1252
apply (subgoal_tac "b'$*q' $+ r $< b $+ (b$*q $+ r)")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1253
 prefer 2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1254
 apply (erule ssubst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1255
 apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1256
 apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1257
  apply (assumption)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1258
 apply simp
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1259
apply (simp (no_asm_use) add: zadd_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1260
apply (rule zle_zless_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1261
 prefer 2 apply (assumption)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1262
apply (simp (no_asm_simp) add: zmult_zle_cancel2)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1263
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
  1264
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1265
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1266
lemma zdiv_mono2_neg_raw:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1267
     "[| a $< #0;  #0 $< b';  b' $<= b;  a \<in> int |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1268
      ==> a zdiv b' $<= a zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1269
apply (subgoal_tac "#0 $< b")
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1270
 prefer 2 apply (blast dest: zless_zle_trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1271
apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1272
apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1273
apply (rule zdiv_mono2_neg_lemma)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1274
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1275
apply (erule subst)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1276
apply (simp_all add: pos_mod_sign pos_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1277
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1278
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1279
lemma zdiv_mono2_neg: "[| a $< #0;  #0 $< b';  b' $<= b |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1280
      ==> a zdiv b' $<= a zdiv b"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1281
apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1282
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1283
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1284
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1285
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1286
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1287
subsection{* More algebraic laws for zdiv and zmod *}
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1288
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1289
(** proving (a*b) zdiv c = a $* (b zdiv c) $+ a * (b zmod c) **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1290
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1291
lemma zmult1_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1292
     "[| quorem(<b,c>, <q,r>);  c \<in> int;  c \<noteq> #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1293
      ==> quorem (<a$*b, c>, <a$*q $+ (a$*r) zdiv c, (a$*r) zmod c>)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1294
apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1295
                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1296
apply (auto intro: raw_zmod_zdiv_equality)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1297
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1298
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1299
lemma zdiv_zmult1_eq_raw:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1300
     "[|b \<in> int;  c \<in> int|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1301
      ==> (a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1302
apply (case_tac "c = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1303
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1304
apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1305
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1306
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1307
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1308
lemma zdiv_zmult1_eq: "(a$*b) zdiv c = a$*(b zdiv c) $+ a$*(b zmod c) zdiv c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1309
apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1310
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1311
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1312
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1313
lemma zmod_zmult1_eq_raw:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1314
     "[|b \<in> int;  c \<in> int|] ==> (a$*b) zmod c = a$*(b zmod c) zmod c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1315
apply (case_tac "c = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1316
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1317
apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1318
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1319
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1320
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1321
lemma zmod_zmult1_eq: "(a$*b) zmod c = a$*(b zmod c) zmod c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1322
apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1323
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1324
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1325
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1326
lemma zmod_zmult1_eq': "(a$*b) zmod c = ((a zmod c) $* b) zmod c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1327
apply (rule trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1328
apply (rule_tac b = " (b $* a) zmod c" in trans)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1329
apply (rule_tac [2] zmod_zmult1_eq)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1330
apply (simp_all (no_asm) add: zmult_commute)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1331
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1332
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1333
lemma zmod_zmult_distrib: "(a$*b) zmod c = ((a zmod c) $* (b zmod c)) zmod c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1334
apply (rule zmod_zmult1_eq' [THEN trans])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1335
apply (rule zmod_zmult1_eq)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1336
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1337
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1338
lemma zdiv_zmult_self1 [simp]: "intify(b) \<noteq> #0 ==> (a$*b) zdiv b = intify(a)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1339
  by (simp add: zdiv_zmult1_eq)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1340
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1341
lemma zdiv_zmult_self2 [simp]: "intify(b) \<noteq> #0 ==> (b$*a) zdiv b = intify(a)"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1342
  by (simp add: zmult_commute) 
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1343
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1344
lemma zmod_zmult_self1 [simp]: "(a$*b) zmod b = #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1345
  by (simp add: zmod_zmult1_eq)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1346
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1347
lemma zmod_zmult_self2 [simp]: "(b$*a) zmod b = #0"
46993
7371429c527d tidying and structured proofs
paulson
parents: 46821
diff changeset
  1348
  by (simp add: zmult_commute zmod_zmult1_eq)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1349
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1350
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1351
(** proving (a$+b) zdiv c =
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1352
            a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c) **)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1353
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1354
lemma zadd1_lemma:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1355
     "[| quorem(<a,c>, <aq,ar>);  quorem(<b,c>, <bq,br>);
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1356
         c \<in> int;  c \<noteq> #0 |]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1357
      ==> quorem (<a$+b, c>, <aq $+ bq $+ (ar$+br) zdiv c, (ar$+br) zmod c>)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1358
apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1359
                      pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1360
apply (auto intro: raw_zmod_zdiv_equality)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1361
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1362
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1363
(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1364
lemma zdiv_zadd1_eq_raw:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1365
     "[|a \<in> int; b \<in> int; c \<in> int|] ==>
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1366
      (a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1367
apply (case_tac "c = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1368
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1369
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1370
                                 THEN quorem_div])
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1371
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1372
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1373
lemma zdiv_zadd1_eq:
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1374
     "(a$+b) zdiv c = a zdiv c $+ b zdiv c $+ ((a zmod c $+ b zmod c) zdiv c)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1375
apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)"
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1376
       in zdiv_zadd1_eq_raw)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1377
apply auto
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1378
done
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1379
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1380
lemma zmod_zadd1_eq_raw:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1381
     "[|a \<in> int; b \<in> int; c \<in> int|]
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1382
      ==> (a$+b) zmod c = (a zmod c $+ b zmod c) zmod c"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
diff changeset
  1383
apply (case_tac "c = #0")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1384
 apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
  1385
apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod,
26056