src/HOL/Library/Rewrite.thy
author wenzelm
Wed, 08 Apr 2015 21:24:27 +0200
changeset 59975 da10875adf8e
parent 59739 4ed50ebf5d36
child 60047 58e5b16cbd94
permissions -rw-r--r--
more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;
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")
4ed50ebf5d36 added proof method rewrite
noschinl
parents:
diff changeset
    13
notation rewrite_HOLE ("\<box>")
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