Theory List_Syntax

section ‹List Syntax›

theory List_Syntax imports Main begin

abbreviation list_member_syntax :: ‹'a ⇒ 'a list ⇒ bool› (‹_ [∈] _› [51, 51] 50) where
  ‹x [∈] A ≡ x ∈ set A›

abbreviation list_not_member_syntax :: ‹'a ⇒ 'a list ⇒ bool› (‹_ [∉] _› [51, 51] 50) where
  ‹x [∉] A ≡ x ∉ set A›

abbreviation list_subset_syntax :: ‹'a list ⇒ 'a list ⇒ bool› (‹_ [⊂] _› [51, 51] 50) where
  ‹A [⊂] B ≡ set A ⊂ set B›

abbreviation list_subset_eq_syntax :: ‹'a list ⇒ 'a list ⇒ bool› (‹_ [⊆] _› [51, 51] 50) where
  ‹A [⊆] B ≡ set A ⊆ set B›

abbreviation removeAll_syntax :: ‹'a list ⇒ 'a ⇒ 'a list› (infix ‹[÷]› 75) where
  ‹A [÷] x ≡ removeAll x A›

syntax (ASCII)
  "_BallList"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3ALL (_/[:]_)./ _)› [0, 0, 10] 10)
  "_BexList"        :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3EX (_/[:]_)./ _)› [0, 0, 10] 10)
  "_Bex1List"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3EX! (_/[:]_)./ _)› [0, 0, 10] 10)
  "_BleastList"     :: ‹id ⇒ 'a list ⇒ bool ⇒ 'a›       (‹(3LEAST (_/[:]_)./ _)› [0, 0, 10] 10)

syntax (input)
  "_BallList"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3! (_/[:]_)./ _)› [0, 0, 10] 10)
  "_BexList"        :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3? (_/[:]_)./ _)› [0, 0, 10] 10)
  "_Bex1List"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3?! (_/[:]_)./ _)› [0, 0, 10] 10)

syntax
  "_BallList"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3∀(_/[∈]_)./ _)› [0, 0, 10] 10)
  "_BexList"        :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3∃(_/[∈]_)./ _)› [0, 0, 10] 10)
  "_Bex1List"       :: ‹pttrn ⇒ 'a list ⇒ bool ⇒ bool›  (‹(3∃!(_/[∈]_)./ _)› [0, 0, 10] 10)
  "_BleastList"     :: ‹id ⇒ 'a list ⇒ bool ⇒ 'a›       (‹(3LEAST(_/[∈]_)./ _)› [0, 0, 10] 10)

syntax_consts
  "_BallList" ⇌ Ball and
  "_BexList" ⇌ Bex and
  "_Bex1List" ⇌ Ex1 and
  "_BleastList" ⇌ Least

translations
  "∀x[∈]A. P" ⇌ "CONST Ball (CONST set A) (λx. P)"
  "∃x[∈]A. P" ⇌ "CONST Bex (CONST set A) (λx. P)"
  "∃!x[∈]A. P" ⇀ "∃!x. x [∈] A ∧ P"
  "LEAST x[:]A. P" ⇀ "LEAST x. x [∈] A ∧ P"

syntax (ASCII output)
  "_setlessAllList" :: ‹[idt, 'a, bool] ⇒ bool›  (‹(3ALL _[<]_./ _)› [0, 0, 10] 10)
  "_setlessExList"  :: ‹[idt, 'a, bool] ⇒ bool›  (‹(3EX _[<]_./ _)› [0, 0, 10] 10)
  "_setleAllList"   :: ‹[idt, 'a, bool] ⇒ bool›  (‹(3ALL _[<=]_./ _)› [0, 0, 10] 10)
  "_setleExList"    :: ‹[idt, 'a, bool] ⇒ bool›  (‹(3EX _[<=]_./ _)› [0, 0, 10] 10)
  "_setleEx1List"   :: ‹[idt, 'a, bool] ⇒ bool›  (‹(3EX! _[<=]_./ _)› [0, 0, 10] 10)

syntax
  "_setlessAllList" :: ‹[idt, 'a, bool] ⇒ bool›   (‹(3∀_[⊂]_./ _)› [0, 0, 10] 10)
  "_setlessExList"  :: ‹[idt, 'a, bool] ⇒ bool›   (‹(3∃_[⊂]_./ _)› [0, 0, 10] 10)
  "_setleAllList"   :: ‹[idt, 'a, bool] ⇒ bool›   (‹(3∀_[⊆]_./ _)› [0, 0, 10] 10)
  "_setleExList"    :: ‹[idt, 'a, bool] ⇒ bool›   (‹(3∃_[⊆]_./ _)› [0, 0, 10] 10)
  "_setleEx1List"   :: ‹[idt, 'a, bool] ⇒ bool›   (‹(3∃!_[⊆]_./ _)› [0, 0, 10] 10)

syntax_consts
  "_setlessAllList" "_setleAllList" ⇌ All and
  "_setlessExList" "_setleExList" ⇌ Ex and
  "_setleEx1List" ⇌ Ex1

translations
  "∀A[⊂]B. P" ⇀ "∀A. A [⊂] B ⟶ P"
  "∃A[⊂]B. P" ⇀ "∃A. A [⊂] B ∧ P"
  "∀A[⊆]B. P" ⇀ "∀A. A [⊆] B ⟶ P"
  "∃A[⊆]B. P" ⇀ "∃A. A [⊆] B ∧ P"
  "∃!A[⊆]B. P" ⇀ "∃!A. A [⊆] B ∧ P"

end