src/HOL/Library/Rewrite.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69605 a96320074298
permissions -rw-r--r--
improved code equations taken over from AFP
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@61383
    11
consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
noschinl@59739
    12
noschinl@59739
    13
lemma eta_expand:
wenzelm@59975
    14
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
wenzelm@59975
    15
  shows "f \<equiv> \<lambda>x. f x" .
noschinl@59739
    16
noschinl@60054
    17
lemma rewr_imp:
noschinl@60054
    18
  assumes "PROP A \<equiv> PROP B"
noschinl@60054
    19
  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
noschinl@60054
    20
  apply (rule Pure.equal_intr_rule)
noschinl@60054
    21
  apply (drule equal_elim_rule2[OF assms]; assumption)
noschinl@60054
    22
  apply (drule equal_elim_rule1[OF assms]; assumption)
noschinl@60054
    23
  done
noschinl@60054
    24
noschinl@60054
    25
lemma imp_cong_eq:
wenzelm@61383
    26
  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
wenzelm@61383
    27
    ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
noschinl@60054
    28
  apply (intro Pure.equal_intr_rule)
noschinl@60054
    29
     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
noschinl@60054
    30
   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
noschinl@60054
    31
  done
noschinl@60054
    32
wenzelm@69605
    33
ML_file \<open>cconv.ML\<close>
wenzelm@69605
    34
ML_file \<open>rewrite.ML\<close>
noschinl@59739
    35
noschinl@59739
    36
end