Theory Buchberger

(* Author: Alexander Maletzky *)

section ‹Buchberger's Algorithm›

theory Buchberger
  imports Algorithm_Schema
begin

context gd_term
begin

subsection ‹Reduction›

definition trdsp::"('t 0 'b) list  ('t, 'b, 'c) pdata_pair  ('t 0 'b::field)"
  where "trdsp bs p  trd bs (spoly (fst (fst p)) (fst (snd p)))"

lemma trdsp_alt: "trdsp bs (p, q) = trd bs (spoly (fst p) (fst q))"
  by (simp add: trdsp_def)

lemma trdsp_in_pmdl: "trdsp bs (p, q)  pmdl (insert (fst p) (insert (fst q) (set bs)))"
  unfolding trdsp_alt
proof (rule pmdl_closed_trd)
  have "spoly (fst p) (fst q)  pmdl {fst p, fst q}"
  proof (rule pmdl_closed_spoly)
    show "fst p  pmdl {fst p, fst q}" by (rule pmdl.span_base, simp)
  next
    show "fst q  pmdl {fst p, fst q}" by (rule pmdl.span_base, simp)
  qed
  also have "...  pmdl (insert (fst p) (insert (fst q) (set bs)))"
    by (rule pmdl.span_mono, simp)
  finally show "spoly (fst p) (fst q)  pmdl (insert (fst p) (insert (fst q) (set bs)))" .
next
  have "set bs  insert (fst p) (insert (fst q) (set bs))" by blast
  also have "...  pmdl (insert (fst p) (insert (fst q) (set bs)))"
    by (fact pmdl.span_superset)
  finally show "set bs  pmdl (insert (fst p) (insert (fst q) (set bs)))" .
qed

lemma dgrad_p_set_le_trdsp:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d {trdsp bs (p, q)} (insert (fst p) (insert (fst q) (set bs)))"
proof -
  let ?h = "trdsp bs (p, q)"
  have "(red (set bs))** (spoly (fst p) (fst q)) ?h" unfolding trdsp_alt by (rule trd_red_rtrancl)
  with assms have "dgrad_p_set_le d {?h} (insert (spoly (fst p) (fst q)) (set bs))"
    by (rule dgrad_p_set_le_red_rtrancl)
  also have "dgrad_p_set_le d ... ({fst p, fst q}  set bs)"
  proof (rule dgrad_p_set_leI_insert)
    show "dgrad_p_set_le d (set bs) ({fst p, fst q}  set bs)" by (rule dgrad_p_set_le_subset, blast)
  next
    from assms have "dgrad_p_set_le d {spoly (fst p) (fst q)} {fst p, fst q}"
      by (rule dgrad_p_set_le_spoly)
    also have "dgrad_p_set_le d ... ({fst p, fst q}  set bs)"
      by (rule dgrad_p_set_le_subset, blast)
    finally show "dgrad_p_set_le d {spoly (fst p) (fst q)} ({fst p, fst q}  set bs)" .
  qed
  finally show ?thesis by simp
qed

lemma components_trdsp_subset:
  "component_of_term ` keys (trdsp bs (p, q))  component_of_term ` Keys (insert (fst p) (insert (fst q) (set bs)))"
proof -
  let ?h = "trdsp bs (p, q)"
  have "(red (set bs))** (spoly (fst p) (fst q)) ?h" unfolding trdsp_alt by (rule trd_red_rtrancl)
  hence "component_of_term ` keys ?h 
              component_of_term ` keys (spoly (fst p) (fst q))  component_of_term ` Keys (set bs)"
    by (rule components_red_rtrancl_subset)
  also have "...  component_of_term ` Keys {fst p, fst q}  component_of_term ` Keys (set bs)"
    using components_spoly_subset by force
  also have "... = component_of_term ` Keys (insert (fst p) (insert (fst q) (set bs)))"
    by (simp add: Keys_insert image_Un Un_assoc)
  finally show ?thesis .
qed

definition gb_red_aux :: "('t, 'b::field, 'c) pdata list  ('t, 'b, 'c) pdata_pair list 
                          ('t 0 'b) list"
  where "gb_red_aux bs ps =
              (let bs' = map fst bs in
                filter (λh. h  0) (map (trdsp bs') ps)
              )"

text ‹Actually, @{const gb_red_aux} is only called on singleton lists.›

lemma set_gb_red_aux: "set (gb_red_aux bs ps) = (trdsp (map fst bs)) ` set ps - {0}"
  by (simp add: gb_red_aux_def, blast)

lemma in_set_gb_red_auxI:
  assumes "(p, q)  set ps" and "h = trdsp (map fst bs) (p, q)" and "h  0"
  shows "h  set (gb_red_aux bs ps)"
  using assms(1, 3) unfolding set_gb_red_aux assms(2) by force

lemma in_set_gb_red_auxE:
  assumes "h  set (gb_red_aux bs ps)"
  obtains p q where "(p, q)  set ps" and "h = trdsp (map fst bs) (p, q)"
  using assms unfolding set_gb_red_aux by force

lemma gb_red_aux_not_zero: "0  set (gb_red_aux bs ps)"
  by (simp add: set_gb_red_aux)

lemma gb_red_aux_irredudible:
  assumes "h  set (gb_red_aux bs ps)" and "b  set bs" and "fst b  0"
  shows "¬ lt (fst b) addst lt h"
proof
  assume "lt (fst b) addst (lt h)"
  from assms(1) obtain p q :: "('t, 'b, 'c) pdata" where h: "h = trdsp (map fst bs) (p, q)"
    by (rule in_set_gb_red_auxE)
  have "¬ is_red (set (map fst bs)) h" unfolding h trdsp_def by (rule trd_irred)
  moreover have "is_red (set (map fst bs)) h"
  proof (rule is_red_addsI)
    from assms(2) show "fst b  set (map fst bs)" by (simp)
  next
    from assms(1) have "h  0" by (simp add: set_gb_red_aux)
    thus "lt h  keys h" by (rule lt_in_keys)
  qed fact+
  ultimately show False ..
qed

lemma gb_red_aux_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (gb_red_aux bs ps)) (args_to_set ([], bs, ps))"
proof (rule dgrad_p_set_leI)
  fix h
  assume "h  set (gb_red_aux bs ps)"
  then obtain p q where "(p, q)  set ps" and h: "h = trdsp (map fst bs) (p, q)"
    by (rule in_set_gb_red_auxE)
  from assms have "dgrad_p_set_le d {h} (insert (fst p) (insert (fst q) (set (map fst bs))))"
    unfolding h by (rule dgrad_p_set_le_trdsp)
  also have "dgrad_p_set_le d ... (args_to_set ([], bs, ps))"
  proof (rule dgrad_p_set_le_subset, intro insert_subsetI)
    from (p, q)  set ps have "fst p  fst ` fst ` set ps" by force
    thus "fst p  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    from (p, q)  set ps have "fst q  fst ` snd ` set ps" by force
    thus "fst q  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    show "set (map fst bs)  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  qed
  finally show "dgrad_p_set_le d {h} (args_to_set ([], bs, ps))" .
qed

lemma components_gb_red_aux_subset:
  "component_of_term ` Keys (set (gb_red_aux bs ps))  component_of_term ` Keys (args_to_set ([], bs, ps))"
proof
  fix k
  assume "k  component_of_term ` Keys (set (gb_red_aux bs ps))"
  then obtain v where "v  Keys (set (gb_red_aux bs ps))" and k: "k = component_of_term v" ..
  from this(1) obtain h where "h  set (gb_red_aux bs ps)" and "v  keys h" by (rule in_KeysE)
  from this(1) obtain p q where "(p, q)  set ps" and h: "h = trdsp (map fst bs) (p, q)"
    by (rule in_set_gb_red_auxE)
  from v  keys h have "k  component_of_term ` keys h" by (simp add: k)
  have "component_of_term ` keys h  component_of_term ` Keys (insert (fst p) (insert (fst q) (set (map fst bs))))"
    unfolding h by (rule components_trdsp_subset)
  also have "...  component_of_term ` Keys (args_to_set ([], bs, ps))"
  proof (rule image_mono, rule Keys_mono, intro insert_subsetI)
    from (p, q)  set ps have "fst p  fst ` fst ` set ps" by force
    thus "fst p  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    from (p, q)  set ps have "fst q  fst ` snd ` set ps" by force
    thus "fst q  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    show "set (map fst bs)  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  qed
  finally have "component_of_term ` keys h  component_of_term ` Keys (args_to_set ([], bs, ps))" .
  with k  component_of_term ` keys h show "k  component_of_term ` Keys (args_to_set ([], bs, ps))" ..
qed

lemma pmdl_gb_red_aux: "set (gb_red_aux bs ps)  pmdl (args_to_set ([], bs, ps))"
proof
  fix h
  assume "h  set (gb_red_aux bs ps)"
  then obtain p q where "(p, q)  set ps" and h: "h = trdsp (map fst bs) (p, q)"
    by (rule in_set_gb_red_auxE)
  have "h  pmdl (insert (fst p) (insert (fst q) (set (map fst bs))))" unfolding h
    by (fact trdsp_in_pmdl)
  also have "...  pmdl (args_to_set ([], bs, ps))"
  proof (rule pmdl.span_mono, intro insert_subsetI)
    from (p, q)  set ps have "fst p  fst ` fst ` set ps" by force
    thus "fst p  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    from (p, q)  set ps have "fst q  fst ` snd ` set ps" by force
    thus "fst q  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  next
    show "set (map fst bs)  args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
  qed
  finally show "h  pmdl (args_to_set ([], bs, ps))" .
qed

lemma gb_red_aux_spoly_reducible:
  assumes "(p, q)  set ps"
  shows "(red (fst ` set bs  set (gb_red_aux bs ps)))** (spoly (fst p) (fst q)) 0"
proof -
  define h where "h = trdsp (map fst bs) (p, q)"
  from trd_red_rtrancl[of "map fst bs" "spoly (fst p) (fst q)"]
  have "(red (set (map fst bs)))** (spoly (fst p) (fst q)) h"
    by (simp only: h_def trdsp_alt)
  hence "(red (fst ` set bs  set (gb_red_aux bs ps)))** (spoly (fst p) (fst q)) h"
  proof (rule red_rtrancl_subset)
    show "set (map fst bs)  fst ` set bs  set (gb_red_aux bs ps)" by simp
  qed
  moreover have "(red (fst ` set bs  set (gb_red_aux bs ps)))** h 0"
  proof (cases "h = 0")
    case True
    show ?thesis unfolding True ..
  next
    case False
    hence "red {h} h 0" by (rule red_self)
    hence "red (fst ` set bs  set (gb_red_aux bs ps)) h 0"
    proof (rule red_subset)
      from assms h_def False have "h  set (gb_red_aux bs ps)" by (rule in_set_gb_red_auxI)
      thus "{h}  fst ` set bs  set (gb_red_aux bs ps)" by simp
    qed
    thus ?thesis ..
  qed
  ultimately show ?thesis by simp
qed

definition gb_red :: "('t, 'b::field, 'c::default, 'd) complT"
  where "gb_red gs bs ps sps data = (map (λh. (h, default)) (gb_red_aux (gs @ bs) sps), snd data)"

lemma fst_set_fst_gb_red: "fst ` set (fst (gb_red gs bs ps sps data)) = set (gb_red_aux (gs @ bs) sps)"
  by (simp add: gb_red_def, force)

lemma rcp_spec_gb_red: "rcp_spec gb_red"
proof (rule rcp_specI)
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  from gb_red_aux_not_zero show "0  fst ` set (fst (gb_red gs bs ps sps data))"
    unfolding fst_set_fst_gb_red .
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps h b and data::"nat × 'd"
  assume "h  set (fst (gb_red gs bs ps sps data))" and "b  set gs  set bs"
  from this(1) have "fst h  fst ` set (fst (gb_red gs bs ps sps data))" by simp
  hence "fst h  set (gb_red_aux (gs @ bs) sps)" by (simp only: fst_set_fst_gb_red)
  moreover from b  set gs  set bs have "b  set (gs @ bs)" by simp
  moreover assume "fst b  0"
  ultimately show "¬ lt (fst b) addst lt (fst h)" by (rule gb_red_aux_irredudible)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and d::"'a  nat" and data::"nat × 'd"
  assume "dickson_grading d"
  hence "dgrad_p_set_le d (set (gb_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))"
    by (rule gb_red_aux_dgrad_p_set_le)
  also have "... = args_to_set (gs, bs, sps)" by (simp add: args_to_set_alt image_Un)
  finally show "dgrad_p_set_le d (fst ` set (fst (gb_red gs bs ps sps data))) (args_to_set (gs, bs, sps))"
    by (simp only: fst_set_fst_gb_red)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  have "component_of_term ` Keys (set (gb_red_aux (gs @ bs) sps)) 
          component_of_term ` Keys (args_to_set ([], gs @ bs, sps))"
    by (rule components_gb_red_aux_subset)
  also have "... = component_of_term ` Keys (args_to_set (gs, bs, sps))"
    by (simp add: args_to_set_alt image_Un)
  finally show "component_of_term ` Keys (fst ` set (fst (gb_red gs bs ps sps data))) 
                component_of_term ` Keys (args_to_set (gs, bs, sps))" by (simp only: fst_set_fst_gb_red)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  have "set (gb_red_aux (gs @ bs) sps)  pmdl (args_to_set ([], gs @ bs, sps))"
    by (fact pmdl_gb_red_aux)
  also have "... = pmdl (args_to_set (gs, bs, sps))" by (simp add: args_to_set_alt image_Un)
  finally have "fst ` set (fst (gb_red gs bs ps sps data))  pmdl (args_to_set (gs, bs, sps))"
    by (simp only: fst_set_fst_gb_red)
  moreover {
    fix p q :: "('t, 'b, 'c) pdata"
    assume "(p, q)  set sps"
    hence "(red (fst ` set (gs @ bs)  set (gb_red_aux (gs @ bs) sps)))** (spoly (fst p) (fst q)) 0"
      by (rule gb_red_aux_spoly_reducible)
  }
  ultimately show
    "fst ` set (fst (gb_red gs bs ps sps data))  pmdl (args_to_set (gs, bs, sps)) 
     ((p, q)set sps.
         set sps  set bs × (set gs  set bs) 
         (red (fst ` (set gs  set bs)  fst ` set (fst (gb_red gs bs ps sps data))))** (spoly (fst p) (fst q)) 0)"
    by (auto simp add: image_Un fst_set_fst_gb_red)
qed

lemmas compl_struct_gb_red = compl_struct_rcp[OF rcp_spec_gb_red]
lemmas compl_pmdl_gb_red = compl_pmdl_rcp[OF rcp_spec_gb_red]
lemmas compl_conn_gb_red = compl_conn_rcp[OF rcp_spec_gb_red]

subsection ‹Pair Selection›

primrec gb_sel :: "('t, 'b::zero, 'c, 'd) selT" where
  "gb_sel gs bs [] data = []"|
  "gb_sel gs bs (p # ps) data = [p]"

lemma sel_spec_gb_sel: "sel_spec gb_sel"
proof (rule sel_specI)
  fix gs bs :: "('t, 'b, 'c) pdata list" and ps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
  assume "ps  []"
  then obtain p ps' where ps: "ps = p # ps'" by (meson list.exhaust)
  show "gb_sel gs bs ps data  []  set (gb_sel gs bs ps data)  set ps" by (simp add: ps)
qed

subsection ‹Buchberger's Algorithm›

lemma struct_spec_gb: "struct_spec gb_sel add_pairs_canon add_basis_canon gb_red"
  using sel_spec_gb_sel ap_spec_add_pairs_canon ab_spec_add_basis_sorted compl_struct_gb_red
  by (rule struct_specI)

definition gb_aux :: "('t, 'b, 'c) pdata list  nat × nat × 'd  ('t, 'b, 'c) pdata list 
                   ('t, 'b, 'c) pdata_pair list  ('t, 'b::field, 'c::default) pdata list"
  where "gb_aux = gb_schema_aux gb_sel add_pairs_canon add_basis_canon gb_red"

lemmas gb_aux_simps [code] = gb_schema_aux_simps[OF struct_spec_gb, folded gb_aux_def]

definition gb :: "('t, 'b, 'c) pdata' list  'd  ('t, 'b::field, 'c::default) pdata' list"
  where "gb = gb_schema_direct gb_sel add_pairs_canon add_basis_canon gb_red"

lemmas gb_simps [code] = gb_schema_direct_def[of gb_sel add_pairs_canon add_basis_canon gb_red, folded gb_def gb_aux_def]

lemmas gb_isGB = gb_schema_direct_isGB[OF struct_spec_gb compl_conn_gb_red, folded gb_def]

lemmas gb_pmdl = gb_schema_direct_pmdl[OF struct_spec_gb compl_pmdl_gb_red, folded gb_def]

subsubsection ‹Special Case: punit›

lemma (in gd_term) struct_spec_gb_punit: "punit.struct_spec punit.gb_sel add_pairs_punit_canon punit.add_basis_canon punit.gb_red"
  using punit.sel_spec_gb_sel ap_spec_add_pairs_punit_canon ab_spec_add_basis_sorted punit.compl_struct_gb_red
  by (rule punit.struct_specI)

definition gb_aux_punit :: "('a, 'b, 'c) pdata list  nat × nat × 'd  ('a, 'b, 'c) pdata list 
                   ('a, 'b, 'c) pdata_pair list  ('a, 'b::field, 'c::default) pdata list"
  where "gb_aux_punit = punit.gb_schema_aux punit.gb_sel add_pairs_punit_canon punit.add_basis_canon punit.gb_red"

lemmas gb_aux_punit_simps [code] = punit.gb_schema_aux_simps[OF struct_spec_gb_punit, folded gb_aux_punit_def]

definition gb_punit :: "('a, 'b, 'c) pdata' list  'd  ('a, 'b::field, 'c::default) pdata' list"
  where "gb_punit = punit.gb_schema_direct punit.gb_sel add_pairs_punit_canon punit.add_basis_canon punit.gb_red"

lemmas gb_punit_simps [code] = punit.gb_schema_direct_def[of "punit.gb_sel" add_pairs_punit_canon
                                "punit.add_basis_canon" "punit.gb_red", folded gb_punit_def gb_aux_punit_def]

lemmas gb_punit_isGB = punit.gb_schema_direct_isGB[OF struct_spec_gb_punit punit.compl_conn_gb_red, folded gb_punit_def]

lemmas gb_punit_pmdl = punit.gb_schema_direct_pmdl[OF struct_spec_gb_punit punit.compl_pmdl_gb_red, folded gb_punit_def]

end (* gd_term *)

end (* theory *)