Lukas Stevens (Oct 22 2020 at 10:39): 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?
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?
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: Dec 21 2024 at 12:33 UTC