src/Sequents/Washing.thy
author wenzelm
Sat, 13 Mar 2010 16:44:12 +0100
changeset 35762 af3ff2ba4c54
parent 26480 544cef16045b
child 39159 0dec18004e75
permissions -rw-r--r--
removed old CVS Ids; tuned headers;
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
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     9
consts
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    10
  dollar :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    11
  quarter :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    12
  loaded :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    13
  dirty :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    14
  wet :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    15
  clean :: o
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    16
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    17
axioms
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    18
  change:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    19
  "dollar |- (quarter >< quarter >< quarter >< quarter)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    20
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    21
  load1:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    22
  "quarter , quarter , quarter , quarter , quarter |- loaded"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    23
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    24
  load2:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    25
  "dollar , quarter |- loaded"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    26
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    27
  wash:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    28
  "loaded , dirty |- wet"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    29
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    30
  dry:
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    31
  "wet, quarter , quarter , quarter |- clean"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    32
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    33
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    34
(* "activate" definitions for use in proof *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    35
26480
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 21426
diff changeset
    36
ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 21426
diff changeset
    37
ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 21426
diff changeset
    38
ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
544cef16045b replaced 'ML_setup' by 'ML';
wenzelm
parents: 21426
diff changeset
    39
ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    40
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    41
(* a load of dirty clothes and two dollars gives you clean clothes *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    42
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    43
lemma "dollar , dollar , dirty |- clean"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    44
  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    45
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    46
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    47
(* order of premises doesn't matter *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    48
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    49
lemma "dollar , dirty , dollar |- clean"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    50
  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    51
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    52
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    53
(* alternative formulation *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    54
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    55
lemma "dollar , dollar |- dirty -o clean"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    56
  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    57
  done
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    58
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    59
end