Theory Cooper

(*  Author:     Tobias Nipkow, 2007  *)

theory Cooper
imports PresArith
begin

subsection‹Cooper›

text‹This section formalizes Cooper's algorithm~\<^cite>‹"Cooper72"›.›

lemma set_atoms0_iff:
 "qfree φ ⟹ a ∈ set(Z.atoms⇩₀ φ) ⟷ a ∈ atoms φ ∧ hd_coeff a ≠ 0"
by(induct φ) (auto split:if_split_asm)

definition
"hd_coeffs1 φ =
 (let m = zlcms(map hd_coeff (Z.atoms⇩₀ φ))
  in And (Atom(Dvd m 0 [1])) (map⇩_f⇩_m (hd_coeff1 m) φ))"

lemma I_hd_coeffs1:
assumes "qfree φ"
shows "(∃x. Z.I (hd_coeffs1 φ) (x#xs)) = (∃x. Z.I φ (x#xs))" (is "?L = ?R")
proof -
  let ?l = "zlcms(map hd_coeff (Z.atoms⇩₀ φ))"
  have "?l>0" by(simp add: zlcms_pos set_atoms0_iff[OF ‹qfree φ›])
  have "?L = (∃x. ?l dvd x+0 ∧ Z.I (map⇩_f⇩_m (hd_coeff1 ?l) φ) (x#xs))"
    by(simp add:hd_coeffs1_def)
  also have "… = (∃x. Z.I (map⇩_f⇩_m (hd_coeff1 ?l) φ) (?l*x#xs))"
    by(rule unity_coeff_ex[THEN meta_eq_to_obj_eq,symmetric])
  also have "… = ?R"
    by(simp add: I_hd_coeff1_mult[OF ‹?l>0› ‹qfree φ›] dvd_zlcms)
  finally show ?thesis .
qed


fun min_inf :: "atom fm ⇒ atom fm" (‹inf⇩_-›) where
"inf⇩_- (And φ⇩₁ φ⇩₂) = and (inf⇩_- φ⇩₁) (inf⇩_- φ⇩₂)" |
"inf⇩_- (Or φ⇩₁ φ⇩₂) = or (inf⇩_- φ⇩₁) (inf⇩_- φ⇩₂)" |
"inf⇩_- (Atom(Le i (k#ks))) =
  (if k<0 then TrueF else if k>0 then FalseF else Atom(Le i (0#ks)))" |
"inf⇩_- φ = φ"


definition
"qe_cooper⇩₁ φ =
 (let as = Z.atoms⇩₀ φ; d = zlcms(map divisor as); ls = lbounds as
  in or (Disj [0..d - 1] (λn. subst n [] (inf⇩_- φ)))
        (Disj ls (λ(i,ks).
           Disj [0..d - 1] (λn. subst (i + n) (-ks) φ))))"


lemma min_inf:
  "nqfree f ⟹ ∀a∈set(Z.atoms⇩₀ f). hd_coeff_is1 a
   ⟹ ∃x.∀y<x. Z.I (inf⇩_- f) (y # xs) = Z.I f (y # xs)"
  (is "_ ⟹ _ ⟹ ∃x. ?P f x")
proof(induct f rule: min_inf.induct)
  case (3 i k ks)
  { assume "k=0" hence ?case using 3 by simp }
  moreover
  { assume "k= -1"
    hence "?P (Atom(Le i (k#ks))) (-i + ⟨ks,xs⟩ - 1)" using 3 by auto
    hence ?case .. }
  moreover
  { assume "k=1"
    hence "?P (Atom(Le i (k#ks))) (i - ⟨ks,xs⟩ - 1)" using 3 by auto
    hence ?case .. }
  ultimately show ?case using 3 by auto
next
  case (1 f1 f2)
  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
  hence "?P (And f1 f2) (min x1 x2)" by simp
  thus ?case ..
next
  case (2 f1 f2)
  then obtain x1 x2 where "?P f1 x1" "?P f2 x2" by fastforce+
  hence "?P (Or f1 f2) (min x1 x2)" by simp
  thus ?case ..
qed simp_all


lemma min_inf_repeats:
  "nqfree φ ⟹ ∀a∈set(Z.atoms⇩₀ φ). divisor a dvd d ⟹
  Z.I (inf⇩_- φ) ((x - k*d)#xs) = Z.I (inf⇩_- φ) (x#xs)"
proof(induct φ rule:min_inf.induct)
  case ("4_4" da i ks)
  show ?case
  proof (cases ks)
    case Nil thus ?thesis by simp
  next
    case (Cons j js)
    show ?thesis
    proof cases
      assume "j=0" thus ?thesis using Cons by simp
    next
      assume "j≠0"
      hence "da dvd d" using Cons "4_4" by simp
      hence "da dvd i + (j * x - j * (k * d) + ⟨js,xs⟩) ⟷
             da dvd i + (j * x + ⟨js,xs⟩)"
      proof -
        have "da dvd i + (j * x - j * (k * d) + ⟨js,xs⟩) ⟷
              da dvd (i + j*x + ⟨js,xs⟩) - (j*k)*d"
          by(simp add: algebra_simps)
        also have "… ⟷ da dvd i + j*x + ⟨js,xs⟩" using ‹da dvd d›
          by (metis dvd_diff zdvd_zdiffD dvd_mult mult.commute)
        also have "… ⟷ da dvd i + (j * x + ⟨js,xs⟩)"
          by(simp add: algebra_simps)
        finally show ?thesis .
      qed
      then show ?thesis using Cons by (simp add:ring_distribs)
    qed
  qed
next
  case ("4_5" da i ks)
  show ?case
  proof (cases ks)
    case Nil thus ?thesis by simp
  next
    case (Cons j js)
    show ?thesis
    proof cases
      assume "j=0" thus ?thesis using Cons by simp
    next
      assume "j≠0"
      hence "da dvd d" using Cons "4_5" by simp
      hence "da dvd i + (j * x - j * (k * d) + ⟨js,xs⟩) ⟷
             da dvd i + (j * x + ⟨js,xs⟩)"
      proof -
        have "da dvd i + (j * x - j * (k * d) + ⟨js,xs⟩) ⟷
              da dvd (i + j*x + ⟨js,xs⟩) - (j*k)*d"
          by(simp add: algebra_simps)
        also have "… ⟷ da dvd i + j*x + ⟨js,xs⟩" using ‹da dvd d›
          by (metis dvd_diff zdvd_zdiffD dvd_mult mult.commute)
        also have "… ⟷ da dvd i + (j * x + ⟨js,xs⟩)"
          by(simp add: algebra_simps)
        finally show ?thesis .
      qed
      then show ?thesis using Cons by (simp add:ring_distribs)
    qed
  qed
qed simp_all


lemma atoms_subset: "qfree f ⟹ set(Z.atoms⇩₀(f::atom fm)) ≤ atoms f"
by (induct f) auto

(* copied from Amine *)
lemma β:
  "⟦ nqfree φ;  ∀a∈set(Z.atoms⇩₀ φ). hd_coeff_is1 a;
     ∀a∈set(Z.atoms⇩₀ φ). divisor a dvd d; d > 0;
     ¬(∃j∈{0 .. d - 1}. ∃(i,ks) ∈ set(lbounds(Z.atoms⇩₀ φ)).
         x = i - ⟨ks,xs⟩ + j); Z.I φ (x#xs) ⟧
  ⟹ Z.I φ ((x-d)#xs)"
proof(induct φ)
  case (Atom a)
  show ?case
  proof (cases a)
    case (Le i js)
    show ?thesis
    proof (cases js)
      case Nil thus ?thesis using Le Atom by simp
    next
      case (Cons k ks) thus ?thesis using Le Atom
        by (auto simp:lbounds_def Ball_def split:if_split_asm) arith
    qed
  next
    case (Dvd m i js)
    show ?thesis
    proof (cases js)
      case Nil thus ?thesis using Dvd Atom by simp
    next
      case (Cons k ks)
      show ?thesis
      proof cases
        assume "k=0" thus ?thesis using Cons Dvd Atom by simp
      next
        assume "k≠0"
        hence "m dvd d" using Cons Dvd Atom by auto
        have "m dvd i + (x + ⟨ks,xs⟩) ⟹ m dvd i + (x - d + ⟨ks,xs⟩)"
          (is "?L ⟹ _")
        proof -
          assume ?L
          hence "m dvd i + (x + ⟨ks,xs⟩) - d"
            by (metis ‹m dvd d› dvd_diff)
          thus ?thesis by(simp add:algebra_simps)
        qed
        thus ?thesis using Atom Dvd Cons by(auto split:if_split_asm)
      qed
    qed
  next
    case (NDvd m i js)
    show ?thesis
    proof (cases js)
      case Nil thus ?thesis using NDvd Atom by simp
    next
      case (Cons k ks)
      show ?thesis
      proof cases
        assume "k=0" thus ?thesis using Cons NDvd Atom by simp
      next
        assume "k≠0"
        hence "m dvd d" using Cons NDvd Atom by auto
        have "m dvd i + (x - d + ⟨ks,xs⟩) ⟹ m dvd i + (x + ⟨ks,xs⟩)"
          (is "?L ⟹ _")
        proof -
          assume ?L
          hence "m dvd i + (x + ⟨ks,xs⟩) - d" by(simp add:algebra_simps)
          thus ?thesis by (metis ‹m dvd d› zdvd_zdiffD)
        qed
        thus ?thesis using Atom NDvd Cons by(auto split:if_split_asm)
      qed
    qed
  qed
qed force+


lemma periodic_finite_ex:
  assumes dpos: "(0::int) < d" and modd: "∀x k. P x = P(x - k*d)"
  shows "(∃x. P x) = (∃j∈{0..d - 1}. P j)"
  (is "?LHS = ?RHS")
proof
  assume ?LHS
  then obtain x where P: "P x" ..
  have "x mod d = x - (x div d)*d"
    by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq)
  hence Pmod: "P x = P(x mod d)" using modd by simp
  have "P(x mod d)" using dpos P Pmod by simp
  moreover have "x mod d ∈ {0..d - 1}" using dpos by auto
  ultimately show ?RHS ..
qed auto

lemma cpmi_eq: "(0::int) < D ⟹ (∃z. ∀x. x < z ⟶ (P x = P1 x))
⟹ ∀x.¬(∃j∈{0..D - 1}. ∃b∈B. P(b+j)) ⟶ P (x) ⟶ P (x - D) 
⟹ ∀x. ∀k. P1 x = P1(x-k*D)
⟹ (∃x. P(x)) = ((∃j∈{0..D - 1}. P1(j)) ∨ (∃j∈{0..D - 1}. ∃b∈B. P(b+j)))"
apply(rule iffI)
prefer 2
apply(drule minusinfinity)
apply assumption+
apply(fastforce)
apply clarsimp
apply(subgoal_tac "⋀k. 0≤k ⟹ ∀x. P x ⟶ P (x - k*D)")
apply(frule_tac x = x and z=z in decr_lemma)
apply(subgoal_tac "P1(x - (¦x - z¦ + 1) * D)")
prefer 2
apply(subgoal_tac "0 ≤ (¦x - z¦ + 1)")
prefer 2 apply arith
 apply fastforce
apply(drule (1)  periodic_finite_ex)
apply blast
apply(blast dest:decr_mult_lemma)
done


theorem cp_thm:
  assumes nq: "nqfree φ"
  and u: "∀a∈set(Z.atoms⇩₀ φ). hd_coeff_is1 a"
  and d: "∀a∈set(Z.atoms⇩₀ φ). divisor a dvd d"
  and dp: "d > 0"
  shows "(∃x. Z.I φ (x#xs)) =
   (∃j∈{0..d - 1}. Z.I (inf⇩_- φ) (j#xs) ∨
   (∃(i,ks) ∈ set(lbounds(Z.atoms⇩₀ φ)). Z.I φ ((i - ⟨ks,xs⟩ + j) # xs)))"
  (is "(∃x. ?P (x)) = (∃ j∈ ?D. ?M j ∨ (∃(i,ks)∈ ?B. ?P (?I i ks + j)))")
proof-
  from min_inf[OF nq u] have th: "∃z.∀x<z. ?P x = ?M x" by blast
  let ?B' = "{?I i ks |i ks. (i,ks) ∈ ?B}"
  have BB': "(∃j∈?D. ∃(i,ks)∈ ?B. ?P (?I i ks + j)) = (∃j ∈ ?D. ∃b ∈ ?B'. ?P (b + j))" by auto
  hence th2: "∀ x. ¬ (∃ j ∈ ?D. ∃ b ∈ ?B'. ?P ((b + j))) ⟶ ?P (x) ⟶ ?P ((x - d))"
    using β[OF nq u d dp, of _ xs] by(simp add:Bex_def) metis
  from min_inf_repeats[OF nq d]
  have th3: "∀ x k. ?M x = ?M (x-k*d)" by simp
  from cpmi_eq[OF dp th th2 th3] BB' show ?thesis by simp blast
qed

(* end of Amine *)

lemma qfree_min_inf[simp]: "qfree φ ⟹ qfree (inf⇩_- φ)"
by (induct φ rule:min_inf.induct) simp_all

lemma I_qe_cooper⇩₁:
assumes norm: "∀a∈atoms φ. divisor a ≠ 0"
and hd: "∀a∈set(Z.atoms⇩₀ φ). hd_coeff_is1 a" and "nqfree φ"
shows "Z.I (qe_cooper⇩₁ φ) xs = (∃x. Z.I φ (x#xs))"
proof -
  let ?as = "Z.atoms⇩₀ φ"
  let ?d = "zlcms(map divisor ?as)"
  have "?d > 0" using norm atoms_subset[of φ] ‹nqfree φ›
    by(fastforce intro:zlcms_pos)
  have alld: "∀a∈set(Z.atoms⇩₀ φ). divisor a dvd ?d" by(simp add:dvd_zlcms)
  from cp_thm[OF ‹nqfree φ› hd alld ‹?d>0›]
  show ?thesis using ‹nqfree φ›
    by (simp add:qe_cooper⇩₁_def I_subst[symmetric] split_def algebra_simps) blast
qed

lemma divisor_hd_coeff1_neq0:
  "qfree φ ⟹ a ∈ atoms φ ⟹ divisor a ≠ 0 ⟹
   divisor (hd_coeff1 (zlcms (map hd_coeff (Z.atoms⇩₀ φ))) a) ≠ 0"
apply (case_tac a)

apply simp
apply(rename_tac list) apply(case_tac list) apply simp apply(simp split:if_split_asm)

apply simp
apply(rename_tac list)apply(case_tac list) apply simp
apply(clarsimp split:if_split_asm)
apply(hypsubst_thin)
apply(subgoal_tac "a ∈ set(map hd_coeff (Z.atoms⇩₀ φ))")
 apply(subgoal_tac "∀i∈set(map hd_coeff (Z.atoms⇩₀ φ)). i ≠ 0")
  apply (metis dvd_zlcms mult_eq_0_iff dvd_mult_div_cancel zlcms0_iff)
 apply (simp add:set_atoms0_iff)
apply(fastforce simp:image_def set_atoms0_iff Bex_def)

apply simp
apply(rename_tac list) apply(case_tac list) apply simp
apply(clarsimp split:if_split_asm)
apply(hypsubst_thin)
apply(subgoal_tac "a ∈ set(map hd_coeff (Z.atoms⇩₀ φ))")
 apply(subgoal_tac "∀i∈set(map hd_coeff (Z.atoms⇩₀ φ)). i ≠ 0")
  apply (metis dvd_zlcms mult_eq_0_iff dvd_mult_div_cancel zlcms0_iff)
 apply (simp add:set_atoms0_iff)
apply(fastforce simp:image_def set_atoms0_iff Bex_def)
done

lemma hd_coeff_is1_hd_coeff1:
  "hd_coeff (hd_coeff1 m a) ≠ 0 ⟶ hd_coeff_is1 (hd_coeff1 m a)"
by (induct a rule: hd_coeff1.induct) (simp_all add:zsgn_def)

lemma I_cooper1_hd_coeffs1: "Z.normal φ ⟹ nqfree φ
       ⟹ Z.I (qe_cooper⇩₁(hd_coeffs1 φ)) xs = (∃x. Z.I φ (x # xs))"
apply(simp add:Z.normal_def)
apply(subst I_qe_cooper⇩₁)
   apply(clarsimp simp:hd_coeffs1_def image_def set_atoms0_iff divisor_hd_coeff1_neq0)
  apply (clarsimp simp:hd_coeffs1_def qfree_map_fm set_atoms0_iff
                     hd_coeff_is1_hd_coeff1)
 apply(simp add:hd_coeffs1_def nqfree_map_fm)
apply(simp add: I_hd_coeffs1)
done

definition "qe_cooper = Z.lift_nnf_qe (qe_cooper⇩₁ ∘ hd_coeffs1)"

lemma qfree_cooper1_hd_coeffs1: "qfree φ ⟹ qfree (qe_cooper⇩₁ (hd_coeffs1 φ))"
by(auto simp:qe_cooper⇩₁_def hd_coeffs1_def qfree_map_fm
        intro!: qfree_or qfree_and qfree_list_disj qfree_min_inf)


lemma normal_min_inf: "Z.normal φ ⟹ Z.normal(inf⇩_- φ)"
by(induct φ rule:min_inf.induct) simp_all

lemma normal_cooper1: "Z.normal φ ⟹ Z.normal(qe_cooper⇩₁ φ)"
by(simp add:qe_cooper⇩₁_def Logic.or_def Z.normal_map_fm normal_min_inf split_def)

lemma normal_hd_coeffs1: "qfree φ ⟹ Z.normal φ ⟹ Z.normal(hd_coeffs1 φ)"
by(auto simp: hd_coeffs1_def image_def set_atoms0_iff
              divisor_hd_coeff1_neq0 Z.normal_def)

theorem I_cooper: "Z.normal φ ⟹  Z.I (qe_cooper φ) xs = Z.I φ xs"
by(simp add:qe_cooper_def Z.I_lift_nnf_qe_normal qfree_cooper1_hd_coeffs1 I_cooper1_hd_coeffs1 normal_cooper1 normal_hd_coeffs1)

theorem qfree_cooper: "qfree (qe_cooper φ)"
by(simp add:qe_cooper_def Z.qfree_lift_nnf_qe qfree_cooper1_hd_coeffs1)

end