src/HOL/NatArith.thy
author wenzelm
Thu, 22 Dec 2005 00:28:36 +0100
changeset 18457 356a9f711899
parent 17688 91d3604ec4b5
child 21238 c46bc715bdfd
permissions -rw-r--r--
structure ProjectRule; updated auxiliary facts for induct method; tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatArith.thy
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
13297
wenzelm
parents: 11655
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm
parents: 11655
diff changeset
     4
*)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     5
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
     6
header {*Further Arithmetic Facts Concerning the Natural Numbers*}
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15048
diff changeset
     8
theory NatArith
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports Nat
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15861
diff changeset
    10
uses "arith_data.ML"
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15048
diff changeset
    11
begin
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    12
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    13
setup arith_setup
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    14
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    15
text{*The following proofs may rely on the arithmetic proof procedures.*}
13297
wenzelm
parents: 11655
diff changeset
    16
17688
91d3604ec4b5 new lemma
paulson
parents: 17085
diff changeset
    17
lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
91d3604ec4b5 new lemma
paulson
parents: 17085
diff changeset
    18
  by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
91d3604ec4b5 new lemma
paulson
parents: 17085
diff changeset
    19
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    20
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
14208
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    21
by (simp add: less_eq reflcl_trancl [symmetric]
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    22
            del: reflcl_trancl, arith)
11454
7514e5e21cb8 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents: 11324
diff changeset
    23
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    24
lemma nat_diff_split:
10599
2df753cf86e9 miniscoping of nat_diff_split
paulson
parents: 10214
diff changeset
    25
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
13297
wenzelm
parents: 11655
diff changeset
    26
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm
parents: 11655
diff changeset
    27
  by (cases "a<b" rule: case_split)
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    28
     (auto simp add: diff_is_0_eq [THEN iffD2])
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    29
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    30
lemma nat_diff_split_asm:
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    31
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
13297
wenzelm
parents: 11655
diff changeset
    32
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    33
  by (simp split: nat_diff_split)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    34
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    35
lemmas [arith_split] = nat_diff_split split_min split_max
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    36
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    37
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    38
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    39
lemma le_square: "m \<le> m*(m::nat)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    40
by (induct_tac "m", auto)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    41
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    42
lemma le_cube: "(m::nat) \<le> m*(m*m)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    43
by (induct_tac "m", auto)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    44
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    45
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    46
text{*Subtraction laws, mostly by Clemens Ballarin*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    47
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    48
lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    49
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    50
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    51
lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    52
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    53
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    54
lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    55
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    56
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    57
lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    58
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    59
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    60
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    61
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    62
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    63
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    64
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    65
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    66
(*Replaces the previous diff_less and le_diff_less, which had the stronger
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    67
  second premise n\<le>m*)
15439
71c0f98e31f1 made diff_less a simp rule
nipkow
parents: 15404
diff changeset
    68
lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    69
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    70
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    71
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    72
(** Simplification of relational expressions involving subtraction **)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    73
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    74
lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    75
by (simp split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    76
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    77
lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    78
by (auto split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    79
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    80
lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    81
by (auto split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    82
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    83
lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    84
by (auto split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    85
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    86
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    87
text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    88
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    89
(* Monotonicity of subtraction in first argument *)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    90
lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    91
by (simp split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    92
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    93
lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    94
by (simp split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    95
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    96
lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    97
by (simp split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    98
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
    99
lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   100
by (simp split add: nat_diff_split)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   101
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   102
text{*Lemmas for ex/Factorization*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   103
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   104
lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   105
by (case_tac "m", auto)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   106
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   107
lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   108
by (case_tac "m", auto)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   109
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   110
lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   111
by (case_tac "m", auto)
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   112
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   113
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   114
text{*Rewriting to pull differences out*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   115
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   116
lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   117
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   118
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   119
lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   120
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   121
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   122
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   123
by arith
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   124
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   125
(*The others are
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   126
      i - j - k = i - (j + k),
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   127
      k \<le> j ==> j - k + i = j + i - k,
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   128
      k \<le> j ==> i + (j - k) = i + j - k *)
17085
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   129
lemmas add_diff_assoc = diff_add_assoc [symmetric]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   130
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   131
declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   132
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   133
text{*At present we prove no analogue of @{text not_less_Least} or @{text
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   134
Least_Suc}, since there appears to be no need.*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   135
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   136
ML
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   137
{*
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   138
val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   139
val nat_diff_split = thm "nat_diff_split";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   140
val nat_diff_split_asm = thm "nat_diff_split_asm";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   141
val le_square = thm "le_square";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   142
val le_cube = thm "le_cube";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   143
val diff_less_mono = thm "diff_less_mono";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   144
val less_diff_conv = thm "less_diff_conv";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   145
val le_diff_conv = thm "le_diff_conv";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   146
val le_diff_conv2 = thm "le_diff_conv2";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   147
val diff_diff_cancel = thm "diff_diff_cancel";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   148
val le_add_diff = thm "le_add_diff";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   149
val diff_less = thm "diff_less";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   150
val diff_diff_eq = thm "diff_diff_eq";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   151
val eq_diff_iff = thm "eq_diff_iff";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   152
val less_diff_iff = thm "less_diff_iff";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   153
val le_diff_iff = thm "le_diff_iff";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   154
val diff_le_mono = thm "diff_le_mono";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   155
val diff_le_mono2 = thm "diff_le_mono2";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   156
val diff_less_mono2 = thm "diff_less_mono2";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   157
val diffs0_imp_equal = thm "diffs0_imp_equal";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   158
val one_less_mult = thm "one_less_mult";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   159
val n_less_m_mult_n = thm "n_less_m_mult_n";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   160
val n_less_n_mult_m = thm "n_less_n_mult_m";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   161
val diff_diff_right = thm "diff_diff_right";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   162
val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   163
val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   164
*}
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   165
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   166
subsection{*Embedding of the Naturals into any @{text
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   167
comm_semiring_1_cancel}: @{term of_nat}*}
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   168
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   169
consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   170
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   171
primrec
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   172
  of_nat_0:   "of_nat 0 = 0"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   173
  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   174
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   175
lemma of_nat_1 [simp]: "of_nat 1 = 1"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   176
by simp
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   177
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   178
lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   179
apply (induct m)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   180
apply (simp_all add: add_ac)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   181
done
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   182
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   183
lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   184
apply (induct m)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   185
apply (simp_all add: mult_ac add_ac right_distrib)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   186
done
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   187
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   188
lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   189
apply (induct m, simp_all)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   190
apply (erule order_trans)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   191
apply (rule less_add_one [THEN order_less_imp_le])
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   192
done
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   193
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   194
lemma less_imp_of_nat_less:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   195
     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   196
apply (induct m n rule: diff_induct, simp_all)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   197
apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   198
done
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   199
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   200
lemma of_nat_less_imp_less:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   201
     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   202
apply (induct m n rule: diff_induct, simp_all)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   203
apply (insert zero_le_imp_of_nat)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   204
apply (force simp add: linorder_not_less [symmetric])
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   205
done
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   206
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   207
lemma of_nat_less_iff [simp]:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   208
     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   209
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   210
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   211
text{*Special cases where either operand is zero*}
17085
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   212
lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   213
lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   214
declare of_nat_0_less_iff [simp]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   215
declare of_nat_less_0_iff [simp]
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   216
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   217
lemma of_nat_le_iff [simp]:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   218
     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   219
by (simp add: linorder_not_less [symmetric])
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   220
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   221
text{*Special cases where either operand is zero*}
17085
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   222
lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   223
lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   224
declare of_nat_0_le_iff [simp]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   225
declare of_nat_le_0_iff [simp]
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   226
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   227
text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   228
to exclude the possibility of a finite field, which indeed wraps back to
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   229
zero.*}
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   230
lemma of_nat_eq_iff [simp]:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   231
     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   232
by (simp add: order_eq_iff)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   233
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   234
text{*Special cases where either operand is zero*}
17085
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   235
lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   236
lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   237
declare of_nat_0_eq_iff [simp]
5b57f995a179 more simprules now have names
paulson
parents: 16417
diff changeset
   238
declare of_nat_eq_0_iff [simp]
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   239
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   240
lemma of_nat_diff [simp]:
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   241
     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   242
by (simp del: of_nat_add
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   243
	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15439
diff changeset
   244
15404
a9a762f586b5 removal of NatArith.ML and Product_Type.ML
paulson
parents: 15140
diff changeset
   245
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
   246
end