Quelle Washing.thy Sprache: Isabelle

(*  Title:      Sequents/Washing.thy
    Author:     Sara Kalvala
*)

theory Washing
imports ILL
begin

axiomatization
  dollar :: o and
  quarter :: o and
  loaded :: o and
  dirty :: o and
  wet :: o and
  clean :: o
where
  change:
  "dollar \ (quarter >< quarter >< quarter >< quarter)" and

  load1:
  "quarter , quarter , quarter , quarter , quarter \ loaded" and

  load2:
  "dollar , quarter \ loaded" and

  wash:
  "loaded , dirty \ wet" and

  dry:
  "wet, quarter , quarter , quarter \ clean"

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

ML \<open>ML_Thms.bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}])))\<close>
ML \<open>ML_Thms.bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}])))\<close>
ML \<open>ML_Thms.bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}])))\<close>
ML \<open>ML_Thms.bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}])))\<close>

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

lemma "dollar , dollar , dirty \ clean"
  by (best add!: changeI load1I washI dryI)

(* order of premises doesn't matter *)

lemma "dollar , dirty , dollar \ clean"
  by (best add!: changeI load1I washI dryI)

(* alternative formulation *)

lemma "dollar , dollar \ dirty -o clean"
  by (best add!: changeI load1I washI dryI)

end

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.