src/ZF/ex/BinFn.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	ZF/ex/bin.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For bin.thy.  Arithmetic on binary integers.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open BinFn;
clasohm@0
    10
clasohm@0
    11
clasohm@0
    12
(** bin_rec -- by Vset recursion **)
clasohm@0
    13
clasohm@0
    14
goal BinFn.thy "bin_rec(Plus,a,b,h) = a";
clasohm@0
    15
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    16
by (rewrite_goals_tac Bin.con_defs);
clasohm@0
    17
by (SIMP_TAC rank_ss 1);
clasohm@0
    18
val bin_rec_Plus = result();
clasohm@0
    19
clasohm@0
    20
goal BinFn.thy "bin_rec(Minus,a,b,h) = b";
clasohm@0
    21
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    22
by (rewrite_goals_tac Bin.con_defs);
clasohm@0
    23
by (SIMP_TAC rank_ss 1);
clasohm@0
    24
val bin_rec_Minus = result();
clasohm@0
    25
clasohm@0
    26
goal BinFn.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
clasohm@0
    27
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
clasohm@0
    28
by (rewrite_goals_tac Bin.con_defs);
clasohm@0
    29
by (SIMP_TAC (rank_ss addcongs 
clasohm@0
    30
	      (mk_typed_congs BinFn.thy [("h", "[i,i,i]=>i")])) 1);
clasohm@0
    31
val bin_rec_Bcons = result();
clasohm@0
    32
clasohm@0
    33
(*Type checking*)
clasohm@0
    34
val prems = goal BinFn.thy
clasohm@0
    35
    "[| w: bin;    \
clasohm@0
    36
\       a: C(Plus);   b: C(Minus);       \
clasohm@0
    37
\       !!w x r. [| w: bin;  x: bool;  r: C(w) |] ==> h(w,x,r): C(w$$x)  \
clasohm@0
    38
\    |] ==> bin_rec(w,a,b,h) : C(w)";
clasohm@0
    39
by (bin_ind_tac "w" prems 1);
clasohm@0
    40
by (ALLGOALS 
clasohm@0
    41
    (ASM_SIMP_TAC (ZF_ss addrews (prems@[bin_rec_Plus,bin_rec_Minus,
clasohm@0
    42
					 bin_rec_Bcons]))));
clasohm@0
    43
val bin_rec_type = result();
clasohm@0
    44
clasohm@0
    45
(** Versions for use with definitions **)
clasohm@0
    46
clasohm@0
    47
val [rew] = goal BinFn.thy
clasohm@0
    48
    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Plus) = a";
clasohm@0
    49
by (rewtac rew);
clasohm@0
    50
by (rtac bin_rec_Plus 1);
clasohm@0
    51
val def_bin_rec_Plus = result();
clasohm@0
    52
clasohm@0
    53
val [rew] = goal BinFn.thy
clasohm@0
    54
    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Minus) = b";
clasohm@0
    55
by (rewtac rew);
clasohm@0
    56
by (rtac bin_rec_Minus 1);
clasohm@0
    57
val def_bin_rec_Minus = result();
clasohm@0
    58
clasohm@0
    59
val [rew] = goal BinFn.thy
clasohm@0
    60
    "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(w$$x) = h(w,x,j(w))";
clasohm@0
    61
by (rewtac rew);
clasohm@0
    62
by (rtac bin_rec_Bcons 1);
clasohm@0
    63
val def_bin_rec_Bcons = result();
clasohm@0
    64
clasohm@0
    65
fun bin_recs def = map standard
clasohm@0
    66
	([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
clasohm@0
    67
clasohm@0
    68
(** Type checking **)
clasohm@0
    69
clasohm@0
    70
val bin_typechecks0 = bin_rec_type :: Bin.intrs;
clasohm@0
    71
clasohm@0
    72
goalw BinFn.thy [integ_of_bin_def]
clasohm@0
    73
    "!!w. w: bin ==> integ_of_bin(w) : integ";
clasohm@0
    74
by (typechk_tac (bin_typechecks0@integ_typechecks@
clasohm@0
    75
		 nat_typechecks@[bool_into_nat]));
clasohm@0
    76
val integ_of_bin_type = result();
clasohm@0
    77
clasohm@0
    78
goalw BinFn.thy [bin_succ_def]
clasohm@0
    79
    "!!w. w: bin ==> bin_succ(w) : bin";
clasohm@0
    80
by (typechk_tac (bin_typechecks0@bool_typechecks));
clasohm@0
    81
val bin_succ_type = result();
clasohm@0
    82
clasohm@0
    83
goalw BinFn.thy [bin_pred_def]
clasohm@0
    84
    "!!w. w: bin ==> bin_pred(w) : bin";
clasohm@0
    85
by (typechk_tac (bin_typechecks0@bool_typechecks));
clasohm@0
    86
val bin_pred_type = result();
clasohm@0
    87
clasohm@0
    88
goalw BinFn.thy [bin_minus_def]
clasohm@0
    89
    "!!w. w: bin ==> bin_minus(w) : bin";
clasohm@0
    90
by (typechk_tac ([bin_pred_type]@bin_typechecks0@bool_typechecks));
clasohm@0
    91
val bin_minus_type = result();
clasohm@0
    92
clasohm@0
    93
goalw BinFn.thy [bin_add_def]
clasohm@0
    94
    "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin";
clasohm@0
    95
by (typechk_tac ([bin_succ_type,bin_pred_type]@bin_typechecks0@
clasohm@0
    96
		 bool_typechecks@ZF_typechecks));
clasohm@0
    97
val bin_add_type = result();
clasohm@0
    98
clasohm@0
    99
goalw BinFn.thy [bin_mult_def]
clasohm@0
   100
    "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
clasohm@0
   101
by (typechk_tac ([bin_minus_type,bin_add_type]@bin_typechecks0@
clasohm@0
   102
		 bool_typechecks));
clasohm@0
   103
val bin_mult_type = result();
clasohm@0
   104
clasohm@0
   105
val bin_typechecks = bin_typechecks0 @
clasohm@0
   106
    [integ_of_bin_type, bin_succ_type, bin_pred_type, 
clasohm@0
   107
     bin_minus_type, bin_add_type, bin_mult_type];
clasohm@0
   108
clasohm@0
   109
val bin_congs = mk_congs BinFn.thy
clasohm@0
   110
    ["bin_rec","op $$","integ_of_bin","bin_succ","bin_pred",
clasohm@0
   111
     "bin_minus","bin_add","bin_mult"];
clasohm@0
   112
clasohm@0
   113
val bin_ss = integ_ss 
clasohm@0
   114
    addcongs (bin_congs@bool_congs)
clasohm@0
   115
    addrews([bool_1I, bool_0I,
clasohm@0
   116
	     bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @ 
clasohm@0
   117
	     bin_recs integ_of_bin_def @ bool_rews @ bin_typechecks);
clasohm@0
   118
clasohm@0
   119
val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
clasohm@0
   120
                 [bool_subset_nat RS subsetD];
clasohm@0
   121
clasohm@0
   122
(**** The carry/borrow functions, bin_succ and bin_pred ****)
clasohm@0
   123
clasohm@0
   124
(** Lemmas **)
clasohm@0
   125
clasohm@0
   126
goal Integ.thy 
clasohm@0
   127
    "!!z v. [| z $+ v = z' $+ v';  \
clasohm@0
   128
\       z: integ; z': integ;  v: integ; v': integ;  w: integ |]   \
clasohm@0
   129
\    ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
clasohm@0
   130
by (ASM_SIMP_TAC (integ_ss addrews ([zadd_assoc RS sym])) 1);
clasohm@0
   131
val zadd_assoc_cong = result();
clasohm@0
   132
clasohm@0
   133
goal Integ.thy 
clasohm@0
   134
    "!!z v w. [| z: integ;  v: integ;  w: integ |]   \
clasohm@0
   135
\    ==> z $+ (v $+ w) = v $+ (z $+ w)";
clasohm@0
   136
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
clasohm@0
   137
val zadd_assoc_swap = result();
clasohm@0
   138
clasohm@0
   139
val [zadd_cong] = mk_congs Integ.thy ["op $+"];
clasohm@0
   140
clasohm@0
   141
val zadd_kill = (refl RS zadd_cong);
clasohm@0
   142
val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
clasohm@0
   143
clasohm@0
   144
(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
clasohm@0
   145
val zadd_assoc_znat = standard (znat_type RS zadd_assoc_swap);
clasohm@0
   146
clasohm@0
   147
goal Integ.thy 
clasohm@0
   148
    "!!z w. [| z: integ;  w: integ |]   \
clasohm@0
   149
\    ==> w $+ (z $+ (w $+ z)) = w $+ (w $+ (z $+ z))";
clasohm@0
   150
by (REPEAT (ares_tac [zadd_kill, zadd_assoc_swap] 1));
clasohm@0
   151
val zadd_swap_pairs = result();
clasohm@0
   152
clasohm@0
   153
clasohm@0
   154
val carry_ss = bin_ss addrews 
clasohm@0
   155
               (bin_recs bin_succ_def @ bin_recs bin_pred_def);
clasohm@0
   156
clasohm@0
   157
goal BinFn.thy
clasohm@0
   158
    "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
clasohm@0
   159
by (etac Bin.induct 1);
clasohm@0
   160
by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
clasohm@0
   161
by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
clasohm@0
   162
by (etac boolE 1);
clasohm@0
   163
by (ALLGOALS (ASM_SIMP_TAC (carry_ss addrews [zadd_assoc])));
clasohm@0
   164
by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
clasohm@0
   165
val integ_of_bin_succ = result();
clasohm@0
   166
clasohm@0
   167
goal BinFn.thy
clasohm@0
   168
    "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
clasohm@0
   169
by (etac Bin.induct 1);
clasohm@0
   170
by (SIMP_TAC (carry_ss addrews [zadd_0_right]) 1);
clasohm@0
   171
by (SIMP_TAC (carry_ss addrews [zadd_zminus_inverse]) 1);
clasohm@0
   172
by (etac boolE 1);
clasohm@0
   173
by (ALLGOALS 
clasohm@0
   174
    (ASM_SIMP_TAC 
clasohm@0
   175
     (carry_ss addrews [zadd_assoc RS sym,
clasohm@0
   176
			zadd_zminus_inverse, zadd_zminus_inverse2])));
clasohm@0
   177
by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
clasohm@0
   178
val integ_of_bin_pred = result();
clasohm@0
   179
clasohm@0
   180
(*These two results replace the definitions of bin_succ and bin_pred*)
clasohm@0
   181
clasohm@0
   182
clasohm@0
   183
(*** bin_minus: (unary!) negation of binary integers ***)
clasohm@0
   184
clasohm@0
   185
val bin_minus_ss =
clasohm@0
   186
    bin_ss addrews (bin_recs bin_minus_def @
clasohm@0
   187
		    [integ_of_bin_succ, integ_of_bin_pred]);
clasohm@0
   188
clasohm@0
   189
goal BinFn.thy
clasohm@0
   190
    "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
clasohm@0
   191
by (etac Bin.induct 1);
clasohm@0
   192
by (SIMP_TAC (bin_minus_ss addrews [zminus_0]) 1);
clasohm@0
   193
by (SIMP_TAC (bin_minus_ss addrews [zadd_0_right]) 1);
clasohm@0
   194
by (etac boolE 1);
clasohm@0
   195
by (ALLGOALS 
clasohm@0
   196
    (ASM_SIMP_TAC (bin_minus_ss addrews [zminus_zadd_distrib, zadd_assoc])));
clasohm@0
   197
val integ_of_bin_minus = result();
clasohm@0
   198
clasohm@0
   199
clasohm@0
   200
(*** bin_add: binary addition ***)
clasohm@0
   201
clasohm@0
   202
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
clasohm@0
   203
by (ASM_SIMP_TAC bin_ss 1);
clasohm@0
   204
val bin_add_Plus = result();
clasohm@0
   205
clasohm@0
   206
goalw BinFn.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
clasohm@0
   207
by (ASM_SIMP_TAC bin_ss 1);
clasohm@0
   208
val bin_add_Minus = result();
clasohm@0
   209
clasohm@0
   210
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
clasohm@0
   211
by (SIMP_TAC bin_ss 1);
clasohm@0
   212
val bin_add_Bcons_Plus = result();
clasohm@0
   213
clasohm@0
   214
goalw BinFn.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
clasohm@0
   215
by (SIMP_TAC bin_ss 1);
clasohm@0
   216
val bin_add_Bcons_Minus = result();
clasohm@0
   217
clasohm@0
   218
goalw BinFn.thy [bin_add_def]
clasohm@0
   219
    "!!w y. [| w: bin;  y: bool |] ==> \
clasohm@0
   220
\           bin_add(v$$x, w$$y) = \
clasohm@0
   221
\           bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
clasohm@0
   222
by (ASM_SIMP_TAC bin_ss 1);
clasohm@0
   223
val bin_add_Bcons_Bcons = result();
clasohm@0
   224
clasohm@0
   225
val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
clasohm@0
   226
		    bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
clasohm@0
   227
		    integ_of_bin_succ, integ_of_bin_pred];
clasohm@0
   228
clasohm@0
   229
val bin_add_ss = bin_ss addrews ([bool_subset_nat RS subsetD] @ bin_add_rews);
clasohm@0
   230
clasohm@0
   231
goal BinFn.thy
clasohm@0
   232
    "!!v. v: bin ==> \
clasohm@0
   233
\         ALL w: bin. integ_of_bin(bin_add(v,w)) = \
clasohm@0
   234
\                     integ_of_bin(v) $+ integ_of_bin(w)";
clasohm@0
   235
by (etac Bin.induct 1);
clasohm@0
   236
by (SIMP_TAC bin_add_ss 1);
clasohm@0
   237
by (SIMP_TAC bin_add_ss 1);
clasohm@0
   238
by (rtac ballI 1);
clasohm@0
   239
by (bin_ind_tac "wa" [] 1);
clasohm@0
   240
by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_0_right]) 1);
clasohm@0
   241
by (ASM_SIMP_TAC bin_add_ss 1);
clasohm@0
   242
by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
clasohm@0
   243
by (etac boolE 1);
clasohm@0
   244
by (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc, zadd_swap_pairs]) 2);
clasohm@0
   245
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
clasohm@0
   246
by (etac boolE 1);
clasohm@0
   247
by (ALLGOALS (ASM_SIMP_TAC (bin_add_ss addrews [zadd_assoc,zadd_swap_pairs])));
clasohm@0
   248
by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
clasohm@0
   249
		      typechecks) 1));
clasohm@0
   250
val integ_of_bin_add_lemma = result();
clasohm@0
   251
clasohm@0
   252
val integ_of_bin_add = integ_of_bin_add_lemma RS bspec;
clasohm@0
   253
clasohm@0
   254
clasohm@0
   255
(*** bin_add: binary multiplication ***)
clasohm@0
   256
clasohm@0
   257
val bin_mult_ss =
clasohm@0
   258
    bin_ss addrews (bin_recs bin_mult_def @ 
clasohm@0
   259
		       [integ_of_bin_minus, integ_of_bin_add]);
clasohm@0
   260
clasohm@0
   261
clasohm@0
   262
val major::prems = goal BinFn.thy
clasohm@0
   263
    "[| v: bin; w: bin |] ==>	\
clasohm@0
   264
\    integ_of_bin(bin_mult(v,w)) = \
clasohm@0
   265
\    integ_of_bin(v) $* integ_of_bin(w)";
clasohm@0
   266
by (cut_facts_tac prems 1);
clasohm@0
   267
by (bin_ind_tac "v" [major] 1);
clasohm@0
   268
by (SIMP_TAC (bin_mult_ss addrews [zmult_0]) 1);
clasohm@0
   269
by (SIMP_TAC (bin_mult_ss addrews [zmult_1,zmult_zminus]) 1);
clasohm@0
   270
by (etac boolE 1);
clasohm@0
   271
by (ASM_SIMP_TAC (bin_mult_ss addrews [zadd_zmult_distrib]) 2);
clasohm@0
   272
by (ASM_SIMP_TAC 
clasohm@0
   273
    (bin_mult_ss addrews [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
clasohm@0
   274
by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
clasohm@0
   275
		      typechecks) 1));
clasohm@0
   276
val integ_of_bin_mult = result();
clasohm@0
   277
clasohm@0
   278
(**** Computations ****)
clasohm@0
   279
clasohm@0
   280
(** extra rules for bin_succ, bin_pred **)
clasohm@0
   281
clasohm@0
   282
val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def;
clasohm@0
   283
val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
clasohm@0
   284
clasohm@0
   285
goal BinFn.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
clasohm@0
   286
by (SIMP_TAC carry_ss 1);
clasohm@0
   287
val bin_succ_Bcons1 = result();
clasohm@0
   288
clasohm@0
   289
goal BinFn.thy "bin_succ(w$$0) = w$$1";
clasohm@0
   290
by (SIMP_TAC carry_ss 1);
clasohm@0
   291
val bin_succ_Bcons0 = result();
clasohm@0
   292
clasohm@0
   293
goal BinFn.thy "bin_pred(w$$1) = w$$0";
clasohm@0
   294
by (SIMP_TAC carry_ss 1);
clasohm@0
   295
val bin_pred_Bcons1 = result();
clasohm@0
   296
clasohm@0
   297
goal BinFn.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
clasohm@0
   298
by (SIMP_TAC carry_ss 1);
clasohm@0
   299
val bin_pred_Bcons0 = result();
clasohm@0
   300
clasohm@0
   301
(** extra rules for bin_minus **)
clasohm@0
   302
clasohm@0
   303
val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
clasohm@0
   304
clasohm@0
   305
goal BinFn.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
clasohm@0
   306
by (SIMP_TAC bin_minus_ss 1);
clasohm@0
   307
val bin_minus_Bcons1 = result();
clasohm@0
   308
clasohm@0
   309
goal BinFn.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
clasohm@0
   310
by (SIMP_TAC bin_minus_ss 1);
clasohm@0
   311
val bin_minus_Bcons0 = result();
clasohm@0
   312
clasohm@0
   313
(** extra rules for bin_add **)
clasohm@0
   314
clasohm@0
   315
goal BinFn.thy 
clasohm@0
   316
    "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
clasohm@0
   317
by (ASM_SIMP_TAC bin_add_ss 1);
clasohm@0
   318
val bin_add_Bcons_Bcons11 = result();
clasohm@0
   319
clasohm@0
   320
goal BinFn.thy 
clasohm@0
   321
    "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
clasohm@0
   322
by (ASM_SIMP_TAC bin_add_ss 1);
clasohm@0
   323
val bin_add_Bcons_Bcons10 = result();
clasohm@0
   324
clasohm@0
   325
goal BinFn.thy 
clasohm@0
   326
    "!!w y.[| w: bin;  y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
clasohm@0
   327
by (ASM_SIMP_TAC bin_add_ss 1);
clasohm@0
   328
val bin_add_Bcons_Bcons0 = result();
clasohm@0
   329
clasohm@0
   330
(** extra rules for bin_mult **)
clasohm@0
   331
clasohm@0
   332
val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
clasohm@0
   333
clasohm@0
   334
goal BinFn.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
clasohm@0
   335
by (SIMP_TAC bin_mult_ss 1);
clasohm@0
   336
val bin_mult_Bcons1 = result();
clasohm@0
   337
clasohm@0
   338
goal BinFn.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
clasohm@0
   339
by (SIMP_TAC bin_mult_ss 1);
clasohm@0
   340
val bin_mult_Bcons0 = result();
clasohm@0
   341
clasohm@0
   342
clasohm@0
   343
(*** The computation simpset ***)
clasohm@0
   344
clasohm@0
   345
val bin_comp_ss = carry_ss addrews
clasohm@0
   346
    [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, bin_add_Bcons_Minus, 
clasohm@0
   347
     bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11]
clasohm@0
   348
    setauto (type_auto_tac bin_typechecks0);
clasohm@0
   349
clasohm@0
   350
val bin_comp_ss = integ_ss 
clasohm@0
   351
    addcongs bin_congs
clasohm@0
   352
    addrews [bin_succ_Plus, bin_succ_Minus,
clasohm@0
   353
	     bin_succ_Bcons1, bin_succ_Bcons0,
clasohm@0
   354
	     bin_pred_Plus, bin_pred_Minus,
clasohm@0
   355
	     bin_pred_Bcons1, bin_pred_Bcons0,
clasohm@0
   356
	     bin_minus_Plus, bin_minus_Minus,
clasohm@0
   357
	     bin_minus_Bcons1, bin_minus_Bcons0,
clasohm@0
   358
	     bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus, 
clasohm@0
   359
	     bin_add_Bcons_Minus, bin_add_Bcons_Bcons0, 
clasohm@0
   360
	     bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
clasohm@0
   361
	     bin_mult_Plus, bin_mult_Minus,
clasohm@0
   362
	     bin_mult_Bcons1, bin_mult_Bcons0]
clasohm@0
   363
    setauto (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
clasohm@0
   364
clasohm@0
   365
(*** Examples of performing binary arithmetic by simplification ***)
clasohm@0
   366
clasohm@0
   367
proof_timing := true;
clasohm@0
   368
(*All runtimes below are on a SPARCserver 10*)
clasohm@0
   369
clasohm@0
   370
(* 13+19 = 32 *)
clasohm@0
   371
goal BinFn.thy
clasohm@0
   372
    "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
clasohm@0
   373
by (SIMP_TAC bin_comp_ss 1);	(*1.9 secs*)
clasohm@0
   374
result();
clasohm@0
   375
clasohm@0
   376
bin_add(binary_of_int 13, binary_of_int 19);
clasohm@0
   377
clasohm@0
   378
(* 1234+5678 = 6912 *)
clasohm@0
   379
goal BinFn.thy
clasohm@0
   380
    "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
clasohm@0
   381
\	     Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
clasohm@0
   382
\    Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
clasohm@0
   383
by (SIMP_TAC bin_comp_ss 1);	(*8.9 secs*)
clasohm@0
   384
result();
clasohm@0
   385
clasohm@0
   386
bin_add(binary_of_int 1234, binary_of_int 5678);
clasohm@0
   387
clasohm@0
   388
(* 1359-2468 = ~1109 *)
clasohm@0
   389
goal BinFn.thy
clasohm@0
   390
    "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1,		\
clasohm@0
   391
\	     Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = 	\
clasohm@0
   392
\    Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
clasohm@0
   393
by (SIMP_TAC bin_comp_ss 1);	(*7.4 secs*)
clasohm@0
   394
result();
clasohm@0
   395
clasohm@0
   396
bin_add(binary_of_int 1359, binary_of_int ~2468);
clasohm@0
   397
clasohm@0
   398
(* 93746-46375 = 47371 *)
clasohm@0
   399
goal BinFn.thy
clasohm@0
   400
    "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
clasohm@0
   401
\	     Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
clasohm@0
   402
\    Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
clasohm@0
   403
by (SIMP_TAC bin_comp_ss 1);	(*13.7 secs*)
clasohm@0
   404
result();
clasohm@0
   405
clasohm@0
   406
bin_add(binary_of_int 93746, binary_of_int ~46375);
clasohm@0
   407
clasohm@0
   408
(* negation of 65745 *)
clasohm@0
   409
goal BinFn.thy
clasohm@0
   410
    "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
clasohm@0
   411
\    Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
clasohm@0
   412
by (SIMP_TAC bin_comp_ss 1);	(*2.8 secs*)
clasohm@0
   413
result();
clasohm@0
   414
clasohm@0
   415
bin_minus(binary_of_int 65745);
clasohm@0
   416
clasohm@0
   417
(* negation of ~54321 *)
clasohm@0
   418
goal BinFn.thy
clasohm@0
   419
    "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
clasohm@0
   420
\    Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
clasohm@0
   421
by (SIMP_TAC bin_comp_ss 1);	(*3.3 secs*)
clasohm@0
   422
result();
clasohm@0
   423
clasohm@0
   424
bin_minus(binary_of_int ~54321);
clasohm@0
   425
clasohm@0
   426
(* 13*19 = 247 *)
clasohm@0
   427
goal BinFn.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
clasohm@0
   428
\               Plus$$1$$1$$1$$1$$0$$1$$1$$1";
clasohm@0
   429
by (SIMP_TAC bin_comp_ss 1);	(*4.4 secs*)
clasohm@0
   430
result();
clasohm@0
   431
clasohm@0
   432
bin_mult(binary_of_int 13, binary_of_int 19);
clasohm@0
   433
clasohm@0
   434
(* ~84 * 51 = ~4284 *)
clasohm@0
   435
goal BinFn.thy
clasohm@0
   436
    "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
clasohm@0
   437
\    Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
clasohm@0
   438
by (SIMP_TAC bin_comp_ss 1);	(*9.2 secs*)
clasohm@0
   439
result();
clasohm@0
   440
clasohm@0
   441
bin_mult(binary_of_int ~84, binary_of_int 51);
clasohm@0
   442
clasohm@0
   443
(* 255*255 = 65025;  the worst case for 8-bit operands *)
clasohm@0
   444
goal BinFn.thy
clasohm@0
   445
    "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
clasohm@0
   446
\             Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
clasohm@0
   447
\        Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
clasohm@0
   448
by (SIMP_TAC bin_comp_ss 1);	(*38.4 secs*)
clasohm@0
   449
result();
clasohm@0
   450
clasohm@0
   451
bin_mult(binary_of_int 255, binary_of_int 255);
clasohm@0
   452
clasohm@0
   453
(***************** TOO SLOW TO INCLUDE IN TEST RUNS
clasohm@0
   454
(* 1359 * ~2468 = ~3354012 *)
clasohm@0
   455
goal BinFn.thy
clasohm@0
   456
    "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, 		\
clasohm@0
   457
\	      Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = 	\
clasohm@0
   458
\    Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
clasohm@0
   459
by (SIMP_TAC bin_comp_ss 1);	(*54.8 secs*)
clasohm@0
   460
result();
clasohm@0
   461
****************)
clasohm@0
   462
clasohm@0
   463
bin_mult(binary_of_int 1359, binary_of_int ~2468);