isabelle: src/HOL/ex/Reflection.thy@6472c689664f (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
22199 b617ddd200eb Now deals with simples cases where the input equations contain type variables chaieb parents: 21879 diff changeset	10	uses ("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
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	13	lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	14	by (blast intro: ext)
22199 b617ddd200eb Now deals with simples cases where the input equations contain type variables chaieb parents: 21879 diff changeset	15
20374 01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	16	use "reflection.ML"
01b711328990 Reification now handels binders. chaieb parents: 20319 diff changeset	17
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	18	method_setup reify = {*
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	19	fn src =>
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	20	Method.syntax (Attrib.thms --
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	21	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")"))) src #>
21879 a3efbae45735 switched argument order in .syntax lifters haftmann* parents: 21588 diff changeset	22	(fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs 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
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	25	method_setup reflection = {*
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	26	fn src =>
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	27	Method.syntax (Attrib.thms --
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	28	Scan.option (Scan.lift (Args.$$$ "(") \|-- Args.term --\| Scan.lift (Args.$$$ ")"))) src #>
21879 a3efbae45735 switched argument order in .syntax lifters haftmann* parents: 21588 diff changeset	29	(fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
20319 a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	30	*} "reflection method"
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	31
a8761e8568de Generic reflection and reification (by Amine Chaieb). wenzelm parents: diff changeset	32	end

author	nipkow
	Sun, 17 Jun 2007 08:56:13 +0200
changeset 23402	6472c689664f
parent 22199	b617ddd200eb
child 23546	c8a1bd9585a0
permissions	-rw-r--r--