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

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] split_format (complete) for existential and universal quantifiers
*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
*Date*: Thu, 7 Mar 2013 09:29:40 +0100
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130221 Thunderbird/17.0.3

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"
sorry

`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)]
end

`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?
Andreas

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