isabelle: src/HOL/Library/Reflection.thy@b28f258ebc1a (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
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	9	begin
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46765 diff changeset	11	ML_file "~~/src/HOL/Library/reify_data.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46765 diff changeset	12	ML_file "~~/src/HOL/Library/reflection.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46765 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.$$$ ")")) >>
46765 07f9eda810b3 tuned whitespace haftmann parents: 46764 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) >>
46765 07f9eda810b3 tuned whitespace haftmann parents: 46764 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
46765 07f9eda810b3 tuned whitespace haftmann parents: 46764 diff changeset	36	val (ceqs, cths) = Reify_Data.get ctxt
07f9eda810b3 tuned whitespace haftmann parents: 46764 diff changeset	37	val corr_thms = ths @ cths
07f9eda810b3 tuned whitespace haftmann parents: 46764 diff changeset	38	val raw_eqs = eqs @ ceqs
30549 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	hoelzl
	Thu, 17 Jan 2013 11:59:12 +0100
changeset 50936	b28f258ebc1a
parent 48891	c0eafbd55de3
child 51542	738598beeb26
permissions	-rw-r--r--