Theory HOHH

Up to index of Isabelle/HOL/Prolog

theory HOHH
imports HOL
uses [HOHH.ML]
begin

(*  Title:    HOL/Prolog/HOHH.thy
    ID:       $Id: HOHH.thy,v 1.4 2005/09/07 19:07:09 wenzelm Exp $
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)

header {* Higher-order hereditary Harrop formulas *}

theory HOHH
imports HOL
begin

consts

(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
  ":-"          :: "[bool, bool] => bool"         (infixl 29)

(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
                               | True | !x. G | D => G                  *)
(*","           :: "[bool, bool] => bool"         (infixr 35)*)
  "=>"          :: "[bool, bool] => bool"         (infixr 27)

translations

  "D :- G"      =>      "G --> D"
  "D1 .. D2"    =>      "D1 & D2"
(*"G1 , G2"     =>      "G1 & G2"*)
  "D => G"      =>      "D --> G"

end