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