author | huffman |
Sat, 14 Feb 2009 11:11:30 -0800 | |
changeset 29911 | c790a70a3d19 |
parent 29650 | cc3958d31b1d |
child 30510 | 4120fc59dd85 |
permissions | -rw-r--r-- |
29650 | 1 |
(* Title: HOL/Library/Reflection.thy |
20319 | 2 |
Author: Amine Chaieb, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Generic reflection and reification *} |
|
6 |
||
7 |
theory Reflection |
|
8 |
imports Main |
|
29650 | 9 |
uses "reify_data.ML" ("reflection.ML") |
20319 | 10 |
begin |
11 |
||
29650 | 12 |
setup {* Reify_Data.setup *} |
23546
c8a1bd9585a0
reflection and reification methods now manage Context data
chaieb
parents:
22199
diff
changeset
|
13 |
|
20374 | 14 |
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
15 |
by (blast intro: ext) |
|
22199
b617ddd200eb
Now deals with simples cases where the input equations contain type variables
chaieb
parents:
21879
diff
changeset
|
16 |
|
20374 | 17 |
use "reflection.ML" |
18 |
||
29650 | 19 |
method_setup reify = {* fn src => |
20 |
Method.syntax (Attrib.thms -- |
|
21 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #> |
|
23649
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
22 |
(fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to)) |
20319 | 23 |
*} "partial automatic reification" |
24 |
||
23649
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
25 |
method_setup reflection = {* |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
26 |
let |
29650 | 27 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
28 |
val onlyN = "only"; |
|
29 |
val rulesN = "rules"; |
|
30 |
val any_keyword = keyword onlyN || keyword rulesN; |
|
31 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
32 |
val terms = thms >> map (term_of o Drule.dest_term); |
|
33 |
fun optional scan = Scan.optional scan []; |
|
34 |
in fn src => |
|
35 |
Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> |
|
36 |
(fn (((eqs,ths),to), ctxt) => |
|
23649
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
37 |
let |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
38 |
val (ceqs,cths) = Reify_Data.get ctxt |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
39 |
val corr_thms = ths@cths |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
40 |
val raw_eqs = eqs@ceqs |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
41 |
in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) |
4d865f3e4405
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
chaieb
parents:
23607
diff
changeset
|
42 |
end) end |
20319 | 43 |
*} "reflection method" |
29650 | 44 |
|
20319 | 45 |
end |