Up to index of Isabelle/HOL/List-Infinite
theory SetIntervalStep(* Title: SetIntervalStep.thy
Date: Oct 2006
Author: David Trachtenherz
*)
header {* Stepping through sets of natural numbers *}
theory SetIntervalStep
imports SetIntervalCut
begin
subsection {* Function @{text inext} and @{text iprev} for stepping through natural sets *}
definition
inext :: "nat => nat set => nat"
where
"inext n I ≡ (
if (n ∈ I ∧ (I \<down>> n ≠ {}))
then iMin (I \<down>> n)
else n)"
definition
iprev :: "nat => nat set => nat"
where
"iprev n I ≡ (
if (n ∈ I ∧ (I \<down>< n ≠ {}))
then Max (I \<down>< n)
else n)"
text {* @{text inext} and @{text iprev} can be viewed as generalisations of @{text Suc} and @{text prev} *}
lemma inext_UNIV: "inext n UNIV = Suc n"
apply (simp add: inext_def cut_greater_def, safe)
apply (rule iMin_equality)
apply fastsimp+
done
lemma iprev_UNIV: "iprev n UNIV = n - Suc 0"
apply (simp add: iprev_def cut_less_def, safe)
apply (rule Max_equality)
apply fastsimp+
done
lemma inext_empty: "inext n {} = n"
unfolding inext_def by simp
lemma iprev_empty: "iprev n {} = n"
unfolding iprev_def by simp
thm
finite_nat_iff_bounded_le
finite_nat_iff_bounded_le2
lemma not_in_inext_fix: "n ∉ I ==> inext n I = n"
unfolding inext_def by simp
lemma not_in_iprev_fix: "n ∉ I ==> iprev n I = n"
unfolding iprev_def by simp
lemma inext_all_le_fix: "∀x∈I. x ≤ n ==> inext n I = n"
unfolding inext_def by force
lemma iprev_all_ge_fix: "∀x∈I. n ≤ x ==> iprev n I = n"
unfolding iprev_def by force
lemma inext_Max: "finite I ==> inext (Max I) I = Max I"
unfolding inext_def cut_greater_def by (fastsimp dest: Max_ge)
lemma iprev_iMin: "iprev (iMin I) I = iMin I"
unfolding iprev_def cut_less_def by fastsimp
lemma inext_ge_Max: "[| finite I; Max I ≤ n |] ==> inext n I = n"
unfolding inext_def cut_greater_def by (fastsimp dest: Max_ge)
thm iprev_iMin
lemma iprev_le_iMin: "n ≤ iMin I ==> iprev n I = n"
unfolding iprev_def cut_less_def by fastsimp
lemma inext_singleton: "inext n {a} = n"
unfolding inext_def by fastsimp
lemma iprev_singleton: "iprev n {a} = n"
unfolding iprev_def by fastsimp
lemma inext_closed: "n ∈ I ==> inext n I ∈ I"
apply (clarsimp simp: inext_def)
thm subsetD[of "I \<down>> n" I]
apply (rule subsetD[OF cut_greater_subset])
apply (rule iMinI_ex2, assumption)
done
lemma iprev_closed: "n ∈ I ==> iprev n I ∈ I"
apply (clarsimp simp: iprev_def)
thm subsetD[of "I \<down>< n" I]
apply (rule subsetD[of "I \<down>< n"], fastsimp)
thm Max_in[OF nat_cut_less_finite]
by (rule Max_in[OF nat_cut_less_finite])
thm inext_closed
lemma inext_in_imp_in: "inext n I ∈ I ==> n ∈ I"
by (case_tac "n ∈ I", simp_all add: not_in_inext_fix)
lemma inext_in_iff: "(inext n I ∈ I) = (n ∈ I)"
apply (rule iffI)
apply (rule inext_in_imp_in, assumption)
apply (rule inext_closed, assumption)
done
lemma subset_inext_closed: "[| n ∈ B; A ⊆ B |] ==> inext n A ∈ B"
apply (case_tac "n ∈ A")
apply (fastsimp simp: inext_closed)
apply (simp add: not_in_inext_fix)
done
lemma subset_inext_in_imp_in: "[| inext n A ∈ B; A ⊆ B |] ==> n ∈ B"
apply (case_tac "n ∈ A")
apply fastsimp
apply (simp add: not_in_inext_fix)
done
lemma subset_inext_in_iff: "A ⊆ B ==> (inext n A ∈ B) = (n ∈ B)"
apply (rule iffI)
apply (rule subset_inext_in_imp_in, assumption+)
apply (rule subset_inext_closed, assumption+)
done
thm iprev_closed
lemma iprev_in_imp_in: "iprev n I ∈ I ==> n ∈ I"
apply (case_tac "n ∈ I")
apply (simp_all add: not_in_iprev_fix)
done
lemma iprev_in_iff: "(iprev n I ∈ I) = (n ∈ I)"
apply (rule iffI)
apply (rule iprev_in_imp_in, assumption)
apply (rule iprev_closed, assumption)
done
lemma subset_iprev_closed: "[| n ∈ B; A ⊆ B |] ==> iprev n A ∈ B"
apply (case_tac "n ∈ A")
apply (fastsimp simp: iprev_closed)
apply (simp add: not_in_iprev_fix)
done
lemma subset_iprev_in_imp_in: "[| iprev n A ∈ B; A ⊆ B |] ==> n ∈ B"
apply (case_tac "n ∈ A")
apply fastsimp
apply (simp add: not_in_iprev_fix)
done
lemma subset_iprev_in_iff: "A ⊆ B ==> (iprev n A ∈ B) = (n ∈ B)"
apply (rule iffI)
apply (rule subset_iprev_in_imp_in, assumption+)
apply (rule subset_iprev_closed, assumption+)
done
lemma inext_mono: "n ≤ inext n I"
by (simp add: inext_def i_cut_defs iMin_ge_iff)
corollary inext_neq_imp_less: "n ≠ inext n I ==> n < inext n I"
by (insert inext_mono[of n I], simp)
lemma inext_mono2: "[| n ∈ I; ∃x∈I. n < x |] ==> n < inext n I"
by (fastsimp simp add: inext_def i_cut_defs iMin_gr_iff)
lemma inext_mono2_infin: "[| n ∈ I; infinite I |] ==> n < inext n I"
apply (simp add: inext_def i_cut_defs iMin_gr_iff)
apply (fastsimp simp: infinite_nat_iff_unbounded)
done
lemma inext_mono2_fin: "[| n ∈ I; finite I; n ≠ Max I |] ==> n < inext n I"
apply (simp add: inext_def i_cut_defs iMin_gr_iff)
apply (blast intro: Max_ge Max_in)
done
thm inext_mono2
lemma inext_mono2_infin_fin: "
[| n ∈ I; n ≠ Max I ∨ infinite I |] ==> n < inext n I"
by (blast intro: inext_mono2_infin inext_mono2_fin)
thm Nat.zero_less_Suc
lemma inext_neq_iMin: "∃x∈I. n < x ==> inext n I ≠ iMin I"
apply (case_tac "n ∈ I")
prefer 2
apply (simp add: not_in_inext_fix)
apply (blast dest: iMinI)
apply (rule not_sym, rule less_imp_neq)
thm le_less_trans[OF iMin_le[of n], OF _ inext_mono2]
by (rule le_less_trans[OF iMin_le[of n], OF _ inext_mono2])
lemma inext_neq_iMin_infin: "infinite I ==> inext n I ≠ iMin I"
apply (rule inext_neq_iMin)
thm infinite_nat_iff_unbounded[THEN iffD1]
apply (blast dest: infinite_nat_iff_unbounded[THEN iffD1])
done
thm Max_le_Min_imp_singleton
lemma Max_le_iMin_imp_singleton: "[| finite I; I ≠ {}; Max I ≤ iMin I |] ==> I = {iMin I}"
by (simp add: iMin_Min_conv Max_le_Min_imp_singleton)
lemma inext_neq_iMin_not_singleton: "
[| I ≠ {}; ¬(∃a. I = {a}) |] ==> inext n I ≠ iMin I"
apply (case_tac "finite I")
prefer 2
apply (simp add: inext_neq_iMin_infin)
apply (case_tac "n ∈ I")
prefer 2
apply (simp add: not_in_inext_fix)
apply (blast intro: iMinI_ex2)
by (metis Max_le_iMin_imp_singleton iMin_le_Max inext_Max inext_mono2_infin_fin not_less_iMin)
corollary inext_neq_iMin_not_card_1: "
[| I ≠ {}; card I ≠ Suc 0 |] ==> inext n I ≠ iMin I"
by (simp add: inext_neq_iMin_not_singleton card_1_singleton_conv)
lemma inext_neq_imp_Max: "n ≠ inext n I ==> n < Max I ∨ infinite I"
by (rule ccontr, clarsimp simp: inext_ge_Max)
lemma inext_less_conv: "(n ∈ I ∧ (n < Max I ∨ infinite I)) = (n < inext n I)"
apply (rule iffI)
apply (blast intro: inext_mono2_infin_fin)
apply (rule conjI)
apply (rule ccontr)
apply (simp add: not_in_inext_fix)
apply (blast dest: inext_neq_imp_Max less_imp_neq)
done
lemma inext_min_step: "[| n < k; k < inext n I |] ==> k ∉ I"
apply (case_tac "n ∈ I")
prefer 2
apply (simp add: inext_def)
thm contrapos_pn[of "k < inext n I" "k ∈ I"]
apply (rule contrapos_pn[of "k < inext n I" "k ∈ I"], simp)
apply (simp add: inext_def i_cut_defs)
apply (case_tac "∃x. x ∈ I ∧ n < x")
apply simp
thm not_less_iMin
thm not_less_iMin[of k "{x ∈ I. n < x}"]
apply (blast dest: not_less_iMin)
apply blast
done
corollary inext_min_step2: "¬(∃k∈I. n < k ∧ k < inext n I)"
by (clarsimp simp add: inext_min_step)
lemma min_step_inext[rule_format]: "
[| x < y; x ∈ I; y ∈ I; !!k. [| x < k; k < y |] ==> k ∉ I |] ==>
inext x I = y"
apply (rule ccontr)
thm nat_neq_iff
apply (simp add: nat_neq_iff, safe)
thm inext_closed[of x I]
thm inext_mono2[of x I]
apply (blast dest: inext_closed inext_mono2)
thm inext_min_step[of x y I]
apply (simp add: inext_min_step)
done
corollary min_step_inext2[rule_format]: "
[| x < y; x ∈ I; y ∈ I; ¬(∃k ∈ I. x < k ∧ k < y) |] ==>
inext x I = y"
by (blast intro: min_step_inext)
lemma between_empty_imp_inext_eq: "
[| n ∈ A; n < inext n A; n ∈ B; inext n A ∈ B; B \<down>> n \<down>< (inext n A) = {} |] ==>
inext n B = inext n A"
by (blast intro: min_step_inext2)
lemma inext_le_mono: "[| a ≤ b; a ∈ I; b ∈ I |] ==> inext a I ≤ inext b I"
apply (drule order_le_less[THEN iffD1], erule disjE)
prefer 2
apply simp
apply (rule order_trans[of _ b])
apply (rule ccontr, simp add: linorder_not_le)
thm inext_min_step
apply (blast dest: inext_min_step)
by (rule inext_mono)
thm inext_mono2
lemma inext_less_mono: "
[| a < b; a ∈ I; b ∈ I; ∃x∈I. b < x |] ==> inext a I < inext b I"
apply (rule le_less_trans[of _ b])
apply (rule ccontr, simp add: linorder_not_le)
thm inext_min_step
apply (blast dest: inext_min_step)
by (rule inext_mono2)
thm inext_mono2_fin
lemma inext_less_mono_fin: "
[| a < b; a ∈ I; b ∈ I; finite I; b ≠ Max I |] ==> inext a I < inext b I"
thm inext_less_mono Max_in
by (blast intro: inext_less_mono Max_in)
thm inext_mono2_infin
lemma inext_less_mono_infin: "
[| a < b; a ∈ I; b ∈ I; infinite I |] ==> inext a I < inext b I"
apply (rule inext_less_mono, assumption+)
apply (blast dest: infinite_imp_asc_chain)
done
thm inext_mono2_infin_fin
lemma inext_less_mono_infin_fin: "
[| a < b; a ∈ I; b ∈ I; b ≠ Max I ∨ infinite I |] ==> inext a I < inext b I"
by (blast intro: inext_less_mono_infin inext_less_mono_fin)
lemma inext_le_mono_rev: "
[| inext a I ≤ inext b I; a ∈ I; b ∈ I; ∃x∈I. inext a I < x |] ==> a ≤ b"
apply (rule ccontr, simp add: linorder_not_le)
thm inext_less_mono
apply (frule inext_less_mono, assumption+)
apply (blast intro: le_less_trans inext_mono)
apply simp
done
lemma inext_le_mono_fin_rev: "
[| inext a I ≤ inext b I; a ∈ I; b ∈ I; finite I; inext a I ≠ Max I|] ==> a ≤ b"
by (metis inext_in_iff inext_le_mono_rev inext_mono2_infin_fin)
lemma inext_le_mono_infin_rev: "
[| inext a I ≤ inext b I; a ∈ I; b ∈ I; infinite I |] ==> a ≤ b"
by (metis inext_in_iff inext_le_mono_rev inext_mono2_infin_fin)
lemma inext_le_mono_infin_fin_rev: "
[| inext a I ≤ inext b I; a ∈ I; b ∈ I; inext a I ≠ Max I ∨ infinite I |] ==> a ≤ b"
by (blast intro: inext_le_mono_infin_rev inext_le_mono_fin_rev)
lemma inext_less_mono_rev: "
[| inext a I < inext b I; a ∈ I; b ∈ I |] ==> a < b"
by (metis inext_le_mono not_le)
lemma less_imp_inext_le: "[| a < b; a ∈ I; b ∈ I |] ==> inext a I ≤ b"
by (metis inext_min_step not_le)
lemma iprev_mono: "iprev n I ≤ n"
unfolding iprev_def i_cut_defs by simp
corollary iprev_neq_imp_greater: "n ≠ iprev n I ==> iprev n I < n"
by (insert iprev_mono[of n I], simp)
lemma iprev_mono2: "[| n ∈ I; ∃x∈I. x < n|] ==> iprev n I < n"
apply (unfold iprev_def i_cut_defs, clarsimp)
thm finite_nat_iff_bounded
apply (blast intro: finite_nat_iff_bounded)+
done
thm inext_mono2_fin
lemma iprev_mono2_if_neq_iMin: "[| n ∈ I; iMin I ≠ n|] ==> iprev n I < n"
thm iMinI
thm iprev_mono2
by (blast intro: iMinI iprev_mono2)
thm inext_neq_iMin
lemma iprev_neq_Max: "[| finite I; ∃x∈I. x < n |] ==> iprev n I ≠ Max I"
apply (case_tac "n ∈ I")
prefer 2
apply (simp add: not_in_iprev_fix)
apply (blast dest: Max_in)
apply (rule less_imp_neq)
thm less_le_trans[OF iprev_mono2 Max_ge]
by (rule less_le_trans[OF iprev_mono2 Max_ge])
thm inext_neq_iMin_not_singleton
lemma iprev_neq_Max_not_singleton: "
[| finite I; I ≠ {}; ¬(∃a. I = {a}) |] ==> iprev n I ≠ Max I"
apply (case_tac "n ∈ I")
prefer 2
thm not_in_iprev_fix
apply (simp add: not_in_iprev_fix)
apply (blast intro: Max_in)
apply (case_tac "n = iMin I")
apply (metis Max_le_Min_conv_singleton iMin_Min_conv iMin_le_Max iprev_iMin)
apply (metis iprev_mono2_if_neq_iMin not_greater_Max)
done
corollary iprev_neq_Max_not_card_1: "
[| finite I; I ≠ {}; card I ≠ Suc 0 |] ==> iprev n I ≠ Max I"
apply (rule iprev_neq_Max_not_singleton, assumption+)
apply (simp add: card_1_singleton_conv)
done
lemma iprev_neq_imp_iMin: "iprev n I ≠ n ==> iMin I < n"
by (rule ccontr, clarsimp simp: iprev_le_iMin)
lemma iprev_greater_conv: "(n ∈ I ∧ iMin I < n) = (iprev n I < n)"
apply (rule iffI)
apply (blast intro: iprev_mono2_if_neq_iMin)
apply (rule conjI)
apply (rule ccontr)
apply (simp add: not_in_iprev_fix)
apply (blast dest: iprev_neq_imp_iMin less_imp_neq)
done
lemma inext_fix_iff: "(n ∉ I ∨ (finite I ∧ Max I = n)) = (inext n I = n)"
apply (case_tac "n ∉ I", simp add: not_in_inext_fix)
by (metis inext_Max inext_min_step2 inext_mono2_infin_fin)
lemma iprev_fix_iff: "(n ∉ I ∨ iMin I = n) = (iprev n I = n)"
apply (case_tac "n ∉ I", simp add: not_in_iprev_fix)
by (metis iprev_iMin iprev_mono2_if_neq_iMin less_not_refl3)
lemma iprev_min_step: "[| iprev n I < k; k < n |] ==> k ∉ I"
apply (case_tac "n ∈ I")
prefer 2
apply (simp add: iprev_def)
thm contrapos_pn[of "iprev n I < k" "k ∈ I"]
apply (rule contrapos_pn[of "iprev n I < k" "k ∈ I"], simp)
apply (unfold iprev_def i_cut_defs, simp)
apply (split split_if_asm)
thm Max_ge[of "{x ∈ I. x < n}" k]
apply (cut_tac Max_ge[of "{x ∈ I. x < n}" k])
apply fastsimp+
done
corollary iprev_min_step2: "¬(∃x∈I. iprev n I < x ∧ x < n)"
by (clarsimp simp add: iprev_min_step)
lemma min_step_iprev: "
[| x < y; x ∈ I; y ∈ I; !!k. [| x < k; k < y |] ==> k ∉ I |] ==>
iprev y I = x"
thm ccontr
apply (rule ccontr)
thm nat_neq_iff
apply (simp add: nat_neq_iff, elim disjE)
thm iprev_min_step
apply (simp add: iprev_min_step)
thm iprev_closed
thm iprev_mono2
apply (blast dest: iprev_closed iprev_mono2 iprev_min_step)
done
corollary min_step_iprev2[rule_format]: "
[| x < y; x ∈ I; y ∈ I; ¬(∃k ∈ I. x < k ∧ k < y) |] ==>
iprev y I = x"
by (blast intro: min_step_iprev)
lemma between_empty_imp_iprev_eq: "
[| n ∈ A; iprev n A < n; n ∈ B; iprev n A ∈ B; B \<down>> (iprev n A) \<down>< n = {} |] ==>
iprev n B = iprev n A"
by (blast intro: min_step_iprev2)
lemma iprev_le_mono: "[| a ≤ b; a ∈ I; b ∈ I |] ==> iprev a I ≤ iprev b I"
apply (drule order_le_less[THEN iffD1], erule disjE)
prefer 2
apply simp
apply (rule order_trans[OF iprev_mono])
apply (rule ccontr, simp add: linorder_not_le)
thm iprev_min_step
by (blast dest: iprev_min_step)
lemma iprev_less_mono: "
[| a < b; a ∈ I; b ∈ I; ∃x∈I. x < a |] ==> iprev a I < iprev b I"
apply (rule less_le_trans[of _ a])
apply (blast intro: iprev_mono2)
apply (rule ccontr, simp add: linorder_not_le)
thm iprev_min_step
by (blast dest: iprev_min_step)
lemma iprev_less_mono_if_neq_iMin: "
[| a < b; a ∈ I; b ∈ I; iMin I ≠ a |] ==> iprev a I < iprev b I"
by (metis iprev_in_iff iprev_less_mono iprev_mono2_if_neq_iMin)
thm inext_le_mono_rev
lemma iprev_le_mono_rev: "
[| iprev a I ≤ iprev b I; a ∈ I; b ∈ I; iMin I ≠ iprev b I |] ==> a ≤ b"
apply (rule ccontr, simp add: linorder_not_le)
by (metis iprev_fix_iff iprev_less_mono_if_neq_iMin less_le_not_le)
thm inext_less_mono_rev
lemma iprev_less_mono_rev: "
[| iprev a I < iprev b I; a ∈ I; b ∈ I |] ==> a < b"
apply (rule ccontr, simp add: linorder_not_less)
by (metis iprev_le_mono less_le_not_le)
lemma set_restriction_inext_eq: "
[| set_restriction interval_fun; n ∈ interval_fun I; inext n I ∈ interval_fun I |] ==>
inext n (interval_fun I) = inext n I"
apply (subgoal_tac "n ∈ I")
prefer 2
apply (blast intro: set_restriction_in_imp)
apply (case_tac "inext n I = n")
apply simp
thm inext_fix_iff
thm inext_fix_iff[THEN iffD1]
apply (frule inext_fix_iff[THEN iffD2], clarsimp)
apply (frule set_restriction_finite, assumption)
apply (subgoal_tac "Max (interval_fun I) = Max I")
prefer 2
apply (blast intro: Max_equality Max_ge set_restriction_in_imp)
thm inext_fix_iff
apply (blast intro: inext_fix_iff[THEN iffD1])
thm inext_mono
thm le_neq_implies_less[OF inext_mono, OF not_sym]
apply (drule le_neq_implies_less[OF inext_mono, OF not_sym])
apply (rule between_empty_imp_inext_eq, assumption+)
thm not_ex_in_conv
apply (simp add: not_ex_in_conv[symmetric] i_cut_mem_iff)
by (metis inext_min_step2 set_restriction_in_imp)
thm set_restriction_inext_eq
lemma set_restriction_inext_singleton_eq: "
[| set_restriction interval_fun; n ∈ interval_fun I; inext n I ∈ interval_fun I |] ==>
{inext n (interval_fun I)} = interval_fun {inext n I}"
apply (case_tac "n ∉ I")
apply (blast dest: set_restriction_not_in_imp)
apply (frule set_restrictionD, erule exE, rename_tac P)
apply (simp add: singleton_iff set_eq_iff)
by (metis set_restriction_inext_eq)
lemma inext_iprev: "iMin I ≠ n ==> inext (iprev n I) I = n"
apply (case_tac "n ∉ I")
apply (simp add: inext_def iprev_def)
apply simp
apply (frule iMin_neq_imp_greater[OF _ not_sym], assumption)
thm iMinI iprev_min_step
thm min_step_inext iprev_mono2 iprev_closed
apply (blast dest: iMinI iprev_min_step intro: min_step_inext iprev_mono2 iprev_closed)
done
lemma iprev_inext_infin: "infinite I ==> iprev (inext n I) I = n"
apply (case_tac "n ∉ I")
apply (simp add: inext_def iprev_def)
apply simp
by (metis inext_in_iff inext_min_step2 inext_mono2_infin_fin min_step_iprev2)
lemma iprev_inext_fin: "
[| finite I; n ≠ Max I |] ==> iprev (inext n I) I = n"
apply (case_tac "n ∉ I")
apply (simp add: inext_def iprev_def)
apply simp
by (metis inext_in_iff inext_min_step2 inext_mono2_infin_fin min_step_iprev2)
lemma iprev_inext: "
n ≠ Max I ∨ infinite I ==> iprev (inext n I) I = n"
by (blast intro: iprev_inext_infin iprev_inext_fin)
lemma inext_eq_infin: "
[| inext a I = inext b I; infinite I |] ==> a = b"
thm arg_cong[where f="λx. iprev x I"]
apply (drule arg_cong[where f="λx. iprev x I"])
apply (simp add: iprev_inext_infin)
done
lemma inext_eq_fin: "
[| inext a I = inext b I; finite I; a ≠ Max I; b ≠ Max I |] ==> a = b"
apply (drule arg_cong[where f="λx. iprev x I"])
apply (simp add: iprev_inext_fin)
done
thm inext_mono2_infin_fin
lemma inext_eq_infin_fin: "
[| inext a I = inext b I; a ≠ Max I ∧ b ≠ Max I ∨ infinite I |] ==> a = b"
thm inext_eq_fin inext_eq_infin
by (blast intro: inext_eq_fin inext_eq_infin)+
lemma inext_eq: "
[| inext a I = inext b I; ∃x∈I. a < x; ∃x∈I. b < x |] ==> a = b"
by (metis iprev_inext not_le wellorder_Max_lemma)
lemma iprev_eq_if_neq_iMin: "
[| iprev a I = iprev b I; iMin I ≠ a; iMin I ≠ b |] ==> a = b"
apply (drule arg_cong[where f="λx. inext x I"])
apply (simp add: inext_iprev)
done
lemma iprev_eq: "
[| iprev a I = iprev b I; ∃x∈I. x < a; ∃x∈I. x < b |] ==> a = b"
by (metis iprev_eq_if_neq_iMin not_less_iMin)
lemma greater_imp_iprev_ge: "[| b < a; a ∈ I; b ∈ I |] ==> b ≤ iprev a I"
apply (rule ccontr, simp add: linorder_not_le)
apply (blast dest: iprev_min_step)
done
lemma inext_cut_less_conv: "inext n I < t ==> inext n (I \<down>< t) = inext n I"
thm le_less_trans[OF inext_mono]
apply (frule le_less_trans[OF inext_mono])
apply (case_tac "n ∈ I")
apply (simp add: inext_def)
thm i_cut_commute_disj[of "op \<down><" "op \<down>>", simplified]
apply (simp add: i_cut_commute_disj[of "op \<down><" "op \<down>>"] cut_less_mem_iff)
apply (case_tac "I \<down>> n ≠ {}")
apply simp
apply (metis cut_less_Min_eq cut_less_Min_not_empty)
apply (simp add: i_cut_empty)
apply (simp add: not_in_inext_fix cut_less_not_in_imp)
done
lemma inext_cut_le_conv: "inext n I ≤ t ==> inext n (I \<down>≤ t) = inext n I"
thm nat_cut_le_less_conv inext_cut_less_conv
by (simp add: nat_cut_le_less_conv inext_cut_less_conv)
lemma inext_cut_greater_conv: "t < n ==> inext n (I \<down>> t) = inext n I"
apply (case_tac "n ∈ I")
thm cut_greater_mem_iff[THEN iffD2, OF conjI]
apply (frule cut_greater_mem_iff[THEN iffD2, OF conjI], simp)
thm i_cut_commute_disj[of "op \<down>>" "op \<down>>", simplified]
thm cut_cut_greater
apply (simp add: inext_def i_cut_commute_disj[of "op \<down>>" "op \<down>>"] cut_cut_greater max_def)
apply (simp add: not_in_inext_fix cut_greater_not_in_imp)
done
lemma inext_cut_ge_conv: "t ≤ n ==> inext n (I \<down>≥ t) = inext n I"
apply (case_tac "t = 0")
apply (simp add: cut_ge_0_all)
thm nat_cut_greater_ge_conv[symmetric]
apply (simp add: nat_cut_greater_ge_conv[symmetric] inext_cut_greater_conv)
done
lemmas inext_cut_conv =
inext_cut_less_conv inext_cut_le_conv
inext_cut_greater_conv inext_cut_ge_conv
lemma iprev_cut_greater_conv: "t < iprev n I ==> iprev n (I \<down>> t) = iprev n I"
thm less_le_trans[OF _ iprev_mono]
apply (frule less_le_trans[OF _ iprev_mono])
apply (case_tac "n ∈ I")
apply (simp add: iprev_def)
thm i_cut_commute_disj[of "op \<down>>" "op \<down><", simplified]
apply (simp add: i_cut_commute_disj[of "op \<down>>" "op \<down><"] cut_greater_mem_iff)
apply (case_tac "I \<down>< n ≠ {}")
apply simp
apply (metis cut_greater_Max_eq cut_greater_Max_not_empty nat_cut_less_finite)
apply (simp add: i_cut_empty)
apply (simp add: not_in_iprev_fix cut_greater_not_in_imp)
done
lemma iprev_cut_ge_conv: "t ≤ iprev n I ==> iprev n (I \<down>≥ t) = iprev n I"
apply (case_tac "t = 0")
apply (simp add: cut_ge_0_all)
thm nat_cut_greater_ge_conv
apply (simp add: nat_cut_greater_ge_conv[symmetric] iprev_cut_greater_conv)
done
lemma iprev_cut_less_conv: "n < t ==> iprev n (I \<down>< t) = iprev n I"
apply (case_tac "n ∈ I")
thm cut_less_mem_iff[THEN iffD2, OF conjI]
apply (frule cut_less_mem_iff[THEN iffD2, OF conjI], simp)
thm i_cut_commute_disj[of "op \<down><" "op \<down><", simplified]
apply (simp add: iprev_def i_cut_commute_disj[of "op \<down><" "op \<down><"] cut_cut_less min_def)
apply (simp add: not_in_iprev_fix cut_less_not_in_imp)
done
lemma iprev_cut_le_conv: "n ≤ t ==> iprev n (I \<down>≤ t) = iprev n I"
thm nat_cut_le_less_conv iprev_cut_less_conv
by (simp add: nat_cut_le_less_conv iprev_cut_less_conv)
lemmas iprev_cut_conv =
iprev_cut_less_conv iprev_cut_le_conv
iprev_cut_greater_conv iprev_cut_ge_conv
thm
inext_cut_conv
iprev_cut_conv
thm inext_cut_less_conv
lemma inext_cut_less_fix: "t ≤ inext n I ==> inext n (I \<down>< t) = n"
apply (case_tac "n ∈ I")
prefer 2
thm contra_subsetD[OF cut_less_subset]
apply (frule contra_subsetD[OF cut_less_subset[of _ t]])
apply (simp add: not_in_inext_fix)
apply (case_tac "t ≤ n")
apply (metis cut_less_mem_iff not_in_inext_fix not_le)
apply (rule_tac t=n and s="Max (I \<down>< t)" in subst)
apply (rule Max_equality[OF _ nat_cut_less_finite])
apply (simp add: cut_less_mem_iff)
apply (rule ccontr)
apply (clarsimp simp: cut_less_mem_iff linorder_not_le)
thm inext_min_step
apply (simp add: inext_min_step)
thm inext_Max nat_cut_less_finite
apply (blast intro: inext_Max nat_cut_less_finite)
done
lemma inext_cut_le_fix: "t < inext n I ==> inext n (I \<down>≤ t) = n"
thm nat_cut_le_less_conv
by (simp add: nat_cut_le_less_conv inext_cut_less_fix)
lemma iprev_cut_greater_fix: "iprev n I ≤ t ==> iprev n (I \<down>> t) = n"
apply (case_tac "n ∈ I")
prefer 2
thm contra_subsetD[OF cut_greater_subset]
apply (frule contra_subsetD[OF cut_greater_subset[of _ t]])
apply (simp add: not_in_iprev_fix)
apply (case_tac "n ≤ t")
apply (metis cut_greater_mem_iff not_in_iprev_fix not_le)
apply (rule_tac t=n and s="iMin (I \<down>> t)" in subst)
apply (rule iMin_equality)
apply (simp add: cut_greater_mem_iff)
apply (metis cut_greater_mem_iff iprev_min_step2 not_leE order_le_less_trans)
thm iprev_iMin
apply (rule iprev_iMin)
done
lemma iprev_cut_ge_fix: "iprev n I < t ==> iprev n (I \<down>≥ t) = n"
apply (case_tac "t = 0")
apply (simp add: cut_ge_0_all)
thm nat_cut_greater_ge_conv[symmetric] iprev_cut_greater_fix
apply (simp add: nat_cut_greater_ge_conv[symmetric] iprev_cut_greater_fix)
done
definition
CommuteWithIntervalCut4 :: "(('a::linorder) set => 'a set) => bool"
where
"CommuteWithIntervalCut4 fun ≡
∀t fun2 I.
(fun2 = (λI. I \<down>< t) ∨ fun2 = (λI. I \<down>≤ t) ∨ fun2 = (λI. I \<down>> t) ∨ fun2 = (λI. I \<down>≥ t) ) -->
fun (fun2 I) = fun2 (fun I)"
definition CommuteWithIntervalCut2 :: "(('a::linorder) set => 'a set) => bool"
where
"CommuteWithIntervalCut2 fun ≡
∀t fun2 I.
(fun2 = (λI. I \<down>< t) ∨ fun2 = (λI. I \<down>> t)) -->
fun (fun2 I) = fun2 (fun I)"
lemma CommuteWithIntervalCut4_imp_2: "CommuteWithIntervalCut4 fun ==> CommuteWithIntervalCut2 fun"
unfolding CommuteWithIntervalCut2_def CommuteWithIntervalCut4_def by blast
lemma nat_CommuteWithIntervalCut2_4_eq: "
CommuteWithIntervalCut4 (fun::nat set => nat set) = CommuteWithIntervalCut2 fun"
apply (unfold CommuteWithIntervalCut2_def CommuteWithIntervalCut4_def)
apply (rule iffI)
apply blast
apply clarify
apply (case_tac "fun2 = (λI. I \<down>< t)", simp)
apply (case_tac "fun2 = (λI. I \<down>> t)", simp)
apply simp
apply (erule disjE)
apply (simp add: nat_cut_le_less_conv)
apply (case_tac "t = 0")
apply (simp add: cut_ge_0_all)
apply (simp add: nat_cut_greater_ge_conv[symmetric])
done
lemma
cut_less_CommuteWithIntervalCut4: "CommuteWithIntervalCut4 (λI. I \<down>< t)" and
cut_le_CommuteWithIntervalCut4: "CommuteWithIntervalCut4 (λI. I \<down>≤ t)" and
cut_greater_CommuteWithIntervalCut4: "CommuteWithIntervalCut4 (λI. I \<down>> t)" and
cut_ge_CommuteWithIntervalCut4: "CommuteWithIntervalCut4 (λI. I \<down>≥ t)"
thm i_cut_commute_disj
unfolding CommuteWithIntervalCut4_def by (simp_all add: i_cut_commute_disj)
lemmas i_cut_CommuteWithIntervalCut4 =
cut_less_CommuteWithIntervalCut4 cut_le_CommuteWithIntervalCut4
cut_greater_CommuteWithIntervalCut4 cut_ge_CommuteWithIntervalCut4
thm cut_greater_image
lemma inext_image: "
[| n ∈ I; strict_mono_on f I |] ==> inext (f n) (f ` I) = f (inext n I)"
apply (case_tac "∃x∈I. n < x")
thm inext_mono2
apply (frule inext_mono2, assumption)
thm cut_greater_not_empty_iff[THEN iffD2]
apply (frule cut_greater_not_empty_iff[THEN iffD2])
apply (simp add: inext_def image_iff)
apply (subgoal_tac "∃x∈I. f n = f x")
prefer 2
apply blast
thm cut_greater_image
apply (simp add: cut_greater_image)
thm iMin_mono_on2[OF strict_mono_on_imp_mono_on]
thm strict_mono_on_subset
apply (blast intro: strict_mono_on_subset iMin_mono_on2 strict_mono_on_imp_mono_on)
apply (drule strict_mono_on_imp_mono_on)
thm inext_all_le_fix
apply (simp add: inext_all_le_fix linorder_not_less mono_on_def)
done
lemma iprev_image: "
[| n ∈ I; strict_mono_on f I |] ==> iprev (f n) (f ` I) = f (iprev n I)"
apply (case_tac "∃x∈I. x < n")
thm iprev_mono2
apply (frule iprev_mono2, assumption)
thm cut_less_not_empty_iff[THEN iffD2]
apply (frule cut_less_not_empty_iff[THEN iffD2])
apply (simp add: iprev_def image_iff)
apply (subgoal_tac "∃x∈I. f n = f x")
prefer 2
apply blast
thm cut_less_image
apply (simp add: cut_less_image)
thm Max_mono_on2[OF strict_mono_on_imp_mono_on]
thm strict_mono_on_subset
thm nat_cut_less_finite
apply (blast intro: strict_mono_on_subset Max_mono_on2 strict_mono_on_imp_mono_on nat_cut_less_finite)
apply (drule strict_mono_on_imp_mono_on)
thm inext_all_le_fix
apply (simp add: iprev_all_ge_fix linorder_not_less mono_on_def)
done
lemma inext_image2: "
strict_mono f ==> inext (f n) (f ` I) = f (inext n I)"
apply (case_tac "n ∈ I")
apply (blast intro: strict_mono_imp_strict_mono_on inext_image)
thm inj_image_mem_iff strict_mono_imp_inj
apply (simp add: not_in_inext_fix inj_image_mem_iff strict_mono_imp_inj)
done
lemma iprev_image2: "
strict_mono f ==> iprev (f n) (f ` I) = f (iprev n I)"
apply (case_tac "n ∈ I")
apply (blast intro: strict_mono_imp_strict_mono_on iprev_image)
apply (simp add: not_in_iprev_fix inj_image_mem_iff strict_mono_imp_inj)
done
lemma inext_imirror_iprev_conv: "
[| finite I; n ≤ iMin I + Max I |] ==>
inext (mirror_elem n I) (imirror I) = mirror_elem (iprev n I) I"
apply (case_tac "n ∈ I")
prefer 2
thm imirror_mem_conv
apply (simp add: not_in_iprev_fix not_in_inext_fix imirror_mem_conv)
apply (frule in_imp_not_empty[of _ I])
apply (frule in_imp_mirror_elem_in[of _ n], assumption)
apply (simp add: inext_def iprev_def)
apply (case_tac "n = iMin I")
thm cut_less_Min_empty
thm mirror_elem_Min
apply (simp add: cut_less_Min_empty mirror_elem_Min)
thm imirror_Max
apply (subst imirror_Max[symmetric], assumption)
thm cut_greater_Max_empty[OF _ order_refl]
apply (simp add: cut_greater_Max_empty imirror_finite)
apply (frule iMin_le[of n I])
apply (intro conjI impI)
thm imirror_cut_greater'
apply (simp add: imirror_cut_greater')
thm imirror_bounds_iMin nat_cut_less_finite
apply (simp add: imirror_bounds_iMin nat_cut_less_finite cut_less_Min_eq)
apply (simp add: mirror_elem_def nat_mirror_def)
apply (simp add: imirror_cut_greater')
apply (simp add: imirror_bounds_def)
thm cut_less_Min_not_empty
apply (simp add: cut_less_Min_not_empty)
done
corollary inext_imirror_iprev_conv': "
[| finite I; n ∈ I |] ==>
inext (mirror_elem n I) (imirror I) = mirror_elem (iprev n I) I"
thm inext_imirror_iprev_conv[OF _ trans_le_add2[OF Max_ge]]
by (simp add: inext_imirror_iprev_conv trans_le_add2)
lemma iprev_imirror_inext_conv: "
[| finite I; n ≤ iMin I + Max I |] ==>
iprev (mirror_elem n I) (imirror I) = mirror_elem (inext n I) I"
apply (case_tac "n ∈ I")
prefer 2
thm imirror_mem_conv
apply (simp add: not_in_iprev_fix not_in_inext_fix imirror_mem_conv)
apply (frule in_imp_not_empty[of _ I])
apply (frule in_imp_mirror_elem_in[of _ n], assumption)
apply (simp add: inext_def iprev_def)
apply (case_tac "n = Max I")
thm cut_greater_Max_empty
thm mirror_elem_Max
apply (simp add: cut_greater_Max_empty mirror_elem_Max)
thm imirror_iMin
apply (subst imirror_iMin[symmetric], assumption)
thm cut_less_Min_empty[OF order_refl]
apply (simp add: cut_less_Min_empty imirror_finite)
thm Max_ge[of I n]
apply (frule Max_ge[of I n], assumption)
apply (drule le_neq_trans, assumption)
apply (intro conjI impI)
thm imirror_cut_less
apply (simp add: imirror_cut_less)
thm imirror_bounds_Max cut_greater_finite cut_greater_Max_eq
thm imirror_bounds_Max[OF cut_greater_finite]
thm Max_le_iff
apply (simp add: imirror_bounds_Max cut_greater_finite cut_greater_Max_eq del: Max_le_iff)
apply (simp add: mirror_elem_def nat_mirror_def)
apply (simp add: imirror_cut_less)
apply (simp add: imirror_bounds_def)
thm cut_greater_Max_not_empty[of I n]
apply (simp add: cut_greater_Max_not_empty)
done
corollary iprev_imirror_inext_conv': "
[| finite I; n ∈ I |] ==>
iprev (mirror_elem n I) (imirror I) = mirror_elem (inext n I) I"
by (simp add: iprev_imirror_inext_conv trans_le_add2)
thm
inext_imirror_iprev_conv
inext_imirror_iprev_conv'
iprev_imirror_inext_conv
iprev_imirror_inext_conv'
lemma inext_insert_ge_Max: "
[| finite I; I ≠ {}; Max I ≤ a |] ==> inext (Max I) (insert a I) = a"
apply (case_tac "a = Max I")
apply (simp add: insert_absorb inext_Max)
thm le_neq_trans
apply (drule le_neq_trans, simp)
apply (rule min_step_inext2)
apply (simp, simp, simp)
apply (simp_all, blast?) (* blast is optional for the case, that the last goal could be solved by the simplifier in a future version, making the blast command superfluous. *)
done
lemma iprev_insert_le_iMin: "
[| finite I; I ≠ {}; a ≤ iMin I |] ==> iprev (iMin I) (insert a I) = a"
apply (case_tac "a = iMin I")
apply (simp add: iMinI_ex2 insert_absorb iprev_iMin)
thm le_neq_trans
apply (drule le_neq_trans, simp)
apply (rule min_step_iprev2)
apply (simp_all add: iMin_Min_conv, blast?)
done
thm cut_le_less_conv
lemma cut_less_le_iprev_conv: "
[| t ∈ I; t ≠ iMin I |] ==> I \<down>< t = I \<down>≤ (iprev t I)"
apply (unfold iprev_def)
apply (rule set_eqI, safe)
apply (simp add: i_cut_defs)
apply simp
apply (split split_if_asm)
thm Max_ge_iff nat_cut_less_finite
apply (simp add: Max_ge_iff nat_cut_less_finite)
apply (blast intro: le_less_trans)
apply (frule iMin_neq_imp_greater, assumption)
apply (blast intro: iMin_in)
done
lemma neq_Max_imp_inext_neq_iMin: "
[| t ∈ I; t ≠ Max I ∨ infinite I |] ==> inext t I ≠ iMin I"
apply (case_tac "finite I")
apply (metis inext_mono2_infin_fin not_less_iMin)
apply (blast dest: inext_neq_iMin_infin)
done
corollary neq_Max_imp_inext_gr_iMin: "
[| t ∈ I; t ≠ Max I ∨ infinite I|] ==> iMin I < inext t I"
apply (frule neq_Max_imp_inext_neq_iMin[THEN not_sym], assumption)
apply (drule neq_le_trans)
thm inext_closed
apply (blast dest: inext_closed)
apply simp
done
lemma cut_le_less_inext_conv: "
[| t ∈ I; t ≠ Max I ∨ infinite I|] ==> I \<down>≤ t = I \<down>< (inext t I)"
thm cut_less_le_iprev_conv[of "inext t I" I]
apply (cut_tac cut_less_le_iprev_conv[of "inext t I" I])
thm iprev_inext[of t I]
apply (cut_tac iprev_inext[of t I], simp)
apply assumption
apply (rule inext_closed, assumption)
apply (rule neq_Max_imp_inext_neq_iMin, assumption+)
done
lemma cut_ge_greater_iprev_conv: "
[| t ∈ I; t ≠ iMin I |] ==> I \<down>≥ t = I \<down>> (iprev t I)"
apply (frule iMin_neq_imp_greater, simp+)
apply (unfold iprev_def)
apply (rule set_eqI, safe)
apply (simp add: i_cut_defs linorder_not_less)
apply (drule iMinI, fastsimp)
apply (split split_if_asm)
apply (rule ccontr)
apply (simp add: nat_cut_less_finite linorder_not_le)
apply blast
apply simp
done
lemma cut_greater_ge_inext_conv: "
[| t ∈ I; t ≠ Max I ∨ infinite I |] ==> I \<down>> t = I \<down>≥ (inext t I)"
thm cut_ge_greater_iprev_conv[of "inext t I" I]
apply (cut_tac cut_ge_greater_iprev_conv[of "inext t I" I])
thm iprev_inext[of t I]
apply (cut_tac iprev_inext[of t I], simp)
apply blast
apply (rule inext_closed, assumption)
apply (rule neq_Max_imp_inext_neq_iMin, assumption+)
done
thm
cut_less_le_iprev_conv
cut_le_less_inext_conv
cut_ge_greater_iprev_conv
cut_greater_ge_inext_conv
lemma inext_append: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B |] ==>
inext n (A ∪ B) = (if n ∈ B then inext n B else (if n = Max A then iMin B else inext n A))"
apply (case_tac "n ∈ A ∪ B")
prefer 2
apply (simp add: not_in_inext_fix)
apply (blast dest: Max_in)
apply (frule Max_less_iMin_imp_disjoint, assumption)
apply (drule Un_iff[THEN iffD1], elim disjE)
apply (drule disjoint_iff_in_not_in1[THEN iffD1])
apply simp
apply (intro conjI impI)
apply (simp add: inext_def cut_greater_Un cut_greater_Max_empty cut_greater_Min_all)
apply (frule Max_neq_imp_less[of A], simp+)
apply (simp add: inext_def cut_greater_Un cut_greater_Min_all)
apply (subgoal_tac "A \<down>> n ≠ {}")
prefer 2
apply (simp add: cut_greater_not_empty_iff)
apply (blast intro: Max_in)
apply (simp add: iMin_Un)
apply (drule iMin_in[THEN cut_greater_in_imp])
apply (rule min_eqL)
apply (rule less_imp_le)
apply blast
apply (drule disjoint_iff_in_not_in2[THEN iffD1])
apply simp
apply (subgoal_tac "A \<down>> n = {}")
prefer 2
apply (simp add: cut_greater_empty_iff)
apply fastsimp
apply (simp add: inext_def cut_greater_Un)
done
corollary inext_append_eq1: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B; n ∈ A; n ≠ Max A |] ==>
inext n (A ∪ B) = inext n A"
apply (frule Max_less_iMin_imp_disjoint, assumption)
apply (drule disjoint_iff_in_not_in1[THEN iffD1])
apply (simp add: inext_append Max_less_iMin_imp_disjoint)
done
corollary inext_append_eq2: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B; n ∈ B |] ==>
inext n (A ∪ B) = inext n B"
by (simp add: inext_append)
corollary inext_append_eq3: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B |] ==>
inext (Max A) (A ∪ B) = iMin B"
by (simp add: inext_append not_less_iMin)
lemma iprev_append: "[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B |] ==>
iprev n (A ∪ B) = (if n ∈ A then iprev n A else (if n = iMin B then Max A else iprev n B))"
apply (case_tac "n ∈ A ∪ B")
prefer 2
apply (simp add: not_in_iprev_fix)
apply (blast intro: iMin_in)
apply (frule Max_less_iMin_imp_disjoint, assumption)
apply (drule Un_iff[THEN iffD1], elim disjE)
apply (drule disjoint_iff_in_not_in1[THEN iffD1])
apply simp
apply (subgoal_tac "B \<down>< n = {}")
prefer 2
apply (simp add: cut_less_empty_iff)
apply fastsimp
apply (simp add: iprev_def cut_less_Un)
apply (drule disjoint_iff_in_not_in2[THEN iffD1])
apply simp
apply (intro conjI impI)
apply (simp add: iprev_def cut_less_Un cut_less_Min_empty cut_less_Max_all)
apply (frule iMin_neq_imp_greater[of _ B], simp+)
apply (simp add: iprev_def cut_less_Un)
apply (subgoal_tac "A \<down>< n = A")
prefer 2
apply (simp add: cut_less_all_iff)
apply fastsimp
apply (subgoal_tac "B \<down>< n ≠ {}")
prefer 2
apply (simp add: cut_less_not_empty_iff)
apply (blast intro: iMin_in)
apply (simp add: Max_Un nat_cut_less_finite)
apply (rule max_eqR)
apply (rule less_imp_le)
thm Max_in[OF nat_cut_less_finite, THEN cut_less_in_imp]
apply (drule Max_in[OF nat_cut_less_finite, THEN cut_less_in_imp])
apply (blast intro: iMin_le Max_in order_less_le_trans)
done
corollary iprev_append_eq1: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B; n ∈ A |] ==>
iprev n (A ∪ B) = iprev n A"
by (simp add: iprev_append)
corollary iprev_append_eq2: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B; n ∈ B; n ≠ iMin B |] ==>
iprev n (A ∪ B) = iprev n B"
apply (frule Max_less_iMin_imp_disjoint, assumption)
apply (drule disjoint_iff_in_not_in2[THEN iffD1])
apply (simp add: iprev_append)
done
corollary iprev_append_eq3: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B |] ==>
iprev (iMin B) (A ∪ B) = Max A"
by (simp add: iprev_append not_greater_Max[of _ "iMin B"])
lemma inext_predicate_change_exists_aux: "!!a.
[| c = card (I \<down>≥ a \<down>< b); a < b; a ∈ I; b ∈ I; ¬ P a; P b |] ==>
∃n ∈ (I \<down>≥ a \<down>< b). ¬ P n ∧ P (inext n I)"
apply (subgoal_tac "0 < c")
prefer 2
apply clarify
apply (rule_tac x=a in not_empty_card_gr0_conv[OF nat_cut_less_finite, THEN iffD1, OF in_imp_not_empty, rule_format])
apply (simp add: i_cut_mem_iff)
apply (induct c)
apply simp
apply (subgoal_tac "a < inext a I")
prefer 2
apply (blast intro: inext_mono2)
apply (drule_tac x="inext a I" in meta_spec)
thm less_imp_inext_le[of _ b I]
apply (frule less_imp_inext_le[of _ b I], assumption+)
apply (case_tac "inext a I < b")
prefer 2
apply simp
apply (subgoal_tac "I \<down>≥ a \<down>< b = {a}")
prefer 2
apply (simp add: set_eq_iff i_cut_mem_iff, clarify)
apply (rule iffI)
prefer 2
apply simp
apply clarify
apply (case_tac "a < x")
apply (simp add: inext_min_step)
apply simp+
apply (subgoal_tac "I \<down>≥ inext a I = I \<down>> a")
prefer 2
apply (rule cut_greater_ge_inext_conv[symmetric], assumption)
apply (case_tac "finite I")
apply (simp, rule less_imp_neq)
thm Max_gr_iff[OF _ in_imp_not_empty]
apply (simp add: Max_gr_iff in_imp_not_empty)
apply (blast intro: inext_closed)
apply simp
apply (simp add: inext_closed)
apply (subgoal_tac "a ∉ (I \<down>> a \<down>< b)")
prefer 2
apply blast
apply (subgoal_tac "(I \<down>≥ a \<down>< b) = insert a (I \<down>> a \<down>< b)")
prefer 2
apply (simp add:
i_cut_commute_disj[of "op \<down>≥" "op \<down><"] i_cut_commute_disj[of "op \<down>>" "op \<down><"])
apply (simp add: cut_ge_greater_conv_if i_cut_mem_iff)
apply (simp add: card_insert_disjoint[OF nat_cut_less_finite])
apply (case_tac "P (inext a I)")
apply blast
apply (case_tac "card (I \<down>> a \<down>< b) = 0")
apply (drule card_0_eq[OF nat_cut_less_finite, THEN iffD1])
apply (simp add: cut_less_empty_iff)
apply (drule_tac x="inext a I" in bspec)
apply (blast intro: inext_closed)
apply simp
apply simp
done
lemma inext_predicate_change_exists: "
[| a ≤ b; a ∈ I; b ∈ I; ¬ P a; P b |] ==>
∃n∈I. a ≤ n ∧ n < b ∧ ¬ P n ∧ P (inext n I)"
apply (drule order_le_less[THEN iffD1], erule disjE)
prefer 2
apply blast
thm inext_predicate_change_exists_aux[OF refl]
apply (drule inext_predicate_change_exists_aux[OF refl], assumption+)
apply blast
done
lemma iprev_predicate_change_exists: "
[| a ≤ b; a ∈ I; b ∈ I; ¬ P b; P a |] ==>
∃n∈I. a < n ∧ n ≤ b ∧ ¬ P n ∧ P (iprev n I)"
apply (frule inext_predicate_change_exists[of a b I "λx. ¬ P x"], simp+)
apply clarify
apply (rule_tac x="inext n I" in bexI)
prefer 2
apply (blast intro: inext_closed)
apply (subgoal_tac "n < inext n I")
prefer 2
apply (blast intro: inext_mono2)
apply (frule_tac x=a and z="inext n I" in le_less_trans, assumption)
apply (frule less_imp_inext_le, assumption+)
apply (cut_tac n=n and I=I in iprev_inext)
apply (case_tac "finite I")
apply simp
apply (rule less_imp_neq)
apply (blast intro: inext_closed Max_ge order_less_le_trans)
apply simp+
done
corollary nat_Suc_predicate_change_exists: "
[| a ≤ b; ¬ P a; P b |] ==> ∃n≥a. n < b ∧ ¬ P n ∧ P (Suc n)"
apply (drule inext_predicate_change_exists[OF _ UNIV_I UNIV_I], assumption+)
apply (simp add: inext_UNIV)
done
corollary nat_pred_predicate_change_exists: "
[| a ≤ b; ¬ P b; P a |] ==> ∃n≤b. a < n ∧ ¬ P n ∧ P (n - Suc 0)"
apply (drule iprev_predicate_change_exists[OF _ UNIV_I UNIV_I], assumption+)
apply (fastsimp simp add: iprev_UNIV)
done
lemma inext_predicate_change_exists2_all: "
[| (a::nat) ≤ b; a ∈ I; b ∈ I; ¬ P a; ∀k ∈ I \<down>≥ b. P k |] ==>
∃n∈I. a ≤ n ∧ n < b ∧ ¬ P n ∧ (∀k ∈ I \<down>> n. P k)"
apply (drule order_le_less[THEN iffD1], erule disjE)
prefer 2
apply blast
thm inext_predicate_change_exists[of a b I "λn. if (n = a) then P n else (∀k∈I\<down>≥n. P k)"]
apply (frule inext_predicate_change_exists[OF less_imp_le,
of a b I "λn. if (n = a) then P n else (∀k∈I\<down>≥n. P k)"])
apply simp+
apply clarify
apply (rule_tac x=n in bexI)
prefer 2
apply assumption
apply (case_tac "a < n")
prefer 2
apply simp
apply (split split_if_asm)
apply (subgoal_tac "I \<down>> n = {}", simp+)
apply (drule not_sym)
thm cut_greater_ge_inext_conv
apply (rule ssubst[OF cut_greater_ge_inext_conv])
apply assumption
apply (case_tac "finite I")
prefer 2
apply simp
apply simp
apply (rule less_imp_neq)
thm inext_neq_imp_less
apply (drule inext_neq_imp_less)
apply (rule less_le_trans[OF _ Max_ge])
apply assumption+
apply (subgoal_tac "a < inext n I")
prefer 2
apply (blast intro: inext_mono order_less_le_trans)
apply (subgoal_tac "I \<down>≥ inext n I = I \<down>> n")
prefer 2
apply (rule cut_greater_ge_inext_conv[symmetric], assumption)
apply (case_tac "finite I")
apply simp
apply (rule less_imp_neq)
apply (blast intro: inext_closed Max_ge order_less_le_trans)
apply simp
apply simp
thm cut_greater_ge_conv_if
apply (simp add: cut_greater_ge_conv_if)
apply blast
done
corollary inext_predicate_change_exists2: "
[| (a::nat) ≤ b; a ∈ I; b ∈ I; ¬ P a; P b |] ==>
∃n∈I. a ≤ n ∧ n < b ∧ ¬ P n ∧ (∀k∈I. n < k ∧ k ≤ b --> P k)"
thm inext_predicate_change_exists2_all[of a b "I \<down>≤ b"]
apply (frule inext_predicate_change_exists2_all[of a b "I \<down>≤ b"])
apply (simp add: i_cut_mem_iff)+
apply fastsimp
apply blast
done
corollary nat_Suc_predicate_change_exists2_all: "
[| (a::nat) ≤ b; ¬ P a; ∀k≥b. P k |] ==>
∃n≥a. n < b ∧ ¬ P n ∧ (∀k>n. P k)"
apply (drule inext_predicate_change_exists2_all[rule_format, OF _ UNIV_I UNIV_I])
apply (simp add: i_cut_mem_iff Ball_def)+
done
corollary nat_Suc_predicate_change_exists2: "
[| (a::nat) ≤ b; ¬ P a; P b |] ==>
∃n≥a. n < b ∧ ¬ P n ∧ (∀k≤b. n < k --> P k)"
thm inext_predicate_change_exists2[of a b UNIV]
apply (drule inext_predicate_change_exists2[of a b UNIV])
apply simp+
apply blast
done
thm inext_predicate_change_exists2_all
lemma iprev_predicate_change_exists2_all: "
[| (a::nat) ≤ b; a ∈ I; b ∈ I; ¬ P b; ∀k∈I\<down>≤a. P k |] ==>
∃n∈I. a < n ∧ n ≤ b ∧ ¬ P n ∧ (∀k∈I\<down><n. P k)"
apply (drule order_le_less[THEN iffD1], erule disjE)
prefer 2
apply blast
thm iprev_predicate_change_exists[of a b I "λn. if (n = b) then P n else (∀k∈I\<down>≤n. P k)"]
apply (frule iprev_predicate_change_exists[OF less_imp_le,
of a b I "λn. if (n = b) then P n else (∀k∈I\<down>≤n. P k)"])
apply simp+
apply clarify
apply (rule_tac x=n in bexI)
prefer 2
apply assumption
apply (case_tac "a < n")
prefer 2
apply simp
apply simp
apply (subgoal_tac "iMin I < n")
prefer 2
apply (blast intro: order_le_less_trans)
apply (split split_if_asm)
apply clarsimp
apply (split split_if_asm)
apply simp
thm cut_less_le_iprev_conv[symmetric]
apply (simp add: cut_less_le_iprev_conv[symmetric])
apply blast
apply (split split_if_asm)
apply simp
apply (simp add: cut_less_le_iprev_conv[symmetric])
apply (clarsimp, rename_tac x)
apply (case_tac "x < n")
apply blast
apply simp
done
thm inext_predicate_change_exists2
corollary iprev_predicate_change_exists2: "
[| (a::nat) ≤ b; a ∈ I; b ∈ I; ¬ P b; P a |] ==>
∃n∈I. a < n ∧ n ≤ b ∧ ¬ P n ∧ (∀k∈I. a ≤ k ∧ k < n --> P k)"
thm iprev_predicate_change_exists2_all[of a b "I \<down>≥ a"]
apply (frule iprev_predicate_change_exists2_all[of a b "I \<down>≥ a"])
apply (simp add: i_cut_mem_iff)+
apply fastsimp
apply blast
done
thm nat_Suc_predicate_change_exists2_all
corollary nat_pred_predicate_change_exists2_all: "
[| (a::nat) ≤ b; ¬ P b; ∀k≤a. P k |] ==>
∃n>a. n ≤ b ∧ ¬ P n ∧ (∀k<n. P k)"
apply (drule iprev_predicate_change_exists2_all[rule_format, OF _ UNIV_I UNIV_I])
apply (simp add: i_cut_mem_iff Ball_def)+
done
thm nat_Suc_predicate_change_exists2
corollary nat_pred_predicate_change_exists2: "
[| (a::nat) ≤ b; ¬ P b; P a |] ==>
∃n>a. n ≤ b ∧ ¬ P n ∧ (∀k≥a. k < n --> P k)"
thm iprev_predicate_change_exists2[of a b UNIV]
apply (drule iprev_predicate_change_exists2[of a b UNIV])
apply simp+
apply blast
done
subsection {* @{text inext_nth} and @{text iprev_nth} -- nth element of a natural set *}
term inext
primrec
inext_nth :: "nat set => nat => nat"
where
"inext_nth I 0 = iMin I"
| "inext_nth I (Suc n) = inext (inext_nth I n) I"
(*<*)
(*
syntax (xsymbols)
"inext_nth" :: "nat set => nat => nat" ("(_ -> _)" [100, 100] 60)
syntax (HTML output)
"inext_nth" :: "nat set => nat => nat" ("(_ -> _)" [100, 100] 60)
*)
(*>*)
notation (xsymbols)
"inext_nth" ("(_ -> _)" [100, 100] 60)
notation (HTML output)
"inext_nth" ("(_ -> _)" [100, 100] 60)
term "(I -> a) + b"
term "(I -> n) ∈ I"
term "(A -> n) + (B -> n)"
lemma inext_nth_closed: "I ≠ {} ==> I -> n ∈ I"
apply (induct n)
apply (simp add: iMinI_ex2)
apply (simp add: inext_closed)
done
thm inext_image
lemma inext_nth_image: "
[| I ≠ {}; strict_mono_on f I |] ==> (f ` I) -> n = f (I -> n)"
apply (induct n)
apply (simp add: iMin_mono_on2 strict_mono_on_imp_mono_on)
apply (simp add: inext_image inext_nth_closed)
done
thm inext_mono2
lemma inext_nth_Suc_mono: "I -> n ≤ I -> Suc n"
by (simp add: inext_mono)
lemma inext_nth_mono: "a ≤ b ==> I -> a ≤ I -> b"
apply (induct b)
apply simp
apply (drule le_Suc_eq[THEN iffD1], erule disjE)
apply (rule_tac y="I -> b" in order_trans)
apply simp
apply (rule inext_nth_Suc_mono)
apply simp
done
thm inext_mono2
lemma inext_nth_Suc_mono2: "∃x∈I. I -> n < x ==> I -> n < I -> Suc n"
apply simp
apply (rule inext_mono2)
apply (blast intro: inext_nth_closed inext_mono2)+
done
lemma inext_nth_mono2: "∃x∈I. I -> a < x ==> (I -> a < I -> b) = (a < b)"
apply (subgoal_tac "I ≠ {}")
prefer 2
apply blast
apply (rule iffI)
apply (rule ccontr)
apply (simp add: linorder_not_less)
apply (drule inext_nth_mono[of _ _ I])
apply simp
apply clarify
apply (induct b)
apply blast
apply (drule less_Suc_eq[THEN iffD1], erule disjE)
apply (blast intro: order_less_le_trans inext_nth_Suc_mono)
apply (blast intro: inext_nth_Suc_mono2)
done
lemma inext_nth_mono2_infin: "
infinite I ==> (I -> a < I -> b) = (a < b)"
apply (drule infinite_nat_iff_unbounded[THEN iffD1])
apply (rule inext_nth_mono2)
apply blast
done
lemma inext_nth_Max_fix: "
[| finite I; I ≠ {}; I -> a = Max I; a ≤ b |] ==> I -> b = Max I"
apply (induct b)
apply simp
apply (drule le_Suc_eq[THEN iffD1], erule disjE)
apply (simp add: inext_Max)
apply blast
done
thm inext_cut_less_conv
lemma inext_nth_cut_less_conv: "
!!I. I -> n < t ==> (I \<down>< t) -> n = I -> n"
apply (case_tac "I = {}")
apply (simp add: cut_less_empty)
apply (induct n)
apply (simp add: cut_less_Min_eq cut_less_Min_not_empty)
apply simp
thm order_le_less_trans[OF inext_mono]
apply (frule order_le_less_trans[OF inext_mono])
thm inext_cut_less_conv
apply (simp add: inext_cut_less_conv)
done
thm
inext_cut_less_conv
inext_nth_cut_less_conv
lemma remove_Min_inext_nth_Suc_conv: "!!I.
Suc 0 < card I ∨ infinite I ==>
(I - {iMin I}) -> n = I -> Suc n"
(*apply (frule card_gt_0_iff[THEN iffD1, OF gr_implies_gr0], clarify)*)
apply (subgoal_tac "I ≠ {}")
prefer 2
thm card_gr0_imp_not_empty[OF gr_implies_gr0]
apply (blast dest: card_gr0_imp_not_empty[OF gr_implies_gr0])
apply (subgoal_tac "I - {iMin I} ≠ {}")
prefer 2
apply (rule ccontr, simp)
apply (erule disjE)
apply (drule card_mono[OF singleton_finite])
apply simp
apply (simp add: subset_singleton_conv)
apply (blast dest: infinite_imp_nonempty infinite_imp_not_singleton)
apply (induct n)
thm cut_greater_Min_eq_Diff[symmetric]
apply (simp add: cut_greater_Min_eq_Diff[symmetric] inext_def iMinI_ex2)
apply simp
thm ssubst[OF inext_def[THEN meta_eq_to_obj_eq], rule_format]
apply (rule_tac n="(inext (I -> n) I)" in ssubst[OF inext_def[THEN meta_eq_to_obj_eq], rule_format])
apply (rule_tac n="(inext (I -> n) I)" in ssubst[OF inext_def[THEN meta_eq_to_obj_eq], rule_format])
apply (simp add: inext_closed inext_nth_closed)
apply (subgoal_tac "inext (I -> n) I ≠ iMin I")
prefer 2
apply (erule disjE)
thm inext_neq_iMin_not_card_1
thm inext_neq_iMin_infin
apply (simp add: inext_neq_iMin_not_card_1 inext_neq_iMin_infin)+
apply (subgoal_tac "iMin I < (I -> Suc n)")
prefer 2
thm iMin_le[OF inext_nth_closed, rule_format]
apply (drule_tac n="Suc n" in iMin_le[OF inext_nth_closed, rule_format])
apply simp
apply (simp add: cut_greater_Diff cut_greater_singleton)
done
corollary remove_Min_inext_nth_Suc_conv_finite: "Suc 0 < card I ==> (I - {iMin I}) -> n = I -> Suc n"
by (simp add: remove_Min_inext_nth_Suc_conv)
corollary remove_Min_inext_nth_Suc_conv_infinite: "infinite I ==> (I - {iMin I}) -> n = I -> Suc n"
by (simp add: remove_Min_inext_nth_Suc_conv)
lemma remove_Max_eq: "[| finite I; I ≠ {}; n ≠ Max I |] ==> Max (I - {n}) = Max I"
by (rule Max_equality, simp+)
lemma remove_iMin_eq: "[| I ≠ {}; n ≠ iMin I |] ==> iMin (I - {n}) = iMin I"
by (rule iMin_equality, simp_all add: iMinI_ex2 iMin_le)
lemma remove_Min_eq: "[| finite I; I ≠ {}; n ≠ Min I |] ==> Min (I - {n}) = Min I"
by (rule Min_eqI, simp+)
lemma Max_le_iMin_conv_singleton: "[| finite I; I ≠ {} |] ==> (Max I ≤ iMin I) = (∃x. I = {x})"
by (simp add: iMin_Min_conv Max_le_Min_conv_singleton del: Max_le_iff Min_ge_iff)
lemma inext_nth_card_less_Max: "
!!I. Suc n < card I ==> I -> n < Max I"
thm card_gr0_imp_not_empty[OF less_trans[OF zero_less_Suc]]
apply (frule card_gr0_imp_not_empty[OF less_trans[OF zero_less_Suc]])
apply (frule card_gr0_imp_finite[OF less_trans[OF zero_less_Suc]])
apply (induct n)
apply (rule ccontr)
apply (simp add: linorder_not_less iMin_Min_conv del: Max_le_iff Min_ge_iff)
thm Max_le_Min_conv_singleton
apply (drule Max_le_Min_conv_singleton[THEN iffD1], assumption+)
apply clarsimp
apply (drule_tac x="I - {iMin I}" in meta_spec)
thm remove_Min_inext_nth_Suc_conv
apply (simp add: remove_Min_inext_nth_Suc_conv)
apply (subgoal_tac "¬ I ⊆ {iMin I}")
prefer 2
apply (rule ccontr, simp)
apply (drule card_mono[OF singleton_finite])
apply simp
apply (simp add: card_Diff_singleton iMin_in Suc_less_pred_conv)
apply (subgoal_tac "Max I ≠ iMin I")
prefer 2
apply (rule ccontr, simp)
thm Max_le_iMin_conv_singleton[THEN iffD1]
apply (frule Max_le_iMin_conv_singleton[THEN iffD1], clarsimp+)
thm remove_Max_eq
apply (simp add: remove_Max_eq Max_le_iMin_conv_singleton)
done
thm inext_nth_card_less_Max
lemma inext_nth_card_less_Max': "
n < card I - Suc 0 ==> I -> n < Max I"
by (simp add: inext_nth_card_less_Max)
lemma inext_nth_card_Max_aux: "
!!I. card I = Suc n ==> I -> n = Max I"
thm card_gr0_imp_not_empty[OF less_le_trans[OF zero_less_Suc, OF eq_imp_le[OF sym]]]
apply (frule card_gr0_imp_not_empty[OF less_le_trans[OF zero_less_Suc, OF eq_imp_le[OF sym]]])
apply (frule card_gr0_imp_finite[OF less_le_trans[OF zero_less_Suc, OF eq_imp_le[OF sym]]])
apply (induct n)
apply (clarsimp simp: card_1_singleton_conv)
apply simp
apply (cut_tac I=I and t="Max I" in nat_cut_less_finite)
apply (subgoal_tac "card (I \<down>< Max I) = Suc n")
prefer 2
apply (simp add: cut_less_le_conv cut_le_Max_all)
thm card_gr0_imp_not_empty[OF less_le_trans[OF zero_less_Suc, OF eq_imp_le[OF sym]], rule_format]
apply (frule_tac n=n in card_gr0_imp_not_empty[OF less_le_trans[OF zero_less_Suc, OF eq_imp_le[OF sym]], rule_format])
apply (subgoal_tac "Max (I \<down>< Max I) < iMin {Max I}")
prefer 2
apply (simp, blast)
apply (subgoal_tac "inext_nth I n < Max I")
prefer 2
thm inext_nth_card_less_Max
apply (simp add: inext_nth_card_less_Max)
apply (frule inext_nth_cut_less_conv[symmetric])
apply simp
apply (rule min_step_inext)
apply simp
apply (rule subsetD, rule cut_less_subset, rule Max_in, assumption+)
apply simp
apply (frule_tac A="I \<down>< Max I" and k=k in not_greater_Max, assumption)
apply (simp add: cut_less_mem_iff)
done
lemma inext_nth_card_Max_aux': "
!!I. [| finite I; I ≠ {} |] ==> I -> (card I - Suc 0) = Max I"
by (simp add: inext_nth_card_Max_aux not_empty_card_gr0_conv)
thm
inext_nth_card_Max_aux
inext_nth_card_Max_aux'
thm
inext_nth_card_less_Max
inext_nth_Max_fix
lemma inext_nth_card_Max: "
[| finite I; I ≠ {}; card I ≤ Suc n |] ==> I -> n = Max I"
thm inext_nth_Max_fix[of _ "card I - Suc 0"]
apply (rule inext_nth_Max_fix[of _ "card I - Suc 0"], assumption+)
apply (simp add: inext_nth_card_Max_aux')
apply simp
done
lemma inext_nth_card_Max': "
[| finite I; I ≠ {}; card I - Suc 0 ≤ n |] ==> I -> n = Max I"
by (simp add: inext_nth_card_Max)
thm
inext_nth_card_less_Max
inext_nth_card_Max
inext_nth_card_Max'
lemma inext_nth_singleton: "{a} -> n = a"
thm inext_nth_Max_fix[OF singleton_finite singleton_not_empty _ le0]
by (simp add: inext_nth_Max_fix[OF singleton_finite singleton_not_empty _ le0])
lemma inext_nth_eq_Min_conv: "
I ≠ {} ==> (I -> n = iMin I) = (n = 0 ∨ (∃a. I = {a}))"
apply (rule iffI)
apply (case_tac n, simp)
apply (rename_tac n')
apply (rule ccontr)
apply (drule_tac n="I -> n'" in inext_neq_iMin_not_singleton, simp)
apply simp
apply (erule disjE, simp)
apply (clarsimp simp: inext_nth_singleton)
done
lemma inext_nth_gr_Min_conv: "
I ≠ {} ==> (iMin I < I -> n) = (0 < n ∧ ¬(∃a. I = {a}))"
apply (rule subst[of "iMin I ≠ I -> n" "iMin I < I -> n"])
apply (frule iMin_le[OF inext_nth_closed[of _ n]])
apply (simp add: linorder_neq_iff)
apply (subst neq_commute[of "iMin I"])
apply (simp add: inext_nth_eq_Min_conv)
done
lemma inext_nth_gr_Min_conv_infinite: "
infinite I ==> (iMin I < I -> n) = (0 < n)"
by (simp add: inext_nth_gr_Min_conv infinite_imp_nonempty infinite_imp_not_singleton)
lemma inext_nth_cut_ge_inext_nth: "!!I b.
I ≠ {} ==> I \<down>≥ (I -> a) -> b = I -> (a + b)"
apply (induct a)
apply (simp add: cut_ge_Min_all)
apply (case_tac "card I = Suc 0")
apply (drule card_1_imp_singleton, clarify)
apply (simp add: inext_nth_singleton inext_singleton cut_ge_Min_all)
apply (subgoal_tac "Suc 0 < card I ∨ infinite I")
prefer 2
apply (rule ccontr, clarsimp simp: linorder_not_less not_empty_card_gr0_conv)
apply (case_tac "I - {iMin I} = {}")
apply (rule_tac t=I and s="{iMin I}" in subst, blast)
apply (simp (no_asm) add: inext_nth_singleton inext_singleton cut_ge_Min_all)
apply (simp add: subset_singleton_conv)
thm remove_Min_inext_nth_Suc_conv
apply (drule_tac x="I - {iMin I}" in meta_spec)
apply (drule_tac x=b in meta_spec)
apply (drule meta_mp, blast)
thm remove_Min_inext_nth_Suc_conv
apply (simp add: remove_Min_inext_nth_Suc_conv)
apply (simp add: cut_ge_Diff cut_ge_singleton)
apply (subgoal_tac "iMin I < inext (I -> a) I", simp)
apply (rule le_neq_trans[OF _ not_sym])
apply (simp add: iMin_le inext_closed inext_nth_closed)
apply (erule disjE)
apply (simp add: inext_neq_iMin_not_card_1 inext_neq_iMin_infin)+
done
thm inext_append_eq1
lemma inext_nth_append_eq1: "
[| finite A; A ≠ {}; Max A < iMin B; A -> n ≠ Max A |] ==>
(A ∪ B) -> n = A -> n"
apply (case_tac "B = {}", simp)
apply (induct n)
apply (simp add: iMin_Un del: Max_less_iff)
apply (rule min_eq)
thm iMin_le_Max
apply (blast intro: order_less_imp_le order_le_less_trans iMin_le_Max)
thm Max_ge[OF _ inext_nth_closed]
apply (frule_tac n="Suc n" in Max_ge[OF _ inext_nth_closed, rule_format], assumption)
apply (drule order_le_neq_trans, simp+)
thm order_le_less_trans[OF inext_mono]
apply (drule order_le_less_trans[OF inext_mono])
thm inext_append_eq1
apply (simp add: inext_append_eq1 inext_nth_closed)
done
thm inext_nth_append_eq1
thm inext_append_eq2
lemma inext_nth_card_append_eq1: "
!!A B.[| Max A < iMin B; n < card A |] ==>
(A ∪ B) -> n = A -> n"
apply (case_tac "B = {}", simp)
thm card_gr0_imp_finite[OF le_less_trans[OF le0]]
apply (frule card_gr0_imp_finite[OF le_less_trans[OF le0]])
apply (frule card_gr0_imp_not_empty[OF le_less_trans[OF le0]])
apply (drule Suc_leI[of n], drule order_le_less[THEN iffD1], erule disjE)
apply (rule inext_nth_append_eq1, assumption+)
apply (simp add: inext_nth_card_less_Max less_imp_neq)
thm inext_nth_card_Max[OF _ _ eq_imp_le[OF sym]]
apply (simp add: inext_nth_card_Max[OF _ _ eq_imp_le[OF sym]] del: Max_less_iff)
apply (induct n)
apply (frule card_1_imp_singleton[OF sym], erule exE)
apply (simp add: iMin_insert)
apply simp
apply (subgoal_tac "inext_nth A n < Max A")
prefer 2
apply (rule inext_nth_card_less_Max, simp)
thm inext_nth_append_eq1
apply (simp add: inext_nth_append_eq1)
apply (rule min_step_inext)
apply (simp add: inext_nth_closed)+
apply (rule conjI)
apply (subgoal_tac "k < A -> Suc n")
prefer 2
apply (subgoal_tac "A -> Suc n = Max A")
prefer 2
thm inext_nth_card_Max
apply (rule inext_nth_card_Max)
apply simp+
apply (rule_tac n="A -> n" and k=k in inext_min_step, simp+)
apply (rule not_less_iMin)
apply (rule_tac y="Max A" in order_less_trans)
apply simp+
done
thm inext_append_eq3
lemma inext_nth_card_append_eq3: "
[| finite A; B ≠ {}; Max A < iMin B |] ==>
(A ∪ B) -> (card A) = iMin B"
apply (case_tac "A = {}", simp)
apply (frule not_empty_card_gr0_conv[THEN iffD1], assumption)
thm subst[OF Suc_pred]
apply (rule subst[OF Suc_pred, of "card A"], assumption)
apply (simp only: inext_nth.simps) (* just "simp" wouldn't work, because it would revert "Suc (card A - Suc 0)" to "card A" instead of applying inext_nth.simps *)
thm inext_nth_card_append_eq1 inext_nth_card_Max' inext_append_eq3
apply (simp add: inext_nth_card_append_eq1 inext_nth_card_Max' inext_append_eq3)
done
lemma inext_nth_card_append_eq2: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B; card A ≤ n |] ==>
(A ∪ B) -> n = B -> (n - card A)"
thm inext_nth_cut_ge_inext_nth
apply (rule_tac t="(A ∪ B) -> n" and s="(A ∪ B) -> (card A + (n - card A))" in subst, simp)
thm inext_nth_cut_ge_inext_nth[symmetric]
apply (subst inext_nth_cut_ge_inext_nth[symmetric], simp)
apply (subst inext_nth_card_append_eq3, assumption+)
apply (simp add: cut_ge_Un cut_ge_Max_empty cut_ge_Min_all del: Max_less_iff)
done
thm inext_append
lemma inext_nth_card_append: "
[| finite A; A ≠ {}; B ≠ {}; Max A < iMin B |] ==>
(A ∪ B) -> n = (if n < card A then A -> n else B -> (n - card A))"
by (simp add: inext_nth_card_append_eq1 inext_nth_card_append_eq2)
lemma inext_nth_insert_Suc: "
[| I ≠ {}; a < iMin I |] ==> (insert a I) -> Suc n = I -> n"
apply (frule not_less_iMin)
apply (rule_tac t="I -> n" and s="(insert a I - {iMin (insert a I)}) -> n" in subst)
apply (simp add: iMin_insert min_eqL)
thm remove_Min_inext_nth_Suc_conv
apply (subst remove_Min_inext_nth_Suc_conv)
apply (case_tac "finite I")
apply (simp add: not_empty_card_gr0_conv)+
done
lemma inext_nth_cut_less_eq: "
n < card (I \<down>< t) ==> (I \<down>< t) -> n = I -> n"
apply (rule_tac t="I -> n" and s="(I \<down>< t ∪ I \<down>≥ t) -> n" in subst)
apply (simp add: cut_less_cut_ge_ident)
thm inext_nth_card_append_eq1
apply (case_tac "I \<down>≥ t = {}", simp)
apply (rule sym, rule inext_nth_card_append_eq1)
apply (drule card_gt_0_iff[THEN iffD1, OF gr_implies_gr0], clarify)
apply (simp add: Ball_def i_cut_mem_iff iMin_gr_iff)
apply simp
done
lemma less_card_cut_less_imp_inext_nth_less: "
n < card (I \<down>< t) ==> I -> n < t"
apply (case_tac "I \<down>< t = {}", simp)
apply (rule subst[OF inext_nth_cut_less_eq], assumption)
apply (rule cut_less_bound[OF inext_nth_closed], assumption)
done
lemma inext_nth_less_less_card_conv: "
I \<down>≥ t ≠ {} ==> (I -> n < t) = (n < card (I \<down>< t))"
apply (case_tac "I = {}", blast)
apply (case_tac "I \<down>< t = {}")
apply (simp add: linorder_not_less)
thm cut_less_empty_iff inext_nth_closed
apply (simp add: cut_less_empty_iff inext_nth_closed)
apply (rule iffI)
apply (rule ccontr, simp add: linorder_not_less)
apply (subgoal_tac "Max (I \<down>< t) < iMin (I \<down>≥ t)")
prefer 2
apply (simp add: nat_cut_less_finite iMin_gr_iff Ball_def i_cut_mem_iff)
thm ssubst[OF cut_less_cut_ge_ident[OF order_refl], of "λx. x -> n < t" _ t]
apply (drule ssubst[OF cut_less_cut_ge_ident[OF order_refl], of "λx. x -> n < t" _ t])
thm inext_nth_card_append_eq2[OF nat_cut_less_finite, of I t "I \<down>≥ t" n]
apply (drule inext_nth_card_append_eq2[OF nat_cut_less_finite, of I t "I \<down>≥ t" n], assumption+)
apply (simp add: inext_nth_card_append_eq2 nat_cut_less_finite)
apply (subgoal_tac "!!x. I \<down>≥ t -> x ≥ t")
prefer 2
apply (rule cut_ge_bound[OF inext_nth_closed], assumption)
apply (simp add: linorder_not_le[symmetric])
apply (rule subst[OF inext_nth_cut_less_eq], assumption)
apply (rule cut_less_bound[OF inext_nth_closed], assumption)
done
lemma cut_less_inext_nth_card_eq1: "
n < card I ∨ infinite I ==> card (I \<down>< (I -> n)) = n"
apply (case_tac "I = {}", simp)
apply (induct n)
apply (simp add: card_eq_0_iff nat_cut_less_finite cut_less_Min_empty)
apply (subgoal_tac "n < card I ∨ infinite I")
prefer 2
apply fastsimp
apply simp
apply (subgoal_tac "I -> n ≠ Max I ∨ infinite I")
prefer 2
thm inext_nth_card_less_Max[THEN less_imp_neq]
apply (blast dest: inext_nth_card_less_Max less_imp_neq)
apply (rule subst[OF cut_le_less_inext_conv[OF inext_nth_closed]], assumption+)
apply (simp add: cut_le_less_conv_if inext_nth_closed cut_less_mem_iff card_insert_if nat_cut_less_finite)
done
lemma cut_less_inext_nth_card_eq2: "
[| finite I; card I ≤ Suc n |] ==> card (I \<down>< (I -> n)) = card I - Suc 0"
apply (case_tac "I = {}", simp add: cut_less_empty)
apply (simp add: inext_nth_card_Max cut_less_Max_eq_Diff)
done
lemma cut_less_inext_nth_card_if: "
card (I \<down>< (I -> n)) = (
if (n < card I ∨ infinite I) then n else card I - Suc 0)"
by (simp add: cut_less_inext_nth_card_eq1 cut_less_inext_nth_card_eq2)
lemma cut_le_inext_nth_card_eq1: "
n < card I ∨ infinite I ==> card (I \<down>≤ (I -> n)) = Suc n"
apply (case_tac "I = {}", simp)
thm cut_le_less_inext_conv[OF inext_nth_closed]
apply (simp add: cut_le_less_conv_if inext_nth_closed card_insert_if nat_cut_less_finite cut_less_mem_iff cut_less_inext_nth_card_eq1)
done
lemma cut_le_inext_nth_card_eq2: "
[| finite I; card I ≤ Suc n |] ==> card (I \<down>≤ (I -> n)) = card I"
apply (case_tac "I = {}", simp add: cut_le_empty)
apply (simp add: inext_nth_card_Max cut_le_Max_all)
done
lemma cut_le_inext_nth_card_if: "
card (I \<down>≤ (I -> n)) = (
if (n < card I ∨ infinite I) then Suc n else card I)"
by (simp add: cut_le_inext_nth_card_eq1 cut_le_inext_nth_card_eq2)
term iprev
primrec
iprev_nth :: "nat set => nat => nat"
where
"iprev_nth I 0 = Max I"
| "iprev_nth I (Suc n) = iprev (iprev_nth I n) I"
thm inext_iprev
(*<*)
(*
syntax (xsymbols)
"iprev_nth" :: "nat set => nat => nat" ("(_ \<leftarrow> _)" [100, 100] 60)
syntax (HTML output)
"iprev_nth" :: "nat set => nat => nat" ("(_ \<leftarrow> _)" [100, 100] 60)
*)
(*>*)
notation (xsymbols)
"iprev_nth" ("(_ \<leftarrow> _)" [100, 100] 60)
notation (HTML output)
"iprev_nth" ("(_ \<leftarrow> _)" [100, 100] 60)
lemma iprev_nth_closed: "[| finite I; I ≠ {} |] ==> I \<leftarrow> n ∈ I"
apply (induct n)
apply simp
apply (simp add: iprev_closed)
done
thm iprev_image
lemma iprev_nth_image: "
[| finite I; I ≠ {}; strict_mono_on f I |] ==> (f ` I) \<leftarrow> n = f (I \<leftarrow> n)"
apply (induct n)
apply (simp add: Max_mono_on2 strict_mono_on_imp_mono_on)
apply (simp add: iprev_image iprev_nth_closed)
done
thm iprev_mono
lemma iprev_nth_Suc_mono: "I \<leftarrow> (Suc n) ≤ I \<leftarrow> n"
by (simp add: iprev_mono)
lemma iprev_nth_mono: "a ≤ b ==> I \<leftarrow> b ≤ I \<leftarrow> a"
apply (induct b)
apply simp
apply (drule le_Suc_eq[THEN iffD1], erule disjE)
apply (rule_tac y="iprev_nth I b" in order_trans)
apply (rule iprev_nth_Suc_mono)
apply simp
apply simp
done
lemma iprev_nth_Suc_mono2:
"[| finite I; ∃x∈I. x < I \<leftarrow> n |] ==> I \<leftarrow> (Suc n) < I \<leftarrow> n"
thm iprev_mono2
apply simp
apply (rule iprev_mono2)
thm iprev_nth_closed
apply (blast intro: iprev_nth_closed)+
done
lemma iprev_nth_mono2: "
[| finite I; ∃x∈I. x < I \<leftarrow> a |] ==> (I \<leftarrow> b < I \<leftarrow> a) = (a < b)"
apply (subgoal_tac "I ≠ {}")
prefer 2
apply blast
apply (rule iffI)
apply (rule ccontr)
apply (simp add: linorder_not_less)
apply (drule iprev_nth_mono[of _ _ I])
apply simp
apply clarify
apply (induct b)
apply blast
apply (drule less_Suc_eq[THEN iffD1], erule disjE)
apply (blast intro: order_le_less_trans iprev_nth_Suc_mono)
apply (blast intro: iprev_nth_Suc_mono2)
done
lemma iprev_nth_iMin_fix: "
[| I ≠ {}; I \<leftarrow> a = iMin I; a ≤ b |] ==> I \<leftarrow> b = iMin I"
apply (induct b)
apply simp
apply (drule le_Suc_eq[THEN iffD1], erule disjE)
apply (simp add: iprev_iMin)
apply blast
done
lemma iprev_nth_singleton: "{a} \<leftarrow> n= a"
thm iprev_nth_iMin_fix[OF singleton_not_empty _ le0]
by (simp add: iprev_nth_iMin_fix[OF singleton_not_empty _ le0])
subsection {* Induction over arbitrary natural sets using the functions @{text inext} and @{text iprev} *}
lemma inext_nth_surj_aux1:"
{x ∈ I. ¬(∃n. I -> n = x)} = {}"
(is "?S = {}"
is "{ x ∈ I. ?P x} = {}")
apply (case_tac "I = {}", blast)
proof (rule ccontr)
assume as_S_not_empty: "?S ≠ {}"
obtain S where s_S: "S = ?S" by blast
hence S_not_empty: "S ≠ {}"
using as_S_not_empty by blast
have s_not_ex: "!!x. [| x ∈ I; ?P x |] ==> x ∈ S"
using s_S by blast
have s_subset:"S ⊆ I"
using s_S by blast
have i_not_empty: "I ≠ {}"
using as_S_not_empty by blast
have s_iMin_S: "iMin S ∈ S"
thm iMinI_ex2
using S_not_empty by (simp add: iMinI_ex2)
hence s_iMin_i: "iMin S ∈ I"
using s_subset by blast
show False
proof cases
assume as:"iMin I < iMin S"
obtain prev where s_prev: "prev = iprev (iMin S) I" by blast
have s_prev_in: "prev ∈ I"
apply (simp add: s_prev)
thm iprev_closed[of "iMin S" i]
apply (rule iprev_closed)
apply (rule s_iMin_i)
done
have s_prev_next_min: "inext prev I = iMin S"
apply (simp add: s_prev)
thm inext_iprev[of I "iMin S"]
apply (rule inext_iprev)
apply (insert as, simp)
done
have s_prev_min_1: "prev < iMin S"
apply (simp only: s_prev)
thm iprev_mono2[of "iMin S" I]
apply (rule iprev_mono2[of "iMin S" ])
apply (rule s_iMin_i)
apply (rule_tac x="iMin I" in bexI)
apply (rule as)
apply (simp add: iMinI_ex2 i_not_empty)
done
hence prev_not_in_s: "prev ∉ S"
thm not_less_iMin
by (simp add: not_less_iMin)
have "∃n. I -> n = prev"
thm s_not_ex[of prev]
by (insert prev_not_in_s s_not_ex[of prev] s_prev_in, blast)
then obtain nPrev where s_nPrev: "I -> nPrev = prev" by blast
hence "I -> (Suc nPrev) = inext prev I" by simp
hence "I -> (Suc nPrev) = iMin S"
using s_prev_next_min by simp
hence "∃n. I -> n = iMin S" by blast
hence "iMin S ∉ S"
using s_iMin_i s_S by blast
thus False
using s_iMin_S by blast
next
assume as:"¬(iMin I < iMin S)"
have "iMin S = iMin I"
apply (insert s_subset S_not_empty as)
thm iMin_subset
apply (frule_tac A=S and B=I in iMin_subset)
by simp_all
hence "∃n. I -> n ∈ S"
apply (rule_tac x=0 in exI)
apply (insert s_iMin_S)
apply simp
done
thus False
using s_S by blast
qed
qed
term inext_nth
term "λn. I -> n"
lemma inext_nth_surj_on:"surj_on (λn. I -> n) UNIV I"
apply (simp add: surj_on_conv)
thm inext_nth_surj_aux1[of I]
by (insert inext_nth_surj_aux1[of I], blast)
corollary in_imp_ex_inext_nth: "x ∈ I ==> ∃n. x = I -> n"
thm surj_onD
thm surj_onD[where A=UNIV, simplified]
apply (rule surj_onD[where A=UNIV, simplified])
apply (rule inext_nth_surj_on)
apply assumption
done
lemma inext_induct: "
[| P (iMin I); !!n. [| n ∈ I; P n |] ==> P (inext n I); n ∈ I |] ==> P n"
thm image_nat_induct
thm image_nat_induct[where P=P and f="λn. I -> n" and I=I and a=n]
apply (rule_tac f="λn. I -> n" and I=I in image_nat_induct)
thm inext_nth_closed[OF in_imp_not_empty]
thm inext_nth_surj_on
apply (simp add: inext_nth_closed[OF in_imp_not_empty] inext_nth_surj_on)+
done
thm inext_induct
lemma iprev_nth_surj_aux1:"
finite I ==> { x ∈ I. ¬(∃n. I \<leftarrow> n = x)} = {}"
apply (case_tac "I = {}", blast)
proof (rule ccontr)
assume as_finite_i: "finite I"
let ?S = "{x ∈ I. ¬ (∃n. I \<leftarrow> n = x)}"
assume as_S_not_empty: "?S ≠ {}"
obtain S where s_S: "S = ?S" by blast
hence S_not_empty: "S ≠ {}"
using as_S_not_empty by blast
have s_not_ex: "!!x. [| x ∈ I; ¬(∃n. I \<leftarrow> n = x) |] ==> x ∈ S"
using s_S by blast
have s_subset:"S ⊆ I"
using s_S by blast
have i_not_empty: "I ≠ {}"
using as_S_not_empty by blast
from as_finite_i
have S_finite: "finite S"
using s_subset by (blast intro: finite_subset)
have s_Max_S: "Max S ∈ S"
thm Max_in
using S_not_empty S_finite by simp
hence s_Max_i: "Max S ∈ I"
using s_subset by blast
show False
proof cases
assume as:"Max S < Max I"
obtain next' where s_next: "next' = inext (Max S) I" by blast
have s_next_in: "next' ∈ I"
thm inext_closed[of "Max S" I]
by (simp add: s_next inext_closed s_Max_i)
have s_next_prev_max: "iprev next' I = Max S"
apply (simp add: s_next)
thm iprev_inext[of "Max S" I]
apply (rule iprev_inext)
apply (insert as, simp)
done
have s_next_max_1: "Max S < next'"
apply (simp add: s_next)
thm inext_mono2[of "Max S" I]
apply (rule inext_mono2[of "Max S" I])
apply (rule s_Max_i)
apply (rule_tac x="Max I" in bexI)
apply (rule as)
apply (simp add: as_finite_i i_not_empty)
done
hence next_not_in_s: "next' ∉ S"
using S_finite S_not_empty
apply clarify
thm Max_ge[of S next']
apply (drule Max_ge[of _ next'])
apply simp_all
done
have "∃n. I \<leftarrow> n = next'"
thm s_not_ex[of next']
by (insert next_not_in_s s_not_ex[of next'] s_next_in, blast)
then obtain nNext where s_nNext: "I \<leftarrow> nNext = next'" by blast
hence "I \<leftarrow> (Suc nNext) = iprev next' I" by simp
hence "I \<leftarrow> (Suc nNext) = Max S"
using s_next_prev_max by simp
hence "∃n. I \<leftarrow> n = Max S" by blast
hence "Max S ∉ S"
using s_Max_i s_S by blast
thus False
using s_Max_S by blast+
next
assume as:"¬(Max S < Max I)"
have "Max S = Max I"
apply (insert s_subset S_not_empty as_finite_i as)
thm Max_subset[of S I]
apply (drule Max_subset[of _ I])
by simp_all
hence "∃n. I \<leftarrow> n ∈ S"
apply (rule_tac x=0 in exI)
apply (insert s_Max_S)
apply simp
done
thus False
using s_S by blast
qed
qed
term iprev_nth
term "λn. iprev_nth I n"
lemma iprev_nth_surj_on: "finite I ==> surj_on (λn. I \<leftarrow> n) UNIV I"
apply (simp add: surj_on_def)
thm iprev_nth_surj_aux1[of I]
by (insert iprev_nth_surj_aux1[of I], blast)
corollary in_imp_ex_iprev_nth: "
[| finite I; x ∈ I |] ==> ∃n. x = I \<leftarrow> n"
thm surj_onD
thm surj_onD[of _ UNIV I, simplified]
apply (rule surj_onD[of _ UNIV I, simplified])
apply (rule iprev_nth_surj_on)
apply assumption+
done
lemma iprev_induct: "
[| P (Max I); !!n. [| n ∈ I; P n |] ==> P (iprev n I); finite I; n ∈ I |] ==> P n"
thm image_nat_induct
thm image_nat_induct[where P=P and f="λn. I \<leftarrow> n" and I=I and a=n]
apply (rule_tac f="λn. I \<leftarrow> n" and I=I in image_nat_induct)
thm iprev_nth_closed[OF _ in_imp_not_empty]
apply (simp add: iprev_nth_closed[OF _ in_imp_not_empty] iprev_nth_surj_on)+
done
thm
inext_induct
iprev_induct
subsection {* Natural intervals with @{text inext} and @{text iprev} *}
lemma inext_atLeast: "n ≤ t ==> inext t {n..} = Suc t"
apply (unfold inext_def)
apply (subgoal_tac "Suc t ∈ {n..} \<down>> t")
prefer 2
apply (simp add: cut_greater_mem_iff)
apply (simp add: in_imp_not_empty)
apply (rule iMin_equality, assumption)
apply (simp add: cut_greater_mem_iff)
done
lemma iprev_atLeast': "n ≤ t ==> iprev (Suc t) {n..} = t"
apply (rule subst[OF inext_atLeast], assumption)
apply (rule iprev_inext_infin[OF infinite_atLeast])
done
lemma iprev_atLeast: "n < t ==> iprev t {n..} = t - Suc 0"
by (insert iprev_atLeast'[of n "t - Suc 0"], simp)
lemma inext_atMost: "t < n ==> inext t {..n} = Suc t"
apply (unfold inext_def)
apply (subgoal_tac "Suc t ∈ {..n} \<down>> t")
prefer 2
apply (simp add: cut_greater_mem_iff)
apply (simp add: in_imp_not_empty)
apply (rule iMin_equality, assumption)
apply (simp add: cut_greater_mem_iff)
done
lemma iprev_atMost: "t ≤ n ==> iprev t {..n} = t - Suc 0"
apply (case_tac t)
apply simp
thm subst[OF iMin_atMost[of n]]
apply (rule subst[OF iMin_atMost[of n]])
apply (rule iprev_iMin)
apply simp
apply (drule Suc_le_lessD)
apply (rule subst[OF inext_atMost], assumption)
apply (simp add: Max_atMost iprev_inext_fin)
done
lemma inext_lessThan: "Suc t < n ==> inext t {..<n} = Suc t"
apply (rule subst[OF Suc_pred, of n], simp)
apply (subst lessThan_Suc_atMost)
apply (simp add: inext_atMost)
done
lemma iprev_lessThan: "t < n ==> iprev t {..<n} = t - Suc 0"
apply (case_tac n, simp)
apply (simp add: lessThan_Suc_atMost iprev_atMost)
done
lemma inext_atLeastAtMost: "[| m ≤ t; t < n |] ==> inext t {m..n} = Suc t"
by (simp add: atLeastAtMost_def cut_le_Int_conv[symmetric] inext_atLeast inext_cut_le_conv)
lemma iprev_atLeastAtMost: "[| m < t; t ≤ n |] ==> iprev t {m..n} = t - Suc 0"
by (simp add: atLeastAtMost_def cut_le_Int_conv[symmetric] iprev_atLeast iprev_cut_le_conv)
lemma iprev_atLeastAtMost': "[| m ≤ t; t < n |] ==> iprev (Suc t) {m..n} = t"
by (simp add: iprev_atLeastAtMost[of _ "Suc t"])
lemma inext_nth_atLeast : "{n..} -> a = n + a"
apply (induct a, simp add: iMin_atLeast)
apply (simp add: inext_atLeast)
done
lemma inext_nth_atLeastAtMost: "[| a ≤ n - m; m ≤ n |] ==> {m..n} -> a = m + a"
apply (induct a, simp add: iMin_atLeastAtMost)
apply (simp add: inext_atLeastAtMost)
done
lemma iprev_nth_atLeastAtMost: "[| a ≤ n - m; m ≤ n |] ==> {m..n} \<leftarrow> a = n - a"
apply (induct a, simp add: Max_atLeastAtMost)
apply (simp add: iprev_atLeastAtMost)
done
lemma inext_nth_atMost: "a ≤ n ==> {..n} -> a = a"
apply (insert inext_nth_atLeastAtMost[of a n 0])
apply (simp add: atMost_atLeastAtMost_0_conv)
done
lemma iprev_nth_atMost: "a ≤ n ==> {..n} \<leftarrow> a = n - a"
apply (insert iprev_nth_atLeastAtMost[of a n 0])
apply (simp add: atMost_atLeastAtMost_0_conv)
done
lemma inext_nth_lessThan : "a < n ==> {..<n} -> a = a"
apply (case_tac n, simp)
apply (simp add: lessThan_Suc_atMost inext_nth_atMost)
done
lemma iprev_nth_lessThan: "a < n ==> {..<n} \<leftarrow> a = n - Suc a"
apply (case_tac n, simp)
apply (simp add: lessThan_Suc_atMost iprev_nth_atMost)
done
lemma inext_nth_UNIV: "UNIV -> a = a"
by (simp add: inext_nth_atLeast del: atLeast_0 add: atLeast_0[symmetric])
subsection {* Further result for @{text inext_nth} and @{text iprev_nth} *}
thm inext_iprev
lemma inext_iprev_nth_Suc: "
iMin I ≠ I \<leftarrow> n ==> inext (I \<leftarrow> Suc n) I = I \<leftarrow> n"
by (simp add: inext_iprev)
lemma inext_iprev_nth_pred: "
[| finite I; iMin I ≠ I \<leftarrow> (n - Suc 0) |] ==>
inext (I \<leftarrow> n) I = I \<leftarrow> (n - Suc 0)"
apply (case_tac n)
apply (simp add: inext_Max)
apply (simp add: inext_iprev)
done
lemma iprev_inext_nth_Suc: "
I -> n ≠ Max I ∨ infinite I ==> iprev (I -> Suc n) I = I -> n"
by (simp add: iprev_inext)
lemma iprev_inext_nth_pred: "
I -> (n - Suc 0) ≠ Max I ∨ infinite I ==>
iprev (I -> n) I = I -> (n - Suc 0)"
apply (case_tac n)
apply (simp add: iprev_iMin)
apply (simp add: iprev_inext)
done
thm inext_imirror_iprev_conv
lemma inext_nth_imirror_iprev_nth_conv: "
[| finite I; I ≠ {} |] ==>
(imirror I) -> n = mirror_elem (I \<leftarrow> n) I"
apply (induct n)
apply (simp add: imirror_iMin mirror_elem_Max)
apply (simp add: inext_imirror_iprev_conv' iprev_nth_closed)
done
corollary inext_nth_imirror_iprev_nth_conv2: "
[| finite I; I ≠ {} |] ==>
mirror_elem ((imirror I) \<leftarrow> n) I = I -> n"
thm inext_nth_imirror_iprev_nth_conv[OF imirror_finite imirror_not_empty]
apply (frule inext_nth_imirror_iprev_nth_conv[OF imirror_finite imirror_not_empty, of _ n], assumption)
apply (simp add: imirror_imirror_ident mirror_elem_imirror)
done
lemma iprev_nth_imirror_inext_nth_conv: "
[| finite I; I ≠ {} |] ==>
(imirror I) \<leftarrow> n = mirror_elem (I -> n) I"
apply (induct n)
apply (simp add: imirror_Max mirror_elem_Min)
apply (simp add: iprev_imirror_inext_conv' inext_nth_closed)
done
corollary iprev_nth_imirror_inext_nth_conv2: "
[| finite I; I ≠ {} |] ==>
mirror_elem ((imirror I) -> n) I = (I \<leftarrow> n)"
thm iprev_nth_imirror_inext_nth_conv[OF imirror_finite imirror_not_empty]
apply (frule iprev_nth_imirror_inext_nth_conv[OF imirror_finite imirror_not_empty, of _ n], assumption)
apply (simp add: imirror_imirror_ident mirror_elem_imirror)
done
thm inext_nth_card_less_Max
lemma iprev_nth_card_greater_iMin: "Suc n < card I ==> iMin I < I \<leftarrow> n"
apply (subgoal_tac "I ≠ {}" "finite I")
prefer 2
apply (rule card_gr0_imp_finite, simp)
prefer 2
apply (rule card_gr0_imp_not_empty, simp)
thm subst[OF iprev_nth_imirror_inext_nth_conv2]
apply (subst iprev_nth_imirror_inext_nth_conv2[symmetric], assumption+)
thm subst[OF mirror_elem_Max]
apply (subst mirror_elem_Max[symmetric], assumption+)
thm subst[OF mirror_elem_imirror, of I]
apply (subst mirror_elem_imirror[symmetric], assumption)
apply (subst mirror_elem_imirror[symmetric], assumption)
apply (frule imirror_finite, frule imirror_not_empty)
thm mirror_elem_less_conv
apply (rule mirror_elem_less_conv[THEN iffD2])
apply assumption
apply (rule inext_nth_closed, assumption)
apply (rule subst[OF imirror_Max], assumption)
apply (rule Max_in, assumption+)
apply (rule subst[OF imirror_Max], assumption)
thm inext_nth_card_less_Max
apply (simp add: inext_nth_card_less_Max imirror_card)
done
lemma iprev_nth_card_iMin: "
[| finite I; I ≠ {}; card I ≤ Suc n |] ==> I \<leftarrow> n = iMin I"
thm subst[OF iprev_nth_imirror_inext_nth_conv2]
apply (subst iprev_nth_imirror_inext_nth_conv2[symmetric], assumption+)
thm subst[OF mirror_elem_Max]
apply (subst mirror_elem_Max[symmetric], assumption+)
thm subst[OF mirror_elem_imirror, of I]
apply (subst mirror_elem_imirror[symmetric], assumption)
apply (subst mirror_elem_imirror[symmetric], assumption)
thm subst[OF imirror_Max]
apply (rule subst[OF imirror_Max], assumption)
apply (frule imirror_finite, frule imirror_not_empty)
thm mirror_elem_eq_conv'
apply (simp add: mirror_elem_eq_conv' inext_nth_closed inext_nth_card_Max imirror_card)
done
lemma iprev_nth_card_iMin': "
[| finite I; I ≠ {}; card I - Suc 0 ≤ n |] ==> I \<leftarrow> n = iMin I"
by (simp add: iprev_nth_card_iMin)
end