src/HOL/Prolog/HOHH.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 17311 5b1d47d920ce
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
oheimb@13208
     1
(*  Title:    HOL/Prolog/HOHH.thy
oheimb@13208
     2
    ID:       $Id$
oheimb@13208
     3
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
oheimb@13208
     4
oheimb@13208
     5
higher-order hereditary Harrop formulas 
oheimb@13208
     6
*)
oheimb@9015
     7
oheimb@9015
     8
HOHH = HOL +
oheimb@9015
     9
oheimb@9015
    10
consts
oheimb@9015
    11
oheimb@9015
    12
(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
oheimb@9015
    13
  "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
oheimb@9015
    14
  ":-"		:: [bool, bool] => bool		(infixl 29)
oheimb@9015
    15
oheimb@9015
    16
(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
oheimb@9015
    17
			       | True | !x. G | D => G			*)
oheimb@9015
    18
(*","           :: [bool, bool] => bool		(infixr 35)*)
oheimb@9015
    19
  "=>"		:: [bool, bool] => bool		(infixr 27)
oheimb@9015
    20
oheimb@9015
    21
translations
oheimb@9015
    22
oheimb@9015
    23
  "D :- G"	=>	"G --> D"
oheimb@9015
    24
  "D1 .. D2"	=>	"D1 & D2"
oheimb@9015
    25
(*"G1 , G2"	=>	"G1 & G2"*)
oheimb@9015
    26
  "D => G"	=>	"D --> G"
oheimb@9015
    27
oheimb@9015
    28
end
oheimb@9015
    29