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