Stream: Beginner Questions

Topic: Pure.cong?


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Kevin Kappelmann (Jan 28 2021 at 13:12):

Ahhh, combination and not cong! :light_bulb: Thank you :)


Last updated: Sep 25 2021 at 09:17 UTC