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



Dear Isabelle users,

In the from-have paradigm, we can implicitly refer to the previous proved fact(s) using the “this” keyword. I was wondering if we can similarly refer to collected results implicitly in the moreover-ultimately paradigm? If not, would that be a good feature for future Isabelle?

Here is a minimal example:

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*)]

Many thanks,
Wenda



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