Email Gateway (Aug 18 2022 at 09:46): Email Gateway (Aug 18 2022 at 09:46):From: Christopher L Conway <cconway@cs.nyu.edu>
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
Last updated: Nov 21 2024 at 12:39 UTC