Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: Tim Freeman <tim@fungible.com>
From: Tjark Weber <tjark.weber@gmx.de>
That seemed like an interesting exercise, so I went ahead and did it.
I often feel that my proofs are too wordy, and I suspect there are
good tactics out there that I should be using but I don't know about
them. Is there a list somewhere of all of the generally-useful
tactics, their arguments, and examples of their use?
I found some .dvi documents that came with Isabelle, but they are a
long exposition that I don't know how to search, rather than a list.
Email Gateway (Aug 17 2022 at 14:14):From: kuecuek@rbg.informatik.tu-darmstadt.de
hallo again
i have still problem with cardinality :( maybe can anyone help me
i want to show that
If p is an odd prime and a is a "Quadratischer rest" in p (EX x. [x^2 = a]
(mod p)) then there are exactly two square roots modulo p.
these are in this fall -x and x.
but i can not prove that in isabelle.
lemma "[|zprime p; 2<p; ~a=0; QuadRes p a|] ==>
card {(x::int).[x^2 = a] (mod p)}=(2::nat)"
is it right?
i have tried to show with the help of the lemma zcong_square_zless:
[| zprime p; 0 < a; a < p; [a * a = 1] (mod p) |] ==> a = 1 | a = p - 1
in this case i formula my lemma
lemma "[| zprime p;2<p; 0 < a; a < p; [a * a = 1] (mod p) |]
==> card {(a::int).[a * a = 1] (mod p) }=(2::nat)"
but i couldn't prove it again.
can anybody give an idea ??
thanks
best regards
Email Gateway (Aug 17 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
I suggest you begin by proving the lemma "x ~= y ==> card({x,y})=2",
which is trivial. Then you get rid of card and merely have to exhibit
x and y.
Larry Paulson
Last updated: May 03 2024 at 04:19 UTC