src/HOL/Library/Rewrite.thy
changeset 60054 ef4878146485
parent 60047 58e5b16cbd94
child 61383 6762c8445138
     1.1 --- a/src/HOL/Library/Rewrite.thy	Mon Apr 13 15:32:32 2015 +0200
     1.2 +++ b/src/HOL/Library/Rewrite.thy	Mon Apr 13 20:11:12 2015 +0200
     1.3 @@ -16,6 +16,21 @@
     1.4    fixes f :: "'a::{} \<Rightarrow> 'b::{}"
     1.5    shows "f \<equiv> \<lambda>x. f x" .
     1.6  
     1.7 +lemma rewr_imp:
     1.8 +  assumes "PROP A \<equiv> PROP B"
     1.9 +  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
    1.10 +  apply (rule Pure.equal_intr_rule)
    1.11 +  apply (drule equal_elim_rule2[OF assms]; assumption)
    1.12 +  apply (drule equal_elim_rule1[OF assms]; assumption)
    1.13 +  done
    1.14 +
    1.15 +lemma imp_cong_eq:
    1.16 +  "(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'))"
    1.17 +  apply (intro Pure.equal_intr_rule)
    1.18 +     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    1.19 +   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    1.20 +  done
    1.21 +
    1.22  ML_file "cconv.ML"
    1.23  ML_file "rewrite.ML"
    1.24