haftmann@29650: (*  Title:      HOL/Library/Reflection.thy
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
haftmann@29650: uses "reify_data.ML" ("reflection.ML")
wenzelm@20319: begin
wenzelm@20319: 
haftmann@29650: setup {* Reify_Data.setup *}
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@20374: 
haftmann@29650: method_setup reify = {* fn src =>
haftmann@29650:   Method.syntax (Attrib.thms --
haftmann@29650:     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
wenzelm@30510:   (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
wenzelm@20319: *} "partial automatic reification"
wenzelm@20319: 
chaieb@23649: method_setup reflection = {* 
chaieb@23649: let 
haftmann@29650:   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
haftmann@29650:   val onlyN = "only";
haftmann@29650:   val rulesN = "rules";
haftmann@29650:   val any_keyword = keyword onlyN || keyword rulesN;
haftmann@29650:   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
haftmann@29650:   val terms = thms >> map (term_of o Drule.dest_term);
haftmann@29650:   fun optional scan = Scan.optional scan [];
haftmann@29650: in fn src =>
haftmann@29650:   Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
haftmann@29650:     (fn (((eqs,ths),to), ctxt) => 
chaieb@23649:       let 
chaieb@23649:         val (ceqs,cths) = Reify_Data.get ctxt 
chaieb@23649:         val corr_thms = ths@cths
chaieb@23649:         val raw_eqs = eqs@ceqs
wenzelm@30510:       in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
chaieb@23649:      end) end
wenzelm@20319: *} "reflection method"
haftmann@29650: 
wenzelm@20319: end