isabelle: src/HOL/ex/Reflection.thy@6a8fb529b542 (annotated)

20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	1	(*
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	2	ID: $Id$
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	3	Author: Amine Chaieb, TU Muenchen
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
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	6	header {* Generic reflection and reification *}
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	7
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	8	theory Reflection
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	9	imports Main
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	10	uses "reflection_data.ML" ("reflection.ML")
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	11	begin
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	12
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	13	setup {* Reify_Data.setup*}
c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	14
c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	15
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	16	lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	17	by (blast intro: ext)
22199 b617ddd200eb Now deals with simples cases where the input equations contain type variables chaieb parents: 21879 diff changeset	18
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	19	use "reflection.ML"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	20
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	21	method_setup reify = {*
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	22	fn src =>
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	23	Method.syntax (Attrib.thms --
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	24	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")"))) src #>
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	25	(fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	26	*} "partial automatic reification"
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	27
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	28	method_setup reflection = {*
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	29	fn src =>
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	30	Method.syntax (Attrib.thms --
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	31	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")"))) src #>
23546 c8a1bd9585a0 reflection and reification methods now manage Context data chaieb parents: 22199 diff changeset	32	(fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	33	*} "reflection method"
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	34
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	35	end

author	chaieb
	Fri, 06 Jul 2007 16:09:27 +0200
changeset 23607	6a8fb529b542
parent 23546	c8a1bd9585a0
child 23649	4d865f3e4405
permissions	-rw-r--r--