Theory Polynomial_Instantiation

(*******************************************************************************

  Project: Sumcheck Protocol

  Authors: Azucena Garvia Bosshard <zucegb@gmail.com>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>
           Jonathan Bootle, IBM Research Europe <jbt@zurich.ibm.com>

*******************************************************************************)

section ‹Instantiation for Multivariate Polynomials›

theory Polynomial_Instantiation
  imports 
    "Polynomials.More_MPoly_Type"
begin

text ‹
\textbf{NOTE:} if considered to be useful enough, the definitions and lemmas in this theory could 
be moved to the theory @{theory "Polynomials.More_MPoly_Type"}.
›

text ‹Define instantiation of mpoly's. The conditions @{term "(≠) 1"} and @{term "(≠) 0"} in 
the sets being multiplied or added over are needed to prove the correspondence with evaluation: 
a full instance corresponds to an evaluation (see lemma below).›

subsection ‹Instantiation of monomials›

type_synonym ('a, 'b) subst = "'a ⇀ 'b"

lift_definition 
  inst_monom_coeff :: ‹(nat ⇒⇩0 nat) ⇒ (nat, 'a) subst ⇒ 'a::comm_semiring_1› 
  is ‹λm σ. (∏v | v ∈ dom σ ∧ the (σ v) ^ m v ≠ 1. the (σ v) ^ m v)› .

lift_definition 
  inst_monom_resid :: ‹(nat ⇒⇩0 nat) ⇒ (nat, 'a) subst ⇒ (nat ⇒⇩0 nat)›  
  is ‹(λm σ v. m v when v ∉ dom σ)›
  by (metis (mono_tags, lifting) finite_subset mem_Collect_eq subsetI zero_when) 

lemmas inst_monom_defs = inst_monom_coeff_def inst_monom_resid_def

lemma lookup_inst_monom_resid:
  shows ‹lookup (inst_monom_resid m σ) v = (if v ∈ dom σ then 0 else lookup m v)›
  by transfer simp


subsection ‹Instantiation of polynomials›

definition 
  inst_fun :: ‹((nat ⇒⇩0 nat) ⇒ 'a) ⇒ (nat, 'a) subst ⇒ (nat ⇒⇩0 nat) ⇒ 'a::comm_semiring_1› where
  ‹inst_fun p σ = (λm. (∑m' | inst_monom_resid m' σ = m ∧ p m' * inst_monom_coeff m' σ ≠ 0.
                               p m' * inst_monom_coeff m' σ))›

lemma finite_inst_fun_keys: 
  assumes ‹finite {m. p m ≠ 0}›
  shows ‹finite {m. (∑m' | inst_monom_resid m' σ = m ∧ p m' ≠ 0 ∧ inst_monom_coeff m' σ ≠ 0.
                               p m' * inst_monom_coeff m' σ) ≠ 0}›
proof -
  from ‹finite {m. p m ≠ 0}›
  have ‹finite ((λm'. inst_monom_resid m' σ)`{x. p x ≠ 0})› by auto
  moreover 
  have ‹{m. (∑m' | inst_monom_resid m' σ = m ∧ p m' ≠ 0 ∧ inst_monom_coeff m' σ ≠ 0. 
                         p m' * inst_monom_coeff m' σ) ≠ 0}
            ⊆ (λm'. inst_monom_resid m' σ)`{m. p m ≠ 0}›
    by (auto elim: sum.not_neutral_contains_not_neutral)
  ultimately show ?thesis
    by (auto elim: finite_subset)
qed

lemma finite_inst_fun_keys_ext:
  assumes ‹finite {m. p m ≠ 0}›
  shows  "finite {a. (∑m' | inst_monom_resid m' σ = a ∧ p m' ≠ 0 ∧ inst_monom_coeff m' σ ≠ 0.
        p m' * inst_monom_coeff m' σ * (∏aa. the (ρ aa) ^ lookup (inst_monom_resid m' σ) aa)) ≠ 0}"
proof -
  from ‹finite {m. p m ≠ 0}›
  have ‹finite ((λm'. inst_monom_resid m' σ)`{x. p x ≠ 0})› by auto
  moreover 
  have ‹{m. (∑m' | inst_monom_resid m' σ = m ∧ p m' ≠ 0 ∧ inst_monom_coeff m' σ ≠ 0. 
                         p m' * inst_monom_coeff m' σ * 
                         (∏aa. the (ρ aa) ^ lookup (inst_monom_resid m' σ) aa)) ≠ 0}
            ⊆ (λm'. inst_monom_resid m' σ)`{m. p m ≠ 0}›
    by (auto elim: sum.not_neutral_contains_not_neutral)
  ultimately show ?thesis
    by (auto elim: finite_subset)
qed

lift_definition 
  inst_aux :: ‹((nat ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (nat, 'a) subst ⇒ (nat ⇒⇩0 nat) ⇒⇩0 'a::semidom› 
  is inst_fun 
  by (auto simp add: inst_fun_def intro: finite_inst_fun_keys)

lift_definition inst :: ‹'a mpoly ⇒ (nat, 'a::semidom) subst ⇒ 'a mpoly› 
  is inst_aux .

lemmas inst_defs = inst_def inst_aux_def inst_fun_def


subsection ‹Full instantiation corresponds to evaluation›

lemma dom_Some: ‹dom (Some o f) = UNIV›
  by (simp add: dom_def)

lemma inst_full_eq_insertion:      
  fixes p :: ‹('a::semidom) mpoly› and σ :: ‹nat ⇒ 'a› 
  shows ‹inst p (Some o σ) = Const (insertion σ p)›
proof transfer
  fix p :: ‹(nat ⇒⇩0 nat) ⇒⇩0 'a› and σ :: ‹nat ⇒ 'a› 
  show ‹inst_aux p (Some o σ) = Const⇩0 (insertion_aux σ p)›
    unfolding poly_mapping_eq_iff
    apply (simp add: Const⇩0_def inst_aux.rep_eq inst_fun_def inst_monom_defs
                     Poly_Mapping.single.rep_eq insertion_aux.rep_eq insertion_fun_def)
    apply (rule ext)
    subgoal for m
      by (cases "m = 0") 
         (simp_all add: Sum_any.expand_set Prod_any.expand_set dom_Some)
    done
qed


end