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