author | haftmann |
Tue, 20 Mar 2007 08:27:15 +0100 | |
changeset 22473 | 753123c89d72 |
parent 22199 | b617ddd200eb |
child 23546 | c8a1bd9585a0 |
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 |
|
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21879
diff
changeset
|
10 |
uses ("reflection.ML") |
20319 | 11 |
begin |
12 |
||
20374 | 13 |
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
14 |
by (blast intro: ext) |
|
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21879
diff
changeset
|
15 |
|
20374 | 16 |
use "reflection.ML" |
17 |
||
20319 | 18 |
method_setup reify = {* |
19 |
fn src => |
|
20 |
Method.syntax (Attrib.thms -- |
|
21 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
21879 | 22 |
(fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to)) |
20319 | 23 |
*} "partial automatic reification" |
24 |
||
25 |
method_setup reflection = {* |
|
26 |
fn src => |
|
27 |
Method.syntax (Attrib.thms -- |
|
28 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
21879 | 29 |
(fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to)) |
20319 | 30 |
*} "reflection method" |
31 |
||
32 |
end |