src/HOL/Prolog/Test.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 17311 5b1d47d920ce
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:    HOL/Prolog/Test.thy
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 
     5 basic examples 
     6 *)
     7 
     8 Test = HOHH +
     9 
    10 types nat
    11 arities nat :: type
    12 
    13 types 'a list
    14 arities list :: (type) type
    15 
    16 consts Nil   :: 'a list		 	 		 ("[]")
    17        Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
    18 
    19 syntax
    20   (* list Enumeration *)
    21   "@list"     :: args => 'a list                          ("[(_)]")
    22 
    23 translations
    24   "[x, xs]"     == "x#[xs]"
    25   "[x]"         == "x#[]"
    26 
    27 types   person
    28 arities person  :: type
    29 
    30 consts  
    31 	append  :: ['a list, 'a list, 'a list]		  => bool
    32 	reverse :: ['a list, 'a list]			  => bool
    33 
    34 	mappred	:: [('a => 'b => bool), 'a list, 'b list] => bool
    35 	mapfun	:: [('a => 'b), 'a list, 'b list]	  => bool
    36 
    37 	bob	:: person
    38 	sue	:: person
    39 	ned	:: person
    40 
    41 	"23"	:: nat		("23")
    42 	"24"	:: nat		("24")
    43 	"25"	:: nat		("25")
    44 
    45 	age	:: [person, nat]			  => bool
    46 
    47 	eq	:: ['a, 'a]				  => bool
    48 
    49 	empty	:: ['b]					  => bool
    50 	add	:: ['a, 'b, 'b]				  => bool
    51 	remove	:: ['a, 'b, 'b]				  => bool
    52 	bag_appl:: ['a, 'a, 'a, 'a]			  => bool
    53 
    54 rules   append	"append  []    xs  xs    ..
    55 		 append (x#xs) ys (x#zs) :- append xs ys zs"
    56 	reverse "reverse L1 L2 :- (!rev_aux. 
    57 		  (!L.          rev_aux  []    L  L )..
    58 		  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    59 		  => rev_aux L1 L2 [])"
    60 
    61 	mappred "mappred P  []     []    ..
    62 		 mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
    63 	mapfun  "mapfun f  []     []      ..
    64 		 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
    65 
    66 	age     "age bob 24 ..
    67 		 age sue 23 ..
    68 		 age ned 23"
    69 
    70 	eq	"eq x x"
    71 
    72 (* actual definitions of empty and add is hidden -> yields abstract data type *)
    73 
    74 	bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
    75 				empty    S1    &
    76 				add A    S1 S2 &
    77 				add B    S2 S3 &
    78 				remove X S3 S4 &
    79 				remove Y S4 S5 &
    80 				empty    S5)"
    81 end