isabelle: src/HOL/Library/Reflection.thy@a65e18ceb1e3 (annotated)

29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	1	(* Title: HOL/Library/Reflection.thy
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	2	Author: Amine Chaieb, TU Muenchen
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	3	*)
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	4
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	5	header {* Generic reflection and reification *}
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	6
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	7	theory Reflection
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	8	imports Main
46764 a65e18ceb1e3 tuned import haftmann parents: 46510 diff changeset	9	uses
a65e18ceb1e3 tuned import haftmann parents: 46510 diff changeset	10	"~~/src/HOL/Library/reify_data.ML"
a65e18ceb1e3 tuned import haftmann parents: 46510 diff changeset	11	"~~/src/HOL/Library/reflection.ML"
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	12	begin
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	13
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	14	setup {* Reify_Data.setup *}
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	15
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	16	method_setup reify = {*
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	17	Attrib.thms --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	18	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")")) >>
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	19	(fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	20	*} "partial automatic reification"
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	21
31412 f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	22	method_setup reflection = {*
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	23	let
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	24	fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	25	val onlyN = "only";
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	26	val rulesN = "rules";
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	27	val any_keyword = keyword onlyN \|\| keyword rulesN;
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	28	val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	29	val terms = thms >> map (term_of o Drule.dest_term);
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	30	in
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	31	thms --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	32	Scan.optional (keyword rulesN \|-- thms) [] --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	33	Scan.option (keyword onlyN \|-- Args.term) >>
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	34	(fn ((eqs,ths),to) => fn ctxt =>
31412 f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	35	let
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	36	val (ceqs,cths) = Reify_Data.get ctxt
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	37	val corr_thms = ths@cths
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	38	val raw_eqs = eqs@ceqs
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	39	in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	40	end
42814 5af15f1e2ef6 simplified/unified method_setup/attribute_setup; wenzelm parents: 31412 diff changeset	41	*}
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	42
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	43	end
46764 a65e18ceb1e3 tuned import haftmann parents: 46510 diff changeset	44

author	haftmann
	Fri, 02 Mar 2012 15:18:05 +0100
changeset 46764	a65e18ceb1e3
parent 46510	696f3fec3f83
child 46765	07f9eda810b3
permissions	-rw-r--r--