Theory SetIntervalCut

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

(* header {* Cutting @{term linorder} and @{term nat} sets *} *)
header {* Cutting linearly ordered and natural sets *}

theory SetIntervalCut
imports SetInterval2
begin




subsection {* Set restriction *}

text {* 
  A set to set function @{text f} is a @{text "set restriction"}, 
  if there exists a predicate @{text P},
  so that for every set @{text s} the function result @{text "f s"}
  contains all its elements fulfilling @{text 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 o 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 fastsimp
done
lemma set_restriction_commute: "
  [| set_restriction f; set_restriction g |] ==> f (g I) = g (f I)"
unfolding set_restriction_def by fastsimp

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 fastsimp
lemma set_restriction_Int: "
  set_restriction f ==> f (A ∩ B) = f A ∩ f B"
unfolding set_restriction_def by fastsimp
lemma set_restriction_Diff: "
  set_restriction f ==> f (A - B) = f A - f B"
unfolding set_restriction_def by fastsimp
lemma set_restriction_mono: "
  [| set_restriction f; A ⊆ B |] ==> f A ⊆ f B"
unfolding set_restriction_def by fastsimp
lemma set_restriction_absorb: "
  set_restriction f ==> f (f A) = f A"
unfolding set_restriction_def by fastsimp
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 fastsimp
lemma set_restriction_card: "
  [| set_restriction f; finite A |] ==> 
  card (f A) = card A - card {a ∈ A. f {a} = {}}"
apply (unfold set_restriction_def)
thm card_Diff_subset[symmetric]
apply (subgoal_tac "{a ∈ A. f {a} = {}} ⊆ A")
 prefer 2 
 apply blast
apply (frule finite_subset, simp)
thm card_Diff_subset[symmetric]
apply (simp only: card_Diff_subset[symmetric])
apply (rule arg_cong[where f=card])
apply fastsimp
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 "\<down>≤" 100 )
where
  "I \<down>≤ t ≡ { x∈I. x ≤ t }"
definition
  cut_less :: "'a::linorder set => 'a => 'a set"         ( infixl "\<down><" 100 )
where
  "I \<down>< t ≡ { x∈I. x < t }"

definition
  cut_ge :: "'a::linorder set => 'a => 'a set"           ( infixl "\<down>≥" 100 )
where
  "I \<down>≥ t ≡ { x∈I. t ≤ x }"
definition
  cut_greater :: "'a::linorder set => 'a => 'a set"      ( infixl "\<down>>" 100 )
where
  "I \<down>> t ≡ { x∈I. t < x }"

lemmas i_cut_defs =
  cut_le_def cut_less_def
  cut_ge_def cut_greater_def
thm i_cut_defs

lemma cut_le_mem_iff: "x ∈ I \<down>≤ t = (x ∈ I ∧ x ≤ t)"
by (unfold cut_le_def, blast)
lemma cut_less_mem_iff: "x ∈ I \<down>< t = (x ∈ I ∧ x < t)"
by (unfold cut_less_def, blast)
lemma cut_ge_mem_iff: "x ∈ I \<down>≥ t = (x ∈ I ∧ t ≤ x)"
by (unfold cut_ge_def, blast)
lemma cut_greater_mem_iff: "x ∈ I \<down>> 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
thm i_cut_mem_iff

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

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


lemma 
  cut_less_bound:    "n ∈ I \<down>< t ==> n < t" and
  cut_le_bound:      "n ∈ I \<down>≤ t ==> n ≤ t" and
  cut_greater_bound: "n ∈ i \<down>> t ==> t < n" and
  cut_ge_bound:      "n ∈ i \<down>≥ 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 \<down>≤ t = I ∩ {..t}" and
  cut_less_Int_conv: "I \<down>< t = I ∩ {..<t}" and
  cut_ge_Int_conv: "I \<down>≥ t = I ∩ {t..}" and
  cut_greater_Int_conv: "I \<down>> 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
thm i_cut_Int_conv


lemma 
  cut_le_Diff_conv: "I \<down>≤ t = I - {t<..}" and
  cut_less_Diff_conv: "I \<down>< t = I - {t..}" and
  cut_ge_Diff_conv: "I \<down>≥ t = I - {..<t}" and
  cut_greater_Diff_conv: "I \<down>> t = I - {..t}"
by (fastsimp 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
thm i_cut_Diff_conv


subsubsection {* Basic results for cut operators *}

lemma 
  cut_less_eq_set_restriction_fun':    "(λI. I \<down>< t) = set_restriction_fun (λx. x < t)" and
  cut_le_eq_set_restriction_fun':      "(λI. I \<down>≤ t) = set_restriction_fun (λx. x ≤ t)" and
  cut_greater_eq_set_restriction_fun': "(λI. I \<down>> t) = set_restriction_fun (λx. x > t)" and
  cut_ge_eq_set_restriction_fun':      "(λI. I \<down>≥ 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 \<down>< t = set_restriction_fun (λx. x < t) I" and
  cut_le_eq_set_restriction_fun:      "I \<down>≤ t = set_restriction_fun (λx. x ≤ t) I" and
  cut_greater_eq_set_restriction_fun: "I \<down>> t = set_restriction_fun (λx. x > t) I" and
  cut_ge_eq_set_restriction_fun:      "I \<down>≥ 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 = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥;
    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
thm set_restriction_def
corollary
  i_cut_less_set_restriction:    "set_restriction (λI. I \<down>< t)" and
  i_cut_le_set_restriction:      "set_restriction (λI. I \<down>≤ t)" and
  i_cut_greater_set_restriction: "set_restriction (λI. I \<down>> t)" and
  i_cut_ge_set_restriction:      "set_restriction (λI. I \<down>≥ 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 = op \<down>< ∨ cut_op1 = op \<down>≤ ∨ 
  cut_op1 = op \<down>> ∨ cut_op1 = op \<down>≥;
  cut_op2 = op \<down>< ∨ cut_op2 = op \<down>≤ ∨ 
  cut_op2 = op \<down>> ∨ cut_op2 = op \<down>≥ |] ==>
  cut_op2 (cut_op1 I t1) t2 = cut_op1 (cut_op2 I t2) t1"
thm 
  set_restriction_commute[of "λI. cut_op1 I t"]
  i_cut_set_restriction_disj
apply (rule set_restriction_commute)
apply (simp_all only: i_cut_set_restriction_disj)
done
thm i_cut_commute_disj
thm i_cut_commute_disj[of "op \<down><" "op \<down><", simplified]
thm i_cut_commute_disj[of "op \<down><" "op \<down>>", simplified]
thm i_cut_commute_disj[of "op \<down>≤" "op \<down>>", simplified]
thm i_cut_commute_disj[of "op \<down>≥" "op \<down>>", simplified]

lemma
  cut_less_empty:    "{} \<down>< t = {}" and
  cut_le_empty:      "{} \<down>≤ t = {}" and
  cut_greater_empty: "{} \<down>> t = {}" and
  cut_ge_empty:      "{} \<down>≥ t = {}"
by blast+
lemmas i_cut_empty =
  cut_less_empty cut_le_empty
  cut_greater_empty cut_ge_empty
thm i_cut_empty

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


lemma 
  cut_less_singleton:    "{a} \<down>< t = (if a < t then {a} else {})" and
  cut_le_singleton:      "{a} \<down>≤ t = (if a ≤ t then {a} else {})" and
  cut_greater_singleton: "{a} \<down>> t = (if a > t then {a} else {})" and
  cut_ge_singleton:      "{a} \<down>≥ 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 \<down>< t ⊆ I" and
  cut_le_subset:      "I \<down>≤ t ⊆ I" and
  cut_greater_subset: "I \<down>> t ⊆ I" and
  cut_ge_subset:      "I \<down>≥ t ⊆ I"
thm i_cut_set_restriction[THEN set_restriction_subset]
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
thm i_cut_subset

thm set_restriction_Un
lemma i_cut_Un_disj: "
  [| cut_op = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥ |]
  ==> cut_op (A ∪ B) t = cut_op A t ∪ cut_op B t"
thm i_cut_set_restriction_disj[of cut_op "λI. cut_op I t" t]
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], simp)
thm set_restriction_Un
by (rule set_restriction_Un)


corollary
  cut_less_Un:    "(A ∪ B) \<down>< t = A \<down>< t ∪ B \<down>< t" and
  cut_le_Un:      "(A ∪ B) \<down>≤ t = A \<down>≤ t ∪ B \<down>≤ t" and
  cut_greater_Un: "(A ∪ B) \<down>> t = A \<down>> t ∪ B \<down>> t" and
  cut_ge_Un:      "(A ∪ B) \<down>≥ t = A \<down>≥ t ∪ B \<down>≥ 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 = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥ |]
  ==> 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) \<down>< t = A \<down>< t ∩ B \<down>< t" and
  cut_le_Int:      "(A ∩ B) \<down>≤ t = A \<down>≤ t ∩ B \<down>≤ t" and
  cut_greater_Int: "(A ∩ B) \<down>> t = A \<down>> t ∩ B \<down>> t" and
  cut_ge_Int:      "(A ∩ B) \<down>≥ t = A \<down>≥ t ∩ B \<down>≥ 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) \<down>< t = A \<down>< t ∩ B" and
  cut_le_Int_left:      "(A ∩ B) \<down>≤ t = A \<down>≤ t ∩ B" and
  cut_greater_Int_left: "(A ∩ B) \<down>> t = A \<down>> t ∩ B" and
  cut_ge_Int_left:      "(A ∩ B) \<down>≥ t = A \<down>≥ 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) \<down>< t = A ∩ B \<down>< t" and
  cut_le_Int_right:      "(A ∩ B) \<down>≤ t = A ∩ B \<down>≤ t" and
  cut_greater_Int_right: "(A ∩ B) \<down>> t = A ∩ B \<down>> t" and
  cut_ge_Int_right:      "(A ∩ B) \<down>≥ t = A ∩ B \<down>≥ 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 = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥ |]
  ==> 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) \<down>< t = A \<down>< t - B \<down>< t" and
  cut_le_Diff:      "(A - B) \<down>≤ t = A \<down>≤ t - B \<down>≤ t" and
  cut_greater_Diff: "(A - B) \<down>> t = A \<down>> t - B \<down>> t" and
  cut_ge_Diff:      "(A - B) \<down>≥ t = A \<down>≥ t - B \<down>≥ t"
by (rule i_cut_Diff_disj, blast)+
lemmas i_cut_Diff =
  cut_less_Diff cut_le_Diff
  cut_greater_Diff cut_ge_Diff


thm set_restriction_mono
lemma i_cut_subset_mono_disj: "
  [| cut_op = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥; 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)
thm set_restriction_mono[where f="λI. cut_op I t"]
by (rule set_restriction_mono[where f="λI. cut_op I t"])
corollary
  cut_less_subset_mono:    "A ⊆ B ==> A \<down>< t ⊆ B \<down>< t" and
  cut_le_subset_mono:      "A ⊆ B ==> A \<down>≤ t ⊆ B \<down>≤ t" and
  cut_greater_subset_mono: "A ⊆ B ==> A \<down>> t ⊆ B \<down>> t" and
  cut_ge_subset_mono:      "A ⊆ B ==> A \<down>≥ t ⊆ B \<down>≥ 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 \<down>< t ⊆ I \<down>< t'" and
  cut_greater_mono: "t' ≤ t ==> I \<down>> t ⊆ I \<down>> t'" and
  cut_le_mono:      "t ≤ t' ==> I \<down>≤ t ⊆ I \<down>≤ t'" and
  cut_ge_mono:      "t' ≤ t ==> I \<down>≥ t ⊆ I \<down>≥ 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 \<down>≤ a \<down>≤ b = i \<down>≤ min a b" and
  cut_cut_less: "i \<down>< a \<down>< b = i \<down>< min a b" and
  cut_cut_ge: "i \<down>≥ a \<down>≥ b = i \<down>≥ max a b" and
  cut_cut_greater: "i \<down>> a \<down>> b = i \<down>> 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 = op \<down>< ∨ cut_op = op \<down>≤ ∨ 
    cut_op = op \<down>> ∨ cut_op = op \<down>≥ |]
  ==> cut_op (cut_op I t) t = cut_op I t"
thm i_cut_set_restriction_disj[where f="λI. cut_op I t"]
apply (drule i_cut_set_restriction_disj[where f="λI. cut_op I t"], blast)
thm set_restriction_absorb
apply (blast dest: set_restriction_absorb)
done
corollary
  cut_le_absorb:      "I \<down>≤ t \<down>≤ t = I \<down>≤ t" and
  cut_less_absorb:    "I \<down>< t \<down>< t = I \<down>< t" and
  cut_ge_absorb:      "I \<down>≥ t \<down>≥ t = I \<down>≥ t" and
  cut_greater_absorb: "I \<down>> t \<down>> t = I \<down>> t"
thm i_cut_absorb_disj
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 \<down>< (0::nat) = {}" and
  cut_ge_0_all:     "I \<down>≥ (0::nat) = I"
unfolding i_cut_defs by blast+

lemma
  cut_le_all_iff:      "(I \<down>≤ t = I) = (∀x∈I. x ≤ t)" and
  cut_less_all_iff:    "(I \<down>< t = I) = (∀x∈I. x < t)" and
  cut_ge_all_iff:      "(I \<down>≥ t = I) = (∀x∈I. x ≥ t)" and
  cut_greater_all_iff: "(I \<down>> 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 \<down>≤ t = {}) = (∀x∈I. t < x)" and
  cut_less_empty_iff:    "(I \<down>< t = {}) = (∀x∈I. t ≤ x)" and
  cut_ge_empty_iff:      "(I \<down>≥ t = {}) = (∀x∈I. x < t)" and
  cut_greater_empty_iff: "(I \<down>> t = {}) = (∀x∈I. x ≤ t)"
unfolding i_cut_defs by fastsimp+
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 \<down>≤ t ≠ {}) = (∃x∈I. x ≤ t)" and
  cut_less_not_empty_iff:    "(I \<down>< t ≠ {}) = (∃x∈I. x < t)" and
  cut_ge_not_empty_iff:      "(I \<down>≥ t ≠ {}) = (∃x∈I. t ≤ x)" and
  cut_greater_not_empty_iff: "(I \<down>> 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
thm i_cut_not_empty_iff

lemma nat_cut_ge_infinite_not_empty: "infinite I ==> I \<down>≥ (t::nat) ≠ {}"
by (drule infinite_nat_iff_unbounded_le[THEN iffD1], blast)
lemma nat_cut_greater_infinite_not_empty: "infinite I ==> I \<down>> (t::nat) ≠ {}"
by (drule infinite_nat_iff_unbounded[THEN iffD1], blast)




thm set_restriction_not_in_imp
corollary 
  cut_le_not_in_imp:      "x ∉ I ==> x ∉ I \<down>≤ t" and
  cut_less_not_in_imp:    "x ∉ I ==> x ∉ I \<down>< t" and
  cut_ge_not_in_imp:      "x ∉ I ==> x ∉ I \<down>≥ t" and
  cut_greater_not_in_imp: "x ∉ I ==> x ∉ I \<down>> t"
thm i_cut_set_restriction[THEN set_restriction_not_in_imp] 
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

thm set_restriction_in_imp
corollary 
  cut_le_in_imp:      "x ∈ I \<down>≤ t ==> x ∈ I" and
  cut_less_in_imp:    "x ∈ I \<down>< t ==> x ∈ I" and
  cut_ge_in_imp:      "x ∈ I \<down>≥ t ==> x ∈ I" and
  cut_greater_in_imp: "x ∈ I \<down>> t ==> x ∈ I"
thm i_cut_set_restriction[THEN set_restriction_in_imp] 
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 \<down>< 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 \<down>< 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 \<down>< x). ¬ P y)"
by (drule Collect_minI_ex2, blast)





lemma cut_le_cut_greater_ident: "t2 ≤ t1 ==> I \<down>≤ t1 ∪ I \<down>> t2 = I"
by fastsimp
lemma cut_less_cut_ge_ident: "t2 ≤ t1 ==> I \<down>< t1 ∪ I \<down>≥ t2 = I"
by fastsimp
lemma cut_le_cut_ge_ident: "t2 ≤ t1 ==> I \<down>≤ t1 ∪ I \<down>≥ t2 = I"
by fastsimp

lemma cut_less_cut_greater_ident: "
  [| t2 ≤ t1; I ∩ {t1..t2} = {} |] ==> I \<down>< t1 ∪ I \<down>> t2 = I"
by fastsimp
corollary cut_less_cut_greater_ident': "
  t ∉ I ==> I \<down>< t ∪ I \<down>> t = I"
by (simp add: cut_less_cut_greater_ident)

lemma insert_eq_cut_less_cut_greater: "insert n I = I \<down>< n ∪ {n} ∪ I \<down>> n"
by fastsimp



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 \<down>≤ t = (
  if t ∈ I then insert t (I \<down>< t) else (I \<down>< t))"
by (simp add: i_cut_Int_conv lessThan_insert[symmetric] insert_Int_conv_if)

lemma cut_le_less_conv: "I \<down>≤ t = ({t} ∩ I) ∪ (I \<down>< t)"
by fastsimp

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







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



lemma nat_cut_le_less_conv: "I \<down>≤ t = I \<down>< Suc t"
by fastsimp
lemma nat_cut_less_le_conv: "0 < t ==> I \<down>< t = I \<down>≤ (t - Suc 0)"
by fastsimp
lemma nat_cut_ge_greater_conv: "I \<down>≥ Suc t = I \<down>> t"
by fastsimp
lemma nat_cut_greater_ge_conv: "0 < t ==> I \<down>> (t - Suc 0) = I \<down>≥ t"
by fastsimp





subsubsection {* Function images with cut operators *}

lemma cut_less_image: "
  [| strict_mono_on f A; I ⊆ A; n ∈ A |] ==> 
  (f ` I) \<down>< f n = f ` (I \<down>< 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 set_rev_mp)
apply blast
done

lemma cut_le_image: "
  [| strict_mono_on f A; I ⊆ A; n ∈ A |] ==> 
  (f ` I) \<down>≤ f n = f ` (I \<down>≤ n)"
apply (frule strict_mono_on_imp_inj_on)
thm cut_le_less_conv_if
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) \<down>> f n = f ` (I \<down>> 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 set_rev_mp)
apply blast
done

lemma cut_ge_image: "
  [| strict_mono_on f A; I ⊆ A; n ∈ A |] ==> 
  (f ` I) \<down>≥ f n = f ` (I \<down>≥ n)"
apply (frule strict_mono_on_imp_inj_on)
thm cut_ge_greater_conv_if
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
thm i_cut_image
thm i_cut_image[OF _ subset_refl]






subsubsection {* Finiteness and cardinality with cut operators *}

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


lemma nat_cut_le_finite: "finite (I \<down>≤ (t::nat))"
by (fastsimp simp: finite_nat_iff_bounded_le2 cut_le_def)
lemma nat_cut_less_finite: "finite (I \<down>< (t::nat))"
by (fastsimp simp: finite_nat_iff_bounded2 cut_less_def)
lemma nat_cut_ge_finite_iff: "finite (I \<down>≥ (t::nat)) = finite I"
apply (rule iffI)
 thm cut_less_cut_ge_ident[OF order_refl]
 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 \<down>> (t::nat)) = finite I"
thm cut_ge_greater_conv
by (simp only: nat_cut_ge_greater_conv[symmetric] nat_cut_ge_finite_iff)

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

lemma nat_cut_greater_card: "card (I \<down>> (t::nat)) ≤ card I"
apply (case_tac "finite I")
 apply (simp add: cut_greater_card)
thm nat_cut_greater_finite_iff
apply (simp add: nat_cut_greater_finite_iff)
done
lemma nat_cut_ge_card: "card (I \<down>≥ (t::nat)) ≤ card I"
apply (case_tac "finite I")
 apply (simp add: cut_ge_card)
thm nat_cut_ge_finite_iff
apply (simp add: nat_cut_ge_finite_iff)
done









subsubsection {* Cutting a set at  @{text Min} or @{text Max} element *}

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

lemma cut_le_Min_empty: "t < iMin I ==> I \<down>≤ t = {}"
by (fastsimp simp: i_cut_defs)
lemma cut_less_Min_empty: "t ≤ iMin I ==> I \<down>< t = {}"
by (fastsimp simp: i_cut_defs)


lemma cut_le_Min_not_empty: "[| I ≠ {}; iMin I ≤ t |] ==> I \<down>≤ t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="iMin I" in exI)
thm iMinI_ex2
apply (simp add: iMinI_ex2)
done
lemma cut_less_Min_not_empty: "[| I ≠ {}; iMin I < t |] ==> I \<down>< 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 \<down>≥ t = I"
apply (simp add: i_cut_defs)
apply safe
thm iMin_le
apply (drule iMin_le, simp)
done

lemma cut_greater_Min_all: "t < iMin I ==> I \<down>> t = I"
apply (simp add: i_cut_defs)
apply safe
thm iMin_le
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

thm 
  i_cut_min_empty
  i_cut_min_all

lemma cut_ge_Max_empty: "finite I ==> Max I < t ==> I \<down>≥ t = {}"
by (fastsimp simp: i_cut_defs)

lemma cut_greater_Max_empty: "finite I ==> Max I ≤ t ==> I \<down>> t = {}"
by (fastsimp simp: i_cut_defs)

lemma cut_ge_Max_not_empty: "[| I ≠ {}; finite I; t ≤ Max I |] ==> I \<down>≥ t ≠ {}"
apply (simp add: i_cut_defs)
apply (rule_tac x="Max I" in exI)
thm MaxI_ex2
apply (simp add: MaxI_ex2)
done

lemma cut_greater_Max_not_empty: "[| I ≠ {}; finite I; t < Max I |] ==> I \<down>> 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 \<down>≤ t = I"
by (fastsimp simp: i_cut_defs)

lemma cut_less_Max_all: "finite I ==> Max I < t ==> I \<down>< t = I"
by (fastsimp 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

thm 
  i_cut_max_empty
  i_cut_max_all


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



lemma cut_less_Min_eq: "I \<down>< t ≠ {} ==> iMin (I \<down>< t) = iMin I"
apply (drule cut_less_not_empty_iff[THEN iffD1])
apply (rule iMin_equality)
 apply (fastsimp intro: iMinI)
apply blast
done

lemma cut_le_Min_eq: "I \<down>≤ t ≠ {} ==> iMin (I \<down>≤ t) = iMin I"
apply (drule cut_le_not_empty_iff[THEN iffD1])
apply (rule iMin_equality)
 apply (fastsimp intro: iMinI)
apply blast
done


lemma cut_ge_Max_eq: "[| finite I; I \<down>≥ t ≠ {} |] ==> Max (I \<down>≥ t) = Max I"
apply (drule cut_ge_not_empty_iff[THEN iffD1])
apply (rule Max_equality)
  apply (fastsimp intro: MaxI)
 apply (simp add: cut_ge_finite)
apply fastsimp
done

lemma cut_greater_Max_eq: "[| finite I; I \<down>> t ≠ {} |] ==> Max (I \<down>> t) = Max I"
apply (drule cut_greater_not_empty_iff[THEN iffD1])
apply (rule Max_equality)
  apply (fastsimp intro: MaxI)
 apply (simp add: cut_greater_finite)
apply fastsimp
done



subsubsection {* Cut operators with intervals from SetInterval *}

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

lemma 
  lessThan_cut_le:      "{..<n} \<down>≤ t = (if n ≤ t then {..<n} else {..t})" and
  lessThan_cut_less:    "{..<n} \<down>< t = (if n ≤ t then {..<n} else {..<t})" and
  lessThan_cut_ge:      "{..<n} \<down>≥ t = {t..<n}" and
  lessThan_cut_greater: "{..<n} \<down>> t = {t<..<n}" and
  atMost_cut_le:      "{..n} \<down>≤ t = (if n ≤ t then {..n} else {..t})" and
  atMost_cut_less:    "{..n} \<down>< t = (if n < t then {..n} else {..<t})" and
  atMost_cut_ge:      "{..n} \<down>≥ t = {t..n}" and
  atMost_cut_greager: "{..n} \<down>> t = {t<..n}" and
  greaterThan_cut_le:      "{n<..} \<down>≤ t = {n<..t}" and
  greaterThan_cut_less:    "{n<..} \<down>< t = {n<..<t}" and
  greaterThan_cut_ge:      "{n<..} \<down>≥ t = (if t ≤ n then {n<..} else {t..})" and
  greaterThan_cut_greater: "{n<..} \<down>> t = (if t ≤ n then {n<..} else {t<..})" and
  atLeast_cut_le:      "{n..} \<down>≤ t = {n..t}" and
  atLeast_cut_less:    "{n..} \<down>< t = {n..<t}" and
  atLeast_cut_ge:      "{n..} \<down>≥ t = (if t ≤ n then {n..} else {t..})" and
  atLeast_cut_greater: "{n..} \<down>≥ 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 fastsimp+
done


lemma 
  greaterThanLessThan_cut_le:      "{m<..<n} \<down>≤ t = (if n ≤ t then {m<..<n} else {m<..t})" and
  greaterThanLessThan_cut_less:    "{m<..<n} \<down>< t = (if n ≤ t then {m<..<n} else {m<..<t})" and
  greaterThanLessThan_cut_ge:      "{m<..<n} \<down>≥ t = (if t ≤ m then {m<..<n} else {t..<n})" and
  greaterThanLessThan_cut_greater: "{m<..<n} \<down>> t = (if t ≤ m then {m<..<n} else {t<..<n})" and
  atLeastLessThan_cut_le:      "{m..<n} \<down>≤ t = (if n ≤ t then {m..<n} else {m..t})" and
  atLeastLessThan_cut_less:    "{m..<n} \<down>< t = (if n ≤ t then {m..<n} else {m..<t})" and
  atLeastLessThan_cut_ge:      "{m..<n} \<down>≥ t = (if t ≤ m then {m..<n} else {t..<n})" and
  atLeastLessThan_cut_greater: "{m..<n} \<down>> t = (if t < m then {m..<n} else {t<..<n})" and
  greaterThanAtMost_cut_le:      "{m<..n} \<down>≤ t = (if n ≤ t then {m<..n} else {m<..t})" and
  greaterThanAtMost_cut_less:    "{m<..n} \<down>< t = (if n < t then {m<..n} else {m<..<t})" and
  greaterThanAtMost_cut_ge:      "{m<..n} \<down>≥ t = (if t ≤ m then {m<..n} else {t..n})" and
  greaterThanAtMost_cut_greater: "{m<..n} \<down>> t = (if t ≤ m then {m<..n} else {t<..n})" and
  atLeastAtMost_cut_le:      "{m..n} \<down>≤ t = (if n ≤ t then {m..n} else {m..t})" and
  atLeastAtMost_cut_less:    "{m..n} \<down>< t = (if n < t then {m..n} else {m..<t})" and
  atLeastAtMost_cut_ge:      "{m..n} \<down>≥ t = (if t ≤ m then {m..n} else {t..n})" and
  atLeastAtMost_cut_greater: "{m..n} \<down>> t = (if t < m then {m..n} else {t<..n})"
apply (simp_all add: set_eq_iff i_cut_mem_iff split_if linorder_not_le linorder_not_less)
apply fastsimp+
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 fastsimp

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 fastsimp

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 fastsimp

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 fastsimp

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_leE 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



thm nat_mirror_le_conv
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)

thm nat_mirror_eq_conv
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)
thm iMin_equality
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)
thm imirror_iMin imirror_Max
apply (fastsimp simp: imirror_iMin imirror_Max)
done

thm image_iff
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)
thm nat_mirror_nat_mirror_ident
apply (rule iffI)
 apply (fastsimp simp: nat_mirror_nat_mirror_ident)
apply (rule_tac x=x in bexI)
apply (fastsimp 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)
thm imirror_eq_imirror_bounds
thm imirror_bounds_imirror_bounds_ident
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)
thm inj_on_image_mem_iff[where A="{..l + r}"]
apply (rule inj_on_image_mem_iff)
apply (rule nat_mirror_inj_on)
apply fastsimp
apply simp
done

lemma imirror_mem_conv: "
  [| finite I; n ≤ iMin I + Max I |] ==> ((mirror_elem n I) ∈ imirror I) = (n ∈ I)"
thm imirror_bounds_elem_conv
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"
thm imirror_mem_conv[OF _ trans_le_add2[OF Max_ge], THEN iffD2]
by (rule imirror_mem_conv[OF _ trans_le_add2[OF Max_ge], THEN iffD2])

lemma imirror_cut_less: "
  finite I ==> 
  imirror I \<down>< (mirror_elem t I) = 
  imirror_bounds (I \<down>> 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)
 thm nat_mirror_less_imp_less
 apply (bestsimp intro: nat_mirror_less_imp_less)
thm nat_mirror_less
apply (bestsimp simp add: nat_mirror_less)
done

lemma imirror_cut_le: "
  [| finite I; t ≤ iMin I + Max I |] ==> 
  imirror I \<down>≤ (mirror_elem t I) = 
  imirror_bounds (I \<down>≥ t) (iMin I) (Max I)"
thm nat_cut_le_less_conv nat_cut_greater_ge_conv
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])
thm imirror_cut_less
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 \<down>≥ (mirror_elem t I) = 
  imirror_bounds (I \<down>≤ 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) \<down>≤ mirror_elem (mirror_elem t I) (imirror I)" "I \<down>≤ t"])
 thm mirror_elem_mirror_elem_ident
 apply (simp add: imirror_imirror_ident mirror_elem_imirror mirror_elem_mirror_elem_ident)
thm imirror_cut_le[of "imirror I" "mirror_elem t I", OF imirror_finite]
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 \<down>> (mirror_elem t I) = 
  imirror_bounds (I \<down>< 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)
thm nat_cut_ge_greater_conv
apply (simp add: nat_cut_ge_greater_conv[symmetric])
thm subst[of "mirror_elem (t - Suc 0) I" "Suc (mirror_elem t I)"]
apply (rule subst[of "mirror_elem (t - Suc 0) I" "Suc (mirror_elem t I)"])
 thm nat_mirror_diff
 apply (simp add: mirror_elem_def nat_mirror_diff)
thm imirror_cut_ge nat_cut_less_le_conv
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
thm imirror_cut

corollary imirror_cut_le': "
  [| finite I; t ∈ I |] ==> 
  imirror I \<down>≤ mirror_elem t I =
  imirror_bounds (I \<down>≥ t) (iMin I) (Max I)"
thm imirror_cut_le[OF _ trans_le_add2[OF Max_ge]]
by (rule imirror_cut_le[OF _ trans_le_add2[OF Max_ge]])
corollary imirror_cut_greater': "
  [| finite I; t ∈ I |] ==> 
  imirror I \<down>> mirror_elem t I =
  imirror_bounds (I \<down>< 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'
thm 
  imirror_cut
  imirror_cut'
  


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)
thm inj_on_image_Int[OF _ Un_upper1 Un_upper2]
apply (rule inj_on_image_Int[OF _ Un_upper1 Un_upper2])
thm nat_mirror_inj_on
thm subset_inj_on[OF nat_mirror_inj_on]
apply (rule subset_inj_on[OF nat_mirror_inj_on])
apply (rule Un_least[of A _ B], assumption+)
done

end