src/HOL/ex/Antiquote.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Antiquote.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Antiquotations *}
     7 
     8 theory Antiquote imports Main begin
     9 
    10 text {*
    11   A simple example on quote / antiquote in higher-order abstract
    12   syntax.
    13 *}
    14 
    15 syntax
    16   "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
    17 
    18 constdefs
    19   var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
    20   "var x env == env x"
    21 
    22   Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
    23   "Expr exp env == exp env"
    24 
    25 parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
    26 print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
    27 
    28 term "EXPR (a + b + c)"
    29 term "EXPR (a + b + c + VAR x + VAR y + 1)"
    30 term "EXPR (VAR (f w) + VAR x)"
    31 
    32 term "Expr (\<lambda>env. env x)"				(*improper*)
    33 term "Expr (\<lambda>env. f env)"
    34 term "Expr (\<lambda>env. f env + env x)"			(*improper*)
    35 term "Expr (\<lambda>env. f env y z)"
    36 term "Expr (\<lambda>env. f env + g y env)"
    37 term "Expr (\<lambda>env. f env + g env y + h a env z)"
    38 
    39 end