author  paulson 
Wed, 08 Sep 1999 15:40:39 +0200  
changeset 7517  bad2f36810e1 
parent 7074  e0730ffaafcc 
child 7549  1dcf2a7a2b5b 
permissions  rwrr 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

1 
(* Title: HOL/Integ/Bin.ML 
7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

2 
ID: $Id$ 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

3 
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory 
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

4 
David Spelt, University of Twente 
6060  5 
Tobias Nipkow, Technical University Munich 
1632  6 
Copyright 1994 University of Cambridge 
6060  7 
Copyright 1996 University of Twente 
8 
Copyright 1999 TU Munich 

1632  9 

6060  10 
Arithmetic on binary integers; 
11 
decision procedure for linear arithmetic. 

1632  12 
*) 
13 

14 
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) 

15 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

16 
Goal "NCons Pls False = Pls"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

17 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

18 
qed "NCons_Pls_0"; 
1632  19 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

20 
Goal "NCons Pls True = Pls BIT True"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

21 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

22 
qed "NCons_Pls_1"; 
1632  23 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

24 
Goal "NCons Min False = Min BIT False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

25 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

26 
qed "NCons_Min_0"; 
1632  27 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

28 
Goal "NCons Min True = Min"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

29 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

30 
qed "NCons_Min_1"; 
1632  31 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

32 
Goal "bin_succ(w BIT True) = (bin_succ w) BIT False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

33 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

34 
qed "bin_succ_1"; 
1632  35 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

36 
Goal "bin_succ(w BIT False) = NCons w True"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

37 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

38 
qed "bin_succ_0"; 
1632  39 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

40 
Goal "bin_pred(w BIT True) = NCons w False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

41 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

42 
qed "bin_pred_1"; 
1632  43 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

44 
Goal "bin_pred(w BIT False) = (bin_pred w) BIT True"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

45 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

46 
qed "bin_pred_0"; 
1632  47 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

48 
Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

49 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

50 
qed "bin_minus_1"; 
1632  51 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

52 
Goal "bin_minus(w BIT False) = (bin_minus w) BIT False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

53 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

54 
qed "bin_minus_0"; 
1632  55 

5491  56 

1632  57 
(*** bin_add: binary addition ***) 
58 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

59 
Goal "bin_add (v BIT True) (w BIT True) = \ 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

60 
\ NCons (bin_add v (bin_succ w)) False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

61 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

62 
qed "bin_add_BIT_11"; 
1632  63 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

64 
Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

65 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

66 
qed "bin_add_BIT_10"; 
1632  67 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

68 
Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

69 
by Auto_tac; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

70 
qed "bin_add_BIT_0"; 
1632  71 

5551  72 
Goal "bin_add w Pls = w"; 
73 
by (induct_tac "w" 1); 

74 
by Auto_tac; 

75 
qed "bin_add_Pls_right"; 

1632  76 

7517
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset

77 
Goal "bin_add w Min = bin_pred w"; 
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset

78 
by (induct_tac "w" 1); 
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset

79 
by Auto_tac; 
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset

80 
qed "bin_add_Min_right"; 
1632  81 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

82 
Goal "bin_add (v BIT x) (w BIT y) = \ 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

83 
\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

84 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

85 
qed "bin_add_BIT_BIT"; 
1632  86 

87 

6036  88 
(*** bin_mult: binary multiplication ***) 
1632  89 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

90 
Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

91 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

92 
qed "bin_mult_1"; 
1632  93 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

94 
Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

95 
by (Simp_tac 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

96 
qed "bin_mult_0"; 
1632  97 

98 

99 
(**** The carry/borrow functions, bin_succ and bin_pred ****) 

100 

101 

6910  102 
(**** number_of ****) 
1632  103 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

104 
Goal "number_of(NCons w b) = (number_of(w BIT b)::int)"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

105 
by (induct_tac "w" 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

106 
by (ALLGOALS Asm_simp_tac); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

107 
qed "number_of_NCons"; 
1632  108 

6910  109 
Addsimps [number_of_NCons]; 
1632  110 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

111 
Goal "number_of(bin_succ w) = int 1 + number_of w"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

112 
by (induct_tac "w" 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

113 
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

114 
qed "number_of_succ"; 
5491  115 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

116 
Goal "number_of(bin_pred w) =  (int 1) + number_of w"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

117 
by (induct_tac "w" 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

118 
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

119 
qed "number_of_pred"; 
1632  120 

6910  121 
Goal "number_of(bin_minus w) = ( (number_of w)::int)"; 
122 
by (induct_tac "w" 1); 

5491  123 
by (Simp_tac 1); 
124 
by (Simp_tac 1); 

125 
by (asm_simp_tac (simpset() 

5551  126 
delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] 
6910  127 
addsimps [number_of_succ,number_of_pred, 
5491  128 
zadd_assoc]) 1); 
6910  129 
qed "number_of_minus"; 
1632  130 

131 

6910  132 
val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred]; 
1632  133 

6036  134 
(*This proof is complicated by the mutual recursion*) 
6910  135 
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)"; 
5184  136 
by (induct_tac "v" 1); 
4686  137 
by (simp_tac (simpset() addsimps bin_add_simps) 1); 
138 
by (simp_tac (simpset() addsimps bin_add_simps) 1); 

1632  139 
by (rtac allI 1); 
5184  140 
by (induct_tac "w" 1); 
5540  141 
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); 
6910  142 
qed_spec_mp "number_of_add"; 
1632  143 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

144 

5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

145 
(*Subtraction*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

146 
Goalw [zdiff_def] 
6910  147 
"number_of v  number_of w = (number_of(bin_add v (bin_minus w))::int)"; 
148 
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1); 

149 
qed "diff_number_of_eq"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

150 

6910  151 
val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add]; 
1632  152 

6910  153 
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)"; 
5184  154 
by (induct_tac "v" 1); 
4686  155 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 
156 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 

5491  157 
by (asm_simp_tac 
5540  158 
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); 
6910  159 
qed "number_of_mult"; 
5491  160 

1632  161 

6941  162 
(*The correctness of shifting. But it doesn't seem to give a measurable 
163 
speedup.*) 

164 
Goal "(#2::int) * number_of w = number_of (w BIT False)"; 

165 
by (induct_tac "w" 1); 

166 
by (ALLGOALS (asm_simp_tac 

167 
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac))); 

168 
qed "double_number_of_BIT"; 

169 

170 

5491  171 
(** Simplification rules with integer constants **) 
172 

6910  173 
Goal "#0 + z = (z::int)"; 
5491  174 
by (Simp_tac 1); 
175 
qed "zadd_0"; 

176 

6910  177 
Goal "z + #0 = (z::int)"; 
5491  178 
by (Simp_tac 1); 
179 
qed "zadd_0_right"; 

180 

5592  181 
Addsimps [zadd_0, zadd_0_right]; 
182 

183 

184 
(** Converting simple cases of (int n) to numerals **) 

5491  185 

5592  186 
(*int 0 = #0 *) 
6910  187 
bind_thm ("int_0", number_of_Pls RS sym); 
5491  188 

5592  189 
Goal "int (Suc n) = #1 + int n"; 
190 
by (simp_tac (simpset() addsimps [zadd_int]) 1); 

191 
qed "int_Suc"; 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

192 

6910  193 
Goal " (#0) = (#0::int)"; 
5491  194 
by (Simp_tac 1); 
195 
qed "zminus_0"; 

196 

197 
Addsimps [zminus_0]; 

198 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

199 

6910  200 
Goal "(#0::int)  x = x"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

201 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

202 
qed "zdiff0"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

203 

6910  204 
Goal "x  (#0::int) = x"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

205 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

206 
qed "zdiff0_right"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

207 

6910  208 
Goal "x  x = (#0::int)"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

209 
by (simp_tac (simpset() addsimps [zdiff_def]) 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

210 
qed "zdiff_self"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

211 

a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

212 
Addsimps [zdiff0, zdiff0_right, zdiff_self]; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

213 

6917  214 

215 
(** Special simplification, for constants only **) 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

216 

6917  217 
fun inst x t = read_instantiate_sg (sign_of Bin.thy) [(x,t)]; 
218 

7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

219 
(*Distributive laws for literals*) 
6917  220 
Addsimps (map (inst "w" "number_of ?v") 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

221 
[zadd_zmult_distrib, zadd_zmult_distrib2, 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

222 
zdiff_zmult_distrib, zdiff_zmult_distrib2]); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

223 

6917  224 
Addsimps (map (inst "x" "number_of ?v") 
225 
[zless_zminus, zle_zminus, equation_zminus]); 

226 
Addsimps (map (inst "y" "number_of ?v") 

227 
[zminus_zless, zminus_zle, zminus_equation]); 

228 

7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

229 
(*Moving negation out of products*) 
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

230 
Addsimps [zmult_zminus, zmult_zminus_right]; 
6917  231 

6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

232 
(** Specialcase simplification for small constants **) 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

233 

6910  234 
Goal "#0 * z = (#0::int)"; 
5491  235 
by (Simp_tac 1); 
236 
qed "zmult_0"; 

237 

6910  238 
Goal "z * #0 = (#0::int)"; 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

239 
by (Simp_tac 1); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

240 
qed "zmult_0_right"; 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

241 

6910  242 
Goal "#1 * z = (z::int)"; 
5491  243 
by (Simp_tac 1); 
244 
qed "zmult_1"; 

245 

6910  246 
Goal "z * #1 = (z::int)"; 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

247 
by (Simp_tac 1); 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

248 
qed "zmult_1_right"; 
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

249 

6917  250 
Goal "#1 * z = (z::int)"; 
251 
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1); 

252 
qed "zmult_minus1"; 

253 

254 
Goal "z * #1 = (z::int)"; 

255 
by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1); 

256 
qed "zmult_minus1_right"; 

257 

258 
Addsimps [zmult_0, zmult_0_right, 

259 
zmult_1, zmult_1_right, 

260 
zmult_minus1, zmult_minus1_right]; 

261 

262 
(*For specialist use: NOT as default simprules*) 

6910  263 
Goal "#2 * z = (z+z::int)"; 
5491  264 
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); 
265 
qed "zmult_2"; 

266 

6910  267 
Goal "z * #2 = (z+z::int)"; 
5491  268 
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); 
269 
qed "zmult_2_right"; 

270 

6917  271 

272 
(** Inequality reasoning **) 

5491  273 

6989  274 
Goal "(m*n = (#0::int)) = (m = #0  n = #0)"; 
275 
by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1); 

276 
qed "zmult_eq_0_iff"; 

277 

6910  278 
Goal "(w < z + (#1::int)) = (w<z  w=z)"; 
5592  279 
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1); 
5491  280 
qed "zless_add1_eq"; 
281 

6910  282 
Goal "(w + (#1::int) <= z) = (w<z)"; 
5592  283 
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1); 
5491  284 
qed "add1_zle_eq"; 
6997  285 

286 
Goal "((#1::int) + w <= z) = (w<z)"; 

287 
by (stac zadd_commute 1); 

288 
by (rtac add1_zle_eq 1); 

289 
qed "add1_left_zle_eq"; 

5491  290 

5540  291 
Goal "neg x = (x < #0)"; 
6917  292 
by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1); 
5540  293 
qed "neg_eq_less_0"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

294 

6989  295 
Goal "(~neg x) = (#0 <= x)"; 
6917  296 
by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); 
5540  297 
qed "not_neg_eq_ge_0"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

298 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

299 
Goal "#0 <= int m"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

300 
by (Simp_tac 1); 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

301 
qed "zero_zle_int"; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

302 
AddIffs [zero_zle_int]; 
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

303 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

304 

5747  305 
(** Needed because (int 0) rewrites to #0. 
306 
Can these be generalized without evaluating large numbers?**) 

307 

308 
Goal "~ (int k < #0)"; 

309 
by (Simp_tac 1); 

310 
qed "int_less_0_conv"; 

311 

312 
Goal "(int k <= #0) = (k=0)"; 

313 
by (Simp_tac 1); 

314 
qed "int_le_0_conv"; 

315 

316 
Goal "(int k = #0) = (k=0)"; 

317 
by (Simp_tac 1); 

318 
qed "int_eq_0_conv"; 

319 

320 
Goal "(#0 = int k) = (k=0)"; 

321 
by Auto_tac; 

322 
qed "int_eq_0_conv'"; 

323 

324 
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv']; 

325 

326 

5491  327 
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) 
328 

329 
(** Equals (=) **) 

1632  330 

5491  331 
Goalw [iszero_def] 
6997  332 
"((number_of x::int) = number_of y) = \ 
333 
\ iszero (number_of (bin_add x (bin_minus y)))"; 

5491  334 
by (simp_tac (simpset() addsimps 
6910  335 
(zcompare_rls @ [number_of_add, number_of_minus])) 1); 
336 
qed "eq_number_of_eq"; 

5491  337 

6910  338 
Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
5491  339 
by (Simp_tac 1); 
6910  340 
qed "iszero_number_of_Pls"; 
5491  341 

6910  342 
Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
5491  343 
by (Simp_tac 1); 
6910  344 
qed "nonzero_number_of_Min"; 
5491  345 

346 
Goalw [iszero_def] 

6910  347 
"iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
5491  348 
by (Simp_tac 1); 
6910  349 
by (int_case_tac "number_of w" 1); 
5491  350 
by (ALLGOALS (asm_simp_tac 
5540  351 
(simpset() addsimps zcompare_rls @ 
352 
[zminus_zadd_distrib RS sym, 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

353 
zadd_int]))); 
6910  354 
qed "iszero_number_of_BIT"; 
5491  355 

6910  356 
Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
357 
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 

358 
qed "iszero_number_of_0"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

359 

6910  360 
Goal "~ iszero (number_of (w BIT True)::int)"; 
361 
by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 

362 
qed "iszero_number_of_1"; 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

363 

5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

364 

5491  365 

366 
(** Lessthan (<) **) 

367 

368 
Goalw [zless_def,zdiff_def] 

6910  369 
"(number_of x::int) < number_of y \ 
370 
\ = neg (number_of (bin_add x (bin_minus y)))"; 

5491  371 
by (simp_tac (simpset() addsimps bin_mult_simps) 1); 
6910  372 
qed "less_number_of_eq_neg"; 
5491  373 

6910  374 
Goal "~ neg (number_of Pls)"; 
5491  375 
by (Simp_tac 1); 
6910  376 
qed "not_neg_number_of_Pls"; 
5491  377 

6910  378 
Goal "neg (number_of Min)"; 
5491  379 
by (Simp_tac 1); 
6910  380 
qed "neg_number_of_Min"; 
5491  381 

6910  382 
Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
5491  383 
by (Asm_simp_tac 1); 
6910  384 
by (int_case_tac "number_of w" 1); 
5491  385 
by (ALLGOALS (asm_simp_tac 
6917  386 
(simpset() addsimps [zadd_int, neg_eq_less_int0, 
5540  387 
symmetric zdiff_def] @ zcompare_rls))); 
6910  388 
qed "neg_number_of_BIT"; 
5491  389 

390 

391 
(** Lessthanorequals (<=) **) 

392 

7033  393 
Goal "(number_of x <= (number_of y::int)) = \ 
394 
\ (~ number_of y < (number_of x::int))"; 

395 
by (rtac (linorder_not_less RS sym) 1); 

6910  396 
qed "le_number_of_eq_not_less"; 
5491  397 

5540  398 
(*Delete the original rewrites, with their clumsy conditional expressions*) 
5551  399 
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
400 
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; 

5491  401 

402 
(*Hide the binary representation of integer constants*) 

6910  403 
Delsimps [number_of_Pls, number_of_Min, number_of_BIT]; 
5491  404 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

405 
(*simplification of arithmetic operations on integer constants*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

406 
val bin_arith_extra_simps = 
6910  407 
[number_of_add RS sym, 
408 
number_of_minus RS sym, 

409 
number_of_mult RS sym, 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

410 
bin_succ_1, bin_succ_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

411 
bin_pred_1, bin_pred_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

412 
bin_minus_1, bin_minus_0, 
7517
bad2f36810e1
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
paulson
parents:
7074
diff
changeset

413 
bin_add_Pls_right, bin_add_Min_right, 
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

414 
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, 
6910  415 
diff_number_of_eq, 
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

416 
bin_mult_1, bin_mult_0, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

417 
NCons_Pls_0, NCons_Pls_1, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

418 
NCons_Min_0, NCons_Min_1, NCons_BIT]; 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

419 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

420 
(*For making a minimal simpset, one must include these default simprules 
6910  421 
of thy. Also include simp_thms, or at least (~False)=True*) 
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

422 
val bin_arith_simps = 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

423 
[bin_pred_Pls, bin_pred_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

424 
bin_succ_Pls, bin_succ_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

425 
bin_add_Pls, bin_add_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

426 
bin_minus_Pls, bin_minus_Min, 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

427 
bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps; 
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

428 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

429 
(*Simplification of relational operations*) 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

430 
val bin_rel_simps = 
6910  431 
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min, 
432 
iszero_number_of_0, iszero_number_of_1, 

433 
less_number_of_eq_neg, 

434 
not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT, 

435 
le_number_of_eq_not_less]; 

2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset

436 

5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

437 
Addsimps bin_arith_extra_simps; 
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset

438 
Addsimps bin_rel_simps; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

439 

6997  440 

441 
(** Constant folding inside parentheses **) 

442 

443 
Goal "number_of v + (number_of w + c) = number_of(bin_add v w) + (c::int)"; 

444 
by (stac (zadd_assoc RS sym) 1); 

445 
by (stac number_of_add 1); 

446 
by Auto_tac; 

447 
qed "nested_number_of_add"; 

448 

449 
Goalw [zdiff_def] 

450 
"number_of v + (number_of w  c) = number_of(bin_add v w)  (c::int)"; 

451 
by (rtac nested_number_of_add 1); 

452 
qed "nested_diff1_number_of_add"; 

453 

454 
Goal "number_of v + (c  number_of w) = \ 

455 
\ number_of (bin_add v (bin_minus w)) + (c::int)"; 

456 
by (stac (diff_number_of_eq RS sym) 1); 

457 
by Auto_tac; 

458 
qed "nested_diff2_number_of_add"; 

459 

460 
Goal "number_of v * (number_of w * c) = number_of(bin_mult v w) * (c::int)"; 

461 
by (stac (zmult_assoc RS sym) 1); 

462 
by (stac number_of_mult 1); 

463 
by Auto_tac; 

464 
qed "nested_number_of_mult"; 

465 
Addsimps [nested_number_of_add, nested_diff1_number_of_add, 

466 
nested_diff2_number_of_add, nested_number_of_mult]; 

467 

468 

469 

6060  470 
(**) 
471 
(* Linear arithmetic *) 

472 
(**) 

473 

474 
(* 

475 
Instantiation of the generic linear arithmetic package for int. 

476 
FIXME: multiplication with constants (eg #2 * i) does not work yet. 

477 
Solution: the cancellation simprocs in Int_Cancel should be able to deal with 

478 
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should 

479 
include rules for turning multiplication with constants into addition. 

480 
(The latter option is very inefficient!) 

481 
*) 

482 

6128  483 
structure Int_LA_Data(*: LIN_ARITH_DATA*) = 
6060  484 
struct 
6101  485 

6128  486 
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2]; 
6060  487 

488 
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) 

489 
 Some n => (overwrite(p,(t,n+m:int)), i)); 

490 

491 
(* Turn term into list of summand * multiplicity plus a constant *) 

492 
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) 

493 
 poly(Const("op ",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi)) 

494 
 poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) 

6910  495 
 poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) = 
496 
(poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi)) 

497 
 poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = 

498 
((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i))) 

6060  499 
 poly x = add_atom x; 
500 

6128  501 
fun decomp2(rel,lhs,rhs) = 
6060  502 
let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) 
503 
in case rel of 

504 
"op <" => Some(p,i,"<",q,j) 

505 
 "op <=" => Some(p,i,"<=",q,j) 

506 
 "op =" => Some(p,i,"=",q,j) 

507 
 _ => None 

508 
end; 

509 

6128  510 
val intT = Type("IntDef.int",[]); 
511 
fun iib T = T = ([intT,intT] > HOLogic.boolT); 

6060  512 

6128  513 
fun decomp1(T,xxx) = 
514 
if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx); 

515 

516 
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs)) 

6060  517 
 decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = 
6128  518 
Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs))) 
6060  519 
 decomp _ = None 
520 

521 
(* reduce contradictory <= to False *) 

522 
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0]; 

523 

6128  524 
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules 
6060  525 
addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; 
526 

527 
val simp = simplify cancel_sums_ss; 

528 

6128  529 
val add_mono_thms = Nat_LA_Data.add_mono_thms @ 
530 
map (fn s => prove_goal Int.thy s 

531 
(fn prems => [cut_facts_tac prems 1, 

532 
asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) 

533 
["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", 

534 
"(i = j) & (k <= l) ==> i + k <= j + (l::int)", 

535 
"(i <= j) & (k = l) ==> i + k <= j + (l::int)", 

536 
"(i = j) & (k = l) ==> i + k = j + (l::int)" 

537 
]; 

6060  538 

539 
end; 

540 

6128  541 
(* Update parameters of arithmetic prover *) 
542 
LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms; 

543 
LA_Data_Ref.lessD := Int_LA_Data.lessD; 

544 
LA_Data_Ref.decomp := Int_LA_Data.decomp; 

545 
LA_Data_Ref.simp := Int_LA_Data.simp; 

546 

6060  547 

6128  548 
val int_arith_simproc_pats = 
6394  549 
map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT)) 
6128  550 
["(m::int) < n","(m::int) <= n", "(m::int) = n"]; 
6060  551 

6128  552 
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats 
553 
Fast_Arith.lin_arith_prover; 

554 

555 
Addsimprocs [fast_int_arith_simproc]; 

6060  556 

557 
(* FIXME: K true should be replaced by a sensible test to speed things up 

558 
in case there are lots of irrelevant terms involved. 

6157  559 

6128  560 
val arith_tac = 
561 
refute_tac (K true) (REPEAT o split_tac[nat_diff_split]) 

562 
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac); 

6157  563 
*) 
6060  564 

565 
(* Some test data 

566 
Goal "!!a::int. [ a <= b; c <= d; x+y<z ] ==> a+c <= b+d"; 

6301  567 
by (fast_arith_tac 1); 
6060  568 
Goal "!!a::int. [ a < b; c < d ] ==> ad+ #2 <= b+(c)"; 
6301  569 
by (fast_arith_tac 1); 
6060  570 
Goal "!!a::int. [ a < b; c < d ] ==> a+c+ #1 < b+d"; 
6301  571 
by (fast_arith_tac 1); 
6060  572 
Goal "!!a::int. [ a <= b; b+b <= c ] ==> a+a <= c"; 
6301  573 
by (fast_arith_tac 1); 
6060  574 
Goal "!!a::int. [ a+b <= i+j; a<=b; i<=j ] \ 
575 
\ ==> a+a <= j+j"; 

6301  576 
by (fast_arith_tac 1); 
6060  577 
Goal "!!a::int. [ a+b < i+j; a<b; i<j ] \ 
578 
\ ==> a+a   #1 < j+j  #3"; 

6301  579 
by (fast_arith_tac 1); 
6060  580 
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k > a+a+a <= k+k+k"; 
6301  581 
by (arith_tac 1); 
6060  582 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
583 
\ ==> a <= l"; 

6301  584 
by (fast_arith_tac 1); 
6060  585 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
586 
\ ==> a+a+a+a <= l+l+l+l"; 

6301  587 
by (fast_arith_tac 1); 
6060  588 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
589 
\ ==> a+a+a+a+a <= l+l+l+l+i"; 

6301  590 
by (fast_arith_tac 1); 
6060  591 
Goal "!!a::int. [ a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l ] \ 
592 
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; 

6301  593 
by (fast_arith_tac 1); 
6060  594 
*) 
595 

596 
(**) 

597 
(* End of linear arithmetic *) 

598 
(**) 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

599 

5592  600 
(** Simplification of arithmetic when nested to the right **) 
601 

6910  602 
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"; 
5592  603 
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); 
6910  604 
qed "add_number_of_left"; 
5592  605 

6910  606 
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"; 
5592  607 
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); 
6910  608 
qed "mult_number_of_left"; 
5592  609 

6910  610 
Addsimps [add_number_of_left, mult_number_of_left]; 
5592  611 

5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

612 
(** Simplification of inequalities involving numerical constants **) 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

613 

6910  614 
Goal "(w <= z + (#1::int)) = (w<=z  w = z + (#1::int))"; 
6301  615 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

616 
qed "zle_add1_eq"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

617 

6910  618 
Goal "(w <= z  (#1::int)) = (w<(z::int))"; 
6301  619 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

620 
qed "zle_diff1_eq"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

621 
Addsimps [zle_diff1_eq]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

622 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

623 
(*2nd premise can be proved automatically if v is a literal*) 
6910  624 
Goal "[ w <= z; #0 <= v ] ==> w <= z + (v::int)"; 
6301  625 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

626 
qed "zle_imp_zle_zadd"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

627 

6910  628 
Goal "w <= z ==> w <= z + (#1::int)"; 
6301  629 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

630 
qed "zle_imp_zle_zadd1"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

631 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

632 
(*2nd premise can be proved automatically if v is a literal*) 
6910  633 
Goal "[ w < z; #0 <= v ] ==> w < z + (v::int)"; 
6301  634 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

635 
qed "zless_imp_zless_zadd"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

636 

6910  637 
Goal "w < z ==> w < z + (#1::int)"; 
6301  638 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

639 
qed "zless_imp_zless_zadd1"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

640 

6910  641 
Goal "(w < z + #1) = (w<=(z::int))"; 
6301  642 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

643 
qed "zle_add1_eq_le"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

644 
Addsimps [zle_add1_eq_le]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

645 

6910  646 
Goal "(z = z + w) = (w = (#0::int))"; 
6301  647 
by (arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

648 
qed "zadd_left_cancel0"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

649 
Addsimps [zadd_left_cancel0]; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

650 

ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

651 
(*LOOPS as a simprule!*) 
6910  652 
Goal "[ w + v < z; #0 <= v ] ==> w < (z::int)"; 
6301  653 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

654 
qed "zless_zadd_imp_zless"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

655 

5540  656 
(*LOOPS as a simprule! Analogous to Suc_lessD*) 
6910  657 
Goal "w + #1 < z ==> w < (z::int)"; 
6301  658 
by (fast_arith_tac 1); 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

659 
qed "zless_zadd1_imp_zless"; 
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

660 

6910  661 
Goal "w + #1 = w  (#1::int)"; 
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

662 
by (Simp_tac 1); 
5551  663 
qed "zplus_minus1_conv"; 
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset

664 

5551  665 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

666 
(*** nat ***) 
5551  667 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

668 
Goal "#0 <= z ==> int (nat z) = z"; 
5551  669 
by (asm_full_simp_tac 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

670 
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

671 
qed "nat_0_le"; 
5551  672 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

673 
Goal "z <= #0 ==> nat z = 0"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

674 
by (case_tac "z = #0" 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

675 
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

676 
by (asm_full_simp_tac 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

677 
(simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

678 
qed "nat_le_0"; 
5551  679 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

680 
Addsimps [nat_0_le, nat_le_0]; 
5551  681 

7033  682 
val [major,minor] = Goal "[ #0 <= z; !!m. z = int m ==> P ] ==> P"; 
683 
by (rtac (major RS nat_0_le RS sym RS minor) 1); 

684 
qed "nonneg_eq_int"; 

685 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

686 
Goal "#0 <= w ==> (nat w = m) = (w = int m)"; 
5551  687 
by Auto_tac; 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

688 
qed "nat_eq_iff"; 
5551  689 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

690 
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; 
5551  691 
by (rtac iffI 1); 
692 
by (asm_full_simp_tac 

5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset

693 
(simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

694 
by (etac (nat_0_le RS subst) 1); 
5551  695 
by (Simp_tac 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

696 
qed "nat_less_iff"; 
5551  697 

5747  698 

6716
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

699 
(*Users don't want to see (int 0), int(Suc 0) or w +  z*) 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

700 
Addsimps [int_0, int_Suc, symmetric zdiff_def]; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

701 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

702 
Goal "nat #0 = 0"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

703 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

704 
qed "nat_0"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

705 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

706 
Goal "nat #1 = 1"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

707 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

708 
qed "nat_1"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

709 

87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

710 
Goal "nat #2 = 2"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

711 
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

712 
qed "nat_2"; 
87c750df8888
Better simplification of (nat #0), (int (Suc 0)), etc
paulson
parents:
6394
diff
changeset

713 

5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

714 
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; 
5551  715 
by (case_tac "neg z" 1); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

716 
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); 
5551  717 
by (auto_tac (claset() addIs [zless_trans], 
5747  718 
simpset() addsimps [neg_eq_less_0, zle_def])); 
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset

719 
qed "nat_less_eq_zless"; 
5747  720 

7008
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

721 
Goal "#0 < w  #0 <= z ==> (nat w <= nat z) = (w<=z)"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

722 
by (auto_tac (claset(), 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

723 
simpset() addsimps [linorder_not_less RS sym, 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

724 
zless_nat_conj])); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

725 
qed "nat_le_eq_zle"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

726 

6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

727 
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

728 
Goal "n<=m > int m  int n = int (mn)"; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

729 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

730 
by Auto_tac; 
6def5ce146e2
qed_goal > Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson
parents:
6997
diff
changeset

731 
qed_spec_mp "zdiff_int"; 
6838
941c4f70db91
rewrite rules to distribute CONSTANT multiplication over sum and difference;
paulson
parents:
6716
diff
changeset

732 

6941  733 

734 
(** Products of signs **) 

735 

736 
Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)"; 

737 
by Auto_tac; 

738 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); 

739 
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); 

740 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

741 
by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1_neg], 
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

742 
simpset()addsimps [order_le_less, zmult_commute]) 1); 
6941  743 
qed "neg_imp_zmult_pos_iff"; 
744 

745 
Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)"; 

746 
by Auto_tac; 

747 
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); 

748 
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); 

749 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

750 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], 

751 
simpset() addsimps [order_le_less]) 1); 

752 
qed "neg_imp_zmult_neg_iff"; 

753 

754 
Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)"; 

755 
by Auto_tac; 

756 
by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2); 

757 
by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1); 

758 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

759 
by (force_tac (claset() addDs [zmult_zless_mono1], 

760 
simpset() addsimps [order_le_less]) 1); 

761 
qed "pos_imp_zmult_neg_iff"; 

762 

763 
Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)"; 

764 
by Auto_tac; 

765 
by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2); 

766 
by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1); 

767 
by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1); 

7074
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

768 
by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1], 
e0730ffaafcc
zadd_ac and zmult_ac are no longer included by default
paulson
parents:
7033
diff
changeset

769 
simpset() addsimps [order_le_less, zmult_commute]) 1); 
6941  770 
qed "pos_imp_zmult_pos_iff"; 
6973  771 

772 
(** <= versions of the theorems above **) 

773 

774 
Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)"; 

775 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

776 
neg_imp_zmult_pos_iff]) 1); 

777 
qed "neg_imp_zmult_nonpos_iff"; 

778 

779 
Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)"; 

780 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

781 
neg_imp_zmult_neg_iff]) 1); 

782 
qed "neg_imp_zmult_nonneg_iff"; 

783 

784 
Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)"; 

785 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

786 
pos_imp_zmult_pos_iff]) 1); 

787 
qed "pos_imp_zmult_nonpos_iff"; 

788 

789 
Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)"; 

790 
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 

791 
pos_imp_zmult_neg_iff]) 1); 

792 
qed "pos_imp_zmult_nonneg_iff"; 