src/HOL/Divides.thy
changeset 62597 b3f2b8c906a6
parent 62390 842917225d56
child 63040 eb4ddd18d635
     1.1 --- a/src/HOL/Divides.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -1635,6 +1635,37 @@
     1.4    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
     1.5    by (simp_all add: snd_divmod)
     1.6  
     1.7 +lemma cut_eq_simps: -- \<open>rewriting equivalence on @{text "n mod 2 ^ q"}\<close>
     1.8 +  fixes m n q :: num
     1.9 +  shows
    1.10 +    "numeral n mod numeral Num.One = (0::nat)
    1.11 +      \<longleftrightarrow> True"
    1.12 +    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.13 +      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
    1.14 +    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.15 +      \<longleftrightarrow> False"
    1.16 +    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
    1.17 +      \<longleftrightarrow> True"
    1.18 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.19 +      \<longleftrightarrow> True"
    1.20 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.21 +      \<longleftrightarrow> False"
    1.22 +    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.23 +      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
    1.24 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.25 +      \<longleftrightarrow> False"
    1.26 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.27 +      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.28 +    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.29 +      \<longleftrightarrow> False"
    1.30 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.31 +      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
    1.32 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.33 +      \<longleftrightarrow> False"
    1.34 +    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.35 +      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.36 +  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
    1.37 +
    1.38  
    1.39  subsection \<open>Division on @{typ int}\<close>
    1.40