*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] export_code doesn't define Trueprop for False*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Mon, 02 Dec 2013 16:29:31 -0600*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5296FE01.9070304@informatik.tu-muenchen.de>*References*: <52904D0C.10201@gmx.com> <5296FE01.9070304@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 11/28/2013 2:25 AM, Florian Haftmann wrote:

the trick of the definition "holds == Trueprop True" and the related stuff is just used to allow the code generator (code_runtime.ML) to evaluate expressions of the form (P) "Trueprop _" and check whether they result in "Trueprop True" aka "holds" and then certify the result as theorem (P). It has no further significance. Maybe this answers you abundant questions.

It should produce something that looks like these: value "True" (* True::bool *) value "False" (* False::bool *) value "Trueprop True" (* (Trueprop True)::prop *) value "Trueprop False" (* (Trueprop False)::prop *) value "hNot(True)" (* (Trueprop False)::prop *) value "hNot(False)" (* (Trueprop True)::prop *)

Thanks, GB // Modification to get Scala "val" to work like Isar "value" object I_131123b_mod { abstract sealed class prop final case class trueprop(b: Boolean) extends prop def follows(p: prop, pa: prop): prop = (p, pa) match { case (p, trueprop(true)) => trueprop(true) case (trueprop(false), trueprop(false)) => trueprop(true) case (trueprop(true), trueprop(false)) => trueprop(false) } def hNot(p: prop): prop = follows(p, trueprop(false)) val x1 = true // x1: Boolean = true val x2 = false // x2: Boolean = false val x3 = trueprop(true) // x3: trueprop = trueprop(true) val x4 = trueprop(false) // x4: trueprop = trueprop(false) val x5 = hNot(trueprop(true)) // x5: prop = trueprop(false) val x6 = hNot(trueprop(false)) // x6: prop = trueprop(true) // HOL functions (bool => bool) are just Scala (Boolean => Boolean). def bNot(b: Boolean): Boolean = !b } /* object I_131123b */ theory i131123b__scala_val_should_match_isa_value imports Complex_Main begin definition hNot :: "prop => prop" where "hNot P == (PROP P ==> False)" notation hNot ("hNot _" [5] 5) value "True" (* True::bool *) value "False" (* False::bool *) value "Trueprop True" (* (Trueprop True)::prop *) value "Trueprop False" (* (Trueprop False)::prop *) value "hNot(True)" (* (Trueprop False)::prop *) value "hNot(False)" (* (Trueprop True)::prop *) theorem "hNot(False)" by(unfold hNot_def, simp) definition bNot :: "bool => bool" where "bNot b = (~b)" no_notation hNot ("hNot _" [5] 5)

end // ORIGINAL EXPORT object I_131123b { abstract sealed class prop final case class Holds() extends prop def trueprop(x0: Boolean): prop = x0 match { case true => Holds() } def follows(p: prop, pa: prop): prop = (p, pa) match { case (p, Holds()) => Holds() case (Holds(), p) => p } def bNot(b: Boolean): Boolean = ! b def hNot(p: prop): prop = follows(p, trueprop(false)) } /* object I_131123b */

- Previous by Date: Re: [isabelle] Line numbers vs. icons
- Next by Date: Re: [isabelle] Underscore vs Hyphen in Document Preparation
- Previous by Thread: Re: [isabelle] Error when Importing Theories from Library
- Next by Thread: [isabelle] LaTeXsygar (bug or feature?)
- Cl-isabelle-users December 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list