src/HOL/Prolog/Test.ML
author oheimb
Tue Jun 11 16:43:17 2002 +0200 (2002-06-11)
changeset 13208 965f95a3abd9
parent 12486 0ed8bdd883e0
child 14981 e73f8140af78
permissions -rw-r--r--
added the usual file headers
oheimb@13208
     1
(*  Title:    HOL/Prolog/Test.ML
oheimb@13208
     2
    ID:       $Id$
oheimb@13208
     3
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
oheimb@13208
     4
    License:  GPL (GNU GENERAL PUBLIC LICENSE)
oheimb@13208
     5
*)
oheimb@13208
     6
oheimb@9015
     7
open Test;
oheimb@9015
     8
oheimb@9015
     9
val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
wenzelm@12486
    10
fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
oheimb@9015
    11
val p = ptac prog_Test 1;
oheimb@9015
    12
oheimb@9015
    13
pgoal "append ?x ?y [a,b,c,d]";
oheimb@9015
    14
back();
oheimb@9015
    15
back();
oheimb@9015
    16
back();
oheimb@9015
    17
back();
oheimb@9015
    18
oheimb@9015
    19
pgoal "append [a,b] y ?L";
oheimb@9015
    20
pgoal "!y. append [a,b] y (?L y)";
oheimb@9015
    21
oheimb@9015
    22
pgoal "reverse [] ?L";
oheimb@9015
    23
oheimb@9015
    24
pgoal "reverse [23] ?L";
oheimb@9015
    25
pgoal "reverse [23,24,?x] ?L";
oheimb@9015
    26
pgoal "reverse ?L [23,24,?x]";
oheimb@9015
    27
oheimb@9015
    28
pgoal "mappred age ?x [23,24]";
oheimb@9015
    29
back();
oheimb@9015
    30
oheimb@9015
    31
pgoal "mappred (%x y. ? z. age z y) ?x [23,24]";
oheimb@9015
    32
oheimb@9015
    33
pgoal "mappred ?P [bob,sue] [24,23]";
oheimb@9015
    34
oheimb@9015
    35
pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]";
oheimb@9015
    36
oheimb@9015
    37
pgoal "mapfun (%x. h x 25) [bob,sue] ?L";
oheimb@9015
    38
oheimb@9015
    39
pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]";
oheimb@9015
    40
oheimb@9015
    41
pgoal "mapfun ?F [24] [h 24 24]";
oheimb@9015
    42
back();
oheimb@9015
    43
back();
oheimb@9015
    44
back();
oheimb@9015
    45
oheimb@9015
    46
oheimb@9015
    47
(*
oheimb@9015
    48
goal thy "f a = ?g a a & ?g = x"; 
wenzelm@12486
    49
by (rtac conjI 1);
wenzelm@12486
    50
by (rtac refl 1);
oheimb@9015
    51
back();
oheimb@9015
    52
back();
oheimb@9015
    53
*)
oheimb@9015
    54
oheimb@9015
    55
pgoal "True";
oheimb@9015
    56
oheimb@9015
    57
pgoal "age ?x 24 & age ?y 23";
oheimb@9015
    58
back();
oheimb@9015
    59
oheimb@9015
    60
pgoal "age ?x 24 | age ?x 23";
oheimb@9015
    61
back();
oheimb@9015
    62
back();
oheimb@9015
    63
oheimb@9015
    64
pgoal "? x y. age x y";
oheimb@9015
    65
oheimb@9015
    66
pgoal "!x y. append [] x x";
oheimb@9015
    67
oheimb@9015
    68
pgoal "age sue 24 .. age bob 23 => age ?x ?y";
oheimb@9015
    69
back();
oheimb@9015
    70
back();
oheimb@9015
    71
back();
oheimb@9015
    72
back();
oheimb@9015
    73
oheimb@9015
    74
(*set trace_DEPTH_FIRST;*)
oheimb@9015
    75
pgoal "age bob 25 :- age bob 24 => age bob 25";
oheimb@9015
    76
(*reset trace_DEPTH_FIRST;*)
oheimb@9015
    77
oheimb@9015
    78
pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25";
oheimb@9015
    79
back();
oheimb@9015
    80
back();
oheimb@9015
    81
back();
oheimb@9015
    82
oheimb@9015
    83
pgoal "!x. ? y. eq x y";
oheimb@9015
    84
oheimb@9015
    85
pgoal "? P. P & eq P ?x";
oheimb@9015
    86
(*
oheimb@9015
    87
back();
oheimb@9015
    88
back();
oheimb@9015
    89
back();
oheimb@9015
    90
back();
oheimb@9015
    91
back();
oheimb@9015
    92
back();
oheimb@9015
    93
back();
oheimb@9015
    94
back();
oheimb@9015
    95
*)
oheimb@9015
    96
oheimb@9015
    97
pgoal "? P. eq P (True & True) & P";
oheimb@9015
    98
oheimb@9015
    99
pgoal "? P. eq P op | & P k True";
oheimb@9015
   100
oheimb@9015
   101
pgoal "? P. eq P (Q => True) & P";
oheimb@9015
   102
oheimb@9015
   103
(* P flexible: *)
oheimb@9015
   104
pgoal "(!P k l. P k l :- eq P Q) => Q a b";
oheimb@9015
   105
(*
oheimb@9015
   106
loops:
oheimb@9015
   107
pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b";
oheimb@9015
   108
*)
oheimb@9015
   109
oheimb@9015
   110
(* implication and disjunction in atom: *)
oheimb@9015
   111
goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
wenzelm@12486
   112
by (fast_tac HOL_cs 1);
oheimb@9015
   113
oheimb@9015
   114
(* disjunction in atom: *)
oheimb@9015
   115
goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
wenzelm@12486
   116
by (step_tac HOL_cs 1);
wenzelm@12486
   117
by (step_tac HOL_cs 1);
wenzelm@12486
   118
by (step_tac HOL_cs 1);
wenzelm@12486
   119
by (fast_tac HOL_cs 2);
wenzelm@12486
   120
by (fast_tac HOL_cs 1);
oheimb@9015
   121
(*
oheimb@9015
   122
hangs:
oheimb@9015
   123
goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
wenzelm@12486
   124
by (fast_tac HOL_cs 1);
oheimb@9015
   125
*)
oheimb@9015
   126
oheimb@9015
   127
pgoal "!Emp Stk.(\
oheimb@9015
   128
\                       empty    (Emp::'b) .. \
oheimb@9015
   129
\         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. \
oheimb@9015
   130
\         (!(X::nat) S. remove X ((Stk X S)::'b) S))\
oheimb@9015
   131
\ => bag_appl 23 24 ?X ?Y";
oheimb@9015
   132
oheimb@9015
   133
pgoal "!Qu. ( \
oheimb@9015
   134
\          (!L.            empty    (Qu L L)) .. \
oheimb@9015
   135
\          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..\
oheimb@9015
   136
\          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\
oheimb@9015
   137
\ => bag_appl 23 24 ?X ?Y";
oheimb@9015
   138
oheimb@9015
   139
pgoal "D & (!y. E) :- (!x. True & True) :- True => D";
oheimb@9015
   140
oheimb@9015
   141
pgoal "P x .. P y => P ?X";
oheimb@9015
   142
back();
oheimb@9015
   143
(*
oheimb@9015
   144
back();
oheimb@9015
   145
-> problem with DEPTH_SOLVE:
oheimb@9015
   146
Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
oheimb@9015
   147
Exception raised at run-time
oheimb@9015
   148
*)