[isabelle] Congruence rules for modular arithmetic



Hi,

I'm trying to use congruence rules to simplify modular arithmetic expressions. For example, I'd like to automatically prove the following:

  lemma test1: "((x::int) * y mod 2) mod 2 = (x * y) mod 2"

  lemma test2: "((x::int) + y mod 2) mod 2 = (x + y) mod 2"

To do this, I made a special definition

  definition
    cong_zmod :: "int => int => int" where
   "cong_zmod p x == x mod p"

and then the following congruence rules (among others):

  lemma zmod_cong:
    assumes "p = p'"
        and "cong_zmod p' x = cong_zmod p' x'"
    shows "x mod p = x' mod p'"

  lemma cong_zmod_mod[simp]:
    "p dvd q ==> cong_zmod p (x mod q) = cong_zmod p x"

  lemma cong_zmod_plus[cong]:
    assumes A1: "p = p'"
        and A2: "cong_zmod p' x = cong_zmod p' x'"
        and A3: "cong_zmod p' y = cong_zmod p' y'"
        and A4: "x' + y' = z"
    shows "cong_zmod p (x + y) = cong_zmod p' z"

  lemma cong_zmod_mult[cong]:
    assumes A1: "cong_zmod p x = cong_zmod p x'"
        and A2: "cong_zmod p y = cong_zmod p y'"
        and A3: "x' * y' = z"
    shows "cong_zmod p (x * y) = cong_zmod p z"

With these congruence rules, I can get Isabelle to prove the first lemma:

  lemma test1: "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
  by (simp cong: zmod_cong)

but not the second:

  lemma test2: "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
  by (simp cong: zmod_cong)

  [Isabelle's response:  *** Terminal proof method failed
                         *** At command "by".]

Since Isabelle only stores one congruence rule for any given function symbol, the congruence rule cong_zmod_mult clobbers cong_zmod_plus.

Is there any way to fix this so Isabelle can have multiple congruence rules for a function symbol, when the left-hand-sides are distinct? The alternative of coding this up as a simproc wouldn't interact well with other modular arithmetic simplification rules that users may want to add later on.

I'm appending the complete theory below.

Thanks,
-john

------------------------------------

theory "zmod_cong_plus_example"
imports "~~/src/HOL/Word/WordGenLib"
begin

definition
  cong_zmod :: "int \<Rightarrow> int \<Rightarrow> int" where
 "cong_zmod p x \<equiv> x mod p"

lemma zmod_cong:
  assumes "p = p'"
      and "cong_zmod p' x = cong_zmod p' x'"
  shows "x mod p = x' mod p'"
by (cut_tac prems, simp add: cong_zmod_def)

lemma cong_zmod_mod[simp]:
  "p dvd q \<Longrightarrow> cong_zmod p (x mod q) = cong_zmod p x"
by (simp add: cong_zmod_def zmod_zmod_cancel)

lemma cong_zmod_plus[cong]:
  assumes A1: "p = p'"
      and A2: "cong_zmod p' x = cong_zmod p' x'"
      and A3: "cong_zmod p' y = cong_zmod p' y'"
      and A4: "x' + y' = z"
  shows "cong_zmod p (x + y) = cong_zmod p' z"
apply (cut_tac prems)
by (simp add: cong_zmod_def cong: mod_plus_cong)

-- "REVISIT: Submit to WordGenLib.thy"
lemma mod_mult_cong:
  assumes A1: "b = b'"
      and A2: "(x::int) mod b' = x' mod b'"
      and A3: "(y\<Colon>int) mod b' = y' mod b'"
      and A4: "x' * y' = z'"
  shows "(x * y) mod b = z' mod b'"
apply (simp add: A1)
apply (subst pull_mods(2)[symmetric])
by (simp add: A2 A3 A4 pull_mods(2))

lemma cong_zmod_mult[cong]:
  assumes A1: "cong_zmod p x = cong_zmod p x'"
      and A2: "cong_zmod p y = cong_zmod p y'"
      and A3: "x' * y' = z"
  shows "cong_zmod p (x * y) = cong_zmod p z"
apply (cut_tac prems)
by (simp add: cong_zmod_def cong: mod_mult_cong)

lemma test1:
  "((x::int) * y mod 2) mod 2 = (x * y) mod 2"
apply (simp cong: zmod_cong)
done

lemma test2:
  "((x::int) + y mod 2) mod 2 = (x + y) mod 2"
apply (simp cong: zmod_cong)
done

end








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.