src/HOL/Library/Rewrite.thy
author noschinl
Mon Apr 13 20:11:12 2015 +0200 (2015-04-13)
changeset 60054 ef4878146485
parent 60047 58e5b16cbd94
child 61383 6762c8445138
permissions -rw-r--r--
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
     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::{}"
    12 notation rewrite_HOLE ("HOLE")
    13 notation rewrite_HOLE ("\<hole>")
    14 
    15 lemma eta_expand:
    16   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
    17   shows "f \<equiv> \<lambda>x. f x" .
    18 
    19 lemma rewr_imp:
    20   assumes "PROP A \<equiv> PROP B"
    21   shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
    22   apply (rule Pure.equal_intr_rule)
    23   apply (drule equal_elim_rule2[OF assms]; assumption)
    24   apply (drule equal_elim_rule1[OF assms]; assumption)
    25   done
    26 
    27 lemma imp_cong_eq:
    28   "(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'))"
    29   apply (intro Pure.equal_intr_rule)
    30      apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    31    apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
    32   done
    33 
    34 ML_file "cconv.ML"
    35 ML_file "rewrite.ML"
    36 
    37 end