diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Cfe/Language/Base.agda | 2 | ||||
| -rw-r--r-- | src/Cfe/Language/Properties.agda | 34 |
2 files changed, 28 insertions, 8 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index 2919ed7..d9be456 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -66,9 +66,9 @@ w ∉ A = ¬ w ∈ A ------------------------------------------------------------------------ -- Language Combinators +infix 8 ⋃_ infix 7 _∙_ infix 6 _∪_ -infix 5 ⋃_ _∙_ : Language a → Language b → Language _ A ∙ B = record diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda index 5792216..61a11b2 100644 --- a/src/Cfe/Language/Properties.agda +++ b/src/Cfe/Language/Properties.agda @@ -6,7 +6,14 @@ module Cfe.Language.Properties {c ℓ} (over : Setoid c ℓ) where -open Setoid over using () renaming (Carrier to C; _≈_ to _∼_; refl to ∼-refl) +open Setoid over using () + renaming + ( Carrier to C + ; _≈_ to _∼_ + ; refl to ∼-refl + ; sym to ∼-sym + ; trans to ∼-trans + ) open import Algebra open import Cfe.Function.Power @@ -266,6 +273,19 @@ xyw∉｛c｝ : ∀ c x y w → x ∷ y ∷ w ∉ ｛ c ｝ xyw∉｛c｝ c x y w (_ ∷ ()) ------------------------------------------------------------------------ +-- Algebraic properties of ｛_｝ + +｛｝-cong : ∀ {c c′} → c ∼ c′ → ｛ c ｝ ≈ ｛ c′ ｝ +｛｝-cong c∼c′ = + ⊆-antisym + (sub λ { (c∼x ∷ []) → c∼c′⇒c′∈｛c｝ (∼-trans (∼-sym c∼c′) c∼x) }) + (sub λ { (c′∼x ∷ []) → c∼c′⇒c′∈｛c｝ (∼-trans c∼c′ c′∼x) }) + +｛｝-inj : ∀ {c c′} → ｛ c ｝ ≈ ｛ c′ ｝ → c ∼ c′ +｛｝-inj {c} c≈c′ with ∈-resp-≈ c≈c′ (∼-refl ∷ []) +... | (c′∼c ∷ []) = ∼-sym c′∼c + +------------------------------------------------------------------------ -- Properties of _∙_ ------------------------------------------------------------------------ -- Membership properties of _∙_ @@ -408,14 +428,14 @@ c∈Flast[B]+w∈A⇒c∈Flast[A∙B] {c = c} (x , w , xw∈B , w′ , xwcw′ -- Bundles -∙-Magma : ∀ {a} → Magma (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) -∙-Magma {a} = record { isMagma = ∙-isMagma {a} } +∙-magma : ∀ {a} → Magma (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) +∙-magma {a} = record { isMagma = ∙-isMagma {a} } -∙-Semigroup : ∀ {a} → Semigroup (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) -∙-Semigroup {a} = record { isSemigroup = ∙-isSemigroup {a} } +∙-semigroup : ∀ {a} → Semigroup (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) +∙-semigroup {a} = record { isSemigroup = ∙-isSemigroup {a} } -∙-Monoid : ∀ {a} → Monoid (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) -∙-Monoid {a} = record { isMonoid = ∙-isMonoid {a} } +∙-monoid : ∀ {a} → Monoid (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a)) +∙-monoid {a} = record { isMonoid = ∙-isMonoid {a} } ------------------------------------------------------------------------ -- Other properties of _∙_ |