[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.