[isabelle-dev] Reviving an old thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?
Randy Pollack
rpollack at inf.ed.ac.uk
Wed Oct 12 19:24:28 CEST 2011
Hi Brian and Makarius,
I noticed something else unexpected about "arbitrary". If a variable
that is bound by a rule induction is (erroneously) made "arbitrary"
the "induct" method will make a fresh name for any occurrences not
bound by the induction, thereby splitting what the user probably meant
to be one thing into two things. Here is a stupid example, just to
make the observation clear:
inductive step:: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
s1: "n = m \<Longrightarrow> step n m"
lemma
assumes h:"step n m" "step n p"
shows "n = p"
using h
"proof (induct)" returns goal:
\<And>n m. \<lbrakk>n = m; step n p\<rbrakk> \<Longrightarrow> n = p
whereas "proof (induct arbitrary: n)" returns goal:
\<And>n m na. \<lbrakk>n = m; step na p\<rbrakk> \<Longrightarrow> na = p
The user expected the occurrences of "n" in both assumptions to be the
same variable, but "induct arbitrary: n" split them into two different
variables, and made the new variable arbitrary.
This raises two points. First, there might usefully be a warning
message for making "arbitrary" a variable that is bound by an
induction.
Second, how do we know the Isar behavior is logically sound? When a
user erroneously makes arbitrary a variable that is bound by an
induction, Isar returns a goal that is logically different from the
original goal. "arbitrary" is somewhat of a user-level
transformation; is it checked by the Isabelle kernel that the new goal
implies the original goal?
Best,
Randy
--
On Wed, Oct 12, 2011 at 10:01 AM, Makarius <makarius at sketis.net> wrote:
> On Wed, 12 Oct 2011, Brian Huffman wrote:
>
>> After implementing the warning, I dug through the revision history and
>> was surprised to find that my "new" feature actually used to exist! It
>> was removed in January 2006:
>>
>> http://isabelle.in.tum.de/repos/isabelle/rev/ca56111fe69c
>>
>> I don't understand why the warning message was ever removed. The
>> commit message "fix_tac: no warning" is unhelpful.
>
> This needs some further investigation. My log message from 2006 is an
> example of how not to do it -- just parroting the change without any
> explanation. (2006 was a bad year in Isabelle development.)
>
> Does your own change do anything different from the old version?
>
> BTW, that one was originating from here:
> http://isabelle.in.tum.de/repos/isabelle/rev/dfe5d09514eb
>
>
> Makarius
>
>
More information about the isabelle-dev
mailing list