Theory Rewrite

(*  Title:      HOL/Library/Rewrite.thy
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen

Proof method "rewrite" with support for subterm-selection based on patterns.

Documentation: https://arxiv.org/abs/2111.04082
*)

theory Rewrite
imports Main
begin

consts rewrite_HOLE :: "'a::{}"  ("")

lemma eta_expand:
  fixes f :: "'a::{}  'b::{}"
  shows "f  λx. f x" .

lemma imp_cong_eq:
  "(PROP A  (PROP B  PROP C)  (PROP B'  PROP C')) 
    ((PROP B  PROP A  PROP C)  (PROP B'  PROP A  PROP C'))"
  apply (intro Pure.equal_intr_rule)
     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
  done

ML_file ‹cconv.ML›
ML_file ‹rewrite.ML›

end