# [isabelle] free term instantiations

```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

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)

```

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