src/Sequents/Washing.thy
changeset 21426 87ac12bed1ab
child 26480 544cef16045b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/Washing.thy	Mon Nov 20 23:47:10 2006 +0100
     1.3 @@ -0,0 +1,61 @@
     1.4 +
     1.5 +(* $Id$ *)
     1.6 +
     1.7 +(* code by Sara Kalvala, based on Paulson's LK
     1.8 +                           and Moore's tisl.ML *)
     1.9 +
    1.10 +theory Washing
    1.11 +imports ILL
    1.12 +begin
    1.13 +
    1.14 +consts
    1.15 +  dollar :: o
    1.16 +  quarter :: o
    1.17 +  loaded :: o
    1.18 +  dirty :: o
    1.19 +  wet :: o
    1.20 +  clean :: o
    1.21 +
    1.22 +axioms
    1.23 +  change:
    1.24 +  "dollar |- (quarter >< quarter >< quarter >< quarter)"
    1.25 +
    1.26 +  load1:
    1.27 +  "quarter , quarter , quarter , quarter , quarter |- loaded"
    1.28 +
    1.29 +  load2:
    1.30 +  "dollar , quarter |- loaded"
    1.31 +
    1.32 +  wash:
    1.33 +  "loaded , dirty |- wet"
    1.34 +
    1.35 +  dry:
    1.36 +  "wet, quarter , quarter , quarter |- clean"
    1.37 +
    1.38 +
    1.39 +(* "activate" definitions for use in proof *)
    1.40 +
    1.41 +ML_setup {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
    1.42 +ML_setup {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
    1.43 +ML_setup {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
    1.44 +ML_setup {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
    1.45 +
    1.46 +(* a load of dirty clothes and two dollars gives you clean clothes *)
    1.47 +
    1.48 +lemma "dollar , dollar , dirty |- clean"
    1.49 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    1.50 +  done
    1.51 +
    1.52 +(* order of premises doesn't matter *)
    1.53 +
    1.54 +lemma "dollar , dirty , dollar |- clean"
    1.55 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    1.56 +  done
    1.57 +
    1.58 +(* alternative formulation *)
    1.59 +
    1.60 +lemma "dollar , dollar |- dirty -o clean"
    1.61 +  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
    1.62 +  done
    1.63 +
    1.64 +end