src/HOL/Integ/nat_bin.ML

HOL-Real -> HOL-Complex

(*  Title:      HOL/nat_bin.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1999  University of Cambridge

Binary arithmetic for the natural numbers
*)

val nat_number_of_def = thm "nat_number_of_def";


(** nat (coercion from int to nat) **)

Goal "nat (number_of w) = number_of w";
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
qed "nat_number_of";
Addsimps [nat_number_of, nat_0, nat_1];

Goal "Numeral0 = (0::nat)";
by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); 
qed "numeral_0_eq_0";

Goal "Numeral1 = (1::nat)";
by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); 
qed "numeral_1_eq_1";

Goal "Numeral1 = Suc 0";
by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1); 
qed "numeral_1_eq_Suc_0";

Goalw [nat_number_of_def] "2 = Suc (Suc 0)";
by (rtac nat_2 1); 
qed "numeral_2_eq_2";


(** Distributive laws for "nat".  The others are in IntArith.ML, but these
    require div and mod to be defined for type "int".  They also need 
    some of the lemmas proved just above.**)

Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
by (case_tac "0 <= z'" 1);
by (auto_tac (claset(), 
	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
by (rename_tac "m m'" 1);
by (subgoal_tac "0 <= int m div int m'" 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
by (rtac (inj_int RS injD) 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
 by (Force_tac 2);
by (asm_full_simp_tac 
    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
qed "nat_div_distrib";

(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
by (rename_tac "m m'" 1);
by (subgoal_tac "0 <= int m mod int m'" 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
by (rtac (inj_int RS injD) 1);
by (Asm_simp_tac 1);
by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
 by (Force_tac 2);
by (asm_full_simp_tac 
     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
qed "nat_mod_distrib";


(** int (coercion from nat to int) **)

(*"neg" is used in rewrite rules for binary comparisons*)
Goal "int (number_of v :: nat) = \
\        (if neg (number_of v) then 0 \
\         else (number_of v :: int))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
				  not_neg_nat, int_0]) 1);
qed "int_nat_number_of";
Addsimps [int_nat_number_of];


(** Successor **)

Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
by (rtac sym 1);
by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
qed "Suc_nat_eq_nat_zadd1";

Goal "Suc (number_of v + n) = \
\       (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
				  nat_number_of_def, int_Suc, 
				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
qed "Suc_nat_number_of_add";

Goal "Suc (number_of v) = \
\       (if neg (number_of v) then 1 else number_of (bin_succ v))";
by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);
by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); 
qed "Suc_nat_number_of";
Addsimps [Suc_nat_number_of];

val nat_bin_arith_setup =
 [Fast_Arith.map_data 
   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
      inj_thms = inj_thms,
      lessD = lessD,
      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
                                  not_neg_number_of_Pls,
                                  neg_number_of_Min,neg_number_of_BIT]})];

(** Addition **)

(*"neg" is used in rewrite rules for binary comparisons*)
Goal "(number_of v :: nat) + number_of v' = \
\        (if neg (number_of v) then number_of v' \
\         else if neg (number_of v') then number_of v \
\         else number_of (bin_add v v'))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
				  nat_add_distrib RS sym, number_of_add]) 1);
qed "add_nat_number_of";

Addsimps [add_nat_number_of];


(** Subtraction **)

Goal "nat z - nat z' = \
\       (if neg z' then nat z  \
\        else let d = z-z' in    \
\             if neg d then 0 else nat d)";
by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
qed "diff_nat_eq_if";

Goalw [nat_number_of_def]
     "(number_of v :: nat) - number_of v' = \
\       (if neg (number_of v') then number_of v \
\        else let d = number_of (bin_add v (bin_minus v')) in    \
\             if neg d then 0 else nat d)";
by (simp_tac
    (simpset_of Int.thy delcongs [if_weak_cong]
			addsimps [not_neg_eq_ge_0, nat_0,
				  diff_nat_eq_if, diff_number_of_eq]) 1);
qed "diff_nat_number_of";

Addsimps [diff_nat_number_of];


(** Multiplication **)

Goal "(number_of v :: nat) * number_of v' = \
\      (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
				  nat_mult_distrib RS sym, number_of_mult, 
				  nat_0]) 1);
qed "mult_nat_number_of";

Addsimps [mult_nat_number_of];


(** Quotient **)

Goal "(number_of v :: nat)  div  number_of v' = \
\         (if neg (number_of v) then 0 \
\          else nat (number_of v div number_of v'))";
by (simp_tac
    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
				  nat_div_distrib RS sym, nat_0]) 1);
qed "div_nat_number_of";

Addsimps [div_nat_number_of];


(** Remainder **)

Goal "(number_of v :: nat)  mod  number_of v' = \
\       (if neg (number_of v) then 0 \
\        else if neg (number_of v') then number_of v \
\        else nat (number_of v mod number_of v'))";
by (simp_tac
    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
				  nat_mod_distrib RS sym]) 1);
qed "mod_nat_number_of";

Addsimps [mod_nat_number_of];

structure NatAbstractNumeralsData =
  struct
  val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
  val is_numeral	= Bin_Simprocs.is_numeral
  val numeral_0_eq_0    = numeral_0_eq_0
  val numeral_1_eq_1    = numeral_1_eq_Suc_0
  val prove_conv        = Bin_Simprocs.prove_conv_nohyps_novars
  fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
  val simplify_meta_eq  = Bin_Simprocs.simplify_meta_eq 
  end

structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData)

val nat_eval_numerals = 
  map Bin_Simprocs.prep_simproc
   [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
    ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];

Addsimprocs nat_eval_numerals;


(*** Comparisons ***)

(** Equals (=) **)

Goal "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')";
by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
qed "eq_nat_nat_iff";

(*"neg" is used in rewrite rules for binary comparisons*)
Goal "((number_of v :: nat) = number_of v') = \
\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
\      else if neg (number_of v') then iszero (number_of v) \
\      else iszero (number_of (bin_add v (bin_minus v'))))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
					   iszero_def]) 1);
by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
qed "eq_nat_number_of";

Addsimps [eq_nat_number_of];

(** Less-than (<) **)

(*"neg" is used in rewrite rules for binary comparisons*)
Goal "((number_of v :: nat) < number_of v') = \
\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
\         else neg (number_of (bin_add v (bin_minus v'))))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
				  nat_less_eq_zless, less_number_of_eq_neg,
				  nat_0]) 1);
by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless, 
				number_of_minus, zless_nat_eq_int_zless]) 1);
qed "less_nat_number_of";

Addsimps [less_nat_number_of];


(** Less-than-or-equals (<=) **)

Goal "(number_of x <= (number_of y::nat)) = \
\     (~ number_of y < (number_of x::nat))";
by (rtac (linorder_not_less RS sym) 1);
qed "le_nat_number_of_eq_not_less"; 

Addsimps [le_nat_number_of_eq_not_less];


(*Maps #n to n for n = 0, 1, 2*)
bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
val numeral_ss = simpset() addsimps numerals;

(** Nat **)

Goal "0 < n ==> n = Suc(n - 1)";
by (asm_full_simp_tac numeral_ss 1);
qed "Suc_pred'";

(*Expresses a natural number constant as the Suc of another one.
  NOT suitable for rewriting because n recurs in the condition.*)
bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');

(** Arith **)

Goal "Suc n = n + 1";
by (asm_simp_tac numeral_ss 1);
qed "Suc_eq_add_numeral_1";

(* These two can be useful when m = number_of... *)

Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))";
by (case_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "add_eq_if";

Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))";
by (case_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "mult_eq_if";

Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))";
by (case_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "power_eq_if";

Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)";
by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
qed "diff_less'";

Addsimps [inst "n" "number_of ?v" diff_less'];

(** Power **)

Goal "(p::nat) ^ 2 = p*p";
by (simp_tac numeral_ss 1);
qed "power_two";


(*** Comparisons involving (0::nat) ***)

Goal "(number_of v = (0::nat)) = \
\     (if neg (number_of v) then True else iszero (number_of v))";
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
qed "eq_number_of_0"; 

Goal "((0::nat) = number_of v) = \
\     (if neg (number_of v) then True else iszero (number_of v))";
by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
qed "eq_0_number_of";

Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
qed "less_0_number_of";

(*Simplification already handles n<0, n<=0 and 0<=n.*)
Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];

Goal "neg (number_of v) ==> number_of v = (0::nat)";
by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
qed "neg_imp_number_of_eq_0";



(*** Comparisons involving Suc ***)

Goal "(number_of v = Suc n) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then False else nat pv = n)";
by (simp_tac
    (simpset_of Int.thy addsimps
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
qed "eq_number_of_Suc";

Goal "(Suc n = number_of v) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then False else nat pv = n)";
by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
qed "Suc_eq_number_of";

Goal "(number_of v < Suc n) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then True else nat pv < n)";
by (simp_tac
    (simpset_of Int.thy addsimps
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
qed "less_number_of_Suc";

Goal "(Suc n < number_of v) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then False else n < nat pv)";
by (simp_tac
    (simpset_of Int.thy addsimps
      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
       nat_number_of_def, zadd_0] @ zadd_ac) 1);
by (res_inst_tac [("x", "number_of v")] spec 1);
by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
qed "less_Suc_number_of";

Goal "(number_of v <= Suc n) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then True else nat pv <= n)";
by (simp_tac
    (simpset () addsimps
      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
qed "le_number_of_Suc";

Goal "(Suc n <= number_of v) = \
\       (let pv = number_of (bin_pred v) in \
\        if neg pv then False else n <= nat pv)";
by (simp_tac
    (simpset () addsimps
      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
qed "le_Suc_number_of";

Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
	  less_number_of_Suc, less_Suc_number_of, 
	  le_number_of_Suc, le_Suc_number_of];

(* Push int(.) inwards: *)
Addsimps [zadd_int RS sym];

Goal "(m+m = n+n) = (m = (n::int))";
by Auto_tac;
val lemma1 = result();

Goal "m+m ~= (1::int) + n + n";
by Auto_tac;
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
val lemma2 = result();

Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
\     (x=y & (((number_of v) ::int) = number_of w))"; 
by (simp_tac (simpset_of Int.thy addsimps
	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
qed "eq_number_of_BIT_BIT"; 

Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
\     (x=False & (((number_of v) ::int) = number_of bin.Pls))"; 
by (simp_tac (simpset_of Int.thy addsimps
	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
by (res_inst_tac [("x", "number_of v")] spec 1);
by Safe_tac;
by (ALLGOALS Full_simp_tac);
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
qed "eq_number_of_BIT_Pls"; 

Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
\     (x=True & (((number_of v) ::int) = number_of bin.Min))"; 
by (simp_tac (simpset_of Int.thy addsimps
	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
by (res_inst_tac [("x", "number_of v")] spec 1);
by Auto_tac;
by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
by Auto_tac;
qed "eq_number_of_BIT_Min"; 

Goal "(number_of bin.Pls ::int) ~= number_of bin.Min"; 
by Auto_tac;
qed "eq_number_of_Pls_Min"; 


(*Distributive laws for literals*)
Addsimps (map (inst "k" "number_of ?v")
	  [add_mult_distrib, add_mult_distrib2,
	   diff_mult_distrib, diff_mult_distrib2]);


(*** Literal arithmetic involving powers, type nat ***)

Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
by (induct_tac "n" 1); 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
qed "nat_power_eq";

Goal "(number_of v :: nat) ^ n = \
\      (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
by (simp_tac
    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
				  nat_power_eq]) 1);
qed "power_nat_number_of";

Addsimps [inst "n" "number_of ?w" power_nat_number_of];



(*** Literal arithmetic involving powers, type int ***)

Goal "(z::int) ^ (2*a) = (z^a)^2";
by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1); 
qed "zpower_even";

Goal "(p::int) ^ 2 = p*p"; 
by (simp_tac numeral_ss 1);
qed "zpower_two";  

Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); 
qed "zpower_odd";

Goal "(z::int) ^ number_of (w BIT False) = \
\     (let w = z ^ (number_of w) in  w*w)";
by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
        number_of_BIT, Let_def]) 1);
by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
by (case_tac "(0::int) <= x" 1);
by (auto_tac (claset(), 
     simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); 
qed "zpower_number_of_even";

Goal "(z::int) ^ number_of (w BIT True) = \
\         (if (0::int) <= number_of w                   \
\          then (let w = z ^ (number_of w) in  z*w*w)   \
\          else 1)";
by (simp_tac (simpset_of Int.thy addsimps [nat_number_of_def,
        number_of_BIT, Let_def]) 1);
by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
by (case_tac "(0::int) <= x" 1);
by (auto_tac (claset(), 
              simpset() addsimps [nat_add_distrib, nat_mult_distrib, 
                                  zpower_even, zpower_two])); 
qed "zpower_number_of_odd";

Addsimps (map (inst "z" "number_of ?v")
              [zpower_number_of_even, zpower_number_of_odd]);