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