Email Gateway (Aug 18 2022 at 15:32): Email Gateway (Aug 18 2022 at 15:32):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 18 2022 at 15:32):From: Tobias Nipkow <nipkow@in.tum.de>
`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:
Email Gateway (Aug 18 2022 at 15:32):From: John Munroe <munddr@gmail.com>
On Tue, Jun 22, 2010 at 9:18 AM, Tobias Nipkow <nipkow@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 simpIs 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
Email Gateway (Aug 18 2022 at 15:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
I see. Do you know where 'symmetric' is defined? Also, how about 'combination'?
just to avoid confusion: symmetric and combination as appearing in proof
terms are rules (axioms) of the logical framework; symmetric also
appears as theorem in theory Pure:
thm Pure.symmetric
These rules are implemented in the inference kernel of the system and
not defined in an Isar theory.
Distinguish from these the attribute "symmetric", which may apply one
rule of a larger set of symmetry theorems, one of these being
Pure.symmetric.
Hope this helps,
Florian
signature.asc
Last updated: Apr 25 2024 at 08:20 UTC