Re: [isabelle] Pairs and automation

Hi Christian,

You could prove split rules for your functions, similar to prod.splits:

lemma test_split:
  "!!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 MHonArc.