# Theory Extra_Congruence_Method

```subsection ‹Congruence Method›

text ‹The following is a method for proving equalities of large terms by checking the equivalence
of subterms. It is possible to precisely control which operators to split by.›

theory Extra_Congruence_Method
imports
Main
"HOL-Eisbach.Eisbach"
begin

datatype cong_tag_type = CongTag

definition cong_tag_1 :: "('a ⇒ 'b) ⇒ cong_tag_type"
where "cong_tag_1 x = CongTag"
definition cong_tag_2 :: "('a ⇒ 'b ⇒ 'c) ⇒ cong_tag_type"
where "cong_tag_2 x = CongTag"
definition cong_tag_3 :: "('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ cong_tag_type"
where "cong_tag_3 x = CongTag"

lemma arg_cong3:
assumes "x1 = x2" "y1 = y2" "z1 = z2"
shows "f x1 y1 z1 = f x2 y2 z2"
using assms by auto

method intro_cong for A :: "cong_tag_type list" uses more =
(match (A) in
"cong_tag_1 f#h" (multi) for f :: "'a ⇒ 'b" and h
⇒ ‹intro_cong h more:more arg_cong[where f="f"]›
¦ "cong_tag_2 f#h" (multi) for f :: "'a ⇒ 'b ⇒ 'c" and h
⇒ ‹intro_cong h more:more arg_cong2[where f="f"]›
¦ "cong_tag_3 f#h" (multi) for f :: "'a ⇒ 'b ⇒ 'c ⇒ 'd" and h
⇒ ‹intro_cong h more:more arg_cong3[where f="f"]›
¦ _ ⇒ ‹intro more refl›)

bundle intro_cong_syntax
begin
notation cong_tag_1 ("σ⇩1")
notation cong_tag_2 ("σ⇩2")
notation cong_tag_3 ("σ⇩3")
end

bundle no_intro_cong_syntax
begin
no_notation cong_tag_1 ("σ⇩1")
no_notation cong_tag_2 ("σ⇩2")
no_notation cong_tag_3 ("σ⇩3")
end

lemma restr_Collect_cong:
assumes "⋀x. x ∈ A ⟹ P x = Q x"
shows "{x ∈ A. P x} = {x ∈ A. Q x}"
using assms by auto

end

```