Theory Union

section ‹The union of classes\label{s:union}›

theory Union
  imports R1_BC TOTAL_CONS
begin

text ‹None of the inference types introduced in this chapter are closed
under union of classes. For all inference types except FIN this follows from
@{thm[source] "U0_V0_not_in_BC"}.›

lemma not_closed_under_union:
  "∀ℐ∈{CP, TOTAL, CONS, LIM, BC}. U⇩0 ∈ ℐ ∧ V⇩0 ∈ ℐ ∧ U⇩0 ∪ V⇩0 ∉ ℐ"
  using U0_in_CP U0_in_NUM V0_in_FIN
    FIN_subseteq_CP
    NUM_subseteq_TOTAL
    CP_subseteq_TOTAL
    TOTAL_subseteq_CONS
    CONS_subseteq_Lim
    Lim_subseteq_BC
    U0_V0_not_in_BC
  by blast

text ‹In order to show the analogous result for FIN consider the
classes $\{0^\infty\}$ and $\{0^n10^\infty \mid n \in \mathbb{N}\}$. The
former can be learned finitely by a strategy that hypothesizes $0^\infty$ for
every input. The latter can be learned finitely by a strategy that waits for
the 1 and hypothesizes the only function in the class with a 1 at that
position. However, the union of both classes is not in FIN. This is because
any FIN strategy has to hypothesize $0^\infty$ on some prefix of the form
$0^n$. But the strategy then fails for the function $0^n10^\infty$.›

lemma singleton_in_FIN: "f ∈ ℛ ⟹ {f} ∈ FIN"
proof -
  assume "f ∈ ℛ"
  then obtain i where i: "φ i = f"
    using phi_universal by blast
  define s :: partial1 where "s = (λ_. Some (Suc i))"
  then have "s ∈ ℛ"
    using const_in_Prim1[of "Suc i"] by simp
  have "learn_fin φ {f} s"
  proof (intro learn_finI)
    show "environment φ {f} s"
      using ‹s ∈ ℛ› ‹f ∈ ℛ› by (simp add: phi_in_P2)
    show "∃i n⇩0. φ i = g ∧ (∀n<n⇩0. s (g ▹ n) ↓= 0) ∧ (∀n≥n⇩0. s (g ▹ n) ↓= Suc i)"
      if "g ∈ {f}" for g
    proof -
      from that have "g = f" by simp
      then have "φ i = g"
        using i by simp
      moreover have "∀n<0. s (g ▹ n) ↓= 0" by simp
      moreover have "∀n≥0. s (g ▹ n) ↓= Suc i"
        using s_def by simp
      ultimately show ?thesis by auto
    qed
  qed
  then show "{f} ∈ FIN" using FIN_def by auto
qed

definition U_single :: "partial1 set" where
  "U_single ≡ {(λx. if x = n then Some 1 else Some 0)| n. n ∈ UNIV}"

lemma U_single_in_FIN: "U_single ∈ FIN"
proof -
  define psi :: partial2 where "psi ≡ λn x. if x = n then Some 1 else Some 0"
  have "psi ∈ ℛ⇧2"
    using psi_def by (intro R2I[of "Cn 2 r_not [r_eq]"]) auto
  define s :: partial1 where
    "s ≡ λb. if findr b ↓= e_length b then Some 0 else Some (Suc (the (findr b)))"
  have "s ∈ ℛ"
  proof (rule R1I)
    let ?r = "Cn 1 r_ifeq [r_findr, r_length, Z, Cn 1 S [r_findr]]"
    show "recfn 1 ?r" by simp
    show "total ?r" by auto
    show "eval ?r [b] = s b" for b
    proof -
      let ?b = "the (findr b)"
      have "eval ?r [b] = (if ?b = e_length b then Some 0 else Some (Suc (?b)))"
        using findr_total by simp
      then show "eval ?r [b] = s b"
        by (metis findr_total option.collapse option.inject s_def)
    qed
  qed
  have "U_single ⊆ ℛ"
  proof
    fix f
    assume "f ∈ U_single"
    then obtain n where "f = (λx. if x = n then Some 1 else Some 0)"
      using U_single_def by auto
    then have "f = psi n"
      using psi_def by simp
    then show "f ∈ ℛ"
      using ‹psi ∈ ℛ⇧2› by simp
  qed
  have "learn_fin psi U_single s"
  proof (rule learn_finI)
    show "environment psi U_single s"
      using ‹psi ∈ ℛ⇧2› ‹s ∈ ℛ› ‹U_single ⊆ ℛ› by simp
    show "∃i n⇩0. psi i = f ∧ (∀n<n⇩0. s (f ▹ n) ↓= 0) ∧ (∀n≥n⇩0. s (f ▹ n) ↓= Suc i)"
      if "f ∈ U_single" for f
    proof -
      from that obtain i where i: "f = (λx. if x = i then Some 1 else Some 0)"
        using U_single_def by auto
      then have "psi i = f"
        using psi_def by simp
      moreover have "∀n<i. s (f ▹ n) ↓= 0"
        using i s_def findr_def by simp
      moreover have "∀n≥i. s (f ▹ n) ↓= Suc i"
      proof (rule allI, rule impI)
        fix n
        assume "n ≥ i"
        let ?e = "init f n"
        have "∃i<e_length ?e. e_nth ?e i ≠ 0"
          using ‹n ≥ i› i by simp
        then have less: "the (findr ?e) < e_length ?e"
          and nth_e: "e_nth ?e (the (findr ?e)) ≠ 0"
          using findr_ex by blast+
        then have "s ?e ↓= Suc (the (findr ?e))"
          using s_def by auto
        moreover have "the (findr ?e) = i"
          using nth_e less i by (metis length_init nth_init option.sel)
        ultimately show "s ?e ↓= Suc i" by simp
      qed
      ultimately show ?thesis by auto
    qed
  qed
  then show "U_single ∈ FIN" using FIN_def by blast
qed

lemma zero_U_single_not_in_FIN: "{0⇧∞} ∪ U_single ∉ FIN"
proof
  assume "{0⇧∞} ∪ U_single ∈ FIN"
  then obtain psi s where learn: "learn_fin psi ({0⇧∞} ∪ U_single) s"
    using FIN_def by blast
  then have "learn_fin psi {0⇧∞} s"
    using learn_fin_closed_subseteq by auto
  then obtain i n⇩0 where i:
    "psi i = 0⇧∞"
    "∀n<n⇩0. s (0⇧∞ ▹ n) ↓= 0"
    "∀n≥n⇩0. s (0⇧∞ ▹ n) ↓= Suc i"
    using learn_finE(2) by blast
  let ?f = "λx. if x = Suc n⇩0 then Some 1 else Some 0"
  have "?f ≠ 0⇧∞" by (metis option.inject zero_neq_one)
  have "?f ∈ U_single"
    using U_single_def by auto
  then have "learn_fin psi {?f} s"
    using learn learn_fin_closed_subseteq by simp
  then obtain j m⇩0 where j:
    "psi j = ?f"
    "∀n<m⇩0. s (?f ▹ n) ↓= 0"
    "∀n≥m⇩0. s (?f ▹ n) ↓= Suc j"
    using learn_finE(2) by blast
  consider
    (less) "m⇩0 < n⇩0" | (eq) "m⇩0 = n⇩0" | (gr) "m⇩0 > n⇩0"
    by linarith
  then show False
  proof (cases)
    case less
    then have "s (0⇧∞▹ m⇩0) ↓= 0"
      using i by simp
    moreover have "0⇧∞ ▹ m⇩0 = ?f ▹ m⇩0"
      using less init_eqI[of m⇩0 ?f "0⇧∞"] by simp
    ultimately have "s (?f ▹ m⇩0) ↓= 0" by simp
    then show False using j by simp
  next
    case eq
    then have "0⇧∞ ▹ m⇩0 = ?f ▹ m⇩0"
      using init_eqI[of m⇩0 ?f "0⇧∞"] by simp
    then have "s (0⇧∞ ▹ m⇩0) = s (?f ▹ m⇩0)" by simp
    then have "i = j"
      using i j eq by simp
    then have "psi i = psi j" by simp
    then show False using ‹?f ≠ 0⇧∞› i j by simp
  next
    case gr
    have "0⇧∞ ▹ n⇩0 = ?f ▹ n⇩0"
      using init_eqI[of n⇩0 ?f "0⇧∞"] by simp
    moreover have "s (0⇧∞ ▹ n⇩0) ↓= Suc i"
      using i by simp
    moreover have "s (?f ▹ n⇩0) ↓= 0"
      using j gr by simp
    ultimately show False by simp
  qed
qed

lemma FIN_not_closed_under_union: "∃U V. U ∈ FIN ∧ V ∈ FIN ∧ U ∪ V ∉ FIN"
proof -
  have "{0⇧∞} ∈ FIN"
    using singleton_in_FIN const_in_Prim1 by simp
  moreover have "U_single ∈ FIN"
    using U_single_in_FIN by simp
  ultimately show ?thesis
    using zero_U_single_not_in_FIN by blast
qed

text ‹In contrast to the inference types, NUM is closed under the union
of classes. The total numberings that exist for each NUM class can be
interleaved to produce a total numbering encompassing the union of the
classes. To define the interleaving, modulo and division by two will be
helpful.›

definition "r_div2 ≡
  r_shrink
   (Pr 1 Z
     (Cn 3 r_ifle
       [Cn 3 r_mul [r_constn 2 2, Cn 3 S [Id 3 0]], Id 3 2, Cn 3 S [Id 3 1], Id 3 1]))"

lemma r_div2_prim [simp]: "prim_recfn 1 r_div2"
  unfolding r_div2_def by simp

lemma r_div2 [simp]: "eval r_div2 [n] ↓= n div 2"
proof -
  let ?p = "Pr 1 Z
    (Cn 3 r_ifle
      [Cn 3 r_mul [r_constn 2 2, Cn 3 S [Id 3 0]], Id 3 2, Cn 3 S [Id 3 1], Id 3 1])"
  have "eval ?p [i, n] ↓= min (n div 2) i" for i
    by (induction i) auto
  then have "eval ?p [n, n] ↓= n div 2" by simp
  then show ?thesis unfolding r_div2_def by simp
qed

definition "r_mod2 ≡ Cn 1 r_sub [Id 1 0, Cn 1 r_mul [r_const 2, r_div2]]"

lemma r_mod2_prim [simp]: "prim_recfn 1 r_mod2"
  unfolding r_mod2_def by simp

lemma r_mod2 [simp]: "eval r_mod2 [n] ↓= n mod 2"
  unfolding r_mod2_def using Rings.semiring_modulo_class.minus_mult_div_eq_mod
  by auto

lemma NUM_closed_under_union:
  assumes "U ∈ NUM" and "V ∈ NUM"
  shows "U ∪ V ∈ NUM"
proof -
  from assms obtain psi_u psi_v where
    psi_u: "psi_u ∈ ℛ⇧2" "⋀f. f ∈ U ⟹ ∃i. psi_u i = f" and
    psi_v: "psi_v ∈ ℛ⇧2" "⋀f. f ∈ V ⟹ ∃i. psi_v i = f"
    by fastforce
  define psi where "psi ≡ λi. if i mod 2 = 0 then psi_u (i div 2) else psi_v (i div 2)"
  from psi_u(1) obtain u where u: "recfn 2 u" "total u" "⋀x y. eval u [x, y] = psi_u x y"
    by auto
  from psi_v(1) obtain v where v: "recfn 2 v" "total v" "⋀x y. eval v [x, y] = psi_v x y"
    by auto
  let ?r_psi = "Cn 2 r_ifz
    [Cn 2 r_mod2 [Id 2 0],
     Cn 2 u [Cn 2 r_div2 [Id 2 0], Id 2 1],
     Cn 2 v [Cn 2 r_div2 [Id 2 0], Id 2 1]]"
  show ?thesis
  proof (rule NUM_I[of psi])
    show "psi ∈ ℛ⇧2"
    proof (rule R2I)
      show "recfn 2 ?r_psi"
        using u(1) v(1) by simp
      show "eval ?r_psi [x, y] = psi x y" for x y
        using u v psi_def prim_recfn_total R2_imp_total2[OF psi_u(1)]
          R2_imp_total2[OF psi_v(1)]
        by simp
      moreover have "psi x y ↓" for x y
        using psi_def psi_u(1) psi_v(1) by simp
      ultimately show "total ?r_psi"
        using ‹recfn 2 ?r_psi› totalI2 by simp
    qed
    show "∃i. psi i = f" if "f ∈ U ∪ V" for f
    proof (cases "f ∈ U")
      case True
      then obtain j where "psi_u j = f"
        using psi_u(2) by auto
      then have "psi (2 * j) = f"
        using psi_def by simp
      then show ?thesis by auto
    next
      case False
      then have "f ∈ V"
        using that by simp
      then obtain j where "psi_v j = f"
        using psi_v(2) by auto
      then have "psi (Suc (2 * j)) = f"
        using psi_def by simp
      then show ?thesis by auto
    qed
  qed
qed

end