src/HOL/Library/Rewrite.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 61383 6762c8445138
child 69605 a96320074298
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     1
(*  Title:      HOL/Library/Rewrite.thy
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     2
    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     3
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     4
Proof method "rewrite" with support for subterm-selection based on patterns.
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     5
*)
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
     6
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
     7
theory Rewrite
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
     8
imports Main
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
     9
begin
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    10
61383
6762c8445138 use Isabelle symbols by default;
wenzelm
parents: 60054
diff changeset
    11
consts rewrite_HOLE :: "'a::{}"  ("\<hole>")
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    12
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    13
lemma eta_expand:
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
    14
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
    15
  shows "f \<equiv> \<lambda>x. f x" .
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    16
60054
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    17
lemma rewr_imp:
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    18
  assumes "PROP A \<equiv> PROP B"
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    19
  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    20
  apply (rule Pure.equal_intr_rule)
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    21
  apply (drule equal_elim_rule2[OF assms]; assumption)
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    22
  apply (drule equal_elim_rule1[OF assms]; assumption)
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    23
  done
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    24
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    25
lemma imp_cong_eq:
61383
6762c8445138 use Isabelle symbols by default;
wenzelm
parents: 60054
diff changeset
    26
  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv>
6762c8445138 use Isabelle symbols by default;
wenzelm
parents: 60054
diff changeset
    27
    ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
60054
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    28
  apply (intro Pure.equal_intr_rule)
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    29
     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    30
   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    31
  done
ef4878146485 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents: 60047
diff changeset
    32
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    33
ML_file "cconv.ML"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    34
ML_file "rewrite.ML"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    35
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    36
end