*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] One more case about induction*From*: Tambet <qtvali at gmail.com>*Date*: Sun, 25 Jul 2010 16:46:11 +0300

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

**Follow-Ups**:**Re: [isabelle] One more case about induction***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Questions about speed and CPU usage
- Next by Date: Re: [isabelle] Stuck with proofs about inductive functions
- Previous by Thread: Re: [isabelle] Stuck with proofs about inductive functions
- Next by Thread: Re: [isabelle] One more case about induction
- 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