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] ↓≤ t = [n…,t - n]"
by (simp add: iIN_cut_le iT_iff)
lemma iMOD_cut_le: "
[r, mod m] ↓≤ t = (
if t < r then {}
else [r, mod m, (t - r) div m])"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iMODb_0 iIN_0 i_cut_empty i_cut_singleton)
apply (case_tac "t < r")
apply (simp add: cut_le_Min_empty iMOD_Min)
apply (clarsimp simp: linorder_not_less set_eq_iff i_cut_mem_iff iT_iff)
apply (rule conj_cong, simp)+
apply (clarsimp simp: minus_mod_eq_mult_div [symmetric])
apply (drule_tac x=r and y=x in le_imp_less_or_eq, erule disjE)
prefer 2
apply simp
apply (drule_tac x=r and y=x and m=m in less_mod_eq_imp_add_divisor_le, simp)
apply (rule iffI)
apply (rule_tac x=x in subst[OF mod_eq_imp_diff_mod_eq[of _ m r t], rule_format], simp+)
apply (subgoal_tac "r + (t - x) mod m ≤ t")
prefer 2
apply (simp add: order_trans[OF add_le_mono2[OF mod_le_divisor]])
apply simp
apply (simp add: le_imp_sub_mod_le)
apply (subgoal_tac "r + (t - r) mod m ≤ t")
prefer 2
apply (rule ccontr)
apply simp
apply simp
done
lemma iMOD_cut_le1: "
t ∈ [r, mod m] ⟹
[r, mod m] ↓≤ t = [r, mod m, (t - r) div m]"
by (simp add: iMOD_cut_le iT_iff)
lemma iMODb_cut_le: "
[r, mod m, c] ↓≤ t = (
if t < r then {}
else if t < r + m * c then [r, mod m, (t - r) div m]
else [r, mod m, c])"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 cut_le_singleton)
apply (case_tac "t < r")
apply (simp add: cut_le_Min_empty iT_Min)
apply (case_tac "r + m * c ≤ t")
apply (simp add: cut_le_Max_all iT_Max iT_finite)
apply (simp add: linorder_not_le linorder_not_less)
apply (rule_tac t=c and s="(r + m * c - r) div m" in subst, simp)
apply (subst iMOD_iTILL_iMODb_conv[symmetric], simp)
apply (simp add: cut_le_Int_right iTILL_cut_le)
apply (simp add: iMOD_iTILL_iMODb_conv)
done
lemma iMODb_cut_le1: "
t ∈ [r, mod m, c] ⟹
[r, mod m, c] ↓≤ t = [r, mod m, (t - r) div m]"
by (clarsimp simp: iMODb_cut_le iT_iff iMODb_mod_0)
lemma iTILL_cut_less: "
[…n] ↓< t = (
if n < t then […n] else
if t = 0 then {}
else […t - Suc 0])"
apply (case_tac "n < t")
apply (simp add: cut_less_Max_all iT_Max iT_finite)
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty)
apply (fastforce simp: nat_cut_less_le_conv iTILL_cut_le)
done
lemma iTILL_cut_less1: "
⟦ t ∈ […n]; 0 < t ⟧ ⟹ […n] ↓< t = […t - Suc 0]"
by (simp add: iTILL_cut_less iT_iff)
lemma iFROM_cut_less: "
[n…] ↓< t = (
if t ≤ n then {}
else [n…,t - Suc n])"
apply (case_tac "t ≤ n")
apply (simp add: cut_less_Min_empty iT_Min)
apply (fastforce simp: nat_cut_less_le_conv iFROM_cut_le)
done
lemma iFROM_cut_less1: "
n < t ⟹ [n…] ↓< t = [n…,t - Suc n]"
by (simp add: iFROM_cut_less)
lemma iIN_cut_less: "
[n…,d] ↓< t = (
if t ≤ n then {} else
if t ≤ n + d then [n…, t - Suc n]
else [n…,d])"
apply (case_tac "t ≤ n")
apply (simp add: cut_less_Min_empty iT_Min )
apply (case_tac "n + d < t")
apply (simp add: cut_less_Max_all iT_Max iT_finite)
apply (fastforce simp: nat_cut_less_le_conv iIN_cut_le)
done
lemma iIN_cut_less1: "
⟦ t ∈ [n…,d]; n < t ⟧ ⟹ [n…,d] ↓< t = [n…, t - Suc n]"
by (simp add: iIN_cut_less iT_iff)
lemma iMOD_cut_less: "
[r, mod m] ↓< t = (
if t ≤ r then {}
else [r, mod m, (t - Suc r) div m])"
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty)
apply (simp add: nat_cut_less_le_conv iMOD_cut_le)
apply fastforce
done
lemma iMOD_cut_less1: "
⟦ t ∈ [r, mod m]; r < t ⟧ ⟹
[r, mod m] ↓< t = [r, mod m, (t - r) div m - Suc 0]"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iMODb_mod_0 iIN_0)
apply (simp add: iMOD_cut_less)
apply (simp add: mod_0_imp_diff_Suc_div_conv mod_eq_imp_diff_mod_0 iT_iff)
done
lemma iMODb_cut_less: "
[r, mod m, c] ↓< t = (
if t ≤ r then {} else
if r + m * c < t then [r, mod m, c]
else [r, mod m, (t - Suc r) div m])"
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty)
apply (simp add: nat_cut_less_le_conv iMODb_cut_le)
apply fastforce
done
lemma iMODb_cut_less1: "⟦ t ∈ [r, mod m, c]; r < t ⟧ ⟹
[r, mod m, c] ↓< t = [r, mod m, (t - r) div m - Suc 0]"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0)
apply (simp add: iMODb_cut_less)
apply (simp add: mod_0_imp_diff_Suc_div_conv mod_eq_imp_diff_mod_0 iT_iff)
done
lemmas iT_cut_le =
iTILL_cut_le
iFROM_cut_le
iIN_cut_le
iMOD_cut_le
iMODb_cut_le
lemmas iT_cut_le1 =
iTILL_cut_le1
iFROM_cut_le1
iIN_cut_le1
iMOD_cut_le1
iMODb_cut_le1
lemmas iT_cut_less =
iTILL_cut_less
iFROM_cut_less
iIN_cut_less
iMOD_cut_less
iMODb_cut_less
lemmas iT_cut_less1 =
iTILL_cut_less1
iFROM_cut_less1
iIN_cut_less1
iMOD_cut_less1
iMODb_cut_less1
lemmas iT_cut_le_less =
iTILL_cut_le
iTILL_cut_less
iFROM_cut_le
iFROM_cut_less
iIN_cut_le
iIN_cut_less
iMOD_cut_le
iMOD_cut_less
iMODb_cut_le
iMODb_cut_less
lemmas iT_cut_le_less1 =
iTILL_cut_le1
iTILL_cut_less1
iFROM_cut_le1
iFROM_cut_less1
iIN_cut_le1
iIN_cut_less1
iMOD_cut_le1
iMOD_cut_less1
iMODb_cut_le1
iMODb_cut_less1
lemma iTILL_cut_ge: "
[…n] ↓≥ t = (if n < t then {} else [t…,n-t])"
by (force simp: i_cut_mem_iff iT_iff)
corollary iTILL_cut_ge1: "t ∈ […n] ⟹ […n] ↓≥ t = [t…,n-t]"
by (simp add: iTILL_cut_ge iT_iff)
corollary iTILL_cut_ge2: "t ∉ […n] ⟹ […n] ↓≥ t = {}"
by (simp add: iTILL_cut_ge iT_iff)
lemma iTILL_cut_greater: "
[…n] ↓> t = (if n ≤ t then {} else [Suc t…,n - Suc t])"
by (force simp: i_cut_mem_iff iT_iff)
corollary iTILL_cut_greater1: "
t ∈ […n] ⟹ t < n ⟹ […n] ↓> t = [Suc t…,n - Suc t]"
by (simp add: iTILL_cut_greater iT_iff)
corollary iTILL_cut_greater2: "t ∉ […n] ⟹ […n] ↓> t = {}"
by (simp add: iTILL_cut_greater iT_iff)
lemma iFROM_cut_ge: "
[n…] ↓≥ t = (if n ≤ t then [t…] else [n…])"
by (force simp: i_cut_mem_iff iT_iff)
corollary iFROM_cut_ge1: "t ∈ [n…] ⟹ [n…] ↓≥ t = [t…]"
by (simp add: iFROM_cut_ge iT_iff)
lemma iFROM_cut_greater: "
[n…] ↓> t = (if n ≤ t then [Suc t…] else [n…])"
by (force simp: i_cut_mem_iff iT_iff)
corollary iFROM_cut_greater1: "
t ∈ [n…] ⟹ [n…] ↓> t = [Suc t…]"
by (simp add: iFROM_cut_greater iT_iff)
lemma iIN_cut_ge: "
[n…,d] ↓≥ t = (
if t < n then [n…,d] else
if t ≤ n+d then [t…,n+d-t]
else {})"
by (force simp: i_cut_mem_iff iT_iff)
corollary iIN_cut_ge1: "t ∈ [n…,d] ⟹
[n…,d] ↓≥ t = [t…,n+d-t]"
by (simp add: iIN_cut_ge iT_iff)
corollary iIN_cut_ge2: "t ∉ [n…,d] ⟹
[n…,d] ↓≥ t = (if t < n then [n…,d] else {})"
by (simp add: iIN_cut_ge iT_iff)
lemma iIN_cut_greater: "
[n…,d] ↓> t = (
if t < n then [n…,d] else
if t < n+d then [Suc t…,n + d - Suc t]
else {})"
by (force simp: i_cut_mem_iff iT_iff)
corollary iIN_cut_greater1: "
⟦ t ∈ [n…,d]; t < n + d ⟧⟹
[n…,d] ↓> t = [Suc t…,n + d - Suc t]"
by (simp add: iIN_cut_greater iT_iff)
lemma mod_cut_greater_aux_t_less: "
⟦ 0 < (m::nat); r ≤ t ⟧ ⟹
t < t + m - (t - r) mod m"
by (simp add: less_add_diff add.commute)
lemma mod_cut_greater_aux_le_x: "
⟦ (r::nat) ≤ t; t < x; x mod m = r mod m⟧ ⟹
t + m - (t - r) mod m ≤ x"
apply (insert diff_mod_le[of t r m])
apply (subst diff_add_assoc2, simp)
apply (rule less_mod_eq_imp_add_divisor_le, simp)
apply (simp add: sub_diff_mod_eq)
done
lemma iMOD_cut_greater: "
[r, mod m] ↓> t = (
if t < r then [r, mod m] else
if m = 0 then {}
else [t + m - (t - r) mod m, mod m])"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iIN_0 i_cut_singleton)
apply (case_tac "t < r")
apply (simp add: iT_Min cut_greater_Min_all)
apply (simp add: linorder_not_less)
apply (simp add: set_eq_iff i_cut_mem_iff iT_iff, clarify)
apply (subgoal_tac "(t - r) mod m ≤ t")
prefer 2
apply (rule order_trans[OF mod_le_dividend], simp)
apply (simp add: diff_add_assoc2 del: add_diff_assoc2)
apply (simp add: sub_diff_mod_eq del: add_diff_assoc2)
apply (rule conj_cong, simp)
apply (rule iffI)
apply clarify
apply (rule less_mod_eq_imp_add_divisor_le)
apply simp
apply (simp add: sub_diff_mod_eq)
apply (subgoal_tac "t < x")
prefer 2
apply (rule_tac y="t - (t - r) mod m + m" in order_less_le_trans)
apply (simp add: mod_cut_greater_aux_t_less)
apply simp+
done
lemma iMOD_cut_greater1: "
t ∈ [r, mod m] ⟹
[r, mod m] ↓> t = (
if m = 0 then {}
else [t + m, mod m])"
by (simp add: iMOD_cut_greater iT_iff mod_eq_imp_diff_mod_0)
lemma iMODb_cut_greater_aux: "
⟦ 0 < m; t < r + m * c; r ≤ t⟧ ⟹
(r + m * c - (t + m - (t - r) mod m)) div m =
c - Suc ((t - r) div m)"
apply (subgoal_tac "r ≤ t + m - (t - r) mod m")
prefer 2
apply (rule order_trans[of _ t], simp)
apply (simp add: mod_cut_greater_aux_t_less less_imp_le)
apply (rule_tac t="(r + m * c - (t + m - (t - r) mod m))" and s="m * (c - Suc ((t - r) div m))" in subst)
apply (simp add: diff_mult_distrib2 minus_mod_eq_mult_div [symmetric] del: diff_diff_left)
apply simp
done
lemma iMODb_cut_greater: "
[r, mod m, c] ↓> t = (
if t < r then [r, mod m, c] else
if r + m * c ≤ t then {}
else [t + m - (t - r) mod m, mod m, c - Suc ((t-r) div m)])"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 i_cut_singleton)
apply (case_tac "r + m * c ≤ t")
apply (simp add: cut_greater_Max_empty iT_Max iT_finite)
apply (case_tac "t < r")
apply (simp add: cut_greater_Min_all iT_Min)
apply (simp add: linorder_not_less linorder_not_le)
apply (rule_tac t="[ r, mod m, c ]" and s="[ r, mod m ] ∩ […r + m * c]" in subst)
apply (simp add: iMOD_iTILL_iMODb_conv)
apply (simp add: i_cut_Int_left iMOD_cut_greater)
apply (subst iMOD_iTILL_iMODb_conv)
apply (rule mod_cut_greater_aux_le_x, simp+)
apply (simp add: iMODb_cut_greater_aux)
done
lemma iMODb_cut_greater1: "
t ∈ [r, mod m, c] ⟹
[r, mod m, c] ↓> t = (
if r + m * c ≤ t then {}
else [t + m, mod m, c - Suc ((t-r) div m)])"
by (simp add: iMODb_cut_greater iT_iff mod_eq_imp_diff_mod_0)
lemma iMOD_cut_ge: "
[r, mod m] ↓≥ t = (
if t ≤ r then [r, mod m] else
if m = 0 then {}
else [t + m - Suc ((t - Suc r) mod m), mod m])"
apply (case_tac "t = 0")
apply (simp add: cut_ge_0_all)
apply (force simp: nat_cut_greater_ge_conv[symmetric] iMOD_cut_greater)
done
lemma iMOD_cut_ge1: "
t ∈ [r, mod m] ⟹
[r, mod m] ↓≥ t = [t, mod m]"
by (fastforce simp: iMOD_cut_ge)
lemma iMODb_cut_ge: "
[r, mod m, c] ↓≥ t = (
if t ≤ r then [r, mod m, c] else
if r + m * c < t then {}
else [t + m - Suc ((t - Suc r) mod m), mod m, c - (t + m - Suc r) div m])"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 i_cut_singleton)
apply (case_tac "r + m * c < t")
apply (simp add: cut_ge_Max_empty iT_Max iT_finite)
apply (case_tac "t ≤ r")
apply (simp add: cut_ge_Min_all iT_Min)
apply (simp add: linorder_not_less linorder_not_le)
apply (case_tac "r mod m = t mod m")
apply (simp add: diff_mod_pred)
apply (simp add: mod_0_imp_diff_Suc_div_conv mod_eq_diff_mod_0_conv diff_add_assoc2 del: add_diff_assoc2)
apply (subgoal_tac "0 < (t - r) div m")
prefer 2
apply (frule_tac x=r in less_mod_eq_imp_add_divisor_le)
apply (simp add: mod_eq_diff_mod_0_conv)
apply (drule add_le_imp_le_diff2)
apply (drule_tac m=m and k=m in div_le_mono)
apply simp
apply (simp add: set_eq_iff i_cut_mem_iff iT_iff, intro allI)
apply (simp add: mod_eq_diff_mod_0_conv[symmetric])
apply (rule conj_cong, simp)
apply (case_tac "t ≤ x")
prefer 2
apply simp
apply (simp add: diff_mult_distrib2 minus_mod_eq_mult_div [symmetric] mod_eq_diff_mod_0_conv add.commute[of r])
apply (subgoal_tac "Suc ((t - Suc r) mod m) = (t - r) mod m")
prefer 2
apply (clarsimp simp add: diff_mod_pred mod_eq_diff_mod_0_conv)
apply (rule_tac t="[ r, mod m, c ]" and s="[ r, mod m ] ∩ […r + m * c]" in subst)
apply (simp add: iMOD_iTILL_iMODb_conv)
apply (simp add: i_cut_Int_left iMOD_cut_ge)
apply (subst iMOD_iTILL_iMODb_conv)
apply (drule_tac x=t in le_imp_less_or_eq, erule disjE)
apply (rule mod_cut_greater_aux_le_x, simp+)
apply (rule arg_cong [where y="c - (t + m - Suc r) div m"])
apply (drule_tac x=t in le_imp_less_or_eq, erule disjE)
prefer 2
apply simp
apply (simp add: iMODb_cut_greater_aux)
apply (rule arg_cong[where f="(-) c"])
apply (simp add: diff_add_assoc2 del: add_diff_assoc2)
apply (rule_tac t="t - Suc r" and s="t - r - Suc 0" in subst, simp)
apply (subst div_diff1_eq[of _ "Suc 0"])
apply (case_tac "m = Suc 0", simp)
apply simp
done
lemma iMODb_cut_ge1: "
t ∈ [r, mod m, c] ⟹
[r, mod m, c] ↓≥ t = (
if r + m * c < t then {}
else [t, mod m, c - (t - r) div m])"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iT_iff iIN_0 i_cut_singleton)
apply (clarsimp simp: iMODb_cut_ge iT_iff)
apply (simp add: mod_eq_imp_diff_mod_eq_divisor)
apply (rule_tac t="t + m - Suc r" and s="t - r + (m - Suc 0)" in subst, simp)
apply (subst div_add1_eq)
apply (simp add: mod_eq_imp_diff_mod_0)
done
lemma iMOD_0_cut_greater: "
t ∈ [r, mod 0] ⟹ [r, mod 0] ↓> t = {}"
by (simp add: iT_iff iMOD_0 iIN_0 i_cut_singleton)
lemma iMODb_0_cut_greater: "t ∈ [r, mod 0, c] ⟹
[r, mod 0, c] ↓> t = {}"
by (simp add: iT_iff iMODb_mod_0 iIN_0 i_cut_singleton)
lemmas iT_cut_ge =
iTILL_cut_ge
iFROM_cut_ge
iIN_cut_ge
iMOD_cut_ge
iMODb_cut_ge
lemmas iT_cut_ge1 =
iTILL_cut_ge1
iFROM_cut_ge1
iIN_cut_ge1
iMOD_cut_ge1
iMODb_cut_ge1
lemmas iT_cut_greater =
iTILL_cut_greater
iFROM_cut_greater
iIN_cut_greater
iMOD_cut_greater
iMODb_cut_greater
lemmas iT_cut_greater1 =
iTILL_cut_greater1
iFROM_cut_greater1
iIN_cut_greater1
iMOD_cut_greater1
iMODb_cut_greater1
lemmas iT_cut_ge_greater =
iTILL_cut_ge
iTILL_cut_greater
iFROM_cut_ge
iFROM_cut_greater
iIN_cut_ge
iIN_cut_greater
iMOD_cut_ge
iMOD_cut_greater
iMODb_cut_ge
iMODb_cut_greater
lemmas iT_cut_ge_greater1 =
iTILL_cut_ge1
iTILL_cut_greater1
iFROM_cut_ge1
iFROM_cut_greater1
iIN_cut_ge1
iIN_cut_greater1
iMOD_cut_ge1
iMOD_cut_greater1
iMODb_cut_ge1
iMODb_cut_greater1
subsection ‹Cardinality of intervals›
lemma iFROM_card: "card [n…] = 0"
by (simp add: iFROM_infinite)
lemma iTILL_card: "card […n] = Suc n"
by (simp add: iTILL_def)
lemma iIN_card: "card [n…,d] = Suc d"
by (simp add: iIN_def)
lemma iMOD_0_card: "card [r, mod 0] = Suc 0"
by (simp add: iMOD_0 iIN_card)
lemma iMOD_card: "0 < m ⟹ card [r, mod m] = 0"
by (simp add: iMOD_infinite)
lemma iMOD_card_if: "card [r, mod m] = (if m = 0 then Suc 0 else 0)"
by (simp add: iMOD_0_card iMOD_card)
lemma iMODb_mod_0_card: "card [r, mod 0, c] = Suc 0"
by (simp add: iMODb_mod_0 iIN_card)
lemma iMODb_card: "0 < m ⟹ card [r, mod m, c] = Suc c"
apply (induct c)
apply (simp add: iMODb_0 iIN_card)
apply (subst iMODb_Suc_insert_conv[symmetric])
apply (subst card_insert_disjoint)
apply (simp add: iT_finite iT_iff)+
done
lemma iMODb_card_if: "
card [r, mod m, c] = (if m = 0 then Suc 0 else Suc c)"
by (simp add: iMODb_mod_0_card iMODb_card)
lemmas iT_card =
iFROM_card
iTILL_card
iIN_card
iMOD_card_if
iMODb_card_if
text ‹Cardinality with ‹icard››
lemma iFROM_icard: "icard [n…] = ∞"
by (simp add: iFROM_infinite)
lemma iTILL_icard: "icard […n] = enat (Suc n)"
by (simp add: icard_finite iT_finite iT_card)
lemma iIN_icard: "icard [n…,d] = enat (Suc d)"
by (simp add: icard_finite iT_finite iT_card)
lemma iMOD_0_icard: "icard [r, mod 0] = eSuc 0"
by (simp add: icard_finite iT_finite iT_card eSuc_enat)
lemma iMOD_icard: "0 < m ⟹ icard [r, mod m] = ∞"
by (simp add: iMOD_infinite)
lemma iMOD_icard_if: "icard [r, mod m] = (if m = 0 then eSuc 0 else ∞)"
by (simp add: icard_finite iT_finite iT_infinite eSuc_enat iT_card)
lemma iMODb_mod_0_icard: "icard [r, mod 0, c] = eSuc 0"
by (simp add: icard_finite iT_finite eSuc_enat iT_card)
lemma iMODb_icard: "0 < m ⟹ icard [r, mod m, c] = enat (Suc c)"
by (simp add: icard_finite iT_finite iMODb_card)
lemma iMODb_icard_if: "icard [r, mod m, c] = enat (if m = 0 then Suc 0 else Suc c)"
by (simp add: icard_finite iT_finite iMODb_card_if)
lemmas iT_icard =
iFROM_icard
iTILL_icard
iIN_icard
iMOD_icard_if
iMODb_icard_if
subsection ‹Functions ‹inext› and ‹iprev› with intervals›
lemma
iFROM_inext: "t ∈ [n…] ⟹ inext t [n…] = Suc t" and
iTILL_inext: "t < n ⟹ inext t […n] = Suc t" and
iIN_inext: "⟦ n ≤ t; t < n + d ⟧ ⟹ inext t [n…,d] = Suc t"
by (simp add: iT_defs inext_atLeast inext_atMost inext_atLeastAtMost)+
lemma
iFROM_iprev': "t ∈ [n…] ⟹ iprev (Suc t) [n…] = t" and
iFROM_iprev: "n < t ⟹ iprev t [n…] = t - Suc 0" and
iTILL_iprev: "t ∈ […n] ⟹ iprev t […n] = t - Suc 0" and
iIN_iprev: "⟦ n < t; t ≤ n + d ⟧ ⟹ iprev t [n…,d] = t - Suc 0" and
iIN_iprev': "⟦ n ≤ t; t < n + d ⟧ ⟹ iprev (Suc t) [n…,d] = t"
by (simp add: iT_defs iprev_atLeast iprev_atMost iprev_atLeastAtMost)+
lemma iMOD_inext: "t ∈ [r, mod m] ⟹ inext t [r, mod m] = t + m"
by (clarsimp simp add: inext_def iMOD_cut_greater iT_iff iT_Min iT_not_empty mod_eq_imp_diff_mod_0)
lemma iMOD_iprev: "⟦ t ∈ [r, mod m]; r < t ⟧ ⟹ iprev t [r, mod m] = t - m"
apply (case_tac "m = 0", simp add: iMOD_iff)
apply (clarsimp simp add: iprev_def iMOD_cut_less iT_iff iT_Max iT_not_empty minus_mod_eq_mult_div [symmetric])
apply (simp del: add_Suc_right add: add_Suc_right[symmetric] mod_eq_imp_diff_mod_eq_divisor)
apply (simp add: less_mod_eq_imp_add_divisor_le)
done
lemma iMOD_iprev': "t ∈ [r, mod m] ⟹ iprev (t + m) [r, mod m] = t"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iIN_0 iprev_singleton)
apply (simp add: iMOD_iprev iT_iff)
done
lemma iMODb_inext: "
⟦ t ∈ [r, mod m, c]; t < r + m * c ⟧ ⟹
inext t [r, mod m, c] = t + m"
by (clarsimp simp add: inext_def iMODb_cut_greater iT_iff iT_Min iT_not_empty mod_eq_imp_diff_mod_0)
lemma iMODb_iprev: "
⟦ t ∈ [r, mod m, c]; r < t ⟧ ⟹
iprev t [r, mod m, c] = t - m"
apply (case_tac "m = 0", simp add: iMODb_iff)
apply (clarsimp simp add: iprev_def iMODb_cut_less iT_iff iT_Max iT_not_empty minus_mod_eq_mult_div [symmetric])
apply (simp del: add_Suc_right add: add_Suc_right[symmetric] mod_eq_imp_diff_mod_eq_divisor)
apply (simp add: less_mod_eq_imp_add_divisor_le)
done
lemma iMODb_iprev': "
⟦ t ∈ [r, mod m, c]; t < r + m * c ⟧ ⟹
iprev (t + m) [r, mod m, c] = t"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 iprev_singleton)
apply (simp add: iMODb_iprev iT_iff less_mod_eq_imp_add_divisor_le)
done
lemmas iT_inext =
iFROM_inext
iTILL_inext
iIN_inext
iMOD_inext
iMODb_inext
lemmas iT_iprev =
iFROM_iprev'
iFROM_iprev
iTILL_iprev
iIN_iprev
iIN_iprev'
iMOD_iprev
iMOD_iprev'
iMODb_iprev
iMODb_iprev'
lemma iFROM_inext_if: "
inext t [n…] = (if t ∈ [n…] then Suc t else t)"
by (simp add: iFROM_inext not_in_inext_fix)
lemma iTILL_inext_if: "
inext t […n] = (if t < n then Suc t else t)"
by (simp add: iTILL_inext iT_finite iT_Max inext_ge_Max)
lemma iIN_inext_if: "
inext t [n…,d] = (if n ≤ t ∧ t < n + d then Suc t else t)"
by (fastforce simp: iIN_inext iT_iff not_in_inext_fix iT_finite iT_Max inext_ge_Max)
lemma iMOD_inext_if: "
inext t [r, mod m] = (if t ∈ [r, mod m] then t + m else t)"
by (simp add: iMOD_inext not_in_inext_fix)
lemma iMODb_inext_if: "
inext t [r, mod m, c] =
(if t ∈ [r, mod m, c] ∧ t < r + m * c then t + m else t)"
by (fastforce simp: iMODb_inext iT_iff not_in_inext_fix iT_finite iT_Max inext_ge_Max)
lemmas iT_inext_if =
iFROM_inext_if
iTILL_inext_if
iIN_inext_if
iMOD_inext_if
iMODb_inext_if
lemma iFROM_iprev_if: "
iprev t [n…] = (if n < t then t - Suc 0 else t)"
by (simp add: iFROM_iprev iT_Min iprev_le_iMin)
lemma iTILL_iprev_if: "
iprev t […n] = (if t ∈ […n] then t - Suc 0 else t)"
by (simp add: iTILL_iprev not_in_iprev_fix)
lemma iIN_iprev_if: "
iprev t [n…,d] = (if n < t ∧ t ≤ n + d then t - Suc 0 else t)"
by (fastforce simp: iIN_iprev iT_iff not_in_iprev_fix iT_Min iprev_le_iMin)
lemma iMOD_iprev_if: "
iprev t [r, mod m] =
(if t ∈ [r, mod m] ∧ r < t then t - m else t)"
by (fastforce simp add: iMOD_iprev iT_iff not_in_iprev_fix iT_Min iprev_le_iMin)
lemma iMODb_iprev_if: "
iprev t [r, mod m, c] =
(if t ∈ [r, mod m, c] ∧ r < t then t - m else t)"
by (fastforce simp add: iMODb_iprev iT_iff not_in_iprev_fix iT_Min iprev_le_iMin)
lemmas iT_iprev_if =
iFROM_iprev_if
iTILL_iprev_if
iIN_iprev_if
iMOD_iprev_if
iMODb_iprev_if
text ‹
The difference between an element and the next/previous element is constant
if the element is different from Min/Max of the interval›
lemma iFROM_inext_diff_const: "
t ∈ [n…] ⟹ inext t [n…] - t = Suc 0"
by (simp add: iFROM_inext)
lemma iFROM_iprev_diff_const: "
n < t ⟹ t - iprev t [n…] = Suc 0"
by (simp add: iFROM_iprev )
lemma iFROM_iprev_diff_const': "
t ∈ [n…] ⟹ Suc t - iprev (Suc t) [n…] = Suc 0"
by (simp add: iFROM_iprev')
lemma iTILL_inext_diff_const: "
t < n ⟹ inext t […n] - t = Suc 0"
by (simp add: iTILL_inext)
lemma iTILL_iprev_diff_const: "
⟦ t ∈ […n]; 0 < t ⟧ ⟹ t - iprev t […n] = Suc 0"
by (simp add: iTILL_iprev)
lemma iIN_inext_diff_const: "
⟦ n ≤ t; t < n + d ⟧ ⟹ inext t [n…,d] - t = Suc 0"
by (simp add: iIN_inext)
lemma iIN_iprev_diff_const: "
⟦ n < t; t ≤ n + d ⟧ ⟹ t - iprev t [n…,d] = Suc 0"
by (simp add: iIN_iprev)
lemma iIN_iprev_diff_const': "
⟦ n ≤ t; t < n + d ⟧ ⟹ Suc t - iprev (Suc t) [n…,d] = Suc 0"
by (simp add: iIN_iprev)
lemma iMOD_inext_diff_const: "
t ∈ [r, mod m] ⟹ inext t [r, mod m] - t = m"
by (simp add: iMOD_inext)
lemma iMOD_iprev_diff_const': "
t ∈ [r, mod m] ⟹ (t + m) - iprev (t + m) [r, mod m] = m"
by (simp add: iMOD_iprev')
lemma iMOD_iprev_diff_const: "
⟦ t ∈ [r, mod m]; r < t ⟧ ⟹ t - iprev t [r, mod m] = m"
apply (simp add: iMOD_iprev iT_iff)
apply (drule less_mod_eq_imp_add_divisor_le[where m=m], simp+)
done
lemma iMODb_inext_diff_const: "
⟦ t ∈ [r, mod m, c]; t < r + m * c ⟧ ⟹ inext t [r, mod m, c] - t = m"
by (simp add: iMODb_inext)
lemma iMODb_iprev_diff_const': "
⟦ t ∈ [r, mod m, c]; t < r + m * c ⟧ ⟹ (t + m) - iprev (t + m) [r, mod m, c] = m"
by (simp add: iMODb_iprev')
lemma iMODb_iprev_diff_const: "
⟦ t ∈ [r, mod m, c]; r < t ⟧ ⟹ t - iprev t [r, mod m, c] = m"
apply (simp add: iMODb_iprev iT_iff)
apply (drule less_mod_eq_imp_add_divisor_le[where m=m], simp+)
done
lemmas iT_inext_diff_const =
iFROM_inext_diff_const
iTILL_inext_diff_const
iIN_inext_diff_const
iMOD_inext_diff_const
iMODb_inext_diff_const
lemmas iT_iprev_diff_const =
iFROM_iprev_diff_const
iFROM_iprev_diff_const'
iTILL_iprev_diff_const
iIN_iprev_diff_const
iIN_iprev_diff_const'
iMOD_iprev_diff_const'
iMOD_iprev_diff_const
iMODb_iprev_diff_const'
iMODb_iprev_diff_const
subsubsection ‹Mirroring of intervals›
lemma
iIN_mirror_elem: "mirror_elem x [n…,d] = n + n + d - x" and
iTILL_mirror_elem: "mirror_elem x […n] = n - x" and
iMODb_mirror_elem: "mirror_elem x [r, mod m, c] = r + r + m * c - x"
by (simp add: mirror_elem_def nat_mirror_def iT_Min iT_Max)+
lemma iMODb_imirror_bounds: "
r' + m' * c' ≤ l + r ⟹
imirror_bounds [r', mod m', c'] l r = [l + r - r' - m' * c', mod m', c']"
apply (clarsimp simp: set_eq_iff Bex_def imirror_bounds_iff iT_iff)
apply (frule diff_le_mono[of _ _ r'], simp)
apply (simp add: mod_diff_right_eq)
apply (rule iffI)
apply (clarsimp, rename_tac x')
apply (rule_tac a=x' in ssubst[OF mod_diff_right_eq, rule_format], simp+)
apply (simp add: diff_le_mono2)
apply clarsimp
apply (rule_tac x="l+r-x" in exI)
apply (simp add: le_diff_swap)
apply (simp add: le_diff_conv2)
apply (subst mod_sub_eq_mod_swap, simp+)
apply (simp add: mod_diff_right_eq)
done
lemma iIN_imirror_bounds: "
n + d ≤ l + r ⟹ imirror_bounds [n…,d] l r = [l + r - n - d…,d]"
apply (insert iMODb_imirror_bounds[of n "Suc 0" d l r])
apply (simp add: iMODb_mod_1)
done
lemma iTILL_imirror_bounds: "
n ≤ l + r ⟹ imirror_bounds […n] l r = [l + r - n…,n]"
apply (insert iIN_imirror_bounds[of 0 n l r])
apply (simp add: iIN_0_iTILL_conv)
done
lemmas iT_imirror_bounds =
iTILL_imirror_bounds
iIN_imirror_bounds
iMODb_imirror_bounds
lemma iMODb_imirror_ident: "imirror [r, mod m, c] = [r, mod m, c]"
by (simp add: imirror_eq_imirror_bounds iMODb_Min iMODb_Max iMODb_imirror_bounds)
lemma iIN_imirror_ident: "imirror [n…,d] = [n…,d]"
by (simp add: iMODb_mod_1[symmetric] iMODb_imirror_ident)
lemma iTILL_imirror_ident: "imirror […n] = […n]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_imirror_ident)
lemmas iT_imirror_ident =
iTILL_imirror_ident
iIN_imirror_ident
iMODb_imirror_ident
subsubsection ‹Functions @{term inext_nth} and @{term iprev_nth} on intervals›
lemma iFROM_inext_nth : "[n…] → a = n + a"
by (simp add: iT_defs inext_nth_atLeast)
lemma iIN_inext_nth : "a ≤ d ⟹ [n…,d] → a = n + a"
by (simp add: iT_defs inext_nth_atLeastAtMost)
lemma iIN_iprev_nth: "a ≤ d ⟹ [n…,d] ← a = n + d - a"
by (simp add: iT_defs iprev_nth_atLeastAtMost)
lemma iIN_inext_nth_if : "
[n…,d] → a = (if a ≤ d then n + a else n + d)"
by (simp add: iIN_inext_nth inext_nth_card_Max iT_finite iT_not_empty iT_Max iT_card)
lemma iIN_iprev_nth_if: "
[n…,d] ← a = (if a ≤ d then n + d - a else n)"
by (simp add: iIN_iprev_nth iprev_nth_card_iMin iT_finite iT_not_empty iT_Min iT_card)
lemma iTILL_inext_nth : "a ≤ n ⟹ […n] → a = a"
by (simp add: iTILL_def inext_nth_atMost)
lemma iTILL_inext_nth_if : "
[…n] → a = (if a ≤ n then a else n)"
by (insert iIN_inext_nth_if[of 0 n a], simp add: iIN_0_iTILL_conv)
lemma iTILL_iprev_nth: "a ≤ n ⟹ […n] ← a = n - a"
by (simp add: iTILL_def iprev_nth_atMost)
lemma iTILL_iprev_nth_if: "
[…n] ← a= (if a ≤ n then n - a else 0)"
by (insert iIN_iprev_nth_if[of 0 n a], simp add: iIN_0_iTILL_conv)
lemma iMOD_inext_nth: "[r, mod m] → a = r + m * a"
apply (induct a)
apply (simp add: iT_Min)
apply (simp add: iMOD_inext_if iT_iff)
done
lemma iMODb_inext_nth: "a ≤ c ⟹ [r, mod m, c] → a = r + m * a"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 inext_nth_singleton)
apply (induct a)
apply (simp add: iMODb_Min)
apply (simp add: iMODb_inext_if iT_iff)
done
lemma iMODb_inext_nth_if: "
[r, mod m, c] → a = (if a ≤ c then r + m * a else r + m * c)"
by (simp add: iMODb_inext_nth inext_nth_card_Max iT_finite iT_not_empty iT_Max iT_card)
lemma iMODb_iprev_nth: "
a ≤ c ⟹ [r, mod m, c] ← a = r + m * (c - a)"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 iprev_nth_singleton)
apply (induct a)
apply (simp add: iMODb_Max)
apply (simp add: iMODb_iprev_if iT_iff)
apply (frule mult_left_mono[of _ _ m], simp)
apply (simp add: diff_mult_distrib2)
done
lemma iMODb_iprev_nth_if: "
[r, mod m, c] ← a = (if a ≤ c then r + m * (c - a) else r)"
by (simp add: iMODb_iprev_nth iprev_nth_card_iMin iT_finite iT_not_empty iT_Min iT_card)
lemma iIN_iFROM_inext_nth: "
a ≤ d ⟹ [n…,d] → a = [n…] → a"
by (simp add: iIN_inext_nth iFROM_inext_nth)
lemma iIN_iFROM_inext: "
a < n + d ⟹ inext a [n…,d] = inext a [n…]"
by (simp add: iT_inext_if iT_iff)
lemma iMOD_iMODb_inext_nth: "
a ≤ c ⟹ [r, mod m, c] → a = [r, mod m] → a"
by (simp add: iMOD_inext_nth iMODb_inext_nth)
lemma iMOD_iMODb_inext: "
a < r + m * c ⟹ inext a [r, mod m, c] = inext a [r, mod m]"
by (simp add: iT_inext_if iT_iff)
lemma iMOD_inext_nth_Suc_diff: "
([r, mod m] → (Suc n)) - ([r, mod m] → n) = m"
by (simp add: iMOD_inext_nth del: inext_nth.simps)
lemma iMOD_inext_nth_diff: "
([r, mod m] → a) - ([r, mod m] → b) = (a - b) * m"
by (simp add: iMOD_inext_nth diff_mult_distrib mult.commute[of m])
lemma iMODb_inext_nth_diff: "⟦ a ≤ c; b ≤ c ⟧ ⟹
([r, mod m, c] → a) - ([r, mod m, c] → b) = (a - b) * m"
by (simp add: iMODb_inext_nth diff_mult_distrib mult.commute[of m])
subsection ‹Induction with intervals›
lemma iFROM_induct: "
⟦ P n; ⋀k. ⟦ k ∈ [n…]; P k ⟧ ⟹ P (Suc k); a ∈ [n…] ⟧ ⟹ P a"
apply (rule inext_induct[of _ "[n…]"])
apply (simp add: iT_Min iT_inext_if)+
done
lemma iIN_induct: "
⟦ P n; ⋀k. ⟦ k ∈ [n…,d]; k ≠ n + d; P k ⟧ ⟹ P (Suc k); a ∈ [n…,d] ⟧ ⟹ P a"
apply (rule inext_induct[of _ "[n…,d]"])
apply (simp add: iT_Min iT_inext_if)+
done
lemma iTILL_induct: "
⟦ P 0; ⋀k. ⟦ k ∈ […n]; k ≠ n; P k ⟧ ⟹ P (Suc k); a ∈ […n] ⟧ ⟹ P a"
apply (rule inext_induct[of _ "[…n]"])
apply (simp add: iT_Min iT_inext_if)+
done
lemma iMOD_induct: "
⟦ P r; ⋀k. ⟦ k ∈ [r, mod m]; P k ⟧ ⟹ P (k + m); a ∈ [r, mod m] ⟧ ⟹ P a"
apply (rule inext_induct[of _ "[r, mod m]"])
apply (simp add: iT_Min iT_inext_if)+
done
lemma iMODb_induct: "
⟦ P r; ⋀k. ⟦ k ∈ [r, mod m, c]; k ≠ r + m * c; P k ⟧ ⟹ P (k + m); a ∈ [r, mod m, c] ⟧ ⟹ P a"
apply (rule inext_induct[of _ "[r, mod m, c]"])
apply (simp add: iT_Min iT_inext_if)+
done
lemma iIN_rev_induct: "
⟦ P (n + d); ⋀k. ⟦ k ∈ [n…,d]; k ≠ n; P k ⟧ ⟹ P (k - Suc 0); a ∈ [n…,d] ⟧ ⟹ P a"
apply (rule iprev_induct[of _ "[n…,d]"])
apply (simp add: iT_Max iT_finite iT_iprev_if)+
done
lemma iTILL_rev_induct: "
⟦ P n; ⋀k. ⟦ k ∈ […n]; 0 < k; P k ⟧ ⟹ P (k - Suc 0); a ∈ […n] ⟧ ⟹ P a"
apply (rule iprev_induct[of _ "[…n]"])
apply (fastforce simp: iT_Max iT_finite iT_iprev_if)+
done
lemma iMODb_rev_induct: "
⟦ P (r + m * c); ⋀k. ⟦ k ∈ [r, mod m, c]; k ≠ r; P k ⟧ ⟹ P (k - m); a ∈ [r, mod m, c] ⟧ ⟹ P a"
apply (rule iprev_induct[of _ "[r, mod m, c]"])
apply (simp add: iT_Max iT_finite iT_iprev_if)+
done
end