src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@59189
     1
section \<open>Concrete Syntax\<close>
prensani@13020
     2
haftmann@16417
     3
theory Quote_Antiquote imports Main begin
prensani@13020
     4
prensani@13020
     5
syntax
prensani@13020
     6
  "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
prensani@13020
     7
  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
wenzelm@53241
     8
  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(\<lbrace>_\<rbrace>)" [0] 1000)
prensani@13020
     9
prensani@13020
    10
translations
wenzelm@53241
    11
  "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
prensani@13020
    12
wenzelm@59189
    13
parse_translation \<open>
prensani@13020
    14
  let
wenzelm@42284
    15
    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
prensani@13020
    16
      | quote_tr ts = raise TERM ("quote_tr", ts);
wenzelm@52143
    17
  in [(@{syntax_const "_quote"}, K quote_tr)] end
wenzelm@59189
    18
\<close>
prensani@13020
    19
nipkow@62390
    20
end