[isabelle] export_code doesn't define Trueprop for False



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





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


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