src/HOL/ex/Antiquote.thy
author kleing
Sat, 01 Mar 2003 16:45:51 +0100
changeset 13840 399c8103a98f
parent 11586 d8a7f6318457
child 14981 e73f8140af78
permissions -rw-r--r--
keep a copy of generated files in repository
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/ex/Antiquote.thy
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9297
wenzelm
parents: 8559
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
     5
*)
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
     6
10357
wenzelm
parents: 9297
diff changeset
     7
header {* Antiquotations *}
wenzelm
parents: 9297
diff changeset
     8
9297
wenzelm
parents: 8559
diff changeset
     9
theory Antiquote = Main:
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    10
11586
wenzelm
parents: 10357
diff changeset
    11
text {*
wenzelm
parents: 10357
diff changeset
    12
  A simple example on quote / antiquote in higher-order abstract
wenzelm
parents: 10357
diff changeset
    13
  syntax.
wenzelm
parents: 10357
diff changeset
    14
*}
wenzelm
parents: 10357
diff changeset
    15
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    16
syntax
9297
wenzelm
parents: 8559
diff changeset
    17
  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    18
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    19
constdefs
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    20
  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    21
  "var x env == env x"
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    22
8559
fd3753188232 ex/Antiquote.thy made new-style theory;
wenzelm
parents: 5368
diff changeset
    23
  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
9297
wenzelm
parents: 8559
diff changeset
    24
  "Expr exp env == exp env"
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    25
9297
wenzelm
parents: 8559
diff changeset
    26
parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *}
wenzelm
parents: 8559
diff changeset
    27
print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *}
8559
fd3753188232 ex/Antiquote.thy made new-style theory;
wenzelm
parents: 5368
diff changeset
    28
9297
wenzelm
parents: 8559
diff changeset
    29
term "EXPR (a + b + c)"
wenzelm
parents: 8559
diff changeset
    30
term "EXPR (a + b + c + VAR x + VAR y + 1)"
wenzelm
parents: 8559
diff changeset
    31
term "EXPR (VAR (f w) + VAR x)"
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    32
10357
wenzelm
parents: 9297
diff changeset
    33
term "Expr (\<lambda>env. env x)"				(*improper*)
wenzelm
parents: 9297
diff changeset
    34
term "Expr (\<lambda>env. f env)"
wenzelm
parents: 9297
diff changeset
    35
term "Expr (\<lambda>env. f env + env x)"			(*improper*)
wenzelm
parents: 9297
diff changeset
    36
term "Expr (\<lambda>env. f env y z)"
wenzelm
parents: 9297
diff changeset
    37
term "Expr (\<lambda>env. f env + g y env)"
wenzelm
parents: 9297
diff changeset
    38
term "Expr (\<lambda>env. f env + g env y + h a env z)"
5368
7c8d1c7c876d added Antiquote example;
wenzelm
parents:
diff changeset
    39
9297
wenzelm
parents: 8559
diff changeset
    40
end