src/HOL/Int.thy
author haftmann
Fri, 30 Dec 2016 18:02:27 +0100
changeset 64714 53bab28983f1
parent 64272 f76b6dda2e56
child 64758 3b33d2fc5fc0
permissions -rw-r--r--
complete set of cases rules for integers known to be (non-)positive/negative; legacy theorem branding
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
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   258
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   259
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   260
context ring_char_0
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   261
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   262
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   263
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
   264
  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
   265
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   266
text \<open>Special cases where either operand is zero.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   267
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
   268
  using of_int_eq_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   269
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   270
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
   271
  using of_int_eq_iff [of 0 z] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   272
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   273
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
   274
  using of_int_eq_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   275
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   276
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   277
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   278
context linordered_idom
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   279
begin
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   280
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   281
text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   282
subclass ring_char_0 ..
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   283
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   284
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
   285
  by (transfer fixing: less_eq)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   286
    (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
   287
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   288
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
   289
  by (simp add: less_le order_less_le)
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   290
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   291
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
   292
  using of_int_le_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   293
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   294
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
   295
  using of_int_le_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   296
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   297
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
   298
  using of_int_less_iff [of 0 z] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   299
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   300
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
   301
  using of_int_less_iff [of z 0] by simp
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   302
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   303
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
   304
  using of_int_le_iff [of 1 z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   305
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   306
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
   307
  using of_int_le_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   308
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   309
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
   310
  using of_int_less_iff [of 1 z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   311
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   312
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
   313
  using of_int_less_iff [of z 1] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   314
62128
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   315
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
   316
  by simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   317
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   318
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
   319
  by simp
3201ddb00097 Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents: 61944
diff changeset
   320
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   321
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
   322
  by (auto simp add: abs_if)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   323
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   324
lemma of_int_lessD:
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   325
  assumes "\<bar>of_int n\<bar> < x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   326
  shows "n = 0 \<or> x > 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   327
proof (cases "n = 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   328
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   329
  then show ?thesis by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   330
next
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   331
  case False
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   332
  then have "\<bar>n\<bar> \<noteq> 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   333
  then have "\<bar>n\<bar> > 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   334
  then have "\<bar>n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   335
    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   336
  then have "\<bar>of_int n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   337
    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   338
  then have "1 < x" using assms by (rule le_less_trans)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   339
  then show ?thesis ..
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   340
qed
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   341
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   342
lemma of_int_leD:
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   343
  assumes "\<bar>of_int n\<bar> \<le> x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   344
  shows "n = 0 \<or> 1 \<le> x"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   345
proof (cases "n = 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   346
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   347
  then show ?thesis by simp
62347
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   348
next
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   349
  case False
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   350
  then have "\<bar>n\<bar> \<noteq> 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   351
  then have "\<bar>n\<bar> > 0" by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   352
  then have "\<bar>n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   353
    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   354
  then have "\<bar>of_int n\<bar> \<ge> 1"
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   355
    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   356
  then have "1 \<le> x" using assms by (rule order_trans)
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   357
  then show ?thesis ..
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   358
qed
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   359
2230b7047376 generalized some lemmas;
haftmann
parents: 62128
diff changeset
   360
36424
f3f389fc7974 got rid of [simplified]
haftmann
parents: 36409
diff changeset
   361
end
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   362
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   363
text \<open>Comparisons involving @{term of_int}.\<close>
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   364
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   365
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
   366
  using of_int_eq_iff by fastforce
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   367
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
   368
lemma of_int_le_numeral_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   369
  "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
   370
  using of_int_le_iff [of z "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   371
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
   372
lemma of_int_numeral_le_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   373
  "(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
   374
  using of_int_le_iff [of "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   375
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
   376
lemma of_int_less_numeral_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   377
  "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
   378
  using of_int_less_iff [of z "numeral n"] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   379
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
   380
lemma of_int_numeral_less_iff [simp]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   381
  "(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
   382
  using of_int_less_iff [of "numeral n" z] by simp
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   383
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   384
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
   385
  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
   386
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   387
lemma of_int_eq_id [simp]: "of_int = id"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   388
proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   389
  show "of_int z = id z" for z
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   390
    by (cases z rule: int_diff_cases) simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   391
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   392
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   393
instance int :: no_top
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61144
diff changeset
   394
  apply standard
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   395
  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
   396
  apply simp
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   397
  done
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   398
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   399
instance int :: no_bot
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 61144
diff changeset
   400
  apply standard
51329
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   401
  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
   402
  apply simp
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   403
  done
4a3c453f99a1 split dense into inner_dense_order and no_top/no_bot
hoelzl
parents: 51185
diff changeset
   404
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   405
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   406
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
   407
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   408
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
   409
  by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   410
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   411
lemma nat_int [simp]: "nat (int n) = n"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   412
  by transfer simp
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 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
   415
  by transfer clarsimp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   416
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   417
lemma nat_0_le: "0 \<le> z \<Longrightarrow> int (nat z) = z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   418
  by simp
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_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
   421
  by transfer clarsimp
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_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
   424
  by transfer (clarsimp, arith)
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
text \<open>An alternative condition is @{term "0 \<le> w"}.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   427
lemma nat_mono_iff: "0 < z \<Longrightarrow> nat w < nat z \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   428
  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
   429
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   430
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
   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 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
   434
  by transfer (clarsimp, arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   435
64714
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   436
lemma nonneg_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   437
  assumes "0 \<le> k"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   438
  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
   439
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   440
  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
   441
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   442
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   443
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   444
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   445
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   446
lemma pos_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   447
  assumes "0 < k"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   448
  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
   449
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   450
  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
   451
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   452
  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
   453
    by (rule nonneg_int_cases)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   454
  moreover have "n > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   455
    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
   456
  ultimately show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   457
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   458
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   459
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   460
lemma nonpos_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   461
  assumes "k \<le> 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   462
  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
   463
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   464
  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
   465
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   466
  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
   467
    by (rule nonneg_int_cases)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   468
  then have "k = - int n"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   469
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   470
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   471
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   472
qed
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   473
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   474
lemma neg_int_cases:
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   475
  assumes "k < 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   476
  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
   477
proof -
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   478
  from assms have "- k > 0"
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   479
    by simp
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   480
  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
   481
    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
   482
  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
   483
    by simp_all
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   484
  then show thesis
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   485
    by (rule that)
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   486
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   487
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   488
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
   489
  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
   490
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   491
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
   492
  using nat_eq_iff [of w m] by auto
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   493
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   494
lemma nat_0 [simp]: "nat 0 = 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   495
  by (simp add: nat_eq_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   496
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   497
lemma nat_1 [simp]: "nat 1 = Suc 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   498
  by (simp add: nat_eq_iff)
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   499
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   500
lemma nat_numeral [simp]: "nat (numeral k) = numeral k"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   501
  by (simp add: nat_eq_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   502
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   503
lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0"
54223
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   504
  by simp
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   505
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   506
lemma nat_2: "nat 2 = Suc (Suc 0)"
85705ba18add restructed
haftmann
parents: 54147
diff changeset
   507
  by simp
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   508
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   509
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
   510
  by transfer (clarsimp, arith)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   511
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   512
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
   513
  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
   514
487ae6317f7b move lemmas nat_le_iff and nat_mono into Int.thy
huffman
parents: 44695
diff changeset
   515
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
   516
  by transfer auto
44707
487ae6317f7b move lemmas nat_le_iff and nat_mono into Int.thy
huffman
parents: 44695
diff changeset
   517
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   518
lemma nat_0_iff[simp]: "nat i = 0 \<longleftrightarrow> i \<le> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   519
  for i :: int
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   520
  by transfer clarsimp
29700
22faf21db3df added some simp rules
nipkow
parents: 29668
diff changeset
   521
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   522
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
   523
  by (auto simp add: nat_eq_iff2)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   524
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   525
lemma zero_less_nat_eq [simp]: "0 < nat z \<longleftrightarrow> 0 < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   526
  using zless_nat_conj [of 0] by auto
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 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
   529
  by transfer clarsimp
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_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
   532
  by transfer clarsimp
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   533
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   534
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
   535
  by (rule nat_diff_distrib') auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   536
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   537
lemma nat_zminus_int [simp]: "nat (- int n) = 0"
48045
fbf77fdf9ae4 convert Int.thy to use lifting and transfer
huffman
parents: 48044
diff changeset
   538
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   539
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   540
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
   541
  by transfer auto
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   542
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   543
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
   544
  by transfer (clarsimp simp add: less_diff_conv)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   545
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   546
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
   547
  by transfer (clarsimp simp add: of_nat_diff)
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 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
   550
  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   551
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   552
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   553
text \<open>For termination proofs:\<close>
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   554
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
   555
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   556
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   557
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
   558
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 61070
diff changeset
   559
lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   560
  by (simp add: order_less_le del: of_nat_Suc)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   561
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   562
lemma negative_zless [iff]: "- (int (Suc n)) < int m"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   563
  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
   564
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   565
lemma negative_zle_0: "- int n \<le> 0"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   566
  by (simp add: minus_le_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   567
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   568
lemma negative_zle [iff]: "- int n \<le> int m"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   569
  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
   570
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   571
lemma not_zle_0_negative [simp]: "\<not> 0 \<le> - int (Suc n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   572
  by (subst le_minus_iff) (simp del: of_nat_Suc)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   573
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   574
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
   575
  by transfer simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   576
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   577
lemma not_int_zless_negative [simp]: "\<not> int n < - int m"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   578
  by (simp add: linorder_not_less)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   579
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   580
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
   581
  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
   582
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   583
lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   584
  (is "?lhs \<longleftrightarrow> ?rhs")
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   585
proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   586
  assume ?rhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   587
  then show ?lhs by auto
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   588
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   589
  assume ?lhs
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   590
  then have "0 \<le> z - w" by simp
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   591
  then obtain n where "z - w = int n"
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 62347
diff changeset
   592
    using zero_le_imp_eq_int [of "z - w"] by blast
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   593
  then have "z = w + int n" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   594
  then show ?rhs ..
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   595
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   596
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   597
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   598
  by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   599
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   600
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   601
  This version is proved for all ordered rings, not just integers!
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   602
  It is proved here because attribute \<open>arith_split\<close> is not available
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   603
  in theory \<open>Rings\<close>.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   604
  But is it really better than just rewriting with \<open>abs_if\<close>?
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   605
\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   606
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
   607
  for a :: "'a::linordered_idom"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   608
  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
   609
44709
79f10d9e63c1 introduce abbreviation 'int' earlier in Int.thy
huffman
parents: 44707
diff changeset
   610
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   611
  apply transfer
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   612
  apply clarsimp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   613
  apply (rule_tac x="b - Suc a" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   614
  apply arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   615
  done
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   616
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   617
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   618
subsection \<open>Cases and induction\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   619
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   620
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   621
  Now we replace the case analysis rule by a more conventional one:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   622
  whether an integer is negative or not.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   623
\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   624
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   625
text \<open>This version is symmetric in the two subgoals.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   626
lemma int_cases2 [case_names nonneg nonpos, cases type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   627
  "(\<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
   628
  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
   629
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   630
text \<open>This is the default, with a negative case.\<close>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   631
lemma int_cases [case_names nonneg neg, cases type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   632
  "(\<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
   633
  apply (cases "z < 0")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   634
   apply (blast dest!: negD)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   635
  apply (simp add: linorder_not_less del: of_nat_Suc)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   636
  apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   637
  apply (blast dest: nat_0_le [THEN sym])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   638
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   639
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   640
lemma int_cases3 [case_names zero pos neg]:
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   641
  fixes k :: int
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   642
  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
   643
    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
   644
  shows "P"
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   645
proof (cases k "0::int" rule: linorder_cases)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   646
  case equal
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   647
  with assms(1) show P by simp
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   648
next
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   649
  case greater
63539
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   650
  then have *: "nat k > 0" by simp
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   651
  moreover from * have "k = int (nat k)" by auto
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   652
  ultimately show P using assms(2) by blast
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   653
next
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   654
  case less
63539
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   655
  then have *: "nat (- k) > 0" by simp
70d4d9e5707b tuned proofs -- avoid improper use of "this";
wenzelm
parents: 62390
diff changeset
   656
  moreover from * have "k = - int (nat (- k))" by auto
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   657
  ultimately show P using assms(3) by blast
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   658
qed
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60758
diff changeset
   659
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   660
lemma int_of_nat_induct [case_names nonneg neg, induct type: int]:
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   661
  "(\<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
   662
  by (cases z) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   663
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   664
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   665
  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   666
  by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
37767
a2b7a20d6ea3 dropped superfluous [code del]s
haftmann
parents: 36811
diff changeset
   667
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   668
lemma Let_neg_numeral [simp]: "Let (- numeral v) f = f (- numeral v)"
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   669
  \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   670
  by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   671
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
   672
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   673
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   674
lemmas max_number_of [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   675
  max_def [of "numeral u" "numeral v"]
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   676
  max_def [of "numeral u" "- numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   677
  max_def [of "- numeral u" "numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   678
  max_def [of "- numeral u" "- numeral v"] for u v
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   679
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   680
lemmas min_number_of [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   681
  min_def [of "numeral u" "numeral v"]
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   682
  min_def [of "numeral u" "- numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   683
  min_def [of "- numeral u" "numeral v"]
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54249
diff changeset
   684
  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
   685
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   686
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   687
subsubsection \<open>Binary comparisons\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   688
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   689
text \<open>Preliminaries\<close>
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   690
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   691
lemma le_imp_0_less:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   692
  fixes z :: int
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   693
  assumes le: "0 \<le> z"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   694
  shows "0 < 1 + z"
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   695
proof -
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   696
  have "0 \<le> z" by fact
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   697
  also have "\<dots> < z + 1" by (rule less_add_one)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   698
  also have "\<dots> = 1 + z" by (simp add: ac_simps)
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   699
  finally show "0 < 1 + z" .
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   700
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   701
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   702
lemma odd_less_0_iff: "1 + z + z < 0 \<longleftrightarrow> z < 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   703
  for z :: int
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
   704
proof (cases z)
28958
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   705
  case (nonneg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   706
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   707
    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
   708
next
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   709
  case (neg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   710
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   711
    by (simp del: of_nat_Suc of_nat_add of_nat_1
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   712
        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
   713
qed
74c60b78969c cleaned up subsection headings;
huffman
parents: 28952
diff changeset
   714
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   715
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   716
subsubsection \<open>Comparisons, for Ordered Rings\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   717
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   718
lemmas double_eq_0_iff = double_zero
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   719
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   720
lemma odd_nonzero: "1 + z + z \<noteq> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   721
  for z :: int
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
   722
proof (cases z)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   723
  case (nonneg n)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   724
  have le: "0 \<le> z + z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   725
    by (simp add: nonneg add_increasing)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   726
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   727
    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
   728
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   729
  case (neg n)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   730
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   731
  proof
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   732
    assume eq: "1 + z + z = 0"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   733
    have "0 < 1 + (int n + int n)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   734
      by (simp add: le_imp_0_less add_increasing)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   735
    also have "\<dots> = - (1 + z + z)"
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   736
      by (simp add: neg add.assoc [symmetric])
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   737
    also have "\<dots> = 0" by (simp add: eq)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   738
    finally have "0<0" ..
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   739
    then show False by blast
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   740
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   741
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   742
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
   743
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   744
subsection \<open>The Set of Integers\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   745
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   746
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   747
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   748
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   749
definition Ints :: "'a set"  ("\<int>")
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   750
  where "\<int> = range of_int"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   751
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   752
lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   753
  by (simp add: Ints_def)
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   754
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   755
lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   756
  using Ints_of_int [of "of_nat n"] by simp
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   757
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   758
lemma Ints_0 [simp]: "0 \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   759
  using Ints_of_int [of "0"] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   760
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   761
lemma Ints_1 [simp]: "1 \<in> \<int>"
45533
af3690f6bd79 simplify some proofs
huffman
parents: 45532
diff changeset
   762
  using Ints_of_int [of "1"] by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   763
61552
980dd46a03fb Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents: 61531
diff changeset
   764
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
   765
  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
   766
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   767
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
   768
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   769
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   770
  apply (rule of_int_add [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   771
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   772
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   773
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> -a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   774
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   775
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   776
  apply (rule of_int_minus [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   777
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   778
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   779
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
   780
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   781
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   782
  apply (rule of_int_diff [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   783
  done
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   784
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   785
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
   786
  apply (auto simp add: Ints_def)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   787
  apply (rule range_eqI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   788
  apply (rule of_int_mult [symmetric])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   789
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   790
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   791
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   792
  by (induct n) simp_all
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   793
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   794
lemma Ints_cases [cases set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   795
  assumes "q \<in> \<int>"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   796
  obtains (of_int) z where "q = of_int z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   797
  unfolding Ints_def
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   798
proof -
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   799
  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
   800
  then obtain z where "q = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   801
  then show thesis ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   802
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   803
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   804
lemma Ints_induct [case_names of_int, induct set: Ints]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   805
  "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
   806
  by (rule Ints_cases) auto
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   807
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   808
lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>"
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   809
  unfolding Nats_def Ints_def
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   810
  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
   811
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   812
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
   813
proof (intro subsetI equalityI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   814
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   815
  assume "x \<in> {of_int n |n. n \<ge> 0}"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   816
  then obtain n where "x = of_int n" "n \<ge> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   817
    by (auto elim!: Ints_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   818
  then have "x = of_nat (nat n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   819
    by (subst of_nat_nat) simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   820
  then show "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   821
    by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   822
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   823
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   824
  assume "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   825
  then obtain n where "x = of_nat n"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   826
    by (auto elim!: Nats_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   827
  then have "x = of_int (int n)" by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   828
  also have "int n \<ge> 0" by simp
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   829
  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
   830
  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
   831
qed
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   832
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   833
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   834
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   835
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
   836
proof (intro subsetI equalityI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   837
  fix x :: 'a
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   838
  assume "x \<in> {n \<in> \<int>. n \<ge> 0}"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   839
  then obtain n where "x = of_int n" "n \<ge> 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   840
    by (auto elim!: Ints_cases)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   841
  then have "x = of_nat (nat n)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   842
    by (subst of_nat_nat) simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   843
  then show "x \<in> \<nat>"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   844
    by simp
61524
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   845
qed (auto elim!: Nats_cases)
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   846
f2e51e704a96 added many small lemmas about setsum/setprod/powr/...
eberlm
parents: 61234
diff changeset
   847
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   848
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
   849
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   850
lemma Ints_double_eq_0_iff:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   851
  fixes a :: "'a::ring_char_0"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   852
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   853
  shows "a + a = 0 \<longleftrightarrow> a = 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   854
    (is "?lhs \<longleftrightarrow> ?rhs")
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   855
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   856
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   857
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   858
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   859
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   860
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   861
    assume ?rhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   862
    then show ?lhs by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   863
  next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   864
    assume ?lhs
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   865
    with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   866
    then have "z + z = 0" by (simp only: of_int_eq_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   867
    then have "z = 0" by (simp only: double_eq_0_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   868
    with a show ?rhs by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   869
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   870
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   871
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   872
lemma Ints_odd_nonzero:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   873
  fixes a :: "'a::ring_char_0"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   874
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   875
  shows "1 + a + a \<noteq> 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   876
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   877
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   878
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   879
  then obtain z where a: "a = of_int z" ..
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   880
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   881
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   882
    assume "1 + a + a = 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   883
    with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   884
    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
   885
    with odd_nonzero show False by blast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   886
  qed
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   887
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   888
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   889
lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   890
  using of_nat_in_Nats [of "numeral w"] by simp
35634
6fdfe37b84d6 add more simp rules for Ints
huffman
parents: 35216
diff changeset
   891
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
   892
lemma Ints_odd_less_0:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   893
  fixes a :: "'a::linordered_idom"
61070
b72a990adfe2 prefer symbols;
wenzelm
parents: 60868
diff changeset
   894
  assumes in_Ints: "a \<in> \<int>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   895
  shows "1 + a + a < 0 \<longleftrightarrow> a < 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   896
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   897
  from in_Ints have "a \<in> range of_int"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   898
    unfolding Ints_def [symmetric] .
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   899
  then obtain z where a: "a = of_int z" ..
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   900
  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
   901
    by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   902
  also have "\<dots> \<longleftrightarrow> z < 0"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   903
    by (simp only: of_int_less_iff odd_less_0_iff)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   904
  also have "\<dots> \<longleftrightarrow> a < 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   905
    by (simp add: a)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   906
  finally show ?thesis .
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   907
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   908
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   909
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   910
subsection \<open>@{term sum} and @{term prod}\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   911
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64014
diff changeset
   912
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
   913
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   914
64267
b9a1486e79be setsum -> sum
nipkow
parents: 64014
diff changeset
   915
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
   916
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   917
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   918
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
   919
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   920
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   921
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
   922
  by (induct A rule: infinite_finite_induct) auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   923
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   924
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   925
text \<open>Legacy theorems\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   926
64714
53bab28983f1 complete set of cases rules for integers known to be (non-)positive/negative;
haftmann
parents: 64272
diff changeset
   927
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
   928
lemmas int_prod = of_nat_prod [where 'a=int]
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   929
lemmas zle_int = of_nat_le_iff [where 'a=int]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   930
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
   931
lemmas nonneg_eq_int = nonneg_int_cases
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   932
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   933
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   934
subsection \<open>Setting up simplification procedures\<close>
30802
f9e9e800d27e simplify theorem references
huffman
parents: 30796
diff changeset
   935
54249
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   936
lemmas of_int_simps =
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   937
  of_int_0 of_int_1 of_int_add of_int_mult
ce00f2fef556 streamlined setup of linear arithmetic
haftmann
parents: 54230
diff changeset
   938
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48066
diff changeset
   939
ML_file "Tools/int_arith.ML"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   940
declaration \<open>K Int_Arith.setup\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   941
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   942
simproc_setup fast_arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   943
  ("(m::'a::linordered_idom) < n" |
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   944
    "(m::'a::linordered_idom) \<le> n" |
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   945
    "(m::'a::linordered_idom) = n") =
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 61076
diff changeset
   946
  \<open>K Lin_Arith.simproc\<close>
43595
7ae4a23b5be6 modernized some simproc setup;
wenzelm
parents: 43531
diff changeset
   947
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   948
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
   949
subsection\<open>More Inequality Reasoning\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   950
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   951
lemma zless_add1_eq: "w < z + 1 \<longleftrightarrow> w < z \<or> w = z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   952
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   953
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   954
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   955
lemma add1_zle_eq: "w + 1 \<le> z \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   956
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   957
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   958
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   959
lemma zle_diff1_eq [simp]: "w \<le> z - 1 \<longleftrightarrow> w < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   960
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   961
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   962
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   963
lemma zle_add1_eq_le [simp]: "w < z + 1 \<longleftrightarrow> w \<le> z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   964
  for w z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   965
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   966
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   967
lemma int_one_le_iff_zero_less: "1 \<le> z \<longleftrightarrow> 0 < z"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   968
  for z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   969
  by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   970
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   971
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   972
subsection \<open>The functions @{term nat} and @{term int}\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   973
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   974
text \<open>Simplify the term @{term "w + - z"}.\<close>
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
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
   977
  using zless_nat_conj [of 1 z] by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   978
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   979
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   980
  This simplifies expressions of the form @{term "int n = z"} where
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   981
  \<open>z\<close> is an integer literal.
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   982
\<close>
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
   983
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
   984
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   985
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
   986
  (is "?P = (?L \<and> ?R)")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   987
  for i :: int
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   988
proof (cases "i < 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   989
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   990
  then show ?thesis by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   991
next
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   992
  case False
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   993
  have "?P = ?L"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   994
  proof
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   995
    assume ?P
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   996
    then show ?L using False by auto
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
   997
  next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   998
    assume ?L
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
   999
    then show ?P using False by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1000
  qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1001
  with False show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1002
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1003
59000
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1004
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
  1005
  by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1006
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1007
lemma nat_int_add: "nat (int a + int b) = a + b"
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1008
  by auto
6eb0725503fc import general theorems from AFP/Markov_Models
hoelzl
parents: 58889
diff changeset
  1009
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1010
context ring_1
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1011
begin
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1012
33056
791a4655cae3 renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents: 32437
diff changeset
  1013
lemma of_int_of_nat [nitpick_simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1014
  "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
  1015
proof (cases "k < 0")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1016
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1017
  then have "0 \<le> - k" by simp
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1018
  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
  1019
  with True show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1020
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1021
  case False
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1022
  then show ?thesis by (simp add: not_less)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1023
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1024
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1025
end
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1026
64014
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1027
lemma transfer_rule_of_int:
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1028
  fixes R :: "'a::ring_1 \<Rightarrow> 'b::ring_1 \<Rightarrow> bool"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1029
  assumes [transfer_rule]: "R 0 0" "R 1 1"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1030
    "rel_fun R (rel_fun R R) plus plus"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1031
    "rel_fun R R uminus uminus"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1032
  shows "rel_fun HOL.eq R of_int of_int"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1033
proof -
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1034
  note transfer_rule_of_nat [transfer_rule]
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1035
  have [transfer_rule]: "rel_fun HOL.eq R of_nat of_nat"
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1036
    by transfer_prover
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1037
  show ?thesis
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1038
    by (unfold of_int_of_nat [abs_def]) transfer_prover
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1039
qed
ca1239a3277b more lemmas
haftmann
parents: 63652
diff changeset
  1040
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1041
lemma nat_mult_distrib:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1042
  fixes z z' :: int
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1043
  assumes "0 \<le> z"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1044
  shows "nat (z * z') = nat z * nat z'"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1045
proof (cases "0 \<le> z'")
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1046
  case False
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1047
  with assms have "z * z' \<le> 0"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1048
    by (simp add: not_le mult_le_0_iff)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1049
  then have "nat (z * z') = 0" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1050
  moreover from False have "nat z' = 0" by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1051
  ultimately show ?thesis by simp
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1052
next
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1053
  case True
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1054
  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
  1055
  show ?thesis
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1056
    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
  1057
      (simp only: of_nat_mult of_nat_nat [OF True]
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1058
         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
  1059
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1060
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1061
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
  1062
  for z z' :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1063
  apply (rule trans)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1064
   apply (rule_tac [2] nat_mult_distrib)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1065
   apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1066
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1067
61944
5d06ecfdb472 prefer symbols for "abs";
wenzelm
parents: 61799
diff changeset
  1068
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
  1069
  by (cases "z = 0 \<or> w = 0")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1070
    (auto simp add: abs_if nat_mult_distrib [symmetric]
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1071
      nat_mult_distrib_neg [symmetric] mult_less_0_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1072
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1073
lemma int_in_range_abs [simp]: "int n \<in> range abs"
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1074
proof (rule range_eqI)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1075
  show "int n = \<bar>int n\<bar>" by simp
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1076
qed
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1077
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1078
lemma range_abs_Nats [simp]: "range abs = (\<nat> :: int set)"
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1079
proof -
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1080
  have "\<bar>k\<bar> \<in> \<nat>" for k :: int
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1081
    by (cases k) simp_all
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1082
  moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1083
    using that by induct simp
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1084
  ultimately show ?thesis by blast
61204
3e491e34a62e new lemmas and movement of lemmas into place
paulson
parents: 61169
diff changeset
  1085
qed
60570
7ed2cde6806d more theorems
haftmann
parents: 60162
diff changeset
  1086
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1087
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
  1088
  for z :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1089
  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
  1090
9368aa814518 move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents: 47192
diff changeset
  1091
lemma diff_nat_eq_if:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1092
  "nat z - nat z' =
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1093
    (if z' < 0 then nat z
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1094
     else
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1095
      let d = z - z'
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1096
      in if d < 0 then 0 else nat d)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1097
  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
  1098
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1099
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
  1100
  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
  1101
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1102
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1103
subsection \<open>Induction principles for int\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1104
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1105
text \<open>Well-founded segments of the integers.\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1106
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1107
definition int_ge_less_than :: "int \<Rightarrow> (int \<times> int) set"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1108
  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
  1109
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1110
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
  1111
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1112
  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
  1113
    by (auto simp add: int_ge_less_than_def)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1114
  then show ?thesis
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
  1115
    by (rule wf_subset [OF wf_measure])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1116
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1117
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1118
text \<open>
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1119
  This variant looks odd, but is typical of the relations suggested
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1120
  by RankFinder.\<close>
25919
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
definition int_ge_less_than2 :: "int \<Rightarrow> (int \<times> int) set"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1123
  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
  1124
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1125
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
  1126
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1127
  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
  1128
    by (auto simp add: int_ge_less_than2_def)
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1129
  then show ?thesis
60162
645058aa9d6f tidying some messy proofs
paulson <lp15@cam.ac.uk>
parents: 59667
diff changeset
  1130
    by (rule wf_subset [OF wf_measure])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1131
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1132
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1133
(* `set:int': dummy construction *)
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1134
theorem int_ge_induct [case_names base step, induct set: int]:
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1135
  fixes i :: int
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1136
  assumes ge: "k \<le> i"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1137
    and base: "P k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1138
    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
  1139
  shows "P i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1140
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1141
  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
  1142
  proof (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1143
    case 0
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1144
    then have "i = k" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1145
    with base show "P i" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1146
  next
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1147
    case (Suc n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1148
    then have "n = nat ((i - 1) - k)" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1149
    moreover have k: "k \<le> i - 1" using Suc.prems by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1150
    ultimately have "P (i - 1)" by (rule Suc.hyps)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1151
    from step [OF k this] show ?case by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1152
  qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1153
  with ge show ?thesis by fast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1154
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1155
25928
042e877d9841 tuned code setup
haftmann
parents: 25919
diff changeset
  1156
(* `set:int': dummy construction *)
042e877d9841 tuned code setup
haftmann
parents: 25919
diff changeset
  1157
theorem int_gr_induct [case_names base step, induct set: int]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1158
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1159
  assumes gr: "k < i"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1160
    and base: "P (k + 1)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1161
    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
  1162
  shows "P i"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1163
  apply (rule int_ge_induct[of "k + 1"])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1164
  using gr apply arith
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1165
   apply (rule base)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1166
  apply (rule step)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1167
   apply simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1168
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1169
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1170
theorem int_le_induct [consumes 1, case_names base step]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1171
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1172
  assumes le: "i \<le> k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1173
    and base: "P k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1174
    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
  1175
  shows "P i"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1176
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1177
  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
  1178
  proof (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1179
    case 0
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1180
    then have "i = k" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1181
    with base show "P i" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1182
  next
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1183
    case (Suc n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1184
    then have "n = nat (k - (i + 1))" by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1185
    moreover have k: "i + 1 \<le> k" using Suc.prems by arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1186
    ultimately have "P (i + 1)" by (rule Suc.hyps)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1187
    from step[OF k this] show ?case by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1188
  qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1189
  with le show ?thesis by fast
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1190
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1191
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1192
theorem int_less_induct [consumes 1, case_names base step]:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1193
  fixes i k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1194
  assumes less: "i < k"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1195
    and base: "P (k - 1)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1196
    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
  1197
  shows "P i"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1198
  apply (rule int_le_induct[of _ "k - 1"])
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1199
  using less apply arith
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1200
   apply (rule base)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1201
  apply (rule step)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1202
   apply simp_all
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1203
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1204
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
  1205
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
  1206
  fixes k :: int
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1207
  assumes base: "P k"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1208
    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
  1209
    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
  1210
  shows "P i"
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1211
proof -
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1212
  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
  1213
  then show ?thesis
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1214
  proof
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1215
    assume "i \<ge> k"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1216
    then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1217
      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
  1218
  next
42676
8724f20bf69c proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents: 42411
diff changeset
  1219
    assume "i \<le> k"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1220
    then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1221
      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
  1222
  qed
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1223
qed
3560de0fe851 moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents: 36749
diff changeset
  1224
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1225
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1226
subsection \<open>Intermediate value theorems\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1227
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1228
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
  1229
  for n :: nat and k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1230
  unfolding One_nat_def
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1231
  apply (induct n)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1232
   apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1233
  apply (intro strip)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1234
  apply (erule impE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1235
   apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1236
  apply (erule_tac x = n in allE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1237
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1238
  apply (case_tac "k = f (Suc n)")
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1239
   apply force
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1240
  apply (erule impE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1241
   apply (simp add: abs_if split: if_split_asm)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1242
  apply (blast intro: le_SucI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1243
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1244
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1245
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
  1246
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1247
lemma nat_intermed_int_val:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1248
  "\<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
  1249
    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
  1250
    for f :: "nat \<Rightarrow> int" and k :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1251
  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
  1252
  unfolding One_nat_def
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1253
  apply simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1254
  apply (erule exE)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1255
  apply (rule_tac x = "i+m" in exI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1256
  apply arith
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1257
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1258
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1259
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1260
subsection \<open>Products and 1, by T. M. Rasmussen\<close>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1261
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1262
lemma abs_zmult_eq_1:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1263
  fixes m n :: int
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1264
  assumes mn: "\<bar>m * n\<bar> = 1"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1265
  shows "\<bar>m\<bar> = 1"
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1266
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1267
  from mn have 0: "m \<noteq> 0" "n \<noteq> 0" by auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1268
  have "\<not> 2 \<le> \<bar>m\<bar>"
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1269
  proof
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1270
    assume "2 \<le> \<bar>m\<bar>"
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1271
    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
  1272
    also have "\<dots> = \<bar>m * n\<bar>" by (simp add: abs_mult)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1273
    also from mn have "\<dots> = 1" by simp
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1274
    finally have "2 * \<bar>n\<bar> \<le> 1" .
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1275
    with 0 show "False" by arith
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1276
  qed
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1277
  with 0 show ?thesis by auto
34055
fdf294ee08b2 streamlined proofs
paulson
parents: 33657
diff changeset
  1278
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1279
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1280
lemma pos_zmult_eq_1_iff_lemma: "m * n = 1 \<Longrightarrow> m = 1 \<or> m = - 1"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1281
  for m n :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1282
  using abs_zmult_eq_1 [of m n] by arith
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1283
35815
10e723e54076 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents: 35634
diff changeset
  1284
lemma pos_zmult_eq_1_iff:
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1285
  fixes m n :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1286
  assumes "0 < m"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1287
  shows "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
35815
10e723e54076 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents: 35634
diff changeset
  1288
proof -
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1289
  from assms have "m * n = 1 \<Longrightarrow> m = 1"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1290
    by (auto dest: pos_zmult_eq_1_iff_lemma)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1291
  then show ?thesis
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1292
    by (auto dest: pos_zmult_eq_1_iff_lemma)
35815
10e723e54076 tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents: 35634
diff changeset
  1293
qed
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1294
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1295
lemma zmult_eq_1_iff: "m * n = 1 \<longleftrightarrow> (m = 1 \<and> n = 1) \<or> (m = - 1 \<and> n = - 1)"
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1296
  for m n :: int
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1297
  apply (rule iffI)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1298
   apply (frule pos_zmult_eq_1_iff_lemma)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1299
   apply (simp add: mult.commute [of m])
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1300
   apply (frule pos_zmult_eq_1_iff_lemma)
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1301
   apply auto
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1302
  done
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1303
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1304
lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1305
proof
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1306
  assume "finite (UNIV::int set)"
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 61070
diff changeset
  1307
  moreover have "inj (\<lambda>i::int. 2 * i)"
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1308
    by (rule injI) simp
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 61070
diff changeset
  1309
  ultimately have "surj (\<lambda>i::int. 2 * i)"
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1310
    by (rule finite_UNIV_inj_surj)
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1311
  then obtain i :: int where "1 = 2 * i" by (rule surjE)
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33056
diff changeset
  1312
  then show False by (simp add: pos_zmult_eq_1_iff)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1313
qed
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1314
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff changeset
  1315
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
  1316
subsection \<open>Further theorems on numerals\<close>
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1317
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1318
subsubsection \<open>Special Simplification for Constants\<close>
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1319
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1320
text \<open>These distributive laws move literals inside sums and differences.\<close>
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1321
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 48891
diff changeset
  1322
lemmas distrib_right_numeral [simp] = distrib_right [of _ _ "numeral v"] for v
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 48891
diff changeset
  1323
lemmas distrib_left_numeral [simp] = distrib_left [of "numeral v"] for v
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1324
lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1325
lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1326
63652
804b80a80016 misc tuning and modernization;
wenzelm
parents: 63648
diff changeset
  1327
text \<open>These are actually for fields, like real: but where else to put them?\<close>
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1328
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1329
lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1330
lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1331
lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1332
lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1333
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1334
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 61738
diff changeset
  1335
text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>.  It looks
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60570
diff changeset
  1336
  strange, but then other simprocs simplify the quotient.\<close>
30652
752329615264 distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents: 30496
diff changeset
  1337
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1338
lemmas inverse_eq_divide_numeral [simp] =
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46756
diff changeset
  1339
  inverse_eq_divide [of "numeral w"] for w
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: