Email Gateway (Aug 18 2022 at 15:44): Email Gateway (Aug 18 2022 at 15:44):From: Tambet <qtvali@gmail.com>
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
Email Gateway (Aug 18 2022 at 15:44):From: Tobias Nipkow <nipkow@in.tum.de>
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
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
Last updated: Apr 20 2024 at 01:05 UTC