src/HOL/Prolog/Test.thy
changeset 17311 5b1d47d920ce
parent 14981 e73f8140af78
child 21425 c11ab38b78a7
     1.1 --- a/src/HOL/Prolog/Test.thy	Wed Sep 07 21:00:30 2005 +0200
     1.2 +++ b/src/HOL/Prolog/Test.thy	Wed Sep 07 21:07:09 2005 +0200
     1.3 @@ -1,81 +1,85 @@
     1.4  (*  Title:    HOL/Prolog/Test.thy
     1.5      ID:       $Id$
     1.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 -
     1.8 -basic examples 
     1.9  *)
    1.10  
    1.11 -Test = HOHH +
    1.12 +header {* Basic examples *}
    1.13  
    1.14 -types nat
    1.15 -arities nat :: type
    1.16 +theory Test
    1.17 +imports HOHH
    1.18 +begin
    1.19  
    1.20 -types 'a list
    1.21 -arities list :: (type) type
    1.22 +typedecl nat
    1.23 +
    1.24 +typedecl 'a list
    1.25  
    1.26 -consts Nil   :: 'a list		 	 		 ("[]")
    1.27 -       Cons  :: 'a => 'a list => 'a list		 (infixr "#"  65)
    1.28 +consts
    1.29 +  Nil   :: "'a list"                                  ("[]")
    1.30 +  Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
    1.31  
    1.32  syntax
    1.33    (* list Enumeration *)
    1.34 -  "@list"     :: args => 'a list                          ("[(_)]")
    1.35 +  "@list"     :: "args => 'a list"                          ("[(_)]")
    1.36  
    1.37  translations
    1.38    "[x, xs]"     == "x#[xs]"
    1.39    "[x]"         == "x#[]"
    1.40  
    1.41 -types   person
    1.42 -arities person  :: type
    1.43 +typedecl person
    1.44  
    1.45 -consts  
    1.46 -	append  :: ['a list, 'a list, 'a list]		  => bool
    1.47 -	reverse :: ['a list, 'a list]			  => bool
    1.48 +consts
    1.49 +  append  :: "['a list, 'a list, 'a list]            => bool"
    1.50 +  reverse :: "['a list, 'a list]                     => bool"
    1.51  
    1.52 -	mappred	:: [('a => 'b => bool), 'a list, 'b list] => bool
    1.53 -	mapfun	:: [('a => 'b), 'a list, 'b list]	  => bool
    1.54 +  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
    1.55 +  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool"
    1.56  
    1.57 -	bob	:: person
    1.58 -	sue	:: person
    1.59 -	ned	:: person
    1.60 +  bob     :: person
    1.61 +  sue     :: person
    1.62 +  ned     :: person
    1.63  
    1.64 -	"23"	:: nat		("23")
    1.65 -	"24"	:: nat		("24")
    1.66 -	"25"	:: nat		("25")
    1.67 +  "23"    :: nat          ("23")
    1.68 +  "24"    :: nat          ("24")
    1.69 +  "25"    :: nat          ("25")
    1.70  
    1.71 -	age	:: [person, nat]			  => bool
    1.72 +  age     :: "[person, nat]                          => bool"
    1.73  
    1.74 -	eq	:: ['a, 'a]				  => bool
    1.75 +  eq      :: "['a, 'a]                               => bool"
    1.76  
    1.77 -	empty	:: ['b]					  => bool
    1.78 -	add	:: ['a, 'b, 'b]				  => bool
    1.79 -	remove	:: ['a, 'b, 'b]				  => bool
    1.80 -	bag_appl:: ['a, 'a, 'a, 'a]			  => bool
    1.81 +  empty   :: "['b]                                   => bool"
    1.82 +  add     :: "['a, 'b, 'b]                           => bool"
    1.83 +  remove  :: "['a, 'b, 'b]                           => bool"
    1.84 +  bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
    1.85  
    1.86 -rules   append	"append  []    xs  xs    ..
    1.87 -		 append (x#xs) ys (x#zs) :- append xs ys zs"
    1.88 -	reverse "reverse L1 L2 :- (!rev_aux. 
    1.89 -		  (!L.          rev_aux  []    L  L )..
    1.90 -		  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    1.91 -		  => rev_aux L1 L2 [])"
    1.92 +axioms
    1.93 +        append:  "append  []    xs  xs    ..
    1.94 +                  append (x#xs) ys (x#zs) :- append xs ys zs"
    1.95 +        reverse: "reverse L1 L2 :- (!rev_aux.
    1.96 +                  (!L.          rev_aux  []    L  L )..
    1.97 +                  (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    1.98 +                  => rev_aux L1 L2 [])"
    1.99  
   1.100 -	mappred "mappred P  []     []    ..
   1.101 -		 mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
   1.102 -	mapfun  "mapfun f  []     []      ..
   1.103 -		 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
   1.104 +        mappred: "mappred P  []     []    ..
   1.105 +                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
   1.106 +        mapfun:  "mapfun f  []     []      ..
   1.107 +                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
   1.108  
   1.109 -	age     "age bob 24 ..
   1.110 -		 age sue 23 ..
   1.111 -		 age ned 23"
   1.112 +        age:     "age bob 24 ..
   1.113 +                  age sue 23 ..
   1.114 +                  age ned 23"
   1.115  
   1.116 -	eq	"eq x x"
   1.117 +        eq:      "eq x x"
   1.118  
   1.119  (* actual definitions of empty and add is hidden -> yields abstract data type *)
   1.120  
   1.121 -	bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
   1.122 -				empty    S1    &
   1.123 -				add A    S1 S2 &
   1.124 -				add B    S2 S3 &
   1.125 -				remove X S3 S4 &
   1.126 -				remove Y S4 S5 &
   1.127 -				empty    S5)"
   1.128 +        bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
   1.129 +                                empty    S1    &
   1.130 +                                add A    S1 S2 &
   1.131 +                                add B    S2 S3 &
   1.132 +                                remove X S3 S4 &
   1.133 +                                remove Y S4 S5 &
   1.134 +                                empty    S5)"
   1.135 +
   1.136 +ML {* use_legacy_bindings (the_context ()) *}
   1.137 +
   1.138  end