isabelle: src/HOL/Prolog/HOHH.thy@f1648e009dc1 (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
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	10	uses "prolog.ML"
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	11	begin
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	12
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	13	method_setup ptac =
27229 f656a12e0f4e ptac/prolog_tac: proper context; wenzelm parents: 21588 diff changeset	14	{* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	15	"Basic Lambda Prolog interpreter"
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	16
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	17	method_setup prolog =
27229 f656a12e0f4e ptac/prolog_tac: proper context; wenzelm parents: 21588 diff changeset	18	{* Method.thms_ctxt_args (fn thms => fn ctxt => Method.SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	19	"Lambda Prolog interpreter"
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	20
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	21	consts
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	22
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	23	(* D-formulas (programs): D ::= !x. D \| D .. D \| D :- G \| A *)
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	24	Dand :: "[bool, bool] => bool" (infixr ".." 28)
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	25	Dif :: "[bool, bool] => bool" (infixl ":-" 29)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	26
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	27	(* G-formulas (goals): G ::= A \| G & G \| G \| G \| ? x. G
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	28	\| True \| !x. G \| D => G *)
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	29	(Dand' :: "[bool, bool] => bool" (infixr "," 35))
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	30	Dimp :: "[bool, bool] => bool" (infixr "=>" 27)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	31
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	32	translations
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	33
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	34	"D :- G" => "G --> D"
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	35	"D1 .. D2" => "D1 & D2"
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	36	("G1 , G2" => "G1 & G2")
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	37	"D => G" => "D --> G"
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	38
8006e9009621 added HOL/Prolog oheimb parents: diff changeset	39	end

author	krauss
	Sat, 27 Dec 2008 17:49:15 +0100
changeset 29183	f1648e009dc1
parent 27229	f656a12e0f4e
child 30510	4120fc59dd85
permissions	-rw-r--r--