[isabelle] Restrictions on instance claims



I decided it might be useful to have a class of non trivial types.

axclass
  non_trivial <= type
  non_trivial: "(? y. y ~= x)"

But it seems I can't handle cross product properly.

instance
  "*" :: (non_trivial, type) non_trivial
  apply (intro_classes)
  apply (auto simp add: trivial_false)
  done

works, but then

instance
  "*" :: (type, non_trivial) non_trivial

becomes an error.

Is there anyway around this?
If not, is the restriction well-placed in this case?

------------------------------------------------------------------
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.