src/HOL/Integ/IntArith.thy
author haftmann
Wed, 06 Sep 2006 13:48:02 +0200
changeset 20485 3078fd2eec7b
parent 20402 e2c6d096af01
child 20523 36a59e5d0039
permissions -rw-r--r--
got rid of Numeral.bin type
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
     1
(*  Title:      HOL/Integ/IntArith.thy
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
     2
    ID:         $Id$
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
     3
    Authors:    Larry Paulson and Tobias Nipkow
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
     4
*)
12023
wenzelm
parents: 11868
diff changeset
     5
wenzelm
parents: 11868
diff changeset
     6
header {* Integer arithmetic *}
wenzelm
parents: 11868
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15013
diff changeset
     8
theory IntArith
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports Numeral
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 16413
diff changeset
    10
uses ("int_arith1.ML")
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15013
diff changeset
    11
begin
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
    12
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    13
text{*Duplicate: can't understand why it's necessary*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    14
declare numeral_0_eq_0 [simp]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    15
16413
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
    16
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    17
subsection{*Instantiating Binary Arithmetic for the Integers*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    18
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    19
instance
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    20
  int :: number ..
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    21
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 15003
diff changeset
    22
defs (overloaded)
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
    23
  int_number_of_def: "(number_of w :: int) == of_int w"
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 15003
diff changeset
    24
    --{*the type constraint is essential!*}
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    25
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    26
instance int :: number_ring
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 15003
diff changeset
    27
by (intro_classes, simp add: int_number_of_def) 
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    28
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
    29
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
    30
subsection{*Inequality Reasoning for the Arithmetic Simproc*}
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
    31
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    32
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    33
by simp 
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    34
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    35
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    36
by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    37
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    38
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    39
by simp 
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    40
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    41
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    42
by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    43
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    44
text{*Theorem lists for the cancellation simprocs. The use of binary numerals
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    45
for 0 and 1 reduces the number of special cases.*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    46
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    47
lemmas add_0s = add_numeral_0 add_numeral_0_right
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    48
lemmas mult_1s = mult_numeral_1 mult_numeral_1_right 
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    49
                 mult_minus1 mult_minus1_right
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    50
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    51
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    52
subsection{*Special Arithmetic Rules for Abstract 0 and 1*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    53
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    54
text{*Arithmetic computations are defined for binary literals, which leaves 0
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    55
and 1 as special cases. Addition already has rules for 0, but not 1.
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    56
Multiplication and unary minus already have rules for both 0 and 1.*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    57
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    58
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    59
lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    60
by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    61
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    62
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    63
lemmas add_number_of_eq = number_of_add [symmetric]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    64
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    65
text{*Allow 1 on either or both sides*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    66
lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    67
by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric] add_number_of_eq)
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    68
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    69
lemmas add_special =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    70
    one_add_one_is_two
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    71
    binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    72
    binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    73
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    74
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    75
lemmas diff_special =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    76
    binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    77
    binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    78
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    79
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    80
lemmas eq_special =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    81
    binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    82
    binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    83
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    84
    binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    85
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    86
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    87
lemmas less_special =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    88
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    89
  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    90
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    91
  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    92
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    93
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    94
lemmas le_special =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    95
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    96
    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    97
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    98
    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    99
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   100
lemmas arith_special = 
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   101
       add_special diff_special eq_special less_special le_special
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   102
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   103
12023
wenzelm
parents: 11868
diff changeset
   104
use "int_arith1.ML"
wenzelm
parents: 11868
diff changeset
   105
setup int_arith_setup
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   106
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
   107
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   108
subsection{*Lemmas About Small Numerals*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   109
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   110
lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   111
proof -
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   112
  have "(of_int -1 :: 'a) = of_int (- 1)" by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   113
  also have "... = - of_int 1" by (simp only: of_int_minus)
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   114
  also have "... = -1" by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   115
  finally show ?thesis .
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   116
qed
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   117
14738
83f1a514dcb4 changes made due to new Ring_and_Field theory
obua
parents: 14479
diff changeset
   118
lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})"
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   119
by (simp add: abs_if)
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   120
14436
77017c49c004 some new results
paulson
parents: 14390
diff changeset
   121
lemma abs_power_minus_one [simp]:
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14738
diff changeset
   122
     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
14436
77017c49c004 some new results
paulson
parents: 14390
diff changeset
   123
by (simp add: power_abs)
77017c49c004 some new results
paulson
parents: 14390
diff changeset
   124
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   125
lemma of_int_number_of_eq:
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   126
     "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 15003
diff changeset
   127
by (simp add: number_of_eq) 
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   128
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   129
text{*Lemmas for specialist use, NOT as default simprules*}
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   130
lemma mult_2: "2 * z = (z+z::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   131
proof -
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   132
  have "2*z = (1 + 1)*z" by simp
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   133
  also have "... = z+z" by (simp add: left_distrib)
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   134
  finally show ?thesis .
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   135
qed
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   136
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   137
lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)"
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   138
by (subst mult_commute, rule mult_2)
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   139
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   140
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   141
subsection{*More Inequality Reasoning*}
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   142
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   143
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   144
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   145
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   146
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   147
by arith
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   148
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   149
lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<z)"
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   150
by arith
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   151
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   152
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)"
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   153
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   154
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
   155
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
   156
by arith
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14353
diff changeset
   157
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
   158
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
   159
subsection{*The Functions @{term nat} and @{term int}*}
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   160
14353
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
   161
text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and
79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents: 14295
diff changeset
   162
  @{term "w + - z"}*}
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   163
declare Zero_int_def [symmetric, simp]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   164
declare One_int_def [symmetric, simp]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   165
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   166
text{*cooper.ML refers to this theorem*}
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   167
lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp]
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   168
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   169
lemma nat_0: "nat 0 = 0"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   170
by (simp add: nat_eq_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   171
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   172
lemma nat_1: "nat 1 = Suc 0"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   173
by (subst nat_eq_iff, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   174
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   175
lemma nat_2: "nat 2 = Suc (Suc 0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   176
by (subst nat_eq_iff, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   177
16413
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   178
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   179
apply (insert zless_nat_conj [of 1 z])
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   180
apply (auto simp add: nat_1)
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   181
done
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   182
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   183
text{*This simplifies expressions of the form @{term "int n = z"} where
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   184
      z is an integer literal.*}
17085
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   185
lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   186
declare int_eq_iff_number_of [simp]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   187
13837
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
   188
14295
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14272
diff changeset
   189
lemma split_nat [arith_split]:
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   190
  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
13575
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   191
  (is "?P = (?L & ?R)")
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   192
proof (cases "i < 0")
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   193
  case True thus ?thesis by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   194
next
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   195
  case False
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   196
  have "?P = ?L"
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   197
  proof
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   198
    assume ?P thus ?L using False by clarsimp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   199
  next
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   200
    assume ?L thus ?P using False by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   201
  qed
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   202
  with False show ?thesis by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   203
qed
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   204
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   205
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   206
(*Analogous to zadd_int*)
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 15003
diff changeset
   207
lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   208
by (induct m n rule: diff_induct, simp_all)
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   209
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   210
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   211
apply (case_tac "0 \<le> z'")
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   212
apply (rule inj_int [THEN injD])
16413
47ffc49c7d7b a few new integer lemmas
paulson
parents: 15234
diff changeset
   213
apply (simp add: int_mult zero_le_mult_iff)
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   214
apply (simp add: mult_le_0_iff)
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   215
done
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   216
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   217
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   218
apply (rule trans)
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   219
apply (rule_tac [2] nat_mult_distrib, auto)
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   220
done
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   221
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   222
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   223
apply (case_tac "z=0 | w=0")
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14738
diff changeset
   224
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
14479
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   225
                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   226
done
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   227
0eca4aabf371 streamlined treatment of quotients for the integers
paulson
parents: 14473
diff changeset
   228
17472
bcbf48d59059 tuned document;
wenzelm
parents: 17085
diff changeset
   229
subsection "Induction principles for int"
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   230
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   231
                     (* `set:int': dummy construction *)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   232
theorem int_ge_induct[case_names base step,induct set:int]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   233
  assumes ge: "k \<le> (i::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   234
        base: "P(k)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   235
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   236
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   237
proof -
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   238
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   239
    proof (induct n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   240
      case 0
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   241
      hence "i = k" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   242
      thus "P i" using base by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   243
    next
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   244
      case (Suc n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   245
      hence "n = nat((i - 1) - k)" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   246
      moreover
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   247
      have ki1: "k \<le> i - 1" using Suc.prems by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   248
      ultimately
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   249
      have "P(i - 1)" by(rule Suc.hyps)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   250
      from step[OF ki1 this] show ?case by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   251
    qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   252
  }
14473
846c237bd9b3 stylistic tweaks
paulson
parents: 14436
diff changeset
   253
  with ge show ?thesis by fast
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   254
qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   255
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   256
                     (* `set:int': dummy construction *)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   257
theorem int_gr_induct[case_names base step,induct set:int]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   258
  assumes gr: "k < (i::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   259
        base: "P(k+1)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   260
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   261
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   262
apply(rule int_ge_induct[of "k + 1"])
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   263
  using gr apply arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   264
 apply(rule base)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   265
apply (rule step, simp+)
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   266
done
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   267
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   268
theorem int_le_induct[consumes 1,case_names base step]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   269
  assumes le: "i \<le> (k::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   270
        base: "P(k)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   271
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   272
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   273
proof -
14272
5efbb548107d Tidying of the integer development; towards removing the
paulson
parents: 14271
diff changeset
   274
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   275
    proof (induct n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   276
      case 0
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   277
      hence "i = k" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   278
      thus "P i" using base by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   279
    next
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   280
      case (Suc n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   281
      hence "n = nat(k - (i+1))" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   282
      moreover
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   283
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   284
      ultimately
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   285
      have "P(i+1)" by(rule Suc.hyps)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   286
      from step[OF ki1 this] show ?case by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   287
    qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   288
  }
14473
846c237bd9b3 stylistic tweaks
paulson
parents: 14436
diff changeset
   289
  with le show ?thesis by fast
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   290
qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   291
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   292
theorem int_less_induct [consumes 1,case_names base step]:
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   293
  assumes less: "(i::int) < k" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   294
        base: "P(k - 1)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   295
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   296
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   297
apply(rule int_le_induct[of _ "k - 1"])
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   298
  using less apply arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   299
 apply(rule base)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   300
apply (rule step, simp+)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   301
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   302
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   303
subsection{*Intermediate value theorems*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   304
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   305
lemma int_val_lemma:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   306
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   307
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
14271
8ed6989228bb Simplification of the development of Integers
paulson
parents: 14266
diff changeset
   308
apply (induct_tac "n", simp)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   309
apply (intro strip)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   310
apply (erule impE, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   311
apply (erule_tac x = n in allE, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   312
apply (case_tac "k = f (n+1) ")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   313
 apply force
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   314
apply (erule impE)
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14738
diff changeset
   315
 apply (simp add: abs_if split add: split_if_asm)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   316
apply (blast intro: le_SucI)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   317
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   318
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   319
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   320
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   321
lemma nat_intermed_int_val:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   322
     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   323
         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   324
apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   325
       in int_val_lemma)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   326
apply simp
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   327
apply (erule exE)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   328
apply (rule_tac x = "i+m" in exI, arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   329
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   330
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   331
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   332
subsection{*Products and 1, by T. M. Rasmussen*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   333
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   334
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   335
by arith
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   336
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   337
lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   338
apply (case_tac "\<bar>n\<bar>=1") 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   339
apply (simp add: abs_mult) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   340
apply (rule ccontr) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   341
apply (auto simp add: linorder_neq_iff abs_mult) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   342
apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   343
 prefer 2 apply arith 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   344
apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   345
apply (rule mult_mono, auto) 
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   346
done
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   347
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   348
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   349
by (insert abs_zmult_eq_1 [of m n], arith)
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   350
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   351
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   352
apply (auto dest: pos_zmult_eq_1_iff_lemma) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   353
apply (simp add: mult_commute [of m]) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   354
apply (frule pos_zmult_eq_1_iff_lemma, auto) 
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   355
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   356
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   357
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
15234
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   358
apply (rule iffI) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   359
 apply (frule pos_zmult_eq_1_iff_lemma)
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   360
 apply (simp add: mult_commute [of m]) 
ec91a90c604e simplification tweaks for better arithmetic reasoning
paulson
parents: 15140
diff changeset
   361
 apply (frule pos_zmult_eq_1_iff_lemma, auto) 
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   362
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   363
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   364
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   365
subsection {* code generator setup *}
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   366
20380
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   367
code_typename
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   368
  "Numeral.bit" "IntDef.bit"
20380
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   369
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   370
code_constname
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   371
  "Numeral.Pls" "IntDef.pls"
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   372
  "Numeral.Min" "IntDef.min"
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   373
  "Numeral.Bit" "IntDef.bit"
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   374
  "Numeral.bit.bit_case" "IntDef.bit_case"
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   375
  "Numeral.B0" "IntDef.b0"
14f9f2a1caa6 simplified code generator setup
haftmann
parents: 20355
diff changeset
   376
  "Numeral.B1" "IntDef.b1"
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   377
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   378
lemma
20402
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   379
  Numeral_Pls_refl [code fun]: "Numeral.Pls = Numeral.Pls" ..
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   380
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   381
lemma
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   382
  Numeral_Min_refl [code fun]: "Numeral.Min = Numeral.Min" ..
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   383
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   384
lemma
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   385
  Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
e2c6d096af01 more concise preprocessing of numerals for code generation
haftmann
parents: 20380
diff changeset
   386
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   387
lemma zero_is_num_zero [code fun, code inline]:
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   388
  "(0::int) = Numeral.Pls" 
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   389
  unfolding Pls_def ..
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   390
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   391
lemma one_is_num_one [code fun, code inline]:
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   392
  "(1::int) = Numeral.Pls BIT bit.B1" 
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   393
  unfolding Pls_def Bit_def by simp 
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   394
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   395
lemma number_of_is_id [code fun, code inline]:
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   396
  "number_of (k::int) = k"
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   397
  unfolding int_number_of_def by simp
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   398
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   399
lemma number_of_minus:
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   400
  "number_of (b :: int) = (- number_of (- b) :: int)"
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   401
  unfolding int_number_of_def by simp
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   402
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   403
ML {*
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   404
structure Numeral =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   405
struct
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   406
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   407
val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   408
val minus_rewrites = map (fn thm => eq_reflection OF [thm])
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   409
  [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   410
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   411
fun int_of_numeral thy num = HOLogic.dest_binum num
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   412
  handle TERM _
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   413
    => error ("not a number: " ^ Sign.string_of_term thy num);
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   414
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   415
fun elim_negate thy thms =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   416
  let
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   417
    fun bins_of (Const _) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   418
          I
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   419
      | bins_of (Var _) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   420
          I
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   421
      | bins_of (Free _) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   422
          I
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   423
      | bins_of (Bound _) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   424
          I
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   425
      | bins_of (Abs (_, _, t)) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   426
          bins_of t
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   427
      | bins_of (t as _ $ _) =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   428
          case strip_comb t
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   429
           of (Const ("Numeral.Bit", _), _) => cons t
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   430
            | (t', ts) => bins_of t' #> fold bins_of ts;
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   431
    fun is_negative num = case try HOLogic.dest_binum num
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   432
     of SOME i => i < 0
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   433
      | _ => false;
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   434
    fun instantiate_with bin =
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   435
      Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   436
    val rewrites  =
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   437
      []
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   438
      |> fold (bins_of o prop_of) thms
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   439
      |> filter is_negative
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   440
      |> map instantiate_with
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   441
  in if null rewrites then thms else
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   442
    map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   443
  end;
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   444
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   445
end;
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   446
*}
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   447
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   448
code_const "Numeral.Pls" and "Numeral.Min"
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   449
  (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   450
  (Haskell target_atom "0" and target_atom "(negate ~1)")
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   451
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   452
setup {*
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   453
  CodegenTheorems.add_preproc Numeral.elim_negate
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20402
diff changeset
   454
  #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
20355
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   455
*}
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   456
50aaae6ae4db cleanup code generation for Numerals
haftmann
parents: 20217
diff changeset
   457
19601
299d4cd2ef51 added codegen preprocessors for numerals
haftmann
parents: 17472
diff changeset
   458
subsection {* legacy ML bindings *}
299d4cd2ef51 added codegen preprocessors for numerals
haftmann
parents: 17472
diff changeset
   459
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   460
ML
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   461
{*
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   462
val zle_diff1_eq = thm "zle_diff1_eq";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   463
val zle_add1_eq_le = thm "zle_add1_eq_le";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   464
val nonneg_eq_int = thm "nonneg_eq_int";
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   465
val abs_minus_one = thm "abs_minus_one";
14390
55fe71faadda further tweaks to the numeric theories
paulson
parents: 14387
diff changeset
   466
val of_int_number_of_eq = thm"of_int_number_of_eq";
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   467
val nat_eq_iff = thm "nat_eq_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   468
val nat_eq_iff2 = thm "nat_eq_iff2";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   469
val nat_less_iff = thm "nat_less_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   470
val int_eq_iff = thm "int_eq_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   471
val nat_0 = thm "nat_0";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   472
val nat_1 = thm "nat_1";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   473
val nat_2 = thm "nat_2";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   474
val nat_less_eq_zless = thm "nat_less_eq_zless";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   475
val nat_le_eq_zle = thm "nat_le_eq_zle";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   476
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   477
val nat_intermed_int_val = thm "nat_intermed_int_val";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   478
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   479
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   480
val nat_add_distrib = thm "nat_add_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   481
val nat_diff_distrib = thm "nat_diff_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   482
val nat_mult_distrib = thm "nat_mult_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   483
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   484
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   485
*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   486
7707
1f4b67fdfdae simprocs now in IntArith;
wenzelm
parents:
diff changeset
   487
end