Email Gateway (Aug 22 2022 at 20:20): Email Gateway (Aug 22 2022 at 20:20):From: patrick barlatier via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I reiterate my question:
To help automatic reasoning with Sledgehammer, I wish to break down a single complex axiom by specifying definitions. For that I use the command "local" and "defines", then "assumes" in this way:
locale set_axioms_CLAY = fixes less_eq :: "object ⇒ object ⇒ bool" fixes bd00 :: "object ⇒ bool" fixes bd01 :: "object ⇒ object ⇒ Uniset ⇒ bool" fixes bd02 :: "object ⇒ Uniset ⇒ bool" fixes bd03 :: "object ⇒ object ⇒ Uniset ⇒ bool" defines BDOO : " bd00(B) ≡ less_eq B B" defines BDO1 : "bd01 A B β ≡ (∀α. In α B & (∀C::object. In β C ⟷ (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F::object. In α E & less_eq F D & less_eq F E))))" defines BD02 : "bd02 A β ≡ (∃L. set_eq β (singleton L) & less_eq A L) " defines BD03: "bd03 A B β ≡ bd00(B) ⟶ bd01 A B β ⟶ bd02 A β " assumes BD04: "∀A B::object. less_eq A B ≡ ∀ β::Uniset. BD03 A B β"begin
But I'm not sure that's correct? Here is the axiom:
lemma BDv4: "∀A B. less_eq A B ⟷ ( (∀α β . In α B & (∀C. In β C ⟷ (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F. In α E & less_eq F D &less_eq F E))) ⟶ (∃L. set_eq β (singleton L) & less_eq A L)))" by (meson BD04)
Bests,Patrick
LISTIC - Université de Savoie
Email Gateway (Aug 22 2022 at 20:20):From: Alexander Krauss <krauss@in.tum.de>
Dear Patrick
Am 25.07.2019 um 10:28 schrieb patrick barlatier via Cl-isabelle-users:
I reiterate my question:
To help automatic reasoning with Sledgehammer, I wish to break down a single complex axiom by specifying definitions. For that I use the command "local" and "defines", then "assumes" in this way:
The formal material in your email is lacking line breaks, so it is
basically unreadable, at least in my mail client.
locale set_axioms_CLAY = fixes less_eq :: "object ⇒ object ⇒ bool" fixes bd00 :: "object ⇒ bool" fixes bd01 :: "object ⇒ object ⇒ Uniset ⇒ bool" fixes bd02 :: "object ⇒ Uniset ⇒ bool" fixes bd03 :: "object ⇒ object ⇒ Uniset ⇒ bool" defines BDOO : " bd00(B) ≡ less_eq B B" defines BDO1 : "bd01 A B β ≡ (∀α. In α B & (∀C::object. In β C ⟷ (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F::object. In α E & less_eq F D & less_eq F E))))" defines BD02 : "bd02 A β ≡ (∃L. set_eq β (singleton L) & less_eq A L) " defines BD03: "bd03 A B β ≡ bd00(B) ⟶ bd01 A B β ⟶ bd02 A β " assumes BD04: "∀A B::object. less_eq A B ≡ ∀ β::Uniset. BD03 A B β"begin
But I'm not sure that's correct? Here is the axiom:
lemma BDv4: "∀A B. less_eq A B ⟷ ( (∀α β . In α B & (∀C. In β C ⟷ (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F. In α E & less_eq F D &less_eq F E))) ⟶ (∃L. set_eq β (singleton L) & less_eq A L)))" by (meson BD04)
I am also not really sure what your question is:
If you are unsure about the approach of using locale + defines: This
approach is useful if you want to instantiate the locale later on, to
obtain concrete versions of the results proved in the locale. If this is
not your goal, you may just as well use the axiomatization command.
If you are unsure whether you have formulated the axioms correctly,
you could try to prove one thing from the other.
Alex
Last updated: Apr 23 2024 at 16:19 UTC