isabelle: src/HOL/Tools/Meson/meson_tactic.ML@d969474ddc45 (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
74075 a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output desharna parents: 74051 diff changeset	18	in
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output desharna parents: 74051 diff changeset	19	Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt'
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output desharna parents: 74051 diff changeset	20	false true 0) ths)
a5bab59d580b added support for TFX $let to Sledgehammer's TPTP output desharna parents: 74051 diff changeset	21	end
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	22
58817 4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	23	val _ =
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	24	Theory.setup
67149 e61557884799 prefer control symbol antiquotations; wenzelm parents: 58817 diff changeset	25	(Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt =>
58817 4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	26	SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
4cd778c91fdc modernized setup; wenzelm parents: 45508 diff changeset	27	"MESON resolution proof procedure")
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	28
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: diff changeset	29	end;

author	desharna
	Fri, 10 Dec 2021 08:58:09 +0100
changeset 74903	d969474ddc45
parent 74075	a5bab59d580b
child 75009	d2f97439f53e
permissions	-rw-r--r--