[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"

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 (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.