[isabelle] difficulty with a tutorial example

I was working through a couple of the examples in the tutorial A Proof
Assistant for HigherOrder 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 ifthenelse expressions. A lemma shows that evaluating a
standard boolean expression is equivalent to evaluating its ifthenelse
form. Then the next part of the tutorial introduces normalization of
ifthenelse expressions which removes ifthenelse expressions in the
"if" part. The exercise here is to show that evaluating the normalized
ifthenelse epxression is equivalent to evaluating the original
ifthenelse 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.