src/HOL/Library/Reflection.thy
changeset 29650 cc3958d31b1d
parent 23649 4d865f3e4405
child 30510 4120fc59dd85
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Reflection.thy	Wed Jan 28 11:04:10 2009 +0100
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      HOL/Library/Reflection.thy
     1.5 +    Author:     Amine Chaieb, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Generic reflection and reification *}
     1.9 +
    1.10 +theory Reflection
    1.11 +imports Main
    1.12 +uses "reify_data.ML" ("reflection.ML")
    1.13 +begin
    1.14 +
    1.15 +setup {* Reify_Data.setup *}
    1.16 +
    1.17 +lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    1.18 +  by (blast intro: ext)
    1.19 +
    1.20 +use "reflection.ML"
    1.21 +
    1.22 +method_setup reify = {* fn src =>
    1.23 +  Method.syntax (Attrib.thms --
    1.24 +    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    1.25 +  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    1.26 +*} "partial automatic reification"
    1.27 +
    1.28 +method_setup reflection = {* 
    1.29 +let 
    1.30 +  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    1.31 +  val onlyN = "only";
    1.32 +  val rulesN = "rules";
    1.33 +  val any_keyword = keyword onlyN || keyword rulesN;
    1.34 +  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.35 +  val terms = thms >> map (term_of o Drule.dest_term);
    1.36 +  fun optional scan = Scan.optional scan [];
    1.37 +in fn src =>
    1.38 +  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
    1.39 +    (fn (((eqs,ths),to), ctxt) => 
    1.40 +      let 
    1.41 +        val (ceqs,cths) = Reify_Data.get ctxt 
    1.42 +        val corr_thms = ths@cths
    1.43 +        val raw_eqs = eqs@ceqs
    1.44 +      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    1.45 +     end) end
    1.46 +*} "reflection method"
    1.47 +
    1.48 +end