Email Gateway (Aug 18 2022 at 13:39): Email Gateway (Aug 18 2022 at 13:39):From: barzan stefania <stefania_barzan@yahoo.com>
Dear list members,
I try to define the smallest divisor of a number by the following:
definition :: "nat=> nat" where
"sdiv e == if ((\<not> prime e) \<and> (\<not> e=1)) then (LEAST e1. prime e1 \<and> e1 dvd e) else e"
My experiences showed me that the most hardest lemmas to prove are the one that follow direct from the definitions.
For example now i try to prove: lemma sdiv_le: "e1 dvd e==> prime e1 ==> (sdiv e) <= e1"
lemma sdiv_dvd: "(sdiv e) dvd e"
and i dont figure out how to do it.
Can someone give me some hints?
Thank you,
Stefania
Email Gateway (Aug 18 2022 at 13:39):From: Tobias Nipkow <nipkow@in.tum.de>
lemma sdiv_le: "e1 dvd e==> prime e1 ==> (sdiv e) <= e1"
apply(auto simp:sdiv_def)
apply(metis COMBC_def Collect_conj_eq Collect_def diff_diff_cancel
eq_imp_le inter_code less_imp_diff_less less_le_not_le nat_le_linear
not_less_Least)
apply (metis eq_imp_le nat_one_not_prime prime_nat_def)
The two metis calls were generated automatically by sledgehammer for me.
The first step was to help sledgehammer a little bit because I knew the
definition of sdiv needs to be expanded.
For the other lemma it didn't work - a proof was found (using amongst
other things LeastI and nat_prime_factor) but metis takes too long on it.
Tobias
barzan stefania schrieb:
Email Gateway (Aug 18 2022 at 13:40):From: Johannes Hölzl <hoelzl@in.tum.de>
Am Montag, den 29.06.2009, 02:14 -0700 schrieb barzan stefania:
Dear list members,
I try to define the smallest divisor of a number by the following:
definition :: "nat=> nat" where
"sdiv e == if ((\<not> prime e) \<and> (\<not> e=1)) then (LEAST e1. prime e1 \<and> e1 dvd e) else e"My experiences showed me that the most hardest lemmas to prove are the one that follow direct from the definitions.
For example now i try to prove: lemma sdiv_le: "e1 dvd e ==> prime e1 ==> (sdiv e) <= e1"
lemma sdiv_dvd: "(sdiv e) dvd e"
and i dont figure out how to do it.
Can someone give me some hints?
If you know how to efficiently search lemmas in Isabelle they are easy
to solve. When you type << C-c C-f >> in ProofGeneral you can write
patterns and search for lemmas. For example:
When you write "(LEAST x. _) \<le> ?a" (you also need to write the "s,
the _ and ?a are wildcards) it yields Least_le, which can be used as an
introduction rule.
To unfold sdiv we can use "unfolding sdiv_def". Each definition provides
suchs lemma as <<name>>_def. Often it is enough to unfold the constant
and run the auto tactic. Sometimes we need also to specify some
introduction rules and/or rewrite rules. Instad of using <<unfolding>>
you could also add it as rewrite rule with << simp add: sdiv_def >>.
To see where the auto tactic stops just use << proof auto >> and it
shows the current state.
--- 8< ---------------------------
lemma sdiv_le: "e1 dvd e ==> prime e1 ==> (sdiv e) <= e1"
(* First you need to unfold the constant (the name of the lemma is .._def): *)
unfolding sdiv_def
(* proof auto -- auto knows enough about If that it can split it into two new goals *)
(* proof (auto intro!: Least_le) -- We need to tell it how to handle "LEAST ... \<le> ...",
here we have the introduction rule Least_le *)
by (auto intro!: Least_le
simp add: prime_nat_def) (* To solve it we need also the definition of prime numbers *)
lemma sdiv_dvd: "(sdiv e) dvd e"
(* This works similar *)
by (auto intro!: LeastI2_ex[where Q="% x. x dvd e"]
simp add: nat_prime_factor[of "e"])
--- 8< ---------------------------
Of course in most cases the auto tactic does not solve the goal
immediately. Then it is better to write Isar proofs, introducing new
rules and finally invoking auto with this new rules.
Hope this helped.
Johannes
Thank you,
Stefania
Last updated: May 03 2024 at 04:19 UTC