author  eberlm 
Mon, 11 Jan 2016 16:38:39 +0100  
changeset 62128  3201ddb00097 
parent 61944  5d06ecfdb472 
child 62347  2230b7047376 
permissions  rwrr 
41959  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  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  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 
55404
5cb95b79a51f
transformed 'option' and 'list' into newstyle datatypes (but register them as oldstyle as well)
blanchet
parents:
55096
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  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 

48045  14 
definition intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" where 
15 
"intrel = (\<lambda>(x, y) (u, v). x + v = u + y)" 

16 

17 
lemma intrel_iff [simp]: "intrel (x, y) (u, v) \<longleftrightarrow> x + v = u + y" 

18 
by (simp add: intrel_def) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

19 

48045  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  22 
proof (rule equivpI) 
23 
show "reflp intrel" 

24 
unfolding reflp_def by auto 

25 
show "symp intrel" 

26 
unfolding symp_def by auto 

27 
show "transp intrel" 

28 
unfolding transp_def by auto 

29 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

30 

48045  31 
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 
32 
"(!!x y. z = Abs_Integ (x, y) ==> P) ==> P" 

33 
by (induct z) auto 

34 

60758  35 
subsection \<open>Integers form a commutative ring\<close> 
48045  36 

37 
instantiation int :: comm_ring_1 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

38 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

39 

51994  40 
lift_definition zero_int :: "int" is "(0, 0)" . 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

41 

51994  42 
lift_definition one_int :: "int" is "(1, 0)" . 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

43 

48045  44 
lift_definition plus_int :: "int \<Rightarrow> int \<Rightarrow> int" 
45 
is "\<lambda>(x, y) (u, v). (x + u, y + v)" 

46 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

47 

48045  48 
lift_definition uminus_int :: "int \<Rightarrow> int" 
49 
is "\<lambda>(x, y). (y, x)" 

50 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

51 

48045  52 
lift_definition minus_int :: "int \<Rightarrow> int \<Rightarrow> int" 
53 
is "\<lambda>(x, y) (u, v). (x + v, y + u)" 

54 
by clarsimp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

55 

48045  56 
lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int" 
57 
is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)" 

58 
proof (clarsimp) 

59 
fix s t u v w x y z :: nat 

60 
assume "s + v = u + t" and "w + z = y + x" 

61 
hence "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) 

62 
= (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)" 

63 
by simp 

64 
thus "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)" 

65 
by (simp add: algebra_simps) 

66 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

67 

48045  68 
instance 
61169  69 
by standard (transfer, clarsimp simp: algebra_simps)+ 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

70 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

71 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

72 

44709  73 
abbreviation int :: "nat \<Rightarrow> int" where 
74 
"int \<equiv> of_nat" 

75 

48045  76 
lemma int_def: "int n = Abs_Integ (n, 0)" 
77 
by (induct n, simp add: zero_int.abs_eq, 

78 
simp add: one_int.abs_eq plus_int.abs_eq) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

79 

48045  80 
lemma int_transfer [transfer_rule]: 
56525  81 
"(rel_fun (op =) pcr_int) (\<lambda>n. (n, 0)) int" 
82 
unfolding rel_fun_def int.pcr_cr_eq cr_int_def int_def by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

83 

48045  84 
lemma int_diff_cases: 
85 
obtains (diff) m n where "z = int m  int n" 

86 
by transfer clarsimp 

87 

60758  88 
subsection \<open>Integers are totally ordered\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

89 

48045  90 
instantiation int :: linorder 
91 
begin 

92 

93 
lift_definition less_eq_int :: "int \<Rightarrow> int \<Rightarrow> bool" 

94 
is "\<lambda>(x, y) (u, v). x + v \<le> u + y" 

95 
by auto 

96 

97 
lift_definition less_int :: "int \<Rightarrow> int \<Rightarrow> bool" 

98 
is "\<lambda>(x, y) (u, v). x + v < u + y" 

99 
by auto 

100 

101 
instance 

61169  102 
by standard (transfer, force)+ 
48045  103 

104 
end 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

105 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

106 
instantiation int :: distrib_lattice 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

107 
begin 
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 
definition 
61076  110 
"(inf :: int \<Rightarrow> int \<Rightarrow> int) = min" 
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 
definition 
61076  113 
"(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

114 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

115 
instance 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

116 
by intro_classes 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54489
diff
changeset

117 
(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

118 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

119 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

120 

60758  121 
subsection \<open>Ordering properties of arithmetic operations\<close> 
48045  122 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34055
diff
changeset

123 
instance int :: ordered_cancel_ab_semigroup_add 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

124 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

125 
fix i j k :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

126 
show "i \<le> j \<Longrightarrow> k + i \<le> k + j" 
48045  127 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

128 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

129 

60758  130 
text\<open>Strict Monotonicity of Multiplication\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

131 

60758  132 
text\<open>strict, in 1st argument; proof is by induction on k>0\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

133 
lemma zmult_zless_mono2_lemma: 
44709  134 
"(i::int)<j ==> 0<k ==> int k * i < int k * j" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

135 
apply (induct k) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

136 
apply simp 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

137 
apply (simp add: distrib_right) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

138 
apply (case_tac "k=0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

139 
apply (simp_all add: add_strict_mono) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

140 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

141 

44709  142 
lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = int n" 
48045  143 
apply transfer 
144 
apply clarsimp 

145 
apply (rule_tac x="a  b" in exI, simp) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

146 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

147 

44709  148 
lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = int n" 
48045  149 
apply transfer 
150 
apply clarsimp 

151 
apply (rule_tac x="a  b" in exI, simp) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

152 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

153 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

154 
lemma zmult_zless_mono2: "[ i<j; (0::int) < k ] ==> k*i < k*j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

155 
apply (drule zero_less_imp_eq_int) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

156 
apply (auto simp add: zmult_zless_mono2_lemma) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

157 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

158 

60758  159 
text\<open>The integers form an ordered integral domain\<close> 
48045  160 
instantiation int :: linordered_idom 
161 
begin 

162 

163 
definition 

61076  164 
zabs_def: "\<bar>i::int\<bar> = (if i < 0 then  i else i)" 
48045  165 

166 
definition 

61076  167 
zsgn_def: "sgn (i::int) = (if i=0 then 0 else if 0<i then 1 else  1)" 
48045  168 

169 
instance 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  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  179 
end 
180 

61076  181 
lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1::int) \<le> z" 
48045  182 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

183 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

184 
lemma zless_iff_Suc_zadd: 
61076  185 
"(w :: int) < z \<longleftrightarrow> (\<exists>n. z = w + int (Suc n))" 
48045  186 
apply transfer 
187 
apply auto 

188 
apply (rename_tac a b c d) 

189 
apply (rule_tac x="c+b  Suc(a+d)" in exI) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

190 
apply arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

191 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

192 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

193 
lemmas int_distrib = 
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

194 
distrib_right [of z1 z2 w] 
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

195 
distrib_left [of w z1 z2] 
45607  196 
left_diff_distrib [of z1 z2 w] 
197 
right_diff_distrib [of w z1 z2] 

198 
for z1 z2 w :: int 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

199 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

200 

61799  201 
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

202 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

203 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

204 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

205 

48045  206 
lift_definition of_int :: "int \<Rightarrow> 'a" is "\<lambda>(i, j). of_nat i  of_nat j" 
207 
by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq 

208 
of_nat_add [symmetric] simp del: of_nat_add) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

209 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

210 
lemma of_int_0 [simp]: "of_int 0 = 0" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

211 
by transfer simp 
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 
lemma of_int_1 [simp]: "of_int 1 = 1" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

214 
by transfer simp 
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 
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. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

217 
by transfer (clarsimp simp add: algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

218 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

219 
lemma of_int_minus [simp]: "of_int (z) =  (of_int z)" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

220 
by (transfer fixing: uminus) clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

221 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

222 
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

223 
using of_int_add [of w " z"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

224 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

225 
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

226 
by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

227 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61524
diff
changeset

228 
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

229 
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

230 

60758  231 
text\<open>Collapse nested embeddings\<close> 
44709  232 
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" 
29667  233 
by (induct n) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

234 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

235 
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

236 
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

237 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

238 
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

239 
by simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

240 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

241 
lemma of_int_power [simp]: 
31015  242 
"of_int (z ^ n) = of_int z ^ n" 
243 
by (induct n) simp_all 

244 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

245 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

246 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

247 
context ring_char_0 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

248 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

249 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

250 
lemma of_int_eq_iff [simp]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

251 
"of_int w = of_int z \<longleftrightarrow> w = z" 
48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

252 
by transfer (clarsimp simp add: algebra_simps 
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

253 
of_nat_add [symmetric] simp del: of_nat_add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

254 

60758  255 
text\<open>Special cases where either operand is zero\<close> 
36424  256 
lemma of_int_eq_0_iff [simp]: 
257 
"of_int z = 0 \<longleftrightarrow> z = 0" 

258 
using of_int_eq_iff [of z 0] by simp 

259 

260 
lemma of_int_0_eq_iff [simp]: 

261 
"0 = of_int z \<longleftrightarrow> z = 0" 

262 
using of_int_eq_iff [of 0 z] by simp 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

263 

61234  264 
lemma of_int_eq_1_iff [iff]: 
265 
"of_int z = 1 \<longleftrightarrow> z = 1" 

266 
using of_int_eq_iff [of z 1] by simp 

267 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

268 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

269 

36424  270 
context linordered_idom 
271 
begin 

272 

61799  273 
text\<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close> 
36424  274 
subclass ring_char_0 .. 
275 

276 
lemma of_int_le_iff [simp]: 

277 
"of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" 

48066
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

278 
by (transfer fixing: less_eq) (clarsimp simp add: algebra_simps 
c6783c9b87bf
transfer method now handles transfer rules for compound terms, e.g. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

279 
of_nat_add [symmetric] simp del: of_nat_add) 
36424  280 

281 
lemma of_int_less_iff [simp]: 

282 
"of_int w < of_int z \<longleftrightarrow> w < z" 

283 
by (simp add: less_le order_less_le) 

284 

285 
lemma of_int_0_le_iff [simp]: 

286 
"0 \<le> of_int z \<longleftrightarrow> 0 \<le> z" 

287 
using of_int_le_iff [of 0 z] by simp 

288 

289 
lemma of_int_le_0_iff [simp]: 

290 
"of_int z \<le> 0 \<longleftrightarrow> z \<le> 0" 

291 
using of_int_le_iff [of z 0] by simp 

292 

293 
lemma of_int_0_less_iff [simp]: 

294 
"0 < of_int z \<longleftrightarrow> 0 < z" 

295 
using of_int_less_iff [of 0 z] by simp 

296 

297 
lemma of_int_less_0_iff [simp]: 

298 
"of_int z < 0 \<longleftrightarrow> z < 0" 

299 
using of_int_less_iff [of z 0] by simp 

300 

61234  301 
lemma of_int_1_le_iff [simp]: 
302 
"1 \<le> of_int z \<longleftrightarrow> 1 \<le> z" 

303 
using of_int_le_iff [of 1 z] by simp 

304 

305 
lemma of_int_le_1_iff [simp]: 

306 
"of_int z \<le> 1 \<longleftrightarrow> z \<le> 1" 

307 
using of_int_le_iff [of z 1] by simp 

308 

309 
lemma of_int_1_less_iff [simp]: 

310 
"1 < of_int z \<longleftrightarrow> 1 < z" 

311 
using of_int_less_iff [of 1 z] by simp 

312 

313 
lemma of_int_less_1_iff [simp]: 

314 
"of_int z < 1 \<longleftrightarrow> z < 1" 

315 
using of_int_less_iff [of z 1] by simp 

316 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

317 
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

318 
by simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

319 

3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

320 
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

321 
by simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
61944
diff
changeset

322 

36424  323 
end 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

324 

61234  325 
text \<open>Comparisons involving @{term of_int}.\<close> 
326 

327 
lemma of_int_eq_numeral_iff [iff]: 

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

328 
"of_int z = (numeral n :: 'a::ring_char_0) 
61234  329 
\<longleftrightarrow> z = numeral n" 
330 
using of_int_eq_iff by fastforce 

331 

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

332 
lemma of_int_le_numeral_iff [simp]: 
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

333 
"of_int z \<le> (numeral n :: 'a::linordered_idom) 
61234  334 
\<longleftrightarrow> z \<le> numeral n" 
335 
using of_int_le_iff [of z "numeral n"] by simp 

336 

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

337 
lemma of_int_numeral_le_iff [simp]: 
61234  338 
"(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z" 
339 
using of_int_le_iff [of "numeral n"] by simp 

340 

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

341 
lemma of_int_less_numeral_iff [simp]: 
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

342 
"of_int z < (numeral n :: 'a::linordered_idom) 
61234  343 
\<longleftrightarrow> z < numeral n" 
344 
using of_int_less_iff [of z "numeral n"] by simp 

345 

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

346 
lemma of_int_numeral_less_iff [simp]: 
61234  347 
"(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z" 
348 
using of_int_less_iff [of "numeral n" z] by simp 

349 

56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56525
diff
changeset

350 
lemma of_nat_less_of_int_iff: 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56525
diff
changeset

351 
"(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x" 
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56525
diff
changeset

352 
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

353 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

354 
lemma of_int_eq_id [simp]: "of_int = id" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

355 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

356 
fix z show "of_int z = id z" 
48045  357 
by (cases z rule: int_diff_cases, simp) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

358 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

359 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

360 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

361 
instance int :: no_top 
61169  362 
apply standard 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

363 
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

364 
apply simp 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

365 
done 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

366 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

367 
instance int :: no_bot 
61169  368 
apply standard 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

369 
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

370 
apply simp 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

371 
done 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51185
diff
changeset

372 

61799  373 
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

374 

48045  375 
lift_definition nat :: "int \<Rightarrow> nat" is "\<lambda>(x, y). x  y" 
376 
by auto 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

377 

44709  378 
lemma nat_int [simp]: "nat (int n) = n" 
48045  379 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

380 

44709  381 
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)" 
48045  382 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

383 

44709  384 
corollary nat_0_le: "0 \<le> z ==> int (nat z) = z" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

385 
by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

386 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

387 
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" 
48045  388 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

389 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

390 
lemma nat_le_eq_zle: "0 < w  0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)" 
48045  391 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

392 

60758  393 
text\<open>An alternative condition is @{term "0 \<le> w"}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

394 
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" 
60162  395 
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

396 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

397 
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)" 
60162  398 
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

399 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

400 
lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)" 
48045  401 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

402 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

403 
lemma nonneg_eq_int: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

404 
fixes z :: int 
44709  405 
assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

406 
shows P 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

407 
using assms by (blast dest: nat_0_le sym) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

408 

54223  409 
lemma nat_eq_iff: 
410 
"nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 

48045  411 
by transfer (clarsimp simp add: le_imp_diff_is_add) 
60162  412 

54223  413 
corollary nat_eq_iff2: 
414 
"m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)" 

415 
using nat_eq_iff [of w m] by auto 

416 

417 
lemma nat_0 [simp]: 

418 
"nat 0 = 0" 

419 
by (simp add: nat_eq_iff) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

420 

54223  421 
lemma nat_1 [simp]: 
422 
"nat 1 = Suc 0" 

423 
by (simp add: nat_eq_iff) 

424 

425 
lemma nat_numeral [simp]: 

426 
"nat (numeral k) = numeral k" 

427 
by (simp add: nat_eq_iff) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

428 

54223  429 
lemma nat_neg_numeral [simp]: 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

430 
"nat ( numeral k) = 0" 
54223  431 
by simp 
432 

433 
lemma nat_2: "nat 2 = Suc (Suc 0)" 

434 
by simp 

60162  435 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

436 
lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)" 
48045  437 
by transfer (clarsimp, arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

438 

44709  439 
lemma nat_le_iff: "nat x \<le> n \<longleftrightarrow> x \<le> int n" 
48045  440 
by transfer (clarsimp simp add: le_diff_conv) 
44707  441 

442 
lemma nat_mono: "x \<le> y \<Longrightarrow> nat x \<le> nat y" 

48045  443 
by transfer auto 
44707  444 

29700  445 
lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0" 
48045  446 
by transfer clarsimp 
29700  447 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

448 
lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \<le> z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

449 
by (auto simp add: nat_eq_iff2) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

450 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

451 
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

452 
by (insert zless_nat_conj [of 0], auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

453 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

454 
lemma nat_add_distrib: 
54223  455 
"0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'" 
48045  456 
by transfer clarsimp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

457 

54223  458 
lemma nat_diff_distrib': 
459 
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x  y) = nat x  nat y" 

460 
by transfer clarsimp 

60162  461 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

462 
lemma nat_diff_distrib: 
54223  463 
"0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z  z') = nat z  nat z'" 
464 
by (rule nat_diff_distrib') auto 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

465 

44709  466 
lemma nat_zminus_int [simp]: "nat ( int n) = 0" 
48045  467 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

468 

53065  469 
lemma le_nat_iff: 
470 
"k \<ge> 0 \<Longrightarrow> n \<le> nat k \<longleftrightarrow> int n \<le> k" 

471 
by transfer auto 

60162  472 

44709  473 
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" 
48045  474 
by transfer (clarsimp simp add: less_diff_conv) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

475 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

476 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

477 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

478 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61552
diff
changeset

479 
lemma 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. localedefined constants with hidden parameters
huffman
parents:
48045
diff
changeset

480 
by transfer (clarsimp simp add: of_nat_diff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

481 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

482 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

483 

60162  484 
lemma diff_nat_numeral [simp]: 
54249  485 
"(numeral v :: nat)  numeral v' = nat (numeral v  numeral v')" 
486 
by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral) 

487 

488 

60758  489 
text \<open>For termination proofs:\<close> 
29779  490 
lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. 
491 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

492 

60758  493 
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

494 

61076  495 
lemma negative_zless_0: " (int (Suc n)) < (0 :: int)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

496 
by (simp add: order_less_le del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

497 

44709  498 
lemma negative_zless [iff]: " (int (Suc n)) < int m" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

499 
by (rule negative_zless_0 [THEN order_less_le_trans], simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

500 

44709  501 
lemma negative_zle_0: " int n \<le> 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

502 
by (simp add: minus_le_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

503 

44709  504 
lemma negative_zle [iff]: " int n \<le> int m" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

505 
by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

506 

44709  507 
lemma not_zle_0_negative [simp]: "~ (0 \<le>  (int (Suc n)))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

508 
by (subst le_minus_iff, simp del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

509 

44709  510 
lemma int_zle_neg: "(int n \<le>  int m) = (n = 0 & m = 0)" 
48045  511 
by transfer simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

512 

44709  513 
lemma not_int_zless_negative [simp]: "~ (int n <  int m)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

514 
by (simp add: linorder_not_less) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

515 

44709  516 
lemma negative_eq_positive [simp]: "( int n = of_nat m) = (n = 0 & m = 0)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

517 
by (force simp add: order_eq_iff [of " of_nat n"] int_zle_neg) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

518 

44709  519 
lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

520 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

521 
have "(w \<le> z) = (0 \<le> z  w)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

522 
by (simp only: le_diff_eq add_0_left) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

523 
also have "\<dots> = (\<exists>n. z  w = of_nat n)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

524 
by (auto elim: zero_le_imp_eq_int) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

525 
also have "\<dots> = (\<exists>n. z = w + of_nat n)" 
29667  526 
by (simp only: algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

527 
finally show ?thesis . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

528 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

529 

44709  530 
lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

531 
by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

532 

60758  533 
text\<open>This version is proved for all ordered rings, not just integers! 
61799  534 
It is proved here because attribute \<open>arith_split\<close> is not available 
535 
in theory \<open>Rings\<close>. 

536 
But is it really better than just rewriting with \<open>abs_if\<close>?\<close> 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53652
diff
changeset

537 
lemma abs_split [arith_split, no_atp]: 
61944  538 
"P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a > P a) & (a < 0 > P(a)))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

539 
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

540 

44709  541 
lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x =  (int (Suc n))" 
48045  542 
apply transfer 
543 
apply clarsimp 

544 
apply (rule_tac x="b  Suc a" in exI, arith) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

545 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

546 

60758  547 
subsection \<open>Cases and induction\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

548 

60758  549 
text\<open>Now we replace the case analysis rule by a more conventional one: 
550 
whether an integer is negative or not.\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

551 

60758  552 
text\<open>This version is symmetric in the two subgoals.\<close> 
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

553 
theorem int_cases2 [case_names nonneg nonpos, cases type: int]: 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

554 
"\<lbrakk>!! n. z = int n \<Longrightarrow> P; !! n. z =  (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

555 
apply (cases "z < 0") 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

556 
apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym]) 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

557 
done 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

558 

60758  559 
text\<open>This is the default, with a negative case.\<close> 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

560 
theorem int_cases [case_names nonneg neg, cases type: int]: 
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59582
diff
changeset

561 
"[!! n. z = int n ==> P; !! n. z =  (int (Suc n)) ==> P ] ==> P" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

562 
apply (cases "z < 0") 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

563 
apply (blast dest!: negD) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

564 
apply (simp add: linorder_not_less del: of_nat_Suc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

565 
apply auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

566 
apply (blast dest: nat_0_le [THEN sym]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

567 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

568 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

569 
lemma int_cases3 [case_names zero pos neg]: 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

570 
fixes k :: int 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

571 
assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
61204  572 
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

573 
shows "P" 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

574 
proof (cases k "0::int" rule: linorder_cases) 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

575 
case equal with assms(1) show P by simp 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

576 
next 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

577 
case greater 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

578 
then have "nat k > 0" by simp 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

579 
moreover from this have "k = int (nat k)" by auto 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

580 
ultimately show P using assms(2) by blast 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

581 
next 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

582 
case less 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

583 
then have "nat ( k) > 0" by simp 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

584 
moreover from this have "k =  int (nat ( k))" by auto 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

585 
ultimately show P using assms(3) by blast 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

586 
qed 
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60758
diff
changeset

587 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

588 
theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: 
44709  589 
"[!! n. P (int n); !!n. P ( (int (Suc n))) ] ==> P z" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

590 
by (cases z) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

591 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

592 
lemma nonneg_int_cases: 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

593 
assumes "0 \<le> k" obtains n where "k = int n" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

594 
using assms by (rule nonneg_eq_int) 
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

595 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

596 
lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" 
61799  597 
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> 
598 
by (fact Let_numeral) \<comment> \<open>FIXME drop\<close> 

37767  599 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

600 
lemma Let_neg_numeral [simp]: "Let ( numeral v) f = f ( numeral v)" 
61799  601 
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> 
602 
by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

603 

61799  604 
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close> 
28958  605 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

606 
lemmas max_number_of [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

607 
max_def [of "numeral u" "numeral v"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

608 
max_def [of "numeral u" " numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

609 
max_def [of " numeral u" "numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

610 
max_def [of " numeral u" " numeral v"] for u v 
28958  611 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

612 
lemmas min_number_of [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

613 
min_def [of "numeral u" "numeral v"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

614 
min_def [of "numeral u" " numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

615 
min_def [of " numeral u" "numeral v"] 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

616 
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

617 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

618 

60758  619 
subsubsection \<open>Binary comparisons\<close> 
28958  620 

60758  621 
text \<open>Preliminaries\<close> 
28958  622 

60162  623 
lemma le_imp_0_less: 
28958  624 
assumes le: "0 \<le> z" 
625 
shows "(0::int) < 1 + z" 

626 
proof  

627 
have "0 \<le> z" by fact 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

628 
also have "... < z + 1" by (rule less_add_one) 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

629 
also have "... = 1 + z" by (simp add: ac_simps) 
28958  630 
finally show "0 < 1 + z" . 
631 
qed 

632 

633 
lemma odd_less_0_iff: 

634 
"(1 + z + z < 0) = (z < (0::int))" 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

635 
proof (cases z) 
28958  636 
case (nonneg n) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56889
diff
changeset

637 
thus ?thesis by (simp add: linorder_not_less add.assoc add_increasing 
60162  638 
le_imp_0_less [THEN order_less_imp_le]) 
28958  639 
next 
640 
case (neg n) 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

641 
thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

642 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
28958  643 
qed 
644 

60758  645 
subsubsection \<open>Comparisons, for Ordered Rings\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

646 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

647 
lemmas double_eq_0_iff = double_zero 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

648 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

649 
lemma odd_nonzero: 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

650 
"1 + z + z \<noteq> (0::int)" 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

651 
proof (cases z) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

652 
case (nonneg n) 
60162  653 
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

654 
thus ?thesis using le_imp_0_less [OF le] 
60162  655 
by (auto simp add: add.assoc) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

656 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

657 
case (neg n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

658 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

659 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

660 
assume eq: "1 + z + z = 0" 
44709  661 
have "(0::int) < 1 + (int n + int n)" 
60162  662 
by (simp add: le_imp_0_less add_increasing) 
663 
also have "... =  (1 + z + z)" 

664 
by (simp add: neg add.assoc [symmetric]) 

665 
also have "... = 0" by (simp add: eq) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

666 
finally have "0<0" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

667 
thus False by blast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

668 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

669 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

670 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

671 

60758  672 
subsection \<open>The Set of Integers\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

673 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

674 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

675 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

676 

61070  677 
definition Ints :: "'a set" ("\<int>") 
678 
where "\<int> = range of_int" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

679 

35634  680 
lemma Ints_of_int [simp]: "of_int z \<in> \<int>" 
681 
by (simp add: Ints_def) 

682 

683 
lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>" 

45533  684 
using Ints_of_int [of "of_nat n"] by simp 
35634  685 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

686 
lemma Ints_0 [simp]: "0 \<in> \<int>" 
45533  687 
using Ints_of_int [of "0"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

688 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

689 
lemma Ints_1 [simp]: "1 \<in> \<int>" 
45533  690 
using Ints_of_int [of "1"] by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

691 

61552
980dd46a03fb
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
eberlm
parents:
61531
diff
changeset

692 
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

693 
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

694 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

695 
lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

696 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

697 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

698 
apply (rule of_int_add [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

699 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

700 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

701 
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> a \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

702 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

703 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

704 
apply (rule of_int_minus [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

705 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

706 

35634  707 
lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a  b \<in> \<int>" 
708 
apply (auto simp add: Ints_def) 

709 
apply (rule range_eqI) 

710 
apply (rule of_int_diff [symmetric]) 

711 
done 

712 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

713 
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

714 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

715 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

716 
apply (rule of_int_mult [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

717 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

718 

35634  719 
lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>" 
720 
by (induct n) simp_all 

721 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

722 
lemma Ints_cases [cases set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

723 
assumes "q \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

724 
obtains (of_int) z where "q = of_int z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

725 
unfolding Ints_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

726 
proof  
60758  727 
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

728 
then obtain z where "q = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

729 
then show thesis .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

730 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

731 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

732 
lemma Ints_induct [case_names of_int, induct set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

733 
"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

734 
by (rule Ints_cases) auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

735 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

736 
lemma Nats_subset_Ints: "\<nat> \<subseteq> \<int>" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

737 
unfolding Nats_def Ints_def 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

738 
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

739 

f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

740 
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

741 
proof (intro subsetI equalityI) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

742 
fix x :: 'a assume "x \<in> {of_int n n. n \<ge> 0}" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

743 
then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

744 
hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

745 
thus "x \<in> \<nat>" by simp 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

746 
next 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

747 
fix x :: 'a assume "x \<in> \<nat>" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

748 
then obtain n where "x = of_nat n" by (auto elim!: Nats_cases) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

749 
hence "x = of_int (int n)" by simp 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

750 
also have "int n \<ge> 0" by simp 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

751 
hence "of_int (int n) \<in> {of_int n n. n \<ge> 0}" by blast 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

752 
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

753 
qed 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

754 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

755 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

756 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

757 
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

758 
proof (intro subsetI equalityI) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

759 
fix x :: 'a assume "x \<in> {n \<in> \<int>. n \<ge> 0}" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

760 
then obtain n where "x = of_int n" "n \<ge> 0" by (auto elim!: Ints_cases) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

761 
hence "x = of_nat (nat n)" by (subst of_nat_nat) simp_all 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

762 
thus "x \<in> \<nat>" by simp 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

763 
qed (auto elim!: Nats_cases) 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

764 

f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61234
diff
changeset

765 

60758  766 
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

767 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

768 
lemma Ints_double_eq_0_iff: 
61070  769 
assumes in_Ints: "a \<in> \<int>" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

770 
shows "(a + a = 0) = (a = (0::'a::ring_char_0))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

771 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

772 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

773 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

774 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

775 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

776 
assume "a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

777 
thus "a + a = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

778 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

779 
assume eq: "a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

780 
hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

781 
hence "z + z = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

782 
hence "z = 0" by (simp only: double_eq_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

783 
thus "a = 0" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

784 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

785 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

786 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

787 
lemma Ints_odd_nonzero: 
61070  788 
assumes in_Ints: "a \<in> \<int>" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

789 
shows "1 + a + a \<noteq> (0::'a::ring_char_0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

790 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

791 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

792 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

793 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

794 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

795 
assume eq: "1 + a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

796 
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

797 
hence "1 + z + z = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

798 
with odd_nonzero show False by blast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

799 
qed 
60162  800 
qed 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

801 

61070  802 
lemma Nats_numeral [simp]: "numeral w \<in> \<nat>" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

803 
using of_nat_in_Nats [of "numeral w"] by simp 
35634  804 

60162  805 
lemma Ints_odd_less_0: 
61070  806 
assumes in_Ints: "a \<in> \<int>" 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34055
diff
changeset

807 
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

808 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

809 
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

810 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

811 
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

812 
by (simp add: a) 
45532
74b17a0881b3
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead
huffman
parents:
45219
diff
changeset

813 
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

814 
also have "... = (a < 0)" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

815 
finally show ?thesis . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

816 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

817 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

818 

60758  819 
subsection \<open>@{term setsum} and @{term setprod}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

820 

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

821 
lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

822 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

823 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

824 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

825 

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

826 
lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

827 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

828 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

829 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

830 

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

831 
lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

832 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

833 
apply (erule finite_induct, auto simp add: of_nat_mult) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

834 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

835 

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

836 
lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

837 
apply (cases "finite A") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

838 
apply (erule finite_induct, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

839 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

840 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

841 
lemmas int_setsum = of_nat_setsum [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

842 
lemmas int_setprod = of_nat_setprod [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

843 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

844 

60758  845 
text \<open>Legacy theorems\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

846 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

847 
lemmas zle_int = of_nat_le_iff [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

848 
lemmas int_int_eq = of_nat_eq_iff [where 'a=int] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

849 

60758  850 
subsection \<open>Setting up simplification procedures\<close> 
30802  851 

54249  852 
lemmas of_int_simps = 
853 
of_int_0 of_int_1 of_int_add of_int_mult 

854 

48891  855 
ML_file "Tools/int_arith.ML" 
60758  856 
declaration \<open>K Int_Arith.setup\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

857 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

858 
simproc_setup fast_arith ("(m::'a::linordered_idom) < n"  
61144  859 
"(m::'a::linordered_idom) \<le> n"  
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

860 
"(m::'a::linordered_idom) = n") = 
61144  861 
\<open>K Lin_Arith.simproc\<close> 
43595  862 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

863 

60758  864 
subsection\<open>More Inequality Reasoning\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

865 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

866 
lemma zless_add1_eq: "(w < z + (1::int)) = (w<z  w=z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

867 
by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

868 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

869 
lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

870 
by arith 
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 zle_diff1_eq [simp]: "(w \<le> z  (1::int)) = (w<z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

873 
by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

874 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

875 
lemma zle_add1_eq_le [simp]: "(w < z + (1::int)) = (w\<le>z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

876 
by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

877 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

878 
lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

879 
by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

880 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

881 

60758  882 
subsection\<open>The functions @{term nat} and @{term int}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

883 

60758  884 
text\<open>Simplify the term @{term "w +  z"}\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

885 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

886 
lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" 
60162  887 
using zless_nat_conj [of 1 z] by auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

888 

60758  889 
text\<open>This simplifies expressions of the form @{term "int n = z"} where 
890 
z is an integer literal.\<close> 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

891 
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

892 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

893 
lemma split_nat [arith_split]: 
44709  894 
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

895 
(is "?P = (?L & ?R)") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

896 
proof (cases "i < 0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

897 
case True thus ?thesis by auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

898 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

899 
case False 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

900 
have "?P = ?L" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

901 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

902 
assume ?P thus ?L using False by clarsimp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

903 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

904 
assume ?L thus ?P using False by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

905 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

906 
with False show ?thesis by simp 
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 

59000  909 
lemma nat_abs_int_diff: "nat \<bar>int a  int b\<bar> = (if a \<le> b then b  a else a  b)" 
910 
by auto 

911 

912 
lemma nat_int_add: "nat (int a + int b) = a + b" 

913 
by auto 

914 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

915 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

916 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

917 

33056
791a4655cae3
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents:
32437
diff
changeset

918 
lemma of_int_of_nat [nitpick_simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

919 
"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

920 
proof (cases "k < 0") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

921 
case True then have "0 \<le>  k" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

922 
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

923 
with True show ?thesis by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

924 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

925 
case False then show ?thesis by (simp add: not_less of_nat_nat) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

926 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

927 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

928 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

929 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

930 
lemma nat_mult_distrib: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

931 
fixes z z' :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

932 
assumes "0 \<le> z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

933 
shows "nat (z * z') = nat z * nat z'" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

934 
proof (cases "0 \<le> z'") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

935 
case False with assms have "z * z' \<le> 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

936 
by (simp add: not_le mult_le_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

937 
then have "nat (z * z') = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

938 
moreover from False have "nat z' = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

939 
ultimately show ?thesis by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

940 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

941 
case True with assms have ge_0: "z * z' \<ge> 0" by (simp add: zero_le_mult_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

942 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

943 
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

944 
(simp only: of_nat_mult of_nat_nat [OF True] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

945 
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

946 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

947 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

948 
lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(z) * nat(z')" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

949 
apply (rule trans) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

950 
apply (rule_tac [2] nat_mult_distrib, auto) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

951 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

952 

61944  953 
lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

954 
apply (cases "z=0  w=0") 
60162  955 
apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

956 
nat_mult_distrib_neg [symmetric] mult_less_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

957 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

958 

60570  959 
lemma int_in_range_abs [simp]: 
960 
"int n \<in> range abs" 

961 
proof (rule range_eqI) 

962 
show "int n = \<bar>int n\<bar>" 

963 
by simp 

964 
qed 

965 

966 
lemma range_abs_Nats [simp]: 

967 
"range abs = (\<nat> :: int set)" 

968 
proof  

969 
have "\<bar>k\<bar> \<in> \<nat>" for k :: int 

970 
by (cases k) simp_all 

971 
moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int 

972 
using that by induct simp 

973 
ultimately show ?thesis by blast 

61204  974 
qed 
60570  975 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

976 
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

977 
apply (rule sym) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

978 
apply (simp add: nat_eq_iff) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

979 
done 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

980 

9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

981 
lemma diff_nat_eq_if: 
60162  982 
"nat z  nat z' = 
983 
(if z' < 0 then nat z 

984 
else let d = zz' in 

47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

985 
if d < 0 then 0 else nat d)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

986 
by (simp add: Let_def nat_diff_distrib [symmetric]) 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

987 

9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

988 
lemma nat_numeral_diff_1 [simp]: 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

989 
"numeral v  (1::nat) = nat (numeral v  1)" 
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset

990 
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

991 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

992 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

993 
subsection "Induction principles for int" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

994 

60758  995 
text\<open>Wellfounded segments of the integers\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

996 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

997 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

998 
int_ge_less_than :: "int => (int * int) set" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

999 
where 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1000 
"int_ge_less_than d = {(z',z). d \<le> z' & z' < z}" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1001 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1002 
theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1003 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1004 
have "int_ge_less_than d \<subseteq> measure (%z. nat (zd))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1005 
by (auto simp add: int_ge_less_than_def) 
60162  1006 
thus ?thesis 
1007 
by (rule wf_subset [OF wf_measure]) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1008 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1009 

60758  1010 
text\<open>This variant looks odd, but is typical of the relations suggested 
1011 
by RankFinder.\<close> 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1012 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1013 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1014 
int_ge_less_than2 :: "int => (int * int) set" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1015 
where 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1016 
"int_ge_less_than2 d = {(z',z). d \<le> z & z' < z}" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1017 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1018 
theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1019 
proof  
60162  1020 
have "int_ge_less_than2 d \<subseteq> measure (%z. nat (1+zd))" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1021 
by (auto simp add: int_ge_less_than2_def) 
60162  1022 
thus ?thesis 
1023 
by (rule wf_subset [OF wf_measure]) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1024 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1025 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1026 
(* `set:int': dummy construction *) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1027 
theorem int_ge_induct [case_names base step, induct set: int]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1028 
fixes i :: int 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1029 
assumes ge: "k \<le> i" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1030 
base: "P k" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1031 
step: "\<And>i. k \<le> i \<Longrightarrow> P i \<Longrightarrow> P (i + 1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1032 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1033 
proof  
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1034 
{ fix n 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1035 
have "\<And>i::int. n = nat (i  k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1036 
proof (induct n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1037 
case 0 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1038 
hence "i = k" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1039 
thus "P i" using base by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1040 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1041 
case (Suc n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1042 
then have "n = nat((i  1)  k)" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1043 
moreover 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1044 
have ki1: "k \<le> i  1" using Suc.prems by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1045 
ultimately 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1046 
have "P (i  1)" by (rule Suc.hyps) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1047 
from step [OF ki1 this] show ?case by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1048 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1049 
} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1050 
with ge show ?thesis by fast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1051 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1052 

25928  1053 
(* `set:int': dummy construction *) 
1054 
theorem int_gr_induct [case_names base step, induct set: int]: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1055 
assumes gr: "k < (i::int)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1056 
base: "P(k+1)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1057 
step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1058 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1059 
apply(rule int_ge_induct[of "k + 1"]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1060 
using gr apply arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1061 
apply(rule base) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1062 
apply (rule step, simp+) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1063 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1064 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1065 
theorem int_le_induct [consumes 1, case_names base step]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1066 
assumes le: "i \<le> (k::int)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1067 
base: "P(k)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1068 
step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1069 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1070 
proof  
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1071 
{ fix n 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1072 
have "\<And>i::int. n = nat(ki) \<Longrightarrow> i \<le> k \<Longrightarrow> P i" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1073 
proof (induct n) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1074 
case 0 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1075 
hence "i = k" by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1076 
thus "P i" using base by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1077 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1078 
case (Suc n) 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1079 
hence "n = nat (k  (i + 1))" by arith 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1080 
moreover 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1081 
have ki1: "i + 1 \<le> k" using Suc.prems by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1082 
ultimately 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1083 
have "P (i + 1)" by(rule Suc.hyps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1084 
from step[OF ki1 this] show ?case by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1085 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1086 
} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1087 
with le show ?thesis by fast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1088 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1089 

42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1090 
theorem int_less_induct [consumes 1, case_names base step]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1091 
assumes less: "(i::int) < k" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1092 
base: "P(k  1)" and 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1093 
step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1094 
shows "P i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1095 
apply(rule int_le_induct[of _ "k  1"]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1096 
using less apply arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1097 
apply(rule base) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1098 
apply (rule step, simp+) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1099 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1100 

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

1101 
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

1102 
fixes k :: int 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1103 
assumes base: "P k" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1104 
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

1105 
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

1106 
shows "P i" 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1107 
proof  
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1108 
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

1109 
then show ?thesis 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1110 
proof 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1111 
assume "i \<ge> k" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1112 
then show ?thesis using base 
36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1113 
by (rule int_ge_induct) (fact step1) 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1114 
next 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1115 
assume "i \<le> k" 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1116 
then show ?thesis using base 
36801
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1117 
by (rule int_le_induct) (fact step2) 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1118 
qed 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1119 
qed 
3560de0fe851
moved int induction lemma to theory Int as int_bidirectional_induct
haftmann
parents:
36749
diff
changeset

1120 

60758  1121 
subsection\<open>Intermediate value theorems\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1122 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1123 
lemma int_val_lemma: 
61944  1124 
"(\<forall>i<n::nat. \<bar>f(i+1)  f i\<bar> \<le> 1) > 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1125 
f 0 \<le> k > k \<le> f n > (\<exists>i \<le> n. f i = (k::int))" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

1126 
unfolding One_nat_def 
42676
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1127 
apply (induct n) 
8724f20bf69c
proper case_names for int_cases, int_of_nat_induct;
wenzelm
parents:
42411
diff
changeset

1128 
apply simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1129 
apply (intro strip) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1130 
apply (erule impE, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1131 
apply (erule_tac x = n in allE, simp) 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

1132 
apply (case_tac "k = f (Suc n)") 
27106  1133 
apply force 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1134 
apply (erule impE) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1135 
apply (simp add: abs_if split add: split_if_asm) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1136 
apply (blast intro: le_SucI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1137 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1138 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1139 
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

1140 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1141 
lemma nat_intermed_int_val: 
61944  1142 
"[ \<forall>i. m \<le> i & i < n > \<bar>f(i + 1::nat)  f i\<bar> \<le> 1; m < n; 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1143 
f m \<le> k; k \<le> f n ] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)" 
60162  1144 
apply (cut_tac n = "nm" and f = "%i. f (i+m) " and k = k 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1145 
in int_val_lemma) 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30000
diff
changeset

1146 
unfolding One_nat_def 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1147 
apply simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1148 
apply (erule exE) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1149 
apply (rule_tac x = "i+m" in exI, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1150 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1151 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1152 

60758  1153 
subsection\<open>Products and 1, by T. M. Rasmussen\<close> 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1154 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1155 
lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1156 
by arith 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1157 

34055  1158 
lemma abs_zmult_eq_1: 
1159 
assumes mn: "\<bar>m * n\<bar> = 1" 

1160 
shows "\<bar>m\<bar> = (1::int)" 

1161 
proof  

1162 
have 0: "m \<noteq> 0 & n \<noteq> 0" using mn 

1163 
by auto 

1164 
have "~ (2 \<le> \<bar>m\<bar>)" 

1165 
proof 

1166 
assume "2 \<le> \<bar>m\<bar>" 

1167 
hence "2*\<bar>n\<bar> \<le> \<bar>m\<bar>*\<bar>n\<bar>" 

60162  1168 
by (simp add: mult_mono 0) 
1169 
also have "... = \<bar>m*n\<bar>" 

34055  1170 
by (simp add: abs_mult) 
1171 
also have "... = 1" 

1172 
by (simp add: mn) 

1173 
finally have "2*\<bar>n\<bar> \<le> 1" . 

1174 
thus "False" using 0 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1175 
by arith 
34055  1176 
qed 
1177 
thus ?thesis using 0 

1178 
by auto 

1179 
qed 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1180 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1181 
lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int)  m = 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1182 
by (insert abs_zmult_eq_1 [of m n], arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1183 

35815
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1184 
lemma pos_zmult_eq_1_iff: 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1185 
assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1186 
proof  
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1187 
from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1188 
thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) 
10e723e54076
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
boehmes
parents:
35634
diff
changeset

1189 
qed 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1190 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1191 
lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1)  (m = 1 & n = 1))" 
60162  1192 
apply (rule iffI) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1193 
apply (frule pos_zmult_eq_1_iff_lemma) 
60162  1194 
apply (simp add: mult.commute [of m]) 
1195 
apply (frule pos_zmult_eq_1_iff_lemma, auto) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1196 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1197 

33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1198 
lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1199 
proof 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1200 
assume "finite (UNIV::int set)" 
61076  1201 
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

1202 
by (rule injI) simp 
61076  1203 
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

1204 
by (rule finite_UNIV_inj_surj) 
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33056
diff
changeset

1205 
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

1206 
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

1207 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1208 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1209 

60758  1210 
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

1211 

60758  1212 
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

1213 

60758  1214 
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

1215 

49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
48891
diff
changeset

1216 
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

1217 
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

1218 
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

1219 
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

1220 

60758  1221 
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

1222 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1223 
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

1224 
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

1225 
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

1226 
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

1227 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1228 

61799  1229 
text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>. It looks 
60758  1230 
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

1231 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1232 
lemmas inverse_eq_divide_numeral [simp] = 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1233 
inverse_eq_divide [of "numeral w"] for w 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1234 

2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1235 
lemmas inverse_eq_divide_neg_numeral [simp] = 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1236 
inverse_eq_divide [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

1237 

60758  1238 
text \<open>These laws simplify inequalities, moving unary minus from a term 
1239 
into the literal.\<close> 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1240 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1241 
lemmas equation_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1242 
equation_minus_iff [of "numeral v"] for v 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1243 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1244 
lemmas minus_equation_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1245 
minus_equation_iff [of _ "numeral v"] for v 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1246 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1247 
lemmas le_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1248 
le_minus_iff [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

1249 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1250 
lemmas minus_le_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1251 
minus_le_iff [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

1252 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1253 
lemmas less_minus_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1254 
less_minus_iff [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

1255 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1256 
lemmas minus_less_iff_numeral [no_atp] = 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1257 
minus_less_iff [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

1258 

61799  1259 
\<comment> \<open>FIXME maybe simproc\<close> 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1260 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1261 

61799  1262 
text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close> 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1263 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1264 
lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1265 
lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1266 
lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1267 
lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [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

1268 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1269 

61799  1270 
text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close> 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1271 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1272 
named_theorems divide_const_simps "simplification rules to simplify comparisons involving constant divisors" 
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1273 

c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1274 
lemmas le_divide_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1275 
pos_le_divide_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1276 
neg_le_divide_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1277 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1278 
lemmas divide_le_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1279 
pos_divide_le_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1280 
neg_divide_le_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1281 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1282 
lemmas less_divide_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1283 
pos_less_divide_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1284 
neg_less_divide_eq [of " numeral w", OF neg_numeral_less_zero] for w 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1285 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1286 
lemmas divide_less_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1287 
pos_divide_less_eq [of "numeral w", OF zero_less_numeral] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1288 
neg_divide_less_eq [of " numeral w", OF neg_numeral_less_zero] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1289 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1290 
lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1291 
eq_divide_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1292 
eq_divide_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1293 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1294 
lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1295 
divide_eq_eq [of _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1296 
divide_eq_eq [of _ " numeral w"] for w 
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1297 

30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1298 

60758  1299 
subsubsection\<open>Optional Simplification Rules Involving Constants\<close> 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1300 

60758  1301 
text\<open>Simplify quotients that are compared with a literal constant.\<close> 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1302 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1303 
lemmas le_divide_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1304 
le_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1305 
le_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1306 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1307 
lemmas divide_le_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1308 
divide_le_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1309 
divide_le_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1310 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1311 
lemmas less_divide_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1312 
less_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1313 
less_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1314 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1315 
lemmas divide_less_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1316 
divide_less_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1317 
divide_less_eq [of _ _ " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1318 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1319 
lemmas eq_divide_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1320 
eq_divide_eq [of "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1321 
eq_divide_eq [of " numeral w"] for w 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1322 

61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1323 
lemmas divide_eq_eq_numeral [divide_const_simps] = 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46756
diff
changeset

1324 
divide_eq_eq [of _ _ "numeral w"] 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54249
diff
changeset

1325 
divide_eq_eq [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

1326 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1327 

60758  1328 
text\<open>Not good as automatic simprules because they cause case splits.\<close> 
61738
c4f6031f1310
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
paulson <lp15@cam.ac.uk>
parents:
61694
diff
changeset

1329 
lemmas [divide_const_simps] = le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 
30652
752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1330 

752329615264
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
haftmann
parents:
30496
diff
changeset

1331 

60758  1332 
subsection \<open>The divides relation\<close> 
33320  1333 

33657  1334 
lemma zdvd_antisym_nonneg: 
1335 
"0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" 

33320  1336 
apply (simp add: dvd_def, auto) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56889
diff
changeset

1337 
apply (auto simp add: mult.assoc zero_le_mult_iff zmult_eq_1_iff) 
33320  1338 
done 
1339 

60162  1340 
lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
33320  1341 
shows "\<bar>a\<bar> = \<bar>b\<bar>" 
33657  1342 
proof cases 
1343 
assume "a = 0" with assms show ?thesis by simp 

1344 
next 

1345 
assume "a \<noteq> 0" 

60758  1346 
from \<open>a dvd b\<close> obtain k where k:"b = a*k" unfolding dvd_def by blast 
1347 
from \<open>b dvd a\<close> obtain k' where k':"a = b*k'" unfolding dvd_def by blast 

33320  1348 
from k k' have "a = a*k*k'" by simp 
1349 
with mult_cancel_left1[where c="a" and b="k*k'"] 
