src/HOL/Prolog/Test.ML
changeset 21425 c11ab38b78a7
parent 21424 5295ffa18285
child 21426 87ac12bed1ab
     1.1 --- a/src/HOL/Prolog/Test.ML	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,145 +0,0 @@
     1.4 -(*  Title:    HOL/Prolog/Test.ML
     1.5 -    ID:       $Id$
     1.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 -*)
     1.8 -
     1.9 -val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
    1.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
    1.11 -val p = ptac prog_Test 1;
    1.12 -
    1.13 -pgoal "append ?x ?y [a,b,c,d]";
    1.14 -back();
    1.15 -back();
    1.16 -back();
    1.17 -back();
    1.18 -
    1.19 -pgoal "append [a,b] y ?L";
    1.20 -pgoal "!y. append [a,b] y (?L y)";
    1.21 -
    1.22 -pgoal "reverse [] ?L";
    1.23 -
    1.24 -pgoal "reverse [23] ?L";
    1.25 -pgoal "reverse [23,24,?x] ?L";
    1.26 -pgoal "reverse ?L [23,24,?x]";
    1.27 -
    1.28 -pgoal "mappred age ?x [23,24]";
    1.29 -back();
    1.30 -
    1.31 -pgoal "mappred (%x y. ? z. age z y) ?x [23,24]";
    1.32 -
    1.33 -pgoal "mappred ?P [bob,sue] [24,23]";
    1.34 -
    1.35 -pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]";
    1.36 -
    1.37 -pgoal "mapfun (%x. h x 25) [bob,sue] ?L";
    1.38 -
    1.39 -pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]";
    1.40 -
    1.41 -pgoal "mapfun ?F [24] [h 24 24]";
    1.42 -back();
    1.43 -back();
    1.44 -back();
    1.45 -
    1.46 -
    1.47 -(*
    1.48 -goal (the_context ()) "f a = ?g a a & ?g = x";
    1.49 -by (rtac conjI 1);
    1.50 -by (rtac refl 1);
    1.51 -back();
    1.52 -back();
    1.53 -*)
    1.54 -
    1.55 -pgoal "True";
    1.56 -
    1.57 -pgoal "age ?x 24 & age ?y 23";
    1.58 -back();
    1.59 -
    1.60 -pgoal "age ?x 24 | age ?x 23";
    1.61 -back();
    1.62 -back();
    1.63 -
    1.64 -pgoal "? x y. age x y";
    1.65 -
    1.66 -pgoal "!x y. append [] x x";
    1.67 -
    1.68 -pgoal "age sue 24 .. age bob 23 => age ?x ?y";
    1.69 -back();
    1.70 -back();
    1.71 -back();
    1.72 -back();
    1.73 -
    1.74 -(*set trace_DEPTH_FIRST;*)
    1.75 -pgoal "age bob 25 :- age bob 24 => age bob 25";
    1.76 -(*reset trace_DEPTH_FIRST;*)
    1.77 -
    1.78 -pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25";
    1.79 -back();
    1.80 -back();
    1.81 -back();
    1.82 -
    1.83 -pgoal "!x. ? y. eq x y";
    1.84 -
    1.85 -pgoal "? P. P & eq P ?x";
    1.86 -(*
    1.87 -back();
    1.88 -back();
    1.89 -back();
    1.90 -back();
    1.91 -back();
    1.92 -back();
    1.93 -back();
    1.94 -back();
    1.95 -*)
    1.96 -
    1.97 -pgoal "? P. eq P (True & True) & P";
    1.98 -
    1.99 -pgoal "? P. eq P op | & P k True";
   1.100 -
   1.101 -pgoal "? P. eq P (Q => True) & P";
   1.102 -
   1.103 -(* P flexible: *)
   1.104 -pgoal "(!P k l. P k l :- eq P Q) => Q a b";
   1.105 -(*
   1.106 -loops:
   1.107 -pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b";
   1.108 -*)
   1.109 -
   1.110 -(* implication and disjunction in atom: *)
   1.111 -goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
   1.112 -by (fast_tac HOL_cs 1);
   1.113 -
   1.114 -(* disjunction in atom: *)
   1.115 -goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
   1.116 -by (step_tac HOL_cs 1);
   1.117 -by (step_tac HOL_cs 1);
   1.118 -by (step_tac HOL_cs 1);
   1.119 -by (fast_tac HOL_cs 2);
   1.120 -by (fast_tac HOL_cs 1);
   1.121 -(*
   1.122 -hangs:
   1.123 -goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
   1.124 -by (fast_tac HOL_cs 1);
   1.125 -*)
   1.126 -
   1.127 -pgoal "!Emp Stk.(\
   1.128 -\                       empty    (Emp::'b) .. \
   1.129 -\         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. \
   1.130 -\         (!(X::nat) S. remove X ((Stk X S)::'b) S))\
   1.131 -\ => bag_appl 23 24 ?X ?Y";
   1.132 -
   1.133 -pgoal "!Qu. ( \
   1.134 -\          (!L.            empty    (Qu L L)) .. \
   1.135 -\          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..\
   1.136 -\          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\
   1.137 -\ => bag_appl 23 24 ?X ?Y";
   1.138 -
   1.139 -pgoal "D & (!y. E) :- (!x. True & True) :- True => D";
   1.140 -
   1.141 -pgoal "P x .. P y => P ?X";
   1.142 -back();
   1.143 -(*
   1.144 -back();
   1.145 --> problem with DEPTH_SOLVE:
   1.146 -Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
   1.147 -Exception raised at run-time
   1.148 -*)