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



Dear Peter,

>  have "A" sorry
>   moreover have "B" sorry
>   moreover have "D" using foo[OF calculation] .

Thanks for your quick reply. This is indeed one solution, despite of the slightly misleading syntax :-)

>> 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. 

Best,
Wenda

> On 19 Mar 2018, at 14:43, Peter Lammich <lammich at in.tum.de> wrote:
> 
> Hi Wenda,
> 
> there is "calculation", but it seems to be removed by ultimately ...
> 
> 
> notepad 
> begin
>   fix A B D::bool
>   assume foo:"A ⟹ B ⟹ D" 
> 
>   have "A" "B" sorry
>   from foo[OF this(1) this(2)] (*here, we can implicitly refer to the
> previous facts 
>                                     using the "this" keyword*)
>   have "D" .
> 
>   have "A" sorry
>   moreover have "B" sorry
>   moreover have "D" using foo[OF calculation] .
>   
> ^^ not very nice though to end a proof with moreover ...
> 
> --
>   Peter
> 
> 
> 
> 
> On Mo, 2018-03-19 at 14:08 +0000, Wenda Li wrote:
>> notepad 
>> begin
>>   fix A B D::bool
>>   assume foo:"A ⟹ B ⟹ D" 
>> 
>>   have "A" "B" sorry
>>   from foo[OF this(1) this(2)] (*here, we can implicitly refer to the
>> previous facts 
>>                                     using the "this" keyword*)
>>   have "D" .
>> 
>>   have "A" sorry
>>   moreover have "B" sorry
>>   ultimately have "D"
>>     using foo[OF (*I wish to implicitly refer to A and B here, 
>>                     like using the "this" keyword previously*)]





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