Re: [isabelle] Pairs and automation
You could prove split rules for your functions, similar to prod.splits:
"!!x. P (test x) = (!a b. x = (a, b) --> P (test (a, b)))"
"!!x. P (test x) = (~ (∃a b. x = (a, b) & ~ P (test (a, b))))"
by(simp_all add: split_paired_all)
lemma "test x ==> P"
apply(simp split: test_split)
But these split rules are aggressive, they split the parameter for every
occurrence of test. And they make the simplifier loop if the rhs
occurrence of test does not get simplified away (there's less danger if
you replace the "test (a, b)" on the rhs with the rhs of the function
definition, but then the theorems are less canoncial). Fortunately, the
simplifier tries split rules after applying its simplification steps, so
this should normally work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and