Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I often need to investigate the instantiation of type variables in
a proofterm.
The order in which this is done is that returned by the function
term_tvars : term -> (indexname * sort) list
This works fine when I extract a term from a proofterm, eg
ML {* val (_ %% (_ %% ((((((PAxm(_,x,_) % _) % _) % _) % _)%% _) %%
_)) %% _) = get_proof "HOL.TrueI" *}
ML {* term_tvars x *}
val it = [(("'b", 0), ["logic"]), (("'a", 0), ["logic"])]
: (Term.indexname * Term.sort) list
However, when I construct a term myself, it doesn't
ML {* term_tvars (read "INTER") *}
val it = [] : (Term.indexname * Term.sort) list
even though this INTER has two free type variables.
How can I get this to work?
Thanks,
Sean
Email Gateway (Aug 17 2022 at 13:27):From: Lawrence Paulson <lp15@cam.ac.uk>
One suggestion is that you work directly with the ML level rather
than from the Isar level: use "isabelle" rather than "Isabelle" to
start up. Then use the constructors in Pure/term.ML to express terms.
~: isabelle
Poly/ML RTS version PPC-4.1.3 (12:32:32 Dec 21 2004)
Copyright (c) 2002 CUTS and contributors.
Running with heap parameters
(h=81920K,ib=16384K,ip=100%,mb=20480K,mp=20%)
Mapping /Users/lcp/isabelle/heaps/polyml-4.1.3_ppc-darwin/HOL
Mapping /Users/lcp/isabelle/Repos/polyml-4.1.3/ppc-darwin/ML_dbase
Poly/ML 4.1.3 Release
val it = () : unit
Free ("fred", TVar (("'a",3), ["logic"]));
val it = Free ("fred", "?'a3") : Term.term
term_tvars it;
val it = [(("'a", 3), ["logic"])] : (Term.indexname * Term.sort) list
Larry Paulson
Email Gateway (Aug 17 2022 at 13:27):From: Tjark Weber <tjark.weber@gmx.de>
Sean,
The result of read "INTER" has two TFree's, but no TVar's. Consequently,
term_tvars returns an empty list. Use
term_tfrees : Term.term -> (string * Term.sort) list
to obtain a list with all TFree's in a term. See Pure/term.ML for further
details.
Best regards,
Tjark
Last updated: May 03 2024 at 04:19 UTC