Email Gateway (Aug 18 2022 at 16:11): Email Gateway (Aug 18 2022 at 16:11):From: Joachim Breitner <mail@joachim-breitner.de>
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
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/CPSUtils.thy;h=b76dbbe68a4002b277fc7abbe930d235ff5cc85b;hb=df00ade5a418f1666624f8334ea253accf05d1c1
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
http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/Finite_Inductive_Set.thy;h=23bc9d27951e270342404b546546ccb77caf303c;hb=df00ade5a418f1666624f8334ea253accf05d1c1
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
Finite_Inductive_Set.thy:
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
fields.
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
signature.asc
Last updated: Apr 26 2024 at 12:28 UTC