Re: [isabelle] Stuck with proofs about inductive functions



Tambet schrieb:
> So I have this:
> 
> inductive cf :: "nat => nat => bool" where
>  cnf[intro!]:
>   "cnat n ==> cf (cn n) n" |
>  cff[intro!]:
>   "cf m n ==> cf (cn m) n"
> 
> fun cfe :: "nat => nat => bool" where
>   "cfe m n = ((m = n) | (cf m n))"
> 
> And want to show these:
> 
> lemma cfef:
>    assumes "cnat a"
>    assumes "cf b a"
>    shows "cfe b (cn a)"

I tried to prove this by induction:

lemma cfef: "cf b a ==> cnat a ==> cfe b (cn a)"
proof(induct rule: cf.induct)
  case cnf show ?case by simp
next
  case (cff m n) thus ?case
apply auto

But this leads to the goal

 1. [| cf (cn n) n; cnat n; cn (cn n) ~= cn n |] ==> cf n (cn n)

I don't see how to prove this. In fact, I doubt that the lemma is
provable: the def of cf never forces cn into the second argument, but
your lemmas requires to show that cn shows up in the second argument.
Maybe it is provable given the actual definition of cn.

>    - Way(s) to prove this using structured Isar proof.

See above.

>    - Way(s) to prove this using automated tactics.
>    - Explanation about those tactics.
>    - Link to manual pages, which do not assume too wide knowledge about
>    Isabelle as prerequisite (but the ones, which do, would also be better than
>    nothing).

See my already advertised slides.

Tobias

> As it is very commonly needed thing to prove things about similar functions,
> I would like to catch the underlying logic, thus a few words of explanation
> would be very nice.
> 
> Tambet





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