*To*: Gottfried Barrow <gottfried.barrow at gmx.com>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] export_code doesn't define Trueprop for False*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 28 Nov 2013 09:25:37 +0100*In-reply-to*: <52904D0C.10201@gmx.com>*Organization*: TU Munich*References*: <52904D0C.10201@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

Hi Gottfried, 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. Cheers, Florian Am 23.11.2013 07:37, schrieb Gottfried Barrow: > Hi, > > This is the result of my making comparisons between Scala and Haskell. > I'd like to generate a little code for whatever I'm doing, and messing > around with the meta-logic is something I eventually want to do. It > could be I'm doing things which aren't intended to be done. > > I start with a hybrid version of "not" named "Hnot", (PROP P ==> False), > and I export it. > > definition MFalse :: "prop" ("MFalse") where "MFalse == (!!P. PROP P)" > definition Hnot :: "prop => prop" where "Hnot P == (PROP P ==> False)" > value "Hnot(Trueprop False)" > export_code Hnot in Scala file "i131123a.scala" > export_code Hnot in Haskell file "." > > I actually wanted to use "(PROP P ==> MFalse)", but MFalse uses "!!", so > I get the export_code error message "No code equations for all". > > QUESTION: Are there some magic code equations for "all", or is this a > fundamental limitation? > > Starting here, I make some comments about the Haskell code, since it's > almost like reading the Isar. > > From the generated code, HOL "prop" is converted to a data type "Prop", > which has only one value, "Holds". > > data Prop = Holds; > > I guess it makes sense that "Prop" can only be true, but consequently, > it makes the use of variables in "follows", the meta-implication, rather > meaningless: > > follows :: Prop -> Prop -> Prop; > follows p Holds = Holds; > follows Holds p = p; > > I set that aside because the use of HOL is the main objective for most > people. This brings us to "trueprop", which is the code for "Trueprop". > > trueprop :: Bool -> Prop; > trueprop True = Holds; > > This shows that "trueprop" is only defined for "true". I set that aside, > as a solitary issue, and talk about "hnot", which seems like it should > be a valid function: > > hnot :: HOL.Prop -> HOL.Prop; > hnot p = HOL.follows p (HOL.trueprop False); > > Here, I've reached the limits of knowing what the limits of code > generation is supposed to be, when it comes to the meta-logic. > > In Isabelle I can do this, and I get a value of True: > > value "Hnot(Trueprop False)" > > I'm actually using the Scala code to test the functions in simple ways, > and I can't do that. The function "trueprop" is not defined for "false", > so both "trueprop" and "hnot" throw an exception. > > This is kind of contrary to the following four statements in HOL.thy, > where, by necessity, Trueprop is defined for both True and False: > > typedecl bool > Trueprop :: "bool => prop" > consts > True :: bool > False :: bool > > As I said, it could be that none of this was intended to be used like this. > > Thanks, > GB > > > theory i131123a > imports Complex_Main > begin > > definition MFalse :: "prop" ("MFalse") where > "MFalse == (!!P. PROP P)" > > definition Hnot_try :: "prop => prop" where > "Hnot_try P == (PROP P ==> MFalse)" > export_code Hnot_try in Scala file "i131123a.scala" > (*ERROR: No code equations for all*) > > definition Hnot :: "prop => prop" where > "Hnot P == (PROP P ==> False)" > > value "Hnot(Trueprop False)" > > export_code Hnot in Scala file "i131123a.scala" > export_code Hnot in Haskell file "." > > end > > > > > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**References**:**[isabelle] export_code doesn't define Trueprop for False***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] HOL/Library/Polynomial pcompose
- Next by Date: Re: [isabelle] Code generator forgets to rename type variables for constants with code_abort
- Previous by Thread: Re: [isabelle] export_code doesn't define Trueprop for False
- Next by Thread: [isabelle] Fwd: First Call for Papers: Conf. Intelligent Computer Mathematics (CICM 2014)
- Cl-isabelle-users November 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