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



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.