isabelle: src/HOL/Library/Reflection.thy@dd2f49d88b47 (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
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	9	uses "reify_data.ML" ("reflection.ML")
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	10	begin
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	11
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	12	setup {* Reify_Data.setup *}
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	13
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	14	lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	15	by (blast intro: ext)
22199 b617ddd200eb Now deals with simples cases where the input equations contain type variables chaieb parents: 21879 diff changeset	16
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	17	use "reflection.ML"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	18
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	19	method_setup reify = {*
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	20	Attrib.thms --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	21	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")")) >>
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	22	(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	23	*} "partial automatic reification"
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	24
31412 f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	25	method_setup reflection = {*
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	26	let
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	27	fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	28	val onlyN = "only";
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	29	val rulesN = "rules";
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	30	val any_keyword = keyword onlyN \|\| keyword rulesN;
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	31	val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	32	val terms = thms >> map (term_of o Drule.dest_term);
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	33	in
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	34	thms --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	35	Scan.optional (keyword rulesN \|-- thms) [] --
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	36	Scan.option (keyword onlyN \|-- Args.term) >>
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	37	(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	38	let
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations. hoelzl parents: 30549 diff changeset	39	val (ceqs,cths) = Reify_Data.get ctxt
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	40	val corr_thms = ths@cths
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	41	val raw_eqs = eqs@ceqs
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	42	in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	43	end
d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	44	*} "reflection"
29650 cc3958d31b1d Reflection.thy now in HOL/Library haftmann parents: 23649 diff changeset	45
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	46	end

author	wenzelm
	Mon, 28 Dec 2009 22:58:25 +0100
changeset 34203	dd2f49d88b47
parent 31412	f2e6b6526092
child 42814	5af15f1e2ef6
permissions	-rw-r--r--