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