Email Gateway (Aug 23 2022 at 08:17): Email Gateway (Aug 23 2022 at 08:17):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Dear Isabelle users,
In "HOL-Algebra.Exponent" we find the following function:
definition multiplicity :: "'a ⇒ 'a ⇒ nat" where
"multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
I would like to do computations in Isabelle of this function, e.g.,
value ‹multiplicity 2 12›
My strategy was to redefine this function in a recursive way
lemma multipl'_rec:
fixes n::nat and p::nat
assumes ‹n ≠ 0›
shows ‹(((n+1) div (p+2)))-1 < n›
by (smt add.commute add_diff_inverse_nat add_less_same_cancel2 assms div_less_dividend less_one linorder_neqE_nat nat_add_left_cancel_less not_add_less2 one_less_numeral_iff semiring_norm(76) zero_less_diff)
function multipl' :: "nat ⇒ nat ⇒ nat"
where
"multipl' p 0 = 0"
| "p+2 dvd n+1 ⟹ multipl' p n = Suc (multipl' p (((n+1) div (p+2)))-1)"
| "¬ (p+2 dvd n+1) ⟹ multipl' p n = 0"
apply simp+
apply (metis old.prod.exhaust)
apply metis
apply (metis Suc_1 Suc_eq_plus1 Suc_le_mono Suc_n_not_le_n add_Suc_right divides_aux_eq dvd_1_left
dvd_antisym le0)
apply metis
apply (metis old.prod.inject)
apply (metis prod.inject)
by metis
termination
apply auto
proof
show "multipl'_dom y"
if "multipl'_rel y (a, b)"
for a :: nat
and b :: nat
and y :: "nat × nat"
using that sorry
qed
fun multipl :: "nat ⇒ nat ⇒ nat" where
‹multipl p n = multipl' (p-2) (n-1)›
and to prove that the new definition is equivalent to the old definition, i.e.,
lemma multipl_multiplicity:
fixes p::nat and n::nat
assumes ‹prime p› and ‹n ≠ 0›
shows ‹multipl p n = multiplicity p n›
sorry
Nevertheless, when I write
value ‹multipl 2 12›
I receive the following error message: "exception Match raised (line 10 of "generated code")"
Any suggestions in order to fix this problem? Thank you in advance.
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:22):From: Manuel Eberl <eberlm@in.tum.de>
The problem is that the code generator cannot handle conditional
equations in a function definition. You will have to prove a code
equation that does explicit "if" instead.
By the way, I found the following code in an AFP entry
(Probabilistic_Prime_Tests/Fermat_Witness). I think I wrote this a while
ago. I should probably put this in the library, but until then, feel
free to use it.
definition divide_out :: "'a :: factorial_semiring \<Rightarrow> 'a
\<Rightarrow> 'a \<times> nat" where
"divide_out p x = (x div p ^ multiplicity p x, multiplicity p x)"
lemma fst_divide_out [simp]: "fst (divide_out p x) = x div p ^
multiplicity p x"
and snd_divide_out [simp]: "snd (divide_out p x) = multiplicity p x"
by (simp_all add: divide_out_def)
function divide_out_aux :: "'a :: factorial_semiring \<Rightarrow> 'a
\<times> nat \<Rightarrow> 'a \<times> nat" where
"divide_out_aux p (x, acc) =
(if x = 0 \<or> is_unit p \<or> \<not>p dvd x then (x, acc) else
divide_out_aux p (x div p, acc + 1))"
by auto
termination proof (relation "measure (\<lambda>(p, x, _). multiplicity p
x)")
fix p x :: 'a and acc :: nat
assume "\<not>(x = 0 \<or> is_unit p \<or> \<not>p dvd x)"
thus "((p, x div p, acc + 1), p, x, acc) \<in> measure (\<lambda>(p,
x, _). multiplicity p x)"
by (auto elim!: dvdE simp: multiplicity_times_same)
qed auto
lemmas [simp del] = divide_out_aux.simps
lemma divide_out_aux_correct:
"divide_out_aux p z = (fst z div p ^ multiplicity p (fst z), snd z +
multiplicity p (fst z))"
proof (induction p z rule: divide_out_aux.induct)
case (1 p x acc)
show ?case
proof (cases "x = 0 \<or> is_unit p \<or> \<not>p dvd x")
case False
have "x div p div p ^ multiplicity p (x div p) = x div p ^
multiplicity p x"
using False
by (subst dvd_div_mult2_eq [symmetric])
(auto elim!: dvdE simp: multiplicity_dvd multiplicity_times_same)
with False show ?thesis using 1
by (subst divide_out_aux.simps)
(auto elim: dvdE simp: multiplicity_times_same
multiplicity_unit_left
not_dvd_imp_multiplicity_0)
qed (auto simp: divide_out_aux.simps multiplicity_unit_left
not_dvd_imp_multiplicity_0)
qed
lemma divide_out_code [code]: "divide_out p x = divide_out_aux p (x, 0)"
by (simp add: divide_out_aux_correct divide_out_def)
lemma multiplicity_code [code]: "multiplicity p x = snd (divide_out_aux
p (x, 0))"
by (simp add: divide_out_aux_correct)
Manuel
Last updated: Nov 21 2024 at 12:39 UTC