[isabelle] Question about Axiom specification




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


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