search

moajohansson / IsaHipster

Theory Exploration for Isabelle using HipSpec
19 stars 3 forks source link

Isabelle equality = lost when translating back and forth with Haskell #2

Open Airini opened 9 years ago

Airini commented 9 years ago

Equality = is translated by Isabelle into Haskell as a new function definition equal_T (with T the type). HipSpec gets an additional function, obtaining corresponding properties. When brought back into the Isabelle theory, the symbol for equal_T is not defined and will stand for a free variable symbol in the lemmas obtained.

eg.: with the usual naturals Nat and

fun lez :: "Nat ⇒ bool" where
  "lez x = (x = Z)"

the call hipster lez returns (with equal_Nat a free variable) the refutable lemma

lemma unknown [thy_expl]: "equal_Nat x y = equal_Nat y x"
oops

See theory Examples/NatsBug.thy.

Airini commented 8 years ago

Not a problem for the purpose of researching automated theorem proving, but ultimately something to work on for usability with already existing Isabelle/HOL theories.