[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

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)







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