Theory Recursion-Theory-I.PRecUnGr
section ‹The function which is universal for primitive recursive functions of one variable›
theory PRecUnGr
imports PRecFun2 PRecList
begin
text ‹
We introduce a particular function which is universal for primitive
recursive functions of one variable.
›
definition
g_comp :: "nat ⇒ nat ⇒ nat" where
"g_comp c_ls key = (
let n = c_fst key; x = c_snd key; m = c_snd n;
m1 = c_fst m; m2 = c_snd m in
if c_assoc_have_key c_ls (c_pair m2 x) = 0 then
(let y = c_assoc_value c_ls (c_pair m2 x) in
if c_assoc_have_key c_ls (c_pair m1 y) = 0 then
(let z = c_assoc_value c_ls (c_pair m1 y) in
c_cons (c_pair key z) c_ls)
else c_ls
)
else c_ls
)"
definition
g_pair :: "nat ⇒ nat ⇒ nat" where
"g_pair c_ls key = (
let n = c_fst key; x = c_snd key; m = c_snd n;
m1 = c_fst m; m2 = c_snd m in
if c_assoc_have_key c_ls (c_pair m1 x) = 0 then
(let y1 = c_assoc_value c_ls (c_pair m1 x) in
if c_assoc_have_key c_ls (c_pair m2 x) = 0 then
(let y2 = c_assoc_value c_ls (c_pair m2 x) in
c_cons (c_pair key (c_pair y1 y2)) c_ls)
else c_ls
)
else c_ls
)"
definition
g_rec :: "nat ⇒ nat ⇒ nat" where
"g_rec c_ls key = (
let n = c_fst key; x = c_snd key; m = c_snd n;
m1 = c_fst m; m2 = c_snd m; y1 = c_fst x; x1 = c_snd x in
if y1 = 0 then
(
if c_assoc_have_key c_ls (c_pair m1 x1) = 0 then
c_cons (c_pair key (c_assoc_value c_ls (c_pair m1 x1))) c_ls
else c_ls
)
else
(
let y2 = y1-(1::nat) in
if c_assoc_have_key c_ls (c_pair n (c_pair y2 x1)) = 0 then
(
let t1 = c_assoc_value c_ls (c_pair n (c_pair y2 x1)); t2 = c_pair (c_pair y2 t1) x1 in
if c_assoc_have_key c_ls (c_pair m2 t2) = 0 then
c_cons (c_pair key (c_assoc_value c_ls (c_pair m2 t2))) c_ls
else c_ls
)
else c_ls
)
)"
definition
g_step :: "nat ⇒ nat ⇒ nat" where
"g_step c_ls key = (
let n = c_fst key; x = c_snd key; n1 = (c_fst n) mod 7 in
if n1 = 0 then c_cons (c_pair key 0) c_ls else
if n1 = 1 then c_cons (c_pair key (Suc x)) c_ls else
if n1 = 2 then c_cons (c_pair key (c_fst x)) c_ls else
if n1 = 3 then c_cons (c_pair key (c_snd x)) c_ls else
if n1 = 4 then g_comp c_ls key else
if n1 = 5 then g_pair c_ls key else
if n1 = 6 then g_rec c_ls key else
c_ls
)"
definition
pr_gr :: "nat ⇒ nat" where
pr_gr_def: "pr_gr = PrimRecOp1 0 (λ a b. g_step b (c_fst a))"
lemma pr_gr_at_0: "pr_gr 0 = 0" by (simp add: pr_gr_def)
lemma pr_gr_at_Suc: "pr_gr (Suc x) = g_step (pr_gr x) (c_fst x)" by (simp add: pr_gr_def)
definition
univ_for_pr :: "nat ⇒ nat" where
"univ_for_pr = pr_conv_2_to_1 nat_to_pr"
theorem univ_is_not_pr: "univ_for_pr ∉ PrimRec1"
proof (rule ccontr)
assume "¬ univ_for_pr ∉ PrimRec1" then have A1: "univ_for_pr ∈ PrimRec1" by simp
let ?f = "λ n. univ_for_pr (c_pair n n) + 1"
let ?n0 = "index_of_pr ?f"
from A1 have S1: "?f ∈ PrimRec1" by prec
then have S2: "nat_to_pr ?n0 = ?f" by (rule index_of_pr_is_real)
then have S3: "nat_to_pr ?n0 ?n0 = ?f ?n0" by simp
have S4: "?f ?n0 = univ_for_pr (c_pair ?n0 ?n0) + 1" by simp
from S3 S4 show False by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
qed
definition
c_is_sub_fun :: "nat ⇒ (nat ⇒ nat) ⇒ bool" where
"c_is_sub_fun ls f ⟷ (∀ x. c_assoc_have_key ls x = 0 ⟶ c_assoc_value ls x = f x)"
lemma c_is_sub_fun_lm_1: "⟦ c_is_sub_fun ls f; c_assoc_have_key ls x = 0 ⟧ ⟹ c_assoc_value ls x = f x"
apply(unfold c_is_sub_fun_def)
apply(auto)
done
lemma c_is_sub_fun_lm_2: "c_is_sub_fun ls f ⟹ c_is_sub_fun (c_cons (c_pair x (f x)) ls) f"
proof -
assume A1: "c_is_sub_fun ls f"
show ?thesis
proof (unfold c_is_sub_fun_def, rule allI, rule impI)
fix xa assume A2: "c_assoc_have_key (c_cons (c_pair x (f x)) ls) xa = 0" show "c_assoc_value (c_cons (c_pair x (f x)) ls) xa = f xa"
proof cases
assume C1: "xa = x"
then show "c_assoc_value (c_cons (c_pair x (f x)) ls) xa = f xa" by (simp add: PRecList.c_assoc_lm_2)
next
assume C2: "¬ xa = x"
then have S1: "c_assoc_have_key (c_cons (c_pair x (f x)) ls) xa = c_assoc_have_key ls xa" by (rule c_assoc_lm_3)
from C2 have S2: "c_assoc_value (c_cons (c_pair x (f x)) ls) xa = c_assoc_value ls xa" by (rule c_assoc_lm_4)
from A2 S1 have S3: "c_assoc_have_key ls xa = 0" by simp
from A1 S3 have "c_assoc_value ls xa = f xa" by (rule c_is_sub_fun_lm_1)
with S2 show ?thesis by simp
qed
qed
qed
lemma mod7_lm: "(n::nat) mod 7 = 0 ∨
(n::nat) mod 7 = 1 ∨
(n::nat) mod 7 = 2 ∨
(n::nat) mod 7 = 3 ∨
(n::nat) mod 7 = 4 ∨
(n::nat) mod 7 = 5 ∨
(n::nat) mod 7 = 6" by arith
lemma nat_to_sch_at_pos: "x > 0 ⟹ nat_to_sch x = (let u=(c_fst x) mod 7; v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
proof -
assume A: "x > 0"
show ?thesis
proof cases
assume A1: "x = 1"
then have S1: "c_fst x = 0"
proof -
have "1 = c_pair 0 1" by (simp add: c_pair_def sf_def)
then have "c_fst 1 = c_fst (c_pair 0 1)" by simp
then have "c_fst 1 = 0" by simp
with A1 show ?thesis by simp
qed
from A1 have S2: "nat_to_sch x = Base_zero" by simp
from S1 S2 show "nat_to_sch x = (let u=(c_fst x) mod 7; v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
apply(insert S1 S2)
apply(simp add: Let_def loc_f_def)
done
next
assume "¬ x = 1"
from A this have A2: "x > 1" by simp
from this have "nat_to_sch x = (let u=mod7 (c_fst x); v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (rule loc_srj_lm_2)
from this show "nat_to_sch x = (let u=(c_fst x) mod 7; v=c_snd x; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: mod7_def)
qed
qed
lemma nat_to_sch_0: "c_fst n mod 7 = 0 ⟹ nat_to_sch n = Base_zero"
proof -
assume A: "c_fst n mod 7 = 0"
show ?thesis
proof cases
assume "n=0"
then show "nat_to_sch n = Base_zero" by simp
next
assume "¬ n = 0" then have "n > 0" by simp
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (rule nat_to_sch_at_pos)
with A show "nat_to_sch n = Base_zero" by (simp add: Let_def loc_f_def)
qed
qed
lemma loc_lm_1: "c_fst n mod 7 ≠ 0 ⟹ n > 0"
proof -
assume A: "c_fst n mod 7 ≠ 0"
have "n = 0 ⟹ False"
proof -
assume "n = 0"
then have "c_fst n mod 7 = 0" by (simp add: c_fst_at_0)
with A show ?thesis by simp
qed
then have "¬ n = 0" by auto
then show ?thesis by simp
qed
lemma loc_lm_2: "c_fst n mod 7 ≠ 0 ⟹ nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)"
proof -
assume "c_fst n mod 7 ≠ 0"
then have "n > 0" by (rule loc_lm_1)
then show ?thesis by (rule nat_to_sch_at_pos)
qed
lemma nat_to_sch_1: "c_fst n mod 7 = 1 ⟹ nat_to_sch n = Base_suc"
proof -
assume A1: "c_fst n mod 7 = 1"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Base_suc" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_sch_2: "c_fst n mod 7 = 2 ⟹ nat_to_sch n = Base_fst"
proof -
assume A1: "c_fst n mod 7 = 2"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Base_fst" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_sch_3: "c_fst n mod 7 = 3 ⟹ nat_to_sch n = Base_snd"
proof -
assume A1: "c_fst n mod 7 = 3"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Base_snd" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_sch_4: "c_fst n mod 7 = 4 ⟹ nat_to_sch n = Comp_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))"
proof -
assume A1: "c_fst n mod 7 = 4"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Comp_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_sch_5: "c_fst n mod 7 = 5 ⟹ nat_to_sch n = Pair_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))"
proof -
assume A1: "c_fst n mod 7 = 5"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Pair_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_sch_6: "c_fst n mod 7 = 6 ⟹ nat_to_sch n = Rec_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))"
proof -
assume A1: "c_fst n mod 7 = 6"
then have "nat_to_sch n = (let u=(c_fst n) mod 7; v=c_snd n; v1=c_fst v; v2 = c_snd v; sch1=nat_to_sch v1; sch2=nat_to_sch v2 in loc_f u sch1 sch2)" by (simp add: loc_lm_2)
with A1 show "nat_to_sch n = Rec_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (simp add: Let_def loc_f_def)
qed
lemma nat_to_pr_lm_0: "c_fst n mod 7 = 0 ⟹ nat_to_pr n x = 0"
proof -
assume A: "c_fst n mod 7 = 0"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Base_zero" by (rule nat_to_sch_0)
from S1 S2 show ?thesis by simp
qed
lemma nat_to_pr_lm_1: "c_fst n mod 7 = 1 ⟹ nat_to_pr n x = Suc x"
proof -
assume A: "c_fst n mod 7 = 1"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Base_suc" by (rule nat_to_sch_1)
from S1 S2 show ?thesis by simp
qed
lemma nat_to_pr_lm_2: "c_fst n mod 7 = 2 ⟹ nat_to_pr n x = c_fst x"
proof -
assume A: "c_fst n mod 7 = 2"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Base_fst" by (rule nat_to_sch_2)
from S1 S2 show ?thesis by simp
qed
lemma nat_to_pr_lm_3: "c_fst n mod 7 = 3 ⟹ nat_to_pr n x = c_snd x"
proof -
assume A: "c_fst n mod 7 = 3"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Base_snd" by (rule nat_to_sch_3)
from S1 S2 show ?thesis by simp
qed
lemma nat_to_pr_lm_4: "c_fst n mod 7 = 4 ⟹ nat_to_pr n x = (nat_to_pr (c_fst (c_snd n)) (nat_to_pr (c_snd (c_snd n)) x))"
proof -
assume A: "c_fst n mod 7 = 4"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Comp_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (rule nat_to_sch_4)
from S1 S2 have S3: "nat_to_pr n x = sch_to_pr (Comp_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))) x" by simp
from S3 have S4: "nat_to_pr n x = (sch_to_pr (nat_to_sch (c_fst (c_snd n)))) ((sch_to_pr (nat_to_sch (c_snd (c_snd n)))) x)" by simp
from S4 show ?thesis by (simp add: nat_to_pr_def)
qed
lemma nat_to_pr_lm_5: "c_fst n mod 7 = 5 ⟹ nat_to_pr n x = (c_f_pair (nat_to_pr (c_fst (c_snd n))) (nat_to_pr (c_snd (c_snd n)))) x"
proof -
assume A: "c_fst n mod 7 = 5"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Pair_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (rule nat_to_sch_5)
from S1 S2 have S3: "nat_to_pr n x = sch_to_pr (Pair_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))) x" by simp
from S3 show ?thesis by (simp add: nat_to_pr_def)
qed
lemma nat_to_pr_lm_6: "c_fst n mod 7 = 6 ⟹ nat_to_pr n x = (UnaryRecOp (nat_to_pr (c_fst (c_snd n))) (nat_to_pr (c_snd (c_snd n)))) x"
proof -
assume A: "c_fst n mod 7 = 6"
have S1: "nat_to_pr n x = sch_to_pr (nat_to_sch n) x" by (simp add: nat_to_pr_def)
from A have S2: "nat_to_sch n = Rec_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))" by (rule nat_to_sch_6)
from S1 S2 have S3: "nat_to_pr n x = sch_to_pr (Rec_op (nat_to_sch (c_fst (c_snd n))) (nat_to_sch (c_snd (c_snd n)))) x" by simp
from S3 show ?thesis by (simp add: nat_to_pr_def)
qed
lemma univ_for_pr_lm_0: "c_fst (c_fst key) mod 7 = 0 ⟹ univ_for_pr key = 0"
proof -
assume A: "c_fst (c_fst key) mod 7 = 0"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_0)
qed
lemma univ_for_pr_lm_1: "c_fst (c_fst key) mod 7 = 1 ⟹ univ_for_pr key = Suc (c_snd key)"
proof -
assume A: "c_fst (c_fst key) mod 7 = 1"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_1)
qed
lemma univ_for_pr_lm_2: "c_fst (c_fst key) mod 7 = 2 ⟹ univ_for_pr key = c_fst (c_snd key)"
proof -
assume A: "c_fst (c_fst key) mod 7 = 2"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_2)
qed
lemma univ_for_pr_lm_3: "c_fst (c_fst key) mod 7 = 3 ⟹ univ_for_pr key = c_snd (c_snd key)"
proof -
assume A: "c_fst (c_fst key) mod 7 = 3"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_3)
qed
lemma univ_for_pr_lm_4: "c_fst (c_fst key) mod 7 = 4 ⟹ univ_for_pr key = (nat_to_pr (c_fst (c_snd (c_fst key))) (nat_to_pr (c_snd (c_snd (c_fst key))) (c_snd key)))"
proof -
assume A: "c_fst (c_fst key) mod 7 = 4"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_4)
qed
lemma univ_for_pr_lm_4_1: "c_fst (c_fst key) mod 7 = 4 ⟹ univ_for_pr key = univ_for_pr (c_pair (c_fst (c_snd (c_fst key))) (univ_for_pr (c_pair (c_snd (c_snd (c_fst key))) (c_snd key))))"
proof -
assume A: "c_fst (c_fst key) mod 7 = 4"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_4 univ_for_pr_def pr_conv_2_to_1_def)
qed
lemma univ_for_pr_lm_5: "c_fst (c_fst key) mod 7 = 5 ⟹ univ_for_pr key = c_pair (univ_for_pr (c_pair (c_fst (c_snd (c_fst key))) (c_snd key))) (univ_for_pr (c_pair (c_snd (c_snd (c_fst key))) (c_snd key)))"
proof -
assume A: "c_fst (c_fst key) mod 7 = 5"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A show ?thesis by (simp add: nat_to_pr_lm_5 c_f_pair_def univ_for_pr_def pr_conv_2_to_1_def)
qed
lemma univ_for_pr_lm_6_1: "⟦c_fst (c_fst key) mod 7 = 6; c_fst (c_snd key) = 0⟧ ⟹ univ_for_pr key = univ_for_pr (c_pair (c_fst (c_snd (c_fst key))) (c_snd (c_snd key)))"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 6"
assume A2: "c_fst (c_snd key) = 0"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A1 A2 show ?thesis by (simp add: nat_to_pr_lm_6 UnaryRecOp_def univ_for_pr_def pr_conv_2_to_1_def)
qed
lemma univ_for_pr_lm_6_2: "⟦c_fst (c_fst key) mod 7 = 6; c_fst (c_snd key) = Suc u⟧ ⟹ univ_for_pr key = univ_for_pr
(c_pair (c_snd (c_snd (c_fst key)))
(c_pair (c_pair u (univ_for_pr (c_pair (c_fst key) (c_pair u (c_snd (c_snd key)))))) (c_snd (c_snd key))))"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 6"
assume A2: "c_fst (c_snd key) = Suc u"
have S1: "univ_for_pr key = nat_to_pr (c_fst key) (c_snd key)" by (simp add: univ_for_pr_def pr_conv_2_to_1_def)
with A1 A2 show ?thesis
apply(simp add: nat_to_pr_lm_6 UnaryRecOp_def univ_for_pr_def pr_conv_2_to_1_def)
apply(simp add: pr_conv_1_to_3_def)
done
qed
lemma univ_for_pr_lm_6_3: "⟦c_fst (c_fst key) mod 7 = 6; c_fst (c_snd key) ≠ 0⟧ ⟹ univ_for_pr key = univ_for_pr
(c_pair (c_snd (c_snd (c_fst key)))
(c_pair (c_pair (c_fst (c_snd key) - 1) (univ_for_pr (c_pair (c_fst key) (c_pair (c_fst (c_snd key) - 1) (c_snd (c_snd key)))))) (c_snd (c_snd key))))"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 6"
assume A2: "c_fst (c_snd key) ≠ 0" then have
A3: "c_fst (c_snd key) > 0" by simp
let ?u = "c_fst (c_snd key) - (1::nat)"
from A3 have S1: "c_fst (c_snd key) = Suc ?u" by simp
from A1 S1 have S2: "univ_for_pr key = univ_for_pr
(c_pair (c_snd (c_snd (c_fst key)))
(c_pair (c_pair ?u (univ_for_pr (c_pair (c_fst key) (c_pair ?u (c_snd (c_snd key)))))) (c_snd (c_snd key))))" by (rule univ_for_pr_lm_6_2)
thus ?thesis by simp
qed
lemma g_comp_lm_0: "⟦ c_fst (c_fst key) mod 7 = 4; c_is_sub_fun ls univ_for_pr; g_comp ls key ≠ ls⟧ ⟹ g_comp ls key = c_cons (c_pair key (univ_for_pr key)) ls"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 4"
assume A2: "c_is_sub_fun ls univ_for_pr"
assume A3: "g_comp ls key ≠ ls"
let ?n = "c_fst key"
let ?x = "c_snd key"
let ?m = "c_snd ?n"
let ?m1 = "c_fst ?m"
let ?m2 = "c_snd ?m"
let ?k1 = "c_pair ?m2 ?x"
have S1: "c_assoc_have_key ls ?k1 = 0"
proof (rule ccontr)
assume A1_1: "c_assoc_have_key ls ?k1 ≠ 0"
then have "g_comp ls key = ls" by(simp add: g_comp_def)
with A3 show False by simp
qed
let ?y = "c_assoc_value ls ?k1"
from A2 S1 have S2: "?y = univ_for_pr ?k1" by (rule c_is_sub_fun_lm_1)
let ?k2 = "c_pair ?m1 ?y"
have S3: "c_assoc_have_key ls ?k2 = 0"
proof (rule ccontr)
assume A3_1: "c_assoc_have_key ls ?k2 ≠ 0"
then have "g_comp ls key = ls" by (simp add: g_comp_def Let_def)
with A3 show False by simp
qed
let ?z = "c_assoc_value ls ?k2"
from A2 S3 have S4: "?z = univ_for_pr ?k2" by (rule c_is_sub_fun_lm_1)
from S2 have S5: "?k2 = c_pair ?m1 (univ_for_pr ?k1)" by simp
from S4 S5 have S6: "?z = univ_for_pr (c_pair ?m1 (univ_for_pr ?k1))" by simp
from A1 S6 have S7: "?z = univ_for_pr key" by (simp add: univ_for_pr_lm_4_1)
from S1 S3 S7 show ?thesis by (simp add: g_comp_def Let_def)
qed
lemma g_comp_lm_1: "⟦ c_fst (c_fst key) mod 7 = 4; c_is_sub_fun ls univ_for_pr⟧ ⟹ c_is_sub_fun (g_comp ls key) univ_for_pr"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 4"
assume A2: "c_is_sub_fun ls univ_for_pr"
show ?thesis
proof cases
assume "g_comp ls key = ls"
with A2 show "c_is_sub_fun (g_comp ls key) univ_for_pr" by simp
next
assume "g_comp ls key ≠ ls"
from A1 A2 this have S1: "g_comp ls key = c_cons (c_pair key (univ_for_pr key)) ls" by (rule g_comp_lm_0)
with A2 show "c_is_sub_fun (g_comp ls key) univ_for_pr" by (simp add: c_is_sub_fun_lm_2)
qed
qed
lemma g_pair_lm_0: "⟦ c_fst (c_fst key) mod 7 = 5; c_is_sub_fun ls univ_for_pr; g_pair ls key ≠ ls⟧ ⟹ g_pair ls key = c_cons (c_pair key (univ_for_pr key)) ls"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 5"
assume A2: "c_is_sub_fun ls univ_for_pr"
assume A3: "g_pair ls key ≠ ls"
let ?n = "c_fst key"
let ?x = "c_snd key"
let ?m = "c_snd ?n"
let ?m1 = "c_fst ?m"
let ?m2 = "c_snd ?m"
let ?k1 = "c_pair ?m1 ?x"
have S1: "c_assoc_have_key ls ?k1 = 0"
proof (rule ccontr)
assume A1_1: "c_assoc_have_key ls ?k1 ≠ 0"
then have "g_pair ls key = ls" by(simp add: g_pair_def)
with A3 show False by simp
qed
let ?y1 = "c_assoc_value ls ?k1"
from A2 S1 have S2: "?y1 = univ_for_pr ?k1" by (rule c_is_sub_fun_lm_1)
let ?k2 = "c_pair ?m2 ?x"
have S3: "c_assoc_have_key ls ?k2 = 0"
proof (rule ccontr)
assume A3_1: "c_assoc_have_key ls ?k2 ≠ 0"
then have "g_pair ls key = ls" by (simp add: g_pair_def Let_def)
with A3 show False by simp
qed
let ?y2 = "c_assoc_value ls ?k2"
from A2 S3 have S4: "?y2 = univ_for_pr ?k2" by (rule c_is_sub_fun_lm_1)
let ?z = "c_pair ?y1 ?y2"
from S2 S4 have S5: "?z = c_pair (univ_for_pr ?k1) (univ_for_pr ?k2)" by simp
from A1 S5 have S6: "?z = univ_for_pr key" by (simp add: univ_for_pr_lm_5)
from S1 S3 S6 show ?thesis by (simp add: g_pair_def Let_def)
qed
lemma g_pair_lm_1: "⟦ c_fst (c_fst key) mod 7 = 5; c_is_sub_fun ls univ_for_pr⟧ ⟹ c_is_sub_fun (g_pair ls key) univ_for_pr"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 5"
assume A2: "c_is_sub_fun ls univ_for_pr"
show ?thesis
proof cases
assume "g_pair ls key = ls"
with A2 show "c_is_sub_fun (g_pair ls key) univ_for_pr" by simp
next
assume "g_pair ls key ≠ ls"
from A1 A2 this have S1: "g_pair ls key = c_cons (c_pair key (univ_for_pr key)) ls" by (rule g_pair_lm_0)
with A2 show "c_is_sub_fun (g_pair ls key) univ_for_pr" by (simp add: c_is_sub_fun_lm_2)
qed
qed
lemma g_rec_lm_0: "⟦ c_fst (c_fst key) mod 7 = 6; c_is_sub_fun ls univ_for_pr; g_rec ls key ≠ ls⟧ ⟹ g_rec ls key = c_cons (c_pair key (univ_for_pr key)) ls"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 6"
assume A2: "c_is_sub_fun ls univ_for_pr"
assume A3: "g_rec ls key ≠ ls"
let ?n = "c_fst key"
let ?x = "c_snd key"
let ?m = "c_snd ?n"
let ?m1 = "c_fst ?m"
let ?m2 = "c_snd ?m"
let ?y1 = "c_fst ?x"
let ?x1 = "c_snd ?x"
show ?thesis
proof cases
assume A1_1: "?y1 = 0"
let ?k1 = "c_pair ?m1 ?x1"
have S1_1: "c_assoc_have_key ls ?k1 = 0"
proof (rule ccontr)
assume "c_assoc_have_key ls ?k1 ≠ 0"
with A1_1 have "g_rec ls key = ls" by(simp add: g_rec_def)
with A3 show False by simp
qed
let ?v = "c_assoc_value ls ?k1"
from A2 S1_1 have S1_2: "?v = univ_for_pr ?k1" by (rule c_is_sub_fun_lm_1)
from A1 A1_1 S1_2 have S1_3: "?v = univ_for_pr key" by (simp add: univ_for_pr_lm_6_1)
from A1_1 S1_1 S1_3 show ?thesis by (simp add: g_rec_def Let_def)
next
assume A2_1: "?y1 ≠ 0" then have A2_2: "?y1 > 0" by simp
let ?y2 = "?y1 - (1::nat)"
let ?k2 = "c_pair ?n (c_pair ?y2 ?x1)"
have S2_1: "c_assoc_have_key ls ?k2 = 0"
proof (rule ccontr)
assume "c_assoc_have_key ls ?k2 ≠ 0"
with A2_1 have "g_rec ls key = ls" by (simp add: g_rec_def Let_def)
with A3 show False by simp
qed
let ?t1 = "c_assoc_value ls ?k2"
from A2 S2_1 have S2_2: "?t1 = univ_for_pr ?k2" by (rule c_is_sub_fun_lm_1)
let ?t2 = "c_pair (c_pair ?y2 ?t1) ?x1"
let ?k3 = "c_pair ?m2 ?t2"
have S2_3: "c_assoc_have_key ls ?k3 = 0"
proof (rule ccontr)
assume "c_assoc_have_key ls ?k3 ≠ 0"
with A2_1 have "g_rec ls key = ls" by (simp add: g_rec_def Let_def)
with A3 show False by simp
qed
let ?u = "c_assoc_value ls ?k3"
from A2 S2_3 have S2_4: "?u = univ_for_pr ?k3" by (rule c_is_sub_fun_lm_1)
from S2_4 S2_2 have S2_5: "?u = univ_for_pr (c_pair ?m2 (c_pair (c_pair ?y2 (univ_for_pr ?k2)) ?x1))" by simp
from A1 A2_1 S2_5 have S2_6: "?u = univ_for_pr key" by (simp add: univ_for_pr_lm_6_3)
from A2_1 S2_1 S2_3 S2_6 show ?thesis by (simp add: g_rec_def Let_def)
qed
qed
lemma g_rec_lm_1: "⟦ c_fst (c_fst key) mod 7 = 6; c_is_sub_fun ls univ_for_pr⟧ ⟹ c_is_sub_fun (g_rec ls key) univ_for_pr"
proof -
assume A1: "c_fst (c_fst key) mod 7 = 6"
assume A2: "c_is_sub_fun ls univ_for_pr"
show ?thesis
proof cases
assume "g_rec ls key = ls"
with A2 show "c_is_sub_fun (g_rec ls key) univ_for_pr" by simp
next
assume "g_rec ls key ≠ ls"
from A1 A2 this have S1: "g_rec ls key = c_cons (c_pair key (univ_for_pr key)) ls" by (rule g_rec_lm_0)
with A2 show "c_is_sub_fun (g_rec ls key) univ_for_pr" by (simp add: c_is_sub_fun_lm_2)
qed
qed
lemma g_step_lm_0: "c_fst (c_fst key) mod 7 = 0 ⟹ g_step ls key = c_cons (c_pair key 0) ls" by (simp add: g_step_def)
lemma g_step_lm_1: "c_fst (c_fst key) mod 7 = 1 ⟹ g_step ls key = c_cons (c_pair key (Suc (c_snd key))) ls" by (simp add: g_step_def Let_def)
lemma g_step_lm_2: "c_fst (c_fst key) mod 7 = 2 ⟹ g_step ls key = c_cons (c_pair key (c_fst (c_snd key))) ls" by (simp add: g_step_def Let_def)
lemma g_step_lm_3: "c_fst (c_fst key) mod 7 = 3 ⟹ g_step ls key = c_cons (c_pair key (c_snd (c_snd key))) ls" by (simp add: g_step_def Let_def)
lemma g_step_lm_4: "c_fst (c_fst key) mod 7 = 4 ⟹ g_step ls key = g_comp ls key" by (simp add: g_step_def)
lemma g_step_lm_5: "c_fst (c_fst key) mod 7 = 5 ⟹ g_step ls key = g_pair ls key" by (simp add: g_step_def)
lemma g_step_lm_6: "c_fst (c_fst key) mod 7 = 6 ⟹ g_step ls key = g_rec ls key" by (simp add: g_step_def)
lemma g_step_lm_7: "c_is_sub_fun ls univ_for_pr ⟹ c_is_sub_fun (g_step ls key) univ_for_pr"
proof -
assume A1: "c_is_sub_fun ls univ_for_pr"
let ?n = "c_fst key"
let ?x = "c_snd key"
let ?n1 = "(c_fst ?n) mod 7"
have S1: "?n1 = 0 ⟹ ?thesis"
proof -
assume A: "?n1 = 0"
then have S1_1: "g_step ls key = c_cons (c_pair key 0) ls" by (rule g_step_lm_0)
from A have S1_2: "univ_for_pr key = 0" by (rule univ_for_pr_lm_0)
from A1 have S1_3: "c_is_sub_fun (c_cons (c_pair key (univ_for_pr key)) ls) univ_for_pr" by (rule c_is_sub_fun_lm_2)
from S1_3 S1_1 S1_2 show ?thesis by simp
qed
have S2: "?n1 = 1 ⟹ ?thesis"
proof -
assume A: "?n1 = 1"
then have S2_1: "g_step ls key = c_cons (c_pair key (Suc (c_snd key))) ls" by (rule g_step_lm_1)
from A have S2_2: "univ_for_pr key = Suc (c_snd key)" by (rule univ_for_pr_lm_1)
from A1 have S2_3: "c_is_sub_fun (c_cons (c_pair key (univ_for_pr key)) ls) univ_for_pr" by (rule c_is_sub_fun_lm_2)
from S2_3 S2_1 S2_2 show ?thesis by simp
qed
have S3: "?n1 = 2 ⟹ ?thesis"
proof -
assume A: "?n1 = 2"
then have S2_1: "g_step ls key = c_cons (c_pair key (c_fst (c_snd key))) ls" by (rule g_step_lm_2)
from A have S2_2: "univ_for_pr key = c_fst (c_snd key)" by (rule univ_for_pr_lm_2)
from A1 have S2_3: "c_is_sub_fun (c_cons (c_pair key (univ_for_pr key)) ls) univ_for_pr" by (rule c_is_sub_fun_lm_2)
from S2_3 S2_1 S2_2 show ?thesis by simp
qed
have S4: "?n1 = 3 ⟹ ?thesis"
proof -
assume A: "?n1 = 3"
then have S2_1: "g_step ls key = c_cons (c_pair key (c_snd (c_snd key))) ls" by (rule g_step_lm_3)
from A have S2_2: "univ_for_pr key = c_snd (c_snd key)" by (rule univ_for_pr_lm_3)
from A1 have S2_3: "c_is_sub_fun (c_cons (c_pair key (univ_for_pr key)) ls) univ_for_pr" by (rule c_is_sub_fun_lm_2)
from S2_3 S2_1 S2_2 show ?thesis by simp
qed
have S5: "?n1 = 4 ⟹ ?thesis"
proof -
assume A: "?n1 = 4"
then have S2_1: "g_step ls key = g_comp ls key" by (rule g_step_lm_4)
from A A1 S2_1 show ?thesis by (simp add: g_comp_lm_1)
qed
have S6: "?n1 = 5 ⟹ ?thesis"
proof -
assume A: "?n1 = 5"
then have S2_1: "g_step ls key = g_pair ls key" by (rule g_step_lm_5)
from A A1 S2_1 show ?thesis by (simp add: g_pair_lm_1)
qed
have S7: "?n1 = 6 ⟹ ?thesis"
proof -
assume A: "?n1 = 6"
then have S2_1: "g_step ls key = g_rec ls key" by (rule g_step_lm_6)
from A A1 S2_1 show ?thesis by (simp add: g_rec_lm_1)
qed
have S8: "?n1=0 ∨ ?n1=1 ∨ ?n1=2 ∨ ?n1=3 ∨ ?n1=4 ∨ ?n1=5 ∨ ?n1=6" by (rule mod7_lm)
with S1 S2 S3 S4 S5 S6 S7 show ?thesis by fast
qed
theorem pr_gr_1: "c_is_sub_fun (pr_gr x) univ_for_pr"
apply(induct x)
apply(simp add: pr_gr_at_0 c_is_sub_fun_def c_assoc_have_key_df)
apply(simp add: pr_gr_at_Suc)
apply(simp add: g_step_lm_7)
done
lemma comp_next: "g_comp ls key = ls ∨ c_tl (g_comp ls key) = ls" by(simp add: g_comp_def Let_def)
lemma pair_next: "g_pair ls key = ls ∨ c_tl (g_pair ls key) = ls" by(simp add: g_pair_def Let_def)
lemma rec_next: "g_rec ls key = ls ∨ c_tl (g_rec ls key) = ls" by(simp add: g_rec_def Let_def)
lemma step_next: "g_step ls key = ls ∨ c_tl (g_step ls key) = ls"
apply(simp add: g_step_def comp_next pair_next rec_next Let_def)
done
lemma lm1: "pr_gr (Suc x) = pr_gr x ∨ c_tl (pr_gr (Suc x)) = pr_gr x" by(simp add: pr_gr_at_Suc step_next)
lemma c_assoc_have_key_pos: "c_assoc_have_key ls x = 0 ⟹ ls > 0"
proof -
assume A1: "c_assoc_have_key ls x = 0"
thus ?thesis
proof (cases)
assume A2: "ls = 0"
then have S1: "c_assoc_have_key ls x = 1" by (simp add: c_assoc_have_key_df)
with A1 have S2: False by auto
then show "ls > 0" by auto
next
assume A3: "¬ ls = 0"
then show "ls > 0" by auto
qed
qed
lemma lm2: "c_assoc_have_key (c_tl ls) key = 0 ⟹ c_assoc_have_key ls key = 0"
proof -
assume A1: "c_assoc_have_key (c_tl ls) key = 0"
from A1 have S1: "c_tl ls > 0" by (rule c_assoc_have_key_pos)
have S2: "c_tl ls ≤ ls" by (rule c_tl_le)
from S1 S2 have S3: "ls ≠ 0" by auto
from A1 S3 show ?thesis by (auto simp add: c_assoc_have_key_lm_1)
qed
lemma lm3: "c_assoc_have_key (pr_gr x) key = 0 ⟹ c_assoc_have_key (pr_gr (Suc x)) key = 0"
proof -
assume A1: "c_assoc_have_key (pr_gr x) key = 0"
have S1: "pr_gr (Suc x) = pr_gr x ∨ c_tl (pr_gr (Suc x)) = pr_gr x" by (rule lm1)
from A1 have S2: "pr_gr (Suc x) = pr_gr x ⟹ ?thesis" by auto
have S3: "c_tl (pr_gr (Suc x)) = pr_gr x ⟹ ?thesis"
proof -
assume "c_tl (pr_gr (Suc x)) = pr_gr x" (is "c_tl ?ls = _")
with A1 have "c_assoc_have_key (c_tl ?ls) key = 0" by auto
then show "c_assoc_have_key ?ls key = 0" by (rule lm2)
qed
from S1 S2 S3 show ?thesis by auto
qed
lemma lm4: "⟦ c_assoc_have_key (pr_gr x) key = 0; 0 ≤ y⟧ ⟹ c_assoc_have_key (pr_gr (x+y)) key = 0"
apply(induct_tac y)
apply(auto)
apply(simp add: lm3)
done
lemma lm5: "⟦ c_assoc_have_key (pr_gr x) key = 0; x ≤ y ⟧ ⟹ c_assoc_have_key (pr_gr y) key = 0"
proof -
assume A1: "c_assoc_have_key (pr_gr x) key = 0"
assume A2: "x ≤ y"
let ?z = "y-x"
from A2 have S1: "0 ≤ ?z" by auto
from A2 have S2: "y = x + ?z" by auto
from A1 S1 have S3: "c_assoc_have_key (pr_gr (x+?z)) key = 0" by (rule lm4)
from S2 S3 show ?thesis by auto
qed
lemma loc_upb_lm_1: "n = 0 ⟹ (c_fst n) mod 7 = 0"
apply(simp add: c_fst_at_0)
done
lemma loc_upb_lm_2: "(c_fst n) mod 7 > 1 ⟹ c_snd n < n"
proof -
assume A1: "c_fst n mod 7 > 1"
from A1 have S1: "1 < c_fst n" by simp
have S2: "c_fst n ≤ n" by (rule c_fst_le_arg)
from S1 S2 have S3: "1 < n" by simp
from S3 have S4: "n>1" by simp
from S4 show ?thesis by (rule c_snd_less_arg)
qed
lemma loc_upb_lm_2_0: "(c_fst n) mod 7 = 4 ⟶ c_fst (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 4"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_fst (c_snd n) ≤ c_snd n" by (rule c_fst_le_arg)
from S1 S2 show "c_fst (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_2: "(c_fst n) mod 7 = 4 ⟶ c_snd (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 4"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_snd (c_snd n) ≤ c_snd n" by (rule c_snd_le_arg)
from S1 S2 show "c_snd (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_3: "(c_fst n) mod 7 = 5 ⟶ c_fst (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 5"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_fst (c_snd n) ≤ c_snd n" by (rule c_fst_le_arg)
from S1 S2 show "c_fst (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_4: "(c_fst n) mod 7 = 5 ⟶ c_snd (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 5"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_snd (c_snd n) ≤ c_snd n" by (rule c_snd_le_arg)
from S1 S2 show "c_snd (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_5: "(c_fst n) mod 7 = 6 ⟶ c_fst (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 6"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_fst (c_snd n) ≤ c_snd n" by (rule c_fst_le_arg)
from S1 S2 show "c_fst (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_6: "(c_fst n) mod 7 = 6 ⟶ c_snd (c_snd n) < n"
proof
assume A1: "c_fst n mod 7 = 6"
then have S0: "c_fst n mod 7 > 1" by auto
then have S1: "c_snd n < n" by (rule loc_upb_lm_2)
have S2: "c_snd (c_snd n) ≤ c_snd n" by (rule c_snd_le_arg)
from S1 S2 show "c_snd (c_snd n) < n" by auto
qed
lemma loc_upb_lm_2_7: "⟦y2 = y1 - (1::nat); 0 < y1; x1 = c_snd x; y1 = c_fst x⟧ ⟹ c_pair y2 x1 < x"
proof -
assume A1: "y2 = y1 - (1::nat)" and A2: "0 < y1" and A3: "x1 = c_snd x" and A4: "y1 = c_fst x"
from A1 A2 have S1: "y2 < y1" by auto
from S1 have S2: "c_pair y2 x1 < c_pair y1 x1" by (rule c_pair_strict_mono1)
from A3 A4 have S3: "c_pair y1 x1 = x" by auto
from S2 S3 show "c_pair y2 x1 < x" by auto
qed
function loc_upb :: "nat ⇒ nat ⇒ nat" where
aa: "loc_upb n x = (
let n1 = (c_fst n) mod 7 in
if n1 = 0 then (c_pair (c_pair n x) 0) + 1 else
if n1 = 1 then (c_pair (c_pair n x) 0) + 1 else
if n1 = 2 then (c_pair (c_pair n x) 0) + 1 else
if n1 = 3 then (c_pair (c_pair n x) 0) + 1 else
if n1 = 4 then (
let m = c_snd n; m1 = c_fst m; m2 = c_snd m;
y = c_assoc_value (pr_gr (loc_upb m2 x)) (c_pair m2 x) in
(c_pair (c_pair n x) (loc_upb m2 x + loc_upb m1 y)) + 1
) else
if n1 = 5 then (
let m = c_snd n; m1 = c_fst m; m2 = c_snd m in
(c_pair (c_pair n x) (loc_upb m1 x + loc_upb m2 x)) + 1
) else
if n1 = 6 then (
let m = c_snd n; m1 = c_fst m; m2 = c_snd m; y1 = c_fst x; x1 = c_snd x in
if y1 = 0 then (
(c_pair (c_pair n x) (loc_upb m1 x1)) + 1
) else (
let y2 = y1-(1::nat);
t1 = c_assoc_value (pr_gr (loc_upb n (c_pair y2 x1))) (c_pair n (c_pair y2 x1)); t2 = c_pair (c_pair y2 t1) x1 in
(c_pair (c_pair n x) (loc_upb n (c_pair y2 x1) + loc_upb m2 t2)) + 1
)
)
else 0
)"
by auto
termination
apply (relation "measure (λ m. m) <*lex*> measure (λ n. n)")
apply (simp_all add: loc_upb_lm_2_0 loc_upb_lm_2_2 loc_upb_lm_2_3 loc_upb_lm_2_4 loc_upb_lm_2_5 loc_upb_lm_2_6 loc_upb_lm_2_7)
apply auto
done
definition
lex_p :: "((nat × nat) × nat × nat) set" where
"lex_p = ((measure (λ m. m)) <*lex*> (measure (λ n. n)))"
lemma wf_lex_p: "wf(lex_p)"
apply(simp add: lex_p_def)
apply(auto)
done
lemma lex_p_eq: "((n',x'), (n,x)) ∈ lex_p = (n'<n ∨ n'=n ∧ x'<x) "
apply(simp add: lex_p_def)
done
lemma loc_upb_lex_0: "c_fst n mod 7 = 0 ⟹ c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "c_fst n mod 7 = 0"
let ?key = "c_pair n x"
let ?s = "c_pair ?key 0"
let ?ls = "pr_gr ?s"
from A1 have "loc_upb n x = ?s + 1" by simp
then have S1: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from A1 have S2: "g_step ?ls ?key = c_cons (c_pair ?key 0) ?ls" by (simp add: g_step_def)
from S1 S2 have "pr_gr (loc_upb n x) = c_cons (c_pair ?key 0) ?ls" by auto
thus ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_lex_1: "c_fst n mod 7 = 1 ⟹ c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "c_fst n mod 7 = 1"
let ?key = "c_pair n x"
let ?s = "c_pair ?key 0"
let ?ls = "pr_gr ?s"
from A1 have "loc_upb n x = ?s + 1" by simp
then have S1: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from A1 have S2: "g_step ?ls ?key = c_cons (c_pair ?key (Suc x)) ?ls" by (simp add: g_step_def)
from S1 S2 have "pr_gr (loc_upb n x) = c_cons (c_pair ?key (Suc x)) ?ls" by auto
thus ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_lex_2: "c_fst n mod 7 = 2 ⟹ c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "c_fst n mod 7 = 2"
let ?key = "c_pair n x"
let ?s = "c_pair ?key 0"
let ?ls = "pr_gr ?s"
from A1 have "loc_upb n x = ?s + 1" by simp
then have S1: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from A1 have S2: "g_step ?ls ?key = c_cons (c_pair ?key (c_fst x)) ?ls" by (simp add: g_step_def)
from S1 S2 have "pr_gr (loc_upb n x) = c_cons (c_pair ?key (c_fst x)) ?ls" by auto
thus ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_lex_3: "c_fst n mod 7 = 3 ⟹ c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "c_fst n mod 7 = 3"
let ?key = "c_pair n x"
let ?s = "c_pair ?key 0"
let ?ls = "pr_gr ?s"
from A1 have "loc_upb n x = ?s + 1" by simp
then have S1: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from A1 have S2: "g_step ?ls ?key = c_cons (c_pair ?key (c_snd x)) ?ls" by (simp add: g_step_def)
from S1 S2 have "pr_gr (loc_upb n x) = c_cons (c_pair ?key (c_snd x)) ?ls" by auto
thus ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_lex_4: "⟦⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0;
c_fst n mod 7 = 4⟧ ⟹
c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0"
assume A2: "c_fst n mod 7 = 4"
let ?key = "c_pair n x"
let ?m1 = "c_fst (c_snd n)"
let ?m2 = "c_snd (c_snd n)"
define upb1 where "upb1 = loc_upb ?m2 x"
from A2 have m2_lt_n: "?m2 < n" by (simp add: loc_upb_lm_2_2)
then have M2: "((?m2, x), (n,x)) ∈ lex_p" by (simp add: lex_p_eq)
with A1 upb1_def have S1: "c_assoc_have_key (pr_gr upb1) (c_pair ?m2 x) = 0" by auto
from M2 have M2': "((?m2, x), n, x) ∈ measure (λm. m) <*lex*> measure (λn. n)" by (simp add: lex_p_def)
have T1: "c_is_sub_fun (pr_gr upb1) univ_for_pr" by (rule pr_gr_1)
from T1 S1 have T2: "c_assoc_value (pr_gr upb1) (c_pair ?m2 x) = univ_for_pr (c_pair ?m2 x)" by (rule c_is_sub_fun_lm_1)
define y where "y = c_assoc_value (pr_gr upb1) (c_pair ?m2 x)"
from T2 y_def have T3: "y = univ_for_pr (c_pair ?m2 x)" by auto
define upb2 where "upb2 = loc_upb ?m1 y"
from A2 have "?m1 < n" by (simp add: loc_upb_lm_2_0)
then have M1: "((?m1, y), (n,x)) ∈ lex_p" by (simp add: lex_p_eq)
with A1 have S2: "c_assoc_have_key (pr_gr (loc_upb ?m1 y)) (c_pair ?m1 y) = 0" by auto
from M1 have M1': "((?m1, y), n, x) ∈ measure (λm. m) <*lex*> measure (λn. n)" by (simp add: lex_p_def)
from S1 upb1_def have S3: "c_assoc_have_key (pr_gr upb1) (c_pair ?m2 x) = 0" by auto
from S2 upb2_def have S4: "c_assoc_have_key (pr_gr upb2) (c_pair ?m1 y) = 0" by auto
let ?s = "c_pair ?key (upb1 + upb2)"
let ?ls = "pr_gr ?s"
let ?sum_upb = "upb1 +upb2"
from A2 have "?m1 < n" by (simp add: loc_upb_lm_2_0)
then have "((?m1, x), (n,x)) ∈ lex_p" by (simp add: lex_p_eq)
then have M1'': "((?m1, x), n, x) ∈ measure (λm. m) <*lex*> measure (λn. n)" by (simp add: lex_p_def)
from A2 M2' M1'' have S11: "loc_upb n x = (let y = c_assoc_value (pr_gr (loc_upb ?m2 x)) (c_pair ?m2 x)
in (c_pair (c_pair n x)
(loc_upb ?m2 x + loc_upb ?m1 y)) + 1)"
by(simp add: Let_def)
define upb where "upb = loc_upb n x"
from S11 y_def upb1_def upb2_def have "loc_upb n x = ?s + 1" by (simp add: Let_def)
with upb_def have S11: "upb = ?s + 1" by auto
have S7: "?sum_upb ≤ ?s" by (rule arg2_le_c_pair)
have upb1_le_s: "upb1 ≤ ?s"
proof -
have S1: "upb1 ≤ ?sum_upb" by (rule Nat.le_add1)
from S1 S7 show ?thesis by auto
qed
have upb2_le_s: "upb2 ≤ ?s"
proof -
have S1: "upb2 ≤ ?sum_upb" by (rule Nat.le_add2)
from S1 S7 show ?thesis by auto
qed
have S18: "pr_gr upb = g_comp ?ls ?key"
proof -
from S11 have S1: "pr_gr upb = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from A2 have S2: "g_step ?ls ?key = g_comp ?ls ?key" by (simp add: g_step_def)
from S1 S2 show ?thesis by auto
qed
from S3 upb1_le_s have S19: "c_assoc_have_key ?ls (c_pair ?m2 x) = 0" by (rule lm5)
from S4 upb2_le_s have S20: "c_assoc_have_key ?ls (c_pair ?m1 y) = 0" by (rule lm5)
have T_ls: "c_is_sub_fun ?ls univ_for_pr" by (rule pr_gr_1)
from T_ls S19 have T_ls2: "c_assoc_value ?ls (c_pair ?m2 x) = univ_for_pr (c_pair ?m2 x)" by (rule c_is_sub_fun_lm_1)
from T3 T_ls2 have T_y: "c_assoc_value ?ls (c_pair ?m2 x) = y" by auto
from T_y S19 S20 have S21: "g_comp ?ls ?key = c_cons (c_pair ?key (c_assoc_value ?ls (c_pair ?m1 y))) ?ls"
by(unfold g_comp_def)(simp del: loc_upb.simps add: Let_def)
from S18 S21 have "pr_gr upb = c_cons (c_pair ?key (c_assoc_value ?ls (c_pair ?m1 y))) ?ls" by auto
with upb_def have "pr_gr (loc_upb n x) = c_cons (c_pair ?key (c_assoc_value ?ls (c_pair ?m1 y))) ?ls" by auto
thus ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_lex_5: "⟦⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0;
c_fst n mod 7 = 5⟧ ⟹
c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0"
assume A2: "c_fst n mod 7 = 5"
let ?key = "c_pair n x"
let ?m1 = "c_fst (c_snd n)"
let ?m2 = "c_snd (c_snd n)"
from A2 have "?m1 < n" by (simp add: loc_upb_lm_2_3)
then have "((?m1, x), (n,x)) ∈ lex_p" by (simp add: lex_p_eq)
with A1 have S1: "c_assoc_have_key (pr_gr (loc_upb ?m1 x)) (c_pair ?m1 x) = 0" by auto
from A2 have "?m2 < n" by (simp add: loc_upb_lm_2_4)
then have "((?m2, x), (n,x)) ∈ lex_p" by (simp add: lex_p_eq)
with A1 have S2: "c_assoc_have_key (pr_gr (loc_upb ?m2 x)) (c_pair ?m2 x) = 0" by auto
define upb1 where "upb1 = loc_upb ?m1 x"
define upb2 where "upb2 = loc_upb ?m2 x"
from upb1_def S1 have S3: "c_assoc_have_key (pr_gr upb1) (c_pair ?m1 x) = 0" by auto
from upb2_def S2 have S4: "c_assoc_have_key (pr_gr upb2) (c_pair ?m2 x) = 0" by auto
let ?sum_upb = "upb1 +upb2"
have S5: "upb1 ≤ ?sum_upb" by (rule Nat.le_add1)
have S6: "upb2 ≤ ?sum_upb" by (rule Nat.le_add2)
let ?s = "(c_pair ?key ?sum_upb)"
have S7: "?sum_upb ≤ ?s" by (rule arg2_le_c_pair)
from S5 S7 have S8: "upb1 ≤ ?s" by auto
from S6 S7 have S9: "upb2 ≤ ?s" by auto
let ?ls = "pr_gr ?s"
from A2 upb1_def upb2_def have S10: "loc_upb n x = ?s + 1" by (simp add: Let_def)
define upb where "upb = loc_upb n x"
from upb_def S10 have S11: "upb = ?s + 1" by auto
from S11 have S12: "pr_gr upb = g_step (pr_gr ?s) (c_fst ?s)" by (simp add: pr_gr_at_Suc)
from S8 S10 upb_def have S13: "upb1 ≤ upb" by (simp only:)
from S9 S10 upb_def have S14: "upb2 ≤ upb" by (simp only:)
from S3 S13 have S15: "c_assoc_have_key (pr_gr upb) (c_pair ?m1 x) = 0" by (rule lm5)
from S4 S14 have S16: "c_assoc_have_key (pr_gr upb) (c_pair ?m2 x) = 0" by (rule lm5)
from A2 have S17: "g_step ?ls ?key = g_pair ?ls ?key" by (simp add: g_step_def)
from S12 S17 have S18: "pr_gr upb = g_pair ?ls ?key" by auto
from S3 S8 have S19: "c_assoc_have_key ?ls (c_pair ?m1 x) = 0" by (rule lm5)
from S4 S9 have S20: "c_assoc_have_key ?ls (c_pair ?m2 x) = 0" by (rule lm5)
let ?y1 = "c_assoc_value ?ls (c_pair ?m1 x)"
let ?y2 = "c_assoc_value ?ls (c_pair ?m2 x)"
let ?y = "c_pair ?y1 ?y2"
from S19 S20 have S21: "g_pair ?ls ?key = c_cons (c_pair ?key ?y) ?ls" by (unfold g_pair_def, simp add: Let_def)
from S18 S21 have S22: "pr_gr upb = c_cons (c_pair ?key ?y) ?ls" by auto
from upb_def S22 have S23: "pr_gr (loc_upb n x) = c_cons (c_pair ?key ?y) ?ls" by auto
from S23 show ?thesis by (simp add: c_assoc_lm_1)
qed
lemma loc_upb_6_z: "⟦c_fst n mod 7 =6; c_fst x = 0⟧ ⟹
loc_upb n x = c_pair (c_pair n x) (loc_upb (c_fst (c_snd n)) (c_snd x)) + 1" by (simp add: Let_def)
lemma loc_upb_6: "⟦c_fst n mod 7 =6; c_fst x ≠ 0⟧ ⟹ loc_upb n x = (
let m = c_snd n; m1 = c_fst m; m2 = c_snd m; y1 = c_fst x; x1 = c_snd x;
y2 = y1 - 1;
t1 = c_assoc_value (pr_gr (loc_upb n (c_pair y2 x1))) (c_pair n (c_pair y2 x1));
t2 = c_pair (c_pair y2 t1) x1 in
c_pair (c_pair n x) (loc_upb n (c_pair y2 x1) + (loc_upb m2 t2)) + 1)"
by (simp add: Let_def)
lemma loc_upb_lex_6: "⟦⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0;
c_fst n mod 7 = 6⟧ ⟹
c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0"
assume A2: "c_fst n mod 7 = 6"
let ?key = "c_pair n x"
let ?m1 = "c_fst (c_snd n)"
let ?m2 = "c_snd (c_snd n)"
let ?y1 = "c_fst x"
let ?x1 = "c_snd x"
define upb where "upb = loc_upb n x"
show ?thesis
proof (cases)
assume A: "?y1 = 0"
from A2 A have S1: "loc_upb n x = c_pair ?key (loc_upb ?m1 (c_snd x)) + 1" by (rule loc_upb_6_z)
define upb1 where "upb1 = loc_upb ?m1 (c_snd x)"
from upb1_def S1 have S2: "loc_upb n x = c_pair ?key upb1 + 1" by auto
let ?s = "c_pair ?key upb1"
from S2 have S3: "pr_gr (loc_upb n x) = pr_gr (Suc ?s)" by simp
have "pr_gr (Suc ?s) = g_step (pr_gr ?s) (c_fst ?s)" by (rule pr_gr_at_Suc)
with S3 have S4: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) ?key" by auto
let ?ls = "pr_gr ?s"
from A2 have "g_step ?ls ?key = g_rec ?ls ?key" by (simp add: g_step_def)
with S4 have S5: "pr_gr (loc_upb n x) = g_rec ?ls ?key" by auto
have S6: "c_assoc_have_key ?ls (c_pair ?m1 ?x1) = 0"
proof -
from A2 have "?m1 < n" by (simp add: loc_upb_lm_2_5)
then have "((?m1,?x1), n, x) ∈ lex_p" by (simp add: lex_p_eq)
with A1 upb1_def have "c_assoc_have_key (pr_gr upb1) (c_pair ?m1 ?x1) = 0" by auto
also have "upb1 ≤ ?s" by (rule arg2_le_c_pair)
ultimately show ?thesis by (rule lm5)
qed
from A S6 have "g_rec ?ls ?key = c_cons (c_pair ?key (c_assoc_value ?ls (c_pair ?m1 ?x1))) ?ls" by (simp add: g_rec_def Let_def)
with S5 show ?thesis by (simp add: c_assoc_lm_1)
next
assume A: "c_fst x ≠ 0" then have y1_pos: "c_fst x > 0" by auto
let ?y2 = "?y1 - 1"
from A2 A have "loc_upb n x = (
let m = c_snd n; m1 = c_fst m; m2 = c_snd m; y1 = c_fst x; x1 = c_snd x;
y2 = y1 - 1;
t1 = c_assoc_value (pr_gr (loc_upb n (c_pair y2 x1))) (c_pair n (c_pair y2 x1));
t2 = c_pair (c_pair y2 t1) x1 in
c_pair (c_pair n x) (loc_upb n (c_pair y2 x1) + (loc_upb m2 t2)) + 1)" by (rule loc_upb_6)
then have S1: "loc_upb n x = (
let
t1 = c_assoc_value (pr_gr (loc_upb n (c_pair ?y2 ?x1))) (c_pair n (c_pair ?y2 ?x1));
t2 = c_pair (c_pair ?y2 t1) ?x1 in
c_pair (c_pair n x) (loc_upb n (c_pair ?y2 ?x1) + (loc_upb ?m2 t2)) + 1)" by (simp del: loc_upb.simps add: Let_def)
let ?t1 = "univ_for_pr (c_pair n (c_pair ?y2 ?x1))"
let ?t2 = "c_pair (c_pair ?y2 ?t1) ?x1"
have S1_1: "c_assoc_have_key (pr_gr (loc_upb n (c_pair ?y2 ?x1))) (c_pair n (c_pair ?y2 ?x1)) = 0"
proof -
from A have "?y2 < ?y1" by auto
then have "c_pair ?y2 ?x1 < c_pair ?y1 ?x1" by (rule c_pair_strict_mono1)
then have "((n, c_pair ?y2 ?x1),n,x) ∈ lex_p" by (simp add: lex_p_eq)
with A1 show ?thesis by auto
qed
have S2: "c_assoc_value (pr_gr (loc_upb n (c_pair ?y2 ?x1))) (c_pair n (c_pair ?y2 ?x1)) = univ_for_pr (c_pair n (c_pair ?y2 ?x1))"
proof -
have "c_is_sub_fun (pr_gr (loc_upb n (c_pair ?y2 ?x1))) univ_for_pr" by (rule pr_gr_1)
with S1_1 show ?thesis by (simp add: c_is_sub_fun_lm_1)
qed
from S1 S2 have S3: "loc_upb n x = c_pair (c_pair n x) (loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2) + 1" by (simp del: loc_upb.simps add: Let_def)
let ?s = "c_pair (c_pair n x) (loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2)"
from S3 have S4: "pr_gr (loc_upb n x) = pr_gr (Suc ?s)" by (simp del: loc_upb.simps)
have "pr_gr (Suc ?s) = g_step (pr_gr ?s) (c_fst ?s)" by (rule pr_gr_at_Suc)
with S4 have S5: "pr_gr (loc_upb n x) = g_step (pr_gr ?s) ?key" by (simp del: loc_upb.simps)
let ?ls = "pr_gr ?s"
from A2 have "g_step ?ls ?key = g_rec ?ls ?key" by (simp add: g_step_def)
with S5 have S6: "pr_gr (loc_upb n x) = g_rec ?ls ?key" by (simp del: loc_upb.simps)
have S7: "c_assoc_have_key ?ls (c_pair n (c_pair ?y2 ?x1)) = 0"
proof -
have "loc_upb n (c_pair ?y2 ?x1) ≤ loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2" by (auto simp del: loc_upb.simps)
also have "loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2 ≤ ?s" by (rule arg2_le_c_pair)
ultimately have S7_1: "loc_upb n (c_pair ?y2 ?x1) ≤ ?s" by (auto simp del: loc_upb.simps)
from S1_1 S7_1 show ?thesis by (rule lm5)
qed
have S8: "c_assoc_value ?ls (c_pair n (c_pair ?y2 ?x1)) = ?t1"
proof -
have "c_is_sub_fun ?ls univ_for_pr" by (rule pr_gr_1)
with S7 show ?thesis by (simp add: c_is_sub_fun_lm_1)
qed
have S9: "c_assoc_have_key ?ls (c_pair ?m2 ?t2) = 0"
proof -
from A2 have "?m2 < n" by (simp add: loc_upb_lm_2_6)
then have "((?m2,?t2), n, x) ∈ lex_p" by (simp add: lex_p_eq)
with A1 have "c_assoc_have_key (pr_gr (loc_upb ?m2 ?t2)) (c_pair ?m2 ?t2) = 0" by auto
also have "loc_upb ?m2 ?t2 ≤ ?s"
proof -
have "loc_upb ?m2 ?t2 ≤ loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2" by (auto simp del: loc_upb.simps)
also have "loc_upb n (c_pair ?y2 ?x1) + loc_upb ?m2 ?t2 ≤ ?s" by (rule arg2_le_c_pair)
ultimately show ?thesis by (auto simp del: loc_upb.simps)
qed
ultimately show ?thesis by (rule lm5)
qed
from A S7 S8 S9 have "g_rec ?ls ?key = c_cons (c_pair ?key (c_assoc_value ?ls (c_pair ?m2 ?t2))) ?ls" by (simp del: loc_upb.simps add: g_rec_def Let_def)
with S6 show ?thesis by (simp add: c_assoc_lm_1)
qed
qed
lemma wf_upb_step_0:
"⟦⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0⟧ ⟹
c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
assume A1: "⋀ n' x'. ((n',x'), (n,x)) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0"
let ?n1 = "(c_fst n) mod 7"
have S1: "?n1 = 0 ⟹ ?thesis"
proof -
assume A: "?n1 = 0"
thus ?thesis by (rule loc_upb_lex_0)
qed
have S2: "?n1 = 1 ⟹ ?thesis"
proof -
assume A: "?n1 = 1"
thus ?thesis by (rule loc_upb_lex_1)
qed
have S3: "?n1 = 2 ⟹ ?thesis"
proof -
assume A: "?n1 = 2"
thus ?thesis by (rule loc_upb_lex_2)
qed
have S4: "?n1 = 3 ⟹ ?thesis"
proof -
assume A: "?n1 = 3"
thus ?thesis by (rule loc_upb_lex_3)
qed
have S5: "?n1 = 4 ⟹ ?thesis"
proof -
assume A: "?n1 = 4"
from A1 A show ?thesis by (rule loc_upb_lex_4)
qed
have S6: "?n1 = 5 ⟹ ?thesis"
proof -
assume A: "?n1 = 5"
from A1 A show ?thesis by (rule loc_upb_lex_5)
qed
have S7: "?n1 = 6 ⟹ ?thesis"
proof -
assume A: "?n1 = 6"
from A1 A show ?thesis by (rule loc_upb_lex_6)
qed
have S8: "?n1=0 ∨ ?n1=1 ∨ ?n1=2 ∨ ?n1=3 ∨ ?n1=4 ∨ ?n1=5 ∨ ?n1=6" by (rule mod7_lm)
from S1 S2 S3 S4 S5 S6 S7 S8 show ?thesis by fast
qed
lemma wf_upb_step:
assumes A1: "⋀ p2. (p2, p1) ∈ lex_p ⟹
c_assoc_have_key (pr_gr (loc_upb (fst p2) (snd p2))) (c_pair (fst p2) (snd p2)) = 0"
shows "c_assoc_have_key (pr_gr (loc_upb (fst p1) (snd p1))) (c_pair (fst p1) (snd p1)) = 0"
proof -
let ?n = "fst p1"
let ?x = "snd p1"
from A1 have S1: "⋀ p2. (p2, (?n, ?x)) ∈ lex_p ⟹
c_assoc_have_key (pr_gr (loc_upb (fst p2) (snd p2))) (c_pair (fst p2) (snd p2)) = 0"
by auto
have S2: "(⋀ n' x'. ((n',x'), (fst p1, snd p1)) ∈ lex_p
⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0) ⟹
c_assoc_have_key (pr_gr (loc_upb (fst p1) (snd p1))) (c_pair (fst p1) (snd p1)) = 0"
by (rule wf_upb_step_0)
then have S3: "(⋀ n' x'. ((n',x'), p1) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0)
⟹ c_assoc_have_key (pr_gr (loc_upb (fst p1) (snd p1))) (c_pair (fst p1) (snd p1)) = 0" by auto
have S4: "⋀n' x'. ((n', x'), p1) ∈ lex_p ⟹ c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0"
proof -
fix n' x'
assume A4_1: "((n', x'), p1) ∈ lex_p"
let ?p2 = "(n', x')"
from A4_1 have S4_1: "(?p2, p1) ∈ lex_p" by auto
from S4_1 have "c_assoc_have_key (pr_gr (loc_upb (fst ?p2) (snd ?p2))) (c_pair (fst ?p2) (snd ?p2)) = 0"
by (rule A1)
then show "c_assoc_have_key (pr_gr (loc_upb n' x')) (c_pair n' x') = 0" by auto
qed
from S4 S3 show ?thesis by auto
qed
theorem loc_upb_main: "c_assoc_have_key (pr_gr (loc_upb n x)) (c_pair n x) = 0"
proof -
have loc_upb_lm: "⋀ p. c_assoc_have_key (pr_gr (loc_upb (fst p) (snd p))) (c_pair (fst p) (snd p)) = 0"
proof - fix p show "c_assoc_have_key (pr_gr (loc_upb (fst p) (snd p))) (c_pair (fst p) (snd p)) = 0"
proof -
have S1: "wf lex_p" by (auto simp add: lex_p_def)
from S1 wf_upb_step show ?thesis by (rule wf_induct_rule)
qed
qed
let ?p = "(n,x)"
have "c_assoc_have_key (pr_gr (loc_upb (fst ?p) (snd ?p))) (c_pair (fst ?p) (snd ?p)) = 0" by (rule loc_upb_lm)
thus ?thesis by simp
qed
theorem pr_gr_value: "c_assoc_value (pr_gr (loc_upb n x)) (c_pair n x) = univ_for_pr (c_pair n x)"
by (simp del: loc_upb.simps add: loc_upb_main pr_gr_1 c_is_sub_fun_lm_1)
theorem g_comp_is_pr: "g_comp ∈ PrimRec2"
proof -
from c_assoc_have_key_is_pr c_assoc_value_is_pr c_cons_is_pr have "(λ x y. g_comp x y) ∈ PrimRec2"
unfolding g_comp_def Let_def by prec
thus ?thesis by auto
qed
theorem g_pair_is_pr: "g_pair ∈ PrimRec2"
proof -
from c_assoc_have_key_is_pr c_assoc_value_is_pr c_cons_is_pr have "(λ x y. g_pair x y) ∈ PrimRec2"
unfolding g_pair_def Let_def by prec
thus ?thesis by auto
qed
theorem g_rec_is_pr: "g_rec ∈ PrimRec2"
proof -
from c_assoc_have_key_is_pr c_assoc_value_is_pr c_cons_is_pr have "(λ x y. g_rec x y) ∈ PrimRec2"
unfolding g_rec_def Let_def by prec
thus ?thesis by auto
qed
theorem g_step_is_pr: "g_step ∈ PrimRec2"
proof -
from g_comp_is_pr g_pair_is_pr g_rec_is_pr mod_is_pr c_assoc_have_key_is_pr c_assoc_value_is_pr c_cons_is_pr have
"(λ ls key. g_step ls key) ∈ PrimRec2" unfolding g_step_def Let_def by prec
thus ?thesis by auto
qed
theorem pr_gr_is_pr: "pr_gr ∈ PrimRec1"
proof -
have S1: "(λ x. pr_gr x) = PrimRecOp1 0 (λ x y. g_step y (c_fst x))" (is "_ = ?f")
proof
fix x
show "pr_gr x = ?f x" by (induct x) (simp add: pr_gr_at_0, simp add: pr_gr_at_Suc)
qed
have S2: "PrimRecOp1 0 (λ x y. g_step y (c_fst x)) ∈ PrimRec1"
proof (rule pr_rec1)
from g_step_is_pr show "(λx y. g_step y (c_fst x)) ∈ PrimRec2" by prec
qed
from S1 S2 show ?thesis by auto
qed
end