Theory nest

(*
Title:  Allen's qualitative temporal calculus
Author:  Fadoua Ghourabi (fadouaghourabi@gmail.com)
Affiliation: Ochanomizu University, Japan
*)


theory nest

imports 
    Main  jointly_exhaustive examples
    "HOL-Eisbach.Eisbach_Tools"

begin

section ‹Nests›
text‹Nests are sets of intervals that share a meeting point. We define relation before between nests that give the ordering properties of points.›

subsection ‹Definitions›

type_synonym 'a nest = "'a set"

definition (in arelations) BEGIN :: "'a ⇒ 'a nest" 
where "BEGIN i  = {j | j. (j,i) ∈ ov ∪ s ∪ m ∪ f^-1 ∪ d^-1 ∪ e ∪ s^-1}"

definition (in arelations) END :: "'a ⇒ 'a nest" 
where "END i  = {j | j. (j,i) ∈ e ∪ ov^-1 ∪ s^-1 ∪ d^-1 ∪ f ∪ f^-1 ∪ m^-1}"

definition (in arelations) NEST ::"'a nest ⇒ bool"
where "NEST S ≡ ∃i. ℐ i ∧ (S = BEGIN i ∨ S = END i)"

definition (in arelations) before :: "'a nest ⇒ 'a nest ⇒ bool" (infix "≪" 100)
where "before N M ≡ NEST N ∧ NEST M ∧ (∃n m. ⌦‹ℐ m ∧ ℐ n ∧› n ∈ N ∧ m ∈ M ∧ (n,m) ∈ b)"

subsection ‹Properties of Nests›

lemma intv1:
assumes "ℐ i" 
shows "i ∈ BEGIN i"
unfolding BEGIN_def
by (simp add:e assms)

lemma intv2:
assumes "ℐ i" 
shows "i ∈ END i"
unfolding END_def
by (simp add: e assms)

lemma NEST_nonempty:
assumes "NEST S"
shows "S ≠ {}" 
using assms unfolding NEST_def 
by (insert intv1 intv2, auto)

lemma NEST_BEGIN:
assumes "ℐ i" 
shows "NEST (BEGIN i)"
using NEST_def assms by auto

lemma NEST_END:
assumes "ℐ i" 
shows "NEST (END i)"
using NEST_def assms by auto

lemma before:
assumes a:"ℐ i" 
shows "BEGIN i ≪ END i" 
proof -
  
    obtain p where pi:"(p,i) ∈ m"
    using  a M3 m by blast
    then have p:"p ∈ BEGIN i" using BEGIN_def by auto

    obtain q where qi:"(q,i) ∈ m^-1" 
    using a M3 m by blast
    then have q:"q ∈ END i" using END_def by auto

    from pi qi have c1:"(p,q) ∈ b" using b  m
    by blast 

    with  c1 p q assms show ?thesis  by (auto simp:NEST_def  before_def)

qed

lemma  meets:
fixes i j
 assumes "ℐ i" and "ℐ j" 
shows "(i,j) ∈ m = ((END i) = (BEGIN j))" 
proof 
  assume ij:"(i,j) ∈ m" then have ibj:"i ∈ (BEGIN j)" unfolding BEGIN_def by auto
  from ij have ji:"(j,i) ∈ m^-1" by simp
  then have jeo:"j ∈ (END i)" unfolding END_def by simp
  show "((END i) = (BEGIN j))"
  proof 
      {fix x::"'a" assume a:"x ∈ (END i)"
      then have asimp:"(x,i) ∈ e ∪  ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ m¯ ∪ f^-1"
      unfolding END_def by auto
      then have "x ∈ (BEGIN j)" using ij eovisidifmifiOm
      by (auto simp:BEGIN_def)     
      }
      thus conc1:"END i ⊆ BEGIN j" by auto
   next
     {fix x assume b:"x ∈ (BEGIN j)"
     then have bsimp:"(x,j) ∈ ov ∪ s∪ m  ∪ f^-1 ∪ d^-1 ∪ e ∪ s^-1"
     unfolding BEGIN_def by auto
     then have "x ∈ (END i)" using ij ovsmfidiesiOmi
     by (auto simp:END_def)
     }thus conc2:"BEGIN j ⊆ END i" by auto
  qed
next
  assume a0:"END (i::'a) = BEGIN (j::'a)" show "(i,j) ∈ m"
  proof (rule ccontr)
     assume a:"(i,j) ∉ m" then have "¬i∥j" using m by auto
     from a have "(i,j) ∈ b  ∪ ov  ∪ s ∪ d ∪ f^-1 ∪ e ∪ f  ∪ s^-1  ∪ d^-1 ∪ ov^-1 ∪ m^-1  ∪ b^-1" using assms JE by auto
     thus False
     proof (auto)
       {assume ij:"(i,j) ∈ e" 
        obtain p where ip:"i∥p" using M3 assms(1)  by auto
        then  have pi:"(p,i)∈ m^-1" using m by auto
        then have "p ∈ END i" using END_def by auto
        with a0 have pj:"p ∈ (BEGIN j) " by auto
        from ij pi have "(p,j) ∈ m^-1"  by (simp add: e)
        with pj show   ?thesis
        apply (auto simp:BEGIN_def)
        using m_rules by auto[7] }
       next
       {assume ij: "(j,i) ∈ m" 
        obtain p where ip:"i∥p" using M3  assms(1) by auto
        then  have pi:"(p,i)∈ m^-1" using m by auto
        then have "p ∈ END i" using END_def by auto
        with a0 have pj:"p ∈ (BEGIN j) " by auto
        from ij have "(i,j) ∈ m^-1" by simp
        with  pi have "(p,j) ∈ b^-1" using cmimi  by auto
        with pj show   ?thesis
        apply (auto simp:BEGIN_def)
          using b_rules by auto
        }

       next 

       {assume ij:"(i,j)∈ b"
        have ii:"(i,i)∈e" and "i ∈ END i" using assms  intv2 e by auto
        with a0 have j:"i ∈ BEGIN j" by simp
        with ij  show   ?thesis 
        apply (auto simp:BEGIN_def)
          using b_rules by auto
         }
       
        next 

        { assume ji:"(j,i) ∈ b" then have ij:"(i,j) ∈ b^-1" by simp
          have ii:"(i,i)∈e" and "i ∈ END i" using assms intv2 e by auto
          with a0 have j:"i ∈ BEGIN j" by simp
          with ij  show   ?thesis 
          apply (auto simp:BEGIN_def)
            using b_rules by auto}
        
        next

        {assume ij:"(i,j)∈ov"
         then obtain u v::"'a" where iu:"i∥u" and uv:"u∥v" and uv:"u∥v" using ov by blast
         from iu have "u ∈ END i" using m END_def by auto
         with a0 have u:"u ∈ BEGIN j" by simp
         from iu have "(u,i) ∈ m^-1" using m by auto
         with ij have uj:"(u,j) ∈ ov^-1 ∪ d ∪ f" using covim by auto
         show ?thesis using u uj 
         apply (auto simp:BEGIN_def)
           using ov_rules eovi apply auto[9]
            using s_rules apply auto[2]
              using d_rules apply auto[5]
                using f_rules by auto[5]
        }

        next 
        
        {assume "(j,i) ∈ ov" then have  ij:"(i,j)∈ov^-1" by simp let ?p = i 
        from ij have pi:"(?p, i) ∈ e" by (simp add:e)
        from ij have pj:"(?p,j) ∈ ov^-1" by simp
        from pi have "?p ∈ END i" using END_def by auto
        with a0 have "?p ∈ (BEGIN j) " by auto
        with pj show ?thesis 
        apply (auto simp:BEGIN_def)
          using ov_rules by auto
        }
        next
        {assume ij:"(i,j) ∈ s" 
         then obtain p q t where ip:"i∥p" and pq:"p∥q" and  jq:"j∥q" and ti:"t∥i" and tj:"t∥j" using s by blast
         from ip have "(p,i) ∈ m^-1" using m by auto
         then have "p ∈ END i" using END_def by auto
         with a0 have p:"p ∈ BEGIN j" by simp
         from ti ip pq tj jq have "(p,j) ∈ f" using f by blast
         with p show ?thesis 
         apply (auto simp:BEGIN_def)
           using f_rules by auto
            
         }
         next
         {assume "(j,i) ∈ s" then have  ij:"(i,j) ∈ s^-1" by simp
          then obtain u v where ju:"j∥u" and uv:"u∥v" and iv:"i∥v" using s by blast
          from iv have "(v,i) ∈ m^-1" using m by blast
          then have "v ∈ END i" using END_def by auto
          with a0 have v:"v ∈ BEGIN j" by simp
          from ju uv have "(v,j) ∈ b^-1" using b by auto
          with v show ?thesis 
          apply (auto simp:BEGIN_def)
            using b_rules by auto}
         next
         {assume ij:"(i,j) ∈ f"
          have "(i,i) ∈ e" and "i ∈ END i" 
          by (simp add: e)  (auto simp: assms intv2 )
          with a0 have "i ∈ BEGIN j" by simp
          with ij show ?thesis 
          apply (auto simp:BEGIN_def)
           using f_rules by auto 
         }
         next
         {assume "(j,i) ∈ f" then have "(i,j)∈f^-1" by simp
          then obtain u where ju:"j∥u" and iu:"i∥u" using f by auto
          then have ui:"(u,i) ∈ m^-1" and "u ∈ END i"  
          apply (simp add: converse.intros m)
          using END_def iu m by auto
          with a0 have ubj:"u ∈ BEGIN j" by simp
          from ju have "(u,j) ∈ m^-1"  by (simp add: converse.intros m)
          with ubj show  ?thesis 
          apply (auto simp:BEGIN_def)
            using m_rules by auto
         }
         next
         {assume ij:"(i,j) ∈ d" then 
          have "(i,i) ∈ e" and "i ∈ END i" using assms e by (blast, simp add:  intv2)
          with a0 have "i ∈ BEGIN j" by simp
          with ij show ?thesis 
          apply (auto simp:BEGIN_def)
            using d_rules by auto}
          next
          {assume ji:"(j,i) ∈ d" then have "(i,j) ∈ d^-1" using d by simp
           then obtain u v where ju:"j∥u" and uv:"u∥v" and iv:"i∥v" using d using ji by blast
           then have "(v,i) ∈ m^-1" and "v ∈ END i" using m END_def by auto
           with a0 ju uv have  vj:"(v,j) ∈ b^-1" and  "v ∈ BEGIN j" using b by auto
           with vj show ?thesis 
           apply (auto simp:BEGIN_def)
             using b_rules by auto}
          
        qed
    qed
qed


lemma starts:
fixes i j
assumes "ℐ i" and "ℐ j" 
shows "((i,j) ∈ s ∪ s^-1 ∪ e) = (BEGIN i = BEGIN j)"
proof 
   assume a3:"(i,j) ∈ s ∪ s^-1 ∪ e" show "BEGIN i = BEGIN j"
   proof -
    { fix x assume "x ∈ BEGIN i" then have "(x,i) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
    hence "x ∈ BEGIN j" using a3 ovsmfidiesiOssie
    by (auto simp:BEGIN_def)
    } note c1 = this

    { fix x assume "x ∈ BEGIN j" then have xj:"(x,j) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
    then have "x ∈ BEGIN i" 
    apply (insert converseI[OF a3] xj)
    apply (subst (asm) converse_Un)+
    apply (subst (asm) converse_converse)
    using ovsmfidiesiOssie  
    by (auto simp:BEGIN_def)
    } note c2 = this

    from c1 have "BEGIN i ⊆ BEGIN j" by auto
    moreover with c2 have "BEGIN j ⊆ BEGIN i" by auto
    ultimately show ?thesis by auto  
 qed
next
   assume a4:"BEGIN i = BEGIN j"
   with assms have "i ∈ BEGIN j" and "j ∈ BEGIN i" using intv1 by auto
   then have ij:"(i,j) ∈ ov ∪ s ∪ m ∪ f^-1 ∪ d^-1 ∪ e ∪ s^-1" and ji:"(j,i) ∈  ov ∪ s ∪ m ∪ f^-1 ∪ d^-1 ∪ e ∪ s^-1"
   unfolding BEGIN_def by auto
   then have ijov:"(i,j) ∉ ov"  
    apply auto
    using ov_rules  by auto
   
   from ij ji have ijm:"(i,j) ∉ m"  
   apply (simp_all, elim disjE, simp_all)
    using ov_rules apply auto[13]
      using s_rules apply auto[11]
        using m_rules apply auto[9]
          using f_rules apply auto[7]
            using d_rules apply auto[5]
              using m_rules by auto[4]

   from ij ji have  ijfi:"(i,j) ∉ f^-1"  
   apply (simp_all, elim disjE, simp_all)
    using ov_rules apply auto[13]
     using s_rules apply auto[11]
      using m_rules apply auto[9]
          using f_rules apply auto[7]
            using d_rules apply auto[5]
              using f_rules by auto[4]

   from ij ji have  ijdi:"(i,j) ∉ d^-1"  
   apply (simp_all, elim disjE, simp_all)
    using ov_rules apply auto[13]
     using s_rules apply auto[11]
      using m_rules apply auto[9]
          using f_rules apply auto[7]
            using d_rules apply auto[5]
              using d_rules by auto[4]

   from ij ijm ijov ijfi ijdi show "(i, j) ∈ s ∪ s¯ ∪ e" by auto 

qed

lemma xj_set:"x ∈ {a |a. (a, j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯} = ((x,j) ∈  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯)"
by blast

lemma ends:
fixes i j
assumes "ℐ i" and "ℐ j"
shows "((i,j) ∈ f ∪ f^-1 ∪ e) = (END i = END j)"
proof 
   assume a3:"(i,j) ∈ f ∪ f^-1 ∪ e" show "END i = END j"
   proof -
    { fix x assume "x ∈ END i" then have "(x,i) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
      then have "x ∈ END j" using a3 unfolding END_def 
      apply (subst xj_set)
      using ceovisidiffimi_ffie_simp by simp
     } note c1 =this

    { fix x assume "x ∈ END j" then have "(x,j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
      then have "x ∈ END i" using a3 unfolding END_def  
      by (metis Un_iff ceovisidiffimi_ffie_simp converse_iff eei mem_Collect_eq)  
     }  note c2 = this

    from c1 have "END i ⊆ END j" by auto
    moreover with c2 have "END j ⊆ END i" by auto
    ultimately show ?thesis by auto  
  qed (*} note conc = this *)
  next
  assume a4:"END i = END j"
  with assms have "i ∈ END j" and "j ∈ END i" using intv2 by auto
  then have ij:"(i,j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" and ji:"(j,i) ∈  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯"
  unfolding END_def by auto
  then  have ijov:"(i,j) ∉ ov^-1"  
  apply (simp_all, elim disjE, simp_all)
   using eov es ed efi ef em eov  apply auto[13] 
    using ov_rules apply auto[11]
     using s_rules apply auto[9]
      using d_rules apply auto[7]
        using f_rules apply auto[8]
          using movi by auto
   
  from ij ji have  ijm:"(i,j) ∉ m^-1"  
  apply (simp_all, elim disjE, simp_all)
    using m_rules by auto

  from ij ji have  ijfi:"(i,j) ∉ s^-1"  
  apply (simp_all, elim disjE, simp_all)
    using s_rules by auto

  from ij ji have  ijdi:"(i,j) ∉ d^-1"  
  apply (simp_all, elim disjE, simp_all)
    using d_rules by auto

  from ij ijm ijov ijfi ijdi  show "(i, j) ∈ f ∪ f¯ ∪ e"  by auto
qed

lemma before_irrefl:
fixes a
shows "¬ a ≪ a" 
proof (rule ccontr, auto)
  assume a0:"a ≪ a"
  then have "NEST a"  unfolding before_def by auto
  then obtain i where   i:"a = BEGIN i ∨ a = END i" unfolding NEST_def by auto
  from i show False
  proof
      assume "a = BEGIN i"
      with a0 have "BEGIN i ≪ BEGIN i" by simp
      then obtain p q where "p∈ BEGIN i" and "q ∈ BEGIN i" and b:"(p,q) ∈ b" unfolding before_def by auto
      then  have a1:"(p,i) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" and a2:"(i,q) ∈ ov^-1 ∪ s^-1 ∪ m^-1 ∪ f ∪ d ∪ e ∪ s" unfolding BEGIN_def  
      apply auto 
      using eei apply fastforce
      by (simp add: e)+
      with b show False 
      using piiq[of p i q] 
        using  b_rules by safe fast+
      next
      assume "a = END i"
      with a0 have "END i ≪ END i" by simp
      then obtain p q where "p∈ END i" and "q ∈ END i" and b:"(p,q) ∈ b" unfolding before_def by auto
      then  have a1:"(p,i) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" and a2:"(q,i) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def  
      by auto 
      with b show False
      apply (subst (asm) converse_iff[THEN sym])
      using cbi_alpha1ialpha4mi neq_bi_alpha1ialpha4mi relcomp.relcompI subsetCE by blast        
     qed
qed

lemma BEGIN_before:
fixes i j
assumes "ℐ i" and "ℐ j" 
shows "BEGIN i ≪ BEGIN j = ((i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯)"
proof 
    
     assume a3:"BEGIN i ≪ BEGIN j"
     from a3 obtain p q where pa:"p ∈ BEGIN i" and qc:"q ∈ BEGIN j" and pq:"(p,q) ∈ b" unfolding before_def by auto
     then obtain r where "p∥r" and "r∥q" using b by auto
     then have pr:"(p,r) ∈ m" and rq:"(r,q) ∈ m" using m by auto
     from pa  have pi:"(p,i) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
     moreover with pr have "(r,p) ∈ m^-1" by simp
     ultimately have "(r,i) ∈ d ∪ f ∪ ov^-1 ∪ e ∪ f^-1 ∪ m^-1 ∪ b^-1 ∪ s ∪ s^-1"
     using cmiov cmis cmim cmifi cmidi  cmisi
     apply ( simp_all,elim disjE, auto)
        by (simp add: e)
     

     then have ir:"(i,r) ∈ d^-1 ∪ f^-1 ∪ ov ∪ e ∪ f ∪ m ∪ b ∪ s^-1 ∪ s" 
     by (metis (mono_tags, lifting) converseD converse_Un converse_converse eei)

     from qc  have "(q,j) ∈  ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
     with rq have rj:"(r,j) ∈ b ∪ s ∪ m "
     using m_ovsmfidiesi using contra_subsetD relcomp.relcompI by blast
      
     with ir have c1:"(i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯ ∪ d ∪ e ∪ s ∪ s¯"
     using difibs by blast
     {assume "(i,j) ∈ s∨ (i,j)∈s^-1 ∨ (i,j) ∈ e" then have "BEGIN i = BEGIN j" 
      using starts Un_iff assms(1) assms(2) by blast
      with a3 have False  by (simp add: before_irrefl)}

      from c1 have c1':"(i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯ ∪ d " 
      using ‹(i, j) ∈ s ∨ (i, j) ∈ s¯ ∨ (i, j) ∈ e ⟹ False› by blast

     {assume "(i,j) ∈ d" with pi have "(p,j) ∈ e ∪  s ∪ d ∪ ov ∪ ov^-1 ∪ s^-1 ∪ f ∪ f^-1  ∪ d^-1"
      using ovsmfidiesi_d using relcomp.relcompI subsetCE by blast
      with pq have "(q,j) ∈  b^-1 ∪ d ∪ f ∪ ov^-1 ∪ m^-1"
      apply (subst (asm) converse_iff[THEN sym])
      using cbi_esdovovisiffidi by blast
      with qc have False unfolding BEGIN_def 
      apply (subgoal_tac "(q, j) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯")
        prefer 2
        apply simp 
          using neq_beta2i_alpha2alpha5m by auto
      }

     with c1' show "((i, j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯)"   by auto  
   next
      assume "(i, j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯"
      then show "BEGIN i ≪ BEGIN j"
      proof  ( simp_all,elim disjE, simp_all)
        assume "(i,j) ∈ b" thus ?thesis using intv1  using before_def NEST_BEGIN assms by metis
        next
        assume iu:"(i,j) ∈ m" 
        obtain l where li:"(l,i) ∈ m" using M3 m meets_wd assms by blast
        with iu have "(l,j) ∈ b" using cmm by auto
        moreover from li  have "l ∈ (BEGIN i)" using BEGIN_def by auto
        ultimately show ?thesis using intv1  before_def NEST_BEGIN assms by blast
        next
        assume iu:"(i,j) ∈ ov"
        obtain l where li:"(l,i) ∈ m" using M3 m meets_wd assms by blast
        with iu have "(l,j) ∈ b" using cmov by auto
        moreover from li have "l ∈ (BEGIN i)" using BEGIN_def by auto
        ultimately show ?thesis using intv1 before_def NEST_BEGIN assms by blast
        next
        assume iu:"(j,i) ∈ f" 
        obtain l where li:"(l,i) ∈ m" using M3 m meets_wd assms by blast
        with iu have "(l,j) ∈ b" using cmfi by auto
        moreover from li have "l ∈ (BEGIN i)" using BEGIN_def by auto
        ultimately show ?thesis using intv1  before_def NEST_BEGIN assms by blast
        next
        assume iu:"(j,i) ∈ d" 
        obtain l where li:"(l,i) ∈ m" using M3 m meets_wd assms by blast
        with iu have "(l,j) ∈ b" using cmdi by auto
        moreover from li have "l ∈ (BEGIN i)" using BEGIN_def by auto
        ultimately show ?thesis using intv1 before_def NEST_BEGIN assms by blast
        
     qed
qed

lemma BEGIN_END_before:
fixes i j
assumes "ℐ i" and "ℐ j"
shows  "BEGIN i ≪ END j = ((i,j) ∈ e ∪ b ∪ m ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ f ∪ f¯ ∪ d ∪ d¯) "
proof 
     assume a3:"BEGIN i ≪ END j"
     then obtain p q where pa:"p ∈ BEGIN i" and qc:"q ∈ END j" and pq:"(p,q) ∈ b" unfolding before_def by auto
     then obtain r where "p∥r" and "r∥q" using b by auto
     then have pr:"(p,r) ∈ m" and rq:"(r,q) ∈ m" using m by auto
     from pa  have pi:"(p,i) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
     moreover with pr have "(r,p) ∈ m^-1" by simp
     ultimately have "(r,i) ∈ d ∪ f ∪ ov^-1 ∪ e ∪ f^-1 ∪ m^-1 ∪ b^-1 ∪ s ∪ s^-1" using cmiov cmis cmim cmifi cmidi e cmisi
     by ( simp_all,elim disjE, auto simp:e)
     
     then have ir:"(i,r) ∈ d^-1 ∪ f^-1 ∪ ov ∪ e ∪ f ∪ m ∪ b ∪ s^-1 ∪ s" 
     by (metis (mono_tags, lifting) converseD converse_Un converse_converse eei)

     from qc  have "(q,j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
     with rq have rj:"(r,j) ∈ m ∪ ov ∪ s ∪ d ∪ b ∪ f^-1 ∪ f ∪ e" using cm_alpha1ialpha4mi by blast

     with ir show  c1:"(i,j) ∈ e ∪ b ∪ m ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ f ∪ f¯ ∪ d ∪ d¯"
     using difimov by blast
     next
     assume a4:"(i, j) ∈ e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯"
     then show "BEGIN i ≪ END j"
     proof  ( simp_all,elim disjE, simp_all)
           assume "(i,j) ∈ e" 
           obtain l k where l:"l∥i" and "i∥k" using M3 meets_wd assms  by blast
           with ‹(i,j) ∈ e› have k:"j∥k" by (simp add: e)
           from l k have "(l,i) ∈ m" and "(k,j) ∈ m^-1" using m by auto
           then  have "l ∈ BEGIN i" and "k ∈ END j" using BEGIN_def END_def by auto 
           moreover from l ‹i∥k› have "(l,k) ∈ b" using b by auto
           ultimately show ?thesis using before_def assms NEST_BEGIN NEST_END  by blast
          next
           assume "(i,j) ∈ b"
           then show ?thesis using before_def assms NEST_BEGIN NEST_END intv1[of i] intv2[of j] by auto
          next
            assume "(i,j) ∈ m"
            obtain l where "l∥i" using M3 assms by blast
            then have "l∈BEGIN i" using m BEGIN_def by auto
            moreover from ‹(i,j)∈m› ‹l∥i› have "(l,j) ∈ b" using b m by blast
            ultimately show ?thesis using intv2[of j] assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(i,j) ∈ ov"
           then obtain l k where li:"l∥i" and lk:"l∥k" and ku:"k∥j" using ov by blast
           from li have "l ∈ BEGIN i" using m BEGIN_def by auto
           moreover from lk ku have "(l,j) ∈ b" using b by auto
           ultimately show ?thesis using intv2[of j] assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(j,i) ∈ ov"
           then obtain l k v where uv:"j∥v" and lk:"l∥k" and kv:"k∥v" and li:"l∥i" using ov by blast
           from li have "l ∈ BEGIN i" using m BEGIN_def by auto
           moreover from uv have "v ∈ END j" using m END_def by auto
           moreover from lk kv have "(l,v) ∈ b" using b by auto
           ultimately show ?thesis using  assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(i,j) ∈ s"
           then obtain v v' where iv:"i∥v" and vvp:"v∥v'" and "j∥v'" using s by blast
           then have "v' ∈ END j" using END_def m by auto
           moreover from iv vvp have "(i,v') ∈ b" using b by auto
           ultimately show ?thesis using intv1[of i]  assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(j,i) ∈ s"
           then obtain l v where li:"l∥i" and lu:"l∥j" and "j∥v" using s by blast
           then have "v ∈ END j" using m END_def by auto
           moreover from li have "l ∈ BEGIN i" using m BEGIN_def by auto
           moreover from lu ‹j∥v› have "(l,v) ∈ b" using b by auto
           ultimately show ?thesis using  assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(i,j) : f"
           then obtain l v where li:"l∥i" and iv:"i∥v" and "j∥v" using f by blast
           then have "v ∈ END j" using m END_def by auto
           moreover from li have "l ∈ BEGIN i" using m BEGIN_def by auto
           moreover from iv li have "(l,v) ∈ b" using b by auto
           ultimately show ?thesis using assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(j,i) ∈ f"
           then obtain l v where li:"l∥i" and iv:"i∥v" and "j∥v" using f by blast
           then have "v ∈ END j" using m END_def by auto
           moreover from li have "l ∈ BEGIN i" using m BEGIN_def by auto
           moreover from iv li have "(l,v) ∈ b" using b by auto
           ultimately show ?thesis using  assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(i,j) : d"
           then obtain k v where ik:"i∥k" and kv:"k∥v" and "j∥v" using d by blast
           then have "v ∈ END j" using END_def m by auto
           moreover from ik kv have "(i,v) ∈ b" using b by auto
           ultimately show ?thesis using intv1[of i]  assms NEST_BEGIN NEST_END before_def by blast
          next
           assume "(j,i) ∈ d"
           then obtain l k where "l∥i" and lk:"l∥k" and ku:"k∥j" using d by blast
           then have "l ∈ BEGIN i" using BEGIN_def m by auto
           moreover from lk ku have "(l,j) ∈ b" using b by auto
           ultimately show ?thesis using intv2[of j] assms NEST_BEGIN NEST_END before_def by blast
       qed           
qed

lemma END_BEGIN_before:
fixes i j
assumes "ℐ i" and "ℐ j"
shows  "END i ≪ BEGIN j =  ((i,j) ∈ b) "
proof 
     assume a3:"END i ≪ BEGIN j"
     from a3 obtain p q where pa:"p ∈ END i" and qc:"q ∈ BEGIN j" and pq:"(p,q) ∈ b" unfolding before_def by auto
     then obtain r where "p∥r" and "r∥q" using b by auto
     then have pr:"(p,r) ∈ m" and rq:"(r,q) ∈ m" using m by auto
     from pa  have pi:"(p,i) ∈  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
     moreover with pr have "(r,p) ∈ m^-1" by simp
     ultimately have "(r,i) ∈ m^-1 ∪ b^-1" using e cmiovi cmisi cmidi cmif cmifi cmimi 
     by ( simp_all,elim disjE, auto simp:e)
     
     then have ir:"(i,r) ∈ m ∪ b" by simp
     
     from qc  have "(q,j) ∈  ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" unfolding BEGIN_def by auto
     with rq have rj:"(r,j) ∈ b ∪ m " using cmov cms cmm cmfi cmdi e cmsi
     by (simp_all, elim disjE, auto simp:e)
     
     with ir show "(i,j) ∈ b" using cmb cmm cbm cbb by auto

   next
     assume "(i,j) ∈ b" thus "END i ≪ BEGIN j" using intv1[of j] intv2[of i] assms before_def NEST_END NEST_BEGIN by auto
qed

lemma END_END_before:
fixes i j
assumes "ℐ i" and "ℐ j"
shows "END i ≪ END j = ((i,j) ∈ b ∪ m ∪ ov ∪ s ∪ d) "
proof 
     assume a3:"END i ≪ END j"
     from a3 obtain p q where pa:"p ∈ END i" and qc:"q ∈ END j" and pq:"(p,q) ∈ b" unfolding before_def by auto
     then obtain r where "p∥r" and "r∥q" using b by auto
     then have pr:"(p,r) ∈ m" and rq:"(r,q) ∈ m" using m by auto
     from pa  have pi:"(p,i) ∈  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
     moreover with pr have "(r,p) ∈ m^-1" by simp
     ultimately have "(r,i) ∈ m^-1 ∪ b^-1" using e cmiovi cmisi cmidi cmif cmifi cmimi 
     by ( simp_all,elim disjE, auto simp:e)
     
     then have ir:"(i,r) ∈ m ∪ b" by simp
     
     from qc  have "(q,j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯" unfolding END_def by auto
     with rq have rj:"(r,j) ∈ m ∪ ov ∪ s ∪ d ∪ b ∪ f^-1 ∪ e ∪ f " using e cmovi cmsi cmdi cmf cmfi cmmi
     by (simp_all, elim disjE, auto simp:e)
     
     with ir show "(i,j) ∈ b ∪ m ∪ ov ∪ s ∪ d" using cmm cmov cms cmd cmb cmfi e cmf cbm cbov cbs cbd cbb cbfi cbf
     by (simp_all, elim disjE, auto simp:e)
    next
     assume "(i, j) ∈ b ∪ m ∪ ov ∪ s ∪ d"
     then show "END i ≪ END j"
     proof  ( simp_all,elim disjE, simp_all)
        assume "(i,j) ∈ b" thus ?thesis using intv2[of i] intv2[of j] assms NEST_END before_def by blast
       next
        assume "(i,j) ∈ m" 
        obtain v where "j∥v" using M3 assms by blast
        with ‹(i,j) ∈ m› have "(i,v) ∈b" using b m by blast
        moreover from ‹j∥v› have "v ∈ END j" using m END_def by auto
        ultimately show ?thesis using intv2[of i] assms NEST_END before_def by blast
       next
        assume "(i,j) : ov"
        then obtain v v' where iv:"i∥v" and vvp:"v∥v'" and "j∥v'" using ov by blast
        then have "v' ∈ END j" using m END_def by auto
        moreover from iv vvp have "(i,v') ∈ b" using b by auto
        ultimately show ?thesis using intv2[of i] assms NEST_END before_def by blast
       next
        assume "(i,j) ∈ s"
        then obtain v v' where iv:"i∥v" and vvp:"v∥v'" and "j∥v'" using s by blast
        then have "v' ∈ END j" using m END_def by auto
        moreover from iv vvp have "(i,v') ∈ b" using b by auto
        ultimately show ?thesis using intv2[of i] assms NEST_END before_def by blast
       next
        assume "(i,j) ∈ d"
        then obtain v v' where iv:"i∥v" and vvp:"v∥v'" and "j∥v'" using d by blast
        then have "v' ∈ END j" using m END_def by auto
        moreover from iv vvp have "(i,v') ∈ b" using b by auto
        ultimately show ?thesis using intv2[of i] assms NEST_END before_def by blast
       qed 
qed

lemma overlaps:
assumes "ℐ i" and "ℐ j"
shows "(i,j) ∈ ov = ((BEGIN i ≪ BEGIN j) ∧ (BEGIN j ≪ END i) ∧ (END i ≪ END j))"
proof 

    assume a:"(i,j) ∈ ov"
    then obtain n t q  u v where nt:"n∥t" and tj:"t∥j" and tq:"t∥q" and qu:"q∥u" and  iu:"i∥u" and uv:"u∥v" and jv:"j∥v" and "n∥i" using ov by blast
    then have ni:"(n,i) ∈ m"  using  m  by blast
    then have  n:"n ∈ BEGIN i" unfolding BEGIN_def by auto
    from nt tj have nj:"(n,j) ∈ b" using b by auto
    have  "j ∈ BEGIN j" using assms(2) by (simp add: intv1)
    with assms n nj  have c1:"BEGIN i ≪ BEGIN j" unfolding before_def using NEST_BEGIN by blast
  
    from tj have a1:"(t,j) ∈ m" and a2:"t ∈ BEGIN j" using m BEGIN_def by auto
    from iu have "(u,i) ∈ m^-1" and "u ∈ END i" using m END_def by auto
    with assms  tq qu a2 have c2:"BEGIN j ≪ END i"  unfolding before_def using b  NEST_BEGIN NEST_END by blast

    have "i ∈ END i" by (simp add: assms  intv2) 
    moreover with jv  have "v ∈ END j" using m END_def by auto
    moreover with iu uv have "(i,v) ∈ b" using b by auto
    ultimately have c3:"END i ≪ END j" using assms NEST_END before_def by blast

    show "((BEGIN i ≪ BEGIN j) ∧ (BEGIN j ≪ END i) ∧ (END i ≪ END j))" using c1 c2 c3 by simp     
  next
    assume a0:"((BEGIN i ≪ BEGIN j) ∧ (BEGIN j ≪ END i) ∧ (END i ≪ END j))"
    then have "(i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯ ∧ (i,j) ∈ e ∪ b^-1 ∪ m^-1 ∪ ov^-1 ∪ ov ∪ s^-1 ∪ s ∪ f^-1 ∪ f ∪ d^-1 ∪ d
                                                                                                              ∧ (i,j) ∈ b ∪ m ∪ ov ∪ s ∪ d"
    using BEGIN_before BEGIN_END_before END_END_before assms 
    by (metis (no_types, lifting) converseD converse_Un converse_converse eei)
    then have "(i,j) ∈  (b ∪ m ∪ ov ∪ f¯ ∪ d¯) ∩ (e ∪ b^-1 ∪ m^-1 ∪ ov^-1 ∪ ov ∪ s^-1 ∪ s ∪ f^-1 ∪ f ∪ d^-1 ∪ d) ∩ (b ∪ m ∪ ov ∪ s ∪ d)" 
    by (auto)
    then show "(i,j) ∈ ov"
    using inter_ov by blast

qed

subsection ‹Ordering of nests›

class  strict_order =
fixes ls::"'a nest ⇒ 'a nest ⇒ bool"
assumes 
  irrefl:"¬ ls a a" and
  trans:"ls a c ⟹ ls c g ⟹ ls a g" and 
  asym:"ls a c ⟹ ¬ ls c a"  

class total_strict_order = strict_order +
assumes trichotomy: "a = c ⟹ (¬ (ls a  c) ∧ ¬ (ls c  a))"

interpretation nest:total_strict_order "(≪) "
proof
{ fix a::"'a nest"
show "¬ a ≪ a"
by (simp add: before_irrefl) } note  irrefl_nest = this

{fix a c::"'a nest"
assume  "a = c"
show "¬ a ≪ c ∧ ¬ c ≪ a" 
by (simp add: ‹a = c› irrefl_nest)} note trichotomy_nest = this

{fix a c g::"'a nest"
assume a:"a ≪ c" and c:" c ≪ g"
show " a ≪ g" 
proof -
   from a c have na:"NEST a"  and nc:"NEST c" and ng:"NEST g" unfolding before_def by auto
   from na obtain i where  i:"a = BEGIN i ∨ a = END i" and wdi:"ℐ i" unfolding NEST_def by auto
   from nc obtain j where  j:"c = BEGIN j ∨ c = END j" and wdj:"ℐ j" unfolding NEST_def by auto
   from ng obtain u where  u:"g = BEGIN u ∨ g = END u" and wdu:"ℐ u" unfolding NEST_def by auto
   from i j u show ?thesis
   proof (elim disjE, auto)
     assume abi:"a = BEGIN i" and  cbj:"c = BEGIN j" and  gbu:"g = BEGIN u"
     from abi cbj a wdi wdj have "(i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯ " using BEGIN_before by auto
     moreover from cbj gbu c wdj wdu have "(j,u) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯" using BEGIN_before by auto

     ultimately have c1:"(i,u) ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
     using cbeta2_beta2 by blast
      
     then have "a ≪ g" by (simp add: BEGIN_before abi gbu wdi wdu)
    
     thus "BEGIN i ≪ BEGIN u" using abi gbu by auto
    next
     assume  abi:"a = BEGIN i" and  cbj:"c = BEGIN j" and  geu:"g = END u" 
     from abi cbj a wdi wdj have "(i,j) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯ " using BEGIN_before by auto
     moreover from cbj geu c wdj wdu have "(j,u) :  e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯" using BEGIN_END_before by auto
     ultimately have "(i,u) ∈ e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯"
     using cbeta2_gammabm by blast
          
     then have "a ≪ g" 
     by (simp add: BEGIN_END_before abi geu wdi wdj wdu)
       
     thus "BEGIN i ≪ END u" using abi geu by auto
    next
     assume abi:"a = BEGIN i" and  cej:"c = END j" and  gbu:"g = BEGIN u"
     from abi cej a wdi wdj  have ij:"(i,j) :  e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯" using BEGIN_END_before by auto
     from cej gbu c wdj wdu  have "(j,u) ∈ b " using END_BEGIN_before by auto
     with ij have "(i,u) ∈ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1" 
     using ebmovovissifsiddib by ( auto)

     thus "BEGIN i ≪ BEGIN u"
     by (simp add: BEGIN_before abi gbu wdi wdu)
    next
     assume abi:"a = BEGIN i" and  cej:"c = END j" and  geu:"g = END u"
     with a  have "(i,j) ∈  e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯"
     using BEGIN_END_before wdi wdj by auto
     moreover from cej geu c wdj wdu  have "(j,u) ∈ b ∪ m ∪ ov ∪ s ∪ d"
     using END_END_before by auto
     ultimately have "(i,u) ∈ b ∪ m ∪ ov ∪ s ∪ d ∪ f^-1 ∪ d^-1 ∪ ov^-1 ∪ s¯ ∪ f ∪ e"
     using ebmovovissiffiddibmovsd by blast
                  
     thus "BEGIN i ≪ END u" using BEGIN_END_before wdi wdu  by auto
    next
     assume aei:"a = END i" and cbj:"c = BEGIN j" and gbu:"g = BEGIN u"
     from a  aei cbj wdi wdj have "(i,j) ∈ b"
     using END_BEGIN_before by auto
     moreover from c  cbj gbu wdj wdu have "(j,u) ∈ b ∪ m ∪ ov ∪ f¯ ∪ d¯" 
     using BEGIN_before by auto 
     ultimately have "(i,u) : b" using cbb cbm cbov cbfi cbdi 
     by (simp_all, elim disjE, auto)
     thus "END i ≪ BEGIN u" using END_BEGIN_before wdi wdu  by auto
    next
     assume  aei:"a = END i" and cbj:"c = BEGIN j" and  geu:"g = END u"
     from a  aei cbj wdi wdj have "(i,j) ∈ b"
     using END_BEGIN_before by auto
     moreover from c  cbj geu wdj wdu have "(j,u) ∈ e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯" 
     using BEGIN_END_before by auto 
     ultimately have "(i,u) ∈ b ∪ m ∪ ov ∪ s ∪ d"
     using bebmovovissiffiddi by blast
     thus "END i ≪ END u" using END_END_before wdi wdu by auto
    next
     assume aei:"a = END i" and cej:"c = END j" and  gbu:"g = BEGIN u" 
     from aei cej wdi wdj have "(i,j) ∈ b ∪ m ∪ ov ∪ s ∪ d" using END_END_before a by auto
     moreover from cej gbu c wdj wdu have "(j,u) ∈ b" using END_BEGIN_before by auto
     ultimately have "(i,u) ∈ b"
     using cbb cmb covb csb cdb
     by (simp_all, elim disjE, auto)
     thus "END i ≪ BEGIN u" using END_BEGIN_before wdi wdu  by auto
    next
     assume aei:"a = END i" and cej:"c = END j" and geu:"g = END u"
     from aei cej wdi wdj  have "(i,j) ∈ b ∪ m ∪ ov ∪ s ∪ d" using  END_END_before a by auto
     moreover from cej geu c wdj wdu have "(j,u) ∈  b ∪ m ∪ ov ∪ s ∪ d" using END_END_before by auto
     ultimately have "(i,u) ∈ b ∪ m ∪ ov ∪ s ∪ d" 
     using calpha1_alpha1 by auto
     thus "END i ≪ END u" using END_END_before wdi wdu by auto
   qed
qed} note trans_nest = this    

{ fix a c::"'a nest"
  assume a:"a ≪ c"
  show "¬ c ≪ a"
  apply (rule ccontr, auto)
  using a  irrefl_nest trans_nest by blast}
qed  
         
end