src/HOL/Library/Rewrite.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 61383 6762c8445138
child 69605 a96320074298
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Rewrite.thy
     2     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     3 
     4 Proof method "rewrite" with support for subterm-selection based on patterns.
     5 *)
     6 
     7 theory Rewrite
     8 imports Main
     9 begin
    10 
    11 consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
    12 
    13 lemma eta_expand:
    14   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    15   shows "f \<equiv> \<lambda>x. f x" .
    16 
    17 lemma rewr_imp:
    18   assumes "PROP A \<equiv> PROP B"
    19   shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
    20   apply (rule Pure.equal_intr_rule)
    21   apply (drule equal_elim_rule2[OF assms]; assumption)
    22   apply (drule equal_elim_rule1[OF assms]; assumption)
    23   done
    24 
    25 lemma imp_cong_eq:
    26   "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
    27     ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
    28   apply (intro Pure.equal_intr_rule)
    29      apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    30    apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    31   done
    32 
    33 ML_file "cconv.ML"
    34 ML_file "rewrite.ML"
    35 
    36 end