HuanSun (Dec 15 2022 at 13:11): HuanSun (Dec 15 2022 at 13:11):I want a function to convert nat to string and satisfies that n1 ≠ n2 ⟹ f n1 ≠ f n2 . A question in stackoverflow have provided serval functions that convert a nat to its corresponding string. However, It seems not easy to prove the property n1 ≠ n2 ⟹ f n1 ≠ f n2 . So is there a simple proof for functions in stackoverflow or just a easier way to define a function that satisfies n1 ≠ n2 ⟹ f n1 ≠ f n2 ?
Adrián Löwenberg (Feb 16 2023 at 09:48):My quick attempt at this:
theory NatToString imports Main
begin
fun char_of_digit :: "nat ⇒ char" where
"char_of_digit n = char_of (n + 48)"
fun f :: "nat ⇒ string" where
"f n = (if n < 10 then [char_of_digit n] else (f (n div 10) @ [(char_of_digit (n mod 10))]))"
lemma nat_notequal_mod_10:
assumes "(n::nat) ≠ m" shows "(n div 10 ≠ m div 10 ∨ n mod 10 ≠ m mod 10 )"
proof -
{
assume "n div 10 = m div 10 ∧ n mod 10 = m mod 10"
hence "n div 10 * 10 + n mod 10 = m div 10 * 10 + m mod 10" by presburger
hence "n = m" by presburger
with assms have False by blast
}
thus ?thesis by blast
qed
lemma "n ≠ m ⟹ f n ≠ f m"
proof (induction arbitrary: n rule: f.induct)
case (1 m)
{
assume "m div 10 ≠ n div 10"
with 1(1) have ?case by auto
} note case1 = this
{
assume "m mod 10 ≠ n mod 10"
hence ?case by auto
} note case2 = this
{
assume "m div 10 = n div 10" "m mod 10 = n mod 10"
hence False using nat_notequal_mod_10 ‹n ≠ m› by simp
} note case3 = this
from case1 case2 case3 show ?case by blast
qed
end
``
Last updated: Apr 18 2024 at 16:19 UTC