Email Gateway (Aug 22 2022 at 13:02): Email Gateway (Aug 22 2022 at 13:02):From: n s <nedsri1988@gmail.com>
-
I was working through a couple of the examples in the tutorial A Proof
Assistant for Higher-Order Logic 2015, particularly 2.5.6 Case Study:
Boolean Expressions and ran into a problem. Without repeating the entire
contents of that section, the case study introduces a type definition
for boolean expressions, and a way of evaluating them in the usual
manner. Then it introduces a more efficient representation of boolean
expressions as if-then-else expressions. A lemma shows that evaluating a
standard boolean expression is equivalent to evaluating its if-then-else
form. Then the next part of the tutorial introduces normalization of
if-then-else expressions which removes if-then-else expressions in the
"if" part. The exercise here is to show that evaluating the normalized
if-then-else epxression is equivalent to evaluating the original
if-then-else expression.
Trying
theorem "valif (norm b) env = valif b env"
apply (induct_tac b)
apply (auto)
leaves 8 subgoals.
The tutorial says that the proof is canonical, provided we first show
the following simplification lemma, which also helps to understand what
normif does:
lemma [simp]:
"∀t e. valif (normif b t e) env = valif (IF b t e) env"
Isabelle is able to prove the lemma, but unfortunately it appears to
have no impact on the proof of the theorem, which is still stuck with 8
subgoals. I am able to prove the theorem by hand using structural
induction, applying the theorem to the subparts t and e. Any ideas why
its stuck?
thanks!
(I am running Isabelle 2015)
Email Gateway (Aug 22 2022 at 13:02):From: Corey Richardson <corey@octayn.net>
You may find it useful to compare your theory to the theory the tutorial is
generated from. This is present in
$ISABELLE_HOME/src/Doc/Tutorial/Ifexpr/Ifexpr.thy
signature.asc
Last updated: Apr 25 2024 at 12:23 UTC