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.
*)

theory Rewrite
imports Main
begin

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

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

lemma rewr_imp:
  assumes "PROP A ≡ PROP B"
  shows "(PROP A ⟹ PROP C) ≡ (PROP B ⟹ PROP C)"
  apply (rule Pure.equal_intr_rule)
  apply (drule equal_elim_rule2[OF assms]; assumption)
  apply (drule equal_elim_rule1[OF assms]; assumption)
  done

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