author  huffman 
Wed, 03 Dec 2008 20:45:42 0800  
changeset 28962  f603183f7a5c 
parent 28958  74c60b78969c 
child 28967  3bdb1eae352c 
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 
ID: $Id$ 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

5 
Copyright 1994 University of Cambridge 
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 

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

9 
header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

10 

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

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

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

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

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

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

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

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

18 
"~~/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

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

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

21 

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

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

23 

28661  24 
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where 
28562  25 
[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

26 

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

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

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

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

30 

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

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

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

33 

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

34 
definition 
28562  35 
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

36 

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

37 
definition 
28562  38 
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

39 

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

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

42 
(\<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

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

44 

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

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

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

48 

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

49 
definition 
28562  50 
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

51 

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

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

54 
(\<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

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

56 

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

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

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

60 

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

61 
definition 
28562  62 
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

63 

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

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

65 
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

66 

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

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

68 
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

69 

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

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

71 

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

72 
end 
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 

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

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

76 

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

77 
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

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

79 

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

80 
lemma equiv_intrel: "equiv UNIV intrel" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

81 
by (simp add: intrel_def equiv_def refl_def sym_def trans_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

82 

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

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

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

85 
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

86 

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

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

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

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

90 

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

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

92 
@{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

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

94 

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

95 
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

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

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

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

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

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

101 
done 
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 

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

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

105 

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

106 
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

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

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

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

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

111 
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

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

113 

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

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

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

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

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

118 
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

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

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

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

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

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

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

125 

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

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

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

128 
"(%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

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

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

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

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

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

134 
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

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

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

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

138 

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

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

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

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

142 
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

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

144 

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

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

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

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

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

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

150 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

170 

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

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

172 
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

173 

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

174 

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

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

176 

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

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

178 
"(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

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

180 

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

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

182 
"(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

183 
by (simp add: less_int_def le order_less_le) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

184 

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

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

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

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

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

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

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

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

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

194 
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

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

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

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

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

199 

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

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

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

202 

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

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

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

205 

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

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

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

208 

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

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

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

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

212 

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

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

214 

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

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

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

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

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

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

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

221 

25961  222 

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

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

224 

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

225 
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

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

227 
"(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

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

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

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

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

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

233 

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

234 
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

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

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

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

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

239 

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

240 
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

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

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

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

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

245 

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

246 
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

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

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

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

250 

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

251 
text{*The integers form an ordered integral domain*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

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

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

259 
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

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

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

262 

25961  263 
instance int :: lordered_ring 
264 
proof 

265 
fix k :: int 

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

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

268 
qed 

269 

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

270 
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

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

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

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

274 

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

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

276 
"(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

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

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

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

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

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

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

283 

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

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

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

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

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

288 
right_diff_distrib [of "w::int" "z1" "z2", standard] 
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 

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

291 
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

292 

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

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

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

295 

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

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

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

298 
where 
28562  299 
[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

300 

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

301 
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

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

303 
have "(\<lambda>(i,j). { of_nat i  (of_nat j :: 'a) }) respects intrel" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

304 
by (simp add: congruent_def compare_rls of_nat_add [symmetric] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

307 
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

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

309 

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

310 
lemma of_int_0 [simp]: "of_int 0 = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

312 

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

313 
lemma of_int_1 [simp]: "of_int 1 = 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

315 

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

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

317 
by (cases w, cases z, simp add: compare_rls of_int OrderedGroup.compare_rls add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

318 

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

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

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

321 

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

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

323 
by (simp add: OrderedGroup.diff_minus diff_minus) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

324 

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

325 
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

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

327 
apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

328 
mult add_ac of_nat_mult) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

330 

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

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

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

333 
by (induct n) auto 
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 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

336 

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

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

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

339 

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

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

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

342 
by (cases w, cases z, simp add: of_int le minus compare_rls of_nat_add [symmetric] del: of_nat_add) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

343 

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

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

345 
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

346 
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

347 

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

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

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

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

351 

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

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

353 
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

354 
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

355 

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

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

357 

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

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

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

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

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

362 

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

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

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

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

366 
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

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

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

369 

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

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

371 
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

372 
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

373 

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

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

375 

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

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

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

378 

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

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

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

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

382 
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

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

384 

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 
subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

387 

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

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

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

390 
where 
28562  391 
[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

392 

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

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

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

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

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

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

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

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

400 

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

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

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

403 

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

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

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

406 

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

407 
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

408 
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

409 

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

410 
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

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

412 

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

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

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

415 

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

416 
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

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

418 
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

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

420 

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

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

422 
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

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

424 

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

425 
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

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

427 

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

428 
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

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

430 
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

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

432 

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

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

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

435 
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

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

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

438 

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

439 
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

440 
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

441 

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

442 
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

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

444 

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

445 
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

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

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

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

449 

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

450 
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

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

452 

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

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

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

455 

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

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

457 
"[ (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

458 
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

459 

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

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

461 
"[ (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

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

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

464 

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

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

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

467 

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

468 
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

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

470 

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

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

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

473 

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

474 
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

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

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

477 

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

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

479 

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

480 

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

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

482 

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

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

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

485 

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

486 
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

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

488 

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

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

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

491 

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

492 
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

493 
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

494 

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

495 
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

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

497 

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

498 
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

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

500 

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

501 
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

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

503 

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

504 
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

505 
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

506 

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

507 
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

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

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

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

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

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

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

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

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

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

517 

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

518 
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

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

520 

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

521 
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

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

523 

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

524 
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

525 
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

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

527 
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

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

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

530 
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

531 

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

532 
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

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

534 
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

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

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

537 

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

538 

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

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

540 

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

541 
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

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

543 

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

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

545 
"[!! 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

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

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

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

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

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

551 

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

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

553 
"[!! 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

554 
by (cases z rule: int_cases) auto 
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 
text{*Contributed by Brian Huffman*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

558 
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

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

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

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

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

563 

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

564 

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

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

566 

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

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

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

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

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

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

572 

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

573 
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

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

575 
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

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

577 

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

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

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

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

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

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

583 

28958  584 
subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} 
585 

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

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

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

589 

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 
Min :: int where 
28562  592 
[code del]: "Min =  1" 
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 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

595 
Bit0 :: "int \<Rightarrow> int" where 
28562  596 
[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

597 

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

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

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

601 

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

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

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

604 

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

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

606 

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

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

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

609 

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

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

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

612 

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

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

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

615 

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

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

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

618 

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

619 
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

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

621 
unfolding Let_def .. 
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 
definition 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

624 
succ :: "int \<Rightarrow> int" where 
28562  625 
[code del]: "succ k = k + 1" 
25919
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 
pred :: "int \<Rightarrow> int" where 
28562  629 
[code del]: "pred 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 
lemmas 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

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

638 

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

639 
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

640 
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

641 

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

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

643 

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

644 
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

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

646 
unfolding numeral_simps by simp 
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 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

649 
"Bit1 Min = Min" 
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 

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

652 
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

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

654 

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

655 

28958  656 
subsubsection {* Successor and predecessor functions *} 
657 

658 
text {* Successor *} 

659 

660 
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

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

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

663 

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

665 
"succ Min = Pls" 
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_Bit0: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

669 
"succ (Bit0 k) = Bit1 k" 
25919
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_Bit1: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

673 
"succ (Bit1 k) = Bit0 (succ 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 
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

677 
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

678 

28958  679 
text {* Predecessor *} 
680 

681 
lemma pred_Pls: 

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

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

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

684 

28958  685 
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

686 
"pred Min = Bit0 Min" 
25919
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_Bit0: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

690 
"pred (Bit0 k) = Bit1 (pred k)" 
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_Bit1: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

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

695 
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

696 

28958  697 
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

698 
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

699 

28958  700 

701 
subsubsection {* Binary arithmetic *} 

702 

703 
text {* Addition *} 

704 

705 
lemma add_Pls: 

706 
"Pls + k = k" 

707 
unfolding numeral_simps by simp 

708 

709 
lemma add_Min: 

710 
"Min + k = pred k" 

711 
unfolding numeral_simps by simp 

712 

713 
lemma add_Bit0_Bit0: 

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

715 
unfolding numeral_simps by simp 

716 

717 
lemma add_Bit0_Bit1: 

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

719 
unfolding numeral_simps by simp 

720 

721 
lemma add_Bit1_Bit0: 

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

723 
unfolding numeral_simps by simp 

724 

725 
lemma add_Bit1_Bit1: 

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

727 
unfolding numeral_simps by simp 

728 

729 
lemma add_Pls_right: 

730 
"k + Pls = k" 

731 
unfolding numeral_simps by simp 

732 

733 
lemma add_Min_right: 

734 
"k + Min = pred k" 

735 
unfolding numeral_simps by simp 

736 

737 
lemmas add_bin_simps [simp] = 

738 
add_Pls add_Min add_Pls_right add_Min_right 

739 
add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1 

740 

741 
text {* Negation *} 

742 

743 
lemma minus_Pls: 

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

744 
" Pls = Pls" 
28958  745 
unfolding numeral_simps by simp 
746 

747 
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

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

751 
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

752 
" (Bit0 k) = Bit0 ( k)" 
28958  753 
unfolding numeral_simps by simp 
754 

755 
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

756 
" (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

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

758 

28958  759 
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

760 
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

761 

28958  762 
text {* Subtraction *} 
763 

764 
lemma diff_Pls: 

765 
"Pls  k =  k" 

766 
unfolding numeral_simps by simp 

767 

768 
lemma diff_Min: 

769 
"Min  k = pred ( k)" 

770 
unfolding numeral_simps by simp 

771 

772 
lemma diff_Bit0_Bit0: 

773 
"(Bit0 k)  (Bit0 l) = Bit0 (k  l)" 

774 
unfolding numeral_simps by simp 

775 

776 
lemma diff_Bit0_Bit1: 

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

778 
unfolding numeral_simps by simp 

779 

780 
lemma diff_Bit1_Bit0: 

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

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

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

783 

28958  784 
lemma diff_Bit1_Bit1: 
785 
"(Bit1 k)  (Bit1 l) = Bit0 (k  l)" 

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

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

787 

28958  788 
lemma diff_Pls_right: 
789 
"k  Pls = k" 

790 
unfolding numeral_simps by simp 

791 

792 
lemma diff_Min_right: 

793 
"k  Min = succ k" 

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

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

795 

28958  796 
lemmas diff_bin_simps [simp] = 
797 
diff_Pls diff_Min diff_Pls_right diff_Min_right 

798 
diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1 

799 

800 
text {* Multiplication *} 

801 

802 
lemma mult_Pls: 

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

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

805 

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

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

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

809 

28958  810 
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

811 
"(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

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

813 

28958  814 
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

815 
"(Bit1 k) * l = (Bit0 (k * l)) + l" 
28958  816 
unfolding numeral_simps int_distrib by simp 
817 

818 
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

819 
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

820 

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

821 

28958  822 
subsubsection {* Binary comparisons *} 
823 

824 
text {* Preliminaries *} 

825 

826 
lemma even_less_0_iff: 

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

828 
proof  

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

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

831 
by (simp add: mult_less_0_iff zero_less_two 

832 
order_less_not_sym [OF zero_less_two]) 

833 
finally show ?thesis . 

834 
qed 

835 

836 
lemma le_imp_0_less: 

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

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

839 
proof  

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

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

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

843 
finally show "0 < 1 + z" . 

844 
qed 

845 

846 
lemma odd_less_0_iff: 

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

848 
proof (cases z rule: int_cases) 

849 
case (nonneg n) 

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

851 
le_imp_0_less [THEN order_less_imp_le]) 

852 
next 

853 
case (neg n) 

854 
thus ?thesis by (simp del: of_nat_Suc of_nat_add 

855 
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) 

856 
qed 

857 

858 
lemma neg_simps: 

859 
"Pls < 0 \<longleftrightarrow> False" 

860 
"Min < 0 \<longleftrightarrow> True" 

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

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

863 
unfolding numeral_simps 

864 
by (simp_all add: even_less_0_iff odd_less_0_iff) 

865 

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

867 
by simp 

868 

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

870 
unfolding numeral_simps 

871 
proof 

872 
have "k  1 < k" by simp 

873 
also assume "k \<le> l" 

874 
finally show "k  1 < l" . 

875 
next 

876 
assume "k  1 < l" 

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

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

879 
qed 

880 

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

882 
unfolding numeral_simps by simp 

883 

884 
text {* Lessthan *} 

885 

886 
lemma less_bin_simps [simp]: 

887 
"Pls < Pls \<longleftrightarrow> False" 

888 
"Pls < Min \<longleftrightarrow> False" 

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

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

891 
"Min < Pls \<longleftrightarrow> True" 

892 
"Min < Min \<longleftrightarrow> False" 

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

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

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

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

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

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

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

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

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

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

903 
unfolding le_iff_pred_less 

904 
less_bin_lemma [of Pls] 

905 
less_bin_lemma [of Min] 

906 
less_bin_lemma [of "k"] 

907 
less_bin_lemma [of "Bit0 k"] 

908 
less_bin_lemma [of "Bit1 k"] 

909 
less_bin_lemma [of "pred Pls"] 

910 
less_bin_lemma [of "pred k"] 

911 
by (simp_all add: neg_simps succ_pred) 

912 

913 
text {* Lessthanorequal *} 

914 

915 
lemma le_bin_simps [simp]: 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

932 
unfolding not_less [symmetric] 

933 
by (simp_all add: not_le) 

934 

935 
text {* Equality *} 

936 

937 
lemma eq_bin_simps [simp]: 

938 
"Pls = Pls \<longleftrightarrow> True" 

939 
"Pls = Min \<longleftrightarrow> False" 

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

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

942 
"Min = Pls \<longleftrightarrow> False" 

943 
"Min = Min \<longleftrightarrow> True" 

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

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

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

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

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

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

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

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

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

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

954 
unfolding order_eq_iff [where 'a=int] 

955 
by (simp_all add: not_less) 

956 

957 

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

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

959 

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

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

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

962 

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

963 
text {* selfembedding of the integers *} 
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 
instantiation int :: number_ring 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

967 

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

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

970 

28724  971 
instance proof 
972 
qed (simp only: int_number_of_def) 

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

973 

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

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

975 

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

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

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

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

979 

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

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

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

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

983 

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

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

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

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

987 

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

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

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

991 

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

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

993 
"number_of (v + w) = (number_of v + number_of w::'a::number_ring)" 
28958  994 
unfolding number_of_eq by (rule of_int_add) 
995 

996 
lemma number_of_diff: 

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

998 
unfolding number_of_eq by (rule of_int_diff) 

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

999 

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

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

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

1003 

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

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

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

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

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

1008 

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

1009 
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

1010 
"(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

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

1012 

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

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

1014 
Converting numerals 0 and 1 to their abstract versions. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1016 

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

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

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

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

1020 

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

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

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

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

1024 

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

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

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

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

1028 

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

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

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

1031 
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

1032 
*} 
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 numeral_m1_eq_minus_1: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1037 

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

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

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

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

1041 

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

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

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

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

1045 

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

1046 
(*Negation of a coefficient*) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1048 
" (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

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

1050 

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

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

1052 

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

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

1054 
"number_of v  number_of w = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1055 
(number_of (v + uminus w)::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

1061 

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

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

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

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

1065 

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

1066 
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

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

1068 
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

1069 

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

1070 
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

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

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

1073 

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

1074 

28958  1075 
subsubsection {* Equality of Binary Numbers *} 
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 
text {* First version by Norbert Voelker *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1078 

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

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

1080 
neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1082 
"neg Z \<longleftrightarrow> Z < 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1083 

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

1084 
definition (*for simplifying equalities*) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1085 
iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1087 
"iszero z \<longleftrightarrow> z = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1088 

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

1089 
lemma not_neg_int [simp]: "~ neg (of_nat n)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1091 

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

1092 
lemma neg_zminus_int [simp]: "neg ( (of_nat (Suc n)))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1094 

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

1095 
lemmas neg_eq_less_0 = neg_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1096 

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

1097 
lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1099 

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

1100 
text{*To simplify inequalities when Numeral1 can get simplified to 1*} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1101 

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

1102 
lemma not_neg_0: "~ neg 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1104 

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

1105 
lemma not_neg_1: "~ neg 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1107 

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

1108 
lemma iszero_0: "iszero 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1110 

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

1111 
lemma not_iszero_1: "~ iszero 1" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1113 

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

1114 
lemma neg_nat: "neg z ==> nat z = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1116 

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

1117 
lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1119 

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

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

1121 
"((number_of x::'a::number_ring) = number_of y) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1122 
iszero (number_of (x + uminus y) :: 'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1123 
unfolding iszero_def number_of_add number_of_minus 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1125 

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

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

1127 
"iszero ((number_of Pls)::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1128 
unfolding iszero_def numeral_0_eq_0 .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1129 

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

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

1131 
"~ iszero ((number_of Min)::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1132 
unfolding iszero_def numeral_m1_eq_minus_1 by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1133 

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

1134 

28958  1135 
subsubsection {* Comparisons, for Ordered Rings *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1136 

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

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

1138 

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

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

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

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

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

1143 
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

1144 
thus ?thesis using le_imp_0_less [OF le] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

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

1151 
have "(0::int) < 1 + (of_nat n + of_nat n)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1153 
also have "... =  (1 + z + z)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

1157 
thus False by blast 
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 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1160 

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

1161 
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

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

1163 
iszero (number_of w::'a::{ring_char_0,number_ring})" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1165 
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

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

1167 
assume eq: "of_int w + of_int w = (0::'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1168 
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

1169 
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

1170 
then show "w = 0" by (simp only: double_eq_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1173 
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

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

1175 

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

1176 
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

1177 
"~ 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

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

1179 
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

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

1181 
assume eq: "1 + of_int w + of_int w = (0::'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1182 
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

1183 
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

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

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

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

1187 
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

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

1189 

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

1190 

28958  1191 
subsubsection {* The LessThan Relation *} 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1192 

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

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

1194 
"((number_of x::'a::{ordered_idom,number_ring}) < number_of y) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1195 
= neg (number_of (x + uminus y) :: 'a)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1196 
apply (subst less_iff_diff_less_0) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1197 
apply (simp add: neg_def diff_minus number_of_add number_of_minus) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1199 

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

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

1201 
If @{term Numeral0} is rewritten to 0 then this rule can't be applied: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1202 
@{term Numeral0} IS @{term "number_of Pls"} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1203 
*} 
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 
lemma not_neg_number_of_Pls: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1206 
"~ neg (number_of Pls ::'a::{ordered_idom,number_ring})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1207 
by (simp add: neg_def numeral_0_eq_0) 
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 
lemma neg_number_of_Min: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1210 
"neg (number_of Min ::'a::{ordered_idom,number_ring})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1211 
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1212 

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

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

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

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

1216 
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

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

1218 
by (simp add: mult_less_0_iff zero_less_two 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1219 
order_less_not_sym [OF zero_less_two]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1222 

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

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

1224 
"(1 + z + z < 0) = (z < (0::int))"; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1227 
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

1228 
le_imp_0_less [THEN order_less_imp_le]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1231 
thus ?thesis by (simp del: of_nat_Suc of_nat_add 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1232 
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1234 

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

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

1236 
"neg (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

1237 
neg (number_of w :: 'a::{ordered_idom,number_ring})" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1238 
by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff) 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26075
diff
changeset

1239 

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

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

1241 
"neg (number_of (Bit1 w)::'a) = 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1242 
neg (number_of w :: 'a::{ordered_idom,number_ring})" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

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

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

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

1248 
by (simp add: neg_def number_of_eq numeral_simps) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1250 

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

1251 

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

1252 
text {* LessThan or Equals *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1253 

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

1254 
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

1255 

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

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

1257 
linorder_not_less [of "number_of w" "number_of v", symmetric, 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1259 

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

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

1261 
"((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1262 
= (~ (neg (number_of (y + uminus x) :: 'a)))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1264 

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

1265 

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

1266 
text {* Absolute value (@{term abs}) *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1267 

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

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

1269 
"abs(number_of x::'a::{ordered_idom,number_ring}) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

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

1272 

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 
text {* Reorientation of the equation nnn=x *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1275 

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

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

1277 
"(number_of w = x) = (x = number_of w)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1279 

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

1280 

28958  1281 
subsubsection {* Simplification of arithmetic operations on integer constants. *} 
25919
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 
lemmas arith_extra_simps [standard, simp] = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1284 
number_of_add [symmetric] 
28958  1285 
number_of_minus [symmetric] 
1286 
numeral_m1_eq_minus_1 [symmetric] 

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

1287 
number_of_mult [symmetric] 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1289 

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

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

1291 
For making a minimal simpset, one must include these default simprules. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1292 
Also include @{text simp_thms}. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1293 
*} 
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 
lemmas arith_simps = 
26075
815f3ccc0b45
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
huffman
parents:
26072
diff
changeset

1296 
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

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

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

1299 

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

1300 
text {* Simplification of relational operations *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1301 

28962
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1302 
lemma less_number_of [simp]: 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1303 
"(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

1304 
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

1305 

f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1306 
lemma le_number_of [simp]: 
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1307 
"(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

1308 
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

1309 

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

1310 
lemmas rel_simps [simp] = 
28962
f603183f7a5c
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
huffman
parents:
28958
diff
changeset

1311 
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

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

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

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

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

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

1317 
(* iszero_number_of_Pls would never be used 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1318 
because its lhs simplifies to "iszero 0" *) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1319 

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

1320 

28958  1321 
subsubsection {* Simplification of arithmetic when nested to the right. *} 
25919
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 add_number_of_left [simp]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1324 
"number_of v + (number_of w + z) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1325 
(number_of(v + w) + z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1327 

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

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

1329 
"number_of v * (number_of w * z) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1330 
(number_of(v * w) * z::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1332 

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

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

1334 
"number_of v + (number_of w  c) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1335 
number_of(v + w)  (c::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1337 

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

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

1339 
"number_of v + (c  number_of w) = 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1340 
number_of (v + uminus w) + (c::'a::number_ring)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1341 
apply (subst diff_number_of_eq [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1342 
apply (simp only: compare_rls) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

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

1344 

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

1345 

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

1346 
subsection {* The Set of Integers *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1347 

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

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

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

1350 

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

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

1352 
Ints :: "'a set" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1353 
where 
28562  1354 
[code del]: "Ints = range of_int" 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1355 

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

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

1357 

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

1358 
notation (xsymbols) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1359 
Ints ("\<int>") 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1360 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1361 
context ring_1 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1362 
begin 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1363 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1364 
lemma Ints_0 [simp]: "0 \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1365 
apply (simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1366 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1367 
apply (rule of_int_0 [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1368 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1369 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1370 
lemma Ints_1 [simp]: "1 \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1371 
apply (simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1372 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1373 
apply (rule of_int_1 [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1374 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1375 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1376 
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

1377 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1378 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1379 
apply (rule of_int_add [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1380 
done 
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 
lemma Ints_minus [simp]: "a \<in> \<int> \<Longrightarrow> a \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1383 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1384 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1385 
apply (rule of_int_minus [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1386 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1387 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1388 
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

1389 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1390 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1391 
apply (rule of_int_mult [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1392 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1393 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1394 
lemma Ints_cases [cases set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1395 
assumes "q \<in> \<int>" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1396 
obtains (of_int) z where "q = of_int z" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1397 
unfolding Ints_def 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1398 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1399 
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

1400 
then obtain z where "q = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1401 
then show thesis .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1402 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1403 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1404 
lemma Ints_induct [case_names of_int, induct set: Ints]: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1405 
"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

1406 
by (rule Ints_cases) auto 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1407 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1408 
end 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1409 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1410 
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

1411 
apply (auto simp add: Ints_def) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1412 
apply (rule range_eqI) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1413 
apply (rule of_int_diff [symmetric]) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1414 
done 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1415 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1416 
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1417 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1418 
lemma Ints_double_eq_0_iff: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1419 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1420 
shows "(a + a = 0) = (a = (0::'a::ring_char_0))" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1421 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1422 
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

1423 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1424 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1425 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1426 
assume "a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1427 
thus "a + a = 0" by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1428 
next 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1429 
assume eq: "a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1430 
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

1431 
hence "z + z = 0" by (simp only: of_int_eq_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1432 
hence "z = 0" by (simp only: double_eq_0_iff) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1433 
thus "a = 0" by (simp add: a) 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1434 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1435 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1436 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1437 
lemma Ints_odd_nonzero: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1438 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1439 
shows "1 + a + a \<noteq> (0::'a::ring_char_0)" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1440 
proof  
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1441 
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

1442 
then obtain z where a: "a = of_int z" .. 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1443 
show ?thesis 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1444 
proof 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1445 
assume eq: "1 + a + a = 0" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1446 
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

1447 
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

1448 
with odd_nonzero show False by blast 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1449 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1450 
qed 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1451 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1452 
lemma Ints_number_of: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1453 
"(number_of w :: 'a::number_ring) \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1454 
unfolding number_of_eq Ints_def by simp 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1455 

8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1456 
lemma Ints_odd_less_0: 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1457 
assumes in_Ints: "a \<in> Ints" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1458 
shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"; 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
diff
changeset

1459 
proof  