isabelle: src/HOL/Prolog/HOHH.thy@9f9b088d8824 (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	Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
965f95a3abd9 added the usual file headers oheimb parents: 9015 diff changeset	3	*)
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	4
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 48891 diff changeset	5	section {* Higher-order hereditary Harrop formulas *}
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory HOHH
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports HOL
5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 42814 diff changeset	11	ML_file "prolog.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 42814 diff changeset	12
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 17311 diff changeset	13	method_setup ptac =
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	14	{* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
42814 5af15f1e2ef6 simplified/unified method_setup/attribute_setup; wenzelm parents: 34974 diff changeset	15	"basic Lambda Prolog interpreter"
21425 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 =
30549 d2d7874648bd simplified method setup; wenzelm parents: 30510 diff changeset	18	{* Attrib.thms >> (fn thms => fn ctxt => 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	blanchet
	Thu, 01 Oct 2015 17:35:28 +0200
changeset 61302	9f9b088d8824
parent 58889	5b7a9633cfa8
child 63167	0909deb8059b
permissions	-rw-r--r--