*To*: Tambet <qtvali at gmail.com>*Subject*: Re: [isabelle] One more case about induction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 26 Jul 2010 10:02:33 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTins0Oe2c0hqJftktVnhuOh6gPW_PVJJvVkNjVfN@mail.gmail.com>*References*: <AANLkTins0Oe2c0hqJftktVnhuOh6gPW_PVJJvVkNjVfN@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20100302)

Tambet wrote: > I'm still stuck with inductive proofs. I did seek manuals of inductive > functions, searched Google about induction etc., but they all seem to lack > something. > > Case 1: > (* If someone would hint, how to make this a subclass of nat so that lemmas > about nat would be used and I could use it in fix part of lemmas, it would > be nice *) > definition cnat :: "nat => bool" where "cnat n = (0 < n)" > > (* This one is already proven - thanks to Lawrence and Rafal *) > lemma cn_is_cnat: "cnat n ==> cnat (cn n)" > > (* This defines the following function - an ordered list, which will go to > infinite cycle at end. This would be nice to have a constructor for list, > which contains those elements, but currently this basic syntax should be > enough? *) > inductive cf :: "nat => nat => bool" where > cnf[intro!]: > "cnat n ==> cf (cn n) n" | > cff[intro!]: > "cf m n ==> cf (cn m) n" > > (* This follows directly from cf_def and cn_is_cnat. *) > lemma cf_is_cnat: "cnat n ==> cf m n ==> cnat m" lemma cf_is_cnat: "cf m n ==> n>0 ==> m>0" apply(induct rule: cf.induct) apply (metis cn_is_cnat) by (metis cn_is_cnat) You can easily turn into a structured proof. I have eliminated cnat - I don't see the point of it. More importantly, your whole approach is overly complicated. You want to iterate function cn. Well, simply use function iteration: (cn^^k)(n) is the result of the k-fold application of cn to n. See compower in theory Nat.thy. Tobias > I did try strategies described in > http://www.mkm-ig.org/meetings/mkm06/Presentations/Wenzel.pdf > > For example, this: > lemma cf_is_cnat: > assumes "cnat n" > assumes f: "cf m n" > shows "cnat m" > using f > proof (induct n fixing: m) > > I would read it as that if I fix m, then I can prove general statements, > which hold for any m. Then I could have case with cnf followed by case with > cff and it would be proven. > > Anyway, what I get is that I actually could not fix m: > *** method "HOL.induct": bad arguments > *** : m > *** At command "proof". > > lemma cf_is_cnat: > assumes "cnat n" > assumes "cf m n" > shows "cnat m" > proof - > fix x > show "cf (cn x) x ==> cnat (cn x)" > *** Local statement will fail to refine any pending goal > *** Failed attempt to solve goal by exported rule: > *** cf (cn (?x2::nat)) ?x2 ==> cnat (cn ?x2) > *** At command "show". > > Now, how could I extract the cases of definition - first case > (non-inductive) is the case "cf (cn x) x"; second case is the inductive case > "cf (cn y) x", where y is resulting "cn ?" from first or second case. It > should be proven if I show that first case gives me number with property > cnat and inductive case gives me number with property cnat if it's given > number with property cnat. > > Anyway, I am unable to close such circle. I am unable to define that these > are the cases and all cases. > > This is the pattern from isar-overview I also tried: > lemma cf_is_cnat: > assumes "cnat n" > assumes f: "cf m n" > shows "cnat m" > using f > proof (induct m) > fix x > case "cnat n ==> cf (cn n) n" > case "cnat n" > case "cn n" > case cnf > > That last list of cases is all kinds of things I tried to use to point out > that I mean the first, noninductive case there. > > I can understand that the best way to prove something about recursive > function is: > > - Show that the parts of function, which are not recursive ("entry > points") will be True if values given have property x (and False otherwise). > - Show that the parts of function, which are recursive and call those > parts will be True if values given have property x (and False otherwise). > > This could be extended by having properties x, y and z and paths, which have > this property. This is finite task to create all possible paths from one to > another and show that iff given values have property x, y or z, then all > calls they make have property z, y or x (for example) and thus, all paths > lead to True if input has any of such properties; then to show that some > such property is assumed. > > Anyway, I am probably lacking some critical bit of knowledge to actually > create such path and show about those properties ...manuals give this rather > by example, but my current tries to generalize them to my case do not meet > some constraint if any of them is interpreted as meant at all. > > How to solve such cases - example for concrete examples would be nice, link > to general manual not needing too much foreknowledge would be also very > nice. Because this is totally critical for me to have such things proven to > continue - I can already handle the simple non-recursive proofs in many > cases, but I do not catch the logic(s?) behind cases. > > Tambet

**References**:**[isabelle] One more case about induction***From:*Tambet

- Previous by Date: [isabelle] One more question about recursive functions
- Next by Date: Re: [isabelle] an inductive datatype and n inductively defined set
- Previous by Thread: [isabelle] One more case about induction
- Next by Thread: [isabelle] One more question about recursive functions
- Cl-isabelle-users July 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