--- a/src/HOL/Prolog/Test.thy Wed Sep 07 21:00:30 2005 +0200
+++ b/src/HOL/Prolog/Test.thy Wed Sep 07 21:07:09 2005 +0200
@@ -1,81 +1,85 @@
(* Title: HOL/Prolog/Test.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-
-basic examples
*)
-Test = HOHH +
+header {* Basic examples *}
-types nat
-arities nat :: type
+theory Test
+imports HOHH
+begin
-types 'a list
-arities list :: (type) type
+typedecl nat
+
+typedecl 'a list
-consts Nil :: 'a list ("[]")
- Cons :: 'a => 'a list => 'a list (infixr "#" 65)
+consts
+ Nil :: "'a list" ("[]")
+ Cons :: "'a => 'a list => 'a list" (infixr "#" 65)
syntax
(* list Enumeration *)
- "@list" :: args => 'a list ("[(_)]")
+ "@list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
-types person
-arities person :: type
+typedecl person
-consts
- append :: ['a list, 'a list, 'a list] => bool
- reverse :: ['a list, 'a list] => bool
+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
+ mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
+ mapfun :: "[('a => 'b), 'a list, 'b list] => bool"
- bob :: person
- sue :: person
- ned :: person
+ bob :: person
+ sue :: person
+ ned :: person
- "23" :: nat ("23")
- "24" :: nat ("24")
- "25" :: nat ("25")
+ "23" :: nat ("23")
+ "24" :: nat ("24")
+ "25" :: nat ("25")
- age :: [person, nat] => bool
+ age :: "[person, nat] => bool"
- eq :: ['a, 'a] => 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
+ empty :: "['b] => bool"
+ add :: "['a, 'b, 'b] => bool"
+ remove :: "['a, 'b, 'b] => bool"
+ bag_appl:: "['a, 'a, 'a, 'a] => bool"
-rules 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 [])"
+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"
+ 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"
+ age: "age bob 24 ..
+ age sue 23 ..
+ age ned 23"
- eq "eq x x"
+ 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)"
+ 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