Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Several proof methods in one proof?

Email Gateway (Aug 18 2022 at 16:33):

From: Tobias Nipkow <nipkow@in.tum.de>
Victor Porton schrieb:

I incidentally wrote:

lemma comp_fun2: "[| g: A->B1; f: B0->C; B1<=B0 |] ==> (f O g) : A->C"
proof -
assume "g: A->B1" "f: B0->C" "B1<=B0"
with g: A->B1 have "g: A->B0" by auto (rule fun_weaken_type)
with f: B0->C show "(f O g) : A->C" sorry
qed

Surprisingly it works. But I don't understand what "auto (rule
fun_weaken_type)" means. Is it both "auto" and "(rule fun_weaken_type)"?
If yes, in which order these proof methods are applied?

That's a special idiom where the two proof methods are applied in
succession (from left to right). Doesn't work for three or more methods ;-)

Which .pdf to read about that? Should I read a manual (tutorials seem
not enough)?

You will find a precise description in the Isar reference manual.
Introductory manuals probably do not mention it.

Tobias

--
Victor Porton - http://portonvictor.org

Email Gateway (Aug 18 2022 at 16:45):

From: Victor Porton <porton@narod.ru>
I incidentally wrote:

lemma comp_fun2: "[| g: A->B1; f: B0->C; B1<=B0 |] ==> (f O g) : A->C"
proof -
assume "g: A->B1" "f: B0->C" "B1<=B0"
with g: A->B1 have "g: A->B0" by auto (rule fun_weaken_type)
with f: B0->C show "(f O g) : A->C" sorry
qed

Surprisingly it works. But I don't understand what "auto (rule
fun_weaken_type)" means. Is it both "auto" and "(rule fun_weaken_type)"? If
yes, in which order these proof methods are applied?

Which .pdf to read about that? Should I read a manual (tutorials seem not
enough)?

\--
Victor Porton - http://portonvictor.org

Last updated: Nov 21 2024 at 12:39 UTC