IsFinerThan

formal source

  98/-- R₁ is *at least as fine as* R₂: whenever R₁ identifies two configurations,
  99    R₂ also identifies them. Equivalently, ~_{R₁} ⊆ ~_{R₂} as sets of pairs.
 100    This is the heterogeneous refinement relation (event types may differ). -/
 101def IsFinerThan {E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Prop :=
 102  ∀ c₁ c₂ : C, Indistinguishable r₁ c₁ c₂ → Indistinguishable r₂ c₁ c₂
 103
 104/-- Refinement is reflexive. -/
 105theorem isFinerThan_refl {E : Type*} (r : Recognizer C E) : IsFinerThan r r :=
 106  fun _ _ h => h
 107
 108/-- Refinement is transitive. -/
 109theorem isFinerThan_trans {E₁ E₂ E₃ : Type*}
 110    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃)
 111    (h₁₂ : IsFinerThan r₁ r₂) (h₂₃ : IsFinerThan r₂ r₃) :
 112    IsFinerThan r₁ r₃ :=
 113  fun c₁ c₂ h => h₂₃ c₁ c₂ (h₁₂ c₁ c₂ h)
 114
 115/-- The composite is finer than both components. -/
 116theorem composite_isFinerThan_left {E₁ E₂ : Type*}
 117    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 118    IsFinerThan (r₁ ⊗ r₂) r₁ :=
 119  fun c₁ c₂ h => ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).1
 120
 121theorem composite_isFinerThan_right {E₁ E₂ : Type*}
 122    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
 123    IsFinerThan (r₁ ⊗ r₂) r₂ :=
 124  fun c₁ c₂ h => ((composite_indistinguishable_iff r₁ r₂ c₁ c₂).mp h).2
 125
 126/-- The composite is the coarsest recognizer finer than both components. -/
 127theorem composite_isFinerThan_glb {E₁ E₂ E₃ : Type*}
 128    (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (r₃ : Recognizer C E₃)
 129    (h₁ : IsFinerThan r₃ r₁) (h₂ : IsFinerThan r₃ r₂) :
 130    IsFinerThan r₃ (r₁ ⊗ r₂) :=
 131  fun c₁ c₂ h => (composite_indistinguishable_iff r₁ r₂ c₁ c₂).mpr ⟨h₁ c₁ c₂ h, h₂ c₁ c₂ h⟩