Email Gateway (Aug 17 2022 at 13:46): Email Gateway (Aug 17 2022 at 13:46):From: Sean McLaughlin <seanmcl@cmu.edu>
Hello,
I was under the impression that all terms with free variables have
their terms instantiated (in full proof terms) in the order occurring in
the term. However, I happened upon the following counterexample:
which is instantiated
x, y,below,inf
instead of
below,inf,x,y
as a term order would indicate. Would someone please explain
the exact order of instantiation.
Thanks for your time (on this and previous questions),
Sean
Const ("==>", "prop => prop => prop") $
(Const ("Trueprop", "bool => prop") $
(Const
("Lattice_Locales.partial_order",
"('a => 'a => bool) => bool") $
Free ("below", "'a => 'a => bool"))) $
(Const ("==>", "prop => prop => prop") $
(Const ("Trueprop", "bool => prop") $
(Const
("Lattice_Locales.lower_semilattice_axioms",
"('a => 'a => bool) => ('a => 'a => 'a)
=> bool")
$ Free ("below", "'a => 'a => bool") $
Free ("inf", "'a => 'a => 'a"))) $
(Const ("Trueprop", "bool => prop") $
(Const ("op =", "'a => 'a => bool") $
(Free ("inf", "'a => 'a => 'a") $ Var (("x", 0),
"'a") $
Var (("y", 0), "'a")) $
(Free ("inf", "'a => 'a => 'a") $ Var (("y", 0), "'a") $
Var (("x", 0), "'a"))))) : Term.term
SOME (Var (("x", 0), "?'a")) %
SOME (Var (("y", 0), "?'a")) %
SOME (Var (("below", 0), "?'a => ?'a => bool")) %
SOME (Var (("inf", 0), "?'a => ?'a => ?'a")) %%
A more readable version (in HOL Light syntax) is:
Trueprop (lattice_locales_partial_order below)
==> Trueprop (lattice_locales_lower_semilattice_axioms
below inf)
==> Trueprop (inf x y = inf y x)
Last updated: May 03 2024 at 08:18 UTC