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