author  haftmann 
Wed, 28 Jan 2009 11:04:10 +0100  
changeset 29650  cc3958d31b1d 
parent 23649  src/HOL/ex/Reflection.thy@4d865f3e4405 
child 30510  4120fc59dd85 
permissions  rwrr 
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 