src/HOL/Prolog/Test.thy
changeset 9015 8006e9009621
child 12338 de0f4a63baa5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Prolog/Test.thy	Fri Jun 02 12:44:04 2000 +0200
     1.3 @@ -0,0 +1,76 @@
     1.4 +(* basic examples *)
     1.5 +
     1.6 +Test = HOHH +
     1.7 +
     1.8 +types nat
     1.9 +arities nat :: term
    1.10 +
    1.11 +types 'a list
    1.12 +arities list :: (term) term
    1.13 +
    1.14 +consts Nil   :: 'a list		 	 		 ("[]")
    1.15 +       Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
    1.16 +
    1.17 +syntax
    1.18 +  (* list Enumeration *)
    1.19 +  "@list"     :: args => 'a list                          ("[(_)]")
    1.20 +
    1.21 +translations
    1.22 +  "[x, xs]"     == "x#[xs]"
    1.23 +  "[x]"         == "x#[]"
    1.24 +
    1.25 +types   person
    1.26 +arities person  :: term
    1.27 +
    1.28 +consts  
    1.29 +	append  :: ['a list, 'a list, 'a list]		  => bool
    1.30 +	reverse :: ['a list, 'a list]			  => bool
    1.31 +
    1.32 +	mappred	:: [('a => 'b => bool), 'a list, 'b list] => bool
    1.33 +	mapfun	:: [('a => 'b), 'a list, 'b list]	  => bool
    1.34 +
    1.35 +	bob	:: person
    1.36 +	sue	:: person
    1.37 +	ned	:: person
    1.38 +
    1.39 +	"23"	:: nat		("23")
    1.40 +	"24"	:: nat		("24")
    1.41 +	"25"	:: nat		("25")
    1.42 +
    1.43 +	age	:: [person, nat]			  => bool
    1.44 +
    1.45 +	eq	:: ['a, 'a]				  => bool
    1.46 +
    1.47 +	empty	:: ['b]					  => bool
    1.48 +	add	:: ['a, 'b, 'b]				  => bool
    1.49 +	remove	:: ['a, 'b, 'b]				  => bool
    1.50 +	bag_appl:: ['a, 'a, 'a, 'a]			  => bool
    1.51 +
    1.52 +rules   append	"append  []    xs  xs    ..
    1.53 +		 append (x#xs) ys (x#zs) :- append xs ys zs"
    1.54 +	reverse "reverse L1 L2 :- (!rev_aux. 
    1.55 +		  (!L.          rev_aux  []    L  L )..
    1.56 +		  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    1.57 +		  => rev_aux L1 L2 [])"
    1.58 +
    1.59 +	mappred "mappred P  []     []    ..
    1.60 +		 mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
    1.61 +	mapfun  "mapfun f  []     []      ..
    1.62 +		 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
    1.63 +
    1.64 +	age     "age bob 24 ..
    1.65 +		 age sue 23 ..
    1.66 +		 age ned 23"
    1.67 +
    1.68 +	eq	"eq x x"
    1.69 +
    1.70 +(* actual definitions of empty and add is hidden -> yields abstract data type *)
    1.71 +
    1.72 +	bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
    1.73 +				empty    S1    &
    1.74 +				add A    S1 S2 &
    1.75 +				add B    S2 S3 &
    1.76 +				remove X S3 S4 &
    1.77 +				remove Y S4 S5 &
    1.78 +				empty    S5)"
    1.79 +end