Re: [isabelle] HOL quantifiers in intro rules



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

Attachment: signature.asc
Description: This is a digitally signed message part



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