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