src/Sequents/ILL/washing.ML
author wenzelm
Sun, 18 Sep 2005 15:20:08 +0200
changeset 17481 75166ebb619b
parent 16415 d4e2f121e219
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16415
diff changeset
     1
(* $Id$ *)
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16415
diff changeset
     2
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     3
(* "activate" definitions for use in proof *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     4
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     5
val changeI = [context1] RL ([change] RLN (2,[cut]));
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     6
val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     7
val washI =   [context1] RL ([wash]   RLN (2,[cut]));
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     8
val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
     9
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    10
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    11
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    12
(* a load of dirty clothes and two dollars gives you clean clothes *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    13
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    14
Goal "dollar , dollar , dirty |- clean";
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    15
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    16
by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    17
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    18
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    19
(* order of premises doesn't matter *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    20
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16415
diff changeset
    21
prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    22
(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    23
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    24
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    25
(* alternative formulation *)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    26
17481
75166ebb619b converted to Isar theory format;
wenzelm
parents: 16415
diff changeset
    27
prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset
    28
(fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);