1(*  Title:      Sequents/Washing.thy
2    Author:     Sara Kalvala
3*)
4
5theory Washing
6imports ILL
7begin
8
9axiomatization
10  dollar :: o and
11  quarter :: o and
12  loaded :: o and
13  dirty :: o and
14  wet :: o and
15  clean :: o
16where
17  change:
18  "dollar \<turnstile> (quarter >< quarter >< quarter >< quarter)" and
19
20  load1:
21  "quarter , quarter , quarter , quarter , quarter \<turnstile> loaded" and
22
23  load2:
24  "dollar , quarter \<turnstile> loaded" and
25
26  wash:
27  "loaded , dirty \<turnstile> wet" and
28
29  dry:
30  "wet, quarter , quarter , quarter \<turnstile> clean"
31
32
33(* "activate" definitions for use in proof *)
34
35ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
36ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
37ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
38ML \<open>ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}])))\<close>
39
40(* a load of dirty clothes and two dollars gives you clean clothes *)
41
42lemma "dollar , dollar , dirty \<turnstile> clean"
43  by (best add!: changeI load1I washI dryI)
44
45(* order of premises doesn't matter *)
46
47lemma "dollar , dirty , dollar \<turnstile> clean"
48  by (best add!: changeI load1I washI dryI)
49
50(* alternative formulation *)
51
52lemma "dollar , dollar \<turnstile> dirty -o clean"
53  by (best add!: changeI load1I washI dryI)
54
55end
56