isabelle: src/HOL/Prolog/HOHH.thy@043921b0e587 (annotated)

13208 965f95a3abd9 added the usual file headers oheimb parents: 9015 diff changeset	1	(* Title: HOL/Prolog/HOHH.thy
965f95a3abd9 added the usual file headers oheimb parents: 9015 diff changeset	2	ID: $Id$
965f95a3abd9 added the usual file headers oheimb parents: 9015 diff changeset	3	Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
965f95a3abd9 added the usual file headers oheimb parents: 9015 diff changeset	4	*)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	5
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* Higher-order hereditary Harrop formulas *}
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory HOHH
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports HOL
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	11
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	12	consts
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	13
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	(* D-formulas (programs): D ::= !x. D \| D .. D \| D :- G \| A *)
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	"Dand" :: "[bool, bool] => bool" (infixr ".." 28)
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	16	":-" :: "[bool, bool] => bool" (infixl 29)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	17
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	18	(* G-formulas (goals): G ::= A \| G & G \| G \| G \| ? x. G
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	19	\| True \| !x. G \| D => G *)
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	20	("," :: "[bool, bool] => bool" (infixr 35))
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	21	"=>" :: "[bool, bool] => bool" (infixr 27)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	22
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	23	translations
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	24
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	25	"D :- G" => "G --> D"
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	26	"D1 .. D2" => "D1 & D2"
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	("G1 , G2" => "G1 & G2")
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	28	"D => G" => "D --> G"
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	29
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	30	end

author	wenzelm
	Tue, 16 May 2006 13:01:30 +0200
changeset 19647	043921b0e587
parent 17311	5b1d47d920ce
child 21425	c11ab38b78a7
permissions	-rw-r--r--