# Theory RecEnSet

Up to index of Isabelle/HOL/Recursion-Theory-I

theory RecEnSet
imports PRecFinSet PRecUnGr
`(*  Title:       Computably enumerable sets of natural numbers    Author:      Michael Nedzelsky <MichaelNedzelsky at yandex.ru>, 2008    Maintainer:  Michael Nedzelsky <MichaelNedzelsky at yandex.ru>*)header {* Computably enumerable sets of natural numbers *}theory RecEnSetimports PRecList PRecFun2 PRecFinSet PRecUnGrbeginsubsection {* Basic definitions *}definition  fn_to_set :: "(nat => nat => nat) => nat set" where  "fn_to_set f = { x. ∃ y. f x y = 0 }"definition  ce_sets :: "(nat set) set" where  "ce_sets = { (fn_to_set p) | p. p ∈ PrimRec2 }"subsection {* Basic properties of computably enumerable sets *}lemma ce_set_lm_1: "p ∈ PrimRec2 ==> fn_to_set p ∈ ce_sets" by (auto simp add: ce_sets_def)lemma ce_set_lm_2: "[| p ∈ PrimRec2; ∀ x. (x ∈ A) = (∃ y. p x y = 0)|] ==> A ∈ ce_sets"proof -  assume p_is_pr: "p ∈ PrimRec2"  assume "∀ x. (x ∈ A) = (∃ y. p x y = 0)"  then have "A = fn_to_set p" by (unfold fn_to_set_def, auto)  with p_is_pr show "A ∈ ce_sets" by (simp add: ce_set_lm_1)qedlemma ce_set_lm_3: "A ∈ ce_sets ==> ∃ p ∈ PrimRec2. A = fn_to_set p"proof -  assume "A ∈ ce_sets"  then have "A ∈ { (fn_to_set p) | p. p ∈ PrimRec2 }" by (simp add: ce_sets_def)  thus ?thesis by autoqedlemma ce_set_lm_4: "A ∈ ce_sets ==> ∃ p ∈ PrimRec2. ∀ x. (x ∈ A) = (∃ y. p x y = 0)"proof -  assume "A ∈ ce_sets"  then have "∃ p ∈ PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)  then obtain p where p_is_pr: "p ∈ PrimRec2" and L1: "A = fn_to_set p" ..  from p_is_pr L1 show ?thesis by (unfold fn_to_set_def, auto)qedlemma ce_set_lm_5: "[| A ∈ ce_sets; p ∈ PrimRec1 |] ==> { x . p x ∈ A } ∈ ce_sets"proof -  assume A1: "A ∈ ce_sets"  assume A2: "p ∈ PrimRec1"  from A1 have "∃ pA ∈ PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)  then obtain pA where pA_is_pr: "pA ∈ PrimRec2" and S1: "A = fn_to_set pA" ..  from S1 have S2: "A = { x . ∃ y. pA x y = 0 }" by (simp add: fn_to_set_def)  def q_def: q ≡ "λ x y. pA (p x) y"  from pA_is_pr A2 have q_is_pr: "q ∈ PrimRec2" unfolding q_def by prec  have "!! x. (p x ∈ A) = (∃ y. q x y = 0)"  proof -    fix x show "(p x ∈ A) = (∃ y. q x y = 0)"    proof      assume A: "p x ∈ A"      with S2 obtain y where L1: "pA (p x) y = 0" by auto      then have "q x y = 0" by (simp add: q_def)      thus "∃ y. q x y = 0" ..    next      assume A: "∃y. q x y = 0"      then obtain y where L1: "q x y = 0" ..      then have "pA (p x) y = 0" by (simp add: q_def)      with S2 show "p x ∈ A" by auto    qed  qed  then have "{ x . p x ∈ A } = { x. ∃ y. q x y = 0 }" by auto  then have "{ x . p x ∈ A } = fn_to_set q" by (simp add: fn_to_set_def)  moreover from q_is_pr have "fn_to_set q ∈ ce_sets" by (rule ce_set_lm_1)  ultimately show ?thesis by autoqedlemma ce_set_lm_6: "[| A ∈ ce_sets; A ≠ {}|] ==> ∃ q ∈ PrimRec1. A = { q x | x. x ∈ UNIV }"proof -  assume A1: "A ∈ ce_sets"  assume A2: "A ≠ {}"  from A1 have "∃ pA ∈ PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)  then obtain pA where pA_is_pr: "pA ∈ PrimRec2" and S1: "A = fn_to_set pA" ..  from S1 have S2: "A = { x. ∃ y. pA x y = 0 }" by (simp add: fn_to_set_def)  from A2 obtain a where a_in: "a ∈ A" by auto  def q_def: q ≡ "λ z. if pA (c_fst z) (c_snd z) = 0 then c_fst z else a"  from pA_is_pr have q_is_pr: "q ∈ PrimRec1" unfolding q_def by prec  have S3: "∀ z. q z ∈ A"  proof    fix z show "q z ∈ A"    proof cases      assume A: "pA (c_fst z) (c_snd z) = 0"      with S2 have "c_fst z ∈ A" by auto      moreover from A q_def have "q z = c_fst z" by simp      ultimately show "q z ∈ A" by auto    next      assume A: "pA (c_fst z) (c_snd z) ≠ 0"      with q_def have "q z = a" by simp      with a_in show "q z ∈ A" by auto    qed  qed  then have S4: "{ q x | x. x ∈ UNIV } ⊆ A" by auto  have S5: "A ⊆ { q x | x. x ∈ UNIV }"  proof    fix x assume A: "x ∈ A" show "x ∈ {q x |x. x ∈ UNIV}"    proof      from A S2 obtain y where L1: "pA x y = 0" by auto      let ?z = "c_pair x y"      from L1 have "q ?z = x" by (simp add: q_def)      then have "∃ u. q u = x" by blast      then show "∃u. x = q u ∧ u ∈ UNIV" by auto    qed  qed  from S4 S5 have S6: "A = { q x | x. x ∈ UNIV }" by auto  with q_is_pr show ?thesis by blastqedlemma ce_set_lm_7: "[| A ∈ ce_sets; p ∈ PrimRec1|] ==> { p x | x. x ∈ A } ∈ ce_sets"proof -  assume A1: "A ∈ ce_sets"  assume A2: "p ∈ PrimRec1"  let ?B = "{ p x | x. x ∈ A }"  fix y have S1: "(y ∈ ?B) = (∃ x. x ∈ A ∧ (y = p x))" by auto  from A1 have "∃ pA ∈ PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)  then obtain pA where pA_is_pr: "pA ∈ PrimRec2" and S2: "A = fn_to_set pA" ..  from S2 have S3: "A = { x. ∃ y. pA x y = 0 }" by (simp add: fn_to_set_def)  def q_def: q ≡ "λ y t. if y = p (c_snd t) then pA (c_snd t) (c_fst t) else 1"  from pA_is_pr A2 have q_is_pr: "q ∈ PrimRec2" unfolding q_def by prec  have L1: "!! y. (y ∈ ?B) = (∃ z. q y z = 0)"  proof - fix y show "(y ∈ ?B) = (∃ z. q y z = 0)"  proof    assume AA1: "y ∈ ?B"    then obtain x0 where LL_2: "x0 ∈ A" and LL_3: "y = p x0" by auto    from S3 have LL_4: "(x0 ∈ A) = (∃ z. pA x0 z = 0)" by auto    from LL_2 LL_4 obtain z0 where LL_5: "pA x0 z0 = 0" by auto    def t_def: t ≡ "c_pair z0 x0"    from t_def q_def LL_3 LL_5 have "q y t = 0" by simp    then show "∃ z. q y z = 0" by auto  next    assume A1: "∃ z. q y z = 0"    then obtain z0 where LL_1: "q y z0 = 0" ..    have LL2: "y = p (c_snd z0)"    proof (rule ccontr)      assume "y ≠ p (c_snd z0)"      with q_def LL_1 have "q y z0 = 1" by auto      with LL_1 show False by auto    qed    from LL2 LL_1 q_def have LL3: "pA (c_snd z0) (c_fst z0) = 0" by auto    with S3 have LL4: "c_snd z0 ∈ A" by auto    with LL2 show "y ∈ {p x | x. x ∈ A}" by auto  qed  qed  then have L2: "?B = { y | y. ∃ z. q y z = 0}" by auto  with fn_to_set_def have "?B = fn_to_set q" by auto  with q_is_pr ce_set_lm_1 show ?thesis by autoqedtheorem ce_empty: "{} ∈ ce_sets"proof -  let ?f = "(λ x a. (1::nat))"  have S1: "?f ∈ PrimRec2" by (rule const_is_pr_2)  then have "∀ x a. ?f x a ≠ 0" by simp  then have "{x. ∃ a. ?f x a = 0 }={}" by auto  also have "fn_to_set ?f = …" by (simp add: fn_to_set_def)  with S1 show ?thesis by (auto simp add: ce_sets_def)qedtheorem ce_univ: "UNIV ∈ ce_sets"proof -  let ?f = "(λ x a. (0::nat))"  have S1: "?f ∈ PrimRec2" by (rule const_is_pr_2)  then have "∀ x a. ?f x a = 0" by simp  then have "{x. ∃ a. ?f x a = 0 }=UNIV" by auto  also have "fn_to_set ?f = …" by (simp add: fn_to_set_def)  with S1 show ?thesis by (auto simp add: ce_sets_def)qedtheorem ce_singleton: "{a} ∈ ce_sets"proof -  let ?f = "λ x y. (abs_of_diff x a) + y"  have S1: "?f ∈ PrimRec2" using const_is_pr_2 [where ?n="a"] by prec  then have "∀ x y. (?f x y = 0) = (x=a ∧ y=0)" by (simp add: abs_of_diff_eq)  then have S2: "{x. ∃ y. ?f x y = 0 }={a}" by auto  have "fn_to_set ?f = {x. ∃ y. ?f x y = 0 }" by (simp add: fn_to_set_def)  with S2 have "fn_to_set ?f = {a}" by simp  with S1 show ?thesis by (auto simp add: ce_sets_def)qedtheorem ce_union: "[| A ∈ ce_sets; B ∈ ce_sets |] ==> A ∪ B ∈ ce_sets"proof -  assume A1: "A ∈ ce_sets"  then obtain p_a where S2: "p_a ∈ PrimRec2" and S3: "A = fn_to_set p_a"    by (auto simp add: ce_sets_def)  assume A2: "B ∈ ce_sets"  then obtain p_b where S5: "p_b ∈ PrimRec2" and S6: "B = fn_to_set p_b"    by (auto simp add: ce_sets_def)  let ?p = "(λ x y. (p_a x y) * (p_b x y))"  from S2 S5 have S7: "?p ∈ PrimRec2" by prec  have S8: "∀ x y. (?p x y = 0) = ((p_a x y = 0) ∨ (p_b x y = 0))" by simp  let ?C = "fn_to_set ?p"  have S9: "?C = {x. ∃ y. ?p x y = 0}" by (simp add: fn_to_set_def)  from S3 have S10: "A = {x. ∃ y. p_a x y = 0}" by (simp add: fn_to_set_def)  from S6 have S11: "B = {x. ∃ y. p_b x y = 0}" by (simp add: fn_to_set_def)  from S10 S11 S9 S8 have S12: "?C = A ∪ B" by auto  from S7 have "?C ∈ ce_sets" by (auto simp add: ce_sets_def)  with S12 show ?thesis by simpqedtheorem ce_intersect: "[| A ∈ ce_sets; B ∈ ce_sets |] ==> A ∩ B ∈ ce_sets"proof -  assume A1: "A ∈ ce_sets"  then obtain p_a where S2: "p_a ∈ PrimRec2" and S3: "A = fn_to_set p_a"    by (auto simp add: ce_sets_def)  assume A2: "B ∈ ce_sets"  then obtain p_b where S5: "p_b ∈ PrimRec2" and S6: "B = fn_to_set p_b"    by (auto simp add: ce_sets_def)  let ?p = "(λ x y. (p_a x (c_fst y)) + (p_b x (c_snd y)))"  from S2 S5 have S7: "?p ∈ PrimRec2" by prec  have S8: "∀ x. (∃ y. ?p x y = 0) = ((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0))"  proof    fix x show "(∃ y. ?p x y = 0) = ((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0))"    proof -    have 1: "(∃ y. ?p x y = 0) ==> ((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0))"    by blast    have 2: "((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0)) ==> (∃ y. ?p x y = 0)"    proof -      assume "((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0))"      then obtain z1 z2 where s_23: "p_a x z1 = 0" and s_24: "p_b x z2 = 0" by auto      let ?y1 = "c_pair z1 z2"      from s_23 have s_25: "p_a x (c_fst ?y1) = 0" by simp      from s_24 have s_26: "p_b x (c_snd ?y1) = 0" by simp      from s_25 s_26 have s_27: "p_a x (c_fst ?y1) + p_b x (c_snd ?y1) = 0" by simp      then show ?thesis ..    qed    from 1 2 have "(∃ y. ?p x y = 0) = ((∃ z. p_a x z = 0) ∧ (∃ z. p_b x z = 0))" by (rule iffI)    then show ?thesis by auto    qed  qed  let ?C = "fn_to_set ?p"  have S9: "?C = {x. ∃ y. ?p x y = 0}" by (simp add: fn_to_set_def)  from S3 have S10: "A = {x. ∃ y. p_a x y = 0}" by (simp add: fn_to_set_def)  from S6 have S11: "B = {x. ∃ y. p_b x y = 0}" by (simp add: fn_to_set_def)  from S10 S11 S9 S8 have S12: "?C = A ∩ B" by auto  from S7 have "?C ∈ ce_sets" by (auto simp add: ce_sets_def)  with S12 show ?thesis by simpqedsubsection {* Enumeration of computably enumerable sets *}definition  nat_to_ce_set :: "nat => (nat set)" where  "nat_to_ce_set = (λ n. fn_to_set (pr_conv_1_to_2 (nat_to_pr n)))"lemma nat_to_ce_set_lm_1: "nat_to_ce_set n = { x . ∃ y. (nat_to_pr n) (c_pair x y) = 0 }"proof -  have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))" by (simp add: nat_to_ce_set_def)  then have S2: "nat_to_ce_set n = { x . ∃ y. (pr_conv_1_to_2 (nat_to_pr n)) x y = 0}" by (simp add: fn_to_set_def)  have S3: "!! x y. (pr_conv_1_to_2 (nat_to_pr n)) x y = (nat_to_pr n) (c_pair x y)" by (simp add: pr_conv_1_to_2_def)  from S2 S3 show ?thesis by autoqedlemma nat_to_ce_set_into_ce: "nat_to_ce_set n ∈ ce_sets"proof -  have S1: "nat_to_ce_set n = fn_to_set (pr_conv_1_to_2 (nat_to_pr n))" by (simp add: nat_to_ce_set_def)  have "(nat_to_pr n) ∈ PrimRec1" by (rule nat_to_pr_into_pr)  then have S2: "(pr_conv_1_to_2 (nat_to_pr n)) ∈ PrimRec2" by (rule pr_conv_1_to_2_lm)  from S2 S1 show ?thesis by (simp add: ce_set_lm_1)qedlemma nat_to_ce_set_srj: "A ∈ ce_sets ==> ∃ n. A = nat_to_ce_set n"proof -  assume A: "A ∈ ce_sets"  then have "∃ p ∈ PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)  then obtain p where p_is_pr: "p ∈ PrimRec2" and S1: "A = fn_to_set p" ..  def q_def: q ≡ "pr_conv_2_to_1 p"  from p_is_pr have q_is_pr: "q ∈ PrimRec1" by (unfold q_def, rule pr_conv_2_to_1_lm)  from q_def have S2: "pr_conv_1_to_2 q = p" by simp  let ?n = "index_of_pr q"  from q_is_pr have "nat_to_pr ?n = q" by (rule index_of_pr_is_real)  with S2 S1 have "A = fn_to_set (pr_conv_1_to_2 (nat_to_pr ?n))" by auto  then have "A = nat_to_ce_set ?n" by (simp add: nat_to_ce_set_def)  thus ?thesis ..qedsubsection {* Characteristic functions *}definition  chf :: "nat set => (nat => nat)" -- "Characteristic function" where  "chf = (λ A x. if x ∈ A then 0 else 1 )"definition  zero_set :: "(nat => nat) => nat set" where  "zero_set = (λ f. { x. f x = 0})"lemma chf_lm_1 [simp]: "zero_set (chf A) = A" by (unfold chf_def, unfold zero_set_def, simp)lemma chf_lm_2: "(x ∈ A) = (chf A x = 0)" by (unfold chf_def, simp)lemma chf_lm_3: "(x ∉ A) = (chf A x = 1)" by (unfold chf_def, simp)lemma chf_lm_4: "chf A ∈ PrimRec1 ==> A ∈ ce_sets"proof -  assume A: "chf A ∈ PrimRec1"  def p_def: p ≡ "chf A"  from A p_def have p_is_pr: "p ∈ PrimRec1" by auto  def q_def: q ≡ "λ x (y::nat). p x"  from p_is_pr have q_is_pr: "q ∈ PrimRec2" unfolding q_def by prec  have S1: "A = {x. p(x) = 0}"  proof -    have "zero_set p = A" by (unfold p_def, simp)    thus ?thesis by (simp add: zero_set_def)  qed  have S2: "fn_to_set q = {x. ∃ y. q x y = 0}" by (simp add: fn_to_set_def)  have S3: "!! x. (p x = 0) = (∃ y. q x y = 0)" by (unfold q_def, auto)  then have S4: "{x. p x = 0} = {x. ∃ y. q x y = 0}" by auto  with S1 S2 have S5: "fn_to_set q = A" by auto  from q_is_pr have "fn_to_set q ∈ ce_sets" by (rule ce_set_lm_1)  with S5 show ?thesis by autoqedlemma chf_lm_5: "finite A ==> chf A ∈ PrimRec1"proof -  assume A: "finite A"  def u_def: u ≡ "set_to_nat A"  from A have S1: "nat_to_set u = A" by (unfold u_def, rule nat_to_set_srj)  have "chf A = (λ x. sgn2 (c_in x u))"  proof    fix x show "chf A x = sgn2 (c_in x u)"    proof cases      assume A: "x ∈ A"      then have S1_1: "chf A x = 0" by (simp add: chf_lm_2)      from A S1 have "x ∈ nat_to_set u" by auto      then have "c_in x u = 1" by (simp add: x_in_u_eq)      with S1_1 show ?thesis by simp    next      assume A: "x ∉ A"      then have S1_1: "chf A x = 1" by (simp add: chf_def)      from A S1 have "x ∉ nat_to_set u" by auto      then have "c_in x u = 0" by (simp add: x_in_u_eq c_in_def)      with S1_1 show ?thesis by simp    qed  qed  moreover from c_in_is_pr have "(λ x. sgn2 (c_in x u)) ∈ PrimRec1" by prec  ultimately show ?thesis by autoqedtheorem ce_finite: "finite A ==> A ∈ ce_sets"proof -  assume A: "finite A"  then have "chf A ∈ PrimRec1" by (rule chf_lm_5)  then show ?thesis by (rule chf_lm_4)qedsubsection {* Computably enumerable relations *}definition  ce_set_to_rel :: "nat set => (nat * nat) set" where  "ce_set_to_rel = (λ A. { (c_fst x, c_snd x) | x. x ∈ A})"definition  ce_rel_to_set :: "(nat * nat) set => nat set" where  "ce_rel_to_set = (λ R. { c_pair x y | x y. (x,y) ∈ R})"definition  ce_rels :: "((nat * nat) set) set" where  "ce_rels = { R | R. ce_rel_to_set R ∈ ce_sets }"lemma ce_rel_lm_1 [simp]: "ce_set_to_rel (ce_rel_to_set r) = r"proof  show " ce_set_to_rel (ce_rel_to_set r) ⊆ r"  proof fix z    assume A: "z ∈ ce_set_to_rel (ce_rel_to_set r)"    then obtain u where L1: "u ∈ (ce_rel_to_set r)" and L2: "z = (c_fst u, c_snd u)"      unfolding ce_set_to_rel_def by auto    from L1 obtain x y where L3: "(x,y) ∈ r" and L4: "u = c_pair x y"      unfolding ce_rel_to_set_def by auto    from L4 have L5: "c_fst u = x" by simp    from L4 have L6: "c_snd u = y" by simp    from L5 L6 L2 have "z = (x,y)" by simp    with L3 show "z ∈ r" by auto  qednext  show "r ⊆ ce_set_to_rel (ce_rel_to_set r)"  proof fix z show "z ∈ r ==> z ∈ ce_set_to_rel (ce_rel_to_set r)"    proof -      assume A: "z ∈ r"      def x_def: x ≡ "fst z"      def y_def: y ≡ "snd z"      from x_def y_def have L1: "z = (x,y)" by simp      def u_def: u ≡ "c_pair x y"      from A L1 u_def have L2: "u ∈ ce_rel_to_set r" by (unfold ce_rel_to_set_def, auto)      from L1 u_def have L3: "z = (c_fst u, c_snd u)" by simp      from L2 L3 show "z ∈ ce_set_to_rel (ce_rel_to_set r)" by (unfold ce_set_to_rel_def, auto)    qed  qedqedlemma ce_rel_lm_2 [simp]: "ce_rel_to_set (ce_set_to_rel A) = A"proof  show "ce_rel_to_set (ce_set_to_rel A) ⊆ A"  proof fix z show "z ∈ ce_rel_to_set (ce_set_to_rel A) ==> z ∈ A"    proof -      assume A: "z ∈ ce_rel_to_set (ce_set_to_rel A)"      then obtain x y where L1: "z = c_pair x y" and L2: "(x,y) ∈ ce_set_to_rel A"        unfolding ce_rel_to_set_def by auto      from L2 obtain u where L3: "(x,y) = (c_fst u, c_snd u)" and L4: "u ∈ A"        unfolding ce_set_to_rel_def by auto      from L3 L1 have L5: "z = u" by simp      with L4 show "z ∈ A" by auto    qed  qednext  show "A ⊆ ce_rel_to_set (ce_set_to_rel A)"  proof fix z show "z ∈ A ==> z ∈ ce_rel_to_set (ce_set_to_rel A)"    proof -      assume A: "z ∈ A"      then have L1: "(c_fst z, c_snd z) ∈ ce_set_to_rel A" by (unfold ce_set_to_rel_def, auto)      def x_def: x ≡ "c_fst z"      def y_def: y ≡ "c_snd z"      from L1 x_def y_def have L2: "(x,y) ∈ ce_set_to_rel A" by simp      then have L3: "c_pair x y ∈ ce_rel_to_set (ce_set_to_rel A)" by (unfold ce_rel_to_set_def, auto)      with x_def y_def show "z ∈ ce_rel_to_set (ce_set_to_rel A)" by simp    qed  qedqedlemma ce_rels_def1: "ce_rels = { ce_set_to_rel A | A. A ∈ ce_sets}"proof  show "ce_rels ⊆ {ce_set_to_rel A |A. A ∈ ce_sets}"  proof fix r show " r ∈ ce_rels ==> r ∈ {ce_set_to_rel A |A. A ∈ ce_sets}"    proof -      assume A: "r ∈ ce_rels"      then have L1: "ce_rel_to_set r ∈ ce_sets" by (unfold ce_rels_def, auto)      def A_def: A ≡ "ce_rel_to_set r"      from A_def L1 have L2: "A ∈ ce_sets" by auto      from A_def have L3: "ce_set_to_rel A = r" by simp      with L2 show "r ∈ {ce_set_to_rel A |A. A ∈ ce_sets}" by auto    qed  qednext  show "{ce_set_to_rel A |A. A ∈ ce_sets} ⊆ ce_rels"  proof fix r show "r ∈ {ce_set_to_rel A |A. A ∈ ce_sets} ==> r ∈ ce_rels"    proof -      assume A: "r ∈ {ce_set_to_rel A |A. A ∈ ce_sets}"      then obtain A where L1: "r = ce_set_to_rel A" and L2: "A ∈ ce_sets" by auto      from L1 have "ce_rel_to_set r = A" by simp      with L2 show "r ∈ ce_rels" unfolding ce_rels_def by auto    qed  qedqedlemma ce_rel_to_set_inj: "inj ce_rel_to_set"proof (rule inj_on_inverseI)  fix x assume A: "(x::(nat×nat) set) ∈ UNIV" show "ce_set_to_rel (ce_rel_to_set x) = x" by (rule ce_rel_lm_1)qedlemma ce_rel_to_set_srj: "surj ce_rel_to_set"proof (rule surjI [where ?f=ce_set_to_rel])  fix x show "ce_rel_to_set (ce_set_to_rel x) = x" by (rule ce_rel_lm_2)qedlemma ce_rel_to_set_bij: "bij ce_rel_to_set"proof (rule bijI)  show "inj ce_rel_to_set" by (rule ce_rel_to_set_inj)next  show "surj ce_rel_to_set" by (rule ce_rel_to_set_srj)qedlemma ce_set_to_rel_inj: "inj ce_set_to_rel"proof (rule inj_on_inverseI)  fix x assume A: "(x::nat set) ∈ UNIV" show "ce_rel_to_set (ce_set_to_rel x) = x" by (rule ce_rel_lm_2)qedlemma ce_set_to_rel_srj: "surj ce_set_to_rel"proof (rule surjI [where ?f=ce_rel_to_set])  fix x show "ce_set_to_rel (ce_rel_to_set x) = x" by (rule ce_rel_lm_1)qedlemma ce_set_to_rel_bij: "bij ce_set_to_rel"proof (rule bijI)  show "inj ce_set_to_rel" by (rule ce_set_to_rel_inj)next  show "surj ce_set_to_rel" by (rule ce_set_to_rel_srj)qedlemma ce_rel_lm_3: "A ∈ ce_sets ==> ce_set_to_rel A ∈ ce_rels"proof -  assume A: "A ∈ ce_sets"  from A ce_rels_def1 show ?thesis by autoqedlemma ce_rel_lm_4: "ce_set_to_rel A ∈ ce_rels ==> A ∈ ce_sets"proof -  assume A: "ce_set_to_rel A ∈ ce_rels"  from A show ?thesis by (unfold ce_rels_def, auto)qedlemma ce_rel_lm_5: "(A ∈ ce_sets) = (ce_set_to_rel A ∈ ce_rels)"proof  assume "A ∈ ce_sets" then show "ce_set_to_rel A ∈ ce_rels" by (rule ce_rel_lm_3)next  assume "ce_set_to_rel A ∈ ce_rels" then show "A ∈ ce_sets" by (rule ce_rel_lm_4)qedlemma ce_rel_lm_6: "r ∈ ce_rels ==> ce_rel_to_set r ∈ ce_sets"proof -  assume A: "r ∈ ce_rels"  then show ?thesis by (unfold ce_rels_def, auto)qedlemma ce_rel_lm_7: "ce_rel_to_set r ∈ ce_sets ==> r ∈ ce_rels"proof -  assume "ce_rel_to_set r ∈ ce_sets"  then show ?thesis by (unfold ce_rels_def, auto)qedlemma ce_rel_lm_8: "(r ∈ ce_rels) = (ce_rel_to_set r ∈ ce_sets)" by (unfold ce_rels_def, auto)lemma ce_rel_lm_9: "(x,y) ∈ r ==> c_pair x y ∈ ce_rel_to_set r" by (unfold ce_rel_to_set_def, auto)lemma ce_rel_lm_10: "x ∈ A ==> (c_fst x, c_snd x) ∈ ce_set_to_rel A" by (unfold ce_set_to_rel_def, auto)lemma ce_rel_lm_11: "c_pair x y ∈ ce_rel_to_set r ==> (x,y) ∈ r"proof -  assume A: "c_pair x y ∈ ce_rel_to_set r"  let ?z = "c_pair x y"  from A have "(c_fst ?z, c_snd ?z) ∈ ce_set_to_rel (ce_rel_to_set r)" by (rule ce_rel_lm_10)  then show "(x,y) ∈ r" by simpqedlemma ce_rel_lm_12: "(c_pair x y ∈ ce_rel_to_set r) = ((x,y) ∈ r)"proof  assume "c_pair x y ∈ ce_rel_to_set r" then show "(x, y) ∈ r" by (rule ce_rel_lm_11)next  assume "(x, y) ∈ r" then show "c_pair x y ∈ ce_rel_to_set r" by (rule ce_rel_lm_9)qedlemma ce_rel_lm_13: "(x,y) ∈ ce_set_to_rel A ==> c_pair x y ∈ A"proof -  assume "(x,y) ∈ ce_set_to_rel A"  then have "c_pair x y ∈ ce_rel_to_set (ce_set_to_rel A)" by (rule ce_rel_lm_9)  then show ?thesis by simpqedlemma ce_rel_lm_14: "c_pair x y ∈ A ==> (x,y) ∈ ce_set_to_rel A"proof -  assume "c_pair x y ∈ A"  then have "c_pair x y ∈ ce_rel_to_set (ce_set_to_rel A)" by simp  then show ?thesis by (rule ce_rel_lm_11)qedlemma ce_rel_lm_15: "((x,y) ∈ ce_set_to_rel A) = (c_pair x y ∈ A)"proof  assume "(x, y) ∈ ce_set_to_rel A" then show "c_pair x y ∈ A" by (rule ce_rel_lm_13)next  assume "c_pair x y ∈ A" then show "(x, y) ∈ ce_set_to_rel A" by (rule ce_rel_lm_14)qedlemma ce_rel_lm_16: "x ∈ ce_rel_to_set r ==> (c_fst x, c_snd x) ∈ r"proof -  assume "x ∈ ce_rel_to_set r"  then have "(c_fst x, c_snd x) ∈ ce_set_to_rel (ce_rel_to_set r)" by (rule ce_rel_lm_10)  then show ?thesis by simpqedlemma ce_rel_lm_17: "(c_fst x, c_snd x) ∈ ce_set_to_rel A ==> x ∈ A"proof -  assume "(c_fst x, c_snd x) ∈ ce_set_to_rel A"  then have "c_pair (c_fst x) (c_snd x) ∈ A" by (rule ce_rel_lm_13)  then show ?thesis by simpqedlemma ce_rel_lm_18: "((c_fst x, c_snd x) ∈ ce_set_to_rel A) = (x ∈ A)"proof  assume "(c_fst x, c_snd x) ∈ ce_set_to_rel A" then show "x ∈ A" by (rule ce_rel_lm_17)next  assume "x ∈ A" then show "(c_fst x, c_snd x) ∈ ce_set_to_rel A" by (rule ce_rel_lm_10)qedlemma ce_rel_lm_19: "(c_fst x, c_snd x) ∈ r ==> x ∈ ce_rel_to_set r"proof -  assume "(c_fst x, c_snd x) ∈ r"  then have "(c_fst x, c_snd x) ∈ ce_set_to_rel (ce_rel_to_set r)" by simp  then show ?thesis by (rule ce_rel_lm_17)qedlemma ce_rel_lm_20: "((c_fst x, c_snd x) ∈ r) = (x ∈ ce_rel_to_set r)"proof  assume "(c_fst x, c_snd x) ∈ r" then show "x ∈ ce_rel_to_set r" by (rule ce_rel_lm_19)next  assume "x ∈ ce_rel_to_set r" then show "(c_fst x, c_snd x) ∈ r" by (rule ce_rel_lm_16)qedlemma ce_rel_lm_21: "r ∈ ce_rels ==> ∃ p ∈ PrimRec3. ∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)"proof -  assume r_ce: "r ∈ ce_rels"  def A_def: A ≡ "ce_rel_to_set r"  from r_ce have A_ce: "A ∈ ce_sets" by (unfold A_def, rule ce_rel_lm_6)  then have "∃ p ∈ PrimRec2. A = fn_to_set p" by (rule ce_set_lm_3)  then obtain q where q_is_pr: "q ∈ PrimRec2" and A_def1: "A = fn_to_set q" ..  from A_def1 have A_def2: "A = { x. ∃ y. q x y = 0}" by (unfold fn_to_set_def)  def p_def: p ≡ "λ x y u. q (c_pair x y) u"  from q_is_pr have p_is_pr: "p ∈ PrimRec3" unfolding p_def by prec  have "!! x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)"  proof - fix x y show "((x,y) ∈ r) = (∃ u. p x y u = 0)"    proof      assume A: "(x,y) ∈ r"      def z_def: z ≡ "c_pair x y"      with A_def A have z_in_A: "z ∈ A" by (unfold ce_rel_to_set_def, auto)      with A_def2 have "z ∈ { x. ∃ y. q x y = 0}" by auto      then obtain u where "q z u = 0" by auto      with z_def have "p x y u = 0" by (simp add: z_def p_def)      then show "∃ u. p x y u = 0" by auto    next      assume A: "∃ u. p x y u = 0"      def z_def: z ≡ "c_pair x y"      from A obtain u where "p x y u = 0" by auto      then have q_z: "q z u = 0" by (simp add: z_def p_def)      with A_def2 have z_in_A: "z ∈ A" by auto      then have "c_pair x y ∈ A" by (unfold z_def)      then have "c_pair x y ∈ ce_rel_to_set r" by (unfold A_def)      then show "(x,y) ∈ r" by (rule ce_rel_lm_11)    qed  qed  with p_is_pr show ?thesis by autoqedlemma ce_rel_lm_22: "r ∈ ce_rels ==> ∃ p ∈ PrimRec3. r = { (x,y). ∃ u. p x y u = 0 }"proof -  assume r_ce: "r ∈ ce_rels"  then have "∃ p ∈ PrimRec3. ∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)" by (rule ce_rel_lm_21)  then obtain p where p_is_pr: "p ∈ PrimRec3" and L1: "∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)" by auto  from p_is_pr L1 show ?thesis by blastqedlemma ce_rel_lm_23: "[| p ∈ PrimRec3; ∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0) |] ==> r ∈ ce_rels"proof -  assume p_is_pr: "p ∈ PrimRec3"  assume A: "∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)"  def q_def: q ≡ "λ z u. p (c_fst z) (c_snd z) u"  from p_is_pr have q_is_pr: "q ∈ PrimRec2" unfolding q_def by prec  def A_def: A ≡ "{ x. ∃ y. q x y = 0}"  then have A_def1: "A = fn_to_set q" by (unfold fn_to_set_def, auto)  from q_is_pr A_def1 have A_ce: "A ∈ ce_sets" by (simp add: ce_set_lm_1)  have main: "A = ce_rel_to_set r"  proof    show "A ⊆ ce_rel_to_set r"    proof fix z assume z_in_A: "z ∈ A" show "z ∈ ce_rel_to_set r"      proof -        def x_def: x ≡ "c_fst z"        def y_def: y ≡ "c_snd z"        from z_in_A A_def obtain u where L2: "q z u = 0" by auto        with x_def y_def q_def have L3: "p x y u = 0" by simp        then have "∃u. p x y u = 0" by auto        with A have "(x,y) ∈ r" by auto        then have "c_pair x y ∈ ce_rel_to_set r" by (rule ce_rel_lm_9)        with x_def y_def show ?thesis by simp      qed    qed  next  show "ce_rel_to_set r ⊆ A"  proof fix z assume z_in_r: "z ∈ ce_rel_to_set r" show "z ∈ A"    proof -      def x_def: x ≡ "c_fst z"      def y_def: y ≡ "c_snd z"      from z_in_r have "(c_fst z, c_snd z) ∈ r" by (rule ce_rel_lm_16)      with x_def y_def have "(x,y) ∈ r" by simp      with A obtain u where L1: "p x y u = 0" by auto      with x_def y_def q_def have "q z u = 0" by simp      with A_def show "z ∈ A" by auto    qed  qed  qed  with A_ce have "ce_rel_to_set r ∈ ce_sets" by auto  then show "r ∈ ce_rels" by (rule ce_rel_lm_7)qedlemma ce_rel_lm_24: "[| r ∈ ce_rels; s ∈ ce_rels |] ==> s O r ∈ ce_rels"proof -  assume r_ce: "r ∈ ce_rels"  assume s_ce: "s ∈ ce_rels"  from r_ce have "∃ p ∈ PrimRec3. ∀ x y. ((x,y) ∈ r)=(∃ u. p x y u = 0)" by (rule ce_rel_lm_21)  then obtain p_r where p_r_is_pr: "p_r ∈ PrimRec3" and R1: "∀ x y. ((x,y) ∈ r)=(∃ u. p_r x y u = 0)" by auto  from s_ce have "∃ p ∈ PrimRec3. ∀ x y. ((x,y) ∈ s)=(∃ u. p x y u = 0)" by (rule ce_rel_lm_21)  then obtain p_s where p_s_is_pr: "p_s ∈ PrimRec3" and S1: "∀ x y. ((x,y) ∈ s)=(∃ u. p_s x y u = 0)" by auto  def p_def: p ≡ "λ x z u. (p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u)))"  from p_r_is_pr p_s_is_pr have p_is_pr: "p ∈ PrimRec3" unfolding p_def by prec  def sr_def: sr ≡ "s O r"  have main: "∀ x z. ((x,z) ∈ sr) = (∃ u. p x z u = 0)"  proof (rule allI, rule allI) fix x z show "((x, z) ∈ sr) = (∃u. p x z u = 0)"    proof assume A: "(x, z) ∈ sr" show "∃u. p x z u = 0"      proof -        from A sr_def obtain y where L1: "(x,y) ∈ s" and L2: "(y,z) ∈ r" by auto        from L1 S1 obtain u_s where L3: "p_s x y u_s = 0" by auto        from L2 R1 obtain u_r where L4: "p_r y z u_r = 0" by auto        def u_def: u ≡ "c_pair y (c_pair u_s u_r)"        from L3 L4 have "p x z u = 0" by (unfold p_def, unfold u_def, simp)        then show ?thesis by auto      qed    next      assume A: "∃u. p x z u = 0" show "(x, z) ∈ sr"      proof -        from A obtain u where L1: "p x z u = 0" by auto        then have L2: "(p_s x (c_fst u) (c_fst (c_snd u))) + (p_r (c_fst u) z (c_snd (c_snd u))) = 0" by (unfold p_def)        from L2 have L3: "p_s x (c_fst u) (c_fst (c_snd u)) = 0" by auto        from L2 have L4: "p_r (c_fst u) z (c_snd (c_snd u)) = 0" by auto        from L3 S1 have L5: "(x,(c_fst u)) ∈ s" by auto        from L4 R1 have L6: "((c_fst u),z) ∈ r" by auto        from L5 L6 have "(x,z) ∈ s O r" by auto        with sr_def show ?thesis by auto      qed    qed  qed  from p_is_pr main have "sr ∈ ce_rels" by (rule ce_rel_lm_23)  then show ?thesis by (unfold sr_def)qedlemma ce_rel_lm_25: "r ∈ ce_rels ==> r^-1 ∈ ce_rels"proof -  assume r_ce: "r ∈ ce_rels"  have "r^-1 = {(y,x). (x,y) ∈ r}" by auto  then have L1: "∀ x y. ((x,y) ∈ r) = ((y,x) ∈ r^-1)" by auto  from r_ce have "∃ p ∈ PrimRec3. ∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)" by (rule ce_rel_lm_21)  then obtain p where p_is_pr: "p ∈ PrimRec3" and R1: "∀ x y. ((x,y) ∈ r) = (∃ u. p x y u = 0)" by auto  def q_def: q ≡ "λ x y u. p y x u"  from p_is_pr have q_is_pr: "q ∈ PrimRec3" unfolding q_def by prec  from L1 R1 have L2: "∀ x y. ((x,y) ∈ r^-1) = (∃ u. p y x u = 0)" by auto  with q_def have L3: "∀ x y. ((x,y) ∈ r^-1) = (∃ u. q x y u = 0)" by auto  with q_is_pr show ?thesis by (rule ce_rel_lm_23)qedlemma ce_rel_lm_26: "r ∈ ce_rels ==> Domain r ∈ ce_sets"proof -  assume r_ce: "r ∈ ce_rels"  have L1: "∀ x. (x ∈ Domain r) = (∃ y. (x,y) ∈ r)" by auto  def A_def: A ≡ "ce_rel_to_set r"  from r_ce have "ce_rel_to_set r ∈ ce_sets" by (rule ce_rel_lm_6)  then have A_ce: "A ∈ ce_sets" by (unfold A_def)  have "∀ x y. ((x,y) ∈ r) = (c_pair x y ∈ ce_rel_to_set r)" by (simp add: ce_rel_lm_12)  then have L2: "∀ x y. ((x,y) ∈ r) = (c_pair x y ∈ A)" by (unfold A_def)  from A_ce c_fst_is_pr have L3: "{ c_fst z |z.  z ∈ A } ∈ ce_sets" by (rule ce_set_lm_7)  have L4: "∀ x. (x ∈ { c_fst z |z.  z ∈ A }) =(∃ y. c_pair x y ∈ A)"  proof fix x show "(x ∈ { c_fst z |z.  z ∈ A }) =(∃ y. c_pair x y ∈ A)"    proof      assume A: "x ∈ {c_fst z |z. z ∈ A}"      then obtain z where z_in_A: "z ∈ A" and x_z: "x = c_fst z" by auto      from x_z have "z = c_pair x (c_snd z)" by simp      with z_in_A have "c_pair x (c_snd z) ∈ A" by auto      then show "∃y. c_pair x y ∈ A" by auto    next      assume A: "∃y. c_pair x y ∈ A"      then obtain y where y_1: "c_pair x y ∈ A" by auto      def z_def: z ≡ "c_pair x y"      from y_1 have z_in_A: "z ∈ A" by (unfold z_def)      from z_def have x_z: "x = c_fst z" by (unfold z_def, simp)      from z_in_A x_z show "x ∈ {c_fst z |z. z ∈ A}" by auto    qed  qed  from L1 L2 have L5: "∀ x. (x ∈ Domain r) = (∃ y. c_pair x y ∈ A)" by auto  from L4 L5 have L6: "∀ x. (x ∈ Domain r) = (x ∈ { c_fst z |z.  z ∈ A })" by auto  then have "Domain r = { c_fst z |z.  z ∈ A }" by auto    with L3 show "Domain r ∈ ce_sets" by autoqedlemma ce_rel_lm_27: "r ∈ ce_rels ==> Range r ∈ ce_sets"proof -  assume r_ce: "r ∈ ce_rels"  then have "r^-1 ∈ ce_rels" by (rule ce_rel_lm_25)  then have "Domain (r^-1) ∈ ce_sets" by (rule ce_rel_lm_26)  then show ?thesis by (unfold Domain_converse [symmetric])qedlemma ce_rel_lm_28: "r ∈ ce_rels ==> Field r ∈ ce_sets"proof -  assume r_ce: "r ∈ ce_rels"  from r_ce have L1: "Domain r ∈ ce_sets" by (rule ce_rel_lm_26)  from r_ce have L2: "Range r ∈ ce_sets" by (rule ce_rel_lm_27)  from L1 L2 have L3: "Domain r ∪ Range r ∈ ce_sets" by (rule ce_union)  then show ?thesis by (unfold Field_def)qedlemma ce_rel_lm_29: "[| A ∈ ce_sets; B ∈ ce_sets |] ==> A × B ∈ ce_rels"proof -  assume A_ce: "A ∈ ce_sets"  assume B_ce: "B ∈ ce_sets"  def r_a_def: r_a ≡ "{ (x,(0::nat)) | x. x ∈ A}"  def r_b_def: r_b ≡ "{ ((0::nat),z) | z. z ∈ B}"  have L1: "r_a O r_b = A × B" by (unfold r_a_def, unfold r_b_def, auto)  have r_a_ce: "r_a ∈ ce_rels"  proof -    have loc1: "ce_rel_to_set r_a = { c_pair x 0 | x. x ∈ A}" by (unfold r_a_def, unfold ce_rel_to_set_def, auto)    def p_def: p ≡ "λ x. c_pair x 0"    have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec    from A_ce p_is_pr have "{ c_pair x 0 | x. x ∈ A} ∈ ce_sets" by (simp add: p_def ce_set_lm_7)    with loc1 have "ce_rel_to_set r_a ∈ ce_sets" by auto    then show ?thesis by (rule ce_rel_lm_7)  qed  have r_b_ce: "r_b ∈ ce_rels"  proof -    have loc1: "ce_rel_to_set r_b = { c_pair 0 z | z. z ∈ B}" by (unfold r_b_def, unfold ce_rel_to_set_def, auto)    def p_def: p ≡ "λ z. c_pair 0 z"    have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec    from B_ce p_is_pr have "{ c_pair 0 z | z. z ∈ B} ∈ ce_sets" by (simp add: p_def ce_set_lm_7)    with loc1 have "ce_rel_to_set r_b ∈ ce_sets" by auto    then show ?thesis by (rule ce_rel_lm_7)  qed  from r_b_ce r_a_ce have "r_a O r_b ∈ ce_rels" by (rule ce_rel_lm_24)  with L1 show ?thesis by autoqedlemma ce_rel_lm_30: "{} ∈ ce_rels"proof -  have "ce_rel_to_set {} = {}" by (unfold ce_rel_to_set_def, auto)  with ce_empty have "ce_rel_to_set {} ∈ ce_sets" by auto  then show ?thesis by (rule ce_rel_lm_7)qedlemma ce_rel_lm_31: "UNIV ∈ ce_rels"proof -  from ce_univ ce_univ have "UNIV × UNIV ∈ ce_rels" by (rule ce_rel_lm_29)  then show ?thesis by autoqedlemma ce_rel_lm_32: "ce_rel_to_set (r ∪ s) = (ce_rel_to_set r) ∪ (ce_rel_to_set s)" by (unfold ce_rel_to_set_def, auto)lemma ce_rel_lm_33: "[| r ∈ ce_rels; s ∈ ce_rels |] ==> r ∪ s ∈ ce_rels"proof -  assume "r ∈ ce_rels"  then have r_ce: "ce_rel_to_set r ∈ ce_sets" by (rule ce_rel_lm_6)  assume "s ∈ ce_rels"  then have s_ce: "ce_rel_to_set s ∈ ce_sets" by (rule ce_rel_lm_6)    have "ce_rel_to_set (r ∪ s) = (ce_rel_to_set r) ∪ (ce_rel_to_set s)" by (unfold ce_rel_to_set_def, auto)  moreover from r_ce s_ce have "(ce_rel_to_set r) ∪ (ce_rel_to_set s) ∈ ce_sets" by (rule ce_union)  ultimately have "ce_rel_to_set (r ∪ s) ∈ ce_sets" by auto  then show ?thesis by (rule ce_rel_lm_7)qedlemma ce_rel_lm_34: "ce_rel_to_set (r ∩ s) = (ce_rel_to_set r) ∩ (ce_rel_to_set s)"proof  show "ce_rel_to_set (r ∩ s) ⊆ ce_rel_to_set r ∩ ce_rel_to_set s" by (unfold ce_rel_to_set_def, auto)next  show "ce_rel_to_set r ∩ ce_rel_to_set s ⊆ ce_rel_to_set (r ∩ s)"  proof fix x assume A: "x ∈ ce_rel_to_set r ∩ ce_rel_to_set s"    from A have L1: "x ∈ ce_rel_to_set r" by auto    from A have L2: "x ∈ ce_rel_to_set s" by auto    from L1 obtain u v where L3: "(u,v) ∈ r" and L4: "x = c_pair u v"       unfolding ce_rel_to_set_def by auto    from L2 obtain u1 v1 where L5: "(u1,v1) ∈ s" and L6: "x = c_pair u1 v1"       unfolding ce_rel_to_set_def by auto    from L4 L6 have L7: "c_pair u1 v1 = c_pair u v" by auto    then have "u1=u" by (rule c_pair_inj1)    moreover from L7 have "v1=v" by (rule c_pair_inj2)    ultimately have "(u,v)=(u1,v1)" by auto    with L3 L5 have "(u,v) ∈ r ∩ s" by auto    with L4 show "x ∈ ce_rel_to_set (r ∩ s)" by (unfold ce_rel_to_set_def, auto)  qedqedlemma ce_rel_lm_35: "[| r ∈ ce_rels; s ∈ ce_rels |] ==> r ∩ s ∈ ce_rels"proof -  assume "r ∈ ce_rels"  then have r_ce: "ce_rel_to_set r ∈ ce_sets" by (rule ce_rel_lm_6)  assume "s ∈ ce_rels"  then have s_ce: "ce_rel_to_set s ∈ ce_sets" by (rule ce_rel_lm_6)    have "ce_rel_to_set (r ∩ s) = (ce_rel_to_set r) ∩ (ce_rel_to_set s)" by (rule ce_rel_lm_34)  moreover from r_ce s_ce have "(ce_rel_to_set r) ∩ (ce_rel_to_set s) ∈ ce_sets" by (rule ce_intersect)  ultimately have "ce_rel_to_set (r ∩ s) ∈ ce_sets" by auto  then show ?thesis by (rule ce_rel_lm_7)qedlemma ce_rel_lm_36: "ce_set_to_rel (A ∪ B) = (ce_set_to_rel A) ∪ (ce_set_to_rel B)" by (unfold ce_set_to_rel_def, auto)lemma ce_rel_lm_37: "ce_set_to_rel (A ∩ B) = (ce_set_to_rel A) ∩ (ce_set_to_rel B)"proof -  def f_def: f ≡ "λ x. (c_fst x, c_snd x)"  have f_inj: "inj f"  proof (unfold f_def, rule inj_on_inverseI [where ?g="λ (u,v). c_pair u v"])    fix x assume "(x::nat) ∈ UNIV" show "split c_pair (c_fst x, c_snd x) = x" by simp  qed  from f_inj have "f ` (A ∩ B) = f ` A ∩ f ` B" by (rule image_Int)  then show ?thesis by (unfold f_def, unfold ce_set_to_rel_def, auto)qedlemma ce_rel_lm_38: "[| r ∈ ce_rels; A ∈ ce_sets |] ==> r``A ∈ ce_sets"proof -  assume r_ce: "r ∈ ce_rels"  assume A_ce: "A ∈ ce_sets"  have L1: "r``A = Range (r ∩ A × UNIV)" by blast  have L2: "Range (r ∩ A × UNIV) ∈ ce_sets"  proof (rule ce_rel_lm_27)    show "r ∩ A × UNIV ∈ ce_rels"    proof (rule ce_rel_lm_35)      show "r ∈ ce_rels" by (rule r_ce)    next      show "A × UNIV ∈ ce_rels"      proof (rule ce_rel_lm_29)        show "A ∈ ce_sets" by (rule A_ce)      next        show "UNIV ∈ ce_sets" by (rule ce_univ)      qed    qed  qed  from L1 L2 show ?thesis by autoqedsubsection {* Total computable functions *}definition  graph :: "(nat => nat) => (nat × nat) set" where  "graph = (λ f. { (x, f x) | x. x ∈ UNIV})"lemma graph_lm_1: "(x,y) ∈ graph f ==> y = f x" by (unfold graph_def, auto)lemma graph_lm_2: "y = f x ==> (x,y) ∈ graph f" by (unfold graph_def, auto)lemma graph_lm_3: "((x,y) ∈ graph f) = (y = f x)" by (unfold graph_def, auto)lemma graph_lm_4: "graph (f o g) = (graph g) O (graph f)" by (unfold graph_def, auto)definition  c_graph :: "(nat => nat) => nat set" where  "c_graph = (λ f. { c_pair x (f x) | x. x ∈ UNIV})"lemma c_graph_lm_1: "c_pair x y ∈ c_graph f ==> y = f x"proof -  assume A: "c_pair x y ∈ c_graph f"  have S1: "c_graph f = {c_pair x (f x) | x. x ∈ UNIV}" by (simp add: c_graph_def)  from A S1 obtain z where S2: "c_pair x y = c_pair z (f z)" by auto  then have "x = z" by (rule c_pair_inj1)  moreover from S2 have "y = f z" by (rule c_pair_inj2)  ultimately show ?thesis by autoqedlemma c_graph_lm_2: "y = f x ==> c_pair x y ∈ c_graph f" by (unfold c_graph_def, auto)lemma c_graph_lm_3: "(c_pair x y ∈ c_graph f) = (y = f x)"proof  assume "c_pair x y ∈ c_graph f" then show "y = f x" by (rule c_graph_lm_1)next  assume "y = f x" then show "c_pair x y ∈ c_graph f" by (rule c_graph_lm_2)qedlemma c_graph_lm_4: "c_graph f = ce_rel_to_set (graph f)" by (unfold c_graph_def ce_rel_to_set_def graph_def, auto)lemma c_graph_lm_5: "graph f = ce_set_to_rel (c_graph f)" by (simp add: c_graph_lm_4)definition  total_recursive :: "(nat => nat) => bool" where  "total_recursive = (λ f. graph f ∈ ce_rels)"lemma total_recursive_def1: "total_recursive = (λ f. c_graph f ∈ ce_sets)"proof (rule ext) fix f show " total_recursive f = (c_graph f ∈ ce_sets)"  proof    assume A: "total_recursive f"    then have "graph f ∈ ce_rels" by (unfold total_recursive_def)    then have "ce_rel_to_set (graph f) ∈ ce_sets" by (rule ce_rel_lm_6)    then show "c_graph f ∈ ce_sets" by (simp add: c_graph_lm_4)  next    assume "c_graph f ∈ ce_sets"    then have "ce_rel_to_set (graph f) ∈ ce_sets" by (simp add: c_graph_lm_4)    then have "graph f ∈ ce_rels" by (rule ce_rel_lm_7)    then show "total_recursive f" by (unfold total_recursive_def)  qedqedtheorem pr_is_total_rec: "f ∈ PrimRec1 ==> total_recursive f"proof -  assume A: "f ∈ PrimRec1"  def p_def: p ≡ "λ x. c_pair x (f x)"  from A have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec  let ?U = "{ p x | x. x ∈ UNIV }"  from ce_univ p_is_pr have U_ce: "?U ∈ ce_sets" by (rule ce_set_lm_7)  have U_1: "?U = { c_pair x (f x) | x. x ∈ UNIV}" by (simp add: p_def)  with U_ce have S1: "{ c_pair x (f x) | x. x ∈ UNIV} ∈ ce_sets" by simp  with c_graph_def have c_graph_f_is_ce: "c_graph f ∈ ce_sets" by (unfold c_graph_def, auto)  then show ?thesis by (unfold total_recursive_def1, auto)qedtheorem comp_tot_rec: "[| total_recursive f; total_recursive g |] ==> total_recursive (f o g)"proof -  assume "total_recursive f"  then have f_ce: "graph f ∈ ce_rels" by (unfold total_recursive_def)  assume "total_recursive g"  then have g_ce: "graph g ∈ ce_rels" by (unfold total_recursive_def)  from f_ce g_ce have "graph g O graph f ∈ ce_rels" by (rule ce_rel_lm_24)  then have "graph (f o g) ∈ ce_rels" by (simp add: graph_lm_4)  then show ?thesis by (unfold total_recursive_def)qedlemma univ_for_pr_tot_rec_lm: "c_graph univ_for_pr ∈ ce_sets"proof -  def A_def: A ≡ "c_graph univ_for_pr"  from A_def have S1: "A = { c_pair x (univ_for_pr x) | x. x ∈ UNIV }" by (simp add: c_graph_def)  from S1 have S2: "A = { z . ∃ x. z = c_pair x (univ_for_pr x) }" by auto  have S3: "!! z. (∃ x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"  proof -    fix z show "(∃ x. (z = c_pair x (univ_for_pr x))) = (univ_for_pr (c_fst z) = c_snd z)"    proof      assume A: "∃x. z = c_pair x (univ_for_pr x)"      then obtain x where S3_1: "z = c_pair x (univ_for_pr x)" ..      then show "univ_for_pr (c_fst z) = c_snd z" by simp    next      assume A: "univ_for_pr (c_fst z) = c_snd z"      from A have "z = c_pair (c_fst z) (univ_for_pr (c_fst z))" by simp      thus "∃x. z = c_pair x (univ_for_pr x)" ..    qed  qed  with S2 have S4: "A = { z . univ_for_pr (c_fst z) = c_snd z }" by auto  def p_def: p ≡ "λ x y. if c_assoc_have_key (pr_gr y) (c_fst x) = 0 then                         (if c_assoc_value (pr_gr y) (c_fst x) = c_snd x then (0::nat) else 1) else 1"  from c_assoc_have_key_is_pr c_assoc_value_is_pr pr_gr_is_pr have p_is_pr: "p ∈ PrimRec2"    unfolding p_def by prec  have S5: "!! z. (univ_for_pr (c_fst z) = c_snd z) = (∃ y. p z y = 0)"  proof -    fix z show "(univ_for_pr (c_fst z) = c_snd z) = (∃ y. p z y = 0)"    proof      assume A: "univ_for_pr (c_fst z) = c_snd z"      let ?n = "c_fst (c_fst z)"      let ?x = "c_snd (c_fst z)"      let ?y = "loc_upb ?n ?x"      have S5_1: "c_assoc_have_key (pr_gr ?y) (c_pair ?n ?x) = 0" by (rule loc_upb_main)      have S5_2: "c_assoc_value (pr_gr ?y) (c_pair ?n ?x) = univ_for_pr (c_pair ?n ?x)" by (rule pr_gr_value)      from S5_1 have S5_3: "c_assoc_have_key (pr_gr ?y) (c_fst z) = 0" by simp      from S5_2 A have S5_4: "c_assoc_value (pr_gr ?y) (c_fst z) = c_snd z" by simp      from S5_3 S5_4 have "p z ?y = 0" by (simp add: p_def)      thus "∃ y. p z y = 0" ..    next      assume A: "∃y. p z y = 0"      then obtain y where S5_1: "p z y = 0" ..      have S5_2: "c_assoc_have_key (pr_gr y) (c_fst z) = 0"      proof (rule ccontr)        assume A_1: "c_assoc_have_key (pr_gr y) (c_fst z) ≠ 0"        then have "p z y = 1" by (simp add: p_def)        with S5_1 show False by auto      qed      then have S5_3: "p z y = (if c_assoc_value (pr_gr y) (c_fst z) = c_snd z then (0::nat) else 1)" by (simp add: p_def)      have S5_4: "c_assoc_value (pr_gr y) (c_fst z) = c_snd z"      proof (rule ccontr)        assume A_2: "c_assoc_value (pr_gr y) (c_fst z) ≠ c_snd z"        then have "p z y = 1" by (simp add: p_def)        with S5_1 show False by auto      qed      have S5_5: "c_is_sub_fun (pr_gr y) univ_for_pr" by (rule pr_gr_1)      from S5_5 S5_2 have S5_6: "c_assoc_value (pr_gr y) (c_fst z) = univ_for_pr (c_fst z)" by (rule c_is_sub_fun_lm_1)      with S5_4 show "univ_for_pr (c_fst z) = c_snd z" by auto    qed  qed  from S5 S4 have "A = {z. ∃ y. p z y = 0}" by auto  then have "A = fn_to_set p" by (simp add: fn_to_set_def)  moreover from p_is_pr have "fn_to_set p ∈ ce_sets" by (rule ce_set_lm_1)  ultimately have "A ∈ ce_sets" by auto  with A_def show ?thesis by autoqedtheorem univ_for_pr_tot_rec: "total_recursive univ_for_pr"proof -  have "c_graph univ_for_pr ∈ ce_sets" by (rule univ_for_pr_tot_rec_lm)  then show ?thesis by (unfold total_recursive_def1, auto)qedsubsection {* Computable sets, Post's theorem *}definition  computable :: "nat set => bool" where  "computable = (λ A. A ∈ ce_sets ∧ -A ∈ ce_sets)"lemma computable_complement_1: "computable A ==> computable (- A)"proof -  assume "computable A"  then show ?thesis by (unfold computable_def, auto)qedlemma computable_complement_2: "computable (- A) ==> computable A"proof -  assume "computable (- A)"  then show ?thesis by (unfold computable_def, auto)qedlemma computable_complement_3: "(computable A) = (computable (- A))" by (unfold computable_def, auto)theorem comp_impl_tot_rec: "computable A ==> total_recursive (chf A)"proof -  assume A: "computable A"  from A have A1: "A ∈ ce_sets" by (unfold computable_def, simp)  from A have A2: "-A ∈ ce_sets" by (unfold computable_def, simp)  def p_def: p ≡ "λ x. c_pair x 0"  def q_def: q ≡ "λ x. c_pair x 1"  from p_def have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec  from q_def have q_is_pr: "q ∈ PrimRec1" unfolding q_def by prec  def U0_def: U0 ≡ "{ p x | x. x ∈ A}"  def U1_def: U1 ≡ "{ q x | x. x ∈ - A}"  from A1 p_is_pr have U0_ce: "U0 ∈ ce_sets" by(unfold U0_def, rule ce_set_lm_7)  from A2 q_is_pr have U1_ce: "U1 ∈ ce_sets" by(unfold U1_def, rule ce_set_lm_7)  def U_def: U ≡ "U0 ∪ U1"  from U0_ce U1_ce have U_ce: "U ∈ ce_sets" by (unfold U_def, rule ce_union)  def V_def: V ≡ "c_graph (chf A)"  have V_1: "V = { c_pair x (chf A x) | x. x ∈ UNIV}" by (simp add: V_def c_graph_def)  from U0_def p_def have U0_1: "U0 = { c_pair x y | x y. x ∈ A ∧ y=0}" by auto  from U1_def q_def have U1_1: "U1 = { c_pair x y | x y. x ∉ A ∧ y=1}" by auto  from U0_1 U1_1 U_def have U_1: "U = { c_pair x y | x y. (x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)}" by auto  from V_1 have V_2: "V = { c_pair x y | x y. y = chf A x}" by auto  have L1: "!! x y. ((x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)) = (y = chf A x)"  proof - fix x y show "((x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)) = (y = chf A x)" by(unfold chf_def, auto)  qed  from V_2 U_1 L1 have "U=V" by simp  with U_ce have V_ce: "V ∈ ce_sets" by auto  with V_def have "c_graph (chf A) ∈ ce_sets" by auto  then show ?thesis by (unfold total_recursive_def1)qedtheorem tot_rec_impl_comp: "total_recursive (chf A) ==> computable A"proof -  assume A: "total_recursive (chf A)"  then have A1: "c_graph (chf A) ∈ ce_sets" by (unfold total_recursive_def1)  let ?U = "c_graph (chf A)"  have L1: "?U = { c_pair x (chf A x) | x. x ∈ UNIV}" by (simp add: c_graph_def)  have L2: "!! x y. ((x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)) = (y = chf A x)"  proof - fix x y show "((x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)) = (y = chf A x)" by(unfold chf_def, auto)  qed  from L1 L2 have L3: "?U = { c_pair x y | x y. (x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)}" by auto  def p_def: p ≡ "λ x. c_pair x 0"  def q_def: q ≡ "λ x. c_pair x 1"  have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec  have q_is_pr: "q ∈ PrimRec1" unfolding q_def by prec  def V_def: V ≡ "{ c_pair x y | x y. (x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)}"  from V_def L3 A1 have V_ce: "V ∈ ce_sets" by auto  from V_def have L4: "∀ z. (z ∈ V) = (∃ x y. z = c_pair x y ∧  ((x ∈ A ∧ y=0) ∨ (x ∉ A ∧ y=1)))" by blast  have L5: "!! x. (p x ∈ V) = (x ∈ A)"  proof - fix x show "(p x ∈ V) = (x ∈ A)"    proof      assume A: "p x ∈ V"      then have "c_pair x 0 ∈ V" by (unfold p_def)      with V_def obtain x1 y1 where L5_2: "c_pair x 0 = c_pair x1 y1"        and L5_3: "((x1 ∈ A ∧ y1=0) ∨ (x1 ∉ A ∧ y1=1))" by auto      from L5_2 have X_eq_X1: "x=x1" by (rule c_pair_inj1)      from L5_2 have Y1_eq_0: "0=y1" by (rule c_pair_inj2)      from L5_3 X_eq_X1 Y1_eq_0 show "x ∈ A" by auto    next      assume A: "x ∈ A"      let ?z = "c_pair x 0"      from A have L5_1: "∃ x1 y1. c_pair x 0 = c_pair x1 y1 ∧  ((x1 ∈ A ∧ y1=0) ∨ (x1 ∉ A ∧ y1=1))" by auto      with V_def have "c_pair x 0 ∈ V" by auto      with p_def show "p x ∈ V" by simp    qed  qed  then have A_eq: "A = { x. p x ∈ V}" by auto  from V_ce p_is_pr have "{ x. p x ∈ V} ∈ ce_sets" by (rule ce_set_lm_5)  with A_eq have A_ce: "A ∈ ce_sets" by simp  have CA_eq: "- A = {x. q x ∈ V}"  proof -    have "!! x. (q x ∈ V) = (x ∉ A)"    proof - fix x show "(q x ∈ V) = (x ∉ A)"      proof        assume A: "q x ∈ V"        then have "c_pair x 1 ∈ V" by (unfold q_def)        with V_def obtain x1 y1 where L5_2: "c_pair x 1 = c_pair x1 y1"          and L5_3: "((x1 ∈ A ∧ y1=0) ∨ (x1 ∉ A ∧ y1=1))" by auto        from L5_2 have X_eq_X1: "x=x1" by (rule c_pair_inj1)        from L5_2 have Y1_eq_1: "1=y1" by (rule c_pair_inj2)        from L5_3 X_eq_X1 Y1_eq_1 show "x ∉ A" by auto      next        assume A: "x ∉ A"        from A have L5_1: "∃ x1 y1. c_pair x 1 = c_pair x1 y1 ∧  ((x1 ∈ A ∧ y1=0) ∨ (x1 ∉ A ∧ y1=1))" by auto        with V_def have "c_pair x 1 ∈ V" by auto        with q_def show "q x ∈ V" by simp      qed    qed    then show ?thesis by auto  qed  from V_ce q_is_pr have "{ x. q x ∈ V} ∈ ce_sets" by (rule ce_set_lm_5)  with CA_eq have CA_ce: "- A ∈ ce_sets" by simp  from A_ce CA_ce show ?thesis by (simp add: computable_def)qedtheorem post_th_0: "(computable A) = (total_recursive (chf A))"proof  assume "computable A" then show "total_recursive (chf A)" by (rule comp_impl_tot_rec)next  assume "total_recursive (chf A)" then show "computable A" by (rule tot_rec_impl_comp)qedsubsection {* Universal computably enumerable set *}definition  univ_ce :: "nat set" where  "univ_ce = { c_pair n x | n x. x ∈ nat_to_ce_set n }"lemma univ_for_pr_lm: "univ_for_pr (c_pair n x) = (nat_to_pr n) x" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)theorem univ_is_ce: "univ_ce ∈ ce_sets"proof -  def A_def: A ≡ "c_graph univ_for_pr"  then have "A ∈ ce_sets" by (simp add: univ_for_pr_tot_rec_lm)  then have "∃ pA ∈ PrimRec2. A = fn_to_set pA" by (rule ce_set_lm_3)  then obtain pA where pA_is_pr: "pA ∈ PrimRec2" and S1: "A = fn_to_set pA" by auto  from S1 have S2: "A = { x. ∃ y. pA x y = 0 }" by (simp add: fn_to_set_def)  def p_def: p ≡ "λ z y. pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y)"  from pA_is_pr have p_is_pr: "p ∈ PrimRec2" unfolding p_def by prec  have "!! z. (∃ n x. z = c_pair n x ∧ x ∈ nat_to_ce_set n) = (c_snd z ∈ nat_to_ce_set (c_fst z))"  proof -    fix z show "(∃ n x. z = c_pair n x ∧ x ∈ nat_to_ce_set n) = (c_snd z ∈ nat_to_ce_set (c_fst z))"    proof      assume A: "∃n x. z = c_pair n x ∧ x ∈ nat_to_ce_set n"      then obtain n x where L1: "z = c_pair n x ∧ x ∈ nat_to_ce_set n" by auto      from L1 have L2: "z = c_pair n x" by auto      from L1 have L3: "x ∈ nat_to_ce_set n" by auto      from L1 have L4: "c_fst z = n" by simp      from L1 have L5: "c_snd z = x" by simp      from L3 L4 L5 show "c_snd z ∈ nat_to_ce_set (c_fst z)" by auto    next      assume A: "c_snd z ∈ nat_to_ce_set (c_fst z)"      let ?n = "c_fst z"      let ?x = "c_snd z"      have L1: "z = c_pair ?n ?x" by simp      from L1 A have "z = c_pair ?n ?x ∧ ?x ∈ nat_to_ce_set ?n" by auto      thus "∃n x. z = c_pair n x ∧ x ∈ nat_to_ce_set n" by blast    qed  qed  then have "{ c_pair n x | n x. x ∈ nat_to_ce_set n } = { z. c_snd z ∈ nat_to_ce_set (c_fst z)}" by auto  then have S3: "univ_ce  = { z. c_snd z ∈ nat_to_ce_set (c_fst z)}" by (simp add: univ_ce_def)  have S4: "!! z. (c_snd z ∈ nat_to_ce_set (c_fst z)) = (∃ y. p z y = 0)"  proof -    fix z show "(c_snd z ∈ nat_to_ce_set (c_fst z)) = (∃ y. p z y = 0)"    proof      assume A: "c_snd z ∈ nat_to_ce_set (c_fst z)"      have "nat_to_ce_set (c_fst z) = { x . ∃ y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by (simp add: nat_to_ce_set_lm_1)      with A obtain u where S4_1: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) u) = 0"  by auto      then have S4_2: "univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u)) = 0" by (simp add: univ_for_pr_lm)      from A_def have S4_3: "A = { c_pair x (univ_for_pr x) | x. x ∈ UNIV }" by (simp add: c_graph_def)      then have S4_4: "!! x. c_pair x (univ_for_pr x) ∈ A" by auto      then have "c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) (univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) u))) ∈ A" by auto      with S4_2 have S4_5: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0 ∈ A" by auto      with S2 obtain v where S4_6: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) u)) 0) v = 0"         by auto      def y_def: y ≡ "c_pair u v"      from y_def have S4_7: "u = c_fst y" by simp      from y_def have S4_8: "v = c_snd y" by simp      from S4_6 S4_7 S4_8 p_def have "p z y = 0" by simp      thus "∃ y. p z y = 0" ..    next      assume A: "∃y. p z y = 0"      then obtain y where S4_1: "p z y = 0" ..      from S4_1 p_def have S4_2: "pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y) = 0" by simp      with S2 have S4_3: "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 ∈ A" by auto      with A_def have "c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0 ∈ c_graph univ_for_pr" by simp      then have S4_4: "0 = univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y)))" by (rule c_graph_lm_1)      then have S4_5: "univ_for_pr (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) = 0" by auto      then have S4_6: "(nat_to_pr (c_fst z)) (c_pair (c_snd z) (c_fst y)) = 0" by (simp add: univ_for_pr_lm)      then have S4_7: "∃ y. (nat_to_pr (c_fst z)) (c_pair (c_snd z) y) = 0" ..      have S4_8: "nat_to_ce_set (c_fst z) = { x . ∃ y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by (simp add: nat_to_ce_set_lm_1)      from S4_7 have S4_9: "c_snd z ∈ { x . ∃ y. (nat_to_pr (c_fst z)) (c_pair x y) = 0 }" by auto      with S4_8 show "c_snd z ∈ nat_to_ce_set (c_fst z)" by auto    qed  qed  with S3 have "univ_ce = {z. ∃ y. p z y = 0}" by auto  then have "univ_ce = fn_to_set p" by (simp add: fn_to_set_def)  moreover from p_is_pr have "fn_to_set p ∈ ce_sets" by (rule ce_set_lm_1)  ultimately show "univ_ce ∈ ce_sets" by autoqedlemma univ_ce_lm_1: "(c_pair n x ∈ univ_ce) = (x ∈ nat_to_ce_set n)"proof -  from univ_ce_def have S1: "univ_ce = {z . ∃ n x. z = c_pair n x ∧ x ∈ nat_to_ce_set n}" by auto  have S2: "(∃ n1 x1. c_pair n x = c_pair n1 x1 ∧ x1 ∈ nat_to_ce_set n1) = (x ∈ nat_to_ce_set n)"  proof    assume "∃n1 x1. c_pair n x = c_pair n1 x1 ∧ x1 ∈ nat_to_ce_set n1"    then obtain n1 x1 where L1: "c_pair n x = c_pair n1 x1" and L2: "x1 ∈ nat_to_ce_set n1" by auto    from L1 have L3: "n = n1" by (rule c_pair_inj1)    from L1 have L4: "x = x1" by (rule c_pair_inj2)    from L2 L3 L4 show "x ∈ nat_to_ce_set n" by auto  next    assume A: "x ∈ nat_to_ce_set n"    then have "c_pair n x = c_pair n x ∧ x ∈ nat_to_ce_set n" by auto    thus "∃ n1 x1. c_pair n x = c_pair n1 x1 ∧ x1 ∈ nat_to_ce_set n1" by blast  qed  with S1 show ?thesis by autoqedtheorem univ_ce_is_not_comp1: "- univ_ce ∉ ce_sets"proof (rule ccontr)  assume "¬ - univ_ce ∉ ce_sets"  then have A: "- univ_ce ∈ ce_sets" by auto  def p_def: p ≡ "λ x. c_pair x x"  have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec  def A_def: A ≡ "{ x. p x ∈ - univ_ce }"  from A p_is_pr have "{ x. p x ∈ - univ_ce } ∈ ce_sets" by (rule ce_set_lm_5)  with A_def have S1: "A ∈ ce_sets" by auto  then have "∃ n. A = nat_to_ce_set n" by (rule nat_to_ce_set_srj)  then obtain n where S2: "A = nat_to_ce_set n" ..  from A_def have "(n ∈ A) = (p n ∈ - univ_ce)" by auto  with p_def have "(n ∈ A) = (c_pair n n ∉ univ_ce)" by auto  with univ_ce_def univ_ce_lm_1 have "(n ∈ A) = (n ∉ nat_to_ce_set n)" by auto  with S2 have "(n ∈ A) = (n ∉ A)" by auto  thus False by autoqedtheorem univ_ce_is_not_comp2: "¬ total_recursive (chf univ_ce)"proof  assume "total_recursive (chf univ_ce)"  then have "computable univ_ce" by (rule tot_rec_impl_comp)  then have "- univ_ce ∈ ce_sets" by (unfold computable_def, auto)  with univ_ce_is_not_comp1 show False by autoqedtheorem univ_ce_is_not_comp3: "¬ computable univ_ce"proof (rule ccontr)  assume "¬ ¬ computable univ_ce"  then have "computable univ_ce" by auto  then have "total_recursive (chf univ_ce)" by (rule comp_impl_tot_rec)  with univ_ce_is_not_comp2 show False by autoqedsubsection {* s-1-1 theorem, one-one and many-one reducibilities*}definition  index_of_r_to_l :: nat where  "index_of_r_to_l =  pair_by_index    (pair_by_index index_of_c_fst (comp_by_index index_of_c_fst index_of_c_snd))    (comp_by_index index_of_c_snd index_of_c_snd)"lemma index_of_r_to_l_lm: "nat_to_pr index_of_r_to_l (c_pair x (c_pair y z)) = c_pair (c_pair x y) z"  apply(unfold index_of_r_to_l_def)  apply(simp add: pair_by_index_main)  apply(unfold c_f_pair_def)  apply(simp add: index_of_c_fst_main)  apply(simp add: comp_by_index_main)  apply(simp add: index_of_c_fst_main)  apply(simp add: index_of_c_snd_main)donedefinition  s_ce :: "nat => nat => nat" where  "s_ce == (λ e x. s1_1 (comp_by_index e index_of_r_to_l) x)"lemma s_ce_is_pr: "s_ce ∈ PrimRec2"  unfolding s_ce_def using comp_by_index_is_pr s1_1_is_pr by preclemma s_ce_inj: "s_ce e1 x1 = s_ce e2 x2 ==> e1=e2 ∧ x1=x2"proof -  let ?n1 = "index_of_r_to_l"  assume "s_ce e1 x1 = s_ce e2 x2"  then have "s1_1 (comp_by_index e1 ?n1) x1 = s1_1 (comp_by_index e2 ?n1) x2" by (unfold s_ce_def)  then have L1: "comp_by_index e1 ?n1 = comp_by_index e2 ?n1 ∧ x1=x2" by (rule s1_1_inj)  from L1 have "comp_by_index e1 ?n1 = comp_by_index e2 ?n1" ..  then have "e1=e2" by (rule comp_by_index_inj1)  moreover from L1 have "x1=x2" by auto  ultimately show ?thesis by autoqedlemma s_ce_inj1: "s_ce e1 x = s_ce e2 x ==> e1=e2"proof -  assume "s_ce e1 x = s_ce e2 x"  then have "e1=e2 ∧ x=x" by (rule s_ce_inj)  then show "e1=e2" by autoqedlemma s_ce_inj2: "s_ce e x1 = s_ce e x2 ==> x1=x2"proof -  assume "s_ce e x1 = s_ce e x2"  then have "e=e ∧ x1=x2" by (rule s_ce_inj)  then show "x1=x2" by autoqedtheorem s1_1_th1: "∀ n x y. ((nat_to_pr n) (c_pair x y)) = (nat_to_pr (s1_1 n x)) y"proof (rule allI, rule allI, rule allI)  fix n x y show "nat_to_pr n (c_pair x y) = nat_to_pr (s1_1 n x) y"  proof -    have "(λ y. (nat_to_pr n) (c_pair x y)) = nat_to_pr (s1_1 n x)" by (rule s1_1_th)    then show ?thesis by (simp add: fun_eq_iff)  qedqedlemma s_lm: "(nat_to_pr (s_ce e x)) (c_pair y z) = (nat_to_pr e) (c_pair (c_pair x y) z)"proof -  let ?n1 = "index_of_r_to_l"  have "(nat_to_pr (s_ce e x)) (c_pair y z) = nat_to_pr (s1_1 (comp_by_index e ?n1) x) (c_pair y z)" by (unfold s_ce_def, simp)  also have "… = (nat_to_pr (comp_by_index e ?n1)) (c_pair x (c_pair y z))" by (simp add: s1_1_th1)  also have "… = (nat_to_pr e) ((nat_to_pr ?n1) (c_pair x (c_pair y z)))" by (simp add: comp_by_index_main)  finally show ?thesis by (simp add: index_of_r_to_l_lm)qedtheorem s_ce_1_1_th: "(c_pair x y ∈ nat_to_ce_set e) = (y ∈ nat_to_ce_set (s_ce e x))"proof  assume A: "c_pair x y ∈ nat_to_ce_set e"  then obtain z where L1: "(nat_to_pr e) (c_pair (c_pair x y) z) = 0"     by (auto simp add: nat_to_ce_set_lm_1)  have "(nat_to_pr (s_ce e x)) (c_pair y z) = 0" by (simp add: s_lm L1)  with nat_to_ce_set_lm_1 show "y ∈ nat_to_ce_set (s_ce e x)" by autonext  assume A: "y ∈ nat_to_ce_set (s_ce e x)"  then obtain z where L1: "(nat_to_pr (s_ce e x)) (c_pair y z) = 0"     by (auto simp add: nat_to_ce_set_lm_1)  then have "(nat_to_pr e) (c_pair (c_pair x y) z) = 0" by (simp add: s_lm)  with nat_to_ce_set_lm_1 show "c_pair x y ∈ nat_to_ce_set e" by autoqeddefinition  one_reducible_to_via :: "(nat set) => (nat set) => (nat => nat) => bool" where  "one_reducible_to_via = (λ A B f. total_recursive f ∧ inj f ∧ (∀ x. (x ∈ A) = (f x ∈ B)))"definition  one_reducible_to :: "(nat set) => (nat set) => bool" where  "one_reducible_to = (λ A B. ∃ f. one_reducible_to_via A B f)"definition  many_reducible_to_via :: "(nat set) => (nat set) => (nat => nat) => bool" where  "many_reducible_to_via = (λ A B f. total_recursive f ∧ (∀ x. (x ∈ A) = (f x ∈ B)))"definition  many_reducible_to :: "(nat set) => (nat set) => bool" where  "many_reducible_to = (λ A B. ∃ f. many_reducible_to_via A B f)"lemma one_reducible_to_via_trans: "[| one_reducible_to_via A B f; one_reducible_to_via B C g |] ==> one_reducible_to_via A C (g o f)"proof -  assume A1: "one_reducible_to_via A B f"  assume A2: "one_reducible_to_via B C g"  from A1 have f_tr: "total_recursive f" by (unfold one_reducible_to_via_def, auto)  from A1 have f_inj: "inj f" by (unfold one_reducible_to_via_def, auto)  from A1 have L1: "∀ x. (x ∈ A) = (f x ∈ B)" by (unfold one_reducible_to_via_def, auto)  from A2 have g_tr: "total_recursive g" by (unfold one_reducible_to_via_def, auto)  from A2 have g_inj: "inj g" by (unfold one_reducible_to_via_def, auto)  from A2 have L2: "∀ x. (x ∈ B) = (g x ∈ C)" by (unfold one_reducible_to_via_def, auto)  from g_tr f_tr have fg_tr: "total_recursive (g o f)" by (rule comp_tot_rec)  from g_inj f_inj have fg_inj: "inj (g o f)" by (rule inj_comp)  from L1 L2 have L3: "(∀ x. (x ∈ A) = ((g o f) x ∈ C))" by auto  with fg_tr fg_inj show ?thesis by (unfold one_reducible_to_via_def, auto)qedlemma one_reducible_to_trans: "[| one_reducible_to A B; one_reducible_to B C |] ==> one_reducible_to A C"proof -  assume "one_reducible_to A B"  then obtain f where A1: "one_reducible_to_via A B f" unfolding one_reducible_to_def by auto  assume "one_reducible_to B C"  then obtain g where A2: "one_reducible_to_via B C g" unfolding one_reducible_to_def by auto  from A1 A2 have "one_reducible_to_via A C (g o f)" by (rule one_reducible_to_via_trans)  then show ?thesis unfolding one_reducible_to_def by autoqedlemma one_reducible_to_via_refl: "one_reducible_to_via A A (λ x. x)"proof -  have is_pr: "(λ x. x) ∈ PrimRec1" by (rule pr_id1_1)  then have is_tr: "total_recursive (λ x. x)" by (rule pr_is_total_rec)  have is_inj: "inj (λ x. x)" by simp  have L1: "∀ x. (x ∈ A) = (((λ x. x) x) ∈ A)" by simp  with is_tr is_inj show ?thesis by (unfold one_reducible_to_via_def, auto)qedlemma one_reducible_to_refl: "one_reducible_to A A"proof -  have "one_reducible_to_via A A (λ x. x)" by (rule one_reducible_to_via_refl)  then show ?thesis by (unfold one_reducible_to_def, auto)qedlemma many_reducible_to_via_trans: "[| many_reducible_to_via A B f; many_reducible_to_via B C g |] ==> many_reducible_to_via A C (g o f)"proof -  assume A1: "many_reducible_to_via A B f"  assume A2: "many_reducible_to_via B C g"  from A1 have f_tr: "total_recursive f" by (unfold many_reducible_to_via_def, auto)  from A1 have L1: "∀ x. (x ∈ A) = (f x ∈ B)" by (unfold many_reducible_to_via_def, auto)  from A2 have g_tr: "total_recursive g" by (unfold many_reducible_to_via_def, auto)  from A2 have L2: "∀ x. (x ∈ B) = (g x ∈ C)" by (unfold many_reducible_to_via_def, auto)  from g_tr f_tr have fg_tr: "total_recursive (g o f)" by (rule comp_tot_rec)  from L1 L2 have L3: "(∀ x. (x ∈ A) = ((g o f) x ∈ C))" by auto  with fg_tr show ?thesis by (unfold many_reducible_to_via_def, auto)qedlemma many_reducible_to_trans: "[| many_reducible_to A B; many_reducible_to B C |] ==> many_reducible_to A C"proof -  assume "many_reducible_to A B"  then obtain f where A1: "many_reducible_to_via A B f"    unfolding many_reducible_to_def by auto  assume "many_reducible_to B C"  then obtain g where A2: "many_reducible_to_via B C g"    unfolding many_reducible_to_def by auto  from A1 A2 have "many_reducible_to_via A C (g o f)" by (rule many_reducible_to_via_trans)  then show ?thesis unfolding many_reducible_to_def by autoqedlemma one_reducibility_via_is_many: "one_reducible_to_via A B f ==> many_reducible_to_via A B f"proof -  assume A: "one_reducible_to_via A B f"  from A have f_tr: "total_recursive f" by (unfold one_reducible_to_via_def, auto)  from A have "∀ x. (x ∈ A) = (f x ∈ B)" by (unfold one_reducible_to_via_def, auto)  with f_tr show ?thesis by (unfold many_reducible_to_via_def, auto)qedlemma one_reducibility_is_many: "one_reducible_to A B ==> many_reducible_to A B"proof -  assume "one_reducible_to A B"  then obtain f where A: "one_reducible_to_via A B f"     unfolding one_reducible_to_def by auto  then have "many_reducible_to_via A B f" by (rule one_reducibility_via_is_many)  then show ?thesis unfolding many_reducible_to_def by autoqedlemma many_reducible_to_via_refl: "many_reducible_to_via A A (λ x. x)"proof -  have "one_reducible_to_via A A (λ x. x)" by (rule one_reducible_to_via_refl)  then show ?thesis by (rule one_reducibility_via_is_many)qedlemma many_reducible_to_refl: "many_reducible_to A A"proof -  have "one_reducible_to A A" by (rule one_reducible_to_refl)  then show ?thesis by (rule one_reducibility_is_many)qedtheorem m_red_to_comp: "[| many_reducible_to A B; computable B |] ==> computable A"proof -  assume "many_reducible_to A B"  then obtain f where A1: "many_reducible_to_via A B f"     unfolding many_reducible_to_def by auto  from A1 have f_tr: "total_recursive f" by (unfold many_reducible_to_via_def, auto)  from A1 have L1: "∀ x. (x ∈ A) = (f x ∈ B)" by (unfold many_reducible_to_via_def, auto)  assume "computable B"  then have L2: "total_recursive (chf B)" by (rule comp_impl_tot_rec)  have L3: "chf A = (chf B) o f"  proof fix x    have "chf A x = (chf B) (f x)"    proof cases      assume A: "x ∈ A"      then have L3_1: "chf A x = 0" by (simp add: chf_lm_2)      from A L1 have "f x ∈ B" by auto      then have L3_2: "(chf B) (f x) = 0" by (simp add: chf_lm_2)      from L3_1 L3_2 show "chf A x = (chf B) (f x)" by auto    next      assume A: "x ∉ A"      then have L3_1: "chf A x = 1" by (simp add: chf_lm_3)      from A L1 have "f x ∉ B" by auto      then have L3_2: "(chf B) (f x) = 1" by (simp add: chf_lm_3)      from L3_1 L3_2 show "chf A x = (chf B) (f x)" by auto    qed    then show "chf A x = (chf B o f) x" by auto  qed  from L2 f_tr have "total_recursive (chf B o f)" by (rule comp_tot_rec)  with L3 have "total_recursive (chf A)" by auto  then show ?thesis by (rule tot_rec_impl_comp)qedlemma many_reducible_lm_1: "many_reducible_to univ_ce A ==> ¬ computable A"proof (rule ccontr)  assume A1: "many_reducible_to univ_ce A"  assume "¬ ¬ computable A"  then have A2: "computable A" by auto  from A1 A2 have "computable univ_ce" by (rule m_red_to_comp)  with univ_ce_is_not_comp3 show False by autoqedlemma one_reducible_lm_1: "one_reducible_to univ_ce A ==> ¬ computable A"proof -  assume "one_reducible_to univ_ce A"  then have "many_reducible_to univ_ce A" by (rule one_reducibility_is_many)  then show ?thesis by (rule many_reducible_lm_1)qedlemma one_reducible_lm_2: "one_reducible_to_via (nat_to_ce_set n) univ_ce (λ x. c_pair n x)"proof -  def f_def: f ≡ "λ x. c_pair n x"  have f_is_pr: "f ∈ PrimRec1" unfolding f_def by prec  then have f_tr: "total_recursive f" by (rule pr_is_total_rec)  have f_inj: "inj f"  proof (rule injI)    fix x y assume A: "f x = f y"    then have "c_pair n x = c_pair n y" by (unfold f_def)    then show "x = y" by (rule c_pair_inj2)  qed  have "∀ x. (x ∈ (nat_to_ce_set n)) = (f x ∈ univ_ce)"  proof fix x show "(x ∈ nat_to_ce_set n) = (f x ∈ univ_ce)" by (unfold f_def, simp add: univ_ce_lm_1)  qed  with f_tr f_inj show ?thesis by (unfold f_def, unfold one_reducible_to_via_def, auto)qedlemma one_reducible_lm_3: "one_reducible_to (nat_to_ce_set n) univ_ce"proof -  have "one_reducible_to_via (nat_to_ce_set n) univ_ce (λ x. c_pair n x)" by (rule one_reducible_lm_2)  then show ?thesis by (unfold one_reducible_to_def, auto)qedlemma one_reducible_lm_4: "A ∈ ce_sets ==> one_reducible_to A univ_ce"proof -  assume "A ∈ ce_sets"  then have "∃ n. A = nat_to_ce_set n" by (rule nat_to_ce_set_srj)  then obtain n where "A = nat_to_ce_set n" by auto  with one_reducible_lm_3 show ?thesis by autoqedsubsection {* One-complete sets *}definition  one_complete :: "nat set => bool" where  "one_complete = (λ A. A ∈ ce_sets ∧ (∀ B. B ∈ ce_sets --> one_reducible_to B A))"theorem univ_is_complete: "one_complete univ_ce"proof (unfold one_complete_def)  show "univ_ce ∈ ce_sets ∧ (∀B. B ∈ ce_sets --> one_reducible_to B univ_ce)"  proof    show "univ_ce ∈ ce_sets" by (rule univ_is_ce)  next    show "∀B. B ∈ ce_sets --> one_reducible_to B univ_ce"    proof (rule allI, rule impI)      fix B assume "B ∈ ce_sets" then show "one_reducible_to B univ_ce" by (rule one_reducible_lm_4)    qed  qedqedsubsection {* Index sets, Rice's theorem *}definition  index_set :: "nat set => bool" where  "index_set = (λ A. ∀ n m. n ∈ A ∧ (nat_to_ce_set n = nat_to_ce_set m) --> m ∈ A)"lemma index_set_lm_1: "[| index_set A; n∈ A; nat_to_ce_set n = nat_to_ce_set m |] ==> m ∈ A"proof -  assume A1: "index_set A"  assume A2: "n ∈ A"  assume A3: "nat_to_ce_set n = nat_to_ce_set m"  from A2 A3 have L1: "n ∈ A ∧ (nat_to_ce_set n = nat_to_ce_set m)" by auto  from A1 have L2: "∀ n m. n ∈ A ∧ (nat_to_ce_set n = nat_to_ce_set m) --> m ∈ A" by (unfold index_set_def)  from L1 L2 show ?thesis by autoqedlemma index_set_lm_2: "index_set A ==> index_set (-A)"proof -  assume A: "index_set A"  show "index_set (-A)"  proof (unfold index_set_def)    show "∀n m. n ∈ - A ∧ nat_to_ce_set n = nat_to_ce_set m --> m ∈ - A"    proof (rule allI, rule allI, rule impI)      fix n m assume A1: "n ∈ - A ∧ nat_to_ce_set n = nat_to_ce_set m"      from A1 have A2: "n ∈ -A" by auto      from A1 have A3: "nat_to_ce_set m = nat_to_ce_set n" by auto      show "m ∈ - A"      proof        assume "m ∈ A"        from A this A3 have "n ∈ A" by (rule index_set_lm_1)        with A2 show False by auto      qed    qed  qedqedlemma Rice_lm_1: "[| index_set A; A ≠ {}; A ≠ UNIV; ∃ n ∈ A. nat_to_ce_set n = {} |] ==> one_reducible_to univ_ce (- A)"proof -  assume A1: "index_set A"  assume A2: "A ≠ {}"  assume A3: "A ≠ UNIV"  assume "∃ n ∈ A. nat_to_ce_set n = {}"  then obtain e_0 where e_0_in_A: "e_0 ∈ A" and e_0_empty: "nat_to_ce_set e_0 = {}" by auto  from e_0_in_A A3 obtain e_1 where e_1_not_in_A: "e_1 ∈ (- A)" by auto  with e_0_in_A have e_0_neq_e_1: "e_0 ≠ e_1" by auto  have "nat_to_ce_set e_0 ≠ nat_to_ce_set e_1"  proof    assume "nat_to_ce_set e_0 = nat_to_ce_set e_1"    with A1 e_0_in_A have "e_1 ∈ A" by (rule index_set_lm_1)    with e_1_not_in_A show False by auto  qed  with e_0_empty have e1_not_empty: "nat_to_ce_set e_1 ≠ {}" by auto  def we_1_def: we_1 ≡ "nat_to_ce_set e_1"  from e1_not_empty have we_1_not_empty: "we_1 ≠ {}" by (unfold we_1_def)  def r_def: r ≡ "univ_ce × we_1"  have loc_lm_1: "!! x. x ∈ univ_ce ==> ∀ y. (y ∈ we_1) = ((x,y) ∈ r)" by (unfold r_def, auto)  have loc_lm_2: "!! x. x ∉ univ_ce ==> ∀ y. (y ∈ {}) = ((x,y) ∈ r)" by (unfold r_def, auto)  have r_ce: "r ∈ ce_rels"  proof (unfold r_def, rule ce_rel_lm_29)    show "univ_ce ∈ ce_sets" by (rule univ_is_ce)  next    show "we_1 ∈ ce_sets" by (unfold we_1_def, rule nat_to_ce_set_into_ce)  qed  def we_n_def: we_n ≡ "ce_rel_to_set r"  from r_ce have we_n_ce: "we_n ∈ ce_sets" by (unfold we_n_def, rule ce_rel_lm_6)  then have "∃ n. we_n = nat_to_ce_set n" by (rule nat_to_ce_set_srj)  then obtain n where we_n_df1: "we_n = nat_to_ce_set n" by auto  def f_def: f ≡ "λ x. s_ce n x"  from s_ce_is_pr have f_is_pr: "f ∈ PrimRec1" unfolding f_def by prec  then have f_tr: "total_recursive f" by (rule pr_is_total_rec)  have f_inj: "inj f"  proof (rule injI)    fix x y    assume "f x = f y"    then have "s_ce n x = s_ce n y" by (unfold f_def)    then show "x = y" by (rule s_ce_inj2)  qed  have loc_lm_3: "∀ x y. (c_pair x y ∈ we_n) = (y ∈ nat_to_ce_set (f x))"  proof (rule allI, rule allI)    fix x y show "(c_pair x y ∈ we_n) = (y ∈ nat_to_ce_set (f x))" by (unfold f_def, unfold we_n_df1, simp add: s_ce_1_1_th)  qed  from A1 have loc_lm_4: "index_set (- A)" by (rule index_set_lm_2)  have loc_lm_5: "∀ x. (x ∈ univ_ce) = (f x ∈ -A)"  proof fix x show "(x ∈ univ_ce) = (f x ∈ -A)"    proof      assume A: "x ∈ univ_ce"      then have S1: "∀ y. (y ∈ we_1) = ((x,y) ∈ r)" by (rule loc_lm_1)      from ce_rel_lm_12 have "∀ y. (c_pair x y ∈ ce_rel_to_set r) = ((x,y) ∈ r)" by auto      then have "∀ y. ((x,y) ∈ r) = (c_pair x y ∈ we_n)" by (unfold we_n_def, auto)      with S1 have "∀ y. (y ∈ we_1) = (c_pair x y ∈ we_n)" by auto      with loc_lm_3 have "∀ y. (y ∈ we_1) = (y ∈ nat_to_ce_set (f x))" by auto      then have S2: "we_1 = nat_to_ce_set (f x)" by auto      then have "nat_to_ce_set e_1 = nat_to_ce_set (f x)" by (unfold we_1_def)      with loc_lm_4 e_1_not_in_A show "f x ∈ -A" by (rule index_set_lm_1)    next      show " f x ∈ - A ==> x ∈ univ_ce"      proof (rule ccontr)        assume fx_in_A: "f x ∈ - A"        assume x_not_in_univ: "x ∉ univ_ce"        then have S1: "∀ y. (y ∈ {}) = ((x,y) ∈ r)" by (rule loc_lm_2)        from ce_rel_lm_12 have "∀ y. (c_pair x y ∈ ce_rel_to_set r) = ((x,y) ∈ r)" by auto        then have "∀ y. ((x,y) ∈ r) = (c_pair x y ∈ we_n)" by (unfold we_n_def, auto)        with S1 have "∀ y. (y ∈ {}) = (c_pair x y ∈ we_n)" by auto        with loc_lm_3 have "∀ y. (y ∈ {}) = (y ∈ nat_to_ce_set (f x))" by auto        then have S2: "{} = nat_to_ce_set (f x)" by auto        then have "nat_to_ce_set e_0 = nat_to_ce_set (f x)" by (unfold e_0_empty)        with A1 e_0_in_A have "f x ∈ A" by (rule index_set_lm_1)        with fx_in_A show False by auto      qed    qed  qed  with f_tr f_inj have "one_reducible_to_via univ_ce (-A) f" by (unfold one_reducible_to_via_def, auto)  then show ?thesis by (unfold one_reducible_to_def, auto)qedlemma Rice_lm_2: "[| index_set A; A ≠ {}; A ≠ UNIV; n ∈ A;  nat_to_ce_set n = {} |] ==> one_reducible_to univ_ce (- A)"proof -  assume A1: "index_set A"  assume A2: "A ≠ {}"  assume A3: "A ≠ UNIV"  assume A4: "n ∈ A"  assume A5: "nat_to_ce_set n = {}"  from A4 A5 have S1: "∃ n ∈ A. nat_to_ce_set n = {}" by auto  from A1 A2 A3 S1 show ?thesis by (rule Rice_lm_1)qedtheorem Rice_1: "[| index_set A; A ≠ {}; A ≠ UNIV |] ==> one_reducible_to univ_ce A ∨ one_reducible_to univ_ce (- A)"proof -  assume A1: "index_set A"  assume A2: "A ≠ {}"  assume A3: "A ≠ UNIV"  from ce_empty have "∃ n. {} = nat_to_ce_set n" by (rule nat_to_ce_set_srj)  then obtain n where n_empty: "nat_to_ce_set n = {}" by auto  show ?thesis  proof cases    assume A: "n ∈ A"    from A1 A2 A3 A n_empty have "one_reducible_to univ_ce (- A)" by (rule Rice_lm_2)    then show ?thesis by auto  next    assume "n ∉ A" then have A: "n ∈ - A" by auto    from A1 have S1: "index_set (- A)" by (rule index_set_lm_2)    from A3 have S2: "- A ≠ {}" by auto    from A2 have S3: "- A ≠ UNIV" by auto    from S1 S2 S3 A n_empty have "one_reducible_to univ_ce (- (- A))" by (rule Rice_lm_2)    then have "one_reducible_to univ_ce A" by simp    then show ?thesis by auto  qedqedtheorem Rice_2: "[| index_set A; A ≠ {}; A ≠ UNIV |] ==> ¬ computable A"proof -  assume A1: "index_set A"  assume A2: "A ≠ {}"  assume A3: "A ≠ UNIV"  from A1 A2 A3 have "one_reducible_to univ_ce A ∨ one_reducible_to univ_ce (- A)" by (rule Rice_1)  then have S1: "¬ one_reducible_to univ_ce A --> one_reducible_to univ_ce (- A)" by auto  show ?thesis  proof cases    assume "one_reducible_to univ_ce A"    then show "¬ computable A" by (rule one_reducible_lm_1)  next    assume "¬ one_reducible_to univ_ce A"    with S1 have "one_reducible_to univ_ce (- A)" by auto    then have "¬ computable (- A)" by (rule one_reducible_lm_1)    with computable_complement_3 show "¬ computable A" by auto  qedqedtheorem Rice_3: "[| C ⊆ ce_sets; computable { n. nat_to_ce_set n ∈ C} |] ==> C = {} ∨ C = ce_sets"proof (rule ccontr)  assume A1: "C ⊆ ce_sets"  assume A2: "computable { n. nat_to_ce_set n ∈ C}"  assume A3: "¬ (C = {} ∨ C = ce_sets)"  from A3 have A4: "C ≠ {}" by auto  from A3 have A5: "C ≠ ce_sets" by auto  def A_def: A ≡ "{ n. nat_to_ce_set n ∈ C}"  have S1: "index_set A"  proof (unfold index_set_def)    show "∀n m. n ∈ A ∧ nat_to_ce_set n = nat_to_ce_set m --> m ∈ A"    proof (rule allI, rule allI, rule impI)      fix n m assume A1_1: "n ∈ A ∧ nat_to_ce_set n = nat_to_ce_set m"      from A1_1 have "n ∈ A" by auto      then have S1_1: "nat_to_ce_set n ∈ C" by (unfold A_def, auto)      from A1_1 have "nat_to_ce_set n = nat_to_ce_set m" by auto      with S1_1 have "nat_to_ce_set m ∈ C" by auto      then show "m ∈ A" by (unfold A_def, auto)    qed  qed  have S2: "A ≠ {}"  proof -    from A4 obtain B where S2_1: "B ∈ C" by auto    with A1 have "B ∈ ce_sets" by auto    then have "∃ n. B = nat_to_ce_set n" by (rule nat_to_ce_set_srj)    then obtain n where "B = nat_to_ce_set n" ..    with S2_1 have "nat_to_ce_set n ∈ C" by auto    then show ?thesis by (unfold A_def, auto)  qed  have S3: "A ≠ UNIV"  proof -    from A1 A5 obtain B where S2_1: "B ∉ C" and S2_2: "B ∈ ce_sets" by auto    from S2_2 have "∃ n. B = nat_to_ce_set n" by (rule nat_to_ce_set_srj)    then obtain n where "B = nat_to_ce_set n" ..    with S2_1 have "nat_to_ce_set n ∉ C" by auto    then show ?thesis by (unfold A_def, auto)  qed  from S1 S2 S3 have "¬ computable A" by (rule Rice_2)  with A2 show False unfolding A_def by autoqedend`