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



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

and the conclusion of this rule (topmost operator is =) does not unify
with "I a' b'", so you cannot use it as introduction rule.
Indeed, apply (rule arg_cong2[where f=I]) fails.
However, a (lengthy)
    apply (erule rev_iffD2[OF _ arg_cong2[where f=I]])
does the job, and yields a'=a &&& b'=b

I have defined a shortcut for rev_iffD2[OF _ arg_cong2], and use this.

Best and thanks again,
  Peter






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