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])
done

lemma "[1…,2] = {1,2,3}"
apply fastforce
done

lemma "[1…,2]⊗2 = {2,4,6}"
apply auto
done
lemma "[10…]⊗k = {x*k | x. 10 ≤ x}"
by blast

lemma "[…4] ⊗ 10 = {0, 10, 20, 30, 40}"
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"

lemma iT_Mult_image_conv: "I ⊗ k = (λn.(n * k)) ` I"

lemma iT_Plus_empty: "{} ⊕ k = {}"

lemma iT_Mult_empty: "{} ⊗ k = {}"

lemma iT_Plus_not_empty: "I ≠ {} ⟹ I ⊕ k ≠ {}"

lemma iT_Mult_not_empty: "I ≠ {} ⟹ I ⊗ k ≠ {}"

lemma iT_Plus_empty_iff: "(I ⊕ k = {}) = (I = {})"

lemma iT_Mult_empty_iff: "(I ⊗ k = {}) = (I = {})"

lemma iT_Plus_mono: "A ⊆ B ⟹ A ⊕ k ⊆ B ⊕ k"

lemma iT_Mult_mono: "A ⊆ B ⟹ A ⊗ k ⊆ B ⊗ k"

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])"

lemma iT_Plus_mem_iff: "x ∈ (I ⊕ k) = (k ≤ x ∧ (x - k) ∈ I)"
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)"

lemma iT_Mult_mem_iff_0: "x ∈ (I ⊗ 0) = (I ≠ {} ∧ x = 0)"
apply (case_tac "I = {}")
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)"

lemma iT_Plus_singleton: "{a} ⊕ k = {a + k}"

lemma iT_Mult_singleton: "{a} ⊗ k = {a * k}"

lemma iT_Plus_Un: "(A ∪ B) ⊕ k = (A ⊕ k) ∪ (B ⊕ k)"

lemma iT_Mult_Un: "(A ∪ B) ⊗ k = (A ⊗ k) ∪ (B ⊗ k)"

lemma iT_Plus_Int: "(A ∩ B) ⊕ k = (A ⊕ k) ∩ (B ⊕ k)"

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"

(*<*)
lemma "i ⊗ n1 ⊗ n2 ⊗ n3 ⊗ n4 ⊗ n5 ⊗ n6 ⊗ n7 =
i ⊗ n1 * n2 * n3 * n4 * n5 * n6 * n7"
lemma "i ⊕ n1 ⊕ n2 ⊕ n3 ⊕ n4 ⊕ n5 = i ⊕ n1 + n2 + n3 + n4 + n5"
lemma "i ⊕ n1 ⊗ m ⊕ n2 = i ⊗ m ⊕ n1 * m + n2"
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"
(*>*)

lemma iT_Plus_finite_iff: "finite (I ⊕ k) = finite I"

lemma iT_Mult_0_finite: "finite (I ⊗ 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]"

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"

lemma iT_Mult_1: "I ⊗ Suc 0 = I"

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_mult_Min =
iIN_mult_Min
iTILL_mult_Min
iFROM_mult_Min
iMOD_mult_Min
iMODb_mult_Min

lemma iFROM_add: "[n…] ⊕ k = [n+k…]"

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]"

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 (rule_tac x="x - k" in exI)
apply clarsimp
done

lemma iMODb_add: "[r, mod m, c] ⊕ k = [r + k, mod m, c]"

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 (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 (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 ]"

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 (rule iffI)
apply (elim conjE)
apply (drule mult_le_mono1[of _ _ k])
apply (elim conjE)
apply (subgoal_tac "x mod k = 0")
prefer 2
apply (drule_tac arg_cong[where f="λx. x mod 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)
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"

lemma iIN_conv: "[n…,d] = […d] ⊕ n"

lemma iMOD_conv: "[r, mod m] = [0…] ⊗ m ⊕ r"
apply (case_tac "m = 0")
done

lemma iMODb_conv: "[r, mod m, c] = […c] ⊗ m ⊕ r"
apply (case_tac "m = 0")
done

text ‹Some examples showing the utility of iMODb\_conv›
lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
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 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 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)"

lemma iT_Plus_neg_mem_iff2: "k ≤ x ⟹ (x - k ∈ I ⊕- k) = (x ∈ I)"

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"

lemma iT_Plus_neg_empty: "{} ⊕- k = {}"
lemma iT_Plus_neg_Max_less_empty: "
⟦ finite I; Max I < k ⟧ ⟹ I ⊕- k = {}"

lemma iT_Plus_neg_not_empty_iff: "(I ⊕- k ≠ {}) = (∃x∈I. k ≤ x)"

lemma iT_Plus_neg_empty_iff: "
(I ⊕- k = {}) = (I = {} ∨ (finite I ∧ Max I < k))"
apply (case_tac "I = {}")
apply (case_tac "infinite I")
done

lemma iT_Plus_neg_assoc: "(I ⊕- a) ⊕- b = I ⊕- (a + b)"
done

lemma iT_Plus_neg_commute: "I ⊕- a ⊕- b = I ⊕- b ⊕- a"

lemma iT_Plus_neg_0: "I ⊕- 0 = I"

lemma iT_Plus_Plus_neg_assoc: "b ≤ a ⟹ I ⊕ a ⊕- b = I ⊕ (a - b)"
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)
done

lemma iT_Plus_Plus_neg_assoc2: "a ≤ b ⟹ I ⊕ a ⊕- b = I ⊕- (b - a)"
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 (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 fastforce
done

corollary iT_Plus_neg_Plus_le_Min_eq: "
⟦ a ≤ b; a ≤ iMin I ⟧ ⟹ (I ⊕- a) ⊕ b = I ⊕ (b - a)"

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)
done

corollary iT_Plus_neg_Plus_ge_Min_eq: "
⟦ b ≤ a; a ≤ iMin I ⟧ ⟹ (I ⊕- a) ⊕ b = I ⊕- (a - b)"

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 (clarsimp, rename_tac x')
apply (rule_tac x="x' - n" in exI)
apply fastforce
done

lemma iT_Plus_neg_Plus_le_inverse: "k ≤ iMin I ⟹ I ⊕- k ⊕ k = I"

lemma iT_Plus_neg_Plus_inverse: "I ⊕- k ⊕ k = I ↓≥ k"

lemma iT_Plus_Plus_neg_inverse: "I ⊕ k ⊕- k = I"

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 (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}"

corollary iT_Plus_neg_singleton2: "a < k ⟹ {a} ⊕- k= {}"

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

lemma iT_Plus_neg_Min: "
I ⊕- k ≠ {} ⟹ iMin (I ⊕- k) = iMin (I ↓≥ k) - k"
done

lemma iT_Plus_neg_Max: "
⟦ finite I; I ⊕- k ≠ {} ⟧ ⟹ Max (I ⊕- k) = Max I - k"
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]"
lemma iTILL_add_neg2: "n < k ⟹ […n] ⊕- k = {}"

[n…,d] ⊕- k = (
if k ≤ n then [n - k…,d]
else if k ≤ n + d then […n + d - k] else {})"

lemma iIN_add_neg1: "k ≤ n ⟹ [n…,d] ⊕- k = [n - k…,d]"

lemma iIN_add_neg2: "⟦ n ≤ k; k ≤ n + d ⟧ ⟹ [n…,d] ⊕- k = […n + d - k]"

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"

(*
lemma "[25, mod 10] ⊕- 32 = [3, mod 10]"
apply (rule set_eqI)
apply clarify
apply (rule iffI)
apply simp+
done
*)

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: 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 safe
apply (drule sym)
apply simp
done

[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_0 iIN_0 iT_Plus_neg_singleton)
done

k ≤ r ⟹ [r, mod m] ⊕- k = [r - k, mod m]"

⟦ 0 < m; r < k ⟧ ⟹ [r, mod m] ⊕- k = [(m + r mod m - k mod m) mod m, mod m]"

lemma iMODb_mod_0_add_neg: "[r, mod 0, c] ⊕- k = {r} ⊕- k"

(*
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 (rule_tac t="(x - 3) mod 10 = 0" and s="x mod 10 = 3" in subst)
apply (rule_tac t="(7 + x) mod 10 = 0" and s="x mod 10 = 3" in subst)
apply (rule conj_cong[OF refl])
done

lemma "[25, mod 10, 5] ⊕- 32 = [3, mod 10, 4]"
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)
done
*)

[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 (rule_tac t="(m + r mod m - k mod m) mod m" and s="(r + m * c - k) mod m" in subst)
apply (subst iMOD_iTILL_iMODb_conv, simp)
apply (subst sub_mod_div_eq_div, simp)
done

[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 (case_tac "m = 0", simp+)
apply (case_tac "k mod m ≤ r mod m")
apply (clarsimp simp: linorder_not_le)
apply (clarsimp simp: linorder_not_le)
done

k ≤ r ⟹ [r, mod m, c] ⊕- k = [r - k, mod m, c]"

⟦ 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]"

⟦ 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]"

⟦ 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) ]"

lemma iMODb_add_neg3: "r + m * c < k  ⟹ [r, mod m, c] ⊕- k = {}"

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)"

lemma iT_Minus_mono: "A ⊆ B ⟹ k ⊖ A ⊆ k ⊖ B"

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 ⊖ {} = {}"

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"

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

lemma iT_Minus_less_Min_empty: "k < iMin I ⟹ k ⊖ I = {}"

lemma iT_Minus_Min_singleton: "I ≠ {} ⟹ (iMin I) ⊖ I = {0}"
apply (rule set_eqI)
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 (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 (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)
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 (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)
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)
done

lemma iT_Minus_Minus_eq2: "I ⊆ […k] ⟹ k ⊖ (k ⊖ I) = I"
apply (case_tac "I = {}")
apply (rule iT_Minus_Minus_eq)
apply (frule Max_subset)
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_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 (rule iT_Minus_Plus_assoc)
apply (frule Max_subset)
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 {})"
corollary iT_Minus_singleton1: "a ≤ k ⟹ k ⊖ {a} = {k-a}"
corollary iT_Minus_singleton2: "k < a ⟹ k ⊖ {a} = {}"

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 (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]"

corollary iMOD_sub2: "k < r ⟹ k ⊖ [r, mod m] = {}"
apply (rule iT_Minus_less_Min_empty)
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]"

corollary iTILL_sub2: "k ≤ n ⟹ k ⊖ […n] = […k]"

(* 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 (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 div_le_mono[of _ _ m], simp)
apply (drule mult_le_mono2[of _ _ m])
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)
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)
done

corollary iMODb_sub3: "
r + m * c ≤ k ⟹ k ⊖ [r, mod m, c] = [ k - r - m * c, mod m, c]"

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]"

corollary iFROM_sub_empty: "k < n ⟹ k ⊖ [n…] = {}"

(* 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 {})"
done

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

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] = {}"

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)
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)
done

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

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]"

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"

lemma iT_Div_mono: "A ⊆ B ⟹ A ⊘ k ⊆ B ⊘ k"

lemma iT_Div_empty: "{} ⊘ k = {}"
lemma iT_Div_not_empty: "I ≠ {} ⟹ I ⊘ k ≠ {}"

lemma iT_Div_empty_iff: "(I ⊘ k = {}) = (I = {})"

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]"

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"

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 (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}"

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)

lemma subset_iT_Div_Int: "A ⊆ B ⟹ (A ∩ B) ⊘ k = (A ⊘ k) ∩ (B ⊘ k)"

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)"
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 (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}"
(*>*)

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"
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)
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)"

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 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 (clarify, rename_tac x)
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 (case_tac "n mod k ≤ (n + d) mod k", simp)
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 (rule order_trans, assumption)
apply (rule diff_le_mono2)
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)]"
done

corollary iIN_div_eq1: "
⟦ 0 < k; n mod k + d mod k < k ⟧ ⟹
[n…,d] ⊘ k = [n div k…,d div k]"

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

corollary iIN_div_mod_eq_0: "
⟦ 0 < k; n mod k = 0 ⟧ ⟹ [n…,d] ⊘ k = [n div k…,d div k]"

lemma iTILL_div: "
0 < k ⟹ […n] ⊘ k = […n div k]"

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 (case_tac "x * k mod m = 0")
apply (clarsimp elim!: dvdE)
apply (drule sym)
apply (blast intro: div_less order_less_le_trans mod_less_divisor)
apply simp
apply (intro conjI impI)
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
done
corollary iMOD_div_self: "
0 < m ⟹ [r, mod m] ⊘ m = [r div m…]"

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 (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_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 (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 (subst iT_Div_Un)
apply (case_tac "(r + m * c) mod k + m mod k < k")
apply (rule insert_absorb)
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)
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)]"

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)