src/HOL/Library/Reflection.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 31412 f2e6b6526092
child 42814 5af15f1e2ef6
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
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
wenzelm@30549
    19
method_setup reify = {*
wenzelm@30549
    20
  Attrib.thms --
wenzelm@30549
    21
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
wenzelm@30549
    22
  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
wenzelm@20319
    23
*} "partial automatic reification"
wenzelm@20319
    24
hoelzl@31412
    25
method_setup reflection = {*
hoelzl@31412
    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);
wenzelm@30549
    33
in
wenzelm@30549
    34
  thms --
wenzelm@30549
    35
  Scan.optional (keyword rulesN |-- thms) [] --
wenzelm@30549
    36
  Scan.option (keyword onlyN |-- Args.term) >>
wenzelm@30549
    37
  (fn ((eqs,ths),to) => fn ctxt =>
hoelzl@31412
    38
    let
hoelzl@31412
    39
      val (ceqs,cths) = Reify_Data.get ctxt
wenzelm@30549
    40
      val corr_thms = ths@cths
wenzelm@30549
    41
      val raw_eqs = eqs@ceqs
wenzelm@30549
    42
    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
wenzelm@30549
    43
end
wenzelm@30549
    44
*} "reflection"
haftmann@29650
    45
wenzelm@20319
    46
end