[isabelle] 'symmetric' and full proofs



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.