Email Gateway (Aug 18 2022 at 09:51): Email Gateway (Aug 18 2022 at 09:51):From: Tao Ma <separable@gmail.com>
hi,
i am learning Isabelle/Isar, i am trying to practice by writing some test
lemmas using HOL/Algebra.
the following basically define a set in ring R that has x*x = x and shows
1 \in this set. but what should i do next to get this proved?
thanks
tao
constdefs (structure R) test_set :: "('a, 'm) ring_scheme => 'a set"
"test_set R == {z. z \<in> carrier R & z \<otimes> z = z }"
lemma (in ring) lm8: includes ring R
assumes kk: "z = \<one>"
shows "z \<in> (test_set R)"
proof (unfold test_set_def)
from kk have k1: "z \<in> carrier R" by auto
from kk have k2: "z \<otimes> z = z" by auto
from k1 and k2 have k3: "z \<in> carrier R & z \<otimes> z = z" by auto
Email Gateway (Aug 18 2022 at 09:55):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Tao Ma,
You have to apply the lemma CollectI in order to get the set
comprehension. You could continue your proof by
from k3 show "z \<in> {z \<in> carrier R. z \<otimes> z = z}" by rule
The rule method is able to pick the lemma automatically.
Note that in your goal statement, "includes ring R" is not necessary
since the ring specification is already included by the the target
specification (in ring).
Clemens
Last updated: May 03 2024 at 08:18 UTC