[isabelle] Problem with congruence rule for unit type



Dear all,

I recently came across a strange problem with case expressions involving the unit type.
Trying to prove something like

  lemma "(case () of () => x) = x"

using "apply simp" causes the new goal

  "(case ?M' of () => x) = x"

with a schematic variable to be generated, while "apply auto" just diverges. This slightly odd
behaviour is caused by the rule old.unit.case_cong_weak, whose premise "?M = ?M'" is directly
simplified to "True", rather than proved by reflexivity, which would eliminate the variable ?M'.
Would it make sense to remove this rule from the simpset?
Of course, the above example has been simplified a little. I actually noticed this problem when trying
to provide case syntax for record types, whose "more" fields usually contain the unit element.

Greetings,
Stefan




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