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