Re: [isabelle] One more case about induction

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.


> I did try strategies described in
> 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

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