*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Proving finiteness for inductive sets*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Thu, 07 Oct 2010 16:57:54 +0200*Sender*: Joachim Breitner <msg at 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 -- 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**

- Previous by Date: Re: [isabelle] G.U.T.
- Next by Date: Re: [isabelle] Finite set datatype?
- Previous by Thread: [isabelle] Fwd: Re: G.U.T.
- Next by Thread: [isabelle] Research Associate. DYVERSE: A New Kind of Control for Hybrid Systems
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list