Up to index of Isabelle/HOL/List-Infinite/Nat-Interval-Logic
theory IL_Interval(* Title: IL_Interval.thy
Date: Oct 2006
Author: David Trachtenherz
*)
header {* Intervals and operations for temporal logic declarations *}
theory IL_Interval
imports
Main Nat_Infinity
SetInterval2 InfiniteSet2 SetIntervalStep
Util_Nat Util_MinMax Util_Div
begin
subsection {* Time intervals -- definitions and basic lemmata *}
subsubsection {* Definitions *}
types Time = nat
(* Time interval *)
types iT = "Time set"
typ iT
text {* Infinite interval starting at some natural @{term "n"}. *}
definition
iFROM :: "Time => iT" ("[_…]") (* [n, ∞) *)
where
"[n…] ≡ {n..}"
text {* Finite interval starting at @{term "0"} and ending at some natural @{term "n"}. *}
definition
iTILL :: "Time => iT" ("[…_]") (* [0, n] *) (* Equivalent to [0…,n] *)
where
"[…n] ≡ {..n}"
text {*
Finite bounded interval containing the naturals between
@{term "n"} and @{term "n + d"}.
@{term "d"} denotes the difference between left and right interval bound.
The number of elements is @{term "d + 1"} so that an empty interval cannot be defined. *}
definition
iIN :: "Time => nat => iT" ( "[_…,_]") (* [n, n+d] *)
where
"[n…,d] ≡ {n..n+d}"
text {*
Infinite modulo interval containing all naturals
having the same division remainder modulo @{term "m"}
as @{term "r"}, and beginning at @{term "n"}. *}
definition
iMOD :: "Time => nat => iT" ( "[ _, mod _ ]" )
where
"[r, mod m] ≡ { x. x mod m = r mod m ∧ r ≤ x}"
text {*
Finite bounded modulo interval containing all naturals
having the same division remainder modulo @{term "m"}
as @{term "r"}, beginning at @{term "n"},
and ending after @{term "c"} cycles at @{term "r + m * c"}.
The number of elements is @{term "c + 1"} so that an empty interval cannot be defined. *}
definition
iMODb :: "Time => nat => nat => iT" ( "[ _, mod _, _ ]" )
where
"[r, mod m, c] ≡ { x. x mod m = r mod m ∧ r ≤ x ∧ x ≤ r + m * c}"
subsubsection {* Membership in an interval *}
lemmas iT_defs = iFROM_def iTILL_def iIN_def iMOD_def iMODb_def
lemma iFROM_iff: "x ∈ [n…] = (n ≤ x)"
by (simp add: iFROM_def)
lemma iTILL_iff: "x ∈ […n] = (x ≤ n)"
by (simp add: iTILL_def)
lemma iIN_iff:"x ∈ [n…,d] = (n ≤ x ∧ x ≤ n + d)"
by (simp add: iIN_def)
lemma iMOD_iff: "x ∈ [r, mod m] = (x mod m = r mod m ∧ r ≤ x)"
by (simp add: iMOD_def)
lemma iMODb_iff: "x ∈ [r, mod m, c] =
(x mod m = r mod m ∧ r ≤ x ∧ x ≤ r + m * c)"
by (simp add: iMODb_def)
lemma iFROM_D: "x ∈ [n…] ==> (n ≤ x)"
by (rule iFROM_iff[THEN iffD1])
lemma iTILL_D: "x ∈ […n] ==> (x ≤ n)"
by (rule iTILL_iff[THEN iffD1])
corollary iIN_geD: "x ∈ [n…,d] ==> n ≤ x"
by (simp add: iIN_iff)
corollary iIN_leD: "x ∈ [n…,d] ==> x ≤ n + d"
by (simp add: iIN_iff)
corollary iMOD_modD: "x ∈ [r, mod m] ==> x mod m = r mod m"
by (simp add: iMOD_iff)
corollary iMOD_geD: "x ∈ [r, mod m] ==> r ≤ x"
by (simp add: iMOD_iff)
corollary iMODb_modD: "x ∈ [r, mod m, c] ==> x mod m = r mod m"
by (simp add: iMODb_iff)
corollary iMODb_geD: "x ∈ [r, mod m, c] ==> r ≤ x"
by (simp add: iMODb_iff)
corollary iMODb_leD: "x ∈ [r, mod m, c] ==> x ≤ r + m * c"
by (simp add: iMODb_iff)
lemmas iT_iff = iFROM_iff iTILL_iff iIN_iff iMOD_iff iMODb_iff
lemmas iT_drule =
iFROM_D
iTILL_D
iIN_geD iIN_leD
iMOD_modD iMOD_geD
iMODb_modD iMODb_geD iMODb_leD
thm iT_drule
lemma
iFROM_I [intro]: "n ≤ x ==> x ∈ [n…]" and
iTILL_I [intro]: "x ≤ n ==> x ∈ […n]" and
iIN_I [intro]: "n ≤ x ==> x ≤ n + d ==> x ∈ [n…,d]" and
iMOD_I [intro]: "x mod m = r mod m ==> r ≤ x ==> x ∈ [r, mod m]" and
iMODb_I [intro]: "x mod m = r mod m ==> r ≤ x ==> x ≤ r + m * c ==> x ∈ [r, mod m, c]"
by (simp add: iT_iff)+
lemma
iFROM_E [elim]: "x ∈ [n…] ==> (n ≤ x ==> P) ==> P" and
iTILL_E [elim]: "x ∈ […n] ==> (x ≤ n ==> P) ==> P" and
iIN_E [elim]: "x ∈ [n…,d] ==> (n ≤ x ==> x ≤ n + d ==> P) ==> P" and
iMOD_E [elim]: "x ∈ [r, mod m] ==> (x mod m = r mod m ==> r ≤ x ==> P) ==> P" and
iMODb_E [elim]: "x ∈ [r, mod m, c] ==> (x mod m = r mod m ==> r ≤ x ==> x ≤ r + m * c ==> P) ==> P"
by (simp add: iT_iff)+
(*
lemma "0 < n ==> ∃x ∈ [n…,2*n]. x mod 2 = 0"
apply (simp add: iT_defs)
apply (rule_tac x="2*n" in bexI)
apply simp
apply simp
done
lemma "0 < n ==> ∃x ∈ [n…,2*n]. x mod 2 = 0"
apply (simp add: iT_defs atLeastAtMost_def atLeast_def atMost_def Collect_conj_eq[symmetric])
apply (rule_tac x="2*n" in exI)
apply simp
done
*)
lemma iIN_Suc_insert_conv: "
insert (Suc (n + d)) [n…,d] = [n…,Suc d]"
by (fastsimp simp: iIN_iff)
lemma iTILL_Suc_insert_conv: "insert (Suc n) […n] = […Suc n]"
by (fastsimp 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 fastsimp
apply (elim conjE)
apply (drule_tac x=x in order_le_less[THEN iffD1, rule_format])
apply (erule disjE)
thm less_mod_eq_imp_add_divisor_le
apply (frule less_mod_eq_imp_add_divisor_le[where m=m], simp)
thm add_le_imp_le_right
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 (fastsimp simp: iFROM_iff)
lemma iIN_pred_insert_conv: "
0 < n ==> insert (n - Suc 0) [n…,d] = [n - Suc 0…,Suc d]"
by (fastsimp 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)
thm less_mod_eq_imp_add_divisor_le[of "r-m" x m]
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 (fastsimp 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 mult_div_cancel)
apply (rule iffI)
apply clarify
thm le_imp_sub_mod_le
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 fastsimp
done
lemma iMOD_iIN_iMODb_conv: "
[r, mod m] ∩ [r…,d] = [r, mod m, d div m]"
apply (case_tac "r = 0")
thm iMOD_iTILL_iMODb_conv
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)
thm subst[of "{}" _ "λt. ∀x.(x - t) = x"]
thm subst[of "{}" _ "λt. ∀x.(x - t) = x", THEN spec]
apply (rule subst[of "{}" _ "λt. ∀x.(x - t) = x", THEN spec])
prefer 2
apply simp
apply (rule sym)
thm disjoint_iff_not_equal
apply (fastsimp simp: disjoint_iff_not_equal iMOD_iff iTILL_iff)
done
thm UNIV_def
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 (fastsimp simp: iIN_0 iMOD_def)
lemma iMODb_mod_0: "[r, mod 0, c] = [r…,0]"
by (fastsimp simp: iMODb_def iIN_0)
lemma iMODb_0: "[r, mod m, 0] = [r…,0]"
by (fastsimp simp: iMODb_def iIN_0 set_eq_iff)
lemmas iT_0 =
iFROM_0
iTILL_0
iIN_0
iMOD_0
iMODb_mod_0
iMODb_0
thm iT_0
lemma iMOD_1: "[r, mod Suc 0] = [r…]"
by (fastsimp simp: iFROM_iff)
lemma iMODb_mod_1: "[r, mod Suc 0, c] = [r…,c]"
by (fastsimp 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 (fastsimp simp: iT_iff)+
lemmas iT_not_empty =
iFROM_not_empty
iTILL_not_empty
iIN_not_empty
iMOD_not_empty
iMODb_not_empty
thm iT_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]"
thm infinite_nat_iff_asc_chain
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
thm iT_finite
lemmas iT_infinite =
iFROM_infinite
iMOD_infinite
thm iT_infinite
thm
iMax_finite_conv
iMax_infinite_conv
subsubsection {* @{text Min} and @{text 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"
thm iMin_equality
by (rule iMin_equality, (simp add: iT_iff)+)+
lemmas iT_Min =
iIN_Min
iTILL_Min
iFROM_Min
iMOD_Min
iMODb_Min
thm iT_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
thm iT_Max
lemma
iTILL_iMax: "iMax […n] = Fin n" and
iIN_iMax: "iMax [n…,d] = Fin (n+d)" and
iMODb_iMax: "iMax [r, mod m, c] = Fin (r + m * c)" and
iMOD_0_iMax: "iMax [r, mod 0] = Fin 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
thm iT_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 (fastsimp 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 (fastsimp simp: iIN_iff)
lemma iIN_pred: "[| x ∈ [n…,d]; n < x |] ==> x - Suc 0 ∈ [n…,d]"
by (fastsimp 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]"
thm mod_diff_mult_self1
by (fastsimp 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])
thm mod_0_div_mult_cancel[THEN iffD1, OF mod_eq_imp_diff_mod_0]
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)
thm iMOD_minus_divisor_mult[of x r m 1]
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)+
thm mod_add_eq_imp_mod_0[THEN iffD1]
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
apply simp
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 split_if_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 (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
thm iMOD_Suc[of "x - Suc 0", THEN iffD1]
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 (fastsimp 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]"
thm less_mod_eq_imp_add_divisor_le
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]"
thm mod_diff_mult_self1
by (fastsimp 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
thm mod_add_eq_imp_mod_0[THEN iffD1]
apply (rule mod_add_eq_imp_mod_0[of x, THEN iffD1])
apply (simp add: iT_iff)
apply fastsimp
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)
thm iMOD_pred[THEN iffD1, of x r m]
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 (fastsimp simp add: iMODb_iff)
done
lemmas iFROM_plus_minus =
iFROM_plus
iFROM_Suc
iFROM_minus
iFROM_pred
thm iFROM_plus_minus
lemmas iTILL_plus_minus =
iTILL_plus
iTILL_Suc
iTILL_minus
iTILL_pred
thm iTILL_plus_minus
lemmas iIN_plus_minus =
iIN_plus
iIN_Suc
iTILL_minus
iIN_pred
thm iIN_plus_minus
lemmas iMOD_plus_minus_divisor =
iMOD_plus_divisor_mult
iMOD_plus_divisor
iMOD_minus_divisor_mult
iMOD_minus_divisor_mult2
iMOD_minus_divisor
thm iMOD_plus_minus_divisor
lemmas iMOD_plus_minus =
iMOD_plus
iMOD_Suc
iMOD_minus
iMOD_pred
thm iMOD_plus_minus
lemmas iMODb_plus_minus_divisor =
iMODb_plus_divisor_mult
iMODb_plus_divisor_mult2
iMODb_plus_divisor
iMODb_minus_divisor_mult
thm iMODb_plus_minus_divisor
lemmas iMODb_plus_minus =
iMODb_plus
iMODb_Suc
iMODb_minus
iMODb_pred
thm iMODb_plus_minus
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
thm iT_plus_minus
(*
lemma "a ∈ [3…,2] ==> 3 ≤ a ∧ a ≤ 5"
by (simp add: iT_iff)
lemma "15 ∈ [5, mod 10]"
by (simp add: iT_iff)
lemma "n ∈ [15, mod 10] ==> n ∈ [5, mod 10]"
by (simp add: iT_iff)
lemma "[15, mod 10] ⊆ [5, mod 10]"
by (fastsimp simp: iMOD_def)
lemma "n ≤ i ==> n ∈ […i]"
by (simp add: iT_iff)
lemma "∀n ∈ […i]. n ≤ i"
by (simp add: iT_iff)
lemma "∃n ∈ [2, mod 10].n ∉ [12, mod 10]"
apply (simp add: iT_defs)
apply (rule_tac x=2 in exI)
apply simp
done
*)
subsection {* Relations between intervals *}
subsubsection {* Auxiliary lemmata *}
lemma Suc_in_imp_not_subset_iMOD: "
[| n ∈ S; Suc n ∈ S; m ≠ Suc 0 |] ==> ¬ S ⊆ [r, mod m]"
thm iMOD_Suc[THEN iffD1]
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)
thm iMODb_Suc[THEN iffD1]
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
thm iT_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 (fastsimp 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'])
thm mod_add_eq_imp_mod_0[of r' m' 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)
thm mod_add_eq_imp_mod_0[of r' m' m]
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]"
thm subsetD
apply (frule subsetD[of _ _ r'])
apply (simp add: iMODb_iff)
thm subsetI
apply (rule subsetI)
apply (simp add: iMOD_iff iMODb_iff, clarify)
thm mod_eq_mod_0_imp_mod_eq
apply (drule mod_eq_mod_0_imp_mod_eq[where m=m and m'=m'])
thm iMODb_subset_imp_divisor_mod_0
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)
thm iMin_subset[OF iFROM_not_empty]
apply (drule iMin_subset[OF iFROM_not_empty])
apply (simp add: iT_Min)
apply (rule ccontr)
thm Suc_in_imp_not_subset_iMOD
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 (fastsimp simp: subset_iff iFROM_iff iIN_iff)
lemma iIN_iTILL_subset_conv: "([n'…,d'] ⊆ […n]) = (n' + d' ≤ n)"
by (fastsimp 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)
thm Suc_in_imp_not_subset_iMOD
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)
thm subset_trans[OF _ iMODb_iMOD_subset_same]
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 (fastsimp simp: subset_iff iT_iff)
lemma iMODb_iFROM_subset_conv: "([r', mod m', c'] ⊆ [n…]) = (n ≤ r')"
by (fastsimp simp: subset_iff iT_iff)
lemma iMODb_iIN_subset_conv: "
([r', mod m', c'] ⊆ [n…,d]) = (n ≤ r' ∧ r' + m' * c' ≤ n + d)"
by (fastsimp simp: subset_iff iT_iff)
lemma iMODb_iTILL_subset_conv: "
([r', mod m', c'] ⊆ […n]) = (r' + m' * c' ≤ n)"
by (fastsimp 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 (fastsimp 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)
thm mod_eq_mod_0_imp_mod_eq
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)
thm iMODb_subset_imp_iMOD_subset
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)
thm iMOD_subset_imp_iMODb_subset
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)
thm add_less_le_mono[of 0 "m' * c'" r r']
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)
thm subsetD[OF _ iMinI_ex2[OF iMODb_not_empty]]
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)
thm iMOD_iTILL_iMODb_conv iMODb_subset_imp_divisor_mod_0
apply (simp add: iMOD_iTILL_iMODb_conv iMODb_subset_imp_divisor_mod_0)
thm subset_trans[OF iMODb_iMOD_subset_same]
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
thm iT_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]"
thm infinite_not_subset_finite
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'")
thm iIN_iTILL_subset[OF order_refl]
thm Int_greatest[OF _ iIN_iTILL_subset[OF order_refl]]
apply (drule Int_greatest[OF _ iIN_iTILL_subset[OF order_refl]])
thm iMOD_iTILL_iMODb_conv not_iIN_iMODb_subset
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)
thm not_iIN_iMOD_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])
thm iMOD_subset_conv
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…]"
thm iMODb_iFROM_subset_conv[THEN iffD2]
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])
thm iMODb_iIN_subset_conv
lemma iMODb_iIN_subset: "
[| n ≤ r'; r' + m' * c' ≤ n + d |] ==> [r', mod m', c'] ⊆ [n…,d]"
by (simp add: iMODb_iIN_subset_conv)
thm iMODb_iMOD_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)
thm iMODb_iMOD_subset_conv
apply (simp add: iMODb_iMOD_subset_conv)
done
thm iMODb_subset_conv
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]])
thm iIN_subset
lemma iIN_trans: "
[| y ∈ [x…,d]; z ∈ [y…,d']; d' ≤ x + d - y |] ==> z ∈ [x…,d]"
by fastsimp
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 fastsimp
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 mult_div_cancel)
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')"
thm iIN_eq_conv[of 0 n 0 n']
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_eq_conv)
thm iMOD_singleton_eq_conv
lemma iMOD_0_eq_conv: "([r, mod 0] = [r', mod m']) = (r = r' ∧ m' = 0)"
apply (simp add: iMOD_0 iIN_0)
thm iMOD_singleton_eq_conv
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 (fastsimp simp add: set_eq_subset iMOD_subset_conv)
apply simp
done
thm iMODb_singleton_eq_conv
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 (fastsimp 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 (fastsimp 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 (fastsimp 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 (fastsimp simp: iMOD_1[symmetric] iMOD_eq_conv)
thm iMODb_singleton_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 (fastsimp 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")
thm iMODb_singleton_eq_conv
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 (fastsimp 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
thm iT_neq
subsection {* Union and intersection of intervals *}
lemma iFROM_union': "[n…] ∪ [n'…] = [min n n'…]"
by (fastsimp 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 (fastsimp 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 (fastsimp 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 (fastsimp simp: iT_iff)
lemma iTILL_inter': "[…n] ∩ […n'] = […min n n']"
by (fastsimp 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 (fastsimp simp add: iIN_iff)
(* The case of the second interval starting directly after the first one *)
lemma iIN_append_union: "
[n…,d] ∪ [n + d…,d'] = [n…,d + d']"
by (simp add: iIN_union)
lemma iIN_append_union_Suc: "
[n…,d] ∪ [Suc (n + d)…,d'] = [n…,Suc (d + d')]"
by (simp add: iIN_union)
lemma iIN_append_union_pred: "
0 < d ==> [n…,d - Suc 0] ∪ [n + d…,d'] = [n…,d + d']"
by (simp add: iIN_union)
lemma iIN_iFROM_union: "
n' ≤ Suc (n + d) ==> [n…,d] ∪ [n'…] = [min n n'…]"
by (fastsimp 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 (fastsimp simp: iIN_iff)
lemma iMOD_union: "
[| r ≤ r'; r mod m = r' mod m |] ==>
[r, mod m] ∪ [r', mod m] = [r, mod m]"
by (fastsimp 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 (fastsimp 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 (fastsimp 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 (fastsimp 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 (fastsimp simp: add_mult_distrib2 diff_mult_distrib2 mult_div_cancel)
done
thm iMODb_iMOD_subset_same
thm Un_absorb1[OF iMODb_iMOD_subset_same]
lemma iMODb_append_union: "
[r, mod m, c] ∪ [ r + m * c, mod m, c'] = [r, mod m, c + c']"
thm iMODb_union[of r "r + m * c" 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 fastsimp
apply (clarsimp simp: linorder_not_le)
apply (case_tac "r ≤ r'")
apply (simp add: min_eqL)
thm add_le_imp_le_right[of _ m]
apply (rule add_le_imp_le_right[of _ m])
thm less_mod_eq_imp_add_divisor_le
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]"
thm iMODb_iMOD_append_union'
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')]"
thm insert_absorb[of "r + m * c" "[r, mod m, c] ∪ [ r + m * Suc c, mod m, 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)
thm iMODb_append_union[of r m c]
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"])
thm mod_0_div_mult_cancel[THEN iffD1, OF mod_eq_imp_diff_mod_0]
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 fastsimp
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
thm iT_union'
thm iT_union
thm iT_union_append
thm iT_inter'
thm iT_inter
thm partition_Union
lemma mod_partition_Union: "
0 < m ==> (\<Union>k. A ∩ [k * m…,m - Suc 0]) = A"
apply simp
thm subst[where s=UNIV and P="λx. A ∩ x = A"]
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)
thm div_mult_cancel
apply (simp add: div_mult_cancel)
thm le_add_diff
apply (subst add_commute)
apply (rule le_add_diff)
thm Suc_mod_le_divisor
apply (simp add: Suc_mod_le_divisor)
apply simp
done
thm mod_partition_Union
lemma finite_mod_partition_Union: "
[| 0 < m; finite A |] ==>
(\<Union>k≤Max A div m. A ∩ [k*m…,m - Suc 0]) = A"
thm subst[OF mod_partition_Union[of m], where
P="λx. (\<Union>k≤Max A div m. A ∩ [k*m…,m - Suc 0]) = x"]
apply (rule subst[OF mod_partition_Union[of m], where
P="λx. (\<Union>k≤Max A div m. A ∩ [k*m…,m - Suc 0]) = x"])
apply assumption
apply (rule set_eqI)
apply (simp add: Bex_def iIN_iff)
apply (rule iffI, blast)
apply clarsimp
apply (rename_tac x x1)
apply (rule_tac x="x div m" in exI)
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
thm setsum_UN_disjoint
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", blast)
thm le_less_imp_div
apply (rule le_less_imp_div, assumption)
apply simp
done
subsection {* Cutting intervals *}
thm i_cut_defs
thm i_cut_subset
thm i_cut_bound
thm
cut_le_less_conv
cut_less_le_conv
thm
cut_ge_greater_conv
cut_greater_ge_conv
(*
lemma "[10…,5] \<down>< 12 = [10…,1]"
apply (simp add: iT_iff cut_less_def)
apply (simp add: iT_defs set_interval_defs Collect_conj_eq[symmetric])
apply fastsimp
done
*)
thm
cut_le_Min_empty
cut_less_Min_empty
cut_le_Min_not_empty
cut_less_Min_not_empty
thm
i_cut_min_empty
thm
i_cut_min_all
thm
i_cut_max_empty
thm
i_cut_max_all
lemma iTILL_cut_le: "[…n] \<down>≤ 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] \<down>≤ t = […t]"
by (simp add: iTILL_cut_le iT_iff)
corollary iTILL_cut_le2: "t ∉ […n] ==> […n] \<down>≤ t = […n]"
by (simp add: iTILL_cut_le iT_iff)
lemma iFROM_cut_le: "
[n…] \<down>≤ 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…] \<down>≤ t = [n…,t - n]"
by (simp add: iFROM_cut_le iT_iff)
lemma iIN_cut_le: "
[n…,d] \<down>≤ 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] \<down>≤ t = [n…,t - n]"
by (simp add: iIN_cut_le iT_iff)
lemma iMOD_cut_le: "
[r, mod m] \<down>≤ 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: mult_div_cancel)
apply (drule_tac x=r and y=x in le_imp_less_or_eq, erule disjE)
prefer 2
apply simp
thm less_mod_eq_imp_add_divisor_le
apply (drule_tac x=r and y=x and m=m in less_mod_eq_imp_add_divisor_le, simp)
apply (rule iffI)
thm mod_eq_imp_diff_mod_eq[of _ m r t, rule_format]
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
thm add_le_mono2[OF mod_le_divisor]
thm order_trans[OF add_le_mono2[OF mod_le_divisor]]
apply (simp add: order_trans[OF add_le_mono2[OF mod_le_divisor]])
apply simp
thm le_imp_sub_mod_le[of _ t]
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] \<down>≤ t = [r, mod m, (t - r) div m]"
by (simp add: iMOD_cut_le iT_iff)
lemma iMODb_cut_le: "
[r, mod m, c] \<down>≤ 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)
thm iMOD_iTILL_iMODb_conv[of r "r + m * c" m]
apply (rule_tac t=c and s="(r + m * c - r) div m" in subst, simp)
apply (subst iMOD_iTILL_iMODb_conv[symmetric], simp)
find_theorems "cut_le (_ ∩ _)"
apply (simp add: cut_le_Int_right iTILL_cut_le)
thm iMOD_iTILL_iMODb_conv
apply (simp add: iMOD_iTILL_iMODb_conv)
done
lemma iMODb_cut_le1: "
t ∈ [r, mod m, c] ==>
[r, mod m, c] \<down>≤ t = [r, mod m, (t - r) div m]"
by (clarsimp simp: iMODb_cut_le iT_iff iMODb_mod_0)
lemma iTILL_cut_less: "
[…n] \<down>< 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 (fastsimp simp: nat_cut_less_le_conv iTILL_cut_le)
done
lemma iTILL_cut_less1: "
[| t ∈ […n]; 0 < t |] ==> […n] \<down>< t = […t - Suc 0]"
thm iTILL_cut_less
by (simp add: iTILL_cut_less iT_iff)
lemma iFROM_cut_less: "
[n…] \<down>< 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 (fastsimp simp: nat_cut_less_le_conv iFROM_cut_le)
done
lemma iFROM_cut_less1: "
n < t ==> [n…] \<down>< t = [n…,t - Suc n]"
by (simp add: iFROM_cut_less)
lemma iIN_cut_less: "
[n…,d] \<down>< 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 (fastsimp simp: nat_cut_less_le_conv iIN_cut_le)
done
lemma iIN_cut_less1: "
[| t ∈ [n…,d]; n < t |] ==> [n…,d] \<down>< t = [n…, t - Suc n]"
thm iIN_cut_less
by (simp add: iIN_cut_less iT_iff)
thm
cut_le_less_conv
cut_less_le_conv
lemma iMOD_cut_less: "
[r, mod m] \<down>< t = (
if t ≤ r then {}
else [r, mod m, (t - Suc r) div m])"
thm iMOD_cut_le
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty)
apply (simp add: nat_cut_less_le_conv iMOD_cut_le)
apply fastsimp
done
lemma iMOD_cut_less1: "
[| t ∈ [r, mod m]; r < t |] ==>
[r, mod m] \<down>< 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)
thm mod_0_imp_diff_Suc_div_conv mod_eq_imp_diff_mod_0
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] \<down>< 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])"
thm iMODb_cut_le
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty)
apply (simp add: nat_cut_less_le_conv iMODb_cut_le)
apply fastsimp
done
lemma iMODb_cut_less1: "[| t ∈ [r, mod m, c]; r < t |] ==>
[r, mod m, c] \<down>< 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)
thm mod_0_imp_diff_Suc_div_conv mod_eq_imp_diff_mod_0
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
thm iT_cut_le
lemmas iT_cut_le1 =
iTILL_cut_le1
iFROM_cut_le1
iIN_cut_le1
iMOD_cut_le1
iMODb_cut_le1
thm iT_cut_le1
lemmas iT_cut_less =
iTILL_cut_less
iFROM_cut_less
iIN_cut_less
iMOD_cut_less
iMODb_cut_less
thm iT_cut_less
lemmas iT_cut_less1 =
iTILL_cut_less1
iFROM_cut_less1
iIN_cut_less1
iMOD_cut_less1
iMODb_cut_less1
thm iT_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
thm iT_cut_le_less
thm iT_cut_le_less1
lemma iTILL_cut_ge: "
[…n] \<down>≥ 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] \<down>≥ t = [t…,n-t]"
by (simp add: iTILL_cut_ge iT_iff)
corollary iTILL_cut_ge2: "t ∉ […n] ==> […n] \<down>≥ t = {}"
by (simp add: iTILL_cut_ge iT_iff)
lemma iTILL_cut_greater: "
[…n] \<down>> 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] \<down>> t = [Suc t…,n - Suc t]"
by (simp add: iTILL_cut_greater iT_iff)
corollary iTILL_cut_greater2: "t ∉ […n] ==> […n] \<down>> t = {}"
by (simp add: iTILL_cut_greater iT_iff)
lemma iFROM_cut_ge: "
[n…] \<down>≥ t = (if n ≤ t then [t…] else [n…])"
by (force simp: i_cut_mem_iff iT_iff)
corollary iFROM_cut_ge1: "t ∈ [n…] ==> [n…] \<down>≥ t = [t…]"
by (simp add: iFROM_cut_ge iT_iff)
lemma iFROM_cut_greater: "
[n…] \<down>> 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…] \<down>> t = [Suc t…]"
by (simp add: iFROM_cut_greater iT_iff)
lemma iIN_cut_ge: "
[n…,d] \<down>≥ 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] \<down>≥ t = [t…,n+d-t]"
by (simp add: iIN_cut_ge iT_iff)
corollary iIN_cut_ge2: "t ∉ [n…,d] ==>
[n…,d] \<down>≥ t = (if t < n then [n…,d] else {})"
by (simp add: iIN_cut_ge iT_iff)
lemma iIN_cut_greater: "
[n…,d] \<down>> 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] \<down>> t = [Suc t…,n + d - Suc t]"
by (simp add: iIN_cut_greater iT_iff)
(*
lemma "let m=5 in let r = 12 in let t = 16 in
[r, mod m] \<down>> t = (
if t < r then [r, mod m] else
if (m = 0 ∧ r ≤ t) then {}
else [r + (t - r) div m * m + m, mod m])"
apply (simp add: Let_def)
oops
lemma "let m=5 in let r = 12 in let t = 16 in
[r, mod m] \<down>> t = (
if t < r then [r, mod m] else
if (m = 0 ∧ r ≤ t) then {}
else [t + m - (t - r) mod m, mod m])"
apply (simp add: Let_def)
oops
*)
thm sub_diff_mod_eq'[of r t 1 m, simplified]
lemma mod_cut_greater_aux_t_less: "
[| 0 < (m::nat); r ≤ t |] ==>
t < t + m - (t - r) mod m"
thm less_add_diff
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"
thm diff_mod_le
apply (insert diff_mod_le[of t r m])
thm diff_add_assoc2[of "(t - r) mod m" t m]
apply (subst diff_add_assoc2, simp)
thm less_mod_eq_imp_add_divisor_le[of "t - (t - r) mod m" x m]
apply (rule less_mod_eq_imp_add_divisor_le, simp)
thm sub_diff_mod_eq
apply (simp add: sub_diff_mod_eq)
done
lemma iMOD_cut_greater: "
[r, mod m] \<down>> 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
thm order_trans[OF mod_le_dividend]
apply (rule order_trans[OF mod_le_dividend], simp)
thm diff_add_assoc2[of "(t - r) mod m" t m]
apply (simp add: diff_add_assoc2 del: add_diff_assoc2)
thm sub_diff_mod_eq
apply (simp add: sub_diff_mod_eq del: add_diff_assoc2)
apply (rule conj_cong, simp)
apply (rule iffI)
apply clarify
thm less_mod_eq_imp_add_divisor_le[of "t - (t - r) mod m" x m]
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] \<down>> 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)"
thm diff_diff_right[of r "t+m-(t-r)mod m" "m*c", symmetric]
apply (subgoal_tac "r ≤ t + m - (t - r) mod m")
prefer 2
apply (rule order_trans[of _ t], simp)
thm mod_cut_greater_aux_t_less
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 mult_div_cancel del: diff_diff_left)
apply simp
done
lemma iMODb_cut_greater: "
[r, mod m, c] \<down>> 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)
thm iMOD_iTILL_iMODb_conv[of r "r + m * c" m]
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)
thm iMOD_cut_greater
apply (simp add: i_cut_Int_left iMOD_cut_greater)
thm iMOD_iTILL_iMODb_conv
apply (subst iMOD_iTILL_iMODb_conv)
thm mod_cut_greater_aux_le_x
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] \<down>> 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 "let m=5 in let r = 12 in let t = 17 in
[r, mod m] \<down>≥ 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 (simp add: Let_def)
oops
*)
lemma iMOD_cut_ge: "
[r, mod m] \<down>≥ 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)
thm iMOD_cut_greater nat_cut_greater_ge_conv[symmetric]
apply (force simp: nat_cut_greater_ge_conv[symmetric] iMOD_cut_greater)
done
lemma iMOD_cut_ge1: "
t ∈ [r, mod m] ==>
[r, mod m] \<down>≥ t = [t, mod m]"
by (fastsimp simp: iMOD_cut_ge)
(*
lemma "let m=5 in let r = 12 in let t = 21 in let c=5 in
[r, mod m, c] \<down>≥ 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 (simp add: Let_def)
oops
*)
lemma iMODb_cut_ge: "
[r, mod m, c] \<down>≥ 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])"
thm iMOD_cut_ge
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")
thm diff_mod_pred
apply (simp add: diff_mod_pred)
thm mod_0_imp_diff_Suc_div_conv
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)
thm div_le_mono
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 mult_div_cancel 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
thm diff_mod_pred
apply (clarsimp simp add: diff_mod_pred mod_eq_diff_mod_0_conv)
thm iMOD_iTILL_iMODb_conv[of r "r + m * c" m]
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)
thm iMOD_cut_ge
apply (simp add: i_cut_Int_left iMOD_cut_ge)
thm iMOD_iTILL_iMODb_conv
apply (subst iMOD_iTILL_iMODb_conv)
apply (drule_tac x=t in le_imp_less_or_eq, erule disjE)
thm mod_cut_greater_aux_le_x
apply (rule mod_cut_greater_aux_le_x, simp+)
apply (rule arg_cong)
apply (drule_tac x=t in le_imp_less_or_eq, erule disjE)
prefer 2
apply simp
thm iMODb_cut_greater_aux[of m t r c]
apply (simp add: iMODb_cut_greater_aux)
apply (rule arg_cong[where f="op - 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)
thm div_diff1_eq
apply (subst div_diff1_eq[of _ "Suc 0"])
apply (case_tac "m = Suc 0", simp)
apply simp
done
thm iMODb_cut_greater1
lemma iMODb_cut_ge1: "
t ∈ [r, mod m, c] ==>
[r, mod m, c] \<down>≥ 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)
thm iMODb_cut_ge
apply (clarsimp simp: iMODb_cut_ge iT_iff)
thm mod_eq_imp_diff_mod_eq_divisor
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)
thm div_add1_eq
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] \<down>> 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] \<down>> 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
thm iT_cut_ge
lemmas iT_cut_ge1 =
iTILL_cut_ge1
iFROM_cut_ge1
iIN_cut_ge1
iMOD_cut_ge1
iMODb_cut_ge1
thm iT_cut_le1
lemmas iT_cut_greater =
iTILL_cut_greater
iFROM_cut_greater
iIN_cut_greater
iMOD_cut_greater
iMODb_cut_greater
thm iT_cut_greater
lemmas iT_cut_greater1 =
iTILL_cut_greater1
iFROM_cut_greater1
iIN_cut_greater1
iMOD_cut_greater1
iMODb_cut_greater1
thm iT_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
thm iT_cut_ge_greater
thm iT_cut_ge_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)
thm iMODb_Suc_insert_conv
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 @{text icard} *}
lemma iFROM_icard: "icard [n…] = ∞"
by (simp add: iFROM_infinite)
lemma iTILL_icard: "icard […n] = Fin (Suc n)"
by (simp add: icard_finite iT_finite iT_card)
lemma iIN_icard: "icard [n…,d] = Fin (Suc d)"
by (simp add: icard_finite iT_finite iT_card)
lemma iMOD_0_icard: "icard [r, mod 0] = iSuc 0"
by (simp add: icard_finite iT_finite iT_card iSuc_Fin)
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 iSuc 0 else ∞)"
by (simp add: icard_finite iT_finite iT_infinite iSuc_Fin iT_card)
lemma iMODb_mod_0_icard: "icard [r, mod 0, c] = iSuc 0"
by (simp add: icard_finite iT_finite iSuc_Fin iT_card)
lemma iMODb_icard: "0 < m ==> icard [r, mod m, c] = Fin (Suc c)"
by (simp add: icard_finite iT_finite iMODb_card)
lemma iMODb_icard_if: "icard [r, mod m, c] = Fin (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 @{text inext} and @{text iprev} with intervals *}
thm
inext_def
iprev_def
(*
lemma "inext 5 […10] = 6"
apply (simp add: inext_def)
apply (simp add: iT_iff)
apply (simp add: iT_cut_greater)
apply (simp add: iT_not_empty)
apply (simp add: iT_Min)
done
lemma "inext 12 […10] = 12"
apply (simp add: inext_def)
apply (simp add: iT_iff)
done
lemma "inext 5 [4…,5] = 6"
apply (simp add: inext_def)
apply (simp add: iT_iff)
apply (simp add: iT_cut_greater)
apply (simp add: iT_not_empty)
apply (simp add: iT_Min)
done
lemma "inext 14 [2, mod 4] = 18"
apply (simp add: inext_def)
apply safe
thm iMOD_cut_greater[of 14 2 4]
apply (simp add: iMOD_cut_greater iT_iff
iT_Min)
apply (simp add: iT_iff)
thm iMOD_cut_greater[of 14 2 4, simplified]
apply (simp add: iMOD_cut_greater iT_iff
iT_not_empty)
done
lemma "iprev 5 […10] = 4"
apply (simp add: iprev_def)
apply (simp add: iT_iff)
apply (simp add: i_cut_defs)
apply safe
apply (simp add: iT_iff)
apply (rule le_antisym)
thm Max_le_iff
thm iffD2[OF Max_le_iff]
apply (rule iffD2[OF Max_le_iff])
apply fastsimp+
done
*)
thm
inext_Max
iprev_iMin
thm
inext_closed
iprev_closed
thm
iMin_subset
iMin_Un
thm
Max_Un
Min_Un
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 mult_div_cancel)
thm mod_eq_imp_diff_mod_eq_divisor
apply (simp del: add_Suc_right add: add_Suc_right[symmetric] mod_eq_imp_diff_mod_eq_divisor)
thm less_mod_eq_imp_add_divisor_le
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 mult_div_cancel)
thm mod_eq_imp_diff_mod_eq_divisor
apply (simp del: add_Suc_right add: add_Suc_right[symmetric] mod_eq_imp_diff_mod_eq_divisor)
thm less_mod_eq_imp_add_divisor_le
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)
thm less_mod_eq_imp_add_divisor_le
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'
thm iT_inext
thm iT_iprev
thm iprev_iMin
thm iT_finite[THEN inext_Max]
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 (fastsimp 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 (fastsimp 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
thm iT_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 (fastsimp 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 (fastsimp 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 (fastsimp 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
thm iT_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)
thm iIN_inext
lemma iIN_inext_diff_const: "
[| n ≤ t; t < n + d |] ==> inext t [n…,d] - t = Suc 0"
by (simp add: iIN_inext)
thm iIN_iprev
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)
thm iMOD_inext
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')
thm 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
thm iMODb_inext
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)
thm iMODb_iprev'
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')
thm 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
thm iT_inext_diff_const
thm iT_iprev_diff_const
subsubsection {* Mirroring of intervals *}
thm mirror_elem_def
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)
thm mod_diff_right_eq
apply (simp add: mod_diff_right_eq)
apply (rule iffI)
apply (clarsimp, rename_tac x')
thm mod_diff_right_eq
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)
thm mod_sub_eq_mod_swap
apply (subst mod_sub_eq_mod_swap, simp+)
thm mod_diff_right_eq
apply (simp add: mod_diff_right_eq[symmetric])
done
thm imirror_bounds_def
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
thm iT_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
thm iT_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] \<leftarrow> 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] \<leftarrow> 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] \<leftarrow> a = n - a"
by (simp add: iTILL_def iprev_nth_atMost)
lemma iTILL_iprev_nth_if: "
[…n] \<leftarrow> 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] \<leftarrow> 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] \<leftarrow> 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 *}
thm
inext_induct
iFROM_inext
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
thm
iprev_induct
iIN_inext
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 (fastsimp 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