author | paulson |
Fri, 31 Jul 1998 10:50:47 +0200 | |
changeset 5224 | 8d132a14e722 |
parent 5199 | be986f7a6def |
child 5491 | 22f8331cdf47 |
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 |
||
5224 | 141 |
Goal "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
5184 | 142 |
by (induct_tac "v" 1); |
4686 | 143 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
144 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 145 |
by (rtac allI 1); |
5184 | 146 |
by (induct_tac "w" 1); |
4686 | 147 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1); |
148 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
|
1632 | 149 |
by (cut_inst_tac [("P","bool")] True_or_False 1); |
150 |
by (etac disjE 1); |
|
4686 | 151 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
152 |
by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
|
5224 | 153 |
qed_spec_mp "integ_of_bin_add"; |
1632 | 154 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
155 |
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
|
156 |
integ_of_bin_norm_Bcons]; |
1632 | 157 |
|
5069 | 158 |
Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
5184 | 159 |
by (induct_tac "v" 1); |
4686 | 160 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
161 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
1632 | 162 |
by (cut_inst_tac [("P","bool")] True_or_False 1); |
163 |
by (etac disjE 1); |
|
4686 | 164 |
by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2); |
165 |
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
|
166 |
zadd_ac)) 1); |
1632 | 167 |
qed "integ_of_bin_mult"; |
168 |
||
169 |
||
170 |
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
|
171 |
iob_Plus,iob_Minus,iob_Bcons, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
172 |
norm_Plus,norm_Minus,norm_Bcons]; |
1632 | 173 |
|
174 |
Addsimps [integ_of_bin_add RS sym, |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
175 |
integ_of_bin_minus RS sym, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
176 |
integ_of_bin_mult RS sym, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
177 |
bin_succ_Bcons1,bin_succ_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
178 |
bin_pred_Bcons1,bin_pred_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
179 |
bin_minus_Bcons1,bin_minus_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
180 |
bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
181 |
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
|
182 |
bin_mult_Bcons1,bin_mult_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
183 |
norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
184 |
norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
185 |
norm_Bcons_Bcons]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
186 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
187 |
|
4195 | 188 |
(** 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
|
189 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
190 |
Addsimps [zadd_assoc]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
191 |
|
5224 | 192 |
Goal "(integ_of_bin x = integ_of_bin y) \ |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
193 |
\ = (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
|
194 |
by (simp_tac (HOL_ss addsimps |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
195 |
[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
|
196 |
by (rtac iffI 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
197 |
by (etac ssubst 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
198 |
by (rtac zadd_zminus_inverse 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
199 |
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
|
200 |
by (asm_full_simp_tac |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
201 |
(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
|
202 |
zadd_zminus_inverse2]) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
203 |
val iob_eq_eq_diff_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
204 |
|
5069 | 205 |
Goal "(integ_of_bin PlusSign = $# 0) = True"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
206 |
by (stac iob_Plus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
207 |
val iob_Plus_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
208 |
|
5069 | 209 |
Goal "(integ_of_bin MinusSign = $# 0) = False"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
210 |
by (stac iob_Minus 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
211 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
212 |
val iob_Minus_not_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
213 |
|
5224 | 214 |
Goal "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
215 |
by (stac iob_Bcons 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
216 |
by (case_tac "x" 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
217 |
by (ALLGOALS Asm_simp_tac); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
218 |
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
|
219 |
by (ALLGOALS(int_case_tac "integ_of_bin w")); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
220 |
by (ALLGOALS(asm_simp_tac |
4089 | 221 |
(simpset() addsimps[zminus_zadd_distrib RS sym, |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
222 |
znat_add RS sym]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
223 |
by (rtac notI 1); |
5224 | 224 |
(*Add Suc(Suc(n + n)) to both sides*) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
225 |
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
|
226 |
by (Asm_full_simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
227 |
val iob_Bcons_eq_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
228 |
|
5069 | 229 |
Goalw [zless_def,zdiff_def] |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
230 |
"integ_of_bin x < integ_of_bin y \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
231 |
\ = (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
|
232 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
233 |
val iob_less_eq_diff_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
234 |
|
5069 | 235 |
Goal "(integ_of_bin PlusSign < $# 0) = False"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
236 |
by (stac iob_Plus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
237 |
val iob_Plus_not_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
238 |
|
5069 | 239 |
Goal "(integ_of_bin MinusSign < $# 0) = True"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
240 |
by (stac iob_Minus 1); by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
241 |
val iob_Minus_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
242 |
|
5224 | 243 |
Goal "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
244 |
by (stac iob_Bcons 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
245 |
by (case_tac "x" 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
246 |
by (ALLGOALS Asm_simp_tac); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
247 |
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
|
248 |
by (ALLGOALS(int_case_tac "integ_of_bin w")); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
249 |
by (ALLGOALS(asm_simp_tac |
4089 | 250 |
(simpset() addsimps[zminus_zadd_distrib RS sym, |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
251 |
znat_add RS sym]))); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
252 |
by (stac (zadd_zminus_inverse RS sym) 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
253 |
by (rtac zadd_zless_mono1 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
254 |
by (Simp_tac 1); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
255 |
val iob_Bcons_lt_0 = result(); |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
256 |
|
5224 | 257 |
Goal "integ_of_bin x <= integ_of_bin y \ |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
258 |
\ = ( 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
|
259 |
\ | 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
|
260 |
by (simp_tac (HOL_ss addsimps |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
261 |
[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
|
262 |
,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
|
263 |
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
|
264 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
265 |
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
|
266 |
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
|
267 |
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
|
268 |
zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
269 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
270 |
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
|
271 |
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
|
272 |
iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0]; |