Re: [isabelle] type classes



On Fri, 18 Aug 2006, Jeremy Dawson wrote:

> It seems to me that one ought to be able to prove
> 
> Goal "OFCLASS ('b :: ord, order_class) ==>
>  ((x :: 'b) <= y) = (x < y | x = y)" ;

> How can one use the theorem order_le_less to prove this goal?

In Isabelle2005 (and before) there is no explicit way to move backwards 
from syntactic class constraints to the above logical representation (the 
other direction is provided by Thm.class_triv).

In recent development snapshots you can do it like this:

fun unconstrain_tvars th =
  let
    val certT = Thm.ctyp_of (Thm.theory_of_thm th);
    val tvars = Drule.fold_terms Term.add_tvars th [];
  in fold (Thm.unconstrainT o certT o TVar) tvars th end;

For example:

  ML> unconstrain_tvars order_le_less
  val it = "OFCLASS(?'a, order_class) ==> (?x <= ?y) = (?x < ?y | ?x = ?y)": thm


	Makarius





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