src/HOL/Prolog/Test.thy
author wenzelm
Wed Sep 07 21:07:09 2005 +0200 (2005-09-07)
changeset 17311 5b1d47d920ce
parent 14981 e73f8140af78
child 21425 c11ab38b78a7
permissions -rw-r--r--
converted to Isar theory format;
     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 
     6 header {* Basic examples *}
     7 
     8 theory Test
     9 imports HOHH
    10 begin
    11 
    12 typedecl nat
    13 
    14 typedecl 'a list
    15 
    16 consts
    17   Nil   :: "'a list"                                  ("[]")
    18   Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
    19 
    20 syntax
    21   (* list Enumeration *)
    22   "@list"     :: "args => 'a list"                          ("[(_)]")
    23 
    24 translations
    25   "[x, xs]"     == "x#[xs]"
    26   "[x]"         == "x#[]"
    27 
    28 typedecl person
    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 axioms
    55         append:  "append  []    xs  xs    ..
    56                   append (x#xs) ys (x#zs) :- append xs ys zs"
    57         reverse: "reverse L1 L2 :- (!rev_aux.
    58                   (!L.          rev_aux  []    L  L )..
    59                   (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
    60                   => rev_aux L1 L2 [])"
    61 
    62         mappred: "mappred P  []     []    ..
    63                   mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys"
    64         mapfun:  "mapfun f  []     []      ..
    65                   mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
    66 
    67         age:     "age bob 24 ..
    68                   age sue 23 ..
    69                   age ned 23"
    70 
    71         eq:      "eq x x"
    72 
    73 (* actual definitions of empty and add is hidden -> yields abstract data type *)
    74 
    75         bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
    76                                 empty    S1    &
    77                                 add A    S1 S2 &
    78                                 add B    S2 S3 &
    79                                 remove X S3 S4 &
    80                                 remove Y S4 S5 &
    81                                 empty    S5)"
    82 
    83 ML {* use_legacy_bindings (the_context ()) *}
    84 
    85 end