isabelle: src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy@3d5e2b7d1374 (annotated)

38074 31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	1	theory Code_Prolog_Examples
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	2	imports Predicate_Compile_Alternative_Defs
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	3	uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	4	begin
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	5
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	6	section {* Example append *}
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	7
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	8	inductive append
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	9	where
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	10	"append [] ys ys"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	11	\| "append xs ys zs ==> append (x # xs) ys (x # zs)"
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	12
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	13	code_pred append .
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	14
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	15	ML {*
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	16	tracing (Code_Prolog.write_program (Code_Prolog.generate @{context} [@{const_name append}]))
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	17	*}
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	18
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	19	ML {*
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	20	Code_Prolog.run (Code_Prolog.generate @{context} [@{const_name append}]) "append" ["X", "Y", "Z"]
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	21	*}
31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	22
38075 3d5e2b7d1374 adding values command and parsing prolog output bulwahn parents: 38074 diff changeset	23	values "{(x, y, z). append x y z}"
3d5e2b7d1374 adding values command and parsing prolog output bulwahn parents: 38074 diff changeset	24
38074 31174744b9a2 adding example file for prolog code generation; adding prolog code generation example to IsaMakefile bulwahn parents: diff changeset	25	end

author	bulwahn
	Thu, 29 Jul 2010 17:27:55 +0200
changeset 38075	3d5e2b7d1374
parent 38074	31174744b9a2
child 38080	8c20eb9a388d
permissions	-rw-r--r--