Re: [isabelle] Proving cardinality



Am 26/07/2012 04:13, schrieb Christian Sternagel:
> Dear John,
> 
> I can reproduce your problem but do not have an explanation. There is a thread
> about "using" in the mailing list archives:
> 
> 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-February/msg00019.html
> 
> which is interesting, but does not give an explanation for your case (since S is
> not polymorphic).
> 
> To make it easier for others to follow, here is the problem again:
> 
> definition S :: "nat set" where "S == {1, 2, 3}"
> lemma "card S > 1" by (auto simp: S_def) (*this works*)
> lemma "card S > 1" using S_def apply auto (*leaves the goal*)
> 1. S = {Suc 0, 2, 3} ⟹ Suc 0 < card S

This is the result of a simplifier heuristic: if it finds an equation "constant
= term" among the assumptions, it turns it around. Otherwise the following
frequently happens: an equation like "0 = x" is produced in the middle of
simplification and then 0 is replaced by x everywhere - not a good idea. The
heuristic does not apply to equation that are added to the simplifier explicitly.

Tobias

> cheers
> 
> chris
> 
> On 07/26/2012 10:06 AM, John Munroe wrote:
>> I gave it with 'using S_def'. Do you know why 'using S_def; by auto'
>> wouldn't work?
> 
>> On Thu, Jul 26, 2012 at 12:57 AM, Christian Sternagel  wrote:
>>> For me, by (auto simp: S_def) did the job. So how did you give S_def/ax1 as
>>> fact?
> 





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