Theory Constants_Equations
subsubsection ‹Equations for arithmetization constants›
theory Constants_Equations imports Equation_Setup "../Register_Machine/MachineMasking"
"../Diophantine/Binary_And"
begin
context rm_eq_fixes
begin
text ‹Equation 4.14›
definition constant_b :: "bool" where
"constant_b ≡ b = B c"
text ‹Equation 4.16›
definition constant_d :: "bool" where
"constant_d ≡ d = D q c b"
text ‹Equation 4.18›
definition constant_e :: "bool" where
"constant_e ≡ e = E q b"
text ‹Equation 4.21›
definition constant_f :: "bool" where
"constant_f ≡ f = F q c b"
text ‹Equation not in the book›
definition c_gt_0 :: "bool" where
"c_gt_0 ≡ c > 0"
text ‹Equation 4.26›
definition a_bound :: "bool" where
"a_bound ≡ a < 2 ^ c"
text ‹Equation not in the book›
definition q_gt_0 :: "bool" where
"q_gt_0 ≡ q > 0"
definition constants_equations :: "bool" where
"constants_equations ≡ constant_b ∧ constant_d ∧ constant_e ∧ constant_f"
definition miscellaneous_equations :: "bool" where
"miscellaneous_equations ≡ c_gt_0 ∧ a_bound ∧ q_gt_0 "
end
context register_machine
begin
definition rm_constant_equations ::
"polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ relation"
("[CONST] _ _ _ _ _ _") where
"[CONST] b c d e f q ≡ NARY (λl. rm_eq_fixes.constants_equations
(l!0) (l!1) (l!2) (l!3) (l!4) (l!5)) [b, c, d, e, f, q]"
definition rm_miscellaneous_equations ::
"polynomial ⇒ polynomial ⇒ polynomial ⇒ relation"
("[MISC] _ _ _") where
"[MISC] c a q ≡ NARY (λl. rm_eq_fixes.miscellaneous_equations
(l!0) (l!1) (l!2)) [c, a, q]"
lemma rm_constant_equations_dioph:
fixes b c d e f q
defines "DR ≡ [CONST] b c d e f q"
shows "is_dioph_rel DR"
proof-
have fx: "rm_eq_fixes p n"
using rm_eq_fixes_def local.register_machine_axioms by auto
define b' c' d' e' f' q' where pushed_defs:
"b' = (push_param b 2)" "c' = (push_param c 2)" "d' = (push_param d 2)"
"e' = (push_param e 2)" "f' = (push_param f 2)" "q' = (push_param q 2)"
define s t where params_def: "s = Param 0" "t = Param 1"
define DS1 where "DS1 ≡ [b' = Const 2 ^ (c' [+] ❙1)] [∧]
[s = Const 2 ^ c'] [∧] [t = b' ^ (q' [+] ❙1)] [∧]
(b' [-] ❙1) [*] d' [=] (s [-] ❙1) [*] (t [-] ❙1)"
define DS2 where "DS2 ≡ (b' [-] ❙1) [*] e' [=] t [-] ❙1 [∧]
(b' [-] ❙1) [*] f' [=] s [*] (t [-] ❙1)"
define DS where "DS ≡ [∃2] DS1 [∧] DS2"
have "eval DS a = eval DR a" for a
unfolding DR_def DS_def DS1_def DS2_def rm_constant_equations_def defs
apply (auto simp add: fx rm_eq_fixes.constants_equations_def[of p n])
unfolding pushed_defs params_def push_push apply (auto simp add: push_list_eval)
apply (auto simp add: fx rm_eq_fixes.constant_b_def[of p n] B_def
rm_eq_fixes.constant_d_def[of p n] rm_eq_fixes.constant_e_def[of p n]
rm_eq_fixes.constant_f_def[of p n])
using d_geom_series[of "2 * 2 ^ peval c a" "peval c a" "(peval q a)" " peval d a"]
using e_geom_series[of "(2 * 2 ^ peval c a)" "peval q a" "peval e a"]
using f_geom_series[of "2 * 2 ^ peval c a" "peval c a" "(peval q a)" " peval f a"]
apply (auto)
apply (rule exI[of _ "[2 ^ peval c a, peval b a * peval b a ^ peval q a]"])
using push_list_def push_push by auto
moreover have "is_dioph_rel DS" unfolding DS_def DS1_def DS2_def by (simp add: dioph)
ultimately show ?thesis
by (simp add: is_dioph_rel_def)
qed
lemma rm_miscellaneous_equations_dioph:
fixes c a q
defines "DR ≡ [MISC] a c q"
shows "is_dioph_rel DR"
proof-
define c' a' q' where pushed_defs:
"c' == (push_param c 1)" "a' == (push_param a 1)" "q' = (push_param q 1)"
define DS where "DS ≡ [∃] c' [>] ❙0
[∧] [(Param 0) = (Const 2) ^ c'] [∧] a'[<] Param 0
[∧] q' [>] ❙0"
have "eval DS a = eval DR a" for a unfolding DS_def defs DR_def
using rm_miscellaneous_equations_def
rm_eq_fixes.miscellaneous_equations_def rm_eq_fixes.c_gt_0_def rm_eq_fixes.a_bound_def
rm_eq_fixes.q_gt_0_def rm_eq_fixes_def local.register_machine_axioms apply auto
unfolding pushed_defs push_push1
apply (auto, rule exI[of _ "2 ^ peval c a"]) unfolding push0 by auto
moreover have "is_dioph_rel DS" unfolding DS_def by (simp add: dioph)
ultimately show ?thesis
by (simp add: is_dioph_rel_def)
qed
end
end