src/HOL/Prolog/HOHH.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66453 cc19f7ca2ed6
child 69605 a96320074298
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:    HOL/Prolog/HOHH.thy
     2     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     3 *)
     4 
     5 section \<open>Higher-order hereditary Harrop formulas\<close>
     6 
     7 theory HOHH
     8 imports HOL.HOL
     9 begin
    10 
    11 ML_file "prolog.ML"
    12 
    13 method_setup ptac =
    14   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
    15   "basic Lambda Prolog interpreter"
    16 
    17 method_setup prolog =
    18   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms))\<close>
    19   "Lambda Prolog interpreter"
    20 
    21 consts
    22 
    23 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
    24   Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
    25   Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
    26 
    27 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
    28                                | True | !x. G | D => G                  *)
    29 (*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
    30   Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
    31 
    32 translations
    33 
    34   "D :- G"      =>      "G --> D"
    35   "D1 .. D2"    =>      "D1 & D2"
    36 (*"G1 , G2"     =>      "G1 & G2"*)
    37   "D => G"      =>      "D --> G"
    38 
    39 end