author  nipkow 
Mon, 17 Jan 2005 15:21:40 +0100  
changeset 15440  d0cd75f7a365 
parent 15439  71c0f98e31f1 
child 15531  08c8dad8e399 
permissions  rwrr 
7032  1 
(* Title: HOL/NatBin.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1999 University of Cambridge 

12838  5 
*) 
7032  6 

12838  7 
header {* Binary arithmetic for the natural numbers *} 
7032  8 

15131  9 
theory NatBin 
15140  10 
imports IntDiv 
15131  11 
begin 
7032  12 

12838  13 
text {* 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

14 
Arithmetic for naturals is reduced to that for the nonnegative integers. 
12838  15 
*} 
16 

17 
instance nat :: number .. 

18 

19 
defs (overloaded) 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

20 
nat_number_of_def: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

21 
"(number_of::bin => nat) v == nat ((number_of :: bin => int) v)" 
12838  22 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

23 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

24 
subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

25 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

26 
declare nat_0 [simp] nat_1 [simp] 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

27 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

28 
lemma nat_number_of [simp]: "nat (number_of w) = number_of w" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

29 
by (simp add: nat_number_of_def) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

30 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

31 
lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

32 
by (simp add: nat_number_of_def) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

33 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

34 
lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

35 
by (simp add: nat_1 nat_number_of_def) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

36 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

37 
lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

38 
by (simp add: nat_numeral_1_eq_1) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

39 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

40 
lemma numeral_2_eq_2: "2 = Suc (Suc 0)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

41 
apply (unfold nat_number_of_def) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

42 
apply (rule nat_2) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

43 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

44 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

45 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

46 
text{*Distributive laws for type @{text nat}. The others are in theory 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

47 
@{text IntArith}, but these require div and mod to be defined for type 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

48 
"int". They also need some of the lemmas proved above.*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

49 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

50 
lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

51 
apply (case_tac "0 <= z'") 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

52 
apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

53 
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

54 
apply (auto elim!: nonneg_eq_int) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

55 
apply (rename_tac m m') 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

56 
apply (subgoal_tac "0 <= int m div int m'") 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

57 
prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

58 
apply (rule inj_int [THEN injD], simp) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

59 
apply (rule_tac r = "int (m mod m') " in quorem_div) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

60 
prefer 2 apply force 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

61 
apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

62 
zmult_int) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

63 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

64 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

65 
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

66 
lemma nat_mod_distrib: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

67 
"[ (0::int) <= z; 0 <= z' ] ==> nat (z mod z') = nat z mod nat z'" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

68 
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

69 
apply (auto elim!: nonneg_eq_int) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

70 
apply (rename_tac m m') 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

71 
apply (subgoal_tac "0 <= int m mod int m'") 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

72 
prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

73 
apply (rule inj_int [THEN injD], simp) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

74 
apply (rule_tac q = "int (m div m') " in quorem_mod) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

75 
prefer 2 apply force 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

76 
apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

77 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

78 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

79 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

80 
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

81 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

82 
(*"neg" is used in rewrite rules for binary comparisons*) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

83 
lemma int_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

84 
"int (number_of v :: nat) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

85 
(if neg (number_of v :: int) then 0 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

86 
else (number_of v :: int))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

87 
by (simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

88 
add: neg_nat nat_number_of_def not_neg_nat add_assoc) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

89 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

90 

14390  91 
subsubsection{*Successor *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

92 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

93 
lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

94 
apply (rule sym) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

95 
apply (simp add: nat_eq_iff int_Suc) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

96 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

97 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

98 
lemma Suc_nat_number_of_add: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

99 
"Suc (number_of v + n) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

100 
(if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

101 
by (simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

102 
add: nat_number_of_def neg_nat 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

103 
Suc_nat_eq_nat_zadd1 number_of_succ) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

104 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

105 
lemma Suc_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

106 
"Suc (number_of v) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

107 
(if neg (number_of v :: int) then 1 else number_of (bin_succ v))" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

108 
apply (cut_tac n = 0 in Suc_nat_number_of_add) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

109 
apply (simp cong del: if_weak_cong) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

110 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

111 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

112 

14390  113 
subsubsection{*Addition *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

114 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

115 
(*"neg" is used in rewrite rules for binary comparisons*) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

116 
lemma add_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

117 
"(number_of v :: nat) + number_of v' = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

118 
(if neg (number_of v :: int) then number_of v' 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

119 
else if neg (number_of v' :: int) then number_of v 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

120 
else number_of (bin_add v v'))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

121 
by (force dest!: neg_nat 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

122 
simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

123 
simp add: nat_number_of_def nat_add_distrib [symmetric]) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

124 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

125 

14390  126 
subsubsection{*Subtraction *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

127 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

128 
lemma diff_nat_eq_if: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

129 
"nat z  nat z' = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

130 
(if neg z' then nat z 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

131 
else let d = zz' in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

132 
if neg d then 0 else nat d)" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

133 
apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

134 
apply (simp add: diff_is_0_eq nat_le_eq_zle) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

135 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

136 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

137 
lemma diff_nat_number_of [simp]: 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

138 
"(number_of v :: nat)  number_of v' = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

139 
(if neg (number_of v' :: int) then number_of v 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

140 
else let d = number_of (bin_add v (bin_minus v')) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

141 
if neg d then 0 else nat d)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

142 
by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

143 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

144 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

145 

14390  146 
subsubsection{*Multiplication *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

147 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

148 
lemma mult_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

149 
"(number_of v :: nat) * number_of v' = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

150 
(if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))" 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

151 
by (force dest!: neg_nat 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

152 
simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

153 
simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

154 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

155 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

156 

14390  157 
subsubsection{*Quotient *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

158 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

159 
lemma div_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

160 
"(number_of v :: nat) div number_of v' = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

161 
(if neg (number_of v :: int) then 0 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

162 
else nat (number_of v div number_of v'))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

163 
by (force dest!: neg_nat 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

164 
simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

165 
simp add: nat_number_of_def nat_div_distrib [symmetric]) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

166 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

167 
lemma one_div_nat_number_of [simp]: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

168 
"(Suc 0) div number_of v' = (nat (1 div number_of v'))" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

169 
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

170 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

171 

14390  172 
subsubsection{*Remainder *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

173 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

174 
lemma mod_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

175 
"(number_of v :: nat) mod number_of v' = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

176 
(if neg (number_of v :: int) then 0 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

177 
else if neg (number_of v' :: int) then number_of v 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

178 
else nat (number_of v mod number_of v'))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

179 
by (force dest!: neg_nat 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

180 
simp del: nat_number_of 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

181 
simp add: nat_number_of_def nat_mod_distrib [symmetric]) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

182 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

183 
lemma one_mod_nat_number_of [simp]: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

184 
"(Suc 0) mod number_of v' = 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

185 
(if neg (number_of v' :: int) then Suc 0 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

186 
else nat (1 mod number_of v'))" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

187 
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric]) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

188 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

189 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

190 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

191 
ML 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

192 
{* 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

193 
val nat_number_of_def = thm"nat_number_of_def"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

194 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

195 
val nat_number_of = thm"nat_number_of"; 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

196 
val nat_numeral_0_eq_0 = thm"nat_numeral_0_eq_0"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

197 
val nat_numeral_1_eq_1 = thm"nat_numeral_1_eq_1"; 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

198 
val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

199 
val numeral_2_eq_2 = thm"numeral_2_eq_2"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

200 
val nat_div_distrib = thm"nat_div_distrib"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

201 
val nat_mod_distrib = thm"nat_mod_distrib"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

202 
val int_nat_number_of = thm"int_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

203 
val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

204 
val Suc_nat_number_of_add = thm"Suc_nat_number_of_add"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

205 
val Suc_nat_number_of = thm"Suc_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

206 
val add_nat_number_of = thm"add_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

207 
val diff_nat_eq_if = thm"diff_nat_eq_if"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

208 
val diff_nat_number_of = thm"diff_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

209 
val mult_nat_number_of = thm"mult_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

210 
val div_nat_number_of = thm"div_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

211 
val mod_nat_number_of = thm"mod_nat_number_of"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

212 
*} 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

213 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

214 

14390  215 
subsection{*Comparisons*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

216 

14390  217 
subsubsection{*Equals (=) *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

218 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

219 
lemma eq_nat_nat_iff: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

220 
"[ (0::int) <= z; 0 <= z' ] ==> (nat z = nat z') = (z=z')" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

221 
by (auto elim!: nonneg_eq_int) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

222 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

223 
(*"neg" is used in rewrite rules for binary comparisons*) 
14390  224 
lemma eq_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

225 
"((number_of v :: nat) = number_of v') = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

226 
(if neg (number_of v :: int) then (iszero (number_of v' :: int)  neg (number_of v' :: int)) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

227 
else if neg (number_of v' :: int) then iszero (number_of v :: int) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

228 
else iszero (number_of (bin_add v (bin_minus v')) :: int))" 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

229 
apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

230 
eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

231 
split add: split_if cong add: imp_cong) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

232 
apply (simp only: nat_eq_iff nat_eq_iff2) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

233 
apply (simp add: not_neg_eq_ge_0 [symmetric]) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

234 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

235 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

236 

14390  237 
subsubsection{*Lessthan (<) *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

238 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

239 
(*"neg" is used in rewrite rules for binary comparisons*) 
14390  240 
lemma less_nat_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

241 
"((number_of v :: nat) < number_of v') = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

242 
(if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int) 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

243 
else neg (number_of (bin_add v (bin_minus v')) :: int))" 
14390  244 
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

245 
nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless 
14390  246 
cong add: imp_cong, simp) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

247 

14390  248 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

249 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

250 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

251 
(*Maps #n to n for n = 0, 1, 2*) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

252 
lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

253 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

254 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

255 
subsection{*Powers with Numeric Exponents*} 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

256 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

257 
text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}. 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

258 
We cannot prove general results about the numeral @{term "1"}, so we have to 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

259 
use @{term " 1"} instead.*} 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

260 

15003  261 
lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

262 
by (simp add: numeral_2_eq_2 Power.power_Suc) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

263 

15003  264 
lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

265 
by (simp add: power2_eq_square) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

266 

15003  267 
lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

268 
by (simp add: power2_eq_square) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

269 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

270 
text{*Squares of literal numerals will be evaluated.*} 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

271 
declare power2_eq_square [of "number_of w", standard, simp] 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

272 

15003  273 
lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

274 
by (simp add: power2_eq_square zero_le_square) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

275 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

276 
lemma zero_less_power2 [simp]: 
15003  277 
"(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

278 
by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

279 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

280 
lemma power2_less_0 [simp]: 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

281 
fixes a :: "'a::{ordered_idom,recpower}" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

282 
shows "~ (a\<twosuperior> < 0)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

283 
by (force simp add: power2_eq_square mult_less_0_iff) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

284 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

285 
lemma zero_eq_power2 [simp]: 
15003  286 
"(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

287 
by (force simp add: power2_eq_square mult_eq_0_iff) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

288 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

289 
lemma abs_power2 [simp]: 
15003  290 
"abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

291 
by (simp add: power2_eq_square abs_mult abs_mult_self) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

292 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

293 
lemma power2_abs [simp]: 
15003  294 
"(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

295 
by (simp add: power2_eq_square abs_mult_self) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

296 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

297 
lemma power2_minus [simp]: 
15003  298 
"( a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

299 
by (simp add: power2_eq_square) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

300 

15003  301 
lemma power_minus1_even: "( 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" 
15251  302 
apply (induct "n") 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

303 
apply (auto simp add: power_Suc power_add) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

304 
done 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

305 

15003  306 
lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

307 
by (simp add: power_mult power_mult_distrib power2_eq_square) 
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

308 

75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

309 
lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2" 
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

310 
by (simp add: power_even_eq) 
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

311 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

312 
lemma power_minus_even [simp]: 
15003  313 
"(a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

314 
by (simp add: power_minus1_even power_minus [of a]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

315 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

316 
lemma zero_le_even_power: 
15003  317 
"0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

318 
proof (induct "n") 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

319 
case 0 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

320 
show ?case by (simp add: zero_le_one) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

321 
next 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

322 
case (Suc n) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

323 
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

324 
by (simp add: mult_ac power_add power2_eq_square) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

325 
thus ?case 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

326 
by (simp add: prems zero_le_square zero_le_mult_iff) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

327 
qed 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

328 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

329 
lemma odd_power_less_zero: 
15003  330 
"(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

331 
proof (induct "n") 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

332 
case 0 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

333 
show ?case by (simp add: Power.power_Suc) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

334 
next 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

335 
case (Suc n) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

336 
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

337 
by (simp add: mult_ac power_add power2_eq_square Power.power_Suc) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

338 
thus ?case 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

339 
by (simp add: prems mult_less_0_iff mult_neg) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

340 
qed 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

341 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

342 
lemma odd_0_le_power_imp_0_le: 
15003  343 
"0 \<le> a ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})" 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

344 
apply (insert odd_power_less_zero [of a n]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

345 
apply (force simp add: linorder_not_less [symmetric]) 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

346 
done 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

347 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

348 
text{*Simprules for comparisons where common factors can be cancelled.*} 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

349 
lemmas zero_compare_simps = 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

350 
add_strict_increasing add_strict_increasing2 add_increasing 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

351 
zero_le_mult_iff zero_le_divide_iff 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

352 
zero_less_mult_iff zero_less_divide_iff 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

353 
mult_le_0_iff divide_le_0_iff 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

354 
mult_less_0_iff divide_less_0_iff 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

355 
zero_le_power2 power2_less_0 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

356 

14390  357 
subsubsection{*Nat *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

358 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

359 
lemma Suc_pred': "0 < n ==> n = Suc(n  1)" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

360 
by (simp add: numerals) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

361 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

362 
(*Expresses a natural number constant as the Suc of another one. 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

363 
NOT suitable for rewriting because n recurs in the condition.*) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

364 
lemmas expand_Suc = Suc_pred' [of "number_of v", standard] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

365 

14390  366 
subsubsection{*Arith *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

367 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

368 
lemma Suc_eq_add_numeral_1: "Suc n = n + 1" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

369 
by (simp add: numerals) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

370 

14467  371 
lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n" 
372 
by (simp add: numerals) 

373 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

374 
(* These two can be useful when m = number_of... *) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

375 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

376 
lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m  1) + n))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

377 
apply (case_tac "m") 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

378 
apply (simp_all add: numerals) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

379 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

380 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

381 
lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m  1) * n))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

382 
apply (case_tac "m") 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

383 
apply (simp_all add: numerals) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

384 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

385 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

386 
lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m  1)))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

387 
apply (case_tac "m") 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

388 
apply (simp_all add: numerals) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

389 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

390 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

391 

14390  392 
subsection{*Comparisons involving (0::nat) *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

393 

14390  394 
text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*} 
395 

396 
lemma eq_number_of_0 [simp]: 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

397 
"(number_of v = (0::nat)) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

398 
(if neg (number_of v :: int) then True else iszero (number_of v :: int))" 
14390  399 
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

400 

14390  401 
lemma eq_0_number_of [simp]: 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

402 
"((0::nat) = number_of v) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

403 
(if neg (number_of v :: int) then True else iszero (number_of v :: int))" 
14390  404 
by (rule trans [OF eq_sym_conv eq_number_of_0]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

405 

14390  406 
lemma less_0_number_of [simp]: 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

407 
"((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

408 
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

409 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

410 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

411 
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)" 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

412 
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

413 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

414 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

415 

14390  416 
subsection{*Comparisons involving Suc *} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

417 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

418 
lemma eq_number_of_Suc [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

419 
"(number_of v = Suc n) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

420 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

421 
if neg pv then False else nat pv = n)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

422 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

423 
number_of_pred nat_number_of_def 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

424 
split add: split_if) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

425 
apply (rule_tac x = "number_of v" in spec) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

426 
apply (auto simp add: nat_eq_iff) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

427 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

428 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

429 
lemma Suc_eq_number_of [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

430 
"(Suc n = number_of v) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

431 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

432 
if neg pv then False else nat pv = n)" 
14390  433 
by (rule trans [OF eq_sym_conv eq_number_of_Suc]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

434 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

435 
lemma less_number_of_Suc [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

436 
"(number_of v < Suc n) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

437 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

438 
if neg pv then True else nat pv < n)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

439 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

440 
number_of_pred nat_number_of_def 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

441 
split add: split_if) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

442 
apply (rule_tac x = "number_of v" in spec) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

443 
apply (auto simp add: nat_less_iff) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

444 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

445 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

446 
lemma less_Suc_number_of [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

447 
"(Suc n < number_of v) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

448 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

449 
if neg pv then False else n < nat pv)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

450 
apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

451 
number_of_pred nat_number_of_def 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

452 
split add: split_if) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

453 
apply (rule_tac x = "number_of v" in spec) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

454 
apply (auto simp add: zless_nat_eq_int_zless) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

455 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

456 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

457 
lemma le_number_of_Suc [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

458 
"(number_of v <= Suc n) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

459 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

460 
if neg pv then True else nat pv <= n)" 
14390  461 
by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

462 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

463 
lemma le_Suc_number_of [simp]: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

464 
"(Suc n <= number_of v) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

465 
(let pv = number_of (bin_pred v) in 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

466 
if neg pv then False else n <= nat pv)" 
14390  467 
by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric]) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

468 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

469 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

470 
(* Push int(.) inwards: *) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

471 
declare zadd_int [symmetric, simp] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

472 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

473 
lemma lemma1: "(m+m = n+n) = (m = (n::int))" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

474 
by auto 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

475 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

476 
lemma lemma2: "m+m ~= (1::int) + (n + n)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

477 
apply auto 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

478 
apply (drule_tac f = "%x. x mod 2" in arg_cong) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

479 
apply (simp add: zmod_zadd1_eq) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

480 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

481 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

482 
lemma eq_number_of_BIT_BIT: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

483 
"((number_of (v BIT x) ::int) = number_of (w BIT y)) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

484 
(x=y & (((number_of v) ::int) = number_of w))" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

485 
by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute 
14738  486 
OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

487 
split add: split_if cong: imp_cong) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

488 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

489 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

490 
lemma eq_number_of_BIT_Pls: 
15013  491 
"((number_of (v BIT x) ::int) = Numeral0) = 
492 
(x=False & (((number_of v) ::int) = Numeral0))" 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

493 
apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

494 
split add: split_if cong: imp_cong) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

495 
apply (rule_tac x = "number_of v" in spec, safe) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

496 
apply (simp_all (no_asm_use)) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

497 
apply (drule_tac f = "%x. x mod 2" in arg_cong) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

498 
apply (simp add: zmod_zadd1_eq) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

499 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

500 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

501 
lemma eq_number_of_BIT_Min: 
15013  502 
"((number_of (v BIT x) ::int) = number_of Numeral.Min) = 
503 
(x=True & (((number_of v) ::int) = number_of Numeral.Min))" 

14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

504 
apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

505 
split add: split_if cong: imp_cong) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

506 
apply (rule_tac x = "number_of v" in spec, auto) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

507 
apply (drule_tac f = "%x. x mod 2" in arg_cong, auto) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

508 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

509 

15013  510 
lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min" 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

511 
by auto 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

512 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

513 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

514 

14390  515 
subsection{*Literal arithmetic involving powers*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

516 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

517 
lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n" 
15251  518 
apply (induct "n") 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

519 
apply (simp_all (no_asm_simp) add: nat_mult_distrib) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

520 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

521 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

522 
lemma power_nat_number_of: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

523 
"(number_of v :: nat) ^ n = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

524 
(if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))" 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

525 
by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

526 
split add: split_if cong: imp_cong) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

527 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

528 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

529 
declare power_nat_number_of [of _ "number_of w", standard, simp] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

530 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

531 

14390  532 
text{*For the integers*} 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

533 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

534 
lemma zpower_number_of_even: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

535 
"(z::int) ^ number_of (w BIT False) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

536 
(let w = z ^ (number_of w) in w*w)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

537 
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

538 
apply (simp only: number_of_add) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

539 
apply (rule_tac x = "number_of w" in spec, clarify) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

540 
apply (case_tac " (0::int) <= x") 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

541 
apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

542 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

543 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

544 
lemma zpower_number_of_odd: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

545 
"(z::int) ^ number_of (w BIT True) = 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

546 
(if (0::int) <= number_of w 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

547 
then (let w = z ^ (number_of w) in z*w*w) 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

548 
else 1)" 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

549 
apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

550 
apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

551 
apply (rule_tac x = "number_of w" in spec, clarify) 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

552 
apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat) 
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

553 
done 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

554 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

555 
declare zpower_number_of_even [of "number_of v", standard, simp] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

556 
declare zpower_number_of_odd [of "number_of v", standard, simp] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

557 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

558 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

559 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

560 
ML 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

561 
{* 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

562 
val numerals = thms"numerals"; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

563 
val numeral_ss = simpset() addsimps numerals; 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

564 

5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

565 
val nat_bin_arith_setup = 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

566 
[Fast_Arith.map_data 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

567 
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

568 
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

569 
inj_thms = inj_thms, 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

570 
lessD = lessD, 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

571 
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of, 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

572 
not_neg_number_of_Pls, 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

573 
neg_number_of_Min,neg_number_of_BIT]})] 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

574 
*} 
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
14194
diff
changeset

575 

12838  576 
setup nat_bin_arith_setup 
577 

13189
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset

578 
(* Enable arith to deal with div/mod k where k is a numeral: *) 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset

579 
declare split_div[of _ _ "number_of k", standard, arith_split] 
81ed5c6de890
Now arith can deal with div/mod arbitrary nat numerals.
nipkow
parents:
13154
diff
changeset

580 
declare split_mod[of _ _ "number_of k", standard, arith_split] 
13154  581 

15013  582 
lemma nat_number_of_Pls: "Numeral0 = (0::nat)" 
12838  583 
by (simp add: number_of_Pls nat_number_of_def) 
584 

15013  585 
lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)" 
12838  586 
apply (simp only: number_of_Min nat_number_of_def nat_zminus_int) 
587 
apply (simp add: neg_nat) 

588 
done 

7032  589 

12838  590 
lemma nat_number_of_BIT_True: 
591 
"number_of (w BIT True) = 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

592 
(if neg (number_of w :: int) then 0 
12838  593 
else let n = number_of w in Suc (n + n))" 
594 
apply (simp only: nat_number_of_def Let_def split: split_if) 

595 
apply (intro conjI impI) 

596 
apply (simp add: neg_nat neg_number_of_BIT) 

597 
apply (rule int_int_eq [THEN iffD1]) 

598 
apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) 

599 
apply (simp only: number_of_BIT if_True zadd_assoc) 

600 
done 

7032  601 

12838  602 
lemma nat_number_of_BIT_False: 
603 
"number_of (w BIT False) = (let n::nat = number_of w in n + n)" 

604 
apply (simp only: nat_number_of_def Let_def) 

14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

605 
apply (cases "neg (number_of w :: int)") 
12838  606 
apply (simp add: neg_nat neg_number_of_BIT) 
607 
apply (rule int_int_eq [THEN iffD1]) 

608 
apply (simp only: not_neg_nat neg_number_of_BIT int_Suc zadd_int [symmetric] simp_thms) 

609 
apply (simp only: number_of_BIT if_False zadd_0 zadd_assoc) 

610 
done 

611 

13043
ad1828b479b7
renamed nat_number_of to nat_number (avoid clash with separate theorem);
wenzelm
parents:
12933
diff
changeset

612 
lemmas nat_number = 
12838  613 
nat_number_of_Pls nat_number_of_Min 
614 
nat_number_of_BIT_True nat_number_of_BIT_False 

615 

616 
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" 

617 
by (simp add: Let_def) 

10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
9509
diff
changeset

618 

15003  619 
lemma power_m1_even: "(1) ^ (2*n) = (1::'a::{number_ring,recpower})" 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

620 
by (simp add: power_mult); 
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

621 

15003  622 
lemma power_m1_odd: "(1) ^ Suc(2*n) = (1::'a::{number_ring,recpower})" 
14443
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

623 
by (simp add: power_mult power_Suc); 
75910c7557c5
generic theorems about exponentials; general tidying up
paulson
parents:
14430
diff
changeset

624 

12440  625 

14390  626 
subsection{*Literal arithmetic and @{term of_nat}*} 
627 

628 
lemma of_nat_double: 

629 
"0 \<le> x ==> of_nat (nat (2 * x)) = of_nat (nat x) + of_nat (nat x)" 

630 
by (simp only: mult_2 nat_add_distrib of_nat_add) 

631 

632 
lemma nat_numeral_m1_eq_0: "1 = (0::nat)" 

633 
by (simp only: nat_number_of_def, simp) 

634 

635 
lemma of_nat_number_of_lemma: 

636 
"of_nat (number_of v :: nat) = 

637 
(if 0 \<le> (number_of v :: int) 

638 
then (number_of v :: 'a :: number_ring) 

639 
else 0)" 

15013  640 
by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat); 
14390  641 

642 
lemma of_nat_number_of_eq [simp]: 

643 
"of_nat (number_of v :: nat) = 

644 
(if neg (number_of v :: int) then 0 

645 
else (number_of v :: 'a :: number_ring))" 

646 
by (simp only: of_nat_number_of_lemma neg_def, simp) 

647 

648 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

649 
subsection {*Lemmas for the Combination and Cancellation Simprocs*} 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

650 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

651 
lemma nat_number_of_add_left: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

652 
"number_of v + (number_of v' + (k::nat)) = 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

653 
(if neg (number_of v :: int) then number_of v' + k 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

654 
else if neg (number_of v' :: int) then number_of v + k 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

655 
else number_of (bin_add v v') + k)" 
14390  656 
by simp 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

657 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

658 
lemma nat_number_of_mult_left: 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

659 
"number_of v * (number_of v' * (k::nat)) = 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

660 
(if neg (number_of v :: int) then 0 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

661 
else number_of (bin_mult v v') * k)" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

662 
by simp 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

663 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

664 

14390  665 
subsubsection{*For @{text combine_numerals}*} 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

666 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

667 
lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

668 
by (simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

669 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

670 

14390  671 
subsubsection{*For @{text cancel_numerals}*} 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

672 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

673 
lemma nat_diff_add_eq1: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

674 
"j <= (i::nat) ==> ((i*u + m)  (j*u + n)) = (((ij)*u + m)  n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

675 
by (simp split add: nat_diff_split add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

676 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

677 
lemma nat_diff_add_eq2: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

678 
"i <= (j::nat) ==> ((i*u + m)  (j*u + n)) = (m  ((ji)*u + n))" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

679 
by (simp split add: nat_diff_split add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

680 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

681 
lemma nat_eq_add_iff1: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

682 
"j <= (i::nat) ==> (i*u + m = j*u + n) = ((ij)*u + m = n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

683 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

684 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

685 
lemma nat_eq_add_iff2: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

686 
"i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (ji)*u + n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

687 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

688 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

689 
lemma nat_less_add_iff1: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

690 
"j <= (i::nat) ==> (i*u + m < j*u + n) = ((ij)*u + m < n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

691 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

692 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

693 
lemma nat_less_add_iff2: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

694 
"i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (ji)*u + n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

695 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

696 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

697 
lemma nat_le_add_iff1: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

698 
"j <= (i::nat) ==> (i*u + m <= j*u + n) = ((ij)*u + m <= n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

699 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

700 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

701 
lemma nat_le_add_iff2: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

702 
"i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (ji)*u + n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

703 
by (auto split add: nat_diff_split simp add: add_mult_distrib) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

704 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

705 

14390  706 
subsubsection{*For @{text cancel_numeral_factors} *} 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

707 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

708 
lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

709 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

710 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

711 
lemma nat_mult_less_cancel1: "(0::nat) < k ==> (k*m < k*n) = (m<n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

712 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

713 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

714 
lemma nat_mult_eq_cancel1: "(0::nat) < k ==> (k*m = k*n) = (m=n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

715 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

716 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

717 
lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

718 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

719 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

720 

14390  721 
subsubsection{*For @{text cancel_factor} *} 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

722 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

723 
lemma nat_mult_le_cancel_disj: "(k*m <= k*n) = ((0::nat) < k > m<=n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

724 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

725 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

726 
lemma nat_mult_less_cancel_disj: "(k*m < k*n) = ((0::nat) < k & m<n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

727 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

728 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

729 
lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat)  m=n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

730 
by auto 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

731 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

732 
lemma nat_mult_div_cancel_disj: 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

733 
"(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

734 
by (simp add: nat_mult_div_cancel1) 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

735 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

736 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

737 
ML 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

738 
{* 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

739 
val eq_nat_nat_iff = thm"eq_nat_nat_iff"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

740 
val eq_nat_number_of = thm"eq_nat_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

741 
val less_nat_number_of = thm"less_nat_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

742 
val power2_eq_square = thm "power2_eq_square"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

743 
val zero_le_power2 = thm "zero_le_power2"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

744 
val zero_less_power2 = thm "zero_less_power2"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

745 
val zero_eq_power2 = thm "zero_eq_power2"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

746 
val abs_power2 = thm "abs_power2"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

747 
val power2_abs = thm "power2_abs"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

748 
val power2_minus = thm "power2_minus"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

749 
val power_minus1_even = thm "power_minus1_even"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

750 
val power_minus_even = thm "power_minus_even"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

751 
val zero_le_even_power = thm "zero_le_even_power"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

752 
val odd_power_less_zero = thm "odd_power_less_zero"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

753 
val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

754 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

755 
val Suc_pred' = thm"Suc_pred'"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

756 
val expand_Suc = thm"expand_Suc"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

757 
val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1"; 
14467  758 
val Suc_eq_add_numeral_1_left = thm"Suc_eq_add_numeral_1_left"; 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

759 
val add_eq_if = thm"add_eq_if"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

760 
val mult_eq_if = thm"mult_eq_if"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

761 
val power_eq_if = thm"power_eq_if"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

762 
val eq_number_of_0 = thm"eq_number_of_0"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

763 
val eq_0_number_of = thm"eq_0_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

764 
val less_0_number_of = thm"less_0_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

765 
val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

766 
val eq_number_of_Suc = thm"eq_number_of_Suc"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

767 
val Suc_eq_number_of = thm"Suc_eq_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

768 
val less_number_of_Suc = thm"less_number_of_Suc"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

769 
val less_Suc_number_of = thm"less_Suc_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

770 
val le_number_of_Suc = thm"le_number_of_Suc"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

771 
val le_Suc_number_of = thm"le_Suc_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

772 
val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

773 
val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

774 
val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

775 
val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min"; 
14390  776 
val of_nat_number_of_eq = thm"of_nat_number_of_eq"; 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

777 
val nat_power_eq = thm"nat_power_eq"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

778 
val power_nat_number_of = thm"power_nat_number_of"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

779 
val zpower_number_of_even = thm"zpower_number_of_even"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

780 
val zpower_number_of_odd = thm"zpower_number_of_odd"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

781 
val nat_number_of_Pls = thm"nat_number_of_Pls"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

782 
val nat_number_of_Min = thm"nat_number_of_Min"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

783 
val nat_number_of_BIT_True = thm"nat_number_of_BIT_True"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

784 
val nat_number_of_BIT_False = thm"nat_number_of_BIT_False"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

785 
val Let_Suc = thm"Let_Suc"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

786 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

787 
val nat_number = thms"nat_number"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

788 

14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

789 
val nat_number_of_add_left = thm"nat_number_of_add_left"; 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14417
diff
changeset

790 
val nat_number_of_mult_left = thm"nat_number_of_mult_left"; 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

791 
val left_add_mult_distrib = thm"left_add_mult_distrib"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

792 
val nat_diff_add_eq1 = thm"nat_diff_add_eq1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

793 
val nat_diff_add_eq2 = thm"nat_diff_add_eq2"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

794 
val nat_eq_add_iff1 = thm"nat_eq_add_iff1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

795 
val nat_eq_add_iff2 = thm"nat_eq_add_iff2"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

796 
val nat_less_add_iff1 = thm"nat_less_add_iff1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

797 
val nat_less_add_iff2 = thm"nat_less_add_iff2"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

798 
val nat_le_add_iff1 = thm"nat_le_add_iff1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

799 
val nat_le_add_iff2 = thm"nat_le_add_iff2"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

800 
val nat_mult_le_cancel1 = thm"nat_mult_le_cancel1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

801 
val nat_mult_less_cancel1 = thm"nat_mult_less_cancel1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

802 
val nat_mult_eq_cancel1 = thm"nat_mult_eq_cancel1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

803 
val nat_mult_div_cancel1 = thm"nat_mult_div_cancel1"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

804 
val nat_mult_le_cancel_disj = thm"nat_mult_le_cancel_disj"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

805 
val nat_mult_less_cancel_disj = thm"nat_mult_less_cancel_disj"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

806 
val nat_mult_eq_cancel_disj = thm"nat_mult_eq_cancel_disj"; 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

807 
val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj"; 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

808 

79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

809 
val power_minus_even = thm"power_minus_even"; 
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14288
diff
changeset

810 
val zero_le_even_power = thm"zero_le_even_power"; 
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

811 
*} 
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

812 

e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset

813 

12440  814 
subsection {* Configuration of the code generator *} 
815 

12933
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

816 
ML {* 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

817 
infix 7 `*; 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

818 
infix 6 `+; 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

819 

b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

820 
val op `* = op * : int * int > int; 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

821 
val op `+ = op + : int * int > int; 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

822 
val `~ = ~ : int > int; 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

823 
*} 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

824 

12440  825 
types_code 
826 
"int" ("int") 

827 

14194
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

828 
constdefs 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

829 
int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

830 
"int_aux i n == (i + int n)" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

831 
nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

832 
"nat_aux n i == (n + nat i)" 
12440  833 

14194
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

834 
lemma [code]: 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

835 
"int_aux i 0 = i" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

836 
"int_aux i (Suc n) = int_aux (i + 1) n"  {* tail recursive *} 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

837 
"int n = int_aux 0 n" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

838 
by (simp add: int_aux_def)+ 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

839 

8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

840 
lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i  1))" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

841 
by (simp add: nat_aux_def Suc_nat_eq_nat_zadd1)  {* tail recursive *} 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

842 
lemma [code]: "nat i = nat_aux 0 i" 
8953b566dfed
Improved efficiency of code generated for functions int and nat.
berghofe
parents:
13491
diff
changeset

843 
by (simp add: nat_aux_def) 
12440  844 

845 
consts_code 

846 
"0" :: "int" ("0") 

847 
"1" :: "int" ("1") 

12933
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

848 
"uminus" :: "int => int" ("`~") 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

849 
"op +" :: "int => int => int" ("(_ `+/ _)") 
b85c62c4e826
Introduced variants of operators + * ~ constrained to type int
berghofe
parents:
12838
diff
changeset

850 
"op *" :: "int => int => int" ("(_ `*/ _)") 
15440  851 
(* Fails for 0: 
15129
fbf90acc5bf4
Replaced `div and `mod in consts_code section by div and mod.
berghofe
parents:
15013
diff
changeset

852 
"op div" :: "int => int => int" ("(_ div/ _)") 
fbf90acc5bf4
Replaced `div and `mod in consts_code section by div and mod.
berghofe
parents:
15013
diff
changeset

853 
"op mod" :: "int => int => int" ("(_ mod/ _)") 
15440  854 
*) 
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

855 
"op <" :: "int => int => bool" ("(_ </ _)") 
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset

856 
"op <=" :: "int => int => bool" ("(_ <=/ _)") 
12440  857 
"neg" ("(_ < 0)") 
858 

14417  859 
ML {* 
860 
fun number_of_codegen thy gr s b (Const ("Numeral.number_of", 

861 
Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) = 

862 
(Some (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin))) 

863 
handle TERM _ => None) 

864 
 number_of_codegen thy gr s b (Const ("Numeral.number_of", 

865 
Type ("fun", [_, Type ("nat", [])])) $ bin) = 

866 
Some (Codegen.invoke_codegen thy s b (gr, 

867 
Const ("IntDef.nat", HOLogic.intT > HOLogic.natT) $ 

868 
(Const ("Numeral.number_of", HOLogic.binT > HOLogic.intT) $ bin))) 

869 
 number_of_codegen _ _ _ _ _ = None; 

870 
*} 

871 

872 
setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} 

873 

7032  874 
end 