Re: [isabelle] Substitute in the whole context



On 18/07/2014 13:02, Joachim Breitner wrote:
> Hi,
> 
> I often see this pattern:
> 
> I am in some isar context:
> 
> case (CaseName a b c d)
> 
> and one of the first few facts is finding out something about d:
> 
> from CaseName(..) obtain e f where "d = (e,f)" <proof>

Here is a naive approximantion of what you want:

                     where [simp]: "d = (e,f)" <proof>

Tobias


> and from now on, I would like to forget d, but I still have to unfold it in
> local facts and goals:
> 
> from CaseName(3)[unfolded `d = _`] have "..." <proof> ... finally show
> ?case unfolding d <proof>
> 
> Is there some better way of handling this, where after I have shown "d = 
> (e,f)" I don’t have to worry about d any more?
> 
> I can imagine a command
> 
> subst_in_context `d = (e,f)`
> 
> which unfolds d in all local facts and all goals, while retaining their 
> names (CaseName(2)) etc. until the next "next" or "qed". Would that be
> desirable? Would it be technical possible?
> 
> Thanks, Joachim
> 




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