Theory IL_Interval
section ‹Intervals and operations for temporal logic declarations›
theory IL_Interval
imports
"List-Infinite.InfiniteSet2"
"List-Infinite.SetIntervalStep"
begin
subsection ‹Time intervals -- definitions and basic lemmata›
subsubsection ‹Definitions›
type_synonym Time = nat
type_synonym iT = "Time set"
text ‹Infinite interval starting at some natural @{term "n"}.›
definition
iFROM :: "Time ⇒ iT" ("[_…]")
where
"[n…] ≡ {n..}"
text ‹Finite interval starting at @{term "0"} and ending at some natural @{term "n"}.›
definition
iTILL :: "Time ⇒ iT" ("[…_]")
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" ( "[_…,_]")
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 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 (simp add: add.commute[of m])
apply (simp add: add.assoc[symmetric])
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 (drule add_le_imp_le_right)
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 "r-m"], 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 "r-m" _ 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: "[0…] = UNIV"
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: "finite [r, mod 0]"
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 1])
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]"
by (simp add: iMODb_iff less_mod_eq_imp_add_divisor_le)
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
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 _ _ 0])
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' 0 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' 0 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 0 "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 (simp add: add.commute[of _ c] add.commute[of _ "m*c"])
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)
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 mod 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 mod 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 (rule less_mod_eq_imp_add_divisor_le)
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, mod m, c] ∪ [ r + m * Suc c, mod 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 0" 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 (simp add: add.commute[of _ r])
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=UNIV 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 (subst add.commute)
apply (rule le_add_diff)
apply (simp add: Suc_mod_le_divisor)
apply simp
done
lemma finite_mod_partition_Union: "
⟦ 0 < m; finite A ⟧ ⟹
(⋃k≤Max A div m. A ∩ [k*m…,m - Suc 0]) = A"
apply (rule subst[OF mod_partition_Union[of m], where
P="λx. (⋃k≤Max A div m. A ∩ [k*m…,m - Suc 0]) = 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: add.commute[of m])
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 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] ↓≤