Re: [isabelle] export_code doesn't define Trueprop for False



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.