Re: [isabelle] overloaded defs



Steven Obua wrote:
Sean McLaughlin wrote:

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

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


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







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