src/HOL/Integ/NatBin.ML
author wenzelm
Thu Jun 22 23:04:34 2000 +0200 (2000-06-22)
changeset 9108 9fff97d29837
parent 9064 eacebbcafe57
child 9425 fd6866d90ec1
permissions -rw-r--r--
bind_thm(s);
paulson@7032
     1
(*  Title:      HOL/NatBin.ML
paulson@7032
     2
    ID:         $Id$
paulson@7032
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7032
     4
    Copyright   1999  University of Cambridge
paulson@7032
     5
paulson@7032
     6
Binary arithmetic for the natural numbers
paulson@7032
     7
*)
paulson@7032
     8
paulson@7032
     9
(** nat (coercion from int to nat) **)
paulson@7032
    10
paulson@7032
    11
Goal "nat (number_of w) = number_of w";
paulson@7032
    12
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
paulson@7032
    13
qed "nat_number_of";
paulson@7032
    14
Addsimps [nat_number_of];
paulson@7032
    15
paulson@7032
    16
(*These rewrites should one day be re-oriented...*)
paulson@7032
    17
paulson@8935
    18
Goal "#0 = (0::nat)";
paulson@7032
    19
by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1);
paulson@7032
    20
qed "numeral_0_eq_0";
paulson@7032
    21
paulson@8935
    22
Goal "#1 = (1::nat)";
paulson@7032
    23
by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1);
paulson@7032
    24
qed "numeral_1_eq_1";
paulson@7032
    25
paulson@8935
    26
Goal "#2 = (2::nat)";
paulson@7032
    27
by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1);
paulson@7032
    28
qed "numeral_2_eq_2";
paulson@7032
    29
paulson@8864
    30
bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
paulson@7032
    31
paulson@7032
    32
(** int (coercion from nat to int) **)
paulson@7032
    33
paulson@7032
    34
(*"neg" is used in rewrite rules for binary comparisons*)
paulson@7032
    35
Goal "int (number_of v :: nat) = \
paulson@7032
    36
\        (if neg (number_of v) then #0 \
paulson@7032
    37
\         else (number_of v :: int))";
paulson@7032
    38
by (simp_tac
paulson@7032
    39
    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
paulson@7032
    40
				  not_neg_nat, int_0]) 1);
paulson@7032
    41
qed "int_nat_number_of";
paulson@7032
    42
Addsimps [int_nat_number_of];
paulson@7032
    43
paulson@7032
    44
paulson@7032
    45
(** Successor **)
paulson@7032
    46
paulson@7032
    47
Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
paulson@7086
    48
by (rtac sym 1);
paulson@7032
    49
by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
paulson@7032
    50
qed "Suc_nat_eq_nat_zadd1";
paulson@7032
    51
paulson@7032
    52
Goal "Suc (number_of v) = \
paulson@7032
    53
\       (if neg (number_of v) then #1 else number_of (bin_succ v))";
paulson@7032
    54
by (simp_tac
paulson@7032
    55
    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
paulson@7032
    56
				  nat_number_of_def, int_Suc, 
paulson@7032
    57
				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
paulson@7032
    58
qed "Suc_nat_number_of";
paulson@8737
    59
Addsimps [Suc_nat_number_of];
paulson@8737
    60
paulson@8737
    61
Goal "Suc (number_of v + n) = \
paulson@8737
    62
\       (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
paulson@8737
    63
by (Simp_tac 1);
paulson@8737
    64
qed "Suc_nat_number_of_add";
paulson@7032
    65
paulson@7032
    66
Goal "Suc #0 = #1";
paulson@8737
    67
by (Simp_tac 1);
paulson@7032
    68
qed "Suc_numeral_0_eq_1";
paulson@7032
    69
paulson@7032
    70
Goal "Suc #1 = #2";
paulson@8737
    71
by (Simp_tac 1);
paulson@7032
    72
qed "Suc_numeral_1_eq_2";
paulson@7032
    73
paulson@7032
    74
(** Addition **)
paulson@7032
    75
paulson@8028
    76
Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
paulson@7032
    77
by (rtac (inj_int RS injD) 1);
paulson@7032
    78
by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
paulson@8028
    79
qed "nat_add_distrib";
paulson@7032
    80
paulson@7032
    81
(*"neg" is used in rewrite rules for binary comparisons*)
paulson@7032
    82
Goal "(number_of v :: nat) + number_of v' = \
paulson@7032
    83
\        (if neg (number_of v) then number_of v' \
paulson@7032
    84
\         else if neg (number_of v') then number_of v \
paulson@7032
    85
\         else number_of (bin_add v v'))";
paulson@7032
    86
by (simp_tac
paulson@7032
    87
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
paulson@8028
    88
				  nat_add_distrib RS sym, number_of_add]) 1);
paulson@7032
    89
qed "add_nat_number_of";
paulson@7032
    90
paulson@7032
    91
Addsimps [add_nat_number_of];
paulson@7032
    92
paulson@7032
    93
paulson@7032
    94
(** Subtraction **)
paulson@7032
    95
paulson@8028
    96
Goal "[| (#0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
paulson@7032
    97
by (rtac (inj_int RS injD) 1);
paulson@7032
    98
by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
paulson@8028
    99
qed "nat_diff_distrib";
paulson@7032
   100
paulson@7032
   101
paulson@7032
   102
Goal "nat z - nat z' = \
paulson@7032
   103
\       (if neg z' then nat z  \
paulson@7032
   104
\        else let d = z-z' in    \
paulson@7032
   105
\             if neg d then 0 else nat d)";
paulson@8028
   106
by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
paulson@7032
   107
				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
paulson@8864
   108
by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
paulson@7032
   109
qed "diff_nat_eq_if";
paulson@7032
   110
paulson@7032
   111
Goalw [nat_number_of_def]
paulson@7032
   112
     "(number_of v :: nat) - number_of v' = \
paulson@7032
   113
\       (if neg (number_of v') then number_of v \
paulson@7032
   114
\        else let d = number_of (bin_add v (bin_minus v')) in    \
paulson@7032
   115
\             if neg d then #0 else nat d)";
paulson@7032
   116
by (simp_tac
paulson@7032
   117
    (simpset_of Int.thy delcongs [if_weak_cong]
paulson@7032
   118
			addsimps [not_neg_eq_ge_0, nat_0,
paulson@7032
   119
				  diff_nat_eq_if, diff_number_of_eq]) 1);
paulson@7032
   120
qed "diff_nat_number_of";
paulson@7032
   121
paulson@7032
   122
Addsimps [diff_nat_number_of];
paulson@7032
   123
paulson@7032
   124
paulson@7032
   125
(** Multiplication **)
paulson@7032
   126
paulson@8028
   127
Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
paulson@7032
   128
by (case_tac "#0 <= z'" 1);
paulson@9064
   129
by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
paulson@7032
   130
by (rtac (inj_int RS injD) 1);
paulson@9064
   131
by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
paulson@9064
   132
				      int_0_le_mult_iff]) 1);
paulson@8028
   133
qed "nat_mult_distrib";
paulson@7032
   134
paulson@7032
   135
Goal "(number_of v :: nat) * number_of v' = \
paulson@7032
   136
\      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
paulson@7032
   137
by (simp_tac
paulson@7032
   138
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
paulson@8028
   139
				  nat_mult_distrib RS sym, number_of_mult, 
paulson@7032
   140
				  nat_0]) 1);
paulson@7032
   141
qed "mult_nat_number_of";
paulson@7032
   142
paulson@7032
   143
Addsimps [mult_nat_number_of];
paulson@7032
   144
paulson@7032
   145
paulson@7032
   146
(** Quotient **)
paulson@7032
   147
paulson@8028
   148
Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
paulson@7032
   149
by (case_tac "#0 <= z'" 1);
paulson@7032
   150
by (auto_tac (claset(), 
paulson@7127
   151
	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
paulson@7032
   152
by (zdiv_undefined_case_tac "z' = #0" 1);
paulson@7032
   153
 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
paulson@7032
   154
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
paulson@7032
   155
by (rename_tac "m m'" 1);
paulson@7032
   156
by (subgoal_tac "#0 <= int m div int m'" 1);
paulson@7032
   157
 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
paulson@7032
   158
				       pos_imp_zdiv_nonneg_iff]) 2);
paulson@7032
   159
by (rtac (inj_int RS injD) 1);
paulson@7032
   160
by (Asm_simp_tac 1);
paulson@7032
   161
by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
paulson@7032
   162
 by (Force_tac 2);
paulson@7032
   163
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
nipkow@8698
   164
				      numeral_0_eq_0, zadd_int, zmult_int]) 1);
paulson@7032
   165
by (rtac (mod_div_equality RS sym RS trans) 1);
paulson@7032
   166
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
paulson@8028
   167
qed "nat_div_distrib";
paulson@7032
   168
paulson@7032
   169
Goal "(number_of v :: nat)  div  number_of v' = \
paulson@7032
   170
\         (if neg (number_of v) then #0 \
paulson@7032
   171
\          else nat (number_of v div number_of v'))";
paulson@7032
   172
by (simp_tac
paulson@7032
   173
    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
paulson@8028
   174
				  nat_div_distrib RS sym, nat_0]) 1);
paulson@7032
   175
qed "div_nat_number_of";
paulson@7032
   176
paulson@7032
   177
Addsimps [div_nat_number_of];
paulson@7032
   178
paulson@7032
   179
paulson@7032
   180
(** Remainder **)
paulson@7032
   181
paulson@7032
   182
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
paulson@8028
   183
Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
paulson@7032
   184
by (zdiv_undefined_case_tac "z' = #0" 1);
paulson@7032
   185
 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
paulson@7032
   186
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
paulson@7032
   187
by (rename_tac "m m'" 1);
paulson@7032
   188
by (subgoal_tac "#0 <= int m mod int m'" 1);
paulson@7032
   189
 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, numeral_0_eq_0, 
paulson@7032
   190
				       pos_mod_sign]) 2);
paulson@7032
   191
by (rtac (inj_int RS injD) 1);
paulson@7032
   192
by (Asm_simp_tac 1);
paulson@7032
   193
by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
paulson@7032
   194
 by (Force_tac 2);
paulson@7032
   195
by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
nipkow@8698
   196
				      numeral_0_eq_0, zadd_int, zmult_int]) 1);
paulson@7032
   197
by (rtac (mod_div_equality RS sym RS trans) 1);
paulson@7032
   198
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
paulson@8028
   199
qed "nat_mod_distrib";
paulson@7032
   200
paulson@7032
   201
Goal "(number_of v :: nat)  mod  number_of v' = \
paulson@7032
   202
\       (if neg (number_of v) then #0 \
paulson@7032
   203
\        else if neg (number_of v') then number_of v \
paulson@7032
   204
\        else nat (number_of v mod number_of v'))";
paulson@7032
   205
by (simp_tac
paulson@7032
   206
    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
paulson@7032
   207
				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
paulson@8028
   208
				  nat_mod_distrib RS sym]) 1);
paulson@7032
   209
qed "mod_nat_number_of";
paulson@7032
   210
paulson@7032
   211
Addsimps [mod_nat_number_of];
paulson@7032
   212
paulson@7032
   213
paulson@7032
   214
(*** Comparisons ***)
paulson@7032
   215
paulson@7032
   216
(** Equals (=) **)
paulson@7032
   217
paulson@7032
   218
Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
paulson@7032
   219
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
paulson@7032
   220
qed "eq_nat_nat_iff";
paulson@7032
   221
paulson@7032
   222
(*"neg" is used in rewrite rules for binary comparisons*)
paulson@7032
   223
Goal "((number_of v :: nat) = number_of v') = \
paulson@8795
   224
\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
paulson@8795
   225
\      else if neg (number_of v') then iszero (number_of v) \
paulson@8795
   226
\      else iszero (number_of (bin_add v (bin_minus v'))))";
paulson@7032
   227
by (simp_tac
paulson@7032
   228
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
paulson@7032
   229
				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
paulson@8795
   230
by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
paulson@8795
   231
					   iszero_def]) 1);
paulson@8795
   232
by (simp_tac (simpset_of Int.thy addsimps [not_neg_eq_ge_0 RS sym]) 1);
paulson@7032
   233
qed "eq_nat_number_of";
paulson@7032
   234
paulson@7032
   235
Addsimps [eq_nat_number_of];
paulson@7032
   236
paulson@7032
   237
(** Less-than (<) **)
paulson@7032
   238
paulson@7032
   239
(*"neg" is used in rewrite rules for binary comparisons*)
paulson@7032
   240
Goal "((number_of v :: nat) < number_of v') = \
paulson@7032
   241
\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
paulson@7032
   242
\         else neg (number_of (bin_add v (bin_minus v'))))";
paulson@7032
   243
by (simp_tac
paulson@7032
   244
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
paulson@7032
   245
				  nat_less_eq_zless, less_number_of_eq_neg,
paulson@7032
   246
				  nat_0]) 1);
paulson@7032
   247
by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
paulson@7519
   248
				number_of_minus, zless_nat_eq_int_zless]) 1);
paulson@7032
   249
qed "less_nat_number_of";
paulson@7032
   250
paulson@7032
   251
Addsimps [less_nat_number_of];
paulson@7032
   252
paulson@7032
   253
paulson@7032
   254
(** Less-than-or-equals (<=) **)
paulson@7032
   255
paulson@7032
   256
Goal "(number_of x <= (number_of y::nat)) = \
paulson@7032
   257
\     (~ number_of y < (number_of x::nat))";
paulson@7032
   258
by (rtac (linorder_not_less RS sym) 1);
paulson@7032
   259
qed "le_nat_number_of_eq_not_less"; 
paulson@7032
   260
paulson@7032
   261
Addsimps [le_nat_number_of_eq_not_less];
paulson@7032
   262
paulson@7032
   263
(*** New versions of existing theorems involving 0, 1, 2 ***)
paulson@7032
   264
paulson@7032
   265
fun change_theory thy th = 
paulson@7032
   266
    [th, read_instantiate_sg (sign_of thy) [("t","dummyVar")] refl] 
paulson@7032
   267
    MRS (conjI RS conjunct1) |> standard;
paulson@7032
   268
paulson@7032
   269
(*Maps n to #n for n = 0, 1, 2*)
paulson@7032
   270
val numeral_sym_ss = 
paulson@7032
   271
    HOL_ss addsimps [numeral_0_eq_0 RS sym, 
paulson@7032
   272
		     numeral_1_eq_1 RS sym, 
paulson@7032
   273
		     numeral_2_eq_2 RS sym,
paulson@7032
   274
		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
paulson@7032
   275
paulson@7032
   276
fun rename_numerals thy th = simplify numeral_sym_ss (change_theory thy th);
paulson@7032
   277
paulson@7032
   278
(*Maps #n to n for n = 0, 1, 2*)
paulson@7032
   279
val numeral_ss = 
paulson@7032
   280
    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
paulson@7032
   281
paulson@7032
   282
(** Nat **)
paulson@7032
   283
paulson@7032
   284
Goal "#0 < n ==> n = Suc(n - #1)";
paulson@7032
   285
by (asm_full_simp_tac numeral_ss 1);
paulson@7032
   286
qed "Suc_pred'";
paulson@7032
   287
paulson@7032
   288
(*Expresses a natural number constant as the Suc of another one.
paulson@7032
   289
  NOT suitable for rewriting because n recurs in the condition.*)
paulson@7032
   290
bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
paulson@7032
   291
paulson@7056
   292
(** NatDef & Nat **)
paulson@7056
   293
paulson@7056
   294
Addsimps (map (rename_numerals thy) 
paulson@7056
   295
	  [min_0L, min_0R, max_0L, max_0R]);
paulson@7056
   296
paulson@7056
   297
AddIffs (map (rename_numerals thy) 
paulson@7056
   298
	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
paulson@7056
   299
	  le0, le_0_eq, 
paulson@7056
   300
	  neq0_conv, zero_neq_conv, not_gr0]);
paulson@7056
   301
paulson@7032
   302
(** Arith **)
paulson@7032
   303
paulson@8776
   304
(*Identity laws for + - * *)	 
paulson@8776
   305
val basic_renamed_arith_simps =
paulson@8776
   306
    map (rename_numerals thy) 
paulson@8776
   307
        [diff_0, diff_0_eq_0, add_0, add_0_right, 
paulson@8776
   308
	 mult_0, mult_0_right, mult_1, mult_1_right];
paulson@8776
   309
	 
paulson@8776
   310
(*Non-trivial simplifications*)	 
paulson@8776
   311
val other_renamed_arith_simps =
paulson@8776
   312
    map (rename_numerals thy) 
paulson@8776
   313
	[add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
paulson@8776
   314
	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
paulson@8776
   315
paulson@8776
   316
Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
paulson@7032
   317
paulson@7032
   318
AddIffs (map (rename_numerals thy) [add_is_0, zero_is_add, add_gr_0]);
paulson@7032
   319
paulson@7056
   320
Goal "Suc n = n + #1";
paulson@7056
   321
by (asm_simp_tac numeral_ss 1);
paulson@7056
   322
qed "Suc_eq_add_numeral_1";
paulson@7056
   323
paulson@7032
   324
(* These two can be useful when m = number_of... *)
paulson@7032
   325
paulson@7032
   326
Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
wenzelm@8442
   327
by (case_tac "m" 1);
paulson@7032
   328
by (ALLGOALS (asm_simp_tac numeral_ss));
paulson@7032
   329
qed "add_eq_if";
paulson@7032
   330
paulson@7032
   331
Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
wenzelm@8442
   332
by (case_tac "m" 1);
paulson@7032
   333
by (ALLGOALS (asm_simp_tac numeral_ss));
paulson@7032
   334
qed "mult_eq_if";
paulson@7032
   335
paulson@7056
   336
Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
wenzelm@8442
   337
by (case_tac "m" 1);
paulson@7056
   338
by (ALLGOALS (asm_simp_tac numeral_ss));
paulson@7056
   339
qed "power_eq_if";
paulson@7056
   340
paulson@7056
   341
Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
paulson@7056
   342
by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
paulson@7056
   343
qed "diff_less'";
paulson@7056
   344
paulson@7056
   345
Addsimps [inst "n" "number_of ?v" diff_less'];
paulson@7056
   346
paulson@7032
   347
(*various theorems that aren't in the default simpset*)
wenzelm@9108
   348
bind_thm ("add_is_one'", rename_numerals thy add_is_1);
wenzelm@9108
   349
bind_thm ("one_is_add'", rename_numerals thy one_is_add);
wenzelm@9108
   350
bind_thm ("zero_induct'", rename_numerals thy zero_induct);
wenzelm@9108
   351
bind_thm ("diff_self_eq_0'", rename_numerals thy diff_self_eq_0);
wenzelm@9108
   352
bind_thm ("mult_eq_self_implies_10'", rename_numerals thy mult_eq_self_implies_10);
wenzelm@9108
   353
bind_thm ("le_pred_eq'", rename_numerals thy le_pred_eq);
wenzelm@9108
   354
bind_thm ("less_pred_eq'", rename_numerals thy less_pred_eq);
paulson@7032
   355
paulson@7032
   356
(** Divides **)
paulson@7032
   357
paulson@8776
   358
Addsimps (map (rename_numerals thy) [mod_1, mod_0, div_1, div_0]);
paulson@7032
   359
paulson@7032
   360
AddIffs (map (rename_numerals thy) 
paulson@7032
   361
	  [dvd_1_left, dvd_0_right]);
paulson@7032
   362
paulson@7032
   363
(*useful?*)
wenzelm@9108
   364
bind_thm ("mod_self'", rename_numerals thy mod_self);
wenzelm@9108
   365
bind_thm ("div_self'", rename_numerals thy div_self);
wenzelm@9108
   366
bind_thm ("div_less'", rename_numerals thy div_less);
wenzelm@9108
   367
bind_thm ("mod_mult_self_is_zero'", rename_numerals thy mod_mult_self_is_0);
paulson@7032
   368
paulson@7032
   369
(** Power **)
paulson@7032
   370
paulson@7032
   371
Goal "(p::nat) ^ #0 = #1";
paulson@7032
   372
by (simp_tac numeral_ss 1);
paulson@7032
   373
qed "power_zero";
paulson@8792
   374
paulson@8792
   375
Goal "(p::nat) ^ #1 = p";
paulson@8792
   376
by (simp_tac numeral_ss 1);
paulson@8792
   377
qed "power_one";
paulson@8792
   378
Addsimps [power_zero, power_one];
paulson@8792
   379
paulson@8792
   380
Goal "(p::nat) ^ #2 = p*p";
paulson@8792
   381
by (simp_tac numeral_ss 1);
paulson@8792
   382
qed "power_two";
paulson@7032
   383
paulson@8864
   384
Goal "#0 < (i::nat) ==> #0 < i^n";
paulson@8864
   385
by (asm_simp_tac numeral_ss 1);
paulson@8864
   386
qed "zero_less_power'";
paulson@8864
   387
Addsimps [zero_less_power'];
paulson@8864
   388
wenzelm@9108
   389
bind_thm ("binomial_zero", rename_numerals thy binomial_0);
wenzelm@9108
   390
bind_thm ("binomial_Suc'", rename_numerals thy binomial_Suc);
wenzelm@9108
   391
bind_thm ("binomial_n_n'", rename_numerals thy binomial_n_n);
paulson@7032
   392
paulson@7032
   393
(*binomial_0_Suc doesn't work well on numerals*)
paulson@7032
   394
Addsimps (map (rename_numerals thy) 
paulson@7032
   395
	  [binomial_n_0, binomial_zero, binomial_1]);
paulson@7032
   396
paulson@8792
   397
Addsimps [rename_numerals thy card_Pow];
paulson@7519
   398
paulson@8935
   399
(*** Comparisons involving (0::nat) ***)
paulson@7519
   400
paulson@8935
   401
Goal "(number_of v = (0::nat)) = \
paulson@7519
   402
\     (if neg (number_of v) then True else iszero (number_of v))";
paulson@7519
   403
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
paulson@7519
   404
qed "eq_number_of_0";
paulson@7519
   405
paulson@8935
   406
Goal "((0::nat) = number_of v) = \
paulson@7519
   407
\     (if neg (number_of v) then True else iszero (number_of v))";
paulson@7519
   408
by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
paulson@7519
   409
qed "eq_0_number_of";
paulson@7519
   410
paulson@8935
   411
Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
paulson@7519
   412
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
paulson@7519
   413
qed "less_0_number_of";
paulson@7519
   414
paulson@7519
   415
(*Simplification already handles n<0, n<=0 and 0<=n.*)
paulson@7519
   416
Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
paulson@7519
   417
paulson@8935
   418
Goal "neg (number_of v) ==> number_of v = (0::nat)";
paulson@8864
   419
by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
paulson@8864
   420
qed "neg_imp_number_of_eq_0";
paulson@8864
   421
paulson@8864
   422
paulson@7519
   423
paulson@7519
   424
(*** Comparisons involving Suc ***)
paulson@7519
   425
paulson@7519
   426
Goal "(number_of v = Suc n) = \
paulson@7519
   427
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   428
\        if neg pv then False else nat pv = n)";
paulson@7519
   429
by (simp_tac
paulson@7519
   430
    (simpset_of Int.thy addsimps
paulson@7519
   431
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
paulson@8864
   432
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
paulson@7519
   433
by (res_inst_tac [("x", "number_of v")] spec 1);
paulson@8864
   434
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
paulson@7519
   435
qed "eq_number_of_Suc";
paulson@7519
   436
paulson@7519
   437
Goal "(Suc n = number_of v) = \
paulson@7519
   438
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   439
\        if neg pv then False else nat pv = n)";
paulson@7519
   440
by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
paulson@7519
   441
qed "Suc_eq_number_of";
paulson@7519
   442
paulson@7519
   443
Goal "(number_of v < Suc n) = \
paulson@7519
   444
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   445
\        if neg pv then True else nat pv < n)";
paulson@7519
   446
by (simp_tac
paulson@7519
   447
    (simpset_of Int.thy addsimps
paulson@7519
   448
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
paulson@8864
   449
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
paulson@7519
   450
by (res_inst_tac [("x", "number_of v")] spec 1);
paulson@8864
   451
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
paulson@7519
   452
qed "less_number_of_Suc";
paulson@7519
   453
paulson@7519
   454
Goal "(Suc n < number_of v) = \
paulson@7519
   455
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   456
\        if neg pv then False else n < nat pv)";
paulson@7519
   457
by (simp_tac
paulson@7519
   458
    (simpset_of Int.thy addsimps
paulson@7519
   459
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
paulson@8864
   460
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
paulson@7519
   461
by (res_inst_tac [("x", "number_of v")] spec 1);
paulson@8864
   462
by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
paulson@7519
   463
qed "less_Suc_number_of";
paulson@7519
   464
paulson@7519
   465
Goal "(number_of v <= Suc n) = \
paulson@7519
   466
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   467
\        if neg pv then True else nat pv <= n)";
paulson@7519
   468
by (simp_tac
paulson@7519
   469
    (simpset_of Int.thy addsimps
paulson@7519
   470
      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
paulson@7519
   471
qed "le_number_of_Suc";
paulson@7519
   472
paulson@7519
   473
Goal "(Suc n <= number_of v) = \
paulson@7519
   474
\       (let pv = number_of (bin_pred v) in \
paulson@7519
   475
\        if neg pv then False else n <= nat pv)";
paulson@7519
   476
by (simp_tac
paulson@7519
   477
    (simpset_of Int.thy addsimps
paulson@7519
   478
      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
paulson@7519
   479
qed "le_Suc_number_of";
paulson@7519
   480
paulson@7519
   481
Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
paulson@7519
   482
	  less_number_of_Suc, less_Suc_number_of, 
paulson@7519
   483
	  le_number_of_Suc, le_Suc_number_of];
nipkow@8116
   484
nipkow@8257
   485
(* Push int(.) inwards: *)
nipkow@8116
   486
Addsimps [int_Suc,zadd_int RS sym];
paulson@8798
   487
paulson@8798
   488
Goal "(m+m = n+n) = (m = (n::int))";
paulson@8798
   489
by Auto_tac;
paulson@8798
   490
val lemma1 = result();
paulson@8798
   491
paulson@8798
   492
Goal "m+m ~= int 1 + n + n";
paulson@8798
   493
by Auto_tac;
paulson@8798
   494
by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
paulson@8798
   495
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
paulson@8798
   496
val lemma2 = result();
paulson@8798
   497
paulson@8798
   498
Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
paulson@8798
   499
\     (x=y & (((number_of v) ::int) = number_of w))"; 
paulson@8798
   500
by (simp_tac (simpset_of Int.thy addsimps
paulson@8798
   501
	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
paulson@8798
   502
qed "eq_number_of_BIT_BIT"; 
paulson@8798
   503
paulson@8798
   504
Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
paulson@8798
   505
\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
paulson@8798
   506
by (simp_tac (simpset_of Int.thy addsimps
paulson@8798
   507
	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
paulson@8798
   508
by (res_inst_tac [("x", "number_of v")] spec 1);
paulson@8798
   509
by Safe_tac;
paulson@8798
   510
by (ALLGOALS Full_simp_tac);
paulson@8798
   511
by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
paulson@8798
   512
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
paulson@8798
   513
qed "eq_number_of_BIT_Pls"; 
paulson@8798
   514
paulson@8798
   515
Goal "((number_of (v BIT x) ::int) = number_of Min) = \
paulson@8798
   516
\     (x=True & (((number_of v) ::int) = number_of Min))"; 
paulson@8798
   517
by (simp_tac (simpset_of Int.thy addsimps
paulson@8798
   518
	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
paulson@8798
   519
by (res_inst_tac [("x", "number_of v")] spec 1);
paulson@8798
   520
by Auto_tac;
paulson@8798
   521
by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
paulson@8798
   522
by Auto_tac;
paulson@8798
   523
qed "eq_number_of_BIT_Min"; 
paulson@8798
   524
paulson@8798
   525
Goal "(number_of Pls ::int) ~= number_of Min"; 
paulson@8798
   526
by Auto_tac;
paulson@8798
   527
qed "eq_number_of_Pls_Min";