Email Gateway (Aug 22 2022 at 11:04): 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é
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.
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
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
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?
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.
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: Nov 21 2024 at 12:39 UTC