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