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