Up to index of Isabelle/HOL/List-Infinite/Nat-Interval-Logic
theory IL_IntervalOperators(* Title: IL_IntOperator.thy
Date: Jan 2007
Author: David Trachtenherz
*)
header {* Arithmetic operators on natural intervals *}
theory IL_IntervalOperators
imports IL_Interval
begin
subsection {* Arithmetic operations with intervals *}
subsubsection {* Addition of and multiplication by constants *}
definition iT_Plus :: "iT => Time => iT" (infixl "⊕" 55) where
"I ⊕ k ≡ (λn.(n + k)) ` I"
definition iT_Mult :: "iT => Time => iT" (infixl "⊗" 55) where
iT_Mult_def : "I ⊗ k ≡ (λn.(n * k)) ` I"
(*<*)
(* Some examples *)
(*
lemma "[…10]⊕5 = {5..15}"
apply (simp only: iIN_0_iTILL_conv[symmetric])
apply (simp add: iT_defs)
apply (simp add: iT_Plus_def)
apply (simp add: image_add_atLeastAtMost)
done
lemma "[1…,2] = {1,2,3}"
apply (simp add: iIN_def)
apply fastsimp
done
lemma "[1…,2]⊗2 = {2,4,6}"
apply (simp add: iT_Mult_def iIN_def)
apply auto
done
lemma "[10…]⊗k = {x*k | x. 10 ≤ x}"
apply (simp add: iFROM_def iT_Mult_def)
by blast
lemma "[…4] ⊗ 10 = {0, 10, 20, 30, 40}"
apply (simp add: iT_Mult_def iTILL_def)
by auto
lemma "[…4] ⊗ 10 ⊕ 2 = {2, 12, 22, 32, 42}"
apply (simp add: iT_Plus_def iT_Mult_def iTILL_def)
by auto
*)
(*>*)
lemma iT_Plus_image_conv: "I ⊕ k = (λn.(n + k)) ` I"
by (simp add: iT_Plus_def)
lemma iT_Mult_image_conv: "I ⊗ k = (λn.(n * k)) ` I"
by (simp add: iT_Mult_def)
lemma iT_Plus_empty: "{} ⊕ k = {}"
by (simp add: iT_Plus_def)
lemma iT_Mult_empty: "{} ⊗ k = {}"
by (simp add: iT_Mult_def)
lemma iT_Plus_not_empty: "I ≠ {} ==> I ⊕ k ≠ {}"
by (simp add: iT_Plus_def)
lemma iT_Mult_not_empty: "I ≠ {} ==> I ⊗ k ≠ {}"
by (simp add: iT_Mult_def)
lemma iT_Plus_empty_iff: "(I ⊕ k = {}) = (I = {})"
by (simp add: iT_Plus_def)
lemma iT_Mult_empty_iff: "(I ⊗ k = {}) = (I = {})"
by (simp add: iT_Mult_def)
lemma iT_Plus_mono: "A ⊆ B ==> A ⊕ k ⊆ B ⊕ k"
by (simp add: iT_Plus_def image_mono)
lemma iT_Mult_mono: "A ⊆ B ==> A ⊗ k ⊆ B ⊗ k"
by (simp add: iT_Mult_def image_mono)
lemma iT_Mult_0: "I ≠ {} ==> I ⊗ 0 = […0]"
by (fastsimp simp add: iTILL_def iT_Mult_def)
corollary iT_Mult_0_if: "I ⊗ 0 = (if I = {} then {} else […0])"
by (simp add: iT_Mult_empty iT_Mult_0)
lemma iT_Plus_mem_iff: "x ∈ (I ⊕ k) = (k ≤ x ∧ (x - k) ∈ I)"
apply (simp add: iT_Plus_def image_iff)
apply (rule iffI)
apply fastsimp
apply (rule_tac x="x - k" in bexI, simp+)
done
lemma iT_Plus_mem_iff2: "x + k ∈ (I ⊕ k) = (x ∈ I)"
by (simp add: iT_Plus_def image_iff)
lemma iT_Mult_mem_iff_0: "x ∈ (I ⊗ 0) = (I ≠ {} ∧ x = 0)"
apply (case_tac "I = {}")
apply (simp add: iT_Mult_empty)
apply (simp add: iT_Mult_0 iT_iff)
done
lemma iT_Mult_mem_iff: "
0 < k ==> x ∈ (I ⊗ k) = (x mod k = 0 ∧ x div k ∈ I)"
by (fastsimp simp: iT_Mult_def image_iff)
lemma iT_Mult_mem_iff2: "0 < k ==> x * k ∈ (I ⊗ k) = (x ∈ I)"
by (simp add: iT_Mult_def image_iff)
lemma iT_Plus_singleton: "{a} ⊕ k = {a + k}"
by (simp add: iT_Plus_def)
lemma iT_Mult_singleton: "{a} ⊗ k = {a * k}"
by (simp add: iT_Mult_def)
lemma iT_Plus_Un: "(A ∪ B) ⊕ k = (A ⊕ k) ∪ (B ⊕ k)"
by (simp add: iT_Plus_def image_Un)
lemma iT_Mult_Un: "(A ∪ B) ⊗ k = (A ⊗ k) ∪ (B ⊗ k)"
by (simp add: iT_Mult_def image_Un)
lemma iT_Plus_Int: "(A ∩ B) ⊕ k = (A ⊕ k) ∩ (B ⊕ k)"
by (simp add: iT_Plus_def image_Int)
lemma iT_Mult_Int: "0 < k ==> (A ∩ B) ⊗ k = (A ⊗ k) ∩ (B ⊗ k)"
by (simp add: iT_Mult_def image_Int mult_right_inj)
thm
iT_Plus_Un
iT_Mult_Un
iT_Plus_Int
iT_Mult_Int
thm imageI
lemma iT_Plus_image: "f ` I ⊕ n = (λx. f x + n) ` I"
by (fastsimp simp: iT_Plus_def)
lemma iT_Mult_image: "f ` I ⊗ n = (λx. f x * n) ` I"
by (fastsimp simp: iT_Mult_def)
lemma iT_Plus_commute: "I ⊕ a ⊕ b = I ⊕ b ⊕ a"
by (fastsimp simp: iT_Plus_def)
lemma iT_Mult_commute: "I ⊗ a ⊗ b = I ⊗ b ⊗ a"
by (fastsimp simp: iT_Mult_def)
lemma iT_Plus_assoc:"I ⊕ a ⊕ b = I ⊕ (a + b)"
by (fastsimp simp: iT_Plus_def)
lemma iT_Mult_assoc:"I ⊗ a ⊗ b = I ⊗ (a * b)"
by (fastsimp simp: iT_Mult_def)
lemma iT_Plus_Mult_distrib: "I ⊕ n ⊗ m = I ⊗ m ⊕ n * m"
by (simp add: iT_Plus_def iT_Mult_def image_image add_mult_distrib)
(*<*)
lemma "i ⊗ n1 ⊗ n2 ⊗ n3 ⊗ n4 ⊗ n5 ⊗ n6 ⊗ n7 =
i ⊗ n1 * n2 * n3 * n4 * n5 * n6 * n7"
by (simp add: iT_Mult_assoc)
lemma "i ⊕ n1 ⊕ n2 ⊕ n3 ⊕ n4 ⊕ n5 = i ⊕ n1 + n2 + n3 + n4 + n5"
by (simp add: iT_Plus_assoc)
lemma "i ⊕ n1 ⊗ m ⊕ n2 = i ⊗ m ⊕ n1 * m + n2"
by (simp add: iT_Plus_assoc iT_Plus_Mult_distrib)
lemma "i ⊕ n1 ⊗ m1 ⊗ m2 ⊕ n2 = i ⊗ m1 * m2 ⊕ n1 * m1 * m2 + n2"
by (simp add: iT_Plus_assoc iT_Mult_assoc iT_Plus_Mult_distrib)
lemma "n ∈ I ⊕ k ==> k ≤ n"
by (clarsimp simp add: iT_Plus_def)
(*>*)
lemma iT_Plus_finite_iff: "finite (I ⊕ k) = finite I"
by (simp add: iT_Plus_def inj_on_finite_image_iff)
lemma iT_Mult_0_finite: "finite (I ⊗ 0)"
by (simp add: iT_Mult_0_if iTILL_0)
lemma iT_Mult_finite_iff: "0 < k ==> finite (I ⊗ k) = finite I"
by (simp add: iT_Mult_def inj_on_finite_image_iff[OF inj_imp_inj_on] mult_right_inj)
lemma iT_Plus_Min: "I ≠ {} ==> iMin (I ⊕ k) = iMin I + k"
by (simp add: iT_Plus_def iMin_mono2 mono_def)
lemma iT_Mult_Min: "I ≠ {} ==> iMin (I ⊗ k) = iMin I * k"
by (simp add: iT_Mult_def iMin_mono2 mono_def)
thm Max_mono2
lemma iT_Plus_Max: "[| finite I; I ≠ {} |] ==> Max (I ⊕ k) = Max I + k"
by (simp add: iT_Plus_def Max_mono2 mono_def)
lemma iT_Mult_Max: "[| finite I; I ≠ {} |] ==> Max (I ⊗ k) = Max I * k"
by (simp add: iT_Mult_def Max_mono2 mono_def)
thm iT_Mult_0
corollary
iMOD_mult_0: "[r, mod m] ⊗ 0 = […0]" and
iMODb_mult_0: "[r, mod m, c] ⊗ 0 = […0]" and
iFROM_mult_0: "[n…] ⊗ 0 = […0]" and
iIN_mult_0: "[n…,d] ⊗ 0 = […0]" and
iTILL_mult_0: "[…n] ⊗ 0 = […0]"
by (simp add: iT_not_empty iT_Mult_0)+
lemmas iT_mult_0 =
iTILL_mult_0
iFROM_mult_0
iIN_mult_0
iMOD_mult_0
iMODb_mult_0
thm iT_mult_0
lemma iT_Plus_0: "I ⊕ 0 = I"
by (simp add: iT_Plus_def)
lemma iT_Mult_1: "I ⊗ Suc 0 = I"
by (simp add: iT_Mult_def)
thm iT_Plus_Min
corollary
iFROM_add_Min: "iMin ([n…] ⊕ k) = n + k" and
iIN_add_Min: "iMin ([n…,d] ⊕ k) = n + k" and
iTILL_add_Min: "iMin ([…n] ⊕ k) = k" and
iMOD_add_Min: "iMin ([r, mod m] ⊕ k) = r + k" and
iMODb_add_Min: "iMin ([r, mod m, c] ⊕ k) = r + k"
by (simp add: iT_not_empty iT_Plus_Min iT_Min)+
corollary
iFROM_mult_Min: "iMin ([n…] ⊗ k) = n * k" and
iIN_mult_Min: "iMin ([n…,d] ⊗ k) = n * k" and
iTILL_mult_Min: "iMin ([…n] ⊗ k) = 0" and
iMOD_mult_Min: "iMin ([r, mod m] ⊗ k) = r * k" and
iMODb_mult_Min: "iMin ([r, mod m, c] ⊗ k) = r * k"
by (simp add: iT_not_empty iT_Mult_Min iT_Min)+
lemmas iT_add_Min =
iIN_add_Min
iTILL_add_Min
iFROM_add_Min
iMOD_add_Min
iMODb_add_Min
thm iT_add_Min
lemmas iT_mult_Min =
iIN_mult_Min
iTILL_mult_Min
iFROM_mult_Min
iMOD_mult_Min
iMODb_mult_Min
thm iT_mult_Min
lemma iFROM_add: "[n…] ⊕ k = [n+k…]"
by (simp add: iFROM_def iT_Plus_def image_add_atLeast)
lemma iIN_add: "[n…,d] ⊕ k = [n+k…,d]"
by (fastsimp simp add: iIN_def iT_Plus_def image_add_atLeastAtMost)
lemma iTILL_add: "[…i] ⊕ k = [k…,i]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_add)
lemma iMOD_add: "[r, mod m] ⊕ k = [r + k, mod m]"
apply (clarsimp simp: set_eq_iff iMOD_def iT_Plus_def image_iff)
apply (rule iffI)
thm mod_add
apply (clarsimp simp: mod_add)
apply (rule_tac x="x - k" in exI)
apply clarsimp
thm mod_sub_add[of k x]
apply (simp add: mod_sub_add)
done
lemma iMODb_add: "[r, mod m, c] ⊕ k = [r + k, mod m, c]"
by (simp add: iMODb_iMOD_iIN_conv iT_Plus_Int iMOD_add iIN_add)
lemmas iT_add =
iMOD_add
iMODb_add
iFROM_add
iIN_add
iTILL_add
iT_Plus_singleton
thm iT_add
thm
mod_mult_distrib
mod_mult_distrib2
thm
mod_eq_mult_distrib
mod_factor_imp_mod_0
mod_factor_div
mod_factor_div_mod
lemma iFROM_mult: "[n…] ⊗ k = [ n * k, mod k ]"
apply (case_tac "k = 0")
apply (simp add: iMOD_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (rule conj_cong, simp)
apply (rule iffI)
apply (drule mult_le_mono1[of _ _ k])
apply (rule order_trans, assumption)
apply (simp add: div_mult_cancel)
apply (drule div_le_mono[of _ _ k])
apply simp
done
lemma iIN_mult: "[n…,d] ⊗ k = [ n * k, mod k, d ]"
apply (case_tac "k = 0")
apply (simp add: iMODb_mod_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (rule conj_cong, simp)
apply (rule iffI)
apply (elim conjE)
apply (drule mult_le_mono1[of _ _ k], drule mult_le_mono1[of _ _ k])
apply (rule conjI)
apply (rule order_trans, assumption)
apply (simp add: div_mult_cancel)
apply (simp add: div_mult_cancel add_mult_distrib mult_commute[of k])
apply (erule conjE)
apply (drule div_le_mono[of _ _ k], drule div_le_mono[of _ _ k])
apply simp
done
lemma iTILL_mult: "[…n] ⊗ k = [ 0, mod k, n ]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_mult)
lemma iMOD_mult: "[r, mod m ] ⊗ k = [ r * k, mod m * k ]"
apply (case_tac "k = 0")
apply (simp add: iMOD_0 iT_mult_0 iIN_0 iTILL_0)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff iT_iff)
apply (subst mult_commute[of m k])
thm mod_mult2_eq
apply (simp add: mod_mult2_eq)
apply (rule iffI)
apply (elim conjE)
apply (drule mult_le_mono1[of _ _ k])
apply (simp add: div_mult_cancel)
apply (elim conjE)
apply (subgoal_tac "x mod k = 0")
prefer 2
apply (drule_tac arg_cong[where f="λx. x mod k"])
apply (simp add: mult_commute[of k])
apply (drule div_le_mono[of _ _ k])
apply simp
done
lemma iMODb_mult: "
[r, mod m, c ] ⊗ k = [ r * k, mod m * k, c ]"
apply (case_tac "k = 0")
apply (simp add: iMODb_mod_0 iT_mult_0 iIN_0 iTILL_0)
thm iMODb_iMOD_iTILL_conv
apply (subst iMODb_iMOD_iTILL_conv)
apply (simp add: iT_Mult_Int iMOD_mult iTILL_mult iMODb_iMOD_iTILL_conv)
apply (subst Int_assoc[symmetric])
thm Int_absorb2
apply (subst Int_absorb2)
apply (simp add: iMOD_subset)
thm iMOD_iTILL_iMODb_conv
apply (simp add: iMOD_iTILL_iMODb_conv add_mult_distrib2)
done
lemmas iT_mult =
iTILL_mult
iFROM_mult
iIN_mult
iMOD_mult
iMODb_mult
iT_Mult_singleton
thm
iT_mult
iT_mult_0
subsubsection {* Some conversions between intervals using constant addition and multiplication *}
lemma iFROM_conv: "[n…] = UNIV ⊕ n"
by (simp add: iFROM_0[symmetric] iFROM_add)
lemma iIN_conv: "[n…,d] = […d] ⊕ n"
by (simp add: iTILL_add)
lemma iMOD_conv: "[r, mod m] = [0…] ⊗ m ⊕ r"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iT_mult_0 iTILL_add)
by (simp add: iFROM_mult iMOD_add)
lemma iMODb_conv: "[r, mod m, c] = […c] ⊗ m ⊕ r"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iT_mult_0 iTILL_add)
apply (simp add: iTILL_mult iMODb_add)
done
text {* Some examples showing the utility of iMODb\_conv *}
lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp add: iT_defs)
apply safe
defer 1
apply simp+
txt {* The direct proof without iMODb\_conv fails *}
oops
lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def)
apply safe
apply simp+
done
lemma "[12, mod 10, 4] = {12, 22, 32, 42, 52}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def)
apply (simp add: atMost_def)
apply safe
apply simp+
done
lemma "[r, mod m, 4] = {r, r+m, r+2*m, r+3*m, r+4*m}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Mult_def iT_Plus_def atMost_def)
thm image_Collect
apply (simp add: image_Collect)
apply safe
apply fastsimp+
done
lemma "[2, mod 10, 4] = {2, 12, 22, 32, 42}"
apply (simp only: iMODb_conv)
apply (simp add: iT_defs iT_Plus_def iT_Mult_def)
apply fastsimp
done
subsubsection {* Subtraction of constants *}
definition iT_Plus_neg :: "iT => Time => iT" (infixl "⊕-" 55) where
"I ⊕- k ≡ {x. x + k ∈ I}"
lemma iT_Plus_neg_mem_iff: "(x ∈ I ⊕- k) = (x + k ∈ I)"
by (simp add: iT_Plus_neg_def)
thm iT_Plus_mem_iff2
lemma iT_Plus_neg_mem_iff2: "k ≤ x ==> (x - k ∈ I ⊕- k) = (x ∈ I)"
by (simp add: iT_Plus_neg_def)
lemma iT_Plus_neg_image_conv: "I ⊕- k = (λn.(n - k)) ` (I \<down>≥ k)"
apply (simp add: iT_Plus_neg_def cut_ge_def, safe)
thm image_eqI
apply (rule_tac x="x+k" in image_eqI)
apply simp+
done
lemma iT_Plus_neg_cut_eq: "t ≤ k ==> (I \<down>≥ t) ⊕- k = I ⊕- k"
by (simp add: set_eq_iff iT_Plus_neg_mem_iff cut_ge_mem_iff)
lemma iT_Plus_neg_mono: "A ⊆ B ==> A ⊕- k ⊆ B ⊕- k"
by (simp add: iT_Plus_neg_def subset_iff)
lemma iT_Plus_neg_empty: "{} ⊕- k = {}"
by (simp add: iT_Plus_neg_def)
lemma iT_Plus_neg_Max_less_empty: "
[| finite I; Max I < k |] ==> I ⊕- k = {}"
by (simp add: iT_Plus_neg_image_conv cut_ge_Max_empty)
lemma iT_Plus_neg_not_empty_iff: "(I ⊕- k ≠ {}) = (∃x∈I. k ≤ x)"
by (simp add: iT_Plus_neg_image_conv cut_ge_not_empty_iff)
lemma iT_Plus_neg_empty_iff: "
(I ⊕- k = {}) = (I = {} ∨ (finite I ∧ Max I < k))"
apply (case_tac "I = {}")
apply (simp add: iT_Plus_neg_empty)
apply (simp add: iT_Plus_neg_image_conv)
apply (case_tac "infinite I")
apply (simp add: nat_cut_ge_infinite_not_empty)
apply (simp add: cut_ge_empty_iff)
done
lemma iT_Plus_neg_assoc: "(I ⊕- a) ⊕- b = I ⊕- (a + b)"
apply (simp add: iT_Plus_neg_def)
apply (simp add: add_assoc add_commute[of b])
done
lemma iT_Plus_neg_commute: "I ⊕- a ⊕- b = I ⊕- b ⊕- a"
by (simp add: iT_Plus_neg_assoc add_commute[of b])
lemma iT_Plus_neg_0: "I ⊕- 0 = I"
by (simp add: iT_Plus_neg_image_conv cut_ge_0_all)
thm diff_add_assoc
lemma iT_Plus_Plus_neg_assoc: "b ≤ a ==> I ⊕ a ⊕- b = I ⊕ (a - b)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
apply fastsimp
apply (rule_tac x="x + b" in exI)
apply (simp add: le_diff_conv)
done
lemma iT_Plus_Plus_neg_assoc2: "a ≤ b ==> I ⊕ a ⊕- b = I ⊕- (b - a)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
apply fastsimp
apply (clarify, rename_tac x')
apply (rule_tac x="x' + a" in exI)
apply simp
done
lemma iT_Plus_neg_Plus_le_cut_eq: "
a ≤ b ==> (I ⊕- a) ⊕ b = (I \<down>≥ a) ⊕ (b - a)"
apply (simp add: iT_Plus_neg_image_conv)
apply (clarsimp simp add: set_eq_iff image_iff Bex_def cut_ge_mem_iff iT_Plus_mem_iff)
apply (rule iffI)
apply (clarify, rename_tac x')
apply (subgoal_tac "x' = x + a - b")
prefer 2
apply simp
apply (simp add: le_imp_diff_le le_add_diff)
apply fastsimp
done
corollary iT_Plus_neg_Plus_le_Min_eq: "
[| a ≤ b; a ≤ iMin I |] ==> (I ⊕- a) ⊕ b = I ⊕ (b - a)"
by (simp add: iT_Plus_neg_Plus_le_cut_eq cut_ge_Min_all)
lemma iT_Plus_neg_Plus_ge_cut_eq: "
b ≤ a ==> (I ⊕- a) ⊕ b = (I \<down>≥ a) ⊕- (a - b)"
apply (simp add: iT_Plus_neg_image_conv iT_Plus_def cut_cut_ge max_eqL)
apply (subst image_compose[symmetric])
apply (rule image_cong, simp)
apply (simp add: cut_ge_mem_iff)
done
corollary iT_Plus_neg_Plus_ge_Min_eq: "
[| b ≤ a; a ≤ iMin I |] ==> (I ⊕- a) ⊕ b = I ⊕- (a - b)"
by (simp add: iT_Plus_neg_Plus_ge_cut_eq cut_ge_Min_all)
lemma iT_Plus_neg_Mult_distrib: "
0 < m ==> I ⊕- n ⊗ m = I ⊗ m ⊕- n * m"
apply (clarsimp simp: set_eq_iff iT_Plus_neg_image_conv image_iff iT_Plus_def iT_Mult_def Bex_def cut_ge_mem_iff)
apply (rule iffI)
apply (clarsimp, rename_tac x')
apply (rule_tac x="x' * m" in exI)
apply (simp add: diff_mult_distrib)
apply (clarsimp, rename_tac x')
apply (rule_tac x="x' - n" in exI)
apply (simp add: diff_mult_distrib)
apply fastsimp
done
thm le_add_diff_inverse2
lemma iT_Plus_neg_Plus_le_inverse: "k ≤ iMin I ==> I ⊕- k ⊕ k = I"
by (simp add: iT_Plus_neg_Plus_le_Min_eq iT_Plus_0)
lemma iT_Plus_neg_Plus_inverse: "I ⊕- k ⊕ k = I \<down>≥ k"
by (simp add: iT_Plus_neg_Plus_ge_cut_eq iT_Plus_neg_0)
thm diff_add_inverse2
lemma iT_Plus_Plus_neg_inverse: "I ⊕ k ⊕- k = I"
by (simp add: iT_Plus_Plus_neg_assoc iT_Plus_0)
lemma iT_Plus_neg_Un: "(A ∪ B) ⊕- k = (A ⊕- k) ∪ (B ⊕- k)"
by (fastsimp simp: iT_Plus_neg_def)
lemma iT_Plus_neg_Int: "(A ∩ B) ⊕- k = (A ⊕- k) ∩ (B ⊕- k)"
by (fastsimp simp: iT_Plus_neg_def)
lemma iT_Plus_neg_Max_singleton: "[| finite I; I ≠ {} |] ==> I ⊕- Max I= {0}"
apply (rule set_eqI)
apply (simp add: iT_Plus_neg_def)
apply (case_tac "x = 0")
apply simp
apply fastsimp
done
lemma iT_Plus_neg_singleton: "{a} ⊕- k = (if k ≤ a then {a - k} else {})"
by (force simp add: set_eq_iff iT_Plus_neg_mem_iff singleton_iff)
corollary iT_Plus_neg_singleton1: "k ≤ a ==> {a} ⊕- k = {a-k}"
by (simp add: iT_Plus_neg_singleton)
corollary iT_Plus_neg_singleton2: "a < k ==> {a} ⊕- k= {}"
by (simp add: iT_Plus_neg_singleton)
lemma iT_Plus_neg_finite_iff: "finite (I ⊕- k) = finite I"
apply (simp add: iT_Plus_neg_image_conv)
thm inj_on_finite_image_iff
apply (simp add: inj_on_finite_image_iff inj_on_diff_nat cut_ge_mem_iff)
thm nat_cut_ge_finite_iff
apply (simp add: nat_cut_ge_finite_iff)
done
lemma iT_Plus_neg_Min: "
I ⊕- k ≠ {} ==> iMin (I ⊕- k) = iMin (I \<down>≥ k) - k"
apply (simp add: iT_Plus_neg_image_conv)
apply (simp add: iMin_mono2 monoI)
done
lemma iT_Plus_neg_Max: "
[| finite I; I ⊕- k ≠ {} |] ==> Max (I ⊕- k) = Max I - k"
apply (simp add: iT_Plus_neg_image_conv)
apply (simp add: Max_mono2 monoI cut_ge_finite cut_ge_Max_eq)
done
text {* Subtractions of constants from intervals *}
lemma iFROM_add_neg: "[n…] ⊕- k = [n - k…]"
by (fastsimp simp: set_eq_iff iT_Plus_neg_mem_iff)
lemma iTILL_add_neg: "[…n] ⊕- k = (if k ≤ n then […n - k] else {})"
by (force simp add: set_eq_iff iT_Plus_neg_mem_iff iT_iff)
lemma iTILL_add_neg1: "k ≤ n ==> […n] ⊕- k = […n-k]"
by (simp add: iTILL_add_neg)
lemma iTILL_add_neg2: "n < k ==> […n] ⊕- k = {}"
by (simp add: iTILL_add_neg)
lemma iIN_add_neg: "
[n…,d] ⊕- k = (
if k ≤ n then [n - k…,d]
else if k ≤ n + d then […n + d - k] else {})"
by (simp add: iIN_iFROM_iTILL_conv iT_Plus_neg_Int iFROM_add_neg iTILL_add_neg iFROM_0)
lemma iIN_add_neg1: "k ≤ n ==> [n…,d] ⊕- k = [n - k…,d]"
by (simp add: iIN_add_neg)
lemma iIN_add_neg2: "[| n ≤ k; k ≤ n + d |] ==> [n…,d] ⊕- k = […n + d - k]"
by (simp add: iIN_add_neg iIN_0_iTILL_conv)
lemma iIN_add_neg3: "n + d < k ==> [n…,d] ⊕- k = {}"
by (simp add: iT_Plus_neg_Max_less_empty iT_finite iT_Max)
lemma iMOD_0_add_neg: "[r, mod 0] ⊕- k = {r} ⊕- k"
by (simp add: iMOD_0 iIN_0)
(*
lemma "[25, mod 10] ⊕- 32 = [3, mod 10]"
apply (rule set_eqI)
apply (simp add: iT_Plus_neg_mem_iff iMOD_iff)
apply (simp add: mod_add_eq[of _ 32] mod_Suc)
apply clarify
apply (rule iffI)
apply simp+
done
*)
lemma iMOD_gr0_add_neg: "
0 < m ==>
[r, mod m] ⊕- k = (
if k ≤ r then [r - k, mod m]
else [(m + r mod m - k mod m) mod m, mod m])"
apply (rule set_eqI)
apply (simp add: iMOD_def iT_Plus_neg_def)
apply (simp add: eq_sym_conv[of _ "r mod m"])
apply (intro conjI impI)
thm mod_sub_add[of k r m] le_diff_conv
apply (simp add: eq_sym_conv[of _ "(r - k) mod m"] mod_sub_add le_diff_conv)
thm eq_commute[of "r mod m"]
thm mod_add_eq_mod_conv[of m x k r]
apply (simp add: eq_commute[of "r mod m"] mod_add_eq_mod_conv)
apply safe
apply (drule sym)
apply simp
done
lemma iMOD_add_neg: "
[r, mod m] ⊕- k = (
if k ≤ r then [r - k, mod m]
else if 0 < m then [(m + r mod m - k mod m) mod m, mod m] else {})"
apply (case_tac "0 < m")
apply (simp add: iMOD_gr0_add_neg)
apply (simp add: iMOD_0 iIN_0 iT_Plus_neg_singleton)
done
corollary iMOD_add_neg1: "
k ≤ r ==> [r, mod m] ⊕- k = [r - k, mod m]"
by (simp add: iMOD_add_neg)
lemma iMOD_add_neg2: "
[| 0 < m; r < k |] ==> [r, mod m] ⊕- k = [(m + r mod m - k mod m) mod m, mod m]"
by (simp add: iMOD_add_neg)
lemma iMODb_mod_0_add_neg: "[r, mod 0, c] ⊕- k = {r} ⊕- k"
by (simp add: iMODb_mod_0 iIN_0)
(*
lemma "[25, mod 10, 5] ⊕- 32 = [3, mod 10, 4]"
apply (rule set_eqI)
apply (simp add: iMODb_conv iT_Plus_neg_mem_iff iT_Plus_mem_iff iT_Mult_mem_iff)
apply (case_tac "x < 3", simp)
apply (simp add: linorder_not_less)
apply (rule_tac t="(x - 3) mod 10 = 0" and s="x mod 10 = 3" in subst)
thm mod_eq_diff_mod_0_conv
apply (simp add: mod_eq_diff_mod_0_conv[symmetric])
apply (rule_tac t="(7 + x) mod 10 = 0" and s="x mod 10 = 3" in subst)
apply (simp add: mod_add1_eq_if[of 7])
apply (rule conj_cong[OF refl])
thm div_add1_eq_if
apply (simp add: div_add1_eq_if)
thm div_diff1_eq1[where a=3 and b=x and m=10]
apply (simp add: div_diff1_eq1)
apply (simp add: iTILL_iff)
done
lemma "[25, mod 10, 5] ⊕- 32 = [3, mod 10, 4]"
apply (simp add: iT_Plus_neg_image_conv iMODb_cut_ge)
apply (simp add: iMODb_conv iT_Mult_def iT_Plus_def)
apply (rule_tac t=4 and s="Suc(Suc(Suc(Suc 0)))" in subst, simp)
apply (simp add: iTILL_def atMost_Suc)
done
*)
lemma iMODb_add_neg: "
[r, mod m, c] ⊕- k = (
if k ≤ r then [r - k, mod m, c]
else
if k ≤ r + m * c then
[(m + r mod m - k mod m) mod m, mod m, (r + m * c - k) div m]
else {})"
apply (clarsimp simp add: iMODb_iMOD_iIN_conv iT_Plus_neg_Int iMOD_add_neg iIN_add_neg)
apply (simp add: iMOD_iIN_iMODb_conv)
apply (rule_tac t="(m + r mod m - k mod m) mod m" and s="(r + m * c - k) mod m" in subst)
thm mod_diff1_eq[of k]
apply (simp add: mod_diff1_eq[of k])
apply (subst iMOD_iTILL_iMODb_conv, simp)
thm sub_mod_div_eq_div
apply (subst sub_mod_div_eq_div, simp)
done
lemma iMODb_add_neg': "
[r, mod m, c] ⊕- k = (
if k ≤ r then [r - k, mod m, c]
else if k ≤ r + m * c then
if k mod m ≤ r mod m
then [ r mod m - k mod m, mod m, c + r div m - k div m]
else [ m + r mod m - k mod m, mod m, c + r div m - Suc (k div m) ]
else {})"
apply (clarsimp simp add: iMODb_add_neg)
apply (case_tac "m = 0", simp+)
apply (case_tac "k mod m ≤ r mod m")
apply (clarsimp simp: linorder_not_le)
apply (simp add: divisor_add_diff_mod_if)
apply (simp add: div_diff1_eq_if)
apply (clarsimp simp: linorder_not_le)
apply (simp add: div_diff1_eq_if)
done
corollary iMODb_add_neg1: "
k ≤ r ==> [r, mod m, c] ⊕- k = [r - k, mod m, c]"
by (simp add: iMODb_add_neg)
corollary iMODb_add_neg2: "
[| r < k; k ≤ r + m * c |] ==>
[r, mod m, c] ⊕- k =
[(m + r mod m - k mod m) mod m, mod m, (r + m * c - k) div m]"
by (simp add: iMODb_add_neg)
corollary iMODb_add_neg2_mod_le: "
[| r < k; k ≤ r + m * c; k mod m ≤ r mod m |] ==>
[r, mod m, c] ⊕- k =
[ r mod m - k mod m, mod m, c + r div m - k div m]"
by (simp add: iMODb_add_neg')
corollary iMODb_add_neg2_mod_less: "
[| r < k; k ≤ r + m * c; r mod m < k mod m|] ==>
[r, mod m, c] ⊕- k =
[ m + r mod m - k mod m, mod m, c + r div m - Suc (k div m) ]"
by (simp add: iMODb_add_neg')
lemma iMODb_add_neg3: "r + m * c < k ==> [r, mod m, c] ⊕- k = {}"
by (simp add: iMODb_add_neg)
lemmas iT_add_neg =
iFROM_add_neg
iIN_add_neg
iTILL_add_neg
iMOD_add_neg
iMODb_add_neg
iT_Plus_neg_singleton
thm iT_add_neg
subsubsection {* Subtraction of intervals from constants *}
definition iT_Minus :: "Time => iT => iT" (infixl "\<ominus>" 55) where
"k \<ominus> I ≡ {x. x ≤ k ∧ (k - x) ∈ I}"
lemma iT_Minus_mem_iff: "(x ∈ k \<ominus> I) = (x ≤ k ∧ k - x ∈ I)"
by (simp add: iT_Minus_def)
lemma iT_Minus_mono: "A ⊆ B ==> k \<ominus> A ⊆ k \<ominus> B"
by (simp add: subset_iff iT_Minus_mem_iff)
lemma iT_Minus_image_conv: "k \<ominus> I = (λx. k - x) ` (I \<down>≤ k)"
by (fastsimp simp: iT_Minus_def cut_le_def image_iff)
lemma iT_Minus_cut_eq: "k ≤ t ==> k \<ominus> (I \<down>≤ t) = k \<ominus> I"
by (fastsimp simp: set_eq_iff iT_Minus_mem_iff)
lemma iT_Minus_Minus_cut_eq: "k \<ominus> (k \<ominus> (I \<down>≤ k)) = I \<down>≤ k"
by (fastsimp simp: iT_Minus_def)
lemma "10 \<ominus> […3] = [7…,3]"
by (fastsimp simp: iT_Minus_def)
lemma iT_Minus_empty: "k \<ominus> {} = {}"
by (simp add: iT_Minus_def)
lemma iT_Minus_0: "k \<ominus> {0} = {k}"
by (simp add: iT_Minus_image_conv cut_le_def image_Collect)
lemma iT_Minus_bound: "x ∈ k \<ominus> I ==> x ≤ k"
by (simp add: iT_Minus_def)
lemma iT_Minus_finite: "finite (k \<ominus> I)"
thm finite_nat_iff_bounded_le2
apply (rule finite_nat_iff_bounded_le2[THEN iffD2])
apply (rule_tac x=k in exI)
apply (simp add: iT_Minus_bound)
done
lemma iT_Minus_less_Min_empty: "k < iMin I ==> k \<ominus> I = {}"
by (simp add: iT_Minus_image_conv cut_le_Min_empty)
lemma iT_Minus_Min_singleton: "I ≠ {} ==> (iMin I) \<ominus> I = {0}"
apply (rule set_eqI)
apply (simp add: iT_Minus_mem_iff)
apply (fastsimp intro: iMinI_ex2)
done
lemma iT_Minus_empty_iff: "(k \<ominus> I = {}) = (I = {} ∨ k < iMin I)"
apply (case_tac "I = {}", simp add: iT_Minus_empty)
apply (simp add: iT_Minus_image_conv cut_le_empty_iff iMin_gr_iff)
done
(*
An example:
100 \<ominus> {60, 70, 80, 90, 95} = {5, 10, 20, 30, 40}
imirror {60, 70, 80, 90, 95} = {60, 65, 75, 95, 95}
{60, 65, 75, 85, 95} ⊕ 100 ⊕- (60 + 95)
= {160, 165, 175, 185, 195} ⊕- 155
= {5, 10, 20, 30, 40}
I ⊕ k ⊕- (iMin I + Max I))
*)
lemma iT_Minus_imirror_conv: "
k \<ominus> I = imirror (I \<down>≤ k) ⊕ k ⊕- (iMin I + Max (I \<down>≤ k))"
apply (case_tac "I = {}")
apply (simp add: iT_Minus_empty cut_le_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (case_tac "k < iMin I")
apply (simp add: iT_Minus_less_Min_empty cut_le_Min_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (simp add: linorder_not_less)
apply (frule cut_le_Min_not_empty[of _ k], assumption)
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_neg_image_conv iT_Plus_neg_mem_iff iT_Plus_mem_iff imirror_iff image_iff Bex_def i_cut_mem_iff cut_le_Min_eq)
apply (rule iffI)
apply (clarsimp, rename_tac x')
apply (rule_tac x="k - x' + iMin I + Max (I \<down>≤ k)" in exI, simp)
apply (simp add: add_assoc le_add_diff)
apply (simp add: add_commute[of k] le_add_diff nat_cut_le_finite cut_leI trans_le_add2)
apply (rule_tac x=x' in exI, simp)
apply (clarsimp, rename_tac x1 x2)
apply (rule_tac x=x2 in exI)
apply simp
thm nat_add_right_cancel[THEN iffD2, of _ _ k]
apply (drule nat_add_right_cancel[THEN iffD2, of _ _ k], simp)
thm add_diff_assoc2
apply (simp add: trans_le_add2 nat_cut_le_finite cut_le_mem_iff)
done
thm iT_Minus_imirror_conv
lemma iT_Minus_imirror_conv': "
k \<ominus> I = imirror (I \<down>≤ k) ⊕ k ⊕- (iMin (I \<down>≤ k) + Max (I \<down>≤ k))"
apply (case_tac "I = {}")
apply (simp add: iT_Minus_empty cut_le_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
apply (case_tac "k < iMin I")
apply (simp add: iT_Minus_less_Min_empty cut_le_Min_empty imirror_empty iT_Plus_empty iT_Plus_neg_empty)
thm cut_le_Min_eq
apply (simp add: cut_le_Min_not_empty cut_le_Min_eq iT_Minus_imirror_conv)
done
thm iT_Minus_bound
lemma iT_Minus_Max: "
[| I ≠ {}; iMin I ≤ k |] ==> Max (k \<ominus> I) = k - (iMin I)"
thm Max_equality
apply (rule Max_equality)
apply (simp add: iT_Minus_mem_iff iMinI_ex2)
apply (simp add: iT_Minus_finite)
apply (fastsimp simp: iT_Minus_def)
done
lemma iT_Minus_Min: "
[| I ≠ {}; iMin I ≤ k |] ==> iMin (k \<ominus> I) = k - (Max (I \<down>≤ k))"
apply (insert nat_cut_le_finite[of I k])
apply (frule cut_le_Min_not_empty[of _ k], assumption)
apply (rule iMin_equality)
apply (simp add: iT_Minus_mem_iff nat_cut_le_Max_le del: Max_le_iff)
thm subsetD[OF cut_le_subset, OF Max_in]
apply (simp add: subsetD[OF cut_le_subset, OF Max_in])
apply (clarsimp simp add: iT_Minus_image_conv image_iff, rename_tac x')
apply (rule diff_le_mono2)
apply (simp add: Max_ge_iff cut_le_mem_iff)
done
lemma iT_Minus_Minus_eq: "[| finite I; Max I ≤ k |] ==> k \<ominus> (k \<ominus> I) = I"
thm iT_Minus_cut_eq[of k k I, symmetric] iT_Minus_Minus_cut_eq
apply (simp add: iT_Minus_cut_eq[of k k I, symmetric] iT_Minus_Minus_cut_eq)
apply (simp add: cut_le_Max_all)
done
lemma iT_Minus_Minus_eq2: "I ⊆ […k] ==> k \<ominus> (k \<ominus> I) = I"
apply (case_tac "I = {}")
apply (simp add: iT_Minus_empty)
apply (rule iT_Minus_Minus_eq)
apply (simp add: finite_subset iTILL_finite)
thm Max_subset
apply (frule Max_subset)
apply (simp add: iTILL_finite iTILL_Max)+
done
(* An example:
10 \<ominus> (100 \<ominus> {97,98,99,101,102}) = {7,8,9}
1000 \<ominus> (100 \<ominus> {97,98,99,101,102, 998,1002}) = {997,998,999}
*)
lemma iT_Minus_Minus: "a \<ominus> (b \<ominus> I) = (I \<down>≤ b) ⊕ a ⊕- b"
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_image_conv iT_Plus_neg_image_conv image_iff Bex_def i_cut_mem_iff)
apply fastsimp
done
lemma iT_Minus_Plus_empty: "k < n ==> k \<ominus> (I ⊕ n) = {}"
apply (case_tac "I = {}")
apply (simp add: iT_Plus_empty iT_Minus_empty)
apply (simp add: iT_Minus_empty_iff iT_Plus_empty_iff iT_Plus_Min)
done
lemma iT_Minus_Plus_commute: "n ≤ k ==> k \<ominus> (I ⊕ n) = (k - n) \<ominus> I"
apply (rule set_eqI)
apply (simp add: iT_Minus_image_conv iT_Plus_image_conv image_iff Bex_def i_cut_mem_iff)
apply fastsimp
done
lemma iT_Minus_Plus_cut_assoc: "(k \<ominus> I) ⊕ n = (k + n) \<ominus> (I \<down>≤ k)"
apply (rule set_eqI)
apply (simp add: iT_Plus_mem_iff iT_Minus_mem_iff cut_le_mem_iff)
apply fastsimp
done
lemma iT_Minus_Plus_assoc: "
[| finite I; Max I ≤ k |] ==> (k \<ominus> I) ⊕ n = (k + n) \<ominus> I"
by (insert iT_Minus_Plus_cut_assoc[of k I n], simp add: cut_le_Max_all)
lemma iT_Minus_Plus_assoc2: "
I ⊆ […k] ==> (k \<ominus> I) ⊕ n = (k + n) \<ominus> I"
apply (case_tac "I = {}")
apply (simp add: iT_Minus_empty iT_Plus_empty)
apply (rule iT_Minus_Plus_assoc)
apply (simp add: finite_subset iTILL_finite)
thm Max_subset
apply (frule Max_subset)
apply (simp add: iTILL_finite iTILL_Max)+
done
lemma iT_Minus_Un: "k \<ominus> (A ∪ B) = (k \<ominus> A) ∪ (k \<ominus> B)"
by (fastsimp simp: iT_Minus_def)
lemma iT_Minus_Int: "k \<ominus> (A ∩ B) = (k \<ominus> A) ∩ (k \<ominus> B)"
by (fastsimp simp: set_eq_iff iT_Minus_mem_iff)
lemma iT_Minus_singleton: "k \<ominus> {a} = (if a ≤ k then {k - a} else {})"
by (simp add: iT_Minus_image_conv cut_le_singleton)
corollary iT_Minus_singleton1: "a ≤ k ==> k \<ominus> {a} = {k-a}"
by (simp add: iT_Minus_singleton)
corollary iT_Minus_singleton2: "k < a ==> k \<ominus> {a} = {}"
by (simp add: iT_Minus_singleton)
lemma iMOD_sub: "
k \<ominus> [r, mod m] =
(if r ≤ k then [(k - r) mod m, mod m, (k - r) div m] else {})"
apply (rule set_eqI)
apply (simp add: iT_Minus_mem_iff iT_iff)
thm mod_sub_eq_mod_swap[of r k x m, symmetric]
apply (fastsimp simp add: mod_sub_eq_mod_swap[of r, symmetric])
done
corollary iMOD_sub1: "
r ≤ k ==> k \<ominus> [r, mod m] = [(k - r) mod m, mod m, (k - r) div m]"
by (simp add: iMOD_sub)
corollary iMOD_sub2: "k < r ==> k \<ominus> [r, mod m] = {}"
thm iT_Minus_less_Min_empty
apply (rule iT_Minus_less_Min_empty)
apply (simp add: iMOD_Min)
done
lemma iTILL_sub: "k \<ominus> […n] = (if n ≤ k then [k - n…,n] else […k])"
by (force simp add: set_eq_iff iT_Minus_mem_iff iT_iff)
corollary iTILL_sub1: "n ≤ k ==> k \<ominus> […n] = [k - n…,n]"
by (simp add: iTILL_sub)
corollary iTILL_sub2: "k ≤ n ==> k \<ominus> […n] = […k]"
by (simp add: iTILL_sub iIN_0_iTILL_conv)
(* An example: 30 \<ominus> [2, mod 10] = {8,18,28} *)
lemma iMODb_sub: "
k \<ominus> [r, mod m, c] = (
if r + m * c ≤ k then [ k - r - m * c, mod m, c] else
if r ≤ k then [ (k - r) mod m, mod m, (k - r) div m] else {})"
apply (case_tac "m = 0")
apply (simp add: iMODb_mod_0 iIN_0 iT_Minus_singleton)
thm iMODb_iMOD_iTILL_conv
apply (subst iMODb_iMOD_iTILL_conv)
thm iT_Minus_Int
apply (subst iT_Minus_Int)
apply (simp add: iMOD_sub iTILL_sub)
apply (intro conjI impI)
apply simp
apply (subgoal_tac "(k - r) mod m ≤ k - (r + m * c)")
prefer 2
apply (subgoal_tac "m * c ≤ k - r - (k - r) mod m")
prefer 2
thm add_le_imp_le_diff2
apply (drule add_le_imp_le_diff2)
apply (drule div_le_mono[of _ _ m], simp)
apply (drule mult_le_mono2[of _ _ m])
apply (simp add: mult_div_cancel)
thm le_diff_conv2[OF mod_le_dividend]
apply (simp add: le_diff_conv2[OF mod_le_dividend] del: diff_diff_left)
thm iMODb_iMOD_iIN_conv
apply (subst iMODb_iMOD_iIN_conv)
apply (simp add: Int_assoc mult_div_cancel)
thm iIN_inter
apply (subst iIN_inter, simp+)
apply (rule set_eqI)
apply (fastsimp simp add: iT_iff mod_diff_mult_self2 diff_diff_left[symmetric] simp del: diff_diff_left)
apply (simp add: Int_absorb2 iMODb_iTILL_subset)
done
corollary iMODb_sub1: "
[| r ≤ k; k ≤ r + m * c |] ==>
k \<ominus> [r, mod m, c] = [(k - r) mod m, mod m, (k - r) div m]"
by (clarsimp simp: iMODb_sub iMODb_mod_0)
corollary iMODb_sub2: "k < r ==> k \<ominus> [r, mod m, c] = {}"
thm iT_Minus_less_Min_empty
apply (rule iT_Minus_less_Min_empty)
apply (simp add: iMODb_Min)
done
corollary iMODb_sub3: "
r + m * c ≤ k ==> k \<ominus> [r, mod m, c] = [ k - r - m * c, mod m, c]"
by (simp add: iMODb_sub)
lemma iFROM_sub: "k \<ominus> [n…] = (if n ≤ k then […k - n] else {})"
by (simp add: iMOD_1[symmetric] iMOD_sub iMODb_mod_1 iIN_0_iTILL_conv)
corollary iFROM_sub1: "n ≤ k ==> k \<ominus> [n…] = […k-n]"
by (simp add: iFROM_sub)
corollary iFROM_sub_empty: "k < n ==> k \<ominus> [n…] = {}"
by (simp add: iFROM_sub)
(* Examples:
10 \<ominus> [2…,3] = {3,4,5,6,7,8}
10 \<ominus> [7…,5] = {0,1,2,3}
*)
lemma iIN_sub: "
k \<ominus> [n…,d] = (
if n + d ≤ k then [k - (n + d)…,d]
else if n ≤ k then […k - n] else {})"
apply (simp add: iMODb_mod_1[symmetric] iMODb_sub)
apply (simp add: iMODb_mod_1 iIN_0_iTILL_conv)
done
lemma iIN_sub1: "n + d ≤ k ==> k \<ominus> [n…,d] = [k - (n + d)…,d]"
by (simp add: iIN_sub)
lemma iIN_sub2: "[| n ≤ k; k ≤ n + d |] ==> k \<ominus> [n…,d] = […k - n]"
by (clarsimp simp: iIN_sub iIN_0_iTILL_conv)
lemma iIN_sub3: "k < n ==> k \<ominus> [n…,d] = {}"
by (simp add: iIN_sub)
lemmas iT_sub =
iFROM_sub
iIN_sub
iTILL_sub
iMOD_sub
iMODb_sub
iT_Minus_singleton
thm iT_sub
subsubsection {* Division of intervals by constants *}
text {* Monotonicity and injectivity of artithmetic operators *}
lemma iMOD_div_right_strict_mono_on: "
[| 0 < k; k ≤ m |] ==> strict_mono_on (λx. x div k) [r, mod m]"
apply (rule div_right_strict_mono_on, assumption)
apply (clarsimp simp: iT_iff)
apply (drule_tac s="y mod m" in sym, simp)
apply (rule_tac y="x + m" in order_trans, simp)
apply (simp add: less_mod_eq_imp_add_divisor_le)
done
corollary iMOD_div_right_inj_on: "
[| 0 < k; k ≤ m |] ==> inj_on (λx. x div k) [r, mod m]"
by (rule strict_mono_on_imp_inj_on[OF iMOD_div_right_strict_mono_on])
lemma iMOD_mult_div_right_inj_on: "
inj_on (λx. x div (k::nat)) [r, mod (k * m)]"
apply (case_tac "k * m = 0")
apply (simp del: mult_is_0 add: iMOD_0 iIN_0)
apply (simp add: iMOD_div_right_inj_on)
done
lemma iMOD_mult_div_right_inj_on2: "
m mod k = 0 ==> inj_on (λx. x div k) [r, mod m]"
by (clarsimp simp add: iMOD_mult_div_right_inj_on)
lemma iMODb_div_right_strict_mono_on: "
[| 0 < k; k ≤ m |] ==> strict_mono_on (λx. x div k) [r, mod m, c]"
thm strict_mono_on_subset[OF iMOD_div_right_strict_mono_on iMODb_iMOD_subset_same]
by (rule strict_mono_on_subset[OF iMOD_div_right_strict_mono_on iMODb_iMOD_subset_same])
corollary iMODb_div_right_inj_on: "
[| 0 < k; k ≤ m |] ==> inj_on (λx. x div k) [r, mod m, c]"
by (rule strict_mono_on_imp_inj_on[OF iMODb_div_right_strict_mono_on])
lemma iMODb_mult_div_right_inj_on: "
inj_on (λx. x div (k::nat)) [r, mod (k * m), c]"
thm subset_inj_on[OF iMOD_div_right_inj_on iMODb_iMOD_subset_same]
by (rule subset_inj_on[OF iMOD_mult_div_right_inj_on iMODb_iMOD_subset_same])
corollary iMODb_mult_div_right_inj_on2: "
m mod k = 0 ==> inj_on (λx. x div k) [r, mod m, c]"
by (clarsimp simp: iMODb_mult_div_right_inj_on)
definition iT_Div :: "iT => Time => iT" (infixl "\<oslash>" 55) where
"I \<oslash> k ≡ (λn.(n div k)) ` I"
lemma iT_Div_image_conv: "I \<oslash> k = (λn.(n div k)) ` I"
by (simp add: iT_Div_def)
lemma iT_Div_mono: "A ⊆ B ==> A \<oslash> k ⊆ B \<oslash> k"
by (simp add: iT_Div_def image_mono)
lemma iT_Div_empty: "{} \<oslash> k = {}"
by (simp add: iT_Div_def)
lemma iT_Div_not_empty: "I ≠ {} ==> I \<oslash> k ≠ {}"
by (simp add: iT_Div_def)
lemma iT_Div_empty_iff: "(I \<oslash> k = {}) = (I = {})"
by (simp add: iT_Div_def)
lemma iT_Div_0: "I ≠ {} ==> I \<oslash> 0 = […0]"
by (force simp: iT_Div_def)
corollary iT_Div_0_if: "I \<oslash> 0 = (if I = {} then {} else […0])"
by (force simp: iT_Div_def)
corollary
iFROM_div_0: "[n…] \<oslash> 0 = […0]" and
iTILL_div_0: "[…n] \<oslash> 0 = […0]" and
iIN_div_0: "[n…,d] \<oslash> 0 = […0]" and
iMOD_div_0: "[r, mod m] \<oslash> 0 = […0]" and
iMODb_div_0: "[r, mod m, c] \<oslash> 0 = […0]"
by (simp add: iT_Div_0 iT_not_empty)+
lemmas iT_div_0 =
iTILL_div_0
iFROM_div_0
iIN_div_0
iMOD_div_0
iMODb_div_0
thm iT_div_0
lemma iT_Div_1: "I \<oslash> Suc 0 = I"
by (simp add: iT_Div_def)
lemma iT_Div_mem_iff_0: "x ∈ (I \<oslash> 0) = (I ≠ {} ∧ x = 0)"
by (force simp: iT_Div_0_if)
lemma iT_Div_mem_iff: "
0 < k ==> x ∈ (I \<oslash> k) = (∃y ∈ I. y div k = x)"
by (force simp: iT_Div_def)
lemma iT_Div_mem_iff2: "
0 < k ==> x div k ∈ (I \<oslash> k) = (∃y ∈ I. y div k = x div k)"
by (rule iT_Div_mem_iff)
lemma iT_Div_mem_iff_Int: "
0 < k ==> x ∈ (I \<oslash> k) = (I ∩ [x * k…,k - Suc 0] ≠ {})"
thm ex_in_conv[symmetric]
apply (simp add: ex_in_conv[symmetric] iT_Div_mem_iff iT_iff)
thm le_less_div_conv
apply (simp add: le_less_div_conv[symmetric] add_commute[of k])
thm less_eq_le_pred
apply (subst less_eq_le_pred, simp)
apply blast
done
lemma iT_Div_imp_mem: "
0 < k ==> x ∈ I ==> x div k ∈ (I \<oslash> k)"
by (force simp: iT_Div_mem_iff2)
lemma iT_Div_singleton: "{a} \<oslash> k = {a div k}"
by (simp add: iT_Div_def)
lemma iT_Div_Un: "(A ∪ B) \<oslash> k = (A \<oslash> k) ∪ (B \<oslash> k)"
by (fastsimp simp: iT_Div_def)
lemma iT_Div_insert: "(insert n I) \<oslash> k = insert (n div k) (I \<oslash> k)"
by (fastsimp simp: iT_Div_def)
(* Examples:
{1,2,3,4} \<oslash> 3 ∩ {5,6,7} \<oslash> 3 = {0,1} ∩ {1,2} = {1}
({1,2,3,4} ∩ {5,6,7}) \<oslash> 3 = {} \<oslash> 3 = {}
*)
lemma not_iT_Div_Int: "¬ (∀ k A B. (A ∩ B) \<oslash> k = (A \<oslash> k) ∩ (B \<oslash> k))"
apply simp
apply (
rule_tac x=3 in exI,
rule_tac x="{0}" in exI,
rule_tac x="{1}" in exI)
by (simp add: iT_Div_def)
thm subset_image_Int
lemma subset_iT_Div_Int: "A ⊆ B ==> (A ∩ B) \<oslash> k = (A \<oslash> k) ∩ (B \<oslash> k)"
by (simp add: iT_Div_def subset_image_Int)
lemma iFROM_iT_Div_Int: "
[| 0 < k; n ≤ iMin A |] ==> (A ∩ [n…]) \<oslash> k = (A \<oslash> k) ∩ ([n…] \<oslash> k)"
apply (rule subset_iT_Div_Int)
apply (blast intro: order_trans iMin_le)
done
lemma iIN_iT_Div_Int: "
[| 0 < k; n ≤ iMin A; ∀x∈A. x div k ≤ (n + d) div k --> x ≤ n + d |] ==>
(A ∩ [n…,d]) \<oslash> k = (A \<oslash> k) ∩ ([n…,d] \<oslash> k)"
apply (rule set_eqI)
apply (simp add: iT_Div_mem_iff Bex_def iIN_iff)
apply (rule iffI)
apply blast
apply (clarsimp, rename_tac x1 x2)
apply (frule iMin_le)
apply (rule_tac x=x1 in exI, simp)
apply (drule_tac x=x1 in bspec, simp)
apply (drule div_le_mono[of _ "n + d" k])
apply simp
done
corollary iTILL_iT_Div_Int: "
[| 0 < k; ∀x∈A. x div k ≤ n div k --> x ≤ n |] ==>
(A ∩ […n]) \<oslash> k = (A \<oslash> k) ∩ ([…n] \<oslash> k)"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_iT_Div_Int)
lemma iIN_iT_Div_Int_mod_0: "
[| 0 < k; n mod k = 0; ∀x∈A. x div k ≤ (n + d) div k --> x ≤ n + d |] ==>
(A ∩ [n…,d]) \<oslash> k = (A \<oslash> k) ∩ ([n…,d] \<oslash> k)"
apply (rule set_eqI)
apply (simp add: iT_Div_mem_iff Bex_def iIN_iff)
apply (rule iffI)
apply blast
apply (elim conjE exE, rename_tac x1 x2)
apply (rule_tac x=x1 in exI, simp)
apply (rule conjI)
apply (rule ccontr, simp add: linorder_not_le)
thm div_le_mono
apply (drule_tac m=n and n=x2 and k=k in div_le_mono)
thm less_mod_0_imp_div_less
apply (drule_tac a=x1 and m=k in less_mod_0_imp_div_less)
apply simp+
apply (drule_tac x=x1 in bspec, simp)
apply (drule div_le_mono[of _ "n + d" k])
apply simp
done
lemma mod_partition_iT_Div_Int: "
[| 0 < k; 0 < d |] ==>
(A ∩ [n * k…,d * k - Suc 0]) \<oslash> k =
(A \<oslash> k) ∩ ([n * k…,d * k - Suc 0] \<oslash> k)"
thm iIN_iT_Div_Int_mod_0
apply (rule iIN_iT_Div_Int_mod_0, simp+)
apply (clarify, rename_tac x)
apply (simp add: mod_0_imp_sub_1_div_conv)
apply (rule ccontr, simp add: linorder_not_le pred_less_eq_le)
apply (drule_tac n=x and k=k in div_le_mono)
apply simp
done
(*<*)
lemma "{0,1,2} ⊗ x = {0*x, 1*x, 2*x}"
by (simp add: iT_Mult_def)
(*>*)
corollary mod_partition_iT_Div_Int2: "
[| 0 < k; 0 < d; n mod k = 0; d mod k = 0 |] ==>
(A ∩ [n…,d - Suc 0]) \<oslash> k =
(A \<oslash> k) ∩ ([n…,d - Suc 0] \<oslash> k)"
apply (clarsimp simp: mult_commute[of k])
thm mod_partition_iT_Div_Int
apply (simp add: mod_partition_iT_Div_Int)
done
corollary mod_partition_iT_Div_Int_one_segment: "
0 < k ==>
(A ∩ [n * k…,k - Suc 0]) \<oslash> k = (A \<oslash> k) ∩ ([n * k…,k - Suc 0] \<oslash> k)"
by (insert mod_partition_iT_Div_Int[where d=1], simp)
corollary mod_partition_iT_Div_Int_one_segment2: "
[| 0 < k; n mod k = 0 |] ==>
(A ∩ [n…,k - Suc 0]) \<oslash> k = (A \<oslash> k) ∩ ([n…,k - Suc 0] \<oslash> k)"
by (insert mod_partition_iT_Div_Int2[where k=k and d=k and n=n], simp)
thm
iT_Div_Un
subset_iT_Div_Int
thm
mod_partition_iT_Div_Int
mod_partition_iT_Div_Int2
lemma iT_Div_assoc:"I \<oslash> a \<oslash> b = I \<oslash> (a * b)"
by (simp add: iT_Div_def image_image div_mult2_eq)
lemma iT_Div_commute: "I \<oslash> a \<oslash> b = I \<oslash> b \<oslash> a"
by (simp add: iT_Div_assoc mult_commute[of a])
lemma iT_Mult_Div_self: "0 < k ==> I ⊗ k \<oslash> k = I"
by (simp add: iT_Mult_def iT_Div_def image_image)
lemma iT_Mult_Div: "
[| 0 < d; k mod d = 0 |] ==> I ⊗ k \<oslash> d = I ⊗ (k div d)"
apply (clarsimp simp: mult_commute[of d])
apply (simp add: iT_Mult_assoc[symmetric] iT_Mult_Div_self)
done
lemma iT_Div_Mult_self: "
0 < k ==> I \<oslash> k ⊗ k = {y. ∃x ∈ I. y = x - x mod k}"
by (simp add: set_eq_iff iT_Mult_def iT_Div_def image_image image_iff div_mult_cancel)
thm div_add1_eq
lemma iT_Plus_Div_distrib_mod_less: "
∀x∈I. x mod m + n mod m < m ==> I ⊕ n \<oslash> m = I \<oslash> m ⊕ n div m"
by (simp add: set_eq_iff iT_Div_def iT_Plus_def image_image image_iff div_add1_eq1)
corollary iT_Plus_Div_distrib_mod_0: "
n mod m = 0 ==> I ⊕ n \<oslash> m = I \<oslash> m ⊕ n div m"
apply (case_tac "m = 0", simp add: iT_Plus_0 iT_Div_0)
apply (simp add: iT_Plus_Div_distrib_mod_less)
done
lemma iT_Div_Min: "I ≠ {} ==> iMin (I \<oslash> k) = iMin I div k"
by (simp add: iT_Div_def iMin_mono2 mono_def div_le_mono)
thm iT_Div_Min
corollary
iFROM_div_Min: "iMin ([n…] \<oslash> k) = n div k" and
iIN_div_Min: "iMin ([n…,d] \<oslash> k) = n div k" and
iTILL_div_Min: "iMin ([…n] \<oslash> k) = 0" and
iMOD_div_Min: "iMin ([r, mod m] \<oslash> k) = r div k" and
iMODb_div_Min: "iMin ([r, mod m, c] \<oslash> k) = r div k"
by (simp add: iT_not_empty iT_Div_Min iT_Min)+
lemmas iT_div_Min =
iFROM_div_Min
iIN_div_Min
iTILL_div_Min
iMOD_div_Min
iMODb_div_Min
thm iT_div_Min
lemma iT_Div_Max: "[| finite I; I ≠ {} |] ==> Max (I \<oslash> k) = Max I div k"
by (simp add: iT_Div_def Max_mono2 mono_def div_le_mono)
corollary
iIN_div_Max: "Max ([n…,d] \<oslash> k) = (n + d) div k" and
iTILL_div_Max: "Max ([…n] \<oslash> k) = n div k" and
iMODb_div_Max: "Max ([r, mod m, c] \<oslash> k) = (r + m * c) div k"
by (simp add: iT_not_empty iT_finite iT_Div_Max iT_Max)+
lemma iT_Div_0_finite: "finite (I \<oslash> 0)"
by (simp add: iT_Div_0_if iTILL_0)
lemma iT_Div_infinite_iff: "0 < k ==> infinite (I \<oslash> k) = infinite I"
apply (unfold iT_Div_def)
apply (rule iffI)
apply (rule infinite_image_imp_infinite, assumption)
apply (clarsimp simp: infinite_nat_iff_unbounded_le image_iff, rename_tac x1)
apply (drule_tac x="x1 * k" in spec, clarsimp, rename_tac x2)
apply (drule div_le_mono[of _ _ k], simp)
apply (rule_tac x="x2 div k" in exI)
apply fastsimp
done
lemma iT_Div_finite_iff: "0 < k ==> finite (I \<oslash> k) = finite I"
by (insert iT_Div_infinite_iff, simp)
lemma iFROM_div: "0 < k ==> [n…] \<oslash> k = [n div k…]"
apply (clarsimp simp: set_eq_iff iT_Div_def image_iff Bex_def iFROM_iff, rename_tac x)
apply (rule iffI)
apply (clarsimp simp: div_le_mono)
apply (rule_tac x="n mod k + k * x" in exI)
apply simp
apply (subst add_commute, subst le_diff_conv[symmetric])
apply (subst mult_div_cancel[symmetric])
apply simp
done
thm div_add1_eq
lemma iIN_div: "
0 < k ==>
[n…,d] \<oslash> k = [n div k…, d div k + (n mod k + d mod k) div k ]"
apply (clarsimp simp: set_eq_iff iT_Div_def image_iff Bex_def iIN_iff, rename_tac x)
apply (rule iffI)
apply clarify
apply (drule div_le_mono[of n _ k])
apply (drule div_le_mono[of _ "n + d" k])
apply (simp add: div_add1_eq[of n d])
apply (clarify, rename_tac x)
apply (simp add: add_assoc[symmetric] div_add1_eq[symmetric])
apply (frule mult_le_mono1[of "n div k" _ k])
apply (frule mult_le_mono1[of _ "(n + d) div k" k])
apply (simp add: mult_commute[of _ k] mult_div_cancel)
apply (simp add: le_diff_conv le_diff_conv2[OF mod_le_dividend])
apply (drule order_le_less[of _ "(n + d) div k", THEN iffD1], erule disjE)
apply (rule_tac x="k * x + n mod k" in exI)
apply (simp add: add_commute[of _ "n mod k"])
apply (case_tac "n mod k ≤ (n + d) mod k", simp)
apply (simp add: linorder_not_le)
apply (drule_tac m=x in less_imp_le_pred)
apply (drule_tac i=x and k=k in mult_le_mono2)
apply (simp add: diff_mult_distrib2 mult_div_cancel)
apply (subst add_commute[of "n mod k"])
apply (subst le_diff_conv2[symmetric])
apply (simp add: trans_le_add1)
apply (rule order_trans, assumption)
apply (rule diff_le_mono2)
apply (simp add: trans_le_add2)
apply (rule_tac x="n + d" in exI, simp)
done
corollary iIN_div_if: "
0 < k ==> [n…,d] \<oslash> k =
[n div k…, d div k + (if n mod k + d mod k < k then 0 else Suc 0)]"
apply (simp add: iIN_div)
apply (simp add: iIN_def add_assoc[symmetric] div_add1_eq[symmetric] div_add1_eq2[where a=n])
done
corollary iIN_div_eq1: "
[| 0 < k; n mod k + d mod k < k |] ==>
[n…,d] \<oslash> k = [n div k…,d div k]"
by (simp add: iIN_div_if)
corollary iIN_div_eq2: "
[| 0 < k; k ≤ n mod k + d mod k |] ==>
[n…,d] \<oslash> k = [n div k…, Suc (d div k)]"
by (simp add: iIN_div_if)
corollary iIN_div_mod_eq_0: "
[| 0 < k; n mod k = 0 |] ==> [n…,d] \<oslash> k = [n div k…,d div k]"
by (simp add: iIN_div_eq1)
lemma iTILL_div: "
0 < k ==> […n] \<oslash> k = […n div k]"
by (simp add: iIN_0_iTILL_conv[symmetric] iIN_div_if)
lemma iMOD_div_ge: "
[| 0 < m; m ≤ k |] ==> [r, mod m] \<oslash> k = [r div k…]"
apply (frule less_le_trans[of _ _ k], assumption)
apply (clarsimp simp: set_eq_iff iT_Div_mem_iff Bex_def iT_iff, rename_tac x)
apply (rule iffI)
apply (fastsimp simp: div_le_mono)
apply (rule_tac x="
if x * k < r then r else
((if x * k mod m ≤ r mod m then 0 else m) + r mod m + (x * k - x * k mod m))"
in exI)
apply (case_tac "x * k < r")
apply simp
apply (drule less_imp_le[of _ r], drule div_le_mono[of _ r k], simp)
apply (simp add: linorder_not_less linorder_not_le)
apply (simp add: div_le_conv add_commute[of k])
apply (subst diff_add_assoc, simp)+
thm div_mult_cancel
apply (simp add: div_mult_cancel[symmetric] del: add_diff_assoc)
apply (case_tac "x * k mod m = 0")
apply clarsimp
apply (drule sym)
apply (simp add: mult_commute[of m])
apply (blast intro: div_less order_less_le_trans mod_less_divisor)
apply simp
apply (intro conjI impI)
apply (simp add: div_mult_cancel)
apply (simp add: div_mult_cancel)
apply (subst add_commute, subst diff_add_assoc, simp)
apply (subst add_commute, subst div_mult_self1, simp)
apply (subst div_less)
apply (rule order_less_le_trans[of _ m], simp add: less_imp_diff_less)
apply simp
apply simp
apply (rule_tac y="x * k" in order_trans, assumption)
apply (simp add: div_mult_cancel)
apply (rule le_add_diff)
apply (simp add: trans_le_add1)
apply (simp add: div_mult_cancel)
apply (subst diff_add_assoc2, simp add: trans_le_add1)
apply simp
done
corollary iMOD_div_self: "
0 < m ==> [r, mod m] \<oslash> m = [r div m…]"
by (simp add: iMOD_div_ge)
lemma iMOD_div: "
[| 0 < k; m mod k = 0 |] ==>
[r, mod m] \<oslash> k = [r div k, mod (m div k) ]"
apply (case_tac "m = 0")
apply (simp add: iMOD_0 iIN_0 iT_Div_singleton)
apply (clarsimp, rename_tac q)
thm iMOD_mult[of "r div k" q k]
apply (cut_tac r="r div k" and k=k and m=q in iMOD_mult)
thm arg_cong[where f="λx. x ⊕ (r mod k)"]
apply (drule arg_cong[where f="λx. x ⊕ (r mod k)"])
apply (drule sym)
apply (simp add: iMOD_add mult_commute[of k])
thm iT_Plus_Div_distrib_mod_less
apply (cut_tac I="[r div k, mod q] ⊗ k" and m=k and n="r mod k" in iT_Plus_Div_distrib_mod_less)
apply (rule ballI)
apply (simp only: iMOD_mult iMOD_iff, elim conjE)
thm mod_factor_imp_mod_0[of x q k]
apply (drule mod_factor_imp_mod_0)
apply simp
apply (simp add: iT_Plus_0)
thm iT_Mult_Div[OF _ mod_self]
apply (simp add: iT_Mult_Div[OF _ mod_self] iT_Mult_1)
done
thm
iMOD_div
iMOD_div_ge
lemma iMODb_div_self: "
0 < m ==> [r, mod m, c] \<oslash> m = [r div m…,c]"
thm iMODb_iMOD_iTILL_conv
apply (subst iMODb_iMOD_iTILL_conv)
thm iTILL_iT_Div_Int
apply (subst iTILL_iT_Div_Int)
apply simp
apply (clarsimp simp: iT_iff simp del: div_mult_self1 div_mult_self2, rename_tac x)
thm div_le_mod_le_imp_le
apply (drule div_le_mod_le_imp_le)
apply simp+
apply (simp add: iMOD_div_self iTILL_div iFROM_iTILL_iIN_conv)
done
lemma iMODb_div_ge: "
[| 0 < m; m ≤ k |] ==>
[r, mod m, c] \<oslash> k = [r div k…,(r + m * c) div k - r div k]"
apply (case_tac "m = k")
apply (simp add: iMODb_div_self)
apply (drule le_neq_trans, simp+)
apply (induct c)
apply (simp add: iMODb_0 iIN_0 iT_Div_singleton)
apply (rule_tac t="[ r, mod m, Suc c ]" and s="[ r, mod m, c ] ∪ {r + m * c + m}" in subst)
thm iMODb_append_union_Suc[of r m c 0, symmetric]
apply (cut_tac c=c and c'=0 and r=r and m=m in iMODb_append_union_Suc[symmetric])
apply (simp add: iMODb_0 iIN_0 add_commute[of m] add_assoc)
apply (subst iT_Div_Un)
apply (simp add: iT_Div_singleton)
apply (simp add: add_commute[of m] add_assoc[symmetric])
apply (case_tac "(r + m * c) mod k + m mod k < k")
thm div_add1_eq1
apply (simp add: div_add1_eq1)
apply (rule insert_absorb)
apply (simp add: iIN_iff div_le_mono)
apply (simp add: linorder_not_less)
thm div_add1_eq2
apply (simp add: div_add1_eq2)
apply (rule_tac t="Suc ((r + m * c) div k)" and s="Suc (r div k + ((r + m * c) div k - r div k))" in subst)
apply (simp add: div_le_mono)
thm iIN_Suc_insert_conv
apply (simp add: iIN_Suc_insert_conv)
done
thm div_add1_eq_if
corollary iMODb_div_ge_if: "
[| 0 < m; m ≤ k |] ==>
[r, mod m, c] \<oslash> k =
[r div k…, m * c div k + (if r mod k + m * c mod k < k then 0 else Suc 0)]"
by (simp add: iMODb_div_ge div_add1_eq_if[of _ r])
thm iMODb_div_ge
lemma iMODb_div: "
[| 0 < k; m mod k = 0 |] ==>
[r, mod m, c] \<oslash> k = [r div k, mod (m div k), c ]"
apply (subst iMODb_iMOD_iTILL_conv)
thm iTILL_iT_Div_Int[of k "[r, mod m]" "m * c"]
apply (subst iTILL_iT_Div_Int)
apply simp
apply (simp add: Ball_def iMOD_iff, intro allI impI, elim conjE, rename_tac x)
apply (drule div_le_mod_le_imp_le)
apply (subst mod_add1_eq_if)
thm mod_0_imp_mod_mult_right_0
apply (simp add: mod_0_imp_mod_mult_right_0)
thm mod_eq_mod_0_imp_mod_eq[of x m r k]
apply (drule mod_eq_mod_0_imp_mod_eq, simp+)
apply (simp add: iMOD_div iTILL_div)
apply (simp add: iMOD_iTILL_iMODb_conv div_le_mono)
apply (clarsimp simp: mult_assoc iMODb_mod_0 iMOD_0)
done
lemmas iT_div =
iTILL_div
iFROM_div
iIN_div
iMOD_div
iMODb_div
iT_Div_singleton
thm
iT_div
iT_div_0
text {* This lemma is valid for all @{term "k ≤ m"},i. e., also for k with @{term "m mod k ≠ 0"}. *}
lemma iMODb_div_unique: "
[| 0 < k; k ≤ m; k ≤ c; [r', mod m', c'] = [r, mod m, c] \<oslash> k |] ==>
r' = r div k ∧ m' = m div k ∧ c' = c"
apply (case_tac "r' ≠ r div k")
thm iT_Div_Min
apply (drule arg_cong[where f="iMin"])
apply (simp add: iT_Min iT_not_empty iT_Div_Min)
apply simp
apply (case_tac "m' = 0 ∨ c' = 0")
apply (subgoal_tac "[ r div k, mod m', c' ] = {r div k}")
prefer 2
apply (rule iMODb_singleton_eq_conv[THEN iffD2], simp)
apply simp
apply (drule arg_cong[where f="Max"])
apply (simp add: iMODb_mod_0 iIN_0 iT_Max iT_Div_Max iT_Div_finite_iff iT_Div_not_empty iT_finite iT_not_empty)
apply (subgoal_tac "r div k < (r + m * c) div k", simp)
thm div_add1_eq_if[of k r "m * c"]
apply (subst div_add1_eq_if, simp)
apply clarsimp
apply (rule order_less_le_trans[of _ "k * k div k"], simp)
apply (rule div_le_mono)
apply (simp add: mult_mono)
apply (subgoal_tac "c' = c")
prefer 2
apply (drule arg_cong[where f="λA. card A"])
thm card_image[OF iMODb_div_right_inj_on]
apply (simp add: iT_Div_def card_image[OF iMODb_div_right_inj_on] iMODb_card)
apply clarsimp
thm iMODb_div_right_strict_mono_on
apply (frule iMODb_div_right_strict_mono_on[of k m r c], assumption)
thm iMODb_inext_nth_diff
apply (frule_tac a=k and b=0 and m=m' and r="r div k" and c=c in iMODb_inext_nth_diff, simp)
thm inext_nth_image[OF iMODb_not_empty]
apply (simp add: iT_Div_Min iT_not_empty iT_Min)
apply (simp add: iT_Div_def inext_nth_image[OF iMODb_not_empty])
apply (simp add: iMODb_inext_nth)
done
lemma iMODb_div_mod_gr0_is_0_not_ex0: "
[| 0 < k; k < m; 0 < m mod k; k ≤ c; r mod k = 0 |] ==>
¬(∃r' m' c'. [r', mod m', c'] = [r, mod m, c] \<oslash> k)"
apply (rule ccontr, simp, elim exE conjE)
thm iMODb_div_unique
apply (frule_tac r'=r' and m'=m' and c'=c' and r=r and k=k and m=m and c=c
in iMODb_div_unique[OF _ less_imp_le], simp+)
apply (drule arg_cong[where f="Max"])
apply (simp add: iT_Max iT_Div_Max iT_Div_finite_iff iT_Div_not_empty iT_finite iT_not_empty)
apply (simp add: div_add1_eq1)
apply (simp add: mult_commute[of m])
thm div_mult1_eq[of m c]
apply (simp add: div_mult1_eq[of c m] div_eq_0_conv)
apply (subgoal_tac "c ≤ c * (m mod k)")
apply simp+
done
lemma iMODb_div_mod_gr0_not_ex__arith_aux1: "
[| (0::nat) < k; k < m; 0 < x1 |] ==>
x1 * m + x2 - x mod k + x3 + x mod k = x1 * m + x2 + x3"
apply (drule Suc_leI[of _ x1])
apply (drule mult_le_mono1[of "Suc 0" _ m])
apply (subgoal_tac "x mod k ≤ x1 * m")
prefer 2
apply (rule order_trans[OF mod_le_divisor], assumption)
apply (rule order_less_imp_le)
apply (rule order_less_le_trans)
apply simp+
done
lemma iMODb_div_mod_gr0_not_ex: "
[| 0 < k; k < m; 0 < m mod k; k ≤ c |] ==>
¬(∃r' m' c'. [r', mod m', c'] = [r, mod m, c] \<oslash> k)"
apply (case_tac "r mod k = 0")
thm iMODb_div_mod_gr0_is_0_not_ex0
apply (simp add: iMODb_div_mod_gr0_is_0_not_ex0)
apply (rule ccontr, simp, elim exE conjE)
thm iMODb_div_unique
apply (frule_tac r'=r' and m'=m' and c'=c' and r=r and k=k and m=m and c=c
in iMODb_div_unique[OF _ less_imp_le], simp+)
apply clarsimp
apply (drule arg_cong[where f="Max"])
apply (simp add: iT_Max iT_Div_Max iT_Div_finite_iff iT_Div_not_empty iT_finite iT_not_empty)
thm div_add1_eq
apply (simp add: div_add1_eq[of r "m * c"])
apply (simp add: mult_commute[of _ c])
thm div_mult1_eq[of c m k]
apply (clarsimp simp add: div_mult1_eq[of c m k])
apply (subgoal_tac "Suc 0 ≤ c * (m mod k) div k", simp)
apply (thin_tac "?x = 0")+
apply (drule div_le_mono[of k c k], simp)
apply (rule order_trans[of _ "c div k"], simp)
apply (rule div_le_mono, simp)
done
thm iMODb_div_mod_gr0_not_ex
thm
cut_le_image
iMOD_div_right_strict_mono_on
iMOD_cut_le
thm card_image[OF strict_mono_on_imp_inj_on]
lemma iMOD_div_eq_imp_iMODb_div_eq: "
[| 0 < k; k ≤ m; [r', mod m'] = [r, mod m] \<oslash> k |] ==>
[r', mod m', c] = [r, mod m, c] \<oslash> k"
apply (subgoal_tac "r' = r div k")
prefer 2
apply (drule arg_cong[where f=iMin])
apply (simp add: iT_Div_Min iMOD_not_empty iMOD_Min)
apply clarsimp
apply (frule iMOD_div_right_strict_mono_on[of _ m r], assumption)
thm iMODb_div_right_strict_mono_on[of k m r c]
thm card_image[OF strict_mono_on_imp_inj_on]
thm card_image[OF strict_mono_on_imp_inj_on[OF iMODb_div_right_strict_mono_on[of k m r c]]]
apply (frule card_image[OF strict_mono_on_imp_inj_on[OF iMODb_div_right_strict_mono_on[of k m r c]]], assumption)
apply (simp add: iMODb_card)
apply (subgoal_tac "r + m * c ∈ [r, mod m]")
prefer 2
apply (simp add: iMOD_iff)
thm iMOD_cut_le[of r m "r + m * c"]
apply (subgoal_tac "[r, mod m, c] = [ r, mod m ] \<down>≤ (r + m * c)")
prefer 2
apply (simp add: iMOD_cut_le1)
apply (simp add: iT_Div_def)
thm cut_le_image[OF _ subset_refl]
apply (simp add: cut_le_image[symmetric])
apply (drule sym)
apply (simp add: iMOD_cut_le)
apply (simp add: linorder_not_le[of "r div k", symmetric])
thm div_le_mono
apply (simp add: div_le_mono)
apply (case_tac "m' = 0")
apply (simp add: iMODb_mod_0_card)
apply (rule arg_cong[where f="λc. [r div k, mod m', c]"])
apply (simp add: iMODb_card)
done
lemma iMOD_div_unique: "
[| 0 < k; k ≤ m; [r', mod m'] = [r, mod m] \<oslash> k |] ==>
r' = r div k ∧ m' = m div k"
thm iMOD_div_eq_imp_iMODb_div_eq
apply (frule iMOD_div_eq_imp_iMODb_div_eq[of k m r' m' r k], assumption+)
thm iMODb_div_unique[of k _ k]
apply (simp add: iMODb_div_unique[of k _ k])
done
thm iMODb_div_mod_gr0_not_ex
lemma iMOD_div_mod_gr0_not_ex: "
[| 0 < k; k < m; 0 < m mod k |] ==>
¬ (∃r' m'. [r', mod m'] = [r, mod m] \<oslash> k)"
apply (rule ccontr, clarsimp)
thm iMOD_div_eq_imp_iMODb_div_eq[OF _ less_imp_le]
apply (frule_tac k=k and m=m and r'=r' and m'=m' and c=k
in iMOD_div_eq_imp_iMODb_div_eq[OF _ less_imp_le], assumption+)
thm iMODb_div_mod_gr0_not_ex[of k m k r]
apply (frule iMODb_div_mod_gr0_not_ex[of k m k r], simp+)
done
subsection {* Interval cut operators with arithmetic interval operators *}
lemma
iT_Plus_cut_le2: "(I ⊕ k) \<down>≤ (t + k) = (I \<down>≤ t) ⊕ k" and
iT_Plus_cut_less2: "(I ⊕ k) \<down>< (t + k) = (I \<down>< t) ⊕ k" and
iT_Plus_cut_ge2: "(I ⊕ k) \<down>≥ (t + k) = (I \<down>≥ t) ⊕ k" and
iT_Plus_cut_greater2: "(I ⊕ k) \<down>> (t + k) = (I \<down>> t) ⊕ k"
unfolding iT_Plus_def by fastsimp+
lemma iT_Plus_cut_le: "
(I ⊕ k) \<down>≤ t = (if t < k then {} else I \<down>≤ (t - k) ⊕ k)"
apply (case_tac "t < k")
apply (simp add: cut_le_empty_iff iT_Plus_mem_iff)
thm iT_Plus_cut_le2[of I k "t - k"]
apply (insert iT_Plus_cut_le2[of I k "t - k"], simp)
done
lemma iT_Plus_cut_less: "(I ⊕ k) \<down>< t = I \<down>< (t - k) ⊕ k"
apply (case_tac "t < k")
apply (simp add: cut_less_0_empty iT_Plus_empty cut_less_empty_iff iT_Plus_mem_iff)
apply (insert iT_Plus_cut_less2[of I k "t - k"], simp)
done
lemma iT_Plus_cut_ge: "(I ⊕ k) \<down>≥ t = I \<down>≥ (t - k) ⊕ k"
apply (case_tac "t < k")
apply (simp add: cut_ge_0_all cut_ge_all_iff iT_Plus_mem_iff)
apply (insert iT_Plus_cut_ge2[of I k "t - k"], simp)
done
lemma iT_Plus_cut_greater: "
(I ⊕ k) \<down>> t = (if t < k then I ⊕ k else I \<down>> (t - k) ⊕ k)"
apply (case_tac "t < k")
apply (simp add: cut_greater_all_iff iT_Plus_mem_iff)
apply (insert iT_Plus_cut_greater2[of I k "t - k"], simp)
done
lemma
iT_Mult_cut_le2: "0 < k ==> (I ⊗ k) \<down>≤ (t * k) = (I \<down>≤ t) ⊗ k" and
iT_Mult_cut_less2: "0 < k ==> (I ⊗ k) \<down>< (t * k) = (I \<down>< t) ⊗ k" and
iT_Mult_cut_ge2: "0 < k ==> (I ⊗ k) \<down>≥ (t * k) = (I \<down>≥ t) ⊗ k" and
iT_Mult_cut_greater2: "0 < k ==> (I ⊗ k) \<down>> (t * k) = (I \<down>> t) ⊗ k"
unfolding iT_Mult_def by fastsimp+
lemma iT_Mult_cut_le: "
0 < k ==> (I ⊗ k) \<down>≤ t = (I \<down>≤ (t div k)) ⊗ k"
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff cut_le_mem_iff)
apply (rule conj_cong, simp)+
apply (rule iffI)
apply (simp add: div_le_mono)
apply (rule div_le_mod_le_imp_le, simp+)
done
lemma iT_Mult_cut_less: "
0 < k ==> (I ⊗ k) \<down>< t =
(if t mod k = 0 then (I \<down>< (t div k)) else I \<down>< Suc (t div k)) ⊗ k"
apply (case_tac "t mod k = 0")
apply (clarsimp simp add: mult_commute[of k] iT_Mult_cut_less2)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff cut_less_mem_iff)
apply (rule conj_cong, simp)+
apply (subst less_Suc_eq_le)
apply (rule iffI)
apply (rule div_le_mono, simp)
apply (rule ccontr, simp add: linorder_not_less)
apply (drule le_imp_less_or_eq[of t], erule disjE)
thm less_mod_0_imp_div_less[of t x k]
apply (fastsimp dest: less_mod_0_imp_div_less[of t _ k])
apply simp
done
lemma iT_Mult_cut_greater: "
0 < k ==> (I ⊗ k) \<down>> t = (I \<down>> (t div k)) ⊗ k"
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff cut_greater_mem_iff)
apply (rule conj_cong, simp)+
apply (rule iffI)
apply (simp add: less_mod_ge_imp_div_less)
apply (rule ccontr, simp add: linorder_not_less)
apply (fastsimp dest: div_le_mono[of _ _ k])
done
lemma iT_Mult_cut_ge: "
0 < k ==> (I ⊗ k) \<down>≥ t =
(if t mod k = 0 then (I \<down>≥ (t div k)) else I \<down>≥ Suc (t div k)) ⊗ k"
apply (case_tac "t mod k = 0")
apply (clarsimp simp add: mult_commute[of k] iT_Mult_cut_ge2)
apply (clarsimp simp: set_eq_iff iT_Mult_mem_iff cut_ge_mem_iff)
apply (rule conj_cong, simp)+
apply (rule iffI)
apply (rule Suc_leI)
apply (simp add: le_mod_greater_imp_div_less)
apply (rule ccontr)
apply (drule Suc_le_lessD)
apply (simp add: linorder_not_le)
thm div_le_mono[OF order_less_imp_le]
apply (fastsimp dest: div_le_mono[OF order_less_imp_le, of _ t k])
done
lemma iT_Plus_neg_cut_le2: "k ≤ t ==> (I ⊕- k) \<down>≤ (t - k) = (I \<down>≤ t) ⊕- k"
apply (simp add: iT_Plus_neg_image_conv)
thm i_cut_commute_disj[of "op \<down>≤" "op \<down>≥"]
apply (simp add: i_cut_commute_disj[of "op \<down>≤" "op \<down>≥"])
apply (rule i_cut_image[OF sub_left_strict_mono_on])
apply (simp add: cut_ge_Int_conv)+
done
lemma iT_Plus_neg_cut_less2: "(I ⊕- k) \<down>< (t - k) = (I \<down>< t) ⊕- k"
apply (case_tac "t ≤ k")
apply (simp add: cut_less_0_empty)
apply (case_tac "I \<down>< t = {}")
apply (simp add: iT_Plus_neg_empty)
apply (rule sym, rule iT_Plus_neg_Max_less_empty[OF nat_cut_less_finite])
apply (rule order_less_le_trans[OF cut_less_Max_less[OF nat_cut_less_finite]], assumption+)
apply (simp add: linorder_not_le iT_Plus_neg_image_conv)
apply (simp add: i_cut_commute_disj[of "op \<down><" "op \<down>≥"])
apply (rule i_cut_image[OF sub_left_strict_mono_on])
apply (simp add: cut_ge_Int_conv)+
done
lemma iT_Plus_neg_cut_ge2: "(I ⊕- k) \<down>≥ (t - k) = (I \<down>≥ t) ⊕- k"
apply (case_tac "t ≤ k")
apply (simp add: cut_ge_0_all iT_Plus_neg_cut_eq)
apply (simp add: linorder_not_le iT_Plus_neg_image_conv)
apply (simp add: i_cut_commute_disj[of "op \<down>≥" "op \<down>≥"])
apply (rule i_cut_image[OF sub_left_strict_mono_on])
apply (simp add: cut_ge_Int_conv)+
done
lemma iT_Plus_neg_cut_greater2: "k ≤ t ==> (I ⊕- k) \<down>> (t - k) = (I \<down>> t) ⊕- k"
apply (simp add: iT_Plus_neg_image_conv)
apply (simp add: i_cut_commute_disj[of "op \<down>>" "op \<down>≥"])
apply (rule i_cut_image[OF sub_left_strict_mono_on])
apply (simp add: cut_ge_Int_conv)+
done
lemma iT_Plus_neg_cut_le: "(I ⊕- k) \<down>≤ t = I \<down>≤ (t + k) ⊕- k"
by (insert iT_Plus_neg_cut_le2[of k "t + k" I, OF le_add2], simp)
lemma iT_Plus_neg_cut_less: "(I ⊕- k) \<down>< t = I \<down>< (t + k) ⊕- k"
by (insert iT_Plus_neg_cut_less2[of I k "t + k"], simp)
lemma iT_Plus_neg_cut_ge: "(I ⊕- k) \<down>≥ t = I \<down>≥ (t + k) ⊕- k"
by (insert iT_Plus_neg_cut_ge2[of I k "t + k"], simp)
lemma iT_Plus_neg_cut_greater: "(I ⊕- k) \<down>> t = I \<down>> (t + k) ⊕- k"
by (insert iT_Plus_neg_cut_greater2[of k "t + k" I], simp)
lemma iT_Minus_cut_le2: "t ≤ k ==> (k \<ominus> I) \<down>≤ (k - t) = k \<ominus> (I \<down>≥ t)"
by (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
lemma iT_Minus_cut_less2: "(k \<ominus> I) \<down>< (k - t) = k \<ominus> (I \<down>> t)"
by (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
lemma iT_Minus_cut_ge2: "(k \<ominus> I) \<down>≥ (k - t) = k \<ominus> (I \<down>≤ t)"
by (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
lemma iT_Minus_cut_greater2: "t ≤ k ==> (k \<ominus> I) \<down>> (k - t) = k \<ominus> (I \<down>< t)"
by (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
lemma iT_Minus_cut_le: "(k \<ominus> I) \<down>≤ t = k \<ominus> (I \<down>≥ (k - t))"
by (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
lemma iT_Minus_cut_less: "
(k \<ominus> I) \<down>< t = (if t ≤ k then k \<ominus> (I \<down>> (k - t)) else k \<ominus> I)"
apply (case_tac "t ≤ k")
apply (cut_tac iT_Minus_cut_less2[of k I "k - t"], simp)
apply (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
done
lemma iT_Minus_cut_ge: "
(k \<ominus> I) \<down>≥ t = (if t ≤ k then k \<ominus> (I \<down>≤ (k - t)) else {})"
apply (case_tac "t ≤ k")
apply (cut_tac iT_Minus_cut_ge2[of k I "k - t"], simp)
apply (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
done
lemma iT_Minus_cut_greater: "(k \<ominus> I) \<down>> t = k \<ominus> (I \<down>< (k - t))"
apply (case_tac "t ≤ k")
apply (cut_tac iT_Minus_cut_greater2[of "k - t" k I], simp+)
apply (fastsimp simp: i_cut_mem_iff iT_Minus_mem_iff)
done
thm iT_Div_def
thm iT_Mult_cut_le2
thm iT_Div_mem_iff
lemma iT_Div_cut_le: "
0 < k ==> (I \<oslash> k) \<down>≤ t = I \<down>≤ (t * k + (k - Suc 0)) \<oslash> k"
apply (simp add: set_eq_iff i_cut_mem_iff iT_Div_mem_iff Bex_def)
thm div_le_conv
apply (fastsimp simp: div_le_conv)
done
lemma iT_Div_cut_less: "
0 < k ==> (I \<oslash> k) \<down>< t = I \<down>< (t * k) \<oslash> k"
apply (case_tac "t = 0")
apply (simp add: cut_less_0_empty iT_Div_empty)
apply (simp add: nat_cut_less_le_conv iT_Div_cut_le diff_mult_distrib)
done
lemma iT_Div_cut_ge: "
0 < k ==> (I \<oslash> k) \<down>≥ t = I \<down>≥ (t * k) \<oslash> k"
apply (simp add: set_eq_iff i_cut_mem_iff iT_Div_mem_iff Bex_def)
thm le_div_conv
apply (fastsimp simp: le_div_conv)
done
lemma iT_Div_cut_greater: "
0 < k ==> (I \<oslash> k) \<down>> t = I \<down>> (t * k + (k - Suc 0)) \<oslash> k"
by (simp add: nat_cut_ge_greater_conv[symmetric] iT_Div_cut_ge add_commute[of k])
lemma iT_Div_cut_le2: "
0 < k ==> (I \<oslash> k) \<down>≤ (t div k) = I \<down>≤ (t - t mod k + (k - Suc 0)) \<oslash> k"
by (frule iT_Div_cut_le[of k I "t div k"], simp add: div_mult_cancel)
lemma iT_Div_cut_less2: "
0 < k ==> (I \<oslash> k) \<down>< (t div k) = I \<down>< (t - t mod k) \<oslash> k"
by (frule iT_Div_cut_less[of k I "t div k"], simp add: div_mult_cancel)
lemma iT_Div_cut_ge2: "
0 < k ==> (I \<oslash> k) \<down>≥ (t div k) = I \<down>≥ (t - t mod k) \<oslash> k"
by (frule iT_Div_cut_ge[of k I "t div k"], simp add: div_mult_cancel)
lemma iT_Div_cut_greater2: "
0 < k ==> (I \<oslash> k) \<down>> (t div k) = I \<down>> (t - t mod k + (k - Suc 0)) \<oslash> k"
by (frule iT_Div_cut_greater[of k I "t div k"], simp add: div_mult_cancel)
subsection {* @{text inext} and @{text iprev} with interval operators *}
lemma iT_Plus_inext: "inext (n + k) (I ⊕ k) = (inext n I) + k"
by (unfold iT_Plus_def, rule inext_image2[OF add_right_strict_mono])
lemma iT_Plus_iprev: "iprev (n + k) (I ⊕ k) = (iprev n I) + k"
by (unfold iT_Plus_def, rule iprev_image2[OF add_right_strict_mono])
lemma iT_Plus_inext2: "k ≤ n ==> inext n (I ⊕ k) = (inext (n - k) I) + k"
by (insert iT_Plus_inext[of "n - k" k I], simp)
lemma iT_Plus_prev2: "k ≤ n ==> iprev n (I ⊕ k) = (iprev (n - k) I) + k"
by (insert iT_Plus_iprev[of "n - k" k I], simp)
lemma iT_Mult_inext: "inext (n * k) (I ⊗ k) = (inext n I) * k"
apply (case_tac "I = {}")
apply (simp add: iT_Mult_empty inext_empty)
apply (case_tac "k = 0")
apply (simp add: iT_Mult_0 iTILL_0 inext_singleton)
apply (simp add: iT_Mult_def inext_image2[OF mult_right_strict_mono])
done
lemma iT_Mult_iprev: "iprev (n * k) (I ⊗ k) = (iprev n I) * k"
apply (case_tac "I = {}")
apply (simp add: iT_Mult_empty iprev_empty)
apply (case_tac "k = 0")
apply (simp add: iT_Mult_0 iTILL_0 iprev_singleton)
apply (simp add: iT_Mult_def iprev_image2[OF mult_right_strict_mono])
done
lemma iT_Mult_inext2_if: "
inext n (I ⊗ k) = (if n mod k = 0 then (inext (n div k) I) * k else n)"
apply (case_tac "I = {}")
apply (simp add: iT_Mult_empty inext_empty div_mult_cancel)
apply (case_tac "k = 0")
apply (simp add: iT_Mult_0 iTILL_0 inext_singleton)
apply (case_tac "n mod k = 0")
apply (clarsimp simp: mult_commute[of k] iT_Mult_inext)
apply (simp add: not_in_inext_fix iT_Mult_mem_iff)
done
lemma iT_Mult_iprev2_if: "
iprev n (I ⊗ k) = (if n mod k = 0 then (iprev (n div k) I) * k else n)"
apply (case_tac "I = {}")
apply (simp add: iT_Mult_empty iprev_empty div_mult_cancel)
apply (case_tac "k = 0")
apply (simp add: iT_Mult_0 iTILL_0 iprev_singleton)
apply (case_tac "n mod k = 0")
apply (clarsimp simp: mult_commute[of k] iT_Mult_iprev)
apply (simp add: not_in_iprev_fix iT_Mult_mem_iff)
done
corollary iT_Mult_inext2: "
n mod k = 0 ==> inext n (I ⊗ k) = (inext (n div k) I) * k"
by (simp add: iT_Mult_inext2_if)
corollary iT_Mult_iprev2: "
n mod k = 0 ==> iprev n (I ⊗ k) = (iprev (n div k) I) * k"
by (simp add: iT_Mult_iprev2_if)
lemma iT_Plus_neg_inext: "
k ≤ n ==> inext (n - k) (I ⊕- k) = inext n I - k"
apply (case_tac "I = {}")
apply (simp add: iT_Plus_neg_empty inext_empty)
apply (case_tac "n ∈ I")
apply (simp add: iT_Plus_neg_image_conv)
thm subst[OF inext_cut_ge_conv]
apply (rule subst[OF inext_cut_ge_conv, of k], simp)
thm inext_image
apply (rule inext_image)
apply (simp add: cut_ge_mem_iff)
apply (subst cut_ge_Int_conv)
thm strict_mono_on_subset[OF _ Int_lower2]
apply (rule strict_mono_on_subset[OF _ Int_lower2])
thm sub_left_strict_mono_on
apply (rule sub_left_strict_mono_on)
apply (subgoal_tac "n - k ∉ I ⊕- k")
prefer 2
apply (simp add: iT_Plus_neg_mem_iff)
apply (simp add: not_in_inext_fix)
done
lemma iT_Plus_neg_iprev: "
iprev (n - k) (I ⊕- k) = iprev n (I \<down>≥ k) - k"
apply (case_tac "I = {}")
apply (simp add: iT_Plus_neg_empty i_cut_empty iprev_empty)
apply (case_tac "n < k")
apply (simp add: iprev_le_iMin)
apply (simp add: order_trans[OF iprev_mono])
apply (simp add: linorder_not_less)
apply (case_tac "n ∈ I")
thm iT_Plus_neg_mem_iff2[THEN iffD2]
apply (frule iT_Plus_neg_mem_iff2[THEN iffD2, of _ _ I], assumption)
apply (simp add: iT_Plus_neg_image_conv)
apply (rule iprev_image)
apply (simp add: cut_ge_mem_iff)
apply (subst cut_ge_Int_conv)
thm strict_mono_on_subset[OF _ Int_lower2]
apply (rule strict_mono_on_subset[OF _ Int_lower2])
thm sub_left_strict_mono_on
apply (rule sub_left_strict_mono_on)
apply (frule cut_ge_not_in_imp[of _ _ k])
apply (subgoal_tac "n - k ∉ I ⊕- k")
prefer 2
apply (simp add: iT_Plus_neg_mem_iff)
apply (simp add: not_in_iprev_fix)
done
corollary iT_Plus_neg_inext2: "inext n (I ⊕- k) = inext (n + k) I - k"
by (insert iT_Plus_neg_inext[of k "n + k" I, OF le_add2], simp)
corollary iT_Plus_neg_iprev2: "iprev n (I ⊕- k) = iprev (n + k) (I \<down>≥ k) - k"
by (insert iT_Plus_neg_iprev[of "n + k" k I], simp)
lemma iT_Minus_inext: "
[| k \<ominus> I ≠ {}; n ≤ k |] ==> inext (k - n) (k \<ominus> I) = k - iprev n I"
apply (subgoal_tac "iMin I ≤ k")
prefer 2
apply (simp add: iT_Minus_empty_iff)
apply (subgoal_tac "I \<down>≤ k ≠ {}")
prefer 2
apply (simp add: iT_Minus_empty_iff cut_le_Min_not_empty)
apply (case_tac "n ∈ I")
thm iT_Minus_imirror_conv
apply (simp add: iT_Minus_imirror_conv)
apply (simp add: iT_Plus_neg_inext2)
apply (subgoal_tac "n ≤ iMin I + Max (I \<down>≤ k)")
prefer 2
apply (rule trans_le_add2)
apply (rule Max_ge[OF nat_cut_le_finite])
apply (simp add: cut_le_mem_iff)
thm iT_Plus_inext
apply (simp add: diff_add_assoc del: add_diff_assoc)
apply (subst add_commute[of k], subst iT_Plus_inext)
apply (simp add: cut_le_Min_eq[of I, symmetric])
apply (fold nat_mirror_def mirror_elem_def)
apply (simp add: inext_imirror_iprev_conv[OF nat_cut_le_finite])
apply (simp add: iprev_cut_le_conv)
apply (simp add: mirror_elem_def nat_mirror_def)
thm iprev_mono[THEN order_trans, of n "iMin (I \<down>≤ k) + Max (I \<down>≤ k)" I]
apply (frule iprev_mono[THEN order_trans, of n "iMin (I \<down>≤ k) + Max (I \<down>≤ k)" I])
apply simp
apply (subgoal_tac "k - n ∉ k \<ominus> I")
prefer 2
apply (simp add: iT_Minus_mem_iff)
apply (simp add: not_in_inext_fix not_in_iprev_fix)
done
corollary iT_Minus_inext2: "
[| k \<ominus> I ≠ {}; n ≤ k |] ==> inext n (k \<ominus> I) = k - iprev (k - n) I"
by (insert iT_Minus_inext[of k I "k - n"], simp)
lemma iT_Minus_iprev: "
[| k \<ominus> I ≠ {}; n ≤ k |] ==> iprev (k - n) (k \<ominus> I) = k - inext n (I \<down>≤ k)"
apply (subgoal_tac "I \<down>≤ k ≠ {}")
prefer 2
apply (simp add: iT_Minus_empty_iff cut_le_Min_not_empty)
apply (subst iT_Minus_cut_eq[OF le_refl, of _ I, symmetric])
apply (insert iT_Minus_inext2[of k "k \<ominus> (I \<down>≤ k)" n])
apply (simp add: iT_Minus_Minus_cut_eq)
apply (rule diff_diff_cancel[symmetric])
apply (rule order_trans[OF iprev_mono])
apply simp
done
lemma iT_Minus_iprev2: "
[| k \<ominus> I ≠ {}; n ≤ k |] ==> iprev n (k \<ominus> I) = k - inext (k - n) (I \<down>≤ k)"
by (insert iT_Minus_iprev[of k I "k - n"], simp)
lemma iT_Plus_inext_nth: "I ≠ {} ==> (I ⊕ k) -> n = (I -> n) + k"
apply (induct n)
apply (simp add: iT_Plus_Min)
apply (simp add: iT_Plus_inext)
done
lemma iT_Plus_iprev_nth: "[| finite I; I ≠ {} |] ==> (I ⊕ k) \<leftarrow> n = (I \<leftarrow> n) + k"
apply (induct n)
apply (simp add: iT_Plus_Max)
apply (simp add: iT_Plus_iprev)
done
lemma iT_Mult_inext_nth: "I ≠ {} ==> (I ⊗ k) -> n = (I -> n) * k"
apply (induct n)
apply (simp add: iT_Mult_Min)
apply (simp add: iT_Mult_inext)
done
lemma iT_Mult_iprev_nth: "[| finite I; I ≠ {} |] ==> (I ⊗ k) \<leftarrow> n = (I \<leftarrow> n) * k"
apply (induct n)
apply (simp add: iT_Mult_Max)
apply (simp add: iT_Mult_iprev)
done
lemma iT_Plus_neg_inext_nth: "
I ⊕- k ≠ {} ==> (I ⊕- k) -> n = (I \<down>≥ k -> n) - k"
apply (subgoal_tac "I \<down>≥ k ≠ {}")
prefer 2
apply (simp add: cut_ge_not_empty_iff iT_Plus_neg_not_empty_iff)
apply (induct n)
apply (simp add: iT_Plus_neg_Min)
thm iT_Plus_neg_cut_eq[of k k I]
apply (simp add: iT_Plus_neg_cut_eq[of k k I, symmetric])
apply (rule iT_Plus_neg_inext)
apply (rule cut_ge_bound[of _ I])
apply (simp add: inext_nth_closed)
done
lemma iT_Plus_neg_iprev_nth: "
[| finite I; I ⊕- k ≠ {} |] ==> (I ⊕- k) \<leftarrow> n = (I \<down>≥ k \<leftarrow> n) - k"
apply (subgoal_tac "I \<down>≥ k ≠ {}")
prefer 2
apply (simp add: cut_ge_not_empty_iff iT_Plus_neg_not_empty_iff)
apply (induct n)
apply (simp add: iT_Plus_neg_Max cut_ge_Max_eq)
apply (simp add: iT_Plus_neg_iprev)
done
lemma iT_Minus_inext_nth: "
k \<ominus> I ≠ {} ==> (k \<ominus> I) -> n = k - ((I \<down>≤ k) \<leftarrow> n)"
apply (subgoal_tac "I \<down>≤ k ≠ {} ∧ I ≠ {} ∧ iMin I ≤ k")
prefer 2
apply (simp add: iT_Minus_empty_iff cut_le_Min_not_empty)
apply (elim conjE)
apply (induct n)
apply(simp add: iT_Minus_Min)
apply (simp add: iT_Minus_cut_eq[OF order_refl, of _ I, symmetric])
apply (rule iT_Minus_inext)
apply simp
by (rule cut_le_bound, rule iprev_nth_closed[OF nat_cut_le_finite])
lemma iT_Minus_iprev_nth: "
k \<ominus> I ≠ {} ==> (k \<ominus> I) \<leftarrow> n = k - ((I \<down>≤ k) -> n)"
apply (subgoal_tac "I \<down>≤ k ≠ {} ∧ I ≠ {} ∧ iMin I ≤ k")
prefer 2
apply (simp add: iT_Minus_empty_iff cut_le_Min_not_empty)
apply (elim conjE)
apply (induct n)
apply(simp add: iT_Minus_Max cut_le_Min_eq)
apply simp
apply (rule iT_Minus_iprev)
apply simp
by (rule cut_le_bound, rule inext_nth_closed)
lemma iT_Div_ge_inext_nth: "
[| I ≠ {}; ∀x∈I. ∀y∈I. x < y --> x + k ≤ y |] ==>
(I \<oslash> k) -> n = (I -> n) div k"
apply (case_tac "k = 0")
apply (simp add: iT_Div_0 iTILL_0 inext_nth_singleton)
apply (simp add: iT_Div_def)
by (rule inext_nth_image[OF _ div_right_strict_mono_on])
lemma iT_Div_mod_inext_nth: "
[| I ≠ {}; ∀x∈I. ∀y∈I. x mod k = y mod k |] ==>
(I \<oslash> k) -> n = (I -> n) div k"
apply (case_tac "k = 0")
apply (simp add: iT_Div_0 iTILL_0 inext_nth_singleton)
apply (simp add: iT_Div_def)
by (rule inext_nth_image[OF _ mod_eq_div_right_strict_mono_on])
lemma iT_Div_ge_iprev_nth: "
[| finite I; I ≠ {}; ∀x∈I. ∀y∈I. x < y --> x + k ≤ y |] ==>
(I \<oslash> k) \<leftarrow> n = (I \<leftarrow> n) div k"
apply (case_tac "k = 0")
apply (simp add: iT_Div_0 iTILL_0 iprev_nth_singleton)
apply (simp add: iT_Div_def)
by (rule iprev_nth_image[OF _ _ div_right_strict_mono_on])
lemma iT_Div_mod_iprev_nth: "
[| finite I; I ≠ {}; ∀x∈I. ∀y∈I. x mod k = y mod k |] ==>
(I \<oslash> k) \<leftarrow> n = (I \<leftarrow> n) div k"
apply (case_tac "k = 0")
apply (simp add: iT_Div_0 iTILL_0 iprev_nth_singleton)
apply (simp add: iT_Div_def)
by (rule iprev_nth_image[OF _ _ mod_eq_div_right_strict_mono_on])
subsection {* Cardinality of intervals with interval operators*}
lemma iT_Plus_card: "card (I ⊕ k) = card I"
apply (unfold iT_Plus_def)
apply (rule card_image)
apply (rule inj_imp_inj_on)
apply (rule add_right_inj)
done
lemma iT_Mult_card: "0 < k ==> card (I ⊗ k) = card I"
apply (unfold iT_Mult_def)
apply (rule card_image)
apply (rule inj_imp_inj_on)
apply (rule mult_right_inj)
apply assumption
done
lemma iT_Plus_neg_card: "card (I ⊕- k) = card (I \<down>≥ k)"
apply (simp add: iT_Plus_neg_image_conv)
apply (rule card_image)
apply (subst cut_ge_Int_conv)
thm Int_lower2
thm subset_inj_on[OF _ Int_lower2]
apply (rule subset_inj_on[OF _ Int_lower2])
thm sub_left_inj_on
apply (rule sub_left_inj_on)
done
lemma iT_Plus_neg_card_le: "card (I ⊕- k) ≤ card I"
apply (simp add: iT_Plus_neg_card)
apply (case_tac "finite I")
apply (rule cut_ge_card, assumption)
thm nat_cut_ge_finite_iff card_infinite
apply (simp add: nat_cut_ge_finite_iff)
done
lemma iT_Minus_card: "card (k \<ominus> I) = card (I \<down>≤ k)"
apply (simp add: iT_Minus_image_conv)
apply (rule card_image)
apply (subst cut_le_Int_conv)
thm subset_inj_on[OF _ Int_lower2]
apply (rule subset_inj_on[OF _ Int_lower2])
apply (rule sub_right_inj_on)
done
lemma iT_Minus_card_le: "finite I ==> card (k \<ominus> I) ≤ card I"
by (subst iT_Minus_card, rule cut_le_card)
lemma iT_Div_0_card_if: "
card (I \<oslash> 0) = (if I ={} then 0 else Suc 0)"
by (fastsimp simp: iT_Div_empty iT_Div_0 iTILL_0)
lemma Int_empty_setsum:"
(∑k≤(n::nat). if {} ∩ (I k) = {} then 0 else Suc 0) = 0"
apply (rule setsum_eq_0_iff[THEN iffD2])
apply (rule finite_atMost)
apply simp
done
lemma iT_Div_mod_partition_card:"
card (I ∩ [n * d…,d - Suc 0] \<oslash> d) =
(if I ∩ [n * d…,d - Suc 0] = {} then 0 else Suc 0)"
apply (case_tac "d = 0")
apply (simp add: iIN_0 iTILL_0 iT_Div_0_if)
apply (split split_if, rule conjI)
apply (simp add: iT_Div_empty)
apply clarsimp
apply (subgoal_tac "I ∩ [n * d…,d - Suc 0] \<oslash> d = {n}", simp)
apply (rule set_eqI)
thm iT_Div_mem_iff
apply (simp add: iT_Div_mem_iff Bex_def iIN_iff)
apply (rule iffI)
thm le_less_imp_div
apply (clarsimp simp: le_less_imp_div)
apply (drule ex_in_conv[THEN iffD2], clarsimp simp: iIN_iff, rename_tac x')
apply (rule_tac x=x' in exI)
apply (simp add: le_less_imp_div)
done
thm iT_Div_mem_iff_Int
lemma iT_Div_conv_count: "
0 < d ==> I \<oslash> d = {k. I ∩ [k * d…,d - Suc 0] ≠ {}}"
apply (case_tac "I = {}")
apply (simp add: iT_Div_empty)
apply (rule set_eqI)
thm iT_Div_mem_iff_Int
apply (simp add: iT_Div_mem_iff_Int)
done
lemma iT_Div_conv_count2: "
[| 0 < d; finite I; Max I div d ≤ n |] ==>
I \<oslash> d = {k. k ≤ n ∧ I ∩ [k * d…,d - Suc 0] ≠ {}}"
apply (simp add: iT_Div_conv_count)
apply (rule set_eqI, simp)
apply (rule iffI)
apply simp
apply (rule ccontr)
apply (drule ex_in_conv[THEN iffD2], clarify, rename_tac x')
apply (clarsimp simp: linorder_not_le iIN_iff)
apply (drule order_le_less_trans, simp)
thm div_less_conv
apply (drule div_less_conv[THEN iffD1, of _ "Max I"], simp)
apply (drule_tac x=x' in Max_ge, simp)
apply simp+
done
lemma mod_partition_count_Suc: "
{k. k ≤ Suc n ∧ I ∩ [k * d…,d - Suc 0] ≠ {}} =
{k. k ≤ n ∧ I ∩ [k * d…,d - Suc 0] ≠ {}} ∪
(if I ∩ [Suc n * d…,d - Suc 0] ≠ {} then {Suc n} else {})"
apply (rule set_eqI, rename_tac x)
apply (simp add: le_less[of _ "Suc n"] less_Suc_eq_le)
apply (simp add: conj_disj_distribR)
apply (intro conjI impI)
apply fastsimp
apply (rule iffI, clarsimp+)
done
lemma iT_Div_card: "
!!I.[| 0 < d; finite I; Max I div d ≤ n|] ==>
card (I \<oslash> d) = (∑k≤n.
if I ∩ [k * d…,d - Suc 0] = {} then 0 else Suc 0)"
apply (case_tac "I = {}")
apply (simp add: iT_Div_empty)
thm iT_Div_conv_count2
apply (simp add: iT_Div_conv_count2)
apply (induct n)
apply (simp add: div_eq_0_conv iIN_0_iTILL_conv)
apply (subgoal_tac "I ∩ […d - Suc 0] ≠ {}")
prefer 2
apply (simp add: ex_in_conv[symmetric], fastsimp)
apply (simp add: card_1_singleton_conv)
apply (rule_tac x=0 in exI)
apply (rule set_eqI)
apply (simp add: ex_in_conv[symmetric], fastsimp)
apply simp
thm mod_partition_count_Suc
apply (simp add: mod_partition_count_Suc)
apply (drule_tac x="I ∩ […n * d + d - Suc 0]" in meta_spec)
apply simp
apply (case_tac "I ∩ […n * d + d - Suc 0] = {}")
apply simp
apply (subgoal_tac "{k. k ≤ n ∧ I ∩ [k * d…,d - Suc 0] ≠ {}} = {}", simp)
apply (clarsimp, rename_tac x)
apply (subgoal_tac "I ∩ [x * d…,d - Suc 0] ⊆ I ∩ […n * d + d - Suc 0]", simp)
apply (rule Int_mono[OF order_refl])
apply (simp add: iIN_iTILL_subset_conv)
apply (simp add: diff_le_mono)
find_theorems "_ div _ <= _" name: conv
apply (subgoal_tac "Max (I ∩ […n * d + d - Suc 0]) div d ≤ n")
prefer 2
thm div_le_conv
apply (simp add: div_le_conv add_commute[of d] iTILL_iff)
apply (subgoal_tac "!!k. k ≤ n ==> […n * d + d - Suc 0] ∩ [k * d…,d - Suc 0] = [k * d…,d - Suc 0]")
prefer 2
apply (subst Int_commute)
thm cut_le_Int_conv
apply (simp add: iTILL_def cut_le_Int_conv[symmetric])
apply (rule cut_le_Max_all[OF iIN_finite])
apply (simp add: iIN_Max diff_le_mono)
apply (simp add: Int_assoc)
apply (subgoal_tac "
{k. k ≤ n ∧ I ∩ ([…n * d + d - Suc 0] ∩ [k * d…,d - Suc 0]) ≠ {}} =
{k. k ≤ n ∧ I ∩ [k * d…,d - Suc 0] ≠ {}}")
prefer 2
apply (rule set_eqI, rename_tac x)
apply simp
apply (rule conj_cong, simp)
apply simp
apply simp
done
thm iT_Div_card
thm iT_Div_card[OF _ _ le_refl, of d i]
corollary iT_Div_card_Suc: "
!!I.[| 0 < d; finite I; Max I div d ≤ n|] ==>
card (I \<oslash> d) = (∑k<Suc n.
if I ∩ [k * d…,d - Suc 0] = {} then 0 else Suc 0)"
by (simp add: lessThan_Suc_atMost iT_Div_card)
corollary iT_Div_Max_card: "[| 0 < d; finite I |] ==>
card (I \<oslash> d) = (∑k≤Max I div d.
if I ∩ [k * d…,d - Suc 0] = {} then 0 else Suc 0)"
by (simp add: iT_Div_card)
lemma iT_Div_card_le: "0 < k ==> card (I \<oslash> k) ≤ card I"
apply (case_tac "finite I")
apply (simp add: iT_Div_def card_image_le)
apply (simp add: iT_Div_finite_iff)
done
thm iT_Div_def
lemma iT_Div_card_inj_on: "
inj_on (λn. n div k) I ==> card (I \<oslash> k) = card I"
by (unfold iT_Div_def, rule card_image)
(*
lemma "let I=[…19] in
d ∈ {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21} -->
card I div d ≤ card (I \<oslash> d)"
apply (simp add: Let_def iTILL_card iTILL_div)
done
lemma "let I=[…19] in
d ∈ {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21} -->
card I div d + (if card I mod d ≠ 0 then 1 else 0) ≤ card (I \<oslash> d)"
apply (simp add: Let_def iTILL_card iTILL_div)
done
lemma "let I=[5…,19] in
d ∈ {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21} -->
card I div d + (if card I mod d ≠ 0 then 1 else 0) ≤ card (I \<oslash> d)"
apply (simp add: Let_def iIN_card iIN_div)
done
*)
(* ToDo: to be moved to Util_Div *)
thm mod_Suc
lemma mod_Suc': "
0 < n ==> Suc m mod n = (if m mod n < n - Suc 0 then Suc (m mod n) else 0)"
apply (simp add: mod_Suc)
apply (intro conjI impI)
apply simp
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
done
lemma div_Suc: "
0 < n ==> Suc m div n = (if Suc (m mod n) = n then Suc (m div n) else m div n)"
apply (drule Suc_leI, drule le_imp_less_or_eq)
apply (case_tac "n = Suc 0", simp)
apply (split split_if, intro conjI impI)
apply (rule_tac t="Suc m" and s="m + 1" in subst, simp)
apply (subst div_add1_eq2, simp+)
thm le_neq_trans[OF mod_less_divisor[THEN Suc_leI]]
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
apply (rule_tac t="Suc m" and s="m + 1" in subst, simp)
apply (subst div_add1_eq1, simp+)
done
lemma div_Suc': "
0 < n ==> Suc m div n = (if m mod n < n - Suc 0 then m div n else Suc (m div n))"
apply (simp add: div_Suc)
apply (intro conjI impI)
apply simp
apply (insert le_neq_trans[OF mod_less_divisor[THEN Suc_leI, of n m]], simp)
done
lemma iT_Div_card_ge_aux: "
!!I. [| 0 < d; finite I; Max I div d ≤ n |] ==>
card I div d + (if card I mod d = 0 then 0 else Suc 0) ≤ card (I \<oslash> d)"
apply (induct n)
apply (case_tac "I = {}", simp)
thm div_le_conv[THEN iffD1]
apply (frule_tac m=d and n="Max I" and k=0 in div_le_conv[THEN iffD1, rule_format], assumption)
apply (simp del: Max_le_iff)
apply (subgoal_tac "I \<oslash> d = {0}")
prefer 2
apply (rule set_eqI)
apply (simp add: iT_Div_mem_iff)
apply (rule iffI)
apply (fastsimp simp: div_eq_0_conv')
apply fastsimp
apply (simp add: iT_Div_singleton card_singleton del: Max_le_iff)
apply (drule Suc_le_mono[THEN iffD2, of _ "d - Suc 0"])
thm nat_card_le_Max
thm order_trans[OF nat_card_le_Max]
apply (drule order_trans[OF nat_card_le_Max])
apply (simp, intro conjI impI)
thm div_le_mono[of _ _ d]
apply (drule div_le_mono[of _ d d])
apply simp
apply (subgoal_tac "card I ≠ d", simp)
apply clarsimp
apply (drule order_le_less[THEN iffD1], erule disjE)
apply simp
thm subst[where t=I and s="I ∩ […n * d + d - Suc 0] ∪ I ∩ [Suc n * d…,d - Suc 0]"]
apply (rule_tac t=I and s="I ∩ […n * d + d - Suc 0] ∪ I ∩ [Suc n * d…,d - Suc 0]" in subst)
apply (simp add: Int_Un_distrib[symmetric] add_commute[of d])
apply (subst iIN_0_iTILL_conv[symmetric])
apply (simp add: iIN_union)
apply (rule Int_absorb2)
apply (simp add: iIN_0_iTILL_conv iTILL_def)
apply (case_tac "I = {}", simp)
thm subset_atMost_Max_le_conv
thm le_less_div_conv
apply (simp add: subset_atMost_Max_le_conv le_less_div_conv[symmetric] less_eq_le_pred[symmetric] add_commute[of d])
thm card_Un_disjoint
apply (cut_tac A="I ∩ […n * d + d - Suc 0]" and B="I ∩ [Suc n * d…,d - Suc 0]" in card_Un_disjoint)
apply simp
apply simp
apply (clarsimp simp: disjoint_iff_in_not_in1 iT_iff)
apply (case_tac "I ∩ […n * d + d - Suc 0] = {}")
thm iT_Div_mod_partition_card
apply (simp add: iT_Div_mod_partition_card del: mult_Suc)
apply (intro conjI impI)
apply (rule div_le_conv[THEN iffD2], assumption)
apply simp
thm Int_card2[OF iIN_finite]
thm order_trans[OF Int_card2[OF iIN_finite]]
apply (rule order_trans[OF Int_card2[OF iIN_finite]])
apply (simp add: iIN_card)
thm Int_card2[OF iIN_finite, rule_format]
apply (cut_tac A=I and n="Suc n * d" and d="d - Suc 0" in Int_card2[OF iIN_finite, rule_format])
apply (simp add: iIN_card)
apply (drule order_le_less[THEN iffD1], erule disjE)
apply simp
apply simp
apply (subgoal_tac "Max (I ∩ […n * d + d - Suc 0]) div d ≤ n")
prefer 2
apply (rule div_le_conv[THEN iffD2], assumption)
thm Max_Int_le2[OF _ iTILL_finite]
thm order_trans[OF Max_Int_le2[OF _ iTILL_finite]]
apply (rule order_trans[OF Max_Int_le2[OF _ iTILL_finite]], assumption)
apply (simp add: iTILL_Max)
apply (simp only: iT_Div_Un)
thm card_Un_disjoint
apply (cut_tac A="I ∩ […n * d + d - Suc 0] \<oslash> d" and B="I ∩ [Suc n * d…,d - Suc 0] \<oslash> d" in card_Un_disjoint)
apply (simp add: iT_Div_finite_iff)
apply (simp add: iT_Div_finite_iff)
thm mod_partition_iT_Div_Int_one_segment
apply (subst iIN_0_iTILL_conv[symmetric])
thm mod_partition_iT_Div_Int_one_segment
apply (subst mod_partition_iT_Div_Int_one_segment, simp)
thm mod_partition_iT_Div_Int2
apply (cut_tac n=0 and d="n * d+d" and k=d and A=I in mod_partition_iT_Div_Int2, simp+)
thm disjoint_iff_in_not_in1
apply (rule disjoint_iff_in_not_in1[THEN iffD2])
apply clarsimp
thm iIN_div_mod_eq_0
apply (simp add: iIN_div_mod_eq_0)
apply (simp add: mod_0_imp_sub_1_div_conv iIN_0_iTILL_conv iIN_0 iTILL_iff)
thm iT_Div_mod_partition_card
apply (simp only: iT_Div_mod_partition_card)
apply (subgoal_tac "finite (I ∩ […n * d + d - Suc 0])")
prefer 2
apply simp
apply simp
apply (intro conjI impI)
thm add_le_divisor_imp_le_Suc_div
apply (rule add_le_divisor_imp_le_Suc_div)
apply (rule add_leD1, blast)
thm Int_card2[OF iIN_finite, THEN le_trans]
apply (rule Int_card2[OF iIN_finite, THEN le_trans])
apply (simp add: iIN_card)
apply (cut_tac A=I and n="Suc n * d" and d="d - Suc 0" in Int_card2[OF iIN_finite, rule_format])
apply (simp add: iIN_card)
thm order_trans[where x="card I div d + (if card I mod d ≠ 0 then Suc 0 else 0)"]
apply (rule_tac y="let I=I ∩ […n * d + d - Suc 0] in
card I div d + (if card I mod d = 0 then 0 else Suc 0)" in order_trans)
prefer 2
apply (simp add: Let_def)
apply (unfold Let_def)
apply (split split_if, intro conjI impI)
apply (subgoal_tac "card (I ∩ [Suc n * d…,d - Suc 0]) ≠ d")
prefer 2
apply (rule ccontr, simp)
thm div_add1_eq1_mod_0_left
apply (simp add: div_add1_eq1_mod_0_left)
thm add_le_divisor_imp_le_Suc_div
apply (simp add: add_le_divisor_imp_le_Suc_div)
done
lemma iT_Div_card_ge: "
card I div d + (if card I mod d = 0 then 0 else Suc 0) ≤ card (I \<oslash> d)"
apply (case_tac "I = {}", simp)
apply (case_tac "finite I")
prefer 2
apply simp
apply (case_tac "d = 0")
apply (simp add: iT_Div_0 iTILL_0)
thm iT_Div_card_ge_aux[OF _ _ order_refl]
apply (simp add: iT_Div_card_ge_aux[OF _ _ order_refl])
done
corollary iT_Div_card_ge_div: "card I div d ≤ card (I \<oslash> d)"
by (rule iT_Div_card_ge[THEN add_leD1])
text {*
There is no better lower bound function @{term f} for @{term "(i \<oslash> d)"}
with @{term "card i"} and @{term d} as arguments. *}
lemma iT_Div_card_ge__is_maximal_lower_bound: "
∀I d. card I div d + (if card I mod d = 0 then 0 else Suc 0) ≤ f (card I) d ∧
f (card I) d ≤ card (I \<oslash> d) ==>
f (card (I::nat set)) d = card I div d + (if card I mod d = 0 then 0 else Suc 0)"
apply (case_tac "I = {}")
apply (erule_tac x=I in allE, erule_tac x=d in allE)
apply (simp add: iT_Div_empty)
apply (case_tac "d = 0")
apply (frule_tac x="{}" in spec, erule_tac x=I in allE)
apply (erule_tac x=d in allE, erule_tac x=d in allE)
apply (clarsimp simp: iT_Div_0 iTILL_card iT_Div_empty)
apply (rule order_antisym)
prefer 2
apply simp
apply (case_tac "finite I")
prefer 2
apply (erule_tac x=I in allE, erule_tac x=d in allE)
apply (simp add: iT_Div_finite_iff)
apply (erule_tac x="[…card I - Suc 0]" in allE, erule_tac x=d in allE, elim conjE)
apply (frule not_empty_card_gr0_conv[THEN iffD1], assumption)
thm iTILL_div iTILL_card
apply (simp add: iTILL_card iTILL_div)
apply (intro conjI impI)
apply (simp add: mod_0_imp_sub_1_div_conv)
apply (subgoal_tac "d ≤ card I")
prefer 2
apply clarsimp
apply (drule div_le_mono[of d _ d])
apply simp
apply (case_tac "d = Suc 0", simp)
thm div_diff1_eq1[of "Suc 0" d "card I"]
apply (simp add: div_diff1_eq1)
done
thm iT_Div_card_ge__is_maximal_lower_bound[rule_format]
thm iT_Plus_card
lemma iT_Plus_icard: "icard (I ⊕ k) = icard I"
by (simp add: iT_Plus_def icard_image)
thm iT_Mult_card
lemma iT_Mult_icard: "0 < k ==> icard (I ⊗ k) = icard I"
apply (unfold iT_Mult_def)
apply (rule icard_image)
apply (rule inj_imp_inj_on)
apply (simp add: mult_right_inj)
done
thm iT_Plus_neg_card
lemma iT_Plus_neg_icard: "icard (I ⊕- k) = icard (I \<down>≥ k)"
apply (case_tac "finite I")
thm iT_Plus_neg_finite_iff cut_ge_finite
apply (simp add: iT_Plus_neg_finite_iff cut_ge_finite icard_finite iT_Plus_neg_card)
apply (simp add: iT_Plus_neg_finite_iff nat_cut_ge_finite_iff)
done
thm iT_Plus_neg_card_le
lemma iT_Plus_neg_icard_le: "icard (I ⊕- k) ≤ icard I"
apply (case_tac "finite I")
apply (simp add: iT_Plus_neg_finite_iff icard_finite iT_Plus_neg_card_le)
apply simp
done
thm iT_Minus_card
lemma iT_Minus_icard: "icard (k \<ominus> I) = icard (I \<down>≤ k)"
by (simp add: icard_finite iT_Minus_finite nat_cut_le_finite iT_Minus_card)
thm iT_Minus_card_le
lemma iT_Minus_icard_le: "icard (k \<ominus> I) ≤ icard I"
apply (case_tac "finite I")
apply (simp add: icard_finite iT_Minus_finite iT_Minus_card_le)
apply simp
done
thm iT_Div_0_card_if
lemma iT_Div_0_icard_if: "icard (I \<oslash> 0) = Fin (if I = {} then 0 else Suc 0)"
thm iT_Div_0_finite
by (simp add: icard_finite iT_Div_0_finite iT_Div_0_card_if)
thm iT_Div_mod_partition_card
lemma iT_Div_mod_partition_icard: "
icard (I ∩ [n * d…,d - Suc 0] \<oslash> d) =
Fin (if I ∩ [n * d…,d - Suc 0] = {} then 0 else Suc 0)"
apply (subgoal_tac "finite (I ∩ [n * d…,d - Suc 0] \<oslash> d)")
prefer 2
apply (case_tac "d = 0", simp add: iT_Div_0_finite)
apply (simp add: iT_Div_finite_iff iIN_finite)
apply (simp add: icard_finite iT_Div_mod_partition_card)
done
thm iT_Div_card
lemma iT_Div_icard: "
[| 0 < d; finite I ==> Max I div d ≤ n|] ==>
icard (I \<oslash> d) =
(if finite I then Fin (∑k≤n. if I ∩ [k * d…,d - Suc 0] = {} then 0 else Suc 0) else ∞)"
by (simp add: icard_finite iT_Div_finite_iff iT_Div_card)
thm iT_Div_Max_card
corollary iT_Div_Max_icard: "0 < d ==>
icard (I \<oslash> d) = (if finite I
then Fin (∑k≤Max I div d. if I ∩ [k * d…,d - Suc 0] = {} then 0 else Suc 0) else ∞)"
by (simp add: iT_Div_icard)
thm iT_Div_card_le
lemma iT_Div_icard_le: "0 < k ==> icard (I \<oslash> k) ≤ icard I"
apply (case_tac "finite I")
apply (simp add: iT_Div_finite_iff icard_finite iT_Div_card_le)
apply simp
done
thm iT_Div_card_inj_on
lemma iT_Div_icard_inj_on: "inj_on (λn. n div k) I ==> icard (I \<oslash> k) = icard I"
by (simp add: iT_Div_def icard_image)
thm iT_Div_card_ge
lemma iT_Div_icard_ge: "icard I div (Fin d) + Fin (if icard I mod (Fin d) = 0 then 0 else Suc 0) ≤ icard (I \<oslash> d)"
apply (case_tac "d = 0")
apply (simp add: icard_finite iT_Div_0_finite)
apply (case_tac "icard I")
apply (fastsimp simp: iT_Div_0_card_if)
apply (simp add: iT_Div_0_card_if icard_infinite_conv infinite_imp_nonempty)
apply (case_tac "finite I")
apply (simp add: iT_Div_finite_iff icard_finite iT_Div_card_ge)
apply (simp add: iT_Div_finite_iff)
done
thm iT_Div_card_ge_div
corollary iT_Div_icard_ge_div: "icard I div (Fin d) ≤ icard (I \<oslash> d)"
by (rule iT_Div_icard_ge[THEN iadd_ileD1])
thm iT_Div_card_ge__is_maximal_lower_bound
lemma iT_Div_icard_ge__is_maximal_lower_bound: "
∀I d. icard I div (Fin d) + Fin (if icard I mod (Fin d) = 0 then 0 else Suc 0)
≤ f (icard I) d ∧
f (icard I) d ≤ icard (I \<oslash> d) ==>
f (icard (I::nat set)) d =
icard I div (Fin d) + Fin (if icard I mod (Fin d) = 0 then 0 else Suc 0)"
apply (case_tac "d = 0")
apply (drule_tac x=I in spec, drule_tac x=d in spec, erule conjE)
apply (simp add: iT_Div_0_icard_if icard_0_eq[unfolded zero_inat_def])
thm iT_Div_card_ge__is_maximal_lower_bound
apply (case_tac "finite I")
prefer 2
apply (drule_tac x=I in spec, drule_tac x=d in spec)
apply simp
apply simp
apply (frule_tac iT_Div_finite_iff[THEN iffD2], assumption)
thm iT_Div_card_ge__is_maximal_lower_bound
apply (cut_tac f="λc d. the_Fin (f (Fin c) d)" and I=I and d=d in iT_Div_card_ge__is_maximal_lower_bound)
apply (intro allI, rename_tac I' d')
apply (subgoal_tac "!!k. f 0 k = 0")
prefer 2
apply (drule_tac x="{}" in spec, drule_tac x=k in spec, erule conjE)
apply (simp add: iT_Div_empty)
apply (drule_tac x=I' in spec, drule_tac x=d' in spec, erule conjE)
apply (case_tac "d' = 0")
apply (simp add: idiv_by_0 imod_by_0 iT_Div_0_card_if iT_Div_0_icard_if)
apply (case_tac "I' = {}", simp)
apply (case_tac "finite I'")
apply (simp add: icard_finite)
apply simp
apply simp
apply (case_tac "finite I'")
apply (frule_tac I=I' and k=d' in iT_Div_finite_iff[THEN iffD2, rule_format], assumption)
apply (simp add: icard_finite)
apply (subgoal_tac "∃n. f (Fin (card I')) d' = Fin n")
prefer 2
apply (rule Fin_ile, assumption)
apply clarsimp
apply (subgoal_tac "infinite (I' \<oslash> d')")
prefer 2
apply (simp add: iT_Div_finite_iff)
apply simp
apply (drule_tac x=I in spec, drule_tac x=d in spec, erule conjE)
apply (simp add: icard_finite)
apply (subgoal_tac "∃n. f (Fin (card I)) d = Fin n")
prefer 2
apply (rule Fin_ile, assumption)
apply clarsimp
done
subsection {* Results about sets of intervals *}
subsubsection {* Set of intervals without and with emtpy interval *}
definition iFROM_UN_set :: "(nat set) set" where
"iFROM_UN_set ≡ \<Union>n. {[n…]}"
definition iTILL_UN_set :: "(nat set) set" where
"iTILL_UN_set ≡ \<Union>n. {[…n]}"
definition iIN_UN_set :: "(nat set) set" where
"iIN_UN_set ≡ \<Union>n d. {[n…,d]}"
definition iMOD_UN_set :: "(nat set) set" where
"iMOD_UN_set ≡ \<Union>r m. {[r, mod m]}"
definition iMODb_UN_set :: "(nat set) set" where
"iMODb_UN_set ≡ \<Union>r m c. {[r, mod m, c]}"
definition iFROM_set :: "(nat set) set" where
"iFROM_set ≡ {[n…] |n. True}"
definition iTILL_set :: "(nat set) set" where
"iTILL_set ≡ {[…n] |n. True}"
definition iIN_set :: "(nat set) set" where
"iIN_set ≡ {[n…,d] |n d. True}"
definition iMOD_set :: "(nat set) set" where
"iMOD_set ≡ {[r, mod m] |r m. True}"
definition iMODb_set :: "(nat set) set" where
"iMODb_set ≡ {[r, mod m, c] |r m c. True}"
definition iMOD2_set :: "(nat set) set" where
"iMOD2_set ≡ {[r, mod m] |r m. 2 ≤ m}"
definition iMODb2_set :: "(nat set) set" where
"iMODb2_set ≡ {[r, mod m, c] |r m c. 2 ≤ m ∧ 1 ≤ c}"
definition iMOD2_UN_set :: "(nat set) set" where
"iMOD2_UN_set ≡ \<Union>r. \<Union>m∈{2..}. {[r, mod m]}"
definition iMODb2_UN_set :: "(nat set) set" where
"iMODb2_UN_set ≡ \<Union>r. \<Union>m∈{2..}. \<Union>c∈{1..}. {[r, mod m, c]}"
lemmas i_set_defs =
iFROM_set_def iTILL_set_def iIN_set_def
iMOD_set_def iMODb_set_def
iMOD2_set_def iMODb2_set_def
lemmas i_UN_set_defs =
iFROM_UN_set_def iTILL_UN_set_def iIN_UN_set_def
iMOD_UN_set_def iMODb_UN_set_def
iMOD2_UN_set_def iMODb2_UN_set_def
lemma iFROM_set_UN_set_eq: "iFROM_set = iFROM_UN_set"
by (fastsimp simp: iFROM_set_def iFROM_UN_set_def)
lemma
iTILL_set_UN_set_eq: "iTILL_set = iTILL_UN_set" and
iIN_set_UN_set_eq: "iIN_set = iIN_UN_set" and
iMOD_set_UN_set_eq: "iMOD_set = iMOD_UN_set" and
iMODb_set_UN_set_eq: "iMODb_set = iMODb_UN_set"
by (fastsimp simp: i_set_defs i_UN_set_defs)+
lemma iMOD2_set_UN_set_eq: "iMOD2_set = iMOD2_UN_set"
by (fastsimp simp: i_set_defs i_UN_set_defs)
lemma iMODb2_set_UN_set_eq: "iMODb2_set = iMODb2_UN_set"
by (fastsimp simp: i_set_defs i_UN_set_defs)
lemmas i_set_i_UN_set_sets_eq =
iFROM_set_UN_set_eq
iTILL_set_UN_set_eq
iIN_set_UN_set_eq
iMOD_set_UN_set_eq
iMODb_set_UN_set_eq
iMOD2_set_UN_set_eq
iMODb2_set_UN_set_eq
thm i_set_i_UN_set_sets_eq
lemma iMOD2_set_iMOD_set_subset: "iMOD2_set ⊆ iMOD_set"
by (fastsimp simp: i_set_defs)
lemma iMODb2_set_iMODb_set_subset: "iMODb2_set ⊆ iMODb_set"
by (fastsimp simp: i_set_defs)
definition i_set :: "(nat set) set" where
"i_set ≡ iFROM_set ∪ iTILL_set ∪ iIN_set ∪ iMOD_set ∪ iMODb_set"
definition i_UN_set :: "(nat set) set" where
"i_UN_set ≡ iFROM_UN_set ∪ iTILL_UN_set ∪ iIN_UN_set ∪ iMOD_UN_set ∪ iMODb_UN_set"
text {* Minimal definitions for @{term i_set} and @{term i_set} *}
definition i_set_min :: "(nat set) set" where
"i_set_min ≡ iFROM_set ∪ iIN_set ∪ iMOD2_set ∪ iMODb2_set"
definition i_UN_set_min :: "(nat set) set" where
"i_UN_set_min ≡ iFROM_UN_set ∪ iIN_UN_set ∪ iMOD2_UN_set ∪ iMODb2_UN_set"
definition i_set0 :: "(nat set) set" where
"i_set0 ≡ insert {} i_set"
thm i_set0_def
thm i_set_i_UN_set_sets_eq
lemma i_set_i_UN_set_eq: "i_set = i_UN_set"
by (simp add: i_set_def i_UN_set_def i_set_i_UN_set_sets_eq)
lemma i_set_min_i_UN_set_min_eq: "i_set_min = i_UN_set_min"
by (simp add: i_set_min_def i_UN_set_min_def i_set_i_UN_set_sets_eq)
lemma i_set_min_eq: "i_set = i_set_min"
apply (unfold i_set_def i_set_min_def)
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: i_set_defs)
apply (elim disjE)
apply blast
apply (fastsimp simp: iIN_0_iTILL_conv[symmetric])
apply blast
apply (elim exE)
apply (case_tac "2 ≤ m", blast)
apply (simp add: nat_ge2_conv)
apply (fastsimp simp: iMOD_0 iMOD_1)
apply (elim exE)
apply (case_tac "1 ≤ c")
apply (case_tac "2 ≤ m", fastsimp)
apply (simp add: nat_ge2_conv)
apply (fastsimp simp: iMODb_mod_0 iMODb_mod_1)
apply (fastsimp simp: linorder_not_le less_Suc_eq_le iMODb_0)
thm Un_mono
apply (rule Un_mono)+
apply (simp_all add: iMOD2_set_iMOD_set_subset iMODb2_set_iMODb_set_subset)
done
corollary i_UN_set_i_UN_min_set_eq: "i_UN_set = i_UN_set_min"
by (simp add: i_set_min_eq i_set_i_UN_set_eq[symmetric] i_set_min_i_UN_set_min_eq[symmetric])
thm
i_set_def i_set_min_def
i_set_min_eq
lemma i_set_min_is_minimal_let: "
let s1 = iFROM_set; s2= iIN_set; s3= iMOD2_set; s4= iMODb2_set in
s1 ∩ s2 = {} ∧ s1 ∩ s3 = {} ∧ s1 ∩ s4 = {} ∧
s2 ∩ s3 = {} ∧ s2 ∩ s4 = {} ∧ s3 ∩ s4 = {}"
apply (unfold Let_def i_set_defs, intro conjI)
apply (rule disjoint_iff_in_not_in1[THEN iffD2], clarsimp simp: iT_neq)+
done
lemmas i_set_min_is_minimal = i_set_min_is_minimal_let[simplified]
thm i_set_min_is_minimal
thm conjunct1
thm
i_set_min_is_minimal[THEN conjunct1]
i_set_min_is_minimal[THEN conjunct1[OF conjunct2]]
i_set_min_is_minimal[THEN conjunct1[OF conjunct2[OF conjunct2]]]
i_set_min_is_minimal[THEN conjunct1[OF conjunct2[OF conjunct2[OF conjunct2]]]]
i_set_min_is_minimal[THEN conjunct1[OF conjunct2[OF conjunct2[OF conjunct2[OF conjunct2]]]]]
i_set_min_is_minimal[THEN conjunct2[OF conjunct2[OF conjunct2[OF conjunct2[OF conjunct2]]]]]
thm
i_set_def
i_set_defs
inductive_set
i_set_ind:: "(nat set) set"
where
i_set_ind_FROM[intro!]: "[n…] ∈ i_set_ind"
| i_set_ind_TILL[intro!]: "[…n] ∈ i_set_ind"
| i_set_ind_IN[intro!]: "[n…,d] ∈ i_set_ind"
| i_set_ind_MOD[intro!]: "[r, mod m] ∈ i_set_ind"
| i_set_ind_MODb[intro!]: "[r, mod m, c] ∈ i_set_ind"
inductive_set
i_set0_ind :: "(nat set) set"
where
i_set0_ind_empty[intro!] : "{} ∈ i_set0_ind"
| i_set0_ind_i_set[intro]: "I ∈ i_set_ind ==> I ∈ i_set0_ind"
text {*
The introduction rule @{text i_set0_ind_i_set} is not declared a safe introduction rule,
because it would disturb the correct usage of the @{text safe} method. *}
lemma i_set_ind_subset_i_set0_ind: "i_set_ind ⊆ i_set0_ind"
by (rule subsetI, rule i_set0_ind_i_set)
thm
i_set_ind_FROM
i_set_ind_TILL
i_set_ind_IN
i_set_ind_MOD
i_set_ind_MODb
lemma
i_set0_ind_FROM[intro!] : "[n…] ∈ i_set0_ind" and
i_set0_ind_TILL[intro!] : "[…n] ∈ i_set0_ind" and
i_set0_ind_IN[intro!] : "[n…,d] ∈ i_set0_ind" and
i_set0_ind_MOD[intro!] : "[r, mod m] ∈ i_set0_ind" and
i_set0_ind_MODb[intro!] : "[r, mod m, c] ∈ i_set0_ind"
by (rule subsetD[OF i_set_ind_subset_i_set0_ind], rule i_set_ind.intros)+
lemmas i_set0_ind_intros2 =
i_set0_ind_empty
i_set0_ind_FROM
i_set0_ind_TILL
i_set0_ind_IN
i_set0_ind_MOD
i_set0_ind_MODb
thm i_set0_ind_intros2
lemma i_set_i_set_ind_eq: "i_set = i_set_ind"
apply (rule set_eqI, unfold i_set_def i_set_defs)
apply (rule iffI, blast)
apply (induct_tac x rule: i_set_ind.induct)
apply blast+
done
lemma i_set0_i_set0_ind_eq: "i_set0 = i_set0_ind"
apply (rule set_eqI, unfold i_set0_def)
thm i_set_i_set_ind_eq
apply (simp add: i_set_i_set_ind_eq)
apply (rule iffI)
apply blast
apply (rule_tac a=x in i_set0_ind.cases)
apply blast+
done
lemma i_set_imp_not_empty: "I ∈ i_set ==> I ≠ {}"
apply (simp add: i_set_i_set_ind_eq)
apply (induct I rule: i_set_ind.induct)
apply (rule iT_not_empty)+
done
lemma i_set0_i_set_mem_conv: "(I ∈ i_set0) = (I ∈ i_set ∨ I = {})"
apply (simp add: i_set_i_set_ind_eq i_set0_i_set0_ind_eq)
apply (rule iffI)
apply (rule i_set0_ind.cases[of I])
apply blast+
done
lemma i_set_i_set0_mem_conv: "(I ∈ i_set) = (I ∈ i_set0 ∧ I ≠ {})"
apply (insert i_set_imp_not_empty[of I])
apply (fastsimp simp: i_set0_i_set_mem_conv)
done
lemma i_set0_i_set_conv: "i_set0 - {{}} = i_set"
by (fastsimp simp: i_set_i_set0_mem_conv)
corollary i_set_subset_i_set0: "i_set ⊆ i_set0"
by (simp add: i_set0_i_set_conv[symmetric] Diff_subset)
lemma i_set_singleton: "{a} ∈ i_set"
by (fastsimp simp: i_set_def iIN_set_def iIN_0[symmetric])
lemma i_set0_singleton: "{a} ∈ i_set0"
apply (rule subsetD[OF i_set_subset_i_set0])
apply (simp add: iIN_0[symmetric] i_set_i_set_ind_eq i_set_ind.intros)
done
thm i_set_ind.intros
corollary
i_set_FROM[intro!] : "[n…] ∈ i_set" and
i_set_TILL[intro!] : "[…n] ∈ i_set" and
i_set_IN[intro!] : "[n…,d] ∈ i_set" and
i_set_MOD[intro!] : "[r, mod m] ∈ i_set" and
i_set_MODb[intro!] : "[r, mod m, c] ∈ i_set"
thm i_set_i_set_ind_eq
by (rule ssubst[OF i_set_i_set_ind_eq], rule i_set_ind.intros)+
lemmas i_set_intros =
i_set_FROM
i_set_TILL
i_set_IN
i_set_MOD
i_set_MODb
thm i_set0_ind_intros2
lemma
i_set0_empty[intro!]: "{} ∈ i_set0" and
i_set0_FROM[intro!] : "[n…] ∈ i_set0" and
i_set0_TILL[intro!] : "[…n] ∈ i_set0" and
i_set0_IN[intro!] : "[n…,d] ∈ i_set0" and
i_set0_MOD[intro!] : "[r, mod m] ∈ i_set0" and
i_set0_MODb[intro!] : "[r, mod m, c] ∈ i_set0"
by (rule ssubst[OF i_set0_i_set0_ind_eq], rule i_set0_ind_intros2)+
lemmas i_set0_intros =
i_set0_empty
i_set0_FROM
i_set0_TILL
i_set0_IN
i_set0_MOD
i_set0_MODb
thm i_set0_intros
lemma i_set_infinite_as_iMOD:"
[| I ∈ i_set; infinite I |] ==> ∃r m. I = [r, mod m]"
apply (simp add: i_set_i_set_ind_eq)
apply (induct I rule: i_set_ind.induct)
apply (simp_all add: iT_finite)
apply (rule_tac x=n in exI, rule_tac x="Suc 0" in exI, simp add: iMOD_1)
apply blast
done
lemma i_set_finite_as_iMODb:"
[| I ∈ i_set; finite I |] ==> ∃r m c. I = [r, mod m, c]"
apply (simp add: i_set_i_set_ind_eq)
apply (induct I rule: i_set_ind.induct)
apply (simp add: iT_infinite)
apply (rule_tac x=0 in exI, rule_tac x="Suc 0" in exI, rule_tac x=n in exI)
apply (simp add: iMODb_mod_1 iIN_0_iTILL_conv)
apply (rule_tac x=n in exI, rule_tac x="Suc 0" in exI, rule_tac x=d in exI)
apply (simp add: iMODb_mod_1)
apply (case_tac "m = 0")
apply (rule_tac x=r in exI, rule_tac x="Suc 0" in exI, rule_tac x=0 in exI)
apply (simp add: iMOD_0 iIN_0 iMODb_0)
apply (simp add: iT_infinite)
apply blast
done
lemma i_set_as_iMOD_iMODb: "
I ∈ i_set ==> (∃r m. I = [r, mod m]) ∨ (∃r m c. I = [r, mod m, c])"
by (blast intro: i_set_finite_as_iMODb i_set_infinite_as_iMOD)
subsubsection {* Interval sets are closed under cutting *}
lemma i_set_cut_le_ge_closed_disj: "
[| I ∈ i_set; t ∈ I; cut_op = op \<down>≤ ∨ cut_op = op \<down>≥ |] ==>
cut_op I t ∈ i_set"
apply (simp add: i_set_i_set_ind_eq)
apply (induct rule: i_set_ind.induct)
apply safe
apply (simp_all add: iT_cut_le1 iT_cut_ge1 i_set_ind.intros iMODb_iff)
done
thm i_set_cut_le_ge_closed_disj[of _ _ "op \<down>≥", simplified]
corollary
i_set_cut_le_closed: "[| I ∈ i_set; t ∈ I |] ==> I \<down>≤ t ∈ i_set" and
i_set_cut_ge_closed: "[| I ∈ i_set; t ∈ I |] ==> I \<down>≥ t ∈ i_set"
by (simp_all add: i_set_cut_le_ge_closed_disj)
lemmas i_set_cut_le_ge_closed = i_set_cut_le_closed i_set_cut_ge_closed
thm i_set_cut_le_ge_closed
lemma i_set0_cut_closed_disj: "
[| I ∈ i_set0;
cut_op = op \<down>≤ ∨ cut_op = op \<down>≥ ∨
cut_op = op \<down>< ∨ cut_op = op \<down>> |] ==>
cut_op I t ∈ i_set0"
apply (simp add: i_set0_i_set0_ind_eq)
apply (induct rule: i_set0_ind.induct)
thm i_set0_ind_empty
thm ssubst[OF set_restriction_empty, where P="λx. x ∈ i_set0_ind"]
apply (rule ssubst[OF set_restriction_empty, where P="λx. x ∈ i_set0_ind"])
thm i_cut_set_restriction_disj
apply (rule i_cut_set_restriction_disj[of cut_op], blast)
apply blast
apply blast
apply (induct_tac I rule: i_set_ind.induct)
apply safe
apply (simp_all add: iT_cut_le iT_cut_ge iT_cut_less iT_cut_greater i_set0_ind_intros2)
done
thm i_set0_cut_closed_disj[of _ "op \<down>>", simplified]
corollary
i_set0_cut_le_closed: "I ∈ i_set0 ==> I \<down>≤ t ∈ i_set0" and
i_set0_cut_less_closed: "I ∈ i_set0 ==> I \<down>< t ∈ i_set0" and
i_set0_cut_ge_closed: "I ∈ i_set0 ==> I \<down>≥ t ∈ i_set0" and
i_set0_cut_greater_closed: "I ∈ i_set0 ==> I \<down>> t ∈ i_set0"
by (simp_all add: i_set0_cut_closed_disj)
thm i_set0_ind.intros
thm
i_set0_FROM[ THEN i_set0_cut_closed_disj[of _ "op \<down><", simplified] ]
i_set0_TILL[ THEN i_set0_cut_closed_disj[of _ "op \<down>≥", simplified] ]
i_set0_IN[ THEN i_set0_cut_closed_disj[of _ "op \<down>≤", simplified] ]
i_set0_MOD[ THEN i_set0_cut_closed_disj[of _ "op \<down>>", simplified] ]
i_set0_MODb[ THEN i_set0_cut_closed_disj[of _ "op \<down>>", simplified] ]
lemmas i_set0_cut_closed =
i_set0_cut_le_closed
i_set0_cut_less_closed
i_set0_cut_ge_closed
i_set0_cut_greater_closed
thm i_set0_cut_closed
subsubsection {* Interval sets are closed under addition and multiplication *}
lemma i_set_Plus_closed: "I ∈ i_set ==> I ⊕ k ∈ i_set"
apply (simp add: i_set_i_set_ind_eq)
apply (induct rule: i_set_ind.induct)
apply (simp_all add: iT_add i_set_ind.intros)
done
lemma i_set_Mult_closed: "I ∈ i_set ==> I ⊗ k ∈ i_set"
apply (case_tac "k = 0")
apply (simp add: i_set_imp_not_empty iT_Mult_0_if i_set_intros)
apply (simp add: i_set_i_set_ind_eq)
apply (induct rule: i_set_ind.induct)
apply (simp_all add: iT_mult i_set_ind.intros)
done
lemma i_set0_Plus_closed: "I ∈ i_set0 ==> I ⊕ k ∈ i_set0"
apply (simp add: i_set0_i_set0_ind_eq)
apply (induct I rule: i_set0_ind.induct)
apply (simp add: iT_Plus_empty i_set0_ind_empty)
apply (rule subsetD[OF i_set_ind_subset_i_set0_ind])
apply (simp add: i_set_i_set_ind_eq[symmetric] i_set_Plus_closed)
done
lemma i_set0_Mult_closed: "I ∈ i_set0 ==> I ⊗ k ∈ i_set0"
apply (simp add: i_set0_i_set0_ind_eq)
apply (induct I rule: i_set0_ind.induct)
apply (simp add: iT_Mult_empty i_set0_ind_empty)
apply (rule subsetD[OF i_set_ind_subset_i_set0_ind])
apply (simp add: i_set_i_set_ind_eq[symmetric] i_set_Mult_closed)
done
subsubsection {* Interval sets are closed with certain conditions under subtraction *}
lemma i_set_Plus_neg_closed: "
[| I ∈ i_set; ∃x∈I. k ≤ x |] ==> I ⊕- k ∈ i_set"
apply (simp add: i_set_i_set_ind_eq)
apply (induct rule: i_set_ind.induct)
apply (fastsimp simp: iT_iff iT_add_neg)+
done
lemma i_set_Minus_closed: "
[| I ∈ i_set; iMin I ≤ k |] ==> k \<ominus> I ∈ i_set"
apply (simp add: i_set_i_set_ind_eq)
apply (induct rule: i_set_ind.induct)
apply (fastsimp simp: iT_Min iT_sub)+
done
lemma i_set0_Plus_neg_closed: "I ∈ i_set0 ==> I ⊕- k ∈ i_set0"
apply (simp add: i_set0_i_set0_ind_eq)
apply (induct rule: i_set0_ind.induct)
apply (fastsimp simp: iT_Plus_neg_empty)
apply (induct_tac I rule: i_set_ind.induct)
apply (fastsimp simp: iT_add_neg)+
done
lemma i_set0_Minus_closed: "I ∈ i_set0 ==> k \<ominus> I ∈ i_set0"
apply (simp add: i_set0_i_set0_ind_eq)
apply (induct rule: i_set0_ind.induct)
apply (simp add: iT_Minus_empty i_set0_ind_empty)
apply (induct_tac I rule: i_set_ind.induct)
apply (fastsimp simp: iT_sub)+
done
lemmas i_set_IntOp_closed =
i_set_Plus_closed
i_set_Mult_closed
i_set_Plus_neg_closed
i_set_Minus_closed
lemmas i_set0_IntOp_closed =
i_set0_Plus_closed
i_set0_Mult_closed
i_set0_Plus_neg_closed
i_set0_Minus_closed
thm i_set_IntOp_closed
thm i_set0_IntOp_closed
subsubsection {* Interval sets are not closed under division *}
thm i_set_as_iMOD_iMODb
thm iMOD_div_mod_gr0_not_ex
lemma iMOD_div_mod_gr0_not_in_i_set: "
[| 0 < k; k < m; 0 < m mod k |] ==> [r, mod m] \<oslash> k ∉ i_set"
apply (rule ccontr, simp)
thm i_set_infinite_as_iMOD
apply (drule i_set_infinite_as_iMOD)
apply (simp add: iT_Div_finite_iff iMOD_infinite)
apply (elim exE, rename_tac r' m')
apply (frule iMOD_div_mod_gr0_not_ex[of k m r], assumption+)
apply fastsimp
done
lemma iMODb_div_mod_gr0_not_in_i_set: "
[| 0 < k; k < m; 0 < m mod k; k ≤ c |] ==> [r, mod m, c] \<oslash> k ∉ i_set"
apply (rule ccontr, simp)
apply (drule i_set_finite_as_iMODb)
apply (simp add: iT_Div_finite_iff iMODb_finite)
apply (elim exE, rename_tac r' m' c')
apply (frule iMODb_div_mod_gr0_not_ex[of k m c r], assumption+)
apply fastsimp
done
lemma "[0, mod 3] \<oslash> 2 ∉ i_set"
by (rule iMOD_div_mod_gr0_not_in_i_set, simp+)
lemma i_set_Div_not_closed: "Suc 0 < k ==> ∃I∈i_set. I \<oslash> k ∉ i_set"
apply (rule_tac x="[0, mod (Suc k)]" in bexI)
apply (rule iMOD_div_mod_gr0_not_in_i_set)
apply (simp_all add: mod_Suc i_set_MOD)
done
lemma i_set0_Div_not_closed: "Suc 0 < k ==> ∃I∈i_set0. I \<oslash> k ∉ i_set0"
apply (frule i_set_Div_not_closed, erule bexE)
apply (rule_tac x=I in bexI)
apply (simp add: i_set0_def iT_Div_not_empty i_set_imp_not_empty)
apply (rule subsetD[OF i_set_subset_i_set0], assumption)
done
thm
i_set_Div_not_closed
i_set0_Div_not_closed
subsubsection {* Sets of intervals closed under division *}
inductive_set
NatMultiples :: "nat set => nat set"
for F :: "nat set"
where
NatMultiples_Factor: "
k ∈ F ==> k ∈ NatMultiples F"
| NatMultiples_Product: "
[| k ∈ F; m ∈ NatMultiples F |] ==> k * m ∈ NatMultiples F"
thm NatMultiples.induct
lemma NatMultiples_ex_divisor: "m ∈ NatMultiples F ==> ∃k∈F. m mod k = 0"
apply (induct m rule: NatMultiples.induct)
apply (rule_tac x=k in bexI, simp+)+
done
lemma NatMultiples_product_factor: "[| a ∈ F; b ∈ F |] ==> a * b ∈ NatMultiples F"
by (drule NatMultiples_Factor[of b], rule NatMultiples_Product)
lemma NatMultiples_product_factor_multiple: "
[| a ∈ F; b ∈ NatMultiples F |] ==> a * b ∈ NatMultiples F"
by (rule NatMultiples_Product)
lemma NatMultiples_product_multiple_factor: "
[| a ∈ NatMultiples F; b ∈ F |] ==> a * b ∈ NatMultiples F"
by (simp add: mult_commute[of a] NatMultiples_Product)
lemma NatMultiples_product_multiple: "
[| a ∈ NatMultiples F; b ∈ NatMultiples F |] ==> a * b ∈ NatMultiples F"
apply (induct a rule: NatMultiples.induct)
apply (simp add: NatMultiples_Product)
apply (simp add: mult_assoc[of _ _ b] NatMultiples_Product)
done
text {* Subset of @{term i_set} containing only continuous intervals, i. e., without @{term iMOD} and @{term iMODb}. *}
inductive_set i_set_cont :: "(nat set) set"
where
i_set_cont_FROM[intro]: "[n…] ∈ i_set_cont"
| i_set_cont_TILL[intro]: "[…n] ∈ i_set_cont"
| i_set_cont_IN[intro]: "[n…,d] ∈ i_set_cont"
definition i_set0_cont :: "(nat set) set" where
"i_set0_cont ≡ insert {} i_set_cont"
lemma i_set_cont_subset_i_set: "i_set_cont ⊆ i_set"
apply (unfold subset_eq, rule ballI, rename_tac x)
apply (rule_tac a=x in i_set_cont.cases)
apply blast+
done
lemma i_set0_cont_subset_i_set0: "i_set0_cont ⊆ i_set0"
apply (unfold i_set0_cont_def i_set0_def)
apply (rule insert_mono)
apply (rule i_set_cont_subset_i_set)
done
text {* Minimal definition of @{term i_set_cont} *}
inductive_set i_set_cont_min :: "(nat set) set"
where
i_set_cont_FROM[intro]: "[n…] ∈ i_set_cont_min"
| i_set_cont_IN[intro]: "[n…,d] ∈ i_set_cont_min"
definition i_set0_cont_min :: "(nat set) set" where
"i_set0_cont_min ≡ insert {} i_set_cont_min"
lemma i_set_cont_min_eq: "i_set_cont = i_set_cont_min"
apply (rule set_eqI, rule iffI)
apply (rename_tac x, rule_tac a=x in i_set_cont.cases)
apply (fastsimp simp: iIN_0_iTILL_conv[symmetric])+
apply (rename_tac x, rule_tac a=x in i_set_cont_min.cases)
apply blast+
done
text {* @{text inext} and @{text iprev} with continuous intervals *}
lemma i_set_cont_inext: "
[| I ∈ i_set_cont; n ∈ I; finite I ==> n < Max I |] ==> inext n I = Suc n"
apply (simp add: i_set_cont_min_eq)
apply (rule i_set_cont_min.cases, assumption)
apply (simp_all add: iT_finite iT_Max iT_inext_if iT_iff)
done
lemma i_set_cont_iprev: "
[| I ∈ i_set_cont; n ∈ I; iMin I < n |] ==> iprev n I = n - Suc 0"
apply (simp add: i_set_cont_min_eq)
apply (rule i_set_cont_min.cases, assumption)
apply (simp_all add: iT_iprev_if iT_Min iT_iff)
done
lemma i_set_cont_inext__less: "
[| I ∈ i_set_cont; n ∈ I; n < n0; n0 ∈ I |] ==> inext n I = Suc n"
apply (case_tac "finite I")
apply (rule i_set_cont_inext, assumption+)
thm order_less_le_trans[OF _ Max_ge]
apply (rule order_less_le_trans[OF _ Max_ge], assumption+)
apply (rule i_set_cont.cases, assumption)
apply (simp_all add: iT_finite iT_inext)
done
lemma i_set_cont_iprev__greater: "
[| I ∈ i_set_cont; n ∈ I; n0 < n; n0 ∈ I |] ==> iprev n I = n - Suc 0"
apply (rule i_set_cont_iprev, assumption+)
thm order_le_less_trans[OF iMin_le, of n0]
apply (rule order_le_less_trans[OF iMin_le, of n0], assumption+)
done
text {* Sets of modulo intervals *}
inductive_set i_set_mult :: "nat => (nat set) set"
for k :: nat
where
i_set_mult_FROM[intro!]: "[n…] ∈ i_set_mult k"
| i_set_mult_TILL[intro!]: "[…n] ∈ i_set_mult k"
| i_set_mult_IN[intro!]: "[n…,d] ∈ i_set_mult k"
| i_set_mult_MOD[intro!]: "[r, mod m * k] ∈ i_set_mult k"
| i_set_mult_MODb[intro!]: "[r, mod m * k, c] ∈ i_set_mult k"
definition i_set0_mult :: "nat => (nat set) set" where
"i_set0_mult k ≡ insert {} (i_set_mult k)"
lemma
i_set0_mult_empty[intro!]: "{} ∈ i_set0_mult k" and
i_set0_mult_FROM[intro!] : "[n…] ∈ i_set0_mult k" and
i_set0_mult_TILL[intro!] : "[…n] ∈ i_set0_mult k" and
i_set0_mult_IN[intro!] : "[n…,d] ∈ i_set0_mult k" and
i_set0_mult_MOD[intro!] : "[r, mod m * k] ∈ i_set0_mult k" and
i_set0_mult_MODb[intro!] : "[r, mod m * k, c] ∈ i_set0_mult k"
by (simp_all add: i_set0_mult_def i_set_mult.intros)
lemmas i_set0_mult_intros =
i_set0_mult_empty
i_set0_mult_FROM
i_set0_mult_TILL
i_set0_mult_IN
i_set0_mult_MOD
i_set0_mult_MODb
thm i_set0_mult_intros
lemma i_set_mult_subset_i_set0_mult: "i_set_mult k ⊆ i_set0_mult k"
by (unfold i_set0_mult_def, rule subset_insertI)
lemma i_set_mult_subset_i_set: "i_set_mult k ⊆ i_set"
apply (clarsimp simp: subset_iff)
apply (rule_tac a=t in i_set_mult.cases[of _ k])
apply (simp_all add: i_set_intros)
done
thm subsetD[OF i_set_mult_subset_i_set]
lemma i_set0_mult_subset_i_set0: "i_set0_mult k ⊆ i_set0"
apply (simp add: i_set0_mult_def i_set0_empty)
thm order_trans[OF _ i_set_subset_i_set0, OF i_set_mult_subset_i_set]
apply (rule order_trans[OF _ i_set_subset_i_set0, OF i_set_mult_subset_i_set])
done
lemma i_set_mult_0_eq_i_set_cont: "i_set_mult 0 = i_set_cont"
apply (rule set_eqI, rule iffI)
apply (rename_tac x, rule_tac a=x in i_set_mult.cases[of _ 0])
apply (simp_all add: i_set_cont.intros iMOD_0 iMODb_mod_0)
apply (rename_tac x, rule_tac a=x in i_set_cont.cases)
apply (simp_all add: i_set_mult.intros)
done
lemma i_set0_mult_0_eq_i_set0_cont: "i_set0_mult 0 = i_set0_cont"
by (simp add: i_set0_mult_def i_set0_cont_def i_set_mult_0_eq_i_set_cont)
lemma i_set_mult_1_eq_i_set: "i_set_mult (Suc 0) = i_set"
apply (rule set_eqI, rule iffI)
apply (rename_tac x, induct_tac x rule: i_set_mult.induct[of _ 1])
apply (simp_all add: i_set_intros)
apply (simp add: i_set_i_set_ind_eq)
apply (rename_tac x, induct_tac x rule: i_set_ind.induct)
apply (simp_all add: i_set_mult.intros)
apply (rule_tac t=m and s="m * Suc 0" in subst, simp, rule i_set_mult.intros)+
done
lemma i_set0_mult_1_eq_i_set0: "i_set0_mult (Suc 0) = i_set0"
by (simp add: i_set0_mult_def i_set0_def i_set_mult_1_eq_i_set)
lemma i_set_mult_imp_not_empty: "I ∈ i_set_mult k ==> I ≠ {}"
by (induct I rule: i_set_mult.induct, simp_all add: iT_not_empty)
lemma iMOD_in_i_set_mult_imp_divisor_mod_0: "
[| m ≠ Suc 0; [r, mod m] ∈ i_set_mult k |] ==> m mod k = 0"
apply (case_tac "m = 0", simp)
apply (rule i_set_mult.cases[of "[r, mod m]" k], assumption)
apply (blast dest: iFROM_iMOD_neq)
apply (blast dest: iTILL_iMOD_neq)
apply (blast dest: iIN_iMOD_neq)
apply (simp add: iMOD_eq_conv)
apply (blast dest: iMOD_iMODb_neq)
done
lemma
divisor_mod_0_imp_iMOD_in_i_set_mult: "m mod k = 0 ==> [r, mod m] ∈ i_set_mult k" and
divisor_mod_0_imp_iMODb_in_i_set_mult: "m mod k = 0 ==> [r, mod m, c] ∈ i_set_mult k"
by (clarsimp simp: mult_commute[of k])+
lemma iMOD_in_i_set_mult__divisor_mod_0_conv: "
m ≠ Suc 0 ==> ([r, mod m] ∈ i_set_mult k) = (m mod k = 0)"
apply (rule iffI)
apply (simp add: iMOD_in_i_set_mult_imp_divisor_mod_0)
apply (simp add: divisor_mod_0_imp_iMOD_in_i_set_mult)
done
lemma i_set_mult_neq1_subset_i_set: "k ≠ Suc 0 ==> i_set_mult k ⊂ i_set"
apply (rule psubsetI, rule i_set_mult_subset_i_set)
apply (simp add: set_eq_iff)
apply (drule neq_iff[THEN iffD1], erule disjE)
apply (simp add: i_set_mult_0_eq_i_set_cont)
apply (thin_tac "k = 0")
apply (rule_tac x="[0, mod 2]" in exI)
apply (rule ccontr)
apply (simp add: i_set_intros)
apply (drule i_set_cont.cases[where P=False])
apply (drule sym, simp add: iT_neq)+
apply simp
apply (rule_tac x="[0, mod Suc k]" in exI)
apply (rule ccontr)
apply (simp add: i_set_intros)
apply (insert iMOD_in_i_set_mult_imp_divisor_mod_0[of "Suc k" 0 k])
apply (simp add: mod_Suc)
done
lemma mod_0_imp_i_set_mult_subset: "
a mod b = 0 ==> i_set_mult a ⊆ i_set_mult b"
apply (clarsimp simp: mult_commute[of b], rename_tac q)
thm i_set_mult.cases
apply (rule_tac a=x and k="q * b" in i_set_mult.cases)
apply (simp_all add: i_set_mult.intros mult_assoc[symmetric])
done
lemma i_set_mult_subset_imp_mod_0: "
[| a ≠ Suc 0; (i_set_mult a ⊆ i_set_mult b) |] ==> a mod b = 0"
apply (simp add: subset_iff)
apply (erule_tac x="[0, mod a]" in allE)
apply (simp add: divisor_mod_0_imp_iMOD_in_i_set_mult)
thm iMOD_in_i_set_mult_imp_divisor_mod_0[of _ 0 b]
apply (simp add: iMOD_in_i_set_mult_imp_divisor_mod_0[of _ 0 b])
done
lemma i_set_mult_subset_conv: "
a ≠ Suc 0 ==> (i_set_mult a ⊆ i_set_mult b) = (a mod b = 0)"
apply (rule iffI)
apply (simp add: i_set_mult_subset_imp_mod_0)
apply (simp add: mod_0_imp_i_set_mult_subset)
done
lemma i_set_mult_mod_0_div: "
[| I ∈ i_set_mult k; k mod d = 0 |] ==> I \<oslash> d ∈ i_set_mult (k div d)"
apply (case_tac "d = 0")
thm iT_Div_0[OF i_set_mult_imp_not_empty]
apply (simp add: iT_Div_0[OF i_set_mult_imp_not_empty] i_set_mult.intros)
apply (induct I rule: i_set_mult.induct)
apply (simp_all add: iT_div i_set_mult.intros)
thm mod_0_imp_mod_mult_left_0
thm mod_0_imp_div_mult_right_eq
thm iMOD_div iMODb_div
apply (simp_all add: iMOD_div iMODb_div mod_0_imp_mod_mult_left_0 mod_0_imp_div_mult_left_eq i_set_mult.intros)
done
text {* Intervals from @{term "i_set_mult k"} remain in @{term i_set} after division by @{term d} a divisor of @{term k}. *}
corollary i_set_mult_mod_0_div_i_set: "
[| I ∈ i_set_mult k; k mod d = 0 |] ==> I \<oslash> d ∈ i_set"
thm subsetD[OF i_set_mult_subset_i_set[of "k div d"]]
by (rule subsetD[OF i_set_mult_subset_i_set[of "k div d"]], rule i_set_mult_mod_0_div)
corollary i_set_mult_div_self_i_set: "
I ∈ i_set_mult k ==> I \<oslash> k ∈ i_set"
by (simp add: i_set_mult_mod_0_div_i_set)
lemma i_set_mod_0_mult_in_i_set_mult: "
[| I ∈ i_set; m mod k = 0 |] ==> I ⊗ m ∈ i_set_mult k"
apply (case_tac "m = 0")
apply (simp add: iT_Mult_0 i_set_imp_not_empty i_set_mult.intros)
apply (clarsimp simp: mult_commute[of k])
apply (simp add: i_set_i_set_ind_eq)
apply (rule_tac a=I in i_set_ind.cases)
apply (simp_all add: iT_mult mult_assoc[symmetric] i_set_mult.intros)
done
lemma i_set_self_mult_in_i_set_mult: "
I ∈ i_set ==> I ⊗ k ∈ i_set_mult k"
by (rule i_set_mod_0_mult_in_i_set_mult[OF _ mod_self])
lemma i_set_mult_mod_gr0_div_not_in_i_set:"
[| 0 < k; 0 < d; 0 < k mod d |] ==> ∃I∈i_set_mult k. I \<oslash> d ∉ i_set"
apply (case_tac "d = Suc 0", simp)
thm iMOD_div_mod_gr0_not_ex[of d "Suc d * k" 0]
apply (frule iMOD_div_mod_gr0_not_ex[of d "Suc d * k" 0])
apply (rule Suc_le_lessD, rule gr0_imp_self_le_mult1, assumption)
apply simp
apply (rule_tac x="[0, mod Suc d * k]" in bexI)
apply (rule ccontr, simp)
thm i_set_infinite_as_iMOD
apply (frule i_set_infinite_as_iMOD)
apply (simp add: iT_Div_finite_iff iMOD_infinite)
apply fastsimp
apply (simp add: i_set_mult.intros del: mult_Suc)
done
lemma i_set0_mult_mod_0_div: "
[| I ∈ i_set0_mult k; k mod d = 0 |] ==> I \<oslash> d ∈ i_set0_mult (k div d)"
apply (simp add: i_set0_mult_def)
apply (elim disjE)
apply (simp add: iT_Div_empty)
apply (simp add: i_set_mult_mod_0_div)
done
corollary i_set0_mult_mod_0_div_i_set0: "
[| I ∈ i_set0_mult k; k mod d = 0 |] ==> I \<oslash> d ∈ i_set0"
by (rule subsetD[OF i_set0_mult_subset_i_set0[of "k div d"]], rule i_set0_mult_mod_0_div)
corollary i_set0_mult_div_self_i_set0: "
I ∈ i_set0_mult k ==> I \<oslash> k ∈ i_set0"
by (simp add: i_set0_mult_mod_0_div_i_set0)
lemma i_set0_mod_0_mult_in_i_set0_mult: "
[| I ∈ i_set0; m mod k = 0 |] ==> I ⊗ m ∈ i_set0_mult k"
apply (simp add: i_set0_def)
apply (erule disjE)
apply (simp add: iT_Mult_empty i_set0_mult_empty)
apply (rule subsetD[OF i_set_mult_subset_i_set0_mult])
apply (simp add: i_set_mod_0_mult_in_i_set_mult)
done
lemma i_set0_self_mult_in_i_set0_mult: "
I ∈ i_set0 ==> I ⊗ k ∈ i_set0_mult k"
by (simp add: i_set0_mod_0_mult_in_i_set0_mult)
lemma i_set0_mult_mod_gr0_div_not_in_i_set0:"
[| 0 < k; 0 < d; 0 < k mod d |] ==> ∃I∈i_set0_mult k. I \<oslash> d ∉ i_set0"
apply (frule i_set_mult_mod_gr0_div_not_in_i_set[of k d], assumption+)
apply (erule bexE, rename_tac I, rule_tac x=I in bexI)
apply (simp add: i_set0_def iT_Div_not_empty i_set_mult_imp_not_empty)
apply (simp add: subsetD[OF i_set_mult_subset_i_set0_mult])
done
end