Theory IL_Interval

(*  Title:      IL_Interval.thy
Date:       Oct 2006
Author:     David Trachtenherz
*)

section ‹Intervals and operations for temporal logic declarations›

theory IL_Interval
imports

begin

subsection ‹Time intervals -- definitions and basic lemmata›

subsubsection ‹Definitions›

type_synonym Time = nat

(* Time interval *)
type_synonym iT = "Time set"

text ‹Infinite interval starting at some natural @{term "n"}.›
definition
iFROM :: "Time  iT" ("[_…]") (* [n, ∞) *)
where
"[n…]  {n..}"

text ‹Finite interval starting at @{term "0"} and ending at some natural @{term "n"}.›
definition
iTILL :: "Time  iT" ("[…_]") (* [0, n] *) (* Equivalent to [0…,n] *)
where
"[…n]  {..n}"

text ‹
Finite bounded interval containing the naturals between
@{term "n"} and @{term "n + d"}.
@{term "d"} denotes the difference between left and right interval bound.
The number of elements is @{term "d + 1"} so that an empty interval cannot be defined.›
definition
iIN   :: "Time  nat  iT" ( "[_…,_]") (* [n, n+d] *)
where
"[n…,d]  {n..n+d}"

text ‹
Infinite modulo interval containing all naturals
having the same division remainder modulo @{term "m"}
as @{term "r"}, and beginning at @{term "n"}.›
definition
iMOD  :: "Time  nat  iT" ( "[ _, mod _ ]" )
where
"[r, mod m]  { x. x mod m = r mod m  r  x}"

text ‹
Finite bounded modulo interval containing all naturals
having the same division remainder modulo @{term "m"}
as @{term "r"}, beginning at @{term "n"},
and ending after @{term "c"} cycles at @{term "r + m * c"}.
The number of elements is @{term "c + 1"} so that an empty interval cannot be defined.›
definition
iMODb :: "Time  nat  nat  iT" ( "[ _, mod _, _ ]" )
where
"[r, mod m, c]  { x. x mod m = r mod m  r  x  x  r + m * c}"

subsubsection ‹Membership in an interval›

lemmas iT_defs = iFROM_def iTILL_def iIN_def iMOD_def iMODb_def

lemma iFROM_iff: "x  [n…] = (n  x)"
by (simp add: iFROM_def)
lemma iTILL_iff: "x  […n] = (x  n)"
by (simp add: iTILL_def)
lemma iIN_iff:"x  [n…,d] = (n  x  x  n + d)"
by (simp add: iIN_def)
lemma iMOD_iff: "x  [r, mod m] = (x mod m = r mod m  r  x)"
by (simp add: iMOD_def)
lemma iMODb_iff: "x  [r, mod m, c] =
(x mod m = r mod m  r  x  x  r + m * c)"
by (simp add: iMODb_def)

lemma iFROM_D: "x  [n…]  (n  x)"
by (rule iFROM_iff[THEN iffD1])
lemma iTILL_D: "x  […n]  (x  n)"
by (rule iTILL_iff[THEN iffD1])
corollary iIN_geD: "x  [n…,d]  n  x"
by (simp add: iIN_iff)
corollary iIN_leD: "x  [n…,d]  x  n + d"
by (simp add: iIN_iff)
corollary iMOD_modD: "x  [r, mod m]  x mod m = r mod m"
by (simp add: iMOD_iff)
corollary iMOD_geD: "x  [r, mod m]  r  x"
by (simp add: iMOD_iff)
corollary iMODb_modD: "x  [r, mod m, c]  x mod m = r mod m"
by (simp add: iMODb_iff)
corollary iMODb_geD: "x  [r, mod m, c]  r  x"
by (simp add: iMODb_iff)
corollary iMODb_leD: "x  [r, mod m, c]  x  r + m * c"
by (simp add: iMODb_iff)

lemmas iT_iff = iFROM_iff iTILL_iff iIN_iff iMOD_iff iMODb_iff

lemmas iT_drule =
iFROM_D
iTILL_D
iIN_geD iIN_leD
iMOD_modD iMOD_geD
iMODb_modD iMODb_geD iMODb_leD

lemma
iFROM_I [intro]: "n  x  x  [n…]" and
iTILL_I [intro]: "x  n  x  […n]" and
iIN_I [intro]:   "n  x  x  n + d  x  [n…,d]" and
iMOD_I [intro]:  "x mod m = r mod m  r  x  x  [r, mod m]" and
iMODb_I [intro]: "x mod m = r mod m  r  x  x  r + m * c  x  [r, mod m, c]"
by (simp add: iT_iff)+

lemma
iFROM_E [elim]:  "x  [n…]  (n  x  P)  P" and
iTILL_E [elim]:  "x  […n]  (x  n  P)  P" and
iIN_E [elim]:    "x  [n…,d]  (n  x  x  n + d  P)  P" and
iMOD_E [elim]:   "x  [r, mod m]  (x mod m = r mod m  r  x  P)  P" and
iMODb_E [elim]:   "x  [r, mod m, c]  (x mod m = r mod m  r  x  x  r + m * c  P)  P"
by (simp add: iT_iff)+

(*
lemma "0 < n ⟹ ∃x ∈ [n…,2*n]. x mod 2 = 0"
apply (simp add: iT_defs)
apply (rule_tac x="2*n" in bexI)
apply simp
apply simp
done
lemma "0 < n ⟹ ∃x ∈ [n…,2*n]. x mod 2 = 0"
apply (simp add: iT_defs atLeastAtMost_def atLeast_def atMost_def Collect_conj_eq[symmetric])
apply (rule_tac x="2*n" in exI)
apply simp
done
*)

lemma iIN_Suc_insert_conv: "
insert (Suc (n + d)) [n…,d] = [n…,Suc d]"
by (fastforce simp: iIN_iff)

lemma iTILL_Suc_insert_conv: "insert (Suc n) […n] = […Suc n]"
by (fastforce simp: iIN_Suc_insert_conv[of 0 n])

lemma iMODb_Suc_insert_conv: "
insert (r + m * Suc c) [r, mod m, c] = [r, mod m, Suc c]"
apply (rule set_eqI)
apply (simp add: iMODb_iff add.commute[of _ r])
apply (rule iffI)
apply fastforce
apply (elim conjE)
apply (drule_tac x=x in order_le_less[THEN iffD1, rule_format])
apply (erule disjE)
apply (frule less_mod_eq_imp_add_divisor_le[where m=m], simp)
apply simp
apply simp
done

lemma iFROM_pred_insert_conv: "insert (n - Suc 0) [n…] = [n - Suc 0…]"
by (fastforce simp: iFROM_iff)

lemma iIN_pred_insert_conv: "
0 < n  insert (n - Suc 0) [n…,d] = [n - Suc 0…,Suc d]"
by (fastforce simp: iIN_iff)

lemma iMOD_pred_insert_conv: "
m  r  insert (r - m) [r, mod m] = [r - m, mod m]"
apply (case_tac "m = 0")
apply (simp add: iMOD_iff insert_absorb)
apply simp
apply (rule set_eqI)
apply (simp add: iMOD_iff mod_diff_self2)
apply (rule iffI)
apply (erule disjE)
apply (simp add: mod_diff_self2)
apply (simp add: le_imp_diff_le)
apply (erule conjE)
apply (drule order_le_less[THEN iffD1, of "rm"], erule disjE)
prefer 2
apply simp
apply (frule order_less_le_trans[of _ m r], assumption)
apply (drule less_mod_eq_imp_add_divisor_le[of "rm" _ m])
apply (simp add: mod_diff_self2)
apply simp
done

lemma iMODb_pred_insert_conv: "
m  r  insert (r - m) [r, mod m, c] = [r - m, mod m, Suc c]"
apply (rule set_eqI)
apply (frule iMOD_pred_insert_conv)
apply (drule_tac f="λs. x  s" in arg_cong)
apply (force simp: iMOD_iff iMODb_iff)
done

lemma iFROM_Suc_pred_insert_conv: "insert n [Suc n…] = [n…]"
by (insert iFROM_pred_insert_conv[of "Suc n"], simp)
lemma iIN_Suc_pred_insert_conv: "insert n [Suc n…,d] = [n…,Suc d]"
by (insert iIN_pred_insert_conv[of "Suc n"], simp)
lemma iMOD_Suc_pred_insert_conv: "insert r [r + m, mod m] = [r, mod m]"
by (insert iMOD_pred_insert_conv[of m "r  m"], simp)
lemma iMODb_Suc_pred_insert_conv: "insert r [r + m, mod m, c] = [r, mod m, Suc c]"
by (insert iMODb_pred_insert_conv[of m "r  m"], simp)

lemmas iT_Suc_insert =
iIN_Suc_insert_conv
iTILL_Suc_insert_conv
iMODb_Suc_insert_conv
lemmas iT_pred_insert =
iFROM_pred_insert_conv
iIN_pred_insert_conv
iMOD_pred_insert_conv
iMODb_pred_insert_conv
lemmas iT_Suc_pred_insert =
iFROM_Suc_pred_insert_conv
iIN_Suc_pred_insert_conv
iMOD_Suc_pred_insert_conv
iMODb_Suc_pred_insert_conv

lemma iMOD_mem_diff: " a  [r, mod m]; b  [r, mod m]   (a - b) mod m = 0"
by (simp add: iMOD_iff mod_eq_imp_diff_mod_0)
lemma iMODb_mem_diff: " a  [r, mod m, c]; b  [r, mod m, c]   (a - b) mod m = 0"
by (simp add: iMODb_iff mod_eq_imp_diff_mod_0)

subsubsection ‹Interval conversions›

lemma iIN_0_iTILL_conv:"[0…,n] = […n]"
by (simp add: iTILL_def iIN_def atMost_atLeastAtMost_0_conv)
lemma iIN_iTILL_iTILL_conv: "0 < n  [n…,d] = […n+d] - […n - Suc 0]"
by (fastforce simp: iTILL_iff iIN_iff)
lemma iIN_iFROM_iTILL_conv: "[n…,d] = [n…]  […n+d]"
by (simp add: iT_defs atLeastAtMost_def)
lemma iMODb_iMOD_iTILL_conv: "[r, mod m, c] = [r, mod m]  […r+m*c]"
by (force simp: iT_defs set_interval_defs)
lemma iMODb_iMOD_iIN_conv: "[r, mod m, c] = [r, mod m]  [r…,m*c]"
by (force simp: iT_defs set_interval_defs)

lemma iFROM_iTILL_iIN_conv: "n  n'  [n…]  […n'] = [n…,n'-n]"
by (simp add: iT_defs atLeastAtMost_def)
lemma iMOD_iTILL_iMODb_conv: "
r  n  [r, mod m]  […n] = [r, mod m, (n - r) div m]"
apply (rule set_eqI)
apply (simp add: iT_iff minus_mod_eq_mult_div [symmetric])
apply (rule iffI)
apply clarify
apply (frule_tac x=x and y=n and m=m in le_imp_sub_mod_le)
apply (simp add: mod_diff_right_eq)
apply fastforce
done

lemma iMOD_iIN_iMODb_conv: "
[r, mod m]  [r…,d] = [r, mod m, d div m]"
apply (case_tac "r = 0")
apply (simp add: iIN_0_iTILL_conv iMOD_iTILL_iMODb_conv)
apply (simp add: iIN_iTILL_iTILL_conv Diff_Int_distrib iMOD_iTILL_iMODb_conv diff_add_inverse)
apply (rule subst[of "" _ "λt. x(x  t)  x", THEN spec])
prefer 2
apply simp
apply (rule sym)
apply (fastforce simp: disjoint_iff_not_equal iMOD_iff iTILL_iff)
done

lemma iFROM_0:
by (simp add: iFROM_def)

lemma iTILL_0: "[…0] = {0}"
by (simp add: iTILL_def)

lemma iIN_0: "[n…,0] = {n}"
by (simp add: iIN_def)

lemma iMOD_0: "[r, mod 0] = [r…,0]"
by (fastforce simp: iIN_0 iMOD_def)

lemma iMODb_mod_0: "[r, mod 0, c] = [r…,0]"
by (fastforce simp: iMODb_def iIN_0)

lemma iMODb_0: "[r, mod m, 0] = [r…,0]"
by (fastforce simp: iMODb_def iIN_0 set_eq_iff)

lemmas iT_0 =
iFROM_0
iTILL_0
iIN_0
iMOD_0
iMODb_mod_0
iMODb_0

lemma iMOD_1: "[r, mod Suc 0] = [r…]"
by (fastforce simp: iFROM_iff)

lemma iMODb_mod_1: "[r, mod Suc 0, c] = [r…,c]"
by (fastforce simp: iT_iff)

subsubsection ‹Finiteness and emptiness of intervals›

lemma
iFROM_not_empty: "[n…]  {}" and
iTILL_not_empty: "[…n]  {}" and
iIN_not_empty: "[n…,d]  {}" and
iMOD_not_empty: "[r, mod m]  {}" and
iMODb_not_empty: "[r, mod m, c]  {}"
by (fastforce simp: iT_iff)+

lemmas iT_not_empty =
iFROM_not_empty
iTILL_not_empty
iIN_not_empty
iMOD_not_empty
iMODb_not_empty

lemma
iTILL_finite: "finite […n]" and
iIN_finite: "finite [n…,d]" and
iMODb_finite: "finite [r, mod m, c]" and
iMOD_0_finite:
by (simp add: iT_defs)+

lemma iFROM_infinite: "infinite [n…]"
by (simp add: iT_defs infinite_atLeast)

lemma iMOD_infinite: "0 < m  infinite [r, mod m]"
apply (rule infinite_nat_iff_asc_chain[THEN iffD2])
apply (rule iT_not_empty)
apply (rule ballI, rename_tac n)
apply (rule_tac x="n+m" in bexI, simp)
apply (simp add: iMOD_iff)
done

lemmas iT_finite =
iTILL_finite
iIN_finite
iMODb_finite iMOD_0_finite

lemmas iT_infinite =
iFROM_infinite
iMOD_infinite

subsubsection Min› and Max› element of an interval›

lemma
iTILL_Min: "iMin […n] = 0" and
iFROM_Min: "iMin [n…] = n" and
iIN_Min:   "iMin [n…,d] = n" and
iMOD_Min:  "iMin [r, mod m] = r" and
iMODb_Min: "iMin [r, mod m, c] = r"
by (rule iMin_equality, (simp add: iT_iff)+)+

lemmas iT_Min =
iIN_Min
iTILL_Min
iFROM_Min
iMOD_Min
iMODb_Min

lemma
iTILL_Max: "Max […n] = n" and
iIN_Max: "Max [n…,d] = n+d" and
iMODb_Max: "Max [r, mod m, c] = r + m * c" and
iMOD_0_Max: "Max [r, mod 0] = r"
by (rule Max_equality, (simp add: iT_iff iT_finite)+)+

lemmas iT_Max =
iTILL_Max
iIN_Max
iMODb_Max
iMOD_0_Max

lemma
iTILL_iMax: "iMax […n] = enat n" and
iIN_iMax: "iMax [n…,d] = enat (n+d)" and
iMODb_iMax: "iMax [r, mod m, c] = enat (r + m * c)" and
iMOD_0_iMax: "iMax [r, mod 0] = enat r" and
iFROM_iMax: "iMax [n…] = " and
iMOD_iMax: "0 < m  iMax [r, mod m] = "
by (simp add: iMax_def iT_finite iT_infinite iT_Max)+

lemmas iT_iMax =
iTILL_iMax
iIN_iMax
iMODb_iMax
iMOD_0_iMax
iFROM_iMax
iMOD_iMax

subsection ‹Adding and subtracting constants to interval elements›

lemma
iFROM_plus: "x  [n…]  x + k  [n…]" and
iFROM_Suc: "x  [n…]  Suc x  [n…]" and
iFROM_minus: " x  [n…]; k  x - n   x - k  [n…]" and
iFROM_pred: "n < x   x - Suc 0  [n…]"
by (simp add: iFROM_iff)+

lemma
iTILL_plus: " x  […n]; k  n - x   x + k  […n]" and
iTILL_Suc: "x < n  Suc x  […n]" and
iTILL_minus: "x  […n]  x - k  […n]" and
iTILL_pred: "x  […n]  x - Suc 0  […n]"
by (simp add: iTILL_iff)+

lemma iIN_plus: " x  [n…,d]; k  n + d - x   x + k  [n…,d]"
by (fastforce simp: iIN_iff)

lemma iIN_Suc: " x  [n…,d]; x < n + d   Suc x  [n…,d]"
by (simp add: iIN_iff)

lemma iIN_minus: " x  [n…,d]; k  x - n   x - k  [n…,d]"
by (fastforce simp: iIN_iff)

lemma iIN_pred: " x  [n…,d]; n < x   x - Suc 0  [n…,d]"
by (fastforce simp: iIN_iff)

lemma iMOD_plus_divisor_mult: "x  [r, mod m]  x + k * m  [r, mod m]"
by (simp add: iMOD_def)

corollary iMOD_plus_divisor: "x  [r, mod m]  x + m  [r, mod m]"
by (simp add: iMOD_def)

lemma iMOD_minus_divisor_mult: "
x  [r, mod m]; k * m  x - r   x - k * m  [r, mod m]"
by (fastforce simp: iMOD_def mod_diff_mult_self1)

corollary iMOD_minus_divisor_mult2: "
x  [r, mod m]; k  (x - r) div m   x - k * m  [r, mod m]"
apply (rule iMOD_minus_divisor_mult, assumption)
apply (clarsimp simp: iMOD_iff)
apply (drule mult_le_mono1[of _ _ m])
apply (simp add: mod_0_div_mult_cancel[THEN iffD1, OF mod_eq_imp_diff_mod_0])
done

corollary iMOD_minus_divisor: "
x  [r, mod m]; m + r  x   x - m  [r, mod m]"
apply (frule iMOD_geD)
apply (insert iMOD_minus_divisor_mult[of x r m ])
apply simp
done

lemma iMOD_plus: "
x  [r, mod m]  (x + k  [r, mod m]) = (k mod m = 0)"
apply safe
apply (drule iMOD_modD)+
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
apply simp
apply (erule dvdE)
apply (simp add: mult.commute iMOD_plus_divisor_mult)
done
corollary iMOD_Suc: "
x  [r, mod m]  (Suc x  [r, mod m]) = (m = Suc 0)"
apply (simp add: iMOD_iff, safe)
apply (simp add: mod_Suc, split if_split_asm)
apply simp+
done

lemma iMOD_minus: "
x  [r, mod m]; k  x - r   (x - k  [r, mod m]) = (k mod m = 0)"
apply safe
apply (clarsimp simp: iMOD_iff)
apply (rule mod_add_eq_imp_mod_0[of "x  k" k, THEN iffD1])
apply simp
apply (erule dvdE)
apply (simp add: mult.commute iMOD_minus_divisor_mult)
done

corollary iMOD_pred: "
x  [r, mod m]; r < x   (x - Suc 0  [r, mod m]) = (m = Suc 0)"
apply safe
apply (simp add: iMOD_Suc[of "x - Suc 0" r, THEN iffD1])
apply (simp add: iMOD_iff)
done

lemma iMODb_plus_divisor_mult: "
x  [r, mod m, c]; k * m  r + m * c - x   x + k * m  [r, mod m, c]"
by (fastforce simp: iMODb_def)

lemma iMODb_plus_divisor_mult2: "
x  [r, mod m, c]; k  c - (x - r) div m
x + k * m  [r, mod m, c]"
apply (rule iMODb_plus_divisor_mult, assumption)
apply (clarsimp simp: iMODb_iff)
apply (drule mult_le_mono1[of _ _ m])
apply (simp add: diff_mult_distrib
mod_0_div_mult_cancel[THEN iffD1, OF mod_eq_imp_diff_mod_0]
add.commute[of r] mult.commute[of c])
done
lemma iMODb_plus_divisor: "
x  [r, mod m, c]; x < r + m * c   x + m  [r, mod m, c]"

lemma iMODb_minus_divisor_mult: "
x  [r, mod m, c]; r + k * m  x    x - k * m  [r, mod m, c]"
by (fastforce simp: iMODb_def mod_diff_mult_self1)

lemma iMODb_plus: "
x  [r, mod m, c]; k  r + m * c - x
(x + k  [r, mod m, c]) = (k mod m = 0)"
apply safe
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
apply (simp add: iT_iff)
apply fastforce
done

corollary iMODb_Suc: "
x  [r, mod m, c]; x < r + m * c
(Suc x  [r, mod m, c]) = (m = Suc 0)"
apply (rule iffI)
apply (simp add: iMODb_iMOD_iTILL_conv iMOD_Suc)
apply (simp add: iMODb_iMOD_iTILL_conv iMOD_1 iFROM_Suc iTILL_Suc)
done

lemma iMODb_minus: "
x  [r, mod m, c]; k  x - r
(x - k  [r, mod m, c]) = (k mod m = 0)"
apply (rule iffI)
apply (simp add: iMODb_iMOD_iTILL_conv iMOD_minus)
apply (simp add: iMODb_iMOD_iTILL_conv iMOD_minus iTILL_minus)
done

corollary iMODb_pred: "
x  [r, mod m, c]; r < x
(x - Suc 0  [r, mod m, c]) = (m = Suc 0)"
apply (rule iffI)
apply (subgoal_tac "x  [r, mod m]  x - Suc 0  [r, mod m]")
prefer 2
apply (simp add: iT_iff)
apply (clarsimp simp: iMOD_pred)
apply (fastforce simp add: iMODb_iff)
done

lemmas iFROM_plus_minus =
iFROM_plus
iFROM_Suc
iFROM_minus
iFROM_pred

lemmas iTILL_plus_minus =
iTILL_plus
iTILL_Suc
iTILL_minus
iTILL_pred

lemmas iIN_plus_minus =
iIN_plus
iIN_Suc
iTILL_minus
iIN_pred

lemmas iMOD_plus_minus_divisor =
iMOD_plus_divisor_mult
iMOD_plus_divisor
iMOD_minus_divisor_mult
iMOD_minus_divisor_mult2
iMOD_minus_divisor

lemmas iMOD_plus_minus =
iMOD_plus
iMOD_Suc
iMOD_minus
iMOD_pred

lemmas iMODb_plus_minus_divisor =
iMODb_plus_divisor_mult
iMODb_plus_divisor_mult2
iMODb_plus_divisor
iMODb_minus_divisor_mult

lemmas iMODb_plus_minus =
iMODb_plus
iMODb_Suc
iMODb_minus
iMODb_pred

lemmas iT_plus_minus =
iFROM_plus_minus
iTILL_plus_minus
iIN_plus_minus
iMOD_plus_minus_divisor
iMOD_plus_minus
iMODb_plus_minus_divisor
iMODb_plus_minus

(*
lemma "a ∈ [3…,2] ⟹ 3 ≤ a ∧ a ≤ 5"
by (simp add: iT_iff)
lemma "15 ∈ [5, mod 10]"
by (simp add: iT_iff)

lemma "n ∈ [15, mod 10] ⟹ n ∈ [5, mod 10]"
by (simp add: iT_iff)

lemma "[15, mod 10] ⊆ [5, mod 10]"
by (fastforce simp: iMOD_def)

lemma "n ≤ i ⟹ n ∈ […i]"
by (simp add: iT_iff)
lemma "∀n ∈ […i]. n ≤ i"
by (simp add: iT_iff)

lemma "∃n ∈ [2, mod 10].n ∉ [12, mod 10]"
apply (simp add: iT_defs)
apply (rule_tac x=2 in exI)
apply simp
done
*)

subsection ‹Relations between intervals›

subsubsection ‹Auxiliary lemmata›

lemma Suc_in_imp_not_subset_iMOD: "
n  S; Suc n  S; m  Suc 0   ¬ S  [r, mod m]"
by (blast intro: iMOD_Suc[THEN iffD1])

corollary Suc_in_imp_neq_iMOD: "
n  S; Suc n  S; m  Suc 0   S  [r, mod m]"
by (blast dest: Suc_in_imp_not_subset_iMOD)

lemma Suc_in_imp_not_subset_iMODb: "
n  S; Suc n  S; m  Suc 0   ¬ S  [r, mod m, c]"
apply (rule ccontr, simp)
apply (frule subsetD[of _ _ n], assumption)
apply (drule subsetD[of _ _ "Suc n"], assumption)
apply (frule iMODb_Suc[THEN iffD1])
apply (drule iMODb_leD[of "Suc n"])
apply simp
apply blast+
done
corollary Suc_in_imp_neq_iMODb: "
n  S; Suc n  S; m  Suc 0   S  [r, mod m, c]"
by (blast dest: Suc_in_imp_not_subset_iMODb)

subsubsection ‹Subset relation between intervals›

lemma
iIN_iFROM_subset_same: "[n…,d]  [n…]" and
iIN_iTILL_subset_same: "[n…,d]  […n+d]" and
iMOD_iFROM_subset_same: "[r, mod m]  [r…]" and
iMODb_iTILL_subset_same: "[r, mod m, c]  […r+m*c]" and
iMODb_iIN_subset_same: "[r, mod m, c]  [r…,m*c]" and
iMODb_iMOD_subset_same: "[r, mod m, c]  [r, mod m]"
by (simp add: subset_iff iT_iff)+

lemmas iT_subset_same =
iIN_iFROM_subset_same
iIN_iTILL_subset_same
iMOD_iFROM_subset_same
iMODb_iTILL_subset_same
iMODb_iIN_subset_same
iMODb_iTILL_subset_same
iMODb_iMOD_subset_same

lemma iMODb_imp_iMOD: "x  [r, mod m, c]  x  [r, mod m]"
by (blast intro: iMODb_iMOD_subset_same)

lemma iMOD_imp_iMODb: "
x  [r, mod m]; x  r + m * c   x  [r, mod m, c]"
by (simp add: iT_iff)

lemma iMOD_singleton_subset_conv: "([r, mod m]  {a}) = (r = a  m = 0)"
apply (rule iffI)
apply (simp add: subset_singleton_conv iT_not_empty)
apply (simp add: set_eq_iff iT_iff)
apply (frule_tac x=r in spec, drule_tac x="r+m" in spec)
apply simp
apply (simp add: iMOD_0 iIN_0)
done
lemma iMOD_singleton_eq_conv: "([r, mod m] = {a}) = (r = a  m = 0)"
apply (rule_tac t="[r, mod m] = {a}" and s="[r, mod m]  {a}" in subst)
apply (simp add: subset_singleton_conv iMOD_not_empty)
apply (simp add: iMOD_singleton_subset_conv)
done

lemma iMODb_singleton_subset_conv: "
([r, mod m, c]  {a}) = (r = a  (m = 0  c = 0))"
apply (rule iffI)
apply (simp add: subset_singleton_conv iT_not_empty)
apply (simp add: set_eq_iff iT_iff)
apply (frule_tac x=r in spec, drule_tac x="r+m" in spec)
apply clarsimp
apply (fastforce simp: iMODb_0 iMODb_mod_0 iIN_0)
done
lemma iMODb_singleton_eq_conv: "
([r, mod m, c] = {a}) = (r = a  (m = 0  c = 0))"
apply (rule_tac t="[r, mod m, c] = {a}" and s="[r, mod m, c]  {a}" in subst)
apply (simp add:  subset_singleton_conv iMODb_not_empty)
apply (simp add: iMODb_singleton_subset_conv)
done

lemma iMODb_subset_imp_divisor_mod_0: "
0 < c'; [r', mod m', c']  [r, mod m, c]   m' mod m = 0"
apply (simp add: subset_iff iMODb_iff)
apply (drule gr0_imp_self_le_mult1[of _ m'])
apply (rule mod_add_eq_imp_mod_0[of r' m' m, THEN iffD1])
apply (frule_tac x=r' in spec, drule_tac x="r'+m'" in spec)
apply simp
done

lemma iMOD_subset_imp_divisor_mod_0: "
[r', mod m']  [r, mod m]  m' mod m = 0"
apply (simp add: subset_iff iMOD_iff)
apply (rule mod_add_eq_imp_mod_0[of r' m' m, THEN iffD1])
apply simp
done

lemma iMOD_subset_imp_iMODb_subset: "
[r', mod m']  [r, mod m]; r' + m' * c'  r + m * c
[r', mod m', c']  [r, mod m, c]"
by (simp add: subset_iff iT_iff)

lemma iMODb_subset_imp_iMOD_subset: "
[r', mod m', c']  [r, mod m, c]; 0 < c'
[r', mod m']  [r, mod m]"
apply (frule subsetD[of _ _ r'])
apply (simp add: iMODb_iff)
apply (rule subsetI)
apply (simp add: iMOD_iff iMODb_iff, clarify)
apply (drule mod_eq_mod_0_imp_mod_eq[where m=m and m'=m'])
apply (simp add: iMODb_subset_imp_divisor_mod_0)
apply simp
done

lemma iMODb_0_iMOD_subset_conv: "
([r', mod m', 0]  [r, mod m]) =
(r' mod m = r mod m  r  r')"
by (simp add: iMODb_0 iIN_0 singleton_subset_conv iMOD_iff)

lemma iFROM_subset_conv: "([n'…]  [n…]) = (n  n')"
by (simp add: iFROM_def)

lemma iFROM_iMOD_subset_conv: "([n'…]  [r, mod m]) = (r  n'  m = Suc 0)"
apply (rule iffI)
apply (rule conjI)
apply (drule iMin_subset[OF iFROM_not_empty])
apply (simp add: iT_Min)
apply (rule ccontr)
apply (cut_tac Suc_in_imp_not_subset_iMOD[of n' "n'" m r])
apply (simp add: iT_iff)+
apply (simp add: subset_iff iT_iff)
done

lemma iIN_subset_conv: "([n'…,d']  [n…,d]) = (n  n'  n'+d'  n+d)"
apply (rule iffI)
apply (frule iMin_subset[OF iIN_not_empty])
apply (drule Max_subset[OF iIN_not_empty _ iIN_finite])
apply (simp add: iIN_Min iIN_Max)
apply (simp add: subset_iff iIN_iff)
done

lemma iIN_iFROM_subset_conv: "([n'…,d']  [n…]) = (n  n')"
by (fastforce simp: subset_iff iFROM_iff iIN_iff)

lemma iIN_iTILL_subset_conv: "([n'…,d']  […n]) = (n' + d'  n)"
by (fastforce simp: subset_iff iT_iff)

lemma iIN_iMOD_subset_conv: "
0 < d'  ([n'…,d']  [r, mod m]) = (r  n'  m = Suc 0)"
apply (rule iffI)
apply (frule iMin_subset[OF iIN_not_empty])
apply (simp add: iT_Min)
apply (subgoal_tac "n'  [n'…,d']")
prefer 2
apply (simp add: iIN_iff)
apply (rule ccontr)
apply (frule Suc_in_imp_not_subset_iMOD[where r=r and m=m])
apply (simp add: iIN_Suc)+
apply (simp add: iMOD_1 iIN_iFROM_subset_conv)
done

lemma iIN_iMODb_subset_conv: "
0 < d'
([n'…,d']  [r, mod m, c]) =
(r  n'  m = Suc 0  n' + d'  r + m * c)"
apply (rule iffI)
apply (frule subset_trans[OF _ iMODb_iMOD_subset_same])
apply (simp add: iIN_iMOD_subset_conv iMODb_mod_1 iIN_subset_conv)
apply (clarsimp simp: iMODb_mod_1 iIN_subset_conv)
done

lemma iTILL_subset_conv: "([…n']  […n]) = (n'  n)"
by (simp add: iTILL_def)

lemma iTILL_iFROM_subset_conv: "([…n']  [n…]) = (n = 0)"
apply (rule iffI)
apply (drule subsetD[of _ _ ])
apply (simp add: iT_iff)+
apply (simp add: iFROM_0)
done

lemma iTILL_iIN_subset_conv: "([…n']  [n…,d]) = (n = 0  n'  d)"
apply (rule iffI)
apply (frule iMin_subset[OF iTILL_not_empty])
apply (drule Max_subset[OF iTILL_not_empty _ iIN_finite])
apply (simp add: iT_Min iT_Max)
apply (simp add: iIN_0_iTILL_conv iTILL_subset_conv)
done

lemma iTILL_iMOD_subset_conv: "
0 < n'  ([…n']  [r, mod m]) = (r = 0  m = Suc 0)"
apply (drule iIN_iMOD_subset_conv[of n'  r m])
apply (simp add: iIN_0_iTILL_conv)
done

lemma iTILL_iMODb_subset_conv: "
0 < n'  ([…n']  [r, mod m, c]) = (r = 0  m = Suc 0  n'  r + m * c)"
apply (drule iIN_iMODb_subset_conv[of n'  r m c])
apply (simp add: iIN_0_iTILL_conv)
done

lemma iMOD_iFROM_subset_conv: "([r', mod m'])  [n…] = (n  r')"
by (fastforce simp: subset_iff iT_iff)

lemma iMODb_iFROM_subset_conv: "([r', mod m', c']  [n…]) = (n  r')"
by (fastforce simp: subset_iff iT_iff)

lemma iMODb_iIN_subset_conv: "
([r', mod m', c']  [n…,d]) = (n  r'  r' + m' * c'  n + d)"
by (fastforce simp: subset_iff iT_iff)

lemma iMODb_iTILL_subset_conv: "
([r', mod m', c']  […n]) = (r' + m' * c'  n)"
by (fastforce simp: subset_iff iT_iff)

lemma iMOD_0_subset_conv: "([r', mod 0]  [r, mod m]) = (r' mod m = r mod m    r  r')"
by (fastforce simp: iMOD_0 iIN_0 singleton_subset_conv iMOD_iff)

lemma iMOD_subset_conv: "0 < m
([r', mod m']  [r, mod m]) =
(r' mod m = r mod m    r  r'    m' mod m = 0)"
apply (rule iffI)
apply (frule subsetD[of _ _ r'])
apply (simp add: iMOD_iff)
apply (drule iMOD_subset_imp_divisor_mod_0)
apply (simp add: iMOD_iff)
apply (rule subsetI)
apply (simp add: iMOD_iff, elim conjE)
apply (drule mod_eq_mod_0_imp_mod_eq[where m'=m' and m=m])
apply simp+
done

lemma iMODb_subset_mod_0_conv: "
([r', mod m', c']  [r, mod 0, c ]) = (r'=r  (m'=0  c'=0))"
by (simp add: iMODb_mod_0 iIN_0 iMODb_singleton_subset_conv)

lemma iMODb_subset_0_conv: "
([r', mod m', c']  [r, mod m, 0 ]) = (r'=r  (m'=0  c'=0))"
by (simp add: iMODb_0 iIN_0 iMODb_singleton_subset_conv)

lemma iMODb_0_subset_conv: "
([r', mod m', 0]  [r, mod m, c ]) = (r'  [r, mod m, c])"
by (simp add: iMODb_0 iIN_0)

lemma iMODb_mod_0_subset_conv: "
([r', mod 0, c']  [r, mod m, c ]) = (r'  [r, mod m, c])"
by (simp add: iMODb_mod_0 iIN_0)

lemma iMODb_subset_conv': " 0 < c; 0 < c'
([r', mod m', c']  [r, mod m, c]) =
(r' mod m = r mod m    r  r'    m' mod m = 0
r' + m' * c'  r + m * c)"
apply (rule iffI)
apply (frule iMODb_subset_imp_iMOD_subset, assumption)
apply (drule iMOD_subset_imp_divisor_mod_0)
apply (frule subsetD[OF _ iMinI_ex2[OF iMODb_not_empty]])
apply (drule Max_subset[OF iMODb_not_empty _ iMODb_finite])
apply (simp add: iMODb_iff iMODb_Min iMODb_Max)
apply (elim conjE)
apply (case_tac "m = 0", simp add: iMODb_mod_0)
apply (simp add: iMOD_subset_imp_iMODb_subset iMOD_subset_conv)
done

lemma iMODb_subset_conv: " 0 < m'; 0 < c'
([r', mod m', c']  [r, mod m, c]) =
(r' mod m = r mod m    r  r'    m' mod m = 0
r' + m' * c'  r + m * c)"
apply (case_tac "c = 0")
apply (simp add: iMODb_0 iIN_0 iMODb_singleton_subset_conv linorder_not_le, intro impI)
apply (case_tac "r' < r", simp)
apply (simp add: linorder_not_less)
apply (insert add_less_le_mono[of  "m'  c'" r r'])
apply simp
apply (simp add: iMODb_subset_conv')
done

lemma iMODb_iMOD_subset_conv: "0 < c'
([r', mod m', c']  [r, mod m]) =
(r' mod m = r mod m    r  r'    m' mod m = 0)"
apply (rule iffI)
apply (frule subsetD[OF _ iMinI_ex2[OF iMODb_not_empty]])
apply (simp add: iMODb_Min iMOD_iff, elim conjE)
apply (simp add: iMODb_iMOD_iTILL_conv)
apply (subgoal_tac "[ r', mod m', c' ]  [ r, mod m ]  […r' + m' * c']")
prefer 2
apply (simp add: iMODb_iMOD_iTILL_conv)
apply (simp add: iMOD_iTILL_iMODb_conv iMODb_subset_imp_divisor_mod_0)
apply (rule subset_trans[OF iMODb_iMOD_subset_same])
apply (case_tac "m = 0", simp)
apply (simp add: iMOD_subset_conv)
done

lemmas iT_subset_conv =
iFROM_subset_conv
iFROM_iMOD_subset_conv
iTILL_subset_conv
iTILL_iFROM_subset_conv
iTILL_iIN_subset_conv
iTILL_iMOD_subset_conv
iTILL_iMODb_subset_conv
iIN_subset_conv
iIN_iFROM_subset_conv
iIN_iTILL_subset_conv
iIN_iMOD_subset_conv
iIN_iMODb_subset_conv
iMOD_subset_conv
iMOD_iFROM_subset_conv
iMODb_subset_conv'
iMODb_subset_conv
iMODb_iFROM_subset_conv
iMODb_iIN_subset_conv
iMODb_iTILL_subset_conv
iMODb_iMOD_subset_conv

lemma iFROM_subset: "n  n'  [n'…]  [n…]"
by (simp add: iFROM_subset_conv)

lemma not_iFROM_iIN_subset: "¬ [n'…]  [n…,d]"
apply (rule ccontr, simp)
apply (drule subsetD[of _ _ "max n' (Suc (n  d))"])
apply (simp add: iFROM_iff)
apply (simp add: iIN_iff)
done

lemma not_iFROM_iTILL_subset: "¬ [n'…]  […n]"
by (simp add: iIN_0_iTILL_conv [symmetric] not_iFROM_iIN_subset)

lemma not_iFROM_iMOD_subset: "m  Suc 0  ¬ [n'…]  [r, mod m]"
apply (rule Suc_in_imp_not_subset_iMOD[of n'])
apply (simp add: iT_iff)+
done

lemma not_iFROM_iMODb_subset: "¬ [n'…]  [r, mod m, c]"
by (rule infinite_not_subset_finite[OF iFROM_infinite iMODb_finite])

lemma iIN_subset: " n  n'; n' + d'  n + d   [n'…,d']  [n…,d]"
by (simp add: iIN_subset_conv)

lemma iIN_iFROM_subset: "n  n'  [n'…,d']  [n…]"
by (simp add: subset_iff iT_iff)

lemma iIN_iTILL_subset: "n' + d'  n  [n'…,d']  […n]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_subset)

lemma not_iIN_iMODb_subset: " 0 < d'; m  Suc 0   ¬ [n'…,d']  [r, mod m, c]"
apply (rule Suc_in_imp_not_subset_iMODb[of n'])
apply (simp add: iIN_iff)+
done

lemma not_iIN_iMOD_subset: " 0 < d'; m  Suc 0   ¬ [n'…,d']  [r, mod m]"
apply (rule ccontr, simp)
apply (case_tac "r  n' + d'")
apply (drule Int_greatest[OF _ iIN_iTILL_subset[OF order_refl]])
apply (simp add: iMOD_iTILL_iMODb_conv not_iIN_iMODb_subset)
apply (drule subsetD[of _ _ "n'd'"])
apply (simp add: iT_iff)+
done

lemma iTILL_subset: "n'  n  […n']  […n]"
by (rule iTILL_subset_conv[THEN iffD2])

lemma iTILL_iFROM_subset: "([…n']  [0…])"
by (simp add: iFROM_0)

lemma iTILL_iIN_subset: "n'  d  ([…n']  [0…,d])"
by (simp add: iIN_0_iTILL_conv iTILL_subset)

lemma not_iTILL_iMOD_subset: "
0 < n'; m  Suc 0   ¬ […n']  [r, mod m]"
by (simp add: iIN_0_iTILL_conv[symmetric] not_iIN_iMOD_subset)

lemma not_iTILL_iMODb_subset: "
0 < n'; m  Suc 0   ¬ […n']  [r, mod m, c]"
by (simp add: iIN_0_iTILL_conv[symmetric] not_iIN_iMODb_subset)

lemma iMOD_iFROM_subset: "n  r'  [r', mod m']  [n…]"
by (rule iMOD_iFROM_subset_conv[THEN iffD2])

lemma not_iMOD_iIN_subset: "0 < m'  ¬ [r', mod m']  [n…,d]"
by (rule infinite_not_subset_finite[OF iMOD_infinite iIN_finite])

lemma not_iMOD_iTILL_subset: "0 < m'  ¬ [r', mod m']  […n]"
by (rule infinite_not_subset_finite[OF iMOD_infinite iTILL_finite])

lemma iMOD_subset: "
r  r'; r' mod m = r mod m; m' mod m = 0   [r', mod m']  [r, mod m]"
apply (case_tac "m = 0", simp)
apply (simp add: iMOD_subset_conv)
done

lemma not_iMOD_iMODb_subset: "0 < m'  ¬ [r', mod m']  [r, mod m, c]"
by (rule infinite_not_subset_finite[OF iMOD_infinite iMODb_finite])

lemma iMODb_iFROM_subset: "n  r'  [r', mod m', c']  [n…]"
by (rule iMODb_iFROM_subset_conv[THEN iffD2])

lemma iMODb_iTILL_subset: "
r' + m' * c'  n  [r', mod m', c']  […n]"
by (rule iMODb_iTILL_subset_conv[THEN iffD2])

lemma iMODb_iIN_subset: "
n  r'; r' + m' * c'  n + d   [r', mod m', c']  [n…,d]"
by (simp add: iMODb_iIN_subset_conv)

lemma iMODb_iMOD_subset: "
r  r'; r' mod m = r mod m; m' mod m = 0   [r', mod m', c']  [r, mod m]"
apply (case_tac "c' = 0")
apply (simp add: iMODb_0 iIN_0 iMOD_iff)
apply (simp add: iMODb_iMOD_subset_conv)
done

lemma iMODb_subset: "
r  r'; r' mod m = r mod m; m' mod m = 0; r' + m' * c'  r + m * c
[r', mod m', c']  [r, mod m, c]"
apply (case_tac "m' = 0")
apply (simp add: iMODb_mod_0 iIN_0 iMODb_iff)
apply (case_tac "c' = 0")
apply (simp add: iMODb_0 iIN_0 iMODb_iff)
apply (simp add: iMODb_subset_conv)
done

lemma iFROM_trans: " y  [x…]; z  [y…]   z  [x…]"
by (rule subsetD[OF iFROM_subset[OF iFROM_D]])

lemma iTILL_trans: " y  […x]; z  […y]   z  […x]"
by (rule subsetD[OF iTILL_subset[OF iTILL_D]])

lemma iIN_trans: "
y  [x…,d]; z  [y…,d']; d'  x + d - y   z  [x…,d]"
by fastforce

lemma iMOD_trans: "
y  [x, mod m]; z  [y, mod m]   z  [x, mod m]"
by (rule subsetD[OF iMOD_subset[OF iMOD_geD iMOD_modD mod_self]])

lemma iMODb_trans: "
y  [x, mod m, c]; z  [y, mod m, c']; m * c'  x + m * c - y
z  [x, mod m, c]"
by fastforce

lemma iMODb_trans': "
y  [x, mod m, c]; z  [y, mod m, c']; c'  x div m + c - y div m
z  [x, mod m, c]"
apply (rule iMODb_trans[where c'=c'], assumption+)
apply (frule iMODb_geD, frule div_le_mono[of x y m])
apply (drule mult_le_mono[OF le_refl, of _ _ m])
apply (simp add: add_mult_distrib2 diff_mult_distrib2 minus_mod_eq_mult_div [symmetric])
apply (simp add: iMODb_iff)
done

subsubsection ‹Equality of intervals›

lemma iFROM_eq_conv: "([n…] = [n'…]) = (n = n')"
apply (rule iffI)
apply (drule set_eq_subset[THEN iffD1])
apply (simp add: iFROM_subset_conv)
apply simp
done

lemma iIN_eq_conv: "([n…,d] = [n'…,d']) = (n = n'  d = d')"
apply (rule iffI)
apply (drule set_eq_subset[THEN iffD1])
apply (simp add: iIN_subset_conv)
apply simp
done

lemma iTILL_eq_conv: "([…n] = […n']) = (n = n')"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_eq_conv)

lemma iMOD_0_eq_conv: "([r, mod 0] = [r', mod m']) = (r = r'  m' = 0)"
apply (simp add: iMOD_0 iIN_0)
apply (simp add: iMOD_singleton_eq_conv eq_sym_conv[of "{r}"] eq_sym_conv[of "r"])
done

lemma iMOD_eq_conv: "0 < m  ([r, mod m] = [r', mod m']) = (r = r'  m = m')"
apply (case_tac "m' = 0")
apply (simp add: eq_sym_conv[of "[r, mod m]"] iMOD_0_eq_conv)
apply (rule iffI)
apply (fastforce simp add: set_eq_subset iMOD_subset_conv)
apply simp
done

lemma iMODb_mod_0_eq_conv: "
([r, mod 0, c] = [r', mod m', c']) = (r = r'  (m' = 0  c' = 0))"
apply (simp add: iMODb_mod_0 iIN_0)
apply (fastforce simp: iMODb_singleton_eq_conv eq_sym_conv[of "{r}"])
done

lemma iMODb_0_eq_conv: "
([r, mod m, 0] = [r', mod m', c']) = (r = r'  (m' = 0  c' = 0))"
apply (simp add: iMODb_0 iIN_0)
apply (fastforce simp: iMODb_singleton_eq_conv eq_sym_conv[of "{r}"])
done

lemma iMODb_eq_conv: " 0 < m; 0 < c
([r, mod m, c] = [r', mod m', c']) = (r = r'  m = m'  c = c')"
apply (case_tac "c' = 0")
apply (simp add: iMODb_0 iIN_0 iMODb_singleton_eq_conv)
apply (rule iffI)
apply (fastforce simp: set_eq_subset iMODb_subset_conv')
apply simp
done

lemma iMOD_iFROM_eq_conv: "([n…] = [r, mod m]) = (n = r  m = Suc 0)"
by (fastforce simp: iMOD_1[symmetric] iMOD_eq_conv)

lemma iMODb_iIN_0_eq_conv: "
([n…,0] = [r, mod m, c]) = (n = r  (m = 0  c = 0))"
by (simp add: iIN_0 eq_commute[of "{n}"] eq_commute[of n] iMODb_singleton_eq_conv)

lemma iMODb_iIN_eq_conv: "
0 < d  ([n…,d] = [r, mod m, c]) = (n = r  m = Suc 0  c = d)"
by (fastforce simp: iMODb_mod_1[symmetric] iMODb_eq_conv)

subsubsection ‹Inequality of intervals›

lemma iFROM_iIN_neq: "[n'…]  [n…,d]"
apply (rule ccontr)
apply (insert iFROM_infinite[of n'], insert iIN_finite[of n d])
apply simp
done

corollary iFROM_iTILL_neq: "[n'…]  […n]"
by (simp add: iIN_0_iTILL_conv[symmetric] iFROM_iIN_neq)

corollary iFROM_iMOD_neq: "m  Suc 0  [n…]  [r, mod m]"
apply (subgoal_tac "n  [n…]")
prefer 2
apply (simp add: iFROM_iff)
apply (simp add: Suc_in_imp_neq_iMOD iFROM_Suc)
done
corollary iFROM_iMODb_neq: "[n…]  [r, mod m, c]"
apply (rule ccontr)
apply (insert iMODb_finite[of r m c], insert iFROM_infinite[of n])
apply simp
done

corollary iIN_iMOD_neq: "0 < m  [n…,d]  [r, mod m]"
apply (rule ccontr)
apply (insert iMOD_infinite[of m r], insert iIN_finite[of n d])
apply simp
done

corollary iIN_iMODb_neq2: " m  Suc 0; 0 < d   [n…,d]  [r, mod m, c]"
apply (subgoal_tac "n  [n…,d]")
prefer 2
apply (simp add: iIN_iff)
apply (simp add: Suc_in_imp_neq_iMODb iIN_Suc)
done

lemma iIN_iMODb_neq: " 2  m; 0 < c   [n…,d]  [r, mod m, c]"
apply (simp add: nat_ge2_conv, elim conjE)
apply (case_tac "d=0")
apply (rule not_sym)
apply (simp add: iIN_0 iMODb_singleton_eq_conv)
apply (simp add: iIN_iMODb_neq2)
done

lemma iTILL_iIN_neq: "0 < n  […n']  [n…,d]"
by (fastforce simp: set_eq_iff iT_iff)

corollary iTILL_iMOD_neq: "0 < m  […n]  [r, mod m]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_iMOD_neq)

corollary iTILL_iMODb_neq: "
m  Suc 0; 0 < n   […n]  [r, mod m, c]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_iMODb_neq2)

lemma iMOD_iMODb_neq: "0 < m  [r, mod m]  [r', mod m', c']"
apply (rule ccontr)
apply (insert iMODb_finite[of r' m' c'], insert iMOD_infinite[of m r])
apply simp
done

lemmas iT_neq =
iFROM_iTILL_neq iFROM_iIN_neq iFROM_iMOD_neq iFROM_iMODb_neq
iTILL_iIN_neq iTILL_iMOD_neq iTILL_iMODb_neq
iIN_iMOD_neq  iIN_iMODb_neq iIN_iMODb_neq2
iMOD_iMODb_neq

subsection ‹Union and intersection of intervals›

lemma iFROM_union': "[n…]  [n'…] = [min n n'…]"
by (fastforce simp: iFROM_iff)

corollary iFROM_union: "n  n'  [n…]  [n'…] = [n…]"
by (simp add: iFROM_union' min_eqL)

lemma iFROM_inter': "[n…]  [n'…] = [max n n'…]"
by (fastforce simp: iFROM_iff)

corollary iFROM_inter: "n'  n  [n…]  [n'…] = [n…]"
by (simp add: iFROM_inter' max_eqL)

lemma iTILL_union': "[…n]  […n'] = […max n n']"
by (fastforce simp: iTILL_iff)

corollary iTILL_union: "n'  n  […n]  […n'] = […n]"
by (simp add: iTILL_union' max_eqL)

lemma iTILL_iFROM_union: "n  n'  […n']  [n…] = UNIV"
by (fastforce simp: iT_iff)

lemma iTILL_inter': "[…n]  […n'] = […min n n']"
by (fastforce simp: iT_iff)

corollary iTILL_inter: "n  n'  […n]  […n'] = […n]"
by (simp add: iTILL_inter' min_eqL)

text ‹
Union and intersection for iIN
only when there intersection is not empty and
none of them is other's subset,
for instance:
..  n    ..   n+d
..      n'    ..   n'+d'
›
lemma iIN_union: "
n  n'; n'  Suc (n + d); n + d  n' + d'
[n…,d]  [n'…,d'] = [n…,n' - n + d'] "
by (fastforce simp add: iIN_iff)

(* The case of the second interval starting directly after the first one *)
lemma iIN_append_union: "
[n…,d]  [n + d…,d'] = [n…,d + d']"
by (simp add: iIN_union)

lemma iIN_append_union_Suc: "
[n…,d]  [Suc (n + d)…,d'] = [n…,Suc (d + d')]"
by (simp add: iIN_union)

lemma iIN_append_union_pred: "
0 < d  [n…,d - Suc 0]  [n + d…,d'] = [n…,d + d']"
by (simp add: iIN_union)

lemma iIN_iFROM_union: "
n'  Suc (n + d)  [n…,d]  [n'…] = [min n n'…]"
by (fastforce simp: iIN_iff)

lemma iIN_iFROM_append_union: "
[n…,d]  [n + d…] = [n…]"
by (simp add: iIN_iFROM_union min_eqL)

lemma iIN_iFROM_append_union_Suc: "
[n…,d]  [Suc (n + d)…] = [n…]"
by (simp add: iIN_iFROM_union min_eqL)

lemma iIN_iFROM_append_union_pred: "
0 < d  [n…,d - Suc 0]  [n + d…] = [n…]"
by (simp add: iIN_iFROM_union min_eqL)

lemma iIN_inter: "
n  n'; n'  n + d; n + d  n' + d'
[n…,d]  [n'…,d'] = [n'…,n + d - n']"
by (fastforce simp: iIN_iff)

lemma iMOD_union: "
r  r'; r mod m = r' mod m
[r, mod m]  [r', mod m] = [r, mod m]"
by (fastforce simp: iT_iff)
lemma iMOD_union': "
r mod m = r' mod m
[r, mod m]  [r', mod m] = [min r r', mod m]"
apply (case_tac "r  r'")
apply (fastforce simp: iMOD_union min_eq)+
done

lemma iMOD_inter: "
r  r'; r mod m = r' mod m
[r, mod m]  [r', mod m] = [r', mod m]"
by (fastforce simp: iT_iff)

lemma iMOD_inter': "
r mod m = r' mod m
[r, mod m]  [r', mod m] = [max r r', mod m]"
apply (case_tac "r  r'")
apply (fastforce simp: iMOD_inter max_eq)+
done

lemma iMODb_union: "
r  r'; r mod m = r' mod m; r'  r + m * c; r + m * c  r' + m * c'
[r, mod m, c]  [r', mod m, c'] = [r, mod m, r' div m - r div m + c']"
apply (rule set_eqI)
apply (simp add: iMODb_iff)
apply (drule sym[of "r  m"], simp)
apply (fastforce simp: add_mult_distrib2 diff_mult_distrib2 minus_mod_eq_mult_div [symmetric])
done

lemma iMODb_append_union: "
[r, mod m, c]  [ r + m * c, mod m, c'] = [r, mod m, c + c']"
apply (insert iMODb_union[of r "r  m  c" m c c'])
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0)
apply simp
done

lemma iMODb_iMOD_append_union': "
r mod m = r' mod m; r'  r + m * Suc c
[r, mod m, c]  [ r', mod m ] = [min r r', mod m]"
apply (subgoal_tac "(min r r') mod m = r' mod m")
prefer 2
apply (simp add: min_def)
apply (rule set_eqI)
apply (simp add: iT_iff)
apply (drule sym[of "r  m"], simp)
apply (rule iffI)
apply fastforce
apply (clarsimp simp: linorder_not_le)
apply (case_tac "r  r'")
apply (simp add: min_eqL)
apply (rule add_le_imp_le_right[of _ m])
apply simp+
done

lemma iMODb_iMOD_append_union: "
r  r'; r mod m = r' mod m; r'  r + m * Suc c
[r, mod m, c]  [ r', mod m ] = [r, mod m]"
by (simp add: iMODb_iMOD_append_union' min_eqL)

lemma iMODb_append_union_Suc: "
[r, mod m, c]  [ r + m * Suc c, mod m, c'] = [r, mod m, Suc (c + c')]"
apply (subst insert_absorb[of "r  m  c" "r  m c   r  m  Suc c  m c'", symmetric])
apply (simp add: iT_iff)
apply (simp del: Un_insert_right add: Un_insert_right[symmetric] add.commute[of m] add.assoc[symmetric] iMODb_Suc_pred_insert_conv)
apply (simp add: iMODb_append_union)
done

lemma iMODb_append_union_pred: "
0 < c  [r, mod m, c - Suc 0]  [ r + m * c, mod m, c'] = [r, mod m, c + c']"
by (insert iMODb_append_union_Suc[of r m "c  Suc " c'], simp)

lemma iMODb_inter: "
r  r'; r mod m = r' mod m; r'  r + m * c; r + m * c  r' + m * c'
[r, mod m, c]  [r', mod m, c'] = [r', mod m, c - (r'-r) div m]"
apply (rule set_eqI)
apply (simp add: iMODb_iff)
apply (simp add: diff_mult_distrib2)
apply (simp add: mult.commute[of _ "(r' - r) div m"])
apply (simp add: mod_0_div_mult_cancel[THEN iffD1, OF mod_eq_imp_diff_mod_0])
apply fastforce
done

lemmas iT_union' =
iFROM_union'
iTILL_union'
iMOD_union'
iMODb_iMOD_append_union'
lemmas iT_union =
iFROM_union
iTILL_union
iTILL_iFROM_union
iIN_union
iIN_iFROM_union
iMOD_union
iMODb_union
lemmas iT_union_append =
iIN_append_union
iIN_append_union_Suc
iIN_append_union_pred
iIN_iFROM_append_union
iIN_iFROM_append_union_Suc
iIN_iFROM_append_union_pred
iMODb_append_union
iMODb_iMOD_append_union
iMODb_append_union_Suc
iMODb_append_union_pred

lemmas iT_inter' =
iFROM_inter'
iTILL_inter'
iMOD_inter'
lemmas iT_inter =
iFROM_inter
iTILL_inter
iIN_inter
iMOD_inter
iMODb_inter

lemma mod_partition_Union: "
0 < m  (k. A  [k * m…,m - Suc 0]) = A"
apply simp
apply (rule subst[where s= and P="λx. A  x  A"])
apply (rule set_eqI)
apply (simp add: iT_iff)
apply (rule_tac x="x div m" in exI)
apply (simp add: div_mult_cancel)
apply (simp add: Suc_mod_le_divisor)
apply simp
done

lemma finite_mod_partition_Union: "
0 < m; finite A
(kMax A div m. A  [k*m…,m - Suc 0]) = A"
apply (rule subst[OF mod_partition_Union[of m], where
P="λx. (kMax A  m. A  kmm  Suc )  x"])
apply assumption
apply (rule set_eqI)
apply (simp add: iIN_iff)
apply (rule iffI, blast)
apply clarsimp
apply (rename_tac x x1)
apply (rule_tac x="x div m" in bexI)
apply (frule in_imp_not_empty[where A=A])
apply (frule_tac Max_ge, assumption)
apply (cut_tac n=x and k="x div m" and m=m in div_imp_le_less)
apply clarsimp+
apply (drule_tac m=x in less_imp_le_pred)
apply (simp add: div_le_mono)
done

lemma mod_partition_is_disjoint: "
0 < (m::nat); k  k'
(A  [k * m…,m - Suc 0])   (A  [k' * m…,m - Suc 0]) = {}"
apply (clarsimp simp add: all_not_in_conv[symmetric] iT_iff)
apply (subgoal_tac "k.  k * m  x; x  k * m + m - Suc 0   x div m = k")
apply blast
apply (rule le_less_imp_div, assumption)
apply simp
done

subsection ‹Cutting intervals›

(*
lemma "[10…,5] ↓< 12 = [10…,1]"
apply (simp add: iT_iff cut_less_def)
apply (simp add: iT_defs set_interval_defs Collect_conj_eq[symmetric])
apply fastforce
done
*)

lemma iTILL_cut_le: "[…n] ↓≤ t = (if t  n then […t] else […n])"
unfolding i_cut_defs iT_defs atMost_def
by force

corollary iTILL_cut_le1: "t  […n]  […n] ↓≤ t = […t]"
by (simp add: iTILL_cut_le iT_iff)

corollary iTILL_cut_le2: "t  […n]  […n] ↓≤ t = […n]"
by (simp add: iTILL_cut_le iT_iff)

lemma iFROM_cut_le: "
[n…] ↓≤ t =
(if t < n then {} else [n…,t-n])"
by (simp add: set_eq_iff i_cut_mem_iff iT_iff)

corollary iFROM_cut_le1: "t  [n…]  [n…] ↓≤ t = [n…,t - n]"
by (simp add: iFROM_cut_le iT_iff)

lemma iIN_cut_le: "
[n…,d] ↓≤ t = (
if t < n then {} else
if t  n+d then [n…,t-n]
else [n…,d])"
by (force simp: set_eq_iff i_cut_mem_iff iT_iff)

corollary iIN_cut_le1: "
t  [n…,d]  [n…,d] ↓≤