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