Theory SetIntervalCut

(*  Title:      SetIntervalCut.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Cutting linearly ordered and natural sets›

theory SetIntervalCut
imports SetInterval2
begin

subsection ‹Set restriction›

text ‹
  A set to set function ‹f› is a ‹set restriction›,
  if there exists a predicate ‹P›,
  so that for every set ‹s› the function result ‹f s›
  contains all its elements fulfilling ‹P››

definition set_restriction :: "('a set ⇒ 'a set) ⇒ bool"
  where "set_restriction f ≡ ∃P. ∀A. f A = {x ∈ A. P x}"

lemma set_restrictionD: "set_restriction f ⟹ ∃P. ∀A. f A = {x ∈ A. P x}"
unfolding set_restriction_def by blast
lemma set_restrictionD_spec: "set_restriction f ⟹ ∃P. f A = {x ∈ A. P x}"
unfolding set_restriction_def by blast
lemma set_restrictionI: "f = (λA. {x ∈ A. P x}) ⟹ set_restriction f"
unfolding set_restriction_def by blast

lemma set_restriction_comp: "
  ⟦ set_restriction f; set_restriction g ⟧ ⟹ set_restriction (f ∘ g)"
apply (unfold set_restriction_def)
apply (elim exE, rename_tac P1 P2)
apply (rule_tac x="λx. P1 x ∧ P2 x" in exI)
apply fastforce
done
lemma set_restriction_commute: "
  ⟦ set_restriction f; set_restriction g ⟧ ⟹ f (g I) = g (f I)"
unfolding set_restriction_def by fastforce

text ‹Constructs a set restriction function with the given restriction predicate›
definition
  set_restriction_fun :: "('a ⇒ bool) ⇒ ('a set ⇒ 'a set)"
where
  "set_restriction_fun P ≡ λA. {x ∈ A. P x}"

lemma set_restriction_fun_is_set_restriction: "
  set_restriction (set_restriction_fun P)"
unfolding set_restriction_def set_restriction_fun_def by blast

lemma set_restriction_Int_conv:
  "set_restriction f = (∃B. ∀A. f A = A ∩ B)"
apply (unfold set_restriction_def)
apply (rule iffI)
apply (erule exE, rule_tac x="Collect P" in exI, blast)
apply (erule exE, rule_tac x="λx. x ∈ B" in exI, blast)
done

lemma set_restriction_Un: "
  set_restriction f ⟹ f (A ∪ B) = f A ∪ f B"
unfolding set_restriction_def by fastforce
lemma set_restriction_Int: "
  set_restriction f ⟹ f (A ∩ B) = f A ∩ f B"
unfolding set_restriction_def by fastforce
lemma set_restriction_Diff: "
  set_restriction f ⟹ f (A - B) = f A - f B"
unfolding set_restriction_def by fastforce
lemma set_restriction_mono: "
  ⟦ set_restriction f; A ⊆ B ⟧ ⟹ f A ⊆ f B"
unfolding set_restriction_def by fastforce
lemma set_restriction_absorb: "
  set_restriction f ⟹ f (f A) = f A"
unfolding set_restriction_def by fastforce
lemma set_restriction_empty: "
  set_restriction f ⟹ f {} = {}"
unfolding set_restriction_def by blast
lemma set_restriction_non_empty_imp: "
  ⟦ set_restriction f; f A ≠ {} ⟧ ⟹ A ≠ {}"
unfolding set_restriction_def by blast
lemma set_restriction_subset: "
  set_restriction f ⟹ f A ⊆ A"
unfolding set_restriction_def by blast
lemma set_restriction_finite: "
  ⟦ set_restriction f; finite A ⟧ ⟹ finite (f A)"
unfolding set_restriction_def by fastforce
lemma set_restriction_card: "
  ⟦ set_restriction f; finite A ⟧ ⟹
  card (f A) = card A - card {a ∈ A. f {a} = {}}"
apply (unfold set_restriction_def)
apply (subgoal_tac "{a ∈ A. f {a} = {}} ⊆ A")
 prefer 2
 apply blast
apply (frule finite_subset, simp)
apply (simp only: card_Diff_subset[symmetric])
apply (rule arg_cong[where f=card])
apply fastforce
done

lemma set_restriction_card_le: "
  ⟦ set_restriction f; finite A ⟧ ⟹ card (f A) ≤ card A"
by (simp add: set_restriction_card)

lemma set_restriction_not_in_imp: "
  ⟦ set_restriction f; x ∉ A ⟧ ⟹ x ∉ f A"
unfolding set_restriction_def by blast

lemma set_restriction_in_imp: "
  ⟦ set_restriction f; x ∈ f A ⟧ ⟹ x ∈ A"
unfolding set_restriction_def by blast

lemma set_restriction_fun_singleton: "
  set_restriction_fun P {a} = (if P a then {a} else {})"
unfolding set_restriction_fun_def by force
lemma set_restriction_fun_all_conv: "
  ((set_restriction_fun P) A = A) = (∀x∈A. P x)"
unfolding set_restriction_fun_def by blast
lemma set_restriction_fun_empty_conv: "
  ((set_restriction_fun P) A = {}) = (∀x∈A. ¬ P x)"
unfolding set_restriction_fun_def by blast


subsection ‹Cut operators for sets/intervals›

subsubsection ‹Definitions and basic lemmata for cut operators›

definition cut_le :: "'a::linorder set ⇒ 'a ⇒ 'a set"   (infixl ‹↓≤› 100)
  where "I ↓≤ t ≡ {x∈I. x ≤ t}"

definition cut_less :: "'a::linorder set ⇒ 'a ⇒ 'a set"  (infixl ‹↓<› 100)
  where "I ↓< t ≡ {x∈I. x < t}"

definition cut_ge :: "'a::linorder set ⇒ 'a ⇒ 'a set"  (infixl ‹↓≥› 100)
  where "I ↓≥ t ≡ {x∈I. t ≤ x}"

definition cut_greater :: "'a::linorder set ⇒ 'a ⇒ 'a set"  (infixl ‹↓>› 100)
  where "I ↓> t ≡ {x∈I. t < x}"

lemmas i_cut_defs =
  cut_le_def cut_less_def
  cut_ge_def cut_greater_def

lemma cut_le_mem_iff: "x ∈ I ↓≤ t = (x ∈ I ∧ x ≤ t)"
by (unfold cut_le_def, blast)

lemma cut_less_mem_iff: "x ∈ I ↓< t = (x ∈ I ∧ x < t)"
by (unfold cut_less_def, blast)

lemma cut_ge_mem_iff: "x ∈ I ↓≥ t = (x ∈ I ∧ t ≤ x)"
by (unfold cut_ge_def, blast)

lemma cut_greater_mem_iff: "x ∈ I ↓> t = (x ∈ I ∧ t < x)"
by (unfold cut_greater_def, blast)

lemmas i_cut_mem_iff =
  cut_le_mem_iff cut_less_mem_iff
  cut_ge_mem_iff cut_greater_mem_iff

lemma
  cut_leI [intro!]:      "x ∈ I ⟹ x ≤ t ⟹ x ∈ I ↓≤ t" and
  cut_lessI [intro!]:    "x ∈ I ⟹ x < t ⟹ x ∈ I ↓< t" and
  cut_geI [intro!]:      "x ∈ I ⟹ x ≥ t ⟹ x ∈ I ↓≥ t" and
  cut_greaterI [intro!]: "x ∈ I ⟹ x > t ⟹ x ∈ I ↓> t"
by (simp_all add: i_cut_mem_iff)

lemma
  cut_leE [elim!]:      "x ∈ I ↓≤ t ⟹ (x ∈ I ⟹ x ≤ t ⟹ P) ⟹ P" and
  cut_lessE [elim!]:    "x ∈ I ↓< t ⟹ (x ∈ I ⟹ x < t ⟹ P) ⟹ P" and
  cut_geE [elim!]:      "x ∈ I ↓≥ t ⟹ (x ∈ I ⟹ x ≥ t ⟹ P) ⟹ P" and
  cut_greaterE [elim!]: "x ∈ I ↓> t ⟹ (x ∈ I ⟹ x > t ⟹ P) ⟹ P"
by (simp_all add: i_cut_mem_iff)


lemma
  cut_less_bound:    "n ∈ I ↓< t ⟹ n < t" and
  cut_le_bound:      "n ∈ I ↓≤ t ⟹ n ≤ t" and
  cut_greater_bound: "n ∈ i ↓> t ⟹ t < n" and
  cut_ge_bound:      "n ∈ i ↓≥ t ⟹ t ≤ n"
unfolding i_cut_defs by simp_all

lemmas i_cut_bound =
  cut_less_bound cut_le_bound
  cut_greater_bound cut_ge_bound

lemma
  cut_le_Int_conv: "I ↓≤ t = I ∩ {..t}" and
  cut_less_Int_conv: "I ↓< t = I ∩ {..<t}" and
  cut_ge_Int_conv: "I ↓≥ t = I ∩ {t..}" and
  cut_greater_Int_conv: "I ↓> t = I ∩ {t<..}"
unfolding i_cut_defs by blast+

lemmas i_cut_Int_conv =
  cut_le_Int_conv cut_less_Int_conv
  cut_ge_Int_conv cut_greater_Int_conv

lemma
  cut_le_Diff_conv: "I ↓≤ t = I - {t<..}" and
  cut_less_Diff_conv: "I ↓< t = I - {t..}" and
  cut_ge_Diff_conv: "I ↓≥ t = I - {..<t}" and
  cut_greater_Diff_conv: "I ↓> t = I - {..t}"
by (fastforce simp: i_cut_defs)+
lemmas i_cut_Diff_conv =
  cut_le_Diff_conv cut_less_Diff_conv
  cut_ge_Diff_conv cut_greater_Diff_conv


subsubsection ‹Basic results for cut operators›

lemma
  cut_less_eq_set_restriction_fun':    "(λI. I ↓< t) = set_restriction_fun (λx. x < t)" and
  cut_le_eq_set_restriction_fun':      "(λI. I ↓≤ t) = set_restriction_fun (λx. x ≤ t)" and
  cut_greater_eq_set_restriction_fun': "(λI. I ↓> t) = set_restriction_fun (λx. x > t)" and
  cut_ge_eq_set_restriction_fun':      "(λI. I ↓≥ t) = set_restriction_fun (λx. x ≥ t)"
unfolding set_restriction_fun_def i_cut_defs by blast+
lemmas i_cut_eq_set_restriction_fun' =
  cut_less_eq_set_restriction_fun' cut_le_eq_set_restriction_fun'
  cut_greater_eq_set_restriction_fun' cut_ge_eq_set_restriction_fun'

lemma
  cut_less_eq_set_restriction_fun:    "I ↓< t = set_restriction_fun (λx. x < t) I" and
  cut_le_eq_set_restriction_fun:      "I ↓≤ t = set_restriction_fun (λx. x ≤ t) I" and
  cut_greater_eq_set_restriction_fun: "I ↓> t = set_restriction_fun (λx. x > t) I" and
  cut_ge_eq_set_restriction_fun:      "I ↓≥ t = set_restriction_fun (λx. x ≥ t) I"
by (simp_all only: i_cut_eq_set_restriction_fun'[symmetric])
lemmas i_cut_eq_set_restriction_fun =
  cut_less_eq_set_restriction_fun cut_le_eq_set_restriction_fun
  cut_greater_eq_set_restriction_fun cut_ge_eq_set_restriction_fun

lemma i_cut_set_restriction_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥);
    f = (λI. cut_op I t)  ⟧ ⟹ set_restriction f"
apply safe
apply (simp_all only: i_cut_eq_set_restriction_fun set_restriction_fun_is_set_restriction)
done

corollary
  i_cut_less_set_restriction:    "set_restriction (λI. I ↓< t)" and
  i_cut_le_set_restriction:      "set_restriction (λI. I ↓≤ t)" and
  i_cut_greater_set_restriction: "set_restriction (λI. I ↓> t)" and
  i_cut_ge_set_restriction:      "set_restriction (λI. I ↓≥ t)"
by (simp_all only: i_cut_eq_set_restriction_fun set_restriction_fun_is_set_restriction)

lemmas i_cut_set_restriction =
  i_cut_le_set_restriction i_cut_less_set_restriction
  i_cut_ge_set_restriction i_cut_greater_set_restriction

lemma i_cut_commute_disj: "⟦
  cut_op1 = (↓<) ∨ cut_op1 = (↓≤) ∨
  cut_op1 = (↓>) ∨ cut_op1 = (↓≥);
  cut_op2 = (↓<) ∨ cut_op2 = (↓≤) ∨
  cut_op2 = (↓>) ∨ cut_op2 = (↓≥) ⟧ ⟹
  cut_op2 (cut_op1 I t1) t2 = cut_op1 (cut_op2 I t2) t1"
apply (rule set_restriction_commute)
apply (simp_all only: i_cut_set_restriction_disj)
done

lemma
  cut_less_empty:    "{} ↓< t = {}" and
  cut_le_empty:      "{} ↓≤ t = {}" and
  cut_greater_empty: "{} ↓> t = {}" and
  cut_ge_empty:      "{} ↓≥ t = {}"
by blast+

lemmas i_cut_empty =
  cut_less_empty cut_le_empty
  cut_greater_empty cut_ge_empty

lemma
  cut_less_not_empty_imp:    "I ↓< t ≠ {} ⟹ I ≠ {}" and
  cut_le_not_empty_imp:      "I ↓≤ t ≠ {} ⟹ I ≠ {}" and
  cut_greater_not_empty_imp: "I ↓> t ≠ {} ⟹ I ≠ {}" and
  cut_ge_not_empty_imp:      "I ↓≥ t ≠ {} ⟹ I ≠ {}"
by blast+


lemma
  cut_less_singleton:    "{a} ↓< t = (if a < t then {a} else {})" and
  cut_le_singleton:      "{a} ↓≤ t = (if a ≤ t then {a} else {})" and
  cut_greater_singleton: "{a} ↓> t = (if a > t then {a} else {})" and
  cut_ge_singleton:      "{a} ↓≥ t = (if a ≥ t then {a} else {})"
by (rule i_cut_eq_set_restriction_fun[THEN ssubst], simp only: set_restriction_fun_singleton)+
lemmas i_cut_singleton =
  cut_le_singleton cut_less_singleton
  cut_ge_singleton cut_greater_singleton




lemma
  cut_less_subset:    "I ↓< t ⊆ I" and
  cut_le_subset:      "I ↓≤ t ⊆ I" and
  cut_greater_subset: "I ↓> t ⊆ I" and
  cut_ge_subset:      "I ↓≥ t ⊆ I"
by (simp_all only: i_cut_set_restriction[THEN set_restriction_subset])

lemmas i_cut_subset =
  cut_less_subset cut_le_subset
  cut_greater_subset cut_ge_subset

lemma i_cut_Un_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥) ⟧
  ⟹ cut_op (A ∪ B) t = cut_op A t ∪ cut_op B t"
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], simp)
by (rule set_restriction_Un)


corollary
  cut_less_Un:    "(A ∪ B) ↓< t = A ↓< t ∪ B ↓< t" and
  cut_le_Un:      "(A ∪ B) ↓≤ t = A ↓≤ t ∪ B ↓≤ t" and
  cut_greater_Un: "(A ∪ B) ↓> t = A ↓> t ∪ B ↓> t" and
  cut_ge_Un:      "(A ∪ B) ↓≥ t = A ↓≥ t ∪ B ↓≥ t"
by (rule i_cut_Un_disj, blast)+
lemmas i_cut_Un =
  cut_less_Un cut_le_Un
  cut_greater_Un cut_ge_Un




lemma i_cut_Int_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥) ⟧
  ⟹ cut_op (A ∩ B) t = cut_op A t ∩ cut_op B t"
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], simp)
by (rule set_restriction_Int)

lemma
  cut_less_Int:    "(A ∩ B) ↓< t = A ↓< t ∩ B ↓< t" and
  cut_le_Int:      "(A ∩ B) ↓≤ t = A ↓≤ t ∩ B ↓≤ t" and
  cut_greater_Int: "(A ∩ B) ↓> t = A ↓> t ∩ B ↓> t" and
  cut_ge_Int:      "(A ∩ B) ↓≥ t = A ↓≥ t ∩ B ↓≥ t"
by blast+
lemmas i_cut_Int =
  cut_less_Int cut_le_Int
  cut_greater_Int cut_ge_Int

lemma
  cut_less_Int_left:    "(A ∩ B) ↓< t = A ↓< t ∩ B" and
  cut_le_Int_left:      "(A ∩ B) ↓≤ t = A ↓≤ t ∩ B" and
  cut_greater_Int_left: "(A ∩ B) ↓> t = A ↓> t ∩ B" and
  cut_ge_Int_left:      "(A ∩ B) ↓≥ t = A ↓≥ t ∩ B"
by blast+
lemmas i_cut_Int_left =
  cut_less_Int_left cut_le_Int_left
  cut_greater_Int_left cut_ge_Int_left

lemma
  cut_less_Int_right:    "(A ∩ B) ↓< t = A ∩ B ↓< t" and
  cut_le_Int_right:      "(A ∩ B) ↓≤ t = A ∩ B ↓≤ t" and
  cut_greater_Int_right: "(A ∩ B) ↓> t = A ∩ B ↓> t" and
  cut_ge_Int_right:      "(A ∩ B) ↓≥ t = A ∩ B ↓≥ t"
by blast+
lemmas i_cut_Int_right =
  cut_less_Int_right cut_le_Int_right
  cut_greater_Int_right cut_ge_Int_right

lemma i_cut_Diff_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥) ⟧
  ⟹ cut_op (A - B) t = cut_op A t - cut_op B t"
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], simp)
by (rule set_restriction_Diff)
corollary
  cut_less_Diff:    "(A - B) ↓< t = A ↓< t - B ↓< t" and
  cut_le_Diff:      "(A - B) ↓≤ t = A ↓≤ t - B ↓≤ t" and
  cut_greater_Diff: "(A - B) ↓> t = A ↓> t - B ↓> t" and
  cut_ge_Diff:      "(A - B) ↓≥ t = A ↓≥ t - B ↓≥ t"
by (rule i_cut_Diff_disj, blast)+
lemmas i_cut_Diff =
  cut_less_Diff cut_le_Diff
  cut_greater_Diff cut_ge_Diff

lemma i_cut_subset_mono_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥); A ⊆ B ⟧
  ⟹ cut_op A t ⊆ cut_op B t"
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], simp)
by (rule set_restriction_mono[where f="λI. cut_op I t"])

corollary
  cut_less_subset_mono:    "A ⊆ B ⟹ A ↓< t ⊆ B ↓< t" and
  cut_le_subset_mono:      "A ⊆ B ⟹ A ↓≤ t ⊆ B ↓≤ t" and
  cut_greater_subset_mono: "A ⊆ B ⟹ A ↓> t ⊆ B ↓> t" and
  cut_ge_subset_mono:      "A ⊆ B ⟹ A ↓≥ t ⊆ B ↓≥ t"
by (rule i_cut_subset_mono_disj[of _ A], simp+)+

lemmas i_cut_subset_mono =
  cut_less_subset_mono cut_le_subset_mono
  cut_greater_subset_mono cut_ge_subset_mono





lemma
  cut_less_mono:    "t ≤ t' ⟹ I ↓< t ⊆ I ↓< t'" and
  cut_greater_mono: "t' ≤ t ⟹ I ↓> t ⊆ I ↓> t'" and
  cut_le_mono:      "t ≤ t' ⟹ I ↓≤ t ⊆ I ↓≤ t'" and
  cut_ge_mono:      "t' ≤ t ⟹ I ↓≥ t ⊆ I ↓≥ t'"
by (unfold i_cut_defs, safe, simp_all)
lemmas i_cut_mono =
  cut_le_mono cut_less_mono
  cut_ge_mono cut_greater_mono




lemma
  cut_cut_le: "i ↓≤ a ↓≤ b = i ↓≤ min a b" and
  cut_cut_less: "i ↓< a ↓< b = i ↓< min a b" and
  cut_cut_ge: "i ↓≥ a ↓≥ b = i ↓≥ max a b" and
  cut_cut_greater: "i ↓> a ↓> b = i ↓> max a b"
unfolding i_cut_defs by simp_all
lemmas i_cut_cut =
  cut_cut_le cut_cut_less
  cut_cut_ge cut_cut_greater

lemma i_cut_absorb_disj: "
  ⟦ cut_op = (↓<) ∨ cut_op = (↓≤) ∨
    cut_op = (↓>) ∨ cut_op = (↓≥) ⟧
  ⟹ cut_op (cut_op I t) t = cut_op I t"
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], blast)
apply (blast dest: set_restriction_absorb)
done

corollary
  cut_le_absorb:      "I ↓≤ t ↓≤ t = I ↓≤ t" and
  cut_less_absorb:    "I ↓< t ↓< t = I ↓< t" and
  cut_ge_absorb:      "I ↓≥ t ↓≥ t = I ↓≥ t" and
  cut_greater_absorb: "I ↓> t ↓> t = I ↓> t"
by (rule i_cut_absorb_disj, blast)+

lemmas i_cut_absorb =
  cut_le_absorb cut_less_absorb
  cut_ge_absorb cut_greater_absorb

lemma
  cut_less_0_empty: "I ↓< (0::nat) = {}" and
  cut_ge_0_all:     "I ↓≥ (0::nat) = I"
unfolding i_cut_defs by blast+

lemma
  cut_le_all_iff:      "(I ↓≤ t = I) = (∀x∈I. x ≤ t)" and
  cut_less_all_iff:    "(I ↓< t = I) = (∀x∈I. x < t)" and
  cut_ge_all_iff:      "(I ↓≥ t = I) = (∀x∈I. x ≥ t)" and
  cut_greater_all_iff: "(I ↓> t = I) = (∀x∈I. x > t)"
by blast+

lemmas i_cut_all_iff =
  cut_le_all_iff cut_less_all_iff
  cut_ge_all_iff cut_greater_all_iff

lemma
  cut_le_empty_iff:      "(I ↓≤ t = {}) = (∀x∈I. t < x)" and
  cut_less_empty_iff:    "(I ↓< t = {}) = (∀x∈I. t ≤ x)" and
  cut_ge_empty_iff:      "(I ↓≥ t = {}) = (∀x∈I. x < t)" and
  cut_greater_empty_iff: "(I ↓> t = {}) = (∀x∈I. x ≤ t)"
unfolding i_cut_defs by fastforce+

lemmas i_cut_empty_iff =
  cut_le_empty_iff cut_less_empty_iff
  cut_ge_empty_iff cut_greater_empty_iff

lemma
  cut_le_not_empty_iff:      "(I ↓≤ t ≠ {}) = (∃x∈I. x ≤ t)" and
  cut_less_not_empty_iff:    "(I ↓< t ≠ {}) = (∃x∈I. x < t)" and
  cut_ge_not_empty_iff:      "(I ↓≥ t ≠ {}) = (∃x∈I. t ≤ x)" and
  cut_greater_not_empty_iff: "(I ↓> t ≠ {}) = (∃x∈I. t < x)"
unfolding i_cut_defs by blast+

lemmas i_cut_not_empty_iff =
  cut_le_not_empty_iff cut_less_not_empty_iff
  cut_ge_not_empty_iff cut_greater_not_empty_iff

lemma nat_cut_ge_infinite_not_empty: "infinite I ⟹ I ↓≥ (t::nat) ≠ {}"
by (drule infinite_nat_iff_unbounded_le[THEN iffD1], blast)

lemma nat_cut_greater_infinite_not_empty: "infinite I ⟹ I ↓> (t::nat) ≠ {}"
by (drule infinite_nat_iff_unbounded[THEN iffD1], blast)

corollary
  cut_le_not_in_imp:      "x ∉ I ⟹ x ∉ I ↓≤ t" and
  cut_less_not_in_imp:    "x ∉ I ⟹ x ∉ I ↓< t" and
  cut_ge_not_in_imp:      "x ∉ I ⟹ x ∉ I ↓≥ t" and
  cut_greater_not_in_imp: "x ∉ I ⟹ x ∉ I ↓> t"
by (rule i_cut_set_restriction[THEN set_restriction_not_in_imp], assumption)+

lemmas i_cut_not_in_imp =
  cut_le_not_in_imp cut_less_not_in_imp
  cut_ge_not_in_imp cut_greater_not_in_imp

corollary
  cut_le_in_imp:      "x ∈ I ↓≤ t ⟹ x ∈ I" and
  cut_less_in_imp:    "x ∈ I ↓< t ⟹ x ∈ I" and
  cut_ge_in_imp:      "x ∈ I ↓≥ t ⟹ x ∈ I" and
  cut_greater_in_imp: "x ∈ I ↓> t ⟹ x ∈ I"
by (rule i_cut_set_restriction[THEN set_restriction_in_imp], assumption)+

lemmas i_cut_in_imp =
  cut_le_in_imp cut_less_in_imp
  cut_ge_in_imp cut_greater_in_imp


lemma Collect_minI_cut: "⟦ k ∈ I; P (k::('a::wellorder)) ⟧ ⟹ ∃x∈I. P x ∧ (∀y∈(I ↓< x). ¬ P y)"
by (drule Collect_minI, assumption, blast)

corollary Collect_minI_ex_cut: "∃k∈I. P (k::('a::wellorder)) ⟹ ∃x∈I. P x ∧ (∀y∈(I ↓< x). ¬ P y)"
by (drule Collect_minI_ex, blast)

corollary Collect_minI_ex2_cut: "{k∈I. P (k::('a::wellorder))} ≠ {} ⟹ ∃x∈I. P x ∧ (∀y∈(I ↓< x). ¬ P y)"
by (drule Collect_minI_ex2, blast)





lemma cut_le_cut_greater_ident: "t2 ≤ t1 ⟹ I ↓≤ t1 ∪ I ↓> t2 = I"
by fastforce
lemma cut_less_cut_ge_ident: "t2 ≤ t1 ⟹ I ↓< t1 ∪ I ↓≥ t2 = I"
by fastforce
lemma cut_le_cut_ge_ident: "t2 ≤ t1 ⟹ I ↓≤ t1 ∪ I ↓≥ t2 = I"
by fastforce

lemma cut_less_cut_greater_ident: "
  ⟦ t2 ≤ t1; I ∩ {t1..t2} = {} ⟧ ⟹ I ↓< t1 ∪ I ↓> t2 = I"
by fastforce
corollary cut_less_cut_greater_ident': "
  t ∉ I ⟹ I ↓< t ∪ I ↓> t = I"
by (simp add: cut_less_cut_greater_ident)

lemma insert_eq_cut_less_cut_greater: "insert n I = I ↓< n ∪ {n} ∪ I ↓> n"
by fastforce



subsubsection ‹Relations between cut operators›

lemma insert_Int_conv_if: "A ∩ (insert x B) = (
  if x ∈ A then insert x (A ∩ B) else A ∩ B)"
by simp

lemma cut_le_less_conv_if: "I ↓≤ t = (
  if t ∈ I then insert t (I ↓< t) else (I ↓< t))"
by (simp add: i_cut_Int_conv lessThan_insert[symmetric] insert_Int_conv_if)

lemma cut_le_less_conv: "I ↓≤ t = ({t} ∩ I) ∪ (I ↓< t)"
by fastforce

lemma cut_less_le_conv: "I ↓< t = (I ↓≤ t) - {t}"
by fastforce
lemma cut_less_le_conv_if: "I ↓< t = (
  if t ∈ I then (I ↓≤ t) - {t} else (I ↓≤ t))"
by (simp only: cut_less_le_conv, force)







lemma cut_ge_greater_conv_if: "I ↓≥ t = (
  if t ∈ I then insert t (I ↓> t) else (I ↓> t))"
by (simp add: i_cut_Int_conv greaterThan_insert[symmetric] insert_Int_conv_if)
lemma cut_ge_greater_conv: "I ↓≥ t = ({t} ∩ I) ∪ (I ↓> t)"
apply (simp only: cut_ge_greater_conv_if)
apply (case_tac "t ∈ I")
apply simp_all
done
lemma cut_greater_ge_conv: "I ↓> t = (I ↓≥ t) - {t}"
by fastforce
lemma cut_greater_ge_conv_if: "I ↓> t = (
  if t ∈ I then (I ↓≥ t) - {t} else (I ↓≥ t))"
by (simp only: cut_greater_ge_conv, force)



lemma nat_cut_le_less_conv: "I ↓≤ t = I ↓< Suc t"
by fastforce
lemma nat_cut_less_le_conv: "0 < t ⟹ I ↓< t = I ↓≤ (t - Suc 0)"
by fastforce
lemma nat_cut_ge_greater_conv: "I ↓≥ Suc t = I ↓> t"
by fastforce
lemma nat_cut_greater_ge_conv: "0 < t ⟹ I ↓> (t - Suc 0) = I ↓≥ t"
by fastforce


subsubsection ‹Function images with cut operators›

lemma cut_less_image: "
  ⟦ strict_mono_on f A; I ⊆ A; n ∈ A ⟧ ⟹
  (f ` I) ↓< f n = f ` (I ↓< n)"
apply (rule set_eqI)
apply (simp add: image_iff Bex_def cut_less_mem_iff)
apply (unfold strict_mono_on_def)
apply (rule iffI)
 apply (metis not_less_iff_gr_or_eq rev_subsetD)
apply blast
done

lemma cut_le_image: "
  ⟦ strict_mono_on f A; I ⊆ A; n ∈ A ⟧ ⟹
  (f ` I) ↓≤ f n = f ` (I ↓≤ n)"
apply (frule strict_mono_on_imp_inj_on)
apply (clarsimp simp: cut_le_less_conv_if cut_less_image inj_on_def)
apply blast
done

lemma cut_greater_image: "
  ⟦ strict_mono_on f A; I ⊆ A; n ∈ A ⟧ ⟹
  (f ` I) ↓> f n = f ` (I ↓> n)"
apply (rule set_eqI)
apply (simp add: image_iff Bex_def cut_greater_mem_iff)
apply (unfold strict_mono_on_def)
apply (rule iffI)
 apply (metis not_less_iff_gr_or_eq rev_subsetD)
apply blast
done

lemma cut_ge_image: "
  ⟦ strict_mono_on f A; I ⊆ A; n ∈ A ⟧ ⟹
  (f ` I) ↓≥ f n = f ` (I ↓≥ n)"
apply (frule strict_mono_on_imp_inj_on)
apply (clarsimp simp: cut_ge_greater_conv_if cut_greater_image inj_on_def)
apply blast
done

lemmas i_cut_image =
  cut_le_image cut_less_image
  cut_ge_image cut_greater_image


subsubsection ‹Finiteness and cardinality with cut operators›

lemma
  cut_le_finite:      "finite I ⟹ finite (I ↓≤ t)" and
  cut_less_finite:    "finite I ⟹ finite (I ↓< t)" and
  cut_ge_finite:      "finite I ⟹ finite (I ↓≥ t)" and
  cut_greater_finite: "finite I ⟹ finite (I ↓> t)"
by (rule finite_subset[of _ I], rule i_cut_subset, assumption+)+

lemma nat_cut_le_finite: "finite (I ↓≤ (t::nat))"
by (fastforce simp: finite_nat_iff_bounded_le2 cut_le_def)

lemma nat_cut_less_finite: "finite (I ↓< (t::nat))"
by (fastforce simp: finite_nat_iff_bounded2 cut_less_def)

lemma nat_cut_ge_finite_iff: "finite (I ↓≥ (t::nat)) = finite I"
apply (rule iffI)
 apply (subst cut_less_cut_ge_ident[of t, OF order_refl, symmetric])
 apply (simp add: nat_cut_less_finite)
apply (simp add: cut_ge_finite)
done

lemma nat_cut_greater_finite_iff: "finite (I ↓> (t::nat)) = finite I"
by (simp only: nat_cut_ge_greater_conv[symmetric] nat_cut_ge_finite_iff)

lemma
  cut_le_card:      "finite I ⟹ card (I ↓≤ t) ≤ card I" and
  cut_less_card:    "finite I ⟹ card (I ↓< t) ≤ card I" and
  cut_ge_card:      "finite I ⟹ card (I ↓≥ t) ≤ card I" and
  cut_greater_card: "finite I ⟹ card (I ↓> t) ≤ card I"
by (rule card_mono, assumption, rule i_cut_subset)+

lemma nat_cut_greater_card: "card (I ↓> (t::nat)) ≤ card I"
apply (case_tac "finite I")
 apply (simp add: cut_greater_card)
apply (simp add: nat_cut_greater_finite_iff)
done

lemma nat_cut_ge_card: "card (I ↓≥ (t::nat)) ≤ card I"
apply (case_tac "finite I")
 apply (simp add: cut_ge_card)
apply (simp add: nat_cut_ge_finite_iff)
done


subsubsection ‹Cutting a set at  ‹Min› or ‹Max› element›

lemma cut_greater_Min_eq_Diff: "I ↓> (iMin I) = I - {iMin I}"
by blast
lemma cut_less_Max_eq_Diff: "finite I ⟹ I ↓< (Max I) = I - {Max I}"
by blast

lemma cut_le_Min_empty: "t < iMin I ⟹ I ↓≤ t = {}"
by (fastforce simp: i_cut_defs)
lemma cut_less_Min_empty: "t ≤ iMin I ⟹ I ↓< t = {}"
by (fastforce simp: i_cut_defs)


lemma cut_le_Min_not_empty: "⟦ I ≠ {}; iMin I ≤ t ⟧ ⟹ I ↓≤ t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="iMin I" in exI)
apply (simp add: iMinI_ex2)
done

lemma cut_less_Min_not_empty: "⟦ I ≠ {}; iMin I < t ⟧ ⟹ I ↓< t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="iMin I" in exI)
apply (simp add: iMinI_ex2)
done

lemma cut_ge_Min_all: "t ≤ iMin I ⟹ I ↓≥ t = I"
apply (simp add: i_cut_defs)
apply safe
apply (drule iMin_le, simp)
done

lemma cut_greater_Min_all: "t < iMin I ⟹ I ↓> t = I"
apply (simp add: i_cut_defs)
apply safe
apply (drule iMin_le, simp)
done

lemmas i_cut_min_empty =
  cut_le_Min_empty
  cut_less_Min_empty
  cut_le_Min_not_empty
  cut_less_Min_not_empty
lemmas i_cut_min_all =
  cut_ge_Min_all
  cut_greater_Min_all

lemma cut_ge_Max_empty: "finite I ⟹ Max I < t ⟹ I ↓≥ t = {}"
by (fastforce simp: i_cut_defs)

lemma cut_greater_Max_empty: "finite I ⟹ Max I ≤ t ⟹ I ↓> t = {}"
by (fastforce simp: i_cut_defs)

lemma cut_ge_Max_not_empty: "⟦ I ≠ {}; finite I; t ≤ Max I ⟧ ⟹ I ↓≥ t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="Max I" in exI)
apply (simp add: MaxI_ex2)
done

lemma cut_greater_Max_not_empty: "⟦ I ≠ {}; finite I; t < Max I ⟧ ⟹ I ↓> t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="Max I" in exI)
apply (simp add: MaxI_ex2)
done

lemma cut_le_Max_all: "finite I ⟹ Max I ≤ t ⟹ I ↓≤ t = I"
by (fastforce simp: i_cut_defs)

lemma cut_less_Max_all: "finite I ⟹ Max I < t ⟹ I ↓< t = I"
by (fastforce simp: i_cut_defs)

lemmas i_cut_max_empty =
  cut_ge_Max_empty
  cut_greater_Max_empty
  cut_ge_Max_not_empty
  cut_greater_Max_not_empty
lemmas i_cut_max_all =
  cut_le_Max_all
  cut_less_Max_all

lemma cut_less_Max_less: "
  ⟦ finite (I ↓< t); I ↓< t ≠ {} ⟧ ⟹ Max (I ↓< t) < t"
by (rule cut_less_bound[OF Max_in])
lemma cut_le_Max_le: "
  ⟦ finite (I ↓≤ t); I ↓≤ t ≠ {} ⟧ ⟹ Max (I ↓≤ t) ≤ t"
by (rule cut_le_bound[OF Max_in])
lemma nat_cut_less_Max_less: "
  I ↓< t ≠ {} ⟹ Max (I ↓< t) < (t::nat)"
by (rule cut_less_bound[OF Max_in[OF nat_cut_less_finite]])
lemma nat_cut_le_Max_le: "
  I ↓≤ t ≠ {} ⟹ Max (I ↓≤ t) ≤ (t::nat)"
by (rule cut_le_bound[OF Max_in[OF nat_cut_le_finite]])
lemma cut_greater_Min_greater: "
  I ↓> t ≠ {} ⟹ iMin (I ↓> t) > t"
by (rule cut_greater_bound[OF iMinI_ex2])
lemma cut_ge_Min_greater: "
  I ↓≥ t ≠ {} ⟹ iMin (I ↓≥ t) ≥ t"
by (rule cut_ge_bound[OF iMinI_ex2])



lemma cut_less_Min_eq: "I ↓< t ≠ {} ⟹ iMin (I ↓< t) = iMin I"
apply (drule cut_less_not_empty_iff[THEN iffD1])
apply (rule iMin_equality)
 apply (fastforce intro: iMinI)
apply blast
done

lemma cut_le_Min_eq: "I ↓≤ t ≠ {} ⟹ iMin (I ↓≤ t) = iMin I"
apply (drule cut_le_not_empty_iff[THEN iffD1])
apply (rule iMin_equality)
 apply (fastforce intro: iMinI)
apply blast
done


lemma cut_ge_Max_eq: "⟦ finite I; I ↓≥ t ≠ {} ⟧ ⟹ Max (I ↓≥ t) = Max I"
apply (drule cut_ge_not_empty_iff[THEN iffD1])
apply (rule Max_equality)
  apply (fastforce intro: MaxI)
 apply (simp add: cut_ge_finite)
apply fastforce
done

lemma cut_greater_Max_eq: "⟦ finite I; I ↓> t ≠ {} ⟧ ⟹ Max (I ↓> t) = Max I"
apply (drule cut_greater_not_empty_iff[THEN iffD1])
apply (rule Max_equality)
  apply (fastforce intro: MaxI)
 apply (simp add: cut_greater_finite)
apply fastforce
done


subsubsection ‹Cut operators with intervals from SetInterval›

lemma
  UNIV_cut_le:      "UNIV ↓≤ t = {..t}" and
  UNIV_cut_less:    "UNIV ↓< t = {..<t}" and
  UNIV_cut_ge:      "UNIV ↓≥ t = {t..}" and
  UNIV_cut_greater: "UNIV ↓> t = {t<..}"
by blast+

lemma
  lessThan_cut_le:      "{..<n} ↓≤ t = (if n ≤ t then {..<n} else {..t})" and
  lessThan_cut_less:    "{..<n} ↓< t = (if n ≤ t then {..<n} else {..<t})" and
  lessThan_cut_ge:      "{..<n} ↓≥ t = {t..<n}" and
  lessThan_cut_greater: "{..<n} ↓> t = {t<..<n}" and
  atMost_cut_le:      "{..n} ↓≤ t = (if n ≤ t then {..n} else {..t})" and
  atMost_cut_less:    "{..n} ↓< t = (if n < t then {..n} else {..<t})" and
  atMost_cut_ge:      "{..n} ↓≥ t = {t..n}" and
  atMost_cut_greager: "{..n} ↓> t = {t<..n}" and
  greaterThan_cut_le:      "{n<..} ↓≤ t = {n<..t}" and
  greaterThan_cut_less:    "{n<..} ↓< t = {n<..<t}" and
  greaterThan_cut_ge:      "{n<..} ↓≥ t = (if t ≤ n then {n<..} else {t..})" and
  greaterThan_cut_greater: "{n<..} ↓> t = (if t ≤ n then {n<..} else {t<..})" and
  atLeast_cut_le:      "{n..} ↓≤ t = {n..t}" and
  atLeast_cut_less:    "{n..} ↓< t = {n..<t}" and
  atLeast_cut_ge:      "{n..} ↓≥ t = (if t ≤ n then {n..} else {t..})" and
  atLeast_cut_greater: "{n..} ↓≥ t = (if t ≤ n then {n..} else {t..})"
apply (simp_all add: set_eq_iff i_cut_mem_iff linorder_not_le linorder_not_less)
apply fastforce+
done


lemma
  greaterThanLessThan_cut_le:      "{m<..<n} ↓≤ t = (if n ≤ t then {m<..<n} else {m<..t})" and
  greaterThanLessThan_cut_less:    "{m<..<n} ↓< t = (if n ≤ t then {m<..<n} else {m<..<t})" and
  greaterThanLessThan_cut_ge:      "{m<..<n} ↓≥ t = (if t ≤ m then {m<..<n} else {t..<n})" and
  greaterThanLessThan_cut_greater: "{m<..<n} ↓> t = (if t ≤ m then {m<..<n} else {t<..<n})" and
  atLeastLessThan_cut_le:      "{m..<n} ↓≤ t = (if n ≤ t then {m..<n} else {m..t})" and
  atLeastLessThan_cut_less:    "{m..<n} ↓< t = (if n ≤ t then {m..<n} else {m..<t})" and
  atLeastLessThan_cut_ge:      "{m..<n} ↓≥ t = (if t ≤ m then {m..<n} else {t..<n})" and
  atLeastLessThan_cut_greater: "{m..<n} ↓> t = (if t < m then {m..<n} else {t<..<n})" and
  greaterThanAtMost_cut_le:      "{m<..n} ↓≤ t = (if n ≤ t then {m<..n} else {m<..t})" and
  greaterThanAtMost_cut_less:    "{m<..n} ↓< t = (if n < t then {m<..n} else {m<..<t})" and
  greaterThanAtMost_cut_ge:      "{m<..n} ↓≥ t = (if t ≤ m then {m<..n} else {t..n})" and
  greaterThanAtMost_cut_greater: "{m<..n} ↓> t = (if t ≤ m then {m<..n} else {t<..n})" and
  atLeastAtMost_cut_le:      "{m..n} ↓≤ t = (if n ≤ t then {m..n} else {m..t})" and
  atLeastAtMost_cut_less:    "{m..n} ↓< t = (if n < t then {m..n} else {m..<t})" and
  atLeastAtMost_cut_ge:      "{m..n} ↓≥ t = (if t ≤ m then {m..n} else {t..n})" and
  atLeastAtMost_cut_greater: "{m..n} ↓> t = (if t < m then {m..n} else {t<..n})"
apply (simp_all add: set_eq_iff i_cut_mem_iff if_split linorder_not_le linorder_not_less)
apply fastforce+
done


subsubsection ‹Mirroring finite natural sets between their @{term Min} and @{term Max} element›

text ‹Mirroring a number at the middle of the interval {min l r..max l r}›
text_raw ‹\bigskip›

text ‹Mirroring a single element n between the interval boundaries l and r›
definition nat_mirror :: "nat ⇒ nat ⇒ nat ⇒ nat"
  where "nat_mirror n l r ≡ l + r - n"

lemma nat_mirror_commute: "nat_mirror n l r = nat_mirror n r l"
unfolding nat_mirror_def by simp

lemma nat_mirror_inj_on: "inj_on (λx. nat_mirror x l r) {..l + r}"
unfolding inj_on_def nat_mirror_def by fastforce

lemma nat_mirror_nat_mirror_ident: "
  n ≤ l + r ⟹ nat_mirror (nat_mirror n l r) l r = n"
unfolding nat_mirror_def by simp

lemma nat_mirror_add: "
  nat_mirror (n + k) l r = (nat_mirror n l r) - k"
unfolding nat_mirror_def by simp
lemma nat_mirror_diff: "
  ⟦ k ≤ n; n ≤ l + r ⟧ ⟹
  nat_mirror (n - k) l r = (nat_mirror n l r) + k"
unfolding nat_mirror_def by simp

lemma nat_mirror_le: "a ≤ b ⟹ nat_mirror b l r ≤ nat_mirror a l r"
unfolding nat_mirror_def by simp
lemma nat_mirror_le_conv: "
  a ≤ l + r ⟹ (nat_mirror b l r ≤ nat_mirror a l r) = (a ≤ b)"
unfolding nat_mirror_def by fastforce

lemma nat_mirror_less: "
  ⟦ a < b; a < l + r ⟧ ⟹
  nat_mirror b l r < nat_mirror a l r"
unfolding nat_mirror_def by simp
lemma nat_mirror_less_imp_less: "
  nat_mirror b l r < nat_mirror a l r ⟹ a < b"
unfolding nat_mirror_def by simp
lemma nat_mirror_less_conv: "
  a < l + r ⟹ (nat_mirror b l r < nat_mirror a l r) = (a < b)"
unfolding nat_mirror_def by fastforce

lemma nat_mirror_eq_conv: "
  ⟦ a ≤ l + r; b ≤ l + r ⟧ ⟹
  (nat_mirror a l r = nat_mirror b l r) = (a = b)"
unfolding nat_mirror_def by fastforce

text ‹Mirroring a single element n between the interval boundaries of I›
definition
  mirror_elem :: "nat ⇒ nat set ⇒ nat"
where
  "mirror_elem n I ≡ nat_mirror n (iMin I) (Max I)"

lemma mirror_elem_inj_on: "finite I ⟹ inj_on (λx. mirror_elem x I) I"
unfolding mirror_elem_def
by (metis Max_le_imp_subset_atMost nat_mirror_inj_on not_add_less2 not_le_imp_less subset_inj_on)

lemma mirror_elem_add: "
  finite I ⟹ mirror_elem (n + k) I = mirror_elem n I - k"
unfolding mirror_elem_def by (rule nat_mirror_add)
lemma mirror_elem_diff: "
  ⟦ finite I; k ≤ n; n ∈ I ⟧ ⟹ mirror_elem (n - k) I = mirror_elem n I + k"
apply (unfold mirror_elem_def)
apply (rule nat_mirror_diff, assumption)
apply (simp add: trans_le_add2)
done
lemma mirror_elem_Min: "
  ⟦ finite I; I ≠ {} ⟧ ⟹ mirror_elem (iMin I) I = Max I"
unfolding mirror_elem_def nat_mirror_def by simp
lemma mirror_elem_Max: "
  ⟦ finite I; I ≠ {} ⟧ ⟹ mirror_elem (Max I) I = iMin I"
unfolding mirror_elem_def nat_mirror_def by simp

lemma mirror_elem_mirror_elem_ident: "
  ⟦ finite I; n ≤ iMin I + Max I ⟧ ⟹ mirror_elem (mirror_elem n I) I = n"
unfolding mirror_elem_def nat_mirror_def by simp

lemma mirror_elem_le_conv: "
  ⟦ finite I; a ∈ I; b ∈ I ⟧ ⟹
  (mirror_elem b I ≤ mirror_elem a I) = (a ≤ b)"
apply (unfold mirror_elem_def)
apply (rule nat_mirror_le_conv)
apply (simp add: trans_le_add2)
done

lemma mirror_elem_less_conv: "
  ⟦ finite I; a ∈ I; b ∈ I ⟧ ⟹
  (mirror_elem b I < mirror_elem a I) = (a < b)"
unfolding mirror_elem_def nat_mirror_def
by (metis diff_less_mono2 nat_diff_left_cancel_less nat_ex_greater_infinite_finite_Max_conv' trans_less_add2)

lemma mirror_elem_eq_conv: "
  ⟦ a ≤ iMin I + Max I; b ≤ iMin I + Max I ⟧ ⟹
  (mirror_elem a I = mirror_elem b I) = (a = b)"
by (simp add: mirror_elem_def nat_mirror_eq_conv)
lemma mirror_elem_eq_conv': "
  ⟦ finite I; a ∈ I; b ∈ I ⟧ ⟹ (mirror_elem a I = mirror_elem b I) = (a = b)"
apply (rule mirror_elem_eq_conv)
apply (simp_all add: trans_le_add2)
done


definition
  imirror_bounds :: "nat set ⇒ nat ⇒ nat ⇒ nat set"
where
  "imirror_bounds I l r ≡ (λx. nat_mirror x l r) ` I"

text ‹Mirroring all elements between the interval boundaries of I›
definition
  imirror :: "nat set ⇒ nat set"
where
  "imirror I ≡ (λx. iMin I + Max I - x) ` I"

lemma imirror_eq_nat_mirror_image: "
  imirror I = (λx. nat_mirror x (iMin I) (Max I)) ` I"
unfolding imirror_def nat_mirror_def by simp
lemma imirror_eq_mirror_elem_image: "
  imirror I = (λx. mirror_elem x I) ` I"
by (simp add: mirror_elem_def imirror_eq_nat_mirror_image)

lemma imirror_eq_imirror_bounds: "
  imirror I = imirror_bounds I (iMin I) (Max I)"
unfolding imirror_def imirror_bounds_def nat_mirror_def by simp




lemma imirror_empty: "imirror {} = {}"
unfolding imirror_def by simp
lemma imirror_is_empty: "(imirror I = {}) = (I = {})"
unfolding imirror_def by simp
lemma imirror_not_empty: "I ≠ {} ⟹ imirror I ≠ {}"
unfolding imirror_def by simp

lemma imirror_singleton: "imirror {a} = {a}"
unfolding imirror_def by simp


lemma imirror_finite: "finite I ⟹ finite (imirror I)"
unfolding imirror_def by simp

lemma imirror_bounds_iMin: "
  ⟦ finite I; I ≠ {}; iMin I ≤ l + r ⟧ ⟹
  iMin (imirror_bounds I l r) = l + r - Max I"
apply (unfold imirror_bounds_def nat_mirror_def)
apply (rule iMin_equality)
 apply (blast intro: Max_in)
apply (blast intro: Max_ge diff_le_mono2)
done

lemma imirror_bounds_Max: "
  ⟦ finite I; I ≠ {}; Max I ≤ l + r ⟧ ⟹
  Max (imirror_bounds I l r) = l + r - iMin I"
apply (unfold imirror_bounds_def nat_mirror_def)
apply (rule Max_equality)
  apply (blast intro: iMinI)
 apply simp
apply (blast intro: iMin_le diff_le_mono2)
done

lemma imirror_iMin: "finite I ⟹ iMin (imirror I) = iMin I"
apply (case_tac "I = {}", simp add: imirror_empty)
apply (simp add: imirror_eq_imirror_bounds imirror_bounds_iMin le_add1)
done

lemma imirror_Max: "finite I ⟹ Max (imirror I) = Max I"
apply (case_tac "I = {}", simp add: imirror_empty)
apply (simp add: imirror_eq_imirror_bounds imirror_bounds_Max trans_le_add2)
done
corollary imirror_iMin_Max: "⟦ finite I; n ∈ imirror I ⟧ ⟹ iMin I ≤ n ∧ n ≤ Max I"
apply (frule Max_ge[OF imirror_finite, of _ n], assumption)
apply (fastforce simp: imirror_iMin imirror_Max)
done

lemma imirror_bounds_iff:
  "(n ∈ imirror_bounds I l r) = (∃x∈I. n = l + r - x)"
by (simp add: imirror_bounds_def nat_mirror_def image_iff)

lemma imirror_iff: "(n ∈ imirror I) = (∃x∈I. n = iMin I + Max I - x)"
by (simp add: imirror_def image_iff)

lemma imirror_bounds_imirror_bounds_ident: "
  ⟦ finite I; Max I ≤ l + r ⟧ ⟹
  imirror_bounds (imirror_bounds I l r) l r = I"
apply (rule set_eqI)
apply (simp add: imirror_bounds_def image_image image_iff)
apply (rule iffI)
 apply (fastforce simp: nat_mirror_nat_mirror_ident)
apply (rule_tac x=x in bexI)
apply (fastforce simp: nat_mirror_nat_mirror_ident)+
done

lemma imirror_imirror_ident: "finite I ⟹ imirror (imirror I) = I"
apply (case_tac "I = {}", simp add: imirror_empty)
apply (simp add: imirror_eq_imirror_bounds imirror_bounds_iMin imirror_bounds_Max
  le_add1 trans_le_add2 imirror_bounds_imirror_bounds_ident)
done

lemma mirror_elem_imirror: "
  finite I ⟹ mirror_elem t (imirror I) = mirror_elem t I"
by (simp add: mirror_elem_def imirror_iMin imirror_Max)

lemma imirror_card: "finite I ⟹ card (imirror I) = card I"
apply (simp only: imirror_eq_mirror_elem_image)
apply (rule inj_on_iff_eq_card[THEN iffD1], assumption)
apply (rule mirror_elem_inj_on, assumption)
done


lemma imirror_bounds_elem_conv: "
  ⟦ finite I; n ≤ l + r; Max I ≤ l + r ⟧ ⟹
  ((nat_mirror n l r) ∈ imirror_bounds I l r) = (n ∈ I)"
apply (unfold imirror_bounds_def)
apply (rule inj_on_image_mem_iff)
apply (rule nat_mirror_inj_on)
apply fastforce
apply simp
done

lemma imirror_mem_conv: "
  ⟦ finite I; n ≤ iMin I + Max I ⟧ ⟹ ((mirror_elem n I) ∈ imirror I) = (n ∈ I)"
by (simp add: mirror_elem_def imirror_eq_imirror_bounds imirror_bounds_elem_conv)

corollary in_imp_mirror_elem_in: "
  ⟦ finite I; n ∈ I ⟧ ⟹ (mirror_elem n I) ∈ imirror I"
by (rule imirror_mem_conv[OF _ trans_le_add2[OF Max_ge], THEN iffD2])

lemma imirror_cut_less: "
  finite I ⟹
  imirror I ↓< (mirror_elem t I) =
  imirror_bounds (I ↓> t) (iMin I) (Max I)"
apply (simp only: imirror_eq_imirror_bounds)
apply (unfold imirror_def imirror_bounds_def mirror_elem_def)
apply (rule set_eqI)
apply (simp add: Bex_def i_cut_mem_iff image_iff)
apply (rule iffI)
 apply (bestsimp intro: nat_mirror_less_imp_less)
apply (bestsimp simp add: nat_mirror_less)
done

lemma imirror_cut_le: "
  ⟦ finite I; t ≤ iMin I + Max I ⟧ ⟹
  imirror I ↓≤ (mirror_elem t I) =
  imirror_bounds (I ↓≥ t) (iMin I) (Max I)"
apply (simp only: nat_cut_le_less_conv)
apply (case_tac "t = 0")
 apply (simp add: cut_ge_0_all i_cut_empty)
 apply (simp only: imirror_eq_imirror_bounds[symmetric])
 apply (rule cut_less_Max_all)
  apply (rule imirror_finite, assumption)
 apply (simp add: mirror_elem_def nat_mirror_def imirror_Max)
apply (simp add: nat_cut_greater_ge_conv[symmetric])
apply (rule subst[of "mirror_elem (t - Suc 0) I" "Suc (mirror_elem t I)"])
 apply (simp add: mirror_elem_def nat_mirror_diff)
apply (rule imirror_cut_less, assumption)
done

lemma imirror_cut_ge: "
  finite I ⟹
  imirror I ↓≥ (mirror_elem t I) =
  imirror_bounds (I ↓≤ t) (iMin I) (Max I)"
  (is "?P ⟹ ?lhs I = ?rhs I t")
apply (case_tac "iMin I + Max I < t")
 apply (simp add: mirror_elem_def nat_mirror_def cut_ge_0_all cut_le_Max_all imirror_eq_imirror_bounds)
apply (case_tac "t < iMin I")
 apply (simp add: cut_le_Min_empty imirror_bounds_def mirror_elem_def nat_mirror_def cut_ge_Max_empty imirror_Max imirror_finite)
apply (simp add: linorder_not_le linorder_not_less)
apply (rule subst[of "imirror (imirror I) ↓≤ mirror_elem (mirror_elem t I) (imirror I)" "I ↓≤ t"])
 apply (simp add: imirror_imirror_ident mirror_elem_imirror mirror_elem_mirror_elem_ident)
apply (subgoal_tac "mirror_elem t I ≤ Max (imirror I)")
 prefer 2
 apply (simp add: imirror_Max mirror_elem_def nat_mirror_def)
apply (simp add: imirror_cut_le imirror_finite)
by (metis cut_ge_Max_eq cut_ge_Max_not_empty imirror_Max imirror_bounds_imirror_bounds_ident imirror_finite imirror_iMin le_add2 nat_cut_ge_finite_iff)

lemma imirror_cut_greater: "⟦ finite I; t ≤ iMin I + Max I ⟧ ⟹
  imirror I ↓> (mirror_elem t I) =
  imirror_bounds (I ↓< t) (iMin I) (Max I)"
apply (case_tac "t = 0")
 apply (simp add: cut_less_0_empty imirror_bounds_def)
 apply (rule cut_greater_Max_empty)
   apply (rule imirror_finite, assumption)
 apply (simp add: imirror_Max mirror_elem_def nat_mirror_def)
apply (simp add: nat_cut_ge_greater_conv[symmetric])
apply (rule subst[of "mirror_elem (t - Suc 0) I" "Suc (mirror_elem t I)"])
 apply (simp add: mirror_elem_def nat_mirror_diff)
apply (simp add: imirror_cut_ge nat_cut_less_le_conv)
done

lemmas imirror_cut =
  imirror_cut_less imirror_cut_ge
  imirror_cut_le imirror_cut_greater

corollary imirror_cut_le': "
  ⟦ finite I; t ∈ I ⟧ ⟹
  imirror I ↓≤ mirror_elem t I =
  imirror_bounds (I ↓≥ t) (iMin I) (Max I)"
by (rule imirror_cut_le[OF _ trans_le_add2[OF Max_ge]])

corollary imirror_cut_greater': "
  ⟦ finite I; t ∈ I ⟧ ⟹
  imirror I ↓> mirror_elem t I =
  imirror_bounds (I ↓< t) (iMin I) (Max I)"
by (rule imirror_cut_greater[OF _ trans_le_add2[OF Max_ge]])

lemmas imirror_cut' =
  imirror_cut_le' imirror_cut_greater'


lemma imirror_bounds_Un: "
  imirror_bounds (A ∪ B) l r =
  imirror_bounds A l r ∪ imirror_bounds B l r"
by (simp add: imirror_bounds_def image_Un)
lemma imirror_bounds_Int: "
  ⟦ A ⊆ {..l + r}; B ⊆ {..l + r} ⟧ ⟹
  imirror_bounds (A ∩ B) l r =
  imirror_bounds A l r ∩ imirror_bounds B l r"
apply (unfold imirror_bounds_def)
apply (rule inj_on_image_Int[OF _ Un_upper1 Un_upper2])
apply (rule subset_inj_on[OF nat_mirror_inj_on])
apply (rule Un_least[of A _ B], assumption+)
done

end