author  huffman 
Mon, 30 Mar 2009 12:07:59 0700  
changeset 30802  f9e9e800d27e 
parent 30796  126701134811 
child 30839  bf99ceb7d015 
permissions  rwrr 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1 
(* Title: Int.thy 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

3 
Tobias Nipkow, Florian Haftmann, TU Muenchen 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

5 

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

6 
*) 
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 
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

9 

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

10 
theory Int 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26732
diff
changeset

11 
imports Equiv_Relations Nat Wellfounded 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

13 
("Tools/numeral.ML") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

14 
("Tools/numeral_syntax.ML") 
30796  15 
"~~/src/Provers/Arith/assoc_fold.ML" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

16 
"~~/src/Provers/Arith/cancel_numerals.ML" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

17 
"~~/src/Provers/Arith/combine_numerals.ML" 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28724
diff
changeset

18 
("Tools/int_arith.ML") 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

20 

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

21 
subsection {* The equivalence relation underlying the integers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

22 

28661  23 
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where 
28562  24 
[code del]: "intrel = {((x, y), (u, v))  x y u v. x + v = u +y }" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

25 

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

26 
typedef (Integ) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

27 
int = "UNIV//intrel" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

29 

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

30 
instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

32 

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

33 
definition 
28562  34 
Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

35 

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

36 
definition 
28562  37 
One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

38 

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

39 
definition 
28562  40 
add_int_def [code del]: "z + w = Abs_Integ 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

41 
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

42 
intrel `` {(x + u, y + v)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

43 

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

44 
definition 
28562  45 
minus_int_def [code del]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

46 
" z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

47 

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

48 
definition 
28562  49 
diff_int_def [code del]: "z  w = z + (w \<Colon> int)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

50 

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

51 
definition 
28562  52 
mult_int_def [code del]: "z * w = Abs_Integ 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

53 
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

54 
intrel `` {(x*u + y*v, x*v + y*u)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

55 

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

56 
definition 
28562  57 
le_int_def [code del]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

58 
"z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

59 

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

60 
definition 
28562  61 
less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

62 

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

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

64 
zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then  i else i)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

65 

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

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

67 
zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

68 

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

69 
instance .. 
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 

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

73 

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

74 
subsection{*Construction of the Integers*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

75 

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

76 
lemma intrel_iff [simp]: "(((x,y),(u,v)) \<in> intrel) = (x+v = u+y)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

78 

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

79 
lemma equiv_intrel: "equiv UNIV intrel" 
30198  80 
by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

81 

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

82 
text{*Reduces equality of equivalence classes to the @{term intrel} relation: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

83 
@{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

84 
lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

85 

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

86 
text{*All equivalence classes belong to set of representatives*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

87 
lemma [simp]: "intrel``{(x,y)} \<in> Integ" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

88 
by (auto simp add: Integ_def intrel_def quotient_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

89 

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

90 
text{*Reduces equality on abstractions to equality on representatives: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

91 
@{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

92 
declare Abs_Integ_inject [simp,noatp] Abs_Integ_inverse [simp,noatp] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

93 

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

94 
text{*Case analysis on the representation of an integer as an equivalence 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

95 
class of pairs of naturals.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

96 
lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

97 
"(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

98 
apply (rule Abs_Integ_cases [of z]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

101 

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

102 

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

103 
subsection {* Arithmetic Operations *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

104 

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

105 
lemma minus: " Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

107 
have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

110 
by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

112 

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

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

114 
"Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

115 
Abs_Integ (intrel``{(x+u, y+v)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

117 
have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

121 
by (simp add: add_int_def UN_UN_split_split_eq 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

122 
UN_equiv_class2 [OF equiv_intrel equiv_intrel]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

124 

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

125 
text{*Congruence property for multiplication*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

127 
"(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

129 
apply (rule equiv_intrel [THEN congruent2_commuteI]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

130 
apply (force simp add: mult_ac, clarify) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

131 
apply (simp add: congruent_def mult_ac) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

132 
apply (rename_tac u v w x y z) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

133 
apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

135 
apply (simp add: add_mult_distrib [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

137 

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

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

139 
"Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

140 
Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

141 
by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

142 
UN_equiv_class2 [OF equiv_intrel equiv_intrel]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

143 

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

144 
text{*The integers form a @{text comm_ring_1}*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

148 
show "(i + j) + k = i + (j + k)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

149 
by (cases i, cases j, cases k) (simp add: add add_assoc) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

150 
show "i + j = j + i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

151 
by (cases i, cases j) (simp add: add_ac add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

152 
show "0 + i = i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

153 
by (cases i) (simp add: Zero_int_def add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

154 
show " i + i = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

155 
by (cases i) (simp add: Zero_int_def minus add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

156 
show "i  j = i +  j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

158 
show "(i * j) * k = i * (j * k)" 
29667  159 
by (cases i, cases j, cases k) (simp add: mult algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

160 
show "i * j = j * i" 
29667  161 
by (cases i, cases j) (simp add: mult algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

162 
show "1 * i = i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

163 
by (cases i) (simp add: One_int_def mult) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

164 
show "(i + j) * k = i * k + j * k" 
29667  165 
by (cases i, cases j, cases k) (simp add: add mult algebra_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

166 
show "0 \<noteq> (1::int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

169 

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

170 
lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

171 
by (induct m, simp_all add: Zero_int_def One_int_def add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

172 

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

173 

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

174 
subsection {* The @{text "\<le>"} Ordering *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

175 

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

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

177 
"(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

179 

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

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

181 
"(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

182 
by (simp add: less_int_def le order_less_le) 
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 
instance int :: linorder 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

186 
fix i j k :: int 
27682  187 
show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j" 
188 
by (cases i, cases j) (simp add: le) 

189 
show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)" 

190 
by (auto simp add: less_int_def dest: antisym) 

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

191 
show "i \<le> i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

192 
by (cases i) (simp add: le) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

193 
show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

194 
by (cases i, cases j, cases k) (simp add: le) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

195 
show "i \<le> j \<or> j \<le> i" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

196 
by (cases i, cases j) (simp add: le linorder_linear) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

198 

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

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

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

201 

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

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

203 
"(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

204 

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

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

206 
"(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

207 

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

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

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

210 
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

211 

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

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

213 

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

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

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

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

217 
show "i \<le> j \<Longrightarrow> k + i \<le> k + j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

218 
by (cases i, cases j, cases k) (simp add: le add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

220 

25961  221 

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

222 
text{*Strict Monotonicity of Multiplication*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

223 

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

224 
text{*strict, in 1st argument; proof is by induction on k>0*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

226 
"(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

227 
apply (induct "k", simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

232 

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

233 
lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

234 
apply (cases k) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

235 
apply (auto simp add: le add int_def Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

236 
apply (rule_tac x="xy" in exI, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

238 

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

239 
lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

240 
apply (cases k) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

241 
apply (simp add: less int_def Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

242 
apply (rule_tac x="xy" in exI, simp) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

244 

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

245 
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

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

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

248 
done 
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 
text{*The integers form an ordered integral domain*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

254 
show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

256 
show "\<bar>i\<bar> = (if i < 0 then i else i)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

258 
show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else  1)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

261 

25961  262 
instance int :: lordered_ring 
263 
proof 

264 
fix k :: int 

265 
show "abs k = sup k ( k)" 

266 
by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric]) 

267 
qed 

268 

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

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

270 
apply (cases w, cases z) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

271 
apply (simp add: less le add One_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

273 

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

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

275 
"(w \<Colon> int) < z \<longleftrightarrow> (\<exists>n. z = w + of_nat (Suc n))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

276 
apply (cases z, cases w) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

278 
apply (rename_tac a b c d) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

279 
apply (rule_tac x="a+d  Suc(c+b)" in exI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

282 

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

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

284 
left_distrib [of "z1::int" "z2" "w", standard] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

285 
right_distrib [of "w::int" "z1" "z2", standard] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

286 
left_diff_distrib [of "z1::int" "z2" "w", standard] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

287 
right_diff_distrib [of "w::int" "z1" "z2", standard] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

288 

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

289 

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

290 
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

291 

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

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

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

294 

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

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

296 
of_int :: "int \<Rightarrow> 'a" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

297 
where 
28562  298 
[code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i  of_nat j })" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

299 

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

300 
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i  of_nat j" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

302 
have "(\<lambda>(i,j). { of_nat i  (of_nat j :: 'a) }) respects intrel" 
29667  303 
by (simp add: congruent_def algebra_simps of_nat_add [symmetric] 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

306 
by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

308 

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

309 
lemma of_int_0 [simp]: "of_int 0 = 0" 
29667  310 
by (simp add: of_int Zero_int_def) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

311 

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

312 
lemma of_int_1 [simp]: "of_int 1 = 1" 
29667  313 
by (simp add: of_int One_int_def) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

314 

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

315 
lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" 
29667  316 
by (cases w, cases z, simp add: algebra_simps of_int add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

317 

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

318 
lemma of_int_minus [simp]: "of_int (z) =  (of_int z)" 
29667  319 
by (cases z, simp add: algebra_simps of_int minus) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

320 

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

321 
lemma of_int_diff [simp]: "of_int (w  z) = of_int w  of_int z" 
29667  322 
by (simp add: OrderedGroup.diff_minus diff_minus) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

323 

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

324 
lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

325 
apply (cases w, cases z) 
29667  326 
apply (simp add: algebra_simps of_int mult of_nat_mult) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

328 

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

329 
text{*Collapse nested embeddings*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

330 
lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" 
29667  331 
by (induct n) auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

332 

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

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

334 

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

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

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

337 

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

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

339 
"of_int w \<le> of_int z \<longleftrightarrow> w \<le> z" 
29667  340 
by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

341 

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

342 
text{*Special cases where either operand is zero*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

343 
lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

344 
lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

345 

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

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

347 
"of_int w < of_int z \<longleftrightarrow> w < z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

348 
by (simp add: not_le [symmetric] linorder_not_le [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

349 

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

350 
text{*Special cases where either operand is zero*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

351 
lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

352 
lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

353 

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

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

355 

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

356 
text{*Class for unital rings with characteristic zero. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

357 
Includes nonordered rings like the complex numbers.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

358 
class ring_char_0 = ring_1 + semiring_char_0 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

360 

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

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

362 
"of_int w = of_int z \<longleftrightarrow> w = z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

363 
apply (cases w, cases z, simp add: of_int) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

364 
apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

365 
apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

367 

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

368 
text{*Special cases where either operand is zero*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

369 
lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

370 
lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

371 

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

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

373 

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

374 
text{*Every @{text ordered_idom} has characteristic zero.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

375 
subclass (in ordered_idom) ring_char_0 by intro_locales 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

376 

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

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

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

379 
fix z show "of_int z = id z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

380 
by (cases z) (simp add: of_int add minus int_def diff_minus) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

382 

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

383 

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

384 
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

385 

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

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

387 
nat :: "int \<Rightarrow> nat" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

388 
where 
28562  389 
[code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {xy})" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

390 

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

391 
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = xy" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

393 
have "(\<lambda>(x,y). {xy}) respects intrel" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

396 
by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

398 

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

399 
lemma nat_int [simp]: "nat (of_nat n) = n" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

401 

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

402 
lemma nat_zero [simp]: "nat 0 = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

404 

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

405 
lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \<le> z then z else 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

406 
by (cases z, simp add: nat le int_def Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

407 

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

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

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

410 

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

411 
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

412 
by (cases z, simp add: nat le Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

413 

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

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

415 
apply (cases w, cases z) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

416 
apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

418 

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

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

420 
corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

421 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

422 

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

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

424 
by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

425 

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

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

427 
apply (cases w, cases z) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

428 
apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

430 

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

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

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

433 
assumes "0 \<le> z" and "\<And>m. z = of_nat m \<Longrightarrow> P" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

436 

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

437 
lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = of_nat m else m=0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

438 
by (cases w, simp add: nat le int_def Zero_int_def, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

439 

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

440 
corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = of_nat m else m=0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

441 
by (simp only: eq_commute [of m] nat_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

442 

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

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

444 
apply (cases w) 
29700  445 
apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

447 

29700  448 
lemma nat_0_iff[simp]: "nat(i::int) = 0 \<longleftrightarrow> i\<le>0" 
449 
by(simp add: nat_eq_iff) arith 

450 

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

451 
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

452 
by (auto simp add: nat_eq_iff2) 
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 zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

456 

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

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

458 
"[ (0::int) \<le> z; 0 \<le> z' ] ==> nat (z+z') = nat z + nat z'" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

459 
by (cases z, cases z', simp add: nat add le Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

460 

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

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

462 
"[ (0::int) \<le> z'; z' \<le> z ] ==> nat (zz') = nat z  nat z'" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

463 
by (cases z, cases z', 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

464 
simp add: nat add minus diff_minus le Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

465 

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

466 
lemma nat_zminus_int [simp]: "nat ( (of_nat n)) = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

467 
by (simp add: int_def minus nat Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

468 

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

469 
lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

470 
by (cases z, simp add: nat less int_def, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

471 

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

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

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

474 

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

475 
lemma of_nat_nat: "0 \<le> z \<Longrightarrow> of_nat (nat z) = of_int z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

476 
by (cases z rule: eq_Abs_Integ) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

477 
(simp add: nat le of_int Zero_int_def of_nat_diff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

478 

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

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

480 

29779  481 
text {* For termination proofs: *} 
482 
lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. 

483 

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

484 

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

485 
subsection{*Lemmas about the Function @{term of_nat} and Orderings*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

486 

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

487 
lemma negative_zless_0: " (of_nat (Suc n)) < (0 \<Colon> int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

489 

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

490 
lemma negative_zless [iff]: " (of_nat (Suc n)) < (of_nat m \<Colon> int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

492 

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

493 
lemma negative_zle_0: " of_nat n \<le> (0 \<Colon> int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

495 

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

496 
lemma negative_zle [iff]: " of_nat n \<le> (of_nat m \<Colon> int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

497 
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

498 

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

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

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

501 

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

502 
lemma int_zle_neg: "((of_nat n \<Colon> int) \<le>  of_nat m) = (n = 0 & m = 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

503 
by (simp add: int_def le minus Zero_int_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

504 

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

505 
lemma not_int_zless_negative [simp]: "~ ((of_nat n \<Colon> int) <  of_nat m)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

507 

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

508 
lemma negative_eq_positive [simp]: "(( of_nat n \<Colon> int) = of_nat m) = (n = 0 & m = 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

509 
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

510 

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

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

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

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

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

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

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

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

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

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

521 

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

522 
lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\<Colon>int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

524 

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

525 
lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\<Colon>int)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

527 

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

528 
text{*This version is proved for all ordered rings, not just integers! 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

529 
It is proved here because attribute @{text arith_split} is not available 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

530 
in theory @{text Ring_and_Field}. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

531 
But is it really better than just rewriting with @{text abs_if}?*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

532 
lemma abs_split [arith_split,noatp]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

533 
"P(abs(a::'a::ordered_idom)) = ((0 \<le> a > P a) & (a < 0 > P(a)))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

534 
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

535 

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

536 
lemma negD: "(x \<Colon> int) < 0 \<Longrightarrow> \<exists>n. x =  (of_nat (Suc n))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

537 
apply (cases x) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

538 
apply (auto simp add: le minus Zero_int_def int_def order_less_le) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

539 
apply (rule_tac x="y  Suc x" in exI, arith) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

541 

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

542 

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

543 
subsection {* Cases and induction *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

544 

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

545 
text{*Now we replace the case analysis rule by a more conventional one: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

546 
whether an integer is negative or not.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

547 

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

548 
theorem int_cases [cases type: int, case_names nonneg neg]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

549 
"[!! n. (z \<Colon> int) = of_nat n ==> P; !! n. z =  (of_nat (Suc n)) ==> P ] ==> P" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

550 
apply (cases "z < 0", blast dest!: negD) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

555 

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

556 
theorem int_induct [induct type: int, case_names nonneg neg]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

557 
"[!! n. P (of_nat n \<Colon> int); !!n. P ( (of_nat (Suc n))) ] ==> P z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

559 

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

560 
text{*Contributed by Brian Huffman*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

562 
obtains (diff) m n where "(z\<Colon>int) = of_nat m  of_nat n" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

563 
apply (cases z rule: eq_Abs_Integ) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

564 
apply (rule_tac m=x and n=y in diff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

565 
apply (simp add: int_def diff_def minus add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

567 

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

568 

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

569 
subsection {* Binary representation *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

570 

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

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

572 
This formalization defines binary arithmetic in terms of the integers 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

573 
rather than using a datatype. This avoids multiple representations (leading 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

574 
zeroes, etc.) See @{text "ZF/Tools/twoscompl.ML"}, function @{text 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

575 
int_of_binary}, for the numerical interpretation. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

576 

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

577 
The representation expects that @{text "(m mod 2)"} is 0 or 1, 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

578 
even if m is negative; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

579 
For instance, @{text "5 div 2 = 3"} and @{text "5 mod 2 = 1"}; thus 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

580 
@{text "5 = (3)*2 + 1"}. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

581 

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

582 
This two's complement binary representation derives from the paper 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

583 
"An Efficient Representation of Arithmetic for Term Rewriting" by 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

584 
Dave Cohen and Phil Watson, Rewriting Techniques and Applications, 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

585 
Springer LNCS 488 (240251), 1991. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

587 

28958  588 
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} 
589 

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

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

591 
Pls :: int where 
28562  592 
[code del]: "Pls = 0" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

593 

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

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

595 
Min :: int where 
28562  596 
[code del]: "Min =  1" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

597 

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

598 
definition 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

599 
Bit0 :: "int \<Rightarrow> int" where 
28562  600 
[code del]: "Bit0 k = k + k" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

601 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

602 
definition 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

603 
Bit1 :: "int \<Rightarrow> int" where 
28562  604 
[code del]: "Bit1 k = 1 + k + k" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

605 

29608  606 
class number =  {* for numeric types: nat, int, real, \dots *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

607 
fixes number_of :: "int \<Rightarrow> 'a" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

608 

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

609 
use "Tools/numeral.ML" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

610 

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

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

612 
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

613 

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

614 
use "Tools/numeral_syntax.ML" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

616 

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

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

618 
"Numeral0 \<equiv> number_of Pls" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

619 

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

620 
abbreviation 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

621 
"Numeral1 \<equiv> number_of (Bit1 Pls)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

622 

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

623 
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

624 
 {* Unfold all @{text let}s involving constants *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

626 

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

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

628 
succ :: "int \<Rightarrow> int" where 
28562  629 
[code del]: "succ k = k + 1" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

630 

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

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

632 
pred :: "int \<Rightarrow> int" where 
28562  633 
[code del]: "pred k = k  1" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

634 

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

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

636 
max_number_of [simp] = max_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

637 
[of "number_of u" "number_of v", standard, simp] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

639 
min_number_of [simp] = min_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

640 
[of "number_of u" "number_of v", standard, simp] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

641 
 {* unfolding @{text minx} and @{text max} on numerals *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

642 

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

643 
lemmas numeral_simps = 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

644 
succ_def pred_def Pls_def Min_def Bit0_def Bit1_def 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

645 

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

646 
text {* Removal of leading zeroes *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

647 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

648 
lemma Bit0_Pls [simp, code post]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

649 
"Bit0 Pls = Pls" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

651 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

652 
lemma Bit1_Min [simp, code post]: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

653 
"Bit1 Min = Min" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

655 

26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

656 
lemmas normalize_bin_simps = 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

657 
Bit0_Pls Bit1_Min 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

658 

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

659 

28958  660 
subsubsection {* Successor and predecessor functions *} 
661 

662 
text {* Successor *} 

663 

664 
lemma succ_Pls: 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

665 
"succ Pls = Bit1 Pls" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

667 

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

669 
"succ Min = Pls" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

671 

28958  672 
lemma succ_Bit0: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

673 
"succ (Bit0 k) = Bit1 k" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

675 

28958  676 
lemma succ_Bit1: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

677 
"succ (Bit1 k) = Bit0 (succ k)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

679 

28958  680 
lemmas succ_bin_simps [simp] = 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

681 
succ_Pls succ_Min succ_Bit0 succ_Bit1 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

682 

28958  683 
text {* Predecessor *} 
684 

685 
lemma pred_Pls: 

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

686 
"pred Pls = Min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

688 

28958  689 
lemma pred_Min: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

690 
"pred Min = Bit0 Min" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

692 

28958  693 
lemma pred_Bit0: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

694 
"pred (Bit0 k) = Bit1 (pred k)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

696 

28958  697 
lemma pred_Bit1: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

698 
"pred (Bit1 k) = Bit0 k" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

699 
unfolding numeral_simps by simp 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

700 

28958  701 
lemmas pred_bin_simps [simp] = 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

702 
pred_Pls pred_Min pred_Bit0 pred_Bit1 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

703 

28958  704 

705 
subsubsection {* Binary arithmetic *} 

706 

707 
text {* Addition *} 

708 

709 
lemma add_Pls: 

710 
"Pls + k = k" 

711 
unfolding numeral_simps by simp 

712 

713 
lemma add_Min: 

714 
"Min + k = pred k" 

715 
unfolding numeral_simps by simp 

716 

717 
lemma add_Bit0_Bit0: 

718 
"(Bit0 k) + (Bit0 l) = Bit0 (k + l)" 

719 
unfolding numeral_simps by simp 

720 

721 
lemma add_Bit0_Bit1: 

722 
"(Bit0 k) + (Bit1 l) = Bit1 (k + l)" 

723 
unfolding numeral_simps by simp 

724 

725 
lemma add_Bit1_Bit0: 

726 
"(Bit1 k) + (Bit0 l) = Bit1 (k + l)" 

727 
unfolding numeral_simps by simp 

728 

729 
lemma add_Bit1_Bit1: 

730 
"(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)" 

731 
unfolding numeral_simps by simp 

732 

733 
lemma add_Pls_right: 

734 
"k + Pls = k" 

735 
unfolding numeral_simps by simp 

736 

737 
lemma add_Min_right: 

738 
"k + Min = pred k" 

739 
unfolding numeral_simps by simp 

740 

741 
lemmas add_bin_simps [simp] = 

742 
add_Pls add_Min add_Pls_right add_Min_right 

743 
add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1 

744 

745 
text {* Negation *} 

746 

747 
lemma minus_Pls: 

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

748 
" Pls = Pls" 
28958  749 
unfolding numeral_simps by simp 
750 

751 
lemma minus_Min: 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

752 
" Min = Bit1 Pls" 
28958  753 
unfolding numeral_simps by simp 
754 

755 
lemma minus_Bit0: 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

756 
" (Bit0 k) = Bit0 ( k)" 
28958  757 
unfolding numeral_simps by simp 
758 

759 
lemma minus_Bit1: 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

760 
" (Bit1 k) = Bit1 (pred ( k))" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

761 
unfolding numeral_simps by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

762 

28958  763 
lemmas minus_bin_simps [simp] = 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

764 
minus_Pls minus_Min minus_Bit0 minus_Bit1 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

765 

28958  766 
text {* Subtraction *} 
767 

29046  768 
lemma diff_bin_simps [simp]: 
769 
"k  Pls = k" 

770 
"k  Min = succ k" 

771 
"Pls  (Bit0 l) = Bit0 (Pls  l)" 

772 
"Pls  (Bit1 l) = Bit1 (Min  l)" 

773 
"Min  (Bit0 l) = Bit1 (Min  l)" 

774 
"Min  (Bit1 l) = Bit0 (Min  l)" 

28958  775 
"(Bit0 k)  (Bit0 l) = Bit0 (k  l)" 
776 
"(Bit0 k)  (Bit1 l) = Bit1 (pred k  l)" 

777 
"(Bit1 k)  (Bit0 l) = Bit1 (k  l)" 

778 
"(Bit1 k)  (Bit1 l) = Bit0 (k  l)" 

29046  779 
unfolding numeral_simps by simp_all 
28958  780 

781 
text {* Multiplication *} 

782 

783 
lemma mult_Pls: 

784 
"Pls * w = Pls" 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

785 
unfolding numeral_simps by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

786 

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

788 
"Min * k =  k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

790 

28958  791 
lemma mult_Bit0: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

792 
"(Bit0 k) * l = Bit0 (k * l)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

793 
unfolding numeral_simps int_distrib by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

794 

28958  795 
lemma mult_Bit1: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

796 
"(Bit1 k) * l = (Bit0 (k * l)) + l" 
28958  797 
unfolding numeral_simps int_distrib by simp 
798 

799 
lemmas mult_bin_simps [simp] = 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

800 
mult_Pls mult_Min mult_Bit0 mult_Bit1 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

801 

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

802 

28958  803 
subsubsection {* Binary comparisons *} 
804 

805 
text {* Preliminaries *} 

806 

807 
lemma even_less_0_iff: 

808 
"a + a < 0 \<longleftrightarrow> a < (0::'a::ordered_idom)" 

809 
proof  

810 
have "a + a < 0 \<longleftrightarrow> (1+1)*a < 0" by (simp add: left_distrib) 

811 
also have "(1+1)*a < 0 \<longleftrightarrow> a < 0" 

812 
by (simp add: mult_less_0_iff zero_less_two 

813 
order_less_not_sym [OF zero_less_two]) 

814 
finally show ?thesis . 

815 
qed 

816 

817 
lemma le_imp_0_less: 

818 
assumes le: "0 \<le> z" 

819 
shows "(0::int) < 1 + z" 

820 
proof  

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

822 
also have "... < z + 1" by (rule less_add_one) 

823 
also have "... = 1 + z" by (simp add: add_ac) 

824 
finally show "0 < 1 + z" . 

825 
qed 

826 

827 
lemma odd_less_0_iff: 

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

829 
proof (cases z rule: int_cases) 

830 
case (nonneg n) 

831 
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing 

832 
le_imp_0_less [THEN order_less_imp_le]) 

833 
next 

834 
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

835 
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

836 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
28958  837 
qed 
838 

28985
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

839 
lemma bin_less_0_simps: 
28958  840 
"Pls < 0 \<longleftrightarrow> False" 
841 
"Min < 0 \<longleftrightarrow> True" 

842 
"Bit0 w < 0 \<longleftrightarrow> w < 0" 

843 
"Bit1 w < 0 \<longleftrightarrow> w < 0" 

844 
unfolding numeral_simps 

845 
by (simp_all add: even_less_0_iff odd_less_0_iff) 

846 

847 
lemma less_bin_lemma: "k < l \<longleftrightarrow> k  l < (0::int)" 

848 
by simp 

849 

850 
lemma le_iff_pred_less: "k \<le> l \<longleftrightarrow> pred k < l" 

851 
unfolding numeral_simps 

852 
proof 

853 
have "k  1 < k" by simp 

854 
also assume "k \<le> l" 

855 
finally show "k  1 < l" . 

856 
next 

857 
assume "k  1 < l" 

858 
hence "(k  1) + 1 \<le> l" by (rule zless_imp_add1_zle) 

859 
thus "k \<le> l" by simp 

860 
qed 

861 

862 
lemma succ_pred: "succ (pred x) = x" 

863 
unfolding numeral_simps by simp 

864 

865 
text {* Lessthan *} 

866 

867 
lemma less_bin_simps [simp]: 

868 
"Pls < Pls \<longleftrightarrow> False" 

869 
"Pls < Min \<longleftrightarrow> False" 

870 
"Pls < Bit0 k \<longleftrightarrow> Pls < k" 

871 
"Pls < Bit1 k \<longleftrightarrow> Pls \<le> k" 

872 
"Min < Pls \<longleftrightarrow> True" 

873 
"Min < Min \<longleftrightarrow> False" 

874 
"Min < Bit0 k \<longleftrightarrow> Min < k" 

875 
"Min < Bit1 k \<longleftrightarrow> Min < k" 

876 
"Bit0 k < Pls \<longleftrightarrow> k < Pls" 

877 
"Bit0 k < Min \<longleftrightarrow> k \<le> Min" 

878 
"Bit1 k < Pls \<longleftrightarrow> k < Pls" 

879 
"Bit1 k < Min \<longleftrightarrow> k < Min" 

880 
"Bit0 k < Bit0 l \<longleftrightarrow> k < l" 

881 
"Bit0 k < Bit1 l \<longleftrightarrow> k \<le> l" 

882 
"Bit1 k < Bit0 l \<longleftrightarrow> k < l" 

883 
"Bit1 k < Bit1 l \<longleftrightarrow> k < l" 

884 
unfolding le_iff_pred_less 

885 
less_bin_lemma [of Pls] 

886 
less_bin_lemma [of Min] 

887 
less_bin_lemma [of "k"] 

888 
less_bin_lemma [of "Bit0 k"] 

889 
less_bin_lemma [of "Bit1 k"] 

890 
less_bin_lemma [of "pred Pls"] 

891 
less_bin_lemma [of "pred k"] 

28985
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

892 
by (simp_all add: bin_less_0_simps succ_pred) 
28958  893 

894 
text {* Lessthanorequal *} 

895 

896 
lemma le_bin_simps [simp]: 

897 
"Pls \<le> Pls \<longleftrightarrow> True" 

898 
"Pls \<le> Min \<longleftrightarrow> False" 

899 
"Pls \<le> Bit0 k \<longleftrightarrow> Pls \<le> k" 

900 
"Pls \<le> Bit1 k \<longleftrightarrow> Pls \<le> k" 

901 
"Min \<le> Pls \<longleftrightarrow> True" 

902 
"Min \<le> Min \<longleftrightarrow> True" 

903 
"Min \<le> Bit0 k \<longleftrightarrow> Min < k" 

904 
"Min \<le> Bit1 k \<longleftrightarrow> Min \<le> k" 

905 
"Bit0 k \<le> Pls \<longleftrightarrow> k \<le> Pls" 

906 
"Bit0 k \<le> Min \<longleftrightarrow> k \<le> Min" 

907 
"Bit1 k \<le> Pls \<longleftrightarrow> k < Pls" 

908 
"Bit1 k \<le> Min \<longleftrightarrow> k \<le> Min" 

909 
"Bit0 k \<le> Bit0 l \<longleftrightarrow> k \<le> l" 

910 
"Bit0 k \<le> Bit1 l \<longleftrightarrow> k \<le> l" 

911 
"Bit1 k \<le> Bit0 l \<longleftrightarrow> k < l" 

912 
"Bit1 k \<le> Bit1 l \<longleftrightarrow> k \<le> l" 

913 
unfolding not_less [symmetric] 

914 
by (simp_all add: not_le) 

915 

916 
text {* Equality *} 

917 

918 
lemma eq_bin_simps [simp]: 

919 
"Pls = Pls \<longleftrightarrow> True" 

920 
"Pls = Min \<longleftrightarrow> False" 

921 
"Pls = Bit0 l \<longleftrightarrow> Pls = l" 

922 
"Pls = Bit1 l \<longleftrightarrow> False" 

923 
"Min = Pls \<longleftrightarrow> False" 

924 
"Min = Min \<longleftrightarrow> True" 

925 
"Min = Bit0 l \<longleftrightarrow> False" 

926 
"Min = Bit1 l \<longleftrightarrow> Min = l" 

927 
"Bit0 k = Pls \<longleftrightarrow> k = Pls" 

928 
"Bit0 k = Min \<longleftrightarrow> False" 

929 
"Bit1 k = Pls \<longleftrightarrow> False" 

930 
"Bit1 k = Min \<longleftrightarrow> k = Min" 

931 
"Bit0 k = Bit0 l \<longleftrightarrow> k = l" 

932 
"Bit0 k = Bit1 l \<longleftrightarrow> False" 

933 
"Bit1 k = Bit0 l \<longleftrightarrow> False" 

934 
"Bit1 k = Bit1 l \<longleftrightarrow> k = l" 

935 
unfolding order_eq_iff [where 'a=int] 

936 
by (simp_all add: not_less) 

937 

938 

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

939 
subsection {* Converting Numerals to Rings: @{term number_of} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

940 

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

941 
class number_ring = number + comm_ring_1 + 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

942 
assumes number_of_eq: "number_of k = of_int k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

943 

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

944 
text {* selfembedding of the integers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

945 

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

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

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

948 

28724  949 
definition int_number_of_def [code del]: 
950 
"number_of w = (of_int w \<Colon> int)" 

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

951 

28724  952 
instance proof 
953 
qed (simp only: int_number_of_def) 

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

954 

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

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

956 

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

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

958 
"number_of (k::int) = k" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

960 

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

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

962 
"number_of (succ k) = (1 + number_of k ::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

963 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

964 

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

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

966 
"number_of (pred w) = ( 1 + number_of w ::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

967 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

968 

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

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

970 
"number_of (uminus w) = ( (number_of w)::'a::number_ring)" 
28958  971 
unfolding number_of_eq by (rule of_int_minus) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

972 

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

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

974 
"number_of (v + w) = (number_of v + number_of w::'a::number_ring)" 
28958  975 
unfolding number_of_eq by (rule of_int_add) 
976 

977 
lemma number_of_diff: 

978 
"number_of (v  w) = (number_of v  number_of w::'a::number_ring)" 

979 
unfolding number_of_eq by (rule of_int_diff) 

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

980 

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

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

982 
"number_of (v * w) = (number_of v * number_of w::'a::number_ring)" 
28958  983 
unfolding number_of_eq by (rule of_int_mult) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

984 

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

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

986 
The correctness of shifting. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

987 
But it doesn't seem to give a measurable speedup. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

989 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

990 
lemma double_number_of_Bit0: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

991 
"(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

992 
unfolding number_of_eq numeral_simps left_distrib by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

993 

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

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

995 
Converting numerals 0 and 1 to their abstract versions. 
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 

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

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

999 
"Numeral0 = (0::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1000 
unfolding number_of_eq numeral_simps by simp 
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 
lemma numeral_1_eq_1 [simp]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1003 
"Numeral1 = (1::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1004 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1005 

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

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

1007 
Specialcase simplification for small constants. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1009 

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

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

1011 
Unary minus for the abstract constant 1. Cannot be inserted 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1012 
as a simprule until later: it is @{text number_of_Min} reoriented! 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1014 

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

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

1016 
"(1::'a::number_ring) =  1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1017 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1018 

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

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

1020 
"1 * z = (z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1021 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1022 

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

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

1024 
"z * 1 = (z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1025 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1026 

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

1027 
(*Negation of a coefficient*) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1029 
" (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1031 

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

1032 
text {* Subtraction *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1033 

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

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

1035 
"number_of v  number_of w = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1036 
(number_of (v + uminus w)::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1038 

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

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

1040 
"number_of Pls = (0::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1041 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1042 

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

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

1044 
"number_of Min = ( 1::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1045 
unfolding number_of_eq numeral_simps by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1046 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1047 
lemma number_of_Bit0: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1048 
"number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1049 
unfolding number_of_eq numeral_simps by simp 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1050 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1051 
lemma number_of_Bit1: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1052 
"number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1053 
unfolding number_of_eq numeral_simps by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1054 

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

1055 

28958  1056 
subsubsection {* Equality of Binary Numbers *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1057 

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

1058 
text {* First version by Norbert Voelker *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1059 

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

1060 
definition (*for simplifying equalities*) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1061 
iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1063 
"iszero z \<longleftrightarrow> z = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1064 

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

1065 
lemma iszero_0: "iszero 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1067 

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

1068 
lemma not_iszero_1: "~ iszero 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1070 

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

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

1072 
"((number_of x::'a::number_ring) = number_of y) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1073 
iszero (number_of (x + uminus y) :: 'a)" 
29667  1074 
unfolding iszero_def number_of_add number_of_minus 
1075 
by (simp add: algebra_simps) 

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

1076 

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

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

1078 
"iszero ((number_of Pls)::'a::number_ring)" 
29667  1079 
unfolding iszero_def numeral_0_eq_0 .. 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1080 

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

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

1082 
"~ iszero ((number_of Min)::'a::number_ring)" 
29667  1083 
unfolding iszero_def numeral_m1_eq_minus_1 by simp 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1084 

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

1085 

28958  1086 
subsubsection {* Comparisons, for Ordered Rings *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1087 

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

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

1089 

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

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

1091 
"1 + z + z \<noteq> (0::int)"; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

1095 
thus ?thesis using le_imp_0_less [OF le] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

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

1102 
have "(0::int) < 1 + (of_nat n + of_nat n)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1104 
also have "... =  (1 + z + z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1105 
by (simp add: neg add_assoc [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

1111 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1112 
lemma iszero_number_of_Bit0: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1113 
"iszero (number_of (Bit0 w)::'a) = 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1114 
iszero (number_of w::'a::{ring_char_0,number_ring})" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1116 
have "(of_int w + of_int w = (0::'a)) \<Longrightarrow> (w = 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1118 
assume eq: "of_int w + of_int w = (0::'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1119 
then have "of_int (w + w) = (of_int 0 :: 'a)" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1120 
then have "w + w = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1121 
then show "w = 0" by (simp only: double_eq_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1122 
qed 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1123 
thus ?thesis 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1124 
by (auto simp add: iszero_def number_of_eq numeral_simps) 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1125 
qed 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1126 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1127 
lemma iszero_number_of_Bit1: 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1128 
"~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1129 
proof  
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1130 
have "1 + of_int w + of_int w \<noteq> (0::'a)" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1132 
assume eq: "1 + of_int w + of_int w = (0::'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

1136 
qed 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1137 
thus ?thesis 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1138 
by (auto simp add: iszero_def number_of_eq numeral_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1140 

28985
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1141 
lemmas iszero_simps = 
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1142 
iszero_0 not_iszero_1 
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1143 
iszero_number_of_Pls nonzero_number_of_Min 
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1144 
iszero_number_of_Bit0 iszero_number_of_Bit1 
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1145 
(* iszero_number_of_Pls would never normally be used 
af325cd29b15
add named lemma lists: neg_simps and iszero_simps
huffman
parents:
28984
diff
changeset

1146 
because its lhs simplifies to "iszero 0" *) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1147 

28958  1148 
subsubsection {* The LessThan Relation *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1149 

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

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

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

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

1153 
have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1155 
by (simp add: mult_less_0_iff zero_less_two 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1156 
order_less_not_sym [OF zero_less_two]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1159 

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

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

1161 
"(1 + z + z < 0) = (z < (0::int))"; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1164 
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1165 
le_imp_0_less [THEN order_less_imp_le]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1167 
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

1168 
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

1169 
add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1171 

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

1172 
text {* LessThan or Equals *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1173 

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

1174 
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1175 

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

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

1177 
linorder_not_less [of "number_of w" "number_of v", symmetric, 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1179 

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 
text {* Absolute value (@{term abs}) *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1182 

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

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

1184 
"abs(number_of x::'a::{ordered_idom,number_ring}) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1185 
(if number_of x < (0::'a) then number_of x else number_of x)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1187 

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

1188 

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

1189 
text {* Reorientation of the equation nnn=x *} 
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 number_of_reorient: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1192 
"(number_of w = x) = (x = number_of w)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1194 

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

1195 

28958  1196 
subsubsection {* Simplification of arithmetic operations on integer constants. *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1197 

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

1198 
lemmas arith_extra_simps [standard, simp] = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1199 
number_of_add [symmetric] 
28958  1200 
number_of_minus [symmetric] 
1201 
numeral_m1_eq_minus_1 [symmetric] 

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

1202 
number_of_mult [symmetric] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1204 

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

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

1206 
For making a minimal simpset, one must include these default simprules. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1207 
Also include @{text simp_thms}. 
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 

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

1210 
lemmas arith_simps = 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

1211 
normalize_bin_simps pred_bin_simps succ_bin_simps 
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

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

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

1214 

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

1215 
text {* Simplification of relational operations *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1216 

28962
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1217 
lemma less_number_of [simp]: 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1218 
"(number_of x::'a::{ordered_idom,number_ring}) < number_of y \<longleftrightarrow> x < y" 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1219 
unfolding number_of_eq by (rule of_int_less_iff) 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1220 

f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1221 
lemma le_number_of [simp]: 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1222 
"(number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y \<longleftrightarrow> x \<le> y" 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1223 
unfolding number_of_eq by (rule of_int_le_iff) 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1224 

28967
3bdb1eae352c
enable eq_bin_simps for simplifying equalities on numerals
huffman
parents:
28962
diff
changeset

1225 
lemma eq_number_of [simp]: 
3bdb1eae352c
enable eq_bin_simps for simplifying equalities on numerals
huffman
parents:
28962
diff
changeset

1226 
"(number_of x::'a::{ring_char_0,number_ring}) = number_of y \<longleftrightarrow> x = y" 
3bdb1eae352c
enable eq_bin_simps for simplifying equalities on numerals
huffman
parents:
28962
diff
changeset

1227 
unfolding number_of_eq by (rule of_int_eq_iff) 
3bdb1eae352c
enable eq_bin_simps for simplifying equalities on numerals
huffman
parents:
28962
diff
changeset

1228 

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

1229 
lemmas rel_simps [simp] = 
28962
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1230 
less_number_of less_bin_simps 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1231 
le_number_of le_bin_simps 
28988
13d6f120992b
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
huffman
parents:
28985
diff
changeset

1232 
eq_number_of_eq eq_bin_simps 
29039  1233 
iszero_simps 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1234 

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

1235 

28958  1236 
subsubsection {* Simplification of arithmetic when nested to the right. *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1237 

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

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

1239 
"number_of v + (number_of w + z) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1240 
(number_of(v + w) + z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1241 
by (simp add: add_assoc [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1242 

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

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

1244 
"number_of v * (number_of w * z) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1245 
(number_of(v * w) * z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1246 
by (simp add: mult_assoc [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1247 

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

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

1249 
"number_of v + (number_of w  c) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1250 
number_of(v + w)  (c::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1252 

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

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

1254 
"number_of v + (c  number_of w) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1255 
number_of (v + uminus w) + (c::'a::number_ring)" 
29667  1256 
by (simp add: algebra_simps diff_number_of_eq [symmetric]) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1257 

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

1258 

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

1259 

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

1260 

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

1261 
subsection {* The Set of Integers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1262 

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

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

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

1265 

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

1266 
definition Ints :: "'a set" where 
28562  1267 
[code del]: "Ints = range of_int" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1268 

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

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

1270 

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

1271 
notation (xsymbols) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1272 
Ints ("\<int>") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1273 

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

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

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

1276 

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

1277 
lemma Ints_0 [simp]: "0 \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

1282 

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

1283 
lemma Ints_1 [simp]: "1 \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

1288 

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

1289 
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

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

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

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

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

1294 

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

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

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

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

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

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

1300 

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

1301 
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

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

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

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

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

1306 

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

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

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

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

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

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

1312 
from `q \<in> \<int>` have "q \<in> range of_int" unfolding Ints_def . 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

1316 

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

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

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

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

1320 

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

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

1322 

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

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

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

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

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

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

1328 

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

1329 
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1330 

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

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

1332 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1335 
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

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

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

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

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

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

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

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

1343 
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

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

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

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

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

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

1349 

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

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

1351 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1354 
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

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

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

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

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

1359 
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

1360 
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

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

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

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

1364 

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

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

1366 
"(number_of w :: 'a::number_ring) \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1367 
unfolding number_of_eq Ints_def by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1368 

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

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

1370 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1373 
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

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

1375 
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

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

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

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

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

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

1381 

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

1382 

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

1383 
subsection {* @{term setsum} and @{term setprod} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1384 

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

1385 
text {*By Jeremy Avigad*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1386 

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

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

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

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

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

1391 

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

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

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

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

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

1396 

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

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

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

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

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

1401 

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

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

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

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

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

1406 

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

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

1408 
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1410 

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

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

1412 
"finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1414 

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

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

1416 
"finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1418 

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

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

1420 
"finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1422 

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

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

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

1425 

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

1426 

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

1427 
subsection{*Inequality Reasoning for the Arithmetic Simproc*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1428 

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

1429 
lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1431 

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

1432 
lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1434 

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

1435 
lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1437 

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

1438 
lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1440 

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

1441 
lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1443 

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

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

1445 
"inverse Numeral1 = (Numeral1::'a::{number_ring,field})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1447 

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

1448 
text{*Theorem lists for the cancellation simprocs. The use of binary numerals 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1449 
for 0 and 1 reduces the number of special cases.*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1450 

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