1.1 --- a/src/HOL/Integ/NatBin.ML Tue Nov 23 11:19:39 1999 +0100
1.2 +++ b/src/HOL/Integ/NatBin.ML Wed Nov 24 10:25:28 1999 +0100
1.3 @@ -66,10 +66,10 @@
1.4
1.5 (** Addition **)
1.6
1.7 -Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat z + nat z' = nat (z+z')";
1.8 +Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
1.9 by (rtac (inj_int RS injD) 1);
1.10 by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
1.11 -qed "add_nat_eq_nat_zadd";
1.12 +qed "nat_add_distrib";
1.13
1.14 (*"neg" is used in rewrite rules for binary comparisons*)
1.15 Goal "(number_of v :: nat) + number_of v' = \
1.16 @@ -78,7 +78,7 @@
1.17 \ else number_of (bin_add v v'))";
1.18 by (simp_tac
1.19 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
1.20 - add_nat_eq_nat_zadd, number_of_add]) 1);
1.21 + nat_add_distrib RS sym, number_of_add]) 1);
1.22 qed "add_nat_number_of";
1.23
1.24 Addsimps [add_nat_number_of];
1.25 @@ -86,17 +86,17 @@
1.26
1.27 (** Subtraction **)
1.28
1.29 -Goal "[| (#0::int) <= z'; z' <= z |] ==> nat z - nat z' = nat (z-z')";
1.30 +Goal "[| (#0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
1.31 by (rtac (inj_int RS injD) 1);
1.32 by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
1.33 -qed "diff_nat_eq_nat_zdiff";
1.34 +qed "nat_diff_distrib";
1.35
1.36
1.37 Goal "nat z - nat z' = \
1.38 \ (if neg z' then nat z \
1.39 \ else let d = z-z' in \
1.40 \ if neg d then 0 else nat d)";
1.41 -by (simp_tac (simpset() addsimps [Let_def, diff_nat_eq_nat_zdiff,
1.42 +by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
1.43 neg_eq_less_0, not_neg_eq_ge_0]) 1);
1.44 by (simp_tac (simpset() addsimps zcompare_rls@
1.45 [diff_is_0_eq, nat_le_eq_zle]) 1);
1.46 @@ -118,7 +118,7 @@
1.47
1.48 (** Multiplication **)
1.49
1.50 -Goal "(#0::int) <= z ==> nat z * nat z' = nat (z*z')";
1.51 +Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
1.52 by (case_tac "#0 <= z'" 1);
1.53 by (subgoal_tac "z'*z <= #0" 2);
1.54 by (rtac (neg_imp_zmult_nonpos_iff RS iffD2) 3);
1.55 @@ -128,13 +128,13 @@
1.56 by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
1.57 by (rtac (inj_int RS injD) 1);
1.58 by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
1.59 -qed "mult_nat_eq_nat_zmult";
1.60 +qed "nat_mult_distrib";
1.61
1.62 Goal "(number_of v :: nat) * number_of v' = \
1.63 \ (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
1.64 by (simp_tac
1.65 (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
1.66 - mult_nat_eq_nat_zmult, number_of_mult,
1.67 + nat_mult_distrib RS sym, number_of_mult,
1.68 nat_0]) 1);
1.69 qed "mult_nat_number_of";
1.70
1.71 @@ -143,7 +143,7 @@
1.72
1.73 (** Quotient **)
1.74
1.75 -Goal "(#0::int) <= z ==> nat z div nat z' = nat (z div z')";
1.76 +Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
1.77 by (case_tac "#0 <= z'" 1);
1.78 by (auto_tac (claset(),
1.79 simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
1.80 @@ -156,7 +156,6 @@
1.81 pos_imp_zdiv_nonneg_iff]) 2);
1.82 by (rtac (inj_int RS injD) 1);
1.83 by (Asm_simp_tac 1);
1.84 -by (rtac sym 1);
1.85 by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
1.86 by (Force_tac 2);
1.87 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
1.88 @@ -164,14 +163,14 @@
1.89 mod_less_divisor]) 1);
1.90 by (rtac (mod_div_equality RS sym RS trans) 1);
1.91 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
1.92 -qed "div_nat_eq_nat_zdiv";
1.93 +qed "nat_div_distrib";
1.94
1.95 Goal "(number_of v :: nat) div number_of v' = \
1.96 \ (if neg (number_of v) then #0 \
1.97 \ else nat (number_of v div number_of v'))";
1.98 by (simp_tac
1.99 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat,
1.100 - div_nat_eq_nat_zdiv, nat_0]) 1);
1.101 + nat_div_distrib RS sym, nat_0]) 1);
1.102 qed "div_nat_number_of";
1.103
1.104 Addsimps [div_nat_number_of];
1.105 @@ -180,7 +179,7 @@
1.106 (** Remainder **)
1.107
1.108 (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
1.109 -Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat z mod nat z' = nat (z mod z')";
1.110 +Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
1.111 by (zdiv_undefined_case_tac "z' = #0" 1);
1.112 by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
1.113 by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
1.114 @@ -190,7 +189,6 @@
1.115 pos_mod_sign]) 2);
1.116 by (rtac (inj_int RS injD) 1);
1.117 by (Asm_simp_tac 1);
1.118 -by (rtac sym 1);
1.119 by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
1.120 by (Force_tac 2);
1.121 by (asm_simp_tac (simpset() addsimps [nat_less_iff RS sym, quorem_def,
1.122 @@ -198,7 +196,7 @@
1.123 mod_less_divisor]) 1);
1.124 by (rtac (mod_div_equality RS sym RS trans) 1);
1.125 by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
1.126 -qed "mod_nat_eq_nat_zmod";
1.127 +qed "nat_mod_distrib";
1.128
1.129 Goal "(number_of v :: nat) mod number_of v' = \
1.130 \ (if neg (number_of v) then #0 \
1.131 @@ -207,7 +205,7 @@
1.132 by (simp_tac
1.133 (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def,
1.134 neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
1.135 - mod_nat_eq_nat_zmod]) 1);
1.136 + nat_mod_distrib RS sym]) 1);
1.137 qed "mod_nat_number_of";
1.138
1.139 Addsimps [mod_nat_number_of];