Re: [isabelle] overloaded defs

Steven Obua wrote:
Sean McLaughlin wrote:


  How do I find the actual constant an overloaded constant refers to?

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"?



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.


I have some code to do this sort of thing.

tc["op <="];
val it =
         "ACIfSL min op <="),
         "?x <= ?x"),


filrpm "a <= b == x" it;
val it =
   [(["Nat.le_def"], "?m <= ?n == ~ ?n < ?m"),
      (["Set.subset_def"], "?A <= ?B == ALL x:?A. x : ?B"),
         "?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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.