isabelle: src/HOL/Tools/Sledgehammer/meson_tactic.ML@135f7d489492 (annotated)

35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	1	(* Title: HOL/Tools/Sledgehammer/meson_tactic.ML
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	2	Author: Jia Meng, Cambridge University Computer Laboratory
37619 bcb19259f92a killed "expand_defs_tac"; blanchet parents: 37618 diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	4
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	5	MESON general tactic and proof method.
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	6	*)
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	7
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	8	signature MESON_TACTIC =
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	9	sig
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	10	val meson_general_tac : Proof.context -> thm list -> int -> tactic
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	11	val setup: theory -> theory
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	12	end;
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	13
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	14	structure Meson_Tactic : MESON_TACTIC =
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	15	struct
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	16
37619 bcb19259f92a killed "expand_defs_tac"; blanchet parents: 37618 diff changeset	17	fun meson_general_tac ctxt ths =
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	18	let
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	19	val thy = ProofContext.theory_of ctxt
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	20	val ctxt0 = Classical.put_claset HOL_cs ctxt
38016 135f7d489492 get rid of more dead wood blanchet parents: 37628 diff changeset	21	in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	22
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	23	val setup =
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	24	Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	25	SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	26	"MESON resolution proof procedure";
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	27
2f8fb5242799 more Sledgehammer refactoring blanchet parents: diff changeset	28	end;

author	blanchet
	Tue, 27 Jul 2010 17:15:12 +0200
changeset 38016	135f7d489492
parent 37628	78334f400ae6
child 38027	505657ddb047
permissions	-rw-r--r--