# Re: [isabelle] 'symmetric' and full proofs

`symmetric' is an attribute that acts on thms (excuse the fact that
attributes act). It turns "R s t" into "R t s", where R is some
symmetric predicate. It works for both "=", "~=", "^-1" and "==" and can
be extended with other symmetric predicates.
Tobias
John Munroe schrieb:
> Hello all,
>
> I see that the 'symmetric' option is quite commonly use -- what does
> it actually do? For example, from LocaleTest.thy:
>
> lemma rcancel:
> "y ** x = z ** x <-> y = z"
> proof
> assume "y ** x = z ** x"
> then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
> by (simp add: assoc [symmetric])
> then show "y = z" by (simp add: rone rinv)
> qed simp
>
> Is it the same as the 'symmetric' that is often found in the output of
> full_prf? Are 'combination', 'reflexive', 'transitive', etc. in full
> proofs rules like 'exI'? What do these do/mean?
>
> Best,
> John

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