[isabelle] Proving finiteness for inductive sets

Dear list,

for a current project of mine, I have to talk about the set of
subexpressions of a syntax tree and I need both the fact that this set
is finite and the individual introduction rules.

My first attempt, which can be seen at
was to define the set of subexpressions using the fun package. Showing
finiteness was easily done by induction. But proving the local rules I
need (e.g. lambdas1, lambdas2, app1, app2,... in that file) turned out
to be very inelegant, repetitive and ugly.

If I had defined the sets of subexpressions inductively, these rules
would be provided directly, but then the proof of finiteness is harder.
I worked on a general solution and the result so far can be seen at

The main result is

  84 lemma lfp_finite:
  85   assumes mono: "mono F"
  86       and finite: "finiteness_preserving F"
  87       and desc: "descending_functional p F"
  88   shows "finite (lfp F)"

where finiteness_preserving means that F S is finite if S already is and
descending_functional means that newly added elements are smaller than
previously added elements when measured with "p" (for which I later only
use the size function).

Here is an example application of the system. I define an inductive set
giving the tails of a list:

 194 inductive tails for l
 195   where "tails l l"
 196       | "tails l (x#xs) \<Longrightarrow> tails l xs"

 207 lemma "finite (tails l)"
 208 unfolding tails_def
 209 proof (induct rule: lfp_finite[of _ size, case_names mono finiteness desc])
 210 case mono show ?case by mono
 211 next
 212 case finiteness show ?case by (intro finiteness_preserving_lemmas, simp)
 213 next
 214 case desc show ?case
 215   by (rule, auto simp add: Bex_def mem_def fun_diff_def bool_diff_def)
 216 qed

For the proof of monotonicity, I copied the ML code from inductive.ML
into a custom method.

For the proof of finiteness preserving I wrote some intro rules breaking
down the functional generated by inductive_set and handling the types of
clauses I observed so far.

For the proof that the functional is descending I had to persuade
Isabelle not to be confused by sets vs. predicates, then it went through
easily (at least in this simple case).

So far so nice. For these kind of inductive sets, the result is quite
satisfying, and maybe can be useful for others as well.

Unfortunately, in my case, I need mutually recursive sets. Line 29 of
CPSUtils has "inductive_set lambdas' and calls' and values'"
demonstrating the issue, but a smaller example is at the end of

 296 inductive tails' and elems' for l
 297   where "tails' l l"
 298       | "tails' l (x#xs) \<Longrightarrow> tails' l xs"
 299       | "tails' l (x#xs) \<Longrightarrow> elems' l x"

The problem is that inducive_set generates a combined fixed point of
type "bool => 'a list => 'a => bool". This large set is then projected
onto "'a list => bool" or "'a => bool" by extracting those elements
where the boolean flag fits and where the “other” field is undefined.

I wrote a rule that converts such a fixed point to one with uncurried
arguments, i.e. "((bool \<times> 'a list) \<times> 'a) => bool" in
lfp_curry and the variant lfp_curryD which carries the monotonicity
requirement along. This way I end up at a fixed point where I can apply
lfp_finite. Unfortunately, these fixed points do not preserve
finiteness, as can be seen by this unsolvable goal:

	finiteness_preserving (λp x. ¬ fst (fst x) ∧ snd x = l)

This rule, which comes from the first equation about tails', adds all
triples where the first field is False and the last field is l (as
expected), but makes no statement about the second fields. I.e. this
rule adds one element per member of 'a! And naturally, this makes my
whole process fail.

The other rules share the same problem in that they do not specify all

I’m not sure how to proceed from here. A workaround would be to define a
combined set using Inl/Inr:

inductive tailselems for l
  where "tailselems l (Inl l)"
      | "tailselems l (Inl (x#xs)) ⟹ tailselems l (Inl xs)"
      | "tailselems l (Inl (x#xs)) ⟹ tailselems l (Inr x)"

But this would get quickly very unwieldy, especially as I need to
recursively define more than one set.

Another possible fix could involve changes to inducitve_set. Why not set
all invalid fields of the added members to undefined, and thus do not
add all those never-used elements? BTW, what is the reason not to use
Inl/Inr there in the first place?

Or is there maybe a completely different solution that I’m just not
seeing yet?

Thanks in advance,

Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part

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