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



On Mon, 14 Dec 2009, munddr at googlemail.com 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?


	Makarius





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