src/HOL/Integ/IntArith.thy
author paulson
Tue, 18 Nov 2003 11:01:52 +0100
changeset 14259 79f7d3451b1e
parent 13849 2584233cf3ef
child 14266 08b34c902618
permissions -rw-r--r--
conversion of ML to Isar scripts
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
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
     8
theory IntArith = Bin
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
     9
files ("int_arith1.ML"):
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents: 9214
diff changeset
    10
12023
wenzelm
parents: 11868
diff changeset
    11
use "int_arith1.ML"
wenzelm
parents: 11868
diff changeset
    12
setup int_arith_setup
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    13
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    14
lemma zle_diff1_eq [simp]: "(w <= z - (1::int)) = (w<(z::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    15
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    16
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    17
lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w<=(z::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    18
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    19
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    20
lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    21
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    22
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    23
subsection{*Results about @{term nat}*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    24
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    25
lemma nonneg_eq_int: "[| 0 <= z;  !!m. z = int m ==> P |] ==> P"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    26
by (blast dest: nat_0_le sym)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    27
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    28
lemma nat_eq_iff: "(nat w = m) = (if 0 <= w then w = int m else m=0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    29
by auto
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    30
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    31
lemma nat_eq_iff2: "(m = nat w) = (if 0 <= w then w = int m else m=0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    32
by auto
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    33
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    34
lemma nat_less_iff: "0 <= w ==> (nat w < m) = (w < int m)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    35
apply (rule iffI)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    36
apply (erule nat_0_le [THEN subst])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    37
apply (simp_all del: zless_int add: zless_int [symmetric]) 
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    38
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    39
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    40
lemma int_eq_iff: "(int m = z) = (m = nat z & 0 <= z)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    41
by (auto simp add: nat_eq_iff2)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    42
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    43
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    44
(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    45
declare Zero_int_def [symmetric, simp]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    46
declare One_int_def [symmetric, simp]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    47
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    48
text{*cooper.ML refers to this theorem*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    49
lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    50
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    51
lemma nat_0: "nat 0 = 0"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    52
by (simp add: nat_eq_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    53
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    54
lemma nat_1: "nat 1 = Suc 0"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    55
by (subst nat_eq_iff, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    56
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    57
lemma nat_2: "nat 2 = Suc (Suc 0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    58
by (subst nat_eq_iff, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    59
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    60
lemma nat_less_eq_zless: "0 <= w ==> (nat w < nat z) = (w<z)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    61
apply (case_tac "neg z")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    62
apply (auto simp add: nat_less_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    63
apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    64
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    65
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    66
lemma nat_le_eq_zle: "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    67
by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    68
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    69
subsection{*@{term abs}: Absolute Value, as an Integer*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    70
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    71
(* Simpler: use zabs_def as rewrite rule
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    72
   but arith_tac is not parameterized by such simp rules
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    73
*)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    74
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    75
lemma zabs_split: "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    76
by (simp add: zabs_def)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    77
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    78
lemma zero_le_zabs [iff]: "0 <= abs (z::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    79
by (simp add: zabs_def)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    80
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    81
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    82
text{*This simplifies expressions of the form @{term "int n = z"} where
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    83
      z is an integer literal.*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    84
declare int_eq_iff [of _ "number_of v", standard, simp]
13837
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
    85
12023
wenzelm
parents: 11868
diff changeset
    86
declare zabs_split [arith_split]
wenzelm
parents: 11868
diff changeset
    87
13837
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
    88
lemma zabs_eq_iff:
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
    89
    "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
    90
  by (auto simp add: zabs_def)
8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes
paulson
parents: 13685
diff changeset
    91
13849
2584233cf3ef new simprule for int (nat n)
paulson
parents: 13837
diff changeset
    92
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
2584233cf3ef new simprule for int (nat n)
paulson
parents: 13837
diff changeset
    93
  by simp
2584233cf3ef new simprule for int (nat n)
paulson
parents: 13837
diff changeset
    94
13575
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
    95
lemma split_nat[arith_split]:
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
    96
  "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
    97
  (is "?P = (?L & ?R)")
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
    98
proof (cases "i < 0")
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
    99
  case True thus ?thesis by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   100
next
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   101
  case False
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   102
  have "?P = ?L"
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   103
  proof
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   104
    assume ?P thus ?L using False by clarsimp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   105
  next
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   106
    assume ?L thus ?P using False by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   107
  qed
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   108
  with False show ?thesis by simp
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   109
qed
ecb6ecd9af13 added nat_split
nipkow
parents: 12023
diff changeset
   110
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   111
subsubsection "Induction principles for int"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   112
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   113
                     (* `set:int': dummy construction *)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   114
theorem int_ge_induct[case_names base step,induct set:int]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   115
  assumes ge: "k \<le> (i::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   116
        base: "P(k)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   117
        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   118
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   119
proof -
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   120
  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   121
    proof (induct n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   122
      case 0
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   123
      hence "i = k" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   124
      thus "P i" using base by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   125
    next
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   126
      case (Suc n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   127
      hence "n = nat((i - 1) - k)" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   128
      moreover
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   129
      have ki1: "k \<le> i - 1" using Suc.prems by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   130
      ultimately
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   131
      have "P(i - 1)" by(rule Suc.hyps)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   132
      from step[OF ki1 this] show ?case by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   133
    qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   134
  }
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   135
  from this ge show ?thesis by fast
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   136
qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   137
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   138
                     (* `set:int': dummy construction *)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   139
theorem int_gr_induct[case_names base step,induct set:int]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   140
  assumes gr: "k < (i::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   141
        base: "P(k+1)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   142
        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   143
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   144
apply(rule int_ge_induct[of "k + 1"])
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   145
  using gr apply arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   146
 apply(rule base)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   147
apply (rule step, simp+)
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   148
done
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   149
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   150
theorem int_le_induct[consumes 1,case_names base step]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   151
  assumes le: "i \<le> (k::int)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   152
        base: "P(k)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   153
        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   154
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   155
proof -
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   156
  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i <= k \<Longrightarrow> P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   157
    proof (induct n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   158
      case 0
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   159
      hence "i = k" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   160
      thus "P i" using base by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   161
    next
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   162
      case (Suc n)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   163
      hence "n = nat(k - (i+1))" by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   164
      moreover
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   165
      have ki1: "i + 1 \<le> k" using Suc.prems by arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   166
      ultimately
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   167
      have "P(i+1)" by(rule Suc.hyps)
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   168
      from step[OF ki1 this] show ?case by simp
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   169
    qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   170
  }
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   171
  from this le show ?thesis by fast
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   172
qed
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   173
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   174
theorem int_less_induct[consumes 1,case_names base step]:
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   175
  assumes less: "(i::int) < k" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   176
        base: "P(k - 1)" and
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   177
        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   178
  shows "P i"
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   179
apply(rule int_le_induct[of _ "k - 1"])
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   180
  using less apply arith
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   181
 apply(rule base)
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   182
apply (rule step, simp+)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   183
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   184
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   185
subsection{*Simple Equations*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   186
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   187
lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   188
by simp
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   189
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   190
lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   191
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   192
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   193
lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   194
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   195
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   196
lemma triangle_ineq: "abs(x+y) <= abs(x) + abs(y::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   197
by arith
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   198
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   199
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   200
subsection{*Intermediate value theorems*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   201
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   202
lemma int_val_lemma:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   203
     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   204
      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   205
apply (induct_tac "n")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   206
 apply (simp (no_asm_simp))
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   207
apply (intro strip)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   208
apply (erule impE, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   209
apply (erule_tac x = n in allE, simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   210
apply (case_tac "k = f (n+1) ")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   211
 apply force
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   212
apply (erule impE)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   213
 apply (simp add: zabs_def split add: split_if_asm)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   214
apply (blast intro: le_SucI)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   215
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   216
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   217
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   218
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   219
lemma nat_intermed_int_val:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   220
     "[| \<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
   221
         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
   222
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
   223
       in int_val_lemma)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   224
apply simp
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   225
apply (erule impE)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   226
 apply (intro strip)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   227
 apply (erule_tac x = "i+m" in allE, arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   228
apply (erule exE)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   229
apply (rule_tac x = "i+m" in exI, arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   230
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   231
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   232
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   233
subsection{*Some convenient biconditionals for products of signs*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   234
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   235
lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   236
by (drule zmult_zless_mono1, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   237
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   238
lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   239
by (drule zmult_zless_mono1_neg, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   240
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   241
lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   242
by (drule zmult_zless_mono1_neg, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   243
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   244
lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   245
apply (auto simp add: order_le_less linorder_not_less zmult_pos zmult_neg)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   246
apply (rule_tac [!] ccontr)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   247
apply (auto simp add: order_le_less linorder_not_less)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   248
apply (erule_tac [!] rev_mp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   249
apply (drule_tac [!] zmult_pos_neg)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   250
apply (auto dest: order_less_not_sym simp add: zmult_commute)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   251
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   252
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   253
lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   254
by (auto simp add: order_le_less linorder_not_less int_0_less_mult_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   255
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   256
lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   257
by (auto simp add: int_0_le_mult_iff linorder_not_le [symmetric])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   258
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   259
lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   260
by (auto dest: order_less_not_sym simp add: int_0_less_mult_iff linorder_not_less [symmetric])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   261
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   262
lemma abs_mult: "abs (x * y) = abs x * abs (y::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   263
by (simp del: number_of_reorient split
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   264
          add: zabs_split split add: zabs_split add: zmult_less_0_iff zle_def)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   265
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   266
lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   267
by (simp split add: zabs_split)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   268
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   269
lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   270
by (simp split add: zabs_split, arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   271
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   272
(* THIS LOOKS WRONG: [intro]*)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   273
lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   274
apply (subgoal_tac " (- x) * x \<le> 0")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   275
 apply simp
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   276
apply (simp only: zmult_le_0_iff, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   277
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   278
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   279
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   280
subsection{*Products and 1, by T. M. Rasmussen*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   281
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   282
lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   283
apply auto
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   284
apply (subgoal_tac "m*1 = m*n")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   285
apply (drule zmult_cancel1 [THEN iffD1], auto)
13685
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   286
done
0b8fbcf65d73 added induction thms
nipkow
parents: 13575
diff changeset
   287
14259
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   288
lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   289
apply (rule_tac y = "1*n" in order_less_trans)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   290
apply (rule_tac [2] zmult_zless_mono1)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   291
apply (simp_all (no_asm_simp))
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   292
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   293
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   294
lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   295
apply auto
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   296
apply (case_tac "m=1")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   297
apply (case_tac [2] "n=1")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   298
apply (case_tac [4] "m=1")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   299
apply (case_tac [5] "n=1", auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   300
apply (tactic"distinct_subgoals_tac")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   301
apply (subgoal_tac "1<m*n", simp)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   302
apply (rule zless_1_zmult, arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   303
apply (subgoal_tac "0<n", arith)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   304
apply (subgoal_tac "0<m*n")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   305
apply (drule int_0_less_mult_iff [THEN iffD1], auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   306
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   307
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   308
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   309
apply (case_tac "0<m")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   310
apply (simp (no_asm_simp) add: pos_zmult_eq_1_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   311
apply (case_tac "m=0")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   312
apply (simp (no_asm_simp) del: number_of_reorient)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   313
apply (subgoal_tac "0 < -m")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   314
apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   315
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   316
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   317
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   318
subsection{*More about nat*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   319
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   320
lemma nat_add_distrib:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   321
     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   322
apply (rule inj_int [THEN injD])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   323
apply (simp (no_asm_simp) add: zadd_int [symmetric])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   324
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   325
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   326
lemma nat_diff_distrib:
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   327
     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   328
apply (rule inj_int [THEN injD])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   329
apply (simp (no_asm_simp) add: zdiff_int [symmetric] nat_le_eq_zle)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   330
done
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
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   333
apply (case_tac "0 \<le> z'")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   334
apply (rule inj_int [THEN injD])
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   335
apply (simp (no_asm_simp) add: zmult_int [symmetric] int_0_le_mult_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   336
apply (simp add: zmult_le_0_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   337
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   338
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   339
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   340
apply (rule trans)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   341
apply (rule_tac [2] nat_mult_distrib, auto)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   342
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   343
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   344
lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   345
apply (case_tac "z=0 | w=0")
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   346
apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   347
                      nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   348
done
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   349
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   350
ML
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   351
{*
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   352
val zle_diff1_eq = thm "zle_diff1_eq";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   353
val zle_add1_eq_le = thm "zle_add1_eq_le";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   354
val nonneg_eq_int = thm "nonneg_eq_int";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   355
val nat_eq_iff = thm "nat_eq_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   356
val nat_eq_iff2 = thm "nat_eq_iff2";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   357
val nat_less_iff = thm "nat_less_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   358
val int_eq_iff = thm "int_eq_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   359
val nat_0 = thm "nat_0";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   360
val nat_1 = thm "nat_1";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   361
val nat_2 = thm "nat_2";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   362
val nat_less_eq_zless = thm "nat_less_eq_zless";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   363
val nat_le_eq_zle = thm "nat_le_eq_zle";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   364
val zabs_split = thm "zabs_split";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   365
val zero_le_zabs = thm "zero_le_zabs";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   366
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   367
val int_diff_minus_eq = thm "int_diff_minus_eq";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   368
val abs_abs = thm "abs_abs";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   369
val abs_minus = thm "abs_minus";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   370
val triangle_ineq = thm "triangle_ineq";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   371
val nat_intermed_int_val = thm "nat_intermed_int_val";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   372
val zmult_pos = thm "zmult_pos";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   373
val zmult_neg = thm "zmult_neg";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   374
val zmult_pos_neg = thm "zmult_pos_neg";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   375
val int_0_less_mult_iff = thm "int_0_less_mult_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   376
val int_0_le_mult_iff = thm "int_0_le_mult_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   377
val zmult_less_0_iff = thm "zmult_less_0_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   378
val zmult_le_0_iff = thm "zmult_le_0_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   379
val abs_mult = thm "abs_mult";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   380
val abs_eq_0 = thm "abs_eq_0";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   381
val zero_less_abs_iff = thm "zero_less_abs_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   382
val square_nonzero = thm "square_nonzero";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   383
val zmult_eq_self_iff = thm "zmult_eq_self_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   384
val zless_1_zmult = thm "zless_1_zmult";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   385
val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   386
val zmult_eq_1_iff = thm "zmult_eq_1_iff";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   387
val nat_add_distrib = thm "nat_add_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   388
val nat_diff_distrib = thm "nat_diff_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   389
val nat_mult_distrib = thm "nat_mult_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   390
val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   391
val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   392
*}
79f7d3451b1e conversion of ML to Isar scripts
paulson
parents: 13849
diff changeset
   393
7707
1f4b67fdfdae simprocs now in IntArith;
wenzelm
parents:
diff changeset
   394
end