src/HOL/Library/Reflection.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 42814 5af15f1e2ef6
child 45966 03ce2b2a29a2
permissions -rw-r--r--
add nat => enat coercion
     1 (*  Title:      HOL/Library/Reflection.thy
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 header {* Generic reflection and reification *}
     6 
     7 theory Reflection
     8 imports Main
     9 uses "reify_data.ML" ("reflection.ML")
    10 begin
    11 
    12 setup {* Reify_Data.setup *}
    13 
    14 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    15   by (blast intro: ext)
    16 
    17 use "reflection.ML"
    18 
    19 method_setup reify = {*
    20   Attrib.thms --
    21     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    22   (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    23 *} "partial automatic reification"
    24 
    25 method_setup reflection = {*
    26 let
    27   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    28   val onlyN = "only";
    29   val rulesN = "rules";
    30   val any_keyword = keyword onlyN || keyword rulesN;
    31   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    32   val terms = thms >> map (term_of o Drule.dest_term);
    33 in
    34   thms --
    35   Scan.optional (keyword rulesN |-- thms) [] --
    36   Scan.option (keyword onlyN |-- Args.term) >>
    37   (fn ((eqs,ths),to) => fn ctxt =>
    38     let
    39       val (ceqs,cths) = Reify_Data.get ctxt
    40       val corr_thms = ths@cths
    41       val raw_eqs = eqs@ceqs
    42     in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    43 end
    44 *}
    45 
    46 end