Theory Diophantine_Relations

subsection ‹Diophantine Relations and Predicates›

theory Diophantine_Relations
  imports Assignments
begin           

datatype relation =
  NARY "nat list ⇒ bool" "polynomial list"
    | AND relation relation (infixl ‹[∧]› 35)
    | OR  relation relation (infixl ‹[∨]› 30)
    | EXIST_LIST nat relation (‹[∃_] _› 10)

fun eval :: "relation ⇒ assignment ⇒ bool" where
  "eval (NARY R PL) a = R (map (λP. peval P a) PL)"
    | "eval (AND D1 D2) a = (eval D1 a ∧ eval D2 a)"
    | "eval (OR D1 D2) a = (eval D1 a ∨ eval D2 a)"
    | "eval ([∃n] D) a = (∃ks::nat list. n = length ks ∧ eval D (push_list a ks))"

definition is_dioph_rel :: "relation ⇒ bool" where
  "is_dioph_rel DR = (∃P⇩1 P⇩2::ppolynomial. ∀a. (eval DR a) ⟷ (∃v. ppeval P⇩1 a v = ppeval P⇩2 a v))"


definition UNARY :: "(nat ⇒ bool) ⇒ polynomial ⇒ relation" where
  "UNARY R P = NARY (λl. R (l!0)) [P]"

lemma unary_eval: "eval (UNARY R P) a = R (peval P a)"
  unfolding UNARY_def by simp

definition BINARY :: "(nat ⇒ nat ⇒ bool) ⇒ polynomial ⇒ polynomial ⇒ relation" where
  "BINARY R P⇩1 P⇩2 = NARY (λl. R (l!0) (l!1)) [P⇩1, P⇩2]"

lemma binary_eval: "eval (BINARY R P⇩1 P⇩2) a = R (peval P⇩1 a) (peval P⇩2 a)"
  unfolding BINARY_def by simp

definition TERNARY :: "(nat ⇒ nat ⇒ nat ⇒ bool)
                        ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ relation" where
  "TERNARY R P⇩1 P⇩2 P⇩3 = NARY (λl. R (l!0) (l!1) (l!2)) [P⇩1, P⇩2, P⇩3]"

lemma ternary_eval: "eval (TERNARY R P⇩1 P⇩2 P⇩3) a = R (peval P⇩1 a) (peval P⇩2 a) (peval P⇩3 a)"
  unfolding TERNARY_def by simp

definition QUATERNARY :: "(nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool)
                        ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ polynomial ⇒ relation" where
  "QUATERNARY R P⇩1 P⇩2 P⇩3 P⇩4 = NARY (λl. R (l!0) (l!1) (l!2) (l!3)) [P⇩1, P⇩2, P⇩3, P⇩4]"

definition EXIST :: "relation ⇒ relation" (‹[∃] _› 10) where
  "([∃] D) = ([∃1] D)"

definition TRUE where "TRUE = UNARY ((=) 0) (Const 0)"

text ‹Bounded constant all quantifier (i.e. recursive conjunction)›
fun ALLC_LIST :: "nat list ⇒ (nat ⇒ relation) ⇒ relation" (‹[∀ in _] _›) where
  "[∀ in []] DF = TRUE" |
  "[∀ in (l # ls)] DF = (DF l [∧] [∀ in ls] DF)"

lemma ALLC_LIST_eval_list_all: "eval ([∀ in L] DF) a = list_all (λl. eval (DF l) a) L"
  by (induction L, auto simp: TRUE_def UNARY_def)

lemma ALLC_LIST_eval:  "eval ([∀ in L] DF) a = (∀k<length L. eval (DF (L!k)) a)"
  by (simp add: ALLC_LIST_eval_list_all list_all_length)

definition ALLC :: "nat ⇒ (nat ⇒ relation) ⇒ relation" (‹[∀<_] _›) where
  "[∀<n] D ≡ [∀ in [0..<n]] D"

lemma ALLC_eval: "eval ([∀<n] DF) a = (∀k<n. eval (DF k) a)"
  unfolding ALLC_def by (simp add: ALLC_LIST_eval)

fun concat :: "'a list list ⇒ 'a list" where
  "concat [] = []" |
  "concat (l # ls) = l @ concat ls"

fun splits :: "'a list ⇒ nat list ⇒ 'a list list" where
  "splits L [] = []" |
  "splits L (n # ns) = (take n L) # (splits (drop n L) ns)"

lemma split_concat:
  "splits (map f (concat pls)) (map length pls) = map (map f) pls"
  by (induction pls, auto)

definition LARY :: "(nat list list ⇒ bool) ⇒ (polynomial list list) ⇒ relation" where
  "LARY R PLL = NARY (λl. R (splits l (map length PLL))) (concat PLL)"

lemma LARY_eval:
  fixes PLL :: "polynomial list list"
  shows "eval (LARY R PLL) a = R (map (map (λP. peval P a)) PLL)"
  unfolding LARY_def apply (induction PLL, simp)
  subgoal for pl pls by (induction pl, auto simp: split_concat)
  done

lemma or_dioph:
  assumes "is_dioph_rel A" and "is_dioph_rel B"
  shows "is_dioph_rel (A [∨] B)"
proof -
  from assms obtain PA1 PA2 where PA: "∀a. (eval A a) ⟷ (∃v. ppeval PA1 a v = ppeval PA2 a v)"
    by (auto simp: is_dioph_rel_def)
  from assms obtain PB1 PB2 where PB: "∀a. (eval B a) ⟷ (∃v. ppeval PB1 a v = ppeval PB2 a v)"
    by (auto simp: is_dioph_rel_def)

  (* OR means (A1 - A2) * (B1 - B2) = 0
     Rewrite as A1*B1 + A2*B2 = A1*B2 + A2*B1 to eliminate subtraction. *)
  show ?thesis
    unfolding is_dioph_rel_def
    apply (rule exI[of _ "PA1 ❙* PB1 ❙+ PA2 ❙* PB2"])
    apply (rule exI[of _ "PA1 ❙* PB2 ❙+ PA2 ❙* PB1"])
    using PA PB by (auto) (metis crossproduct_eq add.commute)+
    (* For each subgoal, a different fact is unused. The warning is due to 'metis+' being used. *)
qed

lemma exists_disjoint_vars:
  fixes Q1 Q2 :: ppolynomial
  fixes A :: relation
  assumes "is_dioph_rel A"
  shows "∃P1 P2. disjoint_var (P1 ❙+ P2) (Q1 ❙+ Q2)
                ∧ (∀a. eval A a ⟷ (∃v. ppeval P1 a v = ppeval P2 a v))"
proof -
  obtain P1 P2 where p_defs: "∀a. eval A a ⟷ (∃v. ppeval P1 a v = ppeval P2 a v)"
    using assms is_dioph_rel_def by auto

  define n::nat where "n ≡ Max (var_set (Q1 ❙+ Q2))"

  define P1' P2' where p'_defs: "P1' ≡ push_var P1 (Suc n)" "P2' ≡ push_var P2 (Suc n)" 

  have "disjoint_var (P1' ❙+ P2') (Q1 ❙+ Q2)"
  proof -
    have "finite (var_set (Q1 ❙+ Q2))"
      apply (induction Q1, auto)
      by (induction Q2, auto)+

    hence "∀x ∈ var_set (Q1 ❙+ Q2). x ≤ n"
      unfolding n_def using Max.coboundedI by blast

    moreover have "∀x ∈ var_set (P1' ❙+ P2'). x > n"
      unfolding p'_defs using push_var_bound by auto

    ultimately show ?thesis
      unfolding disjoint_var_def by fastforce
  qed

  moreover have "∀a. eval A a ⟷ (∃v. ppeval P1' a v = ppeval P2' a v)"
    unfolding p'_defs apply (auto simp add: p_defs push_var_pull_assignment pull_assignment_def)
    subgoal for a v by (rule exI[of _ "λi. v (i - Suc n)"]) auto
    done

  ultimately show ?thesis
    by auto
qed

(* Combine the two results to show that AND has a diophantine representation *)
lemma and_dioph:
  assumes "is_dioph_rel A" and "is_dioph_rel B"
  shows "is_dioph_rel (A [∧] B)"
proof -
  from assms(1) obtain PA1 PA2 where PA: "∀a. (eval A a) ⟷ (∃v. ppeval PA1 a v = ppeval PA2 a v)"
    by (auto simp: is_dioph_rel_def)
  from assms(2) obtain PB1 PB2 where disj: "disjoint_var (PB1 ❙+ PB2) (PA1 ❙+ PA2)"
                                   and PB: "(∀a. eval B a ⟷ (∃v. ppeval PB1 a v = ppeval PB2 a v))"
    using exists_disjoint_vars[of B] by blast

  from disjoint_var_unifies have unified: "∀a. (eval (A [∧] B) a)
                        ⟷ (∃v. ppeval PA1 a v = ppeval PA2 a v ∧ ppeval PB1 a v = ppeval PB2 a v)"
    using PA PB disj disjoint_var_sym by simp blast

  (* AND means (A1 - A2)^2 + (B1 - B2)^2 = 0
     Rewrite as A1^2 + A2^2 + B1^2 + B2^2 = 2*A1*A2 + 2*B1*B2 to eliminate subtraction. *)
  have h0: "p1 = p2 ⟷ p1^2 + p2^2 = 2*p1*p2" for p1 p2 :: nat
    apply (auto simp: algebra_simps power2_eq_square)
    using crossproduct_eq by fastforce

  have "p1 = p2 ∧ q1 = q2 ⟷ p1^2 + p2^2 + q1^2 + q2^2 = 2*p1*p2 + 2*q1*q2" for p1 p2 q1 q2 :: nat
  proof (rule)
    assume "p1 = p2 ∧ q1 = q2"
    thus "p1⇧2 + p2⇧2 + q1⇧2 + q2⇧2 = 2 * p1 * p2 + 2 * q1 * q2"
      by (auto simp: algebra_simps power2_eq_square)
  next
    assume "p1⇧2 + p2⇧2 + q1⇧2 + q2⇧2 = 2 * p1 * p2 + 2 * q1 * q2"
    hence "(int p1)⇧2 + (int p2)⇧2 + (int q1)⇧2 + (int q2)⇧2 - 2 * int p1 * int p2 - 2 * int q1 * int q2 = 0"
      by (auto) (smt (verit, best) mult_2 of_nat_add of_nat_mult power2_eq_square)
    hence "(int p1 - int p2)^2 + (int q1 - int q2)^2 = 0"
      by (simp add: power2_diff)
    hence "int p1 = int p2" and "int q1 = int q2"
      by (simp add: sum_power2_eq_zero_iff)+
    thus "p1 = p2 ∧ q1 = q2"
      by auto
  qed

  thus ?thesis
    apply (simp only: is_dioph_rel_def)
    apply (rule exI[of _ "PA1❙^❙2 ❙+ PA2❙^❙2 ❙+ PB1❙^❙2 ❙+ PB2❙^❙2"])
    apply (rule exI[of _ "(ppolynomial.Const 2) ❙* PA1 ❙* PA2 ❙+ (ppolynomial.Const 2) ❙* PB1 ❙* PB2"])
    apply (subst unified)
    by (simp add: Sq_pp_def power2_eq_square)
qed


(* Some basic relations are diophantine *)
definition eq (infix ‹[=]› 50) where "eq Q R ≡ BINARY (=) Q R"
definition lt (infix ‹[<]› 50) where "lt Q R ≡ BINARY (<) Q R"
definition le (infix ‹[≤]› 50) where "le Q R ≡ Q [<] R [∨] Q [=] R"
definition gt (infix ‹[>]› 50) where "gt Q R ≡ R [<] Q"
definition ge (infix ‹[≥]› 50) where "ge Q R ≡ Q [>] R [∨] Q [=] R"

named_theorems defs
lemmas [defs] = zero_p_def one_p_def eq_def lt_def le_def gt_def ge_def LARY_eval
                UNARY_def BINARY_def TERNARY_def QUATERNARY_def ALLC_LIST_eval ALLC_eval

named_theorems dioph
lemmas [dioph] = or_dioph and_dioph

lemma true_dioph[dioph]: "is_dioph_rel TRUE" 
  unfolding TRUE_def UNARY_def is_dioph_rel_def by auto

lemma eq_dioph[dioph]: "is_dioph_rel (Q [=] R)"
  unfolding is_dioph_rel_def
  apply (rule exI[of _ "convert Q"])
  apply (rule exI[of _ "convert R"])
  using convert_eval BINARY_def by (auto simp: eq_def)

lemma lt_dioph[dioph]: "is_dioph_rel (Q [<] R)"
  unfolding is_dioph_rel_def
  apply (rule exI[of _ "(ppolynomial.Const 1) ❙+ (ppolynomial.Var 0) ❙+ convert Q"])
  apply (rule exI[of _ "convert R"])
  using convert_eval BINARY_def apply (auto simp: lt_def)
  by (metis add.commute add.right_neutral less_natE)

definition zero (‹[0=] _› [60] 60) where[defs]: "zero Q ≡ ❙0 [=] Q"
lemma zero_dioph[dioph]: "is_dioph_rel ([0=] Q)"
  unfolding zero_def by (auto simp: eq_dioph)

lemma gt_dioph[dioph]: "is_dioph_rel (Q [>] R)"
  unfolding gt_def by (auto simp: lt_dioph)

lemma le_dioph[dioph]: "is_dioph_rel (Q [≤] R)"
  unfolding le_def by (auto simp: lt_dioph eq_dioph or_dioph)

lemma ge_dioph[dioph]: "is_dioph_rel (Q [≥] R)"
  unfolding ge_def by (auto simp: gt_dioph eq_dioph or_dioph)

text ‹Bounded Constant All Quantifier, dioph rules›

lemma ALLC_LIST_dioph[dioph]: "list_all (is_dioph_rel ∘ DF) L ⟹ is_dioph_rel ([∀ in L] DF)"
  by (induction L, auto simp add: dioph)

lemma ALLC_dioph[dioph]: "∀i<n. is_dioph_rel (DF i) ⟹ is_dioph_rel ([∀<n] DF)"
  unfolding ALLC_def using ALLC_LIST_dioph[of DF "[0..<n]"] by (auto simp: list_all_length)

end