src/Sequents/ex/ILL/washing.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/washing.ML	Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,33 @@
+
+open washing;
+
+(* "activate" definitions for use in proof *)
+
+val changeI = [context1] RL ([change] RLN (2,[cut]));
+val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
+val washI =   [context1] RL ([wash]   RLN (2,[cut]));
+val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
+
+
+
+(* a load of dirty clothes and two dollars gives you clean clothes *)
+
+goal thy "dollar , dollar , dirty |- clean";
+
+by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
+
+
+(* order of premises doesn't matter *)
+
+prove_goal thy "dollar , dirty , dollar |- clean"
+(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
+
+
+(* alternative formulation *)
+
+prove_goal thy "dollar , dollar |- dirty -o clean"
+(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
+
+
+
+