Theory All_Equations

subsubsection ‹Wrap-Up: Combining all equations›

theory All_Equations
  imports All_Equations_Invariance
 
begin

context register_machine
begin

definition all_equations_relation :: "polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial
  ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial list ⇒ polynomial list ⇒ polynomial list
  ⇒ relation" ("[ALLEQ] _ _ _ _ _ _ _ _ _ _") where
  "[ALLEQ] a q b c d e f r z s 
         ≡ LARY (λll. all_equations (ll!0!0) (ll!0!1) (ll!0!2) (ll!0!3) (ll!0!4) (ll!0!5) (ll!0!6)
                                     (nth (ll!1)) (nth (ll!2)) (nth (ll!3)))
                                     [[a, q, b, c, d, e, f], r, z, s]"

lemma all_equations_dioph: 
  fixes A f e d c b q :: polynomial
  fixes r z s :: "polynomial list"
  assumes "length r = n" "length z = n" "length s = Suc m"
  defines "DR ≡ [ALLEQ] A q b c d e f r z s"
  shows "is_dioph_rel DR"
proof - 
  define DS where "DS ≡ ([REG] A b q r z s) 
                     [∧] ([STATE] b e q z s)
                     [∧] ([MASK] c d e f r z)
                     [∧] ([CONST] b c d e f q)
                     [∧] [MISC] A c q"

  have "eval DS a = eval DR a" for a 
    unfolding DR_def DS_def all_equations_relation_def all_equations_def 
    unfolding register_equations_relation_def state_equations_relation_def 
      mask_equations_relation_def rm_constant_equations_def rm_miscellaneous_equations_def
    by (simp add: defs)

  moreover have "is_dioph_rel DS"
    unfolding DS_def apply (rule and_dioph)+
    apply (simp_all add: rm_constant_equations_dioph rm_miscellaneous_equations_dioph)
    using assms reg_dioph[of r z s A b q] state_equations_dioph[of s z b e q] 
          mask_equations_relation_dioph[of r z c d e f] by metis+

  ultimately show ?thesis using is_dioph_rel_def by auto
qed

definition rm_equations :: "nat ⇒ bool" where
  "rm_equations a ≡ ∃ q :: nat.
                      ∃ b c d e f :: nat. 
                      ∃ r z :: register ⇒ nat. 
                      ∃ s :: state ⇒ nat.
                      all_equations a q b c d e f r z s"

definition rm_equations_relation :: "polynomial ⇒ relation" ("[RM] _") where
  "[RM] A ≡ UNARY (rm_equations) A"

(* Correct assumptions: Need validity of p *)

lemma rm_dioph:
  fixes A
  fixes ic :: configuration
  defines "DR ≡ [RM] A"
  shows "is_dioph_rel DR"
proof - 
  define q b c d e f where "q ≡ Param 0" and
                           "b ≡ Param 1" and
                           "c ≡ Param 2" and
                           "d ≡ Param 3" and
                           "e ≡ Param 4" and
                           "f ≡ Param 5" 

  define r where "r ≡ map Param [6..<n + 6]"
  define z where "z ≡ map Param [n+6..<2*n + 6]"
  define s where "s ≡ map Param [2*n + 6..<2*n + 6 + m + 1]"

  define number_of_ex_vars where "number_of_ex_vars ≡ 2*n + 6 + m + 1" 

  define A' where "A' ≡ push_param A number_of_ex_vars"

  define DS where "DS ≡ [∃number_of_ex_vars] [ALLEQ] A' q b c d e f r z s"

  have "length r = n" and "length z = n" and "length s = Suc m"
    unfolding r_def z_def s_def by auto

  have "eval DS a = eval DR a" for a
  proof (rule)
    assume "eval DS a"
    then obtain ks where 
      ks_length: "number_of_ex_vars = length ks" and
      ALLEQ: "eval ([ALLEQ] A' q b c d e f r z s) (push_list a ks)" 
      unfolding DS_def by (auto simp add: defs)

    define q' b' c' d' e' f' where "q' ≡ ks!0" and
                                   "b' ≡ ks!1" and
                                   "c' ≡ ks!2" and
                                   "d' ≡ ks!3" and
                                   "e' ≡ ks!4" and
                                   "f' ≡ ks!5" 

    define r_list where "r_list ≡ (take n (drop 6 ks))"
    define z_list where "z_list ≡ (take n (drop (6+n) ks))"
    define s_list where "s_list ≡ (drop (6 + 2*n) ks)"
    
    define r' where "r' ≡ (!) r_list"
    define z' where "z' ≡ (!) z_list"
    define s' where "s' ≡ (!) s_list"

    have A: "peval A' (push_list a ks) = peval A a" for a 
      using ks_length push_push_simp unfolding A'_def by auto

    have q: "peval q (push_list a ks) = q'"
      unfolding q_def q'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto
    have b: "peval b (push_list a ks) = b'"
      unfolding b_def b'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto
    have c: "peval c (push_list a ks) = c'"
      unfolding c_def c'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto
    have d: "peval d (push_list a ks) = d'"
      unfolding d_def d'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto
    have e: "peval e (push_list a ks) = e'"
      unfolding e_def e'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto
    have f: "peval f (push_list a ks) = f'"
      unfolding f_def f'_def push_list_def using ks_length unfolding number_of_ex_vars_def by auto

    have r: "(!) (map (λP. peval P (push_list a ks)) r) x = (!) r_list x" if "x < n" for x 
      unfolding r_def r_list_def using that unfolding push_list_def 
      using ks_length unfolding number_of_ex_vars_def by auto

    have z: "(map (λP. peval P (push_list a ks)) z) ! x = z_list ! x" if "x < n" for x 
      unfolding z_def z_list_def using that unfolding push_list_def 
      using ks_length unfolding number_of_ex_vars_def by (auto simp add: add.commute)

    have s: "(map (λP. peval P (push_list a ks)) s) ! x = s_list ! x" if "x < Suc m" for x 
      unfolding s_def s_list_def using that unfolding push_list_def 
      using ks_length unfolding number_of_ex_vars_def by (auto simp add: add.commute)

    have "all_equations (peval A a) q' b' c' d' e' f' r' z' s'"
      using ALLEQ unfolding all_equations_relation_def apply (simp add: defs)
      unfolding A q b c d e f 
      using all_equations_invariance[of 
                                     "(!) (map (λP. peval P (push_list a ks)) r)" r' 
                                     "(!) (map (λP. peval P (push_list a ks)) z)" z' 
                                     "(!) (map (λP. peval P (push_list a ks)) s)" s' 
                                     "peval A a" q' b' c' d' e' f'] r z s
      using r'_def s'_def z'_def by fastforce 

    thus "eval DR a" 
      unfolding DR_def rm_equations_def rm_equations_relation_def by (auto simp: defs) (blast) 
  next
    assume "eval DR a"
    then obtain q' b' c' d' e' f' r' z' s' where 
         all_eq: "all_equations (peval A a) q' b' c' d' e' f' r' z' s'"
    unfolding DR_def rm_equations_def rm_equations_relation_def by (auto simp: defs)

    define r_list where "r_list ≡ map r' [0..<n]"
    define z_list where "z_list ≡ map z' [0..<n]"
    define s_list where "s_list ≡ map s' [0..<Suc m]"

    define ks where "ks ≡ [q', b', c', d', e', f'] @ r_list @ z_list @ s_list"

    have "number_of_ex_vars = length ks"
      unfolding number_of_ex_vars_def ks_def r_list_def z_list_def s_list_def by auto

    have A: "peval A' (push_list a ks) = peval A a" for a 
      unfolding A'_def  
      using push_push_simp[of A ks a] unfolding ‹number_of_ex_vars = length ks› by auto
        

    have q: "peval q (push_list a ks) = q'"
      unfolding q_def ks_def push_list_def by auto
    have b: "peval b (push_list a ks) = b'"
      unfolding b_def ks_def push_list_def by auto
    have c: "peval c (push_list a ks) = c'"
      unfolding c_def ks_def push_list_def by auto
    have d: "peval d (push_list a ks) = d'"
      unfolding d_def ks_def push_list_def by auto
    have e: "peval e (push_list a ks) = e'"
      unfolding e_def ks_def push_list_def by auto
    have f: "peval f (push_list a ks) = f'"
      unfolding f_def ks_def push_list_def by auto

    have r: "(map (λP. peval P (push_list a ks)) r) ! x = r' x" if "x < n" for x
      using that unfolding ks_def r_list_def r_def push_list_def 
      using nth_append[of "map r' [0..<n]" "z_list @ s_list"] by auto 

    have z: "(map (λP. peval P (push_list a ks)) z) ! x = z' x" if "x < n" for x
      using that unfolding ks_def z_list_def r_list_def z_def push_list_def apply simp
      using nth_append[of "map r' [0..<n] @ map z' [0..<n]" "s_list"]
      by (metis add_diff_cancel_left' gen_length_def length_code length_map length_upt 
          not_add_less1 nth_append nth_map_upt) 

    have s: "(map (λP. peval P (push_list a ks)) s) ! x = s' x" if "x < Suc m" for x
      using that unfolding ks_def r_list_def z_list_def s_list_def s_def push_list_def apply simp 
      using nth_append[of "map r' [0..<n] @ map z' [0..<n]" "map s' [0..<m] @ [s' m]" "(2 * n + x)"]
      by (auto) (metis (mono_tags, lifting) add_cancel_left_left diff_zero length_map length_upt 
          less_antisym nth_append nth_append_length nth_map_upt)

    have "eval ([ALLEQ] A' q b c d e f r z s) (push_list a ks)" 
      using all_eq unfolding all_equations_relation_def apply (simp add: defs)
      unfolding A q b c d e f
      using all_equations_invariance[of "(!) (map (λP. peval P (push_list a ks)) r)" r' 
                                        "(!) (map (λP. peval P (push_list a ks)) z)" z' 
                                        "(!) (map (λP. peval P (push_list a ks)) s)" s' 
                                        "peval A a" q' b' c' d' e' f'] r z s
      using r_list_def s_list_def z_list_def by auto

    thus "eval DS a"
      unfolding DS_def using ‹number_of_ex_vars = length ks› by (auto) 
  qed

  moreover have "is_dioph_rel DS"
    unfolding DS_def
    using all_equations_dioph ‹length r = n› ‹length z = n› ‹length s = Suc m› assms  
    by (auto simp: dioph)
    
  ultimately show ?thesis 
    using is_dioph_rel_def by auto

qed

end

end