src/Sequents/Washing.thy
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21426 87ac12bed1ab
child 26480 544cef16045b
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 
     2 (* $Id$ *)
     3 
     4 (* code by Sara Kalvala, based on Paulson's LK
     5                            and Moore's tisl.ML *)
     6 
     7 theory Washing
     8 imports ILL
     9 begin
    10 
    11 consts
    12   dollar :: o
    13   quarter :: o
    14   loaded :: o
    15   dirty :: o
    16   wet :: o
    17   clean :: o
    18 
    19 axioms
    20   change:
    21   "dollar |- (quarter >< quarter >< quarter >< quarter)"
    22 
    23   load1:
    24   "quarter , quarter , quarter , quarter , quarter |- loaded"
    25 
    26   load2:
    27   "dollar , quarter |- loaded"
    28 
    29   wash:
    30   "loaded , dirty |- wet"
    31 
    32   dry:
    33   "wet, quarter , quarter , quarter |- clean"
    34 
    35 
    36 (* "activate" definitions for use in proof *)
    37 
    38 ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
    39 ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
    40 ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
    41 ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
    42 
    43 (* a load of dirty clothes and two dollars gives you clean clothes *)
    44 
    45 lemma "dollar , dollar , dirty |- clean"
    46   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    47   done
    48 
    49 (* order of premises doesn't matter *)
    50 
    51 lemma "dollar , dirty , dollar |- clean"
    52   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    53   done
    54 
    55 (* alternative formulation *)
    56 
    57 lemma "dollar , dollar |- dirty -o clean"
    58   apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    59   done
    60 
    61 end