wenzelm@20319: (*
wenzelm@20319:     ID:         $Id$
wenzelm@20319:     Author:     Amine Chaieb, TU Muenchen
wenzelm@20319: *)
wenzelm@20319: 
wenzelm@20319: header {* Generic reflection and reification *}
wenzelm@20319: 
wenzelm@20319: theory Reflection
wenzelm@20319: imports Main
chaieb@23546:   uses "reflection_data.ML" ("reflection.ML")
wenzelm@20319: begin
wenzelm@20319: 
chaieb@23546: setup {* Reify_Data.setup*}
chaieb@23546: 
chaieb@23546: 
chaieb@20374: lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
chaieb@20374:   by (blast intro: ext)
chaieb@22199: 
chaieb@20374: use "reflection.ML"
chaieb@23546: ML{* Reify_Data.get @{context}*}
chaieb@20374: 
wenzelm@20319: method_setup reify = {*
wenzelm@20319:   fn src =>
wenzelm@20319:     Method.syntax (Attrib.thms --
wenzelm@20319:       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
chaieb@23546:   (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
wenzelm@20319: *} "partial automatic reification"
wenzelm@20319: 
wenzelm@20319: method_setup reflection = {*
wenzelm@20319:   fn src =>
wenzelm@20319:     Method.syntax (Attrib.thms --
wenzelm@20319:       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
chaieb@23546:   (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
wenzelm@20319: *} "reflection method"
wenzelm@20319: 
wenzelm@20319: end