Theory Infimum_Nat

section ‹Infimum nat lemmas \label{S:infimum-nat}›

theory Infimum_Nat
imports 
  Refinement_Lattice
begin

locale infimum_nat
begin

lemma INF_partition_nat3: 
  fixes f :: "nat ⇒ nat ⇒ 'a::refinement_lattice"
  shows "(⨅j. f i j) =
    (⨅j∈{j. i = j}. f i j) ⊓
    (⨅j∈{j. i < j}. f i j) ⊓
    (⨅j∈{j. j < i}. f i j)"
proof -
  have univ_part: "UNIV = {j. i = j} ∪ {j. i < j} ∪ {j. j < i}" by auto
  have "(⨅j ∈ {j. i = j} ∪ {j. i < j} ∪ {j. j < i}. f i j) =
          (⨅j∈{j. i = j}. f i j) ⊓
          (⨅j∈{j. i < j}. f i j) ⊓
          (⨅j∈{j. j < i}. f i j)" by (metis INF_union)
  with univ_part show ?thesis by simp
qed

lemma INF_INF_partition_nat3: 
  fixes f :: "nat ⇒ nat ⇒ 'a::refinement_lattice"
  shows "(⨅i. ⨅j. f i j) =
    (⨅i. ⨅j∈{j. i = j}. f i j) ⊓
    (⨅i. ⨅j∈{j. i < j}. f i j) ⊓
    (⨅i. ⨅j∈{j. j < i}. f i j)"
proof -
  have "(⨅i. ⨅j. f i j) = (⨅i. ((⨅j∈{j. i = j}. f i j) ⊓
                                  (⨅j∈{j. i < j}. f i j) ⊓
                                  (⨅j∈{j. j < i}. f i j)))"
    by (simp add: INF_partition_nat3)
  also have "... = (⨅i. ⨅j∈{j. i = j}. f i j) ⊓
                   (⨅i. ⨅j∈{j. i < j}. f i j) ⊓
                   (⨅i. ⨅j∈{j. j < i}. f i j)"
    by (simp add: INF_inf_distrib)
  finally show ?thesis .
qed

lemma INF_nat_shift: "(⨅i∈{i. 0 < i}. f i) = (⨅i. f (Suc i))"
  by (metis greaterThan_0 greaterThan_def range_composition)

lemma INF_nat_minus:
  fixes f :: "nat ⇒ 'a::refinement_lattice"
  shows "(⨅j∈{j. i < j}. f (j - i)) = (⨅k∈{k. 0 < k}. f k)"
  apply (rule antisym)
  apply (rule INF_mono, simp)
  apply (metis add.right_neutral add_diff_cancel_left' add_less_cancel_left order_refl)
  apply (rule INF_mono, simp)
  by (meson order_refl zero_less_diff)

(* TODO: generalise to P j i? *)
lemma INF_INF_guarded_switch:
  fixes f :: "nat ⇒ nat ⇒ 'a::refinement_lattice"
  shows "(⨅i. ⨅j∈{j. j < i}. f j (i - j)) = (⨅j. ⨅i∈{i. j < i}. f j (i - j))"
proof (rule antisym)
  have "⋀jj ii. jj < ii ⟹ ∃i. ∃j<i. f j (i - j) ⊑ f jj (ii - jj)"
    by blast
  then have "⋀jj ii. jj < ii ⟹ ∃i. (⨅j∈{j. j < i}. f j (i - j)) ⊑ f jj (ii - jj)"
    by (meson INF_lower mem_Collect_eq)
  then have "⋀jj ii. jj < ii ⟹ (⨅i. ⨅j∈{j. j < i}. f j (i - j)) ⊑ f jj (ii - jj)"
    by (meson UNIV_I INF_lower dual_order.trans)
  then have "⋀jj. (⨅i. ⨅j∈{j. j < i}. f j (i - j)) ⊑ (⨅ii∈{ii. jj < ii}. f jj (ii - jj))"
    by (metis (mono_tags, lifting) INF_greatest mem_Collect_eq)
  then have "(⨅i. ⨅j∈{j. j < i}. f j (i - j)) ⊑ (⨅jj. ⨅ii∈{ii. jj < ii}. f jj (ii - jj))"
    by (simp add: INF_greatest)
  then show "(⨅i. ⨅j∈{j. j < i}. f j (i - j)) ⊑ (⨅j. ⨅i∈{i. j < i}. f j (i - j))"
    by simp
next
  have "⋀ii jj. jj < ii ⟹ ∃j. ∃i>j. f j (i - j) ⊑ f jj (ii - jj)"
    by blast
  then have "⋀ii jj. jj < ii ⟹ ∃j. (⨅i∈{i. j < i}. f j (i - j)) ⊑ f jj (ii - jj)"
    by (meson INF_lower mem_Collect_eq)
  then have "⋀ii jj. jj < ii ⟹ (⨅j. ⨅i∈{i. j < i}. f j (i - j)) ⊑ f jj (ii - jj)"
    by (meson UNIV_I INF_lower dual_order.trans)
  then have "⋀ii. (⨅j. ⨅i∈{i. j < i}. f j (i - j)) ⊑ (⨅jj∈{jj. jj < ii}. f jj (ii - jj))"
    by (metis (mono_tags, lifting) INF_greatest mem_Collect_eq)
  then have "(⨅j. ⨅i∈{i. j < i}. f j (i - j)) ⊑ (⨅ii. ⨅jj∈{jj. jj < ii}. f jj (ii - jj))"
    by (simp add: INF_greatest)
  then show "(⨅j. ⨅i∈{i. j < i}. f j (i - j)) ⊑ (⨅i. ⨅j∈{j. j < i}. f j (i - j))"
    by simp
qed

end

end