src/HOL/Divides.thy
changeset 64630 96015aecfeba
parent 64593 50c715579715
child 64635 255741c5f862
     1.1 --- a/src/HOL/Divides.thy	Wed Dec 21 17:37:58 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Dec 20 15:39:13 2016 +0100
     1.3 @@ -781,7 +781,38 @@
     1.4  lemma one_mod_numeral [simp]:
     1.5    "1 mod numeral n = snd (divmod num.One n)"
     1.6    by (simp add: snd_divmod)
     1.7 -  
     1.8 +
     1.9 +text \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close>
    1.10 +
    1.11 +lemma cong_exp_iff_simps:
    1.12 +  "numeral n mod numeral Num.One = 0
    1.13 +    \<longleftrightarrow> True"
    1.14 +  "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
    1.15 +    \<longleftrightarrow> numeral n mod numeral q = 0"
    1.16 +  "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
    1.17 +    \<longleftrightarrow> False"
    1.18 +  "numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
    1.19 +    \<longleftrightarrow> True"
    1.20 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.21 +    \<longleftrightarrow> True"
    1.22 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.23 +    \<longleftrightarrow> False"
    1.24 +  "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.25 +    \<longleftrightarrow> (numeral n mod numeral q) = 0"
    1.26 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.27 +    \<longleftrightarrow> False"
    1.28 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.29 +    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
    1.30 +  "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.31 +    \<longleftrightarrow> False"
    1.32 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
    1.33 +    \<longleftrightarrow> (numeral m mod numeral q) = 0"
    1.34 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
    1.35 +    \<longleftrightarrow> False"
    1.36 +  "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
    1.37 +    \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)"
    1.38 +  by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])
    1.39 +
    1.40  end
    1.41  
    1.42  
    1.43 @@ -1636,37 +1667,6 @@
    1.44    shows "Suc 0 mod numeral k = snd (divmod Num.One k)"
    1.45    by (simp_all add: snd_divmod)
    1.46  
    1.47 -lemma cut_eq_simps: \<comment> \<open>rewriting equivalence on \<open>n mod 2 ^ q\<close>\<close>
    1.48 -  fixes m n q :: num
    1.49 -  shows
    1.50 -    "numeral n mod numeral Num.One = (0::nat)
    1.51 -      \<longleftrightarrow> True"
    1.52 -    "numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.53 -      \<longleftrightarrow> numeral n mod numeral q = (0::nat)"
    1.54 -    "numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = (0::nat)
    1.55 -      \<longleftrightarrow> False"
    1.56 -    "numeral m mod numeral Num.One = (numeral n mod numeral Num.One :: nat)
    1.57 -      \<longleftrightarrow> True"
    1.58 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.59 -      \<longleftrightarrow> True"
    1.60 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.61 -      \<longleftrightarrow> False"
    1.62 -    "numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.63 -      \<longleftrightarrow> (numeral n mod numeral q :: nat) = 0"
    1.64 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.65 -      \<longleftrightarrow> False"
    1.66 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.67 -      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.68 -    "numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.69 -      \<longleftrightarrow> False"
    1.70 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q) :: nat)
    1.71 -      \<longleftrightarrow> (numeral m mod numeral q :: nat) = 0"
    1.72 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) :: nat)
    1.73 -      \<longleftrightarrow> False"
    1.74 -    "numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) :: nat)
    1.75 -      \<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q :: nat)"
    1.76 -  by (auto simp add: case_prod_beta Suc_double_not_eq_double double_not_eq_Suc_double)
    1.77 -
    1.78  
    1.79  subsection \<open>Division on @{typ int}\<close>
    1.80