Stream: General

Topic: Discharging OFCLASS assumption


view this post on Zulip Lukas Stevens (Oct 22 2020 at 10:39):

Suppose I have a theorem OFCLASS(?'a::order, preorder_class) ⟹ (?y::?'a::order) ≤ (?z::?'a::order) ⟹ ?y ≤ ?z. Using Isabelle/ML, how can I obtain the theorem (?y::?'a::order) ≤ (?z::?'a::order) ⟹ ?y ≤ ?z?

view this post on Zulip Lukas Stevens (Oct 22 2020 at 10:51):

Ok, if the former theorem is bound to thm then I can do:

thm OF [@{lemma ‹OFCLASS('a::order, preorder_class)› by intro_classes}]

But what If I don't know how x and y in OFCLASS(x, y) look like?

view this post on Zulip Lukas Stevens (Oct 22 2020 at 13:16):

The solution I found is the following:

val thm = ...
val assm = Goal.prove @{context} [] [] (hd (Thm.prems_of thm)) (K (Class.intro_classes_tac @{context} []))
val thm' = thm OF [assm]

Last updated: Aug 15 2022 at 04:16 UTC