src/HOL/Int.thy
author haftmann
Sun, 08 Oct 2017 22:28:22 +0200
changeset 66816 212a3334e7da
parent 66035 de6cd60b1226
child 66836 4eb431c3f974
permissions -rw-r--r--
more fundamental definition of div and mod on int
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 40819
diff changeset
     1
(*  Title:      HOL/Int.thy
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
41959
b460124855b8 tuned headers;
wenzelm
parents: 40819
diff changeset
     3
    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     4
*)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     5
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
     6
section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     7
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
     8
theory Int
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
     9
  imports Equiv_Relations Power Quotient Fun_Def
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    10
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    11
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
    12
subsection \<open>Definition of integers as a quotient type\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    13
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    14
definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    15
  where "intrel = (\<lambda>(x, y) (u, v). x + v = u + y)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    16
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    17
lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    18
  by (simp add: intrel_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    19
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    20
quotient_type int = "nat \<times> nat" / "intrel"
45694
4a8743618257 prefer typedef without extra definition and alternative name;
wenzelm
parents: 45607
diff changeset
    21
  morphisms Rep_Integ Abs_Integ
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    22
proof (rule equivpI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    23
  show "reflp intrel" by (auto simp: reflp_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    24
  show "symp intrel" by (auto simp: symp_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    25
  show "transp intrel" by (auto simp: transp_def)
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    26
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    27
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    28
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    29
  "(\<And>x y. z = Abs_Integ (x, y) \<Longrightarrow> P) \<Longrightarrow> P"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    30
  by (induct z) auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    31
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    32
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
    33
subsection \<open>Integers form a commutative ring\<close>
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    34
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    35
instantiation int :: comm_ring_1
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    36
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    37
51994
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51329
diff changeset
    38
lift_definition zero_int :: "int" is "(0, 0)" .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    39
51994
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51329
diff changeset
    40
lift_definition one_int :: "int" is "(1, 0)" .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    41
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    42
lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    43
  is "\<lambda>(x, y) (u, v). (x + u, y + v)"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    44
  by clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    45
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    46
lift_definition uminus_int :: "int \<Rightarrow> int"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    47
  is "\<lambda>(x, y). (y, x)"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    48
  by clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    49
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    50
lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    51
  is "\<lambda>(x, y) (u, v). (x + v, y + u)"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    52
  by clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    53
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    54
lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    55
  is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    56
proof (clarsimp)
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    57
  fix s t u v w x y z :: nat
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    58
  assume "s + v = u + t" and "w + z = y + x"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    59
  then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    60
    (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    61
    by simp
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    62
  then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    63
    by (simp add: algebra_simps)
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    64
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    65
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    66
instance
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    67
  by standard (transfer; clarsimp simp: algebra_simps)+
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    68
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    69
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    70
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    71
abbreviation int :: "nat \<Rightarrow> int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    72
  where "int \<equiv> of_nat"
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
    73
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    74
lemma int_def: "int n = Abs_Integ (n, 0)"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    75
  by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    76
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    77
lemma int_transfer [transfer_rule]: "(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    78
  by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    79
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    80
lemma int_diff_cases: obtains (diff) m n where "z = int m - int n"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    81
  by transfer clarsimp
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    82
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
    83
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
    84
subsection \<open>Integers are totally ordered\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
    85
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    86
instantiation int :: linorder
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    87
begin
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    88
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    89
lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    90
  is "\<lambda>(x, y) (u, v). x + v \<le> u + y"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    91
  by auto
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    92
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    93
lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    94
  is "\<lambda>(x, y) (u, v). x + v < u + y"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    95
  by auto
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    96
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    97
instance
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61144
diff changeset
    98
  by standard (transfer, force)+
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
    99
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   100
end
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   101
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   102
instantiation int :: distrib_lattice
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   103
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   104
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   105
definition "(inf :: int \<Rightarrow> int \<Rightarrow> int) = min"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   106
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   107
definition "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   108
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   109
instance
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   110
  by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   111
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   112
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   113
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   114
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   115
subsection \<open>Ordering properties of arithmetic operations\<close>
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   116
35028
108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents: 34055
diff changeset
   117
instance int :: ordered_cancel_ab_semigroup_add
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   118
proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   119
  fix i j k :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   120
  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   121
    by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   122
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   123
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   124
text \<open>Strict Monotonicity of Multiplication.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   125
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   126
text \<open>Strict, in 1st argument; proof is by induction on \<open>k > 0\<close>.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   127
lemma zmult_zless_mono2_lemma: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> int k * i < int k * j"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   128
  for i j :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   129
proof (induct k)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   130
  case 0
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   131
  then show ?case by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   132
next
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   133
  case (Suc k)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   134
  then show ?case
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   135
    by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   136
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   137
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   138
lemma zero_le_imp_eq_int: "0 \<le> k \<Longrightarrow> \<exists>n. k = int n"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   139
  for k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   140
  apply transfer
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   141
  apply clarsimp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   142
  apply (rule_tac x="a - b" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   143
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   144
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   145
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   146
lemma zero_less_imp_eq_int: "0 < k \<Longrightarrow> \<exists>n>0. k = int n"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   147
  for k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   148
  apply transfer
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   149
  apply clarsimp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   150
  apply (rule_tac x="a - b" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   151
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   152
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   153
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   154
lemma zmult_zless_mono2: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   155
  for i j k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   156
  by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   157
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   158
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   159
text \<open>The integers form an ordered integral domain.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   160
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   161
instantiation int :: linordered_idom
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   162
begin
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   163
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   164
definition zabs_def: "\<bar>i::int\<bar> = (if i < 0 then - i else i)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   165
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   166
definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   167
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   168
instance
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   169
proof
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   170
  fix i j k :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   171
  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   172
    by (rule zmult_zless_mono2)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   173
  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   174
    by (simp only: zabs_def)
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 61070
diff changeset
   175
  show "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   176
    by (simp only: zsgn_def)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   177
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   178
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   179
end
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   180
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   181
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + 1 \<le> z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   182
  for w z :: int
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   183
  by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   184
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   185
lemma zless_iff_Suc_zadd: "w < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   186
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   187
  apply transfer
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   188
  apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   189
  apply (rename_tac a b c d)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   190
  apply (rule_tac x="c+b - Suc(a+d)" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   191
  apply arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   192
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   193
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   194
lemma zabs_less_one_iff [simp]: "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?lhs \<longleftrightarrow> ?rhs")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   195
  for z :: int
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   196
proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   197
  assume ?rhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   198
  then show ?lhs by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   199
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   200
  assume ?lhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   201
  with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   202
  then have "\<bar>z\<bar> \<le> 0" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   203
  then show ?rhs by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   204
qed
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   205
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   206
lemmas int_distrib =
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 48891
diff changeset
   207
  distrib_right [of z1 z2 w]
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 48891
diff changeset
   208
  distrib_left [of w z1 z2]
45607
16b4f5774621 eliminated obsolete "standard";
wenzelm
parents: 45533
diff changeset
   209
  left_diff_distrib [of z1 z2 w]
16b4f5774621 eliminated obsolete "standard";
wenzelm
parents: 45533
diff changeset
   210
  right_diff_distrib [of w z1 z2]
16b4f5774621 eliminated obsolete "standard";
wenzelm
parents: 45533
diff changeset
   211
  for z1 z2 w :: int
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   212
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   213
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   214
subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   215
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   216
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   217
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   218
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   219
lift_definition of_int :: "int \<Rightarrow> 'a"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   220
  is "\<lambda>(i, j). of_nat i - of_nat j"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   221
  by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   222
      of_nat_add [symmetric] simp del: of_nat_add)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   223
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   224
lemma of_int_0 [simp]: "of_int 0 = 0"
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48045
diff changeset
   225
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   226
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   227
lemma of_int_1 [simp]: "of_int 1 = 1"
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48045
diff changeset
   228
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   229
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   230
lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z"
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48045
diff changeset
   231
  by transfer (clarsimp simp add: algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   232
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   233
lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)"
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48045
diff changeset
   234
  by (transfer fixing: uminus) clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   235
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   236
lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 54223
diff changeset
   237
  using of_int_add [of w "- z"] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   238
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   239
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   240
  by (transfer fixing: times) (clarsimp simp add: algebra_simps)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   241
61531
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61524
diff changeset
   242
lemma mult_of_int_commute: "of_int x * y = y * of_int x"
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61524
diff changeset
   243
  by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
ab2e862263e7 Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents: 61524
diff changeset
   244
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   245
text \<open>Collapse nested embeddings.\<close>
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   246
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   247
  by (induct n) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   248
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   249
lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   250
  by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   251
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   252
lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   253
  by simp
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   254
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   255
lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
31015
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   256
  by (induct n) simp_all
555f4033cd97 reorganization of power lemmas
haftmann
parents: 31010
diff changeset
   257
66816
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   258
lemma of_int_of_bool [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   259
  "of_int (of_bool P) = of_bool P"
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   260
  by auto
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   261
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   262
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   263
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   264
context ring_char_0
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   265
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   266
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   267
lemma of_int_eq_iff [simp]: "of_int w = of_int z \<longleftrightarrow> w = z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   268
  by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   269
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   270
text \<open>Special cases where either operand is zero.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   271
lemma of_int_eq_0_iff [simp]: "of_int z = 0 \<longleftrightarrow> z = 0"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   272
  using of_int_eq_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   273
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   274
lemma of_int_0_eq_iff [simp]: "0 = of_int z \<longleftrightarrow> z = 0"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   275
  using of_int_eq_iff [of 0 z] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   276
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   277
lemma of_int_eq_1_iff [iff]: "of_int z = 1 \<longleftrightarrow> z = 1"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   278
  using of_int_eq_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   279
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   280
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   281
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   282
context linordered_idom
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   283
begin
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   284
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   285
text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   286
subclass ring_char_0 ..
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   287
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   288
lemma of_int_le_iff [simp]: "of_int w \<le> of_int z \<longleftrightarrow> w \<le> z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   289
  by (transfer fixing: less_eq)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   290
    (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   291
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   292
lemma of_int_less_iff [simp]: "of_int w < of_int z \<longleftrightarrow> w < z"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   293
  by (simp add: less_le order_less_le)
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   294
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   295
lemma of_int_0_le_iff [simp]: "0 \<le> of_int z \<longleftrightarrow> 0 \<le> z"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   296
  using of_int_le_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   297
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   298
lemma of_int_le_0_iff [simp]: "of_int z \<le> 0 \<longleftrightarrow> z \<le> 0"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   299
  using of_int_le_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   300
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   301
lemma of_int_0_less_iff [simp]: "0 < of_int z \<longleftrightarrow> 0 < z"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   302
  using of_int_less_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   303
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   304
lemma of_int_less_0_iff [simp]: "of_int z < 0 \<longleftrightarrow> z < 0"
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   305
  using of_int_less_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   306
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   307
lemma of_int_1_le_iff [simp]: "1 \<le> of_int z \<longleftrightarrow> 1 \<le> z"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   308
  using of_int_le_iff [of 1 z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   309
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   310
lemma of_int_le_1_iff [simp]: "of_int z \<le> 1 \<longleftrightarrow> z \<le> 1"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   311
  using of_int_le_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   312
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   313
lemma of_int_1_less_iff [simp]: "1 < of_int z \<longleftrightarrow> 1 < z"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   314
  using of_int_less_iff [of 1 z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   315
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   316
lemma of_int_less_1_iff [simp]: "of_int z < 1 \<longleftrightarrow> z < 1"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   317
  using of_int_less_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   318
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   319
lemma of_int_pos: "z > 0 \<Longrightarrow> of_int z > 0"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   320
  by simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   321
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   322
lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   323
  by simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   324
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   325
lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   326
  by (auto simp add: abs_if)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   327
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   328
lemma of_int_lessD:
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   329
  assumes "\<bar>of_int n\<bar> < x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   330
  shows "n = 0 \<or> x > 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   331
proof (cases "n = 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   332
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   333
  then show ?thesis by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   334
next
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   335
  case False
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   336
  then have "\<bar>n\<bar> \<noteq> 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   337
  then have "\<bar>n\<bar> > 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   338
  then have "\<bar>n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   339
    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   340
  then have "\<bar>of_int n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   341
    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   342
  then have "1 < x" using assms by (rule le_less_trans)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   343
  then show ?thesis ..
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   344
qed
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   345
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   346
lemma of_int_leD:
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   347
  assumes "\<bar>of_int n\<bar> \<le> x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   348
  shows "n = 0 \<or> 1 \<le> x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   349
proof (cases "n = 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   350
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   351
  then show ?thesis by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   352
next
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   353
  case False
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   354
  then have "\<bar>n\<bar> \<noteq> 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   355
  then have "\<bar>n\<bar> > 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   356
  then have "\<bar>n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   357
    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   358
  then have "\<bar>of_int n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   359
    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   360
  then have "1 \<le> x" using assms by (rule order_trans)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   361
  then show ?thesis ..
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   362
qed
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   363
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   364
end
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   365
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   366
text \<open>Comparisons involving @{term of_int}.\<close>
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   367
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   368
lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \<longleftrightarrow> z = numeral n"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   369
  using of_int_eq_iff by fastforce
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   370
61649
268d88ec9087 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents: 61609
diff changeset
   371
lemma of_int_le_numeral_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   372
  "of_int z \<le> (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z \<le> numeral n"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   373
  using of_int_le_iff [of z "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   374
61649
268d88ec9087 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents: 61609
diff changeset
   375
lemma of_int_numeral_le_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   376
  "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   377
  using of_int_le_iff [of "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   378
61649
268d88ec9087 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents: 61609
diff changeset
   379
lemma of_int_less_numeral_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   380
  "of_int z < (numeral n :: 'a::linordered_idom) \<longleftrightarrow> z < numeral n"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   381
  using of_int_less_iff [of z "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   382
61649
268d88ec9087 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents: 61609
diff changeset
   383
lemma of_int_numeral_less_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   384
  "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   385
  using of_int_less_iff [of "numeral n" z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   386
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   387
lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
56889
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56525
diff changeset
   388
  by (metis of_int_of_nat_eq of_int_less_iff)
48a745e1bde7 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents: 56525
diff changeset
   389
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   390
lemma of_int_eq_id [simp]: "of_int = id"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   391
proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   392
  show "of_int z = id z" for z
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   393
    by (cases z rule: int_diff_cases) simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   394
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   395
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   396
instance int :: no_top
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61144
diff changeset
   397
  apply standard
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   398
  apply (rule_tac x="x + 1" in exI)
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   399
  apply simp
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   400
  done
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   401
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   402
instance int :: no_bot
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61144
diff changeset
   403
  apply standard
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   404
  apply (rule_tac x="x - 1" in exI)
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   405
  apply simp
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   406
  done
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   407
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   408
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   409
subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   410
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   411
lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x - y"
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   412
  by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   413
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   414
lemma nat_int [simp]: "nat (int n) = n"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   415
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   416
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   417
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   418
  by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   419
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   420
lemma nat_0_le: "0 \<le> z \<Longrightarrow> int (nat z) = z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   421
  by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   422
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   423
lemma nat_le_0 [simp]: "z \<le> 0 \<Longrightarrow> nat z = 0"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   424
  by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   425
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   426
lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> nat w \<le> nat z \<longleftrightarrow> w \<le> z"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   427
  by transfer (clarsimp, arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   428
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   429
text \<open>An alternative condition is @{term "0 \<le> w"}.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   430
lemma nat_mono_iff: "0 < z \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   431
  by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   432
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   433
lemma nat_less_eq_zless: "0 \<le> w \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   434
  by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   435
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   436
lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   437
  by transfer (clarsimp, arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   438
64714
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   439
lemma nonneg_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   440
  assumes "0 \<le> k"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   441
  obtains n where "k = int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   442
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   443
  from assms have "k = int (nat k)"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   444
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   445
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   446
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   447
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   448
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   449
lemma pos_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   450
  assumes "0 < k"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   451
  obtains n where "k = int n" and "n > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   452
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   453
  from assms have "0 \<le> k"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   454
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   455
  then obtain n where "k = int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   456
    by (rule nonneg_int_cases)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   457
  moreover have "n > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   458
    using \<open>k = int n\<close> assms by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   459
  ultimately show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   460
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   461
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   462
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   463
lemma nonpos_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   464
  assumes "k \<le> 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   465
  obtains n where "k = - int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   466
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   467
  from assms have "- k \<ge> 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   468
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   469
  then obtain n where "- k = int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   470
    by (rule nonneg_int_cases)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   471
  then have "k = - int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   472
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   473
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   474
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   475
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   476
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   477
lemma neg_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   478
  assumes "k < 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   479
  obtains n where "k = - int n" and "n > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   480
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   481
  from assms have "- k > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   482
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   483
  then obtain n where "- k = int n" and "- k > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   484
    by (blast elim: pos_int_cases)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   485
  then have "k = - int n" and "n > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   486
    by simp_all
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   487
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   488
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   489
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   490
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   491
lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   492
  by transfer (clarsimp simp add: le_imp_diff_is_add)
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   493
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   494
lemma nat_eq_iff2: "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   495
  using nat_eq_iff [of w m] by auto
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   496
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   497
lemma nat_0 [simp]: "nat 0 = 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   498
  by (simp add: nat_eq_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   499
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   500
lemma nat_1 [simp]: "nat 1 = Suc 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   501
  by (simp add: nat_eq_iff)
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   502
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   503
lemma nat_numeral [simp]: "nat (numeral k) = numeral k"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   504
  by (simp add: nat_eq_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   505
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   506
lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   507
  by simp
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   508
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   509
lemma nat_2: "nat 2 = Suc (Suc 0)"
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   510
  by simp
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   511
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   512
lemma nat_less_iff: "0 \<le> w \<Longrightarrow> nat w < m \<longleftrightarrow> w < of_nat m"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   513
  by transfer (clarsimp, arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   514
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   515
lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   516
  by transfer (clarsimp simp add: le_diff_conv)
44707
487ae6317f7b move lemmas nat_le_iff and nat_mono into Int.thy
huffman
parents: 44695
diff changeset
   517
487ae6317f7b move lemmas nat_le_iff and nat_mono into Int.thy
huffman
parents: 44695
diff changeset
   518
lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   519
  by transfer auto
44707
487ae6317f7b move lemmas nat_le_iff and nat_mono into Int.thy
huffman
parents: 44695
diff changeset
   520
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   521
lemma nat_0_iff[simp]: "nat i = 0 \<longleftrightarrow> i \<le> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   522
  for i :: int
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   523
  by transfer clarsimp
29700
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   524
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   525
lemma int_eq_iff: "of_nat m = z \<longleftrightarrow> m = nat z \<and> 0 \<le> z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   526
  by (auto simp add: nat_eq_iff2)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   527
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   528
lemma zero_less_nat_eq [simp]: "0 < nat z \<longleftrightarrow> 0 < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   529
  using zless_nat_conj [of 0] by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   530
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   531
lemma nat_add_distrib: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   532
  by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   533
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   534
lemma nat_diff_distrib': "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   535
  by transfer clarsimp
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   536
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   537
lemma nat_diff_distrib: "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   538
  by (rule nat_diff_distrib') auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   539
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   540
lemma nat_zminus_int [simp]: "nat (- int n) = 0"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   541
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   542
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   543
lemma le_nat_iff: "k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k"
53065
de1816a7293e added lemma
haftmann
parents: 52435
diff changeset
   544
  by transfer auto
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   545
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   546
lemma zless_nat_eq_int_zless: "m < nat z \<longleftrightarrow> int m < z"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   547
  by transfer (clarsimp simp add: less_diff_conv)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   548
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   549
lemma (in ring_1) of_nat_nat [simp]: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z"
48066
c6783c9b87bf transfer method now handles transfer rules for compound terms, e.g. locale-defined constants with hidden parameters
huffman
parents: 48045
diff changeset
   550
  by transfer (clarsimp simp add: of_nat_diff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   551
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   552
lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
54249
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   553
  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   554
66816
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   555
lemma nat_of_bool [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   556
  "nat (of_bool P) = of_bool P"
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   557
  by auto
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   558
54249
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   559
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   560
text \<open>For termination proofs:\<close>
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   561
lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
29779
2786b348c376 declare "nat o abs" as default measure for int
krauss
parents: 29700
diff changeset
   562
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   563
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   564
subsection \<open>Lemmas about the Function @{term of_nat} and Orderings\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   565
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 61070
diff changeset
   566
lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   567
  by (simp add: order_less_le del: of_nat_Suc)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   568
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   569
lemma negative_zless [iff]: "- (int (Suc n)) < int m"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   570
  by (rule negative_zless_0 [THEN order_less_le_trans], simp)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   571
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   572
lemma negative_zle_0: "- int n \<le> 0"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   573
  by (simp add: minus_le_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   574
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   575
lemma negative_zle [iff]: "- int n \<le> int m"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   576
  by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   577
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   578
lemma not_zle_0_negative [simp]: "\<not> 0 \<le> - int (Suc n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   579
  by (subst le_minus_iff) (simp del: of_nat_Suc)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   580
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   581
lemma int_zle_neg: "int n \<le> - int m \<longleftrightarrow> n = 0 \<and> m = 0"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   582
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   583
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   584
lemma not_int_zless_negative [simp]: "\<not> int n < - int m"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   585
  by (simp add: linorder_not_less)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   586
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   587
lemma negative_eq_positive [simp]: "- int n = of_nat m \<longleftrightarrow> n = 0 \<and> m = 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   588
  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   589
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   590
lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   591
  (is "?lhs \<longleftrightarrow> ?rhs")
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   592
proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   593
  assume ?rhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   594
  then show ?lhs by auto
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   595
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   596
  assume ?lhs
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   597
  then have "0 \<le> z - w" by simp
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   598
  then obtain n where "z - w = int n"
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   599
    using zero_le_imp_eq_int [of "z - w"] by blast
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   600
  then have "z = w + int n" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   601
  then show ?rhs ..
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   602
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   603
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   604
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   605
  by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   606
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   607
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   608
  This version is proved for all ordered rings, not just integers!
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   609
  It is proved here because attribute \<open>arith_split\<close> is not available
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   610
  in theory \<open>Rings\<close>.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   611
  But is it really better than just rewriting with \<open>abs_if\<close>?
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   612
\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   613
lemma abs_split [arith_split, no_atp]: "P \<bar>a\<bar> \<longleftrightarrow> (0 \<le> a \<longrightarrow> P a) \<and> (a < 0 \<longrightarrow> P (- a))"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   614
  for a :: "'a::linordered_idom"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   615
  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   616
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   617
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   618
  apply transfer
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   619
  apply clarsimp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   620
  apply (rule_tac x="b - Suc a" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   621
  apply arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   622
  done
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   623
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   624
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   625
subsection \<open>Cases and induction\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   626
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   627
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   628
  Now we replace the case analysis rule by a more conventional one:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   629
  whether an integer is negative or not.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   630
\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   631
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   632
text \<open>This version is symmetric in the two subgoals.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   633
lemma int_cases2 [case_names nonneg nonpos, cases type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   634
  "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int n) \<Longrightarrow> P) \<Longrightarrow> P"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   635
  by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
59613
7103019278f0 The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents: 59582
diff changeset
   636
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   637
text \<open>This is the default, with a negative case.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   638
lemma int_cases [case_names nonneg neg, cases type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   639
  "(\<And>n. z = int n \<Longrightarrow> P) \<Longrightarrow> (\<And>n. z = - (int (Suc n)) \<Longrightarrow> P) \<Longrightarrow> P"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   640
  apply (cases "z < 0")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   641
   apply (blast dest!: negD)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   642
  apply (simp add: linorder_not_less del: of_nat_Suc)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   643
  apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   644
  apply (blast dest: nat_0_le [THEN sym])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   645
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   646
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   647
lemma int_cases3 [case_names zero pos neg]:
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   648
  fixes k :: int
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   649
  assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61169
diff changeset
   650
    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   651
  shows "P"
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   652
proof (cases k "0::int" rule: linorder_cases)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   653
  case equal
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   654
  with assms(1) show P by simp
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   655
next
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   656
  case greater
63539
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   657
  then have *: "nat k > 0" by simp
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   658
  moreover from * have "k = int (nat k)" by auto
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   659
  ultimately show P using assms(2) by blast
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   660
next
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   661
  case less
63539
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   662
  then have *: "nat (- k) > 0" by simp
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   663
  moreover from * have "k = - int (nat (- k))" by auto
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   664
  ultimately show P using assms(3) by blast
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   665
qed
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   666
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   667
lemma int_of_nat_induct [case_names nonneg neg, induct type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   668
  "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z"
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
   669
  by (cases z) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   670
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   671
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   672
  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   673
  by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 36811
diff changeset
   674
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   675
lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   676
  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   677
  by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   678
66816
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   679
lemma sgn_mult_dvd_iff [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   680
  "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   681
  by (cases r rule: int_cases3) auto
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   682
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   683
lemma mult_sgn_dvd_iff [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   684
  "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   685
  using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   686
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   687
lemma dvd_sgn_mult_iff [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   688
  "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   689
  by (cases r rule: int_cases3) simp_all
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   690
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   691
lemma dvd_mult_sgn_iff [simp]:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   692
  "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   693
  using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   694
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   695
lemma int_sgnE:
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   696
  fixes k :: int
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   697
  obtains n and l where "k = sgn l * int n"
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   698
proof -
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   699
  have "k = sgn k * int (nat \<bar>k\<bar>)"
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   700
    by (simp add: sgn_mult_abs)
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   701
  then show ?thesis ..
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   702
qed
212a3334e7da more fundamental definition of div and mod on int
haftmann
parents: 66035
diff changeset
   703
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   704
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   705
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   706
lemmas max_number_of [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   707
  max_def [of "numeral u" "numeral v"]
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   708
  max_def [of "numeral u" "- numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   709
  max_def [of "- numeral u" "numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   710
  max_def [of "- numeral u" "- numeral v"] for u v
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   711
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   712
lemmas min_number_of [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   713
  min_def [of "numeral u" "numeral v"]
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   714
  min_def [of "numeral u" "- numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   715
  min_def [of "- numeral u" "numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   716
  min_def [of "- numeral u" "- numeral v"] for u v
26075
815f3ccc0b45 added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents: 26072
diff changeset
   717
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   718
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   719
subsubsection \<open>Binary comparisons\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   720
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   721
text \<open>Preliminaries\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   722
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   723
lemma le_imp_0_less:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   724
  fixes z :: int
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   725
  assumes le: "0 \<le> z"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   726
  shows "0 < 1 + z"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   727
proof -
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   728
  have "0 \<le> z" by fact
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   729
  also have "\<dots> < z + 1" by (rule less_add_one)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   730
  also have "\<dots> = 1 + z" by (simp add: ac_simps)
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   731
  finally show "0 < 1 + z" .
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   732
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   733
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   734
lemma odd_less_0_iff: "1 + z + z < 0 \<longleftrightarrow> z < 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   735
  for z :: int
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
   736
proof (cases z)
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   737
  case (nonneg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   738
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   739
    by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le])
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   740
next
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   741
  case (neg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   742
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   743
    by (simp del: of_nat_Suc of_nat_add of_nat_1
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   744
        add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   745
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   746
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   747
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   748
subsubsection \<open>Comparisons, for Ordered Rings\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   749
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   750
lemmas double_eq_0_iff = double_zero
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   751
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   752
lemma odd_nonzero: "1 + z + z \<noteq> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   753
  for z :: int
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
   754
proof (cases z)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   755
  case (nonneg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   756
  have le: "0 \<le> z + z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   757
    by (simp add: nonneg add_increasing)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   758
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   759
    using  le_imp_0_less [OF le] by (auto simp: add.assoc)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   760
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   761
  case (neg n)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   762
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   763
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   764
    assume eq: "1 + z + z = 0"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   765
    have "0 < 1 + (int n + int n)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   766
      by (simp add: le_imp_0_less add_increasing)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   767
    also have "\<dots> = - (1 + z + z)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   768
      by (simp add: neg add.assoc [symmetric])
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   769
    also have "\<dots> = 0" by (simp add: eq)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   770
    finally have "0<0" ..
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   771
    then show False by blast
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   772
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   773
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   774
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
   775
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   776
subsection \<open>The Set of Integers\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   777
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   778
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   779
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   780
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   781
definition Ints :: "'a set"  ("\<int>")
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   782
  where "\<int> = range of_int"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   783
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   784
lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   785
  by (simp add: Ints_def)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   786
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   787
lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   788
  using Ints_of_int [of "of_nat n"] by simp
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   789
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   790
lemma Ints_0 [simp]: "0 \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   791
  using Ints_of_int [of "0"] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   792
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   793
lemma Ints_1 [simp]: "1 \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   794
  using Ints_of_int [of "1"] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   795
61552
980dd46a03fb Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents: 61531
diff changeset
   796
lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
980dd46a03fb Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents: 61531
diff changeset
   797
  by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
980dd46a03fb Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents: 61531
diff changeset
   798
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   799
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   800
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   801
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   802
  apply (rule of_int_add [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   803
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   804
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   805
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   806
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   807
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   808
  apply (rule of_int_minus [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   809
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   810
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   811
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   812
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   813
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   814
  apply (rule of_int_diff [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   815
  done
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   816
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   817
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   818
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   819
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   820
  apply (rule of_int_mult [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   821
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   822
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   823
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   824
  by (induct n) simp_all
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   825
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   826
lemma Ints_cases [cases set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   827
  assumes "q \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   828
  obtains (of_int) z where "q = of_int z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   829
  unfolding Ints_def
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   830
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   831
  from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   832
  then obtain z where "q = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   833
  then show thesis ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   834
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   835
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   836
lemma Ints_induct [case_names of_int, induct set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   837
  "q \<in> \<int> \<Longrightarrow> (\<And>z. P (of_int z)) \<Longrightarrow> P q"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   838
  by (rule Ints_cases) auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   839
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   840
lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   841
  unfolding Nats_def Ints_def
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   842
  by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   843
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   844
lemma Nats_altdef1: "\<nat> = {of_int n |n. n \<ge> 0}"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   845
proof (intro subsetI equalityI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   846
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   847
  assume "x \<in> {of_int n |n. n \<ge> 0}"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   848
  then obtain n where "x = of_int n" "n \<ge> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   849
    by (auto elim!: Ints_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   850
  then have "x = of_nat (nat n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   851
    by (subst of_nat_nat) simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   852
  then show "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   853
    by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   854
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   855
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   856
  assume "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   857
  then obtain n where "x = of_nat n"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   858
    by (auto elim!: Nats_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   859
  then have "x = of_int (int n)" by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   860
  also have "int n \<ge> 0" by simp
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   861
  then have "of_int (int n) \<in> {of_int n |n. n \<ge> 0}" by blast
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   862
  finally show "x \<in> {of_int n |n. n \<ge> 0}" .
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   863
qed
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   864
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   865
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   866
64758
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
   867
lemma (in linordered_idom) Ints_abs [simp]:
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
   868
  shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
   869
  by (auto simp: abs_if)
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
   870
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   871
lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   872
proof (intro subsetI equalityI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   873
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   874
  assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   875
  then obtain n where "x = of_int n" "n \<ge> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   876
    by (auto elim!: Ints_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   877
  then have "x = of_nat (nat n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   878
    by (subst of_nat_nat) simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   879
  then show "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   880
    by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   881
qed (auto elim!: Nats_cases)
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   882
64849
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   883
lemma (in idom_divide) of_int_divide_in_Ints: 
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   884
  "of_int a div of_int b \<in> \<int>" if "b dvd a"
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   885
proof -
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   886
  from that obtain c where "a = b * c" ..
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   887
  then show ?thesis
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   888
    by (cases "of_int b = 0") simp_all
766db3539859 moved some lemmas to appropriate places
haftmann
parents: 64758
diff changeset
   889
qed
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   890
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   891
text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   892
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   893
lemma Ints_double_eq_0_iff:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   894
  fixes a :: "'a::ring_char_0"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   895
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   896
  shows "a + a = 0 \<longleftrightarrow> a = 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   897
    (is "?lhs \<longleftrightarrow> ?rhs")
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   898
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   899
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   900
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   901
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   902
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   903
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   904
    assume ?rhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   905
    then show ?lhs by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   906
  next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   907
    assume ?lhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   908
    with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   909
    then have "z + z = 0" by (simp only: of_int_eq_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   910
    then have "z = 0" by (simp only: double_eq_0_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   911
    with a show ?rhs by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   912
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   913
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   914
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   915
lemma Ints_odd_nonzero:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   916
  fixes a :: "'a::ring_char_0"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   917
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   918
  shows "1 + a + a \<noteq> 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   919
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   920
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   921
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   922
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   923
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   924
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   925
    assume "1 + a + a = 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   926
    with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   927
    then have "1 + z + z = 0" by (simp only: of_int_eq_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   928
    with odd_nonzero show False by blast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   929
  qed
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   930
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   931
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   932
lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   933
  using of_nat_in_Nats [of "numeral w"] by simp
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   934
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   935
lemma Ints_odd_less_0:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   936
  fixes a :: "'a::linordered_idom"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   937
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   938
  shows "1 + a + a < 0 \<longleftrightarrow> a < 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   939
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   940
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   941
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   942
  then obtain z where a: "a = of_int z" ..
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   943
  with a have "1 + a + a < 0 \<longleftrightarrow> of_int (1 + z + z) < (of_int 0 :: 'a)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   944
    by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   945
  also have "\<dots> \<longleftrightarrow> z < 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   946
    by (simp only: of_int_less_iff odd_less_0_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   947
  also have "\<dots> \<longleftrightarrow> a < 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   948
    by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   949
  finally show ?thesis .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   950
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   951
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   952
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   953
subsection \<open>@{term sum} and @{term prod}\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   954
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64014
diff changeset
   955
lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   956
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   957
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64014
diff changeset
   958
lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   959
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   960
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   961
lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   962
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   963
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   964
lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   965
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   966
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   967
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   968
text \<open>Legacy theorems\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   969
64714
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   970
lemmas int_sum = of_nat_sum [where 'a=int]
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   971
lemmas int_prod = of_nat_prod [where 'a=int]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   972
lemmas zle_int = of_nat_le_iff [where 'a=int]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   973
lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
64714
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   974
lemmas nonneg_eq_int = nonneg_int_cases
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   975
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   976
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   977
subsection \<open>Setting up simplification procedures\<close>
30802
f9e9e800d27e simplify theorem references
huffman
parents: 30796
diff changeset
   978
54249
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   979
lemmas of_int_simps =
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   980
  of_int_0 of_int_1 of_int_add of_int_mult
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   981
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48066
diff changeset
   982
ML_file "Tools/int_arith.ML"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   983
declaration \<open>K Int_Arith.setup\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   984
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   985
simproc_setup fast_arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   986
  ("(m::'a::linordered_idom) < n" |
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   987
    "(m::'a::linordered_idom) \<le> n" |
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   988
    "(m::'a::linordered_idom) = n") =
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 61076
diff changeset
   989
  \<open>K Lin_Arith.simproc\<close>
43595
7ae4a23b5be6 modernized some simproc setup;
wenzelm
parents: 43531
diff changeset
   990
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   991
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   992
subsection\<open>More Inequality Reasoning\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   993
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   994
lemma zless_add1_eq: "w < z + 1 \<longleftrightarrow> w < z \<or> w = z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   995
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   996
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   997
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   998
lemma add1_zle_eq: "w + 1 \<le> z \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   999
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1000
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1001
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1002
lemma zle_diff1_eq [simp]: "w \<le> z - 1 \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1003
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1004
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1005
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1006
lemma zle_add1_eq_le [simp]: "w < z + 1 \<longleftrightarrow> w \<le> z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1007
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1008
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1009
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1010
lemma int_one_le_iff_zero_less: "1 \<le> z \<longleftrightarrow> 0 < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1011
  for z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1012
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1013
64758
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1014
lemma Ints_nonzero_abs_ge1:
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1015
  fixes x:: "'a :: linordered_idom"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1016
    assumes "x \<in> Ints" "x \<noteq> 0"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1017
    shows "1 \<le> abs x"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1018
proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1019
  fix z::int
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1020
  assume "x = of_int z"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1021
    with \<open>x \<noteq> 0\<close> 
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1022
  show "1 \<le> \<bar>x\<bar>"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1023
    apply (auto simp add: abs_if)
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1024
    by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1025
qed
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1026
  
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1027
lemma Ints_nonzero_abs_less1:
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1028
  fixes x:: "'a :: linordered_idom"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1029
  shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1030
    using Ints_nonzero_abs_ge1 [of x] by auto
3b33d2fc5fc0 A few new lemmas and needed adaptations
paulson <lp15@cam.ac.uk>
parents: 64714
diff changeset
  1031
    
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1032
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1033
subsection \<open>The functions @{term nat} and @{term int}\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1034
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1035
text \<open>Simplify the term @{term "w + - z"}.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1036
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1037
lemma one_less_nat_eq [simp]: "Suc 0 < nat z \<longleftrightarrow> 1 < z"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
  1038
  using zless_nat_conj [of 1 z] by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1039
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1040
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1041
  This simplifies expressions of the form @{term "int n = z"} where
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1042
  \<open>z\<close> is an integer literal.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1043
\<close>
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1044
lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1045
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1046
lemma split_nat [arith_split]: "P (nat i) = ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1047
  (is "?P = (?L \<and> ?R)")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1048
  for i :: int
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1049
proof (cases "i < 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1050
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1051
  then show ?thesis by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1052
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1053
  case False
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1054
  have "?P = ?L"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1055
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1056
    assume ?P
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1057
    then show ?L using False by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1058
  next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1059
    assume ?L
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1060
    then show ?P using False by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1061
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1062
  with False show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1063
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1064
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1065
lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1066
  by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1067
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1068
lemma nat_int_add: "nat (int a + int b) = a + b"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1069
  by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1070
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1071
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1072
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1073
33056
791a4655cae3 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents: 32437
diff changeset
  1074
lemma of_int_of_nat [nitpick_simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1075
  "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1076
proof (cases "k < 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1077
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1078
  then have "0 \<le> - k" by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1079
  then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1080
  with True show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1081
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1082
  case False
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1083
  then show ?thesis by (simp add: not_less)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1084
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1085
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1086
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1087
64014
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1088
lemma transfer_rule_of_int:
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1089
  fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1090
  assumes [transfer_rule]: "R 0 0" "R 1 1"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1091
    "rel_fun R (rel_fun R R) plus plus"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1092
    "rel_fun R R uminus uminus"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1093
  shows "rel_fun HOL.eq R of_int of_int"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1094
proof -
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1095
  note transfer_rule_of_nat [transfer_rule]
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1096
  have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1097
    by transfer_prover
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1098
  show ?thesis
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1099
    by (unfold of_int_of_nat [abs_def]) transfer_prover
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1100
qed
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1101
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1102
lemma nat_mult_distrib:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1103
  fixes z z' :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1104
  assumes "0 \<le> z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1105
  shows "nat (z * z') = nat z * nat z'"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1106
proof (cases "0 \<le> z'")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1107
  case False
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1108
  with assms have "z * z' \<le> 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1109
    by (simp add: not_le mult_le_0_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1110
  then have "nat (z * z') = 0" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1111
  moreover from False have "nat z' = 0" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1112
  ultimately show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1113
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1114
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1115
  with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1116
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1117
    by (rule injD [of "of_nat :: nat \<Rightarrow> int", OF inj_of_nat])
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1118
      (simp only: of_nat_mult of_nat_nat [OF True]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1119
         of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1120
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1121
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1122
lemma nat_mult_distrib_neg: "z \<le> 0 \<Longrightarrow> nat (z * z') = nat (- z) * nat (- z')"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1123
  for z z' :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1124
  apply (rule trans)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1125
   apply (rule_tac [2] nat_mult_distrib)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1126
   apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1127
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1128
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
  1129
lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1130
  by (cases "z = 0 \<or> w = 0")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1131
    (auto simp add: abs_if nat_mult_distrib [symmetric]
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1132
      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1133
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1134
lemma int_in_range_abs [simp]: "int n \<in> range abs"
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1135
proof (rule range_eqI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1136
  show "int n = \<bar>int n\<bar>" by simp
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1137
qed
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1138
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1139
lemma range_abs_Nats [simp]: "range abs = (\<nat> :: int set)"
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1140
proof -
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1141
  have "\<bar>k\<bar> \<in> \<nat>" for k :: int
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1142
    by (cases k) simp_all
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1143
  moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1144
    using that by induct simp
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1145
  ultimately show ?thesis by blast
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61169
diff changeset
  1146
qed
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1147
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1148
lemma Suc_nat_eq_nat_zadd1: "0 \<le> z \<Longrightarrow> Suc (nat z) = nat (1 + z)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1149
  for z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1150
  by (rule sym) (simp add: nat_eq_iff)
47207
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1151
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1152
lemma diff_nat_eq_if:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1153
  "nat z - nat z' =
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1154
    (if z' < 0 then nat z
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1155
     else
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1156
      let d = z - z'
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1157
      in if d < 0 then 0 else nat d)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1158
  by (simp add: Let_def nat_diff_distrib [symmetric])
47207
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1159
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1160
lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)"
47207
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1161
  using diff_nat_numeral [of v Num.One] by simp
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1162
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1163
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1164
subsection \<open>Induction principles for int\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1165
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1166
text \<open>Well-founded segments of the integers.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1167
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1168
definition int_ge_less_than :: "int \<Rightarrow> (int \<times> int) set"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1169
  where "int_ge_less_than d = {(z', z). d \<le> z' \<and> z' < z}"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1170
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1171
lemma wf_int_ge_less_than: "wf (int_ge_less_than d)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1172
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1173
  have "int_ge_less_than d \<subseteq> measure (\<lambda>z. nat (z - d))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1174
    by (auto simp add: int_ge_less_than_def)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1175
  then show ?thesis
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
  1176
    by (rule wf_subset [OF wf_measure])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1177
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1178
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1179
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1180
  This variant looks odd, but is typical of the relations suggested
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1181
  by RankFinder.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1182
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1183
definition int_ge_less_than2 :: "int \<Rightarrow> (int \<times> int) set"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1184
  where "int_ge_less_than2 d = {(z',z). d \<le> z \<and> z' < z}"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1185
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1186
lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1187
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1188
  have "int_ge_less_than2 d \<subseteq> measure (\<lambda>z. nat (1 + z - d))"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1189
    by (auto simp add: int_ge_less_than2_def)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1190
  then show ?thesis
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
  1191
    by (rule wf_subset [OF wf_measure])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1192
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1193
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1194
(* `set:int': dummy construction *)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1195
theorem int_ge_induct [case_names base step, induct set: int]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1196
  fixes i :: int
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1197
  assumes ge: "k \<le> i"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1198
    and base: "P k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1199
    and step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1200
  shows "P i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1201
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1202
  have "\<And>i::int. n = nat (i - k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" for n
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1203
  proof (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1204
    case 0
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1205
    then have "i = k" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1206
    with base show "P i" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1207
  next
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1208
    case (Suc n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1209
    then have "n = nat ((i - 1) - k)" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1210
    moreover have k: "k \<le> i - 1" using Suc.prems by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1211
    ultimately have "P (i - 1)" by (rule Suc.hyps)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1212
    from step [OF k this] show ?case by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1213
  qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1214
  with ge show ?thesis by fast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1215
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1216
25928
042e877d9841 tuned code setup
haftmann
parents: 25919
diff changeset
  1217
(* `set:int': dummy construction *)
042e877d9841 tuned code setup
haftmann
parents: 25919
diff changeset
  1218
theorem int_gr_induct [case_names base step, induct set: int]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1219
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1220
  assumes gr: "k < i"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1221
    and base: "P (k + 1)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1222
    and step: "\<And>i. k < i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1223
  shows "P i"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1224
  apply (rule int_ge_induct[of "k + 1"])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1225
  using gr apply arith
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1226
   apply (rule base)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1227
  apply (rule step)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1228
   apply simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1229
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1230
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1231
theorem int_le_induct [consumes 1, case_names base step]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1232
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1233
  assumes le: "i \<le> k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1234
    and base: "P k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1235
    and step: "\<And>i. i \<le> k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1236
  shows "P i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1237
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1238
  have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" for n
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1239
  proof (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1240
    case 0
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1241
    then have "i = k" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1242
    with base show "P i" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1243
  next
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1244
    case (Suc n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1245
    then have "n = nat (k - (i + 1))" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1246
    moreover have k: "i + 1 \<le> k" using Suc.prems by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1247
    ultimately have "P (i + 1)" by (rule Suc.hyps)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1248
    from step[OF k this] show ?case by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1249
  qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1250
  with le show ?thesis by fast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1251
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1252
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1253
theorem int_less_induct [consumes 1, case_names base step]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1254
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1255
  assumes less: "i < k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1256
    and base: "P (k - 1)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1257
    and step: "\<And>i. i < k \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1258
  shows "P i"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1259
  apply (rule int_le_induct[of _ "k - 1"])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1260
  using less apply arith
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1261
   apply (rule base)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1262
  apply (rule step)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1263
   apply simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1264
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1265
36811
4ab4aa5bee1c renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
haftmann
parents: 36801
diff changeset
  1266
theorem int_induct [case_names base step1 step2]:
36801
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1267
  fixes k :: int
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1268
  assumes base: "P k"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1269
    and step1: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1270
    and step2: "\<And>i. k \<ge> i \<Longrightarrow> P i \<Longrightarrow> P (i - 1)"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1271
  shows "P i"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1272
proof -
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1273
  have "i \<le> k \<or> i \<ge> k" by arith
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1274
  then show ?thesis
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1275
  proof
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1276
    assume "i \<ge> k"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1277
    then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1278
      using base by (rule int_ge_induct) (fact step1)
36801
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1279
  next
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1280
    assume "i \<le> k"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1281
    then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1282
      using base by (rule int_le_induct) (fact step2)
36801
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1283
  qed
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1284
qed
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1285
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1286
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1287
subsection \<open>Intermediate value theorems\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1288
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1289
lemma int_val_lemma: "(\<forall>i<n. \<bar>f (i + 1) - f i\<bar> \<le> 1) \<longrightarrow> f 0 \<le> k \<longrightarrow> k \<le> f n \<longrightarrow> (\<exists>i \<le> n. f i = k)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1290
  for n :: nat and k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1291
  unfolding One_nat_def
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1292
  apply (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1293
   apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1294
  apply (intro strip)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1295
  apply (erule impE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1296
   apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1297
  apply (erule_tac x = n in allE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1298
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1299
  apply (case_tac "k = f (Suc n)")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1300
   apply force
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1301
  apply (erule impE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1302
   apply (simp add: abs_if split: if_split_asm)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1303
  apply (blast intro: le_SucI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1304
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1305
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1306
lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1307
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1308
lemma nat_intermed_int_val:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1309
  "\<forall>i. m \<le> i \<and> i < n \<longrightarrow> \<bar>f (i + 1) - f i\<bar> \<le> 1 \<Longrightarrow> m < n \<Longrightarrow>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1310
    f m \<le> k \<Longrightarrow> k \<le> f n \<Longrightarrow> \<exists>i. m \<le> i \<and> i \<le> n \<and> f i = k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1311
    for f :: "nat \<Rightarrow> int" and k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1312
  apply (cut_tac n = "n-m" and f = "\<lambda>i. f (i + m)" and k = k in int_val_lemma)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1313
  unfolding One_nat_def
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1314
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1315
  apply (erule exE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1316
  apply (rule_tac x = "i+m" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1317
  apply arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1318
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1319
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1320
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1321
subsection \<open>Products and 1, by T. M. Rasmussen\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1322
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1323
lemma abs_zmult_eq_1:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1324
  fixes m n :: int
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1325
  assumes mn: "\<bar>m * n\<bar> = 1"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1326
  shows "\<bar>m\<bar> = 1"
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1327
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1328
  from mn have 0: "m \<noteq> 0" "n \<noteq> 0" by auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1329
  have "\<not> 2 \<le> \<bar>m\<bar>"
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1330
  proof
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1331
    assume "2 \<le> \<bar>m\<bar>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1332
    then have "2 * \<bar>n\<bar> \<le> \<bar>m\<bar> * \<bar>n\<bar>" by (simp add: mult_mono 0)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1333
    also have "\<dots> = \<bar>m * n\<bar>" by (simp add: abs_mult)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1334
    also from mn have "\<dots> = 1" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1335
    finally have "2 * \<bar>n\<bar> \<le> 1" .
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1336
    with 0 show "False" by arith
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1337
  qed
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1338
  with 0 show ?thesis by auto
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1339
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1340
6