[isabelle] difficulty with a tutorial example



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





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