Email Gateway (Aug 22 2022 at 20:18): Email Gateway (Aug 22 2022 at 20:18):From: patrick barlatier via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I wish to decomposed an axiom by using intermediate definitions,
I proceed in this way, does it seem correct to you?
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
Here is the source 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)))"
Patrick Barlatier
Last updated: Apr 24 2024 at 16:18 UTC