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: "(\x. f x = g x) \ f = g" chaieb@20374: by (blast intro: ext) chaieb@22199: chaieb@20374: use "reflection.ML" chaieb@20374: wenzelm@30549: method_setup reify = {* wenzelm@30549: Attrib.thms -- wenzelm@30549: Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >> wenzelm@30549: (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) wenzelm@20319: *} "partial automatic reification" wenzelm@20319: hoelzl@31412: method_setup reflection = {* hoelzl@31412: 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); wenzelm@30549: in wenzelm@30549: thms -- wenzelm@30549: Scan.optional (keyword rulesN |-- thms) [] -- wenzelm@30549: Scan.option (keyword onlyN |-- Args.term) >> wenzelm@30549: (fn ((eqs,ths),to) => fn ctxt => hoelzl@31412: let hoelzl@31412: val (ceqs,cths) = Reify_Data.get ctxt wenzelm@30549: val corr_thms = ths@cths wenzelm@30549: val raw_eqs = eqs@ceqs wenzelm@30549: in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end) wenzelm@30549: end wenzelm@42814: *} haftmann@29650: wenzelm@20319: end