Theory All_State_Equations

subsubsection ‹Wrap-up: Combining all state equations›

theory All_State_Equations imports State_Unique_Equations State_d_Equation
                                                                 
begin

text ‹The remaining equations:›

context rm_eq_fixes
begin

  text ‹Equation 4.27›
  definition state_m :: "bool" where
    "state_m ≡ s m = b ^ q"

  text ‹Equation not in the book›
  definition state_partial_sum_mask :: "bool" where
    "state_partial_sum_mask ≡ ∀M≤m. (∑k≤M. s k) ≼ e"

  text ‹Wrapping it all up›

  definition state_equations :: "bool" where
    "state_equations ≡ state_relations_from_recursion ∧ state_unique_equations 
                     ∧ state_partial_sum_mask ∧ state_m"

end

context register_machine
begin

lemma state_m_dioph:
  fixes b q :: polynomial
  fixes s :: "polynomial list"
  assumes "length s = Suc m"
  defines "DR ≡ LARY (λll. rm_eq_fixes.state_m p (ll!0!0) (ll!0!1) (nth (ll!1))) [[b, q], s]"
  shows "is_dioph_rel DR"
proof - 
  define DS where "DS ≡ [(s!m) = b ^ q]"

  have "eval DS a = eval DR a" for a 
    using DS_def DR_def rm_eq_fixes.state_m_def rm_eq_fixes_def local.register_machine_axioms 
    using assms by (simp add: defs)

  moreover have "is_dioph_rel DS"
    unfolding DS_def by (auto simp: dioph)

  ultimately show ?thesis using is_dioph_rel_def by auto
qed

lemma state_partial_sum_mask_dioph:
  fixes e :: polynomial
  fixes s :: "polynomial list"
  assumes "length s = Suc m"
  defines "DR ≡ LARY (λll. rm_eq_fixes.state_partial_sum_mask p (ll!0!0) (nth (ll!1))) [[e], s]"
  shows "is_dioph_rel DR"
proof - 

  define partial_sum_mask where "partial_sum_mask ≡ (λm. (sum_polynomial (nth s) [0..<Suc m] [≼] e))"
  define DS where "DS ≡ [∀<Suc m] partial_sum_mask"

  have "eval DS a = eval DR a" for a 
  proof - 

    have aux: "((∑j = 0..<k. peval (s ! (([0..<Suc k]) ! j)) a) 
                        + peval (s ! (([0..<Suc k]) ! k)) a ≼ peval e a) 
             = ((∑j = 0..<k. peval (s ! j) a) 
                        + peval (s ! k) a ≼ peval e a)" for k
    proof -
      have "[0..<Suc k] ! k = 0 + k"
        using nth_upt[of 0 k "Suc k"] by simp

      moreover have "(∑j = 0..<k. peval (s ! (([0..<Suc k]) ! j)) a) 
                   = (∑j = 0..<k. peval (s ! j) a)" 
        apply (rule sum.cong, simp) using nth_upt[of 0 _ "Suc k"] 
        by (metis Suc_lessD add_cancel_right_left ex_nat_less_eq not_less_eq)
      ultimately show ?thesis 
        by auto 
    qed

    have aux2: "(∑j = 0..<Suc k. peval (s ! j) a) =
                (sum ((!) (map (λP. peval P a) s)) {..k})" if "k≤m" for k
      apply (rule sum.cong, auto) 
      by (metis assms(1) dual_order.strict_trans le_imp_less_Suc nth_map 
          order.not_eq_order_implies_strict that)

    have "eval DS a = (∀k<Suc m.
                      (∑j = 0..<k. peval (s ! j) a) + peval (s ! k) a ≼ peval e a)"
      unfolding DS_def partial_sum_mask_def using aux
      by (simp add: defs ‹length s = Suc m› sum_polynomial_eval)

    also have "... = (∀k≤m.
                     (∑j = 0..<k. peval (s ! j) a) + peval (s ! k) a ≼ peval e a)"
      by (simp add: less_Suc_eq_le)

    finally show ?thesis using rm_eq_fixes_def local.register_machine_axioms DR_def 
      rm_eq_fixes.state_partial_sum_mask_def aux2 by (simp add: defs)
  qed

  moreover have "is_dioph_rel DS"
    unfolding DS_def partial_sum_mask_def by (auto simp: dioph)

  ultimately show ?thesis using is_dioph_rel_def by auto
qed

definition state_equations_relation :: "polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial list
    ⇒ polynomial list ⇒ relation" ("[STATE] _ _ _ _ _")where
  "[STATE] b e q z s ≡ LARY (λll. rm_eq_fixes.state_equations p (ll!0!0) (ll!0!1) (ll!0!2) 
                                                          (nth (ll!1)) (nth (ll!2))) 
                        [[b, e, q], z, s]"

lemma state_equations_dioph:
  fixes b e q :: polynomial
  fixes s z :: "polynomial list"
  assumes "length s = Suc m" "length z = n"
  defines "DR ≡ [STATE] b e q z s"
  shows "is_dioph_rel DR"
proof - 

  define DS where 
    "DS ≡  (LARY (λll. rm_eq_fixes.state_relations_from_recursion p (ll!0!0) (ll!0!1)
                 (nth (ll!1)) (nth (ll!2))) [[b, e], z, s])
       [∧] (LARY (λll. rm_eq_fixes.state_unique_equations p (ll!0!0) (ll!0!1) (ll!0!2) (nth (ll!1))) 
                 [[b, e, q], s])
       [∧] (LARY (λll. rm_eq_fixes.state_partial_sum_mask p (ll!0!0) (nth (ll!1))) [[e], s])
       [∧] (LARY (λll. rm_eq_fixes.state_m p (ll!0!0) (ll!0!1) (nth (ll!1))) [[b, q], s])"

  have "eval DS a = eval DR a" for a 
    using DS_def DR_def rm_eq_fixes.state_equations_def 
    state_equations_relation_def rm_eq_fixes_def local.register_machine_axioms by (auto simp: defs)

  moreover have "is_dioph_rel DS"
    unfolding DS_def using assms state_relations_from_recursion_dioph[of z s] state_m_dioph[of s] 
    state_partial_sum_mask_dioph state_unique_equations_dioph and_dioph 
    by (auto simp: dioph)

  ultimately show ?thesis using is_dioph_rel_def by auto
qed

end

end