src/Sequents/Washing.thy
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 35762 af3ff2ba4c54
child 39159 0dec18004e75
permissions -rw-r--r--
storing options for prolog code generation in the theory
     1 (*  Title:      Sequents/Washing.thy
     2     Author:     Sara Kalvala
     3 *)
     4 
     5 theory Washing
     6 imports ILL
     7 begin
     8 
     9 consts
    10   dollar :: o
    11   quarter :: o
    12   loaded :: o
    13   dirty :: o
    14   wet :: o
    15   clean :: o
    16 
    17 axioms
    18   change:
    19   "dollar |- (quarter >< quarter >< quarter >< quarter)"
    20 
    21   load1:
    22   "quarter , quarter , quarter , quarter , quarter |- loaded"
    23 
    24   load2:
    25   "dollar , quarter |- loaded"
    26 
    27   wash:
    28   "loaded , dirty |- wet"
    29 
    30   dry:
    31   "wet, quarter , quarter , quarter |- clean"
    32 
    33 
    34 (* "activate" definitions for use in proof *)
    35 
    36 ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
    37 ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
    38 ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
    39 ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
    40 
    41 (* a load of dirty clothes and two dollars gives you clean clothes *)
    42 
    43 lemma "dollar , dollar , dirty |- clean"
    44   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    45   done
    46 
    47 (* order of premises doesn't matter *)
    48 
    49 lemma "dollar , dirty , dollar |- clean"
    50   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    51   done
    52 
    53 (* alternative formulation *)
    54 
    55 lemma "dollar , dollar |- dirty -o clean"
    56   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    57   done
    58 
    59 end