src/FOLP/ex/Prolog.ML
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 5061 f947332d5465
child 24584 01e83ffa6c54
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1464
a608f83e3421 expanded tabs; removed commit() from ROOT.ML
clasohm
parents: 1459
diff changeset
     1
(*  Title:      FOLP/ex/prolog.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For ex/prolog.thy.  First-Order Logic: PROLOG examples
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Prolog;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    11
Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
by (resolve_tac [appNil,appCons] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (resolve_tac [appNil,appCons] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
by (resolve_tac [appNil,appCons] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
by (resolve_tac [appNil,appCons] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
prth (result());
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    18
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
by (REPEAT (resolve_tac [appNil,appCons] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    23
Goal "app(?x, ?y, a:b:c:d:Nil)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
by (REPEAT (resolve_tac [appNil,appCons] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    35
Goal "rev(a:b:c:d:Nil, ?x)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val rules = [appNil,appCons,revNil,revCons];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
by (REPEAT (resolve_tac rules 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    40
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (REPEAT (resolve_tac rules 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    44
Goal "rev(?x, a:b:c:Nil)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*backtracking version*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
choplev 0;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
by prolog_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    56
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by prolog_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
(*rev([a..p], ?w) requires 153 inferences *)
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    61
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(*Poly/ML: 4 secs >> 38 lips*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  total inferences = 2 + 1 + 17 + 561 = 581*)
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1464
diff changeset
    68
Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    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)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
(*Poly/ML: 29 secs >> 20 lips*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
writeln"Reached end of file.";