Re: [isabelle] some problems with the /\ quantifier


> after which the goal is
>   goal (1 subgoal):
>    1. â z. w = real_of_int z ==> P w
> so, the only thing left is to substitute w and z in tl1 :
>       apply (rule tl1 [of w z])
> but this doesn't work as I expected, and I get a new goal with a new
> variable za.

the clue lies in the highlighting of the variable 'z': it has a
yellow-ish background. In a proof, this denotes a free variable which
doesn't occur in the statement and hasn't been fixed in any other way.
In your example, it decidedly does not refer to the 'z' bound by the
quantifier. This isn't a problem with the quantifier, but an effect of
how bound variables are treated in Isabelle.

There are two ways to solve your problem:

1. Don't instantiate.

     apply (rule tl1)
     apply assumption

   This will solve your goal just fine. There are no ambiguities at
   all in how the variables should be instantiated here.

2. Use 'rule_tac'.

     apply (rule_tac y=z in tl1)
     apply assumption

   Here, the 'z' refers to the bound variable, which is why it is
   coloured red. The ability to refer to bound variable is a specialty
   of 'rule_tac' and not available to all methods or attributes.

In general, I strongly recommend against the use of 'rule_tac' together
with explicit instantiations talking about bound variables (unless it is
temporary and pending refactoring). (Imagine a huge red warning sign
popping up when you use it.) The reason is quite simple: Bound variable
names are usually system-generated and thus sometimes unpredictable.
Your proof will break when you have another variable called 'z', someone
renames the 'z' in 'Int_cases', ...

Here is how I would write the proof:

  from assms obtain z where "w = real_of_int z"
    by (auto elim: Ints_cases)
  thus "P(w)"
    by (rule tl1)

The 'z' above is written down explicitly and much more robust and you
will find that explicit instantiation using 'of' works as expected.


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