[isabelle] Pairs and automation



Dear Isabelle-Wizards,

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"
apply(case_tac x)
apply(simp) 
done

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

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)
done

I toyed with definitions like

fun test2
where
  "test2 x = (let (a, b) = x in False)"

lemma "test2 x ==> P"
apply(simp)
done

But I am wondering whether there is some other magic that
lets my problem go away (automatically). Does anybody else
encountered this problem?

Best wishes,
Christian






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