Re: [isabelle] obtains and is-bindings



Dear all,

I ran into an issue related to one that was reported on this list before
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-November/msg00002.html,
by Andreas Lochbihler) but didn't get answered back then.

Is there a way of abbreviating, with '(is "<abbrev-pattern>")', terms in
a statement involving 'obtain … where "<term>"' or 'obtains … where
"<term>"' such that the abbreviations are usable in the proof of the
statement?  Or, if there is no such way, is there are particular reason
for why this is not possible?

I encountered this in a lemma roughly structured as follows:

lemma
  assumes …
  obtains thing where "prop1 thing" (* actually a lengthy expression *)
      and "prop2 thing"
proof -
  from assms obtain thing
    where "prop1 thing"
      and "prop2 thing"
    … (* proof *)
  then show ?thesis ..
qed

I would have liked to abbreviate this to, e.g.,

lemma
  assumes …
  obtains thing where "prop1 thing" (is "?prop1")
      and "prop2 thing" (is "?prop2")
proof -
  from assms obtain thing
    where "?prop1"
      and "?prop2"
    … (* proof *)
  then show ?thesis ..
qed

Cheers, and thanks in advance for any help,

Christoph

-- 
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
  Early registration deadline 23 June; http://cicm-conference.org/2013/
→ Knowledge and Experience Management, 7-9 October, Bamberg, Germany.
  Submission until 1 July; http://minf.uni-bamberg.de/lwa2013/cfp/fgwm/
→ Modular Ontologies (WoMO), 15 September, Corunna, Spain.
  Submission until 5 July; http://www.iaoa.org/womo/2013.html




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