[isabelle] Pairs and automation
I have a theory where I need to define functions
over tuples, say this contrived one
fun test where
"test (a, b) = False"
Now I like to prove lemmas like
lemma "test x ==> P"
As can be seen this can be proved, but needs the explicit
case_tac in order to make Isabelle aware the x is in fact
Is there a way I can make Isabelle figure this out automatically?
If I had a !!-quantifier around x, then this seems
to do the job:
lemma "!!x. test x ==> P"
apply(simp add: split_paired_all)
I toyed with definitions like
"test2 x = (let (a, b) = x in False)"
lemma "test2 x ==> P"
But I am wondering whether there is some other magic that
lets my problem go away (automatically). Does anybody else
encountered this problem?
This archive was generated by a fusion of
Pipermail (Mailman edition) and