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



Code generation has been an excellent tutor. Seeing "data prop Holds" by the code generator has drove home a simple idea, that I can never make a false statement at the prop level of logic. Sounds simple, but until now, I've always consider true and false to both be available to me.

However, my "hnot(false)" doesn't attempt to make a false statement. It makes the statement "False ==> False", which is true, and so it shouldn't throw an exception.

I don't know if this is good enough for the future, but for the moment, I made "trueprop" part of the "prop" data type, and defined "follows" so that an exception is thrown there when a false meta-implication is attempted.

The Scala objects below, "HOL2" and "HOL" are a combination of the Scala objects that were exported for the source in my last email. "HOL2" is my modification.

If one says, "Is not an exception thrown semantically equivalent to a meta-logic false?" I reply, "I know nothing about semantics or predicates. Those computer scientists, that is what they talk about, but me, I know nothing about semantics or predicates."

Regards,
GB


// FIXED FOR NOW, MAYBE.
object HOL2 {
  sealed abstract class prop
  final case class      Holds() extends prop
  final case class      trueprop(x0: Boolean) extends prop

  // ECLIPSE WARNING: match may not be exhaustive. It would fail on the
  // following input:
  //   (trueprop(true), trueprop(false))
  // Dude, exactly, it's impossible to make a false statement at the prop
  // level of logic. Exceptions are acceptable, but meta-logic false is
  // semantically offensive to those in the know.
  def follows(p: prop, pa: prop): prop = (p, pa) match {
    case (p, Holds()) => Holds()
    case (Holds(), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(true)) => Holds()
    case (trueprop(true), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(false)) => Holds()
  }

  def hnot(p: prop): prop = follows(p, trueprop(false))

  // Return value of Holds(). It's legit, is it not?
  val x = hnot(trueprop(false))

  // No error. Simple assignment. I'm not making any logical claim.
  val y = trueprop(false)

// Throws exception. Not because or "trueprop", but because of "follows".
  // That's what I want for now. Concerning the future, maybe not.
  val z = hnot(trueprop(true))
}


// ORIGINAL: THROWS EXCEPTION FOR A LEGIT STATEMENT.
object HOL {
    sealed abstract 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 hnot(p: prop): prop = follows(p, trueprop(false))

// Throws exception. This is not where it should throw the exception, because
  // hnot(false) should be an acceptable statement.
  val x = trueprop(false)
}

// FIXED FOR NOW, MAYBE.
object HOL2 {
  sealed abstract class prop
  final case class      Holds() extends prop
  final case class      trueprop(x0: Boolean) extends prop
  
  // ECLIPSE WARNING: match may not be exhaustive. It would fail on the  
  // following input: 
  //   (trueprop(true), trueprop(false))
  // Dude, exactly, it's impossible to make a false statement at the prop
  // level of logic. Exceptions are acceptable, but meta-logic false is 
  // semantically offensive to those in the know.
  def follows(p: prop, pa: prop): prop = (p, pa) match {
    case (p, Holds()) => Holds()
    case (Holds(), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(true)) => Holds()
    case (trueprop(true), trueprop(true)) => Holds()
    case (trueprop(false), trueprop(false)) => Holds()
  } 
    
  def hnot(p: prop): prop = follows(p, trueprop(false))
                                                  
  // Return value of Holds(). It's legit, is it not?
  val x = hnot(trueprop(false))
  
  // No error. Simple assignment. I'm not making any logical claim.
  val y = trueprop(false)
  
  // Throws exception. Not because or "trueprop", but because of "follows". 
  // That's what I want for now. Concerning the future, maybe not.
  val z = hnot(trueprop(true))
}


// ORIGINAL: THROWS EXCEPTION FOR A LEGIT STATEMENT.
object HOL {
	sealed abstract 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 hnot(p: prop): prop = follows(p, trueprop(false))
  
  // Throws exception. This is not where it should throw the exception, because
  // hnot(false) should be an acceptable statement.
  val x = trueprop(false)
}



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