author | wenzelm |
Fri, 24 Jul 1998 17:55:57 +0200 | |
changeset 5199 | be986f7a6def |
parent 5184 | 9b8547a9496a |
child 5224 | 8d132a14e722 |
permissions | -rw-r--r-- |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
1 |
(* Title: HOL/Integ/Bin.ML |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
2 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
3 |
David Spelt, University of Twente |
1632 | 4 |
Copyright 1994 University of Cambridge |
5 |
Copyright 1996 University of Twente |
|
6 |
||
7 |
Arithmetic on binary integers. |
|
8 |
*) |
|
9 |
||
10 |
open Bin; |
|
11 |
||
12 |
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
|
13 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
14 |
qed_goal "norm_Bcons_Plus_0" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
15 |
"norm_Bcons PlusSign False = PlusSign" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
16 |
(fn _ => [(Simp_tac 1)]); |
1632 | 17 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
18 |
qed_goal "norm_Bcons_Plus_1" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
19 |
"norm_Bcons PlusSign True = Bcons PlusSign True" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
20 |
(fn _ => [(Simp_tac 1)]); |
1632 | 21 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
22 |
qed_goal "norm_Bcons_Minus_0" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
23 |
"norm_Bcons MinusSign False = Bcons MinusSign False" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
24 |
(fn _ => [(Simp_tac 1)]); |
1632 | 25 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
26 |
qed_goal "norm_Bcons_Minus_1" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
27 |
"norm_Bcons MinusSign True = MinusSign" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
28 |
(fn _ => [(Simp_tac 1)]); |
1632 | 29 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
30 |
qed_goal "norm_Bcons_Bcons" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
31 |
"norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
32 |
(fn _ => [(Simp_tac 1)]); |
1632 | 33 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
34 |
qed_goal "bin_succ_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
35 |
"bin_succ(Bcons w True) = Bcons (bin_succ w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
36 |
(fn _ => [(Simp_tac 1)]); |
1632 | 37 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
38 |
qed_goal "bin_succ_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
39 |
"bin_succ(Bcons w False) = norm_Bcons w True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
40 |
(fn _ => [(Simp_tac 1)]); |
1632 | 41 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
42 |
qed_goal "bin_pred_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
43 |
"bin_pred(Bcons w True) = norm_Bcons w False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
44 |
(fn _ => [(Simp_tac 1)]); |
1632 | 45 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
46 |
qed_goal "bin_pred_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
47 |
"bin_pred(Bcons w False) = Bcons (bin_pred w) True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
48 |
(fn _ => [(Simp_tac 1)]); |
1632 | 49 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
50 |
qed_goal "bin_minus_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
51 |
"bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
52 |
(fn _ => [(Simp_tac 1)]); |
1632 | 53 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
54 |
qed_goal "bin_minus_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
55 |
"bin_minus(Bcons w False) = Bcons (bin_minus w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
56 |
(fn _ => [(Simp_tac 1)]); |
1632 | 57 |
|
58 |
(*** bin_add: binary addition ***) |
|
59 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
60 |
qed_goal "bin_add_Bcons_Bcons11" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
61 |
"bin_add (Bcons v True) (Bcons w True) = \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
62 |
\ norm_Bcons (bin_add v (bin_succ w)) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
63 |
(fn _ => [(Simp_tac 1)]); |
1632 | 64 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
65 |
qed_goal "bin_add_Bcons_Bcons10" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
66 |
"bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
67 |
(fn _ => [(Simp_tac 1)]); |
1632 | 68 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
69 |
val lemma = prove_goal HOL.thy "(False = (~P)) = P" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
70 |
(fn _ => [(Fast_tac 1)]); |
1632 | 71 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
72 |
qed_goal "bin_add_Bcons_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
73 |
"bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" |
4089 | 74 |
(fn _ => [(simp_tac (simpset() addsimps [lemma]) 1)]); |
1632 | 75 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
76 |
qed_goal "bin_add_Bcons_Plus" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
77 |
"bin_add (Bcons v x) PlusSign = Bcons v x" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
78 |
(fn _ => [(Simp_tac 1)]); |
1632 | 79 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
80 |
qed_goal "bin_add_Bcons_Minus" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
81 |
"bin_add (Bcons v x) MinusSign = bin_pred (Bcons v x)" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
82 |
(fn _ => [(Simp_tac 1)]); |
1632 | 83 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
84 |
qed_goal "bin_add_Bcons_Bcons" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
85 |
"bin_add (Bcons v x) (Bcons w y) = \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
86 |
\ norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
87 |
(fn _ => [(Simp_tac 1)]); |
1632 | 88 |
|
89 |
||
90 |
(*** bin_add: binary multiplication ***) |
|
91 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
92 |
qed_goal "bin_mult_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
93 |
"bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
94 |
(fn _ => [(Simp_tac 1)]); |
1632 | 95 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
96 |
qed_goal "bin_mult_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
97 |
"bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
98 |
(fn _ => [(Simp_tac 1)]); |
1632 | 99 |
|
100 |
||
101 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
102 |
||
103 |
||
104 |
(**** integ_of_bin ****) |
|
105 |
||
106 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
107 |
qed_goal "integ_of_bin_norm_Bcons" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
108 |
"integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)" |
5184 | 109 |
(fn _ =>[(induct_tac "w" 1), |
4686 | 110 |
(ALLGOALS Simp_tac) ]); |
1632 | 111 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
112 |
qed_goal "integ_of_bin_succ" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
113 |
"integ_of_bin(bin_succ w) = $#1 + integ_of_bin w" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
114 |
(fn _ =>[(rtac bin.induct 1), |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
115 |
(ALLGOALS(asm_simp_tac |
4686 | 116 |
(simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); |
1632 | 117 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
118 |
qed_goal "integ_of_bin_pred" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
119 |
"integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
120 |
(fn _ =>[(rtac bin.induct 1), |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
121 |
(ALLGOALS(asm_simp_tac |
4686 | 122 |
(simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); |
1632 | 123 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
124 |
qed_goal "integ_of_bin_minus" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
125 |
"integ_of_bin(bin_minus w) = $~ (integ_of_bin w)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
126 |
(fn _ =>[(rtac bin.induct 1), |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
127 |
(Simp_tac 1), |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
128 |
(Simp_tac 1), |
4686 | 129 |
(asm_simp_tac (simpset() |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
130 |
delsimps [pred_Plus,pred_Minus,pred_Bcons] |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
131 |
addsimps [integ_of_bin_succ,integ_of_bin_pred, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
132 |
zadd_assoc]) 1)]); |
1632 | 133 |
|
134 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
135 |
val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
136 |
bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
137 |
integ_of_bin_succ, integ_of_bin_pred, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
138 |
integ_of_bin_norm_Bcons]; |
1632 | 139 |
val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; |
140 |
||
5069 | 141 |
Goal |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
142 |
"! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
5184 | 143 |
by (induct_tac "v" 1); |
4686 | 144 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
145 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 146 |
by (rtac allI 1); |
5184 | 147 |
by (induct_tac "w" 1); |
4686 | 148 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1); |
149 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
|
1632 | 150 |
by (cut_inst_tac [("P","bool")] True_or_False 1); |
151 |
by (etac disjE 1); |
|
4686 | 152 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
153 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
|
1632 | 154 |
val integ_of_bin_add_lemma = result(); |
155 |
||
5069 | 156 |
Goal "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
1632 | 157 |
by (cut_facts_tac [integ_of_bin_add_lemma] 1); |
1894 | 158 |
by (Fast_tac 1); |
1632 | 159 |
qed "integ_of_bin_add"; |
160 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
161 |
val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
162 |
integ_of_bin_norm_Bcons]; |
1632 | 163 |
|
5069 | 164 |
Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
5184 | 165 |
by (induct_tac "v" 1); |
4686 | 166 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
167 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
1632 | 168 |
by (cut_inst_tac [("P","bool")] True_or_False 1); |
169 |
by (etac disjE 1); |
|
4686 | 170 |
by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2); |
171 |
by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
172 |
zadd_ac)) 1); |
1632 | 173 |
qed "integ_of_bin_mult"; |
174 |
||
175 |
||
176 |
Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons, |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
177 |
iob_Plus,iob_Minus,iob_Bcons, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
178 |
norm_Plus,norm_Minus,norm_Bcons]; |
1632 | 179 |
|
180 |
Addsimps [integ_of_bin_add RS sym, |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
181 |
integ_of_bin_minus RS sym, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
182 |
integ_of_bin_mult RS sym, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
183 |
bin_succ_Bcons1,bin_succ_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
184 |
bin_pred_Bcons1,bin_pred_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
185 |
bin_minus_Bcons1,bin_minus_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
186 |
bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
187 |
bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
188 |
bin_mult_Bcons1,bin_mult_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
189 |
norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
190 |
norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
191 |
norm_Bcons_Bcons]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
192 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
193 |
|
4195 | 194 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
195 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
196 |
Addsimps [zadd_assoc]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
197 |
|
5069 | 198 |
Goal |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
199 |
"(integ_of_bin x = integ_of_bin y) \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
200 |
\ = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
201 |
by (simp_tac (HOL_ss addsimps |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
202 |
[integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
203 |
by (rtac iffI 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
204 |
by (etac ssubst 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
205 |
by (rtac zadd_zminus_inverse 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
206 |
by (dres_inst_tac [("f","(% z. z + integ_of_bin y)")] arg_cong 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
207 |
by (asm_full_simp_tac |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
208 |
(HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
209 |
zadd_zminus_inverse2]) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
210 |
val iob_eq_eq_diff_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
211 |
|
5069 | 212 |
Goal "(integ_of_bin PlusSign = $# 0) = True"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
213 |
by (stac iob_Plus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
214 |
val iob_Plus_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
215 |
|
5069 | 216 |
Goal "(integ_of_bin MinusSign = $# 0) = False"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
217 |
by (stac iob_Minus 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
218 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
219 |
val iob_Minus_not_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
220 |
|
5069 | 221 |
Goal |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
222 |
"(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
223 |
by (stac iob_Bcons 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
224 |
by (case_tac "x" 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
225 |
by (ALLGOALS Asm_simp_tac); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
226 |
by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
227 |
by (ALLGOALS(int_case_tac "integ_of_bin w")); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
228 |
by (ALLGOALS(asm_simp_tac |
4089 | 229 |
(simpset() addsimps[zminus_zadd_distrib RS sym, |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
230 |
znat_add RS sym]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
231 |
by (rtac notI 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
232 |
by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
233 |
by (Asm_full_simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
234 |
val iob_Bcons_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
235 |
|
5069 | 236 |
Goalw [zless_def,zdiff_def] |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
237 |
"integ_of_bin x < integ_of_bin y \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
238 |
\ = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)"; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
239 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
240 |
val iob_less_eq_diff_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
241 |
|
5069 | 242 |
Goal "(integ_of_bin PlusSign < $# 0) = False"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
243 |
by (stac iob_Plus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
244 |
val iob_Plus_not_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
245 |
|
5069 | 246 |
Goal "(integ_of_bin MinusSign < $# 0) = True"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
247 |
by (stac iob_Minus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
248 |
val iob_Minus_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
249 |
|
5069 | 250 |
Goal |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
251 |
"(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
252 |
by (stac iob_Bcons 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
253 |
by (case_tac "x" 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
254 |
by (ALLGOALS Asm_simp_tac); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
255 |
by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
256 |
by (ALLGOALS(int_case_tac "integ_of_bin w")); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
257 |
by (ALLGOALS(asm_simp_tac |
4089 | 258 |
(simpset() addsimps[zminus_zadd_distrib RS sym, |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
259 |
znat_add RS sym]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
260 |
by (stac (zadd_zminus_inverse RS sym) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
261 |
by (rtac zadd_zless_mono1 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
262 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
263 |
val iob_Bcons_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
264 |
|
5069 | 265 |
Goal |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
266 |
"integ_of_bin x <= integ_of_bin y \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
267 |
\ = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
268 |
\ | integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
269 |
by (simp_tac (HOL_ss addsimps |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
270 |
[zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
271 |
,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
272 |
val iob_le_diff_lt_0_or_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
273 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
274 |
Delsimps [zless_eq_less, zle_eq_le, zadd_assoc, znegative_zminus_znat, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
275 |
not_znegative_znat, zero_zless_Suc_pos, negative_zless_0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
276 |
negative_zle_0, not_zle_0_negative, not_znat_zless_negative, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
277 |
zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
278 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
279 |
Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
280 |
iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
281 |
iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0]; |