Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
How do I find the actual constant an overloaded constant refers to?
Eg.
read "(A::bool set) <= (B :: bool set)";
val it =
Const ("op <=", "bool set => bool set => bool") $ Free ("A",
"bool set") $
Free ("B", "bool set") : Term.term
How do I find that "op <=" means "subset"?
Thanks,
Sean
Email Gateway (Aug 17 2022 at 13:46):From: Lawrence Paulson <lp15@cam.ac.uk>
An overloaded constant simply refers to itself. There isn't a
separate constant called "subset".
Larry
Email Gateway (Aug 17 2022 at 13:46):From: Steven Obua <obua@in.tum.de>
Sean McLaughlin wrote:
Maybe you just want the definition of this constant for these special
types; the only way to do this right now in Isabelle is to scan through
the axioms of a theory and look for something that looks like this
definition.
Steven
Email Gateway (Aug 17 2022 at 13:46):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Steven Obua wrote:
I have some code to do this sort of thing.
tc["op <="];
val it =
[(["Finite_Set.min_max.below_inf_sup_Inf_Sup.ACIfSL_inf"],
"ACIfSL min op <="),
(["Orderings.order_class.order_refl",
"Orderings.order_class.axioms_1"],
"?x <= ?x"),
(etc)
filrpm "a <= b == x" it;
val it =
[(["Nat.le_def"], "?m <= ?n == ~ ?n < ?m"),
(["Set.subset_def"], "?A <= ?B == ALL x:?A. x : ?B"),
(["IntDef.le_int_def"],
"?z <= ?w ==
EX x y u v.
x + v <= u + y &
(x, y) : Rep_Integ ?z & (u, v) : Rep_Integ ?w")]
: (string list * Thm.thm) list
It's in
http://users.rsise.anu.edu.au/~jeremy/isabelle/gen05/gen.ML
Jeremy
Last updated: May 03 2024 at 08:18 UTC