src/HOL/Library/Reflection.thy
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 -rw-r--r--
Reflection.thy now in HOL/Library
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
     1
(*  Title:      HOL/Library/Reflection.thy
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     3
*)
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     4
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     5
header {* Generic reflection and reification *}
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     6
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     7
theory Reflection
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     8
imports Main
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
     9
uses "reify_data.ML" ("reflection.ML")
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    10
begin
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    11
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    12
setup {* Reify_Data.setup *}
23546
c8a1bd9585a0 reflection and reification methods now manage Context data
chaieb
parents: 22199
diff changeset
    13
20374
01b711328990 Reification now handels binders.
chaieb
parents: 20319
diff changeset
    14
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
01b711328990 Reification now handels binders.
chaieb
parents: 20319
diff changeset
    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
01b711328990 Reification now handels binders.
chaieb
parents: 20319
diff changeset
    17
use "reflection.ML"
01b711328990 Reification now handels binders.
chaieb
parents: 20319
diff changeset
    18
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    19
method_setup reify = {* fn src =>
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    20
  Method.syntax (Attrib.thms --
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    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
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    23
*} "partial automatic reification"
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    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
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    27
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    28
  val onlyN = "only";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    29
  val rulesN = "rules";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    30
  val any_keyword = keyword onlyN || keyword rulesN;
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    31
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    32
  val terms = thms >> map (term_of o Drule.dest_term);
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    33
  fun optional scan = Scan.optional scan [];
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    34
in fn src =>
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    35
  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    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
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    43
*} "reflection method"
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    44
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    45
end