[isabelle] Conditional interpretations?

Suppose I can prove

lemma f_locI: "p x ==> loc (f x)"

Is there any way to parley that into an interpretation?

Something like:

interpretation fl:
  assumes "p x"
  interprets loc ["f x"],

where fl.result is of the form "p x ==> R (f x)" for result (in loc) of the form "R y".

In a proof I can do

  assumes a1: "p x"
  shows "Q x"
proof -
  from f_locI [OF a1] interpret fl: loc ["f x"]

but the first form would be preferable.

Also, is there anyway the interpretation could leave its top goal as "loc (f x)"? Automatically applying the intro_classes analog is pretty annoying for locales (it might be more acceptable for axclasses!). It seems natural to me to do proofs about the locale predicate (sub-algebras, homomorphic images etc) and this convention makes unnecessarily awkward to use such results.

It would also be nice if the intro_locales method actually fully unwound all of the locale axioms for you, so that interpretation proofs were more like instance proofs.


Dr Brendan Mahony
Information Networks Division                   ph +61 8 8259 6046
Defence Science and Technology Organisation     fx +61 8 8259 5589
Edinburgh, South Australia      Brendan.Mahony at dsto.defence.gov.au

Important: This document remains the property of the Australian
Government Department of Defence and is subject to the jurisdiction
of the Crimes Act section 70. If you have received this document in
error, you are requested to contact the sender and delete the document.

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