--- a/src/HOL/Library/Rewrite.thy Mon Apr 13 15:32:32 2015 +0200
+++ b/src/HOL/Library/Rewrite.thy Mon Apr 13 20:11:12 2015 +0200
@@ -16,6 +16,21 @@
fixes f :: "'a::{} \<Rightarrow> 'b::{}"
shows "f \<equiv> \<lambda>x. f x" .
+lemma rewr_imp:
+ assumes "PROP A \<equiv> PROP B"
+ shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> 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 \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv> ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> 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"