# Theory Hamming_Stream

```(*  Title:       Hamming_Stream.thy
Author:      Andreas Lochbihler, ETH Zurich
*)

section ‹The Hamming stream defined as a least fixpoint›

theory Hamming_Stream imports
"../Coinductive_List"
"HOL-Computational_Algebra.Primes"
begin

lemma infinity_inf_enat [simp]:
fixes n :: enat
shows "∞ ⊓ n = n" "n ⊓ ∞ = n"

lemma eSuc_inf_eSuc [simp]: "eSuc n ⊓ eSuc m = eSuc (n ⊓ m)"

lemma if_pull2: "(if b then f x x' else f y y') = f (if b then x else y) (if b then x' else y')"
by simp

context ord begin

primcorec lmerge :: "'a llist ⇒ 'a llist ⇒ 'a llist"
where
"lmerge xs ys =
(case xs of LNil ⇒ LNil | LCons x xs' ⇒
case ys of LNil ⇒ LNil | LCons y ys' ⇒
if lhd xs < lhd ys then LCons x (lmerge xs' ys)
else LCons y (if lhd ys < lhd xs then lmerge xs ys' else lmerge xs' ys'))"

lemma lnull_lmerge [simp]: "lnull (lmerge xs ys) ⟷ (lnull xs ∨ lnull ys)"

lemma lmerge_eq_LNil_iff: "lmerge xs ys = LNil ⟷ (xs = LNil ∨ ys = LNil)"
using lnull_lmerge unfolding lnull_def .

lemma lhd_lmerge: "⟦ ¬ lnull xs; ¬ lnull ys ⟧ ⟹ lhd (lmerge xs ys) = (if lhd xs < lhd ys then lhd xs else lhd ys)"
by(auto split: llist.split)

lemma ltl_lmerge:
"⟦ ¬ lnull xs; ¬ lnull ys ⟧ ⟹
ltl (lmerge xs ys) =
(if lhd xs < lhd ys then lmerge (ltl xs) ys
else if lhd ys < lhd xs then lmerge xs (ltl ys)
else lmerge (ltl xs) (ltl ys))"
by(auto split: llist.split)

declare lmerge.sel [simp del]

lemma lmerge_simps:
"lmerge (LCons x xs) (LCons y ys) =
(if x < y then LCons x (lmerge xs (LCons y ys))
else if y < x then LCons y (lmerge (LCons x xs) ys)
else LCons y (lmerge xs ys))"

lemma lmerge_LNil [simp]:
"lmerge LNil ys = LNil"
"lmerge xs LNil = LNil"
by simp_all

lemma lprefix_lmergeI:
"⟦ lprefix xs xs'; lprefix ys ys' ⟧
⟹ lprefix (lmerge xs ys) (lmerge xs' ys')"
by(coinduction arbitrary: xs xs' ys ys')(fastforce simp add: lhd_lmerge ltl_lmerge dest: lprefix_lhdD lprefix_lnullD simp add: not_lnull_conv split: if_split_asm)

lemma [partial_function_mono]:
assumes F: "mono_llist F" and G: "mono_llist G"
shows "mono_llist (λf. lmerge (F f) (G f))"
by(blast intro: monotoneI lprefix_lmergeI monotoneD[OF F] monotoneD[OF G])

lemma in_lset_lmergeD: "x ∈ lset (lmerge xs ys) ⟹ x ∈ lset xs ∨ x ∈ lset ys"
by(induct zs≡"lmerge xs ys" arbitrary: xs ys rule: llist_set_induct)(auto simp add: lhd_lmerge ltl_lmerge split: if_split_asm dest: in_lset_ltlD)

lemma lset_lmerge: "lset (lmerge xs ys) ⊆ lset xs ∪ lset ys"
by(auto dest: in_lset_lmergeD)

lemma lfinite_lmergeD: "lfinite (lmerge xs ys) ⟹ lfinite xs ∨ lfinite ys"
by(induct zs≡"lmerge xs ys" arbitrary: xs ys rule: lfinite_induct)(fastforce simp add: ltl_lmerge if_pull2 split: if_split_asm)+

lemma fixes F
defines "F ≡ λlmerge (xs, ys). case xs of LNil ⇒ LNil | LCons x xs' ⇒ case ys of LNil ⇒ LNil | LCons y ys' ⇒ (if x < y then LCons x (curry lmerge xs' ys) else if y < x then LCons y (curry lmerge xs ys') else LCons y (curry lmerge xs' ys'))"
shows lmerge_conv_fixp: "lmerge ≡ curry (ccpo.fixp (fun_lub lSup) (fun_ord lprefix) F)" (is "?lhs ≡ ?rhs")
and lmerge_mono: "mono_llist (λlmerge. F lmerge xs)" (is "?mono xs")
proof(intro eq_reflection ext)
show mono: "⋀xs. ?mono xs" unfolding F_def by(tactic ‹Partial_Function.mono_tac @{context} 1›)
fix xs ys
show "lmerge xs ys = ?rhs xs ys"
proof(coinduction arbitrary: xs ys)
case Eq_llist thus ?case
by(subst (1 3 4) llist.mono_body_fixp[OF mono])(auto simp add: F_def lmerge_simps split: llist.split)
qed
qed

lemma monotone_lmerge: "monotone (rel_prod lprefix lprefix) lprefix (case_prod lmerge)"
apply(rule llist.fixp_preserves_mono2[OF lmerge_mono lmerge_conv_fixp])
apply(erule conjE|rule allI conjI cont_intro|simp|erule allE, erule llist.mono2mono)+
done

lemma mono2mono_lmerge1 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_lmerge1: "monotone lprefix lprefix (λxs. lmerge xs ys)"

lemma mono2mono_lmerge2 [THEN llist.mono2mono, cont_intro, simp]:
shows monotone_lmerge2: "monotone lprefix lprefix (λys. lmerge xs ys)"

lemma mcont_lmerge: "mcont (prod_lub lSup lSup) (rel_prod lprefix lprefix) lSup lprefix (case_prod lmerge)"
apply(rule llist.fixp_preserves_mcont2[OF lmerge_mono lmerge_conv_fixp])
apply(erule conjE|rule allI conjI cont_intro|simp|erule allE, erule llist.mcont2mcont)+
done

lemma mcont2mcont_lmerge1 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_lmerge1: "mcont lSup lprefix lSup lprefix (λxs. lmerge xs ys)"

lemma mcont2mcont_lmerge2 [THEN llist.mcont2mcont, cont_intro, simp]:
shows mcont_lmerge2: "mcont lSup lprefix lSup lprefix (λys. lmerge xs ys)"

lemma lfinite_lmergeI [simp]: "⟦ lfinite xs; lfinite ys ⟧ ⟹ lfinite (lmerge xs ys)"
proof(induction arbitrary: ys rule: lfinite_induct)
case (LCons xs)
from LCons.prems LCons.hyps LCons.IH
show ?case by induct(clarsimp simp add: not_lnull_conv lmerge_simps)+
qed simp

lemma linfinite_lmerge [simp]: "⟦ ¬ lfinite xs; ¬ lfinite ys ⟧ ⟹ ¬ lfinite (lmerge xs ys)"
by(auto dest: lfinite_lmergeD)

lemma llength_lmerge_above: "llength xs ⊓ llength ys ≤ llength (lmerge xs ys)"
proof(induction xs arbitrary: ys)
case (LCons x xs)
show ?case
proof(induct ys)
case LCons thus ?case using LCons.IH
by(fastforce simp add: bot_enat_def[symmetric] lmerge_simps le_infI1 le_infI2 intro: order_trans[rotated])

end

context linorder begin

lemma in_lset_lmergeI1:
"⟦ x ∈ lset xs; lsorted xs; ¬ lfinite ys; ∃y∈lset ys. x ≤ y ⟧
⟹ x ∈ lset (lmerge xs ys)"
proof(induction arbitrary: ys rule: lset_induct)
case (find xs)
then obtain y where "y ∈ lset ys" "x ≤ y" by blast
thus ?case by induct(auto simp add: lmerge_simps not_less)
next
case (step x' xs)
then obtain y where "y ∈ lset ys" "x ≤ y" by blast
moreover from ‹lsorted (LCons x' xs)› ‹x ∈ lset xs› ‹x ≠ x'›
have "x' < x" "lsorted xs" by(auto simp add: lsorted_LCons)
ultimately show ?case using ‹¬ lfinite ys›
by induct(auto 4 3 simp add: lmerge_simps ‹x ≠ x'› not_less intro: step.IH dest: in_lset_lmergeD)
qed

lemma in_lset_lmergeI2:
"⟦ x ∈ lset ys; lsorted ys; ¬ lfinite xs; ∃y∈lset xs. x ≤ y ⟧
⟹ x ∈ lset (lmerge xs ys)"
proof(induction arbitrary: xs rule: lset_induct)
case (find ys)
then obtain y where "y ∈ lset xs" "x ≤ y" by blast
thus ?case by induct(auto simp add: lmerge_simps not_less)
next
case (step x' ys)
then obtain y where "y ∈ lset xs" "x ≤ y" by blast
moreover from ‹lsorted (LCons x' ys)› ‹x ∈ lset ys› ‹x ≠ x'›
have "x' < x" "lsorted ys" by(auto simp add: lsorted_LCons)
ultimately show ?case using ‹¬ lfinite xs›
by induct(auto 4 3 simp add: lmerge_simps ‹x ≠ x'› not_less intro: step.IH dest: in_lset_lmergeD)
qed

lemma lsorted_lmerge: "⟦ lsorted xs; lsorted ys ⟧ ⟹ lsorted (lmerge xs ys)"
proof(coinduction arbitrary: xs ys)
case (lsorted xs ys)
have ?lhd using lsorted
by(auto 4 3 simp add: not_lnull_conv lsorted_LCons lhd_lmerge ltl_lmerge dest!: in_lset_lmergeD)
moreover have ?ltl using lsorted by(auto simp add: ltl_lmerge intro: lsorted_ltlI)
ultimately show ?case ..
qed

lemma ldistinct_lmerge:
"⟦ lsorted xs; lsorted ys; ldistinct xs; ldistinct ys ⟧
⟹ ldistinct (lmerge xs ys)"
by(coinduction arbitrary: xs ys)(auto 4 3 simp add: lhd_lmerge ltl_lmerge not_lnull_conv lsorted_LCons not_less dest!: in_lset_lmergeD dest: order.antisym)

end

partial_function (llist) hamming' :: "unit ⇒ nat llist"
where
"hamming' _ =
LCons 1 (lmerge (lmap ((*) 2) (hamming' ())) (lmerge (lmap ((*) 3) (hamming' ())) (lmap ((*) 5) (hamming' ()))))"

definition hamming :: "nat llist"
where "hamming = hamming' ()"

lemma lnull_hamming [simp]: "¬ lnull hamming"
unfolding hamming_def by(subst hamming'.simps) simp

lemma hamming_eq_LNil_iff [simp]: "hamming = LNil ⟷ False"
using lnull_hamming unfolding lnull_def by simp

lemma lhd_hamming [simp]: "lhd hamming = 1"
unfolding hamming_def by(subst hamming'.simps) simp

lemma ltl_hamming [simp]:
"ltl hamming = lmerge (lmap ((*) 2) hamming) (lmerge (lmap ((*) 3) hamming) (lmap ((*) 5) hamming))"
unfolding hamming_def by(subst hamming'.simps) simp

lemma hamming_unfold:
"hamming = LCons 1 (lmerge (lmap ((*) 2) hamming) (lmerge (lmap ((*) 3) hamming) (lmap ((*) 5) hamming)))"
by(rule llist.expand) simp_all

definition smooth :: "nat ⇒ bool"
where "smooth n ⟷ (∀p. prime p ⟶ p dvd n ⟶ p ≤ 5)"

lemma smooth_0 [simp]: "¬ smooth 0"
by(auto simp add: smooth_def intro: exI[where x=7])

lemma smooth_Suc0 [simp]: "smooth (Suc 0)"

lemma smooth_gt0: "smooth n ⟹ n > 0"
by(cases n) simp_all

lemma smooth_ge_Suc0: "smooth n ⟹ n ≥ Suc 0"
by(cases n) simp_all

lemma prime_nat_dvdD: "prime p ⟹ (n :: nat) dvd p ⟹ n = 1 ∨ n = p"
unfolding prime_nat_iff by simp

lemma smooth_times [simp]: "smooth (x * y) ⟷ smooth x ∧ smooth y"

lemma smooth2 [simp]: "smooth 2"
by(auto simp add: smooth_def dest: prime_nat_dvdD[of 2, simplified])

lemma smooth3 [simp]: "smooth 3"
by(auto simp add: smooth_def dest: prime_nat_dvdD[of 3, simplified])

lemma smooth5 [simp]: "smooth 5"
by(auto simp add: smooth_def dest: prime_nat_dvdD[of 5, simplified])

lemma hamming_in_smooth: "lset hamming ⊆ {n. smooth n}"
unfolding hamming_def by(induct rule: hamming'.fixp_induct)(auto 6 6 dest: in_lset_lmergeD)

lemma lfinite_hamming [simp]: "¬ lfinite hamming"
proof
assume "lfinite hamming"
then obtain n where n: "llength hamming = enat n" unfolding lfinite_conv_llength_enat by fastforce
have "llength (lmap ((*) 3) hamming) ⊓ llength (lmap ((*) 5) hamming) ≤ llength (lmerge (lmap ((*) 3) hamming) (lmap ((*) 5) hamming))"
by(rule llength_lmerge_above)
hence "llength hamming ≤ …" by simp
moreover have "llength (lmap ((*) 2) hamming) ⊓ … ≤
llength (lmerge (lmap ((*) 2) hamming) (lmerge (lmap ((*) 3) hamming) (lmap ((*) 5) hamming)))"
by(rule llength_lmerge_above)
ultimately have "llength hamming ≤ …" by(simp add: inf.absorb1)
also from n have "… < enat n"
by(subst (asm) hamming_unfold)(cases n, auto simp add: zero_enat_def[symmetric] eSuc_enat[symmetric])
finally show False unfolding n by simp
qed

lemma lsorted_hamming [simp]: "lsorted hamming"
and ldistinct_hamming [simp]: "ldistinct hamming"
proof -
have "lsorted hamming ∧ ldistinct hamming ∧ lset hamming ⊆ {1..}"
unfolding hamming_def
by(induct rule: hamming'.fixp_induct)(auto 6 6 simp add: lsorted_LCons dest: in_lset_lmergeD intro: smooth_ge_Suc0 lsorted_lmerge lsorted_lmap monotoneI ldistinct_lmerge inj_onI)
thus "lsorted hamming" "ldistinct hamming" by simp_all
qed

lemma smooth_hamming:
assumes "smooth n"
shows "n ∈ lset hamming"
using assms
proof(induction n rule: less_induct)
have [simp]:
"monotone (≤) (≤) ((*) 2 :: nat ⇒ nat)"
"monotone (≤) (≤) ((*) 3 :: nat ⇒ nat)"
"monotone (≤) (≤) ((*) 5 :: nat ⇒ nat)"

case (less n)
show ?case
proof(cases "n > 1")
case False
moreover from ‹smooth n› have "n ≠ 0" by(rule contrapos_pn) simp
ultimately have "n = 1" by(simp)
thus ?thesis by(subst hamming_unfold) simp
next
case True
hence "∃p. prime p ∧ p dvd n" by(metis less_numeral_extra(4) prime_factor_nat)
with ‹smooth n› obtain p where "prime p" "p dvd n" "p ≤ 5" by(auto simp add: smooth_def)
from ‹p dvd n› obtain n' where n: "n = p * n'" by(auto simp add: dvd_def)
with ‹smooth n› ‹prime p› have "smooth n'" by(simp add: smooth_def)
with ‹prime p› n have "n' < n" by(simp add: smooth_gt0 prime_gt_Suc_0_nat)
hence n': "n' ∈ lset hamming" using ‹smooth n'› by(rule less.IH)

from ‹p ≤ 5› have "p = 0 ∨ p = 1 ∨ p = 2 ∨ p = 3 ∨ p = 4 ∨ p = 5"
by presburger
with ‹prime p› have "p = 2 ∨ p = 3 ∨ p = 5" by auto
thus ?thesis
proof(elim disjE)
assume "p = 2"
with n n' show ?thesis
by(subst hamming_unfold)(simp_all add: in_lset_lmergeI1 not_less lsorted_lmap bexI[where x="n'"] bexI[where x="3*n'"])
next
assume "p = 3"
moreover with n ‹smooth n'› have "2 * n' < n" by(simp add: smooth_gt0)
hence "2 * n' ∈ lset hamming" by(rule less.IH)(simp add: ‹smooth n'›)
ultimately show ?thesis using n n'
by(subst hamming_unfold)(auto 4 4 simp add: not_less lsorted_lmap lsorted_lmerge intro: in_lset_lmergeI1 in_lset_lmergeI2 bexI[where x="4*n'"] bexI[where x="5*n'"])
next
assume "p = 5"
moreover with n ‹smooth n'› have "2 * (2 * n') < n" by(simp add: smooth_gt0)
hence "2 * (2 * n') ∈ lset hamming" by(rule less.IH)(simp only: smooth_times smooth2 ‹smooth n'› simp_thms)
moreover from ‹p = 5› n ‹smooth n'› have "3 * n' < n" by(simp add: smooth_gt0)
hence "3 * n' ∈ lset hamming" by(rule less.IH)(simp add: ‹smooth n'›)
ultimately show ?thesis using n n'
by(subst hamming_unfold)(auto 4 4 simp add: lsorted_lmap lsorted_lmerge intro: in_lset_lmergeI2 bexI[where x="9*n'"] bexI[where x="8 * n'"])
qed
qed
qed

corollary hamming_smooth: "lset hamming = {n. smooth n}"
using hamming_in_smooth by(blast intro: smooth_hamming)

lemma hamming_THE:
"(THE xs. lsorted xs ∧ ldistinct xs ∧ lset xs = {n. smooth n}) = hamming"