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