# [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
lemma
assumes a1: "p x"
shows "Q x"
proof -
from f_locI [OF a1] interpret fl: loc ["f x"]
...
qed
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.
`
Brendan
------------------------------------------------------------------
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.*