Re: [isabelle] Conjunctions commutative in function arguments?



Viktor,

On Thursday 02 March 2006 22:14, Viktor Kuncak wrote:
> Speaking of equality, what is a robust way to prove combinations of
> linear arithmetic and uninterpreted function symbols?
>
> For example, we would like to prove this simple lemma:
>
> (g (j - (2::int)) :: int) = g ((-2::int) + j)

here's three possibilities:

,----- (1) -----
lemma aux: "(j::int) - 2 = (-2) + j"
  by simp

lemma "g ((j::int) - 2) = g (-2 + j)"
  by (simp add: aux)
`-----

,----- (2) -----
lemma "g ((j::int) - 2) = g (-2 + j)"
  apply (rule cong [of g])
    apply (rule refl)
  apply simp
done
`-----

,----- (3) -----
lemma "g ((j::int) - 2) = g (-2 + j)"
  apply (rule arg_cong [of _ _ g])
  apply simp
done
`-----

Best,
Tjark





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