[isabelle] Stuck with proofs about inductive functions



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

lemma cfff:
   assumes "cnat a"
   assumes "cf b a"
   assumes "cf c b"
   shows "cf c a"

I did search similar proofs for Nat.thy, but what I found were rather
cryptic and didn't show their inner structure (as they were all using
tactics). I did not find proof for "a < b & b <= c ==> a < c", which would
have been probably most direct match. Also I would like to know, how to name
those lemmas according to Isabelle's standards and style guidelines. Second
one of those is more needed, but first one seems to be simpler.

I would be happy to get any or all of these:

   - Way(s) to prove this using structured Isar proof.
   - 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).

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.