Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm



On 20/03/18 13:40, Wenda Li wrote:
>>> fix A B D::bool
>>>   assume foo:"A ⟹ B ⟹ D" 
>>>
>>>   have "A" sorry
>>>   moreover have "B" sorry
>>>   ultimately have "D"
>>>     using foo
> 
> My main motivation for this is that when “A” and “B” are complex, we may want to perform some manual forward reasoning in the “ultimately” step, rather than solely relying on automatic tactics. Explicit naming “A” and “B” will do the job, but it seems a little unnatural and unnecessary. 

Naming facts that are referenced later in a non-local / non-linear
manner is the normal way in the Isar proof language. In practice about
5-10% of facts mightr require explicit names.

I don't see anything unnatural or unnecessary about it. On the contrary
too much implicit fact management can make Isar proofs hard to read and
hard to maintain, also hard to explain to casual readers who are not
familiar with the language.


	Makarius





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