Theory State_0_Equation
subsubsection ‹State 0 equation›
theory State_0_Equation imports "../Register_Machine/MultipleStepState"
RM_Sums_Diophantine "../Diophantine/Binary_And"
begin
context rm_eq_fixes
begin
text ‹Equation 4.24›
definition state_0 :: "bool" where
"state_0 ≡ s 0 = 1 + b*∑S+ p 0 s + b*∑S- p 0 (λk. s k && z (modifies (p!k)))
+ b*∑S0 p 0 (λk. s k && (e - z (modifies (p!k))))"
end
context register_machine
begin
no_notation ppolynomial.Sum (infixl "❙+" 65)
no_notation ppolynomial.NatDiff (infixl "❙-" 65)
no_notation ppolynomial.Prod (infixl "❙*" 70)
lemma state_0_dioph:
fixes b e :: polynomial
fixes z s :: "polynomial list"
assumes "length z = n" "length s = Suc m"
defines "DR ≡ LARY (λll. rm_eq_fixes.state_0 p (ll!0!0) (ll!0!1)
(nth (ll!1)) (nth (ll!2))) [[b, e], z, s]"
shows "is_dioph_rel DR"
proof -
let ?N = "2"
define b' e' z' s' where pushed_def: "b' = push_param b ?N"
"e' = push_param e ?N"
"z' = map (λx. push_param x ?N) z"
"s' = map (λx. push_param x ?N) s"
define z0 z1 where z_def: "z0 ≡ map (λi. z' ! modifies (p!i)) [0..<length p]"
"z1 ≡ map (λi. e' [-] z' ! modifies (p!i)) [0..<length p]"
define param_0_is_sum_sub_nzero_term where
"param_0_is_sum_sub_nzero_term ≡ [Param 0 = ∑S- 0 (s' && z0)]"
define param_1_is_sum_sub_zero_term where
"param_1_is_sum_sub_zero_term ≡ [Param 1 = ∑S0 0 (s' && z1)]"
define step_relation where
"step_relation ≡ (s'!0 [=] ❙1 [+] b' [*] ([∑S+] p 0 (nth s'))
[+] b' [*] Param 0 [+] b' [*] Param 1)"
define DS where "DS ≡ [∃?N] step_relation
[∧] param_0_is_sum_sub_nzero_term
[∧] param_1_is_sum_sub_zero_term"
have "p ≠ []" using p_nonempty by auto
have ps_lengths: "length p = length s"
using ‹length s = Suc m› m_def ‹p ≠ []› by auto
have s_len: "length s > 0"
using ps_lengths ‹p ≠ []› by auto
have p_len: "length p > 0"
using ps_lengths s_len by auto
have p_len2: "length p = Suc m"
using ps_lengths ‹length s = Suc m› by auto
have len_s': "length s' = Suc m"
unfolding pushed_def using ‹length s = Suc m› by auto
have "length z0 = Suc m"
unfolding z_def ps_lengths ‹length s = Suc m› by simp
have "length z1 = Suc m"
unfolding z_def ps_lengths ‹length s = Suc m› by simp
have modifies_le_n: "k < length p ⟹ modifies (p!k) < n" for k
using modifies_yields_valid_register ‹length z = n› by auto
have "eval DS a = eval DR a" for a
proof -
have b'_unfold: "peval b' (push_list a ks) = peval b a" if "length ks = 2" for ks
using push_push_simp unfolding pushed_def using that by metis
have s'_0_unfold: "peval (s' ! 0) (push_list a ks) = peval (s ! 0) a" if "length ks = 2" for ks
unfolding pushed_def using push_push_map_i[of ks 2 0 s a] that unfolding list_eval_def
‹length s > 0› using s_len by auto
have sum_nzero_unfold:
"eval [polynomial.Param 0 = ∑S- 0 (s' && z0)] (push_list a ks)
= (peval (polynomial.Param 0) (push_list a ks)
= ∑S- p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)))" for ks
using sum_rsub_nzero_of_bit_and_eval[of s' z0 "Param 0" 0 "push_list a ks"]
‹length p > 0› ‹length s' = Suc m› ‹length z0 = Suc m› by auto
have sum_zero_unfold:
"eval [polynomial.Param 1 = ∑S0 0 (s' && z1)] (push_list a ks)
= (peval (polynomial.Param 1) (push_list a ks)
= ∑S0 p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks)))" for ks
using sum_rsub_zero_of_bit_and_eval[of s' z1 "Param 1" 0 "push_list a ks"]
‹length p > 0› ‹length s' = Suc m› ‹length z1 = Suc m› by auto
have param_0_unfold: "peval (Param 0) (push_list a ks) = ks ! 0" if "length ks = 2" for ks
unfolding push_list_def using that by auto
have param_1_unfold: "peval (Param 1) (push_list a ks) = ks ! 1" if "length ks = 2" for ks
unfolding push_list_def using that by auto
have sum_sadd_unfold:
"peval ([∑S+] p 0 ((!) s')) (push_list a ks) = ∑S+ p 0 (λx. peval (s ! x) a)"
if "length ks = 2" for ks
using sum_sadd_polynomial_eval ‹length p > 0› apply auto
apply (rule sum_sadd_cong, auto)
unfolding pushed_def using push_push_map_i[of ks 2 _ s a] that
unfolding ‹length p = length s› list_eval_def
by (smt One_nat_def assms le_imp_less_Suc m_def nth_map p_len2)
have z0_unfold:
"peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)
= peval (s ! k) a && peval (z ! modifies (p ! k)) a"
if "length ks = 2" and "k < length p" for k ks
proof -
have map: "map (λi. z' ! modifies (p ! i)) [0..<length p] ! k
= z' ! modifies (p ! k)"
unfolding z_def using nth_map[of k "[0..<length p]" "λi. z' ! modifies (p ! i)"]
using ‹k < length p› by auto
have s: "peval (map (λx. push_param x 2) s ! k) (push_list a ks) = peval (s ! k) a"
using push_push_map_i[of ks 2 k s] that nth_map[of k s]
unfolding ‹length s = Suc m› ‹length p = Suc m› list_eval_def by auto
have z: "peval (map (λx. push_param x 2) z ! modifies (p ! k)) (push_list a ks)
= peval (z ! modifies (p ! k)) a"
using push_push_map_i[of ks 2 "modifies (p!k)" z a] modifies_le_n[of k] that nth_map[of _ z]
unfolding ‹length z = n› list_eval_def by auto
show ?thesis
unfolding z_def map unfolding pushed_def s z by auto
qed
have z1_unfold:
"peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks)
= peval (s ! k) a && (peval e a - peval (z ! modifies (p ! k)) a)"
if "length ks = 2" and "k < length p" for k ks
proof -
have map:
"map (λi. e' [-] (z' ! (modifies (p ! i)))) [0..<length p] ! k
= e' [-] (z' ! modifies (p ! k))"
using nth_map[of k "[0..<length p]" "λi. z' ! modifies (p ! i)"]
using ‹k < length p› by auto
have s: "peval (map (λx. push_param x 2) s ! k) (push_list a ks) = peval (s ! k) a"
using push_push_map_i[of ks 2 k s] that nth_map[of k s]
unfolding ‹length s = Suc m› ‹length p = Suc m› list_eval_def by auto
have z: "peval (push_param e 2) (push_list a ks)
- peval (map (λx. push_param x 2) z ! modifies (p ! k)) (push_list a ks)
= peval e a - peval (z ! (modifies (p!k))) a"
using push_push_simp[of e ks a] unfolding ‹length ks = 2› apply simp
using push_push_map_i[of ks 2 "modifies (p!k)" z a] modifies_le_n[of k] that
nth_map[of "modifies (p!k)" z "(λx. peval x a)"]
unfolding ‹length z = n› list_eval_def by auto
show ?thesis
unfolding z_def map unfolding pushed_def s using z by auto
qed
have z0sum_unfold:
"(∑S- p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)))
=(∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a))"
if "length ks = 2" for ks
apply (rule sum_ssub_nzero_cong) using z0_unfold[of ks] that
by (metis ‹length s = Suc m› le_imp_less_Suc m_def ps_lengths)
have z1sum_unfold:
"(∑S0 p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks)))
=(∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a))"
if "length ks = 2" for ks
apply (rule sum_ssub_zero_cong) using z1_unfold[of ks] that
by (metis ‹length s = Suc m› le_imp_less_Suc m_def ps_lengths)
have sum_sadd_map: "∑S+ p 0 ((!) (map (λP. peval P a) s)) = ∑S+ p 0 (λx. peval (s ! x) a)"
apply (rule sum_sadd_cong, auto)
using nth_map[of _ s "(λP. peval P a)"] m_def ‹length s = Suc m› by auto
have sum_ssub_nzero_map:
"(∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a))
= (∑S- p 0 (λk. map (λP. peval P a) s ! k && map (λP. peval P a) z ! modifies (p ! k)))"
proof -
have 1: "peval (s ! k) a && peval (z ! modifies (p ! k)) a =
map (λP. peval P a) s ! k && map (λP. peval P a) z ! modifies (p ! k) "
if "k < length p" for k
proof -
have "peval (s ! k) a = map (λP. peval P a) s ! k"
using nth_map that ps_lengths by auto
moreover have "peval (z ! modifies (p ! k)) a
= map (λP. peval P a) z ! modifies (p ! k) "
using nth_map[of "modifies (p!k)" z "(λP. peval P a)"] modifies_le_n[of k] that
using ‹length z = n› by auto
ultimately show ?thesis by auto
qed
show ?thesis apply (rule sum_ssub_nzero_cong, auto)
using 1 by (metis Suc_le_mono Suc_pred less_eq_Suc_le p_len)
qed
have sum_ssub_zero_map:
"(∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a))
= (∑S0 p 0 (λk. map (λP. peval P a) s ! k && peval e a
- map (λP. peval P a) z ! modifies (p ! k)))"
proof -
have 1: "peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a =
map (λP. peval P a) s ! k && peval e a - map (λP. peval P a) z ! modifies (p ! k) "
if "k < length p" for k
proof -
have "peval (s ! k) a = map (λP. peval P a) s ! k"
using nth_map that ps_lengths by auto
moreover have "peval (z ! modifies (p ! k)) a
= map (λP. peval P a) z ! modifies (p ! k) "
using nth_map[of "modifies (p!k)" z "(λP. peval P a)"] modifies_le_n[of k] that
using ‹length z = n› by auto
ultimately show ?thesis by auto
qed
show ?thesis apply (rule sum_ssub_zero_cong, auto)
using 1 by (metis Suc_le_mono Suc_pred less_eq_Suc_le p_len)
qed
have "eval DS a =
(∃ks. length ks = 2 ∧
eval (s' ! 0 [=] ❙1 [+] b' [*] ([∑S+] p 0 (!) s') [+] b' [*] Param 0
[+] b' [*] Param (Suc 0)) (push_list a ks)
∧ eval [polynomial.Param 0 = ∑S- 0 (s' && z0)] (push_list a ks)
∧ eval [polynomial.Param 1 = ∑S0 0 (s' && z1)] (push_list a ks))"
unfolding DS_def step_relation_def param_0_is_sum_sub_nzero_term_def
param_1_is_sum_sub_zero_term_def by (simp add: defs)
also have "... = (∃ks. length ks = 2 ∧
peval (s' ! 0) (push_list a ks) =
Suc (peval b' (push_list a ks) * peval ([∑S+] p 0 ((!) s')) (push_list a ks) +
peval b' (push_list a ks) * push_list a ks 0 +
peval b' (push_list a ks) * push_list a ks (Suc 0))
∧ (peval (Param 0) (push_list a ks)
= ∑S- p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)))
∧ (peval (Param 1) (push_list a ks)
= ∑S0 p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks))))"
unfolding sum_nzero_unfold sum_zero_unfold by (simp add: defs )
also have "... = (∃ks. length ks = 2 ∧
peval (s ! 0) a =
Suc (peval b a * peval ([∑S+] p 0 ((!) s')) (push_list a ks) +
peval b a * push_list a ks 0 +
peval b a * push_list a ks (Suc 0))
∧ (ks!0
= ∑S- p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)))
∧ (ks!1
= ∑S0 p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks))))"
using b'_unfold s'_0_unfold param_0_unfold param_1_unfold by auto
also have "... = (∃ks. length ks = 2 ∧
peval (s ! 0) a =
Suc (peval b a * ∑S+ p 0 (λx. peval (s ! x) a) +
peval b a * (ks!0) + peval b a * (ks!1))
∧ (ks!0 = ∑S- p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z0 ! k) (push_list a ks)))
∧ (ks!1 = ∑S0 p 0 (λk. peval (s' ! k) (push_list a ks) && peval (z1 ! k) (push_list a ks))))"
using push_list_def sum_sadd_unfold by auto
also have "... = (∃ks. length ks = 2 ∧
peval (s ! 0) a = Suc (peval b a * ∑S+ p 0 (λx. peval (s ! x) a)
+ peval b a * (ks!0) + peval b a * (ks!1))
∧ (ks!0 = ∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a))
∧ (ks!1 = ∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a)))"
using z0sum_unfold z1sum_unfold by auto
also have "... = (∃ks. length ks = 2 ∧
peval (s ! 0) a
= Suc (peval b a * ∑S+ p 0 (λx. peval (s ! x) a)
+ peval b a * ∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a)
+ peval b a * ∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a))
∧ (ks!0 = ∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a))
∧ (ks!1 = ∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a)))"
by auto
also have "... = (peval (s ! 0) a
= Suc (peval b a * ∑S+ p 0 (λx. peval (s ! x) a)
+ peval b a * ∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a)
+ peval b a * ∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a)))"
apply auto
apply (rule exI[of _ "[(∑S- p 0 (λk. peval (s ! k) a && peval (z ! modifies (p ! k)) a)),
∑S0 p 0 (λk. peval (s ! k) a && peval e a - peval (z ! modifies (p ! k)) a) ]"])
by auto
also have "... = (map (λP. peval P a) s ! 0 =
Suc (peval b a * ∑S+ p 0 ((!) (map (λP. peval P a) s)) +
peval b a * ∑S- p 0 (λk. map (λP. peval P a) s ! k
&& map (λP. peval P a) z ! modifies (p ! k)) +
peval b a *
∑S0 p 0 (λk. map (λP. peval P a) s ! k && peval e a
- map (λP. peval P a) z ! modifies (p ! k)) ))"
using nth_map[of _ _ "(λP. peval P a)"] ‹length s > 0›
using sum_ssub_zero_map sum_sadd_map sum_ssub_nzero_map by auto
finally show ?thesis unfolding DR_def using rm_eq_fixes_def local.register_machine_axioms
rm_eq_fixes.state_0_def by (simp add: defs)
qed
moreover have "is_dioph_rel DS"
unfolding DS_def param_1_is_sum_sub_zero_term_def param_0_is_sum_sub_nzero_term_def
step_relation_def by (auto simp add: dioph)
ultimately show ?thesis
by (simp add: is_dioph_rel_def)
qed
end
end