Email Gateway (Aug 18 2022 at 09:33): Email Gateway (Aug 18 2022 at 09:33):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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)" ;
(where the consequent is just a theorem of the order class, in this case
(["Orderings.order_le_less"], "(?x <= ?y) = (?x < ?y | ?x = ?y)"),
How can one use the theorem order_le_less to prove this goal?
Regards,
Jeremy Dawson
Email Gateway (Aug 18 2022 at 09:33):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 08:18 UTC