Re: [isabelle] Basic question about apply-style reasoning



On 05/04/2011 04:59 AM, Peter Lammich wrote:

apply (subst arg_cong2[where f=I]) by auto
does the job, but introduces some odd-looking schematic variables in
between.

In your case, this rule is more suitable as an introduction rule, i.e.

    by (rule arg_cong2[where f=I]) auto


This does not work.
   thm arg_cong2[where f=I]
yields
   [|?a = ?b; ?c = ?d|] ==>  I ?a ?c = I ?b ?d


Because of exactly this situation some years ago I enquired if it could be possible to turn off higher order unification (ie, leaving first-order unification), so then one could simply use arg_cong2
(which would in effect look like
... ==> app (app f a) c = ..., so would unify unambiguously with your goal)

Jeremy





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