isabelle: src/HOL/Tools/Meson/meson_tactic.ML@e9e7209eb375 (annotated)

39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	1	(* Title: HOL/Tools/Meson/meson_tactic.ML
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	2	Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	4
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	5	The "meson" proof method for HOL.
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	6	*)
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	7
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	8	signature MESON_TACTIC =
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	9	sig
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	10	val meson_general_tac : Proof.context -> thm list -> int -> tactic
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	11	val setup: theory -> theory
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	12	end;
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	13
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	14	structure Meson_Tactic : MESON_TACTIC =
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	15	struct
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	16
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	17	open Meson_Clausify
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	18
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	19	fun meson_general_tac ctxt ths =
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 39948 diff changeset	20	let val ctxt' = put_claset HOL_cs ctxt
45508 b216dc1b3630 started implementing lambda-lifting in Metis blanchet parents: 42793 diff changeset	21	in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	22
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	23	val setup =
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	24	Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	25	SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	26	"MESON resolution proof procedure"
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	27
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	28	end;

author	haftmann
	Thu, 01 Mar 2012 19:34:52 +0100
changeset 46752	e9e7209eb375
parent 45508	b216dc1b3630
child 58817	4cd778c91fdc
permissions	-rw-r--r--