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