Kevin Kappelmann (Jan 28 2021 at 12:34): Kevin Kappelmann (Jan 28 2021 at 12:34):I can't find the function congruence lemma for Pure anywhere:
lemma pure_cong: "f ≡ g ⟹ x ≡ y ⟹ f x ≡ g y" by simp
with sorts, just for clarification:
⟦?f::?'a::{} ⇒ ?'b::{} ≡ ?g::?'a::{} ⇒ ?'b::{}; ?x::?'a::{} ≡ ?y::?'a::{}⟧ ⟹ ?f ?x ≡ ?g ?y
Is it really not stated as such anywhere in Pure or am I missing the obvious?
Simon Roßkopf (Jan 28 2021 at 13:01):As far as I know this an axiom about Pure equality(Pure.combination). It could be retrieved from ML
Thm.axiom @{theory} "Pure.combination"
I do not know why this is not made available like other ones(e.g. Pure.reflexive)
Kevin Kappelmann (Jan 28 2021 at 13:12):Ahhh, combination and not cong! :light_bulb: Thank you :)
Last updated: Sep 28 2026 at 16:33 UTC