src/HOL/Prolog/Test.thy

--- a/src/HOL/Prolog/Test.thy	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Test.thy	Mon Nov 20 21:23:12 2006 +0100
@@ -80,6 +80,202 @@
                                 remove Y S4 S5 &
                                 empty    S5)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
+
+lemma "append ?x ?y [a,b,c,d]"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  back
+  done
+
+lemma "append [a,b] y ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "!y. append [a,b] y (?L y)"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [23] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [23,24,?x] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse ?L [23,24,?x]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mappred age ?x [23,24]"
+  apply (prolog prog_Test)
+  back
+  done
+
+lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mappred ?P [bob,sue] [24,23]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun (%x. h x 25) [bob,sue] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun ?F [24] [h 24 24]"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  done
+
+lemma "True"
+  apply (prolog prog_Test)
+  done
+
+lemma "age ?x 24 & age ?y 23"
+  apply (prolog prog_Test)
+  back
+  done
+
+lemma "age ?x 24 | age ?x 23"
+  apply (prolog prog_Test)
+  back
+  back
+  done
+
+lemma "? x y. age x y"
+  apply (prolog prog_Test)
+  done
+
+lemma "!x y. append [] x x"
+  apply (prolog prog_Test)
+  done
+
+lemma "age sue 24 .. age bob 23 => age ?x ?y"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  back
+  done
+
+(*set trace_DEPTH_FIRST;*)
+lemma "age bob 25 :- age bob 24 => age bob 25"
+  apply (prolog prog_Test)
+  done
+(*reset trace_DEPTH_FIRST;*)
+
+lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  done
+
+lemma "!x. ? y. eq x y"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. P & eq P ?x"
+  apply (prolog prog_Test)
+(*
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+*)
+  done
+
+lemma "? P. eq P (True & True) & P"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. eq P op | & P k True"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. eq P (Q => True) & P"
+  apply (prolog prog_Test)
+  done
+
+(* P flexible: *)
+lemma "(!P k l. P k l :- eq P Q) => Q a b"
+  apply (prolog prog_Test)
+  done
+(*
+loops:
+lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
+*)
+
+(* implication and disjunction in atom: *)
+lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
+  by fast
+
+(* disjunction in atom: *)
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+  apply (tactic "step_tac HOL_cs 1")
+  apply (tactic "step_tac HOL_cs 1")
+  apply (tactic "step_tac HOL_cs 1")
+   prefer 2
+   apply fast
+  apply fast
+  done
+
+(*
+hangs:
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+  by fast
+*)
+
+lemma "!Emp Stk.(
+                       empty    (Emp::'b) .. 
+         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
+         (!(X::nat) S. remove X ((Stk X S)::'b) S))
+ => bag_appl 23 24 ?X ?Y"
+  oops
+
+lemma "!Qu. ( 
+          (!L.            empty    (Qu L L)) .. 
+          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
+          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
+ => bag_appl 23 24 ?X ?Y"
+  oops
+
+lemma "D & (!y. E) :- (!x. True & True) :- True => D"
+  apply (prolog prog_Test)
+  done
+
+lemma "P x .. P y => P ?X"
+  apply (prolog prog_Test)
+  back
+  done
+(*
+back
+-> problem with DEPTH_SOLVE:
+Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
+Exception raised at run-time
+*)
 
 end