*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Parameterized Types?*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Wed, 29 Mar 2006 11:04:24 -0800*In-reply-to*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E2B@beta.ad.stetson.edu>*References*: <16530916C2FEF64EBE4C333390E3BEFC04FB5E2B@beta.ad.stetson.edu>*User-agent*: KMail/1.8

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) qed - Brian

**References**:**Re: [isabelle] Parameterized Types?***From:*Robert Lamar

- Previous by Date: Re: [isabelle] Featherweight Java formalization in Isabelle?
- Next by Date: Re: [isabelle] Parameterized Types?
- Previous by Thread: Re: [isabelle] Parameterized Types?
- Next by Thread: Re: [isabelle] Parameterized Types?
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list