src/HOL/Library/Rewrite.thy
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 60054 ef4878146485
child 61383 6762c8445138
permissions -rw-r--r--
isabelle update_cartouches;
wenzelm@59975
     1
(*  Title:      HOL/Library/Rewrite.thy
wenzelm@59975
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
wenzelm@59975
     3
wenzelm@59975
     4
Proof method "rewrite" with support for subterm-selection based on patterns.
wenzelm@59975
     5
*)
wenzelm@59975
     6
noschinl@59739
     7
theory Rewrite
noschinl@59739
     8
imports Main
noschinl@59739
     9
begin
noschinl@59739
    10
wenzelm@59975
    11
consts rewrite_HOLE :: "'a::{}"
noschinl@59739
    12
notation rewrite_HOLE ("HOLE")
noschinl@60047
    13
notation rewrite_HOLE ("\<hole>")
noschinl@59739
    14
noschinl@59739
    15
lemma eta_expand:
wenzelm@59975
    16
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
wenzelm@59975
    17
  shows "f \<equiv> \<lambda>x. f x" .
noschinl@59739
    18
noschinl@60054
    19
lemma rewr_imp:
noschinl@60054
    20
  assumes "PROP A \<equiv> PROP B"
noschinl@60054
    21
  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
noschinl@60054
    22
  apply (rule Pure.equal_intr_rule)
noschinl@60054
    23
  apply (drule equal_elim_rule2[OF assms]; assumption)
noschinl@60054
    24
  apply (drule equal_elim_rule1[OF assms]; assumption)
noschinl@60054
    25
  done
noschinl@60054
    26
noschinl@60054
    27
lemma imp_cong_eq:
noschinl@60054
    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'))"
noschinl@60054
    29
  apply (intro Pure.equal_intr_rule)
noschinl@60054
    30
     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
noschinl@60054
    31
   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
noschinl@60054
    32
  done
noschinl@60054
    33
noschinl@59739
    34
ML_file "cconv.ML"
noschinl@59739
    35
ML_file "rewrite.ML"
noschinl@59739
    36
noschinl@59739
    37
end