Re: [isabelle] 'symmetric' and full proofs



On Tue, Jun 22, 2010 at 9:18 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> `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.
>

I see. Do you know where 'symmetric' is defined? Also, how about 'combination'?

John

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