Theory Polynomial_Interpretation

section ‹Definition of Monotone Algebras and Polynomial Interpretations›

theory Polynomial_Interpretation
  imports 
    Preliminaries_on_Polynomials_1
    First_Order_Terms.Term
    First_Order_Terms.Subterm_and_Context
begin
abbreviation "PVar ≡ MPoly_Type.Var" 
abbreviation "TVar ≡ Term.Var" 
 
type_synonym ('f,'v)rule = "('f,'v)term × ('f,'v)term" 

text ‹We fix the domain to the set of nonnegative numbers›

lemma subterm_size[termination_simp]: "x < length ts ⟹ size (ts ! x) < Suc (size_list size ts)" 
  by (meson Suc_n_not_le_n less_eq_Suc_le not_less_eq nth_mem size_list_estimation)

definition assignment :: "(var ⇒ 'a :: {ord,zero}) ⇒ bool" where
  "assignment α = (∀ x. α x ≥ 0)"

lemma assignmentD: assumes "assignment α" 
  shows "α x ≥ 0" 
  using assms unfolding assignment_def by auto

definition monotone_fun_wrt :: "('a :: {zero,ord} ⇒ 'a ⇒ bool) ⇒ nat ⇒ ('a list ⇒ 'a) ⇒ bool" where
  "monotone_fun_wrt gt n f = (∀ v' i vs. length vs = n ⟶ (∀ v ∈ set vs. v ≥ 0) 
     ⟶ i < n ⟶ gt v' (vs ! i) ⟶ 
     gt (f (vs [ i := v'])) (f vs))" 

definition valid_fun :: "nat ⇒ ('a list ⇒ 'a :: {zero,ord}) ⇒ bool" where
  "valid_fun n f = (∀ vs. length vs = n ⟶ (∀ v ∈ set vs. v ≥ 0) ⟶ f vs ≥ 0)"

definition monotone_poly_wrt :: "('a :: {comm_semiring_1,zero,ord} ⇒ 'a ⇒ bool) ⇒ var set ⇒ 'a mpoly ⇒ bool" where
  "monotone_poly_wrt gt V p = (∀ α x v. assignment α ⟶ x ∈ V ⟶ gt v (α x) ⟶ 
     gt (insertion (α(x := v)) p) (insertion α p))" 

definition valid_poly :: "'a :: {ord,comm_semiring_1} mpoly ⇒ bool" where
  "valid_poly p = (∀ α. assignment α ⟶ insertion α p ≥ 0)"


locale term_algebra = 
  fixes F :: "('f × nat) set" 
  and I :: "'f ⇒ ('a :: {ord,zero} list) ⇒ 'a" 
  and gt :: "'a ⇒ 'a ⇒ bool"
begin

abbreviation monotone_fun where "monotone_fun ≡ monotone_fun_wrt gt" 

definition valid_monotone_fun :: "('f × nat) ⇒ bool" where
  "valid_monotone_fun fn = (∀ f n p. fn = (f,n) ⟶ p = I f
      ⟶ valid_fun n p ∧ monotone_fun n p)"

definition valid_monotone_inter where "valid_monotone_inter = Ball F valid_monotone_fun" 

definition orient_rule :: "('f,var)rule ⇒ bool" where
  "orient_rule rule = (case rule of (l,r) ⇒ (∀ α. assignment α ⟶ gt (I⟦l⟧α) (I⟦r⟧α)))"
end

locale omega_term_algebra = term_algebra F I "(>) :: int ⇒ int ⇒ bool" for F and I :: "'f ⇒ _" +
  assumes vm_inter: valid_monotone_inter
begin
definition termination_by_interpretation :: "('f,var) rule set ⇒ bool" where
  "termination_by_interpretation R = (∀ (l,r) ∈ R. orient_rule (l,r) ∧ funas_term l ∪ funas_term r ⊆ F)"
end

locale poly_inter =
  fixes F :: "('f × nat) set" 
  and   I :: "'f ⇒ 'a :: linordered_idom mpoly" 
  and   gt :: "'a ⇒ 'a ⇒ bool" (infix ‹≻› 50) 
begin

definition I' where "I' f vs = insertion (λ i. if i < length vs then vs ! i else 0) (I f)" 
sublocale term_algebra F I' gt .

abbreviation monotone_poly where "monotone_poly ≡ monotone_poly_wrt gt"

abbreviation weakly_monotone_poly where "weakly_monotone_poly ≡ monotone_poly_wrt (≥)" 

definition gt_poly :: "'a mpoly ⇒ 'a mpoly ⇒ bool" (infix ‹≻⇩p› 50) where
  "(p ≻⇩p q) = (∀ α. assignment α ⟶ insertion α p ≻ insertion α q)" 

definition valid_monotone_poly :: "('f × nat) ⇒ bool" where
  "valid_monotone_poly fn = (∀ f n p. fn = (f,n) ⟶ p = I f
      ⟶ valid_poly p ∧ monotone_poly {..<n} p ∧ vars p = {..<n})"

definition valid_weakly_monotone_poly :: "('f × nat) ⇒ bool" where
  "valid_weakly_monotone_poly fn = (∀ f n p. fn = (f,n) ⟶ p = I f
      ⟶ valid_poly p ∧ weakly_monotone_poly {..<n} p ∧ vars p ⊆ {..<n})"

definition valid_monotone_poly_inter where "valid_monotone_poly_inter = Ball F valid_monotone_poly" 
definition valid_weakly_monotone_inter where "valid_weakly_monotone_inter = Ball F valid_weakly_monotone_poly" 

fun eval :: "('f,var)term ⇒ 'a mpoly" where
  "eval (TVar x) = PVar x" 
| "eval (Fun f ts) = substitute (λ i. if i < length ts then eval (ts ! i) else 0) (I f)" 

lemma I'_is_insertion_eval: "I' ⟦t⟧ α = insertion α (eval t)" 
proof (induct t)
  case (Var x)
  then show ?case by (simp add: insertion_Var)
next
  case (Fun f ts)
  then show ?case 
    apply (simp add: insertion_substitute I'_def[of f])
    apply (intro arg_cong[of _ _ "λ α. insertion α (I f)"] ext)
    subgoal for i by (cases "i < length ts", auto)
    done
qed

lemma orient_rule: "orient_rule (l,r) = (eval l ≻⇩p eval r)" 
  unfolding orient_rule_def split I'_is_insertion_eval gt_poly_def ..

lemma vars_eval: "vars (eval t) ⊆ vars_term t" 
proof (induct t)
  case (Fun f ts)
  define V where "V = vars_term (Fun f ts)" 
  define σ where "σ = (λi. if i < length ts then eval (ts ! i) else 0)" 
  {
    fix i  
    have IH: "vars (σ i) ⊆ V" 
    proof (cases "i < length ts")
      case False
      thus ?thesis unfolding σ_def by auto
    next
      case True
      hence "ts ! i ∈ set ts" by auto
      with Fun(1)[OF this] have "vars (eval (ts ! i)) ⊆ V" by (auto simp: V_def)
      thus ?thesis unfolding σ_def using True by auto
    qed
  } note σ_vars = this
  define p where "p = (I f)" 
  show ?case unfolding eval.simps σ_def[symmetric] V_def[symmetric] p_def[symmetric] using σ_vars
    vars_substitute[of σ] by auto
qed auto

lemma monotone_imp_weakly_monotone: assumes valid: "valid_monotone_poly p"
  and gt: "⋀ x y. (x ≻ y) = (x > y)" 
  shows "valid_weakly_monotone_poly p" 
  unfolding valid_weakly_monotone_poly_def
proof (intro allI impI, clarify, intro conjI)
  fix f n
  assume "p = (f,n)" 
  note * = valid[unfolded valid_monotone_poly_def, rule_format, OF this refl]
  from * show "valid_poly (I f)" by auto
  from * show "vars (I f) ⊆ {..<n}" by auto
  show "weakly_monotone_poly {..<n} (I f)" 
    unfolding monotone_poly_wrt_def
  proof (intro allI impI, goal_cases)
    case (1 α x a)
    from * have "monotone_poly {..<n} (I f)" by auto
    from this[unfolded monotone_poly_wrt_def, rule_format, OF 1(1-2), of a]
    show ?case unfolding gt using 1(3) by force
  qed
qed

lemma valid_imp_insertion_eval_pos: assumes valid: valid_monotone_poly_inter 
  and "funas_term t ⊆ F"
  and "assignment α" 
shows "insertion α (eval t) ≥ 0"  
  using assms(2-3)
proof (induct t arbitrary: α)
  case (Var x)
  thus ?case by (auto simp: assignment_def insertion_Var)
next
  case (Fun f ts)
  let ?n = "length ts" 
  let ?f = "(f,?n)"
  let ?p = "I f" 
  from Fun have "?f ∈ F" by auto
  from valid[unfolded valid_monotone_poly_inter_def, rule_format, OF this, unfolded valid_monotone_poly_def]
  have valid: "valid_poly ?p" and "vars ?p = {..<?n}" by auto
  from valid[unfolded valid_poly_def]
  have ins: "assignment α ⟹ 0 ≤ insertion α (I f)" for α by auto
  {
    fix i
    assume "i < ?n" 
    hence "ts ! i ∈ set ts" by auto
    with Fun(1)[OF this _ Fun(3)] Fun(2) have "0 ≤ insertion α (eval (ts ! i))" by auto
  }
  note IH = this
  show ?case 
    apply (simp add: insertion_substitute)
    apply (intro ins, unfold assignment_def, intro allI)
    subgoal for i using IH[of i] by auto
    done
qed

end

locale delta_poly_inter = poly_inter F I "(λ x y. x ≥ y + δ)" for F :: "('f × nat) set" and I and 
  δ :: "'a :: {floor_ceiling,linordered_field}" +
  assumes valid: valid_monotone_poly_inter 
  and δ0: "δ > 0" 
begin
definition termination_by_delta_interpretation :: "('f,var) rule set ⇒ bool" where
  "termination_by_delta_interpretation R = (∀ (l,r) ∈ R. orient_rule (l,r) ∧ funas_term l ∪ funas_term r ⊆ F)"
end

locale int_poly_inter = poly_inter F I "(>) :: int ⇒ int ⇒ bool" for F :: "('f × nat) set" and I +
  assumes valid: valid_monotone_poly_inter 
begin

sublocale omega_term_algebra F I'
proof (unfold_locales, unfold valid_monotone_inter_def, intro ballI)
  fix fn
  assume "fn ∈ F" 
  from valid[unfolded valid_monotone_poly_inter_def, rule_format, OF this]
  have valid: "valid_monotone_poly fn" .
  show "valid_monotone_fun fn" unfolding valid_monotone_fun_def
  proof (intro allI impI conjI)
    fix f n p
    assume fn: "fn = (f,n)" and p: "p = I' f" 
    from valid[unfolded valid_monotone_poly_def, rule_format, OF fn refl]
    have valid: "valid_poly (I f)" and mono: "monotone_poly {..<n} (I f)" by auto
    
    show "valid_fun n p" unfolding valid_fun_def
    proof (intro allI impI)
      fix vs
      assume "length vs = n" and vs: "Ball (set vs) ((≤) (0 :: int))" 
      show "0 ≤ p vs" unfolding p I'_def 
        by (rule valid[unfolded valid_poly_def, rule_format], insert vs, auto simp: assignment_def)
    qed

    show "monotone_fun n p" unfolding monotone_fun_wrt_def
    proof (intro allI impI)
      fix v' i vs
      assume *: "length vs = n" "Ball (set vs) ((≤) (0 :: int))" "i < n" "vs ! i < v'" 
      show "p vs < p (vs[i := v'])" unfolding p I'_def 
        by (rule ord_less_eq_trans[OF mono[unfolded monotone_poly_wrt_def, rule_format, of _ i v'] 
            insertion_irrelevant_vars], insert *, auto simp: assignment_def)
    qed
  qed
qed

  
definition termination_by_poly_interpretation :: "('f,var) rule set ⇒ bool" where
  "termination_by_poly_interpretation = termination_by_interpretation"
end

locale wm_int_poly_inter = poly_inter F I "(>) :: int ⇒ int ⇒ bool" for F :: "('f × nat) set" and I +
  assumes valid: valid_weakly_monotone_inter 
begin
definition oriented_by_interpretation :: "('f,var) rule set ⇒ bool" where
  "oriented_by_interpretation R = (∀ (l,r) ∈ R. orient_rule (l,r) ∧ funas_term l ∪ funas_term r ⊆ F)"
end

locale linear_poly_inter = poly_inter F I gt for F I gt + 
  assumes linear: "⋀ f n. (f,n) ∈ F ⟹ total_degree (I f) ≤ 1" 

locale linear_int_poly_inter = int_poly_inter F I + linear_poly_inter F I "(>)"
  for F :: "('f × nat) set" and I

locale linear_wm_int_poly_inter = wm_int_poly_inter F I + linear_poly_inter F I "(>)"
  for F :: "('f × nat) set" and I

definition termination_by_linear_int_poly_interpretation :: "('f × nat)set ⇒ ('f,var)rule set ⇒ bool" where
  "termination_by_linear_int_poly_interpretation F R = (∃ I. linear_int_poly_inter F I ∧ 
     int_poly_inter.termination_by_poly_interpretation F I R)" 

definition omega_termination :: "('f × nat)set ⇒ ('f,var)rule set ⇒ bool" where
  "omega_termination F R = (∃ I. omega_term_algebra F I ∧ 
     omega_term_algebra.termination_by_interpretation F I R)" 

definition termination_by_int_poly_interpretation :: "('f × nat)set ⇒ ('f,var)rule set ⇒ bool" where
  "termination_by_int_poly_interpretation F R = (∃ I. int_poly_inter F I ∧ 
     int_poly_inter.termination_by_poly_interpretation F I R)" 

definition termination_by_delta_poly_interpretation :: "'a :: {floor_ceiling,linordered_field} itself ⇒ ('f × nat)set ⇒ ('f,var)rule set ⇒ bool" where
  "termination_by_delta_poly_interpretation TYPE('a) F R = (∃ I δ. delta_poly_inter F I (δ :: 'a) ∧ 
     delta_poly_inter.termination_by_delta_interpretation F I δ R)" 

definition orientation_by_linear_wm_int_poly_interpretation :: "('f × nat)set ⇒ ('f,var)rule set ⇒ bool" where
  "orientation_by_linear_wm_int_poly_interpretation F R = (∃ I. linear_wm_int_poly_inter F I ∧ 
     wm_int_poly_inter.oriented_by_interpretation F I R)" 

end