# [isabelle] scope of quantifiers

```I'm working through the Isabelle tutorial and I'm a little mystified by
some behavior I'm seeing in my solution to Exercise 3.4.1.
Preliminaries: a and b are values of a two mutually recursive datatype
representing, respectively, arithmetic and boolean expressions; norma
and normif are mutually recursive normalization functions over those
datatypes; "evala expr env" does what one would expect. (Full source
code is included below.)

The following proof goes through with no problem:

lemma [simp]:
"evala (norma a) env = evala a env &
(! t e . evala (normif b t e) env = evala (IF b t e) env )"
apply (induct_tac a and b, simp_all)
done

The following proof fails with:
*** empty result sequence -- proof command failed
*** At command "apply".

lemma [simp]:
"! t e . (evala (norma a) env = evala a env &
evala (normif b t e) env = evala (IF b t e) env)"
apply (induct_tac a and b, simp_all)
done

Note the only difference between the two is the scope of the quantifier.
Also note that t and e do not appear free in the first line. What's
going on here?

Thanks,
Chris

Source code:

theory Expr
imports Main
begin

datatype 'a aexp =
IF "'a bexp" "'a aexp" "'a aexp"
| Sum "'a aexp" "'a aexp"
| Diff "'a aexp" "'a aexp"
| Var 'a
| Num nat
and 'a bexp =
Less "'a aexp" "'a aexp"
| And "'a bexp" "'a bexp"
| Neg "'a bexp"

consts
evala :: "'a aexp => ('a => nat) => nat"
evalb :: "'a bexp => ('a => nat) => bool"

primrec
"evala (IF b a1 a2) env =
(if evalb b env then evala a1 env else evala a2 env)"
"evala (Sum a1 a2) env = evala a1 env + evala a2 env"
"evala (Diff a1 a2) env = evala a1 env - evala a2 env"
"evala (Var v) env = env v"
"evala (Num n) env = n"

"evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
"evalb (And b1 b2) env = (evalb b1 env & evalb b2 env)"
"evalb (Neg b) env = (~evalb b env)"

consts
norma :: "'a aexp => 'a aexp"
normif :: "'a bexp ^ 'a aexp ^ 'a aexp ^ 'a aexp"

primrec
"norma (IF b a1 a2) = normif b (norma a1) (norma a2)"
"norma (Sum a1 a2)  = Sum (norma a1) (norma a2)"
"norma (Diff a1 a2) = Diff (norma a1) (norma a2)"
"norma (Var v) = Var v"
"norma (Num n) = Num n"

"normif (Less a1 a2) t e = IF (Less (norma a1) (norma a2)) t e"
"normif (And b1 b2) t e = normif b1 (normif b2 t e) e"
"normif (Neg b) t e = normif b e t"

done

```

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