Theory NatInt

(*  Title:      NatInt.thy
    Author:     Sven Linker, University of Liverpool

Intervals based on natural numbers. Defines a 
bottom element (empty set), infimum (set intersection),
partial order (subset relation), cardinality (set cardinality).

The union of intervals i and j can only be created, if they are consecutive, i.e.,
max i +1 = min j (or vice versa). To express consecutiveness, we employ the 
predicate consec.

Also contains a "chopping" predicate N_Chop(i,j,k): i can be divided into
consecutive intervals j and k.
*)

section ‹Discrete Intervals based on Natural Numbers›

text‹We define a type of intervals based on the natural numbers. To that 
end, we employ standard operators of Isabelle, but in addition prove some
structural properties of the intervals. In particular, we show that this type
constitutes a meet-semilattice with a bottom element and equality.

Furthermore, we show that this semilattice allows for a constrained join, i.e.,
the union of two intervals is defined, if either one of them is empty, or they are
consecutive. Finally, we define the notion of \emph{chopping} an interval into
two consecutive subintervals.›

theory NatInt
  imports Main 
begin

text ‹A discrete interval is a set of consecutive natural numbers, or the empty 
set.›

typedef nat_int = "{S . ( (m::nat) n . {m..n }=S) }"  
  by auto
setup_lifting type_definition_nat_int

subsection ‹Basic properties of discrete intervals.›
  
locale nat_int 
interpretation nat_int_class?: nat_int .

context nat_int
begin
  
lemma un_consec_seq: "(m::nat) n  n+1  l  {m..n}  {n+1..l} = {m..l}" 
  by auto
    
lemma int_conseq_seq: " {(m::nat)..n}  {n+1..l} = {}"
  by auto
        
lemma empty_type: "{}  { S .  (m:: nat) n . {m..n}=S}"
  by auto
    
lemma inter_result: "x  {S . ( (m::nat) n .  {m..n }=S) }. 
         y  {S . ( (m::nat) n . {m..n }=S) }. 
           x  y {S . ( (m::nat) n .  {m..n }=S)}" 
  using Int_atLeastAtMost by blast      
    
lemma union_result: "x  {S . ( (m::nat) n .  {m..n }=S) }. 
         y  {S . ( (m::nat) n .  {m..n }=S)  }. 
           x  {}  y  {}  Max x +1 = Min y 
             x  y {S . ( (m::nat) n . {m..n }=S)  }"  
proof (rule ballI)+
  fix x y
  assume "x {S . ( (m::nat) n .  {m..n }=S) }" 
    and "y {S . ( (m::nat) n .  {m..n }=S) }"
  then have x_def:"(m n.  {m..n} = x) "  
    and y_def:"(m n.  {m..n} = y) " by blast+    
  show   " x  {}  y  {}    Max x+1 = Min y 
             x   y  {S. (m n.  {m..n} = S) }"
  proof
    assume pre:"x  {}  y  {}  Max x + 1 = Min y"
    then have x_int:"m n. m  n  {m..n} = x" 
          and y_int:"(m n. m  n  {m..n} = y)"
      using  x_def y_def by force+      
    {
      fix ya yb xa xb
      assume y_prop:"ya  yb  {ya..yb} = y" and x_prop:"xa  xb  {xa..xb} = x"          
      then have upper_x:"Max x = xb" and lower_y: "Min y = ya" 
        by (auto simp: Max_eq_iff Min_eq_iff)
      from upper_x and lower_y and pre have upper_eq_lower: "xb+1 = ya" 
        by blast
      hence "y= {xb+1 .. yb}" using y_prop by blast
      hence "x  y = {xa..yb}" 
        using un_consec_seq upper_eq_lower x_prop y_prop by blast
      then have " x  y  {S.(m n.  {m..n} = S) }"
        by auto
    }      
    then show "x  y  {S.(m n.  {m..n} = S)}" 
      using x_int y_int by blast
  qed
qed
  
  

lemma union_empty_result1: "i  {S . ( (m::nat) n .  {m..n }=S) }.
                                  i  {}  {S . ( (m::nat) n .  {m..n }=S) }" 
  by blast   

lemma union_empty_result2: "i  {S . ( (m::nat) n . {m..n }=S)  }.
                                  {}  i  {S . ( (m::nat) n . {m..n }=S)  }" 
  by blast 
    
lemma finite:" i  {S . ( (m::nat) n .  {m..n }=S) } . (finite i)"
  by blast
    
lemma not_empty_means_seq:"i  {S . ( (m::nat) n .  {m..n }=S) } . i  {}
                             ( m n . m  n  {m..n} = i)" 
  using atLeastatMost_empty_iff 
  by force   
end
  
text ‹The empty set is the bottom element of the type. The infimum/meet of 
the semilattice is set intersection. The order is given by the subset relation.
›

instantiation nat_int :: bot
begin
lift_definition bot_nat_int :: "nat_int" is Set.empty by force
instance by standard
end

instantiation nat_int ::  inf
begin
lift_definition inf_nat_int  ::"nat_int  nat_int  nat_int" is Set.inter  by force
instance
proof qed
end

instantiation nat_int :: "order_bot"
begin
lift_definition less_eq_nat_int :: "nat_int  nat_int  bool" is Set.subset_eq .
lift_definition less_nat_int :: "nat_int  nat_int  bool" is Set.subset .
instance
proof
  fix i j k ::nat_int
  show "(i < j) = (i  j  ¬ j  i)" 
    by (simp add: less_eq_nat_int.rep_eq less_le_not_le less_nat_int.rep_eq)
  show "i  i" by (simp add:less_eq_nat_int.rep_eq) 
  show " i  j  j  k  i  k" by (simp add:less_eq_nat_int.rep_eq)
  show "i  j  j  i  i = j"  
    by (simp add: Rep_nat_int_inject less_eq_nat_int.rep_eq )
  show "bot  i" using  less_eq_nat_int.rep_eq 
    using bot_nat_int.rep_eq by blast
qed
end  

instantiation nat_int ::  "semilattice_inf"
begin
instance 
proof
  fix i j k :: nat_int
  show "i  j  i  k  i  inf j k" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq)
  show " inf i   j  i" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
  show "inf i  j  j" 
    by (simp add: inf_nat_int.rep_eq less_eq_nat_int.rep_eq) 
qed      
end

instantiation nat_int:: "equal"
begin
definition equal_nat_int :: "nat_int  nat_int  bool"  
  where "equal_nat_int i  j  i  j  j  i"
instance 
proof
  fix i j :: nat_int
  show " equal_class.equal i j = (i = j)" using equal_nat_int_def  by auto
qed
end
  
  
context nat_int 
begin
abbreviation subseteq :: "nat_int  nat_int bool" (infix "" 30)
  where  "i  j == i  j "
abbreviation empty :: "nat_int" ("")
  where "  bot"
    
notation inf (infix "" 70)


text ‹The union of two intervals is only defined, if it is also
a discrete interval.›
definition union :: "nat_int  nat_int  nat_int" (infix "" 65)
  where "i  j = Abs_nat_int (Rep_nat_int i  Rep_nat_int j)"

text ‹Non-empty intervals contain a minimal and maximal element. 
Two non-empty intervals \(i\) and \(j\) are 
consecutive, if the minimum of \(j\) is the successor of the
maximum of \(i\).
Furthermore, the interval \(i\) can be chopped into the intervals \(j\)
and \(k\), if the union of \(j\) and \(k\) equals \(i\), and if \(j\)
and \(k\) are not-empty, they must be consecutive. Finally, we define
the cardinality of discrete intervals by lifting the cardinality of
sets. 
›
definition maximum :: "nat_int  nat"
  where maximum_def: "i    maximum (i) =   Max (Rep_nat_int i)" 
    
definition minimum :: "nat_int  nat"
  where minimum_def: "i    minimum(i) = Min (Rep_nat_int i)"

definition consec:: "nat_intnat_int  bool" 
  where "consec i j  (i  j    (maximum(i)+1 = minimum j))"
    
definition N_Chop :: "nat_int  nat_int  nat_int  bool" ("N'_Chop'(_,_,_')" 51)
  where nchop_def :
    "N_Chop(i,j,k)  (i =  j  k    (j =    k =   consec j k))"

lift_definition card' ::"nat_int  nat"  ( "|_|" 70) is card .


text‹For convenience, we also lift the membership relation and its negation
to discrete intervals.›

lift_definition el::"nat  nat_int  bool" (infix "" 50) is "Set.member" .

lift_definition not_in ::"nat  nat_int  bool" (infix "" 40)  is Set.not_member . 
end
  
lemmas[simp] = nat_int.el.rep_eq nat_int.not_in.rep_eq nat_int.card'.rep_eq

context nat_int 
begin
  
lemma in_not_in_iff1 :"n  i  ¬ n i" by simp
lemma in_not_in_iff2: "n i  ¬ n  i" by simp
    
    
lemma rep_non_empty_means_seq:"i  
                                 (m n. m  n  ({m..n} =( Rep_nat_int i)))" 
  by (metis Rep_nat_int Rep_nat_int_inject bot_nat_int.rep_eq nat_int.not_empty_means_seq)
  
lemma non_empty_max: "i    (m . maximum(i) = m)" 
  by auto
    
lemma non_empty_min: "i    (m . minimum(i) = m)" 
  by auto
    
lemma minimum_in: "i    minimum i  i"
  by (metis Min_in atLeastatMost_empty_iff2 finite_atLeastAtMost minimum_def
      el.rep_eq rep_non_empty_means_seq)
    
lemma maximum_in: "i    maximum i  i"
  by (metis Max_in atLeastatMost_empty_iff2 finite_atLeastAtMost maximum_def 
      el.rep_eq rep_non_empty_means_seq)
    
lemma non_empty_elem_in:"i    (n. n  i)"   
proof
  assume assm:"i  "
  show "n . n  i" 
    by (metis assm Rep_nat_int_inverse all_not_in_conv el.rep_eq bot_nat_int_def)
next
  assume assm:"n. n  i"
  show "i  " 
    using Abs_nat_int_inverse assm el.rep_eq bot_nat_int_def by fastforce
qed
  
lemma leq_nat_non_empty:"(m::nat)  n  Abs_nat_int{m..n}  "  
proof
  assume assm:"m n"
  then have non_empty:"{m..n}  {} " 
    using atLeastatMost_empty_iff by blast
  with assm have "{m..n}  {S . ( (m::nat) n .  {m..n }=S)  }" by blast
  then show "Abs_nat_int {m..n}  " 
    using Abs_nat_int_inject empty_type non_empty bot_nat_int_def 
    by (simp add: bot_nat_int.abs_eq)
qed
  
lemma leq_max_sup:"(m::nat)  n  Max {m..n} = n" 
  by (auto simp: Max_eq_iff)
    
lemma leq_min_inf: "(m::nat)  n  Min {m..n} = m"
  by (auto simp: Min_eq_iff)
    
lemma leq_max_sup':"(m::nat)  n  maximum(Abs_nat_int{m..n}) = n" 
proof 
  assume assm:"m  n"
  hence in_type:"{m..n}  {S . ( (m::nat) n . m  n  {m..n }=S)  S={} }" by blast
  from assm have "Abs_nat_int{m..n}  " using leq_nat_non_empty by blast
  hence max:"maximum(Abs_nat_int{m..n}) = Max (Rep_nat_int (Abs_nat_int {m..n}))"
    using maximum_def by blast
  from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}" 
    using Abs_nat_int_inverse by blast
  hence  "Max (Rep_nat_int (Abs_nat_int{m..n})) = Max {m..n}" by simp
  with max have simp_max:"maximum(Abs_nat_int{m..n}) = Max {m..n}" by simp
  from assm have "Max {m..n} = n" using leq_max_sup by blast
  with simp_max show "maximum(Abs_nat_int{m..n}) = n" by simp
qed
  
lemma leq_min_inf':"(m::nat)  n  minimum(Abs_nat_int{m..n}) = m" 
proof 
  assume assm:"m  n"
  hence in_type:"{m..n}  {S . ( (m::nat) n . m  n  {m..n }=S)  S={} }" by blast
  from assm have "Abs_nat_int{m..n}  " using leq_nat_non_empty by blast
  hence min:"minimum(Abs_nat_int{m..n}) = Min(Rep_nat_int (Abs_nat_int {m..n}))"
    using  minimum_def by blast
  from in_type have " (Rep_nat_int (Abs_nat_int {m..n})) = {m..n}" 
    using Abs_nat_int_inverse by blast
  hence  "Min (Rep_nat_int (Abs_nat_int{m..n})) = Min {m..n}" by simp
  with min have simp_min:"minimum(Abs_nat_int{m..n}) = Min {m..n}" by simp
  from assm have "Min {m..n} = m" using leq_min_inf by blast
  with simp_min show "minimum(Abs_nat_int{m..n}) = m" by simp
qed
  
lemma in_refl:"(n::nat)   Abs_nat_int {n}"
proof -
  have "(n::nat)  n" by simp
  hence "{n}  {S . ( (m::nat) n . m  n  {m..n }=S)  S={} }" by auto
  then show "n  Abs_nat_int {n}" 
    by (simp add: Abs_nat_int_inverse el_def)
qed
  
lemma in_singleton:" m  Abs_nat_int{n}  m = n"
proof
  assume assm:" m  Abs_nat_int{n}"
  have "(n::nat)  n" by simp
  hence "{n}  {S . ( (m::nat) n . m  n  {m..n }=S)  S={} }" by auto
  with assm show "m=n" by (simp add: Abs_nat_int_inverse el_def)
qed

subsection ‹Algebraic properties of intersection and union.›
  
lemma inter_empty1:"(i::nat_int)   = " 
  using Rep_nat_int_inject inf_nat_int.rep_eq bot_nat_int.abs_eq bot_nat_int.rep_eq 
  by fastforce 
    
lemma inter_empty2:"  (i::nat_int) = " 
  by (metis inf_commute nat_int.inter_empty1)
        
lemma un_empty_absorb1:"i   = i" 
  using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
  by auto
    
lemma un_empty_absorb2:"  i = i" 
  using  Abs_nat_int_inverse Rep_nat_int_inverse union_def empty_type bot_nat_int.rep_eq
  by auto

text ‹Most properties of the union of two intervals depends on them being consectuive,
to ensure that their union exists.›

lemma consec_un:"consec i j  n  Rep_nat_int(i)  Rep_nat_int j 
                   n   (i  j)"
proof
  assume assm:"consec i j  n   Rep_nat_int i  Rep_nat_int j" 
  thus "n  (i  j)" 
  proof -
    have f1: "Abs_nat_int (Rep_nat_int (i  j)) 
              = Abs_nat_int (Rep_nat_int i  Rep_nat_int j)"
      using Rep_nat_int_inverse union_def by presburger
    have "i    j    maximum i + 1 = minimum j"
      using assm consec_def by auto
    then have "n na. {n..na} = Rep_nat_int i  Rep_nat_int j" 
      by (metis (no_types) leq_max_sup leq_min_inf maximum_def minimum_def 
          rep_non_empty_means_seq un_consec_seq)
    then show ?thesis
      using f1 Abs_nat_int_inject Rep_nat_int not_in.rep_eq assm by auto
  qed
qed
    
lemma un_subset1: "consec i j  i  i  j" 
proof
  assume "consec i j"
  then have assm:"i    j    maximum i+1 = minimum j" 
    using consec_def by blast
  have "Rep_nat_int i  Rep_nat_int j =  {minimum i.. maximum j}" 
    by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def 
        nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
  then show "i  i  j" using Abs_nat_int_inverse Rep_nat_int 
    by (metis (mono_tags, lifting) Un_upper1 less_eq_nat_int.rep_eq mem_Collect_eq
        nat_int.union_def)
qed
  
lemma un_subset2: "consec i j  j  i  j"
proof
  assume "consec i j"
  then have assm:"i    j    maximum i+1 = minimum j" 
    using consec_def by blast
  have "Rep_nat_int i  Rep_nat_int j =  {minimum i.. maximum j}" 
    by (metis assm nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def 
        nat_int.minimum_def nat_int.rep_non_empty_means_seq nat_int.un_consec_seq)
  then show "j  i  j" using Abs_nat_int_inverse Rep_nat_int
    by (metis (mono_tags, lifting) Un_upper2 less_eq_nat_int.rep_eq mem_Collect_eq
        nat_int.union_def)
qed
 
lemma inter_distr1:"consec j k  i  (j  k) = (i  j)  (i  k)"  
  unfolding consec_def
proof  
  assume assm:"j    k    maximum j +1 = minimum k"
  then show " i  (j  k) = (i  j)  (i  k)"  
  proof -
    have f1: "n. n =   maximum n = Max (Rep_nat_int n)"
      using nat_int.maximum_def by auto
    have f2: "Rep_nat_int j  {}"
      using assm nat_int.maximum_in by auto
    have f3: "maximum j = Max (Rep_nat_int j)"
      using f1 by (meson assm)
    have "maximum k  k"
      using assm nat_int.maximum_in by blast
    then have "Rep_nat_int k  {}"
      by fastforce
    then have "Rep_nat_int (j  k) = Rep_nat_int j  Rep_nat_int k"
      using f3 f2 Abs_nat_int_inverse Rep_nat_int assm nat_int.minimum_def 
        nat_int.union_def union_result 
        by auto
    then show ?thesis
      by (metis Rep_nat_int_inverse inf_nat_int.rep_eq inf_sup_distrib1 nat_int.union_def)
  qed
qed
  
lemma inter_distr2:"consec j k  (j  k)  i = (j  i)  (k  i)"
  by (simp add: inter_distr1 inf_commute)
    
lemma consec_un_not_elem1:"consec i j  n i  j   n  i"
  using un_subset1 less_eq_nat_int.rep_eq not_in.rep_eq by blast 
    
lemma consec_un_not_elem2:"consec i j  n i  j   n  j"
  using  un_subset2 less_eq_nat_int.rep_eq not_in.rep_eq by blast
    
lemma consec_un_element1:"consec i j  n  i  n  i  j" 
  using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset1 by blast
    
lemma consec_un_element2:"consec i j  n  j  n  i  j"
  using less_eq_nat_int.rep_eq nat_int.el.rep_eq nat_int.un_subset2 by blast
    
lemma consec_lesser:" consec i j   (n m. (n  i  m  j  n < m))" 
proof (rule allI|rule impI)+
  assume "consec i j"
  fix n and m  
  assume assump:"n  i  m  j "
  then have  max:"n  maximum i" 
    by (metis consec i j atLeastAtMost_iff leq_max_sup maximum_def consec_def
        el.rep_eq rep_non_empty_means_seq)
  from assump have min: "m  minimum j" 
    by (metis Min_le consec i j finite_atLeastAtMost minimum_def consec_def
        el.rep_eq rep_non_empty_means_seq)
  from min and max show less:"n < m" 
    using One_nat_def Suc_le_lessD consec i j add.right_neutral add_Suc_right
      dual_order.trans leD leI consec_def by auto
qed

lemma consec_in_exclusive1:"consec i j  n  i  n  j" 
  using nat_int.consec_lesser nat_int.in_not_in_iff2 by blast

lemma consec_in_exclusive2:"consec i j  n  j  n  i"
  using consec_in_exclusive1 el.rep_eq not_in.rep_eq by blast

lemma consec_un_max:"consec i j  maximum j = maximum (i  j)"
proof
  assume assm:"consec i j"
  then have "(n m. (n  i  m  j  n < m))" 
    using nat_int.consec_lesser by blast
  then have "n . (n  i  n < maximum j)" 
    using assm local.consec_def nat_int.maximum_in by auto
  then have "n. (n  i  j  n  maximum j)" 
    by (metis (no_types, lifting) Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff
        bot_nat_int.rep_eq less_imp_le_nat local.consec_def local.not_empty_means_seq 
        nat_int.consec_un nat_int.el.rep_eq nat_int.in_not_in_iff1 nat_int.leq_max_sup')
  then show "maximum j = maximum (i  j)" 
    by (metis Rep_nat_int_inverse assm atLeastAtMost_iff bot.extremum_uniqueI
        le_antisym local.consec_def nat_int.consec_un_element2 nat_int.el.rep_eq
        nat_int.leq_max_sup' nat_int.maximum_in nat_int.un_subset2 rep_non_empty_means_seq)
qed

lemma consec_un_min:"consec i j  minimum i = minimum (i  j)"
proof
  assume assm:"consec i j"
  then have "(n m. (n  i  m  j  n < m))" 
    using nat_int.consec_lesser by blast
  then have "n . (n  j  n > minimum i)" 
    using assm local.consec_def nat_int.minimum_in by auto
  then have 1:"n. (n  i  j  n  minimum i)"  
    using Rep_nat_int Rep_nat_int_inverse Un_iff assm atLeastAtMost_iff bot_nat_int.rep_eq
      less_imp_le_nat local.consec_def local.not_empty_means_seq nat_int.consec_un 
      nat_int.el.rep_eq nat_int.in_not_in_iff1
    by (metis (no_types, lifting) leq_min_inf local.minimum_def)
  from assm have "i  j  " 
    by (metis bot.extremum_uniqueI nat_int.consec_def nat_int.un_subset2)
  then show "minimum i = minimum (i  j)" 
    by (metis "1" antisym assm atLeastAtMost_iff leq_min_inf nat_int.consec_def 
        nat_int.consec_un_element1 nat_int.el.rep_eq nat_int.minimum_def nat_int.minimum_in
        rep_non_empty_means_seq)
qed

lemma consec_un_defined:
  "consec i j  (Rep_nat_int (i  j)  {S . ( (m::nat) n . {m..n }=S) })"
  using Rep_nat_int by auto

lemma consec_un_min_max:
  "consec i j  Rep_nat_int(i  j) = {minimum i .. maximum j}"
proof
  assume assm:"consec i j"
  then have 1:"minimum j = maximum i +1" 
    by (simp add: nat_int.consec_def)
  have i:"Rep_nat_int i = {minimum i..maximum i}" 
    by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
        rep_non_empty_means_seq)
  have j:"Rep_nat_int j = {minimum j..maximum j}" 
    by (metis Rep_nat_int_inverse assm nat_int.consec_def nat_int.leq_max_sup' nat_int.leq_min_inf'
        rep_non_empty_means_seq)
  show "Rep_nat_int(i  j) = {minimum i .. maximum j}" 
    by (metis Rep_nat_int_inverse antisym assm bot.extremum i nat_int.consec_un_max
        nat_int.consec_un_min nat_int.leq_max_sup' nat_int.leq_min_inf' nat_int.un_subset1
        rep_non_empty_means_seq)
qed

lemma consec_un_equality: 
  "(consec i j  k  ) 
    ( minimum (i  j) = minimum (k)  maximum (i  j) = maximum (k))
       i  j = k"
proof (rule impI)+
  assume cons:"consec i j  k  "
  assume endpoints:" minimum(i  j) = minimum(k)  maximum(i  j) = maximum(k)"
  have "Rep_nat_int( i  j) = {minimum(i  j)..maximum(i  j)}" 
    by (metis cons leq_max_sup leq_min_inf local.consec_def nat_int.consec_un_element2
        nat_int.maximum_def nat_int.minimum_def nat_int.non_empty_elem_in rep_non_empty_means_seq)
  then have 1:"Rep_nat_int( i  j) = {minimum(k) .. maximum(k)}" 
    using endpoints by simp
  have "Rep_nat_int( k) = {minimum(k) .. maximum(k)}" 
    by (metis cons leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
        rep_non_empty_means_seq)
  then  show " i  j = k" using 1 
    by (metis Rep_nat_int_inverse)
qed

lemma consec_trans_lesser:
  "consec i j  consec j k  (n m. (n  i  m  k  n < m))"
proof (rule allI|rule impI)+
  assume cons:" consec i j  consec j k"
  fix n and m
  assume assump:"n  i  m  k "
  have "k . k  j  k < m" using consec_lesser assump cons by blast
  hence m_greater:"maximum j < m" using cons maximum_in consec_def by blast
  then show "n < m" 
    by (metis assump cons consec_def dual_order.strict_trans nat_int.consec_lesser
        nat_int.maximum_in)      
qed
  
lemma consec_inter_empty:"consec i j  i  j = " 
proof -
  assume "consec i j"
  then have "i  bot  j  bot  maximum i + 1 = minimum j"
    using consec_def by force
  then show ?thesis
    by (metis (no_types) Rep_nat_int_inverse bot_nat_int_def inf_nat_int.rep_eq int_conseq_seq
        nat_int.leq_max_sup nat_int.leq_min_inf nat_int.maximum_def nat_int.minimum_def
        nat_int.rep_non_empty_means_seq)
qed 
  
lemma consec_intermediate1:"consec j k  consec i (j  k)  consec i j "
proof
  assume assm:"consec j k  consec i (j  k)"
  hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast 
  hence min_max_xyz:"maximum i +1 = minimum (j  k)" 
      using consec_def assm by blast
  have min_y_yz:"minimum j = minimum (j  k)" 
    by (simp add: assm nat_int.consec_un_min)
  hence min_max_xy:"maximum i+1 = minimum j" 
    using min_max_xyz by simp
  thus consec_x_y:"consec i j" using assm consec_def by auto
qed
  
lemma consec_intermediate2:"consec i j  consec (i  j) k  consec j k "
proof
  assume assm:"consec i j  consec (i  j) k"
  hence min_max_yz:"maximum i +1=minimum j" using consec_def by blast 
  hence min_max_xyz:"maximum (i  j) +1 = minimum ( k)" 
      using consec_def assm by blast
  have min_y_yz:"maximum j = maximum (i  j)" 
    using assm nat_int.consec_un_max by blast
  then have min_max_xy:"maximum j+1 = minimum k" 
    using min_max_xyz by simp
  thus consec_x_y:"consec j k" using assm consec_def by auto
qed

lemma un_assoc: "consec i j  consec j k  (i  j)  k = i  (j  k)" 
proof 
  assume assm:"consec i j  consec j k"
  from assm have 3:"maximum (i  j) = maximum j" 
    using nat_int.consec_un_max by auto
  from assm have 4:"minimum (j  k) = minimum (j)" 
    using nat_int.consec_un_min by auto
  have "i  j  = Abs_nat_int{minimum i .. maximum j}" 
    by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
  then have 5:"(i  j)  k = Abs_nat_int{minimum i .. maximum k}" 
    by (metis (no_types, opaque_lifting) "3" Rep_nat_int_inverse antisym assm bot.extremum
        nat_int.consec_def nat_int.consec_un_min nat_int.consec_un_min_max nat_int.un_subset1)
  have "j  k = Abs_nat_int{minimum j .. maximum k}" 
    by (metis Rep_nat_int_inverse assm nat_int.consec_un_min_max)
  then have 6:"i  (j  k) = Abs_nat_int{minimum i .. maximum k}" 
    by (metis (no_types, opaque_lifting) "4" Rep_nat_int_inverse antisym assm bot.extremum
        nat_int.consec_def nat_int.consec_un_max nat_int.consec_un_min_max nat_int.un_subset2)
  from 5 and 6 show " (i  j)  k = i  (j  k)" by simp
qed

lemma consec_assoc1:"consec j k  consec i (j  k)  consec (i  j) k "
proof
  assume assm:"consec j k  consec i (j  k)"
  hence min_max_yz:"maximum j +1=minimum k" using consec_def by blast 
  hence min_max_xyz:"maximum i +1 = minimum (j  k)" 
      using consec_def assm by blast
  have min_y_yz:"minimum j = minimum (j  k)" 
    by (simp add: assm nat_int.consec_un_min) 
  hence min_max_xy:"maximum i+1 = minimum j" using min_max_xyz by simp
  hence consec_x_y:"consec i j" using assm _consec_def by auto
  hence max_y_xy:"maximum j = maximum (i  j)" using consec_lesser assm 
    by (simp add: nat_int.consec_un_max)
  have none_empty:"i    j    k  " using assm by (simp add: consec_def)
  hence un_non_empty:"ij  " 
    using bot.extremum_uniqueI consec_x_y nat_int.un_subset2 by force
  have max:"maximum (ij) +1 = minimum k" 
    using min_max_yz max_y_xy by auto  
  thus "consec (i  j) k"  using max un_non_empty none_empty consec_def by blast
qed
  
lemma consec_assoc2:"consec i j  consec (i j) k  consec i  (j k) "
proof
  assume assm:"consec i j  consec (i j) k"
  hence consec_y_z:"consec j k" using assm consec_def consec_intermediate2 
    by blast
  hence max_y_xy:"maximum j = maximum (i  j)" 
    by (simp add: assm nat_int.consec_un_max)  
  have min_y_yz:"minimum j = minimum (j  k)" 
    by (simp add: consec_y_z nat_int.consec_un_min)
  have none_empty:"i    j    k  " using assm by (simp add: consec_def)
  then have un_non_empty:"jk  " 
    by (metis  bot_nat_int.rep_eq Rep_nat_int_inject consec_y_z  less_eq_nat_int.rep_eq
        un_subset1 subset_empty)
  have max:"maximum (i) +1 = minimum (j k)" 
    using assm min_y_yz consec_def by auto
  thus "consec i ( j  k)"  using max un_non_empty none_empty consec_def by blast
qed
  
  
lemma consec_assoc_mult:
  "(i2= consec i1 i2 )  (i3 =  consec i3 i4)  (consec (i1  i2) (i3  i4)) 
       (i1  i2)  (i3  i4) = (i1  (i2  i3))  i4"
proof
  assume assm:"(i2= consec i1 i2 )  (i3 =  consec i3 i4) 
                 (consec (i1  i2) (i3  i4))"
  hence "(i2= consec i1 i2 )" by simp
  thus " (i1  i2)  (i3  i4) = (i1  (i2  i3))  i4" 
  proof
    assume empty2:"i2 = "
    hence only_l1:"(i1  i2) = i1" using un_empty_absorb1 by simp
    from assm have "(i3 =  consec i3 i4)" by simp
    thus " (i1  i2)  (i3  i4) = (i1  (i2  i3))  i4" 
      by (metis Rep_nat_int_inverse assm bot_nat_int.rep_eq empty2 local.union_def 
          nat_int.consec_intermediate1 nat_int.un_assoc only_l1 sup_bot.left_neutral)
  next
    assume consec12:" consec i1 i2"
    from assm have "(i3 =  consec i3 i4)" by simp
    thus " (i1  i2)  (i3  i4) = (i1  (i2  i3))  i4" 
    proof
      assume empty3:"i3 = "
      hence only_l4:"(i3  i4) = i4 " using un_empty_absorb2 by simp
      have "(i1  (i2  i3)) = i1  i2" using empty3 by (simp add: un_empty_absorb1)
      thus ?thesis by (simp add: only_l4)
    next
      assume  consec34:" consec i3 i4"
      have consec12_3:"consec (i1  i2) i3" 
        using assm consec34 consec_intermediate1 by blast
      show ?thesis 
        by (metis consec12 consec12_3 consec34 consec_intermediate2 un_assoc)
    qed
  qed
qed
  
lemma card_subset_le: "i  i'  |i|  |i'|"  
  by (metis bot_nat_int.rep_eq card_mono finite.intros(1) finite_atLeastAtMost 
      less_eq_nat_int.rep_eq local.card'.rep_eq rep_non_empty_means_seq)
  
lemma card_subset_less:"(i::nat_int) < i'  |i|<|i'|"  
  by (metis bot_nat_int.rep_eq finite.intros(1) finite_atLeastAtMost less_nat_int.rep_eq
      local.card'.rep_eq psubset_card_mono rep_non_empty_means_seq) 
  
lemma card_empty_zero:"|| = 0"  
  using Abs_nat_int_inverse empty_type card'.rep_eq bot_nat_int.rep_eq by auto
    
lemma card_non_empty_geq_one:"i    |i|  1" 
proof
  assume "i  "
  hence "Rep_nat_int i  {}" by (metis Rep_nat_int_inverse bot_nat_int.rep_eq)
  hence "card (Rep_nat_int i) > 0" 
    by (metis i   card_0_eq finite_atLeastAtMost gr0I rep_non_empty_means_seq)
  thus "|i|  1" by (simp add: card'_def) 
next
  assume "|i|  1" thus "i " 
    using card_empty_zero by auto
qed

lemma card_min_max:"i    |i| = (maximum i - minimum i) + 1" 
proof
  assume assm:"i  "
  then have "Rep_nat_int i = {minimum i .. maximum i}" 
    by (metis leq_max_sup leq_min_inf nat_int.maximum_def nat_int.minimum_def
        rep_non_empty_means_seq) 
  then have "card (Rep_nat_int i) = maximum i - minimum i + 1" 
    using Rep_nat_int_inject assm bot_nat_int.rep_eq by fastforce
  then show " |i| = (maximum i - minimum i) + 1"  by simp
qed

lemma card_un_add: " consec i j  |i  j| = |i| + |j|"
proof 
  assume assm:"consec i j" 
  then have 0:"i  j = " 
    using nat_int.consec_inter_empty by auto
  then have "(Rep_nat_int i)  (Rep_nat_int j) = {}" 
    by (metis bot_nat_int.rep_eq inf_nat_int.rep_eq)
  then have 1: 
    "card((Rep_nat_int i)(Rep_nat_int j))=card(Rep_nat_int i)+card(Rep_nat_int j)"
    by (metis Int_iff add.commute add.left_neutral assm card.infinite card_Un_disjoint
        emptyE le_add1 le_antisym local.consec_def nat_int.card'.rep_eq
        nat_int.card_min_max nat_int.el.rep_eq nat_int.maximum_in nat_int.minimum_in)
  then show "|i  j| = |i| + |j|" 
  proof -
    have f1: "i    j    maximum i + 1 = minimum j"
      using assm nat_int.consec_def by blast
    then have f2: "Rep_nat_int i  {}"
      using Rep_nat_int_inject bot_nat_int.rep_eq by auto
    have "Rep_nat_int j  {}"
      using f1 Rep_nat_int_inject bot_nat_int.rep_eq by auto
    then show ?thesis
      using f2 f1 Abs_nat_int_inverse Rep_nat_int 1 local.union_result
        nat_int.union_def nat_int_class.maximum_def nat_int_class.minimum_def
        by force
  qed
qed

lemma singleton:"|i| = 1  (n. Rep_nat_int i = {n})"
  using card_1_singletonE card'.rep_eq by fastforce
    
lemma singleton2:" (n. Rep_nat_int i = {n})  |i| = 1"
  using card_1_singletonE card'.rep_eq by fastforce
    
    
lemma card_seq:"
  i .|i| = x  (Rep_nat_int i = {}  (n. Rep_nat_int i = {n..n+(x-1)}))" 
proof (induct x)
  show IB:
    "i. |i| = 0  (Rep_nat_int i = {}  (n. Rep_nat_int i = {n..n+(0-1)}))" 
    by (metis  card_non_empty_geq_one bot_nat_int.rep_eq  not_one_le_zero)
  fix x
  assume IH:
      "i. |i| = x  Rep_nat_int i = {}  (n. Rep_nat_int i = {n..n+(x-1)})"
  show   " i. |i| = Suc x 
             Rep_nat_int i = {}  (n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
  proof (rule allI|rule impI)+
    fix i
    assume assm_IS:"|i| = Suc x"
    show " Rep_nat_int i = {}  (n. Rep_nat_int i = {n.. n + (Suc x -1)})"
    proof (cases "x = 0")
      assume "x=0"
      hence "|i| = 1" 
        using assm_IS by auto 
      then have "n'. Rep_nat_int i = {n'}" 
        using nat_int.singleton by blast 
      hence "n'. Rep_nat_int i = {n'.. n' + (Suc x) -1}"
        by (simp add: x = 0)
      thus "Rep_nat_int i = {}  (n. Rep_nat_int i = {n.. n + (Suc x - 1)})"
        by simp
    next
      assume x_neq_0:"x 0 "
      hence x_ge_0:"x > 0" using gr0I by blast
      from assm_IS have i_is_seq:"n m. n  m  Rep_nat_int i = {n..m}" 
        by (metis One_nat_def Suc_le_mono card_non_empty_geq_one le0 rep_non_empty_means_seq)
      obtain n and m where seq_def:" n   m  Rep_nat_int i = {n..m}" 
        using i_is_seq by auto
      have n_le_m:"n < m"
      proof (rule ccontr)
        assume "¬n < m"
        hence "n = m" by (simp add: less_le seq_def)
        hence "Rep_nat_int i = {n}" by (simp add: seq_def)
        hence "x = 0" using assm_IS card'.rep_eq by auto
        thus False by (simp add: x_neq_0)
      qed
      hence "n  (m-1)" by simp
      obtain i' where  i_def:"i' = Abs_nat_int {n..m-1}" by blast
      then have card_i':"|i'| = x" 
        using assm_IS leq_nat_non_empty n_le_m
          nat_int_class.card_min_max nat_int_class.leq_max_sup' nat_int_class.leq_min_inf'
          seq_def by auto
      hence "Rep_nat_int i' = {}  (n. Rep_nat_int i' = {n.. n + (x - 1)})" 
        using IH by auto
      hence " (n. Rep_nat_int i' = {n.. n + (x - 1)})" using x_neq_0 
        using card.empty card_i' card'.rep_eq by auto
      hence "m-1 = n + x -1" using assm_IS card'.rep_eq seq_def by auto
      hence "m = n +x" using n_le_m x_ge_0 by linarith
      hence "( Rep_nat_int i = {n.. n + (Suc x -1) })" using seq_def by (simp )
      hence "n. (Rep_nat_int i = {n.. n + (Suc x -1) })" ..
      then show "Rep_nat_int i = {}  (n. Rep_nat_int i ={n.. n + (Suc x-1)})"
        by blast
    qed
  qed
qed
    
lemma rep_single: "Rep_nat_int (Abs_nat_int {m..m}) = {m}"
  by (simp add: Abs_nat_int_inverse)

lemma chop_empty_right: "i. N_Chop(i,i,)"  
  using bot_nat_int.abs_eq nat_int.inter_empty1 nat_int.nchop_def nat_int.un_empty_absorb1
  by auto
    
lemma chop_empty_left: "i. N_Chop(i, , i)"
  using bot_nat_int.abs_eq nat_int.inter_empty2 nat_int.nchop_def nat_int.un_empty_absorb2
  by auto
    
lemma chop_empty : "N_Chop(,,)"
  by (simp add: chop_empty_left)
    
lemma chop_always_possible:"i. j k. N_Chop(i,j,k)" 
  by (metis  chop_empty_right)
    
lemma chop_add1: "N_Chop(i,j,k)  |i| = |j| + |k|"
  using card_empty_zero card_un_add un_empty_absorb1 un_empty_absorb2 nchop_def by auto
    
lemma chop_add2:"|i| = x+y  ( j k. N_Chop(i,j,k)  |j|=x  |k|=y)" 
proof
  assume assm:"|i| = x+y"
  show "( j k. N_Chop(i,j,k)  |j|=x  |k|=y)"
  proof (cases "x+y = 0")
    assume "x+y =0"
    then show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" 
      using assm chop_empty_left nat_int.chop_add1 by fastforce
  next 
    assume "x+y  0"
    show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" 
    proof (cases "x = 0")
      assume x_eq_0:"x=0"
      then show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" 
        using assm nat_int.card_empty_zero nat_int.chop_empty_left by auto
    next
      assume x_neq_0:"x 0"
      show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" 
      proof (cases "y = 0")
        assume y_eq_0:"y=0"
        then show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" 
          using assm nat_int.card_empty_zero nat_int.chop_empty_right by auto
      next
        assume y_neq_0:"y  0"
        have rep_i:"n. Rep_nat_int i = {n..n + (x+y)-1}" 
          using assm card'.rep_eq card_seq x_neq_0 by fastforce
        obtain n where n_def:"Rep_nat_int i = {n..n + (x+y) -1}" 
          using rep_i by auto
        have n_le:"n  n+(x-1)" by simp
        have x_le:"n+(x)  n + (x+y)-1" using y_neq_0 by linarith
        obtain j  where j_def:" j = Abs_nat_int {n..n+(x-1)}" by blast
        from n_le have j_in_type:
          "{n..n+(x-1)}  {S . ( (m::nat) n . m  n  {m..n }=S)  S={}}"
          by blast
        obtain k where k_def:" k =Abs_nat_int {n+x..n+(x+y)-1}" by blast
        from x_le have k_in_type:
          "{n+x..n+(x+y)-1}  {S.( (m::nat) n . m  n  {m..n }=S)  S={}}"
          by blast
        have consec: "consec j k" 
          by (metis j_def k_def One_nat_def Suc_leI add.assoc diff_add n_le consec_def
              leq_max_sup' leq_min_inf' leq_nat_non_empty neq0_conv x_le x_neq_0)
        have union:"i = j  k" 
          by (metis Rep_nat_int_inverse consec j_def k_def n_def n_le nat_int.consec_un_min_max
              nat_int.leq_max_sup' nat_int.leq_min_inf' x_le)
        have disj:"j  k = " using consec by (simp add: consec_inter_empty)
        have chop:"N_Chop(i,j,k)" using consec union disj nchop_def by simp
        have card_j:"|j| = x" 
          using Abs_nat_int_inverse j_def n_le card'.rep_eq x_neq_0 by auto
        have card_k:"|k| = y"
          using Abs_nat_int_inverse k_def x_le card'.rep_eq x_neq_0 y_neq_0 by auto
        have "N_Chop(i,j,k)  |j| = x  |k| = y" using chop card_j card_k by blast
        then show " j k. N_Chop(i,j,k)  |j|=x  |k|=y" by blast
      qed
    qed
  qed
qed
  
lemma chop_single:"(N_Chop(i,j,k)  |i| = 1)  ( |j| =0  |k|=0)"
  using chop_add1 by force
    
lemma chop_leq_max:"N_Chop(i,j,k)  consec j k  
  (n . n  Rep_nat_int i  n  maximum j  n  Rep_nat_int j)" 
  by (metis Un_iff le_antisym less_imp_le_nat nat_int.consec_def nat_int.consec_lesser
      nat_int.consec_un nat_int.el.rep_eq nat_int.maximum_in nat_int.nchop_def
      nat_int.not_in.rep_eq)
    
lemma chop_geq_min:"N_Chop(i,j,k)  consec j k  
  (n . n  Rep_nat_int i  minimum k  n  n  Rep_nat_int k)" 
  by (metis atLeastAtMost_iff bot_nat_int.rep_eq equals0D leq_max_sup leq_min_inf 
      nat_int.consec_def nat_int.consec_un_max nat_int.maximum_def nat_int.minimum_def
      nat_int.nchop_def rep_non_empty_means_seq)
     
lemma chop_min:"N_Chop(i,j,k)  consec j k  minimum i = minimum j" 
  using nat_int.consec_un_min nat_int.nchop_def by auto
  
lemma chop_max:"N_Chop(i,j,k)  consec j k  maximum i = maximum k"
  using nat_int.consec_un_max nat_int.nchop_def by auto
  
lemma chop_assoc1:
  "N_Chop(i,i1,i2)  N_Chop(i2,i3,i4) 
     (N_Chop(i, i1  i3, i4)  N_Chop(i1  i3, i1, i3))" 
proof 
  assume assm:"N_Chop(i,i1,i2)  N_Chop(i2,i3,i4)"
  then have chop_def:"(i =  i1  i2   
        (i1 =    i2 =   ( consec i1 i2)))"
    using nchop_def by blast
  hence "(i1 =    i2 =   ( consec i1 i2))" by simp 
  then show "N_Chop(i, i1  i3, i4)  N_Chop(i1  i3, i1, i3)" 
  proof 
    assume empty:"i1 = "
    then show "N_Chop(i,i1  i3, i4)  N_Chop(i1  i3, i1, i3)" 
      by (simp add: assm chop_def nat_int.chop_empty_left nat_int.un_empty_absorb2)
  next
    assume "i2 =   ( consec i1 i2)"
    then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
    proof 
      assume empty:"i2 = "
      then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
        by (metis assm bot.extremum_uniqueI nat_int.chop_empty_right nat_int.nchop_def
            nat_int.un_empty_absorb2 nat_int.un_subset1)
    next
      assume " consec i1 i2"
      then have consec_i1_i2:"i1   i2   maximum i1 +1 = minimum i2" 
        using consec_def by blast
      from assm have "i3 =   i4 =   consec i3 i4" 
        using nchop_def by blast
      then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
      proof
        assume i3_empty:"i3 = "
        then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
          using assm nat_int.chop_empty_right nat_int.nchop_def nat_int.un_empty_absorb2
            by auto
      next 
        assume "i4 =   consec i3 i4"
        then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
        proof
          assume i4_empty:"i4 = "
          then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
            using assm nat_int.chop_empty_right nat_int.nchop_def by auto
        next
          assume consec_i3_i4:"consec i3 i4"
          then show "N_Chop(i, i1  i3, i4) N_Chop(i1  i3, i1, i3)" 
            by (metis consec i1 i2 assm nat_int.consec_assoc1 nat_int.consec_intermediate1
                nat_int.nchop_def nat_int.un_assoc)
        qed
      qed
    qed
  qed
qed
  
lemma chop_assoc2:
  "N_Chop(i,i1,i2)  N_Chop(i1,i3,i4) 
     N_Chop(i, i3, i4  i2)  N_Chop(i4  i2, i4,i2)" 
proof 
  assume assm: "N_Chop(i,i1,i2)  N_Chop(i1,i3,i4)"
  hence "(i1 =    i2 =   ( consec i1 i2))" 
    using nchop_def by blast 
  then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)"
  proof
    assume i1_empty:"i1 = "
   then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
     by (metis assm nat_int.chop_empty_left nat_int.consec_un_not_elem1 nat_int.in_not_in_iff1
         nat_int.nchop_def nat_int.non_empty_elem_in nat_int.un_empty_absorb1)
  next
    assume "i2 =   consec i1 i2"
    then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)"
    proof
      assume i2_empty:"i2="
      then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
        using assm nat_int.chop_empty_right nat_int.nchop_def by auto
    next
      assume consec_i1_i2:"consec i1 i2"
      from assm have "(i3 =    i4 =   ( consec i3 i4))" 
        by (simp add: nchop_def)
      then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)"
      proof
        assume i3_empty:"i3="
        then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
          using assm nat_int.chop_empty_left nat_int.nchop_def by auto
      next
        assume " i4 =   ( consec i3 i4)"
        then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
        proof
          assume i4_empty:"i4="
          then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
            using assm nat_int.nchop_def nat_int.un_empty_absorb1 nat_int.un_empty_absorb2
            by auto
        next
          assume consec_i3_i4:"consec i3 i4"
          then show "N_Chop(i, i3, i4  i2) N_Chop(i4  i2, i4,i2)" 
            by (metis assm consec_i1_i2 nat_int.consec_assoc2 nat_int.consec_intermediate2
                nat_int.nchop_def nat_int.un_assoc)
        qed
      qed
    qed
  qed
qed
  
lemma chop_subset1:"N_Chop(i,j,k)  j  i"
  using nat_int.chop_empty_right nat_int.nchop_def nat_int.un_subset1 by auto
    
lemma chop_subset2:"N_Chop(i,j,k)  k  i" 
  using nat_int.chop_empty_left nat_int.nchop_def nat_int.un_subset2 by auto
    
end
end