13208
|
1 |
(* Title: HOL/Prolog/Func.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
*)
|
|
6 |
|
9015
|
7 |
open Func;
|
|
8 |
|
|
9 |
val prog_Func = prog_HOHH @ [eval];
|
12486
|
10 |
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
|
9015
|
11 |
val p = ptac prog_Func 1;
|
|
12 |
|
|
13 |
pgoal "eval ((S (S Z)) + (S Z)) ?X";
|
|
14 |
|
|
15 |
pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
|
|
16 |
\(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
|
|
17 |
|
|
18 |
|