wneuper/isa: src/Sequents/Washing.thy@91c4d7397f0e

     1 (*  Title:      Sequents/Washing.thy

     2     Author:     Sara Kalvala

     3 *)

     5 theory Washing

     6 imports ILL

     7 begin

     9 consts

    10   dollar :: o

    11   quarter :: o

    12   loaded :: o

    13   dirty :: o

    14   wet :: o

    15   clean :: o

    17 axioms

    18   change:

    19   "dollar |- (quarter >< quarter >< quarter >< quarter)"

    21   load1:

    22   "quarter , quarter , quarter , quarter , quarter |- loaded"

    24   load2:

    25   "dollar , quarter |- loaded"

    27   wash:

    28   "loaded , dirty |- wet"

    30   dry:

    31   "wet, quarter , quarter , quarter |- clean"

    34 (* "activate" definitions for use in proof *)

    36 ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}

    37 ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}

    38 ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}

    39 ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}

    41 (* a load of dirty clothes and two dollars gives you clean clothes *)

    43 lemma "dollar , dollar , dirty |- clean"

    44   apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})

    45   done

    47 (* order of premises doesn't matter *)

    49 lemma "dollar , dirty , dollar |- clean"

    50   apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})

    51   done

    53 (* alternative formulation *)

    55 lemma "dollar , dollar |- dirty -o clean"

    56   apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})

    57   done

    59 end

author	wenzelm
	Thu, 07 Jul 2011 23:55:15 +0200
changeset 44572	91c4d7397f0e
parent 39406	0dec18004e75
child 52446	473303ef6e34
permissions	-rw-r--r--