[isabelle] split_format (complete) for existential and universal quantifiers

Dear all,

I use coinduction rules of the format as in the following example:

typedecl foo
consts unfoo :: "foo => foo"

lemma foo_coinduct[consumes 1, case_names foo]:
  fixes f g :: "'a => foo"
  assumes "P x"
  "!!x. P x ==>
    (EX x'. unfoo (f x) = f x' & unfoo (g x) = g x' & P x')
    | unfoo (f x) = unfoo (g x)"
  shows "f x = g x"

With the rule, I show equality of two functions are equal on some set specified by the coinduction invariant predicate P. The second premise expresses that P is actually an invariant under the destructors.

Frequently, the functions f and g depend on multiple parameters. To that end, I derive from foo_coinduct one rule where x is split into two parameters. I found that split_format (complete) almost does that:

lemmas foo_coinduct2 =
  foo_coinduct[where x="(a, b)", split_format (complete)]

[| P a b;
   !!a b. P a b
   ==> (EX x'. unfoo (f a b) = (case x' of (x, xa) => f x xa) &
               unfoo (g a b) = (case x' of (x, xa) => g x xa) &
               (case x' of (x, xa) => P x xa))
       | unfoo (f a b) = unfoo (g a b) |]
    ==> f a b = g a b

The ugly thing about this are the "case x' of (x, xa) =>" bits. If split_format (complete) would split the EX quantifier, too, they would be gone. Of course, I can so do manually as follows, but this looses the consumes and case_names declarations:

lemmas foo_coinduct2 =
  foo_coinduct[where x="(a, b)", split_format (complete),
               unfolded split_paired_Ex prod.cases]

Are there better ways to achieve my goal? Would it be sensible to extend split_format such that it also splits EX and ALL quantifiers if needed? These ugly case splits for EX and ALL happen also when there is free uncurried function variable as in

notepad begin
  { fix f :: "('a * 'b) => bool"
    have "EX x. f x" sorry }
  thm this[split_format (complete)]

If there is consent that EX and ALL should also be split, I could try to adapt split_format accordingly. A quick grep across the distribution and the AFP shows that split_format (complete) is so far only used for a few induction rules.

Any opinions?


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