src/HOL/Library/Reflection.thy
author haftmann
Wed Jan 28 11:04:10 2009 +0100 (2009-01-28)
changeset 29650 cc3958d31b1d
parent 23649 src/HOL/ex/Reflection.thy@4d865f3e4405
child 30510 4120fc59dd85
permissions -rw-r--r--
Reflection.thy now in HOL/Library
haftmann@29650
     1
(*  Title:      HOL/Library/Reflection.thy
wenzelm@20319
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     3
*)
wenzelm@20319
     4
wenzelm@20319
     5
header {* Generic reflection and reification *}
wenzelm@20319
     6
wenzelm@20319
     7
theory Reflection
wenzelm@20319
     8
imports Main
haftmann@29650
     9
uses "reify_data.ML" ("reflection.ML")
wenzelm@20319
    10
begin
wenzelm@20319
    11
haftmann@29650
    12
setup {* Reify_Data.setup *}
chaieb@23546
    13
chaieb@20374
    14
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
chaieb@20374
    15
  by (blast intro: ext)
chaieb@22199
    16
chaieb@20374
    17
use "reflection.ML"
chaieb@20374
    18
haftmann@29650
    19
method_setup reify = {* fn src =>
haftmann@29650
    20
  Method.syntax (Attrib.thms --
haftmann@29650
    21
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
chaieb@23649
    22
  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
wenzelm@20319
    23
*} "partial automatic reification"
wenzelm@20319
    24
chaieb@23649
    25
method_setup reflection = {* 
chaieb@23649
    26
let 
haftmann@29650
    27
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
haftmann@29650
    28
  val onlyN = "only";
haftmann@29650
    29
  val rulesN = "rules";
haftmann@29650
    30
  val any_keyword = keyword onlyN || keyword rulesN;
haftmann@29650
    31
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
haftmann@29650
    32
  val terms = thms >> map (term_of o Drule.dest_term);
haftmann@29650
    33
  fun optional scan = Scan.optional scan [];
haftmann@29650
    34
in fn src =>
haftmann@29650
    35
  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
haftmann@29650
    36
    (fn (((eqs,ths),to), ctxt) => 
chaieb@23649
    37
      let 
chaieb@23649
    38
        val (ceqs,cths) = Reify_Data.get ctxt 
chaieb@23649
    39
        val corr_thms = ths@cths
chaieb@23649
    40
        val raw_eqs = eqs@ceqs
chaieb@23649
    41
      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
chaieb@23649
    42
     end) end
wenzelm@20319
    43
*} "reflection method"
haftmann@29650
    44
wenzelm@20319
    45
end