1 (* Title: FOL/ex/prolog.thy
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1992 University of Cambridge
6 First-Order Logic: PROLOG examples
8 Inherits from FOL the class term, the type o, and the coercion Trueprop
13 arities list :: (term)term
14 consts Nil :: "'a list"
15 ":" :: "['a, 'a list]=> 'a list" (infixr 60)
16 app :: "['a list, 'a list, 'a list] => o"
17 rev :: "['a list, 'a list] => o"
18 rules appNil "app(Nil,ys,ys)"
19 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
21 revCons "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"