src/HOL/Eisbach/Eisbach.thy

updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;

(*  Title:      Eisbach.thy
    Author:     Daniel Matichuk, NICTA/UNSW

Main entry point for Eisbach proof method language.
*)

theory Eisbach
imports Pure
keywords
  "method" :: thy_decl and
  "conclusion"
  "premises"
  "declares"
  "methods"
  "\<bar>" "\<Rightarrow>"
  "uses"
begin


ML_file "parse_tools.ML"
ML_file "eisbach_rule_insts.ML"
ML_file "method_closure.ML"
ML_file "match_method.ML"
ML_file "eisbach_antiquotations.ML"

(* FIXME reform Isabelle/Pure attributes to make this work by default *)
attribute_setup THEN =
  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm >> (fn (i, B) =>
    Method_Closure.free_aware_rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
  "resolution with rule"

attribute_setup OF =
  \<open>Attrib.thms >> (fn Bs =>
    Method_Closure.free_aware_rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
  "rule resolved with facts"

attribute_setup rotated =
  \<open>Scan.lift (Scan.optional Parse.int 1 >> (fn n =>
    Method_Closure.free_aware_rule_attribute [] (fn _ => rotate_prems n)))\<close>
  "rotated theorem premises"

method solves methods m = (m; fail)

end