--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/Washing.thy Mon Nov 20 23:47:10 2006 +0100
@@ -0,0 +1,61 @@
+
+(* $Id$ *)
+
+(* code by Sara Kalvala, based on Paulson's LK
+ and Moore's tisl.ML *)
+
+theory Washing
+imports ILL
+begin
+
+consts
+ dollar :: o
+ quarter :: o
+ loaded :: o
+ dirty :: o
+ wet :: o
+ clean :: o
+
+axioms
+ change:
+ "dollar |- (quarter >< quarter >< quarter >< quarter)"
+
+ load1:
+ "quarter , quarter , quarter , quarter , quarter |- loaded"
+
+ load2:
+ "dollar , quarter |- loaded"
+
+ wash:
+ "loaded , dirty |- wet"
+
+ dry:
+ "wet, quarter , quarter , quarter |- clean"
+
+
+(* "activate" definitions for use in proof *)
+
+ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
+ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
+ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
+ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
+
+(* a load of dirty clothes and two dollars gives you clean clothes *)
+
+lemma "dollar , dollar , dirty |- clean"
+ apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ done
+
+(* order of premises doesn't matter *)
+
+lemma "dollar , dirty , dollar |- clean"
+ apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ done
+
+(* alternative formulation *)
+
+lemma "dollar , dollar |- dirty -o clean"
+ apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
+ done
+
+end