Re: [isabelle] A quick question about fixing variables in a proof

On Mon, 14 Dec 2009, munddr at wrote:

Does anyone know how to unify 'func' to G and s/f to the second argument? Why can't auto unify them?

Because auto (and the Isar proof language in general) observe the logical scopes of abstract entities. In the context of your proof, "func", "G", "s", "f" are all fixed, to there is no way to instantiate them (via unification or other means). While global "consts" can never be instantiated without leaving the background theory itself, a locally fixed entity like "func" becomes arbitrary after leaving it scope. Cf. the following canonical Isar pattern:

    fix x
    have "B x" sorry
  have "B a" by fact

Anyway, I couldn't see what you where trying to do. Can you explain the reasoning informally?


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