Theory Recursion-Theory-I.PRecFinSet

(*  Title:       Primitive recursive coding of finite sets
    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008
    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>
*)

section ‹Finite sets›

theory PRecFinSet
imports PRecFun
begin

text ‹
  We introduce a particular mapping nat_to_set› from natural
  numbers to finite sets of natural numbers and a particular mapping
  set_to_nat› from finite sets of natural numbers to natural
  numbers.  See cite"Rogers" and cite"Soare" for more information.
›

definition
  c_in :: "nat  nat  nat" where
  "c_in = (λ x u. (u div (2 ^ x)) mod 2)"

lemma c_in_is_pr: "c_in  PrimRec2"
proof -
  from mod_is_pr power_is_pr div_is_pr have "(λ x u. (u div (2 ^ x)) mod 2)  PrimRec2" by prec
  with c_in_def show ?thesis by auto
qed

definition
  nat_to_set :: "nat  nat set" where
  "nat_to_set u  {x. 2^x  u  c_in x u = 1}"

lemma c_in_upper_bound: "c_in x u = 1  2 ^ x  u"
proof -
  assume A: "c_in x u = 1"
  then have S1: "(u div (2^x)) mod 2 = 1" by (unfold c_in_def)
  then have S2: "u div (2^x) > 0" by arith
  show ?thesis
  proof (rule ccontr)
    assume "¬ 2 ^ x  u"
    then have "u < 2^x" by auto
    then have "u div (2^x) = 0" by (rule div_less)
    with S2 show False by auto
  qed
qed

lemma nat_to_set_upper_bound: "x  nat_to_set u  2 ^ x  u" by (simp add: nat_to_set_def)

lemma x_lt_2_x: "x < 2 ^ x"
  by (rule less_exp)

lemma nat_to_set_upper_bound1: "x  nat_to_set u  x < u"
proof -
  assume "x  nat_to_set u"
  then have S1: "2 ^ x  u" by (simp add: nat_to_set_def)
  have S2: "x < 2 ^ x" by (rule x_lt_2_x)
  from S2 S1 show ?thesis
    by (rule less_le_trans)
qed

lemma nat_to_set_upper_bound2: "nat_to_set u  {i. i < u}"
proof -
  from nat_to_set_upper_bound1 show ?thesis by blast
qed

lemma nat_to_set_is_finite: "finite (nat_to_set u)"
proof -
  have S1: "finite {i. i<u}"
  proof -
    let ?B = "{i. i<u}"
    let ?f = "(λ (x::nat). x)"
    have "?B = ?f ` ?B" by auto
    then show "finite ?B" by (rule nat_seg_image_imp_finite)
  qed
  have S2: "nat_to_set u  {i. i<u}" by (rule nat_to_set_upper_bound2)
  from S2 S1 show ?thesis by (rule finite_subset)
qed

lemma x_in_u_eq: "(x  nat_to_set u) = (c_in x u = 1)" by (auto simp add: nat_to_set_def c_in_upper_bound)

definition
  log2 :: "nat  nat" where
  "log2 = (λ x. Least(%z. x < 2^(z+1)))"

lemma log2_at_0: "log2 0 = 0"
proof -
  let ?v = "log2 0"
  have S1: "0  ?v" by auto
  have S2: "?v = Least(%(z::nat). (0::nat)<2^(z+1))" by (simp add: log2_def)
  have S3: "(0::nat)<2^(0+1)" by auto
  from S3 have S4: "Least(%(z::nat). (0::nat)<2^(z+1))  0" by (rule Least_le)
  from S2 S4 have S5: "?v  0" by auto
  from S1 S5 have S6: "?v = 0" by auto
  thus ?thesis by auto
qed

lemma log2_at_1: "log2 1 = 0"
proof -
  let ?v = "log2 1"
  have S1: "0  ?v" by auto
  have S2: "?v = Least(%(z::nat). (1::nat)<2^(z+1))" by (simp add: log2_def)
  have S3: "(1::nat)<2^(0+1)" by auto
  from S3 have S4: "Least(%(z::nat). (1::nat)<2^(z+1))  0" by (rule Least_le)
  from S2 S4 have S5: "?v  0" by auto
  from S1 S5 have S6: "?v = 0" by auto
  thus ?thesis by auto
qed

lemma log2_le: "x > 0  2 ^ log2 x  x"
proof -
  assume A: "x > 0"
  show ?thesis
  proof (cases)
    assume A1: "log2 x = 0"
    with A show ?thesis by auto
  next
    assume A1: "log2 x  0"
    then have S1: "log2 x > 0" by auto
    define y where "y = log2 x - 1"
    from S1 y_def have S2: "log2 x = y + 1" by auto
    then have S3: "y < log2 x" by auto
    have "2^(y+1)  x"
    proof (rule ccontr)
      assume A2: "¬ 2^(y+1)  x" then have "x < 2^(y+1)" by auto
      then have "log2 x  y" by (simp add: log2_def Least_le)
      with S3 show False by auto
   qed
   with S2 show ?thesis by auto
  qed
qed

lemma log2_gt: "x < 2 ^ (log2 x + 1)"
proof -
  have "x < 2^x" by (rule x_lt_2_x)
  then have S1: "x < 2^(x+1)"
    by (simp add: numeral_2_eq_2)
  define y where "y = x"
  from S1 y_def have S2: "x < 2^(y+1)" by auto
  let ?P = "λ z. x < 2^(z+1)"
  from S2 have S3: "?P y" by auto
  then have S4: "?P (Least ?P)" by (rule LeastI)
  from log2_def have S5: "log2 x = Least ?P" by (unfold log2_def, auto)
  from S4 S5 show ?thesis by auto
qed

lemma x_div_x: "x > 0  (x::nat) div x = 1" by auto
lemma div_ge: "(k::nat)  m div n  n*k  m"
proof -
  assume A: "k  m div n"
  have S1: "n * (m div n) + m mod n = m" by (rule mult_div_mod_eq)
  have S2: "0  m mod n" by auto
  from S1 S2 have S3: "n * (m div n)  m" by arith
  from A have S4: "n * k   n * (m div n)" by auto
  from S4 S3 show ?thesis by (rule order_trans)
qed
lemma div_lt: "m < n*k  m div n < (k::nat)"
proof -
  assume A: "m < n*k"
  show ?thesis
  proof (rule ccontr)
    assume "¬ m div n < k"
    then have S1: "k  m div n" by auto
    then have S2: "n*k  m" by (rule div_ge)
    with A show False by auto
  qed
qed

lemma log2_lm1: "u > 0  u div 2 ^ (log2 u) = 1"
proof -
  assume A: "u > 0"
  then have S1: "2^(log2 u)  u" by (rule log2_le)
  have S2: "u < 2^(log2 u+1)" by (rule log2_gt)
  then have S3: "u < (2^log2 u)*2" by simp
  have "(2::nat) > 0" by simp
  then have "(2::nat)^log2 u > 0" by simp
  then have S4: "(2::nat)^log2 u div 2^log2 u = 1" by auto
  from S1 have S5: "(2::nat)^log2 u div 2^log2 u   u div 2^log2 u" by (rule div_le_mono)
  with S4 have S6: "1  u div 2^log2 u" by auto
  from S3 have S7: "u div 2^log2 u < 2" by (rule div_lt)
  from S6 S7 show ?thesis by auto
qed

lemma log2_lm2: "u > 0  c_in (log2 u) u = 1"
proof -
  assume A: "u > 0"
  then have S1: "u div 2 ^ (log2 u) = 1" by (rule log2_lm1)
  have "c_in (log2 u) u = (u div 2 ^ (log2 u)) mod 2" by (simp add: c_in_def)
  also from S1 have " = 1 mod 2" by simp
  also have " = 1" by auto
  finally show ?thesis by auto
qed

lemma log2_lm3: "log2 u < x  c_in x u = 0"
proof -
  assume A: "log2 u < x"
  then have S1: "(log2 u)+1  x" by auto
  have S2: "1  (2::nat)" by auto
  from S1 S2 have S3: "(2::nat)^ ((log2 u)+1)  2^x" by (rule power_increasing)
  have S4: "u < (2::nat)^ ((log2 u)+1)" by (rule log2_gt)
  from S3 S4 have S5: "u < 2^x" by auto
  then have S6: "u div 2^x = 0" by (rule div_less)
  have "c_in x u = (u div 2^x) mod 2" by (simp add: c_in_def)
  also from S6 have " = 0 mod 2" by simp
  also have " = 0" by auto
  finally have ?thesis by auto
  thus ?thesis by auto
qed

lemma log2_lm4: "c_in x u = 1  x  log2 u"
proof -
  assume A: "c_in x u = 1"
  show ?thesis
  proof (rule ccontr)
    assume "¬ x  log2 u"
    then have S1: "log2 u < x" by auto
    then have S2: "c_in x u = 0" by (rule log2_lm3)
    with A show False by auto
  qed
qed

lemma nat_to_set_lub: "x  nat_to_set u  x  log2 u"
proof -
  assume "x  nat_to_set u"
  then have S1: "c_in x u = 1" by (simp add: x_in_u_eq)
  then show ?thesis by (rule log2_lm4)
qed

lemma log2_lm5: "u > 0  log2 u  nat_to_set u"
proof -
  assume A: "u > 0"
  then have "c_in (log2 u) u = 1" by (rule log2_lm2)
  then show ?thesis by (simp add: x_in_u_eq)
qed

lemma pos_imp_ne: "u > 0  nat_to_set u  {}"
proof -
  assume "u > 0"
  then have "log2 u  nat_to_set u" by (rule log2_lm5)
  thus ?thesis by auto
qed

lemma empty_is_zero: "nat_to_set u = {}  u = 0"
proof (rule ccontr)
  assume A1: "nat_to_set u = {}"
  assume A2: "u  0" then have S1: "u > 0" by auto
  from S1 have "nat_to_set u  {}" by (rule pos_imp_ne)
  with A1 show False by auto
qed

lemma log2_is_max: "u > 0  log2 u = Max (nat_to_set u)"
proof -
  assume A: "u > 0"
  then have S1: "log2 u  nat_to_set u" by (rule log2_lm5)
  define max where "max = Max (nat_to_set u)"
  from A have ne: "nat_to_set u  {}" by (rule pos_imp_ne)
  have finite: "finite (nat_to_set u)" by (rule nat_to_set_is_finite)
  from max_def finite ne have max_in: "max  nat_to_set u" by simp
  from max_in have S2: "c_in max u = 1" by (simp add: x_in_u_eq)
  then have S3: "max  log2 u" by (rule log2_lm4)
  from finite ne S1 max_def have S4: "log2 u  max" by simp
  from S3 S4 max_def show ?thesis by auto
qed

lemma zero_is_empty: "nat_to_set 0 = {}"
proof -
  have S1: "{i. i<(0::nat)} = {}" by blast
  have S2: "nat_to_set 0  {i. i<0}" by (rule nat_to_set_upper_bound2)
  from S1 S2 show ?thesis by auto
qed

lemma ne_imp_pos: "nat_to_set u  {}  u > 0"
proof (rule ccontr)
  assume A1: "nat_to_set u  {}"
  assume "¬ 0 < u" then have "u = 0" by auto
  then have "nat_to_set u = {}" by (simp add: zero_is_empty)
  with A1 show False by auto
qed

lemma div_mod_lm: "y < x  ((u + (2::nat) ^ x) div (2::nat)^y) mod 2 = (u div (2::nat)^y) mod 2"
proof -
  assume y_lt_x: "y < x"
  let ?n = "(2::nat)^y"
  have n_pos: "0 < ?n" by auto
  let ?s = "x-y"
  from y_lt_x have s_pos: "0 < ?s" by auto
  from y_lt_x have S3: "x = y + ?s" by auto
  from S3 have "(2::nat)^x = (2::nat)^(y + ?s)" by auto
  moreover have "(2::nat)^(y +?s) = (2::nat)^y * 2^ ?s" by (rule power_add)
  ultimately have "(2::nat)^x = 2^y * 2^?s" by auto
  then have S4: "u + (2::nat)^x = u + (2::nat)^y * 2^?s" by auto
  from n_pos have S5: "(u + (2::nat)^y * 2^?s) div 2^y = 2^?s + (u div 2^y)" by simp
  from S4 S5 have S6: "(u + (2::nat)^x) div 2^y = 2^?s + (u div 2^y)" by auto
  from s_pos have S8: "?s = (?s - 1) + 1" by auto
  have "(2::nat) ^ ((?s - (1::nat)) + (1::nat)) = (2::nat) ^ (?s - (1::nat)) * 2^1" by (rule power_add)
  with S8 have S9: "(2::nat) ^ ?s = (2::nat) ^ (?s - (1::nat)) * 2" by auto
  then have S10: "2^?s + (u div 2^y) = (u div 2^y) + (2::nat) ^ (?s - (1::nat)) * 2" by auto
  have S11: "((u div 2^y) + (2::nat) ^ (?s - (1::nat)) * 2) mod 2 = (u div 2^y) mod 2" by (rule mod_mult_self1)
  from S6 S10 S11 show ?thesis by auto
qed

lemma add_power: "u < 2^x  nat_to_set (u + 2^x) = nat_to_set u  {x}"
proof -
  assume A: "u < 2^x"
  have log2_is_x: "log2 (u+2^x) = x"
  proof (unfold log2_def, rule Least_equality)
    from A show "u+2^x < 2^(x+1)" by auto
  next
    fix z
    assume A1: "u + 2^x < 2^(z+1)"
    show "x  z"
    proof (rule ccontr)
      assume "¬ x  z"
      then have "z < x" by auto
      then have L1: "z+1  x" by auto
      have L2: "1  (2::nat)" by auto
      from L1 L2 have L3: "(2::nat)^(z+1)  (2::nat)^x" by (rule power_increasing)
      with A1 show False by auto
    qed
  qed
  show ?thesis
  proof (rule subset_antisym)
    show "nat_to_set (u + 2 ^ x)  nat_to_set u  {x}"
    proof fix y
      assume A1: "y  nat_to_set (u + 2 ^ x)"
      show "y  nat_to_set u  {x}"
      proof
        assume "y  {x}" then have S1: "y  x" by auto
        from A1 have "y  log2 (u + 2 ^ x)" by (rule nat_to_set_lub)
        with log2_is_x have "y  x" by auto
        with S1 have y_lt_x: "y < x" by auto
        from A1 have "c_in y (u + 2 ^ x) = 1" by (simp add: x_in_u_eq)
        then have S2: "((u + 2 ^ x) div 2^y) mod 2 = 1" by (unfold c_in_def)
        from y_lt_x have "((u + (2::nat) ^ x) div (2::nat)^y) mod 2 = (u div (2::nat)^y) mod 2" by (rule div_mod_lm)
        with S2 have "(u div 2^y) mod 2 = 1" by auto
        then have "c_in y u = 1" by (simp add: c_in_def)
        then show "y  nat_to_set u" by (simp add: x_in_u_eq)
      qed
    qed
  next
  show "nat_to_set u  {x}  nat_to_set (u + 2 ^ x)"
  proof fix y
    assume A1: "y  nat_to_set u  {x}"
    show "y  nat_to_set (u + 2 ^ x)"
    proof cases
      assume "y  {x}"
      then have "y=x" by auto
      then have "y = log2 (u + 2 ^ x)" by (simp add: log2_is_x)
      then show ?thesis by (simp add: log2_lm5)
    next
      assume y_notin: "y  {x}"
      then have y_ne_x: "y  x" by auto
      from A1 y_notin have y_in: "y  nat_to_set u" by auto
      have y_lt_x: "y < x"
      proof (rule ccontr)
        assume "¬ y < x"
        with y_ne_x have y_gt_x: "x < y" by auto
        have "1 < (2::nat)" by auto
        from y_gt_x this have L1: "(2::nat)^x < 2^y" by (rule power_strict_increasing)
        from y_in have L2: "2^y  u" by (rule nat_to_set_upper_bound)
        from L1 L2 have "(2::nat)^x < u" by arith
        with A show False by auto
      qed
      from y_in have "c_in y u = 1" by (simp add: x_in_u_eq)
      then have S2: "(u div 2^y) mod 2 = 1" by (unfold c_in_def)
      from y_lt_x have "((u + (2::nat) ^ x) div (2::nat)^y) mod 2 = (u div (2::nat)^y) mod 2" by (rule div_mod_lm)
      with S2 have "((u + (2::nat) ^ x)div 2^y) mod 2 = 1" by auto
      then have "c_in y (u + (2::nat) ^ x) = 1" by (simp add: c_in_def)
      then show "y  nat_to_set (u + (2::nat) ^ x)" by (simp add: x_in_u_eq)
    qed
  qed
  qed
qed

theorem nat_to_set_inj: "nat_to_set u = nat_to_set v  u = v"
proof -
  assume A: "nat_to_set u = nat_to_set v"
  let ?P = "λ (n::nat). ( (D::nat set). finite D  card D  n  ( u v. nat_to_set u = D  nat_to_set v = D  u = v))"
  have P_at_0: "?P 0"
  proof fix D show "finite D  card D  0  (u v. nat_to_set u = D  nat_to_set v = D  u = v)"
    proof (rule impI)
      assume A1: "finite D  card D  0"
      from A1 have S1: "finite D" by auto
      from A1 have S2: "card D = 0" by auto
      from S1 S2 have S3: "D = {}" by auto
      show "(u v. nat_to_set u = D  nat_to_set v = D  u = v)"
      proof (rule allI, rule allI) fix u v show "nat_to_set u = D  nat_to_set v = D  u = v"
        proof
          assume A2: " nat_to_set u = D  nat_to_set v = D"
          from A2 have L1: "nat_to_set u = D" by auto
          from A2 have L2: "nat_to_set v = D" by auto
          from L1 S3 have "nat_to_set u = {}" by auto
          then have u_z: "u = 0" by (rule empty_is_zero)
          from L2 S3 have "nat_to_set v = {}" by auto
          then have v_z: "v = 0" by (rule empty_is_zero)
          from u_z v_z show "u=v" by auto
        qed
      qed
    qed
  qed
  have P_at_Suc: " n. ?P n  ?P (Suc n)"
  proof - fix n
    assume A_n: "?P n"
    show "?P (Suc n)"
    proof fix D show "finite D  card D  Suc n  (u v. nat_to_set u = D  nat_to_set v = D  u = v)"
    proof (rule impI)
      assume A1: "finite D  card D  Suc n"
      from A1 have S1: "finite D" by auto
      from A1 have S2: "card D  Suc n" by auto
      show "(u v. nat_to_set u = D  nat_to_set v = D  u = v)"
      proof (rule allI, rule allI, rule impI)
        fix u v
        assume A2: " nat_to_set u = D  nat_to_set v = D"
        from A2 have d_u_d: "nat_to_set u = D" by auto
        from A2 have d_v_d: "nat_to_set v = D" by auto
        show "u = v"
        proof (cases)
          assume A3: "D = {}"
          from A3 d_u_d have "nat_to_set u = {}" by auto
          then have u_z: "u = 0" by (rule empty_is_zero)
          from A3 d_v_d have "nat_to_set v = {}" by auto
          then have v_z: "v = 0" by (rule empty_is_zero)
          from u_z v_z show "u = v" by auto
        next
          assume A3: "D  {}"
          from A3 d_u_d have "nat_to_set u  {}" by auto
          then have u_pos: "u > 0" by (rule ne_imp_pos)
          from A3 d_v_d have "nat_to_set v  {}" by auto
          then have v_pos: "v > 0" by (rule ne_imp_pos)
          define m where "m = Max D"
          from S1 m_def A3 have m_in: "m  D" by auto
          from d_u_d m_def have m_u: "m = Max (nat_to_set u)" by auto
          from d_v_d m_def have m_v: "m = Max (nat_to_set v)" by auto
          from u_pos m_u log2_is_max have m_log_u: "m = log2 u" by auto
          from v_pos m_v log2_is_max have m_log_v: "m = log2 v" by auto
          define D1 where "D1 = D - {m}"
          define u1 where "u1 = u - 2^m"
          define v1 where "v1 = v - 2^m"
          have card_D1: "card D1  n"
          proof -
            from D1_def S1 m_in have "card D1 = (card D) - 1" by (simp add: card_Diff_singleton)
            with S2 show ?thesis by auto
          qed
          have u_u1: "u = u1 + 2^m"
          proof -
            from u_pos have L1: "2 ^ log2 u  u" by (rule log2_le)
            with m_log_u have L2: "2 ^ m  u" by auto
            with u1_def show ?thesis by auto
          qed
          have u1_d1: "nat_to_set u1 = D1"
          proof -
            from m_log_u log2_gt have "u < 2^(m+1)" by auto
            with u_u1 have u1_lt_2_m: "u1 < 2^m" by auto
            with u_u1 have L1: "nat_to_set u = nat_to_set u1  {m}" by (simp add: add_power)
            have m_notin: "m  nat_to_set u1"
            proof (rule ccontr)
              assume "¬ m  nat_to_set u1" then have "m  nat_to_set u1" by auto
              then have "2^m  u1" by (rule nat_to_set_upper_bound)
              with u1_lt_2_m show False by auto
            qed
            from L1 m_notin have "nat_to_set u1 = nat_to_set u - {m}" by auto
            with d_u_d have "nat_to_set u1 = D - {m}" by auto
            with D1_def show ?thesis by auto
          qed
          have v_v1: "v = v1 + 2^m"
          proof -
            from v_pos have L1: "2 ^ log2 v  v" by (rule log2_le)
            with m_log_v have L2: "2 ^ m  v" by auto
            with v1_def show ?thesis by auto
          qed
          have v1_d1: "nat_to_set v1 = D1"
          proof -
            from m_log_v log2_gt have "v < 2^(m+1)" by auto
            with v_v1 have v1_lt_2_m: "v1 < 2^m" by auto
            with v_v1 have L1: "nat_to_set v = nat_to_set v1  {m}" by (simp add: add_power)
            have m_notin: "m  nat_to_set v1"
            proof (rule ccontr)
              assume "¬ m  nat_to_set v1" then have "m  nat_to_set v1" by auto
              then have "2^m  v1" by (rule nat_to_set_upper_bound)
              with v1_lt_2_m show False by auto
            qed
            from L1 m_notin have "nat_to_set v1 = nat_to_set v - {m}" by auto
            with d_v_d have "nat_to_set v1 = D - {m}" by auto
            with D1_def show ?thesis by auto
          qed
          from S1 D1_def have P1: "finite D1" by auto
          with card_D1 have P2: "finite D1  card D1  n" by auto
          from A_n P2 have "(u v. nat_to_set u = D1  nat_to_set v = D1  u = v)" by auto
          with u1_d1 v1_d1 have "u1 = v1" by auto
          with u_u1 v_v1 show "u = v" by auto
        qed
      qed
    qed
  qed
qed
  from P_at_0 P_at_Suc have main: " n. ?P n" by (rule nat.induct)
  define D where "D = nat_to_set u"
  from D_def A have P1: "nat_to_set u = D" by auto
  from D_def A have P2: "nat_to_set v = D" by auto
  from D_def nat_to_set_is_finite have d_finite: "finite D" by auto
  define n where "n = card D"
  from n_def d_finite have card_le: "card D  n" by auto
  from d_finite card_le have P3: "finite D  card D  n" by auto
  with main have P4: "u v. nat_to_set u = D  nat_to_set v = D  u = v" by auto
  with P1 P2 show "u = v" by auto
qed

definition
  set_to_nat :: "nat set => nat" where
  "set_to_nat = (λ D. sum (λ x. 2 ^ x) D)"

lemma two_power_sum: "sum (λ x. (2::nat) ^ x) {i. i< Suc m} = (2 ^ Suc m) - 1"
proof (induct m)
  show "sum (λ x. (2::nat) ^ x) {i. i< Suc 0} = (2 ^ Suc 0) - 1" by auto
next
  fix n
  assume A: "sum (λ x. (2::nat) ^ x) {i. i< Suc n} = (2 ^ Suc n) - 1"
  show "sum (λ x. (2::nat) ^ x) {i. i< Suc (Suc n)} = (2 ^ Suc (Suc n)) - 1"
  proof -
    let ?f = "λ x. (2::nat) ^ x"
    have S1: "{i. i< Suc (Suc n)} = {i. i  Suc n}" by auto
    have S2: "{i. i  Suc n} = {i. i < Suc n}  { Suc n}" by auto
    from S1 S2 have S3: "{i. i< Suc (Suc n)} = {i. i < Suc n}  { Suc n}" by auto
    have S4: "{i. i < Suc n} = (λ x. x) ` {i. i < Suc n}" by auto
    then have S5: "finite {i. i < Suc n}" by (rule nat_seg_image_imp_finite)
    have S6: "Suc n  {i. i < Suc n}" by auto
    from S5 S6 sum.insert have S7: "sum ?f ({i. i< Suc n}  {Suc n}) = 2 ^ Suc n + sum ?f {i. i< Suc n}" by auto
    from S3 have "sum ?f {i. i< Suc (Suc n)} = sum ?f ({i. i< Suc n}  {Suc n})" by auto
    also from S7 have " = 2 ^ Suc n + sum ?f {i. i< Suc n}" by auto
    also from A have " = 2 ^ Suc n + (((2::nat) ^ Suc n)-(1::nat))" by auto
    also have " = (2 ^ Suc (Suc n)) - 1" by auto
    finally show ?thesis by auto
  qed
qed

lemma finite_interval: "finite {i. (i::nat)<m}"
proof -
  have "{i. i < m} = (λ x. x) ` {i. i < m}" by auto
  then show ?thesis by (rule nat_seg_image_imp_finite)
qed

lemma set_to_nat_at_empty: "set_to_nat {} = 0" by (unfold set_to_nat_def, rule sum.empty)

lemma set_to_nat_of_interval: "set_to_nat {i. (i::nat)<m} = 2 ^ m - 1"
proof (induct m)
  show "set_to_nat {i. i < 0} = 2 ^ 0 - 1"
  proof -
    have S1: "{i. (i::nat) < 0} = {}" by auto
    with set_to_nat_at_empty have "set_to_nat {i. i<0} = 0" by auto
    thus ?thesis by auto
  qed
next
  fix n show "set_to_nat {i. i < Suc n} = 2 ^ Suc n - 1" by (unfold set_to_nat_def, rule two_power_sum)
qed

lemma set_to_nat_mono: " finite B; A  B  set_to_nat A  set_to_nat B"
proof -
  assume b_finite: "finite B"
  assume a_le_b: "A  B"
  let ?f = "λ (x::nat). (2::nat) ^ x"
  have S1: "set_to_nat A = sum ?f A" by (simp add: set_to_nat_def)
  have S2: "set_to_nat B = sum ?f B" by (simp add: set_to_nat_def)
  have S3: " x. x   B - A  0  ?f x" by auto
  from b_finite a_le_b S3 have "sum ?f A  sum ?f B" by (rule sum_mono2)
  with S1 S2 show ?thesis by auto
qed

theorem nat_to_set_srj: "finite (D::nat set)  nat_to_set (set_to_nat D) = D"
proof -
  assume A: "finite D"
  let ?P = "λ (n::nat). ( (D::nat set). finite D  card D = n  nat_to_set (set_to_nat D) = D)"
  have P_at_0: "?P 0"
  proof (rule allI)
    fix D
    show "finite D  card D = 0  nat_to_set (set_to_nat D) = D"
    proof
      assume A1: "finite D  card D = 0"
      from A1 have S1: "finite D" by auto
      from A1 have S2: "card D = 0" by auto
      from S1 S2 have S3: "D = {}" by auto
      with set_to_nat_def have "set_to_nat D = sum (λ x. 2 ^ x) D" by simp
      with S3 sum.empty have "set_to_nat D = 0" by auto
      with zero_is_empty S3 show "nat_to_set (set_to_nat D) = D" by auto
    qed
  qed
  have P_at_Suc: " n. ?P n  ?P (Suc n)"
  proof - fix n
    assume A_n: "?P n"
    show "?P (Suc n)"
    proof
      fix D show "finite D  card D = Suc n  nat_to_set (set_to_nat D) = D"
      proof
        assume A1: "finite D  card D = Suc n"
        from A1 have S1: "finite D" by auto
        from A1 have S2: "card D = Suc n" by auto
        define m where "m = Max D"
        from S2 have D_ne: "D  {}" by auto
        with S1 m_def have m_in: "m  D" by auto
        define D1 where "D1 = D - {m}"
        from S1 D1_def have d1_finite: "finite D1" by auto
        from D1_def m_in S1 have "card D1 = card D - 1" by (simp add: card_Diff_singleton)
        with S2 have card_d1: "card D1 = n" by auto
        from d1_finite card_d1 have "finite D1  card D1 = n" by auto
        with A_n have S3: "nat_to_set (set_to_nat D1) = D1" by auto
        define u where "u = set_to_nat D"
        define u1 where "u1 = set_to_nat D1"
        from S1 m_in have "sum (λ (x::nat). (2::nat) ^ x) D = 2 ^ m + sum (λ x. 2 ^ x) (D - {m})"
          by (rule sum.remove)
        with set_to_nat_def have "set_to_nat D = 2 ^ m + set_to_nat (D - {m})" by auto
        with u_def u1_def D1_def have u_u1: "u = u1 + 2 ^ m" by auto
        from S3 u1_def have d1_u1: "nat_to_set u1 = D1" by auto
        have u1_lt: "u1 < 2 ^ m"
        proof -
          have L1: "D1  {i. i<m}"
          proof fix x
            assume A1: "x  D1"
            show "x  {i. i<m}"
            proof
              from A1 D1_def have L1_1: "x  D" by auto
              from S1 D_ne L1_1 m_def have L1_2: "x  m" by auto
              with A1 L1_1 D1_def have "x  m" by auto
              with L1_2 show "x < m" by auto
            qed
          qed
          have L2: "finite {i. i<m}" by (rule finite_interval)
          from L2 L1 have "set_to_nat D1  set_to_nat {i. i<m}" by (rule set_to_nat_mono)
          with u1_def have "u1  set_to_nat {i. i<m}" by auto
          with set_to_nat_of_interval have L3: "u1  2 ^ m - 1" by auto
          have "0 < (2::nat) ^ m" by auto
          then have "(2::nat) ^ m - 1 < (2::nat) ^ m" by auto
          with L3 show ?thesis by arith
        qed
        from u_def have "nat_to_set (set_to_nat D) = nat_to_set u" by auto
        also from u_u1 have " = nat_to_set (u1 + 2 ^ m)" by auto
        also from u1_lt have " = nat_to_set u1  {m}" by (rule add_power)
        also from d1_u1 have " = D1  {m}" by auto
        also from D1_def m_in have " = D" by auto
        finally show "nat_to_set (set_to_nat D) = D" by auto
      qed
    qed
  qed
  from P_at_0 P_at_Suc have main: " n. ?P n" by (rule nat.induct)
  from A main show ?thesis by auto
qed

theorem nat_to_set_srj1: "finite (D::nat set)   u. nat_to_set u = D"
proof -
  assume A: "finite D"
  show "  u. nat_to_set u = D"
  proof
    from A show "nat_to_set (set_to_nat D) = D" by (rule nat_to_set_srj)
  qed
qed

lemma sum_of_pr_is_pr: "g  PrimRec1  (λ n. sum g {i. i<n})  PrimRec1"
proof -
  assume g_is_pr: "g  PrimRec1"
  define f where "f n = sum g {i. i<n}" for n
  from f_def have f_at_0: "f 0 = 0" by auto
  define h where "h a b = g a + b" for a b
  from g_is_pr have h_is_pr: "h  PrimRec2" unfolding h_def by prec
  have f_at_Suc: " y. f (Suc y) = h y (f y)"
  proof
    fix y show "f (Suc y) = h y (f y)"
    proof -
      from f_def have S1: "f (Suc y) = sum g {i. i < Suc y}" by auto
      have S2: "{i. i < Suc y} = {i. i < y}  {y}" by auto
      have S3: "finite {i. i < y}" by (rule finite_interval)
      have S4: "y  {i. i < y}" by auto
      from S1 S2 have "f (Suc y) = sum g ({i. (i::nat) < y}  {y})" by auto
      also from S3 S4 sum.insert have " = g y + sum g {i. i<y}" by auto
      also from f_def have " = g y + f y" by auto
      also from h_def have " = h y (f y)" by auto
      finally show ?thesis by auto
    qed
  qed
  from h_is_pr f_at_0 f_at_Suc have f_is_pr: "f  PrimRec1" by (rule pr_rec1_scheme)
  with f_def [abs_def] show ?thesis by auto
qed

lemma sum_of_pr_is_pr2: "p  PrimRec2  (λ n m. sum (λ x. p x m) {i. i<n})  PrimRec2"
proof -
  assume p_is_pr: "p  PrimRec2"
  define f where "f n m = sum (λ x. p x m) {i. i<n}" for n m
  define g :: "nat  nat" where "g x = 0" for x
  have g_is_pr: "g  PrimRec1" by (unfold g_def, rule const_is_pr [where ?n=0])
  have f_at_0: " x. f 0 x = g x"
  proof
    fix x from f_def g_def show "f 0 x = g x" by auto
  qed
  define h where "h a b c = p a c + b" for a b c
  from p_is_pr have h_is_pr: "h  PrimRec3" unfolding h_def by prec
  have f_at_Suc: " x y. f (Suc y) x = h y (f y x) x"
  proof (rule allI, rule allI)
    fix x y show "f (Suc y) x = h y (f y x) x"
    proof -
      from f_def have S1: "f (Suc y) x = sum (λ z. p z x)  {i. i < Suc y}" by auto
      have S2: "{i. i < Suc y} = {i. i < y}  {y}" by auto
      have S3: "finite {i. i < y}" by (rule finite_interval)
      have S4: "y  {i. i < y}" by auto
      define g1 where "g1 z = p z x" for z
      from S1 S2 g1_def have "f (Suc y) x = sum g1 ({i. (i::nat) < y}  {y})" by auto
      also from S3 S4 sum.insert have " = g1 y + sum g1 {i. i<y}" by auto
      also from f_def g1_def have " = g1 y + f y x" by auto
      also from h_def g1_def  have " = h y (f y x) x" by auto
      finally show ?thesis by auto
    qed
  qed
  from g_is_pr h_is_pr f_at_0 f_at_Suc have f_is_pr: "f  PrimRec2" by (rule pr_rec_scheme)
  with f_def [abs_def] show ?thesis by auto
qed

lemma sum_is_pr: "g  PrimRec1  (λ u. sum g (nat_to_set u))  PrimRec1"
proof -
  assume g_is_pr: "g  PrimRec1"
  define g1 where "g1 x u = (if (c_in x u = 1) then (g x) else 0)" for x u
  have g1_is_pr: "g1  PrimRec2"
  proof (unfold g1_def, rule if_eq_is_pr2)
    show "c_in  PrimRec2" by (rule c_in_is_pr)
  next
    show "(λx y. 1)  PrimRec2" by (rule const_is_pr_2 [where ?n=1])
  next
    from g_is_pr show "(λx y. g x)  PrimRec2" by prec
  next
    show "(λx y. 0)  PrimRec2" by (rule const_is_pr_2 [where ?n=0])
  qed
  define f where "f u = sum (λ x. g1 x u) {i. (i::nat) < u}" for u
  define f1 where "f1 u v = sum (λ x. g1 x v) {i. (i::nat) < u}"  for u v
  from g1_is_pr have "(λ (u::nat) v. sum (λ x. g1 x v) {i. (i::nat) < u})  PrimRec2"
    by (rule sum_of_pr_is_pr2)
  with f1_def [abs_def] have f1_is_pr: "f1  PrimRec2" by auto
  from f_def f1_def have f_f1: "f = (λ u. f1 u u)" by auto
  from f1_is_pr have "(λ u. f1 u u)  PrimRec1" by prec
  with f_f1 have f_is_pr: "f  PrimRec1" by auto
  have f_is_result: "f = (λ u. sum g (nat_to_set u))"
  proof
    fix u show "f u = sum g (nat_to_set u)"
    proof -
      define U where "U = {i. i < u}"
      define A where "A = {x  U. c_in x u = 1}"
      define B where "B = {x  U. c_in x u  1}"
      have U_finite: "finite U" by (unfold U_def, rule finite_interval)
      from A_def U_finite have A_finite: "finite A" by auto
      from B_def U_finite have B_finite: "finite B" by auto
      from U_def A_def B_def have U_A_B: "U = A  B" by auto
      from U_def A_def B_def have A_B: "A  B = {}" by auto
      from B_def g1_def have B_z: "sum (λ x. g1 x u) B = 0" by auto
      have u_in_U: "nat_to_set u  U" by (unfold U_def, rule nat_to_set_upper_bound2)
      from u_in_U x_in_u_eq A_def have A_u: "A = nat_to_set u" by auto
      from A_u x_in_u_eq g1_def have A_res: "sum (λ x. g1 x u) A = sum g (nat_to_set u)" by auto
      from f_def have "f u = sum (λ x. g1 x u) {i. (i::nat) < u}" by auto
      also from U_def have " = sum (λ x. g1 x u) U" by auto
      also from U_A_B have " = sum (λ x. g1 x u) (A  B)" by auto
      also from A_finite B_finite A_B have " = sum (λ x. g1 x u) A + sum (λ x. g1 x u) B" by (rule sum.union_disjoint)
      also from B_z have " = sum (λ x. g1 x u) A" by auto
      also from A_res have " = sum g (nat_to_set u)" by auto
      finally show ?thesis by auto
    qed
  qed
  with f_is_pr show ?thesis by auto
qed

definition
  c_card :: "nat  nat" where
  "c_card = (λ u. card (nat_to_set u))"

theorem c_card_is_pr: "c_card  PrimRec1"
proof -
  define g :: "nat  nat" where "g x = 1" for x
  have g_is_pr: "g  PrimRec1" by (unfold g_def, rule const_is_pr)
  have "c_card = (λ u. sum g (nat_to_set u))"
  proof
    fix u show "c_card u = sum g (nat_to_set u)" by (unfold c_card_def, unfold g_def, rule card_eq_sum)
  qed
  moreover from g_is_pr have "(λ u. sum g (nat_to_set u))  PrimRec1" by (rule sum_is_pr)
  ultimately show ?thesis by auto
qed

definition
  c_insert :: "nat  nat  nat" where
  "c_insert = (λ x u. if c_in x u = 1 then u else u + 2^x)"

lemma c_insert_is_pr: "c_insert  PrimRec2"
proof (unfold c_insert_def, rule if_eq_is_pr2)
  show "c_in  PrimRec2" by (rule c_in_is_pr)
next
  show "(λx y. 1)  PrimRec2" by (rule const_is_pr_2)
next
  show "(λx y. y)  PrimRec2" by (rule pr_id2_2)
next
  from power_is_pr show "(λx y. y + 2 ^ x)  PrimRec2" by prec
qed

lemma [simp]: "set_to_nat (nat_to_set u) = u"
proof -
  define D where "D = nat_to_set u"
  from D_def nat_to_set_is_finite have D_finite: "finite D" by auto
  then have "nat_to_set (set_to_nat D) = D" by (rule nat_to_set_srj)
  with D_def have "nat_to_set (set_to_nat D) = nat_to_set u" by auto
  then have "set_to_nat D = u" by (rule nat_to_set_inj)
  with D_def show ?thesis by auto
qed

lemma insert_lemma: "x  nat_to_set u  set_to_nat (nat_to_set u  {x}) = u + 2 ^ x"
proof -
  assume A: "x  nat_to_set u"
  define D where "D = nat_to_set u"
  from A D_def have S1: "x  D" by auto
  have "finite (nat_to_set u)" by (rule nat_to_set_is_finite)
  with D_def have D_finite: "finite D" by auto
  let ?f = "λ (x::nat). (2::nat)^x"
  from set_to_nat_def have "set_to_nat (D  {x}) = sum ?f (D  {x})" by auto
  also from D_finite S1 have " = ?f x + sum ?f D" by simp
  also from set_to_nat_def have " = 2 ^ x + set_to_nat D" by auto
  finally have "set_to_nat (D  {x}) = set_to_nat D + 2 ^ x" by auto
  with D_def show ?thesis by auto
qed

lemma c_insert_df: "c_insert = (λ x u. set_to_nat ((nat_to_set u)  {x}))"
proof (rule ext, rule ext)
  fix x u show "c_insert x u = set_to_nat (nat_to_set u  {x})"
  proof (cases)
    assume A: "x  nat_to_set u"
    then have "nat_to_set u  {x} = nat_to_set u" by auto
    then have S1: "set_to_nat (nat_to_set u  {x}) = u" by auto
    from A have "c_in x u = 1" by (simp add: x_in_u_eq)
    then have "c_insert x u = u" by (unfold c_insert_def, simp)
    with S1 show ?thesis by auto
  next
    assume A: "x  nat_to_set u"
    then have S1: "c_in x u  1" by (simp add: x_in_u_eq)
    then have S2: "c_insert x u = u + 2 ^ x" by (unfold c_insert_def, simp)
    from A have "set_to_nat (nat_to_set u  {x}) = u + 2 ^ x" by (rule insert_lemma)
    with S2 show ?thesis by auto
  qed
qed

definition
  c_remove :: "nat  nat  nat" where
  "c_remove = (λ x u. if c_in x u = 0 then u else u - 2^x)"

lemma c_remove_is_pr: "c_remove  PrimRec2"
proof (unfold c_remove_def, rule if_eq_is_pr2)
  show "c_in  PrimRec2" by (rule c_in_is_pr)
next
  show "(λx y. 0)  PrimRec2" by (rule const_is_pr_2)
next
  show "(λx y. y)  PrimRec2" by (rule pr_id2_2)
next
  from power_is_pr show "(λx y. y - 2 ^ x)  PrimRec2" by prec
qed

lemma remove_lemma: "x  nat_to_set u  set_to_nat (nat_to_set u - {x}) = u - 2 ^ x"
proof -
  assume A: "x  nat_to_set u"
  define D where "D = nat_to_set u - {x}"
  from A D_def have S1: "x  D" by auto
  have "finite (nat_to_set u)" by (rule nat_to_set_is_finite)
  with D_def have D_finite: "finite D" by auto
  let ?f = "λ (x::nat). (2::nat)^x"
  from set_to_nat_def have "set_to_nat (D  {x}) = sum ?f (D  {x})" by auto
  also from D_finite S1 have " = ?f x + sum ?f D" by simp
  also from set_to_nat_def have " = 2 ^ x + set_to_nat D" by auto
  finally have S2: "set_to_nat (D  {x}) = set_to_nat D + 2 ^ x" by auto
  from A D_def have "D  {x} = nat_to_set u" by auto
  with S2 have S3: "u = set_to_nat D + 2 ^ x" by auto
  from A have S4: "2 ^ x  u" by (rule nat_to_set_upper_bound)
  with S3 D_def show ?thesis by auto
qed

lemma c_remove_df: "c_remove = (λ x u. set_to_nat ((nat_to_set u) - {x}))"
proof (rule ext, rule ext)
  fix x u show "c_remove x u = set_to_nat (nat_to_set u - {x})"
  proof (cases)
    assume A: "x  nat_to_set u"
    then have S1: "c_in x u = 1" by (simp add: x_in_u_eq)
    then have S2: "c_remove x u = u - 2^x" by (simp add: c_remove_def)
    from A have "set_to_nat (nat_to_set u - {x}) = u - 2 ^ x" by (rule remove_lemma)
    with S2 show ?thesis by auto
  next
    assume A: "x  nat_to_set u"
    then have S1: "c_in x u  1" by (simp add: x_in_u_eq)
    then have S2: "c_remove x u = u" by (simp add: c_remove_def c_in_def)
    from A have "nat_to_set u - {x} = nat_to_set u" by auto
    with S2 show ?thesis by auto
  qed
qed

definition
  c_union :: "nat  nat  nat" where
  "c_union = (λ u v. set_to_nat (nat_to_set u  nat_to_set v))"

theorem c_union_is_pr: "c_union  PrimRec2"
proof -
  define f where "f y x = set_to_nat ((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y})"
    for y x
  have f_is_pr: "f  PrimRec2"
  proof -
    define g where "g = c_fst"
    from c_fst_is_pr g_def have g_is_pr: "g  PrimRec1" by auto
    define h where "h a b c = (if c_in a (c_snd c) = 1 then c_insert a b else b)" for a b c
    from c_in_is_pr c_insert_is_pr have h_is_pr: "h  PrimRec3" unfolding h_def by prec
    have f_at_0: " x. f 0 x = g x"
    proof
      fix x show "f 0 x = g x" by (unfold f_def, unfold g_def, simp)
    qed
    have f_at_Suc: " x y. f (Suc y) x = h y (f y x) x"
    proof (rule allI, rule allI)
      fix x y show "f (Suc y) x = h y (f y x) x"
      proof (cases)
        assume A: "c_in y (c_snd x) = 1"
        then have S1: "y  (nat_to_set (c_snd x))" by (simp add: x_in_u_eq)
        from A h_def have S2: "h y (f y x) x = c_insert y (f y x)" by auto
        from S1 have S3: "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}  {y}" by auto
        from nat_to_set_is_finite have S4: "finite ((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y})" by auto
        with nat_to_set_srj f_def have S5: "nat_to_set (f y x) = (nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y}" by auto
        from f_def have S6: "f (Suc y) x = set_to_nat ((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < Suc y})" by simp
        also from S3 have " = set_to_nat (((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y})  {y})" by auto
        also from S5 have " = set_to_nat (nat_to_set (f y x)  {y})" by auto
        also have " = c_insert y (f y x)" by (simp add: c_insert_df)
        finally show ?thesis by (simp add: S2)
      next
        assume A: "¬ c_in y (c_snd x) = 1"
        then have S1: "y  (nat_to_set (c_snd x))" by (simp add: x_in_u_eq)
        from A h_def have S2: "h y (f y x) x = f y x" by auto
        have S3: "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}"
        proof -
          have "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}  {z  nat_to_set (c_snd x). z = y}"
            by auto
          with S1 show ?thesis by auto
        qed
        from nat_to_set_is_finite have S4: "finite ((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y})" by auto
        with nat_to_set_srj f_def have S5: "nat_to_set (f y x) = (nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y}" by auto
        from f_def have S6: "f (Suc y) x = set_to_nat ((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < Suc y})" by simp
        also from S3 have " = set_to_nat (((nat_to_set (c_fst x))  {z  nat_to_set (c_snd x). z < y}))" by auto
        also from S5 have " = set_to_nat (nat_to_set (f y x))" by auto
        also have " = f y x" by simp
        finally show ?thesis by (simp add: S2)
      qed
    qed
    from g_is_pr h_is_pr f_at_0 f_at_Suc show ?thesis by (rule pr_rec_scheme)
  qed
  define union where "union u v = f v (c_pair u v)" for u v
  from f_is_pr have union_is_pr: "union  PrimRec2" unfolding union_def by prec
  have " u v. union u v = set_to_nat (nat_to_set u  nat_to_set v)"
  proof -
    fix u v show "union u v = set_to_nat (nat_to_set u  nat_to_set v)"
    proof -
      from nat_to_set_upper_bound1 have "{z  nat_to_set v. z < v} = nat_to_set v" by auto
      with union_def f_def show ?thesis by auto
    qed
  qed
  then have "union = (λ u v. set_to_nat (nat_to_set u  nat_to_set v))" by (simp add: ext)
  with c_union_def have "c_union = union" by simp
  with union_is_pr show ?thesis by simp
qed

definition
  c_diff :: "nat  nat  nat" where
  "c_diff = (λ u v. set_to_nat (nat_to_set u - nat_to_set v))"

theorem c_diff_is_pr: "c_diff  PrimRec2"
proof -
  define f where "f y x = set_to_nat ((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y})"
    for y x
  have f_is_pr: "f  PrimRec2"
  proof -
    define g where "g = c_fst"
    from c_fst_is_pr g_def have g_is_pr: "g  PrimRec1" by auto
    define h where "h a b c = (if c_in a (c_snd c) = 1 then c_remove a b else b)" for a b c
    from c_in_is_pr c_remove_is_pr have h_is_pr: "h  PrimRec3" unfolding h_def by prec
    have f_at_0: " x. f 0 x = g x"
    proof
      fix x show "f 0 x = g x" by (unfold f_def, unfold g_def, simp)
    qed
    have f_at_Suc: " x y. f (Suc y) x = h y (f y x) x"
    proof (rule allI, rule allI)
      fix x y show "f (Suc y) x = h y (f y x) x"
      proof (cases)
        assume A: "c_in y (c_snd x) = 1"
        then have S1: "y  (nat_to_set (c_snd x))" by (simp add: x_in_u_eq)
        from A h_def have S2: "h y (f y x) x = c_remove y (f y x)" by auto
        have "(nat_to_set (c_fst x)) - ({z  nat_to_set (c_snd x). z < y}  {y}) =
              ((nat_to_set (c_fst x)) - ({z  nat_to_set (c_snd x). z < y}) - {y})" by auto
        then have lm1: "set_to_nat (nat_to_set (c_fst x) - ({z  nat_to_set (c_snd x). z < y}  {y})) =
                        set_to_nat (nat_to_set (c_fst x) - {z  nat_to_set (c_snd x). z < y} - {y})" by auto
        from S1 have S3: "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}  {y}" by auto
        from nat_to_set_is_finite have S4: "finite ((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y})" by auto
        with nat_to_set_srj f_def have S5: "nat_to_set (f y x) = (nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y}" by auto
        from f_def have S6: "f (Suc y) x = set_to_nat ((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < Suc y})" by simp
        also from S3 have " = set_to_nat ((nat_to_set (c_fst x)) - ({z  nat_to_set (c_snd x). z < y}  {y}))" by auto
        also have " = set_to_nat (((nat_to_set (c_fst x)) - ({z  nat_to_set (c_snd x). z < y}) - {y}))" by (rule lm1)
        also from S5 have " = set_to_nat (nat_to_set (f y x) - {y})" by auto
        also have " = c_remove y (f y x)" by (simp add: c_remove_df)
        finally show ?thesis by (simp add: S2)
      next
        assume A: "¬ c_in y (c_snd x) = 1"
        then have S1: "y  (nat_to_set (c_snd x))" by (simp add: x_in_u_eq)
        from A h_def have S2: "h y (f y x) x = f y x" by auto
        have S3: "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}"
        proof -
          have "{z  nat_to_set (c_snd x). z < Suc y} = {z  nat_to_set (c_snd x). z < y}  {z  nat_to_set (c_snd x). z = y}"
            by auto
          with S1 show ?thesis by auto
        qed
        from nat_to_set_is_finite have S4: "finite ((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y})" by auto
        with nat_to_set_srj f_def have S5: "nat_to_set (f y x) = (nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y}" by auto
        from f_def have S6: "f (Suc y) x = set_to_nat ((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < Suc y})" by simp
        also from S3 have " = set_to_nat (((nat_to_set (c_fst x)) - {z  nat_to_set (c_snd x). z < y}))" by auto
        also from S5 have " = set_to_nat (nat_to_set (f y x))" by auto
        also have " = f y x" by simp
        finally show ?thesis by (simp add: S2)
      qed
    qed
    from g_is_pr h_is_pr f_at_0 f_at_Suc show ?thesis by (rule pr_rec_scheme)
  qed
  define diff where "diff u v = f v (c_pair u v)" for u v
  from f_is_pr have diff_is_pr: "diff  PrimRec2" unfolding diff_def by prec
  have " u v. diff u v = set_to_nat (nat_to_set u - nat_to_set v)"
  proof -
    fix u v show "diff u v = set_to_nat (nat_to_set u - nat_to_set v)"
    proof -
      from nat_to_set_upper_bound1 have "{z  nat_to_set v. z < v} = nat_to_set v" by auto
      with diff_def f_def show ?thesis by auto
    qed
  qed
  then have "diff = (λ u v. set_to_nat (nat_to_set u - nat_to_set v))" by (simp add: ext)
  with c_diff_def have "c_diff = diff" by simp
  with diff_is_pr show ?thesis by simp
qed

definition
  c_intersect :: "nat  nat  nat" where
  "c_intersect = (λ u v. set_to_nat (nat_to_set u  nat_to_set v))"

theorem c_intersect_is_pr: "c_intersect  PrimRec2"
proof -
  define f where "f u v = c_diff (c_union u v) (c_union (c_diff u v) (c_diff v u))" for u v
  from c_diff_is_pr c_union_is_pr have f_is_pr: "f  PrimRec2" unfolding f_def by prec
  have " u v. f u v = c_intersect u v"
  proof -
    fix u v show "f u v = c_intersect u v"
    proof -
      let ?A = "nat_to_set u"
      let ?B = "nat_to_set v"
      have A_fin: "finite ?A" by (rule nat_to_set_is_finite)
      have B_fin: "finite ?B" by (rule nat_to_set_is_finite)
      have S1: "c_union u v = set_to_nat (?A  ?B)" by (simp add: c_union_def)
      have S2: "c_diff u v = set_to_nat (?A - ?B)" by (simp add: c_diff_def)
      have S3: "c_diff v u = set_to_nat (?B - ?A)" by (simp add: c_diff_def)
      from S2 A_fin B_fin have S4: "nat_to_set (c_diff u v) = ?A - ?B" by  (simp add: nat_to_set_srj)
      from S3 A_fin B_fin have S5: "nat_to_set (c_diff v u) = ?B - ?A" by  (simp add: nat_to_set_srj)
      from S4 S5 have S6: "c_union (c_diff u v) (c_diff v u) = set_to_nat ((?A - ?B)  (?B - ?A))" by (simp add: c_union_def)
      from S1 A_fin B_fin have S7: "nat_to_set (c_union u v) = ?A  ?B" by  (simp add: nat_to_set_srj)
      from S6 A_fin B_fin have S8: "nat_to_set (c_union (c_diff u v) (c_diff v u)) = (?A - ?B)  (?B - ?A)" by  (simp add: nat_to_set_srj)
      from S7 S8 have S9: "f u v = set_to_nat ((?A  ?B) - ((?A - ?B)  (?B - ?A)))" by (simp add: c_diff_def f_def)
      have S10: "?A  ?B = (?A  ?B) - ((?A - ?B)  (?B - ?A))" by auto
      with S9 have S11: "f u v = set_to_nat (?A  ?B)" by auto
      have "c_intersect u v = set_to_nat (?A  ?B)" by (simp add: c_intersect_def)
      with S11 show ?thesis by auto
    qed
  qed
  then have "f = c_intersect" by (simp add: ext)
  with f_is_pr show ?thesis by auto
qed

end