Theory RecEnSet
section ‹Computably enumerable sets of natural numbers›
theory RecEnSet
imports PRecList PRecFun2 PRecFinSet PRecUnGr
begin
subsection ‹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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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)
define q where "q x y = pA (p x) y" for 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 auto
qed
lemma 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
define q where "q z = (if pA (c_fst z) (c_snd z) = 0 then c_fst z else a)" for z
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 blast
qed
lemma 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)
define q where "q y t = (if y = p (c_snd t) then pA (c_snd t) (c_fst t) else 1)" for y t
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
define t where "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 auto
qed
theorem 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)
qed
theorem 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)
qed
theorem 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)
qed
theorem 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 simp
qed
theorem 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 simp
qed
subsection ‹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 auto
qed
lemma 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)
qed
lemma 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" ..
define q where "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 ..
qed
subsection ‹Characteristic functions›
definition
chf :: "nat set ⇒ (nat ⇒ nat)" 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"
define p where "p = chf A"
from A p_def have p_is_pr: "p ∈ PrimRec1" by auto
define q where "q x y = p x" for x y :: nat
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 auto
qed
lemma chf_lm_5: "finite A ⟹ chf A ∈ PrimRec1"
proof -
assume A: "finite A"
define u where "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 auto
qed
theorem 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)
qed
subsection ‹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
qed
next
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"
define x where "x = fst z"
define y where "y = snd z"
from x_def y_def have L1: "z = (x,y)" by simp
define u where "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
qed
qed
lemma 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
qed
next
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)
define x where "x = c_fst z"
define y where "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
qed
qed
lemma 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)
define A where "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
qed
next
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
qed
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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 simp
qed
lemma 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)
qed
lemma 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 simp
qed
lemma 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)
qed
lemma 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)
qed
lemma 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 simp
qed
lemma 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 simp
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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"
define A where "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)
define p where "p x y u = q (c_pair x y) u" for 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"
define z where "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"
define z where "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 auto
qed
lemma 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 blast
qed
lemma 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)"
define q where "q z u = p (c_fst z) (c_snd z) u" for z u
from p_is_pr have q_is_pr: "q ∈ PrimRec2" unfolding q_def by prec
define A where "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 -
define x where "x = c_fst z"
define y where "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 -
define x where "x = c_fst z"
define y where "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)
qed
lemma 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
define p where "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)))"
for x z u
from p_r_is_pr p_s_is_pr have p_is_pr: "p ∈ PrimRec3" unfolding p_def by prec
define sr where "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
define u where "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)
qed
lemma 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
define q where "q x y u = p y x u" for x y 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)
qed
lemma 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
define A where "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
define z where "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 auto
qed
lemma 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])
qed
lemma 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)
qed
lemma 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"
define r_a where "r_a = {(x,(0::nat)) | x. x ∈ A}"
define r_b where "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)
define p where "p x = c_pair x 0" for x
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"
unfolding p_def by (simp add: 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)
define p where "p z = c_pair 0 z" for 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"
unfolding p_def by (simp add: 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 auto
qed
lemma 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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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)
qed
qed
lemma 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)
qed
lemma 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 -
define f where "f x = (c_fst x, c_snd x)" for x
have f_inj: "inj f"
proof (unfold f_def, rule inj_on_inverseI [where ?g="λ (u,v). c_pair u v"])
fix x :: nat
assume "x ∈ UNIV"
show "case_prod 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)
qed
lemma 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 auto
qed
subsection ‹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 auto
qed
lemma 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)
qed
lemma 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)
qed
qed
theorem pr_is_total_rec: "f ∈ PrimRec1 ⟹ total_recursive f"
proof -
assume A: "f ∈ PrimRec1"
define p where "p x = c_pair x (f x)" for 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)
qed
theorem 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)
qed
lemma univ_for_pr_tot_rec_lm: "c_graph univ_for_pr ∈ ce_sets"
proof -
define A where "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
define p where "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)" for x y
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 auto
qed
theorem 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)
qed
subsection ‹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)
qed
lemma computable_complement_2: "computable (- A) ⟹ computable A"
proof -
assume "computable (- A)"
then show ?thesis by (unfold computable_def, auto)
qed
lemma 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)
define p where "p x = c_pair x 0" for x
define q where "q x = c_pair x 1" for x
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
define U0 where "U0 = {p x | x. x ∈ A}"
define U1 where "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)
define U where "U = U0 ∪ U1"
from U0_ce U1_ce have U_ce: "U ∈ ce_sets" by (unfold U_def, rule ce_union)
define V where "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)
qed
theorem 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
define p where "p x = c_pair x 0" for x
define q where "q x = c_pair x 1" for x
have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec
have q_is_pr: "q ∈ PrimRec1" unfolding q_def by prec
define V where "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)
qed
theorem 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)
qed
subsection ‹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 -
define A where "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)
define p where "p z y = pA (c_pair (c_pair (c_fst z) (c_pair (c_snd z) (c_fst y))) 0) (c_snd y)"
for z 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
define y where "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 auto
qed
lemma 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 auto
qed
theorem 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
define p where "p x = c_pair x x" for x
have p_is_pr: "p ∈ PrimRec1" unfolding p_def by prec
define A where "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 auto
qed
theorem 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 auto
qed
theorem 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 auto
qed
subsection ‹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)
done
definition
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 prec
lemma 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 auto
qed
lemma 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 auto
qed
lemma 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 auto
qed
theorem 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)
qed
qed
lemma 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)
qed
theorem 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 auto
next
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 auto
qed
definition
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_compose)
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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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)
qed
lemma 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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma 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)
qed
theorem 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 ∘ f) x" by auto
qed
from L2 f_tr have "total_recursive (chf B ∘ f)" by (rule comp_tot_rec)
with L3 have "total_recursive (chf A)" by auto
then show ?thesis by (rule tot_rec_impl_comp)
qed
lemma 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 auto
qed
lemma 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)
qed
lemma one_reducible_lm_2: "one_reducible_to_via (nat_to_ce_set n) univ_ce (λ x. c_pair n x)"
proof -
define f where "f x = c_pair n x" for 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)
qed
lemma 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)
qed
lemma 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 auto
qed
subsection ‹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
qed
qed
subsection ‹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 auto
qed
lemma 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
qed
qed
lemma 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
define we_1 where "we_1 = nat_to_ce_set e_1"
from e1_not_empty have we_1_not_empty: "we_1 ≠ {}" by (unfold we_1_def)
define r where "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)
show "we_1 ∈ ce_sets" by (unfold we_1_def, rule nat_to_ce_set_into_ce)
qed
define we_n where "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
define f where "f x = s_ce n x" for 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)
qed
lemma 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)
qed
theorem 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
qed
qed
theorem 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
qed
qed
theorem 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
define A where "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 auto
qed
end