src/HOL/ex/Antiquote.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
wenzelm@5368
     1
(*  Title:      HOL/ex/Antiquote.thy
wenzelm@5368
     2
    ID:         $Id$
wenzelm@5368
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5368
     4
*)
wenzelm@5368
     5
wenzelm@10357
     6
header {* Antiquotations *}
wenzelm@10357
     7
haftmann@16417
     8
theory Antiquote imports Main begin
wenzelm@5368
     9
wenzelm@11586
    10
text {*
wenzelm@11586
    11
  A simple example on quote / antiquote in higher-order abstract
wenzelm@11586
    12
  syntax.
wenzelm@11586
    13
*}
wenzelm@11586
    14
wenzelm@5368
    15
syntax
wenzelm@9297
    16
  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
wenzelm@5368
    17
wenzelm@5368
    18
constdefs
wenzelm@5368
    19
  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
wenzelm@5368
    20
  "var x env == env x"
wenzelm@5368
    21
wenzelm@8559
    22
  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
wenzelm@9297
    23
  "Expr exp env == exp env"
wenzelm@5368
    24
wenzelm@9297
    25
parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
wenzelm@9297
    26
print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
wenzelm@8559
    27
wenzelm@9297
    28
term "EXPR (a + b + c)"
wenzelm@9297
    29
term "EXPR (a + b + c + VAR x + VAR y + 1)"
wenzelm@9297
    30
term "EXPR (VAR (f w) + VAR x)"
wenzelm@5368
    31
wenzelm@10357
    32
term "Expr (\<lambda>env. env x)"				(*improper*)
wenzelm@10357
    33
term "Expr (\<lambda>env. f env)"
wenzelm@10357
    34
term "Expr (\<lambda>env. f env + env x)"			(*improper*)
wenzelm@10357
    35
term "Expr (\<lambda>env. f env y z)"
wenzelm@10357
    36
term "Expr (\<lambda>env. f env + g y env)"
wenzelm@10357
    37
term "Expr (\<lambda>env. f env + g env y + h a env z)"
wenzelm@5368
    38
wenzelm@9297
    39
end