src/Sequents/Washing.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 61386 0a29a984a91b
permissions -rw-r--r--
more permissive;
     1 (*  Title:      Sequents/Washing.thy
     2     Author:     Sara Kalvala
     3 *)
     4 
     5 theory Washing
     6 imports ILL
     7 begin
     8 
     9 axiomatization
    10   dollar :: o and
    11   quarter :: o and
    12   loaded :: o and
    13   dirty :: o and
    14   wet :: o and
    15   clean :: o
    16 where
    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 
    35 ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
    36 ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
    37 ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
    38 ML \<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 
    42 lemma "dollar , dollar , dirty \<turnstile> clean"
    43   by (best add!: changeI load1I washI dryI)
    44 
    45 (* order of premises doesn't matter *)
    46 
    47 lemma "dollar , dirty , dollar \<turnstile> clean"
    48   by (best add!: changeI load1I washI dryI)
    49 
    50 (* alternative formulation *)
    51 
    52 lemma "dollar , dollar \<turnstile> dirty -o clean"
    53   by (best add!: changeI load1I washI dryI)
    54 
    55 end