isabelle: src/HOL/Tools/Meson/meson_tactic.ML@64b47495676d (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	end;
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	12
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	13	structure Meson_Tactic : MESON_TACTIC =
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	14	struct
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	15
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	16	fun meson_general_tac ctxt ths =
42793 88bee9f6eec7 proper Proof.context for classical tactics; wenzelm parents: 39948 diff changeset	17	let val ctxt' = put_claset HOL_cs ctxt
58817 4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	18	in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom ctxt' false true 0) ths) end
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	19
58817 4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	20	val _ =
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	21	Theory.setup
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	22	(Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	23	SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	24	"MESON resolution proof procedure")
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	25
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	26	end;

author	wenzelm
	Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787	64b47495676d
parent 58817	4cd778c91fdc
child 67149	e61557884799
permissions	-rw-r--r--