src/HOL/Library/Rewrite.thy
author noschinl
Mon, 13 Apr 2015 10:21:35 +0200
changeset 60047 58e5b16cbd94
parent 59975 da10875adf8e
child 60054 ef4878146485
permissions -rw-r--r--
enable \<hole> syntax for rewrite
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
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
    11
consts rewrite_HOLE :: "'a::{}"
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    12
notation rewrite_HOLE ("HOLE")
60047
58e5b16cbd94 enable \<hole> syntax for rewrite
noschinl
parents: 59975
diff changeset
    13
notation rewrite_HOLE ("\<hole>")
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    14
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    15
lemma eta_expand:
59975
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
    16
  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
da10875adf8e more standard Isabelle/ML tool setup;
wenzelm
parents: 59739
diff changeset
    17
  shows "f \<equiv> \<lambda>x. f x" .
59739
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    18
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    19
ML_file "cconv.ML"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    20
ML_file "rewrite.ML"
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    21
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    22
end