src/Sequents/Washing.thy
author wenzelm
Tue Mar 18 11:07:47 2014 +0100 (2014-03-18)
changeset 56199 8e8d28ed7529
parent 55232 7a46672934a3
child 60770 240563fbf41d
permissions -rw-r--r--
tuned signature -- rearranged modules;
     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 |- (quarter >< quarter >< quarter >< quarter)" and
    19 
    20   load1:
    21   "quarter , quarter , quarter , quarter , quarter |- loaded" and
    22 
    23   load2:
    24   "dollar , quarter |- loaded" and
    25 
    26   wash:
    27   "loaded , dirty |- wet" and
    28 
    29   dry:
    30   "wet, quarter , quarter , quarter |- clean"
    31 
    32 
    33 (* "activate" definitions for use in proof *)
    34 
    35 ML {* ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
    36 ML {* ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
    37 ML {* ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
    38 ML {* ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
    39 
    40 (* a load of dirty clothes and two dollars gives you clean clothes *)
    41 
    42 lemma "dollar , dollar , dirty |- clean"
    43   by (best add!: changeI load1I washI dryI)
    44 
    45 (* order of premises doesn't matter *)
    46 
    47 lemma "dollar , dirty , dollar |- clean"
    48   by (best add!: changeI load1I washI dryI)
    49 
    50 (* alternative formulation *)
    51 
    52 lemma "dollar , dollar |- dirty -o clean"
    53   by (best add!: changeI load1I washI dryI)
    54 
    55 end