Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/more_conv.ML
author wenzelm
Fri, 02 Oct 2009 22:02:11 +0200
changeset 32859 204f749f35a9
parent 32843 c8f5a7c8353f
permissions -rw-r--r--
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;

(*  Title:       Tools/more_conv.ML
    Author:      Sascha Boehme, TU Muenchen

Further conversions and conversionals.
*)

signature MORE_CONV =
sig
  val rewrs_conv: thm list -> conv

  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv

  val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
end

structure More_Conv : MORE_CONV =
struct

fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)


fun sub_conv conv ctxt =
  Conv.comb_conv (conv ctxt) else_conv
  Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
  Conv.all_conv

fun bottom_conv conv ctxt ct =
  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct

fun top_conv conv ctxt ct =
  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct

fun top_sweep_conv conv ctxt ct =
  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct


fun binder_conv cv ctxt =
  Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)

end
isabelle