Re: [isabelle] HOL quantifiers in intro rules



I would frown or all of these abbreviations. I see the point of relying on the implicit choice of a rule when you are making various attempts to find a proof. But once you find it, you should invest a little effort in making your proof comprehensible to others and more robust against changes, including the precise change to continuous_intros suggested here. At least “safe" and "clarify" are very controlled in what they do, but “rule” could do almost anything.

Larry Paulson


> On 20 Nov 2014, at 14:41, Joachim Breitner <breitner at kit.edu> wrote:
> 
> Hi,
> 
> 
> Am Donnerstag, den 20.11.2014, 14:46 +0100 schrieb Johannes Hölzl:
>> @Joachim: In your specific case you can also use intro:
>> 
>> lemma "closed (⋂K)"
>> proof (intro continuous_intros ballI)
>>  fix S assume "S : K" shows "closed S"
>>     ...
>> qed
> 
> or simply
> 
>        proof rule+
> 
> where I don’t have to find the lemma names.
> 
> 
> Am Donnerstag, den 20.11.2014, 15:30 +0100 schrieb Peter Lammich:
>> As Johannes already pointed out, you could use intro.
>> 
>> I usually use something like the following in those cases:
>>  proof rule safe
>>    fix S
>>    assume ...	
> 
> I guess you mean "proof (rule, safe)". That is even nicer, as in my case
> K is a "range f", so this gets resolved as well. Although this seems to
> be just a small step from
> 
>        proof auto
> 
> which I believe is frowned upon.
> 
> 
> 
> 
> Greetings,
> Joachim
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner





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