(* 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