src/FOLP/ex/Prolog.ML
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 32091 30e2ffbba718
child 35762 af3ff2ba4c54
permissions -rw-r--r--
renamed structure Display_Goal to Goal_Display;
haftmann@24584
     1
(*  Title:      FOLP/ex/Prolog.ML
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For ex/prolog.thy.  First-Order Logic: PROLOG examples
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Prolog;
clasohm@0
    10
wenzelm@5061
    11
Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
clasohm@0
    12
by (resolve_tac [appNil,appCons] 1);
clasohm@0
    13
by (resolve_tac [appNil,appCons] 1);
clasohm@0
    14
by (resolve_tac [appNil,appCons] 1);
clasohm@0
    15
by (resolve_tac [appNil,appCons] 1);
wenzelm@32091
    16
result();
clasohm@0
    17
wenzelm@5061
    18
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
clasohm@0
    19
by (REPEAT (resolve_tac [appNil,appCons] 1));
clasohm@0
    20
result();
clasohm@0
    21
clasohm@0
    22
wenzelm@5061
    23
Goal "app(?x, ?y, a:b:c:d:Nil)";
clasohm@0
    24
by (REPEAT (resolve_tac [appNil,appCons] 1));
clasohm@0
    25
back();
clasohm@0
    26
back();
clasohm@0
    27
back();
clasohm@0
    28
back();
clasohm@0
    29
result();
clasohm@0
    30
clasohm@0
    31
clasohm@0
    32
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
clasohm@0
    33
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
clasohm@0
    34
wenzelm@5061
    35
Goal "rev(a:b:c:d:Nil, ?x)";
clasohm@0
    36
val rules = [appNil,appCons,revNil,revCons];
clasohm@0
    37
by (REPEAT (resolve_tac rules 1));
clasohm@0
    38
result();
clasohm@0
    39
wenzelm@5061
    40
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
clasohm@0
    41
by (REPEAT (resolve_tac rules 1));
clasohm@0
    42
result();
clasohm@0
    43
wenzelm@5061
    44
Goal "rev(?x, a:b:c:Nil)";
clasohm@0
    45
by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*)
clasohm@0
    46
back();
clasohm@0
    47
back();
clasohm@0
    48
clasohm@0
    49
(*backtracking version*)
clasohm@0
    50
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1);
clasohm@0
    51
clasohm@0
    52
choplev 0;
clasohm@0
    53
by prolog_tac;
clasohm@0
    54
result();
clasohm@0
    55
wenzelm@5061
    56
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
clasohm@0
    57
by prolog_tac;
clasohm@0
    58
result();
clasohm@0
    59
clasohm@0
    60
(*rev([a..p], ?w) requires 153 inferences *)
wenzelm@5061
    61
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
clasohm@0
    62
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
clasohm@0
    63
(*Poly/ML: 4 secs >> 38 lips*)
clasohm@0
    64
result();
clasohm@0
    65
clasohm@0
    66
(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences;
clasohm@0
    67
  total inferences = 2 + 1 + 17 + 561 = 581*)
wenzelm@5061
    68
Goal
clasohm@0
    69
    "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)";
clasohm@0
    70
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
clasohm@0
    71
(*Poly/ML: 29 secs >> 20 lips*)
clasohm@0
    72
result();
clasohm@0
    73
clasohm@0
    74
writeln"Reached end of file.";