isabelle: src/HOL/Prolog/HOHH.thy@6f2bcdfa9a19 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Higher-order hereditary Harrop formulas\<close>
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
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	8	imports HOL.HOL
17311 5b1d47d920ce converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
9015 8006e9009621 added HOL/Prolog oheimb parents: diff changeset	10
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 66453 diff changeset	11	ML_file \<open>prolog.ML\<close>
48891 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 =
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	14	\<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
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 =
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	18	\<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms))\<close>
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
81216 2fccbfca1361 clarified concrete vs. abstract syntax; wenzelm parents: 80914 diff changeset	21	syntax
9015 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 *)
81216 2fccbfca1361 clarified concrete vs. abstract syntax; wenzelm parents: 80914 diff changeset	24	"_Dand" :: "[bool, bool] => bool" (infixr \<open>..\<close> 28)
2fccbfca1361 clarified concrete vs. abstract syntax; wenzelm parents: 80914 diff changeset	25	"_Dif" :: "[bool, bool] => bool" (infixl \<open>:-\<close> 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 *)
81216 2fccbfca1361 clarified concrete vs. abstract syntax; wenzelm parents: 80914 diff changeset	29	("_Dand'" :: "[bool, bool] => bool" (infixr "," 35))
2fccbfca1361 clarified concrete vs. abstract syntax; wenzelm parents: 80914 diff changeset	30	"_Dimp" :: "[bool, bool] => bool" (infixr \<open>=>\<close> 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	wenzelm
	Wed, 22 Jan 2025 22:22:19 +0100
changeset 81954	6f2bcdfa9a19
parent 81216	2fccbfca1361
permissions	-rw-r--r--