Re: [isabelle] Question about Axiom specification



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.