removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
(* Title: HOL/Prolog/Test.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
header {* Basic examples *}
theory Test
imports HOHH
begin
typedecl nat
typedecl 'a list
consts
Nil :: "'a list" ("[]")
Cons :: "'a => 'a list => 'a list" (infixr "#" 65)
syntax
(* list Enumeration *)
"@list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
typedecl person
consts
append :: "['a list, 'a list, 'a list] => bool"
reverse :: "['a list, 'a list] => bool"
mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
mapfun :: "[('a => 'b), 'a list, 'b list] => bool"
bob :: person
sue :: person
ned :: person
"23" :: nat ("23")
"24" :: nat ("24")
"25" :: nat ("25")
age :: "[person, nat] => bool"
eq :: "['a, 'a] => bool"
empty :: "['b] => bool"
add :: "['a, 'b, 'b] => bool"
remove :: "['a, 'b, 'b] => bool"
bag_appl:: "['a, 'a, 'a, 'a] => bool"
axioms
append: "append [] xs xs ..
append (x#xs) ys (x#zs) :- append xs ys zs"
reverse: "reverse L1 L2 :- (!rev_aux.
(!L. rev_aux [] L L )..
(!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
=> rev_aux L1 L2 [])"
mappred: "mappred P [] [] ..
mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys"
mapfun: "mapfun f [] [] ..
mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
age: "age bob 24 ..
age sue 23 ..
age ned 23"
eq: "eq x x"
(* actual definitions of empty and add is hidden -> yields abstract data type *)
bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
empty S1 &
add A S1 S2 &
add B S2 S3 &
remove X S3 S4 &
remove Y S4 S5 &
empty S5)"
ML {* use_legacy_bindings (the_context ()) *}
end