author | chaieb |
Fri, 06 Jul 2007 16:09:27 +0200 | |
changeset 23607 | 6a8fb529b542 |
parent 23546 | c8a1bd9585a0 |
child 23649 | 4d865f3e4405 |
permissions | -rw-r--r-- |
20319 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Amine Chaieb, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* Generic reflection and reification *} |
|
7 |
||
8 |
theory Reflection |
|
9 |
imports Main |
|
23546
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
10 |
uses "reflection_data.ML" ("reflection.ML") |
20319 | 11 |
begin |
12 |
||
23546
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
13 |
setup {* Reify_Data.setup*} |
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
14 |
|
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
15 |
|
20374 | 16 |
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
17 |
by (blast intro: ext) |
|
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21879
diff
changeset
|
18 |
|
20374 | 19 |
use "reflection.ML" |
20 |
||
20319 | 21 |
method_setup reify = {* |
22 |
fn src => |
|
23 |
Method.syntax (Attrib.thms -- |
|
24 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
23546
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
25 |
(fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to)) |
20319 | 26 |
*} "partial automatic reification" |
27 |
||
28 |
method_setup reflection = {* |
|
29 |
fn src => |
|
30 |
Method.syntax (Attrib.thms -- |
|
31 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
23546
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
32 |
(fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to)) |
20319 | 33 |
*} "reflection method" |
34 |
||
35 |
end |