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



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.

Exposure to tricks can still result in light-bulb moments. It's more clear to me now that an expression like`value "!!P. PROP P"` and `value "Trueprop False"` never get simplified to some meta-logic false constant. I take that as meaning there is no meta-logic false that's been defined. If there is, maybe someone will tell me where it is.

I guess no one but me cares about exporting functions of type "prop => prop" and "prop => prop => prop".

I decided that Scala "val" should mimic Isar "value" with functions based on type prop.

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 *)

In the exported code, I changed "trueprop" from a function to a datatype and got rid of "Holds". Until the day I can figure out how to export "!!P. PROP P", or "(op ==>) == (op &&&)", I don't see a need for it, but I could be wrong.

Based on my limited knowledge, I think the modified "trueprop" and "follows" should work as a drop-in replacement for any exported functions of type "prop => prop => 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)
export_code hNot bNot Not in Scala module_name "I_131123b" file "i131123b.scala"

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 */








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