Re: [isabelle] Parameterized Types?

Hi Robert,

On Tuesday 28 March 2006 14:28, Robert Lamar wrote:
> My only question for the moment arises from my attempt to prove a lemma,
> that the sum of two elements of a quotient is in the quotient.  I am unable
> to get past a certain step, which I isolate in the following lemma:
>   lemma "EX s. S = coset I s ==> EX s. S = {i + s | i. i \<in> I}"
>   proof -
>     assume "EX s. S = coset I s"
>     from this coset_def [of I s] show "EX s. S = {i + s | i. i \<in> I}"
>     by simp
>   qed
> I have defined
>   constdefs
>     coset ::  "[('a::ring) set, 'a] => 'a set"
>               "coset I a == {i + a | i. i \<in> I}"

The problem with this proof is caused by your usage of the "of" theorem 
attribute. Specifically, coset_def [of I s] instantiates coset_def with the 
free variables "I" and "s" (on my system Proof General renders these in 
blue), where the term you want to replace uses "s" as a bound variable 
(rendered in green). Replace this with coset_def [of I] and the proof works.

> and would like to think that it is a straightforward matter of
> substitution.  However, I know that section 5.11 of the tutorial makes it
> clear that reasoning about existential operators can be very tricky.  Am I
> missing something crucial?
> Robert Lamar

When you instantiate coset_def with free variables "I" and "s", you get an 
assumption that is too weak, since it only asserts the equality for a single 
value of "s". For simp to perform a substitution under a quantifier, on a 
term containing bound variables, the equality needs to hold for all possible 
values of the bound variables. Leaving a variable uninstantiated has the 
effect of a universal quantification over that variable, and simp is able to 
match it against a bound variable.

It appears that [of I] is still necessary to instantiate the free type 
variable in coset_def. Apparently, leaving a type variable uninstantiated 
does not have the same effect as an uninstantiated term variable, as far as 
simp is concerned; simp cannot match the types and it fails.

As a simpler alternative, you can give coset_def as an argument to simp or 
unfold, which avoids the problems with instantiating type variables:

lemma "EX s. S = coset I s ==> EX s. S = {i + s | i. i \<in> I}"
  proof -
    assume "EX s. S = coset I s"
    then show "EX s. S = {i + s | i. i \<in> I}"
    by (unfold coset_def)

- Brian

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