src/FOLP/ex/Prolog.ML
author haftmann
Mon, 01 Mar 2010 13:40:23 +0100
changeset 35416 d8d7d1b785af
parent 32091 30e2ffbba718
child 35762 af3ff2ba4c54
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 5061
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);
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 24584
diff changeset
    16
result();
0
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.";