|
clasohm@0
|
1 |
(* Title: FOL/ex/prolog.thy
|
|
clasohm@0
|
2 |
ID: $Id$
|
|
clasohm@0
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
clasohm@0
|
4 |
Copyright 1992 University of Cambridge
|
|
clasohm@0
|
5 |
|
|
clasohm@0
|
6 |
First-Order Logic: PROLOG examples
|
|
clasohm@0
|
7 |
|
|
clasohm@0
|
8 |
Inherits from FOL the class term, the type o, and the coercion Trueprop
|
|
clasohm@0
|
9 |
*)
|
|
clasohm@0
|
10 |
|
|
clasohm@0
|
11 |
Prolog = FOL +
|
|
lcp@352
|
12 |
types 'a list
|
|
clasohm@0
|
13 |
arities list :: (term)term
|
|
clasohm@0
|
14 |
consts Nil :: "'a list"
|
|
clasohm@0
|
15 |
":" :: "['a, 'a list]=> 'a list" (infixr 60)
|
|
clasohm@0
|
16 |
app :: "['a list, 'a list, 'a list] => o"
|
|
clasohm@0
|
17 |
rev :: "['a list, 'a list] => o"
|
|
clasohm@0
|
18 |
rules appNil "app(Nil,ys,ys)"
|
|
clasohm@0
|
19 |
appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
|
|
clasohm@0
|
20 |
revNil "rev(Nil,Nil)"
|
|
clasohm@0
|
21 |
revCons "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
|
|
clasohm@0
|
22 |
end
|