src/HOL/NatBin.thy

 
 notation (HTML output)
   square  ("(_\<twosuperior>)" [1000] 999)
 
 
+subsection {* Predicate for negative binary numbers *}
+
+definition
+  neg  :: "int \<Rightarrow> bool"
+where
+  "neg Z \<longleftrightarrow> Z < 0"
+
+lemma not_neg_int [simp]: "~ neg (of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+text{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: neg_def order_less_imp_le) 
+
+lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+text {*
+  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+  @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
+lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Min: "neg (number_of Int.Min)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Bit0:
+  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Bit1:
+  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
+  by (simp add: neg_def)
+
+lemmas neg_simps [simp] =
+  not_neg_0 not_neg_1
+  not_neg_number_of_Pls neg_number_of_Min
+  neg_number_of_Bit0 neg_number_of_Bit1
+
+
 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
 
 declare nat_0 [simp] nat_1 [simp]
 
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"

 apply (unfold nat_number_of_def)
 apply (rule nat_2)
 done
 
 
-text{*Distributive laws for type @{text nat}.  The others are in theory
-   @{text IntArith}, but these require div and mod to be defined for type
-   "int".  They also need some of the lemmas proved above.*}
-
-lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
-apply (case_tac "0 <= z'")
-apply (auto simp add: div_nonneg_neg_le0)
-apply (case_tac "z' = 0", simp)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
- prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
-     "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule int_int_eq [THEN iffD1], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
-                 of_nat_add [symmetric] of_nat_mult [symmetric]
-            del: of_nat_add of_nat_mult)
-done
-
-text{*Suggested by Matthias Daum*}
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp (asm_lr) add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all) 
-done
-
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma int_nat_number_of [simp]:
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
   unfolding nat_number_of_def number_of_is_id neg_def

 done
 
 
 subsubsection{*Addition *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
      "(number_of v :: nat) + number_of v' =  
          (if v < Int.Pls then number_of v'  
           else if v' < Int.Pls then number_of v  
           else number_of (v + v'))"

 
 lemma eq_nat_nat_iff:
      "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
 by (auto elim!: nonneg_eq_int)
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma eq_nat_number_of [simp]:
      "((number_of v :: nat) = number_of v') =  
       (if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
        else if neg (number_of v' :: int) then (number_of v :: int) = 0
        else v = v')"

  LinArith.map_data
    (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
      {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
       inj_thms = inj_thms,
       lessD = lessD, neqE = neqE,
-      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
-        @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
-        @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
+      simpset = simpset addsimps @{thms neg_simps} @
+        [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
 *}
 
 declaration {* K nat_bin_arith_setup *}
 
 (* Enable arith to deal with div/mod k where k is a numeral: *)