src/Sequents/Washing.thy
author wenzelm
Sat Jun 02 22:40:03 2018 +0200 (17 months ago)
changeset 68358 e761afd35baa
parent 61386 0a29a984a91b
permissions -rw-r--r--
tuned proofs;
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@51309
     9
axiomatization
wenzelm@51309
    10
  dollar :: o and
wenzelm@51309
    11
  quarter :: o and
wenzelm@51309
    12
  loaded :: o and
wenzelm@51309
    13
  dirty :: o and
wenzelm@51309
    14
  wet :: o and
wenzelm@21426
    15
  clean :: o
wenzelm@51309
    16
where
wenzelm@21426
    17
  change:
wenzelm@61386
    18
  "dollar \<turnstile> (quarter >< quarter >< quarter >< quarter)" and
wenzelm@21426
    19
wenzelm@21426
    20
  load1:
wenzelm@61386
    21
  "quarter , quarter , quarter , quarter , quarter \<turnstile> loaded" and
wenzelm@21426
    22
wenzelm@21426
    23
  load2:
wenzelm@61386
    24
  "dollar , quarter \<turnstile> loaded" and
wenzelm@21426
    25
wenzelm@21426
    26
  wash:
wenzelm@61386
    27
  "loaded , dirty \<turnstile> wet" and
wenzelm@21426
    28
wenzelm@21426
    29
  dry:
wenzelm@61386
    30
  "wet, quarter , quarter , quarter \<turnstile> clean"
wenzelm@21426
    31
wenzelm@21426
    32
wenzelm@21426
    33
(* "activate" definitions for use in proof *)
wenzelm@21426
    34
wenzelm@60770
    35
ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
wenzelm@60770
    36
ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
wenzelm@60770
    37
ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
wenzelm@60770
    38
ML \<open>ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}])))\<close>
wenzelm@21426
    39
wenzelm@21426
    40
(* a load of dirty clothes and two dollars gives you clean clothes *)
wenzelm@21426
    41
wenzelm@61386
    42
lemma "dollar , dollar , dirty \<turnstile> clean"
wenzelm@55232
    43
  by (best add!: changeI load1I washI dryI)
wenzelm@21426
    44
wenzelm@21426
    45
(* order of premises doesn't matter *)
wenzelm@21426
    46
wenzelm@61386
    47
lemma "dollar , dirty , dollar \<turnstile> clean"
wenzelm@55232
    48
  by (best add!: changeI load1I washI dryI)
wenzelm@21426
    49
wenzelm@21426
    50
(* alternative formulation *)
wenzelm@21426
    51
wenzelm@61386
    52
lemma "dollar , dollar \<turnstile> dirty -o clean"
wenzelm@55232
    53
  by (best add!: changeI load1I washI dryI)
wenzelm@21426
    54
wenzelm@21426
    55
end