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"
by(simp_all add: inf_enat_def)

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


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)"
by(simp add: lmerge_def)

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))"
by(rule llist.expand)(simp_all add: lhd_lmerge ltl_lmerge)

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)"
by(simp add: monotone_lmerge[simplified])

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

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)"
by(simp add: mcont_lmerge[simplified])

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

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])
  qed(simp_all add: bot_enat_def[symmetric])
qed(simp_all add: bot_enat_def[symmetric])

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)"
by(auto simp add: smooth_def)

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"
by(auto simp add: smooth_def prime_dvd_mult_iff)

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)" 
    by(simp_all add: monotone_def)

  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"
by(rule the_equality)(simp_all add: hamming_smooth lsorted_ldistinct_lset_unique)

end