Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] how to get start to prove function of function...


view this post on Zulip Email Gateway (Aug 22 2022 at 11:04):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Martin,

I’m unsure whether I understood your question correctly, so here are two answers.

1) If you want to search for functions having certain properties like reflexivity, associativity or similar, you can just use find_theorems.
For instance

find_theorems "?x (?x ?a ?b) ?c = ?x ?a (?x ?b ?c)“

gives you a list of 35 associativity lemmas in Main.

2) If you want to define and reason on functions on an axiomatic way,
you can use type-classes or locales, e.g., have a look at the linorder-class.
Afterwards you just have to instantiate the class or interpret the locale.
For more details on this, please check the isar-ref manual, especially sections 5.7 and 5.8.

Best regards,
René

view this post on Zulip Email Gateway (Aug 22 2022 at 11:05):

From: Buday Gergely <gbuday@karolyrobert.hu>
These are not axioms but function inequations. Is this your homework?

Look for some literature on these.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:05):

From: Mandy Martin <tesleft@hotmail.com>
Hi
this is my personal work.
too many combinations, and i feel that function of function base on function's transitive.besides proving below, i would like to search an axiom which only occur in this second order type's axioms.
f(f(x,y),y) + f(y,f(y,z)) > f(f(x,y),f(y,z))f(f(x,z),y) + f(y,f(y,z)) > f(f(x,z),f(y,z))f(f(y,z),y) + f(y,f(x,y)) > f(f(y,z),f(x,y))f(x,f(y,z)) + f(f(y,z),z) > f(x,z)f(x,f(y,z)) + f(f(y,z),f(x,z)) > f(x,f(x,z))
Regards,
Martin

view this post on Zulip Email Gateway (Aug 22 2022 at 11:05):

From: Mandy Martin <tesleft@hotmail.com>
Hi Thiemann,
so many combinations, and i feel that function of function base on function's transitive.besides proving below, i would like to search an axiom which only occur in this second order type's axioms.
can we search this type of axioms?
f(f(x,y),y) + f(y,f(y,z)) > f(f(x,y),f(y,z))f(f(x,z),y) + f(y,f(y,z)) > f(f(x,z),f(y,z))f(f(y,z),y) + f(y,f(x,y)) > f(f(y,z),f(x,y))f(x,f(y,z)) + f(f(y,z),z) > f(x,z)f(x,f(y,z)) + f(f(y,z),f(x,z)) > f(x,f(x,z))
Regards,
Martin

view this post on Zulip Email Gateway (Aug 22 2022 at 11:05):

From: Buday Gergely <gbuday@karolyrobert.hu>
Dear Martin,

I would call these definitions. What do you want to prove from these definitions?

view this post on Zulip Email Gateway (Aug 22 2022 at 11:09):

From: Buday Gergely <gbuday@karolyrobert.hu>
Hi Martin,

do you mean:

another definition that is equivalent to transitivity?

That is a smallish research question. I doubt if you could find it by using Isabelle.

Isabelle helps you if you have already a pen-and-paper proof, usually.

In this case if you spice up proper automation, Isabelle can check the equivalence though.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:09):

From: Mandy Martin <tesleft@hotmail.com>
Hi Gergely,
Before prove , i would like to search all definitions first. is there method to guess a definition as equivalent important as transitive?
Regards,
Martin


Last updated: Mar 28 2024 at 08:18 UTC