Theory IL_IntervalOperators

(*  Title:      IL_IntOperator.thy
    Date:       Jan 2007
    Author:     David Trachtenherz
*)

section ‹Arithmetic operators on natural intervals›

theory IL_IntervalOperators
imports IL_Interval
begin


subsection ‹Arithmetic operations with intervals›

subsubsection ‹Addition of and multiplication by constants›

definition iT_Plus :: "iT ⇒ Time ⇒ iT" (infixl "⊕" 55)
  where "I ⊕ k ≡ (λn.(n + k)) ` I"

definition iT_Mult :: "iT ⇒ Time ⇒ iT" (infixl "⊗" 55)
  where iT_Mult_def : "I ⊗ k ≡ (λn.(n * k)) ` I"

(*<*)
(* Some examples *)
(*
lemma "[…10]⊕5 = {5..15}"
apply (simp only: iIN_0_iTILL_conv[symmetric])
apply (simp add: iT_defs)
apply (simp add: iT_Plus_def)
apply (simp add: image_add_atLeastAtMost)
done

lemma "[1…,2] = {1,2,3}"
apply (simp add: iIN_def)
apply fastforce
done

lemma "[1…,2]⊗2 = {2,4,6}"
apply (simp add: iT_Mult_def iIN_def)
apply auto
done
lemma "[10…]⊗k = {x*k | x. 10 ≤ x}"
apply (simp add: iFROM_def iT_Mult_def)
by blast

lemma "[…4] ⊗ 10 = {0, 10, 20, 30, 40}"
apply (simp add: iT_Mult_def iTILL_def)
by auto
lemma "[…4] ⊗ 10 ⊕ 2 = {2, 12, 22, 32, 42}"
apply (simp add: iT_Plus_def iT_Mult_def iTILL_def)
by auto
*)
(*>*)

lemma iT_Plus_image_conv: "I ⊕ k = (λn.(n + k)) ` I"
by (simp add:  iT_Plus_def)

lemma iT_Mult_image_conv: "I ⊗ k = (λn.(n * k)) ` I"
by (simp add:  iT_Mult_def)

lemma iT_Plus_empty: "{} ⊕ k = {}"
by (simp add: iT_Plus_def)

lemma iT_Mult_empty: "{} ⊗ k = {}"
by (simp add: iT_Mult_def)

lemma iT_Plus_not_empty: "I ≠ {} ⟹ I ⊕ k ≠ {}"
by (simp add: iT_Plus_def)

lemma iT_Mult_not_empty: "I ≠ {} ⟹ I ⊗ k ≠ {}"
by (simp add: iT_Mult_def)


lemma iT_Plus_empty_iff: "(I ⊕ k = {}) = (I = {})"
by (simp add: iT_Plus_def)

lemma iT_Mult_empty_iff: "(I ⊗ k = {}) = (I = {})"
by (simp add: iT_Mult_def)

lemma iT_Plus_mono: "A ⊆ B ⟹ A ⊕ k ⊆ B ⊕ k"
by (simp add: iT_Plus_def image_mono)

lemma iT_Mult_mono: "A ⊆ B ⟹ A ⊗ k ⊆ B ⊗ k"
by (simp add: iT_Mult_def image_mono)


lemma iT_Mult_0: "I ≠ {} ⟹ I ⊗ 0 = […0]"
by (fastforce simp add: iTILL_def iT_Mult_def)

corollary iT_Mult_0_if: "I ⊗ 0 = (if I = {} then {} else […0])"
by (simp add: iT_Mult_empty iT_Mult_0)


lemma iT_Plus_mem_iff: "x ∈ (I ⊕ k) = (k ≤ x ∧ (x - k) ∈ I)"
apply (simp add: iT_Plus_def image_iff)
apply (rule iffI)
 apply fastforce
apply (rule_tac x="x - k" in bexI, simp+)
done

lemma iT_Plus_mem_iff2: "x + k ∈ (I ⊕ k) = (x ∈ I)"
by (simp add: iT_Plus_def image_iff)

lemma iT_Mult_mem_iff_0: "x ∈ (I ⊗ 0) = (I ≠ {} ∧ x = 0)"
apply (case_tac "I = {}")
 apply (simp add: iT_Mult_empty)
apply (simp add: iT_Mult_0 iT_iff)
done

lemma iT_Mult_mem_iff: "
  0 < k ⟹ x ∈ (I ⊗ k) = (x mod k = 0 ∧ x div k ∈ I)"
by (fastforce simp: iT_Mult_def image_iff)

lemma iT_Mult_mem_iff2: "0 < k ⟹ x * k ∈ (I ⊗ k) = (x ∈ I)"
by (simp add: iT_Mult_def image_iff)

lemma iT_Plus_singleton: "{a} ⊕ k = {a + k}"
by (simp add: iT_Plus_def)

lemma iT_Mult_singleton: "{a} ⊗ k = {a * k}"
by (simp add: iT_Mult_def)


lemma iT_Plus_Un: "(A ∪ B) ⊕ k = (A ⊕ k) ∪ (B ⊕ k)"
by (simp add: iT_Plus_def image_Un)

lemma iT_Mult_Un: "(A ∪ B) ⊗ k = (A ⊗ k) ∪ (B ⊗ k)"
by (simp add: iT_Mult_def image_Un)

lemma iT_Plus_Int: "(A ∩ B) ⊕ k = (A ⊕ k) ∩ (B ⊕ k)"
by (simp add: iT_Plus_def image_Int)

lemma iT_Mult_Int: "0 < k ⟹ (A ∩ B) ⊗ k = (A ⊗ k) ∩ (B ⊗ k)"
by (simp add: iT_Mult_def image_Int mult_right_inj)

lemma iT_Plus_image: "f ` I ⊕ n = (λx. f x + n) ` I"
by (fastforce simp: iT_Plus_def)

lemma iT_Mult_image: "f ` I ⊗ n = (λx. f x * n) ` I"
by (fastforce simp: iT_Mult_def)

lemma iT_Plus_commute: "I ⊕ a ⊕ b = I ⊕ b ⊕ a"
by (fastforce simp: iT_Plus_def)

lemma iT_Mult_commute: "I ⊗ a ⊗ b = I ⊗ b ⊗ a"
by (fastforce simp: iT_Mult_def)

lemma iT_Plus_assoc:"I ⊕ a ⊕ b = I ⊕ (a + b)"
by (fastforce simp: iT_Plus_def)

lemma iT_Mult_assoc:"I ⊗ a ⊗ b = I ⊗ (a * b)"
by (fastforce simp: iT_Mult_def)

lemma iT_Plus_Mult_distrib: "I ⊕ n ⊗ m = I ⊗ m ⊕ n * m"
by (simp add: iT_Plus_def iT_Mult_def image_image add_mult_distrib)


(*<*)
lemma "i ⊗ n1 ⊗ n2 ⊗ n3 ⊗ n4 ⊗ n5 ⊗ n6 ⊗ n7 =
  i ⊗ n1 * n2 * n3 * n4 * n5 * n6 * n7"
by (simp add: iT_Mult_assoc)
lemma "i ⊕ n1 ⊕ n2 ⊕ n3 ⊕ n4 ⊕ n5 = i ⊕ n1 + n2 + n3 + n4 + n5"
by (simp add: iT_Plus_assoc)
lemma "i ⊕ n1 ⊗ m ⊕ n2 = i ⊗ m ⊕ n1 * m + n2"
by (simp add: iT_Plus_assoc iT_Plus_Mult_distrib)
lemma "i ⊕ n1 ⊗ m1 ⊗ m2 ⊕ n2 = i ⊗ m1 * m2 ⊕ n1 * m1 * m2 + n2"
by (simp add: iT_Plus_assoc iT_Mult_assoc iT_Plus_Mult_distrib)

lemma "n ∈ I ⊕ k ⟹ k ≤ n"
by (clarsimp simp add: iT_Plus_def)
(*>*)

lemma iT_Plus_finite_iff: "finite (I ⊕ k) = finite I"
by (simp add: iT_Plus_def inj_on_finite_image_iff)

lemma iT_Mult_0_finite: "finite (I ⊗ 0)"
by (simp add: iT_Mult_0_if iTILL_0)

lemma iT_Mult_finite_iff: "0 < k ⟹ finite (I ⊗ k) = finite I"
by (simp add: iT_Mult_def inj_on_finite_image_iff[OF inj_imp_inj_on] mult_right_inj)

lemma iT_Plus_Min: "I ≠ {} ⟹ iMin (I ⊕ k) = iMin I + k"
by (simp add: iT_Plus_def iMin_mono2 mono_def)

lemma iT_Mult_Min: "I ≠ {} ⟹ iMin (I ⊗ k) = iMin I * k"
by (simp add: iT_Mult_def iMin_mono2 mono_def)

lemma iT_Plus_Max: "⟦ finite I; I ≠ {} ⟧ ⟹ Max (I ⊕ k) = Max I + k"
by (simp add: iT_Plus_def Max_mono2 mono_def)

lemma iT_Mult_Max: "⟦ finite I; I ≠ {} ⟧ ⟹ Max (I ⊗ k) = Max I * k"
by (simp add: iT_Mult_def Max_mono2 mono_def)

corollary
  iMOD_mult_0: "[r, mod m] ⊗ 0 = […0]" and
  iMODb_mult_0: "[r, mod m, c] ⊗ 0 = […0]" and
  iFROM_mult_0: "[n…] ⊗ 0 = […0]" and
  iIN_mult_0: "[n…,d] ⊗ 0 = […0]" and
  iTILL_mult_0: "[…n] ⊗ 0 = […0]"
by (simp add: iT_not_empty iT_Mult_0)+

lemmas iT_mult_0 =
  iTILL_mult_0
  iFROM_mult_0
  iIN_mult_0
  iMOD_mult_0
  iMODb_mult_0

lemma iT_Plus_0: "I ⊕ 0 = I"
by (simp add: iT_Plus_def)

lemma iT_Mult_1: "I ⊗ Suc 0 = I"
by (simp add: iT_Mult_def)

corollary
  iFROM_add_Min: "iMin ([n…] ⊕ k) = n + k" and
  iIN_add_Min:   "iMin ([n…,d] ⊕ k) = n + k" and
  iTILL_add_Min: "iMin ([…n] ⊕ k) = k" and
  iMOD_add_Min:  "iMin ([r, mod m] ⊕ k) = r + k" and
  iMODb_add_Min: "iMin ([r, mod m, c] ⊕ k) = r + k"
by (simp add: iT_not_empty iT_Plus_Min iT_Min)+

corollary
  iFROM_mult_Min: "iMin ([n…] ⊗ k) = n * k" and
  iIN_mult_Min:   "iMin ([n…,d] ⊗ k) = n * k" and
  iTILL_mult_Min: "iMin ([…n] ⊗ k) = 0" and
  iMOD_mult_Min:  "iMin ([r, mod m] ⊗ k) = r * k" and
  iMODb_mult_Min: "iMin ([r, mod m, c] ⊗ k) = r * k"
by (simp add: iT_not_empty iT_Mult_Min iT_Min)+


lemmas iT_add_Min =
  iIN_add_Min
  iTILL_add_Min
  iFROM_add_Min
  iMOD_add_Min
  iMODb_add_Min

lemmas iT_mult_Min =
  iIN_mult_Min
  iTILL_mult_Min
  iFROM_mult_Min
  iMOD_mult_Min
  iMODb_mult_Min


lemma iFROM_add: "[n…] ⊕ k = [n+k…]"
by (simp add: iFROM_def iT_Plus_def image_add_atLeast)

lemma iIN_add: "[n…,d] ⊕ k = [n+k…,d]"
by (fastforce simp add: iIN_def iT_Plus_def)

lemma iTILL_add: "[…i] ⊕ k = [k…,i]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_add)

lemma iMOD_add: "[r, mod m] ⊕ k = [r + k, mod m]"
apply (clarsimp simp: set_eq_iff iMOD_def iT_Plus_def image_iff)
apply (rule iffI)
 apply (clarsimp simp: mod_add)
apply (rule_tac x="x - k" in exI)
apply clarsimp
apply (simp add: mod_sub_add)
done

lemma iMODb_add: "[r, mod m, c] ⊕ k = [r + k, mod m, c]"
by (simp add: iMODb_iMOD_iIN_conv iT_Plus_Int iMOD_add iIN_add)

lemmas iT_add =
  iMOD_add
  iMODb_add
  iFROM_add
  iIN_add
  iTILL_add
  iT_Plus_singleton

lemma iFROM_mult: "[n…] ⊗ k = [ n * k, mod k ]"
apply (case_tac "k = 0")
 apply (simp add: iMOD_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (rule conj_cong, simp)
apply (rule iffI)
 apply (drule mult_le_mono1[of _ _ k])
 apply (rule order_trans, assumption)
 apply (simp add: div_mult_cancel)
apply (drule div_le_mono[of _ _ k])
apply simp
done

lemma iIN_mult: "[n…,d] ⊗ k = [ n * k, mod k, d ]"
apply (case_tac "k = 0")
 apply (simp add: iMODb_mod_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (rule conj_cong, simp)
apply (rule iffI)
 apply (elim conjE)
 apply (drule mult_le_mono1[of _ _ k], drule mult_le_mono1[of _ _ k])
 apply (rule conjI)
  apply (rule order_trans, assumption)
  apply (simp add: div_mult_cancel)
 apply (simp add: div_mult_cancel add_mult_distrib mult.commute[of k])
apply (erule conjE)
apply (drule div_le_mono[of _ _ k], drule div_le_mono[of _ _ k])
apply simp
done

lemma iTILL_mult: "[…n] ⊗ k = [ 0, mod k, n ]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_mult)


lemma iMOD_mult: "[r, mod m ] ⊗ k = [ r * k, mod m * k ]"
apply (case_tac "k = 0")
 apply (simp add: iMOD_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (subst mult.commute[of m k])
apply (simp add: mod_mult2_eq)
apply (rule iffI)
 apply (elim conjE)
 apply (drule mult_le_mono1[of _ _ k])
 apply (simp add: div_mult_cancel)
apply (elim conjE)
apply (subgoal_tac "x mod k = 0")
 prefer 2
 apply (drule_tac arg_cong[where f="λx. x mod k"])
 apply (simp add: mult.commute[of k])
apply (drule div_le_mono[of _ _ k])
apply simp
done

lemma iMODb_mult: "
  [r, mod m, c ] ⊗ k = [ r * k, mod m * k, c ]"
apply (case_tac "k = 0")
 apply (simp add: iMODb_mod_0 iT_mult_0 iIN_0 iTILL_0)
apply (subst iMODb_iMOD_iTILL_conv)
apply (simp add: iT_Mult_Int iMOD_mult iTILL_mult iMODb_iMOD_iTILL_conv)
apply (subst Int_assoc[symmetric])
apply (subst Int_absorb2)
 apply (simp add: iMOD_subset)
apply (simp add: iMOD_iTILL_iMODb_conv add_mult_distrib2)
done

lemmas iT_mult =
  iTILL_mult
  iFROM_mult
  iIN_mult
  iMOD_mult
  iMODb_mult
  iT_Mult_singleton


subsubsection ‹Some conversions between intervals using constant addition and multiplication›

lemma iFROM_conv: "[n…] = UNIV ⊕ n"
by (simp add: iFROM_0[symmetric] iFROM_add)

lemma iIN_conv: "[n…,d] = […d] ⊕ n"
by (simp add: iTILL_add)

lemma iMOD_conv: "[r, mod m] = [0…] ⊗ m ⊕ r"
apply (case_tac "m = 0")
 apply (simp add: iMOD_0 iT_mult_0 iTILL_add)
apply (simp add: iFROM_mult iMOD_add)
done

lemma iMODb_conv: "[r, mod m, c] = […c] ⊗ m ⊕ r"
apply (case_tac "m = 0")
 apply (simp add: iMODb_mod_0 iT_mult_0 iTILL_add)
apply (simp add: iTILL_mult iMODb_add)
done


text ‹Some examples showing the utility of iMODb\_conv›
lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp add: iT_defs)
apply safe
defer 1
apply simp+
txt ‹The direct proof without iMODb\_conv fails›
oops

lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def)
apply safe
apply simp+
done

lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def)
apply (simp add: atMost_def)
apply safe
apply simp+
done

lemma "[r, mod m, 4] = {r, r+m, r+2*m, r+3*m, r+4*m}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def atMost_def)
apply (simp add: image_Collect)
apply safe
apply fastforce+
done

lemma "[2, mod 10, 4] = {2, 12, 22, 32, 42}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Plus_def iT_Mult_def)
apply fastforce
done


subsubsection ‹Subtraction of constants›

definition iT_Plus_neg :: "iT ⇒ Time ⇒ iT" (infixl "⊕-" 55) where
  "I ⊕- k ≡ {x. x + k ∈ I}"

lemma iT_Plus_neg_mem_iff: "(x ∈ I ⊕- k) = (x + k ∈ I)"
by (simp add: iT_Plus_neg_def)

lemma iT_Plus_neg_mem_iff2: "k ≤ x ⟹ (x - k ∈ I ⊕- k) = (x ∈ I)"
by (simp add: iT_Plus_neg_def)

lemma iT_Plus_neg_image_conv: "I ⊕- k = (λn.(n - k)) ` (I ↓≥ k)"
apply (simp add: iT_Plus_neg_def cut_ge_def, safe)
apply (rule_tac x="x+k" in image_eqI)
apply simp+
done

lemma iT_Plus_neg_cut_eq: "t ≤ k ⟹ (I ↓≥ t) ⊕- k = I ⊕- k"
by (simp add: set_eq_iff iT_Plus_neg_mem_iff cut_ge_mem_iff)

lemma iT_Plus_neg_mono: "A ⊆ B ⟹ A ⊕- k ⊆ B ⊕- k"
by (simp add: iT_Plus_neg_def subset_iff)

lemma iT_Plus_neg_empty: "{} ⊕- k = {}"
by (simp add: iT_Plus_neg_def)
lemma iT_Plus_neg_Max_less_empty: "
  ⟦ finite I; Max I < k ⟧ ⟹ I ⊕- k = {}"
by (simp add: iT_Plus_neg_image_conv cut_ge_Max_empty)

lemma iT_Plus_neg_not_empty_iff: "(I ⊕- k ≠ {}) = (∃x∈I. k ≤ x)"
by (simp add: iT_Plus_neg_image_conv cut_ge_not_empty_iff)

lemma iT_Plus_neg_empty_iff: "
  (I ⊕- k = {}) = (I = {} ∨ (finite I ∧ Max I < k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_neg_empty)
apply (simp add: iT_Plus_neg_image_conv)
apply (case_tac "infinite I")
 apply (simp add: nat_cut_ge_infinite_not_empty)
apply (simp add: cut_ge_empty_iff)
done

lemma iT_Plus_neg_assoc: "(I ⊕- a) ⊕- b = I ⊕- (a + b)"
apply (simp add: iT_Plus_neg_def)
apply (simp add: add.assoc add.commute[of b])
done

lemma iT_Plus_neg_commute: "I ⊕- a ⊕- b = I ⊕- b ⊕- a"
by (simp add: iT_Plus_neg_assoc add.commute[of b])

lemma iT_Plus_neg_0: "I ⊕- 0 = I"
by (simp add: iT_Plus_neg_image_conv cut_ge_0_all)

lemma iT_Plus_Plus_neg_assoc: "b ≤ a ⟹ I ⊕ a ⊕- b = I ⊕ (a - b)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
 apply fastforce
apply (rule_tac x="x + b" in exI)
apply (simp add: le_diff_conv)
done

lemma iT_Plus_Plus_neg_assoc2: "a ≤ b ⟹ I ⊕ a ⊕- b = I ⊕- (b - a)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
 apply fastforce
apply (clarify, rename_tac x')
apply (rule_tac x="x' + a" in exI)
apply simp
done

lemma iT_Plus_neg_Plus_le_cut_eq: "
  a ≤ b ⟹ (I ⊕- a) ⊕ b = (I ↓≥ a) ⊕ (b - a)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
 apply (clarify, rename_tac x')
 apply (subgoal_tac "x' = x + a - b")
  prefer 2
  apply simp
 apply (simp add: le_imp_diff_le le_add_diff)
apply fastforce
done

corollary iT_Plus_neg_Plus_le_Min_eq: "
  ⟦ a ≤ b; a ≤ iMin I ⟧ ⟹ (I ⊕- a) ⊕ b = I ⊕ (b - a)"
by (simp add: iT_Plus_neg_Plus_le_cut_eq cut_ge_Min_all)

lemma iT_Plus_neg_Plus_ge_cut_eq: "
  b ≤ a ⟹ (I ⊕- a) ⊕ b = (I ↓≥ a) ⊕- (a - b)"
apply (simp add: iT_Plus_neg_image_conv iT_Plus_def cut_cut_ge max_eqL)
apply (subst image_comp)
apply (rule image_cong, simp)
apply (simp add: cut_ge_mem_iff)
done

corollary iT_Plus_neg_Plus_ge_Min_eq: "
  ⟦ b ≤ a; a ≤ iMin I ⟧ ⟹ (I ⊕- a) ⊕ b = I ⊕- (a - b)"
by (simp add: iT_Plus_neg_Plus_ge_cut_eq cut_ge_Min_all)

lemma iT_Plus_neg_Mult_distrib: "
  0 < m ⟹ I ⊕- n ⊗ m = I ⊗ m ⊕- n * m"
apply (clarsimp simp: set_eq_iff iT_Plus_neg_image_conv image_iff iT_Plus_def iT_Mult_def Bex_def cut_ge_mem_iff)
apply (rule iffI)
 apply (clarsimp, rename_tac x')
 apply (rule_tac x="x' * m" in exI)
 apply (simp add: diff_mult_distrib)
apply (clarsimp, rename_tac x')
apply (rule_tac x="x' - n" in exI)
apply (simp add: diff_mult_distrib)
apply fastforce
done

lemma iT_Plus_neg_Plus_le_inverse: "k ≤ iMin I ⟹ I ⊕- k ⊕ k = I"
by (simp add: iT_Plus_neg_Plus_le_Min_eq iT_Plus_0)

lemma iT_Plus_neg_Plus_inverse: "I ⊕- k ⊕ k = I ↓≥ k"
by (simp add: iT_Plus_neg_Plus_ge_cut_eq iT_Plus_neg_0)

lemma iT_Plus_Plus_neg_inverse: "I ⊕ k ⊕- k = I"
by (simp add: iT_Plus_Plus_neg_assoc iT_Plus_0)


lemma iT_Plus_neg_Un: "(A ∪ B) ⊕- k = (A ⊕- k) ∪ (B ⊕- k)"
by (fastforce simp: iT_Plus_neg_def)

lemma iT_Plus_neg_Int: "(A ∩ B) ⊕- k = (A ⊕- k) ∩ (B ⊕- k)"
by (fastforce simp: iT_Plus_neg_def)

lemma iT_Plus_neg_Max_singleton: "⟦ finite I; I ≠ {} ⟧ ⟹ I ⊕- Max I= {0}"
apply (rule set_eqI)
apply (simp add: iT_Plus_neg_def)
apply (case_tac "x = 0")
 apply simp
apply fastforce
done

lemma iT_Plus_neg_singleton: "{a} ⊕- k = (if k ≤ a then {a - k} else {})"
by (force simp add: set_eq_iff iT_Plus_neg_mem_iff singleton_iff)

corollary iT_Plus_neg_singleton1: "k ≤ a ⟹ {a} ⊕- k = {a-k}"
by (simp add: iT_Plus_neg_singleton)

corollary iT_Plus_neg_singleton2: "a < k ⟹ {a} ⊕- k= {}"
by (simp add: iT_Plus_neg_singleton)

lemma iT_Plus_neg_finite_iff: "finite (I ⊕- k) = finite I"
  apply (simp add: iT_Plus_neg_image_conv)
  apply (subst inj_on_finite_image_iff)
  apply (metis cut_geE inj_on_diff_nat)
  apply (simp add: nat_cut_ge_finite_iff)
  done

lemma iT_Plus_neg_Min: "
  I ⊕- k ≠ {} ⟹ iMin (I ⊕- k) = iMin (I ↓≥ k) - k"
apply (simp add: iT_Plus_neg_image_conv)
apply (simp add: iMin_mono2 monoI)
done

lemma iT_Plus_neg_Max: "
  ⟦ finite I; I ⊕- k ≠ {} ⟧ ⟹ Max (I ⊕- k) = Max I - k"
apply (simp add: iT_Plus_neg_image_conv)
apply (simp add: Max_mono2 monoI cut_ge_finite cut_ge_Max_eq)
done


text ‹Subtractions of constants from intervals›

lemma iFROM_add_neg: "[n…] ⊕- k = [n - k…]"
by (fastforce simp: set_eq_iff iT_Plus_neg_mem_iff)

lemma iTILL_add_neg: "[…n] ⊕- k = (if k ≤ n then […n - k] else {})"
by (force simp add: set_eq_iff iT_Plus_neg_mem_iff iT_iff)
lemma iTILL_add_neg1: "k ≤ n ⟹ […n] ⊕- k = […n-k]"
by (simp add: iTILL_add_neg)
lemma iTILL_add_neg2: "n < k ⟹ […n] ⊕- k = {}"
by (simp add: iTILL_add_neg)

lemma iIN_add_neg: "
  [n…,d] ⊕- k = (
    if k ≤ n then [n - k…,d]
    else if k ≤ n + d then […n + d - k] else {})"
by (simp add: iIN_iFROM_iTILL_conv iT_Plus_neg_Int iFROM_add_neg iTILL_add_neg iFROM_0)

lemma iIN_add_neg1: "k ≤ n ⟹ [n…,d] ⊕- k = [n - k…,d]"
by (simp add: iIN_add_neg)

lemma iIN_add_neg2: "⟦ n ≤ k; k ≤ n + d ⟧ ⟹ [n…,d] ⊕- k = […n + d - k]"
by (simp add: iIN_add_neg iIN_0_iTILL_conv)

lemma iIN_add_neg3: "n + d < k ⟹ [n…,d] ⊕- k = {}"
by (simp add: iT_Plus_neg_Max_less_empty iT_finite iT_Max)

lemma iMOD_0_add_neg: "[r, mod 0] ⊕- k = {r} ⊕- k"
by (simp add: iMOD_0 iIN_0)

(*
lemma "[25, mod 10] ⊕- 32 = [3, mod 10]"
apply (rule set_eqI)
apply (simp add: iT_Plus_neg_mem_iff iMOD_iff)
apply (simp add: mod_add_eq[of _ 32] mod_Suc)
apply clarify
apply (rule iffI)
apply simp+
done
*)

lemma iMOD_gr0_add_neg: "
  0 < m ⟹
  [r, mod m] ⊕- k = (
    if k ≤ r then [r - k, mod m]
    else [(m + r mod m - k mod m) mod m, mod m])"
apply (rule set_eqI)
apply (simp add: iMOD_def iT_Plus_neg_def)
apply (simp add: eq_sym_conv[of _ "r mod m"])
apply (intro conjI impI)
 apply (simp add: eq_sym_conv[of _ "(r - k) mod m"] mod_sub_add le_diff_conv)
apply (simp add: eq_commute[of "r mod m"] mod_add_eq_mod_conv)
apply safe
apply (drule sym)
apply simp
done

lemma iMOD_add_neg: "
  [r, mod m] ⊕- k = (
    if k ≤ r then [r - k, mod m]
    else if 0 < m then [(m + r mod m - k mod m) mod m, mod m] else {})"
apply (case_tac "0 < m")
 apply (simp add: iMOD_gr0_add_neg)
apply (simp add: iMOD_0 iIN_0 iT_Plus_neg_singleton)
done

corollary iMOD_add_neg1: "
  k ≤ r ⟹ [r, mod m] ⊕- k = [r - k, mod m]"
by (simp add: iMOD_add_neg)

lemma iMOD_add_neg2: "
  ⟦ 0 < m; r < k ⟧ ⟹ [r, mod m] ⊕- k = [(m + r mod m - k mod m) mod m, mod m]"
by (simp add: iMOD_add_neg)


lemma iMODb_mod_0_add_neg: "[r, mod 0, c] ⊕- k = {r} ⊕- k"
by (simp add: iMODb_mod_0 iIN_0)

(*
lemma "[25, mod 10, 5] ⊕- 32 = [3, mod 10, 4]"
apply (rule set_eqI)
apply (simp add: iMODb_conv iT_Plus_neg_mem_iff iT_Plus_mem_iff iT_Mult_mem_iff)
apply (case_tac "x < 3", simp)
apply (simp add: linorder_not_less)
apply (rule_tac t="(x - 3) mod 10 = 0" and s="x mod 10 = 3" in subst)
 apply (simp add: mod_eq_diff_mod_0_conv[symmetric])
apply (rule_tac t="(7 + x) mod 10 = 0" and s="x mod 10 = 3" in subst)
 apply (simp add: mod_add1_eq_if[of 7])
apply (rule conj_cong[OF refl])
apply (simp add: div_add1_eq_if)
apply (simp add: div_diff1_eq1)
apply (simp add: iTILL_iff)
done

lemma "[25, mod 10, 5] ⊕- 32 = [3, mod 10, 4]"
apply (simp add: iT_Plus_neg_image_conv iMODb_cut_ge)
apply (simp add: iMODb_conv iT_Mult_def iT_Plus_def)
apply (rule_tac t=4 and s="Suc(Suc(Suc(Suc 0)))" in subst, simp)
apply (simp add: iTILL_def atMost_Suc)
done
*)

lemma iMODb_add_neg: "
  [r, mod m, c] ⊕- k = (
    if k ≤ r then [r - k, mod m, c]
    else
      if k ≤ r + m * c then
      [(m + r mod m - k mod m) mod m, mod m, (r + m * c - k) div m]
      else {})"
apply (clarsimp simp add: iMODb_iMOD_iIN_conv iT_Plus_neg_Int iMOD_add_neg iIN_add_neg)
apply (simp add: iMOD_iIN_iMODb_conv)
apply (rule_tac t="(m + r mod m - k mod m) mod m" and s="(r + m * c - k) mod m" in subst)
 apply (simp add: mod_diff1_eq[of k])
apply (subst iMOD_iTILL_iMODb_conv, simp)
apply (subst sub_mod_div_eq_div, simp)
done

lemma iMODb_add_neg': "
  [r, mod m, c] ⊕- k = (
    if k ≤ r then [r - k, mod m, c]
    else if k ≤ r + m * c then
      if k mod m ≤ r mod m
        then [ r mod m - k mod m, mod m, c + r div m - k div m]
        else [ m + r mod m - k mod m, mod m, c + r div m - Suc (k div m) ]
      else {})"
apply (clarsimp simp add: iMODb_add_neg)
apply (case_tac "m = 0", simp+)
apply (case_tac "k mod m ≤ r mod m")
 apply (clarsimp simp: linorder_not_le)
 apply (simp add: divisor_add_diff_mod_if)
 apply (simp add: div_diff1_eq_if)
apply (clarsimp simp: linorder_not_le)
apply (simp add:  div_diff1_eq_if)
done

corollary iMODb_add_neg1: "
  k ≤ r ⟹ [r, mod m, c] ⊕- k = [r - k, mod m, c]"
by (simp add: iMODb_add_neg)

corollary iMODb_add_neg2: "
  ⟦ r < k; k ≤ r + m * c ⟧ ⟹
  [r, mod m, c] ⊕- k =
  [(m + r mod m - k mod m) mod m, mod m, (r + m * c - k) div m]"
by (simp add: iMODb_add_neg)

corollary iMODb_add_neg2_mod_le: "
  ⟦ r < k; k ≤ r + m * c; k mod m ≤ r mod m ⟧ ⟹
  [r, mod m, c] ⊕- k =
  [ r mod m - k mod m, mod m, c + r div m - k div m]"
by (simp add: iMODb_add_neg')

corollary iMODb_add_neg2_mod_less: "
  ⟦ r < k; k ≤ r + m * c; r mod m < k mod m⟧ ⟹
  [r, mod m, c] ⊕- k =
  [ m + r mod m - k mod m, mod m, c + r div m - Suc (k div m) ]"
by (simp add: iMODb_add_neg')

lemma iMODb_add_neg3: "r + m * c < k  ⟹ [r, mod m, c] ⊕- k = {}"
by (simp add: iMODb_add_neg)

lemmas iT_add_neg =
  iFROM_add_neg
  iIN_add_neg
  iTILL_add_neg
  iMOD_add_neg
  iMODb_add_neg
  iT_Plus_neg_singleton


subsubsection ‹Subtraction of intervals from constants›

definition iT_Minus :: "Time ⇒ iT ⇒ iT" (infixl "⊖" 55)
  where "k ⊖ I ≡ {x. x ≤ k ∧ (k - x) ∈ I}"

lemma iT_Minus_mem_iff: "(x ∈ k ⊖ I) = (x ≤ k ∧ k - x ∈ I)"
by (simp add: iT_Minus_def)

lemma iT_Minus_mono: "A ⊆ B ⟹ k ⊖ A ⊆ k ⊖ B"
by (simp add: subset_iff iT_Minus_mem_iff)

lemma iT_Minus_image_conv: "k ⊖ I = (λx. k - x) ` (I ↓≤ k)"
by (fastforce simp: iT_Minus_def cut_le_def image_iff)

lemma iT_Minus_cut_eq: "k ≤ t ⟹ k ⊖ (I ↓≤ t) = k ⊖ I"
by (fastforce simp: set_eq_iff iT_Minus_mem_iff)

lemma iT_Minus_Minus_cut_eq: "k ⊖ (k ⊖ (I ↓≤ k)) = I ↓≤ k"
by (fastforce simp: iT_Minus_def)

lemma "10 ⊖ […3] = [7…,3]"
by (fastforce simp: iT_Minus_def)

lemma iT_Minus_empty: "k ⊖ {} = {}"
by (simp add: iT_Minus_def)

lemma iT_Minus_0: "k ⊖ {0} = {k}"
by (simp add: iT_Minus_image_conv cut_le_def image_Collect)

lemma iT_Minus_bound: "x ∈ k ⊖ I ⟹ x ≤ k"
by (simp add: iT_Minus_def)

lemma iT_Minus_finite: "finite (k ⊖ I)"
apply (rule finite_nat_iff_bounded_le2[THEN iffD2])
apply (rule_tac x=k in exI)
apply (simp add: iT_Minus_bound)
done

lemma iT_Minus_less_Min_empty: "k < iMin I ⟹ k ⊖ I = {}"
by (simp add: iT_Minus_image_conv cut_le_Min_empty)

lemma iT_Minus_Min_singleton: "I ≠ {} ⟹ (iMin I) ⊖ I = {0}"
apply (rule set_eqI)
apply (simp add: iT_Minus_mem_iff)
apply (fastforce intro: iMinI_ex2)
done

lemma iT_Minus_empty_iff: "(k ⊖ I = {}) = (I = {} ∨ k < iMin I)"
apply (case_tac "I = {}", simp add: iT_Minus_empty)
apply (simp add: iT_Minus_image_conv cut_le_empty_iff iMin_gr_iff)
done


(*
An example:
  100 ⊖ {60, 70, 80, 90, 95} = {5, 10, 20, 30, 40}
  imirror {60, 70, 80, 90, 95} = {60, 65, 75, 95, 95}
  {60, 65, 75, 85, 95} ⊕ 100 ⊕- (60 + 95)
  = {160, 165, 175, 185, 195} ⊕- 155
  = {5, 10, 20, 30, 40}

I ⊕ k ⊕- (iMin I + Max I))
*)
lemma iT_Minus_imirror_conv: "
  k ⊖ I = imirror (I ↓≤ k) ⊕ k ⊕- (iMin I + Max (I ↓≤ k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty cut_le_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (case_tac "k < iMin I")
 apply (simp add: iT_Minus_less_Min_empty cut_le_Min_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (simp add: linorder_not_less)
apply (frule cut_le_Min_not_empty[of _ k], assumption)
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_neg_image_conv iT_Plus_neg_mem_iff iT_Plus_mem_iff imirror_iff image_iff Bex_def i_cut_mem_iff cut_le_Min_eq)
apply (rule iffI)
 apply (clarsimp, rename_tac x')
 apply (rule_tac x="k - x' + iMin I + Max (I ↓≤ k)" in exI, simp)
 apply (simp add: add.assoc le_add_diff)
 apply (simp add: add.commute[of k] le_add_diff nat_cut_le_finite cut_leI trans_le_add2)
 apply (rule_tac x=x' in exI, simp)
apply (clarsimp, rename_tac x1 x2)
apply (rule_tac x=x2 in exI)
apply simp
apply (drule add_right_cancel[THEN iffD2, of _ _ k], simp)
apply (simp add: trans_le_add2 nat_cut_le_finite cut_le_mem_iff)
done

lemma iT_Minus_imirror_conv': "
  k ⊖ I = imirror (I ↓≤ k) ⊕ k ⊕- (iMin (I ↓≤ k) + Max (I ↓≤ k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty cut_le_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (case_tac "k < iMin I")
 apply (simp add: iT_Minus_less_Min_empty cut_le_Min_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (simp add: cut_le_Min_not_empty cut_le_Min_eq iT_Minus_imirror_conv)
done

lemma iT_Minus_Max: "
  ⟦ I ≠ {}; iMin I ≤ k ⟧ ⟹ Max (k ⊖ I) = k - (iMin I)"
apply (rule Max_equality)
  apply (simp add: iT_Minus_mem_iff iMinI_ex2)
 apply (simp add: iT_Minus_finite)
apply (fastforce simp: iT_Minus_def)
done

lemma iT_Minus_Min: "
  ⟦ I ≠ {}; iMin I ≤ k ⟧ ⟹ iMin (k ⊖ I) = k - (Max (I ↓≤ k))"
apply (insert nat_cut_le_finite[of I k])
apply (frule cut_le_Min_not_empty[of _ k], assumption)
apply (rule iMin_equality)
 apply (simp add: iT_Minus_mem_iff nat_cut_le_Max_le del: Max_le_iff)
 apply (simp add: subsetD[OF cut_le_subset, OF Max_in])
apply (clarsimp simp add: iT_Minus_image_conv image_iff, rename_tac x')
apply (rule diff_le_mono2)
apply (simp add: Max_ge_iff cut_le_mem_iff)
done

lemma iT_Minus_Minus_eq: "⟦ finite I; Max I ≤ k ⟧ ⟹ k ⊖ (k ⊖ I) = I"
apply (simp add: iT_Minus_cut_eq[of k k I, symmetric] iT_Minus_Minus_cut_eq)
apply (simp add: cut_le_Max_all)
done

lemma iT_Minus_Minus_eq2: "I ⊆ […k] ⟹ k ⊖ (k ⊖ I) = I"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty)
apply (rule iT_Minus_Minus_eq)
 apply (simp add: finite_subset iTILL_finite)
apply (frule Max_subset)
apply (simp add: iTILL_finite iTILL_Max)+
done

(* An example:
  10 ⊖ (100 ⊖ {97,98,99,101,102}) = {7,8,9}
  1000 ⊖ (100 ⊖ {97,98,99,101,102, 998,1002}) = {997,998,999}
*)
lemma iT_Minus_Minus: "a ⊖ (b ⊖ I) = (I ↓≤ b) ⊕ a ⊕- b"
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_image_conv iT_Plus_neg_image_conv image_iff Bex_def i_cut_mem_iff)
apply fastforce
done

lemma iT_Minus_Plus_empty: "k < n ⟹ k ⊖ (I ⊕ n) = {}"
apply (case_tac "I = {}")
 apply (simp add: iT_Plus_empty iT_Minus_empty)
apply (simp add: iT_Minus_empty_iff iT_Plus_empty_iff iT_Plus_Min)
done
lemma iT_Minus_Plus_commute: "n ≤ k ⟹ k ⊖ (I ⊕ n) = (k - n) ⊖ I"
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_image_conv image_iff Bex_def i_cut_mem_iff)
apply fastforce
done

lemma iT_Minus_Plus_cut_assoc: "(k ⊖ I) ⊕ n = (k + n) ⊖ (I ↓≤ k)"
apply (rule set_eqI)
apply (simp add: iT_Plus_mem_iff iT_Minus_mem_iff cut_le_mem_iff)
apply fastforce
done

lemma iT_Minus_Plus_assoc: "
  ⟦ finite I; Max I ≤ k ⟧ ⟹ (k ⊖ I) ⊕ n = (k + n) ⊖ I"
by (insert iT_Minus_Plus_cut_assoc[of k I n], simp add: cut_le_Max_all)
lemma iT_Minus_Plus_assoc2: "
  I ⊆ […k] ⟹ (k ⊖ I) ⊕ n = (k + n) ⊖ I"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty iT_Plus_empty)
apply (rule iT_Minus_Plus_assoc)
 apply (simp add: finite_subset iTILL_finite)
apply (frule Max_subset)
apply (simp add: iTILL_finite iTILL_Max)+
done


lemma iT_Minus_Un: "k ⊖ (A ∪ B) = (k ⊖ A) ∪ (k ⊖ B)"
by (fastforce simp: iT_Minus_def)

lemma iT_Minus_Int: "k ⊖ (A ∩ B) = (k ⊖ A) ∩ (k ⊖ B)"
by (fastforce simp: set_eq_iff iT_Minus_mem_iff)

lemma iT_Minus_singleton: "k ⊖ {a} = (if a ≤ k then {k - a} else {})"
by (simp add: iT_Minus_image_conv cut_le_singleton)
corollary iT_Minus_singleton1: "a ≤ k ⟹ k ⊖ {a} = {k-a}"
by (simp add: iT_Minus_singleton)
corollary iT_Minus_singleton2: "k < a ⟹ k ⊖ {a} = {}"
by (simp add: iT_Minus_singleton)


lemma iMOD_sub: "
  k ⊖ [r, mod m] =
  (if r ≤ k then [(k - r) mod m, mod m, (k - r) div m] else {})"
apply (rule set_eqI)
apply (simp add: iT_Minus_mem_iff iT_iff)
apply (fastforce simp add: mod_sub_eq_mod_swap[of r, symmetric])
done

corollary iMOD_sub1: "
  r ≤ k ⟹ k ⊖ [r, mod m] = [(k - r) mod m, mod m, (k - r) div m]"
by (simp add: iMOD_sub)

corollary iMOD_sub2: "k < r ⟹ k ⊖ [r, mod m] = {}"
apply (rule iT_Minus_less_Min_empty)
apply (simp add: iMOD_Min)
done


lemma iTILL_sub: "k ⊖ […n] = (if n ≤ k then [k - n…,n] else […k])"
by (force simp add: set_eq_iff iT_Minus_mem_iff iT_iff)

corollary iTILL_sub1: "n ≤ k ⟹ k ⊖ […n] = [k - n…,n]"
by (simp add: iTILL_sub)

corollary iTILL_sub2: "k ≤ n ⟹ k ⊖ […n] = […k]"
by (simp add: iTILL_sub iIN_0_iTILL_conv)

(* An example: 30 ⊖ [2, mod 10] = {8,18,28} *)
lemma iMODb_sub: "
  k ⊖ [r, mod m, c] = (
    if r + m * c ≤ k then [ k - r - m * c, mod m, c] else
      if r ≤ k then [ (k - r) mod m, mod m, (k - r) div m] else {})"
apply (case_tac "m = 0")
 apply (simp add: iMODb_mod_0 iIN_0 iT_Minus_singleton)
apply (subst iMODb_iMOD_iTILL_conv)
apply (subst iT_Minus_Int)
apply (simp add: iMOD_sub iTILL_sub)
apply (intro conjI impI)
 apply simp
 apply (subgoal_tac "(k - r) mod m ≤ k - (r + m * c)")
  prefer 2
  apply (subgoal_tac "m * c ≤ k - r - (k - r) mod m")
   prefer 2
   apply (drule add_le_imp_le_diff2)
   apply (drule div_le_mono[of _ _ m], simp)
   apply (drule mult_le_mono2[of _ _ m])
   apply (simp add: minus_mod_eq_mult_div [symmetric])
  apply (simp add: le_diff_conv2[OF mod_le_dividend] del: diff_diff_left)
 apply (subst iMODb_iMOD_iIN_conv)
 apply (simp add: Int_assoc minus_mod_eq_mult_div [symmetric])
 apply (subst iIN_inter, simp+)
 apply (rule set_eqI)
 apply (fastforce simp add: iT_iff mod_diff_mult_self2 diff_diff_left[symmetric] simp del: diff_diff_left)
apply (simp add: Int_absorb2 iMODb_iTILL_subset)
done

corollary iMODb_sub1: "
  ⟦ r ≤ k; k ≤ r + m * c ⟧ ⟹
  k ⊖ [r, mod m, c] = [(k - r) mod m, mod m, (k - r) div m]"
by (clarsimp simp: iMODb_sub iMODb_mod_0)

corollary iMODb_sub2: "k < r ⟹ k ⊖ [r, mod m, c] = {}"
apply (rule iT_Minus_less_Min_empty)
apply (simp add: iMODb_Min)
done

corollary iMODb_sub3: "
  r + m * c ≤ k ⟹ k ⊖ [r, mod m, c] = [ k - r - m * c, mod m, c]"
by (simp add: iMODb_sub)

lemma iFROM_sub: "k ⊖ [n…] = (if n ≤ k then […k - n] else {})"
by (simp add: iMOD_1[symmetric] iMOD_sub iMODb_mod_1 iIN_0_iTILL_conv)

corollary iFROM_sub1: "n ≤ k ⟹ k ⊖ [n…] = […k-n]"
by (simp add: iFROM_sub)

corollary iFROM_sub_empty: "k < n ⟹ k ⊖ [n…] = {}"
by (simp add: iFROM_sub)


(* Examples:
  10 ⊖ [2…,3] = {3,4,5,6,7,8}
  10 ⊖ [7…,5] = {0,1,2,3}
*)
lemma iIN_sub: "
  k ⊖ [n…,d] = (
  if n + d ≤ k then [k - (n + d)…,d]
  else if n ≤ k then […k - n] else {})"
apply (simp add: iMODb_mod_1[symmetric] iMODb_sub)
apply (simp add: iMODb_mod_1 iIN_0_iTILL_conv)
done

lemma iIN_sub1: "n + d ≤ k ⟹ k ⊖ [n…,d] = [k - (n + d)…,d]"
by (simp add: iIN_sub)

lemma iIN_sub2: "⟦ n ≤ k; k ≤ n + d ⟧ ⟹ k ⊖ [n…,d] = […k - n]"
by (clarsimp simp: iIN_sub iIN_0_iTILL_conv)

lemma iIN_sub3: "k < n ⟹ k ⊖ [n…,d] = {}"
by (simp add: iIN_sub)

lemmas iT_sub =
  iFROM_sub
  iIN_sub
  iTILL_sub
  iMOD_sub
  iMODb_sub
  iT_Minus_singleton


subsubsection ‹Division of intervals by constants›

text ‹Monotonicity and injectivity of artithmetic operators›

lemma iMOD_div_right_strict_mono_on: "
  ⟦ 0 < k; k ≤ m ⟧ ⟹ strict_mono_on (λx. x div k) [r, mod m]"
apply (rule div_right_strict_mono_on, assumption)
apply (clarsimp simp: iT_iff)
apply (drule_tac s="y mod m" in sym, simp)
apply (rule_tac y="x + m" in order_trans, simp)
apply (simp add: less_mod_eq_imp_add_divisor_le)
done

corollary iMOD_div_right_inj_on: "
  ⟦ 0 < k; k ≤ m ⟧ ⟹ inj_on (λx. x div k) [r, mod m]"
by (rule strict_mono_on_imp_inj_on[OF iMOD_div_right_strict_mono_on])

lemma iMOD_mult_div_right_inj_on: "
  inj_on (λx. x div (k::nat)) [r, mod (k * m)]"
apply (case_tac "k * m = 0")
 apply (simp del: mult_is_0 mult_eq_0_iff add: iMOD_0 iIN_0)
apply (simp add: iMOD_div_right_inj_on)
done

lemma iMOD_mult_div_right_inj_on2: "
  m mod k = 0 ⟹ inj_on (λx. x div k) [r, mod m]"
  by (auto simp add: iMOD_mult_div_right_inj_on)

lemma iMODb_div_right_strict_mono_on: "
  ⟦ 0 < k; k ≤ m ⟧ ⟹ strict_mono_on (λx. x div k) [r, mod m, c]"
by (rule strict_mono_on_subset[OF iMOD_div_right_strict_mono_on iMODb_iMOD_subset_same])

corollary iMODb_div_right_inj_on: "
  ⟦ 0 < k; k ≤ m ⟧ ⟹ inj_on (λx. x div k) [r, mod m, c]"
by (rule strict_mono_on_imp_inj_on[OF iMODb_div_right_strict_mono_on])

lemma iMODb_mult_div_right_inj_on: "
  inj_on (λx. x div (k::nat)) [r, mod (k * m), c]"
by (rule subset_inj_on[OF iMOD_mult_div_right_inj_on iMODb_iMOD_subset_same])

corollary iMODb_mult_div_right_inj_on2: "
  m mod k = 0 ⟹ inj_on (λx. x div k) [r, mod m, c]"
  by (auto simp add: iMODb_mult_div_right_inj_on)


definition iT_Div :: "iT ⇒ Time ⇒ iT" (infixl "⊘" 55)
  where "I ⊘ k ≡ (λn.(n div k)) ` I"

lemma iT_Div_image_conv: "I ⊘ k = (λn.(n div k)) ` I"
by (simp add: iT_Div_def)

lemma iT_Div_mono: "A ⊆ B ⟹ A ⊘ k ⊆ B ⊘ k"
by (simp add: iT_Div_def image_mono)

lemma iT_Div_empty: "{} ⊘ k = {}"
by (simp add: iT_Div_def)
lemma iT_Div_not_empty: "I ≠ {} ⟹ I ⊘ k ≠ {}"
by (simp add: iT_Div_def)

lemma iT_Div_empty_iff: "(I ⊘ k = {}) = (I = {})"
by (simp add: iT_Div_def)


lemma iT_Div_0: "I ≠ {} ⟹ I ⊘ 0 = […0]"
by (force simp: iT_Div_def)
corollary iT_Div_0_if: "I ⊘ 0 = (if I = {} then {} else […0])"
by (force simp: iT_Div_def)
corollary
  iFROM_div_0: "[n…] ⊘ 0 = […0]" and
  iTILL_div_0: "[…n] ⊘ 0 = […0]" and
  iIN_div_0: "[n…,d] ⊘ 0 = […0]" and
  iMOD_div_0: "[r, mod m] ⊘ 0 = […0]" and
  iMODb_div_0: "[r, mod m, c] ⊘ 0 = […0]"
by (simp add: iT_Div_0 iT_not_empty)+

lemmas iT_div_0 =
  iTILL_div_0
  iFROM_div_0
  iIN_div_0
  iMOD_div_0
  iMODb_div_0

lemma iT_Div_1: "I ⊘ Suc 0 = I"
by (simp add: iT_Div_def)

lemma iT_Div_mem_iff_0: "x ∈ (I ⊘ 0) = (I ≠ {} ∧ x = 0)"
by (force simp: iT_Div_0_if)

lemma iT_Div_mem_iff: "
  0 < k ⟹ x ∈ (I ⊘ k) = (∃y ∈ I. y div k = x)"
by (force simp: iT_Div_def)

lemma iT_Div_mem_iff2: "
  0 < k ⟹ x div k ∈ (I ⊘ k) = (∃y ∈ I. y div k = x div k)"
by (rule iT_Div_mem_iff)

lemma iT_Div_mem_iff_Int: "
  0 < k ⟹ x ∈ (I ⊘ k) = (I ∩ [x * k…,k - Suc 0] ≠ {})"
apply (simp add: ex_in_conv[symmetric] iT_Div_mem_iff iT_iff)
apply (simp add: le_less_div_conv[symmetric] add.commute[of k])
apply (subst less_eq_le_pred, simp)
apply blast
done

lemma iT_Div_imp_mem: "
  0 < k ⟹ x ∈ I ⟹ x div k ∈ (I ⊘ k)"
by (force simp: iT_Div_mem_iff2)

lemma iT_Div_singleton: "{a} ⊘ k = {a div k}"
by (simp add: iT_Div_def)


lemma iT_Div_Un: "(A ∪ B) ⊘ k = (A ⊘ k) ∪ (B ⊘ k)"
by (fastforce simp: iT_Div_def)

lemma iT_Div_insert: "(insert n I) ⊘ k = insert (n div k) (I ⊘ k)"
by (fastforce simp: iT_Div_def)

(* Examples:
  {1,2,3,4} ⊘ 3 ∩ {5,6,7} ⊘ 3 = {0,1} ∩ {1,2} = {1}
  ({1,2,3,4} ∩ {5,6,7}) ⊘ 3 = {} ⊘ 3 = {}
*)
lemma not_iT_Div_Int: "¬ (∀ k A B. (A ∩ B) ⊘ k = (A ⊘ k) ∩ (B ⊘ k))"
apply simp
apply (
  rule_tac x=3 in exI,
  rule_tac x="{0}" in exI,
  rule_tac x="{1}" in exI)
by (simp add: iT_Div_def)

lemma subset_iT_Div_Int: "A ⊆ B ⟹ (A ∩ B) ⊘ k = (A ⊘ k) ∩ (B ⊘ k)"
by (simp add: iT_Div_def subset_image_Int)

lemma iFROM_iT_Div_Int: "
  ⟦ 0 < k; n ≤ iMin A ⟧ ⟹ (A ∩ [n…]) ⊘ k = (A ⊘ k) ∩ ([n…] ⊘ k)"
apply (rule subset_iT_Div_Int)
apply (blast intro: order_trans iMin_le)
done

lemma iIN_iT_Div_Int: "
  ⟦ 0 < k; n ≤ iMin A; ∀x∈A. x div k ≤ (n + d) div k ⟶ x ≤ n + d ⟧ ⟹
  (A ∩ [n…,d]) ⊘ k = (A ⊘ k) ∩ ([n…,d] ⊘ k)"
apply (rule set_eqI)
apply (simp add: iT_Div_mem_iff Bex_def iIN_iff)
apply (rule iffI)
 apply blast
apply (clarsimp, rename_tac x1 x2)
apply (frule iMin_le)
apply (rule_tac x=x1 in exI, simp)
apply (drule_tac x=x1 in bspec, simp)
apply (drule div_le_mono[of _ "n + d" k])
apply simp
done
corollary iTILL_iT_Div_Int: "
  ⟦ 0 < k; ∀x∈A. x div k ≤ n div k ⟶ x ≤ n ⟧ ⟹
  (A ∩ […n]) ⊘ k = (A ⊘ k) ∩ ([…n] ⊘ k)"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_iT_Div_Int)
lemma iIN_iT_Div_Int_mod_0: "
  ⟦ 0 < k; n mod k = 0; ∀x∈A. x div k ≤ (n + d) div k ⟶ x ≤ n + d ⟧ ⟹
  (A ∩ [n…,d]) ⊘ k = (A ⊘ k) ∩ ([n…,d] ⊘ k)"
apply (rule set_eqI)
apply (simp add: iT_Div_mem_iff Bex_def iIN_iff)
apply (rule iffI)
 apply blast
apply (elim conjE exE, rename_tac x1 x2)
apply (rule_tac x=x1 in exI, simp)
apply (rule conjI)
 apply (rule ccontr, simp add: linorder_not_le)
 apply (drule_tac m=n and n=x2 and k=k in div_le_mono)
 apply (drule_tac a=x1 and m=k in less_mod_0_imp_div_less)
 apply simp+
apply (drule_tac x=x1 in bspec, simp)
apply (drule div_le_mono[of _ "n + d" k])
apply simp
done

lemma mod_partition_iT_Div_Int: "
  ⟦ 0 < k; 0 < d ⟧ ⟹
  (A ∩ [n * k…,d * k - Suc 0]) ⊘ k =
  (A ⊘ k) ∩ ([n * k…,d * k - Suc 0] ⊘ k)"
apply (rule iIN_iT_Div_Int_mod_0, simp+)
apply (clarify, rename_tac x)
apply (simp add: mod_0_imp_sub_1_div_conv)
apply (rule ccontr, simp add: linorder_not_le pred_less_eq_le)
apply (drule_tac n=x and k=k in div_le_mono)
apply simp
done

(*<*)
lemma "{0,1,2} ⊗ x = {0*x, 1*x, 2*x}"
by (simp add: iT_Mult_def)
(*>*)

corollary mod_partition_iT_Div_Int2: "
  ⟦ 0 < k; 0 < d; n mod k = 0; d mod k = 0 ⟧ ⟹
  (A ∩ [n…,d - Suc 0]) ⊘ k =
  (A ⊘ k) ∩ ([n…,d - Suc 0] ⊘ k)"
  by (auto simp add: ac_simps mod_partition_iT_Div_Int elim!: dvdE)

corollary mod_partition_iT_Div_Int_one_segment: "
  0 < k ⟹
  (A ∩ [n * k…,k - Suc 0]) ⊘ k = (A ⊘ k) ∩ ([n * k…,k - Suc 0] ⊘ k)"
by (insert mod_partition_iT_Div_Int[where d=1], simp)

corollary mod_partition_iT_Div_Int_one_segment2: "
  ⟦ 0 < k; n mod k = 0 ⟧ ⟹
  (A ∩ [n…,k - Suc 0]) ⊘ k = (A ⊘ k) ∩ ([n…,k - Suc 0] ⊘ k)"
  using mod_partition_iT_Div_Int2[where k=k and d=k and n=n]
by (insert mod_partition_iT_Div_Int2[where k=k and d=k and n=n], simp)


lemma iT_Div_assoc:"I ⊘ a ⊘ b = I ⊘ (a * b)"
by (simp add: iT_Div_def image_image div_mult2_eq)

lemma iT_Div_commute: "I ⊘ a ⊘ b = I ⊘ b ⊘ a"
by (simp add: iT_Div_assoc mult.commute[of a])

lemma iT_Mult_Div_self: "0 < k ⟹ I ⊗ k ⊘ k = I"
by (simp add: iT_Mult_def iT_Div_def image_image)
lemma iT_Mult_Div: "
  ⟦ 0 < d;  k mod d = 0 ⟧ ⟹ I ⊗ k ⊘ d = I ⊗ (k div d)"
  by (auto simp add: ac_simps iT_Mult_assoc[symmetric] iT_Mult_Div_self)

lemma iT_Div_Mult_self: "
  0 < k ⟹ I ⊘ k ⊗ k = {y. ∃x ∈ I. y = x - x mod k}"
by (simp add: set_eq_iff iT_Mult_def iT_Div_def image_image image_iff div_mult_cancel)

lemma iT_Plus_Div_distrib_mod_less: "
  ∀x∈I. x mod m + n mod m < m ⟹ I ⊕ n ⊘ m = I ⊘ m ⊕ n div m"
by (simp add: set_eq_iff iT_Div_def iT_Plus_def image_image image_iff div_add1_eq1)
corollary iT_Plus_Div_distrib_mod_0: "
  n mod m = 0 ⟹ I ⊕ n ⊘ m = I ⊘ m ⊕ n div m"
apply (case_tac "m = 0", simp add: iT_Plus_0 iT_Div_0)
apply (simp add: iT_Plus_Div_distrib_mod_less)
done

lemma iT_Div_Min: "I ≠ {} ⟹ iMin (I ⊘ k) = iMin I div k"
by (simp add: iT_Div_def iMin_mono2 mono_def div_le_mono)

corollary
  iFROM_div_Min: "iMin ([n…] ⊘ k) = n div k" and
  iIN_div_Min:   "iMin ([n…,d] ⊘ k) = n div k" and
  iTILL_div_Min: "iMin ([…n] ⊘ k) = 0" and
  iMOD_div_Min:  "iMin ([r, mod m] ⊘ k) = r div k" and
  iMODb_div_Min: "iMin ([r, mod m, c] ⊘ k) = r div k"
by (simp add: iT_not_empty iT_Div_Min iT_Min)+

lemmas iT_div_Min =
  iFROM_div_Min
  iIN_div_Min
  iTILL_div_Min
  iMOD_div_Min
  iMODb_div_Min

lemma iT_Div_Max: "⟦ finite I; I ≠ {} ⟧ ⟹ Max (I ⊘ k) = Max I div k"
by (simp add: iT_Div_def Max_mono2 mono_def div_le_mono)

corollary
  iIN_div_Max:   "Max ([n…,d] ⊘ k) = (n + d) div k" and
  iTILL_div_Max: "Max ([…n] ⊘ k) = n div k" and
  iMODb_div_Max: "Max ([r, mod m, c] ⊘ k) = (r + m * c) div k"
by (simp add: iT_not_empty iT_finite iT_Div_Max iT_Max)+

lemma iT_Div_0_finite: "finite (I ⊘ 0)"
by (simp add: iT_Div_0_if iTILL_0)

lemma iT_Div_infinite_iff: "0 < k ⟹ infinite (I ⊘ k) = infinite I"
apply (unfold iT_Div_def)
apply (rule iffI)
 apply (rule infinite_image_imp_infinite, assumption)
apply (clarsimp simp: infinite_nat_iff_unbounded_le image_iff, rename_tac x1)
apply (drule_tac x="x1 * k" in spec, clarsimp, rename_tac x2)
apply (drule div_le_mono[of _ _ k], simp)
apply (rule_tac x="x2 div k" in exI)
apply fastforce
done
lemma iT_Div_finite_iff: "0 < k ⟹ finite (I ⊘ k) = finite I"
by (insert iT_Div_infinite_iff, simp)


lemma iFROM_div: "0 < k ⟹ [n…] ⊘ k = [n div k…]"
apply (clarsimp simp: set_eq_iff iT_Div_def image_iff Bex_def iFROM_iff, rename_tac x)
apply (rule iffI)
 apply (clarsimp simp: div_le_mono)
apply (rule_tac x="n mod k + k * x" in exI)
apply simp
apply (subst add.commute, subst le_diff_conv[symmetric])
apply (subst minus_mod_eq_mult_div)
apply simp
done

lemma iIN_div: "
  0 < k ⟹
  [n…,d] ⊘ k = [n div k…, d div k + (n mod k + d mod k) div k ]"
apply (clarsimp simp: set_eq_iff iT_Div_def image_iff Bex_def iIN_iff, rename_tac x)
apply (rule iffI)
 apply clarify
 apply (drule div_le_mono[of n _ k])
 apply (drule div_le_mono[of _ "n + d" k])
 apply (simp add: div_add1_eq[of n d])
apply (clarify, rename_tac x)
apply (simp add: add.assoc[symmetric] div_add1_eq[symmetric])
apply (frule mult_le_mono1[of "n div k" _ k])
apply (frule mult_le_mono1[of _ "(n + d) div k" k])
apply (simp add: mult.commute[of _ k] minus_mod_eq_mult_div [symmetric])
apply (simp add: le_diff_conv le_diff_conv2[OF mod_le_dividend])
apply (drule order_le_less[of _ "(n + d) div k", THEN iffD1], erule disjE)
 apply (rule_tac x="k * x + n mod k" in exI)
 apply (simp add: add.commute[of _ "n mod k"])
 apply (case_tac "n mod k ≤ (n + d) mod k", simp)
 apply (simp add: linorder_not_le)
 apply (drule_tac m=x in less_imp_le_pred)
 apply (drule_tac i=x and k=k in mult_le_mono2)
 apply (simp add: diff_mult_distrib2 minus_mod_eq_mult_div [symmetric])
 apply (subst add.commute[of "n mod k"])
 apply (subst le_diff_conv2[symmetric])
  apply (simp add: trans_le_add1)
 apply (rule order_trans, assumption)
 apply (rule diff_le_mono2)
 apply (simp add: trans_le_add2)
apply (rule_tac x="n + d" in exI, simp)
done

corollary iIN_div_if: "
  0 < k ⟹ [n…,d] ⊘ k =
  [n div k…, d div k + (if n mod k + d mod k < k then 0 else Suc 0)]"
apply (simp add: iIN_div)
apply (simp add: iIN_def add.assoc[symmetric] div_add1_eq[symmetric] div_add1_eq2[where a=n])
done

corollary iIN_div_eq1: "
  ⟦ 0 < k; n mod k + d mod k < k ⟧ ⟹
  [n…,d] ⊘ k = [n div k…,d div k]"
by (simp add: iIN_div_if)

corollary iIN_div_eq2: "
  ⟦ 0 < k; k ≤ n mod k + d mod k ⟧ ⟹
  [n…,d] ⊘ k = [n div k…, Suc (d div k)]"
by (simp add: iIN_div_if)

corollary iIN_div_mod_eq_0: "
  ⟦ 0 < k; n mod k = 0 ⟧ ⟹ [n…,d] ⊘ k = [n div k…,d div k]"
by (simp add: iIN_div_eq1)


lemma iTILL_div: "
   0 < k ⟹ […n] ⊘ k = […n div k]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_div_if)

lemma iMOD_div_ge: "
  ⟦ 0 < m; m ≤ k ⟧ ⟹ [r, mod m] ⊘ k = [r div k…]"
apply (frule less_le_trans[of _ _ k], assumption)
apply (clarsimp simp: set_eq_iff iT_Div_mem_iff Bex_def iT_iff, rename_tac x)
apply (rule iffI)
 apply (fastforce simp: div_le_mono)
apply (rule_tac x="
  if x * k < r then r else
    ((if x * k mod m ≤ r mod m then 0 else m) + r mod m + (x * k - x * k mod m))"
  in exI)
apply (case_tac "x * k < r")
 apply simp
 apply (drule less_imp_le[of _ r], drule div_le_mono[of _ r k], simp)
apply (simp add: linorder_not_less linorder_not_le)
apply (simp add: div_le_conv add.commute[of k])
apply (subst diff_add_assoc, simp)+
apply (simp add: div_mult_cancel[symmetric] del: add_diff_assoc)
apply (case_tac "x * k mod m = 0")
 apply (clarsimp elim!: dvdE)
 apply (drule sym)
 apply (simp add: mult.commute[of m])
 apply (blast intro: div_less order_less_le_trans mod_less_divisor)
apply simp
apply (intro conjI impI)
   apply (simp add: div_mult_cancel)
  apply (simp add: div_mult_cancel)
  apply (subst add.commute, subst diff_add_assoc, simp)
  apply (subst add.commute, subst div_mult_self1, simp)
  apply (subst div_less)
   apply (rule order_less_le_trans[of _ m], simp add: less_imp_diff_less)
   apply simp
  apply simp
 apply (rule_tac y="x * k" in order_trans, assumption)
 apply (simp add: div_mult_cancel)
 apply (rule le_add_diff)
 apply (simp add: trans_le_add1)
apply (simp add: div_mult_cancel)
apply (subst diff_add_assoc2, simp add: trans_le_add1)
apply simp
done
corollary iMOD_div_self: "
  0 < m ⟹ [r, mod m] ⊘ m = [r div m…]"
by (simp add: iMOD_div_ge)

lemma iMOD_div: "
  ⟦ 0 < k; m mod k = 0 ⟧ ⟹
  [r, mod m] ⊘ k = [r div k, mod (m div k) ]"
apply (case_tac "m = 0")
   apply (simp add: iMOD_0 iIN_0 iT_Div_singleton)
  apply (clarsimp elim!: dvdE)
apply (rename_tac q)
apply hypsubst_thin
apply (cut_tac r="r div k" and k=k and m=q in iMOD_mult)
apply (drule arg_cong[where f="λx. x ⊕ (r mod k)"])
apply (drule sym)
apply (simp add: iMOD_add mult.commute[of k])
apply (cut_tac I="[r div k, mod q] ⊗ k" and m=k and n="r mod k" in iT_Plus_Div_distrib_mod_less)
 apply (rule ballI)
 apply (simp only: iMOD_mult iMOD_iff, elim conjE)
 apply (drule mod_factor_imp_mod_0)
 apply simp
apply (simp add: iT_Plus_0)
apply (simp add: iT_Mult_Div[OF _ mod_self] iT_Mult_1)
done

lemma iMODb_div_self: "
  0 < m ⟹ [r, mod m, c] ⊘ m = [r div m…,c]"
apply (subst iMODb_iMOD_iTILL_conv)
apply (subst iTILL_iT_Div_Int)
  apply simp
 apply (clarsimp simp: iT_iff simp del: div_mult_self1 div_mult_self2, rename_tac x)
 apply (drule div_le_mod_le_imp_le)
 apply simp+
apply (simp add: iMOD_div_self iTILL_div iFROM_iTILL_iIN_conv)
done

lemma iMODb_div_ge: "
  ⟦ 0 < m; m ≤ k ⟧ ⟹
  [r, mod m, c] ⊘ k = [r div k…,(r + m * c) div k - r div k]"
apply (case_tac "m = k")
 apply (simp add: iMODb_div_self)
apply (drule le_neq_trans, simp+)
apply (induct c)
 apply (simp add: iMODb_0 iIN_0 iT_Div_singleton)
apply (rule_tac t="[ r, mod m, Suc c ]" and s="[ r, mod m, c ] ∪ {r + m * c + m}" in subst)
 apply (cut_tac c=c and c'=0 and r=r and m=m in iMODb_append_union_Suc[symmetric])
 apply (simp add: iMODb_0 iIN_0 add.commute[of m] add.assoc)
apply (subst iT_Div_Un)
apply (simp add: iT_Div_singleton)
apply (simp add: add.commute[of m] add.assoc[symmetric])
apply (case_tac "(r + m * c) mod k + m mod k < k")
 apply (simp add: div_add1_eq1)
 apply (rule insert_absorb)
 apply (simp add: iIN_iff div_le_mono)
apply (simp add: linorder_not_less)
apply (simp add: div_add1_eq2)
apply (rule_tac t="Suc ((r + m * c) div k)" and s="Suc (r div k + ((r + m * c) div k - r div k))" in subst)
 apply (simp add: div_le_mono)
apply (simp add: iIN_Suc_insert_conv)
done

corollary iMODb_div_ge_if: "
  ⟦ 0 < m; m ≤ k ⟧ ⟹
  [r, mod m, c] ⊘ k =
  [r div k…, m * c div k + (if r mod k + m * c mod k < k then 0 else Suc 0)]"
by (simp add: iMODb_div_ge div_add1_eq_if[of _ r])

lemma iMODb_div: "
  ⟦ 0 < k; m mod k = 0 ⟧ ⟹
  [r, mod m, c] ⊘ k = [r div k, mod (m div k), c ]"
apply (subst iMODb_iMOD_iTILL_conv)
apply (subst iTILL_iT_Div_Int)
  apply simp
 apply (simp add: Ball_def iMOD_iff, intro allI impI, elim conjE, rename_tac x)
 apply (drule div_le_mod_le_imp_le)
  apply (subst mod_add1_eq_if)
  apply (simp add: mod_0_imp_mod_mult_right_0)
  apply (drule mod_eq_mod_0_imp_mod_eq, simp+)
apply (simp add: iMOD_div iTILL_div)
apply (simp