src/Sequents/Washing.thy
author haftmann
Thu, 23 Nov 2017 17:03:27 +0000
changeset 67087 733017b19de9
parent 61386 0a29a984a91b
permissions -rw-r--r--
generalized more lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 26480
diff changeset
     1
(*  Title:      Sequents/Washing.thy
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 26480
diff changeset
     2
    Author:     Sara Kalvala
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 26480
diff changeset
     3
*)
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     4
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     5
theory Washing
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     6
imports ILL
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     7
begin
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     8
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
     9
axiomatization
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    10
  dollar :: o and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    11
  quarter :: o and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    12
  loaded :: o and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    13
  dirty :: o and
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    14
  wet :: o and
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    15
  clean :: o
51309
473303ef6e34 eliminated legacy 'axioms';
wenzelm
parents: 39159
diff changeset
    16
where
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    17
  change:
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    18
  "dollar \<turnstile> (quarter >< quarter >< quarter >< quarter)" and
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    19
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    20
  load1:
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    21
  "quarter , quarter , quarter , quarter , quarter \<turnstile> loaded" and
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    22
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    23
  load2:
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    24
  "dollar , quarter \<turnstile> loaded" and
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    25
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    26
  wash:
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    27
  "loaded , dirty \<turnstile> wet" and
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    28
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    29
  dry:
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    30
  "wet, quarter , quarter , quarter \<turnstile> clean"
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    31
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    32
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    33
(* "activate" definitions for use in proof *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    34
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 56199
diff changeset
    35
ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 56199
diff changeset
    36
ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 56199
diff changeset
    37
ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 56199
diff changeset
    38
ML \<open>ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}])))\<close>
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    39
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    40
(* a load of dirty clothes and two dollars gives you clean clothes *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    41
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    42
lemma "dollar , dollar , dirty \<turnstile> clean"
55232
7a46672934a3 lazy_pack is default context for ILL;
wenzelm
parents: 55228
diff changeset
    43
  by (best add!: changeI load1I washI dryI)
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    44
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    45
(* order of premises doesn't matter *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    46
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    47
lemma "dollar , dirty , dollar \<turnstile> clean"
55232
7a46672934a3 lazy_pack is default context for ILL;
wenzelm
parents: 55228
diff changeset
    48
  by (best add!: changeI load1I washI dryI)
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    49
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    50
(* alternative formulation *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    51
61386
0a29a984a91b more symbols;
wenzelm
parents: 60770
diff changeset
    52
lemma "dollar , dollar \<turnstile> dirty -o clean"
55232
7a46672934a3 lazy_pack is default context for ILL;
wenzelm
parents: 55228
diff changeset
    53
  by (best add!: changeI load1I washI dryI)
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    54
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    55
end