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.